5 text {* weirdo example from Peter Sewell's bestiary *} |
5 text {* weirdo example from Peter Sewell's bestiary *} |
6 |
6 |
7 nominal_datatype weird = |
7 nominal_datatype weird = |
8 WBind x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird" |
8 WBind x::"name" y::"name" p1::"weird" p2::"weird" p3::"weird" |
9 bind x in p1, bind x in p2, bind y in p2, bind y in p3 |
9 bind x in p1, bind x in p2, bind y in p2, bind y in p3 |
10 | WVar "name" |
10 | WV "name" |
11 | WPair "weird" "weird" |
11 | WP "weird" "weird" |
12 |
12 |
|
13 thm permute_weird_raw.simps[no_vars] |
13 thm alpha_weird_raw.intros[no_vars] |
14 thm alpha_weird_raw.intros[no_vars] |
14 thm fv_weird_raw.simps[no_vars] |
15 thm fv_weird_raw.simps[no_vars] |
15 (* Potential problem: Is it correct that in the fv-function |
16 (* Potential problem: Is it correct that in the fv-function |
16 the first two terms are created? Should be ommitted. Also |
17 the first two terms are created? Should be ommitted. Also |
17 something wrong with the permutations. *) |
18 something wrong with the permutations. *) |
|
19 |
|
20 primrec |
|
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 |
|
29 alpha_weird |
|
30 where |
|
31 "\<exists>p1 p2. |
|
32 ({atom y}, w3) \<approx>gen alpha_weird fv_weird p2 ({atom ya}, w3a) \<and> |
|
33 ({atom x} \<union> {atom y}, w2) \<approx>gen alpha_weird fv_weird (p1 + p2) ({atom xa} \<union> {atom ya}, w2a) \<and> |
|
34 ({atom x}, w1) \<approx>gen alpha_weird fv_weird p1 ({atom xa}, w1a) \<and> |
|
35 supp p1 \<inter> supp p2 = {} \<Longrightarrow> |
|
36 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)" |
|
38 | "alpha_weird w2 w2a \<and> alpha_weird w1 w1a \<Longrightarrow> alpha_weird (WP_raw w1 w2) (WP_raw w1a w2a)" |
|
39 |
|
40 (* |
|
41 abbreviation "WBind \<equiv> WBind_raw" |
|
42 abbreviation "WP \<equiv> WP_raw" |
|
43 abbreviation "WV \<equiv> WV_raw" |
|
44 |
|
45 lemma test: |
|
46 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))) |
|
48 (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) |
|
50 unfolding alpha_gen |
|
51 using a |
|
52 apply(simp) |
|
53 apply(rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
54 apply(rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
55 apply(simp add: fresh_star_def) |
|
56 apply(simp add: flip_def) |
|
57 apply(auto) |
|
58 prefer 2 |
|
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) |
|
65 apply(rule alpha_weird.intros) |
|
66 apply(simp) |
|
67 apply(simp add: alpha_gen) |
|
68 using a |
|
69 apply(simp) |
|
70 *) |
18 |
71 |
19 text {* example 1 *} |
72 text {* example 1 *} |
20 |
73 |
21 nominal_datatype lam = |
74 nominal_datatype lam = |
22 VAR "name" |
75 VAR "name" |