src/HOL/Old_Number_Theory/BijectionRel.thy
changeset 32479 521cc9bf2958
parent 23755 1c4672d130b1
child 38159 e9b4835a54ee
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Old_Number_Theory/BijectionRel.thy	Tue Sep 01 15:39:33 2009 +0200
     1.3 @@ -0,0 +1,229 @@
     1.4 +(*  Author:     Thomas M. Rasmussen
     1.5 +    Copyright   2000  University of Cambridge
     1.6 +*)
     1.7 +
     1.8 +header {* Bijections between sets *}
     1.9 +
    1.10 +theory BijectionRel imports Main begin
    1.11 +
    1.12 +text {*
    1.13 +  Inductive definitions of bijections between two different sets and
    1.14 +  between the same set.  Theorem for relating the two definitions.
    1.15 +
    1.16 +  \bigskip
    1.17 +*}
    1.18 +
    1.19 +inductive_set
    1.20 +  bijR :: "('a => 'b => bool) => ('a set * 'b set) set"
    1.21 +  for P :: "'a => 'b => bool"
    1.22 +where
    1.23 +  empty [simp]: "({}, {}) \<in> bijR P"
    1.24 +| insert: "P a b ==> a \<notin> A ==> b \<notin> B ==> (A, B) \<in> bijR P
    1.25 +    ==> (insert a A, insert b B) \<in> bijR P"
    1.26 +
    1.27 +text {*
    1.28 +  Add extra condition to @{term insert}: @{term "\<forall>b \<in> B. \<not> P a b"}
    1.29 +  (and similar for @{term A}).
    1.30 +*}
    1.31 +
    1.32 +definition
    1.33 +  bijP :: "('a => 'a => bool) => 'a set => bool" where
    1.34 +  "bijP P F = (\<forall>a b. a \<in> F \<and> P a b --> b \<in> F)"
    1.35 +
    1.36 +definition
    1.37 +  uniqP :: "('a => 'a => bool) => bool" where
    1.38 +  "uniqP P = (\<forall>a b c d. P a b \<and> P c d --> (a = c) = (b = d))"
    1.39 +
    1.40 +definition
    1.41 +  symP :: "('a => 'a => bool) => bool" where
    1.42 +  "symP P = (\<forall>a b. P a b = P b a)"
    1.43 +
    1.44 +inductive_set
    1.45 +  bijER :: "('a => 'a => bool) => 'a set set"
    1.46 +  for P :: "'a => 'a => bool"
    1.47 +where
    1.48 +  empty [simp]: "{} \<in> bijER P"
    1.49 +| insert1: "P a a ==> a \<notin> A ==> A \<in> bijER P ==> insert a A \<in> bijER P"
    1.50 +| insert2: "P a b ==> a \<noteq> b ==> a \<notin> A ==> b \<notin> A ==> A \<in> bijER P
    1.51 +    ==> insert a (insert b A) \<in> bijER P"
    1.52 +
    1.53 +
    1.54 +text {* \medskip @{term bijR} *}
    1.55 +
    1.56 +lemma fin_bijRl: "(A, B) \<in> bijR P ==> finite A"
    1.57 +  apply (erule bijR.induct)
    1.58 +  apply auto
    1.59 +  done
    1.60 +
    1.61 +lemma fin_bijRr: "(A, B) \<in> bijR P ==> finite B"
    1.62 +  apply (erule bijR.induct)
    1.63 +  apply auto
    1.64 +  done
    1.65 +
    1.66 +lemma aux_induct:
    1.67 +  assumes major: "finite F"
    1.68 +    and subs: "F \<subseteq> A"
    1.69 +    and cases: "P {}"
    1.70 +      "!!F a. F \<subseteq> A ==> a \<in> A ==> a \<notin> F ==> P F ==> P (insert a F)"
    1.71 +  shows "P F"
    1.72 +  using major subs
    1.73 +  apply (induct set: finite)
    1.74 +   apply (blast intro: cases)+
    1.75 +  done
    1.76 +
    1.77 +
    1.78 +lemma inj_func_bijR_aux1:
    1.79 +    "A \<subseteq> B ==> a \<notin> A ==> a \<in> B ==> inj_on f B ==> f a \<notin> f ` A"
    1.80 +  apply (unfold inj_on_def)
    1.81 +  apply auto
    1.82 +  done
    1.83 +
    1.84 +lemma inj_func_bijR_aux2:
    1.85 +  "\<forall>a. a \<in> A --> P a (f a) ==> inj_on f A ==> finite A ==> F <= A
    1.86 +    ==> (F, f ` F) \<in> bijR P"
    1.87 +  apply (rule_tac F = F and A = A in aux_induct)
    1.88 +     apply (rule finite_subset)
    1.89 +      apply auto
    1.90 +  apply (rule bijR.insert)
    1.91 +     apply (rule_tac [3] inj_func_bijR_aux1)
    1.92 +        apply auto
    1.93 +  done
    1.94 +
    1.95 +lemma inj_func_bijR:
    1.96 +  "\<forall>a. a \<in> A --> P a (f a) ==> inj_on f A ==> finite A
    1.97 +    ==> (A, f ` A) \<in> bijR P"
    1.98 +  apply (rule inj_func_bijR_aux2)
    1.99 +     apply auto
   1.100 +  done
   1.101 +
   1.102 +
   1.103 +text {* \medskip @{term bijER} *}
   1.104 +
   1.105 +lemma fin_bijER: "A \<in> bijER P ==> finite A"
   1.106 +  apply (erule bijER.induct)
   1.107 +    apply auto
   1.108 +  done
   1.109 +
   1.110 +lemma aux1:
   1.111 +  "a \<notin> A ==> a \<notin> B ==> F \<subseteq> insert a A ==> F \<subseteq> insert a B ==> a \<in> F
   1.112 +    ==> \<exists>C. F = insert a C \<and> a \<notin> C \<and> C <= A \<and> C <= B"
   1.113 +  apply (rule_tac x = "F - {a}" in exI)
   1.114 +  apply auto
   1.115 +  done
   1.116 +
   1.117 +lemma aux2: "a \<noteq> b ==> a \<notin> A ==> b \<notin> B ==> a \<in> F ==> b \<in> F
   1.118 +    ==> F \<subseteq> insert a A ==> F \<subseteq> insert b B
   1.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"
   1.120 +  apply (rule_tac x = "F - {a, b}" in exI)
   1.121 +  apply auto
   1.122 +  done
   1.123 +
   1.124 +lemma aux_uniq: "uniqP P ==> P a b ==> P c d ==> (a = c) = (b = d)"
   1.125 +  apply (unfold uniqP_def)
   1.126 +  apply auto
   1.127 +  done
   1.128 +
   1.129 +lemma aux_sym: "symP P ==> P a b = P b a"
   1.130 +  apply (unfold symP_def)
   1.131 +  apply auto
   1.132 +  done
   1.133 +
   1.134 +lemma aux_in1:
   1.135 +    "uniqP P ==> b \<notin> C ==> P b b ==> bijP P (insert b C) ==> bijP P C"
   1.136 +  apply (unfold bijP_def)
   1.137 +  apply auto
   1.138 +  apply (subgoal_tac "b \<noteq> a")
   1.139 +   prefer 2
   1.140 +   apply clarify
   1.141 +  apply (simp add: aux_uniq)
   1.142 +  apply auto
   1.143 +  done
   1.144 +
   1.145 +lemma aux_in2:
   1.146 +  "symP P ==> uniqP P ==> a \<notin> C ==> b \<notin> C ==> a \<noteq> b ==> P a b
   1.147 +    ==> bijP P (insert a (insert b C)) ==> bijP P C"
   1.148 +  apply (unfold bijP_def)
   1.149 +  apply auto
   1.150 +  apply (subgoal_tac "aa \<noteq> a")
   1.151 +   prefer 2
   1.152 +   apply clarify
   1.153 +  apply (subgoal_tac "aa \<noteq> b")
   1.154 +   prefer 2
   1.155 +   apply clarify
   1.156 +  apply (simp add: aux_uniq)
   1.157 +  apply (subgoal_tac "ba \<noteq> a")
   1.158 +   apply auto
   1.159 +  apply (subgoal_tac "P a aa")
   1.160 +   prefer 2
   1.161 +   apply (simp add: aux_sym)
   1.162 +  apply (subgoal_tac "b = aa")
   1.163 +   apply (rule_tac [2] iffD1)
   1.164 +    apply (rule_tac [2] a = a and c = a and P = P in aux_uniq)
   1.165 +      apply auto
   1.166 +  done
   1.167 +
   1.168 +lemma aux_foo: "\<forall>a b. Q a \<and> P a b --> R b ==> P a b ==> Q a ==> R b"
   1.169 +  apply auto
   1.170 +  done
   1.171 +
   1.172 +lemma aux_bij: "bijP P F ==> symP P ==> P a b ==> (a \<in> F) = (b \<in> F)"
   1.173 +  apply (unfold bijP_def)
   1.174 +  apply (rule iffI)
   1.175 +  apply (erule_tac [!] aux_foo)
   1.176 +      apply simp_all
   1.177 +  apply (rule iffD2)
   1.178 +   apply (rule_tac P = P in aux_sym)
   1.179 +   apply simp_all
   1.180 +  done
   1.181 +
   1.182 +
   1.183 +lemma aux_bijRER:
   1.184 +  "(A, B) \<in> bijR P ==> uniqP P ==> symP P
   1.185 +    ==> \<forall>F. bijP P F \<and> F \<subseteq> A \<and> F \<subseteq> B --> F \<in> bijER P"
   1.186 +  apply (erule bijR.induct)
   1.187 +   apply simp
   1.188 +  apply (case_tac "a = b")
   1.189 +   apply clarify
   1.190 +   apply (case_tac "b \<in> F")
   1.191 +    prefer 2
   1.192 +    apply (simp add: subset_insert)
   1.193 +   apply (cut_tac F = F and a = b and A = A and B = B in aux1)
   1.194 +        prefer 6
   1.195 +        apply clarify
   1.196 +        apply (rule bijER.insert1)
   1.197 +          apply simp_all
   1.198 +   apply (subgoal_tac "bijP P C")
   1.199 +    apply simp
   1.200 +   apply (rule aux_in1)
   1.201 +      apply simp_all
   1.202 +  apply clarify
   1.203 +  apply (case_tac "a \<in> F")
   1.204 +   apply (case_tac [!] "b \<in> F")
   1.205 +     apply (cut_tac F = F and a = a and b = b and A = A and B = B
   1.206 +       in aux2)
   1.207 +            apply (simp_all add: subset_insert)
   1.208 +    apply clarify
   1.209 +    apply (rule bijER.insert2)
   1.210 +        apply simp_all
   1.211 +    apply (subgoal_tac "bijP P C")
   1.212 +     apply simp
   1.213 +    apply (rule aux_in2)
   1.214 +          apply simp_all
   1.215 +   apply (subgoal_tac "b \<in> F")
   1.216 +    apply (rule_tac [2] iffD1)
   1.217 +     apply (rule_tac [2] a = a and F = F and P = P in aux_bij)
   1.218 +       apply (simp_all (no_asm_simp))
   1.219 +   apply (subgoal_tac [2] "a \<in> F")
   1.220 +    apply (rule_tac [3] iffD2)
   1.221 +     apply (rule_tac [3] b = b and F = F and P = P in aux_bij)
   1.222 +       apply auto
   1.223 +  done
   1.224 +
   1.225 +lemma bijR_bijER:
   1.226 +  "(A, A) \<in> bijR P ==>
   1.227 +    bijP P A ==> uniqP P ==> symP P ==> A \<in> bijER P"
   1.228 +  apply (cut_tac A = A and B = A and P = P in aux_bijRER)
   1.229 +     apply auto
   1.230 +  done
   1.231 +
   1.232 +end