75 apply (rule major [THEN finite_induct]) |
75 apply (rule major [THEN finite_induct]) |
76 apply (blast intro: rule_context)+ |
76 apply (blast intro: rule_context)+ |
77 done |
77 done |
78 qed |
78 qed |
79 |
79 |
80 lemma aux: "A \<subseteq> B ==> a \<notin> A ==> a \<in> B ==> inj_on f B ==> f a \<notin> f ` A" |
80 lemma inj_func_bijR_aux1: |
|
81 "A \<subseteq> B ==> a \<notin> A ==> a \<in> B ==> inj_on f B ==> f a \<notin> f ` A" |
81 apply (unfold inj_on_def) |
82 apply (unfold inj_on_def) |
82 apply auto |
83 apply auto |
83 done |
84 done |
84 |
85 |
85 lemma aux: |
86 lemma inj_func_bijR_aux2: |
86 "\<forall>a. a \<in> A --> P a (f a) ==> inj_on f A ==> finite A ==> F <= A |
87 "\<forall>a. a \<in> A --> P a (f a) ==> inj_on f A ==> finite A ==> F <= A |
87 ==> (F, f ` F) \<in> bijR P" |
88 ==> (F, f ` F) \<in> bijR P" |
88 apply (rule_tac F = F and A = A in aux_induct) |
89 apply (rule_tac F = F and A = A in aux_induct) |
89 apply (rule finite_subset) |
90 apply (rule finite_subset) |
90 apply auto |
91 apply auto |
91 apply (rule bijR.insert) |
92 apply (rule bijR.insert) |
92 apply (rule_tac [3] aux) |
93 apply (rule_tac [3] inj_func_bijR_aux1) |
93 apply auto |
94 apply auto |
94 done |
95 done |
95 |
96 |
96 lemma inj_func_bijR: |
97 lemma inj_func_bijR: |
97 "\<forall>a. a \<in> A --> P a (f a) ==> inj_on f A ==> finite A |
98 "\<forall>a. a \<in> A --> P a (f a) ==> inj_on f A ==> finite A |
98 ==> (A, f ` A) \<in> bijR P" |
99 ==> (A, f ` A) \<in> bijR P" |
99 apply (rule aux) |
100 apply (rule inj_func_bijR_aux2) |
100 apply auto |
101 apply auto |
101 done |
102 done |
102 |
103 |
103 |
104 |
104 text {* \medskip @{term bijER} *} |
105 text {* \medskip @{term bijER} *} |
164 apply (rule_tac [2] iffD1) |
165 apply (rule_tac [2] iffD1) |
165 apply (rule_tac [2] a = a and c = a and P = P in aux_uniq) |
166 apply (rule_tac [2] a = a and c = a and P = P in aux_uniq) |
166 apply auto |
167 apply auto |
167 done |
168 done |
168 |
169 |
169 lemma aux: "\<forall>a b. Q a \<and> P a b --> R b ==> P a b ==> Q a ==> R b" |
170 lemma aux_foo: "\<forall>a b. Q a \<and> P a b --> R b ==> P a b ==> Q a ==> R b" |
170 apply auto |
171 apply auto |
171 done |
172 done |
172 |
173 |
173 lemma aux_bij: "bijP P F ==> symP P ==> P a b ==> (a \<in> F) = (b \<in> F)" |
174 lemma aux_bij: "bijP P F ==> symP P ==> P a b ==> (a \<in> F) = (b \<in> F)" |
174 apply (unfold bijP_def) |
175 apply (unfold bijP_def) |
175 apply (rule iffI) |
176 apply (rule iffI) |
176 apply (erule_tac [!] aux) |
177 apply (erule_tac [!] aux_foo) |
177 apply simp_all |
178 apply simp_all |
178 apply (rule iffD2) |
179 apply (rule iffD2) |
179 apply (rule_tac P = P in aux_sym) |
180 apply (rule_tac P = P in aux_sym) |
180 apply simp_all |
181 apply simp_all |
181 done |
182 done |