equal
deleted
inserted
replaced
120 apply(induct xs) |
120 apply(induct xs) |
121 apply (metis Suc_neq_Zero card1_0) |
121 apply (metis Suc_neq_Zero card1_0) |
122 apply (metis QUOT_TYPE_I_fset.R_trans card1_cons list_eq_refl mem_cons) |
122 apply (metis QUOT_TYPE_I_fset.R_trans card1_cons list_eq_refl mem_cons) |
123 done |
123 done |
124 |
124 |
|
125 definition |
|
126 rsp_fold |
|
127 where |
|
128 "rsp_fold f = ((!u v. (f u v = f v u)) \<and> (!u v w. ((f u (f v w) = f (f u v) w))))" |
|
129 |
125 primrec |
130 primrec |
126 fold1 |
131 fold1 |
127 where |
132 where |
128 "fold1 f (g :: 'a \<Rightarrow> 'b) (z :: 'b) [] = z" |
133 "fold1 f (g :: 'a \<Rightarrow> 'b) (z :: 'b) [] = z" |
129 | "fold1 f g z (a # A) = |
134 | "fold1 f g z (a # A) = |
130 (if ((!u v. (f u v = f v u)) |
135 (if rsp_fold f |
131 \<and> (!u v w. ((f u (f v w) = f (f u v) w)))) |
|
132 then ( |
136 then ( |
133 if (a memb A) then (fold1 f g z A) else (f (g a) (fold1 f g z A)) |
137 if (a memb A) then (fold1 f g z A) else (f (g a) (fold1 f g z A)) |
134 ) else z)" |
138 ) else z)" |
135 |
139 |
136 (* fold1_def is not usable, but: *) |
140 (* fold1_def is not usable, but: *) |
269 apply (induct) |
273 apply (induct) |
270 apply(auto intro: list_eq.intros) |
274 apply(auto intro: list_eq.intros) |
271 done |
275 done |
272 |
276 |
273 lemma ho_map_rsp: |
277 lemma ho_map_rsp: |
274 "((op = ===> op =) ===> op \<approx> ===> op \<approx>) map map" |
278 "(op = ===> op \<approx> ===> op \<approx>) map map" |
275 by (simp add: FUN_REL_EQ map_rsp) |
279 by (simp add: map_rsp) |
276 |
280 |
277 lemma map_append : |
281 lemma map_append: |
278 "(map f (a @ b)) \<approx> |
282 "(map f (a @ b)) \<approx> |
279 (map f a) @ (map f b)" |
283 (map f a) @ (map f b)" |
280 by simp (rule list_eq_refl) |
284 by simp (rule list_eq_refl) |
281 |
285 |
282 lemma ho_fold_rsp: |
286 lemma ho_fold_rsp: |
283 "((op = ===> op = ===> op =) ===> (op = ===> op =) ===> op = ===> op \<approx> ===> op =) fold1 fold1" |
287 "(op = ===> op = ===> op = ===> op \<approx> ===> op =) fold1 fold1" |
284 apply (auto simp add: FUN_REL_EQ) |
288 apply (auto simp add: FUN_REL_EQ) |
285 sorry |
289 apply (case_tac "rsp_fold x") |
|
290 prefer 2 |
|
291 apply (erule_tac list_eq.induct) |
|
292 apply (simp_all) |
|
293 apply (erule_tac list_eq.induct) |
|
294 apply (simp_all) |
|
295 apply (auto simp add: memb_rsp rsp_fold_def) |
|
296 done |
286 |
297 |
287 print_quotients |
298 print_quotients |
288 |
299 |
289 |
300 |
290 ML {* val qty = @{typ "'a fset"} *} |
301 ML {* val qty = @{typ "'a fset"} *} |