Differences

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

--- faq [2012/04/13 15:28] – [FAQ - Ask Questions] paddy
+++ 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 =====
@@ Line 202: / Line 242: @@
 :!: There are several levels to this question:
-  - First, the latter is a by itself a HOL formula, while the former contains HOL formulas, but is more considered a rule.
+  - First, the latter is by itself a HOL formula, while the former contains HOL formulas, but is more considered a rule.
   - The former says that $G$ can be proven //syntactically// from the given assumptions $A_1, A_2, A_3$. The latter says that you can prove using no assumptions that whenever all $A_1, A_2, A_3$ hold, $G$ holds, too.
   - Maybe the main practical difference: the former is nicely applicable as a rule, where the latter is nearly useless.
@@ Line 315: / Line 355: @@
   - This case does not apply, but still: if we did not have the axiom of infinity, we would have a weaker HOL system, maybe, but still HOL (cf lecture).
-==== Programming Language Semantics ====
-:?: How can we define the semantics of HOL Syntax (Functional Application (T T) and lambda abstraction) using Operational & Denotational semantics?