--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Quot/quotient_term.ML Thu Dec 17 14:58:33 2009 +0100
@@ -0,0 +1,278 @@
+signature QUOTIENT_TERM =
+sig
+ val regularize_trm: Proof.context -> term -> term -> term
+ val inj_repabs_trm: Proof.context -> (term * term) -> term
+end;
+
+structure Quotient_Term: QUOTIENT_TERM =
+struct
+
+(*
+Regularizing an rtrm means:
+
+ - Quantifiers over a type that need lifting are replaced
+ by bounded quantifiers, for example:
+
+ All P ===> All (Respects R) P
+
+ where the relation R is given by the rty and qty;
+
+ - Abstractions over a type that needs lifting are replaced
+ by bounded abstractions:
+
+ %x. P ===> Ball (Respects R) %x. P
+
+ - Equalities over the type being lifted are replaced by
+ corresponding equivalence relations:
+
+ A = B ===> R A B
+
+ or
+
+ A = B ===> (R ===> R) A B
+
+ for more complicated types of A and B
+*)
+
+(* builds the relation that is the argument of respects *)
+fun mk_resp_arg lthy (rty, qty) =
+let
+ val thy = ProofContext.theory_of lthy
+in
+ if rty = qty
+ then HOLogic.eq_const rty
+ else
+ case (rty, qty) of
+ (Type (s, tys), Type (s', tys')) =>
+ if s = s'
+ then let
+ val SOME map_info = maps_lookup thy s
+ (* FIXME dont return an option, raise an exception *)
+ val args = map (mk_resp_arg lthy) (tys ~~ tys')
+ in
+ list_comb (Const (#relfun map_info, dummyT), args)
+ end
+ else let
+ val SOME qinfo = quotdata_lookup_thy thy s'
+ (* FIXME: check in this case that the rty and qty *)
+ (* FIXME: correspond to each other *)
+ val (s, _) = dest_Const (#rel qinfo)
+ (* FIXME: the relation should only be the string *)
+ (* FIXME: and the type needs to be calculated as below; *)
+ (* FIXME: maybe one should actually have a term *)
+ (* FIXME: and one needs to force it to have this type *)
+ in
+ Const (s, rty --> rty --> @{typ bool})
+ end
+ | _ => HOLogic.eq_const dummyT
+ (* FIXME: check that the types correspond to each other? *)
+end
+
+val mk_babs = Const (@{const_name Babs}, dummyT)
+val mk_ball = Const (@{const_name Ball}, dummyT)
+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 *)
+fun apply_subt f trm1 trm2 =
+ case (trm1, trm2) of
+ (Abs (x, T, t), Abs (_ , _, t')) => Abs (x, T, f t t')
+ | _ => f trm1 trm2
+
+(* the major type of All and Ex quantifiers *)
+fun qnt_typ ty = domain_type (domain_type ty)
+
+
+(* produces a regularized version of rtrm *)
+(* *)
+(* - the result is still contains dummyT *)
+(* *)
+(* - for regularisation we do not need any *)
+(* special treatment of bound variables *)
+
+fun regularize_trm lthy rtrm qtrm =
+ case (rtrm, qtrm) of
+ (Abs (x, ty, t), Abs (_, ty', t')) =>
+ let
+ val subtrm = Abs(x, ty, regularize_trm lthy t t')
+ in
+ if ty = ty' then subtrm
+ else mk_babs $ (mk_resp $ mk_resp_arg lthy (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'
+ 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
+ end
+
+ | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
+ let
+ val subtrm = apply_subt (regularize_trm lthy) 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
+ 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')
+
+ | (* in this case we 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')
+ in
+ if rel' = rel then rtrm else raise exc
+ end
+
+ | (_, Const _) =>
+ let
+ fun same_name (Const (s, T)) (Const (s', T')) = (s = s') (*andalso (T = T')*)
+ | same_name _ _ = false
+ (* TODO/FIXME: This test is not enough. *)
+ (* Why? *)
+ (* Because constants can have the same name but not be the same
+ constant. All overloaded constants have the same name but because
+ of different types they do differ.
+
+ This code will let one write a theorem where plus on nat is
+ matched to plus on int, even if the latter is defined differently.
+
+ This would result in hard to understand failures in injection and
+ cleaning. *)
+ (* cu: if I also test the type, then something else breaks *)
+ in
+ 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 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
+ in
+ if Pattern.matches thy (rtrm', rtrm)
+ then rtrm else raise exc2
+ end
+ end
+
+ | (t1 $ t2, t1' $ t2') =>
+ (regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2')
+
+ | (Free (x, ty), Free (x', ty')) =>
+ (* this case cannot arrise as we start with two fully atomized terms *)
+ raise (LIFT_MATCH "regularize (frees)")
+
+ | (Bound i, Bound i') =>
+ if i = i' then rtrm
+ else raise (LIFT_MATCH "regularize (bounds mismatch)")
+
+ | _ =>
+ let
+ val rtrm_str = Syntax.string_of_term lthy rtrm
+ val qtrm_str = Syntax.string_of_term lthy qtrm
+ in
+ raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")"))
+ end
+
+
+
+(*
+Injecting of Rep/Abs means:
+
+ For abstractions
+:
+ * If the type of the abstraction doesn't need lifting we recurse.
+
+ * If it needs lifting then we add Rep/Abs around the whole term and
+ check if the bound variable needs lifting.
+
+ * If it does we recurse and put Rep/Abs around all occurences
+ of the variable in the obtained subterm. This in combination
+ with the Rep/Abs from above will let us change the type of
+ the abstraction with rewriting.
+
+ For applications:
+
+ * If the term is Respects applied to anything we leave it unchanged
+
+ * If the term needs lifting and the head is a constant that we know
+ how to lift, we put a Rep/Abs and recurse
+
+ * If the term needs lifting and the head is a Free applied to subterms
+ (if it is not applied we treated it in Abs branch) then we
+ put Rep/Abs and recurse
+
+ * Otherwise just recurse.
+*)
+
+fun mk_repabs lthy (T, T') trm =
+ Quotient_Def.get_fun repF lthy (T, T')
+ $ (Quotient_Def.get_fun absF lthy (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) =
+ 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 "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>
+ Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm lthy (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')))
+ end
+
+ | (Abs (x, T, t), Abs (x', T', t')) =>
+ let
+ val rty = fastype_of rtrm
+ val qty = fastype_of qtrm
+ 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'))
+ in
+ if rty = qty then result
+ else mk_repabs lthy (rty, qty) result
+ end
+
+ | (t $ s, t' $ s') =>
+ (inj_repabs_trm lthy (t, t')) $ (inj_repabs_trm lthy (s, s'))
+
+ | (Free (_, T), Free (_, T')) =>
+ if T = T' then rtrm
+ else mk_repabs lthy (T, T') rtrm
+
+ | (_, Const (@{const_name "op ="}, _)) => rtrm
+
+ | (_, Const (_, T')) =>
+ let
+ val rty = fastype_of rtrm
+ in
+ if rty = T' then rtrm
+ else mk_repabs lthy (rty, T') rtrm
+ end
+
+ | _ => raise (LIFT_MATCH "injection")
+
+end; (* structure *)
+
+open Quotient_Term;
+
+