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