1 theory Ex4 |
|
2 imports "../NewParser" |
|
3 begin |
|
4 |
|
5 declare [[STEPS = 5]] |
|
6 |
|
7 atom_decl name |
|
8 |
|
9 nominal_datatype trm = |
|
10 Var "name" |
|
11 | App "trm" "trm" |
|
12 | Lam x::"name" t::"trm" bind_set x in t |
|
13 | Let p::"pat" "trm" t::"trm" bind_set "f p" in t |
|
14 | Foo1 p::"pat" q::"pat" t::"trm" bind_set "f p" "f q" in t |
|
15 | Foo2 x::"name" p::"pat" t::"trm" bind_set x "f p" in t |
|
16 and pat = |
|
17 PN |
|
18 | PS "name" |
|
19 | PD "pat" "pat" |
|
20 binder |
|
21 f::"pat \<Rightarrow> atom set" |
|
22 where |
|
23 "f PN = {}" |
|
24 | "f (PS x) = {atom x}" |
|
25 | "f (PD p1 p2) = (f p1) \<union> (f p2)" |
|
26 |
|
27 thm permute_trm_raw_permute_pat_raw.simps |
|
28 thm fv_trm_raw.simps fv_pat_raw.simps fv_f_raw.simps |
|
29 |
|
30 thm alpha_trm_raw_alpha_pat_raw_alpha_f_raw.intros[no_vars] |
|
31 |
|
32 (* |
|
33 inductive |
|
34 alpha_trm_raw and alpha_pat_raw and alpha_f_raw |
|
35 where |
|
36 (* alpha_trm_raw *) |
|
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. (f_raw pat_raw, trm_raw2) \<approx>gen alpha_trm_raw fv_trm_raw p (f_raw pat_rawa, trm_raw2a); |
|
43 alpha_f_raw pat_raw pat_rawa; alpha_trm_raw trm_raw1 trm_raw1a\<rbrakk> |
|
44 \<Longrightarrow> alpha_trm_raw (Let_raw pat_raw trm_raw1 trm_raw2) (Let_raw pat_rawa trm_raw1a trm_raw2a)" |
|
45 | "\<lbrakk>\<exists>p. (f_raw pat_raw1 \<union> f_raw pat_raw2, trm_raw) \<approx>gen alpha_trm_raw fv_trm_raw p (f_raw pat_raw1a \<union> f_raw pat_raw2a, trm_rawa); |
|
46 alpha_f_raw pat_raw1 pat_raw1a; alpha_f_raw pat_raw2 pat_raw2a\<rbrakk> |
|
47 \<Longrightarrow> alpha_trm_raw (Foo1_raw pat_raw1 pat_raw2 trm_raw) (Foo1_raw pat_raw1a pat_raw2a trm_rawa)" |
|
48 | "\<lbrakk>\<exists>p. ({atom name} \<union> f_raw pat_raw, trm_raw) \<approx>gen alpha_trm_raw fv_trm_raw p ({atom namea} \<union> f_raw pat_rawa, trm_rawa); |
|
49 alpha_f_raw pat_raw pat_rawa\<rbrakk> |
|
50 \<Longrightarrow> alpha_trm_raw (Foo2_raw name pat_raw trm_raw) (Foo2_raw namea pat_rawa trm_rawa)" |
|
51 |
|
52 (* alpha_pat_raw *) |
|
53 | "alpha_pat_raw PN_raw PN_raw" |
|
54 | "name = namea \<Longrightarrow> alpha_pat_raw (PS_raw name) (PS_raw namea)" |
|
55 | "\<lbrakk>alpha_pat_raw pat_raw1 pat_raw1a; alpha_pat_raw pat_raw2 pat_raw2a\<rbrakk> |
|
56 \<Longrightarrow> alpha_pat_raw (PD_raw pat_raw1 pat_raw2) (PD_raw pat_raw1a pat_raw2a)" |
|
57 |
|
58 (* alpha_f_raw *) |
|
59 | "alpha_f_raw PN_raw PN_raw" |
|
60 | "alpha_f_raw (PS_raw name) (PS_raw namea)" |
|
61 | "\<lbrakk>alpha_f_raw pat_raw1 pat_raw1a; alpha_f_raw pat_raw2 pat_raw2a\<rbrakk> |
|
62 \<Longrightarrow> alpha_f_raw (PD_raw pat_raw1 pat_raw2) (PD_raw pat_raw1a pat_raw2a)" |
|
63 *) |
|
64 |
|
65 lemmas all = alpha_trm_raw_alpha_pat_raw_alpha_f_raw.intros |
|
66 |
|
67 lemma |
|
68 shows "alpha_trm_raw (Foo2_raw x (PS_raw x) (Var_raw x)) |
|
69 (Foo2_raw y (PS_raw y) (Var_raw y))" |
|
70 apply(rule all) |
|
71 apply(rule_tac x="(atom x \<rightleftharpoons> atom y)" in exI) |
|
72 apply(simp add: alphas) |
|
73 apply(simp add: supp_at_base fresh_star_def) |
|
74 apply(rule conjI) |
|
75 apply(rule all) |
|
76 apply(simp) |
|
77 apply(perm_simp) |
|
78 apply(simp) |
|
79 apply(rule all) |
|
80 done |
|
81 |
|
82 |
|
83 |
|
84 end |
|
85 |
|
86 |
|
87 |
|