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