equal
deleted
inserted
replaced
5 |
5 |
6 header {* Finite sets *} |
6 header {* Finite sets *} |
7 |
7 |
8 theory Finite_Set |
8 theory Finite_Set |
9 imports Option Power |
9 imports Option Power |
10 uses ("Tools/set_comprehension_pointfree.ML") |
|
11 begin |
10 begin |
12 |
11 |
13 subsection {* Predicate for finite sets *} |
12 subsection {* Predicate for finite sets *} |
14 |
13 |
15 inductive finite :: "'a set \<Rightarrow> bool" |
14 inductive finite :: "'a set \<Rightarrow> bool" |
16 where |
15 where |
17 emptyI [simp, intro!]: "finite {}" |
16 emptyI [simp, intro!]: "finite {}" |
18 | insertI [simp, intro!]: "finite A \<Longrightarrow> finite (insert a A)" |
17 | insertI [simp, intro!]: "finite A \<Longrightarrow> finite (insert a A)" |
19 |
18 |
20 (* FIXME: move to Set theory *) |
19 (* FIXME: move to Set theory *) |
21 use "Tools/set_comprehension_pointfree.ML" |
20 ML_file "Tools/set_comprehension_pointfree.ML" |
22 |
21 |
23 simproc_setup finite_Collect ("finite (Collect P)") = |
22 simproc_setup finite_Collect ("finite (Collect P)") = |
24 {* K Set_Comprehension_Pointfree.simproc *} |
23 {* K Set_Comprehension_Pointfree.simproc *} |
25 |
24 |
26 (* FIXME: move to Set theory*) |
25 (* FIXME: move to Set theory*) |