|
1 theory Let |
|
2 imports "../NewParser" |
|
3 begin |
|
4 |
|
5 text {* example 3 or example 5 from Terms.thy *} |
|
6 |
|
7 atom_decl name |
|
8 |
|
9 nominal_datatype trm = |
|
10 Var "name" |
|
11 | App "trm" "trm" |
|
12 | Lam x::"name" t::"trm" bind x in t |
|
13 | Let a::"lts" t::"trm" bind "bn a" in t |
|
14 and lts = |
|
15 Lnil |
|
16 | Lcons "name" "trm" "lts" |
|
17 binder |
|
18 bn |
|
19 where |
|
20 "bn Lnil = []" |
|
21 | "bn (Lcons x t l) = (atom x) # (bn l)" |
|
22 |
|
23 |
|
24 (* |
|
25 |
|
26 thm trm_lts.fv |
|
27 thm trm_lts.eq_iff |
|
28 thm trm_lts.bn |
|
29 thm trm_lts.perm |
|
30 thm trm_lts.induct[no_vars] |
|
31 thm trm_lts.inducts[no_vars] |
|
32 thm trm_lts.distinct |
|
33 thm trm_lts.supp |
|
34 thm trm_lts.fv[simplified trm_lts.supp(1-2)] |
|
35 |
|
36 |
|
37 primrec |
|
38 permute_bn_raw |
|
39 where |
|
40 "permute_bn_raw pi (Lnil_raw) = Lnil_raw" |
|
41 | "permute_bn_raw pi (Lcons_raw a t l) = Lcons_raw (pi \<bullet> a) t (permute_bn_raw pi l)" |
|
42 |
|
43 quotient_definition |
|
44 "permute_bn :: perm \<Rightarrow> lts \<Rightarrow> lts" |
|
45 is |
|
46 "permute_bn_raw" |
|
47 |
|
48 lemma [quot_respect]: "((op =) ===> alpha_lts_raw ===> alpha_lts_raw) permute_bn_raw permute_bn_raw" |
|
49 apply simp |
|
50 apply clarify |
|
51 apply (erule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.inducts) |
|
52 apply (rule TrueI)+ |
|
53 apply simp_all |
|
54 apply (rule_tac [!] alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros) |
|
55 apply simp_all |
|
56 done |
|
57 |
|
58 lemmas permute_bn = permute_bn_raw.simps[quot_lifted] |
|
59 |
|
60 lemma permute_bn_zero: |
|
61 "permute_bn 0 a = a" |
|
62 apply(induct a rule: trm_lts.inducts(2)) |
|
63 apply(rule TrueI)+ |
|
64 apply(simp_all add:permute_bn) |
|
65 done |
|
66 |
|
67 lemma permute_bn_add: |
|
68 "permute_bn (p + q) a = permute_bn p (permute_bn q a)" |
|
69 oops |
|
70 |
|
71 lemma permute_bn_alpha_bn: "alpha_bn lts (permute_bn q lts)" |
|
72 apply(induct lts rule: trm_lts.inducts(2)) |
|
73 apply(rule TrueI)+ |
|
74 apply(simp_all add:permute_bn eqvts trm_lts.eq_iff) |
|
75 done |
|
76 |
|
77 lemma perm_bn: |
|
78 "p \<bullet> bn l = bn(permute_bn p l)" |
|
79 apply(induct l rule: trm_lts.inducts(2)) |
|
80 apply(rule TrueI)+ |
|
81 apply(simp_all add:permute_bn eqvts) |
|
82 done |
|
83 |
|
84 lemma fv_perm_bn: |
|
85 "fv_bn l = fv_bn (permute_bn p l)" |
|
86 apply(induct l rule: trm_lts.inducts(2)) |
|
87 apply(rule TrueI)+ |
|
88 apply(simp_all add:permute_bn eqvts) |
|
89 done |
|
90 |
|
91 lemma Lt_subst: |
|
92 "supp (Abs_lst (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)" |
|
93 apply (simp add: trm_lts.eq_iff permute_bn_alpha_bn) |
|
94 apply (rule_tac x="q" in exI) |
|
95 apply (simp add: alphas) |
|
96 apply (simp add: perm_bn[symmetric]) |
|
97 apply(rule conjI) |
|
98 apply(drule supp_perm_eq) |
|
99 apply(simp add: abs_eq_iff) |
|
100 apply(simp add: alphas_abs alphas) |
|
101 apply(drule conjunct1) |
|
102 apply (simp add: trm_lts.supp) |
|
103 apply(simp add: supp_abs) |
|
104 apply (simp add: trm_lts.supp) |
|
105 done |
|
106 |
|
107 |
|
108 lemma fin_bn: |
|
109 "finite (set (bn l))" |
|
110 apply(induct l rule: trm_lts.inducts(2)) |
|
111 apply(simp_all add:permute_bn eqvts) |
|
112 done |
|
113 |
|
114 thm trm_lts.inducts[no_vars] |
|
115 |
|
116 lemma |
|
117 fixes t::trm |
|
118 and l::lts |
|
119 and c::"'a::fs" |
|
120 assumes a1: "\<And>name c. P1 c (Vr name)" |
|
121 and a2: "\<And>trm1 trm2 c. \<lbrakk>\<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (Ap trm1 trm2)" |
|
122 and a3: "\<And>name trm c. \<lbrakk>atom name \<sharp> c; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lm name trm)" |
|
123 and a4: "\<And>lts trm c. \<lbrakk>set (bn lts) \<sharp>* c; \<And>d. P2 d lts; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lt lts trm)" |
|
124 and a5: "\<And>c. P2 c Lnil" |
|
125 and a6: "\<And>name trm lts c. \<lbrakk>\<And>d. P1 d trm; \<And>d. P2 d lts\<rbrakk> \<Longrightarrow> P2 c (Lcons name trm lts)" |
|
126 shows "P1 c t" and "P2 c l" |
|
127 proof - |
|
128 have "(\<And>(p::perm) (c::'a::fs). P1 c (p \<bullet> t))" and |
|
129 b': "(\<And>(p::perm) (q::perm) (c::'a::fs). P2 c (permute_bn p (q \<bullet> l)))" |
|
130 apply(induct rule: trm_lts.inducts) |
|
131 apply(simp) |
|
132 apply(rule a1) |
|
133 apply(simp) |
|
134 apply(rule a2) |
|
135 apply(simp) |
|
136 apply(simp) |
|
137 apply(simp) |
|
138 apply(subgoal_tac "\<exists>q. (q \<bullet> (atom (p \<bullet> name))) \<sharp> c \<and> supp (Lm (p \<bullet> name) (p \<bullet> trm)) \<sharp>* q") |
|
139 apply(erule exE) |
|
140 apply(rule_tac t="Lm (p \<bullet> name) (p \<bullet> trm)" |
|
141 and s="q\<bullet> Lm (p \<bullet> name) (p \<bullet> trm)" in subst) |
|
142 apply(rule supp_perm_eq) |
|
143 apply(simp) |
|
144 apply(simp) |
|
145 apply(rule a3) |
|
146 apply(simp add: atom_eqvt) |
|
147 apply(subst permute_plus[symmetric]) |
|
148 apply(blast) |
|
149 apply(rule at_set_avoiding2_atom) |
|
150 apply(simp add: finite_supp) |
|
151 apply(simp add: finite_supp) |
|
152 apply(simp add: fresh_def) |
|
153 apply(simp add: trm_lts.fv[simplified trm_lts.supp]) |
|
154 apply(simp) |
|
155 apply(subgoal_tac "\<exists>q. (q \<bullet> set (bn (p \<bullet> lts))) \<sharp>* c \<and> supp (Abs_lst (bn (p \<bullet> lts)) (p \<bullet> trm)) \<sharp>* q") |
|
156 apply(erule exE) |
|
157 apply(erule conjE) |
|
158 thm Lt_subst |
|
159 apply(subst Lt_subst) |
|
160 apply assumption |
|
161 apply(rule a4) |
|
162 apply(simp add:perm_bn[symmetric]) |
|
163 apply(simp add: eqvts) |
|
164 apply (simp add: fresh_star_def fresh_def) |
|
165 apply(rotate_tac 1) |
|
166 apply(drule_tac x="q + p" in meta_spec) |
|
167 apply(simp) |
|
168 apply(rule at_set_avoiding2) |
|
169 apply(rule fin_bn) |
|
170 apply(simp add: finite_supp) |
|
171 apply(simp add: finite_supp) |
|
172 apply(simp add: fresh_star_def fresh_def supp_abs) |
|
173 apply(simp add: eqvts permute_bn) |
|
174 apply(rule a5) |
|
175 apply(simp add: permute_bn) |
|
176 apply(rule a6) |
|
177 apply simp |
|
178 apply simp |
|
179 done |
|
180 then have a: "P1 c (0 \<bullet> t)" by blast |
|
181 have "P2 c (permute_bn 0 (0 \<bullet> l))" using b' by blast |
|
182 then show "P1 c t" and "P2 c l" using a permute_bn_zero by simp_all |
|
183 qed |
|
184 |
|
185 |
|
186 |
|
187 lemma lets_bla: |
|
188 "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt (Lcons x (Vr y) Lnil) (Vr x)) \<noteq> (Lt (Lcons x (Vr z) Lnil) (Vr x))" |
|
189 by (simp add: trm_lts.eq_iff) |
|
190 |
|
191 lemma lets_ok: |
|
192 "(Lt (Lcons x (Vr y) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))" |
|
193 apply (simp add: trm_lts.eq_iff) |
|
194 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
195 apply (simp_all add: alphas eqvts supp_at_base fresh_star_def) |
|
196 done |
|
197 |
|
198 lemma lets_ok3: |
|
199 "x \<noteq> y \<Longrightarrow> |
|
200 (Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq> |
|
201 (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr x) (Vr y)))" |
|
202 apply (simp add: alphas trm_lts.eq_iff) |
|
203 done |
|
204 |
|
205 |
|
206 lemma lets_not_ok1: |
|
207 "x \<noteq> y \<Longrightarrow> |
|
208 (Lt (Lcons x (Vr x) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq> |
|
209 (Lt (Lcons y (Vr x) (Lcons x (Vr y) Lnil)) (Ap (Vr x) (Vr y)))" |
|
210 apply (simp add: alphas trm_lts.eq_iff fresh_star_def eqvts) |
|
211 done |
|
212 |
|
213 lemma lets_nok: |
|
214 "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow> |
|
215 (Lt (Lcons x (Ap (Vr z) (Vr z)) (Lcons y (Vr z) Lnil)) (Ap (Vr x) (Vr y))) \<noteq> |
|
216 (Lt (Lcons y (Vr z) (Lcons x (Ap (Vr z) (Vr z)) Lnil)) (Ap (Vr x) (Vr y)))" |
|
217 apply (simp add: alphas trm_lts.eq_iff fresh_star_def) |
|
218 done |
|
219 *) |
|
220 |
|
221 end |
|
222 |
|
223 |
|
224 |