# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1307519041 -3600
# Node ID 3503432262dc5f4aa905447880cfef4409fdc851
# Parent  394664816e24e8b6e4f5dd1341b44ef6c55ad4d9
using the option "default" the function package allows one to give an explicit default value

diff -r 394664816e24 -r 3503432262dc Nominal/Ex/TypeSchemes.thy
--- a/Nominal/Ex/TypeSchemes.thy	Tue Jun 07 20:58:00 2011 +0100
+++ b/Nominal/Ex/TypeSchemes.thy	Wed Jun 08 08:44:01 2011 +0100
@@ -71,13 +71,28 @@
 using assms
 by blast
 
-nominal_primrec
+definition "MYUNDEFINED \<equiv> undefined"
+
+nominal_primrec (default "\<lambda>x. MYUNDEFINED")
     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
 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)