diff -r c129354f2ff6 -r 3104d62e7a16 Quot/quotient_term.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Quot/quotient_term.ML	Thu Dec 17 14:58:33 2009 +0100
@@ -0,0 +1,278 @@
+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;
+
+