# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1307585441 -32400
# Node ID bcf48a1cb24b01b807172b2cdd0810a536c2fa2d
# Parent  36544bac1659ca1e3d2d833fed0d7b41152a0531
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.

diff -r 36544bac1659 -r bcf48a1cb24b Nominal/Ex/TypeSchemes.thy
--- a/Nominal/Ex/TypeSchemes.thy	Thu Jun 09 09:44:51 2011 +0900
+++ b/Nominal/Ex/TypeSchemes.thy	Thu Jun 09 11:10:41 2011 +0900
@@ -4,6 +4,7 @@
 
 section {*** Type Schemes ***}
 
+thm Set.set_mp Set.subsetD
 
 atom_decl name 
 
@@ -75,15 +76,48 @@
 
 --"The following is accepted by 'function' but not by 'nominal_primrec'"
 
-function (default "\<lambda>(x :: (name \<times> ty) list \<times> ty + (name \<times> ty) list \<times> tys). sum_case (\<lambda>x. Inl (undefined :: ty)) (\<lambda>x. Inr (undefined :: tys)) x")
+function (default "sum_case (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)")
     subst  :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty"
 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys"
 where
   "subst \<theta> (Var X) = lookup \<theta> X"
 | "subst \<theta> (Fun T1 T2) = Fun (subst \<theta> T1) (subst \<theta> T2)"
 | "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs T) = All xs (subst \<theta> T)"
+thm subst_substs_graph_def
+thm subst_substs_sumC_def
 oops
 
+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 = supp S - atom ` ys \<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 (subgoal_tac "supp T - atom ` xs = supp S - atom ` ys")
+  apply (simp add: fresh_star_def f2)
+  apply blast
+  apply (simp add: eqv)
+  done
+
 nominal_primrec (default "\<lambda>(x :: (name \<times> ty) list \<times> ty + (name \<times> ty) list \<times> tys). MYUNDEFINED :: ty + tys")
     subst  :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty"
 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys"
@@ -120,13 +154,9 @@
 apply(drule_tac x="xa" in meta_spec)
 apply(simp)
 --"Eqvt One way"
-thm subst_substs_graph.induct
-thm subst_substs_graph.intros
-thm Projl.simps
 apply(erule subst_substs_graph.induct)
 apply(perm_simp)
 apply(rule subst_substs_graph.intros)
-thm subst_substs_graph.cases
 apply(erule subst_substs_graph.cases)
 apply(simp (no_asm_use) only: eqvts)
 apply(subst test)
@@ -211,11 +241,10 @@
 apply (auto)[1]
 apply (auto)[5]
 --"LAST GOAL"
-apply(simp del: ty_tys.eq_iff)
 apply (simp add: meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff])
 apply (subgoal_tac "eqvt_at (\<lambda>(l, r). subst l r) (\<theta>', T)")
 apply (thin_tac "eqvt_at subst_substs_sumC (Inl (\<theta>', T))")
-defer
+prefer 2
 apply (simp add: eqvt_at_def subst_def)
 apply rule
 apply (subgoal_tac "\<And>x. subst_substs_sumC (Inl (x)) = Inl (?y x)")
@@ -248,89 +277,43 @@
 apply clarify
 --"This is exactly the assumption for the properly defined function"
 defer
-apply (simp only: Abs_eq_res_set)
-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)")
-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)
-thm fresh_star_perm_set_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 \<inter> supp (subst \<theta>' T)]set. subst \<theta>' T)")
-apply (metis Un_absorb2 fresh_star_Un)
-apply (simp add: fresh_star_Un)
-apply (rule conjI)
-apply (simp (no_asm) add: fresh_star_def)
-
-apply rule
-apply(simp (no_asm) only: Abs_fresh_iff)
-apply(clarify)
-apply auto[1]
-apply (simp add: fresh_star_def fresh_def)
-
-apply (simp (no_asm) add: fresh_star_def)
-apply rule
-apply auto[1]
-apply(simp (no_asm) only: Abs_fresh_iff)
-apply(clarify)
-apply auto[1]
-apply(drule_tac a="atom x" in fresh_eqvt_at)
-apply (simp add: supp_Pair finite_supp)
-apply (simp add: fresh_Pair)
-apply(auto simp add: Abs_fresh_iff fresh_star_def)[2]
-apply (simp add: fresh_def)
-apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'")
-prefer 2
-apply (rule perm_supp_eq)
-apply (subgoal_tac "(atom ` fset xs \<inter> supp T \<union> atom ` fset xsa \<inter> supp (p \<bullet> T)) \<sharp>* \<theta>'")
-apply (auto simp add: fresh_star_def)[1]
-apply (simp add: fresh_star_Un fresh_star_def)
-apply blast
-apply(simp add: eqvt_at_def inter_eqvt supp_eqvt)
-apply (simp only: Abs_eq_res_set[symmetric])
-apply (simp add: Abs_eq_iff alphas)
-apply rule
-prefer 2
-apply (rule_tac x="0 :: perm" in exI)
-apply (simp add: fresh_star_zero)
-apply (rule helper)
-prefer 3
-apply (subgoal_tac "supp ((\<lambda>(l, r). subst l r) (\<theta>', (p \<bullet> T))) \<subseteq> supp \<theta>' \<union> supp (p \<bullet> T)")
-apply simp
-apply (subst supp_Pair[symmetric])
-apply (rule supp_eqvt_at)
-apply (simp add: eqvt_at_def)
-apply (thin_tac " p \<bullet> atom ` fset xs \<inter> supp (p \<bullet> T) = atom ` fset xsa \<inter> supp (p \<bullet> T)")
-apply (thin_tac "supp T - atom ` fset xs \<inter> supp T = supp (p \<bullet> T) - atom ` fset xsa \<inter> supp (p \<bullet> T)")
-apply (thin_tac "supp p \<subseteq> atom ` fset xs \<inter> supp T \<union> atom ` fset xsa \<inter> supp (p \<bullet> T)")
-apply (thin_tac "(atom ` fset xsa \<inter> supp (p \<bullet> T) - atom ` fset xs \<inter> supp T) \<sharp>* ([atom ` fset xs \<inter> supp (subst \<theta>' T)]set. T)")
-apply (thin_tac "atom ` fset xs \<sharp>* \<theta>'")
-apply (thin_tac "atom ` fset xsa \<sharp>* \<theta>'")
-apply (thin_tac "(supp (p \<bullet> T) - atom ` fset xsa \<inter> supp (p \<bullet> T)) \<sharp>* p")
-apply (rule)
-apply (subgoal_tac "\<forall>p. p \<bullet> subst \<theta>' T = subst (p \<bullet> \<theta>') (p \<bullet> T)")
-apply (erule_tac x="p" in allE)
-apply (erule_tac x="pa + p" in allE)
-apply (metis permute_plus)
-apply assumption
-apply (simp add: supp_Pair finite_supp)
-prefer 2 apply blast
-prefer 2 apply (metis finite_UNIV finite_imageI obtain_at_base rangeI)
-apply (rule_tac s="supp \<theta>'" in trans)
-apply (subgoal_tac "(p \<bullet> atom ` fset xs) \<sharp>* \<theta>'")
-apply (auto simp add: fresh_star_def fresh_def)[1]
-apply (subgoal_tac "supp p \<sharp>* \<theta>'")
-apply (metis fresh_star_permute_iff)
-apply (subgoal_tac "(atom ` fset xs \<union> atom ` fset xsa) \<sharp>* \<theta>'")
-apply (auto simp add: fresh_star_def)[1]
-apply (simp add: fresh_star_Un)
-apply (auto simp add: fresh_star_def fresh_def)[1]
-oops
+apply clarify
+  apply (frule supp_eqvt_at)
+  apply (simp add: finite_supp)
+  apply (erule Abs_res_fcb)
+  apply (simp add: Abs_fresh_iff)
+  apply (simp add: Abs_fresh_iff)
+  apply auto[1]
+  apply (simp add: fresh_def fresh_star_def)
+  apply (erule contra_subsetD)
+  apply (simp add: supp_Pair)
+  apply blast
+  apply clarify
+  apply (simp)
+  apply (simp add: eqvt_at_def)
+  apply (subst Abs_eq_iff)
+  apply (rule_tac x="0::perm" in exI)
+  apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'")
+  apply (simp add: alphas fresh_star_zero)
+  apply (subgoal_tac "\<And>x. x \<in> supp (subst \<theta>' (p \<bullet> T)) \<Longrightarrow> x \<in> p \<bullet> atom ` fset xs \<longleftrightarrow> x \<in> atom ` fset xsa")
+  apply blast
+  apply (subgoal_tac "x \<in> supp(p \<bullet> \<theta>', p \<bullet> T)")
+  apply (simp add: supp_Pair eqvts eqvts_raw)
+  apply auto[1]
+  apply (subgoal_tac "(atom ` fset (p \<bullet> xs)) \<sharp>* \<theta>'")
+  apply (simp add: fresh_star_def fresh_def)
+  apply(drule_tac p1="p" in iffD2[OF fresh_star_permute_iff])
+  apply (simp add: eqvts eqvts_raw)
+  apply (simp add: fresh_star_def fresh_def)
+  apply (simp (no_asm) only: supp_eqvt[symmetric] Pair_eqvt[symmetric])
+  apply (subgoal_tac "p \<bullet> supp (subst \<theta>' T) \<subseteq> p \<bullet> supp (\<theta>', T)")
+  apply (erule subsetD)
+  apply (simp add: supp_eqvt)
+  apply (metis le_eqvt permute_boolI)
+  apply (rule perm_supp_eq)
+  apply (simp add: fresh_def fresh_star_def)
+  apply blast
+  oops
 
 section {* defined as two separate nominal datatypes *}
 
@@ -401,37 +384,6 @@
   "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 = supp S - atom ` ys \<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 (subgoal_tac "supp T - atom ` xs = supp S - atom ` ys")
-  apply (simp add: fresh_star_def f2)
-  apply blast
-  apply (simp add: eqv)
-  done
-
 nominal_primrec
   substs :: "(name \<times> ty2) list \<Rightarrow> tys2 \<Rightarrow> tys2"
 where
@@ -455,23 +407,18 @@
   apply (rule_tac x="0::perm" in exI)
   apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'")
   apply (simp add: alphas fresh_star_zero)
-  apply auto[1]
-  apply (subgoal_tac "atom xa \<in> p \<bullet> (atom ` fset xs \<inter> supp t)")
-  apply (simp add: inter_eqvt)
+  apply (subgoal_tac "\<And>x. x \<in> supp (subst \<theta>' (p \<bullet> t)) \<Longrightarrow> x \<in> p \<bullet> atom ` fset xs \<longleftrightarrow> x \<in> atom ` fset xsa")
   apply blast
-  apply (subgoal_tac "atom xa \<in> supp(p \<bullet> t)")
-  apply (auto simp add: IntI image_eqI)
-  apply (drule subsetD[OF supp_subst])
+  apply (subgoal_tac "x \<in> supp(p \<bullet> \<theta>', p \<bullet> t)")
+  apply (simp add: supp_Pair eqvts eqvts_raw)
+  apply auto[1]
+  apply (subgoal_tac "(atom ` fset (p \<bullet> xs)) \<sharp>* \<theta>'")
   apply (simp add: fresh_star_def fresh_def)
-  apply (subgoal_tac "x \<in> p \<bullet> (atom ` fset xs \<inter> supp t)")
-  apply (simp)
-  apply (subgoal_tac "x \<in> supp(p \<bullet> t)")
-  apply (metis inf1I inter_eqvt mem_def supp_eqvt)
-  apply (subgoal_tac "x \<notin> supp \<theta>'")
-  apply (metis UnE subsetD supp_subst)
-  apply (subgoal_tac "(p \<bullet> (atom ` fset xs)) \<sharp>* (p \<bullet> \<theta>')")
+  apply(drule_tac p1="p" in iffD2[OF fresh_star_permute_iff])
+  apply (simp add: eqvts eqvts_raw)
   apply (simp add: fresh_star_def fresh_def)
-  apply (simp (no_asm) add: fresh_star_permute_iff)
+  apply (drule subsetD[OF supp_subst])
+  apply (simp add: supp_Pair)
   apply (rule perm_supp_eq)
   apply (simp add: fresh_def fresh_star_def)
   apply blast