11 | WP "weird" "weird" |
11 | WP "weird" "weird" |
12 |
12 |
13 thm permute_weird_raw.simps[no_vars] |
13 thm permute_weird_raw.simps[no_vars] |
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 |
16 (* Potential problem: Is it correct that in the fv-function |
17 abbreviation "fv_weird \<equiv> fv_weird_raw" |
17 the first two terms are created? Should be ommitted. Also |
18 abbreviation "alpha_weird \<equiv> alpha_weird_raw" |
18 something wrong with the permutations. *) |
19 |
19 |
20 (* |
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 |
|
54 |
|
55 primrec |
|
56 fv_weird |
|
57 where |
|
58 "fv_weird (WBind_raw x y p1 p2 p3) = |
|
59 (fv_weird p1 - {atom x}) \<union> (fv_weird p2 - ({atom x} \<union> {atom y})) \<union> (fv_weird p3 - {atom y})" |
|
60 | "fv_weird (WV_raw x) = {atom x}" |
|
61 | "fv_weird (WP_raw p1 p2) = (fv_weird p1 \<union> fv_weird p2)" |
|
62 |
21 inductive |
63 inductive |
22 alpha_weird |
64 alpha_weird |
23 where |
65 where |
24 "\<exists>p1 p2. |
66 "\<exists>p1 p2. |
25 ({atom y}, w3) \<approx>gen alpha_weird fv_weird p2 ({atom ya}, w3a) \<and> |
67 ({atom y}, w3) \<approx>gen alpha_weird fv_weird p2 ({atom ya}, w3a) \<and> |
27 ({atom x}, w1) \<approx>gen alpha_weird fv_weird p1 ({atom xa}, w1a) \<and> |
69 ({atom x}, w1) \<approx>gen alpha_weird fv_weird p1 ({atom xa}, w1a) \<and> |
28 supp p1 \<inter> supp p2 = {} \<Longrightarrow> |
70 supp p1 \<inter> supp p2 = {} \<Longrightarrow> |
29 alpha_weird (WBind_raw x y w1 w2 w3) (WBind_raw xa ya w1a w2a w3a)" |
71 alpha_weird (WBind_raw x y w1 w2 w3) (WBind_raw xa ya w1a w2a w3a)" |
30 | "x = xa \<Longrightarrow> alpha_weird (WV_raw x) (WV_raw xa)" |
72 | "x = xa \<Longrightarrow> alpha_weird (WV_raw x) (WV_raw xa)" |
31 | "alpha_weird w2 w2a \<and> alpha_weird w1 w1a \<Longrightarrow> alpha_weird (WP_raw w1 w2) (WP_raw w1a w2a)" |
73 | "alpha_weird w2 w2a \<and> alpha_weird w1 w1a \<Longrightarrow> alpha_weird (WP_raw w1 w2) (WP_raw w1a w2a)" |
32 *) |
74 |
33 |
75 (* |
34 abbreviation "WBind \<equiv> WBind_raw" |
76 abbreviation "WBind \<equiv> WBind_raw" |
35 abbreviation "WP \<equiv> WP_raw" |
77 abbreviation "WP \<equiv> WP_raw" |
36 abbreviation "WV \<equiv> WV_raw" |
78 abbreviation "WV \<equiv> WV_raw" |
37 |
79 |
38 lemma test: |
80 lemma test: |
39 assumes a: "distinct [x, y, z]" |
81 assumes a: "distinct [x, y, z]" |
40 shows "alpha_weird (WBind x y (WP (WV x) (WV z)) (WP (WV x) (WV y)) (WP (WV z) (WV y))) |
82 shows "alpha_weird (WBind x y (WP (WV x) (WV z)) (WP (WV x) (WV y)) (WP (WV z) (WV y))) |
41 (WBind y x (WP (WV y) (WV z)) (WP (WV y) (WV x)) (WP (WV z) (WV x)))" |
83 (WBind y x (WP (WV y) (WV z)) (WP (WV y) (WV x)) (WP (WV z) (WV x)))" |
42 apply(rule_tac alpha_weird_raw.intros) |
84 apply(rule_tac alpha_weird.intros) |
43 unfolding alpha_gen |
85 unfolding alpha_gen |
44 using a |
86 using a |
45 apply(simp) |
87 apply(simp) |
46 apply(rule_tac x="(x \<leftrightarrow> y)" in exI) |
88 apply(rule_tac x="(x \<leftrightarrow> y)" in exI) |
47 apply(rule conjI) |
89 apply(rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
90 apply(simp add: fresh_star_def) |
48 apply(simp add: flip_def) |
91 apply(simp add: flip_def) |
49 apply(simp add: fresh_star_def) |
92 apply(auto) |
50 defer |
93 prefer 2 |
51 apply(rule conjI) |
94 apply(rule alpha_weird.intros) |
|
95 apply(simp add: alpha_weird.intros(2)) |
|
96 prefer 2 |
|
97 apply(rule alpha_weird.intros) |
|
98 apply(simp add: alpha_weird.intros(2)) |
52 apply(simp) |
99 apply(simp) |
53 apply(rule alpha_weird_raw.intros) |
100 apply(rule alpha_weird.intros) |
54 apply(simp add: alpha_weird_raw.intros(2)) |
|
55 apply(simp add: fresh_star_def) |
|
56 apply(rule conjI) |
|
57 apply(rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
58 apply(rule_tac x="0" in exI) |
|
59 apply(simp) |
101 apply(simp) |
60 apply(rule alpha_weird_raw.intros) |
102 apply(simp add: alpha_gen) |
61 apply(simp add: alpha_weird_raw.intros(2)) |
103 using a |
62 apply(rule conjI) |
|
63 apply(auto)[1] |
|
64 apply(rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
65 apply(rule conjI) |
|
66 apply(simp add: flip_def) |
|
67 apply(auto)[1] |
|
68 defer |
|
69 apply(simp) |
104 apply(simp) |
70 apply(rule alpha_weird_raw.intros) |
105 *) |
71 apply(simp add: alpha_weird_raw.intros(2)) |
|
72 apply(simp add: fresh_perm) |
|
73 defer |
|
74 apply(simp add: fresh_perm) |
|
75 apply(simp add: atom_eqvt) |
|
76 unfolding flip_def[symmetric] |
|
77 apply(simp) |
|
78 done |
|
79 |
|
80 |
|
81 |
106 |
82 text {* example 1 *} |
107 text {* example 1 *} |
83 |
108 |
84 (* ML {* set show_hyps *} *) |
109 (* ML {* set show_hyps *} *) |
85 |
110 |
217 "bv3 ANil = {}" |
242 "bv3 ANil = {}" |
218 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)" |
243 | "bv3 (ACons x t as) = {atom x} \<union> (bv3 as)" |
219 |
244 |
220 (* example 4 from Terms.thy *) |
245 (* example 4 from Terms.thy *) |
221 |
246 |
222 (* 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 |
223 nominal_datatype trm4 = |
248 defined fv and defined alpha... *) |
|
249 (*nominal_datatype trm4 = |
224 Vr4 "name" |
250 Vr4 "name" |
225 | Ap4 "trm4" "trm4 list" |
251 | Ap4 "trm4" "trm4 list" |
226 | Lm4 x::"name" t::"trm4" bind x in t |
252 | Lm4 x::"name" t::"trm4" bind x in t |
227 |
253 |
228 thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars] |
254 thm alpha_trm4_raw_alpha_trm4_raw_list.intros[no_vars] |
229 thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars] |
255 thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]*) |
230 |
256 |
231 (* example 5 from Terms.thy *) |
257 (* example 5 from Terms.thy *) |
232 |
258 |
233 nominal_datatype trm5 = |
259 nominal_datatype trm5 = |
234 Vr5 "name" |
260 Vr5 "name" |