This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | |||
faq [2012/04/16 22:38] 95.89.150.111 [PURE vs. HOL] |
faq [2013/03/01 10:12] (current) 124.207.188.66 [FAQ - Ask Questions] |
||
---|---|---|---|
Line 8: | Line 8: | ||
Also, check out the [[http://www.cl.cam.ac.uk/research/hvg/isabelle/faq.html|official FAQ]] of Isabelle/HOL. | 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 ===== | ===== Syntax ===== | ||