src/CCL/ex/Nat.thy

--- a/src/CCL/ex/Nat.thy	Mon Jul 17 18:42:38 2006 +0200
+++ b/src/CCL/ex/Nat.thy	Tue Jul 18 02:22:38 2006 +0200
@@ -40,7 +40,65 @@
                           ncase(m,ack(x,succ(zero)),%y. ack(x,ack(succ(x),y))))
                     in ack(a,b)"
 
-ML {* use_legacy_bindings (the_context ()) *}
+lemmas nat_defs = not_def add_def mult_def sub_def le_def lt_def ack_def napply_def
+
+lemma natBs [simp]:
+  "not(true) = false"
+  "not(false) = true"
+  "zero #+ n = n"
+  "succ(n) #+ m = succ(n #+ m)"
+  "zero #* n = zero"
+  "succ(n) #* m = m #+ (n #* m)"
+  "f^zero`a = a"
+  "f^succ(n)`a = f(f^n`a)"
+  by (simp_all add: nat_defs)
+
+
+lemma napply_f: "n:Nat ==> f^n`f(a) = f^succ(n)`a"
+  apply (erule Nat_ind)
+   apply simp_all
+  done
+
+lemma addT: "[| a:Nat;  b:Nat |] ==> a #+ b : Nat"
+  apply (unfold add_def)
+  apply (tactic {* typechk_tac [] 1 *})
+  done
+
+lemma multT: "[| a:Nat;  b:Nat |] ==> a #* b : Nat"
+  apply (unfold add_def mult_def)
+  apply (tactic {* typechk_tac [] 1 *})
+  done
+
+(* Defined to return zero if a<b *)
+lemma subT: "[| a:Nat;  b:Nat |] ==> a #- b : Nat"
+  apply (unfold sub_def)
+  apply (tactic {* typechk_tac [] 1 *})
+  apply (tactic clean_ccs_tac)
+  apply (erule NatPRI [THEN wfstI, THEN NatPR_wf [THEN wmap_wf, THEN wfI]])
+  done
+
+lemma leT: "[| a:Nat;  b:Nat |] ==> a #<= b : Bool"
+  apply (unfold le_def)
+  apply (tactic {* typechk_tac [] 1 *})
+  apply (tactic clean_ccs_tac)
+  apply (erule NatPRI [THEN wfstI, THEN NatPR_wf [THEN wmap_wf, THEN wfI]])
+  done
+
+lemma ltT: "[| a:Nat;  b:Nat |] ==> a #< b : Bool"
+  apply (unfold not_def lt_def)
+  apply (tactic {* typechk_tac [thm "leT"] 1 *})
+  done
+
+
+subsection {* Termination Conditions for Ackermann's Function *}
+
+lemmas relI = NatPR_wf [THEN NatPR_wf [THEN lex_wf, THEN wfI]]
+
+lemma "[| a:Nat;  b:Nat |] ==> ackermann(a,b) : Nat"
+  apply (unfold ack_def)
+  apply (tactic "gen_ccs_tac [] 1")
+  apply (erule NatPRI [THEN lexI1 [THEN relI]] NatPRI [THEN lexI2 [THEN relI]])+
+  done
 
 end