--- a/Quot/quotient_term.ML Tue Jan 12 17:46:35 2010 +0100
+++ b/Quot/quotient_term.ML Wed Jan 13 09:19:20 2010 +0100
@@ -24,27 +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 ***)
-(* 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) =
@@ -64,12 +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
@@ -84,7 +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
@@ -94,8 +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)
@@ -132,38 +135,50 @@
["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.
+(** generation of an aggregate absrep 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
+(* - 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 composition is necessary for types like
-
- ('a list) list / ('a foo) foo
+ The test is necessary in order to eliminate superflous
+ identity maps.
+*)
- The matching is necessary for types like
-
- ('a * 'a) list / 'a bar *)
fun absrep_fun flag ctxt (rty, qty) =
if rty = qty
then mk_identity rty
@@ -189,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'
@@ -206,12 +223,17 @@
fun absrep_fun_chk flag ctxt (rty, qty) =
absrep_fun flag ctxt (rty, qty)
|> Syntax.check_term ctxt
- |> id_simplify ctxt
+
(*** 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
@@ -222,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
@@ -266,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
@@ -293,31 +318,32 @@
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 ***)
(* Regularizing an rtrm means:
-
- - Quantifiers over types that need lifting are replaced
+
+ - Quantifiers over types that need lifting are replaced
by bounded quantifiers, for example:
All P ----> All (Respects R) P
where the aggregate relation R is given by the rty and qty;
-
+
- Abstractions over types that need lifting are replaced
by bounded abstractions, for example:
-
+
%x. P ----> Ball (Respects R) %x. P
- Equalities over types that need lifting are replaced by
@@ -338,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'))
@@ -350,10 +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 to treat bound variables specially *)
+ - 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')) =>
@@ -455,7 +485,6 @@
fun regularize_trm_chk ctxt (rtrm, qtrm) =
regularize_trm ctxt (rtrm, qtrm)
|> Syntax.check_term ctxt
- |> id_simplify ctxt
@@ -555,7 +584,6 @@
fun inj_repabs_trm_chk ctxt (rtrm, qtrm) =
inj_repabs_trm ctxt (rtrm, qtrm)
|> Syntax.check_term ctxt
- |> id_simplify ctxt
end; (* structure *)