32 |
32 |
33 typ "'a fset" |
33 typ "'a fset" |
34 thm "Rep_fset" |
34 thm "Rep_fset" |
35 thm "ABS_fset_def" |
35 thm "ABS_fset_def" |
36 |
36 |
37 ML {* @{term "Abs_fset"} *} |
37 quotient_def (for "'a fset") |
38 local_setup {* |
38 EMPTY :: "'a fset" |
39 old_make_const_def @{binding EMPTY} @{term "[]"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
39 where |
40 *} |
40 "EMPTY \<equiv> ([]::'a list)" |
41 |
41 |
42 term Nil |
42 term Nil |
43 term EMPTY |
43 term EMPTY |
44 thm EMPTY_def |
44 thm EMPTY_def |
45 |
45 |
46 |
46 quotient_def (for "'a fset") |
47 local_setup {* |
47 INSERT :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fet" |
48 old_make_const_def @{binding INSERT} @{term "op #"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
48 where |
49 *} |
49 "INSERT \<equiv> op #" |
50 |
50 |
51 term Cons |
51 term Cons |
52 term INSERT |
52 term INSERT |
53 thm INSERT_def |
53 thm INSERT_def |
54 |
54 |
55 local_setup {* |
55 quotient_def (for "'a fset") |
56 old_make_const_def @{binding UNION} @{term "op @"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
56 FUNION :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
57 *} |
57 where |
|
58 "FUNION \<equiv> (op @)" |
58 |
59 |
59 term append |
60 term append |
60 term UNION |
61 term FUNION |
61 thm UNION_def |
62 thm FUNION_def |
62 |
63 |
63 thm QUOTIENT_fset |
64 thm QUOTIENT_fset |
64 |
65 |
65 thm QUOT_TYPE_I_fset.thm11 |
66 thm QUOT_TYPE_I_fset.thm11 |
66 |
67 |
75 card1 :: "'a list \<Rightarrow> nat" |
76 card1 :: "'a list \<Rightarrow> nat" |
76 where |
77 where |
77 card1_nil: "(card1 []) = 0" |
78 card1_nil: "(card1 []) = 0" |
78 | card1_cons: "(card1 (x # xs)) = (if (x memb xs) then (card1 xs) else (Suc (card1 xs)))" |
79 | card1_cons: "(card1 (x # xs)) = (if (x memb xs) then (card1 xs) else (Suc (card1 xs)))" |
79 |
80 |
80 local_setup {* |
81 quotient_def (for "'a fset") |
81 old_make_const_def @{binding card} @{term "card1"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
82 CARD :: "'a fset \<Rightarrow> nat" |
82 *} |
83 where |
|
84 "CARD \<equiv> card1" |
83 |
85 |
84 term card1 |
86 term card1 |
85 term card |
87 term CARD |
86 thm card_def |
88 thm CARD_def |
87 |
89 |
88 (* text {* |
90 (* text {* |
89 Maybe make_const_def should require a theorem that says that the particular lifted function |
91 Maybe make_const_def should require a theorem that says that the particular lifted function |
90 respects the relation. With it such a definition would be impossible: |
92 respects the relation. With it such a definition would be impossible: |
91 make_const_def @{binding CARD} @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
93 make_const_def @{binding CARD} @{term "length"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
140 apply (induct X) |
142 apply (induct X) |
141 apply (simp) |
143 apply (simp) |
142 apply (metis QUOT_TYPE_I_fset.thm11 list_eq_refl mem_cons m1) |
144 apply (metis QUOT_TYPE_I_fset.thm11 list_eq_refl mem_cons m1) |
143 done |
145 done |
144 |
146 |
145 local_setup {* |
147 quotient_def (for "'a fset") |
146 old_make_const_def @{binding IN} @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
148 IN :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" |
147 *} |
149 where |
|
150 "IN \<equiv> membship" |
148 |
151 |
149 term membship |
152 term membship |
150 term IN |
153 term IN |
151 thm IN_def |
154 thm IN_def |
152 |
155 |
|
156 (* FIXME: does not work yet |
|
157 quotient_def (for "'a fset") |
|
158 FOLD :: "('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a fset \<Rightarrow> 'b" |
|
159 where |
|
160 "FOLD \<equiv> fold1" |
|
161 *) |
153 local_setup {* |
162 local_setup {* |
154 old_make_const_def @{binding fold} @{term "fold1::('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
163 old_make_const_def @{binding fold} @{term "fold1::('b \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
155 *} |
164 *} |
156 |
165 |
157 term fold1 |
166 term fold1 |
158 term fold |
167 term fold |
159 thm fold_def |
168 thm fold_def |
160 |
169 |
|
170 (* FIXME: does not work yet for all types*) |
161 quotient_def (for "'a fset") |
171 quotient_def (for "'a fset") |
162 fmap::"('a \<Rightarrow> 'a) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
172 fmap::"('a \<Rightarrow> 'a) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
163 where |
173 where |
164 "fmap \<equiv> (map::('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list)" |
174 "fmap \<equiv> (map::('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list)" |
165 |
175 |
166 term map |
176 term map |
167 term fmap |
177 term fmap |
168 thm fmap_def |
178 thm fmap_def |
169 |
179 |
170 ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def fmap_def fold_def} *} |
180 ML {* val fset_defs = @{thms EMPTY_def IN_def FUNION_def card_def INSERT_def fmap_def fold_def} *} |
171 (* ML {* val consts = map (fst o dest_Const o fst o Logic.dest_equals o concl_of) fset_defs *} *) |
181 (* ML {* val consts = map (fst o dest_Const o fst o Logic.dest_equals o concl_of) fset_defs *} *) |
172 |
182 |
173 ML {* |
183 ML {* |
174 val consts = [@{const_name "Nil"}, @{const_name "Cons"}, |
184 val consts = [@{const_name "Nil"}, @{const_name "Cons"}, |
175 @{const_name "membship"}, @{const_name "card1"}, |
185 @{const_name "membship"}, @{const_name "card1"}, |
176 @{const_name "append"}, @{const_name "fold1"}, |
186 @{const_name "append"}, @{const_name "fold1"}, |
177 @{const_name "map"}]; |
187 @{const_name "map"}]; |
178 *} |
188 *} |
179 |
189 |
|
190 (* FIXME: does not work anymore :o( *) |
180 ML {* val fset_defs_sym = add_lower_defs @{context} fset_defs *} |
191 ML {* val fset_defs_sym = add_lower_defs @{context} fset_defs *} |
181 |
192 |
182 lemma memb_rsp: |
193 lemma memb_rsp: |
183 fixes z |
194 fixes z |
184 assumes a: "list_eq x y" |
195 assumes a: "list_eq x y" |
496 ML {* lift @{thm list_eq.intros(5)} *} |
507 ML {* lift @{thm list_eq.intros(5)} *} |
497 ML {* lift @{thm card1_suc} *} |
508 ML {* lift @{thm card1_suc} *} |
498 ML {* lift @{thm map_append} *} |
509 ML {* lift @{thm map_append} *} |
499 ML {* lift @{thm eq_r[OF append_assoc]} *} |
510 ML {* lift @{thm eq_r[OF append_assoc]} *} |
500 |
511 |
501 thm |
|
502 |
|
503 |
512 |
504 (*notation ( output) "prop" ("#_" [1000] 1000) *) |
513 (*notation ( output) "prop" ("#_" [1000] 1000) *) |
505 notation ( output) "Trueprop" ("#_" [1000] 1000) |
514 notation ( output) "Trueprop" ("#_" [1000] 1000) |
506 |
515 |
507 (* |
516 (* |