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

Eamples of 'datatype'

fun

fun defines a function by pattern matching over datatype constructors.

Examples of 'fun'

definiton

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

Examples of 'definiton'

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

Examples of Proofs

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 \<longrightarrow> A \<or> B"
apply (rule impI)
apply (auto)
done

theorem B: "A \<or> B --> B \<or> 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 | ...

shortcuts


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.

Copyright (c) 1998-2017 Martin John Baker - All rights reserved - privacy policy.