8 |
8 |
9 open Nat; |
9 open Nat; |
10 |
10 |
11 val nat_defs = [not_def,add_def,mult_def,sub_def,le_def,lt_def,ack_def,napply_def]; |
11 val nat_defs = [not_def,add_def,mult_def,sub_def,le_def,lt_def,ack_def,napply_def]; |
12 |
12 |
13 val natBs = map (fn s=>prove_goalw Nat.thy nat_defs s (fn _ => [SIMP_TAC term_ss 1])) |
13 val natBs = map (fn s=>prove_goalw Nat.thy nat_defs s (fn _ => [simp_tac term_ss 1])) |
14 ["not(true) = false", |
14 ["not(true) = false", |
15 "not(false) = true", |
15 "not(false) = true", |
16 "zero #+ n = n", |
16 "zero #+ n = n", |
17 "succ(n) #+ m = succ(n #+ m)", |
17 "succ(n) #+ m = succ(n #+ m)", |
18 "zero #* n = zero", |
18 "zero #* n = zero", |
19 "succ(n) #* m = m #+ (n #* m)", |
19 "succ(n) #* m = m #+ (n #* m)", |
20 "f^zero`a = a", |
20 "f^zero`a = a", |
21 "f^succ(n)`a = f(f^n`a)"]; |
21 "f^succ(n)`a = f(f^n`a)"]; |
22 |
22 |
23 val nat_congs = ccl_mk_congs Nat.thy ["not","op #+","op #*","op #-","op ##", |
23 val nat_ss = term_ss addsimps natBs; |
24 "op #<","op #<=","ackermann","napply"]; |
|
25 |
|
26 val nat_ss = term_ss addrews natBs addcongs nat_congs; |
|
27 |
24 |
28 (*** Lemma for napply ***) |
25 (*** Lemma for napply ***) |
29 |
26 |
30 val [prem] = goal Nat.thy "n:Nat ==> f^n`f(a) = f^succ(n)`a"; |
27 val [prem] = goal Nat.thy "n:Nat ==> f^n`f(a) = f^succ(n)`a"; |
31 br (prem RS Nat_ind) 1; |
28 br (prem RS Nat_ind) 1; |
32 by (ALLGOALS (ASM_SIMP_TAC (nat_ss addcongs [read_instantiate [("f","f")] arg_cong]))); |
29 by (ALLGOALS (asm_simp_tac nat_ss)); |
33 val napply_f = result(); |
30 val napply_f = result(); |
34 |
31 |
35 (****) |
32 (****) |
36 |
33 |
37 val prems = goalw Nat.thy [add_def] "[| a:Nat; b:Nat |] ==> a #+ b : Nat"; |
34 val prems = goalw Nat.thy [add_def] "[| a:Nat; b:Nat |] ==> a #+ b : Nat"; |