|
1 theory Let |
|
2 imports "../Nominal2" |
|
3 begin |
|
4 |
|
5 atom_decl name |
|
6 |
|
7 nominal_datatype trm = |
|
8 Var "name" |
|
9 | App "trm" "trm" |
|
10 | Let as::"assn" t::"trm" binds "bn as" in as t |
|
11 and assn = |
|
12 ANil |
|
13 | ACons "name" "trm" "assn" |
|
14 binder |
|
15 bn |
|
16 where |
|
17 "bn ANil = []" |
|
18 | "bn (ACons x t as) = (atom x) # (bn as)" |
|
19 |
|
20 nominal_primrec substrec where |
|
21 "substrec fa fl fd y z (Var x) = (if (y = x) then z else (Var x))" |
|
22 | "substrec fa fl fd y z (App l r) = fa l r" |
|
23 | "(set (bn as) \<sharp>* (Let as t, y, z) \<and> (\<forall>bs s. set (bn bs) \<sharp>* (Let bs s, y, z) \<longrightarrow> Let as t = Let bs s \<longrightarrow> fl as t = fl bs s)) \<Longrightarrow> |
|
24 substrec fa fl fd y z (Let as t) = fl as t" |
|
25 | "(set (bn as) \<sharp>* (Let as t, y, z) \<and> \<not>(\<forall>bs s. set (bn bs) \<sharp>* (Let bs s, y, z) \<longrightarrow> Let as t = Let bs s \<longrightarrow> fl as t = fl bs s)) \<Longrightarrow> |
|
26 substrec fa fl fd y z (Let as t) = fd" |
|
27 unfolding eqvt_def substrec_graph_def |
|
28 apply (rule, perm_simp, rule, rule) |
|
29 apply (case_tac x) |
|
30 apply (rule_tac y="f" and c="(f, d, e)" in trm_assn.strong_exhaust(1)) |
|
31 apply metis |
|
32 apply metis |
|
33 apply (thin_tac "\<And>fa fl fd y z xa. x = (fa, fl, fd, y, z, Var xa) \<Longrightarrow> P") |
|
34 apply (thin_tac "\<And>fa fl fd y z l r. x = (fa, fl, fd, y, z, App l r) \<Longrightarrow> P") |
|
35 apply (drule_tac x="assn" in meta_spec)+ |
|
36 apply (drule_tac x="trm" in meta_spec)+ |
|
37 apply (drule_tac x="d" in meta_spec)+ |
|
38 apply (drule_tac x="e" in meta_spec)+ |
|
39 apply (drule_tac x="b" in meta_spec)+ |
|
40 apply (drule_tac x="a" in meta_spec)+ |
|
41 apply (drule_tac x="c" in meta_spec)+ |
|
42 apply (case_tac "(\<forall>bs s. |
|
43 set (bn bs) \<sharp>* (Let bs s, d, e) \<longrightarrow> |
|
44 Let.Let assn trm = Let.Let bs s \<longrightarrow> b assn trm = b bs s)") |
|
45 apply simp |
|
46 apply (thin_tac "set (bn assn) \<sharp>* (Let assn trm, d, e) \<and> |
|
47 (\<forall>bs s. |
|
48 set (bn bs) \<sharp>* (Let bs s, d, e) \<longrightarrow> |
|
49 Let.Let assn trm = Let.Let bs s \<longrightarrow> b assn trm = b bs s) \<Longrightarrow> |
|
50 x = (a, b, c, d, e, Let.Let assn trm) \<Longrightarrow> P") |
|
51 apply simp |
|
52 apply simp_all |
|
53 apply clarify |
|
54 apply metis |
|
55 done |
|
56 termination (eqvt) by lexicographic_order |
|
57 |
|
58 nominal_primrec substarec :: "(name \<Rightarrow> trm \<Rightarrow> assn \<Rightarrow> assn) \<Rightarrow> assn \<Rightarrow> assn" where |
|
59 "substarec fac ANil = ANil" |
|
60 | "substarec fac (ACons x t as) = fac x t as" |
|
61 unfolding eqvt_def substarec_graph_def |
|
62 apply (rule, perm_simp, rule, rule) |
|
63 apply (case_tac x) |
|
64 apply (rule_tac y="b" in trm_assn.exhaust(2)) |
|
65 apply auto |
|
66 done |
|
67 termination (eqvt) by lexicographic_order |
|
68 |
|
69 lemma [fundef_cong]: |
|
70 "(\<And>t1 t2. t = App t1 t2 \<Longrightarrow> fa t1 t2 = fa' t1 t2) \<Longrightarrow> |
|
71 (\<And>as s. t = Let as s \<Longrightarrow> fl as s = fl' as s) \<Longrightarrow> |
|
72 substrec fa fl fd y z t = substrec fa' fl' fd y z t" |
|
73 apply (rule_tac y="t" and c="(t, y, z)" in trm_assn.strong_exhaust(1)) |
|
74 apply auto |
|
75 apply (case_tac "(\<forall>bs s. set (bn bs) \<sharp>* (Let bs s, y, z) \<longrightarrow> Let assn trm = Let bs s \<longrightarrow> fl assn trm = fl bs s)") |
|
76 apply (subst substrec.simps(3)) apply simp |
|
77 apply (subst substrec.simps(3)) apply simp |
|
78 apply metis |
|
79 apply (subst substrec.simps(4)) apply simp |
|
80 apply (subst substrec.simps(4)) apply simp_all |
|
81 done |
|
82 |
|
83 lemma [fundef_cong]: |
|
84 "(\<And>x s as. t = ACons x s as \<Longrightarrow> fac x s as = fac' x s as) \<Longrightarrow> |
|
85 substarec fac t = substarec fac' t" |
|
86 by (rule_tac y="t" in trm_assn.exhaust(2)) simp_all |
|
87 |
|
88 function |
|
89 subst :: "name \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> trm" |
|
90 and substa :: "name \<Rightarrow> trm \<Rightarrow> assn \<Rightarrow> assn" |
|
91 where |
|
92 [simp del]: "subst y z t = substrec |
|
93 (\<lambda>l r. App (subst y z l) (subst y z r)) |
|
94 (\<lambda>as t. Let (substa y z as) (subst y z t)) |
|
95 (Let (ACons y (Var y) ANil) (Var y)) y z t" |
|
96 | [simp del]: "substa y z t = substarec |
|
97 (\<lambda>x t as. ACons x (subst y z t) (substa y z as)) t" |
|
98 by pat_completeness auto |
|
99 |
|
100 termination by lexicographic_order |
|
101 |
|
102 lemma testl: |
|
103 assumes a: "\<exists>y. f x = Inl y" |
|
104 shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl ((p \<bullet> f) (p \<bullet> x))" |
|
105 using a |
|
106 apply clarify |
|
107 apply(frule_tac p="p" in permute_boolI) |
|
108 apply(simp (no_asm_use) only: eqvts) |
|
109 apply(subst (asm) permute_fun_app_eq) |
|
110 back |
|
111 apply(simp) |
|
112 done |
|
113 |
|
114 lemma testr: |
|
115 assumes a: "\<exists>y. f x = Inr y" |
|
116 shows "(p \<bullet> (Sum_Type.Projr (f x))) = Sum_Type.Projr ((p \<bullet> f) (p \<bullet> x))" |
|
117 using a |
|
118 apply clarify |
|
119 apply(frule_tac p="p" in permute_boolI) |
|
120 apply(simp (no_asm_use) only: eqvts) |
|
121 apply(subst (asm) permute_fun_app_eq) |
|
122 back |
|
123 apply(simp) |
|
124 done |
|
125 |
|
126 lemma permute_move: "p \<bullet> x = y \<longleftrightarrow> x = -p \<bullet> y" |
|
127 by (metis eqvt_bound unpermute_def) |
|
128 |
|
129 lemma "subst_substa_graph x t \<Longrightarrow> subst_substa_graph (p \<bullet> x) (p \<bullet> t)" |
|
130 proof (induct arbitrary: p rule: subst_substa_graph.induct) |
|
131 fix f y z t p |
|
132 assume a: "\<And>t1 t2 p. t = App t1 t2 \<Longrightarrow> subst_substa_graph (p \<bullet> Inl (y, z, t1)) (p \<bullet> f (Inl (y, z, t1)))" |
|
133 and b: "\<And>t1 t2 p. t = App t1 t2 \<Longrightarrow> subst_substa_graph (p \<bullet> Inl (y, z, t2)) (p \<bullet> f (Inl (y, z, t2)))" |
|
134 and c: "\<And>as s p. t = Let.Let as s \<Longrightarrow> subst_substa_graph (p \<bullet> Inr (y, z, as)) (p \<bullet> f (Inr (y, z, as)))" |
|
135 and d: "\<And>as s p. t = Let.Let as s \<Longrightarrow> subst_substa_graph (p \<bullet> Inl (y, z, s)) (p \<bullet> f (Inl (y, z, s)))" |
|
136 then show "subst_substa_graph (p \<bullet> Inl (y, z, t)) |
|
137 (p \<bullet> Inl (substrec |
|
138 (\<lambda>l r. App (Sum_Type.Projl (f (Inl (y, z, l)))) |
|
139 (Sum_Type.Projl (f (Inl (y, z, r))))) |
|
140 (\<lambda>as t. Let.Let (Sum_Type.Projr (f (Inr (y, z, as)))) |
|
141 (Sum_Type.Projl (f (Inl (y, z, t))))) |
|
142 (Let.Let (ACons y (Var y) ANil) (Var y)) y z t))" |
|
143 proof (rule_tac y="t" and c="(t, y, z)" in trm_assn.strong_exhaust(1)) |
|
144 fix name |
|
145 assume "t = Var name" |
|
146 then show ?thesis |
|
147 apply (simp add: eqvts split del: if_splits) |
|
148 apply (simp only: trm_assn.perm_simps) |
|
149 apply (rule subst_substa_graph.intros(1)[of "Var (p \<bullet> name)" "p \<bullet> y" "p \<bullet> z", simplified]) |
|
150 by simp_all |
|
151 next |
|
152 fix trm1 trm2 |
|
153 assume e: "t = App trm1 trm2" |
|
154 then show ?thesis |
|
155 apply (simp add: eqvts) |
|
156 apply (subst testl) back |
|
157 apply (rule subst_substa_graph.cases[OF a[OF e, of 0, simplified]]) |
|
158 apply metis apply simp |
|
159 apply (subst testl) back |
|
160 apply (rule subst_substa_graph.cases[OF b[OF e, of 0, simplified]]) |
|
161 apply metis apply (simp add: eqvts) |
|
162 apply (simp only: Inl_eqvt) apply simp |
|
163 apply (rule subst_substa_graph.intros(1)[of "App (p \<bullet> trm1) (p \<bullet> trm2)" "p \<bullet> y" "p \<bullet> z", simplified]) |
|
164 apply simp_all apply clarify |
|
165 using a[OF e, simplified Inl_eqvt, simplified] |
|
166 apply (metis (lifting) Inl_eqvt permute_fun_app_eq permute_prod.simps) |
|
167 apply clarify |
|
168 using b[OF e, simplified Inl_eqvt, simplified] |
|
169 by (metis (lifting) Inl_eqvt permute_fun_app_eq permute_prod.simps) |
|
170 next |
|
171 fix assn trm |
|
172 assume e: "t = Let.Let assn trm" and f: "set (bn assn) \<sharp>* (t, y, z)" |
|
173 then show ?thesis |
|
174 apply (simp add: eqvts) |
|
175 apply (simp only: permute_fun_def) |
|
176 apply (simp only: eqvts permute_minus_cancel) |
|
177 apply (case_tac "(\<forall>bs s. set (bn bs) \<sharp>* (Let.Let bs s, p \<bullet> y, p \<bullet> z) \<longrightarrow> |
|
178 Let.Let (p \<bullet> assn) (p \<bullet> trm) = Let.Let bs s \<longrightarrow> |
|
179 Let.Let (p \<bullet> Sum_Type.Projr (f (Inr (y, z, - p \<bullet> p \<bullet> assn)))) |
|
180 (p \<bullet> Sum_Type.Projl (f (Inl (y, z, - p \<bullet> p \<bullet> trm)))) = |
|
181 Let.Let (p \<bullet> Sum_Type.Projr (f (Inr (y, z, - p \<bullet> bs)))) |
|
182 (p \<bullet> Sum_Type.Projl (f (Inl (y, z, - p \<bullet> s)))))") |
|
183 prefer 2 |
|
184 apply (subst substrec.simps(4)) |
|
185 apply rule |
|
186 apply (simp add: fresh_star_Pair) |
|
187 apply (intro conjI) |
|
188 apply (metis fresh_star_permute_iff set_eqvt trm_assn.fv_bn_eqvt(4) trm_assn.perm_simps(3)) |
|
189 apply (metis (lifting) fresh_star_permute_iff set_eqvt trm_assn.fv_bn_eqvt(4)) |
|
190 apply (metis (lifting) fresh_star_permute_iff set_eqvt trm_assn.fv_bn_eqvt(4)) |
|
191 apply assumption |
|
192 prefer 2 |
|
193 apply (subst substrec.simps(3)) |
|
194 apply rule |
|
195 apply (simp add: fresh_star_Pair) |
|
196 apply (intro conjI) |
|
197 apply (metis fresh_star_permute_iff set_eqvt trm_assn.fv_bn_eqvt(4) trm_assn.perm_simps(3)) |
|
198 apply (metis (lifting) fresh_star_permute_iff set_eqvt trm_assn.fv_bn_eqvt(4)) |
|
199 apply (metis (lifting) fresh_star_permute_iff set_eqvt trm_assn.fv_bn_eqvt(4)) |
|
200 apply assumption |
|
201 (* The following subgoal is motivated by: |
|
202 thm subst_substa_graph.intros(1)[of "Let (p \<bullet> assn) (p \<bullet> trm)" "p \<bullet> y" "p \<bullet> z" "(p \<bullet> f)", simplified]*) |
|
203 apply (subgoal_tac "subst_substa_graph (Inl (p \<bullet> y, p \<bullet> z, Let.Let (p \<bullet> assn) (p \<bullet> trm))) |
|
204 (Inl (substrec |
|
205 (\<lambda>l r. App (Sum_Type.Projl ((p \<bullet> f) (Inl (p \<bullet> y, p \<bullet> z, l)))) |
|
206 (Sum_Type.Projl ((p \<bullet> f) (Inl (p \<bullet> y, p \<bullet> z, r))))) |
|
207 (\<lambda>as t. Let.Let (Sum_Type.Projr ((p \<bullet> f) (Inr (p \<bullet> y, p \<bullet> z, as)))) |
|
208 (Sum_Type.Projl ((p \<bullet> f) (Inl (p \<bullet> y, p \<bullet> z, t))))) |
|
209 (Let.Let (ACons (p \<bullet> y) (Var (p \<bullet> y)) ANil) (Var (p \<bullet> y))) (p \<bullet> y) (p \<bullet> z) |
|
210 (Let.Let (p \<bullet> assn) (p \<bullet> trm))))") |
|
211 apply (subst (asm) substrec.simps(3)) |
|
212 apply rule |
|
213 apply (simp add: fresh_star_Pair) |
|
214 apply (intro conjI) |
|
215 apply (metis fresh_star_permute_iff set_eqvt trm_assn.fv_bn_eqvt(4) trm_assn.perm_simps(3)) |
|
216 apply (metis (lifting) fresh_star_permute_iff set_eqvt trm_assn.fv_bn_eqvt(4)) |
|
217 apply (metis (lifting) fresh_star_permute_iff set_eqvt trm_assn.fv_bn_eqvt(4)) |
|
218 (* We don't have equivariance of Projl/Projr at the arbitrary 'bs' point *) |
|
219 defer |
|
220 apply (subst testr) back |
|
221 apply (rule subst_substa_graph.cases[OF c[OF e, of 0, simplified]]) |
|
222 apply simp apply simp |
|
223 apply (subst testl) back |
|
224 apply (rule subst_substa_graph.cases[OF d[OF e, of 0, simplified]]) |
|
225 apply simp apply simp apply simp |
|
226 apply (rule subst_substa_graph.intros(1)[of "Let (p \<bullet> assn) (p \<bullet> trm)" "p \<bullet> y" "p \<bullet> z" "(p \<bullet> f)", simplified]) |
|
227 apply simp apply simp (* These two should follow by d for arbitrary 'as' point *) |
|
228 defer defer |
|
229 sorry |
|
230 qed |
|
231 next |
|
232 fix f y z t p |
|
233 show "subst_substa_graph (p \<bullet> Inr (y, z, t)) (p \<bullet> Inr (substarec (\<lambda>x t as. ACons |
|
234 x (Sum_Type.Projl (f (Inl (y, z, t)))) (Sum_Type.Projr (f (Inr (y, z, as))))) t))" |
|
235 sorry |
|
236 qed |
|
237 |
|
238 (* Will follow from above and accp *) |
|
239 lemma [eqvt]: |
|
240 "p \<bullet> (subst y z t) = subst (p \<bullet> y) (p \<bullet> z) (p \<bullet> t)" |
|
241 "p \<bullet> (substa y z t2) = substa (p \<bullet> y) (p \<bullet> z) (p \<bullet> t2)" |
|
242 sorry |
|
243 |
|
244 lemma substa_simps[simp]: |
|
245 "substa y z ANil = ANil" |
|
246 "substa y z (ACons x t as) = ACons x (subst y z t) (substa y z as)" |
|
247 apply (subst substa.simps) apply (subst substarec.simps) apply rule |
|
248 apply (subst substa.simps) apply (subst substarec.simps) apply rule |
|
249 done |
|
250 |
|
251 lemma bn_substa: "bn (substa y z t) = bn t" |
|
252 by (induct t rule: trm_assn.inducts(2)) (simp_all add: trm_assn.bn_defs) |
|
253 |
|
254 lemma fresh_fun_eqvt_app3: |
|
255 assumes e: "eqvt f" |
|
256 shows "\<lbrakk>a \<sharp> x; a \<sharp> y; a \<sharp> z\<rbrakk> \<Longrightarrow> a \<sharp> f x y z" |
|
257 using fresh_fun_eqvt_app[OF e] fresh_fun_app by (metis (lifting, full_types)) |
|
258 |
|
259 lemma |
|
260 "subst y z (Var x) = (if (y = x) then z else (Var x))" |
|
261 "subst y z (App l r) = App (subst y z l) (subst y z r)" |
|
262 "set (bn as) \<sharp>* (Let as t, y, z) \<Longrightarrow> subst y z (Let as t) = Let (substa y z as) (subst y z t)" |
|
263 apply (subst subst.simps) apply (subst substrec.simps) apply rule |
|
264 apply (subst subst.simps) apply (subst substrec.simps) apply rule |
|
265 apply (subst subst.simps) apply (subst substrec.simps) apply auto |
|
266 apply (subst (asm) Abs_eq_iff2) |
|
267 apply clarify |
|
268 apply (simp add: alphas bn_substa) |
|
269 apply (rule_tac s="p \<bullet> ([bn as]lst. (substa y z as, subst y z t))" in trans) |
|
270 apply (rule sym) |
|
271 defer |
|
272 apply (simp add: eqvts) |
|
273 apply (subgoal_tac "supp p \<sharp>* y") |
|
274 apply (subgoal_tac "supp p \<sharp>* z") |
|
275 apply (simp add: perm_supp_eq) |
|
276 apply (simp add: fresh_Pair fresh_star_def) |
|
277 apply blast |
|
278 apply (simp add: fresh_Pair fresh_star_def) |
|
279 apply blast |
|
280 apply (rule perm_supp_eq) |
|
281 apply (simp add: fresh_star_Pair) |
|
282 apply (simp add: fresh_star_def Abs_fresh_iff) |
|
283 apply (auto) |
|
284 apply (simp add: bn_substa fresh_Pair) |
|
285 apply (rule) |
|
286 apply (rule fresh_fun_eqvt_app3[of substa]) |
|
287 apply (simp add: eqvt_def eqvts_raw) |
|
288 apply (metis (lifting) Diff_partition Un_iff) |
|
289 apply (metis (lifting) Diff_partition Un_iff) |
|
290 apply (simp add: fresh_def trm_assn.supp) |
|
291 apply (metis (lifting) DiffI UnI1 supp_Pair) |
|
292 apply (rule fresh_fun_eqvt_app3[of subst]) |
|
293 apply (simp add: eqvt_def eqvts_raw) |
|
294 apply (metis (lifting) Diff_partition Un_iff) |
|
295 apply (metis (lifting) Diff_partition Un_iff) |
|
296 apply (simp add: fresh_def trm_assn.supp) |
|
297 by (metis Diff_iff Un_iff supp_Pair) |
|
298 |
|
299 end |