Quotient-Paper/Paper.thy
author Christian Urban <urbanc@in.tum.de>
Mon, 07 Jun 2010 11:33:00 +0200
changeset 2213 231a20534950
parent 2212 79cebcc230d6
child 2214 02e03d4287ec
permissions -rw-r--r--
improved abstract, some tuning
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2208
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
     1
(* How to change the notation for \<lbrakk> \<rbrakk> meta-level implications? *)
2195
0c1dcdefb515 Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2194
diff changeset
     2
1975
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     3
(*<*)
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     4
theory Paper
2183
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2182
diff changeset
     5
imports "Quotient"
1975
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     6
        "LaTeXsugar"
2186
762a739c9eb4 added FSet to the correct paper
Christian Urban <urbanc@in.tum.de>
parents: 2183
diff changeset
     7
        "../Nominal/FSet"
1975
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     8
begin
1994
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1978
diff changeset
     9
2208
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
    10
print_syntax
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
    11
1994
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1978
diff changeset
    12
notation (latex output)
2182
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
    13
  rel_conj ("_ OOO _" [53, 53] 52)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
    14
and
2208
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
    15
  "op -->" (infix "\<rightarrow>" 100)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
    16
and
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
    17
  "==>" (infix "\<Rightarrow>" 100)
2182
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
    18
and
2208
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
    19
  fun_map (infix "\<longrightarrow>" 51)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
    20
and
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
    21
  fun_rel (infix "\<Longrightarrow>" 51)
2188
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
    22
and
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
    23
  list_eq (infix "\<approx>" 50) (* Not sure if we want this notation...? *)
1994
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1978
diff changeset
    24
2182
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
    25
ML {*
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
    26
fun nth_conj n (_, r) = nth (HOLogic.dest_conj r) n;
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
    27
fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t =>
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
    28
  let
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
    29
    val concl =
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
    30
      Object_Logic.drop_judgment (ProofContext.theory_of ctxt) (Logic.strip_imp_concl t)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
    31
  in
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
    32
    case concl of (_ $ l $ r) => proj (l, r)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
    33
    | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl)
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
    34
  end);
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
    35
*}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
    36
setup {*
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
    37
  Term_Style.setup "rhs1" (style_lhs_rhs (nth_conj 0)) #>
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
    38
  Term_Style.setup "rhs2" (style_lhs_rhs (nth_conj 1)) #>
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
    39
  Term_Style.setup "rhs3" (style_lhs_rhs (nth_conj 2))
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
    40
*}
1975
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    41
(*>*)
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    42
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    43
section {* Introduction *}
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    44
2102
200954544cae added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
parents: 1994
diff changeset
    45
text {* 
2205
69b4eb4b12c6 added larry's quote
Christian Urban <urbanc@in.tum.de>
parents: 2199
diff changeset
    46
   \begin{flushright}
69b4eb4b12c6 added larry's quote
Christian Urban <urbanc@in.tum.de>
parents: 2199
diff changeset
    47
  {\em ``Not using a [quotient] package has its advantages: we do not have to\\ 
69b4eb4b12c6 added larry's quote
Christian Urban <urbanc@in.tum.de>
parents: 2199
diff changeset
    48
    collect all the theorems we shall ever want into one giant list;''}\\
2213
231a20534950 improved abstract, some tuning
Christian Urban <urbanc@in.tum.de>
parents: 2212
diff changeset
    49
    Larry Paulson \cite{Paulson06}
2205
69b4eb4b12c6 added larry's quote
Christian Urban <urbanc@in.tum.de>
parents: 2199
diff changeset
    50
  \end{flushright}\smallskip
2103
e08e3c29dbc0 a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents: 2102
diff changeset
    51
e08e3c29dbc0 a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents: 2102
diff changeset
    52
  \noindent
2102
200954544cae added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
parents: 1994
diff changeset
    53
  Isabelle is a generic theorem prover in which many logics can be implemented. 
200954544cae added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
parents: 1994
diff changeset
    54
  The most widely used one, however, is
200954544cae added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
parents: 1994
diff changeset
    55
  Higher-Order Logic (HOL). This logic consists of a small number of 
200954544cae added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
parents: 1994
diff changeset
    56
  axioms and inference
200954544cae added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
parents: 1994
diff changeset
    57
  rules over a simply-typed term-language. Safe reasoning in HOL is ensured by two very restricted 
200954544cae added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
parents: 1994
diff changeset
    58
  mechanisms for extending the logic: one is the definition of new constants
200954544cae added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
parents: 1994
diff changeset
    59
  in terms of existing ones; the other is the introduction of new types
200954544cae added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
parents: 1994
diff changeset
    60
  by identifying non-empty subsets in existing types. It is well understood 
2213
231a20534950 improved abstract, some tuning
Christian Urban <urbanc@in.tum.de>
parents: 2212
diff changeset
    61
  to use both mechanisms for dealing with quotient constructions in HOL (see for example 
231a20534950 improved abstract, some tuning
Christian Urban <urbanc@in.tum.de>
parents: 2212
diff changeset
    62
  \cite{Paulson06}).
2102
200954544cae added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
parents: 1994
diff changeset
    63
  For example the integers in Isabelle/HOL are constructed by a quotient construction over 
200954544cae added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
parents: 1994
diff changeset
    64
  the type @{typ "nat \<times> nat"} and the equivalence relation
200954544cae added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
parents: 1994
diff changeset
    65
2182
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
    66
% I would avoid substraction for natural numbers.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
    67
2102
200954544cae added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
parents: 1994
diff changeset
    68
  @{text [display] "(n\<^isub>1, n\<^isub>2) \<approx> (m\<^isub>1, m\<^isub>2) \<equiv> n\<^isub>1 - n \<^isub>2 = m\<^isub>1 - m \<^isub>2"}
200954544cae added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
parents: 1994
diff changeset
    69
200954544cae added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
parents: 1994
diff changeset
    70
  \noindent
2103
e08e3c29dbc0 a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents: 2102
diff changeset
    71
  Similarly one can construct the type of finite sets by quotienting lists
e08e3c29dbc0 a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents: 2102
diff changeset
    72
  according to the equivalence relation
e08e3c29dbc0 a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents: 2102
diff changeset
    73
e08e3c29dbc0 a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents: 2102
diff changeset
    74
  @{text [display] "xs \<approx> ys \<equiv> (\<forall>x. x \<in> xs \<longleftrightarrow> x \<in> ys)"}
e08e3c29dbc0 a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents: 2102
diff changeset
    75
e08e3c29dbc0 a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents: 2102
diff changeset
    76
  \noindent
e08e3c29dbc0 a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents: 2102
diff changeset
    77
  where @{text "\<in>"} stands for membership in a list.
e08e3c29dbc0 a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents: 2102
diff changeset
    78
e08e3c29dbc0 a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents: 2102
diff changeset
    79
  The problem is that in order to start reasoning about, for example integers, 
e08e3c29dbc0 a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents: 2102
diff changeset
    80
  definitions and theorems need to be transferred, or \emph{lifted}, 
e08e3c29dbc0 a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents: 2102
diff changeset
    81
  from the ``raw'' type @{typ "nat \<times> nat"} to the quotient type @{typ int}. 
e08e3c29dbc0 a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents: 2102
diff changeset
    82
  This lifting usually requires a lot of tedious reasoning effort.
e08e3c29dbc0 a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents: 2102
diff changeset
    83
  The purpose of a \emph{quotient package} is to ease the lifting and automate
e08e3c29dbc0 a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents: 2102
diff changeset
    84
  the reasoning involved as much as possible. Such a package is a central
e08e3c29dbc0 a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents: 2102
diff changeset
    85
  component of the new version of Nominal Isabelle where representations 
e08e3c29dbc0 a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents: 2102
diff changeset
    86
  of alpha-equated terms are constructed according to specifications given by
e08e3c29dbc0 a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents: 2102
diff changeset
    87
  the user. 
2102
200954544cae added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
parents: 1994
diff changeset
    88
  
2103
e08e3c29dbc0 a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents: 2102
diff changeset
    89
  In the context of HOL, there have been several quotient packages (...). The
e08e3c29dbc0 a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents: 2102
diff changeset
    90
  most notable is the one by Homeier (...) implemented in HOL4. However, what is
e08e3c29dbc0 a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents: 2102
diff changeset
    91
  surprising, none of them can deal compositions of quotients, for example with 
e08e3c29dbc0 a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents: 2102
diff changeset
    92
  lifting theorems about @{text "concat"}:
2102
200954544cae added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
parents: 1994
diff changeset
    93
2190
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2189
diff changeset
    94
  @{thm [display] concat.simps(1)}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2189
diff changeset
    95
  @{thm [display] concat.simps(2)[no_vars]}
2183
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2182
diff changeset
    96
2103
e08e3c29dbc0 a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents: 2102
diff changeset
    97
  \noindent
2188
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
    98
  One would like to lift this definition to the operation:
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
    99
2190
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2189
diff changeset
   100
  @{thm [display] fconcat_empty[no_vars]}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2189
diff changeset
   101
  @{thm [display] fconcat_insert[no_vars]}
2102
200954544cae added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
parents: 1994
diff changeset
   102
2103
e08e3c29dbc0 a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents: 2102
diff changeset
   103
  \noindent
e08e3c29dbc0 a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents: 2102
diff changeset
   104
  What is special about this operation is that we have as input
e08e3c29dbc0 a bit for the introduction of the q-paper
Christian Urban <urbanc@in.tum.de>
parents: 2102
diff changeset
   105
  lists of lists which after lifting turn into finite sets of finite
2190
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2189
diff changeset
   106
  sets.
2102
200954544cae added some of the quotient literature; a bit more to the qpaper
Christian Urban <urbanc@in.tum.de>
parents: 1994
diff changeset
   107
*}
1975
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   108
1978
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   109
subsection {* Contributions *}
1975
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   110
1978
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   111
text {*
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   112
  We present the detailed lifting procedure, which was not shown before.
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   113
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   114
  The quotient package presented in this paper has the following
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   115
  advantages over existing packages:
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   116
  \begin{itemize}
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   117
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   118
  \item We define quotient composition, function map composition and
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   119
    relation map composition. This lets lifting polymorphic types with
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   120
    subtypes quotiented as well. We extend the notions of
2188
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
   121
    respectfulness and preservation to cope with quotient
1978
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   122
    composition.
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   123
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   124
  \item We allow lifting only some occurrences of quotiented
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   125
    types. Rsp/Prs extended. (used in nominal)
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   126
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   127
  \item The quotient package is very modular. Definitions can be added
2206
2d6cada7d5e0 Qpaper/Minor
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2205
diff changeset
   128
    separately, rsp and prs can be proved separately, Quotients and maps
2d6cada7d5e0 Qpaper/Minor
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2205
diff changeset
   129
    can be defined separately and theorems can
2d6cada7d5e0 Qpaper/Minor
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2205
diff changeset
   130
    be lifted on a need basis. (useful with type-classes).
1978
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   131
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   132
  \item Can be used both manually (attribute, separate tactics,
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   133
    rsp/prs databases) and programatically (automated definition of
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   134
    lifted constants, the rsp proof obligations and theorem statement
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   135
    translation according to given quotients).
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   136
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   137
  \end{itemize}
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   138
*}
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   139
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   140
section {* Quotient Type*}
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   141
2182
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
   142
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
   143
1978
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   144
text {*
2182
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
   145
  In this section we present the definitions of a quotient that follow
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
   146
  those by Homeier, the proofs can be found there.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
   147
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
   148
  \begin{definition}[Quotient]
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
   149
  A relation $R$ with an abstraction function $Abs$
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
   150
  and a representation function $Rep$ is a \emph{quotient}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
   151
  if and only if:
1978
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   152
2182
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
   153
  \begin{enumerate}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
   154
  \item @{thm (rhs1) Quotient_def[of "R", no_vars]}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
   155
  \item @{thm (rhs2) Quotient_def[of "R", no_vars]}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
   156
  \item @{thm (rhs3) Quotient_def[of "R", no_vars]}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
   157
  \end{enumerate}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
   158
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
   159
  \end{definition}
1978
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   160
2188
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
   161
  \begin{definition}[Relation map and function map]\\
2190
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2189
diff changeset
   162
  @{thm fun_rel_def[of "R1" "R2", no_vars]}\\
2182
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
   163
  @{thm fun_map_def[no_vars]}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
   164
  \end{definition}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
   165
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
   166
  The main theorems for building higher order quotients is:
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
   167
  \begin{lemma}[Function Quotient]
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
   168
  If @{thm (prem 1) fun_quotient[no_vars]} and @{thm (prem 2) fun_quotient[no_vars]}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
   169
  then @{thm (concl) fun_quotient[no_vars]}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
   170
  \end{lemma}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
   171
1978
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   172
*}
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   173
2195
0c1dcdefb515 Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2194
diff changeset
   174
subsection {* Higher Order Logic *}
0c1dcdefb515 Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2194
diff changeset
   175
0c1dcdefb515 Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2194
diff changeset
   176
text {*
0c1dcdefb515 Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2194
diff changeset
   177
0c1dcdefb515 Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2194
diff changeset
   178
  Types:
0c1dcdefb515 Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2194
diff changeset
   179
  \begin{eqnarray}\nonumber
0c1dcdefb515 Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2194
diff changeset
   180
  @{text "\<sigma> ::="} & @{text "\<alpha>"} & \textrm{(type variable)} \\ \nonumber
0c1dcdefb515 Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2194
diff changeset
   181
      @{text "|"} & @{text "(\<sigma>,\<dots>,\<sigma>)\<kappa>"} & \textrm{(type construction)}
0c1dcdefb515 Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2194
diff changeset
   182
  \end{eqnarray}
0c1dcdefb515 Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2194
diff changeset
   183
0c1dcdefb515 Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2194
diff changeset
   184
  Terms:
0c1dcdefb515 Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2194
diff changeset
   185
  \begin{eqnarray}\nonumber
0c1dcdefb515 Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2194
diff changeset
   186
  @{text "t ::="} & @{text "x\<^isup>\<sigma>"} & \textrm{(variable)} \\ \nonumber
0c1dcdefb515 Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2194
diff changeset
   187
      @{text "|"} & @{text "c\<^isup>\<sigma>"} & \textrm{(constant)} \\ \nonumber
0c1dcdefb515 Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2194
diff changeset
   188
      @{text "|"} & @{text "t t"} & \textrm{(application)} \\ \nonumber
0c1dcdefb515 Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2194
diff changeset
   189
      @{text "|"} & @{text "\<lambda>x\<^isup>\<sigma>. t"} & \textrm{(abstraction)} \\ \nonumber
0c1dcdefb515 Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2194
diff changeset
   190
  \end{eqnarray}
0c1dcdefb515 Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2194
diff changeset
   191
0c1dcdefb515 Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2194
diff changeset
   192
*}
0c1dcdefb515 Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2194
diff changeset
   193
1978
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   194
section {* Constants *}
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   195
2188
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
   196
(* Say more about containers? *)
2182
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
   197
1978
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   198
text {*
2182
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
   199
2188
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
   200
  To define a constant on the lifted type, an aggregate abstraction
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
   201
  function is applied to the raw constant. Below we describe the operation
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
   202
  that generates
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
   203
  an aggregate @{term "Abs"} or @{term "Rep"} function given the
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
   204
  compound raw type and the compound quotient type.
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
   205
  This operation will also be used in translations of theorem statements
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
   206
  and in the lifting procedure.
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
   207
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
   208
  The operation is additionally able to descend into types for which
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
   209
  maps are known. Such maps for most common types (list, pair, sum,
2195
0c1dcdefb515 Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2194
diff changeset
   210
  option, \ldots) are described in Homeier, and we assume that @{text "map"}
0c1dcdefb515 Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2194
diff changeset
   211
  is the function that returns a map for a given type. Then REP/ABS is defined
0c1dcdefb515 Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2194
diff changeset
   212
  as follows:
2182
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
   213
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
   214
  \begin{itemize}
2195
0c1dcdefb515 Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2194
diff changeset
   215
  \item @{text "ABS(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} = @{text "id"}
0c1dcdefb515 Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2194
diff changeset
   216
  \item @{text "REP(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"}  =  @{text "id"}
0c1dcdefb515 Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2194
diff changeset
   217
  \item @{text "ABS(\<sigma>, \<sigma>)"}  =  @{text "id"}
0c1dcdefb515 Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2194
diff changeset
   218
  \item @{text "REP(\<sigma>, \<sigma>)"}  =  @{text "id"}
2208
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   219
  \item @{text "ABS(\<sigma>\<^isub>1\<rightarrow>\<sigma>\<^isub>2,\<tau>\<^isub>1\<rightarrow>\<tau>\<^isub>2)"}  =  @{text "REP(\<sigma>\<^isub>1,\<tau>\<^isub>1) \<longrightarrow> ABS(\<sigma>\<^isub>2,\<tau>\<^isub>2)"}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   220
  \item @{text "REP(\<sigma>\<^isub>1\<rightarrow>\<sigma>\<^isub>2,\<tau>\<^isub>1\<rightarrow>\<tau>\<^isub>2)"}  =  @{text "ABS(\<sigma>\<^isub>1,\<tau>\<^isub>1) \<longrightarrow> REP(\<sigma>\<^isub>2,\<tau>\<^isub>2)"}
2195
0c1dcdefb515 Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2194
diff changeset
   221
  \item @{text "ABS((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>n))\<kappa>)"}  =  @{text "(map \<kappa>) (ABS(\<sigma>\<^isub>1,\<tau>\<^isub>1)) \<dots> (ABS(\<sigma>\<^isub>n,\<tau>\<^isub>n))"}
0c1dcdefb515 Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2194
diff changeset
   222
  \item @{text "REP((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>n))\<kappa>)"}  =  @{text "(map \<kappa>) (REP(\<sigma>\<^isub>1,\<tau>\<^isub>1)) \<dots> (REP(\<sigma>\<^isub>n,\<tau>\<^isub>n))"}
0c1dcdefb515 Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2194
diff changeset
   223
  \item @{text "ABS((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m))\<kappa>\<^isub>2)"}  =  @{text "Abs_\<kappa>\<^isub>2 \<circ> (map \<kappa>\<^isub>1) (ABS(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (ABS(\<rho>\<^isub>p,\<nu>\<^isub>p)"} provided @{text "\<eta> \<kappa>\<^isub>2 = (\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>p)\<kappa>\<^isub>1 \<and> \<exists>s. s(\<sigma>s\<kappa>\<^isub>1)=\<rho>s\<kappa>\<^isub>1 \<and> s(\<tau>s\<kappa>\<^isub>2)=\<nu>s\<kappa>\<^isub>2"}
0c1dcdefb515 Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2194
diff changeset
   224
  \item @{text "REP((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m))\<kappa>\<^isub>2)"}  =  @{text "(map \<kappa>\<^isub>1) (REP(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (REP(\<rho>\<^isub>p,\<nu>\<^isub>p) \<circ> Rep_\<kappa>\<^isub>2"} provided @{text "\<eta> \<kappa>\<^isub>2 = (\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>p)\<kappa>\<^isub>1 \<and> \<exists>s. s(\<sigma>s\<kappa>\<^isub>1)=\<rho>s\<kappa>\<^isub>1 \<and> s(\<tau>s\<kappa>\<^isub>2)=\<nu>s\<kappa>\<^isub>2"}
2182
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
   225
  \end{itemize}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
   226
2195
0c1dcdefb515 Functionalized the ABS/REP definition.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2194
diff changeset
   227
  Apart from the last 2 points the definition is same as the one implemented in
2208
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   228
  in Homeier's HOL package. Adding composition in last two cases is necessary
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   229
  for compositional quotients. We ilustrate the different behaviour of the
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   230
  definition by showing the derived definition of @{term fconcat}:
2182
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
   231
2188
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
   232
  @{thm fconcat_def[no_vars]}
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
   233
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
   234
  The aggregate @{term Abs} function takes a finite set of finite sets
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
   235
  and applies @{term "map rep_fset"} composed with @{term rep_fset} to
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
   236
  its input, obtaining a list of lists, passes the result to @{term concat}
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
   237
  obtaining a list and applies @{term abs_fset} obtaining the composed
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
   238
  finite set.
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
   239
*}
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
   240
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
   241
subsection {* Respectfulness *}
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
   242
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
   243
text {*
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
   244
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
   245
  A respectfulness lemma for a constant states that the equivalence
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
   246
  class returned by this constant depends only on the equivalence
2207
ea7c3f21d6df Qpaper/more.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2206
diff changeset
   247
  classes of the arguments applied to the constant. To automatically
ea7c3f21d6df Qpaper/more.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2206
diff changeset
   248
  lift a theorem that talks about a raw constant, to a theorem about
ea7c3f21d6df Qpaper/more.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2206
diff changeset
   249
  the quotient type a respectfulness theorem is required.
ea7c3f21d6df Qpaper/more.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2206
diff changeset
   250
ea7c3f21d6df Qpaper/more.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2206
diff changeset
   251
  A respectfulness condition for a constant can be expressed in
ea7c3f21d6df Qpaper/more.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2206
diff changeset
   252
  terms of an aggregate relation between the constant and itself,
ea7c3f21d6df Qpaper/more.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2206
diff changeset
   253
  for example the respectfullness for @{term "append"}
2188
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
   254
  can be stated as:
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
   255
2190
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2189
diff changeset
   256
  @{thm [display] append_rsp[no_vars]}
2182
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2152
diff changeset
   257
2190
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2189
diff changeset
   258
  \noindent
2208
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   259
  Which after unfolding @{term "op \<Longrightarrow>"} is equivalent to:
2188
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
   260
2190
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2189
diff changeset
   261
  @{thm [display] append_rsp_unfolded[no_vars]}
2188
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
   262
2207
ea7c3f21d6df Qpaper/more.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2206
diff changeset
   263
  An aggregate relation is defined in terms of relation composition,
ea7c3f21d6df Qpaper/more.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2206
diff changeset
   264
  so we define it first:
2188
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
   265
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
   266
  \begin{definition}[Composition of Relations]
2190
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2189
diff changeset
   267
  @{abbrev "rel_conj R1 R2"} where @{text OO} is the predicate
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2189
diff changeset
   268
  composition @{thm pred_compI[no_vars]}
2188
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
   269
  \end{definition}
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
   270
2207
ea7c3f21d6df Qpaper/more.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2206
diff changeset
   271
  The aggregate relation for an aggregate raw type and quotient type
ea7c3f21d6df Qpaper/more.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2206
diff changeset
   272
  is defined as:
2188
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
   273
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
   274
  \begin{itemize}
2207
ea7c3f21d6df Qpaper/more.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2206
diff changeset
   275
  \item @{text "REL(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} = @{text "op ="}
ea7c3f21d6df Qpaper/more.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2206
diff changeset
   276
  \item @{text "REL(\<sigma>, \<sigma>)"}  =  @{text "op ="}
ea7c3f21d6df Qpaper/more.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2206
diff changeset
   277
  \item @{text "REL((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>n))\<kappa>)"}  =  @{text "(rel \<kappa>) (REL(\<sigma>\<^isub>1,\<tau>\<^isub>1)) \<dots> (REL(\<sigma>\<^isub>n,\<tau>\<^isub>n))"}
ea7c3f21d6df Qpaper/more.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2206
diff changeset
   278
  \item @{text "REL((\<sigma>\<^isub>1,\<dots>,\<sigma>\<^isub>n))\<kappa>\<^isub>1, (\<tau>\<^isub>1,\<dots>,\<tau>\<^isub>m))\<kappa>\<^isub>2)"}  =  @{text "(rel \<kappa>\<^isub>1) (REL(\<rho>\<^isub>1,\<nu>\<^isub>1) \<dots> (REL(\<rho>\<^isub>p,\<nu>\<^isub>p) OOO Eqv_\<kappa>\<^isub>2"} provided @{text "\<eta> \<kappa>\<^isub>2 = (\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>p)\<kappa>\<^isub>1 \<and> \<exists>s. s(\<sigma>s\<kappa>\<^isub>1)=\<rho>s\<kappa>\<^isub>1 \<and> s(\<tau>s\<kappa>\<^isub>2)=\<nu>s\<kappa>\<^isub>2"}
2189
029bd37d010a qpaper..
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2188
diff changeset
   279
2188
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
   280
  \end{itemize}
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
   281
2207
ea7c3f21d6df Qpaper/more.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2206
diff changeset
   282
  Again, the last case is novel, so lets look at the example of
ea7c3f21d6df Qpaper/more.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2206
diff changeset
   283
  respectfullness for @{term concat}. The statement according to
ea7c3f21d6df Qpaper/more.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2206
diff changeset
   284
  the definition above is:
2190
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2189
diff changeset
   285
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2189
diff changeset
   286
  @{thm [display] concat_rsp[no_vars]}
2189
029bd37d010a qpaper..
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2188
diff changeset
   287
2190
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2189
diff changeset
   288
  \noindent
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2189
diff changeset
   289
  By unfolding the definition of relation composition and relation map
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2189
diff changeset
   290
  we can see the equivalent statement just using the primitive list
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2189
diff changeset
   291
  equivalence relation:
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2189
diff changeset
   292
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2189
diff changeset
   293
  @{thm [display] concat_rsp_unfolded[of "a" "a'" "b'" "b", no_vars]}
2189
029bd37d010a qpaper..
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2188
diff changeset
   294
2190
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2189
diff changeset
   295
  The statement reads that, for any lists of lists @{term a} and @{term b}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2189
diff changeset
   296
  if there exist intermediate lists of lists @{term "a'"} and @{term "b'"}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2189
diff changeset
   297
  such that each element of @{term a} is in the relation with an appropriate
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2189
diff changeset
   298
  element of @{term a'}, @{term a'} is in relation with @{term b'} and each
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2189
diff changeset
   299
  element of @{term b'} is in relation with the appropriate element of
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2189
diff changeset
   300
  @{term b}.
2189
029bd37d010a qpaper..
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2188
diff changeset
   301
029bd37d010a qpaper..
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2188
diff changeset
   302
*}
029bd37d010a qpaper..
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2188
diff changeset
   303
029bd37d010a qpaper..
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2188
diff changeset
   304
subsection {* Preservation *}
029bd37d010a qpaper..
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2188
diff changeset
   305
2190
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2189
diff changeset
   306
text {*
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2189
diff changeset
   307
  To be able to lift theorems that talk about constants that are not
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2189
diff changeset
   308
  lifted but whose type changes when lifting is performed additionally
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2189
diff changeset
   309
  preservation theorems are needed.
2196
74637f186af7 qpaper / a bit about prs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2195
diff changeset
   310
74637f186af7 qpaper / a bit about prs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2195
diff changeset
   311
  To lift theorems that talk about insertion in lists of lifted types
74637f186af7 qpaper / a bit about prs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2195
diff changeset
   312
  we need to know that for any quotient type with the abstraction and
74637f186af7 qpaper / a bit about prs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2195
diff changeset
   313
  representation functions @{text "Abs"} and @{text Rep} we have:
74637f186af7 qpaper / a bit about prs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2195
diff changeset
   314
74637f186af7 qpaper / a bit about prs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2195
diff changeset
   315
  @{thm [display] (concl) cons_prs[no_vars]}
74637f186af7 qpaper / a bit about prs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2195
diff changeset
   316
74637f186af7 qpaper / a bit about prs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2195
diff changeset
   317
  This is not enough to lift theorems that talk about quotient compositions.
74637f186af7 qpaper / a bit about prs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2195
diff changeset
   318
  For some constants (for example empty list) it is possible to show a
74637f186af7 qpaper / a bit about prs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2195
diff changeset
   319
  general compositional theorem, but for @{term "op #"} it is necessary
74637f186af7 qpaper / a bit about prs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2195
diff changeset
   320
  to show that it respects the particular quotient type:
74637f186af7 qpaper / a bit about prs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2195
diff changeset
   321
74637f186af7 qpaper / a bit about prs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2195
diff changeset
   322
  @{thm [display] insert_preserve2[no_vars]}
2190
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2189
diff changeset
   323
*}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2189
diff changeset
   324
2191
8fdfbec54229 qpaper / composition of quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2190
diff changeset
   325
subsection {* Composition of Quotient theorems *}
2189
029bd37d010a qpaper..
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2188
diff changeset
   326
2191
8fdfbec54229 qpaper / composition of quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2190
diff changeset
   327
text {*
8fdfbec54229 qpaper / composition of quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2190
diff changeset
   328
  Given two quotients, one of which quotients a container, and the
8fdfbec54229 qpaper / composition of quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2190
diff changeset
   329
  other quotients the type in the container, we can write the
2193
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2192
diff changeset
   330
  composition of those quotients. To compose two quotient theorems
2207
ea7c3f21d6df Qpaper/more.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2206
diff changeset
   331
  we compose the relations with relation composition as defined above
ea7c3f21d6df Qpaper/more.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2206
diff changeset
   332
  and the abstraction and relation functions are the ones of the sub
ea7c3f21d6df Qpaper/more.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2206
diff changeset
   333
  quotients composed with the usual function composition.
ea7c3f21d6df Qpaper/more.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2206
diff changeset
   334
  The @{term "Rep"} and @{term "Abs"} functions that we obtain agree
ea7c3f21d6df Qpaper/more.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2206
diff changeset
   335
  with the definition of aggregate Abs/Rep functions and the
2193
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2192
diff changeset
   336
  relation is the same as the one given by aggregate relations.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2192
diff changeset
   337
  This becomes especially interesting
2191
8fdfbec54229 qpaper / composition of quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2190
diff changeset
   338
  when we compose the quotient with itself, as there is no simple
8fdfbec54229 qpaper / composition of quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2190
diff changeset
   339
  intermediate step.
8fdfbec54229 qpaper / composition of quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2190
diff changeset
   340
2193
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2192
diff changeset
   341
  Lets take again the example of @{term concat}. To be able to lift
2207
ea7c3f21d6df Qpaper/more.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2206
diff changeset
   342
  theorems that talk about it we provide the composition quotient
ea7c3f21d6df Qpaper/more.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2206
diff changeset
   343
  theorems, which then lets us perform the lifting procedure in an
ea7c3f21d6df Qpaper/more.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2206
diff changeset
   344
  unchanged way:
2188
57972032e20e qpaper.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2186
diff changeset
   345
2190
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2189
diff changeset
   346
  @{thm [display] quotient_compose_list[no_vars]}
2192
87024a9a9d89 fixed compile error
Christian Urban <urbanc@in.tum.de>
parents: 2191
diff changeset
   347
*}
87024a9a9d89 fixed compile error
Christian Urban <urbanc@in.tum.de>
parents: 2191
diff changeset
   348
2191
8fdfbec54229 qpaper / composition of quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2190
diff changeset
   349
8fdfbec54229 qpaper / composition of quotients.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2190
diff changeset
   350
section {* Lifting Theorems *}
1978
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   351
2194
a52499e125ce qpaper / lifting introduction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2193
diff changeset
   352
text {*
a52499e125ce qpaper / lifting introduction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2193
diff changeset
   353
  The core of the quotient package takes an original theorem that
a52499e125ce qpaper / lifting introduction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2193
diff changeset
   354
  talks about the raw types, and the statement of the theorem that
a52499e125ce qpaper / lifting introduction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2193
diff changeset
   355
  it is supposed to produce. This is different from other existing
2207
ea7c3f21d6df Qpaper/more.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2206
diff changeset
   356
  quotient packages, where only the raw theorems were necessary.
2194
a52499e125ce qpaper / lifting introduction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2193
diff changeset
   357
  We notice that in some cases only some occurrences of the raw
a52499e125ce qpaper / lifting introduction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2193
diff changeset
   358
  types need to be lifted. This is for example the case in the
a52499e125ce qpaper / lifting introduction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2193
diff changeset
   359
  new Nominal package, where a raw datatype that talks about
a52499e125ce qpaper / lifting introduction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2193
diff changeset
   360
  pairs of natural numbers or strings (being lists of characters)
a52499e125ce qpaper / lifting introduction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2193
diff changeset
   361
  should not be changed to a quotient datatype with constructors
a52499e125ce qpaper / lifting introduction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2193
diff changeset
   362
  taking integers or finite sets of characters. To simplify the
a52499e125ce qpaper / lifting introduction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2193
diff changeset
   363
  use of the quotient package we additionally provide an automated
a52499e125ce qpaper / lifting introduction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2193
diff changeset
   364
  statement translation mechanism that replaces occurrences of
a52499e125ce qpaper / lifting introduction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2193
diff changeset
   365
  types that match given quotients by appropriate lifted types.
a52499e125ce qpaper / lifting introduction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2193
diff changeset
   366
a52499e125ce qpaper / lifting introduction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2193
diff changeset
   367
  Lifting the theorems is performed in three steps. In the following
a52499e125ce qpaper / lifting introduction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2193
diff changeset
   368
  we call these steps \emph{regularization}, \emph{injection} and
a52499e125ce qpaper / lifting introduction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2193
diff changeset
   369
  \emph{cleaning} following the names used in Homeier's HOL
2197
3a6afcb187ec qpaper / regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2196
diff changeset
   370
  implementation.
2193
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2192
diff changeset
   371
2197
3a6afcb187ec qpaper / regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2196
diff changeset
   372
  We first define the statement of the regularized theorem based
3a6afcb187ec qpaper / regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2196
diff changeset
   373
  on the original theorem and the goal theorem. Then we define
3a6afcb187ec qpaper / regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2196
diff changeset
   374
  the statement of the injected theorem, based on the regularized
2208
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   375
  theorem and the goal. We then show the 3 proofs, as all three
2197
3a6afcb187ec qpaper / regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2196
diff changeset
   376
  can be performed independently from each other.
2193
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2192
diff changeset
   377
2194
a52499e125ce qpaper / lifting introduction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2193
diff changeset
   378
*}
1994
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1978
diff changeset
   379
2197
3a6afcb187ec qpaper / regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2196
diff changeset
   380
subsection {* Regularization and Injection statements *}
1994
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1978
diff changeset
   381
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1978
diff changeset
   382
text {*
2197
3a6afcb187ec qpaper / regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2196
diff changeset
   383
2207
ea7c3f21d6df Qpaper/more.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2206
diff changeset
   384
  We first define the function @{text REG}, which takes the statements
ea7c3f21d6df Qpaper/more.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2206
diff changeset
   385
  of the raw theorem and the lifted theorem (both as terms) and
ea7c3f21d6df Qpaper/more.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2206
diff changeset
   386
  returns the statement of the regularized version. The intuition
ea7c3f21d6df Qpaper/more.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2206
diff changeset
   387
  behind this function is that it replaces quantifiers and
ea7c3f21d6df Qpaper/more.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2206
diff changeset
   388
  abstractions involving raw types by bounded ones, and equalities
ea7c3f21d6df Qpaper/more.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2206
diff changeset
   389
  involving raw types are replaced by appropriate aggregate
ea7c3f21d6df Qpaper/more.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2206
diff changeset
   390
  relations. It is defined as follows:
1994
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1978
diff changeset
   391
2197
3a6afcb187ec qpaper / regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2196
diff changeset
   392
  \begin{itemize}
2198
8fe1a706ade7 qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2197
diff changeset
   393
  \item @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<sigma>. s) = \<lambda>x : \<sigma>. REG (t, s)"}
8fe1a706ade7 qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2197
diff changeset
   394
  \item @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<tau>. s) = \<lambda>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}
8fe1a706ade7 qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2197
diff changeset
   395
  \item @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<sigma>. s) = \<forall>x : \<sigma>. REG (t, s)"}
8fe1a706ade7 qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2197
diff changeset
   396
  \item @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<tau>. s) = \<forall>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}
2197
3a6afcb187ec qpaper / regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2196
diff changeset
   397
  \item @{text "REG ((op =) : \<sigma>, (op =) : \<sigma>) = (op =) : \<sigma>"}
3a6afcb187ec qpaper / regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2196
diff changeset
   398
  \item @{text "REG ((op =) : \<sigma>, (op =) : \<tau>) = REL (\<sigma>, \<tau>) : \<sigma>"}
3a6afcb187ec qpaper / regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2196
diff changeset
   399
  \item @{text "REG (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) = REG (t\<^isub>1, s\<^isub>1) REG (t\<^isub>2, s\<^isub>2)"}
2198
8fe1a706ade7 qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2197
diff changeset
   400
  \item @{text "REG (v\<^isub>1, v\<^isub>2) = v\<^isub>1"}
8fe1a706ade7 qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2197
diff changeset
   401
  \item @{text "REG (c\<^isub>1, c\<^isub>2) = c\<^isub>1"}
2197
3a6afcb187ec qpaper / regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2196
diff changeset
   402
  \end{itemize}
1994
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1978
diff changeset
   403
2207
ea7c3f21d6df Qpaper/more.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2206
diff changeset
   404
  In the above definition we ommited the cases for existential quantifiers
ea7c3f21d6df Qpaper/more.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2206
diff changeset
   405
  and unique existential quantifiers, as they are very similar to the cases
ea7c3f21d6df Qpaper/more.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2206
diff changeset
   406
  for the universal quantifier.
2197
3a6afcb187ec qpaper / regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2196
diff changeset
   407
2207
ea7c3f21d6df Qpaper/more.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2206
diff changeset
   408
  Next we define the function @{text INJ} which takes the statement of
ea7c3f21d6df Qpaper/more.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2206
diff changeset
   409
  the regularized theorems and the statement of the lifted theorem both as
ea7c3f21d6df Qpaper/more.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2206
diff changeset
   410
  terms and returns the statment of the injected theorem:
2198
8fe1a706ade7 qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2197
diff changeset
   411
8fe1a706ade7 qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2197
diff changeset
   412
  \begin{itemize}
8fe1a706ade7 qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2197
diff changeset
   413
  \item @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<sigma>) = \<lambda>x. (INJ (t, s)"}
8fe1a706ade7 qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2197
diff changeset
   414
  \item @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x. (INJ (t, s))))"}
8fe1a706ade7 qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2197
diff changeset
   415
  \item @{text "INJ ((\<lambda>x \<in> R. t) : \<sigma>, (\<lambda>x. s) : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x \<in> R. (INJ (t, s))))"}
8fe1a706ade7 qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2197
diff changeset
   416
  \item @{text "INJ (\<forall> t, \<forall> s) = \<forall> (INJ (t, s)"}
8fe1a706ade7 qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2197
diff changeset
   417
  \item @{text "INJ (\<forall> t \<in> R, \<forall> s) = \<forall> (INJ (t, s) \<in> R"}
8fe1a706ade7 qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2197
diff changeset
   418
  \item @{text "INJ (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) = INJ (t\<^isub>1, s\<^isub>1) INJ (t\<^isub>2, s\<^isub>2)"}
8fe1a706ade7 qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2197
diff changeset
   419
  \item @{text "INJ (v\<^isub>1 : \<sigma>, v\<^isub>2 : \<sigma>) = v\<^isub>1"}
8fe1a706ade7 qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2197
diff changeset
   420
  \item @{text "INJ (v\<^isub>1 : \<sigma>, v\<^isub>2 : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (v\<^isub>1))"}
8fe1a706ade7 qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2197
diff changeset
   421
  \item @{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<sigma>) = c\<^isub>1"}
8fe1a706ade7 qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2197
diff changeset
   422
  \item @{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (c\<^isub>1))"}
8fe1a706ade7 qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2197
diff changeset
   423
  \end{itemize}
8fe1a706ade7 qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2197
diff changeset
   424
8fe1a706ade7 qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2197
diff changeset
   425
  For existential quantifiers and unique existential quantifiers it is
8fe1a706ade7 qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2197
diff changeset
   426
  defined similarily to the universal one.
8fe1a706ade7 qpaper / injection statement
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2197
diff changeset
   427
2197
3a6afcb187ec qpaper / regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2196
diff changeset
   428
*}
3a6afcb187ec qpaper / regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2196
diff changeset
   429
2208
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   430
subsection {* Proof procedure *}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   431
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   432
(* In the below the type-guiding 'QuotTrue' assumption is removed; since we
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   433
   present in a paper a version with typed-variables it is not necessary *)
2197
3a6afcb187ec qpaper / regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2196
diff changeset
   434
3a6afcb187ec qpaper / regularize
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2196
diff changeset
   435
text {*
2208
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   436
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   437
  With the above definitions of @{text "REG"} and @{text "INJ"} we can show
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   438
  how the proof is performed. The first step is always the application of
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   439
  of the following lemma:
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   440
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   441
  @{term "[|A; A --> B; B = C; C = D|] ==> D"}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   442
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   443
  With @{text A} instantiated to the original raw theorem, 
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   444
       @{text B} instantiated to @{text "REG(A)"},
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   445
       @{text C} instantiated to @{text "INJ(REG(A))"},
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   446
   and @{text D} instantiated to the statement of the lifted theorem.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   447
  The first assumption can be immediately discharged using the original
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   448
  theorem and the three left subgoals are exactly the subgoals of regularization,
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   449
  injection and cleaning. The three can be proved independently by the
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   450
  framework and in case there are non-solved subgoals they can be left
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   451
  to the user.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   452
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   453
  The injection and cleaning subgoals are always solved if the appropriate
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   454
  respectfulness and preservation theorems are given. It is not the case
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   455
  with regularization; sometimes a theorem given by the user does not
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   456
  imply a regularized version and a stronger one needs to be proved. This
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   457
  is outside of the scope of the quotient package, so the user is then left
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   458
  with such obligations. As an example lets see the simplest possible
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   459
  non-liftable theorem for integers: When we want to prove @{term "0 \<noteq> 1"}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   460
  on integers the fact that @{term "\<not> (0, 0) = (1, 0)"} is not enough. It
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   461
  only shows that particular items in the equivalence classes are not equal,
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   462
  a more general statement saying that the classes are not equal is necessary.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   463
*}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   464
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   465
subsection {* Proving Regularization *}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   466
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2207
diff changeset
   467
text {*
1994
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1978
diff changeset
   468
2209
5952b0f28261 Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2208
diff changeset
   469
  Isabelle provides a set of \emph{mono} rules, that are used to split implications
5952b0f28261 Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2208
diff changeset
   470
  of similar statements into simpler implication subgoals. These are enchanced
5952b0f28261 Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2208
diff changeset
   471
  with special quotient theorem in the regularization goal. Below we only show
5952b0f28261 Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2208
diff changeset
   472
  the versions for the universal quantifier. For the existential quantifier
5952b0f28261 Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2208
diff changeset
   473
  and abstraction they are analoguous with some symmetry.
2199
6ce64fb5cbd9 qpaper / lemmas used in proofs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2198
diff changeset
   474
2209
5952b0f28261 Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2208
diff changeset
   475
  First, bounded universal quantifiers can be removed on the right:
2199
6ce64fb5cbd9 qpaper / lemmas used in proofs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2198
diff changeset
   476
6ce64fb5cbd9 qpaper / lemmas used in proofs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2198
diff changeset
   477
  @{thm [display] ball_reg_right[no_vars]}
2206
2d6cada7d5e0 Qpaper/Minor
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2205
diff changeset
   478
2209
5952b0f28261 Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2208
diff changeset
   479
  They can be removed anywhere if the relation is an equivalence relation:
5952b0f28261 Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2208
diff changeset
   480
5952b0f28261 Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2208
diff changeset
   481
  @{thm [display] ball_reg_eqv[no_vars]}
5952b0f28261 Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2208
diff changeset
   482
5952b0f28261 Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2208
diff changeset
   483
  And finally it can be removed anywhere if @{term R2} is an equivalence relation, then:
5952b0f28261 Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2208
diff changeset
   484
  \[
5952b0f28261 Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2208
diff changeset
   485
  @{thm (rhs) ball_reg_eqv_range[no_vars]} = @{thm (lhs) ball_reg_eqv_range[no_vars]}
5952b0f28261 Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2208
diff changeset
   486
  \]
5952b0f28261 Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2208
diff changeset
   487
5952b0f28261 Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2208
diff changeset
   488
  The last theorem is new in comparison with Homeier's package; it allows separating
5952b0f28261 Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2208
diff changeset
   489
  regularization from injection.
5952b0f28261 Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2208
diff changeset
   490
2206
2d6cada7d5e0 Qpaper/Minor
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2205
diff changeset
   491
*}
2d6cada7d5e0 Qpaper/Minor
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2205
diff changeset
   492
2d6cada7d5e0 Qpaper/Minor
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2205
diff changeset
   493
(*
2209
5952b0f28261 Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2208
diff changeset
   494
  @{thm (rhs) bex_reg_eqv_range[no_vars]} = @{thm (lhs) bex_reg_eqv_range[no_vars]}
2199
6ce64fb5cbd9 qpaper / lemmas used in proofs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2198
diff changeset
   495
  @{thm [display] bex_reg_left[no_vars]}
6ce64fb5cbd9 qpaper / lemmas used in proofs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2198
diff changeset
   496
  @{thm [display] bex1_bexeq_reg[no_vars]}
2206
2d6cada7d5e0 Qpaper/Minor
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2205
diff changeset
   497
  @{thm [display] bex_reg_eqv[no_vars]}
2209
5952b0f28261 Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2208
diff changeset
   498
  @{thm [display] babs_reg_eqv[no_vars]}
5952b0f28261 Qpaper/regularization proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2208
diff changeset
   499
  @{thm [display] babs_simp[no_vars]}
2206
2d6cada7d5e0 Qpaper/Minor
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2205
diff changeset
   500
*)
1994
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1978
diff changeset
   501
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1978
diff changeset
   502
subsection {* Injection *}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1978
diff changeset
   503
2199
6ce64fb5cbd9 qpaper / lemmas used in proofs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2198
diff changeset
   504
text {*
2211
9d0673c319d1 qpaper / injection proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2210
diff changeset
   505
  The injection proof starts with an equality between the regularized theorem
9d0673c319d1 qpaper / injection proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2210
diff changeset
   506
  and the injected version. The proof again follows by the structure of the
9d0673c319d1 qpaper / injection proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2210
diff changeset
   507
  two term, and is defined for a goal being a relation between the two terms.
2199
6ce64fb5cbd9 qpaper / lemmas used in proofs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2198
diff changeset
   508
2211
9d0673c319d1 qpaper / injection proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2210
diff changeset
   509
  \begin{itemize}
9d0673c319d1 qpaper / injection proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2210
diff changeset
   510
  \item For two constants, an appropriate constant respectfullness assumption is used.
9d0673c319d1 qpaper / injection proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2210
diff changeset
   511
  \item For two variables, the regularization assumptions state that they are related.
9d0673c319d1 qpaper / injection proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2210
diff changeset
   512
  \item For two abstractions, they are eta-expanded and beta-reduced.
9d0673c319d1 qpaper / injection proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2210
diff changeset
   513
  \end{itemize}
2199
6ce64fb5cbd9 qpaper / lemmas used in proofs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2198
diff changeset
   514
2211
9d0673c319d1 qpaper / injection proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2210
diff changeset
   515
  Otherwise the two terms are applications. There are two cases: If there is a REP/ABS
9d0673c319d1 qpaper / injection proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2210
diff changeset
   516
  in the injected theorem we can use the theorem:
9d0673c319d1 qpaper / injection proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2210
diff changeset
   517
2199
6ce64fb5cbd9 qpaper / lemmas used in proofs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2198
diff changeset
   518
  @{thm [display] rep_abs_rsp[no_vars]}
6ce64fb5cbd9 qpaper / lemmas used in proofs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2198
diff changeset
   519
2211
9d0673c319d1 qpaper / injection proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2210
diff changeset
   520
  and continue the proof.
2199
6ce64fb5cbd9 qpaper / lemmas used in proofs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2198
diff changeset
   521
2211
9d0673c319d1 qpaper / injection proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2210
diff changeset
   522
  Otherwise we introduce an appropriate relation between the subterms and continue with
9d0673c319d1 qpaper / injection proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2210
diff changeset
   523
  two subgoals using the lemma:
9d0673c319d1 qpaper / injection proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2210
diff changeset
   524
9d0673c319d1 qpaper / injection proof.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2210
diff changeset
   525
  @{thm [display] apply_rsp[no_vars]}
2199
6ce64fb5cbd9 qpaper / lemmas used in proofs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2198
diff changeset
   526
6ce64fb5cbd9 qpaper / lemmas used in proofs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2198
diff changeset
   527
*}
6ce64fb5cbd9 qpaper / lemmas used in proofs
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2198
diff changeset
   528
1994
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1978
diff changeset
   529
subsection {* Cleaning *}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1978
diff changeset
   530
2212
79cebcc230d6 Qpaper / minor on cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2211
diff changeset
   531
text {*
79cebcc230d6 Qpaper / minor on cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2211
diff changeset
   532
  The @{text REG} and @{text INJ} functions have been defined in such a way
79cebcc230d6 Qpaper / minor on cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2211
diff changeset
   533
  that establishing the goal theorem now consists only on rewriting the
79cebcc230d6 Qpaper / minor on cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2211
diff changeset
   534
  injected theorem with the preservation theorems.
79cebcc230d6 Qpaper / minor on cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2211
diff changeset
   535
79cebcc230d6 Qpaper / minor on cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2211
diff changeset
   536
  \begin{itemize}
79cebcc230d6 Qpaper / minor on cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2211
diff changeset
   537
  \item First for lifted constants, their definitions are the preservation rules for
79cebcc230d6 Qpaper / minor on cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2211
diff changeset
   538
    them.
79cebcc230d6 Qpaper / minor on cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2211
diff changeset
   539
  \item For lambda abstractions lambda preservation establishes
79cebcc230d6 Qpaper / minor on cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2211
diff changeset
   540
    the equality between the injected theorem and the goal. This allows both
79cebcc230d6 Qpaper / minor on cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2211
diff changeset
   541
    abstraction and quantification over lifted types.
79cebcc230d6 Qpaper / minor on cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2211
diff changeset
   542
    @{thm [display] lambda_prs[no_vars]}
79cebcc230d6 Qpaper / minor on cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2211
diff changeset
   543
  \item Relations over lifted types are folded with:
79cebcc230d6 Qpaper / minor on cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2211
diff changeset
   544
    @{thm [display] Quotient_rel_rep[no_vars]}
79cebcc230d6 Qpaper / minor on cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2211
diff changeset
   545
  \item User given preservation theorems, that allow using higher level operations
79cebcc230d6 Qpaper / minor on cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2211
diff changeset
   546
    and containers of types being lifted. An example may be
79cebcc230d6 Qpaper / minor on cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2211
diff changeset
   547
    @{thm [display] map_prs(1)[no_vars]}
79cebcc230d6 Qpaper / minor on cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2211
diff changeset
   548
  \end{itemize}
79cebcc230d6 Qpaper / minor on cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2211
diff changeset
   549
79cebcc230d6 Qpaper / minor on cleaning
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2211
diff changeset
   550
 Preservation of relations and user given constant preservation lemmas *}
1994
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1978
diff changeset
   551
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1978
diff changeset
   552
section {* Examples *}
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1978
diff changeset
   553
2210
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   554
(* Mention why equivalence *)
2206
2d6cada7d5e0 Qpaper/Minor
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2205
diff changeset
   555
2210
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   556
text {*
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   557
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   558
  A user of our quotient package first needs to define an equivalence relation:
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   559
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   560
  @{text "fun \<approx> where (x, y) \<approx> (u, v) = (x + v = u + y)"}
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   561
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   562
  Then the user defines a quotient type:
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   563
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   564
  @{text "quotient_type int = (nat \<times> nat) / \<approx>"}
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   565
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   566
  Which leaves a proof obligation that the relation is an equivalence relation,
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   567
  that can be solved with the automatic tactic with two definitions.
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   568
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   569
  The user can then specify the constants on the quotient type:
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   570
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   571
  @{text "quotient_definition 0 \<Colon> int is (0\<Colon>nat, 0\<Colon>nat)"}
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   572
  @{text "fun plus_raw where plus_raw (x, y) (u, v) = (x + u, y + v)"}
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   573
  @{text "quotient_definition (op +) \<Colon> (int \<Rightarrow> int \<Rightarrow> int) is plus_raw"}
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   574
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   575
  Lets first take a simple theorem about addition on the raw level:
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   576
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   577
  @{text "lemma plus_zero_raw: plus_raw (0, 0) i \<approx> i"}
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   578
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   579
  When the user tries to lift a theorem about integer addition, the respectfulness
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   580
  proof obligation is left, so let us prove it first:
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   581
  
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   582
  @{text "lemma (op \<approx> \<Longrightarrow> op \<approx> \<Longrightarrow> op \<approx>) plus_raw plus_raw"}
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   583
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   584
  Can be proved automatically by the system just by unfolding the definition
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   585
  of @{term "op \<Longrightarrow>"}.
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   586
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   587
  Now the user can either prove a lifted lemma explicitely:
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   588
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   589
  @{text "lemma 0 + i = i by lifting plus_zero_raw"}
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   590
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   591
  Or in this simple case use the automated translation mechanism:
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   592
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   593
  @{text "thm plus_zero_raw[quot_lifted]"}
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   594
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   595
  obtaining the same result.
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   596
*}
2206
2d6cada7d5e0 Qpaper/Minor
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2205
diff changeset
   597
1978
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   598
section {* Related Work *}
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   599
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   600
text {*
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   601
  \begin{itemize}
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   602
2152
d7d4491535a9 starting bibliography
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2103
diff changeset
   603
  \item Peter Homeier's package~\cite{Homeier05} (and related work from there)
d7d4491535a9 starting bibliography
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2103
diff changeset
   604
  \item John Harrison's one~\cite{harrison-thesis} is the first one to lift theorems
d7d4491535a9 starting bibliography
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2103
diff changeset
   605
    but only first order.
1978
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   606
2152
d7d4491535a9 starting bibliography
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2103
diff changeset
   607
  \item PVS~\cite{PVS:Interpretations}
d7d4491535a9 starting bibliography
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2103
diff changeset
   608
  \item MetaPRL~\cite{Nogin02}
d7d4491535a9 starting bibliography
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2103
diff changeset
   609
  \item Manually defined quotients in Isabelle/HOL Library (Markus's Quotient\_Type,
d7d4491535a9 starting bibliography
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2103
diff changeset
   610
    Dixon's FSet, \ldots)
1978
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   611
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   612
  \item Oscar Slotosch defines quotient-type automatically but no
2152
d7d4491535a9 starting bibliography
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2103
diff changeset
   613
    lifting~\cite{Slotosch97}.
1978
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   614
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   615
  \item PER. And how to avoid it.
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   616
2152
d7d4491535a9 starting bibliography
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2103
diff changeset
   617
  \item Necessity of Hilbert Choice op and Larry's quotients~\cite{Paulson06}
1978
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   618
2152
d7d4491535a9 starting bibliography
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2103
diff changeset
   619
  \item Setoids in Coq and \cite{ChicliPS02}
1978
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   620
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   621
  \end{itemize}
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   622
*}
1975
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   623
2210
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   624
section {* Conclusion *}
6aaec9dd0c62 qpaper / example interaction
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 2209
diff changeset
   625
1975
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   626
(*<*)
b1281a0051ae added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   627
end
1978
8feedc0d4ea8 quotient paper
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 1975
diff changeset
   628
(*>*)