92 apply(simp add: supp_Abs) |
91 apply(simp add: supp_Abs) |
93 apply(rule impI) |
92 apply(rule impI) |
94 apply(subgoal_tac "x \<notin> supp \<theta>") |
93 apply(subgoal_tac "x \<notin> supp \<theta>") |
95 prefer 2 |
94 prefer 2 |
96 apply(auto simp add: fresh_star_def fresh_def)[1] |
95 apply(auto simp add: fresh_star_def fresh_def)[1] |
97 apply(subgoal_tac "x \<in> supp t") |
96 apply(subgoal_tac "x \<in> supp T") |
98 using supp_subst |
97 using supp_subst |
99 apply(blast) |
98 apply(blast) |
100 using supp_subst |
99 using supp_subst |
101 apply(blast) |
100 apply(blast) |
102 apply clarify |
101 apply clarify |
103 apply (simp add: subst.eqvt) |
102 apply (simp add: subst.eqvt) |
104 apply (subst Abs_eq_iff) |
103 apply (subst Abs_eq_iff) |
105 apply (rule_tac x="0::perm" in exI) |
104 apply (rule_tac x="0::perm" in exI) |
106 apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'") |
105 apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'") |
107 apply (simp add: alphas fresh_star_zero) |
106 apply (simp add: alphas fresh_star_zero) |
108 apply (subgoal_tac "\<And>x. x \<in> supp (subst \<theta>' (p \<bullet> t)) \<Longrightarrow> x \<in> p \<bullet> atom ` fset xs \<longleftrightarrow> x \<in> atom ` fset xsa") |
107 apply (subgoal_tac "\<And>x. x \<in> supp (subst \<theta>' (p \<bullet> T)) \<Longrightarrow> x \<in> p \<bullet> atom ` fset Xs \<longleftrightarrow> x \<in> atom ` fset Xsa") |
109 apply blast |
108 apply blast |
110 apply (subgoal_tac "x \<in> supp(p \<bullet> \<theta>', p \<bullet> t)") |
109 apply (subgoal_tac "x \<in> supp(p \<bullet> \<theta>', p \<bullet> T)") |
111 apply (simp add: supp_Pair eqvts eqvts_raw) |
110 apply (simp add: supp_Pair eqvts eqvts_raw) |
112 apply auto[1] |
111 apply auto[1] |
113 apply (subgoal_tac "(atom ` fset (p \<bullet> xs)) \<sharp>* \<theta>'") |
112 apply (subgoal_tac "(atom ` fset (p \<bullet> Xs)) \<sharp>* \<theta>'") |
114 apply (simp add: fresh_star_def fresh_def) |
113 apply (simp add: fresh_star_def fresh_def) |
115 apply(drule_tac p1="p" in iffD2[OF fresh_star_permute_iff]) |
114 apply(drule_tac p1="p" in iffD2[OF fresh_star_permute_iff]) |
116 apply (simp add: eqvts eqvts_raw) |
115 apply (simp add: eqvts eqvts_raw) |
117 apply (simp add: fresh_star_def fresh_def) |
116 apply (simp add: fresh_star_def fresh_def) |
118 apply (drule subsetD[OF supp_subst]) |
117 apply (drule subsetD[OF supp_subst]) |
123 done |
122 done |
124 |
123 |
125 text {* Some Tests about Alpha-Equality *} |
124 text {* Some Tests about Alpha-Equality *} |
126 |
125 |
127 lemma |
126 lemma |
128 shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))" |
127 shows "All [{|a, b|}].((Var a) \<rightarrow> (Var b)) = All [{|b, a|}]. ((Var a) \<rightarrow> (Var b))" |
129 apply(simp add: Abs_eq_iff) |
128 apply(simp add: Abs_eq_iff) |
130 apply(rule_tac x="0::perm" in exI) |
129 apply(rule_tac x="0::perm" in exI) |
131 apply(simp add: alphas fresh_star_def ty.supp supp_at_base) |
130 apply(simp add: alphas fresh_star_def ty.supp supp_at_base) |
132 done |
131 done |
133 |
132 |
134 lemma |
133 lemma |
135 shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var b) (Var a))" |
134 shows "All [{|a, b|}].((Var a) \<rightarrow> (Var b)) = All [{|a, b|}].((Var b) \<rightarrow> (Var a))" |
136 apply(simp add: Abs_eq_iff) |
135 apply(simp add: Abs_eq_iff) |
137 apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI) |
136 apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI) |
138 apply(simp add: alphas fresh_star_def supp_at_base ty.supp) |
137 apply(simp add: alphas fresh_star_def supp_at_base ty.supp) |
139 done |
138 done |
140 |
139 |
141 lemma |
140 lemma |
142 shows "All {|a, b, c|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var a) (Var b))" |
141 shows "All [{|a, b, c|}].((Var a) \<rightarrow> (Var b)) = All [{|a, b|}].((Var a) \<rightarrow> (Var b))" |
143 apply(simp add: Abs_eq_iff) |
142 apply(simp add: Abs_eq_iff) |
144 apply(rule_tac x="0::perm" in exI) |
143 apply(rule_tac x="0::perm" in exI) |
145 apply(simp add: alphas fresh_star_def ty.supp supp_at_base) |
144 apply(simp add: alphas fresh_star_def ty.supp supp_at_base) |
146 done |
145 done |
147 |
146 |
148 lemma |
147 lemma |
149 assumes a: "a \<noteq> b" |
148 assumes a: "a \<noteq> b" |
150 shows "\<not>(All {|a, b|} (Fun (Var a) (Var b)) = All {|c|} (Fun (Var c) (Var c)))" |
149 shows "\<not>(All [{|a, b|}].((Var a) \<rightarrow> (Var b)) = All [{|c|}].((Var c) \<rightarrow> (Var c)))" |
151 using a |
150 using a |
152 apply(simp add: Abs_eq_iff) |
151 apply(simp add: Abs_eq_iff) |
153 apply(clarify) |
152 apply(clarify) |
154 apply(simp add: alphas fresh_star_def ty.supp supp_at_base) |
153 apply(simp add: alphas fresh_star_def ty.supp supp_at_base) |
155 apply auto |
154 apply auto |
156 done |
155 done |
157 |
156 |
158 |
157 |
|
158 text {* HERE *} |
|
159 |
|
160 fun |
|
161 compose::"Subst \<Rightarrow> Subst \<Rightarrow> Subst" ("_ \<circ> _" [100,100] 100) |
|
162 where |
|
163 "\<theta>\<^isub>1 \<circ> [] = \<theta>\<^isub>1" |
|
164 | "\<theta>\<^isub>1 \<circ> ((X,T)#\<theta>\<^isub>2) = (X,\<theta>\<^isub>1<T>)#(\<theta>\<^isub>1 \<circ> \<theta>\<^isub>2)" |
|
165 |
|
166 lemma compose_eqvt: |
|
167 fixes \<theta>1 \<theta>2::"Subst" |
|
168 shows "(p \<bullet> (\<theta>1 \<circ> \<theta>2)) = ((p \<bullet> \<theta>1) \<circ> (p \<bullet> \<theta>2))" |
|
169 apply(induct \<theta>2) |
|
170 apply(auto simp add: subst.eqvt) |
|
171 done |
|
172 |
|
173 lemma compose_ty: |
|
174 fixes \<theta>1 :: "Subst" |
|
175 and \<theta>2 :: "Subst" |
|
176 and T :: "ty" |
|
177 shows "\<theta>1<\<theta>2<T>> = (\<theta>1\<circ>\<theta>2)<T>" |
|
178 proof (induct T rule: ty.induct) |
|
179 case (Var X) |
|
180 have "\<theta>1<lookup \<theta>2 X> = lookup (\<theta>1\<circ>\<theta>2) X" |
|
181 by (induct \<theta>2) (auto) |
|
182 then show ?case by simp |
|
183 next |
|
184 case (Fun T1 T2) |
|
185 then show ?case by simp |
|
186 qed |
|
187 |
|
188 fun |
|
189 dom :: "Subst \<Rightarrow> name fset" |
|
190 where |
|
191 "dom [] = {||}" |
|
192 | "dom ((X,T)#\<theta>) = {|X|} |\<union>| dom \<theta>" |
|
193 |
|
194 lemma dom_eqvt[eqvt]: |
|
195 shows "(p \<bullet> dom \<theta>) = dom (p \<bullet> \<theta>)" |
|
196 apply(induct \<theta> rule: dom.induct) |
|
197 apply(simp_all) |
|
198 done |
|
199 |
|
200 nominal_primrec |
|
201 ftv :: "ty \<Rightarrow> name fset" |
|
202 where |
|
203 "ftv (Var X) = {|X|}" |
|
204 | "ftv (T1 \<rightarrow> T2) = (ftv T1) |\<union>| (ftv T2)" |
|
205 unfolding eqvt_def ftv_graph_def |
|
206 apply (rule, perm_simp, rule) |
|
207 apply(auto)[2] |
|
208 apply(rule_tac y="x" in ty.exhaust) |
|
209 apply(blast) |
|
210 apply(blast) |
|
211 apply(simp_all) |
|
212 done |
|
213 |
|
214 termination (eqvt) |
|
215 by lexicographic_order |
|
216 |
|
217 lemma s1: |
|
218 fixes T::"ty" |
|
219 shows "(X \<leftrightarrow> Y) \<bullet> T = [(X, Var Y),(Y, Var X)]<T>" |
|
220 apply(induct T rule: ty.induct) |
|
221 apply(simp_all) |
|
222 done |
|
223 |
|
224 lemma s2: |
|
225 fixes T::"ty" |
|
226 shows "[]<T> = T" |
|
227 apply(induct T rule: ty.induct) |
|
228 apply(simp_all) |
|
229 done |
|
230 |
|
231 lemma perm_struct_induct_name[case_names pure zero swap]: |
|
232 assumes pure: "supp p \<subseteq> atom ` (UNIV::name set)" |
|
233 and zero: "P 0" |
|
234 and swap: "\<And>p a b::name. \<lbrakk>P p; a \<noteq> b\<rbrakk> \<Longrightarrow> P ((a \<leftrightarrow> b) + p)" |
|
235 shows "P p" |
|
236 apply(rule_tac S="supp p \<inter> atom ` (UNIV::name set)" in perm_struct_induct) |
|
237 using pure |
|
238 apply(auto)[1] |
|
239 apply(rule zero) |
|
240 apply(auto) |
|
241 apply(simp add: flip_def[symmetric]) |
|
242 apply(rule swap) |
|
243 apply(auto) |
|
244 done |
|
245 |
|
246 lemma s3: |
|
247 fixes T::"ty" |
|
248 assumes "supp p \<subseteq> atom ` (UNIV::name set)" |
|
249 shows "\<exists>\<theta>. p \<bullet> T = \<theta><T>" |
|
250 apply(induct p rule: perm_struct_induct_name) |
|
251 apply(rule assms) |
|
252 apply(simp) |
|
253 apply(rule_tac x="[]" in exI) |
|
254 apply(simp add: s2) |
|
255 apply(clarify) |
|
256 apply(simp) |
|
257 apply(rule_tac x="[(a, Var b),(b, Var a)] \<circ> \<theta>" in exI) |
|
258 apply(simp add: compose_ty[symmetric]) |
|
259 apply(simp add: s1) |
|
260 done |
|
261 |
|
262 lemma s4: |
|
263 fixes x::"'a::fs" |
|
264 assumes "supp x \<subseteq> atom ` (UNIV::name set)" |
|
265 shows "\<exists>q. p \<bullet> x = q \<bullet> x \<and> supp q \<subseteq> atom ` (UNIV::name set)" |
|
266 apply(induct p rule: perm_simple_struct_induct) |
|
267 apply(rule_tac x="0" in exI) |
|
268 apply(auto)[1] |
|
269 apply(simp add: supp_zero_perm) |
|
270 apply(auto)[1] |
|
271 apply(case_tac "supp (a \<rightleftharpoons> b) \<subseteq> range atom") |
|
272 apply(rule_tac x="(a \<rightleftharpoons> b) + q" in exI) |
|
273 apply(simp) |
|
274 apply(rule subset_trans) |
|
275 apply(rule supp_plus_perm) |
|
276 apply(simp) |
|
277 apply(rule_tac x="q" in exI) |
|
278 apply(simp) |
|
279 apply(rule swap_fresh_fresh) |
|
280 apply(simp add: fresh_permute_left) |
|
281 apply(subst perm_supp_eq) |
|
282 apply(simp add: supp_swap) |
|
283 apply(simp add: supp_minus_perm) |
|
284 apply(simp add: fresh_star_def fresh_def) |
|
285 apply(simp add: supp_atom) |
|
286 apply(auto)[1] |
|
287 apply (metis atom_eqvt image_iff rangeI subsetD swap_atom_simps(2)) |
|
288 apply(simp add: supp_swap) |
|
289 using assms |
|
290 apply(simp add: fresh_def) |
|
291 apply(auto)[1] |
|
292 apply (metis atom_eqvt image_iff rangeI subsetD swap_atom_simps(2)) |
|
293 apply(simp add: fresh_permute_left) |
|
294 apply(subst perm_supp_eq) |
|
295 apply(simp add: supp_swap) |
|
296 apply(simp add: supp_minus_perm) |
|
297 apply(simp add: fresh_star_def fresh_def) |
|
298 apply(simp add: supp_atom) |
|
299 apply(auto)[1] |
|
300 apply (metis atom_eqvt image_iff rangeI subsetD swap_atom_simps(2)) |
|
301 apply(simp add: supp_swap) |
|
302 using assms |
|
303 apply(simp add: fresh_def) |
|
304 apply(auto)[1] |
|
305 apply (metis atom_eqvt image_iff rangeI subsetD swap_atom_simps(2)) |
|
306 done |
|
307 |
|
308 lemma s5: |
|
309 fixes T::"ty" |
|
310 shows "supp T \<subseteq> atom ` (UNIV::name set)" |
|
311 apply(induct T rule: ty.induct) |
|
312 apply(auto simp add: ty.supp supp_at_base) |
|
313 done |
|
314 |
|
315 function |
|
316 generalises :: "ty \<Rightarrow> tys \<Rightarrow> bool" ("_ \<prec>\<prec> _") |
|
317 where |
|
318 "T \<prec>\<prec> All [Xs].T' \<longleftrightarrow> (\<exists>\<theta>. \<theta><T'> = T)" |
|
319 apply auto[1] |
|
320 apply (rule_tac y="b" in tys.exhaust) |
|
321 apply auto[1] |
|
322 apply(simp) |
|
323 apply(clarify) |
|
324 apply(rule iffI) |
|
325 apply(clarify) |
|
326 apply(drule sym) |
|
327 apply(simp add: Abs_eq_iff2) |
|
328 apply(simp add: alphas) |
|
329 apply(clarify) |
|
330 using s4[OF s5] |
|
331 apply - |
|
332 apply(drule_tac x="p" in meta_spec) |
|
333 apply(drule_tac x="T'a" in meta_spec) |
|
334 apply(clarify) |
|
335 apply(simp) |
|
336 using s3 |
|
337 apply - |
|
338 apply(drule_tac x="q" in meta_spec) |
|
339 apply(drule_tac x="T'a" in meta_spec) |
|
340 apply(drule meta_mp) |
|
341 apply(simp) |
|
342 apply(clarify) |
|
343 apply(simp) |
|
344 apply(rule_tac x="\<theta> \<circ> \<theta>'" in exI) |
|
345 apply(simp add: compose_ty) |
|
346 apply(auto) |
|
347 apply(simp add: Abs_eq_iff2) |
|
348 apply(simp add: alphas) |
|
349 apply(clarify) |
|
350 apply(drule_tac x="p" in meta_spec) |
|
351 apply(drule_tac x="T'" in meta_spec) |
|
352 apply(clarify) |
|
353 apply(simp) |
|
354 apply(drule_tac x="q" in meta_spec) |
|
355 apply(drule_tac x="T'" in meta_spec) |
|
356 apply(drule meta_mp) |
|
357 apply(simp) |
|
358 apply(clarify) |
|
359 apply(simp) |
|
360 apply(rule_tac x="\<theta> \<circ> \<theta>'" in exI) |
|
361 apply(simp add: compose_ty) |
|
362 done |
|
363 |
|
364 |
|
365 |
|
366 |
159 |
367 |
160 |
368 |
161 end |
369 end |