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" |
74 definition "MYUNDEFINED \<equiv> undefined" |
75 definition "MYUNDEFINED \<equiv> undefined" |
75 |
76 term "\<lambda>(x :: (name \<times> ty) list \<times> ty + (name \<times> ty) list \<times> tys). MYUNDEFINED :: ty + tys" |
76 nominal_primrec (default "\<lambda>x. MYUNDEFINED") |
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" |
|
78 |
|
79 nominal_primrec (default "\<lambda>(x :: (name \<times> ty) list \<times> ty + (name \<times> ty) list \<times> tys). MYUNDEFINED :: ty + tys") |
77 subst :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty" |
80 subst :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty" |
78 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" |
81 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" |
79 where |
82 where |
80 "subst \<theta> (Var X) = lookup \<theta> X" |
83 "subst \<theta> (Var X) = lookup \<theta> X" |
81 | "subst \<theta> (Fun T1 T2) = Fun (subst \<theta> T1) (subst \<theta> T2)" |
84 | "subst \<theta> (Fun T1 T2) = Fun (subst \<theta> T1) (subst \<theta> T2)" |