equal
deleted
inserted
replaced
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 ML {* @{term "Abs_fset"} *} |
38 local_setup {* |
38 local_setup {* |
39 make_const_def @{binding EMPTY} @{term "[]"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
39 old_make_const_def @{binding EMPTY} @{term "[]"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
40 *} |
40 *} |
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 |
47 local_setup {* |
47 local_setup {* |
48 make_const_def @{binding INSERT} @{term "op #"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
48 old_make_const_def @{binding INSERT} @{term "op #"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
49 *} |
49 *} |
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 local_setup {* |
56 make_const_def @{binding UNION} @{term "op @"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
56 old_make_const_def @{binding UNION} @{term "op @"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
57 *} |
57 *} |
58 |
58 |
59 term append |
59 term append |
60 term UNION |
60 term UNION |
61 thm UNION_def |
61 thm UNION_def |
76 where |
76 where |
77 card1_nil: "(card1 []) = 0" |
77 card1_nil: "(card1 []) = 0" |
78 | card1_cons: "(card1 (x # xs)) = (if (x memb xs) then (card1 xs) else (Suc (card1 xs)))" |
78 | card1_cons: "(card1 (x # xs)) = (if (x memb xs) then (card1 xs) else (Suc (card1 xs)))" |
79 |
79 |
80 local_setup {* |
80 local_setup {* |
81 make_const_def @{binding card} @{term "card1"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
81 old_make_const_def @{binding card} @{term "card1"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
82 *} |
82 *} |
83 |
83 |
84 term card1 |
84 term card1 |
85 term card |
85 term card |
86 thm card_def |
86 thm card_def |
141 apply (simp) |
141 apply (simp) |
142 apply (metis QUOT_TYPE_I_fset.thm11 list_eq_refl mem_cons m1) |
142 apply (metis QUOT_TYPE_I_fset.thm11 list_eq_refl mem_cons m1) |
143 done |
143 done |
144 |
144 |
145 local_setup {* |
145 local_setup {* |
146 make_const_def @{binding IN} @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
146 old_make_const_def @{binding IN} @{term "membship"} NoSyn @{typ "'a list"} @{typ "'a fset"} #> snd |
147 *} |
147 *} |
148 |
148 |
149 term membship |
149 term membship |
150 term IN |
150 term IN |
151 thm IN_def |
151 thm IN_def |
152 |
152 |
153 local_setup {* |
153 local_setup {* |
154 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 |
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 |
155 *} |
155 *} |
156 |
156 |
157 term fold1 |
157 term fold1 |
158 term fold |
158 term fold |
159 thm fold_def |
159 thm fold_def |
160 |
160 |
161 local_setup {* |
161 local_setup {* |
162 make_const_def @{binding fmap} @{term "map::('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list"} NoSyn |
162 old_make_const_def @{binding fmap} @{term "map::('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list"} NoSyn |
163 @{typ "'a list"} @{typ "'a fset"} #> snd |
163 @{typ "'a list"} @{typ "'a fset"} #> snd |
164 *} |
164 *} |
165 |
165 |
166 term map |
166 term map |
167 term fmap |
167 term fmap |