src/CCL/ex/Nat.thy
 changeset 60770 240563fbf41d parent 58977 9576b510f6a2
equal 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)`