equal
deleted
inserted
replaced
1 theory TypeSchemes2 |
1 theory TypeSchemes2 |
2 imports "../Nominal2" |
2 imports "../Nominal2" |
3 begin |
3 begin |
4 |
4 |
|
5 |
5 section {*** Type Schemes defined as a single nominal datatype ***} |
6 section {*** Type Schemes defined as a single nominal datatype ***} |
6 |
7 |
7 atom_decl name |
8 atom_decl name |
8 |
9 |
9 nominal_datatype ty = |
10 nominal_datatype ty = |
58 lemma test2: |
59 lemma test2: |
59 assumes a: "\<exists>y. f x = Inl y" |
60 assumes a: "\<exists>y. f x = Inl y" |
60 shows "(p \<bullet> (Sum_Type.projl (f x))) = Sum_Type.projl (p \<bullet> (f x))" |
61 shows "(p \<bullet> (Sum_Type.projl (f x))) = Sum_Type.projl (p \<bullet> (f x))" |
61 using a |
62 using a |
62 by clarsimp |
63 by clarsimp |
63 |
64 |
64 nominal_function (default "case_sum (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)") |
65 nominal_function (default "case_sum (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)") |
65 subst :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty" |
66 subst :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty" |
66 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" |
67 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" |
67 where |
68 where |
68 "subst \<theta> (Var X) = lookup \<theta> X" |
69 "subst \<theta> (Var X) = lookup \<theta> X" |
69 | "subst \<theta> (Fun T1 T2) = Fun (subst \<theta> T1) (subst \<theta> T2)" |
70 | "subst \<theta> (Fun T1 T2) = Fun (subst \<theta> T1) (subst \<theta> T2)" |
70 | "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs T) = All xs (subst \<theta> T)" |
71 | "fset (atom |`| xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs T) = All xs (subst \<theta> T)" |
71 thm subst_substs_graph_def subst_substs_graph_aux_def |
72 thm subst_substs_graph_def subst_substs_graph_aux_def |
72 apply(simp add: subst_substs_graph_aux_def eqvt_def) |
73 apply(simp add: subst_substs_graph_aux_def eqvt_def) |
73 apply(rule TrueI) |
74 apply(rule TrueI) |
74 apply (case_tac x) |
75 apply (case_tac x) |
75 apply simp apply clarify |
76 apply simp apply clarify |