src/HOL/Quotient.thy
author wenzelm
Mon, 12 Apr 2021 14:14:47 +0200
changeset 73563 55b66a45bc94
parent 71627 2a24c2015a61
child 75455 91c16c5ad3e9
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
41959
b460124855b8 tuned headers;
wenzelm
parents: 41452
diff changeset
     1
(*  Title:      HOL/Quotient.thy
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     2
    Author:     Cezary Kaliszyk and Christian Urban
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     3
*)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     4
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
     5
section \<open>Definition of Quotient Types\<close>
35294
0e1adc24722f proper header and subsection headings
huffman
parents: 35236
diff changeset
     6
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     7
theory Quotient
54555
e8c5e95d338b rationalize imports
blanchet
parents: 53011
diff changeset
     8
imports Lifting
46950
d0181abdbdac declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents: 46947
diff changeset
     9
keywords
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
    10
  "print_quotmapsQ3" "print_quotientsQ3" "print_quotconsts" :: diag and
69913
ca515cf61651 more specific keyword kinds;
wenzelm
parents: 69605
diff changeset
    11
  "quotient_type" :: thy_goal_defn and "/" and
71262
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
    12
  "quotient_definition" :: thy_goal_defn and
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
    13
  "copy_bnf" :: thy_defn and
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
    14
  "lift_bnf" :: thy_goal_defn
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    15
begin
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    16
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
    17
text \<open>
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    18
  Basic definition for equivalence relations
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    19
  that are represented by predicates.
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
    20
\<close>
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    21
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
    22
text \<open>Composition of Relations\<close>
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    23
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    24
abbreviation
40818
b117df72e56b reorienting iff in Quotient_rel prevents simplifier looping;
haftmann
parents: 40814
diff changeset
    25
  rel_conj :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" (infixr "OOO" 75)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    26
where
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    27
  "r1 OOO r2 \<equiv> r1 OO r2 OO r1"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    28
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    29
lemma eq_comp_r:
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 67091
diff changeset
    30
  shows "((=) OOO R) = R"
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39198
diff changeset
    31
  by (auto simp add: fun_eq_iff)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    32
63343
fb5d8a50c641 bundle lifting_syntax;
wenzelm
parents: 61799
diff changeset
    33
context includes lifting_syntax
53011
aeee0a4be6cf introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents: 51112
diff changeset
    34
begin
aeee0a4be6cf introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents: 51112
diff changeset
    35
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
    36
subsection \<open>Quotient Predicate\<close>
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    37
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    38
definition
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
    39
  "Quotient3 R Abs Rep \<longleftrightarrow>
40814
fa64f6278568 moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents: 40615
diff changeset
    40
     (\<forall>a. Abs (Rep a) = a) \<and> (\<forall>a. R (Rep a) (Rep a)) \<and>
40818
b117df72e56b reorienting iff in Quotient_rel prevents simplifier looping;
haftmann
parents: 40814
diff changeset
    41
     (\<forall>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s)"
b117df72e56b reorienting iff in Quotient_rel prevents simplifier looping;
haftmann
parents: 40814
diff changeset
    42
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
    43
lemma Quotient3I:
40818
b117df72e56b reorienting iff in Quotient_rel prevents simplifier looping;
haftmann
parents: 40814
diff changeset
    44
  assumes "\<And>a. Abs (Rep a) = a"
b117df72e56b reorienting iff in Quotient_rel prevents simplifier looping;
haftmann
parents: 40814
diff changeset
    45
    and "\<And>a. R (Rep a) (Rep a)"
b117df72e56b reorienting iff in Quotient_rel prevents simplifier looping;
haftmann
parents: 40814
diff changeset
    46
    and "\<And>r s. R r s \<longleftrightarrow> R r r \<and> R s s \<and> Abs r = Abs s"
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
    47
  shows "Quotient3 R Abs Rep"
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
    48
  using assms unfolding Quotient3_def by blast
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    49
54867
c21a2465cac1 prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents: 54555
diff changeset
    50
context
c21a2465cac1 prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents: 54555
diff changeset
    51
  fixes R Abs Rep
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
    52
  assumes a: "Quotient3 R Abs Rep"
54867
c21a2465cac1 prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents: 54555
diff changeset
    53
begin
c21a2465cac1 prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents: 54555
diff changeset
    54
c21a2465cac1 prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents: 54555
diff changeset
    55
lemma Quotient3_abs_rep:
c21a2465cac1 prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents: 54555
diff changeset
    56
  "Abs (Rep a) = a"
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    57
  using a
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
    58
  unfolding Quotient3_def
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    59
  by simp
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    60
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
    61
lemma Quotient3_rep_reflp:
54867
c21a2465cac1 prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents: 54555
diff changeset
    62
  "R (Rep a) (Rep a)"
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    63
  using a
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
    64
  unfolding Quotient3_def
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    65
  by blast
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    66
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
    67
lemma Quotient3_rel:
61799
4cf66f21b764 isabelle update_cartouches -c -t;
wenzelm
parents: 60758
diff changeset
    68
  "R r r \<and> R s s \<and> Abs r = Abs s \<longleftrightarrow> R r s" \<comment> \<open>orientation does not loop on rewriting\<close>
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    69
  using a
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
    70
  unfolding Quotient3_def
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    71
  by blast
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    72
71262
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
    73
lemma Quotient3_refl1:
54867
c21a2465cac1 prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents: 54555
diff changeset
    74
  "R r s \<Longrightarrow> R r r"
71262
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
    75
  using a unfolding Quotient3_def
47096
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47094
diff changeset
    76
  by fast
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47094
diff changeset
    77
71262
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
    78
lemma Quotient3_refl2:
54867
c21a2465cac1 prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents: 54555
diff changeset
    79
  "R r s \<Longrightarrow> R s s"
71262
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
    80
  using a unfolding Quotient3_def
47096
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47094
diff changeset
    81
  by fast
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47094
diff changeset
    82
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
    83
lemma Quotient3_rel_rep:
54867
c21a2465cac1 prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents: 54555
diff changeset
    84
  "R (Rep a) (Rep b) \<longleftrightarrow> a = b"
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    85
  using a
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
    86
  unfolding Quotient3_def
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    87
  by metis
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    88
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
    89
lemma Quotient3_rep_abs:
54867
c21a2465cac1 prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents: 54555
diff changeset
    90
  "R r r \<Longrightarrow> R (Rep (Abs r)) r"
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
    91
  using a unfolding Quotient3_def
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
    92
  by blast
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
    93
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
    94
lemma Quotient3_rel_abs:
54867
c21a2465cac1 prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents: 54555
diff changeset
    95
  "R r s \<Longrightarrow> Abs r = Abs s"
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
    96
  using a unfolding Quotient3_def
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    97
  by blast
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    98
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
    99
lemma Quotient3_symp:
54867
c21a2465cac1 prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents: 54555
diff changeset
   100
  "symp R"
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   101
  using a unfolding Quotient3_def using sympI by metis
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   102
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   103
lemma Quotient3_transp:
54867
c21a2465cac1 prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents: 54555
diff changeset
   104
  "transp R"
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   105
  using a unfolding Quotient3_def using transpI by (metis (full_types))
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   106
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   107
lemma Quotient3_part_equivp:
54867
c21a2465cac1 prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents: 54555
diff changeset
   108
  "part_equivp R"
c21a2465cac1 prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents: 54555
diff changeset
   109
  by (metis Quotient3_rep_reflp Quotient3_symp Quotient3_transp part_equivpI)
c21a2465cac1 prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents: 54555
diff changeset
   110
c21a2465cac1 prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents: 54555
diff changeset
   111
lemma abs_o_rep:
67091
1393c2340eec more symbols;
wenzelm
parents: 63343
diff changeset
   112
  "Abs \<circ> Rep = id"
54867
c21a2465cac1 prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents: 54555
diff changeset
   113
  unfolding fun_eq_iff
c21a2465cac1 prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents: 54555
diff changeset
   114
  by (simp add: Quotient3_abs_rep)
c21a2465cac1 prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents: 54555
diff changeset
   115
c21a2465cac1 prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents: 54555
diff changeset
   116
lemma equals_rsp:
c21a2465cac1 prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents: 54555
diff changeset
   117
  assumes b: "R xa xb" "R ya yb"
c21a2465cac1 prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents: 54555
diff changeset
   118
  shows "R xa ya = R xb yb"
c21a2465cac1 prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents: 54555
diff changeset
   119
  using b Quotient3_symp Quotient3_transp
c21a2465cac1 prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents: 54555
diff changeset
   120
  by (blast elim: sympE transpE)
c21a2465cac1 prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents: 54555
diff changeset
   121
c21a2465cac1 prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents: 54555
diff changeset
   122
lemma rep_abs_rsp:
c21a2465cac1 prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents: 54555
diff changeset
   123
  assumes b: "R x1 x2"
c21a2465cac1 prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents: 54555
diff changeset
   124
  shows "R x1 (Rep (Abs x2))"
c21a2465cac1 prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents: 54555
diff changeset
   125
  using b Quotient3_rel Quotient3_abs_rep Quotient3_rep_reflp
c21a2465cac1 prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents: 54555
diff changeset
   126
  by metis
c21a2465cac1 prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents: 54555
diff changeset
   127
c21a2465cac1 prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents: 54555
diff changeset
   128
lemma rep_abs_rsp_left:
c21a2465cac1 prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents: 54555
diff changeset
   129
  assumes b: "R x1 x2"
c21a2465cac1 prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents: 54555
diff changeset
   130
  shows "R (Rep (Abs x1)) x2"
c21a2465cac1 prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents: 54555
diff changeset
   131
  using b Quotient3_rel Quotient3_abs_rep Quotient3_rep_reflp
c21a2465cac1 prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents: 54555
diff changeset
   132
  by metis
c21a2465cac1 prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents: 54555
diff changeset
   133
c21a2465cac1 prefer ephemeral interpretation over interpretation in proof contexts;
haftmann
parents: 54555
diff changeset
   134
end
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   135
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   136
lemma identity_quotient3:
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 67091
diff changeset
   137
  "Quotient3 (=) id id"
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   138
  unfolding Quotient3_def id_def
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   139
  by blast
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   140
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   141
lemma fun_quotient3:
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   142
  assumes q1: "Quotient3 R1 abs1 rep1"
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   143
  and     q2: "Quotient3 R2 abs2 rep2"
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   144
  shows "Quotient3 (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   145
proof -
69990
eb072ce80f82 tuned proofs;
wenzelm
parents: 69913
diff changeset
   146
  have "(rep1 ---> abs2) ((abs1 ---> rep2) a) = a" for a
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   147
    using q1 q2 by (simp add: Quotient3_def fun_eq_iff)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   148
  moreover
69990
eb072ce80f82 tuned proofs;
wenzelm
parents: 69913
diff changeset
   149
  have "(R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)" for a
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 54867
diff changeset
   150
    by (rule rel_funI)
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   151
      (insert q1 q2 Quotient3_rel_abs [of R1 abs1 rep1] Quotient3_rel_rep [of R2 abs2 rep2],
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   152
        simp (no_asm) add: Quotient3_def, simp)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   153
  moreover
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   154
  have "(R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
69990
eb072ce80f82 tuned proofs;
wenzelm
parents: 69913
diff changeset
   155
        (rep1 ---> abs2) r  = (rep1 ---> abs2) s)" for r s
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   156
  proof -
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 54867
diff changeset
   157
    have "(R1 ===> R2) r s \<Longrightarrow> (R1 ===> R2) r r" unfolding rel_fun_def
71262
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   158
      using Quotient3_part_equivp[OF q1] Quotient3_part_equivp[OF q2]
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   159
      by (metis (full_types) part_equivp_def)
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 54867
diff changeset
   160
    moreover have "(R1 ===> R2) r s \<Longrightarrow> (R1 ===> R2) s s" unfolding rel_fun_def
71262
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   161
      using Quotient3_part_equivp[OF q1] Quotient3_part_equivp[OF q2]
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   162
      by (metis (full_types) part_equivp_def)
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   163
    moreover have "(R1 ===> R2) r s \<Longrightarrow> (rep1 ---> abs2) r  = (rep1 ---> abs2) s"
69990
eb072ce80f82 tuned proofs;
wenzelm
parents: 69913
diff changeset
   164
      by (auto simp add: rel_fun_def fun_eq_iff)
eb072ce80f82 tuned proofs;
wenzelm
parents: 69913
diff changeset
   165
        (use q1 q2 in \<open>unfold Quotient3_def, metis\<close>)
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   166
    moreover have "((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   167
        (rep1 ---> abs2) r  = (rep1 ---> abs2) s) \<Longrightarrow> (R1 ===> R2) r s"
69990
eb072ce80f82 tuned proofs;
wenzelm
parents: 69913
diff changeset
   168
      by (auto simp add: rel_fun_def fun_eq_iff)
eb072ce80f82 tuned proofs;
wenzelm
parents: 69913
diff changeset
   169
        (use q1 q2 in \<open>unfold Quotient3_def, metis map_fun_apply\<close>)
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   170
    ultimately show ?thesis by blast
69990
eb072ce80f82 tuned proofs;
wenzelm
parents: 69913
diff changeset
   171
  qed
eb072ce80f82 tuned proofs;
wenzelm
parents: 69913
diff changeset
   172
  ultimately show ?thesis by (intro Quotient3I) (assumption+)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   173
qed
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   174
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   175
lemma lambda_prs:
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   176
  assumes q1: "Quotient3 R1 Abs1 Rep1"
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   177
  and     q2: "Quotient3 R2 Abs2 Rep2"
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   178
  shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)"
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39198
diff changeset
   179
  unfolding fun_eq_iff
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   180
  using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]
40814
fa64f6278568 moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents: 40615
diff changeset
   181
  by simp
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   182
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   183
lemma lambda_prs1:
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   184
  assumes q1: "Quotient3 R1 Abs1 Rep1"
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   185
  and     q2: "Quotient3 R2 Abs2 Rep2"
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   186
  shows "(Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x) = (\<lambda>x. f x)"
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39198
diff changeset
   187
  unfolding fun_eq_iff
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   188
  using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]
40814
fa64f6278568 moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
haftmann
parents: 40615
diff changeset
   189
  by simp
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   190
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
   191
text\<open>
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   192
  In the following theorem R1 can be instantiated with anything,
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   193
  but we know some of the types of the Rep and Abs functions;
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   194
  so by solving Quotient assumptions we can get a unique R1 that
61799
4cf66f21b764 isabelle update_cartouches -c -t;
wenzelm
parents: 60758
diff changeset
   195
  will be provable; which is why we need to use \<open>apply_rsp\<close> and
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
   196
  not the primed version\<close>
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   197
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   198
lemma apply_rspQ3:
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   199
  fixes f g::"'a \<Rightarrow> 'c"
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   200
  assumes q: "Quotient3 R1 Abs1 Rep1"
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   201
  and     a: "(R1 ===> R2) f g" "R1 x y"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   202
  shows "R2 (f x) (g y)"
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 54867
diff changeset
   203
  using a by (auto elim: rel_funE)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   204
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   205
lemma apply_rspQ3'':
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   206
  assumes "Quotient3 R Abs Rep"
47096
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47094
diff changeset
   207
  and "(R ===> S) f f"
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47094
diff changeset
   208
  shows "S (f (Rep x)) (f (Rep x))"
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47094
diff changeset
   209
proof -
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   210
  from assms(1) have "R (Rep x) (Rep x)" by (rule Quotient3_rep_reflp)
47096
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47094
diff changeset
   211
  then show ?thesis using assms(2) by (auto intro: apply_rsp')
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47094
diff changeset
   212
qed
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47094
diff changeset
   213
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
   214
subsection \<open>lemmas for regularisation of ball and bex\<close>
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   215
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   216
lemma ball_reg_eqv:
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   217
  fixes P :: "'a \<Rightarrow> bool"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   218
  assumes a: "equivp R"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   219
  shows "Ball (Respects R) P = (All P)"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   220
  using a
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   221
  unfolding equivp_def
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   222
  by (auto simp add: in_respects)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   223
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   224
lemma bex_reg_eqv:
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   225
  fixes P :: "'a \<Rightarrow> bool"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   226
  assumes a: "equivp R"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   227
  shows "Bex (Respects R) P = (Ex P)"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   228
  using a
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   229
  unfolding equivp_def
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   230
  by (auto simp add: in_respects)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   231
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   232
lemma ball_reg_right:
44553
4d39b032a021 avoid intermixing set and predicates; dropped lemmas mem_rsp and mem_prs (now in Quotient_Set.thy)
haftmann
parents: 44413
diff changeset
   233
  assumes a: "\<And>x. x \<in> R \<Longrightarrow> P x \<longrightarrow> Q x"
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   234
  shows "All P \<longrightarrow> Ball R Q"
44921
58eef4843641 tuned proofs
huffman
parents: 44553
diff changeset
   235
  using a by fast
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   236
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   237
lemma bex_reg_left:
44553
4d39b032a021 avoid intermixing set and predicates; dropped lemmas mem_rsp and mem_prs (now in Quotient_Set.thy)
haftmann
parents: 44413
diff changeset
   238
  assumes a: "\<And>x. x \<in> R \<Longrightarrow> Q x \<longrightarrow> P x"
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   239
  shows "Bex R Q \<longrightarrow> Ex P"
44921
58eef4843641 tuned proofs
huffman
parents: 44553
diff changeset
   240
  using a by fast
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   241
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   242
lemma ball_reg_left:
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   243
  assumes a: "equivp R"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   244
  shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ball (Respects R) Q \<longrightarrow> All P"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   245
  using a by (metis equivp_reflp in_respects)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   246
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   247
lemma bex_reg_right:
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   248
  assumes a: "equivp R"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   249
  shows "(\<And>x. (Q x \<longrightarrow> P x)) \<Longrightarrow> Ex Q \<longrightarrow> Bex (Respects R) P"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   250
  using a by (metis equivp_reflp in_respects)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   251
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   252
lemma ball_reg_eqv_range:
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   253
  fixes P::"'a \<Rightarrow> bool"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   254
  and x::"'a"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   255
  assumes a: "equivp R2"
71627
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   256
  shows "(Ball (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = All (\<lambda>f. P (f x)))"
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   257
proof (intro allI iffI)
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   258
  fix f
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   259
  assume "\<forall>f \<in> Respects (R1 ===> R2). P (f x)"
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   260
  moreover have "(\<lambda>y. f x) \<in> Respects (R1 ===> R2)"
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   261
    using a equivp_reflp_symp_transp[of "R2"]
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   262
    by(auto simp add: in_respects rel_fun_def elim: equivpE reflpE)
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   263
  ultimately show "P (f x)"
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   264
    by auto
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   265
qed auto
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   266
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   267
lemma bex_reg_eqv_range:
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   268
  assumes a: "equivp R2"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   269
  shows   "(Bex (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = Ex (\<lambda>f. P (f x)))"
71627
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   270
proof -
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   271
  { fix f
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   272
    assume "P (f x)"
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   273
    have "(\<lambda>y. f x) \<in> Respects (R1 ===> R2)"
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   274
      using a equivp_reflp_symp_transp[of "R2"]
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   275
      by (auto simp add: Respects_def in_respects rel_fun_def elim: equivpE reflpE) }
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   276
  then show ?thesis
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   277
    by auto
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   278
qed
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   279
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   280
(* Next four lemmas are unused *)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   281
lemma all_reg:
67091
1393c2340eec more symbols;
wenzelm
parents: 63343
diff changeset
   282
  assumes a: "\<forall>x :: 'a. (P x \<longrightarrow> Q x)"
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   283
  and     b: "All P"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   284
  shows "All Q"
44921
58eef4843641 tuned proofs
huffman
parents: 44553
diff changeset
   285
  using a b by fast
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   286
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   287
lemma ex_reg:
67091
1393c2340eec more symbols;
wenzelm
parents: 63343
diff changeset
   288
  assumes a: "\<forall>x :: 'a. (P x \<longrightarrow> Q x)"
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   289
  and     b: "Ex P"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   290
  shows "Ex Q"
44921
58eef4843641 tuned proofs
huffman
parents: 44553
diff changeset
   291
  using a b by fast
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   292
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   293
lemma ball_reg:
67091
1393c2340eec more symbols;
wenzelm
parents: 63343
diff changeset
   294
  assumes a: "\<forall>x :: 'a. (x \<in> R \<longrightarrow> P x \<longrightarrow> Q x)"
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   295
  and     b: "Ball R P"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   296
  shows "Ball R Q"
44921
58eef4843641 tuned proofs
huffman
parents: 44553
diff changeset
   297
  using a b by fast
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   298
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   299
lemma bex_reg:
67091
1393c2340eec more symbols;
wenzelm
parents: 63343
diff changeset
   300
  assumes a: "\<forall>x :: 'a. (x \<in> R \<longrightarrow> P x \<longrightarrow> Q x)"
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   301
  and     b: "Bex R P"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   302
  shows "Bex R Q"
44921
58eef4843641 tuned proofs
huffman
parents: 44553
diff changeset
   303
  using a b by fast
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   304
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   305
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   306
lemma ball_all_comm:
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   307
  assumes "\<And>y. (\<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>x. B x y)"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   308
  shows "(\<forall>x\<in>P. \<forall>y. A x y) \<longrightarrow> (\<forall>x. \<forall>y. B x y)"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   309
  using assms by auto
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   310
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   311
lemma bex_ex_comm:
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   312
  assumes "(\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   313
  shows "(\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y)"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   314
  using assms by auto
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   315
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
   316
subsection \<open>Bounded abstraction\<close>
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   317
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   318
definition
40466
c6587375088e type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions
haftmann
parents: 40031
diff changeset
   319
  Babs :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   320
where
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   321
  "x \<in> p \<Longrightarrow> Babs p m x = m x"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   322
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   323
lemma babs_rsp:
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   324
  assumes q: "Quotient3 R1 Abs1 Rep1"
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   325
  and     a: "(R1 ===> R2) f g"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   326
  shows      "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)"
71627
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   327
proof (clarsimp simp add: Babs_def in_respects rel_fun_def)
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   328
  fix x y
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   329
  assume "R1 x y"
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   330
  then have "x \<in> Respects R1 \<and> y \<in> Respects R1"
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   331
    unfolding in_respects rel_fun_def using Quotient3_rel[OF q]by metis
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   332
  then show "R2 (Babs (Respects R1) f x) (Babs (Respects R1) g y)"
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   333
  using \<open>R1 x y\<close> a by (simp add: Babs_def rel_fun_def)
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   334
qed
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   335
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   336
lemma babs_prs:
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   337
  assumes q1: "Quotient3 R1 Abs1 Rep1"
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   338
  and     q2: "Quotient3 R2 Abs2 Rep2"
71627
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   339
shows "((Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f))) = f"
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   340
proof -
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   341
  { fix x
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   342
    have "Rep1 x \<in> Respects R1"
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   343
      by (simp add: in_respects Quotient3_rel_rep[OF q1])
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   344
    then have "Abs2 (Babs (Respects R1) ((Abs1 ---> Rep2) f) (Rep1 x)) = f x" 
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   345
      by (simp add: Babs_def Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2])
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   346
  }
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   347
  then show ?thesis
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   348
    by force
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   349
qed
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   350
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   351
lemma babs_simp:
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   352
  assumes q: "Quotient3 R1 Abs Rep"
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   353
  shows "((R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)) = ((R1 ===> R2) f g)"
71627
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   354
         (is "?lhs = ?rhs")
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   355
proof
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   356
  assume ?lhs
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   357
  then show ?rhs
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   358
    unfolding rel_fun_def by (metis Babs_def in_respects  Quotient3_rel[OF q])
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   359
qed (simp add: babs_rsp[OF q])
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   360
71627
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   361
text \<open>If a user proves that a particular functional relation
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   362
   is an equivalence, this may be useful in regularising\<close>
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   363
lemma babs_reg_eqv:
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   364
  shows "equivp R \<Longrightarrow> Babs (Respects R) P = P"
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39198
diff changeset
   365
  by (simp add: fun_eq_iff Babs_def in_respects equivp_reflp)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   366
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   367
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   368
(* 3 lemmas needed for proving repabs_inj *)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   369
lemma ball_rsp:
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 67091
diff changeset
   370
  assumes a: "(R ===> (=)) f g"
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   371
  shows "Ball (Respects R) f = Ball (Respects R) g"
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 54867
diff changeset
   372
  using a by (auto simp add: Ball_def in_respects elim: rel_funE)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   373
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   374
lemma bex_rsp:
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 67091
diff changeset
   375
  assumes a: "(R ===> (=)) f g"
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   376
  shows "(Bex (Respects R) f = Bex (Respects R) g)"
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 54867
diff changeset
   377
  using a by (auto simp add: Bex_def in_respects elim: rel_funE)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   378
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   379
lemma bex1_rsp:
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 67091
diff changeset
   380
  assumes a: "(R ===> (=)) f g"
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   381
  shows "Ex1 (\<lambda>x. x \<in> Respects R \<and> f x) = Ex1 (\<lambda>x. x \<in> Respects R \<and> g x)"
71262
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   382
  using a by (auto elim: rel_funE simp add: Ex1_def in_respects)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   383
71627
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   384
text \<open>Two lemmas needed for cleaning of quantifiers\<close>
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   385
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   386
lemma all_prs:
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   387
  assumes a: "Quotient3 R absf repf"
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   388
  shows "Ball (Respects R) ((absf ---> id) f) = All f"
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   389
  using a unfolding Quotient3_def Ball_def in_respects id_apply comp_def map_fun_def
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   390
  by metis
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   391
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   392
lemma ex_prs:
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   393
  assumes a: "Quotient3 R absf repf"
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   394
  shows "Bex (Respects R) ((absf ---> id) f) = Ex f"
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   395
  using a unfolding Quotient3_def Bex_def in_respects id_apply comp_def map_fun_def
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   396
  by metis
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   397
61799
4cf66f21b764 isabelle update_cartouches -c -t;
wenzelm
parents: 60758
diff changeset
   398
subsection \<open>\<open>Bex1_rel\<close> quantifier\<close>
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   399
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   400
definition
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   401
  Bex1_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   402
where
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   403
  "Bex1_rel R P \<longleftrightarrow> (\<exists>x \<in> Respects R. P x) \<and> (\<forall>x \<in> Respects R. \<forall>y \<in> Respects R. ((P x \<and> P y) \<longrightarrow> (R x y)))"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   404
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   405
lemma bex1_rel_aux:
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   406
  "\<lbrakk>\<forall>xa ya. R xa ya \<longrightarrow> x xa = y ya; Bex1_rel R x\<rbrakk> \<Longrightarrow> Bex1_rel R y"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   407
  unfolding Bex1_rel_def
68615
3ed4ff0b7ac4 de-applying
paulson <lp15@cam.ac.uk>
parents: 67399
diff changeset
   408
  by (metis in_respects)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   409
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   410
lemma bex1_rel_aux2:
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   411
  "\<lbrakk>\<forall>xa ya. R xa ya \<longrightarrow> x xa = y ya; Bex1_rel R y\<rbrakk> \<Longrightarrow> Bex1_rel R x"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   412
  unfolding Bex1_rel_def
68615
3ed4ff0b7ac4 de-applying
paulson <lp15@cam.ac.uk>
parents: 67399
diff changeset
   413
  by (metis in_respects)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   414
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   415
lemma bex1_rel_rsp:
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   416
  assumes a: "Quotient3 R absf repf"
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 67091
diff changeset
   417
  shows "((R ===> (=)) ===> (=)) (Bex1_rel R) (Bex1_rel R)"
68615
3ed4ff0b7ac4 de-applying
paulson <lp15@cam.ac.uk>
parents: 67399
diff changeset
   418
  unfolding rel_fun_def by (metis bex1_rel_aux bex1_rel_aux2)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   419
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   420
lemma ex1_prs:
68616
cedf3480fdad de-applying (mostly Quotient)
paulson <lp15@cam.ac.uk>
parents: 68615
diff changeset
   421
  assumes "Quotient3 R absf repf"
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   422
  shows "((absf ---> id) ---> id) (Bex1_rel R) f = Ex1 f"
71627
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   423
         (is "?lhs = ?rhs")
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   424
  using assms
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   425
  apply (auto simp add: Bex1_rel_def Respects_def)
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   426
  by (metis (full_types) Quotient3_def)+
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   427
38702
72fd257f4343 Quotient Package / lemma for regularization of bex1_rel for equivalence relations
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 38317
diff changeset
   428
lemma bex1_bexeq_reg:
72fd257f4343 Quotient Package / lemma for regularization of bex1_rel for equivalence relations
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 38317
diff changeset
   429
  shows "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bex1_rel R (\<lambda>x. P x))"
56073
29e308b56d23 enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions
nipkow
parents: 55945
diff changeset
   430
  by (auto simp add: Ex1_def Bex1_rel_def Bex_def Ball_def in_respects)
71262
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   431
38702
72fd257f4343 Quotient Package / lemma for regularization of bex1_rel for equivalence relations
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 38317
diff changeset
   432
lemma bex1_bexeq_reg_eqv:
72fd257f4343 Quotient Package / lemma for regularization of bex1_rel for equivalence relations
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 38317
diff changeset
   433
  assumes a: "equivp R"
72fd257f4343 Quotient Package / lemma for regularization of bex1_rel for equivalence relations
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 38317
diff changeset
   434
  shows "(\<exists>!x. P x) \<longrightarrow> Bex1_rel R P"
72fd257f4343 Quotient Package / lemma for regularization of bex1_rel for equivalence relations
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 38317
diff changeset
   435
  using equivp_reflp[OF a]
68616
cedf3480fdad de-applying (mostly Quotient)
paulson <lp15@cam.ac.uk>
parents: 68615
diff changeset
   436
  by (metis (full_types) Bex1_rel_def in_respects)
38702
72fd257f4343 Quotient Package / lemma for regularization of bex1_rel for equivalence relations
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 38317
diff changeset
   437
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
   438
subsection \<open>Various respects and preserve lemmas\<close>
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   439
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   440
lemma quot_rel_rsp:
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   441
  assumes a: "Quotient3 R Abs Rep"
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 67091
diff changeset
   442
  shows "(R ===> R ===> (=)) R R"
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 54867
diff changeset
   443
  apply(rule rel_funI)+
68616
cedf3480fdad de-applying (mostly Quotient)
paulson <lp15@cam.ac.uk>
parents: 68615
diff changeset
   444
  by (meson assms equals_rsp)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   445
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   446
lemma o_prs:
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   447
  assumes q1: "Quotient3 R1 Abs1 Rep1"
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   448
  and     q2: "Quotient3 R2 Abs2 Rep2"
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   449
  and     q3: "Quotient3 R3 Abs3 Rep3"
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 67091
diff changeset
   450
  shows "((Abs2 ---> Rep3) ---> (Abs1 ---> Rep2) ---> (Rep1 ---> Abs3)) (\<circ>) = (\<circ>)"
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 67091
diff changeset
   451
  and   "(id ---> (Abs1 ---> id) ---> Rep1 ---> id) (\<circ>) = (\<circ>)"
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   452
  using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2] Quotient3_abs_rep[OF q3]
40466
c6587375088e type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions
haftmann
parents: 40031
diff changeset
   453
  by (simp_all add: fun_eq_iff)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   454
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   455
lemma o_rsp:
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 67091
diff changeset
   456
  "((R2 ===> R3) ===> (R1 ===> R2) ===> (R1 ===> R3)) (\<circ>) (\<circ>)"
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 67091
diff changeset
   457
  "((=) ===> (R1 ===> (=)) ===> R1 ===> (=)) (\<circ>) (\<circ>)"
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 54867
diff changeset
   458
  by (force elim: rel_funE)+
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   459
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   460
lemma cond_prs:
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   461
  assumes a: "Quotient3 R absf repf"
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   462
  shows "absf (if a then repf b else repf c) = (if a then b else c)"
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   463
  using a unfolding Quotient3_def by auto
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   464
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   465
lemma if_prs:
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   466
  assumes q: "Quotient3 R Abs Rep"
36123
7f877bbad5b2 add If respectfullness and preservation to Quotient package database
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 36116
diff changeset
   467
  shows "(id ---> Rep ---> Rep ---> Abs) If = If"
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   468
  using Quotient3_abs_rep[OF q]
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39198
diff changeset
   469
  by (auto simp add: fun_eq_iff)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   470
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   471
lemma if_rsp:
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   472
  assumes q: "Quotient3 R Abs Rep"
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 67091
diff changeset
   473
  shows "((=) ===> R ===> R ===> R) If If"
44921
58eef4843641 tuned proofs
huffman
parents: 44553
diff changeset
   474
  by force
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   475
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   476
lemma let_prs:
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   477
  assumes q1: "Quotient3 R1 Abs1 Rep1"
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   478
  and     q2: "Quotient3 R2 Abs2 Rep2"
37049
ca1c293e521e Let rsp and prs in fun_rel/fun_map format
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 36276
diff changeset
   479
  shows "(Rep2 ---> (Abs2 ---> Rep1) ---> Abs1) Let = Let"
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   480
  using Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2]
39302
d7728f65b353 renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents: 39198
diff changeset
   481
  by (auto simp add: fun_eq_iff)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   482
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   483
lemma let_rsp:
37049
ca1c293e521e Let rsp and prs in fun_rel/fun_map format
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 36276
diff changeset
   484
  shows "(R1 ===> (R1 ===> R2) ===> R2) Let Let"
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 54867
diff changeset
   485
  by (force elim: rel_funE)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   486
39669
9e3b035841e4 quotient package: respectfulness and preservation of identity.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
   487
lemma id_rsp:
9e3b035841e4 quotient package: respectfulness and preservation of identity.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
   488
  shows "(R ===> R) id id"
44921
58eef4843641 tuned proofs
huffman
parents: 44553
diff changeset
   489
  by auto
39669
9e3b035841e4 quotient package: respectfulness and preservation of identity.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
   490
9e3b035841e4 quotient package: respectfulness and preservation of identity.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
   491
lemma id_prs:
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   492
  assumes a: "Quotient3 R Abs Rep"
39669
9e3b035841e4 quotient package: respectfulness and preservation of identity.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
   493
  shows "(Rep ---> Abs) id = id"
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   494
  by (simp add: fun_eq_iff Quotient3_abs_rep [OF a])
39669
9e3b035841e4 quotient package: respectfulness and preservation of identity.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
   495
53011
aeee0a4be6cf introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents: 51112
diff changeset
   496
end
39669
9e3b035841e4 quotient package: respectfulness and preservation of identity.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 39302
diff changeset
   497
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   498
locale quot_type =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   499
  fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
44204
3cdc4176638c Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 42814
diff changeset
   500
  and   Abs :: "'a set \<Rightarrow> 'b"
3cdc4176638c Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 42814
diff changeset
   501
  and   Rep :: "'b \<Rightarrow> 'a set"
37493
2377d246a631 Quotient package now uses Partial Equivalence instead place of equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 37049
diff changeset
   502
  assumes equivp: "part_equivp R"
44204
3cdc4176638c Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 42814
diff changeset
   503
  and     rep_prop: "\<And>y. \<exists>x. R x x \<and> Rep y = Collect (R x)"
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   504
  and     rep_inverse: "\<And>x. Abs (Rep x) = x"
44204
3cdc4176638c Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 42814
diff changeset
   505
  and     abs_inverse: "\<And>c. (\<exists>x. ((R x x) \<and> (c = Collect (R x)))) \<Longrightarrow> (Rep (Abs c)) = c"
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   506
  and     rep_inject: "\<And>x y. (Rep x = Rep y) = (x = y)"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   507
begin
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   508
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   509
definition
40466
c6587375088e type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions
haftmann
parents: 40031
diff changeset
   510
  abs :: "'a \<Rightarrow> 'b"
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   511
where
44204
3cdc4176638c Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 42814
diff changeset
   512
  "abs x = Abs (Collect (R x))"
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   513
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   514
definition
40466
c6587375088e type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions
haftmann
parents: 40031
diff changeset
   515
  rep :: "'b \<Rightarrow> 'a"
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   516
where
44204
3cdc4176638c Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 42814
diff changeset
   517
  "rep a = (SOME x. x \<in> Rep a)"
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   518
44204
3cdc4176638c Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 42814
diff changeset
   519
lemma some_collect:
37493
2377d246a631 Quotient package now uses Partial Equivalence instead place of equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 37049
diff changeset
   520
  assumes "R r r"
44204
3cdc4176638c Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 42814
diff changeset
   521
  shows "R (SOME x. x \<in> Collect (R r)) = R r"
3cdc4176638c Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 42814
diff changeset
   522
  apply simp
3cdc4176638c Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 42814
diff changeset
   523
  by (metis assms exE_some equivp[simplified part_equivp_def])
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   524
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   525
lemma Quotient:
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   526
  shows "Quotient3 R abs rep"
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   527
  unfolding Quotient3_def abs_def rep_def
37493
2377d246a631 Quotient package now uses Partial Equivalence instead place of equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 37049
diff changeset
   528
  proof (intro conjI allI)
2377d246a631 Quotient package now uses Partial Equivalence instead place of equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 37049
diff changeset
   529
    fix a r s
44204
3cdc4176638c Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 42814
diff changeset
   530
    show x: "R (SOME x. x \<in> Rep a) (SOME x. x \<in> Rep a)" proof -
3cdc4176638c Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 42814
diff changeset
   531
      obtain x where r: "R x x" and rep: "Rep a = Collect (R x)" using rep_prop[of a] by auto
3cdc4176638c Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 42814
diff changeset
   532
      have "R (SOME x. x \<in> Rep a) x"  using r rep some_collect by metis
3cdc4176638c Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 42814
diff changeset
   533
      then have "R x (SOME x. x \<in> Rep a)" using part_equivp_symp[OF equivp] by fast
3cdc4176638c Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 42814
diff changeset
   534
      then show "R (SOME x. x \<in> Rep a) (SOME x. x \<in> Rep a)"
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
   535
        using part_equivp_transp[OF equivp] by (metis \<open>R (SOME x. x \<in> Rep a) x\<close>)
37493
2377d246a631 Quotient package now uses Partial Equivalence instead place of equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 37049
diff changeset
   536
    qed
44204
3cdc4176638c Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 42814
diff changeset
   537
    have "Collect (R (SOME x. x \<in> Rep a)) = (Rep a)" by (metis some_collect rep_prop)
3cdc4176638c Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 42814
diff changeset
   538
    then show "Abs (Collect (R (SOME x. x \<in> Rep a))) = a" using rep_inverse by auto
3cdc4176638c Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 42814
diff changeset
   539
    have "R r r \<Longrightarrow> R s s \<Longrightarrow> Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> R r = R s"
44242
a5cb6aa77ffc avoid Collect_def in proof
haftmann
parents: 44204
diff changeset
   540
    proof -
a5cb6aa77ffc avoid Collect_def in proof
haftmann
parents: 44204
diff changeset
   541
      assume "R r r" and "R s s"
a5cb6aa77ffc avoid Collect_def in proof
haftmann
parents: 44204
diff changeset
   542
      then have "Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> Collect (R r) = Collect (R s)"
a5cb6aa77ffc avoid Collect_def in proof
haftmann
parents: 44204
diff changeset
   543
        by (metis abs_inverse)
a5cb6aa77ffc avoid Collect_def in proof
haftmann
parents: 44204
diff changeset
   544
      also have "Collect (R r) = Collect (R s) \<longleftrightarrow> (\<lambda>A x. x \<in> A) (Collect (R r)) = (\<lambda>A x. x \<in> A) (Collect (R s))"
a5cb6aa77ffc avoid Collect_def in proof
haftmann
parents: 44204
diff changeset
   545
        by rule simp_all
a5cb6aa77ffc avoid Collect_def in proof
haftmann
parents: 44204
diff changeset
   546
      finally show "Abs (Collect (R r)) = Abs (Collect (R s)) \<longleftrightarrow> R r = R s" by simp
a5cb6aa77ffc avoid Collect_def in proof
haftmann
parents: 44204
diff changeset
   547
    qed
44204
3cdc4176638c Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 42814
diff changeset
   548
    then show "R r s \<longleftrightarrow> R r r \<and> R s s \<and> (Abs (Collect (R r)) = Abs (Collect (R s)))"
3cdc4176638c Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 42814
diff changeset
   549
      using equivp[simplified part_equivp_def] by metis
3cdc4176638c Quotient Package: make quotient_type work with separate set type
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 42814
diff changeset
   550
    qed
44242
a5cb6aa77ffc avoid Collect_def in proof
haftmann
parents: 44204
diff changeset
   551
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   552
end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   553
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
   554
subsection \<open>Quotient composition\<close>
47096
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47094
diff changeset
   555
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   556
lemma OOO_quotient3:
47096
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47094
diff changeset
   557
  fixes R1 :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47094
diff changeset
   558
  fixes Abs1 :: "'a \<Rightarrow> 'b" and Rep1 :: "'b \<Rightarrow> 'a"
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47094
diff changeset
   559
  fixes Abs2 :: "'b \<Rightarrow> 'c" and Rep2 :: "'c \<Rightarrow> 'b"
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47094
diff changeset
   560
  fixes R2' :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47094
diff changeset
   561
  fixes R2 :: "'b \<Rightarrow> 'b \<Rightarrow> bool"
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   562
  assumes R1: "Quotient3 R1 Abs1 Rep1"
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   563
  assumes R2: "Quotient3 R2 Abs2 Rep2"
47096
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47094
diff changeset
   564
  assumes Abs1: "\<And>x y. R2' x y \<Longrightarrow> R1 x x \<Longrightarrow> R1 y y \<Longrightarrow> R2 (Abs1 x) (Abs1 y)"
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47094
diff changeset
   565
  assumes Rep1: "\<And>x y. R2 x y \<Longrightarrow> R2' (Rep1 x) (Rep1 y)"
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   566
  shows "Quotient3 (R1 OO R2' OO R1) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2)"
68616
cedf3480fdad de-applying (mostly Quotient)
paulson <lp15@cam.ac.uk>
parents: 68615
diff changeset
   567
proof -
71262
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   568
  have *: "(R1 OOO R2') r r \<and> (R1 OOO R2') s s \<and> (Abs2 \<circ> Abs1) r = (Abs2 \<circ> Abs1) s
68616
cedf3480fdad de-applying (mostly Quotient)
paulson <lp15@cam.ac.uk>
parents: 68615
diff changeset
   569
           \<longleftrightarrow> (R1 OOO R2') r s" for r s
71627
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   570
  proof (intro iffI conjI; clarify) 
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   571
    show "(R1 OOO R2') r s"
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   572
      if r: "R1 r a" "R2' a b" "R1 b r" and eq: "(Abs2 \<circ> Abs1) r = (Abs2 \<circ> Abs1) s" 
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   573
        and s: "R1 s c" "R2' c d" "R1 d s" for a b c d
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   574
    proof -
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   575
      have "R1 r (Rep1 (Abs1 r))"
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   576
        using r Quotient3_refl1 R1 rep_abs_rsp by fastforce
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   577
      moreover have "R2' (Rep1 (Abs1 r)) (Rep1 (Abs1 s))"
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   578
        using that
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   579
        apply (simp add: )
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   580
        apply (metis (full_types) Rep1 Abs1 Quotient3_rel R2 Quotient3_refl1 [OF R1] Quotient3_refl2 [OF R1] Quotient3_rel_abs [OF R1])
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   581
        done
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   582
      moreover have "R1 (Rep1 (Abs1 s)) s"
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   583
        by (metis s Quotient3_rel R1 rep_abs_rsp_left)
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   584
      ultimately show ?thesis
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   585
        by (metis relcomppI)
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   586
    qed
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   587
  next
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   588
    fix x y
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   589
    assume xy: "R1 r x" "R2' x y" "R1 y s"
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   590
    then have "R2 (Abs1 x) (Abs1 y)"
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   591
      by (iprover dest: Abs1 elim: Quotient3_refl1 [OF R1] Quotient3_refl2 [OF R1])
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   592
    then have "R2' (Rep1 (Abs1 x)) (Rep1 (Abs1 x))" "R2' (Rep1 (Abs1 y)) (Rep1 (Abs1 y))"
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   593
      by (simp_all add: Quotient3_refl1 [OF R2] Quotient3_refl2 [OF R2] Rep1)
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   594
    with \<open>R1 r x\<close> \<open>R1 y s\<close> show "(R1 OOO R2') r r" "(R1 OOO R2') s s"
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   595
      by (metis (full_types) Quotient3_def R1 relcompp.relcompI)+
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   596
    show "(Abs2 \<circ> Abs1) r = (Abs2 \<circ> Abs1) s"
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   597
      using xy by simp (metis (full_types) Abs1 Quotient3_rel R1 R2)
2a24c2015a61 more ugly old proofs
paulson <lp15@cam.ac.uk>
parents: 71494
diff changeset
   598
  qed
68616
cedf3480fdad de-applying (mostly Quotient)
paulson <lp15@cam.ac.uk>
parents: 68615
diff changeset
   599
  show ?thesis
cedf3480fdad de-applying (mostly Quotient)
paulson <lp15@cam.ac.uk>
parents: 68615
diff changeset
   600
    apply (rule Quotient3I)
cedf3480fdad de-applying (mostly Quotient)
paulson <lp15@cam.ac.uk>
parents: 68615
diff changeset
   601
    using * apply (simp_all add: o_def Quotient3_abs_rep [OF R2] Quotient3_abs_rep [OF R1])
cedf3480fdad de-applying (mostly Quotient)
paulson <lp15@cam.ac.uk>
parents: 68615
diff changeset
   602
    apply (metis Quotient3_rep_reflp R1 R2 Rep1 relcompp.relcompI)
cedf3480fdad de-applying (mostly Quotient)
paulson <lp15@cam.ac.uk>
parents: 68615
diff changeset
   603
    done
cedf3480fdad de-applying (mostly Quotient)
paulson <lp15@cam.ac.uk>
parents: 68615
diff changeset
   604
qed
47096
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47094
diff changeset
   605
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   606
lemma OOO_eq_quotient3:
47096
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47094
diff changeset
   607
  fixes R1 :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47094
diff changeset
   608
  fixes Abs1 :: "'a \<Rightarrow> 'b" and Rep1 :: "'b \<Rightarrow> 'a"
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47094
diff changeset
   609
  fixes Abs2 :: "'b \<Rightarrow> 'c" and Rep2 :: "'c \<Rightarrow> 'b"
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   610
  assumes R1: "Quotient3 R1 Abs1 Rep1"
67399
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 67091
diff changeset
   611
  assumes R2: "Quotient3 (=) Abs2 Rep2"
eab6ce8368fa ran isabelle update_op on all sources
nipkow
parents: 67091
diff changeset
   612
  shows "Quotient3 (R1 OOO (=)) (Abs2 \<circ> Abs1) (Rep1 \<circ> Rep2)"
47096
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47094
diff changeset
   613
using assms
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   614
by (rule OOO_quotient3) auto
47096
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47094
diff changeset
   615
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
   616
subsection \<open>Quotient3 to Quotient\<close>
47362
b1f099bdfbba connect the Quotient package to the Lifting package
kuncar
parents: 47361
diff changeset
   617
b1f099bdfbba connect the Quotient package to the Lifting package
kuncar
parents: 47361
diff changeset
   618
lemma Quotient3_to_Quotient:
b1f099bdfbba connect the Quotient package to the Lifting package
kuncar
parents: 47361
diff changeset
   619
assumes "Quotient3 R Abs Rep"
b1f099bdfbba connect the Quotient package to the Lifting package
kuncar
parents: 47361
diff changeset
   620
and "T \<equiv> \<lambda>x y. R x x \<and> Abs x = y"
b1f099bdfbba connect the Quotient package to the Lifting package
kuncar
parents: 47361
diff changeset
   621
shows "Quotient R Abs Rep T"
b1f099bdfbba connect the Quotient package to the Lifting package
kuncar
parents: 47361
diff changeset
   622
using assms unfolding Quotient3_def by (intro QuotientI) blast+
47096
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47094
diff changeset
   623
47362
b1f099bdfbba connect the Quotient package to the Lifting package
kuncar
parents: 47361
diff changeset
   624
lemma Quotient3_to_Quotient_equivp:
b1f099bdfbba connect the Quotient package to the Lifting package
kuncar
parents: 47361
diff changeset
   625
assumes q: "Quotient3 R Abs Rep"
b1f099bdfbba connect the Quotient package to the Lifting package
kuncar
parents: 47361
diff changeset
   626
and T_def: "T \<equiv> \<lambda>x y. Abs x = y"
b1f099bdfbba connect the Quotient package to the Lifting package
kuncar
parents: 47361
diff changeset
   627
and eR: "equivp R"
b1f099bdfbba connect the Quotient package to the Lifting package
kuncar
parents: 47361
diff changeset
   628
shows "Quotient R Abs Rep T"
b1f099bdfbba connect the Quotient package to the Lifting package
kuncar
parents: 47361
diff changeset
   629
proof (intro QuotientI)
b1f099bdfbba connect the Quotient package to the Lifting package
kuncar
parents: 47361
diff changeset
   630
  fix a
b1f099bdfbba connect the Quotient package to the Lifting package
kuncar
parents: 47361
diff changeset
   631
  show "Abs (Rep a) = a" using q by(rule Quotient3_abs_rep)
b1f099bdfbba connect the Quotient package to the Lifting package
kuncar
parents: 47361
diff changeset
   632
next
b1f099bdfbba connect the Quotient package to the Lifting package
kuncar
parents: 47361
diff changeset
   633
  fix a
b1f099bdfbba connect the Quotient package to the Lifting package
kuncar
parents: 47361
diff changeset
   634
  show "R (Rep a) (Rep a)" using q by(rule Quotient3_rep_reflp)
b1f099bdfbba connect the Quotient package to the Lifting package
kuncar
parents: 47361
diff changeset
   635
next
b1f099bdfbba connect the Quotient package to the Lifting package
kuncar
parents: 47361
diff changeset
   636
  fix r s
b1f099bdfbba connect the Quotient package to the Lifting package
kuncar
parents: 47361
diff changeset
   637
  show "R r s = (R r r \<and> R s s \<and> Abs r = Abs s)" using q by(rule Quotient3_rel[symmetric])
b1f099bdfbba connect the Quotient package to the Lifting package
kuncar
parents: 47361
diff changeset
   638
next
b1f099bdfbba connect the Quotient package to the Lifting package
kuncar
parents: 47361
diff changeset
   639
  show "T = (\<lambda>x y. R x x \<and> Abs x = y)" using T_def equivp_reflp[OF eR] by simp
47096
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47094
diff changeset
   640
qed
3ea48c19673e generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
kuncar
parents: 47094
diff changeset
   641
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
   642
subsection \<open>ML setup\<close>
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   643
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
   644
text \<open>Auxiliary data for the quotient package\<close>
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   645
57960
ee1ba4848896 updated to named_theorems;
wenzelm
parents: 56073
diff changeset
   646
named_theorems quot_equiv "equivalence relation theorems"
59028
df7476e79558 named_theorems: multiple args;
wenzelm
parents: 58889
diff changeset
   647
  and quot_respect "respectfulness theorems"
df7476e79558 named_theorems: multiple args;
wenzelm
parents: 58889
diff changeset
   648
  and quot_preserve "preservation theorems"
df7476e79558 named_theorems: multiple args;
wenzelm
parents: 58889
diff changeset
   649
  and id_simps "identity simp rules for maps"
df7476e79558 named_theorems: multiple args;
wenzelm
parents: 58889
diff changeset
   650
  and quot_thm "quotient theorems"
69605
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 68616
diff changeset
   651
ML_file \<open>Tools/Quotient/quotient_info.ML\<close>
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   652
55945
e96383acecf9 renamed 'fun_rel' to 'rel_fun'
blanchet
parents: 54867
diff changeset
   653
declare [[mapQ3 "fun" = (rel_fun, fun_quotient3)]]
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   654
47308
9caab698dbe4 new package Lifting - initial commit
kuncar
parents: 47105
diff changeset
   655
lemmas [quot_thm] = fun_quotient3
44553
4d39b032a021 avoid intermixing set and predicates; dropped lemmas mem_rsp and mem_prs (now in Quotient_Set.thy)
haftmann
parents: 44413
diff changeset
   656
lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp id_rsp
4d39b032a021 avoid intermixing set and predicates; dropped lemmas mem_rsp and mem_prs (now in Quotient_Set.thy)
haftmann
parents: 44413
diff changeset
   657
lemmas [quot_preserve] = if_prs o_prs let_prs id_prs
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   658
lemmas [quot_equiv] = identity_equivp
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   659
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   660
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
   661
text \<open>Lemmas about simplifying id's.\<close>
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   662
lemmas [id_simps] =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   663
  id_def[symmetric]
40602
91e583511113 map_fun combinator in theory Fun
haftmann
parents: 40466
diff changeset
   664
  map_fun_id
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   665
  id_apply
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   666
  id_o
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   667
  o_id
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   668
  eq_comp_r
44413
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 44242
diff changeset
   669
  vimage_id
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   670
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
   671
text \<open>Translation functions for the lifting process.\<close>
69605
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 68616
diff changeset
   672
ML_file \<open>Tools/Quotient/quotient_term.ML\<close>
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   673
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   674
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
   675
text \<open>Definitions of the quotient types.\<close>
69605
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 68616
diff changeset
   676
ML_file \<open>Tools/Quotient/quotient_type.ML\<close>
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   677
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   678
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
   679
text \<open>Definitions for quotient constants.\<close>
69605
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 68616
diff changeset
   680
ML_file \<open>Tools/Quotient/quotient_def.ML\<close>
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   681
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   682
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
   683
text \<open>
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   684
  An auxiliary constant for recording some information
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   685
  about the lifted theorem in a tactic.
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
   686
\<close>
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   687
definition
40466
c6587375088e type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions
haftmann
parents: 40031
diff changeset
   688
  Quot_True :: "'a \<Rightarrow> bool"
c6587375088e type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions
haftmann
parents: 40031
diff changeset
   689
where
c6587375088e type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions
haftmann
parents: 40031
diff changeset
   690
  "Quot_True x \<longleftrightarrow> True"
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   691
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   692
lemma
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   693
  shows QT_all: "Quot_True (All P) \<Longrightarrow> Quot_True P"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   694
  and   QT_ex:  "Quot_True (Ex P) \<Longrightarrow> Quot_True P"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   695
  and   QT_ex1: "Quot_True (Ex1 P) \<Longrightarrow> Quot_True P"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   696
  and   QT_lam: "Quot_True (\<lambda>x. P x) \<Longrightarrow> (\<And>x. Quot_True (P x))"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   697
  and   QT_ext: "(\<And>x. Quot_True (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (Quot_True a \<Longrightarrow> f = g)"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   698
  by (simp_all add: Quot_True_def ext)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   699
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   700
lemma QT_imp: "Quot_True a \<equiv> Quot_True b"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   701
  by (simp add: Quot_True_def)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   702
63343
fb5d8a50c641 bundle lifting_syntax;
wenzelm
parents: 61799
diff changeset
   703
context includes lifting_syntax
53011
aeee0a4be6cf introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents: 51112
diff changeset
   704
begin
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   705
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
   706
text \<open>Tactics for proving the lifted theorems\<close>
69605
a96320074298 isabelle update -u path_cartouches;
wenzelm
parents: 68616
diff changeset
   707
ML_file \<open>Tools/Quotient/quotient_tacs.ML\<close>
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   708
53011
aeee0a4be6cf introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents: 51112
diff changeset
   709
end
aeee0a4be6cf introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents: 51112
diff changeset
   710
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
   711
subsection \<open>Methods / Interface\<close>
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   712
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   713
method_setup lifting =
71262
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   714
  \<open>Attrib.thms >> (fn thms => fn ctxt =>
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
   715
       SIMPLE_METHOD' (Quotient_Tacs.lift_tac ctxt [] thms))\<close>
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
   716
  \<open>lift theorems to quotient types\<close>
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   717
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   718
method_setup lifting_setup =
71262
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   719
  \<open>Attrib.thm >> (fn thm => fn ctxt =>
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
   720
       SIMPLE_METHOD' (Quotient_Tacs.lift_procedure_tac ctxt [] thm))\<close>
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
   721
  \<open>set up the three goals for the quotient lifting procedure\<close>
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   722
37593
2505feaf2d70 separated the lifting and descending procedures in the quotient package
Christian Urban <urbanc@in.tum.de>
parents: 37564
diff changeset
   723
method_setup descending =
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
   724
  \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.descend_tac ctxt []))\<close>
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
   725
  \<open>decend theorems to the raw level\<close>
37593
2505feaf2d70 separated the lifting and descending procedures in the quotient package
Christian Urban <urbanc@in.tum.de>
parents: 37564
diff changeset
   726
2505feaf2d70 separated the lifting and descending procedures in the quotient package
Christian Urban <urbanc@in.tum.de>
parents: 37564
diff changeset
   727
method_setup descending_setup =
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
   728
  \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.descend_procedure_tac ctxt []))\<close>
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
   729
  \<open>set up the three goals for the decending theorems\<close>
37593
2505feaf2d70 separated the lifting and descending procedures in the quotient package
Christian Urban <urbanc@in.tum.de>
parents: 37564
diff changeset
   730
45782
f82020ca3248 added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents: 45680
diff changeset
   731
method_setup partiality_descending =
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
   732
  \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.partiality_descend_tac ctxt []))\<close>
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
   733
  \<open>decend theorems to the raw level\<close>
45782
f82020ca3248 added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents: 45680
diff changeset
   734
f82020ca3248 added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents: 45680
diff changeset
   735
method_setup partiality_descending_setup =
71262
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   736
  \<open>Scan.succeed (fn ctxt =>
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
   737
       SIMPLE_METHOD' (Quotient_Tacs.partiality_descend_procedure_tac ctxt []))\<close>
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
   738
  \<open>set up the three goals for the decending theorems\<close>
45782
f82020ca3248 added a specific tactic and method that deal with partial equivalence relations
Christian Urban <urbanc@in.tum.de>
parents: 45680
diff changeset
   739
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   740
method_setup regularize =
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
   741
  \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.regularize_tac ctxt))\<close>
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
   742
  \<open>prove the regularization goals from the quotient lifting procedure\<close>
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   743
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   744
method_setup injection =
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
   745
  \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.all_injection_tac ctxt))\<close>
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
   746
  \<open>prove the rep/abs injection goals from the quotient lifting procedure\<close>
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   747
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   748
method_setup cleaning =
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
   749
  \<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (Quotient_Tacs.clean_tac ctxt))\<close>
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
   750
  \<open>prove the cleaning goals from the quotient lifting procedure\<close>
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   751
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   752
attribute_setup quot_lifted =
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
   753
  \<open>Scan.succeed Quotient_Tacs.lifted_attrib\<close>
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 59028
diff changeset
   754
  \<open>lift theorems to quotient types\<close>
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   755
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   756
no_notation
53011
aeee0a4be6cf introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
kuncar
parents: 51112
diff changeset
   757
  rel_conj (infixr "OOO" 75)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   758
71262
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   759
section \<open>Lifting of BNFs\<close>
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   760
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   761
lemma sum_insert_Inl_unit: "x \<in> A \<Longrightarrow> (\<And>y. x = Inr y \<Longrightarrow> Inr y \<in> B) \<Longrightarrow> x \<in> insert (Inl ()) B"
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   762
  by (cases x) (simp_all)
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   763
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   764
lemma lift_sum_unit_vimage_commute:
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   765
  "insert (Inl ()) (Inr ` f -` A) = map_sum id f -` insert (Inl ()) (Inr ` A)"
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   766
  by (auto simp: map_sum_def split: sum.splits)
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   767
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   768
lemma insert_Inl_int_map_sum_unit: "insert (Inl ()) A \<inter> range (map_sum id f) \<noteq> {}"
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   769
  by (auto simp: map_sum_def split: sum.splits)
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   770
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   771
lemma image_map_sum_unit_subset:
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   772
  "A \<subseteq> insert (Inl ()) (Inr ` B) \<Longrightarrow> map_sum id f ` A \<subseteq> insert (Inl ()) (Inr ` f ` B)"
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   773
  by auto
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   774
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   775
lemma subset_lift_sum_unitD: "A \<subseteq> insert (Inl ()) (Inr ` B) \<Longrightarrow> Inr x \<in> A \<Longrightarrow> x \<in> B"
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   776
  unfolding insert_def by auto
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   777
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   778
lemma UNIV_sum_unit_conv: "insert (Inl ()) (range Inr) = UNIV"
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   779
  unfolding UNIV_sum UNIV_unit image_insert image_empty Un_insert_left sup_bot.left_neutral..
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   780
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   781
lemma subset_vimage_image_subset: "A \<subseteq> f -` B \<Longrightarrow> f ` A \<subseteq> B"
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   782
  by auto
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   783
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   784
lemma relcompp_mem_Grp_neq_bot:
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   785
  "A \<inter> range f \<noteq> {} \<Longrightarrow> (\<lambda>x y. x \<in> A \<and> y \<in> A) OO (Grp UNIV f)\<inverse>\<inverse> \<noteq> bot"
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   786
  unfolding Grp_def relcompp_apply fun_eq_iff by blast
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   787
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   788
lemma comp_projr_Inr: "projr \<circ> Inr = id"
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   789
  by auto
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   790
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   791
lemma in_rel_sum_in_image_projr:
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   792
  "B \<subseteq> {(x,y). rel_sum ((=) :: unit \<Rightarrow> unit \<Rightarrow> bool) A x y} \<Longrightarrow>
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   793
   Inr ` C = fst ` B \<Longrightarrow> snd ` B = Inr ` D \<Longrightarrow> map_prod projr projr ` B \<subseteq> {(x,y). A x y}"
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   794
  by (force simp: projr_def image_iff dest!: spec[of _ "Inl ()"]  split: sum.splits)
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   795
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   796
lemma subset_rel_sumI: "B \<subseteq> {(x,y). A x y} \<Longrightarrow> rel_sum ((=) :: unit => unit => bool) A
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   797
    (if x \<in> B then Inr (fst x) else Inl ())
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   798
    (if x \<in> B then Inr (snd x) else Inl ())"
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   799
  by auto
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   800
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   801
lemma relcompp_eq_Grp_neq_bot: "(=) OO (Grp UNIV f)\<inverse>\<inverse> \<noteq> bot"
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   802
  unfolding Grp_def relcompp_apply fun_eq_iff by blast
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   803
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   804
lemma rel_fun_rel_OO1: "(rel_fun Q (rel_fun R (=))) A B \<Longrightarrow> conversep Q OO A OO R \<le> B"
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   805
  by (auto simp: rel_fun_def)
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   806
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   807
lemma rel_fun_rel_OO2: "(rel_fun Q (rel_fun R (=))) A B \<Longrightarrow> Q OO B OO conversep R \<le> A"
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   808
  by (auto simp: rel_fun_def)
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   809
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   810
lemma rel_sum_eq2_nonempty: "rel_sum (=) A OO rel_sum (=) B \<noteq> bot"
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   811
  by (auto simp: fun_eq_iff relcompp_apply intro!: exI[of _ "Inl _"])
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   812
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   813
lemma rel_sum_eq3_nonempty: "rel_sum (=) A OO (rel_sum (=) B OO rel_sum (=) C) \<noteq> bot"
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   814
  by (auto simp: fun_eq_iff relcompp_apply intro!: exI[of _ "Inl _"])
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   815
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   816
lemma hypsubst: "A = B \<Longrightarrow> x \<in> B \<Longrightarrow> (x \<in> A \<Longrightarrow> P) \<Longrightarrow> P" by simp
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   817
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   818
lemma Quotient_crel_quotient: "Quotient R Abs Rep T \<Longrightarrow> equivp R \<Longrightarrow> T \<equiv> (\<lambda>x y. Abs x = y)"
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   819
  by (drule Quotient_cr_rel) (auto simp: fun_eq_iff equivp_reflp intro!: eq_reflection)
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   820
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   821
lemma Quotient_crel_typedef: "Quotient (eq_onp P) Abs Rep T \<Longrightarrow> T \<equiv> (\<lambda>x y. x = Rep y)"
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   822
  unfolding Quotient_def
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   823
  by (auto 0 4 simp: fun_eq_iff eq_onp_def intro: sym intro!: eq_reflection)
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   824
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   825
lemma Quotient_crel_typecopy: "Quotient (=) Abs Rep T \<Longrightarrow> T \<equiv> (\<lambda>x y. x = Rep y)"
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   826
  by (subst (asm) eq_onp_True[symmetric]) (rule Quotient_crel_typedef)
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   827
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   828
lemma equivp_add_relconj:
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   829
  assumes equiv: "equivp R" "equivp R'" and le: "S OO T OO U \<le> R OO STU OO R'"
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   830
  shows "R OO S OO T OO U OO R' \<le> R OO STU OO R'"
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   831
proof -
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   832
  have trans: "R OO R \<le> R" "R' OO R' \<le> R'"
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   833
    using equiv unfolding equivp_reflp_symp_transp transp_relcompp by blast+
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   834
  have "R OO S OO T OO U OO R' = R OO (S OO T OO U) OO R'"
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   835
    unfolding relcompp_assoc ..
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   836
  also have "\<dots> \<le> R OO (R OO STU OO R') OO R'"
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   837
    by (intro le relcompp_mono order_refl)
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   838
  also have "\<dots> \<le> (R OO R) OO STU OO (R' OO R')"
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   839
    unfolding relcompp_assoc ..
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   840
  also have "\<dots> \<le> R OO STU OO R'"
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   841
    by (intro trans relcompp_mono order_refl)
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   842
  finally show ?thesis .
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   843
qed
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   844
71354
c71a44893645 eliminated one redundant proof obligation in lift_bnf for quotients
traytel
parents: 71262
diff changeset
   845
lemma Grp_conversep_eq_onp: "((BNF_Def.Grp UNIV f)\<inverse>\<inverse> OO BNF_Def.Grp UNIV f) = eq_onp (\<lambda>x. x \<in> range f)"
c71a44893645 eliminated one redundant proof obligation in lift_bnf for quotients
traytel
parents: 71262
diff changeset
   846
  by (auto simp: fun_eq_iff Grp_def eq_onp_def image_iff)
c71a44893645 eliminated one redundant proof obligation in lift_bnf for quotients
traytel
parents: 71262
diff changeset
   847
c71a44893645 eliminated one redundant proof obligation in lift_bnf for quotients
traytel
parents: 71262
diff changeset
   848
lemma Grp_conversep_nonempty: "(BNF_Def.Grp UNIV f)\<inverse>\<inverse> OO BNF_Def.Grp UNIV f \<noteq> bot"
c71a44893645 eliminated one redundant proof obligation in lift_bnf for quotients
traytel
parents: 71262
diff changeset
   849
  by (auto simp: fun_eq_iff Grp_def)
c71a44893645 eliminated one redundant proof obligation in lift_bnf for quotients
traytel
parents: 71262
diff changeset
   850
c71a44893645 eliminated one redundant proof obligation in lift_bnf for quotients
traytel
parents: 71262
diff changeset
   851
lemma relcomppI2: "r a b \<Longrightarrow> s b c \<Longrightarrow> t c d \<Longrightarrow> (r OO s OO t) a d"
c71a44893645 eliminated one redundant proof obligation in lift_bnf for quotients
traytel
parents: 71262
diff changeset
   852
  by (auto)
c71a44893645 eliminated one redundant proof obligation in lift_bnf for quotients
traytel
parents: 71262
diff changeset
   853
c71a44893645 eliminated one redundant proof obligation in lift_bnf for quotients
traytel
parents: 71262
diff changeset
   854
lemma rel_conj_eq_onp: "equivp R \<Longrightarrow> rel_conj R (eq_onp P) \<le> R"
c71a44893645 eliminated one redundant proof obligation in lift_bnf for quotients
traytel
parents: 71262
diff changeset
   855
  by (auto simp: eq_onp_def transp_def equivp_def)
c71a44893645 eliminated one redundant proof obligation in lift_bnf for quotients
traytel
parents: 71262
diff changeset
   856
71393
fce780f9c9c6 new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents: 71354
diff changeset
   857
lemma Quotient_Quotient3: "Quotient R Abs Rep T \<Longrightarrow> Quotient3 R Abs Rep"
fce780f9c9c6 new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents: 71354
diff changeset
   858
  unfolding Quotient_def Quotient3_def by blast
fce780f9c9c6 new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents: 71354
diff changeset
   859
71494
cbe0b6b0bed8 tuned lift_bnf's user interface for quotients
traytel
parents: 71393
diff changeset
   860
lemma Quotient_reflp_imp_equivp: "Quotient R Abs Rep T \<Longrightarrow> reflp R \<Longrightarrow> equivp R"
cbe0b6b0bed8 tuned lift_bnf's user interface for quotients
traytel
parents: 71393
diff changeset
   861
  using Quotient_symp Quotient_transp equivpI by blast
cbe0b6b0bed8 tuned lift_bnf's user interface for quotients
traytel
parents: 71393
diff changeset
   862
cbe0b6b0bed8 tuned lift_bnf's user interface for quotients
traytel
parents: 71393
diff changeset
   863
lemma Quotient_eq_onp_typedef:
cbe0b6b0bed8 tuned lift_bnf's user interface for quotients
traytel
parents: 71393
diff changeset
   864
  "Quotient (eq_onp P) Abs Rep cr \<Longrightarrow> type_definition Rep Abs {x. P x}"
cbe0b6b0bed8 tuned lift_bnf's user interface for quotients
traytel
parents: 71393
diff changeset
   865
  unfolding Quotient_def eq_onp_def
cbe0b6b0bed8 tuned lift_bnf's user interface for quotients
traytel
parents: 71393
diff changeset
   866
  by unfold_locales auto
cbe0b6b0bed8 tuned lift_bnf's user interface for quotients
traytel
parents: 71393
diff changeset
   867
cbe0b6b0bed8 tuned lift_bnf's user interface for quotients
traytel
parents: 71393
diff changeset
   868
lemma Quotient_eq_onp_type_copy:
cbe0b6b0bed8 tuned lift_bnf's user interface for quotients
traytel
parents: 71393
diff changeset
   869
  "Quotient (=) Abs Rep cr \<Longrightarrow> type_definition Rep Abs UNIV"
cbe0b6b0bed8 tuned lift_bnf's user interface for quotients
traytel
parents: 71393
diff changeset
   870
  unfolding Quotient_def eq_onp_def
cbe0b6b0bed8 tuned lift_bnf's user interface for quotients
traytel
parents: 71393
diff changeset
   871
  by unfold_locales auto
71393
fce780f9c9c6 new examples of BNF lifting across quotients using a new theory of confluence,
traytel
parents: 71354
diff changeset
   872
71262
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   873
ML_file "Tools/BNF/bnf_lift.ML"
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   874
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   875
hide_fact
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   876
  sum_insert_Inl_unit lift_sum_unit_vimage_commute insert_Inl_int_map_sum_unit
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   877
  image_map_sum_unit_subset subset_lift_sum_unitD UNIV_sum_unit_conv subset_vimage_image_subset
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   878
  relcompp_mem_Grp_neq_bot comp_projr_Inr in_rel_sum_in_image_projr subset_rel_sumI
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   879
  relcompp_eq_Grp_neq_bot rel_fun_rel_OO1 rel_fun_rel_OO2 rel_sum_eq2_nonempty rel_sum_eq3_nonempty
71354
c71a44893645 eliminated one redundant proof obligation in lift_bnf for quotients
traytel
parents: 71262
diff changeset
   880
  hypsubst equivp_add_relconj Grp_conversep_eq_onp Grp_conversep_nonempty relcomppI2 rel_conj_eq_onp
71494
cbe0b6b0bed8 tuned lift_bnf's user interface for quotients
traytel
parents: 71393
diff changeset
   881
  Quotient_reflp_imp_equivp Quotient_Quotient3
71262
a30278c8585f extension of lift_bnf to support quotient types
traytel
parents: 69990
diff changeset
   882
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   883
end