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 
```
```   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
```