src/HOL/Equiv_Relations.thy
author paulson
Fri, 19 Nov 2004 17:31:49 +0100
changeset 15300 7dd5853a4812
child 15302 a643fcbc3468
permissions -rw-r--r--
moved and renamed Integ/Equiv.thy
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15300
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
     1
(*  ID:         $Id$
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
     2
    Authors:    Lawrence C Paulson, Cambridge University Computer Laboratory
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
     3
    Copyright   1996  University of Cambridge
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
     4
*)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
     5
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
     6
header {* Equivalence Relations in Higher-Order Set Theory *}
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
     7
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
     8
theory Equiv_Relations
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
     9
imports Relation Finite_Set
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    10
begin
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    11
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    12
subsection {* Equivalence relations *}
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    13
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    14
locale equiv =
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    15
  fixes A and r
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    16
  assumes refl: "refl A r"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    17
    and sym: "sym r"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    18
    and trans: "trans r"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    19
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    20
text {*
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    21
  Suppes, Theorem 70: @{text r} is an equiv relation iff @{text "r\<inverse> O
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    22
  r = r"}.
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    23
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    24
  First half: @{text "equiv A r ==> r\<inverse> O r = r"}.
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    25
*}
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    26
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    27
lemma sym_trans_comp_subset:
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    28
    "sym r ==> trans r ==> r\<inverse> O r \<subseteq> r"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    29
  by (unfold trans_def sym_def converse_def) blast
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    30
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    31
lemma refl_comp_subset: "refl A r ==> r \<subseteq> r\<inverse> O r"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    32
  by (unfold refl_def) blast
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    33
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    34
lemma equiv_comp_eq: "equiv A r ==> r\<inverse> O r = r"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    35
  apply (unfold equiv_def)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    36
  apply clarify
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    37
  apply (rule equalityI)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    38
   apply (rules intro: sym_trans_comp_subset refl_comp_subset)+
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    39
  done
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    40
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    41
text {* Second half. *}
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    42
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    43
lemma comp_equivI:
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    44
    "r\<inverse> O r = r ==> Domain r = A ==> equiv A r"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    45
  apply (unfold equiv_def refl_def sym_def trans_def)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    46
  apply (erule equalityE)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    47
  apply (subgoal_tac "\<forall>x y. (x, y) \<in> r --> (y, x) \<in> r")
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    48
   apply fast
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    49
  apply fast
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    50
  done
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    51
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    52
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    53
subsection {* Equivalence classes *}
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    54
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    55
lemma equiv_class_subset:
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    56
  "equiv A r ==> (a, b) \<in> r ==> r``{a} \<subseteq> r``{b}"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    57
  -- {* lemma for the next result *}
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    58
  by (unfold equiv_def trans_def sym_def) blast
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    59
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    60
theorem equiv_class_eq: "equiv A r ==> (a, b) \<in> r ==> r``{a} = r``{b}"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    61
  apply (assumption | rule equalityI equiv_class_subset)+
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    62
  apply (unfold equiv_def sym_def)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    63
  apply blast
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    64
  done
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    65
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    66
lemma equiv_class_self: "equiv A r ==> a \<in> A ==> a \<in> r``{a}"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    67
  by (unfold equiv_def refl_def) blast
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    68
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    69
lemma subset_equiv_class:
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    70
    "equiv A r ==> r``{b} \<subseteq> r``{a} ==> b \<in> A ==> (a,b) \<in> r"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    71
  -- {* lemma for the next result *}
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    72
  by (unfold equiv_def refl_def) blast
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    73
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    74
lemma eq_equiv_class:
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    75
    "r``{a} = r``{b} ==> equiv A r ==> b \<in> A ==> (a, b) \<in> r"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    76
  by (rules intro: equalityD2 subset_equiv_class)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    77
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    78
lemma equiv_class_nondisjoint:
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    79
    "equiv A r ==> x \<in> (r``{a} \<inter> r``{b}) ==> (a, b) \<in> r"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    80
  by (unfold equiv_def trans_def sym_def) blast
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    81
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    82
lemma equiv_type: "equiv A r ==> r \<subseteq> A \<times> A"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    83
  by (unfold equiv_def refl_def) blast
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    84
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    85
theorem equiv_class_eq_iff:
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    86
  "equiv A r ==> ((x, y) \<in> r) = (r``{x} = r``{y} & x \<in> A & y \<in> A)"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    87
  by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    88
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    89
theorem eq_equiv_class_iff:
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    90
  "equiv A r ==> x \<in> A ==> y \<in> A ==> (r``{x} = r``{y}) = ((x, y) \<in> r)"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    91
  by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    92
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    93
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    94
subsection {* Quotients *}
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    95
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    96
constdefs
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    97
  quotient :: "['a set, ('a*'a) set] => 'a set set"  (infixl "'/'/" 90)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    98
  "A//r == \<Union>x \<in> A. {r``{x}}"  -- {* set of equiv classes *}
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
    99
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   100
lemma quotientI: "x \<in> A ==> r``{x} \<in> A//r"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   101
  by (unfold quotient_def) blast
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   102
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   103
lemma quotientE:
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   104
  "X \<in> A//r ==> (!!x. X = r``{x} ==> x \<in> A ==> P) ==> P"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   105
  by (unfold quotient_def) blast
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   106
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   107
lemma Union_quotient: "equiv A r ==> Union (A//r) = A"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   108
  by (unfold equiv_def refl_def quotient_def) blast
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   109
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   110
lemma quotient_disj:
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   111
  "equiv A r ==> X \<in> A//r ==> Y \<in> A//r ==> X = Y | (X \<inter> Y = {})"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   112
  apply (unfold quotient_def)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   113
  apply clarify
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   114
  apply (rule equiv_class_eq)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   115
   apply assumption
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   116
  apply (unfold equiv_def trans_def sym_def)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   117
  apply blast
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   118
  done
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   119
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   120
lemma quotient_eqI:
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   121
  "[|equiv A r; X \<in> A//r; Y \<in> A//r; x \<in> X; y \<in> Y; (x,y) \<in> r|] ==> X = Y" 
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   122
  apply (clarify elim!: quotientE)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   123
  apply (rule equiv_class_eq, assumption)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   124
  apply (unfold equiv_def sym_def trans_def, blast)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   125
  done
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   126
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   127
lemma quotient_eq_iff:
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   128
  "[|equiv A r; X \<in> A//r; Y \<in> A//r; x \<in> X; y \<in> Y|] ==> (X = Y) = ((x,y) \<in> r)" 
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   129
  apply (rule iffI)  
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   130
   prefer 2 apply (blast del: equalityI intro: quotient_eqI) 
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   131
  apply (clarify elim!: quotientE)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   132
  apply (unfold equiv_def sym_def trans_def, blast)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   133
  done
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   134
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   135
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   136
lemma quotient_empty [simp]: "{}//r = {}"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   137
by(simp add: quotient_def)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   138
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   139
lemma quotient_is_empty [iff]: "(A//r = {}) = (A = {})"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   140
by(simp add: quotient_def)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   141
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   142
lemma quotient_is_empty2 [iff]: "({} = A//r) = (A = {})"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   143
by(simp add: quotient_def)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   144
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   145
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   146
subsection {* Defining unary operations upon equivalence classes *}
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   147
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   148
text{*A congruence-preserving function*}
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   149
locale congruent =
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   150
  fixes r and f
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   151
  assumes congruent: "(y,z) \<in> r ==> f y = f z"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   152
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   153
syntax
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   154
  RESPECTS ::"['a => 'b, ('a * 'a) set] => bool"  (infixr "respects" 80)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   155
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   156
translations
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   157
  "f respects r" == "congruent r f"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   158
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   159
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   160
lemma UN_constant_eq: "a \<in> A ==> \<forall>y \<in> A. f y = c ==> (\<Union>y \<in> A. f(y))=c"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   161
  -- {* lemma required to prove @{text UN_equiv_class} *}
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   162
  by auto
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   163
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   164
lemma UN_equiv_class:
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   165
  "equiv A r ==> f respects r ==> a \<in> A
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   166
    ==> (\<Union>x \<in> r``{a}. f x) = f a"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   167
  -- {* Conversion rule *}
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   168
  apply (rule equiv_class_self [THEN UN_constant_eq], assumption+)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   169
  apply (unfold equiv_def congruent_def sym_def)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   170
  apply (blast del: equalityI)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   171
  done
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   172
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   173
lemma UN_equiv_class_type:
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   174
  "equiv A r ==> f respects r ==> X \<in> A//r ==>
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   175
    (!!x. x \<in> A ==> f x \<in> B) ==> (\<Union>x \<in> X. f x) \<in> B"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   176
  apply (unfold quotient_def)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   177
  apply clarify
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   178
  apply (subst UN_equiv_class)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   179
     apply auto
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   180
  done
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   181
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   182
text {*
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   183
  Sufficient conditions for injectiveness.  Could weaken premises!
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   184
  major premise could be an inclusion; bcong could be @{text "!!y. y \<in>
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   185
  A ==> f y \<in> B"}.
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   186
*}
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   187
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   188
lemma UN_equiv_class_inject:
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   189
  "equiv A r ==> f respects r ==>
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   190
    (\<Union>x \<in> X. f x) = (\<Union>y \<in> Y. f y) ==> X \<in> A//r ==> Y \<in> A//r
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   191
    ==> (!!x y. x \<in> A ==> y \<in> A ==> f x = f y ==> (x, y) \<in> r)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   192
    ==> X = Y"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   193
  apply (unfold quotient_def)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   194
  apply clarify
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   195
  apply (rule equiv_class_eq)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   196
   apply assumption
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   197
  apply (subgoal_tac "f x = f xa")
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   198
   apply blast
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   199
  apply (erule box_equals)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   200
   apply (assumption | rule UN_equiv_class)+
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   201
  done
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   202
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   203
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   204
subsection {* Defining binary operations upon equivalence classes *}
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   205
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   206
text{*A congruence-preserving function of two arguments*}
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   207
locale congruent2 =
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   208
  fixes r1 and r2 and f
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   209
  assumes congruent2:
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   210
    "(y1,z1) \<in> r1 ==> (y2,z2) \<in> r2 ==> f y1 y2 = f z1 z2"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   211
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   212
text{*Abbreviation for the common case where the relations are identical*}
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   213
syntax
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   214
  RESPECTS2 ::"['a => 'b, ('a * 'a) set] => bool"  (infixr "respects2 " 80)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   215
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   216
translations
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   217
  "f respects2 r" => "congruent2 r r f"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   218
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   219
lemma congruent2_implies_congruent:
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   220
    "equiv A r1 ==> congruent2 r1 r2 f ==> a \<in> A ==> congruent r2 (f a)"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   221
  by (unfold congruent_def congruent2_def equiv_def refl_def) blast
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   222
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   223
lemma congruent2_implies_congruent_UN:
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   224
  "equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f ==> a \<in> A2 ==>
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   225
    congruent r1 (\<lambda>x1. \<Union>x2 \<in> r2``{a}. f x1 x2)"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   226
  apply (unfold congruent_def)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   227
  apply clarify
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   228
  apply (rule equiv_type [THEN subsetD, THEN SigmaE2], assumption+)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   229
  apply (simp add: UN_equiv_class congruent2_implies_congruent)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   230
  apply (unfold congruent2_def equiv_def refl_def)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   231
  apply (blast del: equalityI)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   232
  done
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   233
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   234
lemma UN_equiv_class2:
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   235
  "equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f ==> a1 \<in> A1 ==> a2 \<in> A2
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   236
    ==> (\<Union>x1 \<in> r1``{a1}. \<Union>x2 \<in> r2``{a2}. f x1 x2) = f a1 a2"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   237
  by (simp add: UN_equiv_class congruent2_implies_congruent
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   238
    congruent2_implies_congruent_UN)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   239
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   240
lemma UN_equiv_class_type2:
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   241
  "equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   242
    ==> X1 \<in> A1//r1 ==> X2 \<in> A2//r2
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   243
    ==> (!!x1 x2. x1 \<in> A1 ==> x2 \<in> A2 ==> f x1 x2 \<in> B)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   244
    ==> (\<Union>x1 \<in> X1. \<Union>x2 \<in> X2. f x1 x2) \<in> B"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   245
  apply (unfold quotient_def)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   246
  apply clarify
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   247
  apply (blast intro: UN_equiv_class_type congruent2_implies_congruent_UN
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   248
    congruent2_implies_congruent quotientI)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   249
  done
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   250
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   251
lemma UN_UN_split_split_eq:
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   252
  "(\<Union>(x1, x2) \<in> X. \<Union>(y1, y2) \<in> Y. A x1 x2 y1 y2) =
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   253
    (\<Union>x \<in> X. \<Union>y \<in> Y. (\<lambda>(x1, x2). (\<lambda>(y1, y2). A x1 x2 y1 y2) y) x)"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   254
  -- {* Allows a natural expression of binary operators, *}
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   255
  -- {* without explicit calls to @{text split} *}
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   256
  by auto
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   257
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   258
lemma congruent2I:
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   259
  "equiv A1 r1 ==> equiv A2 r2
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   260
    ==> (!!y z w. w \<in> A2 ==> (y,z) \<in> r1 ==> f y w = f z w)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   261
    ==> (!!y z w. w \<in> A1 ==> (y,z) \<in> r2 ==> f w y = f w z)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   262
    ==> congruent2 r1 r2 f"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   263
  -- {* Suggested by John Harrison -- the two subproofs may be *}
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   264
  -- {* \emph{much} simpler than the direct proof. *}
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   265
  apply (unfold congruent2_def equiv_def refl_def)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   266
  apply clarify
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   267
  apply (blast intro: trans)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   268
  done
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   269
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   270
lemma congruent2_commuteI:
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   271
  assumes equivA: "equiv A r"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   272
    and commute: "!!y z. y \<in> A ==> z \<in> A ==> f y z = f z y"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   273
    and congt: "!!y z w. w \<in> A ==> (y,z) \<in> r ==> f w y = f w z"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   274
  shows "f respects2 r"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   275
  apply (rule congruent2I [OF equivA equivA])
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   276
   apply (rule commute [THEN trans])
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   277
     apply (rule_tac [3] commute [THEN trans, symmetric])
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   278
       apply (rule_tac [5] sym)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   279
       apply (assumption | rule congt |
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   280
         erule equivA [THEN equiv_type, THEN subsetD, THEN SigmaE2])+
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   281
  done
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   282
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   283
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   284
subsection {* Cardinality results *}
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   285
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   286
text {*Suggested by Florian Kammüller*}
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   287
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   288
lemma finite_quotient: "finite A ==> r \<subseteq> A \<times> A ==> finite (A//r)"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   289
  -- {* recall @{thm equiv_type} *}
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   290
  apply (rule finite_subset)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   291
   apply (erule_tac [2] finite_Pow_iff [THEN iffD2])
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   292
  apply (unfold quotient_def)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   293
  apply blast
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   294
  done
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   295
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   296
lemma finite_equiv_class:
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   297
  "finite A ==> r \<subseteq> A \<times> A ==> X \<in> A//r ==> finite X"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   298
  apply (unfold quotient_def)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   299
  apply (rule finite_subset)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   300
   prefer 2 apply assumption
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   301
  apply blast
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   302
  done
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   303
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   304
lemma equiv_imp_dvd_card:
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   305
  "finite A ==> equiv A r ==> \<forall>X \<in> A//r. k dvd card X
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   306
    ==> k dvd card A"
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   307
  apply (rule Union_quotient [THEN subst])
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   308
   apply assumption
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   309
  apply (rule dvd_partition)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   310
     prefer 4 apply (blast dest: quotient_disj)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   311
    apply (simp_all add: Union_quotient equiv_type finite_quotient)
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   312
  done
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   313
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   314
ML
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   315
{*
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   316
val UN_UN_split_split_eq = thm "UN_UN_split_split_eq";
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   317
val UN_constant_eq = thm "UN_constant_eq";
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   318
val UN_equiv_class = thm "UN_equiv_class";
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   319
val UN_equiv_class2 = thm "UN_equiv_class2";
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   320
val UN_equiv_class_inject = thm "UN_equiv_class_inject";
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   321
val UN_equiv_class_type = thm "UN_equiv_class_type";
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   322
val UN_equiv_class_type2 = thm "UN_equiv_class_type2";
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   323
val Union_quotient = thm "Union_quotient";
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   324
val comp_equivI = thm "comp_equivI";
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   325
val congruent2I = thm "congruent2I";
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   326
val congruent2_commuteI = thm "congruent2_commuteI";
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   327
val congruent2_def = thm "congruent2_def";
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   328
val congruent2_implies_congruent = thm "congruent2_implies_congruent";
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   329
val congruent2_implies_congruent_UN = thm "congruent2_implies_congruent_UN";
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   330
val congruent_def = thm "congruent_def";
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   331
val eq_equiv_class = thm "eq_equiv_class";
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   332
val eq_equiv_class_iff = thm "eq_equiv_class_iff";
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   333
val equiv_class_eq = thm "equiv_class_eq";
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   334
val equiv_class_eq_iff = thm "equiv_class_eq_iff";
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   335
val equiv_class_nondisjoint = thm "equiv_class_nondisjoint";
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   336
val equiv_class_self = thm "equiv_class_self";
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   337
val equiv_comp_eq = thm "equiv_comp_eq";
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   338
val equiv_def = thm "equiv_def";
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   339
val equiv_imp_dvd_card = thm "equiv_imp_dvd_card";
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   340
val equiv_type = thm "equiv_type";
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   341
val finite_equiv_class = thm "finite_equiv_class";
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   342
val finite_quotient = thm "finite_quotient";
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   343
val quotientE = thm "quotientE";
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   344
val quotientI = thm "quotientI";
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   345
val quotient_def = thm "quotient_def";
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   346
val quotient_disj = thm "quotient_disj";
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   347
val refl_comp_subset = thm "refl_comp_subset";
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   348
val subset_equiv_class = thm "subset_equiv_class";
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   349
val sym_trans_comp_subset = thm "sym_trans_comp_subset";
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   350
*}
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   351
7dd5853a4812 moved and renamed Integ/Equiv.thy
paulson
parents:
diff changeset
   352
end