equal
deleted
inserted
replaced
14 inductive finite :: "'a set \<Rightarrow> bool" |
14 inductive finite :: "'a set \<Rightarrow> bool" |
15 where |
15 where |
16 emptyI [simp, intro!]: "finite {}" |
16 emptyI [simp, intro!]: "finite {}" |
17 | insertI [simp, intro!]: "finite A \<Longrightarrow> finite (insert a A)" |
17 | insertI [simp, intro!]: "finite A \<Longrightarrow> finite (insert a A)" |
18 |
18 |
19 (* FIXME: move to Set theory *) |
19 simproc_setup finite_Collect ("finite (Collect P)") = {* K Set_Comprehension_Pointfree.simproc *} |
20 ML_file "Tools/set_comprehension_pointfree.ML" |
|
21 |
|
22 simproc_setup finite_Collect ("finite (Collect P)") = |
|
23 {* K Set_Comprehension_Pointfree.simproc *} |
|
24 |
|
25 (* FIXME: move to Set theory*) |
|
26 setup {* |
|
27 Code_Preproc.map_pre (fn ss => ss addsimprocs |
|
28 [Raw_Simplifier.make_simproc {name = "set comprehension", lhss = [@{cpat "Collect ?P"}], |
|
29 proc = K Set_Comprehension_Pointfree.code_simproc, identifier = []}]) |
|
30 *} |
|
31 |
20 |
32 lemma finite_induct [case_names empty insert, induct set: finite]: |
21 lemma finite_induct [case_names empty insert, induct set: finite]: |
33 -- {* Discharging @{text "x \<notin> F"} entails extra work. *} |
22 -- {* Discharging @{text "x \<notin> F"} entails extra work. *} |
34 assumes "finite F" |
23 assumes "finite F" |
35 assumes "P {}" |
24 assumes "P {}" |