Top Level Strutcure
|The top level is a theory structure. The name of the theory must match the file name.||
|This is the program-like. Similar to data and functions on that data.|
The keyword 'primrec' is used for a certain type of 'primative recursion' where each recursive call peels off a datatype constructor from one of the arguments.
- 'a = type variable
Eamples of 'datatype'
- datatype bool = True | False
- datatype nat = 0 | Suc nat
- datatype 'a list = Nil | Cons 'a " 'a list"
fun defines a function by pattern matching over datatype constructors.
Examples of 'fun'
- fun conj :: "bool => bool => bool" where
"conj True True = True" |
"conj _ _ = False"
- fun add :: "nat => nat => nat" where
"add 0 n = n" |
"add (Suc m) n = Suc (add m n)"
A definiton defines a non-recursive function without any pattern matching
Examples of 'definiton'
- definition sq :: "nat => nat" where
"sq n = n n"
Abbreviations have the same form as definitons but are only synthetic sugar.
Theorems, Lemmas and Rules
|Theorems, Lemmas and Rules are the same to the program. The difference is only intended to express the importance.|
|We cannot prove all possible theorems but there are varying levels of search that we can use:||
- done tells Isabelle to associate the lemma just proved with its name
- thm name - displays the theorem
Examples of Proofs
- lemma add_02: "add m 0 =m"
apply (induction m)
The results show the proof state. The numbered lines are known as subgoals.
The prefix Vm: is Isabelle’s way of saying "for an arbitrary but fixed m". Universal quantifier at the meta level
The ==> separates assumptions from the conclusion.
Universal quantifier at the meta level
Used to denote parameters
F=another meta-level formula
|A ==> B||
A ==> B ==> C
A and B implies C
A,B=other meta-level formula
%x . F
|This example creates a list structure||
|This example proves theorems about 'or'||
proof ::= 'proof' method statement* 'qed' | 'by' method statement ::= 'fix' variable+ | 'assume' proposition+ | ('from' fact+)? 'have' proposition+ proof | ('from' fact+)? 'show' proposition+ proof proposition ::= (label':')? string fact ::= label method ::= '-' | 'this' | 'rule' fact | 'simp' | 'blast' | 'auto' | 'induct' variable | ...
- show statement establishes the conclusion of the proof
- have statement is for establishing intermediate results
- 'this' refers to the fact proved by the previous statement.
- 'then' = 'from this'
- 'hence' = 'then have'
- 'thus' = 'then show'
- 'with' fact+ = 'from' fact+ 'and' 'this'
- '.' = 'by this'
- '..' = 'by' rule where Isabelle guesses the rule