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