nominal2: comparison Quot/quotient

equal deleted inserted replaced

-:54f186bb5e3e
+:3b21b24a5fb6
 open Quotient_Info;
 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;         *)
+(* Aggregate Rep/Abs Functions *)
-(* function types need to be treated specially, since repF and absF *)
+(*******************************)
-(* change                                                           *)
+(* 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
 fun negF absF = repF
 | negF repF = absF
 fun mk_compose flag (trm1, trm2) =
 case flag of
 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 thy = ProofContext.theory_of ctxt
-val exc = LIFT_MATCH (space_implode " " ["absrep_fun_aux: no map for type", quote s, "."])
+val exc = LIFT_MATCH (space_implode " " ["absrep_fun: no map for type", quote ty_str, "."])
-val info = maps_lookup thy s handle NotFound => raise exc
+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
 absF => Const (Sign.full_bname thy ("abs_" ^ qty_name), dummyT)
 | 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 arg1 = absrep_fun (negF flag) ctxt (ty1, ty1')
-val fs_ty2 = absrep_fun flag lthy (ty2, ty2')
+val arg2 = absrep_fun flag ctxt (ty2, ty2')
 in
-absrep_fun_aux lthy "fun" [fs_ty1, fs_ty2]
+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
+else get_absrep_const flag ctxt rty qty
 | (Type (s, tys), Type (s', tys')) =>
 let
-val args = map (absrep_fun flag lthy) (tys ~~ tys')
+val args = map (absrep_fun flag ctxt) (tys ~~ tys')
-in
+val result = list_comb (get_map ctxt s, args)
+in
 if s = s'
-then absrep_fun_aux lthy s args
+then result
-else mk_compose flag (get_const flag lthy rty qty, absrep_fun_aux lthy s args)
+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)")
 | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)")
 | _ => raise (LIFT_MATCH "absrep_fun (default)")
-fun absrep_fun_chk flag lthy (rty, qty) =
+fun absrep_fun_chk flag ctxt (rty, qty) =
-absrep_fun flag lthy (rty, qty)
+absrep_fun flag ctxt (rty, qty)
-|> Syntax.check_term lthy
+|> 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:
 All P  ----> All (Respects R) P
 for more complicated types of A and B
 *)
 (* 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
 else
 case (rty, qty) of
 if s = s'
 then
 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
 else
 let
 (* - the result still contains dummyTs          *)
 (*                                              *)
 (* - 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
 | (_, Const _) =>
 (* 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 thy = ProofContext.theory_of ctxt
-val qtrm_str = Syntax.string_of_term lthy qtrm
+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
 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'))
+(regularize_trm ctxt (t1, t1')) $ (regularize_trm ctxt (t2, t2'))
 | (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 rtrm_str = Syntax.string_of_term ctxt rtrm
-val qtrm_str = Syntax.string_of_term lthy qtrm
+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) =
+fun regularize_trm_chk ctxt (rtrm, qtrm) =
-regularize_trm lthy (rtrm, qtrm)
+regularize_trm ctxt (rtrm, qtrm)
-|> Syntax.check_term lthy
+|> Syntax.check_term ctxt
 (*
 Injection of Rep/Abs means:
 For abstractions
 * We put aRep/Abs around it if the type needs lifting.
 Vars case cannot occur.
 *)
-fun mk_repabs lthy (T, T') trm =
+fun mk_repabs ctxt (T, T') trm =
-absrep_fun repF lthy (T, T') $ (absrep_fun absF lthy (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')) =>
 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'))
+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
 | (_, Const (_, T')) =>
 let
 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) =
+fun inj_repabs_trm_chk ctxt (rtrm, qtrm) =
-inj_repabs_trm lthy (rtrm, qtrm)
+inj_repabs_trm ctxt (rtrm, qtrm)
-|> Syntax.check_term lthy
+|> Syntax.check_term ctxt
 end; (* structure *)

changeset 779	3b21b24a5fb6
parent 776	d1064fa29424
child 782	86c7ed9f354f