23 |
23 |
24 inductive |
24 inductive |
25 domains "Fin(A)" \<subseteq> "Pow(A)" |
25 domains "Fin(A)" \<subseteq> "Pow(A)" |
26 intros |
26 intros |
27 emptyI: "0 \<in> Fin(A)" |
27 emptyI: "0 \<in> Fin(A)" |
28 consI: "[| a: A; b: Fin(A) |] ==> cons(a,b) \<in> Fin(A)" |
28 consI: "[| a \<in> A; b \<in> Fin(A) |] ==> cons(a,b) \<in> Fin(A)" |
29 type_intros empty_subsetI cons_subsetI PowI |
29 type_intros empty_subsetI cons_subsetI PowI |
30 type_elims PowD [elim_format] |
30 type_elims PowD [elim_format] |
31 |
31 |
32 inductive |
32 inductive |
33 domains "FiniteFun(A,B)" \<subseteq> "Fin(A*B)" |
33 domains "FiniteFun(A,B)" \<subseteq> "Fin(A*B)" |
34 intros |
34 intros |
35 emptyI: "0 \<in> A -||> B" |
35 emptyI: "0 \<in> A -||> B" |
36 consI: "[| a: A; b: B; h: A -||> B; a \<notin> domain(h) |] |
36 consI: "[| a \<in> A; b \<in> B; h \<in> A -||> B; a \<notin> domain(h) |] |
37 ==> cons(<a,b>,h) \<in> A -||> B" |
37 ==> cons(<a,b>,h) \<in> A -||> B" |
38 type_intros Fin.intros |
38 type_intros Fin.intros |
39 |
39 |
40 |
40 |
41 subsection {* Finite Powerset Operator *} |
41 subsection {* Finite Powerset Operator *} |
70 |
70 |
71 lemma Fin_0: "Fin(0) = {0}" |
71 lemma Fin_0: "Fin(0) = {0}" |
72 by (blast intro: Fin.emptyI dest: FinD) |
72 by (blast intro: Fin.emptyI dest: FinD) |
73 |
73 |
74 (*The union of two finite sets is finite.*) |
74 (*The union of two finite sets is finite.*) |
75 lemma Fin_UnI [simp]: "[| b: Fin(A); c: Fin(A) |] ==> b \<union> c \<in> Fin(A)" |
75 lemma Fin_UnI [simp]: "[| b \<in> Fin(A); c \<in> Fin(A) |] ==> b \<union> c \<in> Fin(A)" |
76 apply (erule Fin_induct) |
76 apply (erule Fin_induct) |
77 apply (simp_all add: Un_cons) |
77 apply (simp_all add: Un_cons) |
78 done |
78 done |
79 |
79 |
80 |
80 |
81 (*The union of a set of finite sets is finite.*) |
81 (*The union of a set of finite sets is finite.*) |
82 lemma Fin_UnionI: "C \<in> Fin(Fin(A)) ==> \<Union>(C) \<in> Fin(A)" |
82 lemma Fin_UnionI: "C \<in> Fin(Fin(A)) ==> \<Union>(C) \<in> Fin(A)" |
83 by (erule Fin_induct, simp_all) |
83 by (erule Fin_induct, simp_all) |
84 |
84 |
85 (*Every subset of a finite set is finite.*) |
85 (*Every subset of a finite set is finite.*) |
86 lemma Fin_subset_lemma [rule_format]: "b: Fin(A) ==> \<forall>z. z<=b \<longrightarrow> z: Fin(A)" |
86 lemma Fin_subset_lemma [rule_format]: "b \<in> Fin(A) ==> \<forall>z. z<=b \<longrightarrow> z \<in> Fin(A)" |
87 apply (erule Fin_induct) |
87 apply (erule Fin_induct) |
88 apply (simp add: subset_empty_iff) |
88 apply (simp add: subset_empty_iff) |
89 apply (simp add: subset_cons_iff distrib_simps, safe) |
89 apply (simp add: subset_cons_iff distrib_simps, safe) |
90 apply (erule_tac b = z in cons_Diff [THEN subst], simp) |
90 apply (erule_tac b = z in cons_Diff [THEN subst], simp) |
91 done |
91 done |
92 |
92 |
93 lemma Fin_subset: "[| c<=b; b: Fin(A) |] ==> c: Fin(A)" |
93 lemma Fin_subset: "[| c<=b; b \<in> Fin(A) |] ==> c \<in> Fin(A)" |
94 by (blast intro: Fin_subset_lemma) |
94 by (blast intro: Fin_subset_lemma) |
95 |
95 |
96 lemma Fin_IntI1 [intro,simp]: "b: Fin(A) ==> b \<inter> c \<in> Fin(A)" |
96 lemma Fin_IntI1 [intro,simp]: "b \<in> Fin(A) ==> b \<inter> c \<in> Fin(A)" |
97 by (blast intro: Fin_subset) |
97 by (blast intro: Fin_subset) |
98 |
98 |
99 lemma Fin_IntI2 [intro,simp]: "c: Fin(A) ==> b \<inter> c \<in> Fin(A)" |
99 lemma Fin_IntI2 [intro,simp]: "c \<in> Fin(A) ==> b \<inter> c \<in> Fin(A)" |
100 by (blast intro: Fin_subset) |
100 by (blast intro: Fin_subset) |
101 |
101 |
102 lemma Fin_0_induct_lemma [rule_format]: |
102 lemma Fin_0_induct_lemma [rule_format]: |
103 "[| c: Fin(A); b: Fin(A); P(b); |
103 "[| c \<in> Fin(A); b \<in> Fin(A); P(b); |
104 !!x y. [| x: A; y: Fin(A); x:y; P(y) |] ==> P(y-{x}) |
104 !!x y. [| x \<in> A; y \<in> Fin(A); x \<in> y; P(y) |] ==> P(y-{x}) |
105 |] ==> c<=b \<longrightarrow> P(b-c)" |
105 |] ==> c<=b \<longrightarrow> P(b-c)" |
106 apply (erule Fin_induct, simp) |
106 apply (erule Fin_induct, simp) |
107 apply (subst Diff_cons) |
107 apply (subst Diff_cons) |
108 apply (simp add: cons_subset_iff Diff_subset [THEN Fin_subset]) |
108 apply (simp add: cons_subset_iff Diff_subset [THEN Fin_subset]) |
109 done |
109 done |
110 |
110 |
111 lemma Fin_0_induct: |
111 lemma Fin_0_induct: |
112 "[| b: Fin(A); |
112 "[| b \<in> Fin(A); |
113 P(b); |
113 P(b); |
114 !!x y. [| x: A; y: Fin(A); x:y; P(y) |] ==> P(y-{x}) |
114 !!x y. [| x \<in> A; y \<in> Fin(A); x \<in> y; P(y) |] ==> P(y-{x}) |
115 |] ==> P(0)" |
115 |] ==> P(0)" |
116 apply (rule Diff_cancel [THEN subst]) |
116 apply (rule Diff_cancel [THEN subst]) |
117 apply (blast intro: Fin_0_induct_lemma) |
117 apply (blast intro: Fin_0_induct_lemma) |
118 done |
118 done |
119 |
119 |
120 (*Functions from a finite ordinal*) |
120 (*Functions from a finite ordinal*) |
121 lemma nat_fun_subset_Fin: "n: nat ==> n->A \<subseteq> Fin(nat*A)" |
121 lemma nat_fun_subset_Fin: "n \<in> nat ==> n->A \<subseteq> Fin(nat*A)" |
122 apply (induct_tac "n") |
122 apply (induct_tac "n") |
123 apply (simp add: subset_iff) |
123 apply (simp add: subset_iff) |
124 apply (simp add: succ_def mem_not_refl [THEN cons_fun_eq]) |
124 apply (simp add: succ_def mem_not_refl [THEN cons_fun_eq]) |
125 apply (fast intro!: Fin.consI) |
125 apply (fast intro!: Fin.consI) |
126 done |
126 done |
137 done |
137 done |
138 |
138 |
139 lemma FiniteFun_mono1: "A<=B ==> A -||> A \<subseteq> B -||> B" |
139 lemma FiniteFun_mono1: "A<=B ==> A -||> A \<subseteq> B -||> B" |
140 by (blast dest: FiniteFun_mono) |
140 by (blast dest: FiniteFun_mono) |
141 |
141 |
142 lemma FiniteFun_is_fun: "h: A -||>B ==> h: domain(h) -> B" |
142 lemma FiniteFun_is_fun: "h \<in> A -||>B ==> h \<in> domain(h) -> B" |
143 apply (erule FiniteFun.induct, simp) |
143 apply (erule FiniteFun.induct, simp) |
144 apply (simp add: fun_extend3) |
144 apply (simp add: fun_extend3) |
145 done |
145 done |
146 |
146 |
147 lemma FiniteFun_domain_Fin: "h: A -||>B ==> domain(h) \<in> Fin(A)" |
147 lemma FiniteFun_domain_Fin: "h \<in> A -||>B ==> domain(h) \<in> Fin(A)" |
148 by (erule FiniteFun.induct, simp, simp) |
148 by (erule FiniteFun.induct, simp, simp) |
149 |
149 |
150 lemmas FiniteFun_apply_type = FiniteFun_is_fun [THEN apply_type] |
150 lemmas FiniteFun_apply_type = FiniteFun_is_fun [THEN apply_type] |
151 |
151 |
152 (*Every subset of a finite function is a finite function.*) |
152 (*Every subset of a finite function is a finite function.*) |
153 lemma FiniteFun_subset_lemma [rule_format]: |
153 lemma FiniteFun_subset_lemma [rule_format]: |
154 "b: A-||>B ==> \<forall>z. z<=b \<longrightarrow> z: A-||>B" |
154 "b \<in> A-||>B ==> \<forall>z. z<=b \<longrightarrow> z \<in> A-||>B" |
155 apply (erule FiniteFun.induct) |
155 apply (erule FiniteFun.induct) |
156 apply (simp add: subset_empty_iff FiniteFun.intros) |
156 apply (simp add: subset_empty_iff FiniteFun.intros) |
157 apply (simp add: subset_cons_iff distrib_simps, safe) |
157 apply (simp add: subset_cons_iff distrib_simps, safe) |
158 apply (erule_tac b = z in cons_Diff [THEN subst]) |
158 apply (erule_tac b = z in cons_Diff [THEN subst]) |
159 apply (drule spec [THEN mp], assumption) |
159 apply (drule spec [THEN mp], assumption) |
160 apply (fast intro!: FiniteFun.intros) |
160 apply (fast intro!: FiniteFun.intros) |
161 done |
161 done |
162 |
162 |
163 lemma FiniteFun_subset: "[| c<=b; b: A-||>B |] ==> c: A-||>B" |
163 lemma FiniteFun_subset: "[| c<=b; b \<in> A-||>B |] ==> c \<in> A-||>B" |
164 by (blast intro: FiniteFun_subset_lemma) |
164 by (blast intro: FiniteFun_subset_lemma) |
165 |
165 |
166 (** Some further results by Sidi O. Ehmety **) |
166 (** Some further results by Sidi O. Ehmety **) |
167 |
167 |
168 lemma fun_FiniteFunI [rule_format]: "A:Fin(X) ==> \<forall>f. f:A->B \<longrightarrow> f:A-||>B" |
168 lemma fun_FiniteFunI [rule_format]: "A \<in> Fin(X) ==> \<forall>f. f \<in> A->B \<longrightarrow> f \<in> A-||>B" |
169 apply (erule Fin.induct) |
169 apply (erule Fin.induct) |
170 apply (simp add: FiniteFun.intros, clarify) |
170 apply (simp add: FiniteFun.intros, clarify) |
171 apply (case_tac "a:b") |
171 apply (case_tac "a \<in> b") |
172 apply (simp add: cons_absorb) |
172 apply (simp add: cons_absorb) |
173 apply (subgoal_tac "restrict (f,b) \<in> b -||> B") |
173 apply (subgoal_tac "restrict (f,b) \<in> b -||> B") |
174 prefer 2 apply (blast intro: restrict_type2) |
174 prefer 2 apply (blast intro: restrict_type2) |
175 apply (subst fun_cons_restrict_eq, assumption) |
175 apply (subst fun_cons_restrict_eq, assumption) |
176 apply (simp add: restrict_def lam_def) |
176 apply (simp add: restrict_def lam_def) |
177 apply (blast intro: apply_funtype FiniteFun.intros |
177 apply (blast intro: apply_funtype FiniteFun.intros |
178 FiniteFun_mono [THEN [2] rev_subsetD]) |
178 FiniteFun_mono [THEN [2] rev_subsetD]) |
179 done |
179 done |
180 |
180 |
181 lemma lam_FiniteFun: "A: Fin(X) ==> (\<lambda>x\<in>A. b(x)) \<in> A -||> {b(x). x:A}" |
181 lemma lam_FiniteFun: "A \<in> Fin(X) ==> (\<lambda>x\<in>A. b(x)) \<in> A -||> {b(x). x \<in> A}" |
182 by (blast intro: fun_FiniteFunI lam_funtype) |
182 by (blast intro: fun_FiniteFunI lam_funtype) |
183 |
183 |
184 lemma FiniteFun_Collect_iff: |
184 lemma FiniteFun_Collect_iff: |
185 "f \<in> FiniteFun(A, {y:B. P(y)}) |
185 "f \<in> FiniteFun(A, {y \<in> B. P(y)}) |
186 \<longleftrightarrow> f \<in> FiniteFun(A,B) & (\<forall>x\<in>domain(f). P(f`x))" |
186 \<longleftrightarrow> f \<in> FiniteFun(A,B) & (\<forall>x\<in>domain(f). P(f`x))" |
187 apply auto |
187 apply auto |
188 apply (blast intro: FiniteFun_mono [THEN [2] rev_subsetD]) |
188 apply (blast intro: FiniteFun_mono [THEN [2] rev_subsetD]) |
189 apply (blast dest: Pair_mem_PiD FiniteFun_is_fun) |
189 apply (blast dest: Pair_mem_PiD FiniteFun_is_fun) |
190 apply (rule_tac A1="domain(f)" in |
190 apply (rule_tac A1="domain(f)" in |