src/CCL/ex/Nat.thy
 changeset 20140 98acc6d0fab6 parent 17456 bcf7544875b2 child 24825 c4f13ab78f9d
equal inserted replaced
20139:804927db5311 20140:98acc6d0fab6
`    38   ack_def:`
`    38   ack_def:`
`    39   "ackermann(a,b) == letrec ack n m be ncase(n,succ(m),%x.`
`    39   "ackermann(a,b) == letrec ack n m be ncase(n,succ(m),%x.`
`    40                           ncase(m,ack(x,succ(zero)),%y. ack(x,ack(succ(x),y))))`
`    40                           ncase(m,ack(x,succ(zero)),%y. ack(x,ack(succ(x),y))))`
`    41                     in ack(a,b)"`
`    41                     in ack(a,b)"`
`    42 `
`    42 `
`    43 ML {* use_legacy_bindings (the_context ()) *}`
`    43 lemmas nat_defs = not_def add_def mult_def sub_def le_def lt_def ack_def napply_def`
`       `
`    44 `
`       `
`    45 lemma natBs [simp]:`
`       `
`    46   "not(true) = false"`
`       `
`    47   "not(false) = true"`
`       `
`    48   "zero #+ n = n"`
`       `
`    49   "succ(n) #+ m = succ(n #+ m)"`
`       `
`    50   "zero #* n = zero"`
`       `
`    51   "succ(n) #* m = m #+ (n #* m)"`
`       `
`    52   "f^zero`a = a"`
`       `
`    53   "f^succ(n)`a = f(f^n`a)"`
`       `
`    54   by (simp_all add: nat_defs)`
`       `
`    55 `
`       `
`    56 `
`       `
`    57 lemma napply_f: "n:Nat ==> f^n`f(a) = f^succ(n)`a"`
`       `
`    58   apply (erule Nat_ind)`
`       `
`    59    apply simp_all`
`       `
`    60   done`
`       `
`    61 `
`       `
`    62 lemma addT: "[| a:Nat;  b:Nat |] ==> a #+ b : Nat"`
`       `
`    63   apply (unfold add_def)`
`       `
`    64   apply (tactic {* typechk_tac [] 1 *})`
`       `
`    65   done`
`       `
`    66 `
`       `
`    67 lemma multT: "[| a:Nat;  b:Nat |] ==> a #* b : Nat"`
`       `
`    68   apply (unfold add_def mult_def)`
`       `
`    69   apply (tactic {* typechk_tac [] 1 *})`
`       `
`    70   done`
`       `
`    71 `
`       `
`    72 (* Defined to return zero if a<b *)`
`       `
`    73 lemma subT: "[| a:Nat;  b:Nat |] ==> a #- b : Nat"`
`       `
`    74   apply (unfold sub_def)`
`       `
`    75   apply (tactic {* typechk_tac [] 1 *})`
`       `
`    76   apply (tactic clean_ccs_tac)`
`       `
`    77   apply (erule NatPRI [THEN wfstI, THEN NatPR_wf [THEN wmap_wf, THEN wfI]])`
`       `
`    78   done`
`       `
`    79 `
`       `
`    80 lemma leT: "[| a:Nat;  b:Nat |] ==> a #<= b : Bool"`
`       `
`    81   apply (unfold le_def)`
`       `
`    82   apply (tactic {* typechk_tac [] 1 *})`
`       `
`    83   apply (tactic clean_ccs_tac)`
`       `
`    84   apply (erule NatPRI [THEN wfstI, THEN NatPR_wf [THEN wmap_wf, THEN wfI]])`
`       `
`    85   done`
`       `
`    86 `
`       `
`    87 lemma ltT: "[| a:Nat;  b:Nat |] ==> a #< b : Bool"`
`       `
`    88   apply (unfold not_def lt_def)`
`       `
`    89   apply (tactic {* typechk_tac [thm "leT"] 1 *})`
`       `
`    90   done`
`       `
`    91 `
`       `
`    92 `
`       `
`    93 subsection {* Termination Conditions for Ackermann's Function *}`
`       `
`    94 `
`       `
`    95 lemmas relI = NatPR_wf [THEN NatPR_wf [THEN lex_wf, THEN wfI]]`
`       `
`    96 `
`       `
`    97 lemma "[| a:Nat;  b:Nat |] ==> ackermann(a,b) : Nat"`
`       `
`    98   apply (unfold ack_def)`
`       `
`    99   apply (tactic "gen_ccs_tac [] 1")`
`       `
`   100   apply (erule NatPRI [THEN lexI1 [THEN relI]] NatPRI [THEN lexI2 [THEN relI]])+`
`       `
`   101   done`
`    44 `
`   102 `
`    45 end`
`   103 end`
`    46 `
`   104 `