equal
deleted
inserted
replaced
24 |
24 |
25 quotient_type |
25 quotient_type |
26 fset = "'a list" / "list_eq" |
26 fset = "'a list" / "list_eq" |
27 by (rule equivp_list_eq) |
27 by (rule equivp_list_eq) |
28 |
28 |
29 quotient_def |
29 quotient_definition |
30 "EMPTY :: 'a fset" |
30 "EMPTY :: 'a fset" |
31 as |
31 as |
32 "[]::'a list" |
32 "[]::'a list" |
33 |
33 |
34 quotient_def |
34 quotient_definition |
35 "INSERT :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
35 "INSERT :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
36 as |
36 as |
37 "op #" |
37 "op #" |
38 |
38 |
39 quotient_def |
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 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_definition |
51 "CARD :: 'a fset \<Rightarrow> nat" |
51 "CARD :: 'a fset \<Rightarrow> nat" |
52 as |
52 as |
53 "card1" |
53 "card1" |
54 |
54 |
55 (* text {* |
55 (* text {* |
108 apply (induct X) |
108 apply (induct X) |
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_definition |
114 "IN :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" |
114 "IN :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" |
115 as |
115 as |
116 "op mem" |
116 "op mem" |
117 |
117 |
118 quotient_def |
118 quotient_definition |
119 "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 as |
120 as |
121 "fold1" |
121 "fold1" |
122 |
122 |
123 quotient_def |
123 quotient_definition |
124 "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" |
124 "fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" |
125 as |
125 as |
126 "map" |
126 "map" |
127 |
127 |
128 lemma mem_rsp: |
128 lemma mem_rsp: |
272 done |
272 done |
273 |
273 |
274 quotient_type fset2 = "'a list" / "list_eq" |
274 quotient_type fset2 = "'a list" / "list_eq" |
275 by (rule equivp_list_eq) |
275 by (rule equivp_list_eq) |
276 |
276 |
277 quotient_def |
277 quotient_definition |
278 "EMPTY2 :: 'a fset2" |
278 "EMPTY2 :: 'a fset2" |
279 as |
279 as |
280 "[]::'a list" |
280 "[]::'a list" |
281 |
281 |
282 quotient_def |
282 quotient_definition |
283 "INSERT2 :: 'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2" |
283 "INSERT2 :: 'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2" |
284 as |
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" |
290 |
290 |
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_definition |
296 "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 as |
297 as |
298 "list_rec" |
298 "list_rec" |
299 |
299 |
300 quotient_def |
300 quotient_definition |
301 "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 as |
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 *) |