src/CCL/ex/Nat.thy
changeset 60770 240563fbf41d
parent 58977 9576b510f6a2
equal deleted inserted replaced
60769:cf7f3465eaf1 60770:240563fbf41d
     1 (*  Title:      CCL/ex/Nat.thy
     1 (*  Title:      CCL/ex/Nat.thy
     2     Author:     Martin Coen, Cambridge University Computer Laboratory
     2     Author:     Martin Coen, Cambridge University Computer Laboratory
     3     Copyright   1993  University of Cambridge
     3     Copyright   1993  University of Cambridge
     4 *)
     4 *)
     5 
     5 
     6 section {* Programs defined over the natural numbers *}
     6 section \<open>Programs defined over the natural numbers\<close>
     7 
     7 
     8 theory Nat
     8 theory Nat
     9 imports "../Wfd"
     9 imports "../Wfd"
    10 begin
    10 begin
    11 
    11 
    94   apply (unfold not_def lt_def)
    94   apply (unfold not_def lt_def)
    95   apply (typechk leT)
    95   apply (typechk leT)
    96   done
    96   done
    97 
    97 
    98 
    98 
    99 subsection {* Termination Conditions for Ackermann's Function *}
    99 subsection \<open>Termination Conditions for Ackermann's Function\<close>
   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 "\<lbrakk>a:Nat; b:Nat\<rbrakk> \<Longrightarrow> ackermann(a,b) : Nat"
   103 lemma "\<lbrakk>a:Nat; b:Nat\<rbrakk> \<Longrightarrow> ackermann(a,b) : Nat"
   104   apply (unfold ackermann_def)
   104   apply (unfold ackermann_def)