equal
deleted
inserted
replaced
69 and "E \<subseteq> A \<union> B" |
69 and "E \<subseteq> A \<union> B" |
70 shows "E - C = E - D" |
70 shows "E - C = E - D" |
71 using assms |
71 using assms |
72 by blast |
72 by blast |
73 |
73 |
74 --"The following two terms have the same type, however the first one is a valid default, but the second one no" |
|
75 definition "MYUNDEFINED \<equiv> undefined" |
74 definition "MYUNDEFINED \<equiv> undefined" |
76 term "\<lambda>(x :: (name \<times> ty) list \<times> ty + (name \<times> ty) list \<times> tys). MYUNDEFINED :: ty + tys" |
75 |
77 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" |
76 --"The following is accepted by 'function' but not by 'nominal_primrec'" |
|
77 |
|
78 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") |
|
79 subst :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty" |
|
80 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" |
|
81 where |
|
82 "subst \<theta> (Var X) = lookup \<theta> X" |
|
83 | "subst \<theta> (Fun T1 T2) = Fun (subst \<theta> T1) (subst \<theta> T2)" |
|
84 | "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs T) = All xs (subst \<theta> T)" |
|
85 oops |
78 |
86 |
79 nominal_primrec (default "\<lambda>(x :: (name \<times> ty) list \<times> ty + (name \<times> ty) list \<times> tys). MYUNDEFINED :: ty + tys") |
87 nominal_primrec (default "\<lambda>(x :: (name \<times> ty) list \<times> ty + (name \<times> ty) list \<times> tys). MYUNDEFINED :: ty + tys") |
80 subst :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty" |
88 subst :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty" |
81 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" |
89 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" |
82 where |
90 where |