This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
faq [2011/10/02 13:56] 77.11.139.237 [Programming Language Semantics] |
faq [2013/03/01 10:12] (current) 124.207.188.66 [FAQ - Ask Questions] |
||
---|---|---|---|
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. | 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 ===== | ===== Syntax ===== | ||
Line 202: | Line 242: | ||
:!: There are several levels to this question: | :!: 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. | - 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. | - 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). | - 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? | + |