author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 46953  2b6e55924af3 
child 58871  c399ae4b836f 
permissions  rwrr 
1478  1 
(* Title: ZF/Finite.thy 
2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

516  3 
Copyright 1994 University of Cambridge 
4 

46953  5 
prove: b \<in> Fin(A) ==> inj(b,b) \<subseteq> surj(b,b) 
516  6 
*) 
7 

13328  8 
header{*Finite Powerset Operator and Finite Function Space*} 
9 

26056
6a0801279f4c
Made theory names in ZF disjoint from HOL theory names to allow loading both developments
krauss
parents:
24893
diff
changeset

10 
theory Finite imports Inductive_ZF Epsilon Nat_ZF begin 
9491
1a36151ee2fc
natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents:
6053
diff
changeset

11 

1a36151ee2fc
natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents:
6053
diff
changeset

12 
(*The natural numbers as a datatype*) 
13194  13 
rep_datatype 
14 
elimination natE 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26056
diff
changeset

15 
induction nat_induct 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
26056
diff
changeset

16 
case_eqns nat_case_0 nat_case_succ 
13194  17 
recursor_eqns recursor_0 recursor_succ 
9491
1a36151ee2fc
natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents:
6053
diff
changeset

18 

1a36151ee2fc
natify, a coercion to reduce the number of type constraints in arithmetic
paulson
parents:
6053
diff
changeset

19 

534  20 
consts 
13194  21 
Fin :: "i=>i" 
22 
FiniteFun :: "[i,i]=>i" ("(_ >/ _)" [61, 60] 60) 

534  23 

516  24 
inductive 
46820  25 
domains "Fin(A)" \<subseteq> "Pow(A)" 
13194  26 
intros 
46820  27 
emptyI: "0 \<in> Fin(A)" 
46953  28 
consI: "[ a \<in> A; b \<in> Fin(A) ] ==> cons(a,b) \<in> Fin(A)" 
13194  29 
type_intros empty_subsetI cons_subsetI PowI 
46471  30 
type_elims PowD [elim_format] 
534  31 

32 
inductive 

46820  33 
domains "FiniteFun(A,B)" \<subseteq> "Fin(A*B)" 
13194  34 
intros 
46820  35 
emptyI: "0 \<in> A > B" 
46953  36 
consI: "[ a \<in> A; b \<in> B; h \<in> A > B; a \<notin> domain(h) ] 
46820  37 
==> cons(<a,b>,h) \<in> A > B" 
13194  38 
type_intros Fin.intros 
39 

40 

13356  41 
subsection {* Finite Powerset Operator *} 
13194  42 

46820  43 
lemma Fin_mono: "A<=B ==> Fin(A) \<subseteq> Fin(B)" 
13194  44 
apply (unfold Fin.defs) 
45 
apply (rule lfp_mono) 

46 
apply (rule Fin.bnd_mono)+ 

47 
apply blast 

48 
done 

49 

46820  50 
(* @{term"A \<in> Fin(B) ==> A \<subseteq> B"} *) 
45602  51 
lemmas FinD = Fin.dom_subset [THEN subsetD, THEN PowD] 
13194  52 

53 
(** Induction on finite sets **) 

54 

46820  55 
(*Discharging @{term"x\<notin>y"} entails extra work*) 
13524  56 
lemma Fin_induct [case_names 0 cons, induct set: Fin]: 
46953  57 
"[ b \<in> Fin(A); 
13194  58 
P(0); 
46953  59 
!!x y. [ x \<in> A; y \<in> Fin(A); x\<notin>y; P(y) ] ==> P(cons(x,y)) 
13194  60 
] ==> P(b)" 
61 
apply (erule Fin.induct, simp) 

46953  62 
apply (case_tac "a \<in> b") 
13194  63 
apply (erule cons_absorb [THEN ssubst], assumption) (*backtracking!*) 
64 
apply simp 

65 
done 

66 

13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13194
diff
changeset

67 

13194  68 
(** Simplification for Fin **) 
69 
declare Fin.intros [simp] 

70 

13203
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13194
diff
changeset

71 
lemma Fin_0: "Fin(0) = {0}" 
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13194
diff
changeset

72 
by (blast intro: Fin.emptyI dest: FinD) 
fac77a839aa2
Tidying up. Mainly moving proofs from Main.thy to other (Isar) theory files.
paulson
parents:
13194
diff
changeset

73 

13194  74 
(*The union of two finite sets is finite.*) 
46953  75 
lemma Fin_UnI [simp]: "[ b \<in> Fin(A); c \<in> Fin(A) ] ==> b \<union> c \<in> Fin(A)" 
13194  76 
apply (erule Fin_induct) 
77 
apply (simp_all add: Un_cons) 

78 
done 

79 

80 

81 
(*The union of a set of finite sets is finite.*) 

46820  82 
lemma Fin_UnionI: "C \<in> Fin(Fin(A)) ==> \<Union>(C) \<in> Fin(A)" 
13194  83 
by (erule Fin_induct, simp_all) 
84 

85 
(*Every subset of a finite set is finite.*) 

46953  86 
lemma Fin_subset_lemma [rule_format]: "b \<in> Fin(A) ==> \<forall>z. z<=b \<longrightarrow> z \<in> Fin(A)" 
13194  87 
apply (erule Fin_induct) 
88 
apply (simp add: subset_empty_iff) 

89 
apply (simp add: subset_cons_iff distrib_simps, safe) 

13784  90 
apply (erule_tac b = z in cons_Diff [THEN subst], simp) 
13194  91 
done 
92 

46953  93 
lemma Fin_subset: "[ c<=b; b \<in> Fin(A) ] ==> c \<in> Fin(A)" 
13194  94 
by (blast intro: Fin_subset_lemma) 
95 

46953  96 
lemma Fin_IntI1 [intro,simp]: "b \<in> Fin(A) ==> b \<inter> c \<in> Fin(A)" 
13194  97 
by (blast intro: Fin_subset) 
98 

46953  99 
lemma Fin_IntI2 [intro,simp]: "c \<in> Fin(A) ==> b \<inter> c \<in> Fin(A)" 
13194  100 
by (blast intro: Fin_subset) 
101 

102 
lemma Fin_0_induct_lemma [rule_format]: 

46953  103 
"[ c \<in> Fin(A); b \<in> Fin(A); P(b); 
104 
!!x y. [ x \<in> A; y \<in> Fin(A); x \<in> y; P(y) ] ==> P(y{x}) 

46820  105 
] ==> c<=b \<longrightarrow> P(bc)" 
13194  106 
apply (erule Fin_induct, simp) 
107 
apply (subst Diff_cons) 

108 
apply (simp add: cons_subset_iff Diff_subset [THEN Fin_subset]) 

109 
done 

110 

111 
lemma Fin_0_induct: 

46953  112 
"[ b \<in> Fin(A); 
13194  113 
P(b); 
46953  114 
!!x y. [ x \<in> A; y \<in> Fin(A); x \<in> y; P(y) ] ==> P(y{x}) 
13194  115 
] ==> P(0)" 
116 
apply (rule Diff_cancel [THEN subst]) 

46820  117 
apply (blast intro: Fin_0_induct_lemma) 
13194  118 
done 
119 

120 
(*Functions from a finite ordinal*) 

46953  121 
lemma nat_fun_subset_Fin: "n \<in> nat ==> n>A \<subseteq> Fin(nat*A)" 
13194  122 
apply (induct_tac "n") 
123 
apply (simp add: subset_iff) 

124 
apply (simp add: succ_def mem_not_refl [THEN cons_fun_eq]) 

125 
apply (fast intro!: Fin.consI) 

126 
done 

127 

128 

13356  129 
subsection{*Finite Function Space*} 
13194  130 

131 
lemma FiniteFun_mono: 

46820  132 
"[ A<=C; B<=D ] ==> A > B \<subseteq> C > D" 
13194  133 
apply (unfold FiniteFun.defs) 
134 
apply (rule lfp_mono) 

135 
apply (rule FiniteFun.bnd_mono)+ 

136 
apply (intro Fin_mono Sigma_mono basic_monos, assumption+) 

137 
done 

138 

46820  139 
lemma FiniteFun_mono1: "A<=B ==> A > A \<subseteq> B > B" 
13194  140 
by (blast dest: FiniteFun_mono) 
141 

46953  142 
lemma FiniteFun_is_fun: "h \<in> A >B ==> h \<in> domain(h) > B" 
13194  143 
apply (erule FiniteFun.induct, simp) 
144 
apply (simp add: fun_extend3) 

145 
done 

146 

46953  147 
lemma FiniteFun_domain_Fin: "h \<in> A >B ==> domain(h) \<in> Fin(A)" 
13269  148 
by (erule FiniteFun.induct, simp, simp) 
13194  149 

45602  150 
lemmas FiniteFun_apply_type = FiniteFun_is_fun [THEN apply_type] 
13194  151 

152 
(*Every subset of a finite function is a finite function.*) 

153 
lemma FiniteFun_subset_lemma [rule_format]: 

46953  154 
"b \<in> A>B ==> \<forall>z. z<=b \<longrightarrow> z \<in> A>B" 
13194  155 
apply (erule FiniteFun.induct) 
156 
apply (simp add: subset_empty_iff FiniteFun.intros) 

157 
apply (simp add: subset_cons_iff distrib_simps, safe) 

13784  158 
apply (erule_tac b = z in cons_Diff [THEN subst]) 
13194  159 
apply (drule spec [THEN mp], assumption) 
160 
apply (fast intro!: FiniteFun.intros) 

161 
done 

162 

46953  163 
lemma FiniteFun_subset: "[ c<=b; b \<in> A>B ] ==> c \<in> A>B" 
13194  164 
by (blast intro: FiniteFun_subset_lemma) 
165 

166 
(** Some further results by Sidi O. Ehmety **) 

167 

46953  168 
lemma fun_FiniteFunI [rule_format]: "A \<in> Fin(X) ==> \<forall>f. f \<in> A>B \<longrightarrow> f \<in> A>B" 
13194  169 
apply (erule Fin.induct) 
13269  170 
apply (simp add: FiniteFun.intros, clarify) 
46953  171 
apply (case_tac "a \<in> b") 
13194  172 
apply (simp add: cons_absorb) 
46820  173 
apply (subgoal_tac "restrict (f,b) \<in> b > B") 
13194  174 
prefer 2 apply (blast intro: restrict_type2) 
175 
apply (subst fun_cons_restrict_eq, assumption) 

176 
apply (simp add: restrict_def lam_def) 

46820  177 
apply (blast intro: apply_funtype FiniteFun.intros 
13194  178 
FiniteFun_mono [THEN [2] rev_subsetD]) 
179 
done 

180 

46953  181 
lemma lam_FiniteFun: "A \<in> Fin(X) ==> (\<lambda>x\<in>A. b(x)) \<in> A > {b(x). x \<in> A}" 
13194  182 
by (blast intro: fun_FiniteFunI lam_funtype) 
183 

184 
lemma FiniteFun_Collect_iff: 

46953  185 
"f \<in> FiniteFun(A, {y \<in> B. P(y)}) 
46821
ff6b0c1087f2
Using mathematical notation for <> and cardinal arithmetic
paulson
parents:
46820
diff
changeset

186 
\<longleftrightarrow> f \<in> FiniteFun(A,B) & (\<forall>x\<in>domain(f). P(f`x))" 
13194  187 
apply auto 
188 
apply (blast intro: FiniteFun_mono [THEN [2] rev_subsetD]) 

189 
apply (blast dest: Pair_mem_PiD FiniteFun_is_fun) 

46820  190 
apply (rule_tac A1="domain(f)" in 
13194  191 
subset_refl [THEN [2] FiniteFun_mono, THEN subsetD]) 
192 
apply (fast dest: FiniteFun_domain_Fin Fin.dom_subset [THEN subsetD]) 

193 
apply (rule fun_FiniteFunI) 

194 
apply (erule FiniteFun_domain_Fin) 

195 
apply (rule_tac B = "range (f) " in fun_weaken_type) 

196 
apply (blast dest: FiniteFun_is_fun range_of_fun range_type apply_equality)+ 

197 
done 

198 

14883  199 

200 
subsection{*The Contents of a Singleton Set*} 

201 

24893  202 
definition 
203 
contents :: "i=>i" where 

14883  204 
"contents(X) == THE x. X = {x}" 
205 

206 
lemma contents_eq [simp]: "contents ({x}) = x" 

207 
by (simp add: contents_def) 

208 

516  209 
end 