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