--- a/Quot/quotient_term.ML Tue Jan 12 10:59:51 2010 +0100
+++ b/Quot/quotient_term.ML Wed Jan 13 00:45:28 2010 +0100
@@ -24,28 +24,24 @@
exception LIFT_MATCH of string
-(* simplifies a term according to the id_rules *)
-fun id_simplify ctxt trm =
-let
- val thy = ProofContext.theory_of ctxt
- val id_thms = id_simps_get ctxt
-in
- MetaSimplifier.rewrite_term thy id_thms [] trm
-end
-
-(******************************)
-(* Aggregate Rep/Abs Function *)
-(******************************)
+
+
+(*** 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. *)
+(* 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) =
@@ -65,13 +61,14 @@
(* 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 *)
+(* 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
@@ -86,8 +83,9 @@
fold_rev Term.lambda vs' (mk_mapfun_aux rty)
end
-(* looks up the (varified) rty and qty for *)
-(* a quotient definition *)
+(* looks up the (varified) rty and qty for
+ a quotient definition
+*)
fun get_rty_qty ctxt s =
let
val thy = ProofContext.theory_of ctxt
@@ -97,9 +95,10 @@
(#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 *)
+(* 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)
@@ -136,38 +135,49 @@
["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
end
-(* produces an aggregate absrep function *)
-(* *)
-(* - 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. *)
-(* *)
-(* - 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 match *)
-(* - 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 *)
-(* *)
-(* 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 *)
+
+(** 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 superflous
+ identity maps.
+*)
fun absrep_fun flag ctxt (rty, qty) =
if rty = qty
@@ -194,12 +204,14 @@
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_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'
@@ -211,11 +223,16 @@
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 =
@@ -227,9 +244,11 @@
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 "pred_comp"}, dummyT) $ trm2 $ trm1)
+ Const (@{const_name "rel_conj"}, dummyT) $ trm1 $ trm2
fun get_relmap ctxt s =
let
@@ -271,8 +290,9 @@
["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
end
-(* builds the aggregate equivalence relation *)
-(* that will be the argument of Respects *)
+(* builds the aggregate equivalence relation
+ that will be the argument of Respects
+*)
fun equiv_relation ctxt (rty, qty) =
if rty = qty
then HOLogic.eq_const rty
@@ -298,19 +318,19 @@
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:
@@ -344,10 +364,11 @@
val mk_bex = Const (@{const_name Bex}, dummyT)
val mk_resp = Const (@{const_name Respects}, dummyT)
-(* - applies f to the subterm of an abstraction, *)
-(* otherwise to the given term, *)
-(* - used by regularize, therefore abstracted *)
-(* variables do not have to be treated specially *)
+(* - applies f to the subterm of an abstraction,
+ otherwise to the given term,
+ - used by regularize, therefore abstracted
+ 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'))
@@ -356,14 +377,13 @@
(* 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 *)
-(* *)
-(* - for regularisation we do not need any *)
-(* special treatment of bound variables *)
+ - the result might contain dummyTs
+ - for regularisation we do not need any
+ special treatment of bound variables
+*)
fun regularize_trm ctxt (rtrm, qtrm) =
case (rtrm, qtrm) of
(Abs (x, ty, t), Abs (_, ty', t')) =>
@@ -465,7 +485,6 @@
fun regularize_trm_chk ctxt (rtrm, qtrm) =
regularize_trm ctxt (rtrm, qtrm)
|> Syntax.check_term ctxt
- |> id_simplify ctxt
(*********************)
@@ -567,7 +586,6 @@
fun inj_repabs_trm_chk ctxt (rtrm, qtrm) =
inj_repabs_trm ctxt (rtrm, qtrm)
|> Syntax.check_term ctxt
- |> id_simplify ctxt
end; (* structure *)