src/HOL/Algebra/Congruence.thy
 author wenzelm Mon Mar 16 18:24:30 2009 +0100 (2009-03-16) changeset 30549 d2d7874648bd parent 29237 e90d9d51106b child 35355 613e133966ea permissions -rw-r--r--
simplified method setup;
 ballarin@27701 ` 1` ```(* ``` ballarin@27701 ` 2` ``` Title: Algebra/Congruence.thy ``` ballarin@27701 ` 3` ``` Author: Clemens Ballarin, started 3 January 2008 ``` ballarin@27701 ` 4` ``` Copyright: Clemens Ballarin ``` ballarin@27701 ` 5` ```*) ``` ballarin@27701 ` 6` ballarin@27701 ` 7` ```theory Congruence imports Main begin ``` ballarin@27701 ` 8` ballarin@27701 ` 9` ```section {* Objects *} ``` ballarin@27701 ` 10` ballarin@27717 ` 11` ```subsection {* Structure with Carrier Set. *} ``` ballarin@27701 ` 12` ballarin@27701 ` 13` ```record 'a partial_object = ``` ballarin@27701 ` 14` ``` carrier :: "'a set" ``` ballarin@27701 ` 15` ballarin@27717 ` 16` ballarin@27717 ` 17` ```subsection {* Structure with Carrier and Equivalence Relation @{text eq} *} ``` ballarin@27701 ` 18` ballarin@27701 ` 19` ```record 'a eq_object = "'a partial_object" + ``` ballarin@27701 ` 20` ``` eq :: "'a \ 'a \ bool" (infixl ".=\" 50) ``` ballarin@27701 ` 21` ballarin@27701 ` 22` ```constdefs (structure S) ``` ballarin@27701 ` 23` ``` elem :: "_ \ 'a \ 'a set \ bool" (infixl ".\\" 50) ``` ballarin@27701 ` 24` ``` "x .\ A \ (\y \ A. x .= y)" ``` ballarin@27701 ` 25` ballarin@27701 ` 26` ``` set_eq :: "_ \ 'a set \ 'a set \ bool" (infixl "{.=}\" 50) ``` ballarin@27701 ` 27` ``` "A {.=} B == ((\x \ A. x .\ B) \ (\x \ B. x .\ A))" ``` ballarin@27701 ` 28` ballarin@27701 ` 29` ``` eq_class_of :: "_ \ 'a \ 'a set" ("class'_of\ _") ``` ballarin@27701 ` 30` ``` "class_of x == {y \ carrier S. x .= y}" ``` ballarin@27701 ` 31` ballarin@27701 ` 32` ``` eq_closure_of :: "_ \ 'a set \ 'a set" ("closure'_of\ _") ``` ballarin@27701 ` 33` ``` "closure_of A == {y \ carrier S. y .\ A}" ``` ballarin@27701 ` 34` ballarin@27701 ` 35` ``` eq_is_closed :: "_ \ 'a set \ bool" ("is'_closed\ _") ``` ballarin@27701 ` 36` ``` "is_closed A == (A \ carrier S \ closure_of A = A)" ``` ballarin@27701 ` 37` ballarin@27701 ` 38` ```syntax ``` ballarin@27701 ` 39` ``` not_eq :: "_ \ 'a \ 'a \ bool" (infixl ".\\" 50) ``` ballarin@27701 ` 40` ``` not_elem :: "_ \ 'a \ 'a set \ bool" (infixl ".\\" 50) ``` ballarin@27701 ` 41` ``` set_not_eq :: "_ \ 'a set \ 'a set \ bool" (infixl "{.\}\" 50) ``` ballarin@27701 ` 42` ballarin@27701 ` 43` ```translations ``` ballarin@27701 ` 44` ``` "x .\\ y" == "~(x .=\ y)" ``` ballarin@27701 ` 45` ``` "x .\\ A" == "~(x .\\ A)" ``` ballarin@27701 ` 46` ``` "A {.\}\ B" == "~(A {.=}\ B)" ``` ballarin@27701 ` 47` ballarin@27701 ` 48` ```locale equivalence = ``` ballarin@27701 ` 49` ``` fixes S (structure) ``` ballarin@27701 ` 50` ``` assumes refl [simp, intro]: "x \ carrier S \ x .= x" ``` ballarin@27701 ` 51` ``` and sym [sym]: "\ x .= y; x \ carrier S; y \ carrier S \ \ y .= x" ``` ballarin@27701 ` 52` ``` and trans [trans]: "\ x .= y; y .= z; x \ carrier S; y \ carrier S; z \ carrier S \ \ x .= z" ``` ballarin@27701 ` 53` ballarin@27717 ` 54` ```(* Lemmas by Stephan Hohe *) ``` ballarin@27717 ` 55` ballarin@27701 ` 56` ```lemma elemI: ``` ballarin@27701 ` 57` ``` fixes R (structure) ``` ballarin@27701 ` 58` ``` assumes "a' \ A" and "a .= a'" ``` ballarin@27701 ` 59` ``` shows "a .\ A" ``` ballarin@27701 ` 60` ```unfolding elem_def ``` ballarin@27701 ` 61` ```using assms ``` ballarin@27701 ` 62` ```by fast ``` ballarin@27701 ` 63` ballarin@27701 ` 64` ```lemma (in equivalence) elem_exact: ``` ballarin@27701 ` 65` ``` assumes "a \ carrier S" and "a \ A" ``` ballarin@27701 ` 66` ``` shows "a .\ A" ``` ballarin@27701 ` 67` ```using assms ``` ballarin@27701 ` 68` ```by (fast intro: elemI) ``` ballarin@27701 ` 69` ballarin@27701 ` 70` ```lemma elemE: ``` ballarin@27701 ` 71` ``` fixes S (structure) ``` ballarin@27701 ` 72` ``` assumes "a .\ A" ``` ballarin@27701 ` 73` ``` and "\a'. \a' \ A; a .= a'\ \ P" ``` ballarin@27701 ` 74` ``` shows "P" ``` ballarin@27701 ` 75` ```using assms ``` ballarin@27701 ` 76` ```unfolding elem_def ``` ballarin@27701 ` 77` ```by fast ``` ballarin@27701 ` 78` ballarin@27701 ` 79` ```lemma (in equivalence) elem_cong_l [trans]: ``` ballarin@27701 ` 80` ``` assumes cong: "a' .= a" ``` ballarin@27701 ` 81` ``` and a: "a .\ A" ``` ballarin@27701 ` 82` ``` and carr: "a \ carrier S" "a' \ carrier S" ``` ballarin@27701 ` 83` ``` and Acarr: "A \ carrier S" ``` ballarin@27701 ` 84` ``` shows "a' .\ A" ``` ballarin@27701 ` 85` ```using a ``` ballarin@27701 ` 86` ```apply (elim elemE, intro elemI) ``` ballarin@27701 ` 87` ```proof assumption ``` ballarin@27701 ` 88` ``` fix b ``` ballarin@27701 ` 89` ``` assume bA: "b \ A" ``` ballarin@27701 ` 90` ``` note [simp] = carr bA[THEN subsetD[OF Acarr]] ``` ballarin@27701 ` 91` ``` note cong ``` ballarin@27701 ` 92` ``` also assume "a .= b" ``` ballarin@27701 ` 93` ``` finally show "a' .= b" by simp ``` ballarin@27701 ` 94` ```qed ``` ballarin@27701 ` 95` ballarin@27701 ` 96` ```lemma (in equivalence) elem_subsetD: ``` ballarin@27701 ` 97` ``` assumes "A \ B" ``` ballarin@27701 ` 98` ``` and aA: "a .\ A" ``` ballarin@27701 ` 99` ``` shows "a .\ B" ``` ballarin@27701 ` 100` ```using assms ``` ballarin@27701 ` 101` ```by (fast intro: elemI elim: elemE dest: subsetD) ``` ballarin@27701 ` 102` ballarin@27701 ` 103` ```lemma (in equivalence) mem_imp_elem [simp, intro]: ``` ballarin@27701 ` 104` ``` "[| x \ A; x \ carrier S |] ==> x .\ A" ``` ballarin@27701 ` 105` ``` unfolding elem_def by blast ``` ballarin@27701 ` 106` ballarin@27701 ` 107` ```lemma set_eqI: ``` ballarin@27701 ` 108` ``` fixes R (structure) ``` ballarin@27701 ` 109` ``` assumes ltr: "\a. a \ A \ a .\ B" ``` ballarin@27701 ` 110` ``` and rtl: "\b. b \ B \ b .\ A" ``` ballarin@27701 ` 111` ``` shows "A {.=} B" ``` ballarin@27701 ` 112` ```unfolding set_eq_def ``` ballarin@27701 ` 113` ```by (fast intro: ltr rtl) ``` ballarin@27701 ` 114` ballarin@27701 ` 115` ```lemma set_eqI2: ``` ballarin@27701 ` 116` ``` fixes R (structure) ``` ballarin@27701 ` 117` ``` assumes ltr: "\a b. a \ A \ \b\B. a .= b" ``` ballarin@27701 ` 118` ``` and rtl: "\b. b \ B \ \a\A. b .= a" ``` ballarin@27701 ` 119` ``` shows "A {.=} B" ``` ballarin@27701 ` 120` ``` by (intro set_eqI, unfold elem_def) (fast intro: ltr rtl)+ ``` ballarin@27701 ` 121` ballarin@27701 ` 122` ```lemma set_eqD1: ``` ballarin@27701 ` 123` ``` fixes R (structure) ``` ballarin@27701 ` 124` ``` assumes AA': "A {.=} A'" ``` ballarin@27701 ` 125` ``` and "a \ A" ``` ballarin@27701 ` 126` ``` shows "\a'\A'. a .= a'" ``` ballarin@27701 ` 127` ```using assms ``` ballarin@27701 ` 128` ```unfolding set_eq_def elem_def ``` ballarin@27701 ` 129` ```by fast ``` ballarin@27701 ` 130` ballarin@27701 ` 131` ```lemma set_eqD2: ``` ballarin@27701 ` 132` ``` fixes R (structure) ``` ballarin@27701 ` 133` ``` assumes AA': "A {.=} A'" ``` ballarin@27701 ` 134` ``` and "a' \ A'" ``` ballarin@27701 ` 135` ``` shows "\a\A. a' .= a" ``` ballarin@27701 ` 136` ```using assms ``` ballarin@27701 ` 137` ```unfolding set_eq_def elem_def ``` ballarin@27701 ` 138` ```by fast ``` ballarin@27701 ` 139` ballarin@27701 ` 140` ```lemma set_eqE: ``` ballarin@27701 ` 141` ``` fixes R (structure) ``` ballarin@27701 ` 142` ``` assumes AB: "A {.=} B" ``` ballarin@27701 ` 143` ``` and r: "\\a\A. a .\ B; \b\B. b .\ A\ \ P" ``` ballarin@27701 ` 144` ``` shows "P" ``` ballarin@27701 ` 145` ```using AB ``` ballarin@27701 ` 146` ```unfolding set_eq_def ``` ballarin@27701 ` 147` ```by (blast dest: r) ``` ballarin@27701 ` 148` ballarin@27701 ` 149` ```lemma set_eqE2: ``` ballarin@27701 ` 150` ``` fixes R (structure) ``` ballarin@27701 ` 151` ``` assumes AB: "A {.=} B" ``` ballarin@27701 ` 152` ``` and r: "\\a\A. (\b\B. a .= b); \b\B. (\a\A. b .= a)\ \ P" ``` ballarin@27701 ` 153` ``` shows "P" ``` ballarin@27701 ` 154` ```using AB ``` ballarin@27701 ` 155` ```unfolding set_eq_def elem_def ``` ballarin@27701 ` 156` ```by (blast dest: r) ``` ballarin@27701 ` 157` ballarin@27701 ` 158` ```lemma set_eqE': ``` ballarin@27701 ` 159` ``` fixes R (structure) ``` ballarin@27701 ` 160` ``` assumes AB: "A {.=} B" ``` ballarin@27701 ` 161` ``` and aA: "a \ A" and bB: "b \ B" ``` ballarin@27701 ` 162` ``` and r: "\a' b'. \a' \ A; b .= a'; b' \ B; a .= b'\ \ P" ``` ballarin@27701 ` 163` ``` shows "P" ``` ballarin@27701 ` 164` ```proof - ``` ballarin@27701 ` 165` ``` from AB aA ``` ballarin@27701 ` 166` ``` have "\b'\B. a .= b'" by (rule set_eqD1) ``` ballarin@27701 ` 167` ``` from this obtain b' ``` ballarin@27701 ` 168` ``` where b': "b' \ B" "a .= b'" by auto ``` ballarin@27701 ` 169` ballarin@27701 ` 170` ``` from AB bB ``` ballarin@27701 ` 171` ``` have "\a'\A. b .= a'" by (rule set_eqD2) ``` ballarin@27701 ` 172` ``` from this obtain a' ``` ballarin@27701 ` 173` ``` where a': "a' \ A" "b .= a'" by auto ``` ballarin@27701 ` 174` ballarin@27701 ` 175` ``` from a' b' ``` ballarin@27701 ` 176` ``` show "P" by (rule r) ``` ballarin@27701 ` 177` ```qed ``` ballarin@27701 ` 178` ballarin@27701 ` 179` ```lemma (in equivalence) eq_elem_cong_r [trans]: ``` ballarin@27701 ` 180` ``` assumes a: "a .\ A" ``` ballarin@27701 ` 181` ``` and cong: "A {.=} A'" ``` ballarin@27701 ` 182` ``` and carr: "a \ carrier S" ``` ballarin@27701 ` 183` ``` and Carr: "A \ carrier S" "A' \ carrier S" ``` ballarin@27701 ` 184` ``` shows "a .\ A'" ``` ballarin@27701 ` 185` ```using a cong ``` ballarin@27701 ` 186` ```proof (elim elemE set_eqE) ``` ballarin@27701 ` 187` ``` fix b ``` ballarin@27701 ` 188` ``` assume bA: "b \ A" ``` ballarin@27701 ` 189` ``` and inA': "\b\A. b .\ A'" ``` ballarin@27701 ` 190` ``` note [simp] = carr Carr Carr[THEN subsetD] bA ``` ballarin@27701 ` 191` ``` assume "a .= b" ``` ballarin@27701 ` 192` ``` also from bA inA' ``` ballarin@27701 ` 193` ``` have "b .\ A'" by fast ``` ballarin@27701 ` 194` ``` finally ``` ballarin@27701 ` 195` ``` show "a .\ A'" by simp ``` ballarin@27701 ` 196` ```qed ``` ballarin@27701 ` 197` ballarin@27701 ` 198` ```lemma (in equivalence) set_eq_sym [sym]: ``` ballarin@27701 ` 199` ``` assumes "A {.=} B" ``` ballarin@27701 ` 200` ``` and "A \ carrier S" "B \ carrier S" ``` ballarin@27701 ` 201` ``` shows "B {.=} A" ``` ballarin@27701 ` 202` ```using assms ``` ballarin@27701 ` 203` ```unfolding set_eq_def elem_def ``` ballarin@27701 ` 204` ```by fast ``` ballarin@27701 ` 205` ballarin@27701 ` 206` ```(* FIXME: the following two required in Isabelle 2008, not Isabelle 2007 *) ``` ballarin@27717 ` 207` ```(* alternatively, could declare lemmas [trans] = ssubst [where 'a = "'a set"] *) ``` ballarin@27701 ` 208` ballarin@27701 ` 209` ```lemma (in equivalence) equal_set_eq_trans [trans]: ``` ballarin@27701 ` 210` ``` assumes AB: "A = B" and BC: "B {.=} C" ``` ballarin@27701 ` 211` ``` shows "A {.=} C" ``` ballarin@27701 ` 212` ``` using AB BC by simp ``` ballarin@27701 ` 213` ballarin@27701 ` 214` ```lemma (in equivalence) set_eq_equal_trans [trans]: ``` ballarin@27701 ` 215` ``` assumes AB: "A {.=} B" and BC: "B = C" ``` ballarin@27701 ` 216` ``` shows "A {.=} C" ``` ballarin@27701 ` 217` ``` using AB BC by simp ``` ballarin@27701 ` 218` ballarin@27717 ` 219` ballarin@27701 ` 220` ```lemma (in equivalence) set_eq_trans [trans]: ``` ballarin@27701 ` 221` ``` assumes AB: "A {.=} B" and BC: "B {.=} C" ``` ballarin@27701 ` 222` ``` and carr: "A \ carrier S" "B \ carrier S" "C \ carrier S" ``` ballarin@27701 ` 223` ``` shows "A {.=} C" ``` ballarin@27701 ` 224` ```proof (intro set_eqI) ``` ballarin@27701 ` 225` ``` fix a ``` ballarin@27701 ` 226` ``` assume aA: "a \ A" ``` ballarin@27701 ` 227` ``` with carr have "a \ carrier S" by fast ``` ballarin@27701 ` 228` ``` note [simp] = carr this ``` ballarin@27701 ` 229` ballarin@27701 ` 230` ``` from aA ``` ballarin@27701 ` 231` ``` have "a .\ A" by (simp add: elem_exact) ``` ballarin@27701 ` 232` ``` also note AB ``` ballarin@27701 ` 233` ``` also note BC ``` ballarin@27701 ` 234` ``` finally ``` ballarin@27701 ` 235` ``` show "a .\ C" by simp ``` ballarin@27701 ` 236` ```next ``` ballarin@27701 ` 237` ``` fix c ``` ballarin@27701 ` 238` ``` assume cC: "c \ C" ``` ballarin@27701 ` 239` ``` with carr have "c \ carrier S" by fast ``` ballarin@27701 ` 240` ``` note [simp] = carr this ``` ballarin@27701 ` 241` ballarin@27701 ` 242` ``` from cC ``` ballarin@27701 ` 243` ``` have "c .\ C" by (simp add: elem_exact) ``` ballarin@27701 ` 244` ``` also note BC[symmetric] ``` ballarin@27701 ` 245` ``` also note AB[symmetric] ``` ballarin@27701 ` 246` ``` finally ``` ballarin@27701 ` 247` ``` show "c .\ A" by simp ``` ballarin@27701 ` 248` ```qed ``` ballarin@27701 ` 249` ballarin@27701 ` 250` ```(* FIXME: generalise for insert *) ``` ballarin@27701 ` 251` ballarin@27701 ` 252` ```(* ``` ballarin@27701 ` 253` ```lemma (in equivalence) set_eq_insert: ``` ballarin@27701 ` 254` ``` assumes x: "x .= x'" ``` ballarin@27701 ` 255` ``` and carr: "x \ carrier S" "x' \ carrier S" "A \ carrier S" ``` ballarin@27701 ` 256` ``` shows "insert x A {.=} insert x' A" ``` ballarin@27701 ` 257` ``` unfolding set_eq_def elem_def ``` ballarin@27701 ` 258` ```apply rule ``` ballarin@27701 ` 259` ```apply rule ``` ballarin@27701 ` 260` ```apply (case_tac "xa = x") ``` ballarin@27701 ` 261` ```using x apply fast ``` ballarin@27701 ` 262` ```apply (subgoal_tac "xa \ A") prefer 2 apply fast ``` ballarin@27701 ` 263` ```apply (rule_tac x=xa in bexI) ``` ballarin@27701 ` 264` ```using carr apply (rule_tac refl) apply auto [1] ``` ballarin@27701 ` 265` ```apply safe ``` ballarin@27701 ` 266` ```*) ``` ballarin@27701 ` 267` ballarin@27701 ` 268` ```lemma (in equivalence) set_eq_pairI: ``` ballarin@27701 ` 269` ``` assumes xx': "x .= x'" ``` ballarin@27701 ` 270` ``` and carr: "x \ carrier S" "x' \ carrier S" "y \ carrier S" ``` ballarin@27701 ` 271` ``` shows "{x, y} {.=} {x', y}" ``` ballarin@27701 ` 272` ```unfolding set_eq_def elem_def ``` ballarin@27701 ` 273` ```proof safe ``` ballarin@27701 ` 274` ``` have "x' \ {x', y}" by fast ``` ballarin@27701 ` 275` ``` with xx' show "\b\{x', y}. x .= b" by fast ``` ballarin@27701 ` 276` ```next ``` ballarin@27701 ` 277` ``` have "y \ {x', y}" by fast ``` ballarin@27701 ` 278` ``` with carr show "\b\{x', y}. y .= b" by fast ``` ballarin@27701 ` 279` ```next ``` ballarin@27701 ` 280` ``` have "x \ {x, y}" by fast ``` ballarin@27701 ` 281` ``` with xx'[symmetric] carr ``` ballarin@27701 ` 282` ``` show "\a\{x, y}. x' .= a" by fast ``` ballarin@27701 ` 283` ```next ``` ballarin@27701 ` 284` ``` have "y \ {x, y}" by fast ``` ballarin@27701 ` 285` ``` with carr show "\a\{x, y}. y .= a" by fast ``` ballarin@27701 ` 286` ```qed ``` ballarin@27701 ` 287` ballarin@27701 ` 288` ```lemma (in equivalence) is_closedI: ``` ballarin@27701 ` 289` ``` assumes closed: "!!x y. [| x .= y; x \ A; y \ carrier S |] ==> y \ A" ``` ballarin@27701 ` 290` ``` and S: "A \ carrier S" ``` ballarin@27701 ` 291` ``` shows "is_closed A" ``` ballarin@27701 ` 292` ``` unfolding eq_is_closed_def eq_closure_of_def elem_def ``` ballarin@27701 ` 293` ``` using S ``` ballarin@27701 ` 294` ``` by (blast dest: closed sym) ``` ballarin@27701 ` 295` ballarin@27701 ` 296` ```lemma (in equivalence) closure_of_eq: ``` ballarin@27701 ` 297` ``` "[| x .= x'; A \ carrier S; x \ closure_of A; x \ carrier S; x' \ carrier S |] ==> x' \ closure_of A" ``` ballarin@27701 ` 298` ``` unfolding eq_closure_of_def elem_def ``` ballarin@27701 ` 299` ``` by (blast intro: trans sym) ``` ballarin@27701 ` 300` ballarin@27701 ` 301` ```lemma (in equivalence) is_closed_eq [dest]: ``` ballarin@27701 ` 302` ``` "[| x .= x'; x \ A; is_closed A; x \ carrier S; x' \ carrier S |] ==> x' \ A" ``` ballarin@27701 ` 303` ``` unfolding eq_is_closed_def ``` ballarin@27701 ` 304` ``` using closure_of_eq [where A = A] ``` ballarin@27701 ` 305` ``` by simp ``` ballarin@27701 ` 306` ballarin@27701 ` 307` ```lemma (in equivalence) is_closed_eq_rev [dest]: ``` ballarin@27701 ` 308` ``` "[| x .= x'; x' \ A; is_closed A; x \ carrier S; x' \ carrier S |] ==> x \ A" ``` ballarin@27701 ` 309` ``` by (drule sym) (simp_all add: is_closed_eq) ``` ballarin@27701 ` 310` ballarin@27701 ` 311` ```lemma closure_of_closed [simp, intro]: ``` ballarin@27701 ` 312` ``` fixes S (structure) ``` ballarin@27701 ` 313` ``` shows "closure_of A \ carrier S" ``` ballarin@27701 ` 314` ```unfolding eq_closure_of_def ``` ballarin@27701 ` 315` ```by fast ``` ballarin@27701 ` 316` ballarin@27701 ` 317` ```lemma closure_of_memI: ``` ballarin@27701 ` 318` ``` fixes S (structure) ``` ballarin@27701 ` 319` ``` assumes "a .\ A" ``` ballarin@27701 ` 320` ``` and "a \ carrier S" ``` ballarin@27701 ` 321` ``` shows "a \ closure_of A" ``` ballarin@27701 ` 322` ```unfolding eq_closure_of_def ``` ballarin@27701 ` 323` ```using assms ``` ballarin@27701 ` 324` ```by fast ``` ballarin@27701 ` 325` ballarin@27701 ` 326` ```lemma closure_ofI2: ``` ballarin@27701 ` 327` ``` fixes S (structure) ``` ballarin@27701 ` 328` ``` assumes "a .= a'" ``` ballarin@27701 ` 329` ``` and "a' \ A" ``` ballarin@27701 ` 330` ``` and "a \ carrier S" ``` ballarin@27701 ` 331` ``` shows "a \ closure_of A" ``` ballarin@27701 ` 332` ```unfolding eq_closure_of_def elem_def ``` ballarin@27701 ` 333` ```using assms ``` ballarin@27701 ` 334` ```by fast ``` ballarin@27701 ` 335` ballarin@27701 ` 336` ```lemma closure_of_memE: ``` ballarin@27701 ` 337` ``` fixes S (structure) ``` ballarin@27701 ` 338` ``` assumes p: "a \ closure_of A" ``` ballarin@27701 ` 339` ``` and r: "\a \ carrier S; a .\ A\ \ P" ``` ballarin@27701 ` 340` ``` shows "P" ``` ballarin@27701 ` 341` ```proof - ``` ballarin@27701 ` 342` ``` from p ``` ballarin@27701 ` 343` ``` have acarr: "a \ carrier S" ``` ballarin@27701 ` 344` ``` and "a .\ A" ``` ballarin@27701 ` 345` ``` by (simp add: eq_closure_of_def)+ ``` ballarin@27701 ` 346` ``` thus "P" by (rule r) ``` ballarin@27701 ` 347` ```qed ``` ballarin@27701 ` 348` ballarin@27701 ` 349` ```lemma closure_ofE2: ``` ballarin@27701 ` 350` ``` fixes S (structure) ``` ballarin@27701 ` 351` ``` assumes p: "a \ closure_of A" ``` ballarin@27701 ` 352` ``` and r: "\a'. \a \ carrier S; a' \ A; a .= a'\ \ P" ``` ballarin@27701 ` 353` ``` shows "P" ``` ballarin@27701 ` 354` ```proof - ``` ballarin@27701 ` 355` ``` from p have acarr: "a \ carrier S" by (simp add: eq_closure_of_def) ``` ballarin@27701 ` 356` ballarin@27701 ` 357` ``` from p have "\a'\A. a .= a'" by (simp add: eq_closure_of_def elem_def) ``` ballarin@27701 ` 358` ``` from this obtain a' ``` ballarin@27701 ` 359` ``` where "a' \ A" and "a .= a'" by auto ``` ballarin@27701 ` 360` ballarin@27701 ` 361` ``` from acarr and this ``` ballarin@27701 ` 362` ``` show "P" by (rule r) ``` ballarin@27701 ` 363` ```qed ``` ballarin@27701 ` 364` ballarin@27701 ` 365` ```(* ``` ballarin@27701 ` 366` ```lemma (in equivalence) classes_consistent: ``` ballarin@27701 ` 367` ``` assumes Acarr: "A \ carrier S" ``` ballarin@27701 ` 368` ``` shows "is_closed (closure_of A)" ``` ballarin@27701 ` 369` ```apply (blast intro: elemI elim elemE) ``` ballarin@27701 ` 370` ```using assms ``` ballarin@27701 ` 371` ```apply (intro is_closedI closure_of_memI, simp) ``` ballarin@27701 ` 372` ``` apply (elim elemE closure_of_memE) ``` ballarin@27701 ` 373` ```proof - ``` ballarin@27701 ` 374` ``` fix x a' a'' ``` ballarin@27701 ` 375` ``` assume carr: "x \ carrier S" "a' \ carrier S" ``` ballarin@27701 ` 376` ``` assume a''A: "a'' \ A" ``` ballarin@27701 ` 377` ``` with Acarr have "a'' \ carrier S" by fast ``` ballarin@27701 ` 378` ``` note [simp] = carr this Acarr ``` ballarin@27701 ` 379` ballarin@27701 ` 380` ``` assume "x .= a'" ``` ballarin@27701 ` 381` ``` also assume "a' .= a''" ``` ballarin@27701 ` 382` ``` also from a''A ``` ballarin@27701 ` 383` ``` have "a'' .\ A" by (simp add: elem_exact) ``` ballarin@27701 ` 384` ``` finally show "x .\ A" by simp ``` ballarin@27701 ` 385` ```qed ``` ballarin@27701 ` 386` ```*) ``` ballarin@27701 ` 387` ```(* ``` ballarin@27701 ` 388` ```lemma (in equivalence) classes_small: ``` ballarin@27701 ` 389` ``` assumes "is_closed B" ``` ballarin@27701 ` 390` ``` and "A \ B" ``` ballarin@27701 ` 391` ``` shows "closure_of A \ B" ``` ballarin@27701 ` 392` ```using assms ``` ballarin@27701 ` 393` ```by (blast dest: is_closedD2 elem_subsetD elim: closure_of_memE) ``` ballarin@27701 ` 394` ballarin@27701 ` 395` ```lemma (in equivalence) classes_eq: ``` ballarin@27701 ` 396` ``` assumes "A \ carrier S" ``` ballarin@27701 ` 397` ``` shows "A {.=} closure_of A" ``` ballarin@27701 ` 398` ```using assms ``` ballarin@27701 ` 399` ```by (blast intro: set_eqI elem_exact closure_of_memI elim: closure_of_memE) ``` ballarin@27701 ` 400` ballarin@27701 ` 401` ```lemma (in equivalence) complete_classes: ``` ballarin@27701 ` 402` ``` assumes c: "is_closed A" ``` ballarin@27701 ` 403` ``` shows "A = closure_of A" ``` ballarin@27701 ` 404` ```using assms ``` ballarin@27701 ` 405` ```by (blast intro: closure_of_memI elem_exact dest: is_closedD1 is_closedD2 closure_of_memE) ``` ballarin@27701 ` 406` ```*) ``` ballarin@27701 ` 407` ballarin@27701 ` 408` ```end ```