182 apply(simp) |
182 apply(simp) |
183 --"Eqvt done" |
183 --"Eqvt done" |
184 apply (case_tac x) |
184 apply (case_tac x) |
185 apply simp apply clarify |
185 apply simp apply clarify |
186 apply (rule_tac y="b" in ty_tys.exhaust(1)) |
186 apply (rule_tac y="b" in ty_tys.exhaust(1)) |
187 apply (auto simp add: ty_tys.eq_iff)[1] |
187 apply (auto)[1] |
188 apply (auto simp add: ty_tys.eq_iff)[1] |
188 apply (auto)[1] |
189 apply blast |
|
190 apply simp apply clarify |
189 apply simp apply clarify |
191 apply (rule_tac ya="b" and c="a" in ty_tys.strong_exhaust(2)) |
190 apply (rule_tac ya="b" and c="a" in ty_tys.strong_exhaust(2)) |
192 apply (auto simp add: ty_tys.eq_iff)[1] |
191 apply (auto)[1] |
193 apply (auto simp add: ty_tys.distinct) |
192 apply (auto)[5] |
194 apply (auto simp add: ty_tys.eq_iff ty_tys.distinct)[2] |
|
195 --"LAST GOAL" |
193 --"LAST GOAL" |
|
194 apply(simp del: ty_tys.eq_iff) |
196 thm meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff] |
195 thm meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff] |
197 apply (simp add: meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff]) |
196 apply (simp add: meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff]) |
198 apply (subgoal_tac "eqvt_at (\<lambda>(l, r). subst l r) (\<theta>', T)") |
197 apply (subgoal_tac "eqvt_at (\<lambda>(l, r). subst l r) (\<theta>', T)") |
199 apply (thin_tac "eqvt_at subst_substs_sumC (Inl (\<theta>', T))") |
198 apply (thin_tac "eqvt_at subst_substs_sumC (Inl (\<theta>', T))") |
200 defer |
199 defer |
228 apply (rule the1_equality) |
227 apply (rule the1_equality) |
229 apply metis apply assumption |
228 apply metis apply assumption |
230 apply clarify |
229 apply clarify |
231 --"This is exactly the assumption for the properly defined function" |
230 --"This is exactly the assumption for the properly defined function" |
232 defer |
231 defer |
233 apply (simp add: ty_tys.eq_iff) |
|
234 apply (simp only: Abs_eq_res_set) |
232 apply (simp only: Abs_eq_res_set) |
235 apply (subgoal_tac "(atom ` fset xsa \<inter> supp Ta - atom ` fset xs \<inter> supp T) \<sharp>* ([atom ` fset xs \<inter> supp (subst \<theta>' T)]set. T)") |
233 apply (subgoal_tac "(atom ` fset xsa \<inter> supp Ta - atom ` fset xs \<inter> supp T) \<sharp>* ([atom ` fset xs \<inter> supp (subst \<theta>' T)]set. T)") |
236 apply (subst (asm) Abs_eq_iff2) |
234 apply (subst (asm) Abs_eq_iff2) |
237 apply (clarify) |
235 apply (clarify) |
238 apply (simp add: alphas) |
236 apply (simp add: alphas) |
359 apply(simp) |
357 apply(simp) |
360 apply(rule_tac y="b" in ty2.exhaust) |
358 apply(rule_tac y="b" in ty2.exhaust) |
361 apply(blast) |
359 apply(blast) |
362 apply(blast) |
360 apply(blast) |
363 apply(simp_all add: ty2.distinct) |
361 apply(simp_all add: ty2.distinct) |
364 apply(simp add: ty2.eq_iff) |
|
365 apply(simp add: ty2.eq_iff) |
|
366 apply(subgoal_tac "\<And>p x r. subst_graph x r \<Longrightarrow> subst_graph (p \<bullet> x) (p \<bullet> r)") |
362 apply(subgoal_tac "\<And>p x r. subst_graph x r \<Longrightarrow> subst_graph (p \<bullet> x) (p \<bullet> r)") |
367 apply(simp add: eqvt_def) |
363 apply(simp add: eqvt_def) |
368 apply(rule allI) |
364 apply(rule allI) |
369 apply(simp add: permute_fun_def permute_bool_def) |
365 apply(simp add: permute_fun_def permute_bool_def) |
370 apply(rule ext) |
366 apply(rule ext) |