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 |
16 |
17 the first two terms are created? Should be ommitted. Also |
17 abbreviation "fv_weird \<equiv> fv_weird_raw" |
18 something wrong with the permutations. *) |
18 abbreviation "alpha_weird \<equiv> alpha_weird_raw" |
19 |
19 |
20 primrec |
20 (* |
21 fv_weird |
|
22 where |
|
23 "fv_weird (WBind_raw x y p1 p2 p3) = |
|
24 (fv_weird p1 - {atom x}) \<union> (fv_weird p2 - ({atom x} \<union> {atom y})) \<union> (fv_weird p3 - {atom y})" |
|
25 | "fv_weird (WV_raw x) = {atom x}" |
|
26 | "fv_weird (WP_raw p1 p2) = (fv_weird p1 \<union> fv_weird p2)" |
|
27 |
|
28 inductive |
21 inductive |
29 alpha_weird |
22 alpha_weird |
30 where |
23 where |
31 "\<exists>p1 p2. |
24 "\<exists>p1 p2. |
32 ({atom y}, w3) \<approx>gen alpha_weird fv_weird p2 ({atom ya}, w3a) \<and> |
25 ({atom y}, w3) \<approx>gen alpha_weird fv_weird p2 ({atom ya}, w3a) \<and> |
34 ({atom x}, w1) \<approx>gen alpha_weird fv_weird p1 ({atom xa}, w1a) \<and> |
27 ({atom x}, w1) \<approx>gen alpha_weird fv_weird p1 ({atom xa}, w1a) \<and> |
35 supp p1 \<inter> supp p2 = {} \<Longrightarrow> |
28 supp p1 \<inter> supp p2 = {} \<Longrightarrow> |
36 alpha_weird (WBind_raw x y w1 w2 w3) (WBind_raw xa ya w1a w2a w3a)" |
29 alpha_weird (WBind_raw x y w1 w2 w3) (WBind_raw xa ya w1a w2a w3a)" |
37 | "x = xa \<Longrightarrow> alpha_weird (WV_raw x) (WV_raw xa)" |
30 | "x = xa \<Longrightarrow> alpha_weird (WV_raw x) (WV_raw xa)" |
38 | "alpha_weird w2 w2a \<and> alpha_weird w1 w1a \<Longrightarrow> alpha_weird (WP_raw w1 w2) (WP_raw w1a w2a)" |
31 | "alpha_weird w2 w2a \<and> alpha_weird w1 w1a \<Longrightarrow> alpha_weird (WP_raw w1 w2) (WP_raw w1a w2a)" |
39 |
32 *) |
40 (* |
33 |
41 abbreviation "WBind \<equiv> WBind_raw" |
34 abbreviation "WBind \<equiv> WBind_raw" |
42 abbreviation "WP \<equiv> WP_raw" |
35 abbreviation "WP \<equiv> WP_raw" |
43 abbreviation "WV \<equiv> WV_raw" |
36 abbreviation "WV \<equiv> WV_raw" |
44 |
37 |
45 lemma test: |
38 lemma test: |
46 assumes a: "distinct [x, y, z]" |
39 assumes a: "distinct [x, y, z]" |
47 shows "alpha_weird (WBind x y (WP (WV x) (WV z)) (WP (WV x) (WV y)) (WP (WV z) (WV y))) |
40 shows "alpha_weird (WBind x y (WP (WV x) (WV z)) (WP (WV x) (WV y)) (WP (WV z) (WV y))) |
48 (WBind y x (WP (WV y) (WV z)) (WP (WV y) (WV x)) (WP (WV z) (WV x)))" |
41 (WBind y x (WP (WV y) (WV z)) (WP (WV y) (WV x)) (WP (WV z) (WV x)))" |
49 apply(rule_tac alpha_weird.intros) |
42 apply(rule_tac alpha_weird_raw.intros) |
50 unfolding alpha_gen |
43 unfolding alpha_gen |
51 using a |
44 using a |
52 apply(simp) |
45 apply(simp) |
53 apply(rule_tac x="(x \<leftrightarrow> y)" in exI) |
46 apply(rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
47 apply(rule conjI) |
|
48 apply(simp add: flip_def) |
|
49 apply(simp add: fresh_star_def) |
|
50 defer |
|
51 apply(rule conjI) |
|
52 apply(simp) |
|
53 apply(rule alpha_weird_raw.intros) |
|
54 apply(simp add: alpha_weird_raw.intros(2)) |
|
55 apply(simp add: fresh_star_def) |
|
56 apply(rule conjI) |
54 apply(rule_tac x="(x \<leftrightarrow> y)" in exI) |
57 apply(rule_tac x="(x \<leftrightarrow> y)" in exI) |
55 apply(simp add: fresh_star_def) |
58 apply(rule_tac x="0" in exI) |
|
59 apply(simp) |
|
60 apply(rule alpha_weird_raw.intros) |
|
61 apply(simp add: alpha_weird_raw.intros(2)) |
|
62 apply(rule conjI) |
|
63 apply(auto)[1] |
|
64 apply(rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
65 apply(rule conjI) |
56 apply(simp add: flip_def) |
66 apply(simp add: flip_def) |
57 apply(auto) |
67 apply(auto)[1] |
58 prefer 2 |
68 defer |
59 apply(rule alpha_weird.intros) |
|
60 apply(simp add: alpha_weird.intros(2)) |
|
61 prefer 2 |
|
62 apply(rule alpha_weird.intros) |
|
63 apply(simp add: alpha_weird.intros(2)) |
|
64 apply(simp) |
69 apply(simp) |
65 apply(rule alpha_weird.intros) |
70 apply(rule alpha_weird_raw.intros) |
|
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] |
66 apply(simp) |
77 apply(simp) |
67 apply(simp add: alpha_gen) |
78 done |
68 using a |
79 |
69 apply(simp) |
80 |
70 *) |
|
71 |
81 |
72 text {* example 1 *} |
82 text {* example 1 *} |
73 |
83 |
74 (* ML {* set show_hyps *} *) |
84 (* ML {* set show_hyps *} *) |
75 |
85 |