equal
deleted
inserted
replaced
149 apply (erule FiniteFun.induct, simp) |
149 apply (erule FiniteFun.induct, simp) |
150 apply (simp add: fun_extend3) |
150 apply (simp add: fun_extend3) |
151 done |
151 done |
152 |
152 |
153 lemma FiniteFun_domain_Fin: "h: A -||>B ==> domain(h) : Fin(A)" |
153 lemma FiniteFun_domain_Fin: "h: A -||>B ==> domain(h) : Fin(A)" |
154 apply (erule FiniteFun.induct, simp) |
154 by (erule FiniteFun.induct, simp, simp) |
155 apply simp |
|
156 done |
|
157 |
155 |
158 lemmas FiniteFun_apply_type = FiniteFun_is_fun [THEN apply_type, standard] |
156 lemmas FiniteFun_apply_type = FiniteFun_is_fun [THEN apply_type, standard] |
159 |
157 |
160 (*Every subset of a finite function is a finite function.*) |
158 (*Every subset of a finite function is a finite function.*) |
161 lemma FiniteFun_subset_lemma [rule_format]: |
159 lemma FiniteFun_subset_lemma [rule_format]: |
173 |
171 |
174 (** Some further results by Sidi O. Ehmety **) |
172 (** Some further results by Sidi O. Ehmety **) |
175 |
173 |
176 lemma fun_FiniteFunI [rule_format]: "A:Fin(X) ==> ALL f. f:A->B --> f:A-||>B" |
174 lemma fun_FiniteFunI [rule_format]: "A:Fin(X) ==> ALL f. f:A->B --> f:A-||>B" |
177 apply (erule Fin.induct) |
175 apply (erule Fin.induct) |
178 apply (simp add: FiniteFun.intros) |
176 apply (simp add: FiniteFun.intros, clarify) |
179 apply clarify |
|
180 apply (case_tac "a:b") |
177 apply (case_tac "a:b") |
181 apply (rotate_tac -1) |
178 apply (rotate_tac -1) |
182 apply (simp add: cons_absorb) |
179 apply (simp add: cons_absorb) |
183 apply (subgoal_tac "restrict (f,b) : b -||> B") |
180 apply (subgoal_tac "restrict (f,b) : b -||> B") |
184 prefer 2 apply (blast intro: restrict_type2) |
181 prefer 2 apply (blast intro: restrict_type2) |