# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1307580291 -32400
# Node ID 36544bac1659ca1e3d2d833fed0d7b41152a0531
# Parent  c78c2d565e999122098f7ec06684a11abd2a86af
More experiments with 'default'

diff -r c78c2d565e99 -r 36544bac1659 Nominal/Ex/TypeSchemes.thy
--- a/Nominal/Ex/TypeSchemes.thy	Wed Jun 08 21:44:03 2011 +0900
+++ b/Nominal/Ex/TypeSchemes.thy	Thu Jun 09 09:44:51 2011 +0900
@@ -71,10 +71,18 @@
 using assms
 by blast
 
---"The following two terms have the same type, however the first one is a valid default, but the second one no"
 definition "MYUNDEFINED \<equiv> undefined"
-term "\<lambda>(x :: (name \<times> ty) list \<times> ty + (name \<times> ty) list \<times> tys). MYUNDEFINED :: ty + tys"
-term "\<lambda>(x :: (name \<times> ty) list \<times> ty + (name \<times> ty) list \<times> tys). sum_case (\<lambda>x. Inl (undefined :: ty)) (\<lambda>x. Inr (undefined :: tys)) x"
+
+--"The following is accepted by 'function' but not by 'nominal_primrec'"
+
+function (default "\<lambda>(x :: (name \<times> ty) list \<times> ty + (name \<times> ty) list \<times> tys). sum_case (\<lambda>x. Inl (undefined :: ty)) (\<lambda>x. Inr (undefined :: tys)) x")
+    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)"
+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"