src/HOL/Codatatype/Equiv_Relations_More.thy
author blanchet
Mon Sep 17 21:33:12 2012 +0200 (2012-09-17)
changeset 49430 6df729c6a1a6
parent 48975 7f79f94a432c
child 49509 163914705f8d
permissions -rw-r--r--
tuned simpset
blanchet@48975
     1
(*  Title:      HOL/Codatatype/Equiv_Relations_More.thy
blanchet@48975
     2
    Author:     Andrei Popescu, TU Muenchen
blanchet@48975
     3
    Copyright   2012
blanchet@48975
     4
blanchet@48975
     5
Some preliminaries on equivalence relations and quotients.
blanchet@48975
     6
*)
blanchet@48975
     7
blanchet@48975
     8
header {* Some Preliminaries on Equivalence Relations and Quotients *}
blanchet@48975
     9
blanchet@48975
    10
theory Equiv_Relations_More
blanchet@48975
    11
imports Equiv_Relations Hilbert_Choice
blanchet@48975
    12
begin
blanchet@48975
    13
blanchet@48975
    14
blanchet@48975
    15
(* Recall the following constants and lemmas:
blanchet@48975
    16
blanchet@48975
    17
term Eps
blanchet@48975
    18
term "A//r"
blanchet@48975
    19
lemmas equiv_def
blanchet@48975
    20
lemmas refl_on_def
blanchet@48975
    21
 -- note that "reflexivity on" also assumes inclusion of the relation's field into r
blanchet@48975
    22
blanchet@48975
    23
*)
blanchet@48975
    24
blanchet@48975
    25
definition proj where "proj r x = r `` {x}"
blanchet@48975
    26
blanchet@48975
    27
definition univ where "univ f X == f (Eps (%x. x \<in> X))"
blanchet@48975
    28
blanchet@48975
    29
lemma proj_preserves:
blanchet@48975
    30
"x \<in> A \<Longrightarrow> proj r x \<in> A//r"
blanchet@48975
    31
unfolding proj_def by (rule quotientI)
blanchet@48975
    32
blanchet@48975
    33
lemma proj_in_iff:
blanchet@48975
    34
assumes "equiv A r"
blanchet@48975
    35
shows "(proj r x \<in> A//r) = (x \<in> A)"
blanchet@48975
    36
apply(rule iffI, auto simp add: proj_preserves)
blanchet@48975
    37
unfolding proj_def quotient_def proof clarsimp
blanchet@48975
    38
  fix y assume y: "y \<in> A" and "r `` {x} = r `` {y}"
blanchet@48975
    39
  moreover have "y \<in> r `` {y}" using assms y unfolding equiv_def refl_on_def by blast
blanchet@48975
    40
  ultimately have "(x,y) \<in> r" by blast
blanchet@48975
    41
  thus "x \<in> A" using assms unfolding equiv_def refl_on_def by blast
blanchet@48975
    42
qed
blanchet@48975
    43
blanchet@48975
    44
lemma proj_iff:
blanchet@48975
    45
"\<lbrakk>equiv A r; {x,y} \<subseteq> A\<rbrakk> \<Longrightarrow> (proj r x = proj r y) = ((x,y) \<in> r)"
blanchet@48975
    46
by (simp add: proj_def eq_equiv_class_iff)
blanchet@48975
    47
blanchet@48975
    48
(*
blanchet@48975
    49
lemma in_proj: "\<lbrakk>equiv A r; x \<in> A\<rbrakk> \<Longrightarrow> x \<in> proj r x"
blanchet@48975
    50
unfolding proj_def equiv_def refl_on_def by blast
blanchet@48975
    51
*)
blanchet@48975
    52
blanchet@48975
    53
lemma proj_image: "(proj r) ` A = A//r"
blanchet@48975
    54
unfolding proj_def[abs_def] quotient_def by blast
blanchet@48975
    55
blanchet@48975
    56
lemma in_quotient_imp_non_empty:
blanchet@48975
    57
"\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> X \<noteq> {}"
blanchet@48975
    58
unfolding quotient_def using equiv_class_self by fast
blanchet@48975
    59
blanchet@48975
    60
lemma in_quotient_imp_in_rel:
blanchet@48975
    61
"\<lbrakk>equiv A r; X \<in> A//r; {x,y} \<subseteq> X\<rbrakk> \<Longrightarrow> (x,y) \<in> r"
blanchet@48975
    62
using quotient_eq_iff by fastforce
blanchet@48975
    63
blanchet@48975
    64
lemma in_quotient_imp_closed:
blanchet@48975
    65
"\<lbrakk>equiv A r; X \<in> A//r; x \<in> X; (x,y) \<in> r\<rbrakk> \<Longrightarrow> y \<in> X"
blanchet@48975
    66
unfolding quotient_def equiv_def trans_def by blast
blanchet@48975
    67
blanchet@48975
    68
lemma in_quotient_imp_subset:
blanchet@48975
    69
"\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> X \<subseteq> A"
blanchet@48975
    70
using assms in_quotient_imp_in_rel equiv_type by fastforce
blanchet@48975
    71
blanchet@48975
    72
lemma equiv_Eps_in:
blanchet@48975
    73
"\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> Eps (%x. x \<in> X) \<in> X"
blanchet@48975
    74
apply (rule someI2_ex)
blanchet@48975
    75
using in_quotient_imp_non_empty by blast
blanchet@48975
    76
blanchet@48975
    77
lemma equiv_Eps_preserves:
blanchet@48975
    78
assumes ECH: "equiv A r" and X: "X \<in> A//r"
blanchet@48975
    79
shows "Eps (%x. x \<in> X) \<in> A"
blanchet@48975
    80
apply (rule in_mono[rule_format])
blanchet@48975
    81
 using assms apply (rule in_quotient_imp_subset)
blanchet@48975
    82
by (rule equiv_Eps_in) (rule assms)+
blanchet@48975
    83
blanchet@48975
    84
lemma proj_Eps:
blanchet@48975
    85
assumes "equiv A r" and "X \<in> A//r"
blanchet@48975
    86
shows "proj r (Eps (%x. x \<in> X)) = X"
blanchet@48975
    87
unfolding proj_def proof auto
blanchet@48975
    88
  fix x assume x: "x \<in> X"
blanchet@48975
    89
  thus "(Eps (%x. x \<in> X), x) \<in> r" using assms equiv_Eps_in in_quotient_imp_in_rel by fast
blanchet@48975
    90
next
blanchet@48975
    91
  fix x assume "(Eps (%x. x \<in> X),x) \<in> r"
blanchet@48975
    92
  thus "x \<in> X" using in_quotient_imp_closed[OF assms equiv_Eps_in[OF assms]] by fast
blanchet@48975
    93
qed
blanchet@48975
    94
blanchet@48975
    95
(*
blanchet@48975
    96
lemma Eps_proj:
blanchet@48975
    97
assumes "equiv A r" and "x \<in> A"
blanchet@48975
    98
shows "(Eps (%y. y \<in> proj r x), x) \<in> r"
blanchet@48975
    99
proof-
blanchet@48975
   100
  have 1: "proj r x \<in> A//r" using assms proj_preserves by fastforce
blanchet@48975
   101
  hence "Eps(%y. y \<in> proj r x) \<in> proj r x" using assms equiv_Eps_in by auto
blanchet@48975
   102
  moreover have "x \<in> proj r x" using assms in_proj by fastforce
blanchet@48975
   103
  ultimately show ?thesis using assms 1 in_quotient_imp_in_rel by fastforce
blanchet@48975
   104
qed
blanchet@48975
   105
blanchet@48975
   106
lemma equiv_Eps_iff:
blanchet@48975
   107
assumes "equiv A r" and "{X,Y} \<subseteq> A//r"
blanchet@48975
   108
shows "((Eps (%x. x \<in> X),Eps (%y. y \<in> Y)) \<in> r) = (X = Y)"
blanchet@48975
   109
proof-
blanchet@48975
   110
  have "Eps (%x. x \<in> X) \<in> X \<and> Eps (%y. y \<in> Y) \<in> Y" using assms equiv_Eps_in by auto
blanchet@48975
   111
  thus ?thesis using assms quotient_eq_iff by fastforce
blanchet@48975
   112
qed
blanchet@48975
   113
blanchet@48975
   114
lemma equiv_Eps_inj_on:
blanchet@48975
   115
assumes "equiv A r"
blanchet@48975
   116
shows "inj_on (%X. Eps (%x. x \<in> X)) (A//r)"
blanchet@48975
   117
unfolding inj_on_def proof clarify
blanchet@48975
   118
  fix X Y assume X: "X \<in> A//r" and Y: "Y \<in> A//r" and Eps: "Eps (%x. x \<in> X) = Eps (%y. y \<in> Y)"
blanchet@48975
   119
  hence "Eps (%x. x \<in> X) \<in> A" using assms equiv_Eps_preserves by auto
blanchet@48975
   120
  hence "(Eps (%x. x \<in> X), Eps (%y. y \<in> Y)) \<in> r"
blanchet@48975
   121
  using assms Eps unfolding quotient_def equiv_def refl_on_def by auto
blanchet@48975
   122
  thus "X= Y" using X Y assms equiv_Eps_iff by auto
blanchet@48975
   123
qed
blanchet@48975
   124
*)
blanchet@48975
   125
blanchet@48975
   126
lemma univ_commute:
blanchet@48975
   127
assumes ECH: "equiv A r" and RES: "f respects r" and x: "x \<in> A"
blanchet@48975
   128
shows "(univ f) (proj r x) = f x"
blanchet@48975
   129
unfolding univ_def proof -
blanchet@48975
   130
  have prj: "proj r x \<in> A//r" using x proj_preserves by fast
blanchet@48975
   131
  hence "Eps (%y. y \<in> proj r x) \<in> A" using ECH equiv_Eps_preserves by fast
blanchet@48975
   132
  moreover have "proj r (Eps (%y. y \<in> proj r x)) = proj r x" using ECH prj proj_Eps by fast
blanchet@48975
   133
  ultimately have "(x, Eps (%y. y \<in> proj r x)) \<in> r" using x ECH proj_iff by fast
blanchet@48975
   134
  thus "f (Eps (%y. y \<in> proj r x)) = f x" using RES unfolding congruent_def by fastforce
blanchet@48975
   135
qed
blanchet@48975
   136
blanchet@48975
   137
(*
blanchet@48975
   138
lemma univ_unique:
blanchet@48975
   139
assumes ECH: "equiv A r" and
blanchet@48975
   140
        RES: "f respects r" and  COM: "\<forall> x \<in> A. G (proj r x) = f x"
blanchet@48975
   141
shows "\<forall> X \<in> A//r. G X = univ f X"
blanchet@48975
   142
proof
blanchet@48975
   143
  fix X assume "X \<in> A//r"
blanchet@48975
   144
  then obtain x where x: "x \<in> A" and X: "X = proj r x" using ECH proj_image[of r A] by blast
blanchet@48975
   145
  have "G X = f x" unfolding X using x COM by simp
blanchet@48975
   146
  thus "G X = univ f X" unfolding X using ECH RES x univ_commute by fastforce
blanchet@48975
   147
qed
blanchet@48975
   148
*)
blanchet@48975
   149
blanchet@48975
   150
lemma univ_preserves:
blanchet@48975
   151
assumes ECH: "equiv A r" and RES: "f respects r" and
blanchet@48975
   152
        PRES: "\<forall> x \<in> A. f x \<in> B"
blanchet@48975
   153
shows "\<forall> X \<in> A//r. univ f X \<in> B"
blanchet@48975
   154
proof
blanchet@48975
   155
  fix X assume "X \<in> A//r"
blanchet@48975
   156
  then obtain x where x: "x \<in> A" and X: "X = proj r x" using ECH proj_image[of r A] by blast
blanchet@48975
   157
  hence "univ f X = f x" using assms univ_commute by fastforce
blanchet@48975
   158
  thus "univ f X \<in> B" using x PRES by simp
blanchet@48975
   159
qed
blanchet@48975
   160
blanchet@48975
   161
end