1 signature QUOTIENT_TERM =

     2 sig

     3     val regularize_trm: Proof.context -> term -> term -> term

     4     val inj_repabs_trm: Proof.context -> (term * term) -> term

     5 end;

     6 

     7 structure Quotient_Term: QUOTIENT_TERM =

     8 struct

     9 

    10 (*

    11 Regularizing an rtrm means:

    12  

    13  - Quantifiers over a type that need lifting are replaced 

    14    by bounded quantifiers, for example:

    15 

    16       All P  ===> All (Respects R) P

    17 

    18    where the relation R is given by the rty and qty;

    19  

    20  - Abstractions over a type that needs lifting are replaced

    21    by bounded abstractions:

    22       

    23       %x. P  ===> Ball (Respects R) %x. P

    24 

    25  - Equalities over the type being lifted are replaced by

    26    corresponding equivalence relations:

    27 

    28       A = B  ===> R A B

    29 

    30    or 

    31 

    32       A = B  ===> (R ===> R) A B

    33  

    34    for more complicated types of A and B

    35 *)

    36 

    37 (* builds the relation that is the argument of respects *)

    38 fun mk_resp_arg lthy (rty, qty) =

    39 let

    40   val thy = ProofContext.theory_of lthy

    41 in  

    42   if rty = qty

    43   then HOLogic.eq_const rty

    44   else

    45     case (rty, qty) of

    46       (Type (s, tys), Type (s', tys')) =>

    47        if s = s' 

    48        then let

    49               val SOME map_info = maps_lookup thy s

    50               (* FIXME dont return an option, raise an exception *)

    51               val args = map (mk_resp_arg lthy) (tys ~~ tys')

    52             in

    53               list_comb (Const (#relfun map_info, dummyT), args) 

    54             end  

    55        else let  

    56               val SOME qinfo = quotdata_lookup_thy thy s'

    57               (* FIXME: check in this case that the rty and qty *)

    58               (* FIXME: correspond to each other *)

    59               val (s, _) = dest_Const (#rel qinfo)

    60               (* FIXME: the relation should only be the string        *)

    61               (* FIXME: and the type needs to be calculated as below; *)

    62               (* FIXME: maybe one should actually have a term         *)

    63               (* FIXME: and one needs to force it to have this type   *)

    64             in

    65               Const (s, rty --> rty --> @{typ bool})

    66             end

    67       | _ => HOLogic.eq_const dummyT 

    68              (* FIXME: check that the types correspond to each other? *)

    69 end

    70 

    71 val mk_babs = Const (@{const_name Babs}, dummyT)

    72 val mk_ball = Const (@{const_name Ball}, dummyT)

    73 val mk_bex  = Const (@{const_name Bex}, dummyT)

    74 val mk_resp = Const (@{const_name Respects}, dummyT)

    75 

    76 (* - applies f to the subterm of an abstraction,   *)

    77 (*   otherwise to the given term,                  *)

    78 (* - used by regularize, therefore abstracted      *)

    79 (*   variables do not have to be treated specially *)

    80 fun apply_subt f trm1 trm2 =

    81   case (trm1, trm2) of

    82     (Abs (x, T, t), Abs (_ , _, t')) => Abs (x, T, f t t')

    83   | _ => f trm1 trm2

    84 

    85 (* the major type of All and Ex quantifiers *)

    86 fun qnt_typ ty = domain_type (domain_type ty)  

    87 

    88 

    89 (* produces a regularized version of rtrm       *)

    90 (*                                              *)

    91 (* - the result is still contains dummyT        *)

    92 (*                                              *)

    93 (* - for regularisation we do not need any      *)

    94 (*   special treatment of bound variables       *)

    95 

    96 fun regularize_trm lthy rtrm qtrm =

    97   case (rtrm, qtrm) of

    98     (Abs (x, ty, t), Abs (_, ty', t')) =>

    99        let

   100          val subtrm = Abs(x, ty, regularize_trm lthy t t')

   101        in

   102          if ty = ty' then subtrm

   103          else mk_babs $ (mk_resp $ mk_resp_arg lthy (ty, ty')) $ subtrm

   104        end

   105 

   106   | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>

   107        let

   108          val subtrm = apply_subt (regularize_trm lthy) t t'

   109        in

   110          if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm

   111          else mk_ball $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm

   112        end

   113 

   114   | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>

   115        let

   116          val subtrm = apply_subt (regularize_trm lthy) t t'

   117        in

   118          if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm

   119          else mk_bex $ (mk_resp $ mk_resp_arg lthy (qnt_typ ty, qnt_typ ty')) $ subtrm

   120        end

   121 

   122   | (* equalities need to be replaced by appropriate equivalence relations *) 

   123     (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) =>

   124          if ty = ty' then rtrm

   125          else mk_resp_arg lthy (domain_type ty, domain_type ty') 

   126 

   127   | (* in this case we check whether the given equivalence relation is correct *) 

   128     (rel, Const (@{const_name "op ="}, ty')) =>

   129        let 

   130          val exc = LIFT_MATCH "regularise (relation mismatch)"

   131          val rel_ty = (fastype_of rel) handle TERM _ => raise exc 

   132          val rel' = mk_resp_arg lthy (domain_type rel_ty, domain_type ty') 

   133        in 

   134          if rel' = rel then rtrm else raise exc

   135        end  

   136 

   137   | (_, Const _) =>

   138        let 

   139          fun same_name (Const (s, T)) (Const (s', T')) = (s = s') (*andalso (T = T')*)

   140            | same_name _ _ = false

   141           (* TODO/FIXME: This test is not enough. *) 

   142           (*             Why?                     *)

   143           (* Because constants can have the same name but not be the same

   144              constant.  All overloaded constants have the same name but because

   145              of different types they do differ.

   146         

   147              This code will let one write a theorem where plus on nat is

   148              matched to plus on int, even if the latter is defined differently.

   149     

   150              This would result in hard to understand failures in injection and

   151              cleaning. *)

   152            (* cu: if I also test the type, then something else breaks *)

   153        in

   154          if same_name rtrm qtrm then rtrm

   155          else 

   156            let 

   157              val thy = ProofContext.theory_of lthy

   158              val qtrm_str = Syntax.string_of_term lthy qtrm

   159              val exc1 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " not found)")

   160              val exc2 = LIFT_MATCH ("regularize (constant " ^ qtrm_str ^ " mismatch)")

   161              val rtrm' = (#rconst (qconsts_lookup thy qtrm)) handle NotFound => raise exc1

   162            in 

   163              if Pattern.matches thy (rtrm', rtrm) 

   164              then rtrm else raise exc2

   165            end

   166        end 

   167 

   168   | (t1 $ t2, t1' $ t2') =>

   169        (regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2')

   170 

   171   | (Free (x, ty), Free (x', ty')) => 

   172        (* this case cannot arrise as we start with two fully atomized terms *)

   173        raise (LIFT_MATCH "regularize (frees)")

   174 

   175   | (Bound i, Bound i') =>

   176        if i = i' then rtrm 

   177        else raise (LIFT_MATCH "regularize (bounds mismatch)")

   178 

   179   | _ =>

   180        let 

   181          val rtrm_str = Syntax.string_of_term lthy rtrm

   182          val qtrm_str = Syntax.string_of_term lthy qtrm

   183        in

   184          raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")"))

   185        end

   186 

   187 

   188 

   189 (*

   190 Injecting of Rep/Abs means:

   191 

   192   For abstractions

   193 :

   194   * If the type of the abstraction doesn't need lifting we recurse.

   195 

   196   * If it needs lifting then we add Rep/Abs around the whole term and 

   197     check if the bound variable needs lifting.

   198  

   199     * If it does we recurse and put Rep/Abs around all occurences

   200       of the variable in the obtained subterm. This in combination

   201       with the Rep/Abs from above will let us change the type of 

   202       the abstraction with rewriting.

   203   

   204   For applications:

   205   

   206   * If the term is Respects applied to anything we leave it unchanged

   207 

   208   * If the term needs lifting and the head is a constant that we know

   209     how to lift, we put a Rep/Abs and recurse

   210 

   211   * If the term needs lifting and the head is a Free applied to subterms

   212     (if it is not applied we treated it in Abs branch) then we

   213     put Rep/Abs and recurse

   214 

   215   * Otherwise just recurse.

   216 *)

   217 

   218 fun mk_repabs lthy (T, T') trm = 

   219   Quotient_Def.get_fun repF lthy (T, T') 

   220     $ (Quotient_Def.get_fun absF lthy (T, T') $ trm)

   221 

   222 

   223 (* bound variables need to be treated properly,     *)

   224 (* as the type of subterms needs to be calculated   *)

   225 

   226 fun inj_repabs_trm lthy (rtrm, qtrm) =

   227  case (rtrm, qtrm) of

   228     (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>

   229        Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm lthy (t, t'))

   230 

   231   | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>

   232        Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm lthy (t, t'))

   233 

   234   | (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) =>

   235       let

   236         val rty = fastype_of rtrm

   237         val qty = fastype_of qtrm

   238       in

   239         mk_repabs lthy (rty, qty) (Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t')))

   240       end

   241 

   242   | (Abs (x, T, t), Abs (x', T', t')) =>

   243       let

   244         val rty = fastype_of rtrm

   245         val qty = fastype_of qtrm

   246         val (y, s) = Term.dest_abs (x, T, t)

   247         val (_, s') = Term.dest_abs (x', T', t')

   248         val yvar = Free (y, T)

   249         val result = Term.lambda_name (y, yvar) (inj_repabs_trm lthy (s, s'))

   250       in

   251         if rty = qty then result

   252         else mk_repabs lthy (rty, qty) result

   253       end

   254 

   255   | (t $ s, t' $ s') =>  

   256        (inj_repabs_trm lthy (t, t')) $ (inj_repabs_trm lthy (s, s'))

   257 

   258   | (Free (_, T), Free (_, T')) => 

   259         if T = T' then rtrm 

   260         else mk_repabs lthy (T, T') rtrm

   261 

   262   | (_, Const (@{const_name "op ="}, _)) => rtrm

   263 

   264   | (_, Const (_, T')) =>

   265       let

   266         val rty = fastype_of rtrm

   267       in 

   268         if rty = T' then rtrm

   269         else mk_repabs lthy (rty, T') rtrm

   270       end   

   271   

   272   | _ => raise (LIFT_MATCH "injection")

   273 

   274 end; (* structure *)

   275 

   276 open Quotient_Term;

   277 

   278