14 thm alpha_weird_raw.intros[no_vars] |
14 thm alpha_weird_raw.intros[no_vars] |
15 thm fv_weird_raw.simps[no_vars] |
15 thm fv_weird_raw.simps[no_vars] |
16 (* Potential problem: Is it correct that in the fv-function |
16 (* Potential problem: Is it correct that in the fv-function |
17 the first two terms are created? Should be ommitted. Also |
17 the first two terms are created? Should be ommitted. Also |
18 something wrong with the permutations. *) |
18 something wrong with the permutations. *) |
|
19 |
|
20 lemma "alpha_weird_raw a b \<Longrightarrow> alpha_weird_raw (p \<bullet> a) (p \<bullet> b)" |
|
21 apply (erule alpha_weird_raw.induct) |
|
22 defer |
|
23 apply (simp add: alpha_weird_raw.intros) |
|
24 apply (simp add: alpha_weird_raw.intros) |
|
25 apply (simp only: permute_weird_raw.simps) |
|
26 apply (rule alpha_weird_raw.intros) |
|
27 apply (erule exi[of _ _ "p"]) |
|
28 apply (erule exi[of _ _ "p"]) |
|
29 apply (erule exi[of _ _ "p"]) |
|
30 apply (erule exi[of _ _ "p"]) |
|
31 apply (erule conjE)+ |
|
32 apply (rule conjI) |
|
33 apply (erule alpha_gen_compose_eqvt[of _ _ _ _ "p"]) |
|
34 apply (simp add: eqvts) |
|
35 apply (simp add: eqvts) |
|
36 apply (rule conjI) |
|
37 defer |
|
38 apply (erule alpha_gen_compose_eqvt[of _ _ _ _ "p"]) |
|
39 apply (simp add: eqvts) |
|
40 apply (simp add: eqvts) |
|
41 apply (rule conjI) |
|
42 defer |
|
43 apply (simp add: supp_eqvt[symmetric] inter_eqvt[symmetric] empty_eqvt) |
|
44 apply(simp add: alpha_gen.simps) |
|
45 apply(erule conjE)+ |
|
46 apply(rule conjI) |
|
47 apply(rule_tac ?p1="- p" in permute_eq_iff[THEN iffD1]) |
|
48 apply (simp add: eqvts) |
|
49 apply(rule conjI) |
|
50 apply(rule_tac ?p1="- p" in fresh_star_permute_iff[THEN iffD1]) |
|
51 apply (simp add: eqvts add_perm_eqvt) |
|
52 apply (simp add: permute_eqvt[symmetric]) |
|
53 done |
19 |
54 |
20 primrec |
55 primrec |
21 fv_weird |
56 fv_weird |
22 where |
57 where |
23 "fv_weird (WBind_raw x y p1 p2 p3) = |
58 "fv_weird (WBind_raw x y p1 p2 p3) = |
207 "bv3 ANil = {}" |
242 "bv3 ANil = {}" |
208 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)" |
243 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)" |
209 |
244 |
210 (* example 4 from Terms.thy *) |
245 (* example 4 from Terms.thy *) |
211 |
246 |
212 (* fv_eqvt does not work, we need to repaire defined permute functions... |
247 (* fv_eqvt does not work, we need to repaire defined permute functions |
213 nominal_datatype trm4 = |
248 defined fv and defined alpha... *) |
|
249 (*nominal_datatype trm4 = |
214 Vr4 "name" |
250 Vr4 "name" |
215 | Ap4 "trm4" "trm4 list" |
251 | Ap4 "trm4" "trm4 list" |
216 | Lm4 x::"name" t::"trm4" bind x in t |
252 | Lm4 x::"name" t::"trm4" bind x in t |
217 |
253 |
218 thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars] |
254 thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars] |
219 thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars] |
255 thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]*) |
220 |
256 |
221 (* example 5 from Terms.thy *) |
257 (* example 5 from Terms.thy *) |
222 |
258 |
223 nominal_datatype trm5 = |
259 nominal_datatype trm5 = |
224 Vr5 "name" |
260 Vr5 "name" |