3 Author: Ole Rasmussen |
3 Author: Ole Rasmussen |
4 Copyright 1995 University of Cambridge |
4 Copyright 1995 University of Cambridge |
5 Logic Image: ZF |
5 Logic Image: ZF |
6 *) |
6 *) |
7 |
7 |
8 open Terms; |
8 Addsimps ([lambda.dom_subset RS subsetD] @ lambda.intrs); |
9 |
|
10 (* ------------------------------------------------------------------------- *) |
|
11 (* unmark simplifications *) |
|
12 (* ------------------------------------------------------------------------- *) |
|
13 |
|
14 Goalw [unmark_def] "unmark(Var(n)) = Var(n)"; |
|
15 by (Asm_simp_tac 1); |
|
16 qed "unmark_Var"; |
|
17 |
|
18 Goalw [unmark_def] "unmark(Fun(t)) = Fun(unmark(t))"; |
|
19 by (Asm_simp_tac 1); |
|
20 qed "unmark_Fun"; |
|
21 |
|
22 Goalw [unmark_def] "unmark(App(b,n,m)) = App(0,unmark(n),unmark(m))"; |
|
23 by (Asm_simp_tac 1); |
|
24 qed "unmark_App"; |
|
25 |
|
26 |
|
27 (* ------------------------------------------------------------------------- *) |
|
28 (* term simplification set *) |
|
29 (* ------------------------------------------------------------------------- *) |
|
30 |
|
31 |
|
32 Addsimps ([unmark_App, unmark_Fun, unmark_Var, |
|
33 lambda.dom_subset RS subsetD] @ |
|
34 lambda.intrs); |
|
35 |
9 |
36 |
10 |
37 (* ------------------------------------------------------------------------- *) |
11 (* ------------------------------------------------------------------------- *) |
38 (* unmark lemmas *) |
12 (* unmark lemmas *) |
39 (* ------------------------------------------------------------------------- *) |
13 (* ------------------------------------------------------------------------- *) |
40 |
14 |
41 Goalw [unmark_def] |
15 Goal "u:redexes ==> unmark(u):lambda"; |
42 "u:redexes ==> unmark(u):lambda"; |
|
43 by (etac redexes.induct 1); |
16 by (etac redexes.induct 1); |
44 by (ALLGOALS Asm_simp_tac); |
17 by (ALLGOALS Asm_simp_tac); |
45 qed "unmark_type"; |
18 qed "unmark_type"; |
46 |
19 |
47 Goal "u:lambda ==> unmark(u) = u"; |
20 Goal "u:lambda ==> unmark(u) = u"; |
55 (* ------------------------------------------------------------------------- *) |
28 (* ------------------------------------------------------------------------- *) |
56 |
29 |
57 Goal "v:lambda ==> ALL k:nat. lift_rec(v,k):lambda"; |
30 Goal "v:lambda ==> ALL k:nat. lift_rec(v,k):lambda"; |
58 by (etac lambda.induct 1); |
31 by (etac lambda.induct 1); |
59 by (ALLGOALS (asm_simp_tac (simpset() addsimps [lift_rec_Var]))); |
32 by (ALLGOALS (asm_simp_tac (simpset() addsimps [lift_rec_Var]))); |
60 qed "liftL_typea"; |
33 bind_thm ("liftL_type", result() RS bspec); |
61 val liftL_type =liftL_typea RS bspec ; |
|
62 |
34 |
63 Goal "v:lambda ==> ALL n:nat. ALL u:lambda. subst_rec(u,v,n):lambda"; |
35 Goal "v:lambda ==> ALL n:nat. ALL u:lambda. subst_rec(u,v,n):lambda"; |
64 by (etac lambda.induct 1); |
36 by (etac lambda.induct 1); |
65 by (ALLGOALS (asm_simp_tac (simpset() addsimps [liftL_type,subst_Var]))); |
37 by (ALLGOALS (asm_simp_tac (simpset() addsimps [liftL_type,subst_Var]))); |
66 qed "substL_typea"; |
38 qed "substL_typea"; |
67 val substL_type = substL_typea RS bspec RS bspec ; |
39 bind_thm ("substL_type", result() RS bspec RS bspec); |
68 |
40 |
69 |
41 |
70 (* ------------------------------------------------------------------------- *) |
42 (* ------------------------------------------------------------------------- *) |
71 (* type-rule for reduction definitions *) |
43 (* type-rule for reduction definitions *) |
72 (* ------------------------------------------------------------------------- *) |
44 (* ------------------------------------------------------------------------- *) |