51 by (rule trm_assn.alpha_sym) |
51 by (rule trm_assn.alpha_sym) |
52 |
52 |
53 lemma alpha_bn_trans: "alpha_bn x y \<Longrightarrow> alpha_bn y z \<Longrightarrow> alpha_bn x z" |
53 lemma alpha_bn_trans: "alpha_bn x y \<Longrightarrow> alpha_bn y z \<Longrightarrow> alpha_bn x z" |
54 using trm_assn.alpha_trans by metis |
54 using trm_assn.alpha_trans by metis |
55 |
55 |
|
56 lemma fv_bn_finite[simp]: |
|
57 "finite (fv_bn as)" |
|
58 apply(case_tac as rule: trm_assn.exhaust(2)) |
|
59 apply(simp add: trm_assn.supp finite_supp) |
|
60 done |
|
61 |
|
62 |
56 lemma k: "A \<Longrightarrow> A \<and> A" by blast |
63 lemma k: "A \<Longrightarrow> A \<and> A" by blast |
57 |
64 |
58 lemma max_eqvt[eqvt]: "p \<bullet> (max (a :: _ :: pure) b) = max (p \<bullet> a) (p \<bullet> b)" |
65 lemma max_eqvt[eqvt]: "p \<bullet> (max (a :: _ :: pure) b) = max (p \<bullet> a) (p \<bullet> b)" |
59 by (simp add: permute_pure) |
66 by (simp add: permute_pure) |
60 |
67 |
169 section {* direct definitions --- problems *} |
176 section {* direct definitions --- problems *} |
170 |
177 |
171 lemma cheat: "P" sorry |
178 lemma cheat: "P" sorry |
172 |
179 |
173 nominal_primrec |
180 nominal_primrec |
174 (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") |
|
175 height_trm2 :: "trm \<Rightarrow> nat" |
181 height_trm2 :: "trm \<Rightarrow> nat" |
176 and height_assn2 :: "assn \<Rightarrow> nat" |
182 and height_assn2 :: "assn \<Rightarrow> nat" |
177 where |
183 where |
178 "height_trm2 (Var x) = 1" |
184 "height_trm2 (Var x) = 1" |
179 | "height_trm2 (App l r) = max (height_trm2 l) (height_trm2 r)" |
185 | "height_trm2 (App l r) = max (height_trm2 l) (height_trm2 r)" |
180 | "height_trm2 (Let as b) = max (height_assn2 as) (height_trm2 b)" |
186 | "set (bn as) \<sharp>* fv_bn as \<Longrightarrow> height_trm2 (Let as b) = max (height_assn2 as) (height_trm2 b)" |
181 | "height_assn2 (Assn x t) = (height_trm2 t)" |
187 | "height_assn2 (Assn x t) = (height_trm2 t)" |
182 thm height_trm2_height_assn2_graph.intros[no_vars] |
188 thm height_trm2_height_assn2_graph.intros[no_vars] |
183 thm height_trm2_height_assn2_graph_def |
189 thm height_trm2_height_assn2_graph_def |
184 apply (simp only: eqvt_def height_trm2_height_assn2_graph_def) |
190 apply (simp only: eqvt_def height_trm2_height_assn2_graph_def) |
185 apply (rule, perm_simp, rule) |
191 apply (rule, perm_simp, rule) |
186 apply(erule height_trm2_height_assn2_graph.induct) |
|
187 -- "invariant" |
192 -- "invariant" |
188 apply(simp) |
193 apply(simp) |
189 apply(simp) |
|
190 apply(simp) |
|
191 apply(simp) |
|
192 apply(rule cheat) |
|
193 apply - |
|
194 --"completeness" |
194 --"completeness" |
195 apply (case_tac x) |
195 apply (case_tac x) |
196 apply(simp) |
196 apply(simp) |
197 apply (case_tac a rule: trm_assn.exhaust(1)) |
197 apply (rule_tac y="a" and c="a" in trm_assn.strong_exhaust(1)) |
198 apply (auto simp add: alpha_bn_refl)[3] |
198 apply (auto simp add: alpha_bn_refl)[3] |
199 apply (drule_tac x="assn" in meta_spec) |
199 apply (drule_tac x="assn" in meta_spec) |
200 apply (drule_tac x="trm" in meta_spec) |
200 apply (drule_tac x="trm" in meta_spec) |
201 apply(simp add: alpha_bn_refl) |
201 apply(simp add: alpha_bn_refl) |
|
202 apply(rotate_tac 3) |
|
203 apply(drule meta_mp) |
|
204 apply(simp add: fresh_star_def trm_assn.fresh) |
|
205 apply(simp add: fresh_def) |
|
206 apply(subst supp_finite_atom_set) |
|
207 apply(simp) |
|
208 apply(simp) |
202 apply(simp) |
209 apply(simp) |
203 apply (case_tac b rule: trm_assn.exhaust(2)) |
210 apply (case_tac b rule: trm_assn.exhaust(2)) |
204 apply (auto)[1] |
211 apply (auto)[1] |
205 apply(simp_all)[7] |
212 apply(simp_all)[7] |
206 prefer 2 |
213 prefer 2 |
239 apply(simp (no_asm_use)) |
246 apply(simp (no_asm_use)) |
240 apply(clarify) |
247 apply(clarify) |
241 apply(erule alpha_bn_cases) |
248 apply(erule alpha_bn_cases) |
242 apply(simp del: trm_assn.eq_iff) |
249 apply(simp del: trm_assn.eq_iff) |
243 apply(simp only: trm_assn.bn_defs) |
250 apply(simp only: trm_assn.bn_defs) |
244 apply(erule_tac c="()" in Abs_lst1_fcb2') |
251 apply(erule_tac c="(trm_rawa)" in Abs_lst1_fcb2') |
245 apply(simp_all add: fresh_star_def pure_fresh)[3] |
252 apply(simp_all add: fresh_star_def pure_fresh)[2] |
246 |
253 apply(simp add: trm_assn.supp) |
247 oops |
254 apply(simp add: fresh_def) |
|
255 apply(subst (asm) supp_finite_atom_set) |
|
256 apply(simp add: finite_supp) |
|
257 apply(subst (asm) supp_finite_atom_set) |
|
258 apply(simp add: finite_supp) |
|
259 apply(simp) |
|
260 apply(simp add: eqvt_at_def perm_supp_eq) |
|
261 apply(simp add: eqvt_at_def perm_supp_eq) |
|
262 done |
248 |
263 |
249 |
264 |
250 lemma ww1: |
265 lemma ww1: |
251 shows "finite (fv_trm t)" |
266 shows "finite (fv_trm t)" |
252 and "finite (fv_bn as)" |
267 and "finite (fv_bn as)" |