--- a/Nominal/Ex/TypeSchemes.thy	Tue Jun 14 19:11:44 2011 +0100
+++ b/Nominal/Ex/TypeSchemes.thy	Wed Jun 15 09:31:59 2011 +0900
@@ -43,9 +43,10 @@
 done
 
 lemma test:
-  assumes a: "f x = Inl y"
+  assumes a: "\<exists>y. f x = Inl y"
   shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl ((p \<bullet> f) (p \<bullet> x))"
-using a 
+using a
+apply clarify
 apply(frule_tac p="p" in permute_boolI)
 apply(simp (no_asm_use) only: eqvts)
 apply(subst (asm) permute_fun_app_eq)
@@ -54,9 +55,10 @@
 done
 
 lemma test2:
-  assumes a: "f x = Inl y"
+  assumes a: "\<exists>y. f x = Inl y"
   shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl (p \<bullet> (f x))"
-using a 
+using a
+apply clarify
 apply(frule_tac p="p" in permute_boolI)
 apply(simp (no_asm_use) only: eqvts)
 apply(subst (asm) permute_fun_app_eq)
@@ -64,16 +66,6 @@
 apply(simp)
 done
 
-lemma helper:
-  assumes "A - C = A - D"
-  and "B - C = B - D"
-  and "E \<subseteq> A \<union> B"
-  shows "E - C = E - D"
-using assms
-by blast
-
---"The following is accepted by 'function' but not by 'nominal_primrec'"
-
 nominal_primrec (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"
@@ -81,31 +73,16 @@
   "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
-
-
-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"
-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
-
-nominal_primrec
-    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
+(*unfolding subst_substs_graph_def eqvt_def
+apply rule
+apply perm_simp
+apply (subst test3)
+defer
+apply (subst test3)
+defer
+apply (subst test3)
+defer
+apply rule*)
 apply(subgoal_tac "\<And>p x r. subst_substs_graph x r \<Longrightarrow> subst_substs_graph (p \<bullet> x) (p \<bullet> r)")
 apply(simp add: eqvt_def)
 apply(rule allI)
@@ -129,11 +106,13 @@
 apply(simp (no_asm_use) only: eqvts)
 apply(subst test)
 back
+apply (rule exI)
 apply(assumption)
 apply(rotate_tac 1)
 apply(erule subst_substs_graph.cases)
 apply(subst test)
 back
+apply (rule exI)
 apply(assumption)
 apply(perm_simp)
 apply(rule subst_substs_graph.intros)
@@ -141,6 +120,7 @@
 apply(assumption)
 apply(subst test)
 back
+apply (rule exI)
 apply(assumption)
 apply(perm_simp)
 apply(rule subst_substs_graph.intros)
@@ -151,11 +131,13 @@
 apply(simp (no_asm_use) only: eqvts)
 apply(subst test)
 back
+apply (rule exI)
 apply(assumption)
 apply(rotate_tac 1)
 apply(erule subst_substs_graph.cases)
 apply(subst test)
 back
+apply (rule exI)
 apply(assumption)
 apply(perm_simp)
 apply(rule subst_substs_graph.intros)
@@ -163,6 +145,7 @@
 apply(assumption)
 apply(subst test)
 back
+apply (rule exI)
 apply(assumption)
 apply(perm_simp)
 apply(rule subst_substs_graph.intros)
@@ -176,6 +159,7 @@
 apply(subst test)
 back
 back
+apply (rule exI)
 apply(assumption)
 apply(rule subst_substs_graph.intros)
 apply (simp add: eqvts)
@@ -188,6 +172,7 @@
 apply(subst test)
 back
 back
+apply (rule exI)
 apply(assumption)
 apply(rule subst_substs_graph.intros)
 apply (simp add: eqvts)
@@ -215,16 +200,10 @@
 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)")
 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: subst_substs_sumC_def)
 apply (simp add: THE_default_def)
-apply (case_tac "Ex1 (subst_substs_graph (Inl y))")
+apply (case_tac "Ex1 (subst_substs_graph (Inl (\<theta>', T)))")
 prefer 2
 apply simp
 apply (simp add: the1_equality)
@@ -243,8 +222,8 @@
 apply (rule the1_equality)
 apply metis apply assumption
 apply clarify
---"This is exactly the assumption for the properly defined function"
-defer
+apply simp
+--"-"
 apply clarify
   apply (frule supp_eqvt_at)
   apply (simp add: finite_supp)
@@ -281,7 +260,7 @@
   apply (rule perm_supp_eq)
   apply (simp add: fresh_def fresh_star_def)
   apply blast
-  oops
+  done
 
 section {* defined as two separate nominal datatypes *}