1 (* Title: Residuals.ML |
|
2 ID: $Id$ |
|
3 Author: Ole Rasmussen |
|
4 Copyright 1995 University of Cambridge |
|
5 Logic Image: ZF |
|
6 *) |
|
7 |
|
8 (* ------------------------------------------------------------------------- *) |
|
9 (* Setting up rule lists *) |
|
10 (* ------------------------------------------------------------------------- *) |
|
11 |
|
12 AddIs (Sres.intrs @ Sreg.intrs @ [subst_type]); |
|
13 AddSEs (map Sres.mk_cases |
|
14 ["residuals(Var(n),Var(n),v)", |
|
15 "residuals(Fun(t),Fun(u),v)", |
|
16 "residuals(App(b, u1, u2), App(0, v1, v2),v)", |
|
17 "residuals(App(b, u1, u2), App(1, Fun(v1), v2),v)", |
|
18 "residuals(Var(n),u,v)", |
|
19 "residuals(Fun(t),u,v)", |
|
20 "residuals(App(b, u1, u2), w,v)", |
|
21 "residuals(u,Var(n),v)", |
|
22 "residuals(u,Fun(t),v)", |
|
23 "residuals(w,App(b, u1, u2),v)"]); |
|
24 |
|
25 AddSEs (map Ssub.mk_cases |
|
26 ["Var(n) <== u", |
|
27 "Fun(n) <== u", |
|
28 "u <== Fun(n)", |
|
29 "App(1,Fun(t),a) <== u", |
|
30 "App(0,t,a) <== u"]); |
|
31 |
|
32 AddSEs [redexes.mk_cases "Fun(t):redexes"]; |
|
33 |
|
34 Addsimps Sres.intrs; |
|
35 val resD1 = Sres.dom_subset RS subsetD RS SigmaD1; |
|
36 val resD2 = Sres.dom_subset RS subsetD RS SigmaD2 RS SigmaD1; |
|
37 val resD3 = Sres.dom_subset RS subsetD RS SigmaD2 RS SigmaD2; |
|
38 |
|
39 |
|
40 (* ------------------------------------------------------------------------- *) |
|
41 (* residuals is a partial function *) |
|
42 (* ------------------------------------------------------------------------- *) |
|
43 |
|
44 Goal "residuals(u,v,w) ==> \\<forall>w1. residuals(u,v,w1) --> w1 = w"; |
|
45 by (etac Sres.induct 1); |
|
46 by (ALLGOALS Force_tac); |
|
47 qed_spec_mp "residuals_function"; |
|
48 |
|
49 Goal "u~v ==> regular(v) --> (\\<exists>w. residuals(u,v,w))"; |
|
50 by (etac Scomp.induct 1); |
|
51 by (ALLGOALS Fast_tac); |
|
52 qed "residuals_intro"; |
|
53 |
|
54 Goal "[| u~v; regular(v) |] ==> residuals(u,v,THE w. residuals(u, v, w))"; |
|
55 by (resolve_tac [residuals_intro RS mp RS exE] 1); |
|
56 by (stac the_equality 3); |
|
57 by (ALLGOALS (blast_tac (claset() addIs [residuals_function]))); |
|
58 qed "comp_resfuncD"; |
|
59 |
|
60 |
|
61 (* ------------------------------------------------------------------------- *) |
|
62 (* Residual function *) |
|
63 (* ------------------------------------------------------------------------- *) |
|
64 |
|
65 Goalw [res_func_def] "n \\<in> nat ==> Var(n) |> Var(n) = Var(n)"; |
|
66 by (Blast_tac 1); |
|
67 qed "res_Var"; |
|
68 |
|
69 Goalw [res_func_def] |
|
70 "[|s~t; regular(t)|]==> Fun(s) |> Fun(t) = Fun(s |> t)"; |
|
71 by (blast_tac (claset() addSDs [comp_resfuncD] |
|
72 addIs [residuals_function]) 1); |
|
73 qed "res_Fun"; |
|
74 |
|
75 Goalw [res_func_def] |
|
76 "[|s~u; regular(u); t~v; regular(v); b \\<in> bool|]==> \ |
|
77 \ App(b,s,t) |> App(0,u,v) = App(b, s |> u, t |> v)"; |
|
78 by (blast_tac (claset() addSDs [comp_resfuncD] |
|
79 addIs [residuals_function]) 1); |
|
80 qed "res_App"; |
|
81 |
|
82 Goalw [res_func_def] |
|
83 "[|s~u; regular(u); t~v; regular(v); b \\<in> bool|]==> \ |
|
84 \ App(b,Fun(s),t) |> App(1,Fun(u),v) = (t |> v)/ (s |> u)"; |
|
85 by (blast_tac (claset() addSEs redexes.free_SEs |
|
86 addSDs [comp_resfuncD] |
|
87 addIs [residuals_function]) 1); |
|
88 qed "res_redex"; |
|
89 |
|
90 Goal "[|s~t; regular(t)|]==> regular(t) --> s |> t \\<in> redexes"; |
|
91 by (etac Scomp.induct 1); |
|
92 by (auto_tac (claset(), |
|
93 simpset() addsimps [res_Var,res_Fun,res_App,res_redex])); |
|
94 by (dres_inst_tac [("psi", "Fun(?u) |> ?v \\<in> redexes")] asm_rl 1); |
|
95 by (auto_tac (claset(), |
|
96 simpset() addsimps [res_Fun])); |
|
97 qed "resfunc_type"; |
|
98 |
|
99 Addsimps [res_Var, res_Fun, res_App, res_redex, lift_rec_preserve_comp, |
|
100 lift_rec_preserve_reg, subst_rec_preserve_comp, resfunc_type, |
|
101 subst_rec_preserve_reg]; |
|
102 |
|
103 |
|
104 (* ------------------------------------------------------------------------- *) |
|
105 (* Commutation theorem *) |
|
106 (* ------------------------------------------------------------------------- *) |
|
107 |
|
108 Goal "u<==v ==> u~v"; |
|
109 by (etac Ssub.induct 1); |
|
110 by (ALLGOALS Asm_simp_tac); |
|
111 qed "sub_comp"; |
|
112 |
|
113 Goal "u<==v ==> regular(v) --> regular(u)"; |
|
114 by (etac Ssub.induct 1); |
|
115 by Auto_tac; |
|
116 qed_spec_mp "sub_preserve_reg"; |
|
117 |
|
118 Goal "[|u~v; k \\<in> nat|]==> regular(v)--> (\\<forall>n \\<in> nat. \ |
|
119 \ lift_rec(u,n) |> lift_rec(v,n) = lift_rec(u |> v,n))"; |
|
120 by (etac Scomp.induct 1); |
|
121 by Safe_tac; |
|
122 by (ALLGOALS |
|
123 (asm_full_simp_tac |
|
124 (simpset() addsimps [lift_rec_Var,subst_Var,lift_subst]))); |
|
125 by (rotate_tac ~2 1); |
|
126 by (Asm_full_simp_tac 1); |
|
127 qed "residuals_lift_rec"; |
|
128 |
|
129 Goal "u1~u2 ==> \\<forall>v1 v2. v1~v2 --> regular(v2) --> regular(u2) -->\ |
|
130 \ (\\<forall>n \\<in> nat. subst_rec(v1,u1,n) |> subst_rec(v2,u2,n) = \ |
|
131 \ subst_rec(v1 |> v2, u1 |> u2,n))"; |
|
132 by (etac Scomp.induct 1); |
|
133 by Safe_tac; |
|
134 by (ALLGOALS |
|
135 (asm_simp_tac |
|
136 (simpset() addsimps [lift_rec_Var,subst_Var,residuals_lift_rec]))); |
|
137 by (dres_inst_tac [("psi", "\\<forall>x.?P(x)")] asm_rl 1); |
|
138 by (asm_full_simp_tac (simpset() addsimps [substitution]) 1); |
|
139 qed "residuals_subst_rec"; |
|
140 |
|
141 |
|
142 Goal "[|u1~u2; v1~v2; regular(u2); regular(v2)|]==>\ |
|
143 \ (v1/u1) |> (v2/u2) = (v1 |> v2)/(u1 |> u2)"; |
|
144 by (asm_simp_tac (simpset() addsimps [residuals_subst_rec]) 1); |
|
145 qed "commutation"; |
|
146 |
|
147 (* ------------------------------------------------------------------------- *) |
|
148 (* Residuals are comp and regular *) |
|
149 (* ------------------------------------------------------------------------- *) |
|
150 |
|
151 Goal "u~v ==> \\<forall>w. u~w --> v~w --> regular(w) --> (u|>w) ~ (v|>w)"; |
|
152 by (etac Scomp.induct 1); |
|
153 by (ALLGOALS Force_tac); |
|
154 qed_spec_mp "residuals_preserve_comp"; |
|
155 |
|
156 |
|
157 Goal "u~v ==> regular(u) --> regular(v) --> regular(u|>v)"; |
|
158 by (etac Scomp.induct 1); |
|
159 by Safe_tac; |
|
160 by (TRYALL (dres_inst_tac [("psi", "regular(Fun(?u) |> ?v)")] asm_rl)); |
|
161 by Auto_tac; |
|
162 qed_spec_mp "residuals_preserve_reg"; |
|
163 |
|
164 (* ------------------------------------------------------------------------- *) |
|
165 (* Preservation lemma *) |
|
166 (* ------------------------------------------------------------------------- *) |
|
167 |
|
168 Goal "u~v ==> v ~ (u un v)"; |
|
169 by (etac Scomp.induct 1); |
|
170 by (ALLGOALS Asm_simp_tac); |
|
171 qed "union_preserve_comp"; |
|
172 |
|
173 Goal "u ~ v ==> regular(v) --> u|>v = (u un v)|>v"; |
|
174 by (etac Scomp.induct 1); |
|
175 by Safe_tac; |
|
176 by (dres_inst_tac [("psi", "Fun(?u) |> ?v = ?w")] asm_rl 3); |
|
177 by (auto_tac (claset(), |
|
178 simpset() addsimps [union_preserve_comp,comp_sym_iff])); |
|
179 by (asm_full_simp_tac (simpset() addsimps |
|
180 [union_preserve_comp RS comp_sym, |
|
181 comp_sym RS union_preserve_comp RS comp_sym]) 1); |
|
182 qed_spec_mp "preservation"; |
|