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