--- a/Quot/quotient_term.ML Tue Jan 12 16:03:51 2010 +0100
+++ b/Quot/quotient_term.ML Tue Jan 12 16:12:54 2010 +0100
@@ -33,14 +33,13 @@
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
@@ -65,13 +64,12 @@
(* 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 +84,7 @@
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 +94,8 @@
(#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,39 +132,38 @@
["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 *)
+(* 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 *)
fun absrep_fun flag ctxt (rty, qty) =
if rty = qty
then mk_identity rty
@@ -213,9 +208,9 @@
|> Syntax.check_term ctxt
|> id_simplify ctxt
-(**********************************)
-(* Aggregate Equivalence Relation *)
-(**********************************)
+
+
+(*** Aggregate Equivalence Relation ***)
(* instantiates TVars so that the term is of type ty *)
fun force_typ ctxt trm ty =
@@ -271,8 +266,8 @@
["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
@@ -308,9 +303,8 @@
|> id_simplify ctxt
-(******************)
-(* Regularization *)
-(******************)
+
+(*** Regularization ***)
(* Regularizing an rtrm means:
@@ -468,15 +462,14 @@
|> id_simplify ctxt
-(*********************)
-(* Rep/Abs Injection *)
-(*********************)
+
+(*** Rep/Abs Injection ***)
(*
Injection of Rep/Abs means:
- For abstractions
-:
+ For abstractions:
+
* If the type of the abstraction needs lifting, then we add Rep/Abs
around the abstraction; otherwise we leave it unchanged.
@@ -513,9 +506,8 @@
end
-(* bound variables need to be treated properly, *)
-(* as the type of subterms needs to be calculated *)
-
+(* bound variables need to be treated properly,
+ as the type of subterms needs to be calculated *)
fun inj_repabs_trm ctxt (rtrm, qtrm) =
case (rtrm, qtrm) of
(Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>