Differences

This shows you the differences between two versions of the page.

--- faq [2012/04/16 22:38] – [PURE vs. HOL] 95.89.150.111
+++ faq [2013/03/01 10:12] (current) – [FAQ - Ask Questions] 124.207.188.66
@@ Line 8: / Line 8: @@
 Also, check out the [[http://www.cl.cam.ac.uk/research/hvg/isabelle/faq.html|official FAQ]] of Isabelle/HOL.
+Dear all proof lovers:
+I am really new to Isabelle. Recently I hope to learn HOL and try to use automatic therom prover. So I download the Isabelle2013. Now I hope to use Isabelle/jEdit in Windows OS(so I cannot use proof general) for therom proving. However, what make me confused is, what is the difference between Isabelle/HOL and Isabelle/Isar? And what syntax should I learn, Isabelle/Isar syntax or Isabelle/HOL syntax? Please tell me the specific tutorial I should learn.
+Here, I am learning the simple example, which is in appendix. Am I right?
+Thanks very much.
+Appendix:
+header {* Finite sequences *}
+theory Seq
+imports Main
+begin
+datatype 'a seq = Empty | Seq 'a "'a seq"
+fun conc :: "'a seq \<Rightarrow> 'a seq \<Rightarrow> 'a seq"
+where
+  "conc Empty ys = ys"
+| "conc (Seq x xs) ys = Seq x (conc xs ys)"
+fun reverse :: "'a seq \<Rightarrow> 'a seq"
+where
+  "reverse Empty = Empty"
+| "reverse (Seq x xs) = conc (reverse xs) (Seq x Empty)"
+lemma conc_empty: "conc xs Empty = xs"
+  by (induct xs) simp_all
+lemma conc_assoc: "conc (conc xs ys) zs = conc xs (conc ys zs)"
+  by (induct xs) simp_all
+lemma reverse_conc: "reverse (conc xs ys) = conc (reverse ys) (reverse xs)"
+  by (induct xs) (simp_all add: conc_empty conc_assoc)
+lemma reverse_reverse: "reverse (reverse xs) = xs"
+  by (induct xs) (simp_all add: reverse_conc)
+end
 ===== Syntax =====