29 thm trm_assg.fv[simplified trm_assg.supp(1-2),no_vars] |
29 thm trm_assg.fv[simplified trm_assg.supp(1-2),no_vars] |
30 |
30 |
31 thm permute_trm_raw_permute_assg_raw.simps |
31 thm permute_trm_raw_permute_assg_raw.simps |
32 thm fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps[no_vars] |
32 thm fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps[no_vars] |
33 |
33 |
34 (* there is something wrong with the free variables *) |
34 thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros[no_vars] |
35 |
35 |
36 text {* |
|
37 thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros[no_vars] |
|
38 *} |
|
39 |
|
40 inductive |
|
41 alpha_trm_raw and alpha_assg_raw and alpha_bn_raw |
|
42 where |
|
43 "name = namea \<Longrightarrow> alpha_trm_raw (Var_raw name) (Var_raw namea)" |
|
44 | "\<lbrakk>alpha_trm_raw trm_raw1 trm_raw1a; alpha_trm_raw trm_raw2 trm_raw2a\<rbrakk> |
|
45 \<Longrightarrow> alpha_trm_raw (App_raw trm_raw1 trm_raw2) (App_raw trm_raw1a trm_raw2a)" |
|
46 | "\<exists>p. ({atom name}, trm_raw) \<approx>gen alpha_trm_raw fv_trm_raw p ({atom namea}, trm_rawa) \<Longrightarrow> |
|
47 alpha_trm_raw (Lam_raw name trm_raw) (Lam_raw namea trm_rawa)" |
|
48 | "\<lbrakk>\<exists>p. (bn_raw assg_raw, trm_raw) \<approx>gen alpha_trm_raw fv_trm_raw p (bn_raw assg_rawa, trm_rawa); |
|
49 alpha_bn_raw assg_raw assg_rawa\<rbrakk> |
|
50 \<Longrightarrow> alpha_trm_raw (Let_raw assg_raw trm_raw) (Let_raw assg_rawa trm_rawa)" |
|
51 | "\<lbrakk>\<exists>p. (bn_raw assg_raw1 \<union> bn_raw ass_raw2, trm_raw) \<approx>gen alpha_trm_raw fv_trm_raw p |
|
52 (bn_raw assg_raw1a \<union> bn_raw ass_raw2a, trm_rawa); |
|
53 alpha_bn_raw assg_raw1 assg_raw1a; alpha_bn_raw assg_raw2 assg_raw2a\<rbrakk> |
|
54 \<Longrightarrow> alpha_trm_raw (Foo1_raw assg_raw1 assg_raw2 trm_raw) (Foo1_raw assg_raw1a assg_raw2a trm_rawa)" |
|
55 | "\<lbrakk>\<exists>p. ({atom name} \<union> bn_raw assg_raw, trm_raw) \<approx>gen alpha_trm_raw fv_trm_raw p |
|
56 ({atom namea} \<union> bn_raw assg_rawa, trm_rawa); |
|
57 alpha_bn_raw assg_raw assg_rawa\<rbrakk> |
|
58 \<Longrightarrow> alpha_trm_raw (Foo2_raw name assg_raw trm_raw) (Foo2_raw namea assg_rawa trm_rawa)" |
|
59 |
|
60 | "\<lbrakk>name = namea; alpha_trm_raw trm_raw trm_rawa\<rbrakk> |
|
61 \<Longrightarrow> alpha_assg_raw (As_raw name trm_raw) (As_raw namea trm_rawa)" |
|
62 | "alpha_trm_raw trm_raw trm_rawa \<Longrightarrow> alpha_bn_raw (As_raw name trm_raw) (As_raw namea trm_rawa)" |
|
63 |
36 |
64 lemmas all = alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros |
37 lemmas all = alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros |
65 |
38 |
66 lemma test: "p \<bullet> bn_raw \<equiv> bn_raw" sorry |
39 lemma test: "p \<bullet> bn_raw \<equiv> bn_raw" sorry |
67 |
40 |