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;