src/HOL/Library/Quotient_Type.thy
 changeset 59192 a1d6d6db781b parent 58881 b9556a055632 child 61260 e6f03fae14d5
equal inserted replaced
59191:682aa538c5c0 59192:a1d6d6db781b
     1 (*  Title:      HOL/Library/Quotient_Type.thy
     1 (*  Title:      HOL/Library/Quotient_Type.thy
     2     Author:     Markus Wenzel, TU Muenchen
     2     Author:     Markus Wenzel, TU Muenchen
     3 *)
     3 *)
     4
     4
     5 section {* Quotient types *}
     5 section \<open>Quotient types\<close>
     6
     6
     7 theory Quotient_Type
     7 theory Quotient_Type
     8 imports Main
     8 imports Main
     9 begin
     9 begin
    10
    10
    11 text {*
    11 text \<open>We introduce the notion of quotient types over equivalence relations
    12  We introduce the notion of quotient types over equivalence relations
    12   via type classes.\<close>
    13  via type classes.

    14 *}

    15
    13
    17
    14
    18 text {*
    15 subsection \<open>Equivalence relations and quotient types\<close>
    19  \medskip Type class @{text equiv} models equivalence relations @{text
    16
    20  "\<sim> :: 'a => 'a => bool"}.
    17 text \<open>Type class @{text equiv} models equivalence relations
    21 *}
    18   @{text "\<sim> :: 'a \<Rightarrow> 'a \<Rightarrow> bool"}.\<close>
    22
    19
    23 class eqv =
    20 class eqv =
    24   fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool"    (infixl "\<sim>" 50)
    21   fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infixl "\<sim>" 50)
    25
    22
    26 class equiv = eqv +
    23 class equiv = eqv +
    27   assumes equiv_refl [intro]: "x \<sim> x"
    24   assumes equiv_refl [intro]: "x \<sim> x"
    28   assumes equiv_trans [trans]: "x \<sim> y \<Longrightarrow> y \<sim> z \<Longrightarrow> x \<sim> z"
    25     and equiv_trans [trans]: "x \<sim> y \<Longrightarrow> y \<sim> z \<Longrightarrow> x \<sim> z"
    29   assumes equiv_sym [sym]: "x \<sim> y \<Longrightarrow> y \<sim> x"
    26     and equiv_sym [sym]: "x \<sim> y \<Longrightarrow> y \<sim> x"

    27 begin
    30
    28
    31 lemma equiv_not_sym [sym]: "\<not> (x \<sim> y) ==> \<not> (y \<sim> (x::'a::equiv))"
    29 lemma equiv_not_sym [sym]: "\<not> x \<sim> y \<Longrightarrow> \<not> y \<sim> x"
    32 proof -
    30 proof -
    33   assume "\<not> (x \<sim> y)" then show "\<not> (y \<sim> x)"
    31   assume "\<not> x \<sim> y"
    34     by (rule contrapos_nn) (rule equiv_sym)
    32   then show "\<not> y \<sim> x" by (rule contrapos_nn) (rule equiv_sym)
    35 qed
    33 qed
    36
    34
    37 lemma not_equiv_trans1 [trans]: "\<not> (x \<sim> y) ==> y \<sim> z ==> \<not> (x \<sim> (z::'a::equiv))"
    35 lemma not_equiv_trans1 [trans]: "\<not> x \<sim> y \<Longrightarrow> y \<sim> z \<Longrightarrow> \<not> x \<sim> z"
    38 proof -
    36 proof -
    39   assume "\<not> (x \<sim> y)" and "y \<sim> z"
    37   assume "\<not> x \<sim> y" and "y \<sim> z"
    40   show "\<not> (x \<sim> z)"
    38   show "\<not> x \<sim> z"
    41   proof
    39   proof
    42     assume "x \<sim> z"
    40     assume "x \<sim> z"
    43     also from y \<sim> z have "z \<sim> y" ..
    41     also from \<open>y \<sim> z\<close> have "z \<sim> y" ..
    44     finally have "x \<sim> y" .
    42     finally have "x \<sim> y" .
    45     with \<not> (x \<sim> y) show False by contradiction
    43     with \<open>\<not> x \<sim> y\<close> show False by contradiction
    46   qed
    44   qed
    47 qed
    45 qed
    48
    46
    49 lemma not_equiv_trans2 [trans]: "x \<sim> y ==> \<not> (y \<sim> z) ==> \<not> (x \<sim> (z::'a::equiv))"
    47 lemma not_equiv_trans2 [trans]: "x \<sim> y \<Longrightarrow> \<not> y \<sim> z \<Longrightarrow> \<not> x \<sim> z"
    50 proof -
    48 proof -
    51   assume "\<not> (y \<sim> z)" then have "\<not> (z \<sim> y)" ..
    49   assume "\<not> y \<sim> z"
    52   also assume "x \<sim> y" then have "y \<sim> x" ..
    50   then have "\<not> z \<sim> y" ..
    53   finally have "\<not> (z \<sim> x)" . then show "(\<not> x \<sim> z)" ..
    51   also

    52   assume "x \<sim> y"

    53   then have "y \<sim> x" ..

    54   finally have "\<not> z \<sim> x" .

    55   then show "\<not> x \<sim> z" ..
    54 qed
    56 qed
    55
    57
    56 text {*
    58 end
    57  \medskip The quotient type @{text "'a quot"} consists of all

    58  \emph{equivalence classes} over elements of the base type @{typ 'a}.

    59 *}

    60
    59
    61 definition "quot = {{x. a \<sim> x} | a::'a::eqv. True}"
    60 text \<open>The quotient type @{text "'a quot"} consists of all \emph{equivalence

    61   classes} over elements of the base type @{typ 'a}.\<close>

    62

    63 definition (in eqv) "quot = {{x. a \<sim> x} | a. True}"
    62
    64
    63 typedef 'a quot = "quot :: 'a::eqv set set"
    65 typedef 'a quot = "quot :: 'a::eqv set set"
    64   unfolding quot_def by blast
    66   unfolding quot_def by blast
    65
    67
    66 lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
    68 lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
    67   unfolding quot_def by blast
    69   unfolding quot_def by blast
    68
    70
    69 lemma quotE [elim]: "R \<in> quot ==> (!!a. R = {x. a \<sim> x} ==> C) ==> C"
    71 lemma quotE [elim]:
    70   unfolding quot_def by blast
    72   assumes "R \<in> quot"

    73   obtains a where "R = {x. a \<sim> x}"

    74   using assms unfolding quot_def by blast
    71
    75
    72 text {*
    76 text \<open>Abstracted equivalence classes are the canonical representation of
    73  \medskip Abstracted equivalence classes are the canonical
    77   elements of a quotient type.\<close>
    74  representation of elements of a quotient type.

    75 *}

    76
    78
    77 definition
    79 definition "class" :: "'a::equiv \<Rightarrow> 'a quot"  ("\<lfloor>_\<rfloor>")
    78   "class" :: "'a::equiv => 'a quot"  ("\<lfloor>_\<rfloor>") where
    80   where "\<lfloor>a\<rfloor> = Abs_quot {x. a \<sim> x}"
    79   "\<lfloor>a\<rfloor> = Abs_quot {x. a \<sim> x}"

    80
    81
    81 theorem quot_exhaust: "\<exists>a. A = \<lfloor>a\<rfloor>"
    82 theorem quot_exhaust: "\<exists>a. A = \<lfloor>a\<rfloor>"
    82 proof (cases A)
    83 proof (cases A)
    83   fix R assume R: "A = Abs_quot R"
    84   fix R
    84   assume "R \<in> quot" then have "\<exists>a. R = {x. a \<sim> x}" by blast
    85   assume R: "A = Abs_quot R"

    86   assume "R \<in> quot"

    87   then have "\<exists>a. R = {x. a \<sim> x}" by blast
    85   with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast
    88   with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast
    86   then show ?thesis unfolding class_def .
    89   then show ?thesis unfolding class_def .
    87 qed
    90 qed
    88
    91
    89 lemma quot_cases [cases type: quot]: "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C"
    92 lemma quot_cases [cases type: quot]:

    93   obtains a where "A = \<lfloor>a\<rfloor>"
    90   using quot_exhaust by blast
    94   using quot_exhaust by blast
    91
    95
    92
    96
    93 subsection {* Equality on quotients *}
    97 subsection \<open>Equality on quotients\<close>
    94
    98
    95 text {*
    99 text \<open>Equality of canonical quotient elements coincides with the original
    96  Equality of canonical quotient elements coincides with the original
   100   relation.\<close>
    97  relation.

    98 *}

    99
   101
   100 theorem quot_equality [iff?]: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)"
   102 theorem quot_equality [iff?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> \<longleftrightarrow> a \<sim> b"
   101 proof
   103 proof
   102   assume eq: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"
   104   assume eq: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"
   103   show "a \<sim> b"
   105   show "a \<sim> b"
   104   proof -
   106   proof -
   105     from eq have "{x. a \<sim> x} = {x. b \<sim> x}"
   107     from eq have "{x. a \<sim> x} = {x. b \<sim> x}"
   129     then show ?thesis by (simp only: class_def)
   131     then show ?thesis by (simp only: class_def)
   130   qed
   132   qed
   131 qed
   133 qed
   132
   134
   133
   135
   134 subsection {* Picking representing elements *}
   136 subsection \<open>Picking representing elements\<close>
   135
   137
   136 definition
   138 definition pick :: "'a::equiv quot \<Rightarrow> 'a"
   137   pick :: "'a::equiv quot => 'a" where
   139   where "pick A = (SOME a. A = \<lfloor>a\<rfloor>)"
   138   "pick A = (SOME a. A = \<lfloor>a\<rfloor>)"

   139
   140
   140 theorem pick_equiv [intro]: "pick \<lfloor>a\<rfloor> \<sim> a"
   141 theorem pick_equiv [intro]: "pick \<lfloor>a\<rfloor> \<sim> a"
   141 proof (unfold pick_def)
   142 proof (unfold pick_def)
   142   show "(SOME x. \<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>) \<sim> a"
   143   show "(SOME x. \<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>) \<sim> a"
   143   proof (rule someI2)
   144   proof (rule someI2)
   144     show "\<lfloor>a\<rfloor> = \<lfloor>a\<rfloor>" ..
   145     show "\<lfloor>a\<rfloor> = \<lfloor>a\<rfloor>" ..
   145     fix x assume "\<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>"
   146     fix x assume "\<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>"
   146     then have "a \<sim> x" .. then show "x \<sim> a" ..
   147     then have "a \<sim> x" ..

   148     then show "x \<sim> a" ..
   147   qed
   149   qed
   148 qed
   150 qed
   149
   151
   150 theorem pick_inverse [intro]: "\<lfloor>pick A\<rfloor> = A"
   152 theorem pick_inverse [intro]: "\<lfloor>pick A\<rfloor> = A"
   151 proof (cases A)
   153 proof (cases A)
   153   then have "pick A \<sim> a" by (simp only: pick_equiv)
   155   then have "pick A \<sim> a" by (simp only: pick_equiv)
   154   then have "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" ..
   156   then have "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" ..
   155   with a show ?thesis by simp
   157   with a show ?thesis by simp
   156 qed
   158 qed
   157
   159
   158 text {*
   160 text \<open>The following rules support canonical function definitions on quotient
   159  \medskip The following rules support canonical function definitions
   161   types (with up to two arguments). Note that the stripped-down version
   160  on quotient types (with up to two arguments).  Note that the
   162   without additional conditions is sufficient most of the time.\<close>
   161  stripped-down version without additional conditions is sufficient

   162  most of the time.

   163 *}

   164
   163
   165 theorem quot_cond_function:
   164 theorem quot_cond_function:
   166   assumes eq: "!!X Y. P X Y ==> f X Y == g (pick X) (pick Y)"
   165   assumes eq: "\<And>X Y. P X Y \<Longrightarrow> f X Y \<equiv> g (pick X) (pick Y)"
   167     and cong: "!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor>
   166     and cong: "\<And>x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> \<Longrightarrow> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor>
   168       ==> P \<lfloor>x\<rfloor> \<lfloor>y\<rfloor> ==> P \<lfloor>x'\<rfloor> \<lfloor>y'\<rfloor> ==> g x y = g x' y'"
   167       \<Longrightarrow> P \<lfloor>x\<rfloor> \<lfloor>y\<rfloor> \<Longrightarrow> P \<lfloor>x'\<rfloor> \<lfloor>y'\<rfloor> \<Longrightarrow> g x y = g x' y'"
   169     and P: "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>"
   168     and P: "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>"
   170   shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
   169   shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
   171 proof -
   170 proof -
   172   from eq and P have "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" by (simp only:)
   171   from eq and P have "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" by (simp only:)
   173   also have "... = g a b"
   172   also have "... = g a b"
   181   qed
   180   qed
   182   finally show ?thesis .
   181   finally show ?thesis .
   183 qed
   182 qed
   184
   183
   185 theorem quot_function:
   184 theorem quot_function:
   186   assumes "!!X Y. f X Y == g (pick X) (pick Y)"
   185   assumes "\<And>X Y. f X Y \<equiv> g (pick X) (pick Y)"
   187     and "!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> g x y = g x' y'"
   186     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'"
   188   shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
   187   shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
   189   using assms and TrueI
   188   using assms and TrueI
   190   by (rule quot_cond_function)
   189   by (rule quot_cond_function)
   191
   190
   192 theorem quot_function':
   191 theorem quot_function':
   193   "(!!X Y. f X Y == g (pick X) (pick Y)) ==>
   192   "(\<And>X Y. f X Y \<equiv> g (pick X) (pick Y)) \<Longrightarrow>
   194     (!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> g x y = g x' y') ==>
   193     (\<And>x x' y y'. x \<sim> x' \<Longrightarrow> y \<sim> y' \<Longrightarrow> g x y = g x' y') \<Longrightarrow>
   195     f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
   194     f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
   196   by (rule quot_function) (simp_all only: quot_equality)
   195   by (rule quot_function) (simp_all only: quot_equality)
   197
   196
   198 end
   197 end