diff -r 243a5ceaa088 -r 17ca92ab4660 Quot/quotient_term.ML
--- a/Quot/quotient_term.ML	Thu Feb 11 09:23:59 2010 +0100
+++ b/Quot/quotient_term.ML	Thu Feb 11 10:06:02 2010 +0100
@@ -41,9 +41,9 @@
 (*** 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.               
+(* 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
@@ -56,7 +56,7 @@
 
 fun mk_identity ty = Const (@{const_name "id"}, ty --> ty)
 
-fun mk_fun_compose flag (trm1, trm2) = 
+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
@@ -73,13 +73,13 @@
 (* 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 
+(* 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
@@ -95,8 +95,8 @@
   fold_rev Term.lambda vs' (mk_mapfun_aux rty)
 end
 
-(* looks up the (varified) rty and qty for 
-   a quotient definition                   
+(* looks up the (varified) rty and qty for
+   a quotient definition
 *)
 fun get_rty_qty ctxt s =
 let
@@ -107,9 +107,9 @@
   (#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        
+(* 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
@@ -145,58 +145,58 @@
 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 
+  val ty_str = Syntax.string_of_typ ctxt ty
 in
-  raise LIFT_MATCH (space_implode " " 
+  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 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        
+
+   - 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   
+         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.                                 
-*)  
+     identity maps.
+*)
 
 fun absrep_fun flag ctxt (rty, qty) =
-  if rty = qty  
+  if rty = qty
   then mk_identity rty
   else
     case (rty, qty) of
@@ -209,12 +209,12 @@
         end
     | (Type (s, tys), Type (s', tys')) =>
         if s = s'
-        then 
+        then
            let
              val args = map (absrep_fun flag ctxt) (tys ~~ tys')
            in
              list_comb (get_mapfun ctxt s, args)
-           end 
+           end
         else
            let
              val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
@@ -222,8 +222,8 @@
              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) 
+             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'
@@ -253,7 +253,7 @@
 (* instantiates TVars so that the term is of type ty *)
 fun force_typ ctxt trm ty =
 let
-  val thy = ProofContext.theory_of ctxt 
+  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
@@ -269,7 +269,7 @@
 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 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)
@@ -292,7 +292,7 @@
 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 ^ ")") 
+  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
@@ -300,14 +300,14 @@
 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 
+  val ty_str = Syntax.string_of_typ ctxt ty
 in
-  raise LIFT_MATCH (space_implode " " 
+  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     
+(* builds the aggregate equivalence relation
+   that will be the argument of Respects
 *)
 fun equiv_relation ctxt (rty, qty) =
   if rty = qty
@@ -315,26 +315,26 @@
   else
     case (rty, qty) of
       (Type (s, tys), Type (s', tys')) =>
-       if s = s' 
-       then 
+       if s = s'
+       then
          let
            val args = map (equiv_relation ctxt) (tys ~~ tys')
          in
-           list_comb (get_relmap ctxt s, args) 
-         end  
-       else 
+           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_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 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 
+           if forall is_eq args
            then eqv_rel'
            else mk_rel_compose (result, eqv_rel')
          end
@@ -349,17 +349,17 @@
 (*** Regularization ***)
 
 (* Regularizing an rtrm means:
- 
- - Quantifiers over types that need lifting are replaced 
+
+ - 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
@@ -392,10 +392,10 @@
 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 
+(* - 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
@@ -433,10 +433,10 @@
 
 (* produces a regularized version of rtrm
 
-   - the result might contain dummyTs           
+   - the result might contain dummyTs
 
-   - for regularisation we do not need any      
-     special treatment of bound variables       
+   - for regularisation we do not need any
+     special treatment of bound variables
 *)
 fun regularize_trm ctxt (rtrm, qtrm) =
   case (rtrm, qtrm) of
@@ -474,8 +474,8 @@
        end
 
   | (Const (@{const_name "Ex1"}, ty) $ (Abs (_, _,
-      (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op :"}, _) $ _ $ 
-        (Const (@{const_name "Respects"}, _) $ resrel)) $ (t $ _)))), 
+      (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
@@ -495,7 +495,7 @@
          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 "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t,
      Const (@{const_name "All"}, ty') $ t') =>
        let
          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
@@ -506,7 +506,7 @@
          else mk_ball $ (mk_resp $ resrel) $ subtrm
        end
 
-  | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, 
+  | (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')
@@ -527,18 +527,18 @@
          else mk_bex1_rel $ resrel $ subtrm
        end
 
-  | (* equalities need to be replaced by appropriate equivalence relations *) 
+  | (* 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') 
+         else equiv_relation ctxt (domain_type ty, domain_type ty')
 
-  | (* in this case we just check whether the given equivalence relation is correct *) 
+  | (* 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') 
+         val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty')
        in
-         if rel' aconv rel then rtrm 
+         if rel' aconv rel then rtrm
          else term_mismatch "regularise (relation mismatch)" ctxt rel rel'
        end
 
@@ -557,7 +557,7 @@
              if Pattern.matches thy (rtrm', rtrm)
              then rtrm else term_mismatch "regularize(constant mismatch)" ctxt rtrm qtrm
            end
-       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)))) =>
@@ -571,11 +571,11 @@
        regularize_trm ctxt (t1, t1') $ regularize_trm ctxt (t2, t2')
 
   | (Bound i, Bound i') =>
-       if i = i' then rtrm 
+       if i = i' then rtrm
        else raise (LIFT_MATCH "regularize (bounds mismatch)")
 
   | _ =>
-       let 
+       let
          val rtrm_str = Syntax.string_of_term ctxt rtrm
          val qtrm_str = Syntax.string_of_term ctxt qtrm
        in
@@ -583,7 +583,7 @@
        end
 
 fun regularize_trm_chk ctxt (rtrm, qtrm) =
-  regularize_trm ctxt (rtrm, qtrm) 
+  regularize_trm ctxt (rtrm, qtrm)
   |> Syntax.check_term ctxt
 
 
@@ -595,22 +595,22 @@
 
   For abstractions:
 
-  * If the type of the abstraction needs lifting, then we add Rep/Abs 
+  * 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 
+
+  * 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 
+    are assumed to always need lifting). Otherwise we recurse on both
     arguments.
 
   For constants:
 
-  * If the constant is (op =), we leave it always unchanged. 
+  * 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. 
+    and Rep/Abs around it.
 
   For free variables:
 
@@ -619,13 +619,13 @@
   Vars case cannot occur.
 *)
 
-fun mk_repabs ctxt (T, T') trm = 
+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 
+  val qtrm_str = Syntax.string_of_term ctxt qtrm
 in
   raise LIFT_MATCH (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str])
 end
@@ -662,11 +662,11 @@
         else mk_repabs ctxt (rty, qty) result
       end
 
-  | (t $ s, t' $ s') =>  
+  | (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 
+  | (Free (_, T), Free (_, T')) =>
+        if T = T' then rtrm
         else mk_repabs ctxt (T, T') rtrm
 
   | (_, Const (@{const_name "op ="}, _)) => rtrm
@@ -674,15 +674,15 @@
   | (_, Const (_, T')) =>
       let
         val rty = fastype_of rtrm
-      in 
+      in
         if rty = T' then rtrm
         else mk_repabs ctxt (rty, T') rtrm
-      end   
-  
+      end
+
   | _ => inj_repabs_err ctxt "injection (default):" rtrm qtrm
 
 fun inj_repabs_trm_chk ctxt (rtrm, qtrm) =
-  inj_repabs_trm ctxt (rtrm, qtrm) 
+  inj_repabs_trm ctxt (rtrm, qtrm)
   |> Syntax.check_term ctxt