# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1307532656 -3600
# Node ID 80bbb023402577460f94b5d0bdae3e336230bfd4
# Parent  71382ce4d2ed2157162f8a41cff58c89d7080a83# Parent  76db0b854bf626d94067da8e6d8bf2b583ac300a
merged

diff -r 76db0b854bf6 -r 80bbb0234025 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Wed Jun 08 17:52:06 2011 +0900
+++ b/Nominal/Ex/Lambda.thy	Wed Jun 08 12:30:56 2011 +0100
@@ -618,6 +618,25 @@
 apply(simp_all add: permute_pure)
 done
 
+(* function that evaluates a lambda term *)
+nominal_primrec
+   eval :: "lam \<Rightarrow> lam" and
+   app :: "lam \<Rightarrow> lam \<Rightarrow> lam"
+where
+  "eval (Var x) = Var x"
+| "eval (Lam [x].t) = Lam [x].(eval t)"
+| "eval (App t1 t2) = sub (eval t1) (eval t2)"
+| "app (Var x) t2 = App (Var x) t2"
+| "app (App t0 t1) t2 = App (App t0 t1) t2"
+| "app (Lam [x].t1) t2 = eval (t1[x::= t2])"
+apply(simp add: eval_app_graph_def eqvt_def)
+apply(perm_simp)
+apply(simp)
+apply(rule TrueI)
+defer
+apply(simp_all)
+defer
+oops (* can this be defined ? *)
 
 text {* tests of functions containing if and case *}
 
@@ -725,6 +744,9 @@
 
 
 
+
+
+
 end
 
 
diff -r 76db0b854bf6 -r 80bbb0234025 Nominal/Ex/TypeSchemes.thy
--- a/Nominal/Ex/TypeSchemes.thy	Wed Jun 08 17:52:06 2011 +0900
+++ b/Nominal/Ex/TypeSchemes.thy	Wed Jun 08 12:30:56 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)