modernized historic example;
authorwenzelm
Sun Dec 28 12:37:03 2014 +0100 (2014-12-28)
changeset 59192a1d6d6db781b
parent 59191 682aa538c5c0
child 59193 59f1591a11cb
modernized historic example;
src/HOL/Library/Quotient_Type.thy
     1.1 --- a/src/HOL/Library/Quotient_Type.thy	Sun Dec 28 12:18:01 2014 +0100
     1.2 +++ b/src/HOL/Library/Quotient_Type.thy	Sun Dec 28 12:37:03 2014 +0100
     1.3 @@ -2,63 +2,65 @@
     1.4      Author:     Markus Wenzel, TU Muenchen
     1.5  *)
     1.6  
     1.7 -section {* Quotient types *}
     1.8 +section \<open>Quotient types\<close>
     1.9  
    1.10  theory Quotient_Type
    1.11  imports Main
    1.12  begin
    1.13  
    1.14 -text {*
    1.15 - We introduce the notion of quotient types over equivalence relations
    1.16 - via type classes.
    1.17 -*}
    1.18 +text \<open>We introduce the notion of quotient types over equivalence relations
    1.19 +  via type classes.\<close>
    1.20 +
    1.21  
    1.22 -subsection {* Equivalence relations and quotient types *}
    1.23 +subsection \<open>Equivalence relations and quotient types\<close>
    1.24  
    1.25 -text {*
    1.26 - \medskip Type class @{text equiv} models equivalence relations @{text
    1.27 - "\<sim> :: 'a => 'a => bool"}.
    1.28 -*}
    1.29 +text \<open>Type class @{text equiv} models equivalence relations
    1.30 +  @{text "\<sim> :: 'a \<Rightarrow> 'a \<Rightarrow> bool"}.\<close>
    1.31  
    1.32  class eqv =
    1.33 -  fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool"    (infixl "\<sim>" 50)
    1.34 +  fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infixl "\<sim>" 50)
    1.35  
    1.36  class equiv = eqv +
    1.37    assumes equiv_refl [intro]: "x \<sim> x"
    1.38 -  assumes equiv_trans [trans]: "x \<sim> y \<Longrightarrow> y \<sim> z \<Longrightarrow> x \<sim> z"
    1.39 -  assumes equiv_sym [sym]: "x \<sim> y \<Longrightarrow> y \<sim> x"
    1.40 +    and equiv_trans [trans]: "x \<sim> y \<Longrightarrow> y \<sim> z \<Longrightarrow> x \<sim> z"
    1.41 +    and equiv_sym [sym]: "x \<sim> y \<Longrightarrow> y \<sim> x"
    1.42 +begin
    1.43  
    1.44 -lemma equiv_not_sym [sym]: "\<not> (x \<sim> y) ==> \<not> (y \<sim> (x::'a::equiv))"
    1.45 +lemma equiv_not_sym [sym]: "\<not> x \<sim> y \<Longrightarrow> \<not> y \<sim> x"
    1.46  proof -
    1.47 -  assume "\<not> (x \<sim> y)" then show "\<not> (y \<sim> x)"
    1.48 -    by (rule contrapos_nn) (rule equiv_sym)
    1.49 +  assume "\<not> x \<sim> y"
    1.50 +  then show "\<not> y \<sim> x" by (rule contrapos_nn) (rule equiv_sym)
    1.51  qed
    1.52  
    1.53 -lemma not_equiv_trans1 [trans]: "\<not> (x \<sim> y) ==> y \<sim> z ==> \<not> (x \<sim> (z::'a::equiv))"
    1.54 +lemma not_equiv_trans1 [trans]: "\<not> x \<sim> y \<Longrightarrow> y \<sim> z \<Longrightarrow> \<not> x \<sim> z"
    1.55  proof -
    1.56 -  assume "\<not> (x \<sim> y)" and "y \<sim> z"
    1.57 -  show "\<not> (x \<sim> z)"
    1.58 +  assume "\<not> x \<sim> y" and "y \<sim> z"
    1.59 +  show "\<not> x \<sim> z"
    1.60    proof
    1.61      assume "x \<sim> z"
    1.62 -    also from `y \<sim> z` have "z \<sim> y" ..
    1.63 +    also from \<open>y \<sim> z\<close> have "z \<sim> y" ..
    1.64      finally have "x \<sim> y" .
    1.65 -    with `\<not> (x \<sim> y)` show False by contradiction
    1.66 +    with \<open>\<not> x \<sim> y\<close> show False by contradiction
    1.67    qed
    1.68  qed
    1.69  
    1.70 -lemma not_equiv_trans2 [trans]: "x \<sim> y ==> \<not> (y \<sim> z) ==> \<not> (x \<sim> (z::'a::equiv))"
    1.71 +lemma not_equiv_trans2 [trans]: "x \<sim> y \<Longrightarrow> \<not> y \<sim> z \<Longrightarrow> \<not> x \<sim> z"
    1.72  proof -
    1.73 -  assume "\<not> (y \<sim> z)" then have "\<not> (z \<sim> y)" ..
    1.74 -  also assume "x \<sim> y" then have "y \<sim> x" ..
    1.75 -  finally have "\<not> (z \<sim> x)" . then show "(\<not> x \<sim> z)" ..
    1.76 +  assume "\<not> y \<sim> z"
    1.77 +  then have "\<not> z \<sim> y" ..
    1.78 +  also
    1.79 +  assume "x \<sim> y"
    1.80 +  then have "y \<sim> x" ..
    1.81 +  finally have "\<not> z \<sim> x" .
    1.82 +  then show "\<not> x \<sim> z" ..
    1.83  qed
    1.84  
    1.85 -text {*
    1.86 - \medskip The quotient type @{text "'a quot"} consists of all
    1.87 - \emph{equivalence classes} over elements of the base type @{typ 'a}.
    1.88 -*}
    1.89 +end
    1.90  
    1.91 -definition "quot = {{x. a \<sim> x} | a::'a::eqv. True}"
    1.92 +text \<open>The quotient type @{text "'a quot"} consists of all \emph{equivalence
    1.93 +  classes} over elements of the base type @{typ 'a}.\<close>
    1.94 +
    1.95 +definition (in eqv) "quot = {{x. a \<sim> x} | a. True}"
    1.96  
    1.97  typedef 'a quot = "quot :: 'a::eqv set set"
    1.98    unfolding quot_def by blast
    1.99 @@ -66,38 +68,38 @@
   1.100  lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
   1.101    unfolding quot_def by blast
   1.102  
   1.103 -lemma quotE [elim]: "R \<in> quot ==> (!!a. R = {x. a \<sim> x} ==> C) ==> C"
   1.104 -  unfolding quot_def by blast
   1.105 +lemma quotE [elim]:
   1.106 +  assumes "R \<in> quot"
   1.107 +  obtains a where "R = {x. a \<sim> x}"
   1.108 +  using assms unfolding quot_def by blast
   1.109  
   1.110 -text {*
   1.111 - \medskip Abstracted equivalence classes are the canonical
   1.112 - representation of elements of a quotient type.
   1.113 -*}
   1.114 +text \<open>Abstracted equivalence classes are the canonical representation of
   1.115 +  elements of a quotient type.\<close>
   1.116  
   1.117 -definition
   1.118 -  "class" :: "'a::equiv => 'a quot"  ("\<lfloor>_\<rfloor>") where
   1.119 -  "\<lfloor>a\<rfloor> = Abs_quot {x. a \<sim> x}"
   1.120 +definition "class" :: "'a::equiv \<Rightarrow> 'a quot"  ("\<lfloor>_\<rfloor>")
   1.121 +  where "\<lfloor>a\<rfloor> = Abs_quot {x. a \<sim> x}"
   1.122  
   1.123  theorem quot_exhaust: "\<exists>a. A = \<lfloor>a\<rfloor>"
   1.124  proof (cases A)
   1.125 -  fix R assume R: "A = Abs_quot R"
   1.126 -  assume "R \<in> quot" then have "\<exists>a. R = {x. a \<sim> x}" by blast
   1.127 +  fix R
   1.128 +  assume R: "A = Abs_quot R"
   1.129 +  assume "R \<in> quot"
   1.130 +  then have "\<exists>a. R = {x. a \<sim> x}" by blast
   1.131    with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast
   1.132    then show ?thesis unfolding class_def .
   1.133  qed
   1.134  
   1.135 -lemma quot_cases [cases type: quot]: "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C"
   1.136 +lemma quot_cases [cases type: quot]:
   1.137 +  obtains a where "A = \<lfloor>a\<rfloor>"
   1.138    using quot_exhaust by blast
   1.139  
   1.140  
   1.141 -subsection {* Equality on quotients *}
   1.142 +subsection \<open>Equality on quotients\<close>
   1.143  
   1.144 -text {*
   1.145 - Equality of canonical quotient elements coincides with the original
   1.146 - relation.
   1.147 -*}
   1.148 +text \<open>Equality of canonical quotient elements coincides with the original
   1.149 +  relation.\<close>
   1.150  
   1.151 -theorem quot_equality [iff?]: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)"
   1.152 +theorem quot_equality [iff?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> \<longleftrightarrow> a \<sim> b"
   1.153  proof
   1.154    assume eq: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"
   1.155    show "a \<sim> b"
   1.156 @@ -131,11 +133,10 @@
   1.157  qed
   1.158  
   1.159  
   1.160 -subsection {* Picking representing elements *}
   1.161 +subsection \<open>Picking representing elements\<close>
   1.162  
   1.163 -definition
   1.164 -  pick :: "'a::equiv quot => 'a" where
   1.165 -  "pick A = (SOME a. A = \<lfloor>a\<rfloor>)"
   1.166 +definition pick :: "'a::equiv quot \<Rightarrow> 'a"
   1.167 +  where "pick A = (SOME a. A = \<lfloor>a\<rfloor>)"
   1.168  
   1.169  theorem pick_equiv [intro]: "pick \<lfloor>a\<rfloor> \<sim> a"
   1.170  proof (unfold pick_def)
   1.171 @@ -143,7 +144,8 @@
   1.172    proof (rule someI2)
   1.173      show "\<lfloor>a\<rfloor> = \<lfloor>a\<rfloor>" ..
   1.174      fix x assume "\<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>"
   1.175 -    then have "a \<sim> x" .. then show "x \<sim> a" ..
   1.176 +    then have "a \<sim> x" ..
   1.177 +    then show "x \<sim> a" ..
   1.178    qed
   1.179  qed
   1.180  
   1.181 @@ -155,17 +157,14 @@
   1.182    with a show ?thesis by simp
   1.183  qed
   1.184  
   1.185 -text {*
   1.186 - \medskip The following rules support canonical function definitions
   1.187 - on quotient types (with up to two arguments).  Note that the
   1.188 - stripped-down version without additional conditions is sufficient
   1.189 - most of the time.
   1.190 -*}
   1.191 +text \<open>The following rules support canonical function definitions on quotient
   1.192 +  types (with up to two arguments). Note that the stripped-down version
   1.193 +  without additional conditions is sufficient most of the time.\<close>
   1.194  
   1.195  theorem quot_cond_function:
   1.196 -  assumes eq: "!!X Y. P X Y ==> f X Y == g (pick X) (pick Y)"
   1.197 -    and cong: "!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor>
   1.198 -      ==> P \<lfloor>x\<rfloor> \<lfloor>y\<rfloor> ==> P \<lfloor>x'\<rfloor> \<lfloor>y'\<rfloor> ==> g x y = g x' y'"
   1.199 +  assumes eq: "\<And>X Y. P X Y \<Longrightarrow> f X Y \<equiv> g (pick X) (pick Y)"
   1.200 +    and cong: "\<And>x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> \<Longrightarrow> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor>
   1.201 +      \<Longrightarrow> P \<lfloor>x\<rfloor> \<lfloor>y\<rfloor> \<Longrightarrow> P \<lfloor>x'\<rfloor> \<lfloor>y'\<rfloor> \<Longrightarrow> g x y = g x' y'"
   1.202      and P: "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>"
   1.203    shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
   1.204  proof -
   1.205 @@ -183,15 +182,15 @@
   1.206  qed
   1.207  
   1.208  theorem quot_function:
   1.209 -  assumes "!!X Y. f X Y == g (pick X) (pick Y)"
   1.210 -    and "!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> g x y = g x' y'"
   1.211 +  assumes "\<And>X Y. f X Y \<equiv> g (pick X) (pick Y)"
   1.212 +    and "\<And>x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> \<Longrightarrow> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> \<Longrightarrow> g x y = g x' y'"
   1.213    shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
   1.214    using assms and TrueI
   1.215    by (rule quot_cond_function)
   1.216  
   1.217  theorem quot_function':
   1.218 -  "(!!X Y. f X Y == g (pick X) (pick Y)) ==>
   1.219 -    (!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> g x y = g x' y') ==>
   1.220 +  "(\<And>X Y. f X Y \<equiv> g (pick X) (pick Y)) \<Longrightarrow>
   1.221 +    (\<And>x x' y y'. x \<sim> x' \<Longrightarrow> y \<sim> y' \<Longrightarrow> g x y = g x' y') \<Longrightarrow>
   1.222      f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
   1.223    by (rule quot_function) (simp_all only: quot_equality)
   1.224