type_synonym string ="char list"
datatype 'a tree = Tip | Node "'a tree" 'a "'a tree"
fun mirror :: " 'a tree ⇒ 'a tree" where
"mirror Tip = Tip"|" mirror (Node l a r) = Node mirror r a mirror l"
datatype 'a option =None|Some 'a
fun lookup::"('a * 'b) list => 'a=>'b option" where
"lookup [] x = None"|"lookup ((a,b)#ps) x = (if a =x then Some b else lookup ps x)"
a * b is the type of pairs <==> a 乘 b
Non-recursive
difinition sq::"nat=>nat"where
"sq n = n * n"
abbreviation sq'::"nat =>nat" where
"sq' n==n*n"
fun div2::"nat =>nat" where
"div2 0 = 0"|"div2(Suc 0) = 0"|"div2(Suc(Suc n)) = Suc(div2 n)"
lemma "div2(n) = n div 2"
apply(induction n rule:div2.induct)
对n归纳 规则是div2的定义
f::"A1=>A2...An=>A"
apply(induction x1...xn rule:f.induct)