--- a/Quot/quotient_term.ML Thu Feb 11 09:23:59 2010 +0100
+++ b/Quot/quotient_term.ML Thu Feb 11 10:06:02 2010 +0100
@@ -41,9 +41,9 @@
(*** 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
@@ -56,7 +56,7 @@
fun mk_identity ty = Const (@{const_name "id"}, ty --> ty)
-fun mk_fun_compose flag (trm1, trm2) =
+fun mk_fun_compose flag (trm1, trm2) =
case flag of
AbsF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2
| RepF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1
@@ -73,13 +73,13 @@
(* 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
@@ -95,8 +95,8 @@
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
@@ -107,9 +107,9 @@
(#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
@@ -145,58 +145,58 @@
fun absrep_match_err ctxt ty_pat ty =
let
val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
- val ty_str = Syntax.string_of_typ ctxt ty
+ val ty_str = Syntax.string_of_typ ctxt ty
in
- raise LIFT_MATCH (space_implode " "
+ raise LIFT_MATCH (space_implode " "
["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
end
(** 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 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
+
+ - 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
+ 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 superfluous
- identity maps.
-*)
+ identity maps.
+*)
fun absrep_fun flag ctxt (rty, qty) =
- if rty = qty
+ if rty = qty
then mk_identity rty
else
case (rty, qty) of
@@ -209,12 +209,12 @@
end
| (Type (s, tys), Type (s', tys')) =>
if s = s'
- then
+ then
let
val args = map (absrep_fun flag ctxt) (tys ~~ tys')
in
list_comb (get_mapfun ctxt s, args)
- end
+ end
else
let
val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
@@ -222,8 +222,8 @@
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)
+ val map_fun = mk_mapfun ctxt vs rty_pat
+ val result = list_comb (map_fun, args)
in
if forall is_identity args
then absrep_const flag ctxt s'
@@ -253,7 +253,7 @@
(* instantiates TVars so that the term is of type ty *)
fun force_typ ctxt trm ty =
let
- val thy = ProofContext.theory_of ctxt
+ val thy = ProofContext.theory_of ctxt
val trm_ty = fastype_of trm
val ty_inst = Sign.typ_match thy (trm_ty, ty) Vartab.empty
in
@@ -269,7 +269,7 @@
fun get_relmap ctxt s =
let
val thy = ProofContext.theory_of ctxt
- val exn = LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")
+ val exn = LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")
val relmap = #relmap (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn
in
Const (relmap, dummyT)
@@ -292,7 +292,7 @@
fun get_equiv_rel ctxt s =
let
val thy = ProofContext.theory_of ctxt
- val exn = LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")
+ val exn = LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")
in
#equiv_rel (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn
end
@@ -300,14 +300,14 @@
fun equiv_match_err ctxt ty_pat ty =
let
val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
- val ty_str = Syntax.string_of_typ ctxt ty
+ val ty_str = Syntax.string_of_typ ctxt ty
in
- raise LIFT_MATCH (space_implode " "
+ 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
- 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
@@ -315,26 +315,26 @@
else
case (rty, qty) of
(Type (s, tys), Type (s', tys')) =>
- if s = s'
- then
+ if s = s'
+ then
let
val args = map (equiv_relation ctxt) (tys ~~ tys')
in
- list_comb (get_relmap ctxt s, args)
- end
- else
+ list_comb (get_relmap ctxt s, args)
+ end
+ else
let
val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
val rtyenv = match ctxt equiv_match_err rty_pat rty
val qtyenv = match ctxt equiv_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 (equiv_relation ctxt) args_aux
- val rel_map = mk_relmap ctxt vs rty_pat
+ 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
- if forall is_eq args
+ if forall is_eq args
then eqv_rel'
else mk_rel_compose (result, eqv_rel')
end
@@ -349,17 +349,17 @@
(*** 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
@@ -392,10 +392,10 @@
val mk_bex1_rel = Const (@{const_name Bex1_rel}, 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
@@ -433,10 +433,10 @@
(* produces a regularized version of rtrm
- - the result might contain dummyTs
+ - the result might contain dummyTs
- - for regularisation we do not need any
- special treatment of bound variables
+ - for regularisation we do not need any
+ special treatment of bound variables
*)
fun regularize_trm ctxt (rtrm, qtrm) =
case (rtrm, qtrm) of
@@ -474,8 +474,8 @@
end
| (Const (@{const_name "Ex1"}, ty) $ (Abs (_, _,
- (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op :"}, _) $ _ $
- (Const (@{const_name "Respects"}, _) $ resrel)) $ (t $ _)))),
+ (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op :"}, _) $ _ $
+ (Const (@{const_name "Respects"}, _) $ resrel)) $ (t $ _)))),
Const (@{const_name "Ex1"}, ty') $ t') =>
let
val t_ = incr_boundvars (~1) t
@@ -495,7 +495,7 @@
else mk_bex1_rel $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
end
- | (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t,
+ | (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t,
Const (@{const_name "All"}, ty') $ t') =>
let
val subtrm = apply_subt (regularize_trm ctxt) (t, t')
@@ -506,7 +506,7 @@
else mk_ball $ (mk_resp $ resrel) $ subtrm
end
- | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t,
+ | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t,
Const (@{const_name "Ex"}, ty') $ t') =>
let
val subtrm = apply_subt (regularize_trm ctxt) (t, t')
@@ -527,18 +527,18 @@
else mk_bex1_rel $ resrel $ subtrm
end
- | (* equalities need to be replaced by appropriate equivalence relations *)
+ | (* equalities need to be replaced by appropriate equivalence relations *)
(Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) =>
if ty = ty' then rtrm
- else equiv_relation ctxt (domain_type ty, domain_type ty')
+ else equiv_relation ctxt (domain_type ty, domain_type ty')
- | (* in this case we just check whether the given equivalence relation is correct *)
+ | (* in this case we just check whether the given equivalence relation is correct *)
(rel, Const (@{const_name "op ="}, ty')) =>
let
val rel_ty = fastype_of rel
- val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty')
+ val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty')
in
- if rel' aconv rel then rtrm
+ if rel' aconv rel then rtrm
else term_mismatch "regularise (relation mismatch)" ctxt rel rel'
end
@@ -557,7 +557,7 @@
if Pattern.matches thy (rtrm', rtrm)
then rtrm else term_mismatch "regularize(constant mismatch)" ctxt rtrm qtrm
end
- end
+ end
| (((t1 as Const (@{const_name "split"}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
((t2 as Const (@{const_name "split"}, _)) $ Abs (v2, _ , Abs(v2', _ , s2)))) =>
@@ -571,11 +571,11 @@
regularize_trm ctxt (t1, t1') $ regularize_trm ctxt (t2, t2')
| (Bound i, Bound i') =>
- if i = i' then rtrm
+ if i = i' then rtrm
else raise (LIFT_MATCH "regularize (bounds mismatch)")
| _ =>
- let
+ let
val rtrm_str = Syntax.string_of_term ctxt rtrm
val qtrm_str = Syntax.string_of_term ctxt qtrm
in
@@ -583,7 +583,7 @@
end
fun regularize_trm_chk ctxt (rtrm, qtrm) =
- regularize_trm ctxt (rtrm, qtrm)
+ regularize_trm ctxt (rtrm, qtrm)
|> Syntax.check_term ctxt
@@ -595,22 +595,22 @@
For abstractions:
- * If the type of the abstraction needs lifting, then we add Rep/Abs
+ * If the type of the abstraction needs lifting, then we add Rep/Abs
around the abstraction; otherwise we leave it unchanged.
-
+
For applications:
-
- * If the application involves a bounded quantifier, we recurse on
+
+ * If the application involves a bounded quantifier, we recurse on
the second argument. If the application is a bounded abstraction,
we always put an Rep/Abs around it (since bounded abstractions
- are assumed to always need lifting). Otherwise we recurse on both
+ are assumed to always need lifting). Otherwise we recurse on both
arguments.
For constants:
- * If the constant is (op =), we leave it always unchanged.
+ * If the constant is (op =), we leave it always unchanged.
Otherwise the type of the constant needs lifting, we put
- and Rep/Abs around it.
+ and Rep/Abs around it.
For free variables:
@@ -619,13 +619,13 @@
Vars case cannot occur.
*)
-fun mk_repabs ctxt (T, T') trm =
+fun mk_repabs ctxt (T, T') trm =
absrep_fun RepF ctxt (T, T') $ (absrep_fun AbsF ctxt (T, T') $ trm)
fun inj_repabs_err ctxt msg rtrm qtrm =
let
val rtrm_str = Syntax.string_of_term ctxt rtrm
- val qtrm_str = Syntax.string_of_term ctxt qtrm
+ val qtrm_str = Syntax.string_of_term ctxt qtrm
in
raise LIFT_MATCH (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str])
end
@@ -662,11 +662,11 @@
else mk_repabs ctxt (rty, qty) result
end
- | (t $ s, t' $ s') =>
+ | (t $ s, t' $ s') =>
(inj_repabs_trm ctxt (t, t')) $ (inj_repabs_trm ctxt (s, s'))
- | (Free (_, T), Free (_, T')) =>
- if T = T' then rtrm
+ | (Free (_, T), Free (_, T')) =>
+ if T = T' then rtrm
else mk_repabs ctxt (T, T') rtrm
| (_, Const (@{const_name "op ="}, _)) => rtrm
@@ -674,15 +674,15 @@
| (_, Const (_, T')) =>
let
val rty = fastype_of rtrm
- in
+ in
if rty = T' then rtrm
else mk_repabs ctxt (rty, T') rtrm
- end
-
+ end
+
| _ => inj_repabs_err ctxt "injection (default):" rtrm qtrm
fun inj_repabs_trm_chk ctxt (rtrm, qtrm) =
- inj_repabs_trm ctxt (rtrm, qtrm)
+ inj_repabs_trm ctxt (rtrm, qtrm)
|> Syntax.check_term ctxt