Differences

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

--- faq [2011/07/20 12:10] – [Axioms of HOL in Isabelle] 131.246.161.187
+++ faq [2013/03/01 10:12] (current) – [FAQ - Ask Questions] 124.207.188.66
@@ Line 7: / Line 7: @@
 It would also help us and the other students a lot, if you could post any questions **you had** here, even just syntactical problems! Everything which held you up for more than 10 minutes is already worth mentioning here.
-Also, check out the [[http://www.cl.cam.ac.uk/research/hvg/isabelle/faq.html|official FAQ]].
+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 66: / Line 106: @@
 </code>
+==== Computing functions ====
+:?: How does Isabelle actually "compute" the value of a function application? For example in
+<code>
+value "1::nat + 1"
+</code>
+Is it simply applying simplification (i.e. term rewriting) until the normalized term "2" is reached?
+:!: Yes, Isabelle does not have any notion of operational semantics or the like, but just uses simplification, i.e. equalities. The defining equalities of functions can be used for simplification, as soon as termination is shown. In this case the definition of the relevant function is: <code>
+primrec plus_nat
+where
+  add_0:      "0 + n = (n::nat)"
+  | add_Suc:  "Suc m + n = Suc (m + n)"
+</code>
+So the term ''Suc 0 + Suc 0'' gets reduced to ''Suc (0 + Suc 0)'' by ''add_Suc'', which gets reduced to ''Suc (Suc 0)'' by ''add_0''.
+I am just claiming this, however, if you want to know that is really going on you can try //trace simplification// from the Isabelle menu ;-)
 ===== Theorem Proving =====
@@ Line 186: / 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 254: / Line 310: @@
 Note that this does not mean we necessarly can derive ''False'' now (this is an easy to check breach of this contract if ''T'' is consistent, though!) i.e. ''T''' is not necessarily inconsistent; if ''T'' is not //complete//, you might find proofs for actual theorems in ''T''' that could not be proven in ''T''. Conservative extensions assert that this can not happen.
+==== Non-conservative extensions ====
+:?: Is it possible to perform a non-conservative extension by only defining new types or constants (i.e. without touching the set A of axioms)?
+:!: Considering that all proofs are constructed out of axioms, nothing new can be proven, so no it shouldn't be possible. If you don't add axioms though, you are not actually "defining" anything, as you can just extend the signatures without any meaning or knowledge about the new symbols.
 ==== Empty Types ====
@@ Line 275: / Line 335: @@
 ==== Axioms of HOL in Isabelle ====
-:?:
+:?: About the axiom of infinity:
   - Does Isabelle/HOL have the axiom of infinity or not?
   - If it does, this means the deduction system is incomplete (because of standard models), right?
   - If it does not include the axiom, what are the implications of that? Do we still have a true HOL system?
-:!:
+:!: Answer:
-  - Yes, but not explicitly. The axioms of Isabelle/HOL postulate that there is an infinite type; the "axiom" of infinity is therefore a theorem in Isabelle/HOL.
+  - Yes, the ''Main'' theory of Isabelle/HOL contains ''axioms'' (or ''axiomatizations''), which represent the axioms of HOL. The axiom of infinity is found at the definition of the type ''ind'': <code>
-  - Yes, it is incomplete.
+typedecl ind
+axiomatization
+  Zero_Rep :: ind and
+  Suc_Rep :: "ind => ind"
+where
+  -- {* the axiom of infinity in 2 parts *}
+  Suc_Rep_inject:       "Suc_Rep x = Suc_Rep y ==> x = y" and
+  Suc_Rep_not_Zero_Rep: "Suc_Rep x ≠ Zero_Rep"
+</code> It is just stated there, that there exists an //injective// but //not surjective// function on this type, which //makes// the type infinite.
+  - Yes, it is probably incomplete, yet I dare you to find some theorem which holds but you can't prove it in Isabelle/HOL ;-).
   - 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).