# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1258718581 -3600
# Node ID 7d3d86beacd6e2b1949a09f659d8c7db91af0921
# Parent  0ae9d9e66cb78781cc92ebddab61c54204ad5d8a
started regularize of rtrm/qtrm version; looks quite promising

diff -r 0ae9d9e66cb7 -r 7d3d86beacd6 IntEx.thy
--- a/IntEx.thy	Thu Nov 19 14:17:10 2009 +0100
+++ b/IntEx.thy	Fri Nov 20 13:03:01 2009 +0100
@@ -22,7 +22,6 @@
 
 ML {* print_qconstinfo @{context} *}
 
-
 term ZERO
 thm ZERO_def
 
@@ -143,19 +142,20 @@
 *}
 
 print_quotients
+ML {* quotdata_lookup @{context} "IntEx.my_int" *}
+ML {* quotdata_lookup @{context} "my_int" *}
 
 ML {* 
   val test = lift_thm_my_int @{context} @{thm plus_sym_pre} 
 *}
 
-ML {* my_lift (prop_of test) @{thm plus_sym_pre} @{context} *}
 
 ML {*
-  ObjectLogic.atomize_term @{theory} (prop_of test)
-  |> Syntax.string_of_term @{context}
-  |> writeln
+  val aqtrm = HOLogic.dest_Trueprop (prop_of (atomize_thm test))
+  val artrm = HOLogic.dest_Trueprop (prop_of (atomize_thm @{thm plus_sym_pre})) 
 *}
 
+
 lemma plus_assoc_pre:
   shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"
   apply (cases i)
diff -r 0ae9d9e66cb7 -r 7d3d86beacd6 QuotMain.thy
--- a/QuotMain.thy	Thu Nov 19 14:17:10 2009 +0100
+++ b/QuotMain.thy	Fri Nov 20 13:03:01 2009 +0100
@@ -331,7 +331,7 @@
        end
   | Const (@{const_name "op ="}, ty) $ t =>
       if needs_lift rty (fastype_of t) then
-        (tyRel (fastype_of t) rty rel lthy) $ t
+        (tyRel (fastype_of t) rty rel lthy) $ t   (* FIXME: t should be regularised too *)
       else Const (@{const_name "op ="}, ty) $ (my_reg lthy rel rty t)
   | t1 $ t2 => (my_reg lthy rel rty t1) $ (my_reg lthy rel rty t2)
   | _ => trm
@@ -1144,19 +1144,112 @@
   end
 *}
 
+(******************************************)
+(* version with explicit qtrm             *)
+(******************************************)
+
+(* exception for when qtrm and rtrm do not match *)
+ML {* exception LIFT_MATCH of string *}
+
 ML {*
-fun my_lift qtrm rthm lthy =
+fun mk_resp_arg lthy (rty, qty) =
 let
   val thy = ProofContext.theory_of lthy
+in  
+  case (rty, qty) of
+    (Type (s, tys), Type (s', tys')) =>
+       if s = s' 
+       then let
+              val SOME map_info = maps_lookup thy s
+              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'
+            in
+              #rel qinfo
+            end
+    | _ => HOLogic.eq_const dummyT
+end
+*}
 
-  val a_rthm = atomize_thm rthm
-  val a_qtrm = ObjectLogic.atomize_term thy qtrm
+ML {*
+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)
+*}
+
+ML {*
+(* applies f to the subterm of an abstractions, otherwise to the given term *)
+(* abstracted variables do not have to be treated specially *)
+fun apply_subt f trm1 trm2 =
+  case (trm1, trm2) of
+    (Abs (x, T, t), Abs (x', T', t')) => Abs (x, T, f t t')
+  | _ => f trm1 trm2
+
+fun qnt_typ ty = domain_type (domain_type ty)
+*}
 
-  val _ = Syntax.string_of_term lthy (prop_of a_rthm) |> writeln
-  val _ = Syntax.string_of_term lthy a_qtrm |> writeln
-in
-  (a_rthm, a_qtrm)
-end
+ML {*
+fun REGULARIZE_aux lthy rtrm qtrm =
+  case (rtrm, qtrm) of
+    (Abs (x, T, t), Abs (x', T', t')) =>
+       let
+         val subtrm = REGULARIZE_aux lthy t t'
+       in     
+         if T = T'
+         then Abs (x, T, subtrm)
+         else  mk_babs $ (mk_resp $ mk_resp_arg lthy (T, T')) $ subtrm
+       end
+  | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
+       let
+         val subtrm = apply_subt (REGULARIZE_aux 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_aux 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
+  (* FIXME: why is there a case for equality? is it correct? *)
+  | (Const (@{const_name "op ="}, ty) $ t, Const (@{const_name "op ="}, ty') $ t') =>
+       let
+         val subtrm = REGULARIZE_aux lthy t t'
+       in
+         if ty = ty'
+         then Const (@{const_name "op ="}, ty) $ subtrm
+         else mk_resp_arg lthy (ty, ty') $ subtrm
+       end 
+  | (t1 $ t2, t1' $ t2') =>
+       (REGULARIZE_aux lthy t1 t1') $ (REGULARIZE_aux lthy t2 t2')
+  | (Free (x, ty), Free (x', ty')) =>
+       if x = x' 
+       then rtrm 
+       else raise LIFT_MATCH "quotient and lifted theorem do not match"
+  | (Bound i, Bound i') =>
+       if i = i' 
+       then rtrm 
+       else raise LIFT_MATCH "quotient and lifted theorem do not match"
+  | (Const (s, ty), Const (s', ty')) =>
+       if s = s' andalso ty = ty'
+       then rtrm
+       else rtrm (* FIXME: check correspondence according to definitions *) 
+  | _ => raise LIFT_MATCH "quotient and lifted theorem do not match"
+*}
+
+ML {*
+fun REGULARIZE_trm lthy rtrm qtrm =
+  REGULARIZE_aux lthy rtrm qtrm
+  |> Syntax.check_term lthy
+  
 *}
 
 end
diff -r 0ae9d9e66cb7 -r 7d3d86beacd6 quotient.ML
--- a/quotient.ML	Thu Nov 19 14:17:10 2009 +0100
+++ b/quotient.ML	Fri Nov 20 13:03:01 2009 +0100
@@ -146,10 +146,10 @@
   val quotient_thm_name = Binding.prefix_name "QUOTIENT_" qty_name
 
   (* storing the quot-info *)
-  val qty_str = fst (dest_Type abs_ty)		  
-  val lthy3 = quotdata_update qty_str (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2
+  val qty_str = fst (Term.dest_Type abs_ty)
+  val _ = tracing ("storing under: " ^ qty_str)
+  val lthy3 = quotdata_update qty_str (Logic.varifyT abs_ty, Logic.varifyT rty, rel, equiv_thm) lthy2  
   (* FIXME: varifyT should not be used *)
-  (* the type name maybe should be calculated via qty_name and Sign.intern_type *)
 
   (* interpretation *)
   val bindd = ((Binding.make ("", Position.none)), ([]: Attrib.src list))
diff -r 0ae9d9e66cb7 -r 7d3d86beacd6 quotient_info.ML
--- a/quotient_info.ML	Thu Nov 19 14:17:10 2009 +0100
+++ b/quotient_info.ML	Fri Nov 20 13:03:01 2009 +0100
@@ -79,7 +79,9 @@
    val extend = I
    val merge = Symtab.merge (K true)) 
 
-val quotdata_lookup_thy = Symtab.lookup o QuotData.get
+fun quotdata_lookup_thy thy str = 
+    Symtab.lookup (QuotData.get thy) (Sign.intern_type thy str)
+
 val quotdata_lookup = quotdata_lookup_thy o ProofContext.theory_of
 
 fun quotdata_update_thy qty_name (qty, rty, rel, equiv_thm) =