151 apply (rule_tac y="a" and c="(b,c)" in trm_assn.strong_exhaust(1)) |
150 apply (rule_tac y="a" and c="(b,c)" in trm_assn.strong_exhaust(1)) |
152 apply (auto simp add: alpha_bn_refl)[3] |
151 apply (auto simp add: alpha_bn_refl)[3] |
153 apply(simp_all)[5] |
152 apply(simp_all)[5] |
154 apply(simp) |
153 apply(simp) |
155 apply(erule conjE)+ |
154 apply(erule conjE)+ |
156 thm alpha_bn_cases |
|
157 apply(erule alpha_bn_cases) |
155 apply(erule alpha_bn_cases) |
158 apply(simp) |
156 apply(simp) |
159 apply(simp add: trm_assn.bn_defs) |
157 apply(simp add: trm_assn.bn_defs) |
160 apply(erule_tac c="(ya,sa)" in Abs_lst1_fcb2) |
158 apply(erule_tac c="(ya,sa)" in Abs_lst1_fcb2) |
161 apply(simp add: Abs_fresh_iff fresh_star_def) |
159 apply(simp add: Abs_fresh_iff fresh_star_def) |
164 done |
162 done |
165 |
163 |
166 |
164 |
167 section {* direct definitions --- problems *} |
165 section {* direct definitions --- problems *} |
168 |
166 |
169 |
167 lemma cheat: "P" sorry |
170 nominal_primrec |
168 |
171 height_trm :: "trm \<Rightarrow> nat" |
169 nominal_primrec (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") |
172 and height_assn :: "assn \<Rightarrow> nat" |
170 height_trm2 :: "trm \<Rightarrow> nat" |
173 where |
171 and height_assn2 :: "assn \<Rightarrow> nat" |
174 "height_trm (Var x) = 1" |
172 where |
175 | "height_trm (App l r) = max (height_trm l) (height_trm r)" |
173 "height_trm2 (Var x) = 1" |
176 | "height_trm (Let as b) = max (height_assn as) (height_trm b)" |
174 | "height_trm2 (App l r) = max (height_trm2 l) (height_trm2 r)" |
177 | "height_assn (Assn x t) = (height_trm t)" |
175 | "height_trm2 (Let as b) = max (height_assn2 as) (height_trm2 b)" |
178 apply (simp only: eqvt_def height_trm_height_assn_graph_def) |
176 | "height_assn2 (Assn x t) = (height_trm2 t)" |
179 apply (rule, perm_simp, rule, rule TrueI) |
177 thm height_trm2_height_assn2_graph.intros |
|
178 thm height_trm2_height_assn2_graph_def |
|
179 apply (simp only: eqvt_def height_trm2_height_assn2_graph_def) |
|
180 apply (rule, perm_simp, rule) |
|
181 apply(erule height_trm2_height_assn2_graph.induct) |
|
182 -- "invariant" |
|
183 apply(simp) |
|
184 apply(simp) |
|
185 apply(simp) |
|
186 apply(simp) |
|
187 apply(rule cheat) |
|
188 apply - |
|
189 --"completeness" |
180 apply (case_tac x) |
190 apply (case_tac x) |
181 apply(simp) |
191 apply(simp) |
182 apply (case_tac a rule: trm_assn.exhaust(1)) |
192 apply (case_tac a rule: trm_assn.exhaust(1)) |
183 apply (auto simp add: alpha_bn_refl)[3] |
193 apply (auto simp add: alpha_bn_refl)[3] |
184 apply (drule_tac x="assn" in meta_spec) |
194 apply (drule_tac x="assn" in meta_spec) |
188 apply (case_tac b rule: trm_assn.exhaust(2)) |
198 apply (case_tac b rule: trm_assn.exhaust(2)) |
189 apply (auto)[1] |
199 apply (auto)[1] |
190 apply(simp_all)[7] |
200 apply(simp_all)[7] |
191 prefer 2 |
201 prefer 2 |
192 apply(simp) |
202 apply(simp) |
|
203 prefer 2 |
|
204 apply(simp) |
193 --"let case" |
205 --"let case" |
194 apply (simp only: meta_eq_to_obj_eq[OF height_trm_def, symmetric, unfolded fun_eq_iff]) |
206 apply (simp only: meta_eq_to_obj_eq[OF height_trm2_def, symmetric, unfolded fun_eq_iff]) |
195 apply (simp only: meta_eq_to_obj_eq[OF height_assn_def, symmetric, unfolded fun_eq_iff]) |
207 apply (simp only: meta_eq_to_obj_eq[OF height_assn2_def, symmetric, unfolded fun_eq_iff]) |
196 apply (subgoal_tac "eqvt_at height_assn as") |
208 apply (subgoal_tac "eqvt_at height_assn2 as") |
197 apply (subgoal_tac "eqvt_at height_assn asa") |
209 apply (subgoal_tac "eqvt_at height_assn2 asa") |
198 apply (subgoal_tac "eqvt_at height_trm b") |
210 apply (subgoal_tac "eqvt_at height_trm2 b") |
199 apply (subgoal_tac "eqvt_at height_trm ba") |
211 apply (subgoal_tac "eqvt_at height_trm2 ba") |
200 apply (thin_tac "eqvt_at height_trm_height_assn_sumC (Inr as)") |
212 apply (thin_tac "eqvt_at height_trm2_height_assn2_sumC (Inr as)") |
201 apply (thin_tac "eqvt_at height_trm_height_assn_sumC (Inr asa)") |
213 apply (thin_tac "eqvt_at height_trm2_height_assn2_sumC (Inr asa)") |
202 apply (thin_tac "eqvt_at height_trm_height_assn_sumC (Inl b)") |
214 apply (thin_tac "eqvt_at height_trm2_height_assn2_sumC (Inl b)") |
203 apply (thin_tac "eqvt_at height_trm_height_assn_sumC (Inl ba)") |
215 apply (thin_tac "eqvt_at height_trm2_height_assn2_sumC (Inl ba)") |
204 defer |
216 defer |
205 apply (simp add: eqvt_at_def height_trm_def) |
217 apply (simp add: eqvt_at_def height_trm2_def) |
206 apply (simp add: eqvt_at_def height_trm_def) |
218 apply (simp add: eqvt_at_def height_trm2_def) |
207 apply (simp add: eqvt_at_def height_assn_def) |
219 apply (simp add: eqvt_at_def height_assn2_def) |
208 apply (simp add: eqvt_at_def height_assn_def) |
220 apply (simp add: eqvt_at_def height_assn2_def) |
209 prefer 2 |
221 apply (subgoal_tac "height_assn2 as = height_assn2 asa") |
210 apply (subgoal_tac "height_assn as = height_assn asa") |
222 apply (subgoal_tac "height_trm2 b = height_trm2 ba") |
211 apply (subgoal_tac "height_trm b = height_trm ba") |
|
212 apply simp |
223 apply simp |
213 apply(simp) |
224 apply(simp) |
214 apply(erule conjE)+ |
225 apply(erule conjE)+ |
215 apply(erule alpha_bn_cases) |
226 apply(erule alpha_bn_cases) |
216 apply(simp) |
227 apply(simp) |
217 apply(simp add: trm_assn.bn_defs) |
228 apply(simp add: trm_assn.bn_defs) |
218 thm Abs_lst_fcb2 |
|
219 apply(erule_tac c="()" in Abs_lst_fcb2) |
229 apply(erule_tac c="()" in Abs_lst_fcb2) |
220 apply(simp_all add: fresh_star_def pure_fresh)[3] |
230 apply(simp_all add: fresh_star_def pure_fresh)[3] |
221 apply(simp add: eqvt_at_def) |
231 apply(simp add: eqvt_at_def) |
222 apply(simp add: eqvt_at_def) |
232 apply(simp add: eqvt_at_def) |
223 defer |
|
224 apply(simp) |
|
225 apply(frule Inl_inject) |
|
226 apply(subst (asm) trm_assn.eq_iff) |
|
227 apply(drule Inl_inject) |
233 apply(drule Inl_inject) |
|
234 apply(simp (no_asm_use)) |
228 apply(clarify) |
235 apply(clarify) |
229 apply(erule alpha_bn_cases) |
236 apply(erule alpha_bn_cases) |
230 apply(simp del: trm_assn.eq_iff) |
237 apply(simp del: trm_assn.eq_iff) |
231 apply(rename_tac as s as' s' t' t x x') |
|
232 apply(simp only: trm_assn.bn_defs) |
238 apply(simp only: trm_assn.bn_defs) |
233 (* HERE *) |
239 apply(erule_tac c="()" in Abs_lst1_fcb2') |
|
240 apply(simp_all add: fresh_star_def pure_fresh)[3] |
|
241 |
234 oops |
242 oops |
235 |
243 |
236 |
244 |
237 lemma ww1: |
245 lemma ww1: |
238 shows "finite (fv_trm t)" |
246 shows "finite (fv_trm t)" |