# HG changeset patch # User Cezary Kaliszyk # Date 1307494599 -32400 # Node ID 297cff1d10483db3ac3c7d40cebb7d95a1ee6f5e # Parent 0acb0b8f4106e9fc282075efdb9388b8ac481188 FCB for res binding and simplified proof of subst for type schemes diff -r 0acb0b8f4106 -r 297cff1d1048 Nominal/Ex/TypeSchemes.thy --- a/Nominal/Ex/TypeSchemes.thy Wed Jun 08 07:06:20 2011 +0900 +++ b/Nominal/Ex/TypeSchemes.thy Wed Jun 08 09:56:39 2011 +0900 @@ -347,7 +347,6 @@ apply (rule, perm_simp, rule) apply(rule TrueI) apply(case_tac x) - apply(simp) apply(rule_tac y="b" in ty2.exhaust) apply(blast) apply(blast) @@ -355,15 +354,11 @@ done termination - apply(relation "measure (size o snd)") - apply(simp_all add: ty2.size) - done + by (relation "measure (size o snd)") (simp_all add: ty2.size) lemma subst_eqvt[eqvt]: shows "(p \ subst \ T) = subst (p \ \) (p \ T)" -apply(induct \ T rule: subst.induct) -apply(simp_all add: lookup2_eqvt) -done + by (induct \ T rule: subst.induct) (simp_all add: lookup2_eqvt) lemma supp_fun_app2_eqvt: assumes e: "eqvt f" @@ -379,7 +374,37 @@ lemma fresh_star_inter1: "xs \* z \ (xs \ ys) \* z" unfolding fresh_star_def by blast - + +lemma Abs_res_fcb: + fixes xs ys :: "('a :: at_base) set" + and S T :: "'b :: fs" + assumes e: "(Abs_res (atom ` xs) T) = (Abs_res (atom ` ys) S)" + and f1: "\x. x \ atom ` xs \ x \ supp T \ x \ f xs T" + and f2: "\x. supp T - atom ` xs \ supp T = supp S - atom ` ys \ supp S \ x \ atom ` ys \ x \ supp S \ x \ f xs T" + and eqv: "\p. p \ T = S \ supp p \ atom ` xs \ supp T \ atom ` ys \ supp S + \ p \ (atom ` xs \ supp T) = atom ` ys \ supp S + \ p \ (f xs T) = f ys S" + shows "f xs T = f ys S" + using e apply - + apply (subst (asm) Abs_eq_res_set) + apply (subst (asm) Abs_eq_iff2) + apply (simp add: alphas) + apply (elim exE conjE) + apply(rule trans) + apply (rule_tac p="p" in supp_perm_eq[symmetric]) + apply(rule fresh_star_supp_conv) + apply(drule fresh_star_perm_set_conv) + apply (rule finite_Diff) + apply (rule finite_supp) + apply (subgoal_tac "(atom ` xs \ supp T \ atom ` ys \ supp S) \* f xs T") + apply (metis Un_absorb2 fresh_star_Un) + apply (subst fresh_star_Un) + apply (rule conjI) + apply (simp add: fresh_star_def f1) + apply (simp add: fresh_star_def f2) + apply (simp add: eqv) + done + nominal_primrec substs :: "(name \ ty2) list \ tys2 \ tys2" where @@ -389,33 +414,17 @@ apply auto[2] apply (rule_tac y="b" and c="a" in tys2.strong_exhaust) apply auto - apply (subst (asm) Abs_eq_res_set) - apply (subst (asm) Abs_eq_iff2) - apply (clarify) - apply (simp add: alphas) - apply (clarify) - apply (rule trans) - apply(rule_tac p="p" in supp_perm_eq[symmetric]) - apply(rule fresh_star_supp_conv) - apply(drule fresh_star_perm_set_conv) - apply (rule finite_Diff) - apply (rule finite_supp) - apply (subgoal_tac "(atom ` fset xs \ supp t \ atom ` fset xsa \ supp (p \ t)) \* ([atom ` fset xs]res. subst \' t)") - apply (metis Un_absorb2 fresh_star_Un) - apply (subst fresh_star_Un) - apply (rule conjI) - apply (simp (no_asm) add: fresh_star_def) - apply (rule) + apply (erule Abs_res_fcb) + apply (simp add: Abs_fresh_iff) apply (simp add: Abs_fresh_iff) - apply (simp add: fresh_star_def) - apply (rule) - apply (simp (no_asm) add: Abs_fresh_iff) apply auto[1] - apply (simp add: fresh_def supp_Abs) + apply (simp add: fresh_def fresh_star_def) apply (rule contra_subsetD) apply (rule supp_subst) - apply auto[1] apply simp + apply blast + apply (simp add: subst_eqvt) + apply clarify apply (subst Abs_eq_iff) apply (rule_tac x="0::perm" in exI) apply (subgoal_tac "p \ subst \' t = subst \' (p \ t)") @@ -428,19 +437,20 @@ apply (metis Diff_partition fresh_star_Un) apply (simp add: fresh_star_Un fresh_star_inter1) apply (simp add: alphas fresh_star_zero) + apply (simp add: subst_eqvt) apply auto[1] apply (subgoal_tac "atom xa \ p \ (atom ` fset xs \ supp t)") apply (simp add: inter_eqvt) apply blast apply (subgoal_tac "atom xa \ supp(p \ t)") - apply (simp add: IntI image_eqI) + apply (auto simp add: IntI image_eqI) apply (drule subsetD[OF supp_subst]) apply (simp add: fresh_star_def fresh_def) apply (subgoal_tac "x \ p \ (atom ` fset xs \ supp t)") apply (simp add: ) apply (subgoal_tac "x \ supp(p \ t)") apply (metis inf1I inter_eqvt mem_def supp_eqvt ) - apply (rotate_tac 6) + apply (rotate_tac 4) apply (drule sym) apply (simp add: subst_eqvt) apply (drule subsetD[OF supp_subst])