# Isabelle Language

### Top Level Strutcure

The top level is a theory structure. The name of the theory must match the file name.
 ```theory fileName imports Main Datatype begin``` definitions theorems and proofs `end`

### Definitions

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.

#### Notation

• 'a = type variable

#### Eamples of 'datatype'

• datatype bool = True | False
• datatype nat = 0 | Suc nat
• datatype 'a list = Nil | Cons 'a " 'a list"

#### fun

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" |

#### definiton

A definiton defines a non-recursive function without any pattern matching

#### Examples of 'definiton'

• definition sq :: "nat => nat" where
"sq n = n n"

#### Abbreviations

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.

### Proofs

We cannot prove all possible theorems but there are varying levels of search that we can use:
 ```apply(auto) apply(simp name: theory1 theory2) apply(force apply(fastforce apply(blast sledgehammer try```
• done tells Isabelle to associate the lemma just proved with its name
• thm name - displays the theorem

#### Examples of Proofs

apply (induction m)
apply(auto)
done

#### Results

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.

### Meta Level

 /\ !!x. F 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 Lambda abstraction binds variables =

## Examples

This example creates a list structure
 ```theory Mylist imports Datatype begin datatype 'a list = Nil ("[]") | Cons 'a "'a list" (infixr "#" 65) (* this is the append function: *) primrec app :: "'a list => 'a list =>'a list" (infixr "@" 65) where "[] @ ys = ys" | "(x # xs) @ ys = x # (xs @ ys)" primrec rev :: "'a list => 'a list" where "rev [] = []" | "rev (x # xs) = (rev xs) @ (x # [])" value "rev (True # False # [])" value "rev (c # b # a # [])" theorem rev_rev [simp]: "rev (rev xs) = xs" apply (induct_tac xs) end```
This example proves theorems about 'or'
 ```theory Test1 imports Main begin theorem A: "A \ A \ B" apply (rule impI) apply (auto) done theorem B: "A \ B --> B \ A" (*apply (rule impI)*) apply (rule disjE) apply (rule disjI2) apply (auto) (*apply (rule disjI1) apply (auto) *) done end```

## Isar

 ```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

### shortcuts

• '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

 metadata block see also: Correspondence about this page Book Shop - Further reading. Where I can, I have put links to Amazon for books that are relevant to the subject, click on the appropriate country flag to get more details of the book or to buy it from them. Commercial Software Shop Where I can, I have put links to Amazon for commercial software, not directly related to this site, but related to the subject being discussed, click on the appropriate country flag to get more details of the software or to buy it from them.

This site may have errors. Don't use for critical systems.