equal
deleted
inserted
replaced
20 sorry |
20 sorry |
21 |
21 |
22 quotient fset = "'a list" / "list_eq" |
22 quotient fset = "'a list" / "list_eq" |
23 by (rule list_eq_equivp) |
23 by (rule list_eq_equivp) |
24 |
24 |
25 lemma not_nil_equiv_cons: "[] \<noteq> a # A" sorry |
25 lemma not_nil_equiv_cons: "\<not>[] \<approx> a # A" sorry |
26 |
26 |
27 (* The 2 lemmas below are different from the ones in QuotList *) |
27 (* The 2 lemmas below are different from the ones in QuotList *) |
28 lemma nil_rsp[quot_respect]: |
28 lemma nil_rsp[quot_respect]: |
29 shows "[] \<approx> []" |
29 shows "[] \<approx> []" |
30 by (rule list_eq_reflp) |
30 by (rule list_eq_reflp) |
274 (* We also have map and some properties of it in FSet *) |
274 (* We also have map and some properties of it in FSet *) |
275 (* and the following which still lifts ok *) |
275 (* and the following which still lifts ok *) |
276 lemma "funion (funion x xa) xb = funion x (funion xa xb)" |
276 lemma "funion (funion x xa) xb = funion x (funion xa xb)" |
277 by (lifting append_assoc) |
277 by (lifting append_assoc) |
278 |
278 |
|
279 quotient_def |
|
280 "fset_case :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
|
281 as |
|
282 "list_case" |
|
283 |
|
284 (* NOT SURE IF TRUE *) |
|
285 lemma list_case_rsp[quot_respect]: |
|
286 "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case" |
|
287 apply (auto) |
|
288 sorry |
|
289 |
|
290 lemma "fset_case (f1::'t) f2 (Insert a xa) = f2 a xa" |
|
291 apply (lifting list.cases(2)) |
|
292 done |
|
293 |
|
294 |
279 end |
295 end |