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