24 |
24 |
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 :: "'a fset" |
30 EMPTY :: "EMPTY :: 'a fset" |
31 where |
31 where |
32 "EMPTY \<equiv> ([]::'a list)" |
32 "[]::'a list" |
33 |
33 |
34 quotient_def |
34 quotient_def |
35 INSERT :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
35 INSERT :: "INSERT :: 'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
36 where |
36 where |
37 "INSERT \<equiv> op #" |
37 "op #" |
38 |
38 |
39 quotient_def |
39 quotient_def |
40 FUNION :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
40 FUNION :: "FUNION :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
41 where |
41 where |
42 "FUNION \<equiv> (op @)" |
42 "op @" |
43 |
43 |
44 fun |
44 fun |
45 membship :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infix "memb" 100) |
45 membship :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infix "memb" 100) |
46 where |
46 where |
47 m1: "(x memb []) = False" |
47 m1: "(x memb []) = False" |
51 card1 :: "'a list \<Rightarrow> nat" |
51 card1 :: "'a list \<Rightarrow> nat" |
52 where |
52 where |
53 card1_nil: "(card1 []) = 0" |
53 card1_nil: "(card1 []) = 0" |
54 | card1_cons: "(card1 (x # xs)) = (if (x memb xs) then (card1 xs) else (Suc (card1 xs)))" |
54 | card1_cons: "(card1 (x # xs)) = (if (x memb xs) then (card1 xs) else (Suc (card1 xs)))" |
55 |
55 |
56 quotient_def |
56 quotient_def |
57 CARD :: "'a fset \<Rightarrow> nat" |
57 CARD :: "CARD :: 'a fset \<Rightarrow> nat" |
58 where |
58 where |
59 "CARD \<equiv> card1" |
59 "card1" |
60 |
60 |
61 (* text {* |
61 (* text {* |
62 Maybe make_const_def should require a theorem that says that the particular lifted function |
62 Maybe make_const_def should require a theorem that says that the particular lifted function |
63 respects the relation. With it such a definition would be impossible: |
63 respects the relation. With it such a definition would be impossible: |
64 make_const_def @{binding CARD} @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
64 make_const_def @{binding CARD} @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
115 apply (simp) |
115 apply (simp) |
116 apply (metis QUOT_TYPE_I_fset.thm11 list_eq_refl mem_cons m1) |
116 apply (metis QUOT_TYPE_I_fset.thm11 list_eq_refl mem_cons m1) |
117 done |
117 done |
118 |
118 |
119 quotient_def |
119 quotient_def |
120 IN :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" |
120 IN :: "IN :: 'a \<Rightarrow> 'a fset \<Rightarrow> bool" |
121 where |
121 where |
122 "IN \<equiv> membship" |
122 "membship" |
123 |
123 |
124 quotient_def |
124 quotient_def |
125 FOLD :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b fset \<Rightarrow> 'a" |
125 FOLD :: "FOLD :: ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b fset \<Rightarrow> 'a" |
126 where |
126 where |
127 "FOLD \<equiv> fold1" |
127 "fold1" |
128 |
128 |
129 quotient_def |
129 quotient_def |
130 fmap::"('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" |
130 fmap::"fmap :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" |
131 where |
131 where |
132 "fmap \<equiv> map" |
132 "map" |
133 |
133 |
134 lemma memb_rsp: |
134 lemma memb_rsp: |
135 fixes z |
135 fixes z |
136 assumes a: "x \<approx> y" |
136 assumes a: "x \<approx> y" |
137 shows "(z memb x) = (z memb y)" |
137 shows "(z memb x) = (z memb y)" |
316 |
316 |
317 quotient fset2 = "'a list" / "list_eq" |
317 quotient fset2 = "'a list" / "list_eq" |
318 by (rule equivp_list_eq) |
318 by (rule equivp_list_eq) |
319 |
319 |
320 quotient_def |
320 quotient_def |
321 EMPTY2 :: "'a fset2" |
321 EMPTY2 :: "EMPTY2 :: 'a fset2" |
322 where |
322 where |
323 "EMPTY2 \<equiv> ([]::'a list)" |
323 "[]::'a list" |
324 |
324 |
325 quotient_def |
325 quotient_def |
326 INSERT2 :: "'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2" |
326 INSERT2 :: "INSERT2 :: 'a \<Rightarrow> 'a fset2 \<Rightarrow> 'a fset2" |
327 where |
327 where |
328 "INSERT2 \<equiv> op #" |
328 "op #" |
329 |
329 |
330 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" |
330 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" |
331 apply (lifting list_induct_part) |
331 apply (lifting list_induct_part) |
332 done |
332 done |
333 |
333 |
334 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" |
334 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" |
335 apply (lifting list_induct_part) |
335 apply (lifting list_induct_part) |
336 done |
336 done |
337 |
337 |
338 quotient_def |
338 quotient_def |
339 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
339 fset_rec::"fset_rec :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
340 where |
340 where |
341 "fset_rec \<equiv> list_rec" |
341 "list_rec" |
342 |
342 |
343 quotient_def |
343 quotient_def |
344 fset_case::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
344 fset_case::"fset_case :: 'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
345 where |
345 where |
346 "fset_case \<equiv> list_case" |
346 "list_case" |
347 |
347 |
348 (* Probably not true without additional assumptions about the function *) |
348 (* Probably not true without additional assumptions about the function *) |
349 lemma list_rec_rsp[quot_respect]: |
349 lemma list_rec_rsp[quot_respect]: |
350 "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec" |
350 "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec" |
351 apply (auto) |
351 apply (auto) |