39 apply(simp_all) |
39 apply(simp_all) |
40 done |
40 done |
41 |
41 |
42 lemma TEST1: |
42 lemma TEST1: |
43 assumes "x = Inl y" |
43 assumes "x = Inl y" |
44 shows "(p \<bullet> Sum_Type.Projl x) = Sum_Type.Projl (p \<bullet> x)" |
44 shows "(p \<bullet> Sum_Type.projl x) = Sum_Type.projl (p \<bullet> x)" |
45 using assms by simp |
45 using assms by simp |
46 |
46 |
47 lemma TEST2: |
47 lemma TEST2: |
48 assumes "x = Inr y" |
48 assumes "x = Inr y" |
49 shows "(p \<bullet> Sum_Type.Projr x) = Sum_Type.Projr (p \<bullet> x)" |
49 shows "(p \<bullet> Sum_Type.projr x) = Sum_Type.projr (p \<bullet> x)" |
50 using assms by simp |
50 using assms by simp |
51 |
51 |
52 lemma test: |
52 lemma test: |
53 assumes a: "\<exists>y. f x = Inl y" |
53 assumes a: "\<exists>y. f x = Inl y" |
54 shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl ((p \<bullet> f) (p \<bullet> x))" |
54 shows "(p \<bullet> (Sum_Type.projl (f x))) = Sum_Type.projl ((p \<bullet> f) (p \<bullet> x))" |
55 using a |
55 using a TEST1 |
56 by (metis Inl_eqvt Projl_Inl permute_fun_app_eq) |
56 by (metis eqvt_bound eqvt_lambda permute_eq_iff) |
57 |
57 |
58 lemma test2: |
58 lemma test2: |
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 "sum_case (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)") |
64 nominal_primrec (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)" |
101 apply assumption |
101 apply assumption |
102 apply (rule_tac x="lookup \<theta> X" in exI) |
102 apply (rule_tac x="lookup \<theta> X" in exI) |
103 apply clarify |
103 apply clarify |
104 apply (rule the1_equality) |
104 apply (rule the1_equality) |
105 apply blast apply assumption |
105 apply blast apply assumption |
106 apply (rule_tac x="(Fun (Sum_Type.Projl (subst_substs_sum (Inl (\<theta>, T1)))) |
106 apply (rule_tac x="(Fun (Sum_Type.projl (subst_substs_sum (Inl (\<theta>, T1)))) |
107 (Sum_Type.Projl (subst_substs_sum (Inl (\<theta>, T2)))))" in exI) |
107 (Sum_Type.projl (subst_substs_sum (Inl (\<theta>, T2)))))" in exI) |
108 apply clarify |
108 apply clarify |
109 apply (rule the1_equality) |
109 apply (rule the1_equality) |
110 apply blast apply assumption |
110 apply blast apply assumption |
111 apply clarify |
111 apply clarify |
112 apply simp |
112 apply simp |