nominal2: comparison Quot/quotient

equal deleted inserted replaced

-:2480fb2a5e4e
+:5961edda27d7
 open Quotient_Info;
 exception LIFT_MATCH of string
-(* simplifies a term according to the id_rules *)
-fun id_simplify ctxt trm =
-let
+(*** Aggregate Rep/Abs Function ***)
-val thy = ProofContext.theory_of ctxt
-val id_thms = id_simps_get ctxt
-in
+(* The flag repF is for types in negative position; absF is for types
-MetaSimplifier.rewrite_term thy id_thms [] trm
+in positive position. Because of this, function types need to be
-end
+treated specially, since there the polarity changes.
+*)
-(******************************)
-(* 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
 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       *)
+(* produces an aggregate map function for the
-(* rty-part of a quotient definition; abstracts     *)
+rty-part of a quotient definition; abstracts
-(* over all variables listed in vs (these variables *)
+over all variables listed in vs (these variables
-(* correspond to the type variables in rty)         *)
+correspond to the type variables in rty)
-(*                                                  *)
-(* for example for: (?'a list * ?'b)                *)
+for example for: (?'a list * ?'b)
-(* it produces:     %a b. prod_map (map a) 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 =
 | _ => 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 *)
+(* looks up the (varified) rty and qty for
-(* a quotient definition                   *)
+a quotient definition
+*)
 fun get_rty_qty ctxt s =
 let
 val thy = ProofContext.theory_of ctxt
 val exc = LIFT_MATCH ("No quotient type " ^ (quote s) ^ " found.")
 val qdata = (quotdata_lookup thy s) handle NotFound => raise exc
 in
 (#rtyp qdata, #qtyp qdata)
 end
-(* takes two type-environments and looks    *)
+(* takes two type-environments and looks
-(* up in both of them the variable v, which *)
+up in both of them the variable v, which
-(* must be listed in the environment        *)
+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')))
 in
 raise LIFT_MATCH (space_implode " "
 ["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
 end
-(* produces an aggregate absrep function                           *)
-(*                                                                 *)
+(** generation of an aggregate absrep function **)
-(* - In case of equal types we just return the identity.           *)
-(*                                                                 *)
+(* - In case of equal types we just return the identity.
-(* - In case of function types and TFrees, we recurse, taking in   *)
-(*   the first case the polarity change into account.              *)
+- In case of TFrees we also return the identity.
-(*                                                                 *)
-(* - If the type constructors are equal, we recurse for the        *)
+- In case of function types we recurse taking
-(*   arguments and build the appropriate map function.             *)
+the polarity change into account.
-(*                                                                 *)
-(* - If the type constructors are unequal, there must be an        *)
+- If the type constructors are equal, we recurse for the
-(*   instance of quotient types:                                   *)
+arguments and build the appropriate map function.
-(*     - we first look up the corresponding rty_pat and qty_pat    *)
-(*       from the quotient definition; the arguments of qty_pat    *)
+- If the type constructors are unequal, there must be an
-(*       must be some distinct TVars                               *)
+instance of quotient types:
-(*     - we then match the rty_pat with rty and qty_pat with qty;  *)
-(*       if matching fails the types do not match                  *)
+- we first look up the corresponding rty_pat and qty_pat
-(*     - the matching produces two environments; we look up the    *)
+from the quotient definition; the arguments of qty_pat
-(*       assignments for the qty_pat variables and recurse on the  *)
+must be some distinct TVars
-(*       assignments                                               *)
+- we then match the rty_pat with rty and qty_pat with qty;
-(*     - we prefix the aggregate map function for the rty_pat,     *)
+if matching fails the types do not correspond -> error
-(*       which is an abstraction over all type variables           *)
+- the matching produces two environments; we look up the
-(*     - finally we compose the result with the appropriate        *)
+assignments for the qty_pat variables and recurse on the
-(*       absrep function                                           *)
+assignments
-(*                                                                 *)
+- we prefix the aggregate map function for the rty_pat,
-(*   The composition is necessary for types like                   *)
+which is an abstraction over all type variables
-(*                                                                 *)
+- finally we compose the result with the appropriate
-(*      ('a list) list / ('a foo) foo                              *)
+absrep function in case at least one argument produced
-(*                                                                 *)
+a non-identity function /
-(*   The matching is necessary for types like                      *)
+otherwise we just return the appropriate absrep
-(*                                                                 *)
+function
-(*      ('a * 'a) list / 'a bar                                    *)
+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 superflous
+identity maps.
+*)
 fun absrep_fun flag ctxt (rty, qty) =
 if rty = qty
 then mk_identity rty
 else
 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
-mk_fun_compose flag (absrep_const flag ctxt s', result)
+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)")
 | _ => raise (LIFT_MATCH "absrep_fun (default)")
 fun absrep_fun_chk flag ctxt (rty, qty) =
 absrep_fun flag ctxt (rty, qty)
 |> Syntax.check_term ctxt
-|> id_simplify ctxt
-(**********************************)
-(* Aggregate Equivalence Relation *)
-(**********************************)
+(*** Aggregate Equivalence Relation ***)
+(* works very similar to the absrep generation,
+except there is no need for polarities
+*)
 (* instantiates TVars so that the term is of type ty *)
 fun force_typ ctxt trm ty =
 let
 val thy = ProofContext.theory_of ctxt
 val ty_inst = Sign.typ_match thy (trm_ty, ty) Vartab.empty
 in
 map_types (Envir.subst_type ty_inst) trm
 end
+fun is_eq (Const (@{const_name "op ="}, _)) = true
+| is_eq _ = false
 fun mk_rel_compose (trm1, trm2) =
-Const (@{const_name "pred_comp"}, dummyT) $ trm1 $
+Const (@{const_name "rel_conj"}, dummyT) $ trm1 $ trm2
-(Const (@{const_name "pred_comp"}, dummyT) $ trm2 $ trm1)
 fun get_relmap ctxt s =
 let
 val thy = ProofContext.theory_of ctxt
 val exc =  LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")
 in
 raise LIFT_MATCH (space_implode " "
 ["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
 end
-(* builds the aggregate equivalence relation *)
+(* builds the aggregate equivalence relation
-(* that will be the argument of Respects     *)
+that will be the argument of Respects
+*)
 fun equiv_relation ctxt (rty, qty) =
 if rty = qty
 then HOLogic.eq_const rty
 else
 case (rty, qty) of
 val rel_map = mk_relmap ctxt vs rty_pat
 val result = list_comb (rel_map, args)
 val eqv_rel = get_equiv_rel ctxt s'
 val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool})
 in
-mk_rel_compose (result, eqv_rel')
+if forall is_eq args
+then eqv_rel'
+else mk_rel_compose (result, eqv_rel')
 end
 | _ => HOLogic.eq_const rty
 fun equiv_relation_chk ctxt (rty, qty) =
 equiv_relation ctxt (rty, qty)
 |> Syntax.check_term ctxt
-|> id_simplify ctxt
-(******************)
+(*** Regularization ***)
-(* Regularization *)
-(******************)
 (* Regularizing an rtrm means:
 - Quantifiers over types that need lifting are replaced
 by bounded quantifiers, for example:
 val mk_babs = Const (@{const_name Babs}, dummyT)
 val mk_ball = Const (@{const_name Ball}, dummyT)
 val mk_bex  = Const (@{const_name Bex}, dummyT)
 val mk_resp = Const (@{const_name Respects}, dummyT)
-(* - applies f to the subterm of an abstraction,   *)
+(* - applies f to the subterm of an abstraction,
-(*   otherwise to the given term,                  *)
+otherwise to the given term,
-(* - used by regularize, therefore abstracted      *)
+- used by regularize, therefore abstracted
-(*   variables do not have to be treated specially *)
+variables do not have to be treated specially
+*)
 fun apply_subt f (trm1, trm2) =
 case (trm1, trm2) of
 (Abs (x, T, t), Abs (_ , _, t')) => Abs (x, T, f (t, t'))
 | _ => f (trm1, trm2)
 (* the major type of All and Ex quantifiers *)
 fun qnt_typ ty = domain_type (domain_type ty)
+(* produces a regularized version of rtrm
-(* produces a regularized version of rtrm       *)
-(*                                              *)
+- the result might contain dummyTs
-(* - the result might contain dummyTs           *)
-(*                                              *)
+- for regularisation we do not need any
-(* - for regularisation we do not need any      *)
+special treatment of bound variables
-(*   special treatment of bound variables       *)
+*)
 fun regularize_trm ctxt (rtrm, qtrm) =
 case (rtrm, qtrm) of
 (Abs (x, ty, t), Abs (_, ty', t')) =>
 let
 val subtrm = Abs(x, ty, regularize_trm ctxt (t, t'))
 end
 fun regularize_trm_chk ctxt (rtrm, qtrm) =
 regularize_trm ctxt (rtrm, qtrm)
 |> Syntax.check_term ctxt
-|> id_simplify ctxt
 (*********************)
 (* Rep/Abs Injection *)
 (*********************)
 | _ => inj_repabs_err ctxt "injection (default):" rtrm qtrm
 fun inj_repabs_trm_chk ctxt (rtrm, qtrm) =
 inj_repabs_trm ctxt (rtrm, qtrm)
 |> Syntax.check_term ctxt
-|> id_simplify ctxt
 end; (* structure *)

changeset 854	5961edda27d7
parent 836	c2501b2b262a
child 856	433f7c17255f