nominal2: comparison Quot/quotient

equal deleted inserted replaced

-:243a5ceaa088
+:17ca92ab4660
 (*** 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.
 *)
 datatype flag = AbsF | RepF
 fun negF AbsF = RepF
 fun is_identity (Const (@{const_name "id"}, _)) = true
 | is_identity _ = false
 fun mk_identity ty = Const (@{const_name "id"}, ty --> ty)
 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
 fun get_mapfun ctxt s =
 end
 (* 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
 *)
 fun mk_mapfun ctxt vs rty =
 let
 val vs' = map (mk_Free) vs
 | _ => raise LIFT_MATCH "mk_mapfun (default)"
 in
 fold_rev Term.lambda vs' (mk_mapfun_aux rty)
 end
 (* looks up the (varified) rty and qty for
 a quotient definition
 *)
 fun get_rty_qty ctxt s =
 let
 val thy = ProofContext.theory_of ctxt
 val exn = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
 val qdata = (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn
 in
 (#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
 *)
 fun double_lookup rtyenv qtyenv v =
 let
 val v' = fst (dest_TVar v)
 in
 Syntax.check_term ctxt (absrep_const flag ctxt qty_str)
 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
 in
 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 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
 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
 The test is necessary in order to eliminate superfluous
 identity maps.
 *)
 fun absrep_fun flag ctxt (rty, qty) =
 if rty = qty
 then mk_identity rty
 else
 case (rty, qty) of
 (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) =>
 let
 in
 list_comb (get_mapfun ctxt "fun", [arg1, arg2])
 end
 | (Type (s, tys), Type (s', tys')) =>
 if s = s'
 then
 let
 val args = map (absrep_fun flag ctxt) (tys ~~ tys')
 in
 list_comb (get_mapfun ctxt s, args)
 end
 else
 let
 val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
 val rtyenv = match ctxt absrep_match_err rty_pat rty
 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)
 in
 if forall is_identity args
 then absrep_const flag ctxt s'
 else mk_fun_compose flag (absrep_const flag ctxt s', result)
 end
 *)
 (* instantiates TVars so that the term is of type ty *)
 fun force_typ ctxt trm ty =
 let
 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
 map_types (Envir.subst_type ty_inst) trm
 end
 Const (@{const_name "rel_conj"}, dummyT) $ trm1 $ trm2
 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 relmap = #relmap (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn
 in
 Const (relmap, dummyT)
 end
 end
 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 ^ ")")
 in
 #equiv_rel (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn
 end
 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
 in
 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
 *)
 fun equiv_relation ctxt (rty, qty) =
 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 args = map (equiv_relation ctxt) (tys ~~ tys')
 in
 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 = map (equiv_relation ctxt) args_aux
 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
 then eqv_rel'
 else mk_rel_compose (result, eqv_rel')
 end
 | _ => HOLogic.eq_const rty
 (*** Regularization ***)
 (* Regularizing an rtrm means:
 - 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
 corresponding equivalence relations, for example:
 val mk_ball = Const (@{const_name Ball}, dummyT)
 val mk_bex  = Const (@{const_name Bex}, dummyT)
 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
 *)
 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)
 | _ => false
 (* produces a regularized version of rtrm
 - the result might contain dummyTs
 - for regularisation we do not need any
 special treatment of bound variables
 *)
 fun regularize_trm ctxt (rtrm, qtrm) =
 case (rtrm, qtrm) of
 (Abs (x, ty, t), Abs (_, ty', t')) =>
 let
 if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm
 else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
 end
 | (Const (@{const_name "Ex1"}, ty) $ (Abs (_, _,
 (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
 val subtrm = apply_subt (regularize_trm ctxt) (t_, t')
 val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
 in
 if ty = ty' then Const (@{const_name "Ex1"}, ty) $ subtrm
 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 "All"}, ty') $ t') =>
 let
 val subtrm = apply_subt (regularize_trm ctxt) (t, t')
 val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
 in
 if resrel <> needrel
 then term_mismatch "regularize (Ball)" ctxt resrel needrel
 else mk_ball $ (mk_resp $ resrel) $ subtrm
 end
 | (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')
 val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
 in
 if resrel <> needrel
 then term_mismatch "regularize (Bex1_res)" ctxt resrel needrel
 else mk_bex1_rel $ resrel $ 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 equiv_relation 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 rel_ty = fastype_of rel
 val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty')
 in
 if rel' aconv rel then rtrm
 else term_mismatch "regularise (relation mismatch)" ctxt rel rel'
 end
 | (_, Const _) =>
 let
 handle Quotient_Info.NotFound => term_mismatch "regularize(constant notfound)" ctxt rtrm qtrm
 in
 if Pattern.matches thy (rtrm', rtrm)
 then rtrm else term_mismatch "regularize(constant mismatch)" ctxt rtrm qtrm
 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)))) =>
 regularize_trm ctxt (t1, t2) $ Abs (v1, ty, Abs (v1', ty', regularize_trm ctxt (s1, s2)))
 | (t1 $ t2, t1' $ 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 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 ctxt (rtrm, qtrm) =
 regularize_trm ctxt (rtrm, qtrm)
 |> Syntax.check_term ctxt
 (*** Rep/Abs Injection ***)
 (*
 Injection of Rep/Abs means:
 For abstractions:
 * 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
 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
 arguments.
 For constants:
 * 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.
 For free variables:
 * We put a Rep/Abs around it if the type needs lifting.
 Vars case cannot occur.
 *)
 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
 in
 raise LIFT_MATCH (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str])
 end
 in
 if rty = qty then result
 else mk_repabs ctxt (rty, qty) result
 end
 | (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
 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 ctxt (rty, T') rtrm
 end
 | _ => inj_repabs_err ctxt "injection (default):" rtrm qtrm
 fun inj_repabs_trm_chk ctxt (rtrm, qtrm) =
 inj_repabs_trm ctxt (rtrm, qtrm)
 |> Syntax.check_term ctxt
 (*** Wrapper for automatically transforming an rthm into a qthm ***)

changeset 1128	17ca92ab4660
parent 1113	9f6c606d5b59
child 1188	e5413596e098