--- a/Nominal/Ex/TypeSchemes.thy	Thu Jan 27 20:19:13 2011 +0100
+++ b/Nominal/Ex/TypeSchemes.thy	Sat Jan 29 14:26:47 2011 +0900
@@ -87,12 +87,16 @@
 apply(simp)
 done
 
-lemma
-  "(p \<bullet> (Sum_Type.Projl x)) = Sum_Type.Projl (p \<bullet> x)"
-apply(case_tac x)
+lemma test2:
+  assumes a: "f x = Inl y"
+  shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl (p \<bullet> (f x))"
+using a 
+apply(frule_tac p="p" in permute_boolI)
+apply(simp (no_asm_use) only: eqvts)
+apply(subst (asm) permute_fun_app_eq)
+back
 apply(simp)
-apply(simp)
-
+done
 
 nominal_primrec
     subst  :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty"
@@ -123,6 +127,7 @@
 apply(drule_tac x="x" in meta_spec)
 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
@@ -183,7 +188,10 @@
 back
 apply(assumption)
 apply(rule subst_substs_graph.intros)
-defer
+apply (simp add: eqvts)
+apply (subgoal_tac "(p \<bullet> (atom ` fset xs)) \<sharp>* (p \<bullet> \<theta>)")
+apply (simp add: image_eqvt eqvts_raw eqvts)
+apply (simp add: fresh_star_permute_iff)
 apply(perm_simp)
 apply(assumption)
 apply(simp (no_asm_use) only: eqvts)
@@ -192,61 +200,90 @@
 back
 apply(assumption)
 apply(rule subst_substs_graph.intros)
-defer
+apply (simp add: eqvts)
+apply (subgoal_tac "(p \<bullet> (atom ` fset xs)) \<sharp>* (p \<bullet> \<theta>)")
+apply (simp add: image_eqvt eqvts_raw eqvts)
+apply (simp add: fresh_star_permute_iff)
 apply(perm_simp)
 apply(assumption)
 apply(simp)
-apply(simp_all add: ty_tys.distinct)
+--"Eqvt done"
+apply (case_tac x)
+apply simp apply clarify 
+apply (rule_tac y="b" in ty_tys.exhaust(1))
+apply (auto simp add: ty_tys.eq_iff)[1]
+apply (auto simp add: ty_tys.eq_iff)[1]
+apply blast
+apply simp apply clarify 
+apply (rule_tac ya="b" and c="a" in ty_tys.strong_exhaust(2))
+apply (auto simp add: ty_tys.eq_iff)[1]
+apply (auto simp add: ty_tys.distinct)
+apply (auto simp add: ty_tys.eq_iff ty_tys.distinct)[2]
+--"LAST GOAL"
+thm meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_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
-apply(simp add: ty_tys.eq_iff)
-apply(simp add: ty_tys.eq_iff)
-apply(erule conjE)+
-apply(simp add: ty_tys.eq_iff)
-apply(subst (asm) Abs_eq_iff2)
-apply(erule exE)
-apply(simp add: alphas)
+apply (simp add: eqvt_at_def subst_def)
+apply rule
+apply (subgoal_tac "\<And>x. subst_substs_sumC (Inl (x)) = Inl (?y x)")
+apply (subst test2)
+apply (drule_tac x="(\<theta>', T)" in meta_spec)
+apply assumption
+apply simp
+--"We require that for Inl it returns Inl. It doesn't work for undefined, but it does work for the following"
+ apply (subgoal_tac "\<And>y. \<exists>z. (\<lambda>x. THE_default (sum_case (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined) x) (subst_substs_graph x)) (Inl y) = (Inl z)")
+prefer 2
+apply (simp add: THE_default_def)
+apply (case_tac "Ex1 (subst_substs_graph (Inl y))")
+prefer 2
+apply simp
+apply (simp add: the1_equality)
+apply auto[1]
+apply (erule_tac x="x" in allE)
+apply simp
+apply(cases rule: subst_substs_graph.cases)
+apply assumption
+apply (rule_tac x="lookup \<theta> X" in exI)
+apply clarify
+apply (rule the1_equality)
+apply metis apply assumption
+apply (rule_tac x="(Fun (Sum_Type.Projl (subst_substs_sum (Inl (\<theta>, T1))))
+                  (Sum_Type.Projl (subst_substs_sum (Inl (\<theta>, T2)))))" in exI)
+apply clarify
+apply (rule the1_equality)
+apply metis apply assumption
+apply clarify
+--"This is exactly the assumption for the properly defined function"
+defer
+apply (simp add: ty_tys.eq_iff)
+apply (subst (asm) Abs_eq_iff2)
+apply (simp add: alpha_res.simps)
+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 \<union> atom ` fset xsa) \<sharp>* ([atom ` fset xs]res. subst \<theta>' T)")
+apply (metis Un_absorb2 fresh_star_Un)
+apply (simp add: fresh_star_Un)
+apply (rule conjI)
+apply (simp add: fresh_star_def)
+apply rule
+apply(simp (no_asm) only: Abs_fresh_iff)
 apply(clarify)
-thm subst_def
-
-
-apply(assumption)
-apply(subst test)
-back
-apply(assumption)
-apply(perm_simp)
-apply(rule subst_substs_graph.intros)
-apply(assumption)
-apply(assumption)
-apply(subst test)
-back
-apply(assumption)
-apply(perm_simp)
-apply(rule subst_substs_graph.intros)
-apply(assumption)
-apply(assumption)
-apply(simp)
-
-
-apply(rotate_tac 1)
-apply(erule subst_substs_graph.cases)
-apply(subst test)
-back
-apply(assumption)
-
-
-apply(auto)[4]
-thm  subst_substs_graph.cases
-thm subst_substs_graph.intros
-thm subst_substs_graph.intros(2)[THEN permute_boolI]
-term subst_substs_graph
-apply(simp only: eqvts)
-thm Projl.simps
-term Inl
-term Inr
-apply(perm_simp)
-thm subst_substs_graph.intros
-apply(simp add: permute_fun_def)
-thm Projl.simps
+apply blast
+defer
+apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'")
+prefer 2
+apply (rule perm_supp_eq)
+apply (metis Un_absorb2 fresh_star_Un)
+apply simp
+--"Would work for 'set' and 'list' bindings, not sure how to do 'set+'."
 oops