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