User Tools
faq
Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
faq [2012/04/13 15:28] paddy [FAQ - Ask Questions] |
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 ===== | ||
| 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? | + | |
faq.1334323724.txt.gz · Last modified: 2012/04/13 15:28 by paddy
Page Tools
