85 a1: "a = b \<Longrightarrow> (rVr1 a) \<approx>1 (rVr1 b)" |
86 a1: "a = b \<Longrightarrow> (rVr1 a) \<approx>1 (rVr1 b)" |
86 | a2: "\<lbrakk>t1 \<approx>1 t2; s1 \<approx>1 s2\<rbrakk> \<Longrightarrow> rAp1 t1 s1 \<approx>1 rAp1 t2 s2" |
87 | a2: "\<lbrakk>t1 \<approx>1 t2; s1 \<approx>1 s2\<rbrakk> \<Longrightarrow> rAp1 t1 s1 \<approx>1 rAp1 t2 s2" |
87 | a3: "(\<exists>pi. (({atom aa}, t) \<approx>gen alpha1 rfv_trm1 pi ({atom ab}, s))) \<Longrightarrow> rLm1 aa t \<approx>1 rLm1 ab s" |
88 | a3: "(\<exists>pi. (({atom aa}, t) \<approx>gen alpha1 rfv_trm1 pi ({atom ab}, s))) \<Longrightarrow> rLm1 aa t \<approx>1 rLm1 ab s" |
88 | a4: "t1 \<approx>1 t2 \<Longrightarrow> (\<exists>pi. (((bv1 b1), s1) \<approx>gen alpha1 rfv_trm1 pi ((bv1 b2), s2))) \<Longrightarrow> rLt1 b1 t1 s1 \<approx>1 rLt1 b2 t2 s2" |
89 | a4: "t1 \<approx>1 t2 \<Longrightarrow> (\<exists>pi. (((bv1 b1), s1) \<approx>gen alpha1 rfv_trm1 pi ((bv1 b2), s2))) \<Longrightarrow> rLt1 b1 t1 s1 \<approx>1 rLt1 b2 t2 s2" |
89 |
90 |
90 lemma alpha_inj: |
91 lemma alpha1_inj: |
91 "(rVr1 a \<approx>1 rVr1 b) = (a = b)" |
92 "(rVr1 a \<approx>1 rVr1 b) = (a = b)" |
92 "(rAp1 t1 s1 \<approx>1 rAp1 t2 s2) = (t1 \<approx>1 t2 \<and> s1 \<approx>1 s2)" |
93 "(rAp1 t1 s1 \<approx>1 rAp1 t2 s2) = (t1 \<approx>1 t2 \<and> s1 \<approx>1 s2)" |
93 "(rLm1 aa t \<approx>1 rLm1 ab s) = (\<exists>pi. (({atom aa}, t) \<approx>gen alpha1 rfv_trm1 pi ({atom ab}, s)))" |
94 "(rLm1 aa t \<approx>1 rLm1 ab s) = (\<exists>pi. (({atom aa}, t) \<approx>gen alpha1 rfv_trm1 pi ({atom ab}, s)))" |
94 "(rLt1 b1 t1 s1 \<approx>1 rLt1 b2 t2 s2) = (t1 \<approx>1 t2 \<and> (\<exists>pi. (((bv1 b1), s1) \<approx>gen alpha1 rfv_trm1 pi ((bv1 b2), s2))))" |
95 "(rLt1 b1 t1 s1 \<approx>1 rLt1 b2 t2 s2) = (t1 \<approx>1 t2 \<and> (\<exists>pi. (((bv1 b1), s1) \<approx>gen alpha1 rfv_trm1 pi ((bv1 b2), s2))))" |
95 apply - |
96 apply - |
115 |
116 |
116 quotient_definition |
117 quotient_definition |
117 "Vr1 :: name \<Rightarrow> trm1" |
118 "Vr1 :: name \<Rightarrow> trm1" |
118 as |
119 as |
119 "rVr1" |
120 "rVr1" |
|
121 |
|
122 quotient_definition |
|
123 "Ap1 :: trm1 \<Rightarrow> trm1 \<Rightarrow> trm1" |
|
124 as |
|
125 "rAp1" |
|
126 |
|
127 quotient_definition |
|
128 "Lm1 :: name \<Rightarrow> trm1 \<Rightarrow> trm1" |
|
129 as |
|
130 "rLm1" |
|
131 |
|
132 quotient_definition |
|
133 "Lt1 :: bp \<Rightarrow> trm1 \<Rightarrow> trm1 \<Rightarrow> trm1" |
|
134 as |
|
135 "rLt1" |
|
136 |
|
137 quotient_definition |
|
138 "fv_trm1 :: trm1 \<Rightarrow> atom set" |
|
139 as |
|
140 "rfv_trm1" |
|
141 |
|
142 lemma alpha_rfv1: |
|
143 shows "t \<approx>1 s \<Longrightarrow> rfv_trm1 t = rfv_trm1 s" |
|
144 apply(induct rule: alpha1.induct) |
|
145 apply(simp_all add: alpha_gen.simps) |
|
146 done |
|
147 |
|
148 lemma [quot_respect]: |
|
149 "(op = ===> alpha1) rVr1 rVr1" |
|
150 "(alpha1 ===> alpha1 ===> alpha1) rAp1 rAp1" |
|
151 "(op = ===> alpha1 ===> alpha1) rLm1 rLm1" |
|
152 "(op = ===> alpha1 ===> alpha1 ===> alpha1) rLt1 rLt1" |
|
153 apply (auto intro: alpha1.intros) |
|
154 apply(rule a3) apply (rule_tac x="0" in exI) |
|
155 apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv1 alpha_gen) |
|
156 apply(rule a4) apply assumption apply (rule_tac x="0" in exI) |
|
157 apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv1 alpha_gen) |
|
158 done |
|
159 |
|
160 lemma [quot_respect]: |
|
161 "(op = ===> alpha1 ===> alpha1) permute permute" |
|
162 apply auto |
|
163 apply (rule alpha1_eqvt) |
|
164 apply simp |
|
165 done |
|
166 |
|
167 lemma [quot_respect]: |
|
168 "(alpha1 ===> op =) rfv_trm1 rfv_trm1" |
|
169 apply (simp add: alpha_rfv1) |
|
170 done |
|
171 |
|
172 lemma trm1_bp_induct: " |
|
173 \<lbrakk>\<And>name. P1 (Vr1 name); |
|
174 \<And>rtrm11 rtrm12. \<lbrakk>P1 rtrm11; P1 rtrm12\<rbrakk> \<Longrightarrow> P1 (Ap1 rtrm11 rtrm12); |
|
175 \<And>name rtrm1. P1 rtrm1 \<Longrightarrow> P1 (Lm1 name rtrm1); |
|
176 \<And>bp rtrm11 rtrm12. |
|
177 \<lbrakk>P2 bp; P1 rtrm11; P1 rtrm12\<rbrakk> \<Longrightarrow> P1 (Lt1 bp rtrm11 rtrm12); |
|
178 P2 BUnit; \<And>name. P2 (BVr name); |
|
179 \<And>bp1 bp2. \<lbrakk>P2 bp1; P2 bp2\<rbrakk> \<Longrightarrow> P2 (BPr bp1 bp2)\<rbrakk> |
|
180 \<Longrightarrow> P1 rtrma \<and> P2 bpa" |
|
181 apply (lifting rtrm1_bp.induct) |
|
182 done |
|
183 |
|
184 lemma trm1_bp_inducts: " |
|
185 \<lbrakk>\<And>name. P1 (Vr1 name); |
|
186 \<And>rtrm11 rtrm12. \<lbrakk>P1 rtrm11; P1 rtrm12\<rbrakk> \<Longrightarrow> P1 (Ap1 rtrm11 rtrm12); |
|
187 \<And>name rtrm1. P1 rtrm1 \<Longrightarrow> P1 (Lm1 name rtrm1); |
|
188 \<And>bp rtrm11 rtrm12. |
|
189 \<lbrakk>P2 bp; P1 rtrm11; P1 rtrm12\<rbrakk> \<Longrightarrow> P1 (Lt1 bp rtrm11 rtrm12); |
|
190 P2 BUnit; \<And>name. P2 (BVr name); |
|
191 \<And>bp1 bp2. \<lbrakk>P2 bp1; P2 bp2\<rbrakk> \<Longrightarrow> P2 (BPr bp1 bp2)\<rbrakk> |
|
192 \<Longrightarrow> P1 rtrma" |
|
193 "\<lbrakk>\<And>name. P1 (Vr1 name); |
|
194 \<And>rtrm11 rtrm12. \<lbrakk>P1 rtrm11; P1 rtrm12\<rbrakk> \<Longrightarrow> P1 (Ap1 rtrm11 rtrm12); |
|
195 \<And>name rtrm1. P1 rtrm1 \<Longrightarrow> P1 (Lm1 name rtrm1); |
|
196 \<And>bp rtrm11 rtrm12. |
|
197 \<lbrakk>P2 bp; P1 rtrm11; P1 rtrm12\<rbrakk> \<Longrightarrow> P1 (Lt1 bp rtrm11 rtrm12); |
|
198 P2 BUnit; \<And>name. P2 (BVr name); |
|
199 \<And>bp1 bp2. \<lbrakk>P2 bp1; P2 bp2\<rbrakk> \<Longrightarrow> P2 (BPr bp1 bp2)\<rbrakk> |
|
200 \<Longrightarrow> P2 bpa" |
|
201 by (lifting rtrm1_bp.inducts) |
|
202 |
|
203 instantiation trm1 and bp :: pt |
|
204 begin |
|
205 |
|
206 quotient_definition |
|
207 "permute_trm1 :: perm \<Rightarrow> trm1 \<Rightarrow> trm1" |
|
208 as |
|
209 "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1" |
|
210 |
|
211 lemma permute_trm1 [simp]: |
|
212 shows "pi \<bullet> Vr1 a = Vr1 (pi \<bullet> a)" |
|
213 and "pi \<bullet> Ap1 t1 t2 = Ap1 (pi \<bullet> t1) (pi \<bullet> t2)" |
|
214 and "pi \<bullet> Lm1 a t = Lm1 (pi \<bullet> a) (pi \<bullet> t)" |
|
215 and "pi \<bullet> Lt1 b t s = Lt1 (pi \<bullet> b) (pi \<bullet> t) (pi \<bullet> s)" |
|
216 apply - |
|
217 apply(lifting permute_rtrm1_permute_bp.simps(1)) |
|
218 apply(lifting permute_rtrm1_permute_bp.simps(2)) |
|
219 apply(lifting permute_rtrm1_permute_bp.simps(3)) |
|
220 apply(lifting permute_rtrm1_permute_bp.simps(4)) |
|
221 done |
|
222 instance |
|
223 apply default |
|
224 apply(induct_tac [!] x rule: trm1_bp_inducts(1)) |
|
225 apply(simp_all) |
|
226 done |
|
227 |
|
228 end |
|
229 |
|
230 lemma fv_trm1: |
|
231 "fv_trm1 (Vr1 x) = {atom x}" |
|
232 "fv_trm1 (Ap1 t1 t2) = fv_trm1 t1 \<union> fv_trm1 t2" |
|
233 "fv_trm1 (Lm1 x t) = fv_trm1 t - {atom x}" |
|
234 "fv_trm1 (Lt1 bp t1 t2) = fv_trm1 t1 \<union> (fv_trm1 t2 - bv1 bp)" |
|
235 apply - |
|
236 apply (lifting rfv_trm1_rfv_bp.simps(1)) |
|
237 apply (lifting rfv_trm1_rfv_bp.simps(2)) |
|
238 apply (lifting rfv_trm1_rfv_bp.simps(3)) |
|
239 apply (lifting rfv_trm1_rfv_bp.simps(4)) |
|
240 done |
|
241 |
|
242 lemma fv_trm1_eqvt: |
|
243 shows "(p \<bullet> fv_trm1 t) = fv_trm1 (p \<bullet> t)" |
|
244 apply(lifting rfv_trm1_eqvt) |
|
245 done |
|
246 |
|
247 lemma alpha1_INJ: |
|
248 "(Vr1 a = Vr1 b) = (a = b)" |
|
249 "(Ap1 t1 s1 = Ap1 t2 s2) = (t1 = t2 \<and> s1 = s2)" |
|
250 "(Lm1 aa t = Lm1 ab s) = (\<exists>pi. (({atom aa}, t) \<approx>gen (op =) fv_trm1 pi ({atom ab}, s)))" |
|
251 "(Lt1 b1 t1 s1 = Lt1 b2 t2 s2) = (t1 = t2 \<and> (\<exists>pi. (((bv1 b1), s1) \<approx>gen (op =) fv_trm1 pi ((bv1 b2), s2))))" |
|
252 unfolding alpha_gen apply (lifting alpha1_inj[unfolded alpha_gen]) |
|
253 done |
|
254 |
|
255 lemma supp_fv: |
|
256 shows "supp t = fv_trm1 t" |
|
257 apply(induct t rule: trm1_bp_inducts(1)) |
|
258 apply(simp_all add: supp_def permute_trm1 alpha1_INJ fv_trm1) |
|
259 apply(simp_all only: supp_at_base[simplified supp_def]) |
|
260 apply(simp_all add: Collect_imp_eq Collect_neg_eq) |
|
261 sorry (* Lam & Let still to do *) |
|
262 |
120 |
263 |
121 |
264 |
122 section {*** lets with single assignments ***} |
265 section {*** lets with single assignments ***} |
123 |
266 |
124 datatype trm2 = |
267 datatype trm2 = |