kaliszyk@35222: (*  Title:      quotient_term.thy
kaliszyk@35222:     Author:     Cezary Kaliszyk and Christian Urban
kaliszyk@35222: 
kaliszyk@35222:     Constructs terms corresponding to goals from
kaliszyk@35222:     lifting theorems to quotient types.
kaliszyk@35222: *)
kaliszyk@35222: 
kaliszyk@35222: signature QUOTIENT_TERM =
kaliszyk@35222: sig
kaliszyk@35222:   exception LIFT_MATCH of string
kaliszyk@35222: 
kaliszyk@35222:   datatype flag = AbsF | RepF
kaliszyk@35222: 
kaliszyk@35222:   val absrep_fun: flag -> Proof.context -> typ * typ -> term
kaliszyk@35222:   val absrep_fun_chk: flag -> Proof.context -> typ * typ -> term
kaliszyk@35222: 
kaliszyk@35222:   (* Allows Nitpick to represent quotient types as single elements from raw type *)
kaliszyk@35222:   val absrep_const_chk: flag -> Proof.context -> string -> term
kaliszyk@35222: 
kaliszyk@35222:   val equiv_relation: Proof.context -> typ * typ -> term
kaliszyk@35222:   val equiv_relation_chk: Proof.context -> typ * typ -> term
kaliszyk@35222: 
kaliszyk@35222:   val regularize_trm: Proof.context -> term * term -> term
kaliszyk@35222:   val regularize_trm_chk: Proof.context -> term * term -> term
kaliszyk@35222: 
kaliszyk@35222:   val inj_repabs_trm: Proof.context -> term * term -> term
kaliszyk@35222:   val inj_repabs_trm_chk: Proof.context -> term * term -> term
kaliszyk@35222: 
kaliszyk@35222:   val quotient_lift_const: string * term -> local_theory -> term
kaliszyk@35222:   val quotient_lift_all: Proof.context -> term -> term
kaliszyk@35222: end;
kaliszyk@35222: 
kaliszyk@35222: structure Quotient_Term: QUOTIENT_TERM =
kaliszyk@35222: struct
kaliszyk@35222: 
kaliszyk@35222: open Quotient_Info;
kaliszyk@35222: 
kaliszyk@35222: exception LIFT_MATCH of string
kaliszyk@35222: 
kaliszyk@35222: 
kaliszyk@35222: 
kaliszyk@35222: (*** Aggregate Rep/Abs Function ***)
kaliszyk@35222: 
kaliszyk@35222: 
kaliszyk@35222: (* The flag RepF is for types in negative position; AbsF is for types
kaliszyk@35222:    in positive position. Because of this, function types need to be
kaliszyk@35222:    treated specially, since there the polarity changes.
kaliszyk@35222: *)
kaliszyk@35222: 
kaliszyk@35222: datatype flag = AbsF | RepF
kaliszyk@35222: 
kaliszyk@35222: fun negF AbsF = RepF
kaliszyk@35222:   | negF RepF = AbsF
kaliszyk@35222: 
kaliszyk@35222: fun is_identity (Const (@{const_name "id"}, _)) = true
kaliszyk@35222:   | is_identity _ = false
kaliszyk@35222: 
kaliszyk@35222: fun mk_identity ty = Const (@{const_name "id"}, ty --> ty)
kaliszyk@35222: 
kaliszyk@35222: fun mk_fun_compose flag (trm1, trm2) =
kaliszyk@35222:   case flag of
kaliszyk@35222:     AbsF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2
kaliszyk@35222:   | RepF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1
kaliszyk@35222: 
kaliszyk@35222: fun get_mapfun ctxt s =
kaliszyk@35222: let
kaliszyk@35222:   val thy = ProofContext.theory_of ctxt
kaliszyk@35222:   val exn = LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
kaliszyk@35222:   val mapfun = #mapfun (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn
kaliszyk@35222: in
kaliszyk@35222:   Const (mapfun, dummyT)
kaliszyk@35222: end
kaliszyk@35222: 
kaliszyk@35222: (* makes a Free out of a TVar *)
kaliszyk@35222: fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT)
kaliszyk@35222: 
kaliszyk@35222: (* produces an aggregate map function for the
kaliszyk@35222:    rty-part of a quotient definition; abstracts
kaliszyk@35222:    over all variables listed in vs (these variables
kaliszyk@35222:    correspond to the type variables in rty)
kaliszyk@35222: 
kaliszyk@35222:    for example for: (?'a list * ?'b)
kaliszyk@35222:    it produces:     %a b. prod_map (map a) b
kaliszyk@35222: *)
kaliszyk@35222: fun mk_mapfun ctxt vs rty =
kaliszyk@35222: let
kaliszyk@35222:   val vs' = map (mk_Free) vs
kaliszyk@35222: 
kaliszyk@35222:   fun mk_mapfun_aux rty =
kaliszyk@35222:     case rty of
kaliszyk@35222:       TVar _ => mk_Free rty
kaliszyk@35222:     | Type (_, []) => mk_identity rty
kaliszyk@35222:     | Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys)
kaliszyk@35222:     | _ => raise LIFT_MATCH "mk_mapfun (default)"
kaliszyk@35222: in
kaliszyk@35222:   fold_rev Term.lambda vs' (mk_mapfun_aux rty)
kaliszyk@35222: end
kaliszyk@35222: 
kaliszyk@35222: (* looks up the (varified) rty and qty for
kaliszyk@35222:    a quotient definition
kaliszyk@35222: *)
kaliszyk@35222: fun get_rty_qty ctxt s =
kaliszyk@35222: let
kaliszyk@35222:   val thy = ProofContext.theory_of ctxt
kaliszyk@35222:   val exn = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
kaliszyk@35222:   val qdata = (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn
kaliszyk@35222: in
kaliszyk@35222:   (#rtyp qdata, #qtyp qdata)
kaliszyk@35222: end
kaliszyk@35222: 
kaliszyk@35222: (* takes two type-environments and looks
kaliszyk@35222:    up in both of them the variable v, which
kaliszyk@35222:    must be listed in the environment
kaliszyk@35222: *)
kaliszyk@35222: fun double_lookup rtyenv qtyenv v =
kaliszyk@35222: let
kaliszyk@35222:   val v' = fst (dest_TVar v)
kaliszyk@35222: in
kaliszyk@35222:   (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v')))
kaliszyk@35222: end
kaliszyk@35222: 
kaliszyk@35222: (* matches a type pattern with a type *)
kaliszyk@35222: fun match ctxt err ty_pat ty =
kaliszyk@35222: let
kaliszyk@35222:   val thy = ProofContext.theory_of ctxt
kaliszyk@35222: in
kaliszyk@35222:   Sign.typ_match thy (ty_pat, ty) Vartab.empty
kaliszyk@35222:   handle MATCH_TYPE => err ctxt ty_pat ty
kaliszyk@35222: end
kaliszyk@35222: 
kaliszyk@35222: (* produces the rep or abs constant for a qty *)
kaliszyk@35222: fun absrep_const flag ctxt qty_str =
kaliszyk@35222: let
kaliszyk@35222:   val thy = ProofContext.theory_of ctxt
kaliszyk@35222:   val qty_name = Long_Name.base_name qty_str
kaliszyk@35222: in
kaliszyk@35222:   case flag of
kaliszyk@35222:     AbsF => Const (Sign.full_bname thy ("abs_" ^ qty_name), dummyT)
kaliszyk@35222:   | RepF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT)
kaliszyk@35222: end
kaliszyk@35222: 
kaliszyk@35222: (* Lets Nitpick represent elements of quotient types as elements of the raw type *)
kaliszyk@35222: fun absrep_const_chk flag ctxt qty_str =
kaliszyk@35222:   Syntax.check_term ctxt (absrep_const flag ctxt qty_str)
kaliszyk@35222: 
kaliszyk@35222: fun absrep_match_err ctxt ty_pat ty =
kaliszyk@35222: let
kaliszyk@35222:   val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
kaliszyk@35222:   val ty_str = Syntax.string_of_typ ctxt ty
kaliszyk@35222: in
kaliszyk@35222:   raise LIFT_MATCH (space_implode " "
kaliszyk@35222:     ["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
kaliszyk@35222: end
kaliszyk@35222: 
kaliszyk@35222: 
kaliszyk@35222: (** generation of an aggregate absrep function **)
kaliszyk@35222: 
kaliszyk@35222: (* - In case of equal types we just return the identity.
kaliszyk@35222: 
kaliszyk@35222:    - In case of TFrees we also return the identity.
kaliszyk@35222: 
kaliszyk@35222:    - In case of function types we recurse taking
kaliszyk@35222:      the polarity change into account.
kaliszyk@35222: 
kaliszyk@35222:    - If the type constructors are equal, we recurse for the
kaliszyk@35222:      arguments and build the appropriate map function.
kaliszyk@35222: 
kaliszyk@35222:    - If the type constructors are unequal, there must be an
kaliszyk@35222:      instance of quotient types:
kaliszyk@35222: 
kaliszyk@35222:        - we first look up the corresponding rty_pat and qty_pat
kaliszyk@35222:          from the quotient definition; the arguments of qty_pat
kaliszyk@35222:          must be some distinct TVars
kaliszyk@35222:        - we then match the rty_pat with rty and qty_pat with qty;
kaliszyk@35222:          if matching fails the types do not correspond -> error
kaliszyk@35222:        - the matching produces two environments; we look up the
kaliszyk@35222:          assignments for the qty_pat variables and recurse on the
kaliszyk@35222:          assignments
kaliszyk@35222:        - we prefix the aggregate map function for the rty_pat,
kaliszyk@35222:          which is an abstraction over all type variables
kaliszyk@35222:        - finally we compose the result with the appropriate
kaliszyk@35222:          absrep function in case at least one argument produced
kaliszyk@35222:          a non-identity function /
kaliszyk@35222:          otherwise we just return the appropriate absrep
kaliszyk@35222:          function
kaliszyk@35222: 
kaliszyk@35222:      The composition is necessary for types like
kaliszyk@35222: 
kaliszyk@35222:         ('a list) list / ('a foo) foo
kaliszyk@35222: 
kaliszyk@35222:      The matching is necessary for types like
kaliszyk@35222: 
kaliszyk@35222:         ('a * 'a) list / 'a bar
kaliszyk@35222: 
kaliszyk@35222:      The test is necessary in order to eliminate superfluous
kaliszyk@35222:      identity maps.
kaliszyk@35222: *)
kaliszyk@35222: 
kaliszyk@35222: fun absrep_fun flag ctxt (rty, qty) =
kaliszyk@35222:   if rty = qty
kaliszyk@35222:   then mk_identity rty
kaliszyk@35222:   else
kaliszyk@35222:     case (rty, qty) of
kaliszyk@35222:       (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) =>
kaliszyk@35222:         let
kaliszyk@35222:           val arg1 = absrep_fun (negF flag) ctxt (ty1, ty1')
kaliszyk@35222:           val arg2 = absrep_fun flag ctxt (ty2, ty2')
kaliszyk@35222:         in
kaliszyk@35222:           list_comb (get_mapfun ctxt "fun", [arg1, arg2])
kaliszyk@35222:         end
kaliszyk@35222:     | (Type (s, tys), Type (s', tys')) =>
kaliszyk@35222:         if s = s'
kaliszyk@35222:         then
kaliszyk@35222:            let
kaliszyk@35222:              val args = map (absrep_fun flag ctxt) (tys ~~ tys')
kaliszyk@35222:            in
kaliszyk@35222:              list_comb (get_mapfun ctxt s, args)
kaliszyk@35222:            end
kaliszyk@35222:         else
kaliszyk@35222:            let
kaliszyk@35222:              val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
kaliszyk@35222:              val rtyenv = match ctxt absrep_match_err rty_pat rty
kaliszyk@35222:              val qtyenv = match ctxt absrep_match_err qty_pat qty
kaliszyk@35222:              val args_aux = map (double_lookup rtyenv qtyenv) vs
kaliszyk@35222:              val args = map (absrep_fun flag ctxt) args_aux
kaliszyk@35222:              val map_fun = mk_mapfun ctxt vs rty_pat
kaliszyk@35222:              val result = list_comb (map_fun, args)
kaliszyk@35222:            in
kaliszyk@35222:              if forall is_identity args
kaliszyk@35222:              then absrep_const flag ctxt s'
kaliszyk@35222:              else mk_fun_compose flag (absrep_const flag ctxt s', result)
kaliszyk@35222:            end
kaliszyk@35222:     | (TFree x, TFree x') =>
kaliszyk@35222:         if x = x'
kaliszyk@35222:         then mk_identity rty
kaliszyk@35222:         else raise (LIFT_MATCH "absrep_fun (frees)")
kaliszyk@35222:     | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)")
kaliszyk@35222:     | _ => raise (LIFT_MATCH "absrep_fun (default)")
kaliszyk@35222: 
kaliszyk@35222: fun absrep_fun_chk flag ctxt (rty, qty) =
kaliszyk@35222:   absrep_fun flag ctxt (rty, qty)
kaliszyk@35222:   |> Syntax.check_term ctxt
kaliszyk@35222: 
kaliszyk@35222: 
kaliszyk@35222: 
kaliszyk@35222: 
kaliszyk@35222: (*** Aggregate Equivalence Relation ***)
kaliszyk@35222: 
kaliszyk@35222: 
kaliszyk@35222: (* works very similar to the absrep generation,
kaliszyk@35222:    except there is no need for polarities
kaliszyk@35222: *)
kaliszyk@35222: 
kaliszyk@35222: (* instantiates TVars so that the term is of type ty *)
kaliszyk@35222: fun force_typ ctxt trm ty =
kaliszyk@35222: let
kaliszyk@35222:   val thy = ProofContext.theory_of ctxt
kaliszyk@35222:   val trm_ty = fastype_of trm
kaliszyk@35222:   val ty_inst = Sign.typ_match thy (trm_ty, ty) Vartab.empty
kaliszyk@35222: in
kaliszyk@35222:   map_types (Envir.subst_type ty_inst) trm
kaliszyk@35222: end
kaliszyk@35222: 
kaliszyk@35222: fun is_eq (Const (@{const_name "op ="}, _)) = true
kaliszyk@35222:   | is_eq _ = false
kaliszyk@35222: 
kaliszyk@35222: fun mk_rel_compose (trm1, trm2) =
kaliszyk@35222:   Const (@{const_name "rel_conj"}, dummyT) $ trm1 $ trm2
kaliszyk@35222: 
kaliszyk@35222: fun get_relmap ctxt s =
kaliszyk@35222: let
kaliszyk@35222:   val thy = ProofContext.theory_of ctxt
kaliszyk@35222:   val exn = LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")
kaliszyk@35222:   val relmap = #relmap (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn
kaliszyk@35222: in
kaliszyk@35222:   Const (relmap, dummyT)
kaliszyk@35222: end
kaliszyk@35222: 
kaliszyk@35222: fun mk_relmap ctxt vs rty =
kaliszyk@35222: let
kaliszyk@35222:   val vs' = map (mk_Free) vs
kaliszyk@35222: 
kaliszyk@35222:   fun mk_relmap_aux rty =
kaliszyk@35222:     case rty of
kaliszyk@35222:       TVar _ => mk_Free rty
kaliszyk@35222:     | Type (_, []) => HOLogic.eq_const rty
kaliszyk@35222:     | Type (s, tys) => list_comb (get_relmap ctxt s, map mk_relmap_aux tys)
kaliszyk@35222:     | _ => raise LIFT_MATCH ("mk_relmap (default)")
kaliszyk@35222: in
kaliszyk@35222:   fold_rev Term.lambda vs' (mk_relmap_aux rty)
kaliszyk@35222: end
kaliszyk@35222: 
kaliszyk@35222: fun get_equiv_rel ctxt s =
kaliszyk@35222: let
kaliszyk@35222:   val thy = ProofContext.theory_of ctxt
kaliszyk@35222:   val exn = LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")
kaliszyk@35222: in
kaliszyk@35222:   #equiv_rel (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn
kaliszyk@35222: end
kaliszyk@35222: 
kaliszyk@35222: fun equiv_match_err ctxt ty_pat ty =
kaliszyk@35222: let
kaliszyk@35222:   val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
kaliszyk@35222:   val ty_str = Syntax.string_of_typ ctxt ty
kaliszyk@35222: in
kaliszyk@35222:   raise LIFT_MATCH (space_implode " "
kaliszyk@35222:     ["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
kaliszyk@35222: end
kaliszyk@35222: 
kaliszyk@35222: (* builds the aggregate equivalence relation
kaliszyk@35222:    that will be the argument of Respects
kaliszyk@35222: *)
kaliszyk@35222: fun equiv_relation ctxt (rty, qty) =
kaliszyk@35222:   if rty = qty
kaliszyk@35222:   then HOLogic.eq_const rty
kaliszyk@35222:   else
kaliszyk@35222:     case (rty, qty) of
kaliszyk@35222:       (Type (s, tys), Type (s', tys')) =>
kaliszyk@35222:        if s = s'
kaliszyk@35222:        then
kaliszyk@35222:          let
kaliszyk@35222:            val args = map (equiv_relation ctxt) (tys ~~ tys')
kaliszyk@35222:          in
kaliszyk@35222:            list_comb (get_relmap ctxt s, args)
kaliszyk@35222:          end
kaliszyk@35222:        else
kaliszyk@35222:          let
kaliszyk@35222:            val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
kaliszyk@35222:            val rtyenv = match ctxt equiv_match_err rty_pat rty
kaliszyk@35222:            val qtyenv = match ctxt equiv_match_err qty_pat qty
kaliszyk@35222:            val args_aux = map (double_lookup rtyenv qtyenv) vs
kaliszyk@35222:            val args = map (equiv_relation ctxt) args_aux
kaliszyk@35222:            val rel_map = mk_relmap ctxt vs rty_pat
kaliszyk@35222:            val result = list_comb (rel_map, args)
kaliszyk@35222:            val eqv_rel = get_equiv_rel ctxt s'
kaliszyk@35222:            val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool})
kaliszyk@35222:          in
kaliszyk@35222:            if forall is_eq args
kaliszyk@35222:            then eqv_rel'
kaliszyk@35222:            else mk_rel_compose (result, eqv_rel')
kaliszyk@35222:          end
kaliszyk@35222:       | _ => HOLogic.eq_const rty
kaliszyk@35222: 
kaliszyk@35222: fun equiv_relation_chk ctxt (rty, qty) =
kaliszyk@35222:   equiv_relation ctxt (rty, qty)
kaliszyk@35222:   |> Syntax.check_term ctxt
kaliszyk@35222: 
kaliszyk@35222: 
kaliszyk@35222: 
kaliszyk@35222: (*** Regularization ***)
kaliszyk@35222: 
kaliszyk@35222: (* Regularizing an rtrm means:
kaliszyk@35222: 
kaliszyk@35222:  - Quantifiers over types that need lifting are replaced
kaliszyk@35222:    by bounded quantifiers, for example:
kaliszyk@35222: 
kaliszyk@35222:       All P  ----> All (Respects R) P
kaliszyk@35222: 
kaliszyk@35222:    where the aggregate relation R is given by the rty and qty;
kaliszyk@35222: 
kaliszyk@35222:  - Abstractions over types that need lifting are replaced
kaliszyk@35222:    by bounded abstractions, for example:
kaliszyk@35222: 
kaliszyk@35222:       %x. P  ----> Ball (Respects R) %x. P
kaliszyk@35222: 
kaliszyk@35222:  - Equalities over types that need lifting are replaced by
kaliszyk@35222:    corresponding equivalence relations, for example:
kaliszyk@35222: 
kaliszyk@35222:       A = B  ----> R A B
kaliszyk@35222: 
kaliszyk@35222:    or
kaliszyk@35222: 
kaliszyk@35222:       A = B  ----> (R ===> R) A B
kaliszyk@35222: 
kaliszyk@35222:    for more complicated types of A and B
kaliszyk@35222: 
kaliszyk@35222: 
kaliszyk@35222:  The regularize_trm accepts raw theorems in which equalities
kaliszyk@35222:  and quantifiers match exactly the ones in the lifted theorem
kaliszyk@35222:  but also accepts partially regularized terms.
kaliszyk@35222: 
kaliszyk@35222:  This means that the raw theorems can have:
kaliszyk@35222:    Ball (Respects R),  Bex (Respects R), Bex1_rel (Respects R), Babs, R
kaliszyk@35222:  in the places where:
kaliszyk@35222:    All, Ex, Ex1, %, (op =)
kaliszyk@35222:  is required the lifted theorem.
kaliszyk@35222: 
kaliszyk@35222: *)
kaliszyk@35222: 
kaliszyk@35222: val mk_babs = Const (@{const_name Babs}, dummyT)
kaliszyk@35222: val mk_ball = Const (@{const_name Ball}, dummyT)
kaliszyk@35222: val mk_bex  = Const (@{const_name Bex}, dummyT)
kaliszyk@35222: val mk_bex1_rel = Const (@{const_name Bex1_rel}, dummyT)
kaliszyk@35222: val mk_resp = Const (@{const_name Respects}, dummyT)
kaliszyk@35222: 
kaliszyk@35222: (* - applies f to the subterm of an abstraction,
kaliszyk@35222:      otherwise to the given term,
kaliszyk@35222:    - used by regularize, therefore abstracted
kaliszyk@35222:      variables do not have to be treated specially
kaliszyk@35222: *)
kaliszyk@35222: fun apply_subt f (trm1, trm2) =
kaliszyk@35222:   case (trm1, trm2) of
kaliszyk@35222:     (Abs (x, T, t), Abs (_ , _, t')) => Abs (x, T, f (t, t'))
kaliszyk@35222:   | _ => f (trm1, trm2)
kaliszyk@35222: 
kaliszyk@35222: fun term_mismatch str ctxt t1 t2 =
kaliszyk@35222: let
kaliszyk@35222:   val t1_str = Syntax.string_of_term ctxt t1
kaliszyk@35222:   val t2_str = Syntax.string_of_term ctxt t2
kaliszyk@35222:   val t1_ty_str = Syntax.string_of_typ ctxt (fastype_of t1)
kaliszyk@35222:   val t2_ty_str = Syntax.string_of_typ ctxt (fastype_of t2)
kaliszyk@35222: in
kaliszyk@35222:   raise LIFT_MATCH (cat_lines [str, t1_str ^ "::" ^ t1_ty_str, t2_str ^ "::" ^ t2_ty_str])
kaliszyk@35222: end
kaliszyk@35222: 
kaliszyk@35222: (* the major type of All and Ex quantifiers *)
kaliszyk@35222: fun qnt_typ ty = domain_type (domain_type ty)
kaliszyk@35222: 
kaliszyk@35222: (* Checks that two types match, for example:
kaliszyk@35222:      rty -> rty   matches   qty -> qty *)
kaliszyk@35222: fun matches_typ thy rT qT =
kaliszyk@35222:   if rT = qT then true else
kaliszyk@35222:   case (rT, qT) of
kaliszyk@35222:     (Type (rs, rtys), Type (qs, qtys)) =>
kaliszyk@35222:       if rs = qs then
kaliszyk@35222:         if length rtys <> length qtys then false else
kaliszyk@35222:         forall (fn x => x = true) (map2 (matches_typ thy) rtys qtys)
kaliszyk@35222:       else
kaliszyk@35222:         (case Quotient_Info.quotdata_lookup_raw thy qs of
kaliszyk@35222:           SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo)
kaliszyk@35222:         | NONE => false)
kaliszyk@35222:   | _ => false
kaliszyk@35222: 
kaliszyk@35222: 
kaliszyk@35222: (* produces a regularized version of rtrm
kaliszyk@35222: 
kaliszyk@35222:    - the result might contain dummyTs
kaliszyk@35222: 
kaliszyk@35222:    - for regularisation we do not need any
kaliszyk@35222:      special treatment of bound variables
kaliszyk@35222: *)
kaliszyk@35222: fun regularize_trm ctxt (rtrm, qtrm) =
kaliszyk@35222:   case (rtrm, qtrm) of
kaliszyk@35222:     (Abs (x, ty, t), Abs (_, ty', t')) =>
kaliszyk@35222:        let
kaliszyk@35222:          val subtrm = Abs(x, ty, regularize_trm ctxt (t, t'))
kaliszyk@35222:        in
kaliszyk@35222:          if ty = ty' then subtrm
kaliszyk@35222:          else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm
kaliszyk@35222:        end
kaliszyk@35222:   | (Const (@{const_name "Babs"}, T) $ resrel $ (t as (Abs (_, ty, _))), t' as (Abs (_, ty', _))) =>
kaliszyk@35222:        let
kaliszyk@35222:          val subtrm = regularize_trm ctxt (t, t')
kaliszyk@35222:          val needres = mk_resp $ equiv_relation_chk ctxt (ty, ty')
kaliszyk@35222:        in
kaliszyk@35222:          if resrel <> needres
kaliszyk@35222:          then term_mismatch "regularize (Babs)" ctxt resrel needres
kaliszyk@35222:          else mk_babs $ resrel $ subtrm
kaliszyk@35222:        end
kaliszyk@35222: 
kaliszyk@35222:   | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
kaliszyk@35222:        let
kaliszyk@35222:          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
kaliszyk@35222:        in
kaliszyk@35222:          if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm
kaliszyk@35222:          else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
kaliszyk@35222:        end
kaliszyk@35222: 
kaliszyk@35222:   | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
kaliszyk@35222:        let
kaliszyk@35222:          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
kaliszyk@35222:        in
kaliszyk@35222:          if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm
kaliszyk@35222:          else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
kaliszyk@35222:        end
kaliszyk@35222: 
kaliszyk@35222:   | (Const (@{const_name "Ex1"}, ty) $ (Abs (_, _,
kaliszyk@35222:       (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op :"}, _) $ _ $
kaliszyk@35222:         (Const (@{const_name "Respects"}, _) $ resrel)) $ (t $ _)))),
kaliszyk@35222:      Const (@{const_name "Ex1"}, ty') $ t') =>
kaliszyk@35222:        let
kaliszyk@35222:          val t_ = incr_boundvars (~1) t
kaliszyk@35222:          val subtrm = apply_subt (regularize_trm ctxt) (t_, t')
kaliszyk@35222:          val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
kaliszyk@35222:        in
kaliszyk@35222:          if resrel <> needrel
kaliszyk@35222:          then term_mismatch "regularize (Bex1)" ctxt resrel needrel
kaliszyk@35222:          else mk_bex1_rel $ resrel $ subtrm
kaliszyk@35222:        end
kaliszyk@35222: 
kaliszyk@35222:   | (Const (@{const_name "Ex1"}, ty) $ t, Const (@{const_name "Ex1"}, ty') $ t') =>
kaliszyk@35222:        let
kaliszyk@35222:          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
kaliszyk@35222:        in
kaliszyk@35222:          if ty = ty' then Const (@{const_name "Ex1"}, ty) $ subtrm
kaliszyk@35222:          else mk_bex1_rel $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
kaliszyk@35222:        end
kaliszyk@35222: 
kaliszyk@35222:   | (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t,
kaliszyk@35222:      Const (@{const_name "All"}, ty') $ t') =>
kaliszyk@35222:        let
kaliszyk@35222:          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
kaliszyk@35222:          val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
kaliszyk@35222:        in
kaliszyk@35222:          if resrel <> needrel
kaliszyk@35222:          then term_mismatch "regularize (Ball)" ctxt resrel needrel
kaliszyk@35222:          else mk_ball $ (mk_resp $ resrel) $ subtrm
kaliszyk@35222:        end
kaliszyk@35222: 
kaliszyk@35222:   | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t,
kaliszyk@35222:      Const (@{const_name "Ex"}, ty') $ t') =>
kaliszyk@35222:        let
kaliszyk@35222:          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
kaliszyk@35222:          val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
kaliszyk@35222:        in
kaliszyk@35222:          if resrel <> needrel
kaliszyk@35222:          then term_mismatch "regularize (Bex)" ctxt resrel needrel
kaliszyk@35222:          else mk_bex $ (mk_resp $ resrel) $ subtrm
kaliszyk@35222:        end
kaliszyk@35222: 
kaliszyk@35222:   | (Const (@{const_name "Bex1_rel"}, ty) $ resrel $ t, Const (@{const_name "Ex1"}, ty') $ t') =>
kaliszyk@35222:        let
kaliszyk@35222:          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
kaliszyk@35222:          val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
kaliszyk@35222:        in
kaliszyk@35222:          if resrel <> needrel
kaliszyk@35222:          then term_mismatch "regularize (Bex1_res)" ctxt resrel needrel
kaliszyk@35222:          else mk_bex1_rel $ resrel $ subtrm
kaliszyk@35222:        end
kaliszyk@35222: 
kaliszyk@35222:   | (* equalities need to be replaced by appropriate equivalence relations *)
kaliszyk@35222:     (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) =>
kaliszyk@35222:          if ty = ty' then rtrm
kaliszyk@35222:          else equiv_relation ctxt (domain_type ty, domain_type ty')
kaliszyk@35222: 
kaliszyk@35222:   | (* in this case we just check whether the given equivalence relation is correct *)
kaliszyk@35222:     (rel, Const (@{const_name "op ="}, ty')) =>
kaliszyk@35222:        let
kaliszyk@35222:          val rel_ty = fastype_of rel
kaliszyk@35222:          val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty')
kaliszyk@35222:        in
kaliszyk@35222:          if rel' aconv rel then rtrm
kaliszyk@35222:          else term_mismatch "regularise (relation mismatch)" ctxt rel rel'
kaliszyk@35222:        end
kaliszyk@35222: 
kaliszyk@35222:   | (_, Const _) =>
kaliszyk@35222:        let
kaliszyk@35222:          val thy = ProofContext.theory_of ctxt
kaliszyk@35222:          fun same_const (Const (s, T)) (Const (s', T')) = (s = s') andalso matches_typ thy T T'
kaliszyk@35222:            | same_const _ _ = false
kaliszyk@35222:        in
kaliszyk@35222:          if same_const rtrm qtrm then rtrm
kaliszyk@35222:          else
kaliszyk@35222:            let
kaliszyk@35222:              val rtrm' = #rconst (qconsts_lookup thy qtrm)
kaliszyk@35222:                handle Quotient_Info.NotFound => term_mismatch "regularize(constant notfound)" ctxt rtrm qtrm
kaliszyk@35222:            in
kaliszyk@35222:              if Pattern.matches thy (rtrm', rtrm)
kaliszyk@35222:              then rtrm else term_mismatch "regularize(constant mismatch)" ctxt rtrm qtrm
kaliszyk@35222:            end
kaliszyk@35222:        end
kaliszyk@35222: 
kaliszyk@35222:   | (((t1 as Const (@{const_name "split"}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
kaliszyk@35222:      ((t2 as Const (@{const_name "split"}, _)) $ Abs (v2, _ , Abs(v2', _  , s2)))) =>
kaliszyk@35222:        regularize_trm ctxt (t1, t2) $ Abs (v1, ty, Abs (v1', ty', regularize_trm ctxt (s1, s2)))
kaliszyk@35222: 
kaliszyk@35222:   | (((t1 as Const (@{const_name "split"}, _)) $ Abs (v1, ty, s1)),
kaliszyk@35222:      ((t2 as Const (@{const_name "split"}, _)) $ Abs (v2, _ , s2))) =>
kaliszyk@35222:        regularize_trm ctxt (t1, t2) $ Abs (v1, ty, regularize_trm ctxt (s1, s2))
kaliszyk@35222: 
kaliszyk@35222:   | (t1 $ t2, t1' $ t2') =>
kaliszyk@35222:        regularize_trm ctxt (t1, t1') $ regularize_trm ctxt (t2, t2')
kaliszyk@35222: 
kaliszyk@35222:   | (Bound i, Bound i') =>
kaliszyk@35222:        if i = i' then rtrm
kaliszyk@35222:        else raise (LIFT_MATCH "regularize (bounds mismatch)")
kaliszyk@35222: 
kaliszyk@35222:   | _ =>
kaliszyk@35222:        let
kaliszyk@35222:          val rtrm_str = Syntax.string_of_term ctxt rtrm
kaliszyk@35222:          val qtrm_str = Syntax.string_of_term ctxt qtrm
kaliszyk@35222:        in
kaliszyk@35222:          raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")"))
kaliszyk@35222:        end
kaliszyk@35222: 
kaliszyk@35222: fun regularize_trm_chk ctxt (rtrm, qtrm) =
kaliszyk@35222:   regularize_trm ctxt (rtrm, qtrm)
kaliszyk@35222:   |> Syntax.check_term ctxt
kaliszyk@35222: 
kaliszyk@35222: 
kaliszyk@35222: 
kaliszyk@35222: (*** Rep/Abs Injection ***)
kaliszyk@35222: 
kaliszyk@35222: (*
kaliszyk@35222: Injection of Rep/Abs means:
kaliszyk@35222: 
kaliszyk@35222:   For abstractions:
kaliszyk@35222: 
kaliszyk@35222:   * If the type of the abstraction needs lifting, then we add Rep/Abs
kaliszyk@35222:     around the abstraction; otherwise we leave it unchanged.
kaliszyk@35222: 
kaliszyk@35222:   For applications:
kaliszyk@35222: 
kaliszyk@35222:   * If the application involves a bounded quantifier, we recurse on
kaliszyk@35222:     the second argument. If the application is a bounded abstraction,
kaliszyk@35222:     we always put an Rep/Abs around it (since bounded abstractions
kaliszyk@35222:     are assumed to always need lifting). Otherwise we recurse on both
kaliszyk@35222:     arguments.
kaliszyk@35222: 
kaliszyk@35222:   For constants:
kaliszyk@35222: 
kaliszyk@35222:   * If the constant is (op =), we leave it always unchanged.
kaliszyk@35222:     Otherwise the type of the constant needs lifting, we put
kaliszyk@35222:     and Rep/Abs around it.
kaliszyk@35222: 
kaliszyk@35222:   For free variables:
kaliszyk@35222: 
kaliszyk@35222:   * We put a Rep/Abs around it if the type needs lifting.
kaliszyk@35222: 
kaliszyk@35222:   Vars case cannot occur.
kaliszyk@35222: *)
kaliszyk@35222: 
kaliszyk@35222: fun mk_repabs ctxt (T, T') trm =
kaliszyk@35222:   absrep_fun RepF ctxt (T, T') $ (absrep_fun AbsF ctxt (T, T') $ trm)
kaliszyk@35222: 
kaliszyk@35222: fun inj_repabs_err ctxt msg rtrm qtrm =
kaliszyk@35222: let
kaliszyk@35222:   val rtrm_str = Syntax.string_of_term ctxt rtrm
kaliszyk@35222:   val qtrm_str = Syntax.string_of_term ctxt qtrm
kaliszyk@35222: in
kaliszyk@35222:   raise LIFT_MATCH (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str])
kaliszyk@35222: end
kaliszyk@35222: 
kaliszyk@35222: 
kaliszyk@35222: (* bound variables need to be treated properly,
kaliszyk@35222:    as the type of subterms needs to be calculated   *)
kaliszyk@35222: fun inj_repabs_trm ctxt (rtrm, qtrm) =
kaliszyk@35222:  case (rtrm, qtrm) of
kaliszyk@35222:     (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>
kaliszyk@35222:        Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
kaliszyk@35222: 
kaliszyk@35222:   | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>
kaliszyk@35222:        Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
kaliszyk@35222: 
kaliszyk@35222:   | (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) =>
kaliszyk@35222:       let
kaliszyk@35222:         val rty = fastype_of rtrm
kaliszyk@35222:         val qty = fastype_of qtrm
kaliszyk@35222:       in
kaliszyk@35222:         mk_repabs ctxt (rty, qty) (Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm ctxt (t, t')))
kaliszyk@35222:       end
kaliszyk@35222: 
kaliszyk@35222:   | (Abs (x, T, t), Abs (x', T', t')) =>
kaliszyk@35222:       let
kaliszyk@35222:         val rty = fastype_of rtrm
kaliszyk@35222:         val qty = fastype_of qtrm
kaliszyk@35222:         val (y, s) = Term.dest_abs (x, T, t)
kaliszyk@35222:         val (_, s') = Term.dest_abs (x', T', t')
kaliszyk@35222:         val yvar = Free (y, T)
kaliszyk@35222:         val result = Term.lambda_name (y, yvar) (inj_repabs_trm ctxt (s, s'))
kaliszyk@35222:       in
kaliszyk@35222:         if rty = qty then result
kaliszyk@35222:         else mk_repabs ctxt (rty, qty) result
kaliszyk@35222:       end
kaliszyk@35222: 
kaliszyk@35222:   | (t $ s, t' $ s') =>
kaliszyk@35222:        (inj_repabs_trm ctxt (t, t')) $ (inj_repabs_trm ctxt (s, s'))
kaliszyk@35222: 
kaliszyk@35222:   | (Free (_, T), Free (_, T')) =>
kaliszyk@35222:         if T = T' then rtrm
kaliszyk@35222:         else mk_repabs ctxt (T, T') rtrm
kaliszyk@35222: 
kaliszyk@35222:   | (_, Const (@{const_name "op ="}, _)) => rtrm
kaliszyk@35222: 
kaliszyk@35222:   | (_, Const (_, T')) =>
kaliszyk@35222:       let
kaliszyk@35222:         val rty = fastype_of rtrm
kaliszyk@35222:       in
kaliszyk@35222:         if rty = T' then rtrm
kaliszyk@35222:         else mk_repabs ctxt (rty, T') rtrm
kaliszyk@35222:       end
kaliszyk@35222: 
kaliszyk@35222:   | _ => inj_repabs_err ctxt "injection (default):" rtrm qtrm
kaliszyk@35222: 
kaliszyk@35222: fun inj_repabs_trm_chk ctxt (rtrm, qtrm) =
kaliszyk@35222:   inj_repabs_trm ctxt (rtrm, qtrm)
kaliszyk@35222:   |> Syntax.check_term ctxt
kaliszyk@35222: 
kaliszyk@35222: 
kaliszyk@35222: 
kaliszyk@35222: (*** Wrapper for automatically transforming an rthm into a qthm ***)
kaliszyk@35222: 
kaliszyk@35222: (* subst_tys takes a list of (rty, qty) substitution pairs
kaliszyk@35222:    and replaces all occurences of rty in the given type
kaliszyk@35222:    by appropriate qty, with substitution *)
kaliszyk@35222: fun subst_ty thy ty (rty, qty) r =
kaliszyk@35222:   if r <> NONE then r else
kaliszyk@35222:   case try (Sign.typ_match thy (rty, ty)) Vartab.empty of
kaliszyk@35222:     SOME inst => SOME (Envir.subst_type inst qty)
kaliszyk@35222:   | NONE => NONE
kaliszyk@35222: fun subst_tys thy substs ty =
kaliszyk@35222:   case fold (subst_ty thy ty) substs NONE of
kaliszyk@35222:     SOME ty => ty
kaliszyk@35222:   | NONE =>
kaliszyk@35222:       (case ty of
kaliszyk@35222:         Type (s, tys) => Type (s, map (subst_tys thy substs) tys)
kaliszyk@35222:       | x => x)
kaliszyk@35222: 
kaliszyk@35222: (* subst_trms takes a list of (rtrm, qtrm) substitution pairs
kaliszyk@35222:    and if the given term matches any of the raw terms it
kaliszyk@35222:    returns the appropriate qtrm instantiated. If none of
kaliszyk@35222:    them matched it returns NONE. *)
kaliszyk@35222: fun subst_trm thy t (rtrm, qtrm) s =
kaliszyk@35222:   if s <> NONE then s else
kaliszyk@35222:     case try (Pattern.match thy (rtrm, t)) (Vartab.empty, Vartab.empty) of
kaliszyk@35222:       SOME inst => SOME (Envir.subst_term inst qtrm)
kaliszyk@35222:     | NONE => NONE;
kaliszyk@35222: fun subst_trms thy substs t = fold (subst_trm thy t) substs NONE
kaliszyk@35222: 
kaliszyk@35222: (* prepares type and term substitution pairs to be used by above
kaliszyk@35222:    functions that let replace all raw constructs by appropriate
kaliszyk@35222:    lifted counterparts. *)
kaliszyk@35222: fun get_ty_trm_substs ctxt =
kaliszyk@35222: let
kaliszyk@35222:   val thy = ProofContext.theory_of ctxt
kaliszyk@35222:   val quot_infos  = Quotient_Info.quotdata_dest ctxt
kaliszyk@35222:   val const_infos = Quotient_Info.qconsts_dest ctxt
kaliszyk@35222:   val ty_substs = map (fn ri => (#rtyp ri, #qtyp ri)) quot_infos
kaliszyk@35222:   val const_substs = map (fn ci => (#rconst ci, #qconst ci)) const_infos
kaliszyk@35222:   fun rel_eq rel = HOLogic.eq_const (subst_tys thy ty_substs (domain_type (fastype_of rel)))
kaliszyk@35222:   val rel_substs = map (fn ri => (#equiv_rel ri, rel_eq (#equiv_rel ri))) quot_infos
kaliszyk@35222: in
kaliszyk@35222:   (ty_substs, const_substs @ rel_substs)
kaliszyk@35222: end
kaliszyk@35222: 
kaliszyk@35222: fun quotient_lift_const (b, t) ctxt =
kaliszyk@35222: let
kaliszyk@35222:   val thy = ProofContext.theory_of ctxt
kaliszyk@35222:   val (ty_substs, _) = get_ty_trm_substs ctxt;
kaliszyk@35222:   val (_, ty) = dest_Const t;
kaliszyk@35222:   val nty = subst_tys thy ty_substs ty;
kaliszyk@35222: in
kaliszyk@35222:   Free(b, nty)
kaliszyk@35222: end
kaliszyk@35222: 
kaliszyk@35222: (*
kaliszyk@35222: Takes a term and
kaliszyk@35222: 
kaliszyk@35222: * replaces raw constants by the quotient constants
kaliszyk@35222: 
kaliszyk@35222: * replaces equivalence relations by equalities
kaliszyk@35222: 
kaliszyk@35222: * replaces raw types by the quotient types
kaliszyk@35222: 
kaliszyk@35222: *)
kaliszyk@35222: 
kaliszyk@35222: fun quotient_lift_all ctxt t =
kaliszyk@35222: let
kaliszyk@35222:   val thy = ProofContext.theory_of ctxt
kaliszyk@35222:   val (ty_substs, substs) = get_ty_trm_substs ctxt
kaliszyk@35222:   fun lift_aux t =
kaliszyk@35222:     case subst_trms thy substs t of
kaliszyk@35222:       SOME x => x
kaliszyk@35222:     | NONE =>
kaliszyk@35222:       (case t of
kaliszyk@35222:         a $ b => lift_aux a $ lift_aux b
kaliszyk@35222:       | Abs(a, ty, s) =>
kaliszyk@35222:           let
kaliszyk@35222:             val (y, s') = Term.dest_abs (a, ty, s)
kaliszyk@35222:             val nty = subst_tys thy ty_substs ty
kaliszyk@35222:           in
kaliszyk@35222:             Abs(y, nty, abstract_over (Free (y, nty), lift_aux s'))
kaliszyk@35222:           end
kaliszyk@35222:       | Free(n, ty) => Free(n, subst_tys thy ty_substs ty)
kaliszyk@35222:       | Var(n, ty) => Var(n, subst_tys thy ty_substs ty)
kaliszyk@35222:       | Bound i => Bound i
kaliszyk@35222:       | Const(s, ty) => Const(s, subst_tys thy ty_substs ty))
kaliszyk@35222: in
kaliszyk@35222:   lift_aux t
kaliszyk@35222: end
kaliszyk@35222: 
kaliszyk@35222: 
kaliszyk@35222: end; (* structure *)
kaliszyk@35222: 
kaliszyk@35222: 
kaliszyk@35222: