--- 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 \<bullet> subst \<theta> T) = subst (p \<bullet> \<theta>) (p \<bullet> T)"
-apply(induct \<theta> T rule: subst.induct)
-apply(simp_all add: lookup2_eqvt)
-done
+ by (induct \<theta> 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 \<sharp>* z \<Longrightarrow> (xs \<inter> ys) \<sharp>* 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: "\<And>x. x \<in> atom ` xs \<Longrightarrow> x \<in> supp T \<Longrightarrow> x \<sharp> f xs T"
+ and f2: "\<And>x. supp T - atom ` xs \<inter> supp T = supp S - atom ` ys \<inter> supp S \<Longrightarrow> x \<in> atom ` ys \<Longrightarrow> x \<in> supp S \<Longrightarrow> x \<sharp> f xs T"
+ and eqv: "\<And>p. p \<bullet> T = S \<Longrightarrow> supp p \<subseteq> atom ` xs \<inter> supp T \<union> atom ` ys \<inter> supp S
+ \<Longrightarrow> p \<bullet> (atom ` xs \<inter> supp T) = atom ` ys \<inter> supp S
+ \<Longrightarrow> p \<bullet> (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 \<inter> supp T \<union> atom ` ys \<inter> supp S) \<sharp>* 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 \<times> ty2) list \<Rightarrow> tys2 \<Rightarrow> 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 \<inter> supp t \<union> atom ` fset xsa \<inter> supp (p \<bullet> t)) \<sharp>* ([atom ` fset xs]res. subst \<theta>' 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 \<bullet> subst \<theta>' t = subst \<theta>' (p \<bullet> 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 \<in> p \<bullet> (atom ` fset xs \<inter> supp t)")
apply (simp add: inter_eqvt)
apply blast
apply (subgoal_tac "atom xa \<in> supp(p \<bullet> 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 \<in> p \<bullet> (atom ` fset xs \<inter> supp t)")
apply (simp add: )
apply (subgoal_tac "x \<in> supp(p \<bullet> 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])