(* How to change the notation for \<lbrakk> \<rbrakk> meta-level implications? *)

(*<*)

theory Paper

imports "Quotient"

        "LaTeXsugar"

        "../Nominal/FSet"

begin

print_syntax

notation (latex output)

  rel_conj ("_ OOO _" [53, 53] 52)

and

  "op -->" (infix "\<rightarrow>" 100)

and

  "==>" (infix "\<Rightarrow>" 100)

and

  fun_map (infix "\<longrightarrow>" 51)

and

  fun_rel (infix "\<Longrightarrow>" 51)

and

  list_eq (infix "\<approx>" 50) (* Not sure if we want this notation...? *)

ML {*

fun nth_conj n (_, r) = nth (HOLogic.dest_conj r) n;

fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t =>

  let

    val concl =

      Object_Logic.drop_judgment (ProofContext.theory_of ctxt) (Logic.strip_imp_concl t)

  in

    case concl of (_ $ l $ r) => proj (l, r)

    | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl)

  end);

*}

setup {*

  Term_Style.setup "rhs1" (style_lhs_rhs (nth_conj 0)) #>

  Term_Style.setup "rhs2" (style_lhs_rhs (nth_conj 1)) #>

  Term_Style.setup "rhs3" (style_lhs_rhs (nth_conj 2))

*}

(*>*)

section {* Introduction *}

text {* 

   \begin{flushright}

  {\em ``Not using a [quotient] package has its advantages: we do not have to\\ 

    collect all the theorems we shall ever want into one giant list;''}\\

    Paulson \cite{Paulson06}

  \end{flushright}\smallskip

  \noindent

  Isabelle is a generic theorem prover in which many logics can be implemented. 

  The most widely used one, however, is

  Higher-Order Logic (HOL). This logic consists of a small number of 

  axioms and inference

  rules over a simply-typed term-language. Safe reasoning in HOL is ensured by two very restricted 

  mechanisms for extending the logic: one is the definition of new constants

  in terms of existing ones; the other is the introduction of new types

  by identifying non-empty subsets in existing types. It is well understood 

  to use both mechanism for dealing with quotient constructions in HOL (cite Larry).

  For example the integers in Isabelle/HOL are constructed by a quotient construction over 

  the type @{typ "nat \<times> nat"} and the equivalence relation

% I would avoid substraction for natural numbers.

  @{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"}

  \noindent

  Similarly one can construct the type of finite sets by quotienting lists

  according to the equivalence relation

  @{text [display] "xs \<approx> ys \<equiv> (\<forall>x. x \<in> xs \<longleftrightarrow> x \<in> ys)"}

  \noindent

  where @{text "\<in>"} stands for membership in a list.

  The problem is that in order to start reasoning about, for example integers, 

  definitions and theorems need to be transferred, or \emph{lifted}, 

  from the ``raw'' type @{typ "nat \<times> nat"} to the quotient type @{typ int}. 

  This lifting usually requires a lot of tedious reasoning effort.

  The purpose of a \emph{quotient package} is to ease the lifting and automate

  the reasoning involved as much as possible. Such a package is a central

  component of the new version of Nominal Isabelle where representations 

  of alpha-equated terms are constructed according to specifications given by

  the user. 

  In the context of HOL, there have been several quotient packages (...). The

  most notable is the one by Homeier (...) implemented in HOL4. However, what is

  surprising, none of them can deal compositions of quotients, for example with 

  lifting theorems about @{text "concat"}:

  @{thm [display] concat.simps(1)}

  @{thm [display] concat.simps(2)[no_vars]}

  \noindent

  One would like to lift this definition to the operation:

  @{thm [display] fconcat_empty[no_vars]}

  @{thm [display] fconcat_insert[no_vars]}

  \noindent

  What is special about this operation is that we have as input

  lists of lists which after lifting turn into finite sets of finite

  sets.

*}

subsection {* Contributions *}

text {*

  We present the detailed lifting procedure, which was not shown before.

  The quotient package presented in this paper has the following

  advantages over existing packages:

  \begin{itemize}

  \item We define quotient composition, function map composition and

    relation map composition. This lets lifting polymorphic types with

    subtypes quotiented as well. We extend the notions of

    respectfulness and preservation to cope with quotient

    composition.

  \item We allow lifting only some occurrences of quotiented

    types. Rsp/Prs extended. (used in nominal)

  \item The quotient package is very modular. Definitions can be added

    separately, rsp and prs can be proved separately, Quotients and maps

    can be defined separately and theorems can

    be lifted on a need basis. (useful with type-classes).

  \item Can be used both manually (attribute, separate tactics,

    rsp/prs databases) and programatically (automated definition of

    lifted constants, the rsp proof obligations and theorem statement

    translation according to given quotients).

  \end{itemize}

*}

section {* Quotient Type*}

text {*

  In this section we present the definitions of a quotient that follow

  those by Homeier, the proofs can be found there.

  \begin{definition}[Quotient]

  A relation $R$ with an abstraction function $Abs$

  and a representation function $Rep$ is a \emph{quotient}

  if and only if:

  \begin{enumerate}

  \item @{thm (rhs1) Quotient_def[of "R", no_vars]}

  \item @{thm (rhs2) Quotient_def[of "R", no_vars]}

  \item @{thm (rhs3) Quotient_def[of "R", no_vars]}

  \end{enumerate}

  \end{definition}

  \begin{definition}[Relation map and function map]\\

  @{thm fun_rel_def[of "R1" "R2", no_vars]}\\

  @{thm fun_map_def[no_vars]}

  \end{definition}

  The main theorems for building higher order quotients is:

  \begin{lemma}[Function Quotient]

  If @{thm (prem 1) fun_quotient[no_vars]} and @{thm (prem 2) fun_quotient[no_vars]}

  then @{thm (concl) fun_quotient[no_vars]}

  \end{lemma}

*}

subsection {* Higher Order Logic *}

text {*

  Types:

  \begin{eqnarray}\nonumber

  @{text "\<sigma> ::="} & @{text "\<alpha>"} & \textrm{(type variable)} \\ \nonumber

      @{text "|"} & @{text "(\<sigma>,\<dots>,\<sigma>)\<kappa>"} & \textrm{(type construction)}

  \end{eqnarray}

  Terms:

  \begin{eqnarray}\nonumber

  @{text "t ::="} & @{text "x\<^isup>\<sigma>"} & \textrm{(variable)} \\ \nonumber

      @{text "|"} & @{text "c\<^isup>\<sigma>"} & \textrm{(constant)} \\ \nonumber

      @{text "|"} & @{text "t t"} & \textrm{(application)} \\ \nonumber

      @{text "|"} & @{text "\<lambda>x\<^isup>\<sigma>. t"} & \textrm{(abstraction)} \\ \nonumber

  \end{eqnarray}

*}

section {* Constants *}

(* Say more about containers? *)

text {*

  To define a constant on the lifted type, an aggregate abstraction

  function is applied to the raw constant. Below we describe the operation

  that generates

  an aggregate @{term "Abs"} or @{term "Rep"} function given the

  compound raw type and the compound quotient type.

  This operation will also be used in translations of theorem statements

  and in the lifting procedure.

  The operation is additionally able to descend into types for which

  maps are known. Such maps for most common types (list, pair, sum,

  option, \ldots) are described in Homeier, and we assume that @{text "map"}

  is the function that returns a map for a given type. Then REP/ABS is defined

  as follows:

  \begin{itemize}

  \item @{text "ABS(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} = @{text "id"}

  \item @{text "REP(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"}  =  @{text "id"}

  \item @{text "ABS(\<sigma>, \<sigma>)"}  =  @{text "id"}

  \item @{text "REP(\<sigma>, \<sigma>)"}  =  @{text "id"}

  \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)"}

  \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)"}

  \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))"}

  \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))"}

  \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"}

  \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"}

  \end{itemize}

  Apart from the last 2 points the definition is same as the one implemented in

  in Homeier's HOL package. Adding composition in last two cases is necessary

  for compositional quotients. We ilustrate the different behaviour of the

  definition by showing the derived definition of @{term fconcat}:

  @{thm fconcat_def[no_vars]}

  The aggregate @{term Abs} function takes a finite set of finite sets

  and applies @{term "map rep_fset"} composed with @{term rep_fset} to

  its input, obtaining a list of lists, passes the result to @{term concat}

  obtaining a list and applies @{term abs_fset} obtaining the composed

  finite set.

*}

subsection {* Respectfulness *}

text {*

  A respectfulness lemma for a constant states that the equivalence

  class returned by this constant depends only on the equivalence

  classes of the arguments applied to the constant. To automatically

  lift a theorem that talks about a raw constant, to a theorem about

  the quotient type a respectfulness theorem is required.

  A respectfulness condition for a constant can be expressed in

  terms of an aggregate relation between the constant and itself,

  for example the respectfullness for @{term "append"}

  can be stated as:

  @{thm [display] append_rsp[no_vars]}

  \noindent

  Which after unfolding @{term "op \<Longrightarrow>"} is equivalent to:

  @{thm [display] append_rsp_unfolded[no_vars]}

  An aggregate relation is defined in terms of relation composition,

  so we define it first:

  \begin{definition}[Composition of Relations]

  @{abbrev "rel_conj R1 R2"} where @{text OO} is the predicate

  composition @{thm pred_compI[no_vars]}

  \end{definition}

  The aggregate relation for an aggregate raw type and quotient type

  is defined as:

  \begin{itemize}

  \item @{text "REL(\<alpha>\<^isub>1, \<alpha>\<^isub>2)"} = @{text "op ="}

  \item @{text "REL(\<sigma>, \<sigma>)"}  =  @{text "op ="}

  \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))"}

  \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"}

  \end{itemize}

  Again, the last case is novel, so lets look at the example of

  respectfullness for @{term concat}. The statement according to

  the definition above is:

  @{thm [display] concat_rsp[no_vars]}

  \noindent

  By unfolding the definition of relation composition and relation map

  we can see the equivalent statement just using the primitive list

  equivalence relation:

  @{thm [display] concat_rsp_unfolded[of "a" "a'" "b'" "b", no_vars]}

  The statement reads that, for any lists of lists @{term a} and @{term b}

  if there exist intermediate lists of lists @{term "a'"} and @{term "b'"}

  such that each element of @{term a} is in the relation with an appropriate

  element of @{term a'}, @{term a'} is in relation with @{term b'} and each

  element of @{term b'} is in relation with the appropriate element of

  @{term b}.

*}

subsection {* Preservation *}

text {*

  To be able to lift theorems that talk about constants that are not

  lifted but whose type changes when lifting is performed additionally

  preservation theorems are needed.

  To lift theorems that talk about insertion in lists of lifted types

  we need to know that for any quotient type with the abstraction and

  representation functions @{text "Abs"} and @{text Rep} we have:

  @{thm [display] (concl) cons_prs[no_vars]}

  This is not enough to lift theorems that talk about quotient compositions.

  For some constants (for example empty list) it is possible to show a

  general compositional theorem, but for @{term "op #"} it is necessary

  to show that it respects the particular quotient type:

  @{thm [display] insert_preserve2[no_vars]}

*}

subsection {* Composition of Quotient theorems *}

text {*

  Given two quotients, one of which quotients a container, and the

  other quotients the type in the container, we can write the

  composition of those quotients. To compose two quotient theorems

  we compose the relations with relation composition as defined above

  and the abstraction and relation functions are the ones of the sub

  quotients composed with the usual function composition.

  The @{term "Rep"} and @{term "Abs"} functions that we obtain agree

  with the definition of aggregate Abs/Rep functions and the

  relation is the same as the one given by aggregate relations.

  This becomes especially interesting

  when we compose the quotient with itself, as there is no simple

  intermediate step.

  Lets take again the example of @{term concat}. To be able to lift

  theorems that talk about it we provide the composition quotient

  theorems, which then lets us perform the lifting procedure in an

  unchanged way:

  @{thm [display] quotient_compose_list[no_vars]}

*}

section {* Lifting Theorems *}

text {*

  The core of the quotient package takes an original theorem that

  talks about the raw types, and the statement of the theorem that

  it is supposed to produce. This is different from other existing

  quotient packages, where only the raw theorems were necessary.

  We notice that in some cases only some occurrences of the raw

  types need to be lifted. This is for example the case in the

  new Nominal package, where a raw datatype that talks about

  pairs of natural numbers or strings (being lists of characters)

  should not be changed to a quotient datatype with constructors

  taking integers or finite sets of characters. To simplify the

  use of the quotient package we additionally provide an automated

  statement translation mechanism that replaces occurrences of

  types that match given quotients by appropriate lifted types.

  Lifting the theorems is performed in three steps. In the following

  we call these steps \emph{regularization}, \emph{injection} and

  \emph{cleaning} following the names used in Homeier's HOL

  implementation.

  We first define the statement of the regularized theorem based

  on the original theorem and the goal theorem. Then we define

  the statement of the injected theorem, based on the regularized

  theorem and the goal. We then show the 3 proofs, as all three

  can be performed independently from each other.

*}

subsection {* Regularization and Injection statements *}

text {*

  We first define the function @{text REG}, which takes the statements

  of the raw theorem and the lifted theorem (both as terms) and

  returns the statement of the regularized version. The intuition

  behind this function is that it replaces quantifiers and

  abstractions involving raw types by bounded ones, and equalities

  involving raw types are replaced by appropriate aggregate

  relations. It is defined as follows:

  \begin{itemize}

  \item @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<sigma>. s) = \<lambda>x : \<sigma>. REG (t, s)"}

  \item @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<tau>. s) = \<lambda>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}

  \item @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<sigma>. s) = \<forall>x : \<sigma>. REG (t, s)"}

  \item @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<tau>. s) = \<forall>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"}

  \item @{text "REG ((op =) : \<sigma>, (op =) : \<sigma>) = (op =) : \<sigma>"}

  \item @{text "REG ((op =) : \<sigma>, (op =) : \<tau>) = REL (\<sigma>, \<tau>) : \<sigma>"}

  \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)"}

  \item @{text "REG (v\<^isub>1, v\<^isub>2) = v\<^isub>1"}

  \item @{text "REG (c\<^isub>1, c\<^isub>2) = c\<^isub>1"}

  \end{itemize}

  In the above definition we ommited the cases for existential quantifiers

  and unique existential quantifiers, as they are very similar to the cases

  for the universal quantifier.

  Next we define the function @{text INJ} which takes the statement of

  the regularized theorems and the statement of the lifted theorem both as

  terms and returns the statment of the injected theorem:

  \begin{itemize}

  \item @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<sigma>) = \<lambda>x. (INJ (t, s)"}

  \item @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x. (INJ (t, s))))"}

  \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))))"}

  \item @{text "INJ (\<forall> t, \<forall> s) = \<forall> (INJ (t, s)"}

  \item @{text "INJ (\<forall> t \<in> R, \<forall> s) = \<forall> (INJ (t, s) \<in> R"}

  \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)"}

  \item @{text "INJ (v\<^isub>1 : \<sigma>, v\<^isub>2 : \<sigma>) = v\<^isub>1"}

  \item @{text "INJ (v\<^isub>1 : \<sigma>, v\<^isub>2 : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (v\<^isub>1))"}

  \item @{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<sigma>) = c\<^isub>1"}

  \item @{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (c\<^isub>1))"}

  \end{itemize}

  For existential quantifiers and unique existential quantifiers it is

  defined similarily to the universal one.

*}

subsection {* Proof procedure *}

(* In the below the type-guiding 'QuotTrue' assumption is removed; since we

   present in a paper a version with typed-variables it is not necessary *)

text {*

  With the above definitions of @{text "REG"} and @{text "INJ"} we can show

  how the proof is performed. The first step is always the application of

  of the following lemma:

  @{term "[|A; A --> B; B = C; C = D|] ==> D"}

  With @{text A} instantiated to the original raw theorem, 

       @{text B} instantiated to @{text "REG(A)"},

       @{text C} instantiated to @{text "INJ(REG(A))"},

   and @{text D} instantiated to the statement of the lifted theorem.

  The first assumption can be immediately discharged using the original

  theorem and the three left subgoals are exactly the subgoals of regularization,

  injection and cleaning. The three can be proved independently by the

  framework and in case there are non-solved subgoals they can be left

  to the user.

  The injection and cleaning subgoals are always solved if the appropriate

  respectfulness and preservation theorems are given. It is not the case

  with regularization; sometimes a theorem given by the user does not

  imply a regularized version and a stronger one needs to be proved. This

  is outside of the scope of the quotient package, so the user is then left

  with such obligations. As an example lets see the simplest possible

  non-liftable theorem for integers: When we want to prove @{term "0 \<noteq> 1"}

  on integers the fact that @{term "\<not> (0, 0) = (1, 0)"} is not enough. It

  only shows that particular items in the equivalence classes are not equal,

  a more general statement saying that the classes are not equal is necessary.

*}

subsection {* Proving Regularization *}

text {*

  Isabelle provides a set of \emph{mono} rules, that are used to split implications

  of similar statements into simpler implication subgoals. These are enchanced

  with special quotient theorem in the regularization goal. Below we only show

  the versions for the universal quantifier. For the existential quantifier

  and abstraction they are analoguous with some symmetry.

  First, bounded universal quantifiers can be removed on the right:

  @{thm [display] ball_reg_right[no_vars]}

  They can be removed anywhere if the relation is an equivalence relation:

  @{thm [display] ball_reg_eqv[no_vars]}

  And finally it can be removed anywhere if @{term R2} is an equivalence relation, then:

  \[

  @{thm (rhs) ball_reg_eqv_range[no_vars]} = @{thm (lhs) ball_reg_eqv_range[no_vars]}

  \]

  The last theorem is new in comparison with Homeier's package; it allows separating