equal
deleted
inserted
replaced
25 quotient fset = "'a list" / "list_eq" |
25 quotient fset = "'a list" / "list_eq" |
26 apply(rule equivp_list_eq) |
26 apply(rule equivp_list_eq) |
27 done |
27 done |
28 |
28 |
29 quotient_def |
29 quotient_def |
30 EMPTY :: "EMPTY :: 'a fset" |
30 "EMPTY :: 'a fset" |
31 where |
31 as |
32 "[]::'a list" |
32 "[]::'a list" |
33 |
33 |
34 quotient_def |
34 quotient_def |
35 INSERT :: "INSERT :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
35 "INSERT :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
36 where |
36 as |
37 "op #" |
37 "op #" |
38 |
38 |
39 quotient_def |
39 quotient_def |
40 FUNION :: "FUNION :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
40 "FUNION :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
41 where |
41 as |
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_def |
50 quotient_def |
51 CARD :: "CARD :: 'a fset \<Rightarrow> nat" |
51 "CARD :: 'a fset \<Rightarrow> nat" |
52 where |
52 as |
53 "card1" |
53 "card1" |
54 |
54 |
55 (* text {* |
55 (* text {* |
56 Maybe make_const_def should require a theorem that says that the particular lifted function |
56 Maybe make_const_def should require a theorem that says that the particular lifted function |
57 respects the relation. With it such a definition would be impossible: |
57 respects the relation. With it such a definition would be impossible: |
109 apply (simp) |
109 apply (simp) |
110 apply (metis List.member.simps(1) list_eq.intros(6) list_eq_refl mem_cons) |
110 apply (metis List.member.simps(1) list_eq.intros(6) list_eq_refl mem_cons) |
111 done |
111 done |
112 |
112 |
113 quotient_def |
113 quotient_def |
114 IN :: "IN :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" |
114 "IN :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" |
115 where |
115 as |
116 "op mem" |
116 "op mem" |
117 |
117 |
118 quotient_def |
118 quotient_def |
119 FOLD :: "FOLD :: ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b fset \<Rightarrow> 'a" |
119 "FOLD :: ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b fset \<Rightarrow> 'a" |
120 where |
120 as |
121 "fold1" |
121 "fold1" |
122 |
122 |
123 quotient_def |
123 quotient_def |
124 fmap::"fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" |
124 "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" |
125 where |
125 as |
126 "map" |
126 "map" |
127 |
127 |
128 lemma mem_rsp: |
128 lemma mem_rsp: |
129 fixes z |
129 fixes z |
130 assumes a: "x \<approx> y" |
130 assumes a: "x \<approx> y" |
273 |
273 |
274 quotient fset2 = "'a list" / "list_eq" |
274 quotient fset2 = "'a list" / "list_eq" |
275 by (rule equivp_list_eq) |
275 by (rule equivp_list_eq) |
276 |
276 |
277 quotient_def |
277 quotient_def |
278 EMPTY2 :: "EMPTY2 :: 'a fset2" |
278 "EMPTY2 :: 'a fset2" |
279 where |
279 as |
280 "[]::'a list" |
280 "[]::'a list" |
281 |
281 |
282 quotient_def |
282 quotient_def |
283 INSERT2 :: "INSERT2 :: 'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2" |
283 "INSERT2 :: 'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2" |
284 where |
284 as |
285 "op #" |
285 "op #" |
286 |
286 |
287 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" |
287 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" |
288 apply (lifting list_induct_part) |
288 apply (lifting list_induct_part) |
289 done |
289 done |
291 lemma "P (x :: 'a fset) (EMPTY2 :: 'c fset2) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT2 e t)) \<Longrightarrow> P x l" |
291 lemma "P (x :: 'a fset) (EMPTY2 :: 'c fset2) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT2 e t)) \<Longrightarrow> P x l" |
292 apply (lifting list_induct_part) |
292 apply (lifting list_induct_part) |
293 done |
293 done |
294 |
294 |
295 quotient_def |
295 quotient_def |
296 fset_rec::"fset_rec :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
296 "fset_rec :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
297 where |
297 as |
298 "list_rec" |
298 "list_rec" |
299 |
299 |
300 quotient_def |
300 quotient_def |
301 fset_case::"fset_case :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
301 "fset_case :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
302 where |
302 as |
303 "list_case" |
303 "list_case" |
304 |
304 |
305 (* Probably not true without additional assumptions about the function *) |
305 (* Probably not true without additional assumptions about the function *) |
306 lemma list_rec_rsp[quot_respect]: |
306 lemma list_rec_rsp[quot_respect]: |
307 "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec" |
307 "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec" |