--- a/Nominal/Ex/TypeSchemes.thy	Tue Jan 25 02:51:44 2011 +0900
+++ b/Nominal/Ex/TypeSchemes.thy	Tue Jan 25 18:58:26 2011 +0100
@@ -28,6 +28,60 @@
 thm ty_tys.supp
 thm ty_tys.fresh
 
+fun
+  lookup :: "(name \<times> ty) list \<Rightarrow> name \<Rightarrow> ty"
+where
+  "lookup [] Y = Var Y"
+| "lookup ((X, T) # Ts) Y = (if X = Y then T else lookup Ts Y)"
+
+lemma lookup_eqvt[eqvt]:
+  shows "(p \<bullet> lookup Ts T) = lookup (p \<bullet> Ts) (p \<bullet> T)"
+apply(induct Ts T rule: lookup.induct)
+apply(simp_all)
+done
+
+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)"
+term subst_substs_sumC
+term Inl
+thm subst_substs_graph.induct
+thm subst_substs_graph.intros
+thm Projl.simps
+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)
+apply(simp add: permute_fun_def permute_bool_def)
+apply(rule ext)
+apply(rule ext)
+apply(rule iffI)
+apply(drule_tac x="p" in meta_spec)
+apply(drule_tac x="- p \<bullet> x" in meta_spec)
+apply(drule_tac x="- p \<bullet> xa" in meta_spec)
+apply(simp)
+apply(drule_tac x="-p" in meta_spec)
+apply(drule_tac x="x" in meta_spec)
+apply(drule_tac x="xa" in meta_spec)
+apply(simp)
+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)
+apply(simp only: eqvts)
+thm Projl.simps
+term Inl
+term Inr
+apply(perm_simp)
+thm subst_substs_graph.intros
+thm Projl.simps
+oops
+
 
 section {* defined as two separate nominal datatypes *}
 
@@ -52,22 +106,23 @@
 thm tys2.fresh
 
 fun
-  lookup :: "(name \<times> ty2) list \<Rightarrow> name \<Rightarrow> ty2"
+  lookup2 :: "(name \<times> ty2) list \<Rightarrow> name \<Rightarrow> ty2"
 where
-  "lookup [] Y = Var2 Y"
-| "lookup ((X, T) # Ts) Y = (if X = Y then T else lookup Ts Y)"
+  "lookup2 [] Y = Var2 Y"
+| "lookup2 ((X, T) # Ts) Y = (if X = Y then T else lookup2 Ts Y)"
 
-lemma lookup_eqvt[eqvt]:
-  shows "(p \<bullet> lookup Ts T) = lookup (p \<bullet> Ts) (p \<bullet> T)"
-apply(induct Ts T rule: lookup.induct)
+lemma lookup2_eqvt[eqvt]:
+  shows "(p \<bullet> lookup2 Ts T) = lookup2 (p \<bullet> Ts) (p \<bullet> T)"
+apply(induct Ts T rule: lookup2.induct)
 apply(simp_all)
 done
 
-function
+nominal_primrec
   subst  :: "(name \<times> ty2) list \<Rightarrow> ty2 \<Rightarrow> ty2"
 where
-  "subst \<theta> (Var2 X) = lookup \<theta> X"
+  "subst \<theta> (Var2 X) = lookup2 \<theta> X"
 | "subst \<theta> (Fun2 T1 T2) = Fun2 (subst \<theta> T1) (subst \<theta> T2)"
+defer
 apply(case_tac x)
 apply(simp)
 apply(rule_tac y="b" in ty2.exhaust)
@@ -76,6 +131,28 @@
 apply(simp_all add: ty2.distinct)
 apply(simp add: ty2.eq_iff)
 apply(simp add: ty2.eq_iff)
+apply(subgoal_tac "\<And>p x r. subst_graph x r \<Longrightarrow> subst_graph (p \<bullet> x) (p \<bullet> r)")
+apply(simp add: eqvt_def)
+apply(rule allI)
+apply(simp add: permute_fun_def permute_bool_def)
+apply(rule ext)
+apply(rule ext)
+apply(rule iffI)
+apply(drule_tac x="p" in meta_spec)
+apply(drule_tac x="- p \<bullet> x" in meta_spec)
+apply(drule_tac x="- p \<bullet> xa" in meta_spec)
+apply(simp)
+apply(drule_tac x="-p" in meta_spec)
+apply(drule_tac x="x" in meta_spec)
+apply(drule_tac x="xa" in meta_spec)
+apply(simp)
+apply(erule subst_graph.induct)
+apply(perm_simp)
+apply(rule subst_graph.intros)
+apply(perm_simp)
+apply(rule subst_graph.intros)
+apply(assumption)
+apply(assumption)
 done
 
 termination
@@ -86,14 +163,14 @@
 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: lookup_eqvt)
+apply(simp_all add: lookup2_eqvt)
 done
 
 lemma j:
   assumes "a \<sharp> Ts" " a \<sharp> X"
-  shows "a \<sharp> lookup Ts X"
+  shows "a \<sharp> lookup2 Ts X"
 using assms
-apply(induct Ts X rule: lookup.induct)
+apply(induct Ts X rule: lookup2.induct)
 apply(auto simp add: ty2.fresh fresh_Cons fresh_Pair)
 done