11 (* unmark simplifications *) |
11 (* unmark simplifications *) |
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 lift_ss 1); |
16 by (Asm_simp_tac 1); |
17 val unmark_Var = result(); |
17 val unmark_Var = result(); |
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 lift_ss 1); |
21 by (Asm_simp_tac 1); |
22 val unmark_Fun = result(); |
22 val unmark_Fun = result(); |
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 lift_ss 1); |
26 by (Asm_simp_tac 1); |
27 val unmark_App = result(); |
27 val unmark_App = result(); |
28 |
28 |
29 |
29 |
30 (* ------------------------------------------------------------------------- *) |
30 (* ------------------------------------------------------------------------- *) |
31 (* term simplification set *) |
31 (* term simplification set *) |
32 (* ------------------------------------------------------------------------- *) |
32 (* ------------------------------------------------------------------------- *) |
33 |
33 |
34 |
34 |
35 val term_ss = res1_ss addsimps ([unmark_App,unmark_Fun,unmark_Var, |
35 Addsimps ([unmark_App, unmark_Fun, unmark_Var, |
36 lambda.dom_subset RS subsetD]@lambda.intrs); |
36 lambda.dom_subset RS subsetD] @ |
|
37 lambda.intrs); |
37 |
38 |
38 |
39 |
39 (* ------------------------------------------------------------------------- *) |
40 (* ------------------------------------------------------------------------- *) |
40 (* unmark lemmas *) |
41 (* unmark lemmas *) |
41 (* ------------------------------------------------------------------------- *) |
42 (* ------------------------------------------------------------------------- *) |
42 |
43 |
43 goalw Terms.thy [unmark_def] |
44 goalw Terms.thy [unmark_def] |
44 "!!u.u:redexes ==> unmark(u):lambda"; |
45 "!!u.u:redexes ==> unmark(u):lambda"; |
45 by (eresolve_tac [redexes.induct] 1); |
46 by (eresolve_tac [redexes.induct] 1); |
46 by (ALLGOALS(asm_simp_tac term_ss)); |
47 by (ALLGOALS Asm_simp_tac); |
47 val unmark_type = result(); |
48 val unmark_type = result(); |
48 |
49 |
49 goal Terms.thy |
50 goal Terms.thy |
50 "!!u.u:lambda ==> unmark(u) = u"; |
51 "!!u.u:lambda ==> unmark(u) = u"; |
51 by (eresolve_tac [lambda.induct] 1); |
52 by (eresolve_tac [lambda.induct] 1); |
52 by (ALLGOALS(asm_simp_tac term_ss)); |
53 by (ALLGOALS Asm_simp_tac); |
53 val lambda_unmark = result(); |
54 val lambda_unmark = result(); |
54 |
55 |
55 |
56 |
56 (* ------------------------------------------------------------------------- *) |
57 (* ------------------------------------------------------------------------- *) |
57 (* lift and subst preserve lambda *) |
58 (* lift and subst preserve lambda *) |
58 (* ------------------------------------------------------------------------- *) |
59 (* ------------------------------------------------------------------------- *) |
59 |
60 |
60 goal Terms.thy |
61 goal Terms.thy |
61 "!!u.[|v:lambda|]==> ALL k:nat.lift_rec(v,k):lambda"; |
62 "!!u.[|v:lambda|]==> ALL k:nat.lift_rec(v,k):lambda"; |
62 by (eresolve_tac [lambda.induct] 1); |
63 by (eresolve_tac [lambda.induct] 1); |
63 by (ALLGOALS(asm_full_simp_tac (addsplit term_ss))); |
64 by (ALLGOALS(asm_full_simp_tac (addsplit (!simpset)))); |
64 val liftL_typea = result(); |
65 val liftL_typea = result(); |
65 val liftL_type =liftL_typea RS bspec ; |
66 val liftL_type =liftL_typea RS bspec ; |
66 |
67 |
67 goal Terms.thy |
68 goal Terms.thy |
68 "!!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"; |
69 by (eresolve_tac [lambda.induct] 1); |
70 by (eresolve_tac [lambda.induct] 1); |
70 by (ALLGOALS(asm_full_simp_tac ((addsplit term_ss) addsimps [liftL_type]))); |
71 by (ALLGOALS(asm_full_simp_tac ((addsplit (!simpset)) addsimps [liftL_type]))); |
71 val substL_typea = result(); |
72 val substL_typea = result(); |
72 val substL_type = substL_typea RS bspec RS bspec ; |
73 val substL_type = substL_typea RS bspec RS bspec ; |
73 |
74 |
74 |
75 |
75 (* ------------------------------------------------------------------------- *) |
76 (* ------------------------------------------------------------------------- *) |