41 apply(induct Ts T rule: lookup.induct) |
41 apply(induct Ts T rule: lookup.induct) |
42 apply(simp_all) |
42 apply(simp_all) |
43 done |
43 done |
44 |
44 |
45 lemma test: |
45 lemma test: |
46 assumes a: "f x = Inl y" |
46 assumes a: "\<exists>y. f x = Inl y" |
47 shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl ((p \<bullet> f) (p \<bullet> x))" |
47 shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl ((p \<bullet> f) (p \<bullet> x))" |
48 using a |
48 using a |
|
49 apply clarify |
49 apply(frule_tac p="p" in permute_boolI) |
50 apply(frule_tac p="p" in permute_boolI) |
50 apply(simp (no_asm_use) only: eqvts) |
51 apply(simp (no_asm_use) only: eqvts) |
51 apply(subst (asm) permute_fun_app_eq) |
52 apply(subst (asm) permute_fun_app_eq) |
52 back |
53 back |
53 apply(simp) |
54 apply(simp) |
54 done |
55 done |
55 |
56 |
56 lemma test2: |
57 lemma test2: |
57 assumes a: "f x = Inl y" |
58 assumes a: "\<exists>y. f x = Inl y" |
58 shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl (p \<bullet> (f x))" |
59 shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl (p \<bullet> (f x))" |
59 using a |
60 using a |
|
61 apply clarify |
60 apply(frule_tac p="p" in permute_boolI) |
62 apply(frule_tac p="p" in permute_boolI) |
61 apply(simp (no_asm_use) only: eqvts) |
63 apply(simp (no_asm_use) only: eqvts) |
62 apply(subst (asm) permute_fun_app_eq) |
64 apply(subst (asm) permute_fun_app_eq) |
63 back |
65 back |
64 apply(simp) |
66 apply(simp) |
65 done |
67 done |
66 |
|
67 lemma helper: |
|
68 assumes "A - C = A - D" |
|
69 and "B - C = B - D" |
|
70 and "E \<subseteq> A \<union> B" |
|
71 shows "E - C = E - D" |
|
72 using assms |
|
73 by blast |
|
74 |
|
75 --"The following is accepted by 'function' but not by 'nominal_primrec'" |
|
76 |
68 |
77 nominal_primrec (default "sum_case (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)") |
69 nominal_primrec (default "sum_case (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)") |
78 subst :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty" |
70 subst :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty" |
79 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" |
71 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" |
80 where |
72 where |
81 "subst \<theta> (Var X) = lookup \<theta> X" |
73 "subst \<theta> (Var X) = lookup \<theta> X" |
82 | "subst \<theta> (Fun T1 T2) = Fun (subst \<theta> T1) (subst \<theta> T2)" |
74 | "subst \<theta> (Fun T1 T2) = Fun (subst \<theta> T1) (subst \<theta> T2)" |
83 | "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs T) = All xs (subst \<theta> T)" |
75 | "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs T) = All xs (subst \<theta> T)" |
84 thm subst_substs_graph_def |
76 (*unfolding subst_substs_graph_def eqvt_def |
85 thm subst_substs_sumC_def |
77 apply rule |
86 oops |
78 apply perm_simp |
87 |
79 apply (subst test3) |
88 |
80 defer |
89 nominal_primrec (default "\<lambda>(x :: (name \<times> ty) list \<times> ty + (name \<times> ty) list \<times> tys). MYUNDEFINED :: ty + tys") |
81 apply (subst test3) |
90 subst :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty" |
82 defer |
91 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" |
83 apply (subst test3) |
92 where |
84 defer |
93 "subst \<theta> (Var X) = lookup \<theta> X" |
85 apply rule*) |
94 | "subst \<theta> (Fun T1 T2) = Fun (subst \<theta> T1) (subst \<theta> T2)" |
|
95 | "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs T) = All xs (subst \<theta> T)" |
|
96 thm subst_substs_graph_def |
|
97 thm subst_substs_sumC_def |
|
98 oops |
|
99 |
|
100 nominal_primrec |
|
101 subst :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty" |
|
102 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" |
|
103 where |
|
104 "subst \<theta> (Var X) = lookup \<theta> X" |
|
105 | "subst \<theta> (Fun T1 T2) = Fun (subst \<theta> T1) (subst \<theta> T2)" |
|
106 | "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs T) = All xs (subst \<theta> T)" |
|
107 thm subst_substs_graph_def |
|
108 thm subst_substs_sumC_def |
|
109 apply(subgoal_tac "\<And>p x r. subst_substs_graph x r \<Longrightarrow> subst_substs_graph (p \<bullet> x) (p \<bullet> r)") |
86 apply(subgoal_tac "\<And>p x r. subst_substs_graph x r \<Longrightarrow> subst_substs_graph (p \<bullet> x) (p \<bullet> r)") |
110 apply(simp add: eqvt_def) |
87 apply(simp add: eqvt_def) |
111 apply(rule allI) |
88 apply(rule allI) |
112 apply(simp add: permute_fun_def permute_bool_def) |
89 apply(simp add: permute_fun_def permute_bool_def) |
113 apply(rule ext) |
90 apply(rule ext) |
127 apply(rule subst_substs_graph.intros) |
104 apply(rule subst_substs_graph.intros) |
128 apply(erule subst_substs_graph.cases) |
105 apply(erule subst_substs_graph.cases) |
129 apply(simp (no_asm_use) only: eqvts) |
106 apply(simp (no_asm_use) only: eqvts) |
130 apply(subst test) |
107 apply(subst test) |
131 back |
108 back |
|
109 apply (rule exI) |
132 apply(assumption) |
110 apply(assumption) |
133 apply(rotate_tac 1) |
111 apply(rotate_tac 1) |
134 apply(erule subst_substs_graph.cases) |
112 apply(erule subst_substs_graph.cases) |
135 apply(subst test) |
113 apply(subst test) |
136 back |
114 back |
137 apply(assumption) |
115 apply (rule exI) |
138 apply(perm_simp) |
116 apply(assumption) |
139 apply(rule subst_substs_graph.intros) |
117 apply(perm_simp) |
140 apply(assumption) |
118 apply(rule subst_substs_graph.intros) |
141 apply(assumption) |
119 apply(assumption) |
142 apply(subst test) |
120 apply(assumption) |
143 back |
121 apply(subst test) |
|
122 back |
|
123 apply (rule exI) |
144 apply(assumption) |
124 apply(assumption) |
145 apply(perm_simp) |
125 apply(perm_simp) |
146 apply(rule subst_substs_graph.intros) |
126 apply(rule subst_substs_graph.intros) |
147 apply(assumption) |
127 apply(assumption) |
148 apply(assumption) |
128 apply(assumption) |
149 apply(simp) |
129 apply(simp) |
150 --"A" |
130 --"A" |
151 apply(simp (no_asm_use) only: eqvts) |
131 apply(simp (no_asm_use) only: eqvts) |
152 apply(subst test) |
132 apply(subst test) |
153 back |
133 back |
|
134 apply (rule exI) |
154 apply(assumption) |
135 apply(assumption) |
155 apply(rotate_tac 1) |
136 apply(rotate_tac 1) |
156 apply(erule subst_substs_graph.cases) |
137 apply(erule subst_substs_graph.cases) |
157 apply(subst test) |
138 apply(subst test) |
158 back |
139 back |
159 apply(assumption) |
140 apply (rule exI) |
160 apply(perm_simp) |
141 apply(assumption) |
161 apply(rule subst_substs_graph.intros) |
142 apply(perm_simp) |
162 apply(assumption) |
143 apply(rule subst_substs_graph.intros) |
163 apply(assumption) |
144 apply(assumption) |
164 apply(subst test) |
145 apply(assumption) |
165 back |
146 apply(subst test) |
|
147 back |
|
148 apply (rule exI) |
166 apply(assumption) |
149 apply(assumption) |
167 apply(perm_simp) |
150 apply(perm_simp) |
168 apply(rule subst_substs_graph.intros) |
151 apply(rule subst_substs_graph.intros) |
169 apply(assumption) |
152 apply(assumption) |
170 apply(assumption) |
153 apply(assumption) |
213 apply (subgoal_tac "eqvt_at (\<lambda>(l, r). subst l r) (\<theta>', T)") |
198 apply (subgoal_tac "eqvt_at (\<lambda>(l, r). subst l r) (\<theta>', T)") |
214 apply (thin_tac "eqvt_at subst_substs_sumC (Inl (\<theta>', T))") |
199 apply (thin_tac "eqvt_at subst_substs_sumC (Inl (\<theta>', T))") |
215 prefer 2 |
200 prefer 2 |
216 apply (simp add: eqvt_at_def subst_def) |
201 apply (simp add: eqvt_at_def subst_def) |
217 apply rule |
202 apply rule |
218 apply (subgoal_tac "\<And>x. subst_substs_sumC (Inl (x)) = Inl (?y x)") |
|
219 apply (subst test2) |
203 apply (subst test2) |
220 apply (drule_tac x="(\<theta>', T)" in meta_spec) |
204 apply (simp add: subst_substs_sumC_def) |
221 apply assumption |
|
222 apply simp |
|
223 --"We require that for Inl it returns Inl. It doesn't work for undefined, but it does work for the following" |
|
224 apply (subgoal_tac "\<And>y. \<exists>z. (\<lambda>x. THE_default (sum_case (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined) x) (subst_substs_graph x)) (Inl y) = (Inl z)") |
|
225 prefer 2 |
|
226 apply (simp add: THE_default_def) |
205 apply (simp add: THE_default_def) |
227 apply (case_tac "Ex1 (subst_substs_graph (Inl y))") |
206 apply (case_tac "Ex1 (subst_substs_graph (Inl (\<theta>', T)))") |
228 prefer 2 |
207 prefer 2 |
229 apply simp |
208 apply simp |
230 apply (simp add: the1_equality) |
209 apply (simp add: the1_equality) |
231 apply auto[1] |
210 apply auto[1] |
232 apply (erule_tac x="x" in allE) |
211 apply (erule_tac x="x" in allE) |
241 (Sum_Type.Projl (subst_substs_sum (Inl (\<theta>, T2)))))" in exI) |
220 (Sum_Type.Projl (subst_substs_sum (Inl (\<theta>, T2)))))" in exI) |
242 apply clarify |
221 apply clarify |
243 apply (rule the1_equality) |
222 apply (rule the1_equality) |
244 apply metis apply assumption |
223 apply metis apply assumption |
245 apply clarify |
224 apply clarify |
246 --"This is exactly the assumption for the properly defined function" |
225 apply simp |
247 defer |
226 --"-" |
248 apply clarify |
227 apply clarify |
249 apply (frule supp_eqvt_at) |
228 apply (frule supp_eqvt_at) |
250 apply (simp add: finite_supp) |
229 apply (simp add: finite_supp) |
251 apply (erule Abs_res_fcb) |
230 apply (erule Abs_res_fcb) |
252 apply (simp add: Abs_fresh_iff) |
231 apply (simp add: Abs_fresh_iff) |