25 by (res_inst_tac [("t","t")] term_case 1); |
25 by (res_inst_tac [("t","t")] term_case 1); |
26 by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam]))); |
26 by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam]))); |
27 val letB = result() RS mp; |
27 val letB = result() RS mp; |
28 |
28 |
29 goalw Term.thy [let_def] "let x be bot in f(x) = bot"; |
29 goalw Term.thy [let_def] "let x be bot in f(x) = bot"; |
30 br caseBbot 1; |
30 by (rtac caseBbot 1); |
31 val letBabot = result(); |
31 val letBabot = result(); |
32 |
32 |
33 goalw Term.thy [let_def] "let x be t in bot = bot"; |
33 goalw Term.thy [let_def] "let x be t in bot = bot"; |
34 brs ([caseBbot] RL [term_case]) 1; |
34 by (resolve_tac ([caseBbot] RL [term_case]) 1); |
35 by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam]))); |
35 by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam]))); |
36 val letBbbot = result(); |
36 val letBbbot = result(); |
37 |
37 |
38 goalw Term.thy [apply_def] "(lam x.b(x)) ` a = b(a)"; |
38 goalw Term.thy [apply_def] "(lam x.b(x)) ` a = b(a)"; |
39 by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam]))); |
39 by (ALLGOALS(simp_tac(CCL_ss addsimps [caseBtrue,caseBfalse,caseBpair,caseBlam]))); |
40 val applyB = result(); |
40 val applyB = result(); |
41 |
41 |
42 goalw Term.thy [apply_def] "bot ` a = bot"; |
42 goalw Term.thy [apply_def] "bot ` a = bot"; |
43 br caseBbot 1; |
43 by (rtac caseBbot 1); |
44 val applyBbot = result(); |
44 val applyBbot = result(); |
45 |
45 |
46 goalw Term.thy [fix_def] "fix(f) = f(fix(f))"; |
46 goalw Term.thy [fix_def] "fix(f) = f(fix(f))"; |
47 by (resolve_tac [applyB RS ssubst] 1 THEN resolve_tac [refl] 1); |
47 by (resolve_tac [applyB RS ssubst] 1 THEN rtac refl 1); |
48 val fixB = result(); |
48 val fixB = result(); |
49 |
49 |
50 goalw Term.thy [letrec_def] |
50 goalw Term.thy [letrec_def] |
51 "letrec g x be h(x,g) in g(a) = h(a,%y.letrec g x be h(x,g) in g(y))"; |
51 "letrec g x be h(x,g) in g(a) = h(a,%y.letrec g x be h(x,g) in g(y))"; |
52 by (resolve_tac [fixB RS ssubst] 1 THEN |
52 by (resolve_tac [fixB RS ssubst] 1 THEN |
53 resolve_tac [applyB RS ssubst] 1 THEN resolve_tac [refl] 1); |
53 resolve_tac [applyB RS ssubst] 1 THEN rtac refl 1); |
54 val letrecB = result(); |
54 val letrecB = result(); |
55 |
55 |
56 val rawBs = caseBs @ [applyB,applyBbot]; |
56 val rawBs = caseBs @ [applyB,applyBbot]; |
57 |
57 |
58 fun raw_mk_beta_rl defs s = prove_goalw Term.thy defs s |
58 fun raw_mk_beta_rl defs s = prove_goalw Term.thy defs s |