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 (* Potential problem: Is it correct that in the fv-function |
|
17 the first two terms are created? Should be ommitted. Also |
|
18 something wrong with the permutations. *) |
|
19 |
16 |
20 lemma "alpha_weird_raw a b \<Longrightarrow> alpha_weird_raw (p \<bullet> a) (p \<bullet> b)" |
17 lemma "alpha_weird_raw a b \<Longrightarrow> alpha_weird_raw (p \<bullet> a) (p \<bullet> b)" |
21 apply (erule alpha_weird_raw.induct) |
18 apply (erule alpha_weird_raw.induct) |
22 defer |
19 defer |
23 apply (simp add: alpha_weird_raw.intros) |
20 apply (simp add: alpha_weird_raw.intros) |
50 apply(rule_tac ?p1="- p" in fresh_star_permute_iff[THEN iffD1]) |
47 apply(rule_tac ?p1="- p" in fresh_star_permute_iff[THEN iffD1]) |
51 apply (simp add: eqvts add_perm_eqvt) |
48 apply (simp add: eqvts add_perm_eqvt) |
52 apply (simp add: permute_eqvt[symmetric]) |
49 apply (simp add: permute_eqvt[symmetric]) |
53 done |
50 done |
54 |
51 |
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 |
|
63 inductive |
|
64 alpha_weird |
|
65 where |
|
66 "\<exists>p1 p2. |
|
67 ({atom y}, w3) \<approx>gen alpha_weird fv_weird p2 ({atom ya}, w3a) \<and> |
|
68 ({atom x} \<union> {atom y}, w2) \<approx>gen alpha_weird fv_weird (p1 + p2) ({atom xa} \<union> {atom ya}, w2a) \<and> |
|
69 ({atom x}, w1) \<approx>gen alpha_weird fv_weird p1 ({atom xa}, w1a) \<and> |
|
70 supp p1 \<inter> supp p2 = {} \<Longrightarrow> |
|
71 alpha_weird (WBind_raw x y w1 w2 w3) (WBind_raw xa ya w1a w2a w3a)" |
|
72 | "x = xa \<Longrightarrow> alpha_weird (WV_raw x) (WV_raw xa)" |
|
73 | "alpha_weird w2 w2a \<and> alpha_weird w1 w1a \<Longrightarrow> alpha_weird (WP_raw w1 w2) (WP_raw w1a w2a)" |
|
74 |
52 |
75 (* |
53 (* |
76 abbreviation "WBind \<equiv> WBind_raw" |
54 abbreviation "WBind \<equiv> WBind_raw" |
77 abbreviation "WP \<equiv> WP_raw" |
55 abbreviation "WP \<equiv> WP_raw" |
78 abbreviation "WV \<equiv> WV_raw" |
56 abbreviation "WV \<equiv> WV_raw" |