equal
deleted
inserted
replaced
59 assumes a: "\<exists>y. f x = Inl y" |
59 assumes a: "\<exists>y. f x = Inl y" |
60 shows "(p \<bullet> (Sum_Type.projl (f x))) = Sum_Type.projl (p \<bullet> (f x))" |
60 shows "(p \<bullet> (Sum_Type.projl (f x))) = Sum_Type.projl (p \<bullet> (f x))" |
61 using a |
61 using a |
62 by clarsimp |
62 by clarsimp |
63 |
63 |
64 nominal_primrec (default "case_sum (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)") |
64 nominal_function (default "case_sum (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)") |
65 subst :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty" |
65 subst :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty" |
66 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" |
66 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" |
67 where |
67 where |
68 "subst \<theta> (Var X) = lookup \<theta> X" |
68 "subst \<theta> (Var X) = lookup \<theta> X" |
69 | "subst \<theta> (Fun T1 T2) = Fun (subst \<theta> T1) (subst \<theta> T2)" |
69 | "subst \<theta> (Fun T1 T2) = Fun (subst \<theta> T1) (subst \<theta> T2)" |