|
1 theory SingleLetFoo |
|
2 imports "../NewParser" |
|
3 begin |
|
4 |
|
5 |
|
6 declare [[STEPS = 4]] |
|
7 (* alpha does not work for this type *) |
|
8 |
|
9 atom_decl name |
|
10 |
|
11 nominal_datatype trm = |
|
12 Var "name" |
|
13 | App "trm" "trm" |
|
14 | Lam x::"name" t::"trm" bind_set x in t |
|
15 | Let a::"assg" t::"trm" bind_set "bn a" in t |
|
16 | Foo1 a1::"assg" a2::"assg" t::"trm" bind_set "bn a1" "bn a2" in t |
|
17 | Foo2 x::name a::"assg" t::"trm" bind_set x "bn a" in t |
|
18 and assg = |
|
19 As "name" "trm" |
|
20 binder |
|
21 bn::"assg \<Rightarrow> atom set" |
|
22 where |
|
23 "bn (As x t) = {atom x}" |
|
24 |
|
25 thm permute_trm_raw_permute_assg_raw.simps |
|
26 thm fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps[no_vars] |
|
27 |
|
28 (* there is something wrong with the free variables *) |
|
29 |
|
30 text {* |
|
31 thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros[no_vars] |
|
32 *} |
|
33 |
|
34 inductive |
|
35 alpha_trm_raw and alpha_assg_raw and alpha_bn_raw |
|
36 where |
|
37 "name = namea \<Longrightarrow> alpha_trm_raw (Var_raw name) (Var_raw namea)" |
|
38 | "\<lbrakk>alpha_trm_raw trm_raw1 trm_raw1a; alpha_trm_raw trm_raw2 trm_raw2a\<rbrakk> |
|
39 \<Longrightarrow> alpha_trm_raw (App_raw trm_raw1 trm_raw2) (App_raw trm_raw1a trm_raw2a)" |
|
40 | "\<exists>p. ({atom name}, trm_raw) \<approx>gen alpha_trm_raw fv_trm_raw p ({atom namea}, trm_rawa) \<Longrightarrow> |
|
41 alpha_trm_raw (Lam_raw name trm_raw) (Lam_raw namea trm_rawa)" |
|
42 | "\<lbrakk>\<exists>p. (bn_raw assg_raw, trm_raw) \<approx>gen alpha_trm_raw fv_trm_raw p (bn_raw assg_rawa, trm_rawa); |
|
43 alpha_bn_raw assg_raw assg_rawa\<rbrakk> |
|
44 \<Longrightarrow> alpha_trm_raw (Let_raw assg_raw trm_raw) (Let_raw assg_rawa trm_rawa)" |
|
45 | "\<lbrakk>\<exists>p. (bn_raw assg_raw1 \<union> bn_raw ass_raw2, trm_raw) \<approx>gen alpha_trm_raw fv_trm_raw p |
|
46 (bn_raw assg_raw1a \<union> bn_raw ass_raw2a, trm_rawa); |
|
47 alpha_bn_raw assg_raw1 assg_raw1a; alpha_bn_raw assg_raw2 assg_raw2a\<rbrakk> |
|
48 \<Longrightarrow> alpha_trm_raw (Foo1_raw assg_raw1 assg_raw2 trm_raw) (Foo1_raw assg_raw1a assg_raw2a trm_rawa)" |
|
49 | "\<lbrakk>\<exists>p. ({atom name} \<union> bn_raw assg_raw, trm_raw) \<approx>gen alpha_trm_raw fv_trm_raw p |
|
50 ({atom namea} \<union> bn_raw assg_rawa, trm_rawa); |
|
51 alpha_bn_raw assg_raw assg_rawa\<rbrakk> |
|
52 \<Longrightarrow> alpha_trm_raw (Foo2_raw name assg_raw trm_raw) (Foo2_raw namea assg_rawa trm_rawa)" |
|
53 |
|
54 | "\<lbrakk>name = namea; alpha_trm_raw trm_raw trm_rawa\<rbrakk> |
|
55 \<Longrightarrow> alpha_assg_raw (As_raw name trm_raw) (As_raw namea trm_rawa)" |
|
56 | "alpha_trm_raw trm_raw trm_rawa \<Longrightarrow> alpha_bn_raw (As_raw name trm_raw) (As_raw namea trm_rawa)" |
|
57 |
|
58 lemmas all = alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros |
|
59 |
|
60 lemma test: "p \<bullet> bn_raw \<equiv> bn_raw" sorry |
|
61 |
|
62 lemma |
|
63 assumes "distinct [x,y, z, u]" |
|
64 shows "alpha_trm_raw (Foo2_raw z (As_raw x (Var_raw z)) (Var_raw z)) |
|
65 (Foo2_raw u (As_raw y (Var_raw z)) (Var_raw u))" |
|
66 using assms |
|
67 apply(rule_tac all) |
|
68 apply(rule_tac x="(z \<leftrightarrow> u) + (x \<leftrightarrow> y)" in exI) |
|
69 apply(simp only: alphas) |
|
70 apply(rule conjI) |
|
71 apply(simp) |
|
72 apply(simp add: supp_at_base fresh_star_def) |
|
73 apply(rule conjI) |
|
74 apply(simp add: supp_at_base fresh_star_def) |
|
75 apply(rule conjI) |
|
76 apply(simp) |
|
77 apply(rule all) |
|
78 apply(simp) |
|
79 unfolding flip_def |
|
80 apply(perm_simp add: test) |
|
81 unfolding flip_def[symmetric] |
|
82 apply(simp) |
|
83 apply(subst flip_at_base_simps(3)) |
|
84 apply(auto)[2] |
|
85 apply(simp) |
|
86 apply(rule all) |
|
87 apply(rule all) |
|
88 apply(simp) |
|
89 done |
|
90 |
|
91 lemma |
|
92 assumes "distinct [x,y,z,u]" |
|
93 shows "fv_trm_raw (Foo2_raw z (As_raw x (Var_raw z)) (Var_raw z)) = {atom z}" |
|
94 using assms |
|
95 apply(simp add: supp_at_base) |
|
96 |
|
97 |
|
98 end |
|
99 |
|
100 |
|
101 |