# HG changeset patch # User Christian Urban # Date 1276441275 -7200 # Node ID 8035515bbbc6df9f0854bb4fc0b9ed57439182ce # Parent 22c6b6144abd028b4678854c19db5c51e072b448 something about the quotient ype definitions diff -r 22c6b6144abd -r 8035515bbbc6 Nominal/FSet.thy --- a/Nominal/FSet.thy Sun Jun 13 14:39:55 2010 +0200 +++ b/Nominal/FSet.thy Sun Jun 13 17:01:15 2010 +0200 @@ -1417,4 +1417,223 @@ no_notation list_eq (infix "\" 50) +ML {* +open Quotient_Info; + +exception LIFT_MATCH of string + + + +(*** Aggregate Rep/Abs Function ***) + + +(* The flag RepF is for types in negative position; AbsF is for types + in positive position. Because of this, function types need to be + treated specially, since there the polarity changes. +*) + +datatype flag = AbsF | RepF + +fun negF AbsF = RepF + | negF RepF = AbsF + +fun is_identity (Const (@{const_name "id"}, _)) = true + | is_identity _ = false + +fun mk_identity ty = Const (@{const_name "id"}, ty --> ty) + +fun mk_fun_compose flag (trm1, trm2) = + case flag of + AbsF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2 + | RepF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1 + +fun get_mapfun ctxt s = +let + val thy = ProofContext.theory_of ctxt + val exn = LIFT_MATCH ("No map function for type " ^ quote s ^ " found.") + val mapfun = #mapfun (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn +in + Const (mapfun, dummyT) end + +(* makes a Free out of a TVar *) +fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT) + +(* produces an aggregate map function for the + rty-part of a quotient definition; abstracts + over all variables listed in vs (these variables + correspond to the type variables in rty) + + for example for: (?'a list * ?'b) + it produces: %a b. prod_map (map a) b +*) +fun mk_mapfun ctxt vs rty = +let + val vs' = map (mk_Free) vs + + fun mk_mapfun_aux rty = + case rty of + TVar _ => mk_Free rty + | Type (_, []) => mk_identity rty + | Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys) + | _ => raise LIFT_MATCH "mk_mapfun (default)" +in + fold_rev Term.lambda vs' (mk_mapfun_aux rty) +end + +(* looks up the (varified) rty and qty for + a quotient definition +*) +fun get_rty_qty ctxt s = +let + val thy = ProofContext.theory_of ctxt + val exn = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.") + val qdata = (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn +in + (#rtyp qdata, #qtyp qdata) +end + +(* takes two type-environments and looks + up in both of them the variable v, which + must be listed in the environment +*) +fun double_lookup rtyenv qtyenv v = +let + val v' = fst (dest_TVar v) +in + (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v'))) +end + +(* matches a type pattern with a type *) +fun match ctxt err ty_pat ty = +let + val thy = ProofContext.theory_of ctxt +in + Sign.typ_match thy (ty_pat, ty) Vartab.empty + handle MATCH_TYPE => err ctxt ty_pat ty +end + +(* produces the rep or abs constant for a qty *) +fun absrep_const flag ctxt qty_str = +let + val qty_name = Long_Name.base_name qty_str + val qualifier = Long_Name.qualifier qty_str +in + case flag of + AbsF => Const (Long_Name.qualify qualifier ("abs_" ^ qty_name), dummyT) + | RepF => Const (Long_Name.qualify qualifier ("rep_" ^ qty_name), dummyT) +end + +(* Lets Nitpick represent elements of quotient types as elements of the raw type *) +fun absrep_const_chk flag ctxt qty_str = + Syntax.check_term ctxt (absrep_const flag ctxt qty_str) + +fun absrep_match_err ctxt ty_pat ty = +let + val ty_pat_str = Syntax.string_of_typ ctxt ty_pat + val ty_str = Syntax.string_of_typ ctxt ty +in + raise LIFT_MATCH (space_implode " " + ["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"]) +end + + +(** generation of an aggregate absrep function **) + +(* - In case of equal types we just return the identity. + + - In case of TFrees we also return the identity. + + - In case of function types we recurse taking + the polarity change into account. + + - If the type constructors are equal, we recurse for the + arguments and build the appropriate map function. + + - If the type constructors are unequal, there must be an + instance of quotient types: + + - we first look up the corresponding rty_pat and qty_pat + from the quotient definition; the arguments of qty_pat + must be some distinct TVars + - we then match the rty_pat with rty and qty_pat with qty; + if matching fails the types do not correspond -> error + - the matching produces two environments; we look up the + assignments for the qty_pat variables and recurse on the + assignments + - we prefix the aggregate map function for the rty_pat, + which is an abstraction over all type variables + - finally we compose the result with the appropriate + absrep function in case at least one argument produced + a non-identity function / + otherwise we just return the appropriate absrep + function + + The composition is necessary for types like + + ('a list) list / ('a foo) foo + + The matching is necessary for types like + + ('a * 'a) list / 'a bar + + The test is necessary in order to eliminate superfluous + identity maps. +*) + +fun absrep_fun flag ctxt (rty, qty) = + if rty = qty + then mk_identity rty + else + case (rty, qty) of + (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) => + let + val arg1 = absrep_fun (negF flag) ctxt (ty1, ty1') + val arg2 = absrep_fun flag ctxt (ty2, ty2') + in + list_comb (get_mapfun ctxt "fun", [arg1, arg2]) + end + | (Type (s, tys), Type (s', tys')) => + if s = s' + then + let + val args = map (absrep_fun flag ctxt) (tys ~~ tys') + in + list_comb (get_mapfun ctxt s, args) + end + else + let + val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s' + val rtyenv = match ctxt absrep_match_err rty_pat rty + val qtyenv = match ctxt absrep_match_err qty_pat qty + val args_aux = map (double_lookup rtyenv qtyenv) vs + val args = map (absrep_fun flag ctxt) args_aux + val map_fun = mk_mapfun ctxt vs rty_pat + val result = list_comb (map_fun, args) + in + (*if forall is_identity args + then absrep_const flag ctxt s' + else*) mk_fun_compose flag (absrep_const flag ctxt s', result) + end + | (TFree x, TFree x') => + if x = x' + then mk_identity rty + else raise (LIFT_MATCH "absrep_fun (frees)") + | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)") + | _ => raise (LIFT_MATCH "absrep_fun (default)") + + +*} + +ML {* + absrep_fun AbsF @{context} (@{typ "('a list) list \ 'a list"}, @{typ "('a fset) fset \ 'a fset"}) + |> Syntax.string_of_term @{context} + |> writeln +*} + +lemma "(\ (c::'s \ bool). \(x::'s). c = rel x) = {c. \x. c = rel x}" +apply(auto simp add: mem_def) +done + + +end diff -r 22c6b6144abd -r 8035515bbbc6 Quotient-Paper/Paper.thy --- a/Quotient-Paper/Paper.thy Sun Jun 13 14:39:55 2010 +0200 +++ b/Quotient-Paper/Paper.thy Sun Jun 13 17:01:15 2010 +0200 @@ -114,7 +114,7 @@ The purpose of a \emph{quotient package} is to ease the lifting of theorems and automate the definitions and reasoning as much as possible. In the context of HOL, there have been a few quotient packages already - \cite{harrison-thesis,Slotosch97}. The most notable is the one by Homeier + \cite{harrison-thesis,Slotosch97}. The most notable one is by Homeier \cite{Homeier05} implemented in HOL4. The fundamental construction these quotient packages perform can be illustrated by the following picture: @@ -144,19 +144,19 @@ \end{center} \noindent - The starting point is an existing type, often referred to as the - \emph{raw level}, over which an equivalence relation given by the user is + The starting point is an existing type, often referred to as the \emph{raw + type}, over which an equivalence relation given by the user is defined. With this input the package introduces a new type, to which we - refer as the \emph{quotient level}. This type comes with an + refer as the \emph{quotient type}. This type comes with an \emph{abstraction} and a \emph{representation} function, written @{text Abs} - and @{text Rep}. These functions relate elements in the existing type to - ones in the new type and vice versa; they can be uniquely identified by - their type. For example for the integer quotient construction the types of - @{text Abs} and @{text Rep} are - + and @{text Rep}.\footnote{Actually they need to be derived from slightly + more basic functions. We will show the details later. } These functions + relate elements in the existing type to ones in the new type and vice versa; + they can be uniquely identified by their type. For example for the integer + quotient construction the types of @{text Abs} and @{text Rep} are \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% - @{text "Abs::nat \ nat \ int"}\hspace{10mm}@{text "Rep::int \ nat \ nat"} + @{text "Abs :: nat \ nat \ int"}\hspace{10mm}@{text "Rep :: int \ nat \ nat"} \end{isabelle} \noindent @@ -192,7 +192,7 @@ \noindent We expect that the corresponding operator on finite sets, written @{term "fconcat"}, - behaves as follows: + builds the union of finite sets of finite sets: @{thm [display, indent=10] fconcat_empty[no_vars] fconcat_insert[no_vars]} @@ -205,7 +205,7 @@ the abstraction of the result is \emph{not} enough. The reason is that case in case of @{text "\"} we obtain the incorrect definition - @{text [display, indent=10] "\ S \ Abs (flat (Rep S))"} + @{text [display, indent=10] "\ S \ Abs_fset (flat (Rep_fset S))"} \noindent where the right-hand side is not even typable! This problem can be remedied in the @@ -216,7 +216,7 @@ representation and abstraction functions, which in case of @{text "\"} generate the following definition - @{text [display, indent=10] "\ S \ Abs (flat ((map Rep \ Rep) S))"} + @{text [display, indent=10] "\ S \ Abs_fset (flat ((map Rep_fset \ Rep_fset) S))"} \noindent where @{term map} is the usual mapping function for lists. In this paper we @@ -294,13 +294,52 @@ @{text "|"} & @{text "\x\<^isup>\. t"} & \textrm{(abstraction)} \\ \nonumber \end{eqnarray} + {\it Say more about containers / maping functions } + *} section {* Quotient Types and Lifting of Definitions *} -(* Say more about containers? *) +text {* + The first step in a quotient constructions is to take a name for the new + type, say @{text "\\<^isub>q"}, and an equivalence relation defined over a + raw type, say @{text "\"}. The equivalence relation for the quotient + construction, lets say @{text "R"}, must then be of type @{text "\ \ \ \ + bool"}. Given this data, we can automatically declare the quotient type as + + + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% + \isacommand{typedef}~~@{text "\s \\<^isub>q = {c. \x. c = R x}"} + \end{isabelle} + + \noindent + being the set of equivalence classes of @{text "R"}. The restriction in this declaration + is that the type variables in the raw type @{text "\"} must be included in the + type variables @{text "\s"} declared for @{text "\\<^isub>q"}. HOL will provide us + with abstraction and representation functions having the type -text {* + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% + @{text "abs_\\<^isub>q :: \ set \ \s \\<^isub>q"}\hspace{10mm}@{text "rep_\\<^isub>q :: \s \\<^isub>q \ \ set"} + \end{isabelle} + + \noindent + relating the new quotient type and raw type. However, as Homeier noted, it is easier + to work with the following derived definitions + + \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% + @{text "Abs_\\<^isub>q x \ abs_\\<^isub>q (R x)"}\hspace{10mm}@{text "Rep_\\<^isub>q x \ \ (rep_\\<^isub>q x)"} + \end{isabelle} + + \noindent + on the expense of having to use Hilbert's choice operator @{text "\"}. With these + definitions the abstraction and representation functions relate directly the + quotient and raw types (their type is @{text "\ \ \s \\<^isub>q"} and @{text "\s \\<^isub>q \ \"}, + respectively). We can show that the property + + @{text [display, indent=10] "Quotient R Abs_\\<^isub>q Rep_\\<^isub>q"} + + \noindent + holds (for the proof see \cite{Homeier05}). To define a constant on the lifted type, an aggregate abstraction function is applied to the raw constant. Below we describe the operation @@ -317,17 +356,9 @@ as follows: {\it the first argument is the raw type and the second argument the quotient type} - - + % \begin{center} - \begin{tabular}{rcl} - - % type variable case says that variables must be equal...therefore subsumed by the equal case below - % - %\multicolumn{3}{@ {\hspace{-4mm}}l}{type variables:}\\ - %@{text "ABS (\\<^isub>1, \\<^isub>2)"} & $\dn$ & @{text "id"}\\ - %@{text "REP (\\<^isub>1, \\<^isub>2)"} & $\dn$ & @{text "id"}\smallskip\\ - + \begin{longtable}{rcl} \multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\ @{text "ABS (\, \)"} & $\dn$ & @{text "id"}\\ @{text "REP (\, \)"} & $\dn$ & @{text "id"}\smallskip\\ @@ -338,19 +369,19 @@ @{text "ABS (\s \, \s \)"} & $\dn$ & @{text "map_\ (ABS (\s, \s))"}\\ @{text "REP (\s \, \s \)"} & $\dn$ & @{text "map_\ (REP (\s, \s))"}\smallskip\\ \multicolumn{3}{@ {\hspace{-4mm}}l}{unequal type constructors:}\\ - @{text "ABS (\s \\<^isub>1, \s \\<^isub>2)"} & $\dn$ & @{text "Abs_\\<^isub>2 \ (MAP(\s \\<^isub>1) (ABS (\s', \s')))"}\\ - @{text "REP (\s \\<^isub>1, \s \\<^isub>2)"} & $\dn$ & @{text "(MAP(\s \\<^isub>1) (REP (\s', \s'))) \ Rep_\\<^isub>2"}\\ - \end{tabular} + @{text "ABS (\s \, \s \\<^isub>q)"} & $\dn$ & @{text "Abs_\\<^isub>q \ (MAP(\s \) (ABS (\s', \s')))"}\\ + @{text "REP (\s \, \s \\<^isub>q)"} & $\dn$ & @{text "(MAP(\s \) (REP (\s', \s'))) \ Rep_\\<^isub>q"}\\ + \end{longtable} \end{center} - + % \noindent - where in the last two clauses we have that the quotient type @{text "\s \\<^isub>2"} is a quotient of - the raw type @{text "\s \\<^isub>1"} (for example @{text "\ fset"} and @{text "\ list"}). + where in the last two clauses we have that the quotient type @{text "\s \\<^isub>q"} is a quotient of + the raw type @{text "\s \"} (for example @{text "\ fset"} and @{text "\ list"}). The quotient construction ensures that the type variables in @{text "\s"} must be amongst the @{text "\s"}. Now the @{text "\s'"} are given by the matchers for the @{text "\s"} - when matching @{text "\s \\<^isub>2"} against @{text "\s \\<^isub>2"}; similarly the @{text "\s'"} are given by the - same type-variables when matching @{text "\s \\<^isub>1"} against @{text "\s \\<^isub>1"}. + when matching @{text "\s \\<^isub>q"} against @{text "\s \\<^isub>q"}; similarly the @{text "\s'"} are given by the + same type-variables when matching @{text "\s \"} against @{text "\s \"}. The function @{text "MAP"} calculates an \emph{aggregate map-function} for a type as follows: diff -r 22c6b6144abd -r 8035515bbbc6 Quotient-Paper/document/root.tex --- a/Quotient-Paper/document/root.tex Sun Jun 13 14:39:55 2010 +0200 +++ b/Quotient-Paper/document/root.tex Sun Jun 13 17:01:15 2010 +0200 @@ -9,6 +9,7 @@ \usepackage{tikz} \usepackage{pgf} \usepackage{verbdef} +\usepackage{longtable} \urlstyle{rm} \isabellestyle{it}