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