src/CCL/ex/Nat.thy
changeset 27221 31328dc30196
parent 24825 c4f13ab78f9d
child 35762 af3ff2ba4c54
equal deleted inserted replaced
27220:31adee1f467a 27221:31328dc30196
    59    apply simp_all
    59    apply simp_all
    60   done
    60   done
    61 
    61 
    62 lemma addT: "[| a:Nat;  b:Nat |] ==> a #+ b : Nat"
    62 lemma addT: "[| a:Nat;  b:Nat |] ==> a #+ b : Nat"
    63   apply (unfold add_def)
    63   apply (unfold add_def)
    64   apply (tactic {* typechk_tac [] 1 *})
    64   apply (tactic {* typechk_tac @{context} [] 1 *})
    65   done
    65   done
    66 
    66 
    67 lemma multT: "[| a:Nat;  b:Nat |] ==> a #* b : Nat"
    67 lemma multT: "[| a:Nat;  b:Nat |] ==> a #* b : Nat"
    68   apply (unfold add_def mult_def)
    68   apply (unfold add_def mult_def)
    69   apply (tactic {* typechk_tac [] 1 *})
    69   apply (tactic {* typechk_tac @{context} [] 1 *})
    70   done
    70   done
    71 
    71 
    72 (* Defined to return zero if a<b *)
    72 (* Defined to return zero if a<b *)
    73 lemma subT: "[| a:Nat;  b:Nat |] ==> a #- b : Nat"
    73 lemma subT: "[| a:Nat;  b:Nat |] ==> a #- b : Nat"
    74   apply (unfold sub_def)
    74   apply (unfold sub_def)
    75   apply (tactic {* typechk_tac [] 1 *})
    75   apply (tactic {* typechk_tac @{context} [] 1 *})
    76   apply (tactic clean_ccs_tac)
    76   apply (tactic {* clean_ccs_tac @{context} *})
    77   apply (erule NatPRI [THEN wfstI, THEN NatPR_wf [THEN wmap_wf, THEN wfI]])
    77   apply (erule NatPRI [THEN wfstI, THEN NatPR_wf [THEN wmap_wf, THEN wfI]])
    78   done
    78   done
    79 
    79 
    80 lemma leT: "[| a:Nat;  b:Nat |] ==> a #<= b : Bool"
    80 lemma leT: "[| a:Nat;  b:Nat |] ==> a #<= b : Bool"
    81   apply (unfold le_def)
    81   apply (unfold le_def)
    82   apply (tactic {* typechk_tac [] 1 *})
    82   apply (tactic {* typechk_tac @{context} [] 1 *})
    83   apply (tactic clean_ccs_tac)
    83   apply (tactic {* clean_ccs_tac @{context} *})
    84   apply (erule NatPRI [THEN wfstI, THEN NatPR_wf [THEN wmap_wf, THEN wfI]])
    84   apply (erule NatPRI [THEN wfstI, THEN NatPR_wf [THEN wmap_wf, THEN wfI]])
    85   done
    85   done
    86 
    86 
    87 lemma ltT: "[| a:Nat;  b:Nat |] ==> a #< b : Bool"
    87 lemma ltT: "[| a:Nat;  b:Nat |] ==> a #< b : Bool"
    88   apply (unfold not_def lt_def)
    88   apply (unfold not_def lt_def)
    89   apply (tactic {* typechk_tac [thm "leT"] 1 *})
    89   apply (tactic {* typechk_tac @{context} @{thms leT} 1 *})
    90   done
    90   done
    91 
    91 
    92 
    92 
    93 subsection {* Termination Conditions for Ackermann's Function *}
    93 subsection {* Termination Conditions for Ackermann's Function *}
    94 
    94 
    95 lemmas relI = NatPR_wf [THEN NatPR_wf [THEN lex_wf, THEN wfI]]
    95 lemmas relI = NatPR_wf [THEN NatPR_wf [THEN lex_wf, THEN wfI]]
    96 
    96 
    97 lemma "[| a:Nat;  b:Nat |] ==> ackermann(a,b) : Nat"
    97 lemma "[| a:Nat;  b:Nat |] ==> ackermann(a,b) : Nat"
    98   apply (unfold ack_def)
    98   apply (unfold ack_def)
    99   apply (tactic "gen_ccs_tac [] 1")
    99   apply (tactic {* gen_ccs_tac @{context} [] 1 *})
   100   apply (erule NatPRI [THEN lexI1 [THEN relI]] NatPRI [THEN lexI2 [THEN relI]])+
   100   apply (erule NatPRI [THEN lexI1 [THEN relI]] NatPRI [THEN lexI2 [THEN relI]])+
   101   done
   101   done
   102 
   102 
   103 end
   103 end
   104