equal
deleted
inserted
replaced
26 'a fset = "'a list" / "list_eq" |
26 'a fset = "'a list" / "list_eq" |
27 by (rule equivp_list_eq) |
27 by (rule equivp_list_eq) |
28 |
28 |
29 quotient_definition |
29 quotient_definition |
30 "EMPTY :: 'a fset" |
30 "EMPTY :: 'a fset" |
31 as |
31 is |
32 "[]::'a list" |
32 "[]::'a list" |
33 |
33 |
34 quotient_definition |
34 quotient_definition |
35 "INSERT :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
35 "INSERT :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
36 as |
36 is |
37 "op #" |
37 "op #" |
38 |
38 |
39 quotient_definition |
39 quotient_definition |
40 "FUNION :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
40 "FUNION :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
41 as |
41 is |
42 "op @" |
42 "op @" |
43 |
43 |
44 fun |
44 fun |
45 card1 :: "'a list \<Rightarrow> nat" |
45 card1 :: "'a list \<Rightarrow> nat" |
46 where |
46 where |
47 card1_nil: "(card1 []) = 0" |
47 card1_nil: "(card1 []) = 0" |
48 | card1_cons: "(card1 (x # xs)) = (if (x mem xs) then (card1 xs) else (Suc (card1 xs)))" |
48 | card1_cons: "(card1 (x # xs)) = (if (x mem xs) then (card1 xs) else (Suc (card1 xs)))" |
49 |
49 |
50 quotient_definition |
50 quotient_definition |
51 "CARD :: 'a fset \<Rightarrow> nat" |
51 "CARD :: 'a fset \<Rightarrow> nat" |
52 as |
52 is |
53 "card1" |
53 "card1" |
54 |
54 |
55 quotient_definition |
55 quotient_definition |
56 "fconcat :: ('a fset) fset \<Rightarrow> 'a fset" |
56 "fconcat :: ('a fset) fset \<Rightarrow> 'a fset" |
57 as |
57 is |
58 "concat" |
58 "concat" |
59 |
59 |
60 term concat |
60 term concat |
61 term fconcat |
61 term fconcat |
62 |
62 |
118 apply (metis List.member.simps(1) list_eq.intros(6) list_eq_refl mem_cons) |
118 apply (metis List.member.simps(1) list_eq.intros(6) list_eq_refl mem_cons) |
119 done |
119 done |
120 |
120 |
121 quotient_definition |
121 quotient_definition |
122 "IN :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" |
122 "IN :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" |
123 as |
123 is |
124 "op mem" |
124 "op mem" |
125 |
125 |
126 quotient_definition |
126 quotient_definition |
127 "FOLD :: ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b fset \<Rightarrow> 'a" |
127 "FOLD :: ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b fset \<Rightarrow> 'a" |
128 as |
128 is |
129 "fold1" |
129 "fold1" |
130 |
130 |
131 quotient_definition |
131 quotient_definition |
132 "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" |
132 "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" |
133 as |
133 is |
134 "map" |
134 "map" |
135 |
135 |
136 lemma mem_rsp: |
136 lemma mem_rsp: |
137 fixes z |
137 fixes z |
138 assumes a: "x \<approx> y" |
138 assumes a: "x \<approx> y" |
283 quotient_type 'a fset2 = "'a list" / "list_eq" |
283 quotient_type 'a fset2 = "'a list" / "list_eq" |
284 by (rule equivp_list_eq) |
284 by (rule equivp_list_eq) |
285 |
285 |
286 quotient_definition |
286 quotient_definition |
287 "EMPTY2 :: 'a fset2" |
287 "EMPTY2 :: 'a fset2" |
288 as |
288 is |
289 "[]::'a list" |
289 "[]::'a list" |
290 |
290 |
291 quotient_definition |
291 quotient_definition |
292 "INSERT2 :: 'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2" |
292 "INSERT2 :: 'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2" |
293 as |
293 is |
294 "op #" |
294 "op #" |
295 |
295 |
296 lemma "P (x :: 'a fset2) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l" |
296 lemma "P (x :: 'a fset2) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l" |
297 apply (lifting list_induct_part) |
297 apply (lifting list_induct_part) |
298 done |
298 done |
301 apply (lifting list_induct_part) |
301 apply (lifting list_induct_part) |
302 done |
302 done |
303 |
303 |
304 quotient_definition |
304 quotient_definition |
305 "fset_rec :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
305 "fset_rec :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
306 as |
306 is |
307 "list_rec" |
307 "list_rec" |
308 |
308 |
309 quotient_definition |
309 quotient_definition |
310 "fset_case :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
310 "fset_case :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
311 as |
311 is |
312 "list_case" |
312 "list_case" |
313 |
313 |
314 (* Probably not true without additional assumptions about the function *) |
314 (* Probably not true without additional assumptions about the function *) |
315 lemma list_rec_rsp[quot_respect]: |
315 lemma list_rec_rsp[quot_respect]: |
316 "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec" |
316 "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec" |