--- a/Quot/quotient_term.ML Tue Dec 22 22:10:48 2009 +0100
+++ b/Quot/quotient_term.ML Wed Dec 23 10:31:54 2009 +0100
@@ -21,10 +21,13 @@
exception LIFT_MATCH of string
-(* Calculates the aggregate abs and rep functions for a given type; *)
-(* repF is for constants' arguments; absF is for constants; *)
-(* function types need to be treated specially, since repF and absF *)
-(* change *)
+(*******************************)
+(* Aggregate Rep/Abs Functions *)
+(*******************************)
+
+(* The flag repF is for types in negative position, while 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
@@ -38,19 +41,19 @@
absF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2
| repF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1
-fun absrep_fun_aux lthy s fs =
+fun get_map ctxt ty_str =
let
- val thy = ProofContext.theory_of lthy
- val exc = LIFT_MATCH (space_implode " " ["absrep_fun_aux: no map for type", quote s, "."])
- val info = maps_lookup thy s handle NotFound => raise exc
+ val thy = ProofContext.theory_of ctxt
+ val exc = LIFT_MATCH (space_implode " " ["absrep_fun: no map for type", quote ty_str, "."])
+ val info = maps_lookup thy ty_str handle NotFound => raise exc
in
- list_comb (Const (#mapfun info, dummyT), fs)
+ Const (#mapfun info, dummyT)
end
-fun get_const flag lthy _ qty =
+fun get_absrep_const flag ctxt _ qty =
(* FIXME: check here that the type-constructors of _ and qty are related *)
let
- val thy = ProofContext.theory_of lthy
+ val thy = ProofContext.theory_of ctxt
val qty_name = Long_Name.base_name (fst (dest_Type qty))
in
case flag of
@@ -58,41 +61,42 @@
| repF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT)
end
-fun absrep_fun flag lthy (rty, qty) =
+fun absrep_fun flag ctxt (rty, qty) =
if rty = qty then mk_identity qty else
case (rty, qty) of
(Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) =>
- let
- val fs_ty1 = absrep_fun (negF flag) lthy (ty1, ty1')
- val fs_ty2 = absrep_fun flag lthy (ty2, ty2')
- in
- absrep_fun_aux lthy "fun" [fs_ty1, fs_ty2]
- end
+ let
+ val arg1 = absrep_fun (negF flag) ctxt (ty1, ty1')
+ val arg2 = absrep_fun flag ctxt (ty2, ty2')
+ in
+ list_comb (get_map ctxt "fun", [arg1, arg2])
+ end
| (Type (s, _), Type (s', [])) =>
- if s = s'
- then mk_identity qty
- else get_const flag lthy rty qty
+ if s = s'
+ then mk_identity qty
+ else get_absrep_const flag ctxt rty qty
| (Type (s, tys), Type (s', tys')) =>
- let
- val args = map (absrep_fun flag lthy) (tys ~~ tys')
- in
+ let
+ val args = map (absrep_fun flag ctxt) (tys ~~ tys')
+ val result = list_comb (get_map ctxt s, args)
+ in
if s = s'
- then absrep_fun_aux lthy s args
- else mk_compose flag (get_const flag lthy rty qty, absrep_fun_aux lthy s args)
- end
+ then result
+ else mk_compose flag (get_absrep_const flag ctxt rty qty, result)
+ end
| (TFree x, TFree x') =>
- if x = x'
- then mk_identity qty
- else raise (LIFT_MATCH "absrep_fun (frees)")
+ if x = x'
+ then mk_identity qty
+ else raise (LIFT_MATCH "absrep_fun (frees)")
| (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)")
| _ => raise (LIFT_MATCH "absrep_fun (default)")
-fun absrep_fun_chk flag lthy (rty, qty) =
- absrep_fun flag lthy (rty, qty)
- |> Syntax.check_term lthy
+fun absrep_fun_chk flag ctxt (rty, qty) =
+ absrep_fun flag ctxt (rty, qty)
+ |> Syntax.check_term ctxt
-(*
-Regularizing an rtrm means:
+
+(* Regularizing an rtrm means:
- Quantifiers over types that need lifting are replaced
by bounded quantifiers, for example:
@@ -120,9 +124,9 @@
(* builds the aggregate equivalence relation *)
(* that will be the argument of Respects *)
-fun mk_resp_arg lthy (rty, qty) =
+fun mk_resp_arg ctxt (rty, qty) =
let
- val thy = ProofContext.theory_of lthy
+ val thy = ProofContext.theory_of ctxt
in
if rty = qty
then HOLogic.eq_const rty
@@ -134,7 +138,7 @@
let
val exc = LIFT_MATCH ("mk_resp_arg (no map function found for type " ^ s)
val map_info = maps_lookup thy s handle NotFound => raise exc
- val args = map (mk_resp_arg lthy) (tys ~~ tys')
+ val args = map (mk_resp_arg ctxt) (tys ~~ tys')
in
list_comb (Const (#relfun map_info, dummyT), args)
end
@@ -180,43 +184,43 @@
(* - for regularisation we do not need any *)
(* special treatment of bound variables *)
-fun regularize_trm lthy (rtrm, qtrm) =
+fun regularize_trm ctxt (rtrm, qtrm) =
case (rtrm, qtrm) of
(Abs (x, ty, t), Abs (_, ty', t')) =>
let
- val subtrm = Abs(x, ty, regularize_trm lthy (t, t'))
+ val subtrm = Abs(x, ty, regularize_trm ctxt (t, t'))
in
if ty = ty' then subtrm
- else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm
+ else mk_babs $ (mk_resp $ mk_resp_arg ctxt (ty, ty')) $ subtrm
end
| (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
let
- val subtrm = apply_subt (regularize_trm lthy) (t, t')
+ val subtrm = apply_subt (regularize_trm ctxt) (t, t')
in
if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm
- else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm
+ else mk_ball $ (mk_resp $ mk_resp_arg ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
end
| (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
let
- val subtrm = apply_subt (regularize_trm lthy) (t, t')
+ val subtrm = apply_subt (regularize_trm ctxt) (t, t')
in
if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm
- else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm
+ else mk_bex $ (mk_resp $ mk_resp_arg ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
end
| (* 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 mk_resp_arg lthy (domain_type ty, domain_type ty')
+ else mk_resp_arg ctxt (domain_type ty, domain_type ty')
| (* in this case we just check whether the given equivalence relation is correct *)
(rel, Const (@{const_name "op ="}, ty')) =>
let
val exc = LIFT_MATCH "regularise (relation mismatch)"
val rel_ty = (fastype_of rel) handle TERM _ => raise exc
- val rel' = mk_resp_arg lthy (domain_type rel_ty, domain_type ty')
+ val rel' = mk_resp_arg ctxt (domain_type rel_ty, domain_type ty')
in
if rel' aconv rel then rtrm else raise exc
end
@@ -241,8 +245,8 @@
if same_name rtrm qtrm then rtrm
else
let
- val thy = ProofContext.theory_of lthy
- val qtrm_str = Syntax.string_of_term lthy qtrm
+ val thy = ProofContext.theory_of ctxt
+ val qtrm_str = Syntax.string_of_term ctxt qtrm
val exc1 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " not found)")
val exc2 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " mismatch)")
val rtrm' = (#rconst (qconsts_lookup thy qtrm)) handle NotFound => raise exc1
@@ -253,7 +257,7 @@
end
| (t1 $ t2, t1' $ t2') =>
- (regularize_trm lthy (t1, t1')) $ (regularize_trm lthy (t2, t2'))
+ (regularize_trm ctxt (t1, t1')) $ (regularize_trm ctxt (t2, t2'))
| (Bound i, Bound i') =>
if i = i' then rtrm
@@ -261,15 +265,15 @@
| _ =>
let
- val rtrm_str = Syntax.string_of_term lthy rtrm
- val qtrm_str = Syntax.string_of_term lthy qtrm
+ val rtrm_str = Syntax.string_of_term ctxt rtrm
+ val qtrm_str = Syntax.string_of_term ctxt qtrm
in
raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")"))
end
-fun regularize_trm_chk lthy (rtrm, qtrm) =
- regularize_trm lthy (rtrm, qtrm)
- |> Syntax.check_term lthy
+fun regularize_trm_chk ctxt (rtrm, qtrm) =
+ regularize_trm ctxt (rtrm, qtrm)
+ |> Syntax.check_term ctxt
(*
Injection of Rep/Abs means:
@@ -299,27 +303,27 @@
Vars case cannot occur.
*)
-fun mk_repabs lthy (T, T') trm =
- absrep_fun repF lthy (T, T') $ (absrep_fun absF lthy (T, T') $ trm)
+fun mk_repabs ctxt (T, T') trm =
+ absrep_fun repF ctxt (T, T') $ (absrep_fun absF ctxt (T, T') $ trm)
(* bound variables need to be treated properly, *)
(* as the type of subterms needs to be calculated *)
-fun inj_repabs_trm lthy (rtrm, qtrm) =
+fun inj_repabs_trm ctxt (rtrm, qtrm) =
case (rtrm, qtrm) of
(Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>
- Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm lthy (t, t'))
+ Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
| (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>
- Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm lthy (t, t'))
+ Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
| (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) =>
let
val rty = fastype_of rtrm
val qty = fastype_of qtrm
in
- mk_repabs lthy (rty, qty) (Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t')))
+ mk_repabs ctxt (rty, qty) (Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm ctxt (t, t')))
end
| (Abs (x, T, t), Abs (x', T', t')) =>
@@ -329,18 +333,18 @@
val (y, s) = Term.dest_abs (x, T, t)
val (_, s') = Term.dest_abs (x', T', t')
val yvar = Free (y, T)
- val result = Term.lambda_name (y, yvar) (inj_repabs_trm lthy (s, s'))
+ val result = Term.lambda_name (y, yvar) (inj_repabs_trm ctxt (s, s'))
in
if rty = qty then result
- else mk_repabs lthy (rty, qty) result
+ else mk_repabs ctxt (rty, qty) result
end
| (t $ s, t' $ s') =>
- (inj_repabs_trm lthy (t, t')) $ (inj_repabs_trm lthy (s, s'))
+ (inj_repabs_trm ctxt (t, t')) $ (inj_repabs_trm ctxt (s, s'))
| (Free (_, T), Free (_, T')) =>
if T = T' then rtrm
- else mk_repabs lthy (T, T') rtrm
+ else mk_repabs ctxt (T, T') rtrm
| (_, Const (@{const_name "op ="}, _)) => rtrm
@@ -349,14 +353,14 @@
val rty = fastype_of rtrm
in
if rty = T' then rtrm
- else mk_repabs lthy (rty, T') rtrm
+ else mk_repabs ctxt (rty, T') rtrm
end
| _ => raise (LIFT_MATCH "injection (default)")
-fun inj_repabs_trm_chk lthy (rtrm, qtrm) =
- inj_repabs_trm lthy (rtrm, qtrm)
- |> Syntax.check_term lthy
+fun inj_repabs_trm_chk ctxt (rtrm, qtrm) =
+ inj_repabs_trm ctxt (rtrm, qtrm)
+ |> Syntax.check_term ctxt
end; (* structure *)