diff -r 0eb018699f46 -r fa2b4b7af755 Quot/quotient_term.ML --- 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') =>