src/CCL/ex/Nat.thy
changeset 58971 8c9a319821b3
parent 58889 5b7a9633cfa8
child 58974 cbc2ac19d783
equal deleted inserted replaced
58965:a62cdcc5344b 58971:8c9a319821b3
    65    apply simp_all
    65    apply simp_all
    66   done
    66   done
    67 
    67 
    68 lemma addT: "[| a:Nat;  b:Nat |] ==> a #+ b : Nat"
    68 lemma addT: "[| a:Nat;  b:Nat |] ==> a #+ b : Nat"
    69   apply (unfold add_def)
    69   apply (unfold add_def)
    70   apply (tactic {* typechk_tac @{context} [] 1 *})
    70   apply typechk
    71   done
    71   done
    72 
    72 
    73 lemma multT: "[| a:Nat;  b:Nat |] ==> a #* b : Nat"
    73 lemma multT: "[| a:Nat;  b:Nat |] ==> a #* b : Nat"
    74   apply (unfold add_def mult_def)
    74   apply (unfold add_def mult_def)
    75   apply (tactic {* typechk_tac @{context} [] 1 *})
    75   apply typechk
    76   done
    76   done
    77 
    77 
    78 (* Defined to return zero if a<b *)
    78 (* Defined to return zero if a<b *)
    79 lemma subT: "[| a:Nat;  b:Nat |] ==> a #- b : Nat"
    79 lemma subT: "[| a:Nat;  b:Nat |] ==> a #- b : Nat"
    80   apply (unfold sub_def)
    80   apply (unfold sub_def)
    81   apply (tactic {* typechk_tac @{context} [] 1 *})
    81   apply typechk
    82   apply (tactic {* clean_ccs_tac @{context} *})
    82   apply clean_ccs
    83   apply (erule NatPRI [THEN wfstI, THEN NatPR_wf [THEN wmap_wf, THEN wfI]])
    83   apply (erule NatPRI [THEN wfstI, THEN NatPR_wf [THEN wmap_wf, THEN wfI]])
    84   done
    84   done
    85 
    85 
    86 lemma leT: "[| a:Nat;  b:Nat |] ==> a #<= b : Bool"
    86 lemma leT: "[| a:Nat;  b:Nat |] ==> a #<= b : Bool"
    87   apply (unfold le_def)
    87   apply (unfold le_def)
    88   apply (tactic {* typechk_tac @{context} [] 1 *})
    88   apply typechk
    89   apply (tactic {* clean_ccs_tac @{context} *})
    89   apply clean_ccs
    90   apply (erule NatPRI [THEN wfstI, THEN NatPR_wf [THEN wmap_wf, THEN wfI]])
    90   apply (erule NatPRI [THEN wfstI, THEN NatPR_wf [THEN wmap_wf, THEN wfI]])
    91   done
    91   done
    92 
    92 
    93 lemma ltT: "[| a:Nat;  b:Nat |] ==> a #< b : Bool"
    93 lemma ltT: "[| a:Nat;  b:Nat |] ==> a #< b : Bool"
    94   apply (unfold not_def lt_def)
    94   apply (unfold not_def lt_def)
    95   apply (tactic {* typechk_tac @{context} @{thms leT} 1 *})
    95   apply (typechk leT)
    96   done
    96   done
    97 
    97 
    98 
    98 
    99 subsection {* Termination Conditions for Ackermann's Function *}
    99 subsection {* Termination Conditions for Ackermann's Function *}
   100 
   100 
   101 lemmas relI = NatPR_wf [THEN NatPR_wf [THEN lex_wf, THEN wfI]]
   101 lemmas relI = NatPR_wf [THEN NatPR_wf [THEN lex_wf, THEN wfI]]
   102 
   102 
   103 lemma "[| a:Nat;  b:Nat |] ==> ackermann(a,b) : Nat"
   103 lemma "[| a:Nat;  b:Nat |] ==> ackermann(a,b) : Nat"
   104   apply (unfold ackermann_def)
   104   apply (unfold ackermann_def)
   105   apply (tactic {* gen_ccs_tac @{context} [] 1 *})
   105   apply gen_ccs
   106   apply (erule NatPRI [THEN lexI1 [THEN relI]] NatPRI [THEN lexI2 [THEN relI]])+
   106   apply (erule NatPRI [THEN lexI1 [THEN relI]] NatPRI [THEN lexI2 [THEN relI]])+
   107   done
   107   done
   108 
   108 
   109 end
   109 end