9 theory Finite_Set = Divides + Power + Inductive + SetInterval: |
9 theory Finite_Set = Divides + Power + Inductive + SetInterval: |
10 |
10 |
11 subsection {* Collection of finite sets *} |
11 subsection {* Collection of finite sets *} |
12 |
12 |
13 consts Finites :: "'a set set" |
13 consts Finites :: "'a set set" |
|
14 syntax |
|
15 finite :: "'a set => bool" |
|
16 translations |
|
17 "finite A" == "A : Finites" |
14 |
18 |
15 inductive Finites |
19 inductive Finites |
16 intros |
20 intros |
17 emptyI [simp, intro!]: "{} : Finites" |
21 emptyI [simp, intro!]: "{} : Finites" |
18 insertI [simp, intro!]: "A : Finites ==> insert a A : Finites" |
22 insertI [simp, intro!]: "A : Finites ==> insert a A : Finites" |
19 |
23 |
20 syntax |
|
21 finite :: "'a set => bool" |
|
22 translations |
|
23 "finite A" == "A : Finites" |
|
24 |
|
25 axclass finite \<subseteq> type |
24 axclass finite \<subseteq> type |
26 finite: "finite UNIV" |
25 finite: "finite UNIV" |
|
26 |
|
27 lemma ex_new_if_finite: -- "does not depend on def of finite at all" |
|
28 "\<lbrakk> ~finite(UNIV::'a set); finite A \<rbrakk> \<Longrightarrow> \<exists>a::'a. a ~: A" |
|
29 by(subgoal_tac "A ~= UNIV", blast, blast) |
27 |
30 |
28 |
31 |
29 lemma finite_induct [case_names empty insert, induct set: Finites]: |
32 lemma finite_induct [case_names empty insert, induct set: Finites]: |
30 "finite F ==> |
33 "finite F ==> |
31 P {} ==> (!!F x. finite F ==> x \<notin> F ==> P F ==> P (insert x F)) ==> P F" |
34 P {} ==> (!!F x. finite F ==> x \<notin> F ==> P F ==> P (insert x F)) ==> P F" |