equal
deleted
inserted
replaced
173 |
173 |
174 section {* direct definitions --- problems *} |
174 section {* direct definitions --- problems *} |
175 |
175 |
176 lemma cheat: "P" sorry |
176 lemma cheat: "P" sorry |
177 |
177 |
|
178 definition |
|
179 "eqvt_at_bn f as \<equiv> \<forall>p. (p \<bullet> (f as)) = f (permute_bn p as)" |
|
180 |
|
181 definition |
|
182 "alpha_bn_preserve f as \<equiv> \<forall>p. f as = f (permute_bn p as)" |
|
183 |
|
184 lemma |
|
185 fixes as::"assn" |
|
186 assumes "eqvt_at f as" |
|
187 shows "eqvt_at_bn f as" |
|
188 using assms |
|
189 unfolding eqvt_at_bn_def |
|
190 apply(rule_tac allI) |
|
191 apply(drule k) |
|
192 apply(erule conjE) |
|
193 apply(subst (asm) eqvt_at_def) |
|
194 apply(simp) |
|
195 |
|
196 oops |
|
197 |
|
198 |
|
199 |
178 nominal_primrec |
200 nominal_primrec |
|
201 <<<<<<< variant A |
|
202 (invariant "\<lambda>x y. case x of Inl x1 \<Rightarrow> True | Inr x2 \<Rightarrow> alpha_bn_preserve (height_assn2::assn \<Rightarrow> nat) x2") |
|
203 >>>>>>> variant B |
|
204 ####### Ancestor |
|
205 (invariant "\<lambda>x y. case x of Inl x1 \<Rightarrow> True | Inr x2 \<Rightarrow> \<forall>p. (permute_bn p x2) = x2 \<longrightarrow> (p \<bullet> y) = y") |
|
206 ======= end |
179 height_trm2 :: "trm \<Rightarrow> nat" |
207 height_trm2 :: "trm \<Rightarrow> nat" |
180 and height_assn2 :: "assn \<Rightarrow> nat" |
208 and height_assn2 :: "assn \<Rightarrow> nat" |
181 where |
209 where |
182 "height_trm2 (Var x) = 1" |
210 "height_trm2 (Var x) = 1" |
183 | "height_trm2 (App l r) = max (height_trm2 l) (height_trm2 r)" |
211 | "height_trm2 (App l r) = max (height_trm2 l) (height_trm2 r)" |
187 thm height_trm2_height_assn2_graph_def |
215 thm height_trm2_height_assn2_graph_def |
188 apply (simp only: eqvt_def height_trm2_height_assn2_graph_def) |
216 apply (simp only: eqvt_def height_trm2_height_assn2_graph_def) |
189 apply (rule, perm_simp, rule) |
217 apply (rule, perm_simp, rule) |
190 -- "invariant" |
218 -- "invariant" |
191 apply(simp) |
219 apply(simp) |
|
220 <<<<<<< variant A |
|
221 apply(simp) |
|
222 apply(simp) |
|
223 apply(simp) |
|
224 apply(simp add: alpha_bn_preserve_def) |
|
225 apply(simp add: height_assn2_def) |
|
226 apply(simp add: trm_assn.perm_bn_simps) |
|
227 apply(rule allI) |
|
228 thm height_trm2_height_assn2_graph.intros[no_vars] |
|
229 thm height_trm2_height_assn2_sumC_def |
|
230 apply(rule cheat) |
|
231 apply - |
|
232 >>>>>>> variant B |
|
233 ####### Ancestor |
|
234 apply(simp) |
|
235 apply(simp) |
|
236 apply(simp) |
|
237 apply(rule cheat) |
|
238 apply - |
|
239 ======= end |
192 --"completeness" |
240 --"completeness" |
193 apply (case_tac x) |
241 apply (case_tac x) |
194 apply(simp) |
242 apply(simp) |
195 apply (rule_tac y="a" and c="a" in trm_assn.strong_exhaust(1)) |
243 apply (rule_tac y="a" and c="a" in trm_assn.strong_exhaust(1)) |
196 apply (auto simp add: alpha_bn_refl)[3] |
244 apply (auto simp add: alpha_bn_refl)[3] |
244 apply(simp (no_asm_use)) |
292 apply(simp (no_asm_use)) |
245 apply(clarify) |
293 apply(clarify) |
246 apply(erule alpha_bn_cases) |
294 apply(erule alpha_bn_cases) |
247 apply(simp del: trm_assn.eq_iff) |
295 apply(simp del: trm_assn.eq_iff) |
248 apply(simp only: trm_assn.bn_defs) |
296 apply(simp only: trm_assn.bn_defs) |
|
297 <<<<<<< variant A |
|
298 apply(erule_tac c="()" in Abs_lst1_fcb2') |
|
299 apply(simp_all add: fresh_star_def pure_fresh)[3] |
|
300 apply(simp add: eqvt_at_bn_def) |
|
301 apply(simp add: trm_assn.perm_bn_simps) |
|
302 apply(simp add: eqvt_at_bn_def) |
|
303 apply(simp add: trm_assn.perm_bn_simps) |
|
304 done |
|
305 |
|
306 >>>>>>> variant B |
249 apply(erule_tac c="(trm_rawa)" in Abs_lst1_fcb2') |
307 apply(erule_tac c="(trm_rawa)" in Abs_lst1_fcb2') |
250 apply(simp_all add: fresh_star_def pure_fresh)[2] |
308 apply(simp_all add: fresh_star_def pure_fresh)[2] |
251 apply(simp add: trm_assn.supp) |
309 apply(simp add: trm_assn.supp) |
252 apply(simp add: fresh_def) |
310 apply(simp add: fresh_def) |
253 apply(subst (asm) supp_finite_atom_set) |
311 apply(subst (asm) supp_finite_atom_set) |
256 apply(simp add: finite_supp) |
314 apply(simp add: finite_supp) |
257 apply(simp) |
315 apply(simp) |
258 apply(simp add: eqvt_at_def perm_supp_eq) |
316 apply(simp add: eqvt_at_def perm_supp_eq) |
259 apply(simp add: eqvt_at_def perm_supp_eq) |
317 apply(simp add: eqvt_at_def perm_supp_eq) |
260 done |
318 done |
|
319 ####### Ancestor |
|
320 apply(erule_tac c="()" in Abs_lst1_fcb2') |
|
321 apply(simp_all add: fresh_star_def pure_fresh)[3] |
|
322 |
|
323 oops |
|
324 ======= end |
261 |
325 |
262 termination by lexicographic_order |
326 termination by lexicographic_order |
263 |
327 |
264 lemma ww1: |
328 lemma ww1: |
265 shows "finite (fv_trm t)" |
329 shows "finite (fv_trm t)" |