src/HOL/Old_Number_Theory/BijectionRel.thy
 author wenzelm Sat Oct 10 16:26:23 2015 +0200 (2015-10-10) changeset 61382 efac889fccbc parent 58889 5b7a9633cfa8 permissions -rw-r--r--
isabelle update_cartouches;
1 (*  Title:      HOL/Old_Number_Theory/BijectionRel.thy
2     Author:     Thomas M. Rasmussen
3     Copyright   2000  University of Cambridge
4 *)
6 section \<open>Bijections between sets\<close>
8 theory BijectionRel
9 imports Main
10 begin
12 text \<open>
13   Inductive definitions of bijections between two different sets and
14   between the same set.  Theorem for relating the two definitions.
16   \bigskip
17 \<close>
19 inductive_set
20   bijR :: "('a => 'b => bool) => ('a set * 'b set) set"
21   for P :: "'a => 'b => bool"
22 where
23   empty [simp]: "({}, {}) \<in> bijR P"
24 | insert: "P a b ==> a \<notin> A ==> b \<notin> B ==> (A, B) \<in> bijR P
25     ==> (insert a A, insert b B) \<in> bijR P"
27 text \<open>
28   Add extra condition to @{term insert}: @{term "\<forall>b \<in> B. \<not> P a b"}
29   (and similar for @{term A}).
30 \<close>
32 definition
33   bijP :: "('a => 'a => bool) => 'a set => bool" where
34   "bijP P F = (\<forall>a b. a \<in> F \<and> P a b --> b \<in> F)"
36 definition
37   uniqP :: "('a => 'a => bool) => bool" where
38   "uniqP P = (\<forall>a b c d. P a b \<and> P c d --> (a = c) = (b = d))"
40 definition
41   symP :: "('a => 'a => bool) => bool" where
42   "symP P = (\<forall>a b. P a b = P b a)"
44 inductive_set
45   bijER :: "('a => 'a => bool) => 'a set set"
46   for P :: "'a => 'a => bool"
47 where
48   empty [simp]: "{} \<in> bijER P"
49 | insert1: "P a a ==> a \<notin> A ==> A \<in> bijER P ==> insert a A \<in> bijER P"
50 | insert2: "P a b ==> a \<noteq> b ==> a \<notin> A ==> b \<notin> A ==> A \<in> bijER P
51     ==> insert a (insert b A) \<in> bijER P"
54 text \<open>\medskip @{term bijR}\<close>
56 lemma fin_bijRl: "(A, B) \<in> bijR P ==> finite A"
57   apply (erule bijR.induct)
58   apply auto
59   done
61 lemma fin_bijRr: "(A, B) \<in> bijR P ==> finite B"
62   apply (erule bijR.induct)
63   apply auto
64   done
66 lemma aux_induct:
67   assumes major: "finite F"
68     and subs: "F \<subseteq> A"
69     and cases: "P {}"
70       "!!F a. F \<subseteq> A ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)"
71   shows "P F"
72   using major subs
73   apply (induct set: finite)
74    apply (blast intro: cases)+
75   done
78 lemma inj_func_bijR_aux1:
79     "A \<subseteq> B ==> a \<notin> A ==> a \<in> B ==> inj_on f B ==> f a \<notin> f ` A"
80   apply (unfold inj_on_def)
81   apply auto
82   done
84 lemma inj_func_bijR_aux2:
85   "\<forall>a. a \<in> A --> P a (f a) ==> inj_on f A ==> finite A ==> F <= A
86     ==> (F, f ` F) \<in> bijR P"
87   apply (rule_tac F = F and A = A in aux_induct)
88      apply (rule finite_subset)
89       apply auto
90   apply (rule bijR.insert)
91      apply (rule_tac [3] inj_func_bijR_aux1)
92         apply auto
93   done
95 lemma inj_func_bijR:
96   "\<forall>a. a \<in> A --> P a (f a) ==> inj_on f A ==> finite A
97     ==> (A, f ` A) \<in> bijR P"
98   apply (rule inj_func_bijR_aux2)
99      apply auto
100   done
103 text \<open>\medskip @{term bijER}\<close>
105 lemma fin_bijER: "A \<in> bijER P ==> finite A"
106   apply (erule bijER.induct)
107     apply auto
108   done
110 lemma aux1:
111   "a \<notin> A ==> a \<notin> B ==> F \<subseteq> insert a A ==> F \<subseteq> insert a B ==> a \<in> F
112     ==> \<exists>C. F = insert a C \<and> a \<notin> C \<and> C <= A \<and> C <= B"
113   apply (rule_tac x = "F - {a}" in exI)
114   apply auto
115   done
117 lemma aux2: "a \<noteq> b ==> a \<notin> A ==> b \<notin> B ==> a \<in> F ==> b \<in> F
118     ==> F \<subseteq> insert a A ==> F \<subseteq> insert b B
119     ==> \<exists>C. F = insert a (insert b C) \<and> a \<notin> C \<and> b \<notin> C \<and> C \<subseteq> A \<and> C \<subseteq> B"
120   apply (rule_tac x = "F - {a, b}" in exI)
121   apply auto
122   done
124 lemma aux_uniq: "uniqP P ==> P a b ==> P c d ==> (a = c) = (b = d)"
125   apply (unfold uniqP_def)
126   apply auto
127   done
129 lemma aux_sym: "symP P ==> P a b = P b a"
130   apply (unfold symP_def)
131   apply auto
132   done
134 lemma aux_in1:
135     "uniqP P ==> b \<notin> C ==> P b b ==> bijP P (insert b C) ==> bijP P C"
136   apply (unfold bijP_def)
137   apply auto
138   apply (subgoal_tac "b \<noteq> a")
139    prefer 2
140    apply clarify
142   apply auto
143   done
145 lemma aux_in2:
146   "symP P ==> uniqP P ==> a \<notin> C ==> b \<notin> C ==> a \<noteq> b ==> P a b
147     ==> bijP P (insert a (insert b C)) ==> bijP P C"
148   apply (unfold bijP_def)
149   apply auto
150   apply (subgoal_tac "aa \<noteq> a")
151    prefer 2
152    apply clarify
153   apply (subgoal_tac "aa \<noteq> b")
154    prefer 2
155    apply clarify
157   apply (subgoal_tac "ba \<noteq> a")
158    apply auto
159   apply (subgoal_tac "P a aa")
160    prefer 2
162   apply (subgoal_tac "b = aa")
163    apply (rule_tac [2] iffD1)
164     apply (rule_tac [2] a = a and c = a and P = P in aux_uniq)
165       apply auto
166   done
168 lemma aux_foo: "\<forall>a b. Q a \<and> P a b --> R b ==> P a b ==> Q a ==> R b"
169   apply auto
170   done
172 lemma aux_bij: "bijP P F ==> symP P ==> P a b ==> (a \<in> F) = (b \<in> F)"
173   apply (unfold bijP_def)
174   apply (rule iffI)
175   apply (erule_tac [!] aux_foo)
176       apply simp_all
177   apply (rule iffD2)
178    apply (rule_tac P = P in aux_sym)
179    apply simp_all
180   done
183 lemma aux_bijRER:
184   "(A, B) \<in> bijR P ==> uniqP P ==> symP P
185     ==> \<forall>F. bijP P F \<and> F \<subseteq> A \<and> F \<subseteq> B --> F \<in> bijER P"
186   apply (erule bijR.induct)
187    apply simp
188   apply (case_tac "a = b")
189    apply clarify
190    apply (case_tac "b \<in> F")
191     prefer 2
193    apply (cut_tac F = F and a = b and A = A and B = B in aux1)
194         prefer 6
195         apply clarify
196         apply (rule bijER.insert1)
197           apply simp_all
198    apply (subgoal_tac "bijP P C")
199     apply simp
200    apply (rule aux_in1)
201       apply simp_all
202   apply clarify
203   apply (case_tac "a \<in> F")
204    apply (case_tac [!] "b \<in> F")
205      apply (cut_tac F = F and a = a and b = b and A = A and B = B
206        in aux2)
208     apply clarify
209     apply (rule bijER.insert2)
210         apply simp_all
211     apply (subgoal_tac "bijP P C")
212      apply simp
213     apply (rule aux_in2)
214           apply simp_all
215    apply (subgoal_tac "b \<in> F")
216     apply (rule_tac [2] iffD1)
217      apply (rule_tac [2] a = a and F = F and P = P in aux_bij)
218        apply (simp_all (no_asm_simp))
219    apply (subgoal_tac [2] "a \<in> F")
220     apply (rule_tac [3] iffD2)
221      apply (rule_tac [3] b = b and F = F and P = P in aux_bij)
222        apply auto
223   done
225 lemma bijR_bijER:
226   "(A, A) \<in> bijR P ==>
227     bijP P A ==> uniqP P ==> symP P ==> A \<in> bijER P"
228   apply (cut_tac A = A and B = A and P = P in aux_bijRER)
229      apply auto
230   done
232 end