12 (* ------------------------------------------------------------------------- *) |
12 (* ------------------------------------------------------------------------- *) |
13 |
13 |
14 goalw Terms.thy [unmark_def] |
14 goalw Terms.thy [unmark_def] |
15 "unmark(Var(n)) = Var(n)"; |
15 "unmark(Var(n)) = Var(n)"; |
16 by (Asm_simp_tac 1); |
16 by (Asm_simp_tac 1); |
17 val unmark_Var = result(); |
17 qed "unmark_Var"; |
18 |
18 |
19 goalw Terms.thy [unmark_def] |
19 goalw Terms.thy [unmark_def] |
20 "unmark(Fun(t)) = Fun(unmark(t))"; |
20 "unmark(Fun(t)) = Fun(unmark(t))"; |
21 by (Asm_simp_tac 1); |
21 by (Asm_simp_tac 1); |
22 val unmark_Fun = result(); |
22 qed "unmark_Fun"; |
23 |
23 |
24 goalw Terms.thy [unmark_def] |
24 goalw Terms.thy [unmark_def] |
25 "unmark(App(b,n,m)) = App(0,unmark(n),unmark(m))"; |
25 "unmark(App(b,n,m)) = App(0,unmark(n),unmark(m))"; |
26 by (Asm_simp_tac 1); |
26 by (Asm_simp_tac 1); |
27 val unmark_App = result(); |
27 qed "unmark_App"; |
28 |
28 |
29 |
29 |
30 (* ------------------------------------------------------------------------- *) |
30 (* ------------------------------------------------------------------------- *) |
31 (* term simplification set *) |
31 (* term simplification set *) |
32 (* ------------------------------------------------------------------------- *) |
32 (* ------------------------------------------------------------------------- *) |
43 |
43 |
44 goalw Terms.thy [unmark_def] |
44 goalw Terms.thy [unmark_def] |
45 "!!u.u:redexes ==> unmark(u):lambda"; |
45 "!!u.u:redexes ==> unmark(u):lambda"; |
46 by (eresolve_tac [redexes.induct] 1); |
46 by (eresolve_tac [redexes.induct] 1); |
47 by (ALLGOALS Asm_simp_tac); |
47 by (ALLGOALS Asm_simp_tac); |
48 val unmark_type = result(); |
48 qed "unmark_type"; |
49 |
49 |
50 goal Terms.thy |
50 goal Terms.thy |
51 "!!u.u:lambda ==> unmark(u) = u"; |
51 "!!u.u:lambda ==> unmark(u) = u"; |
52 by (eresolve_tac [lambda.induct] 1); |
52 by (eresolve_tac [lambda.induct] 1); |
53 by (ALLGOALS Asm_simp_tac); |
53 by (ALLGOALS Asm_simp_tac); |
54 val lambda_unmark = result(); |
54 qed "lambda_unmark"; |
55 |
55 |
56 |
56 |
57 (* ------------------------------------------------------------------------- *) |
57 (* ------------------------------------------------------------------------- *) |
58 (* lift and subst preserve lambda *) |
58 (* lift and subst preserve lambda *) |
59 (* ------------------------------------------------------------------------- *) |
59 (* ------------------------------------------------------------------------- *) |
60 |
60 |
61 goal Terms.thy |
61 goal Terms.thy |
62 "!!u.[|v:lambda|]==> ALL k:nat.lift_rec(v,k):lambda"; |
62 "!!u.[|v:lambda|]==> ALL k:nat.lift_rec(v,k):lambda"; |
63 by (eresolve_tac [lambda.induct] 1); |
63 by (eresolve_tac [lambda.induct] 1); |
64 by (ALLGOALS(asm_full_simp_tac (addsplit (!simpset)))); |
64 by (ALLGOALS(asm_full_simp_tac (addsplit (!simpset)))); |
65 val liftL_typea = result(); |
65 qed "liftL_typea"; |
66 val liftL_type =liftL_typea RS bspec ; |
66 val liftL_type =liftL_typea RS bspec ; |
67 |
67 |
68 goal Terms.thy |
68 goal Terms.thy |
69 "!!n.[|v:lambda|]==> ALL n:nat.ALL u:lambda.subst_rec(u,v,n):lambda"; |
69 "!!n.[|v:lambda|]==> ALL n:nat.ALL u:lambda.subst_rec(u,v,n):lambda"; |
70 by (eresolve_tac [lambda.induct] 1); |
70 by (eresolve_tac [lambda.induct] 1); |
71 by (ALLGOALS(asm_full_simp_tac ((addsplit (!simpset)) addsimps [liftL_type]))); |
71 by (ALLGOALS(asm_full_simp_tac ((addsplit (!simpset)) addsimps [liftL_type]))); |
72 val substL_typea = result(); |
72 qed "substL_typea"; |
73 val substL_type = substL_typea RS bspec RS bspec ; |
73 val substL_type = substL_typea RS bspec RS bspec ; |
74 |
74 |
75 |
75 |
76 (* ------------------------------------------------------------------------- *) |
76 (* ------------------------------------------------------------------------- *) |
77 (* type-rule for reduction definitions *) |
77 (* type-rule for reduction definitions *) |