# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1258979052 -3600
# Node ID 5a7024be908317715cbf18085ce69fd6ef7e6ada
# Parent  7851e2a74f850c8a005b3375fbb44d2bfd4c3572
code review with Cezary

diff -r 7851e2a74f85 -r 5a7024be9083 FSet.thy
--- a/FSet.thy	Mon Nov 23 10:26:59 2009 +0100
+++ b/FSet.thy	Mon Nov 23 13:24:12 2009 +0100
@@ -377,6 +377,8 @@
 
 thm list.recs(2)
 ML {* val t_a = atomize_thm @{thm list_induct_part} *}
+
+
 (* prove {* build_regularize_goal t_a rty rel @{context}  *}
  ML_prf {*  fun tac ctxt = FIRST' [
       rtac rel_refl,
@@ -384,7 +386,7 @@
       rtac @{thm universal_twice},
       (rtac @{thm impI} THEN' atac),
       rtac @{thm implication_twice},
-      (*rtac @{thm equality_twice},*)
+      //comented out  rtac @{thm equality_twice}, //
       EqSubst.eqsubst_tac ctxt [0]
         [(@{thm equiv_res_forall} OF [rel_eqv]),
          (@{thm equiv_res_exists} OF [rel_eqv])],
@@ -393,7 +395,7 @@
      ]; *}
   apply (atomize(full))
   apply (tactic {* REPEAT_ALL_NEW (tac @{context}) 1 *})
-  done*)
+  done  *)
 ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *}
 ML {*
   val rt = build_repabs_term @{context} t_r consts rty qty
@@ -589,9 +591,24 @@
 ML {* val (tta, ttb) = (my_reg2 @{context} (prop_of t_a) (term_of glac)) *}
 
 (* Does not work. *)
-(* ML {* val ttar = REGULARIZE_trm @{context} (prop_of t_a) (term_of glac) *} *)
+ML {* 
+  prop_of t_a 
+  |> Syntax.string_of_term @{context}
+  |> writeln
+*}
+
+ML {* 
+  (term_of glac) 
+  |> Syntax.string_of_term @{context}
+  |> writeln
+*}
+
+ML {* val ttar = REGULARIZE_trm @{context} (prop_of t_a) (term_of glac) *} 
 
 ML {* val tt = Syntax.check_term @{context} tta *}
+ML {* val ttr = Syntax.check_term @{context} ttar *}
+
+
 
 prove t_r: {* Logic.mk_implies
        ((prop_of t_a), tt) *}
diff -r 7851e2a74f85 -r 5a7024be9083 IntEx.thy
--- a/IntEx.thy	Mon Nov 23 10:26:59 2009 +0100
+++ b/IntEx.thy	Mon Nov 23 13:24:12 2009 +0100
@@ -187,22 +187,26 @@
   val qty = fastype_of qtrm
 in
   case (rtrm, qtrm) of
-    (Abs (x, T, t), Abs (x', T', t')) =>
+    (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>
+       Const (@{const_name "Ball"}, T) $ r $ (inj_REPABS lthy (t, t'))
+  | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>
+       Const (@{const_name "Bex"}, T) $ r $ (inj_REPABS lthy (t, t'))
+  | (Const (@{const_name "Babs"}, T) $ r $ t, t') =>
+       Const (@{const_name "Babs"}, T) $ r $ (inj_REPABS lthy (t, t'))
+  | (Abs (x, T, t), Abs (x', T', t')) =>
       let
         val (y, s) = Term.dest_abs (x, T, t)
-        val (y', s') = Term.dest_abs (x', T', t')
+        val (_, s') = Term.dest_abs (x', T', t')
         val yvar = Free (y, T)
         val res = lambda yvar (inj_REPABS lthy (s, s'))
       in
-        if T = T'
+        if rty = qty
         then res
-        else mk_repabs lthy (rty, qty) (replace_bnd0 (mk_repabs lthy (T, T') (Bound 0), res))
+        else if T = T'
+             then mk_repabs lthy (rty, qty) res
+             else mk_repabs lthy (rty, qty) (replace_bnd0 (mk_repabs lthy (T, T') (Bound 0), res))
       end
-  (* FIXME: Does one have to look at the abstraction or have to go under the lambda? *) 
-  | (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>
-       Const (@{const_name "Ball"}, T) $ r $ (inj_REPABS lthy (t, t'))
-  | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>
-       Const (@{const_name "Bex"}, T) $ r $ (inj_REPABS lthy (t, t'))
+    (* TODO: check what happens if head is a constant *)
   | (_ $ _, _ $ _) => 
       let
         val (rhead, rargs) = strip_comb rtrm
@@ -213,9 +217,14 @@
       in
         if rty = qty
         then result
-        else mk_repabs lthy (rty, qty) res
+        else mk_repabs lthy (rty, qty) result
       end
-  (* FIXME: cases for frees and vars? *)
+  (* TODO: maybe leave result without mk_repabs when head is a constant *)
+  (* TODO: that we do not know how to lift *)
+  | (Const (s, T), Const (s', T')) =>
+       if T = T'
+       then rtrm
+       else mk_repabs lthy (T, T') rtrm
   | _ => rtrm
 end
 *}
@@ -286,6 +295,10 @@
   |> Syntax.check_term @{context}
 *}
 
+
+ML {* val my_goal = cterm_of @{theory} (mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm)) *}
+ML {* val yr_goal = cterm_of @{theory} (build_repabs_goal @{context} (@{thm testtest} OF [arthm]) consts rty qty) *}
+
 prove {* mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm) *}
 apply(tactic {* ObjectLogic.full_atomize_tac 1 *})
 (* does not work *)
diff -r 7851e2a74f85 -r 5a7024be9083 QuotMain.thy
--- a/QuotMain.thy	Mon Nov 23 10:26:59 2009 +0100
+++ b/QuotMain.thy	Mon Nov 23 13:24:12 2009 +0100
@@ -1212,10 +1212,16 @@
 let
   val thy = ProofContext.theory_of lthy
 in  
-  case (rty, qty) of
-    (Type (s, tys), Type (s', tys')) =>
+  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 _ = tracing ("maps lookup for  " ^ s)
+              val _ = tracing (Syntax.string_of_typ lthy rty)
+              val _ = tracing (Syntax.string_of_typ lthy qty)
               val SOME map_info = maps_lookup thy s
               val args = map (mk_resp_arg lthy) (tys ~~ tys')
             in
@@ -1228,7 +1234,7 @@
             in
               #rel qinfo
             end
-    | _ => HOLogic.eq_const dummyT 
+      | _ => HOLogic.eq_const dummyT 
            (* FIXME: do the types correspond to each other? *)
 end
 *}
@@ -1263,7 +1269,7 @@
   | _ => f trm1 trm2
 
 (* the major type of All and Ex quantifiers *)
-fun qnt_typ ty = domain_type (domain_type ty)
+fun qnt_typ ty = domain_type (domain_type ty)  
 *}
 
 (*
@@ -1305,6 +1311,9 @@
   | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
        let
          val subtrm = apply_subt (REGULARIZE_trm lthy) t t'
+         val _ = tracing "quantor types All"
+         val _ = tracing (Syntax.string_of_typ lthy ty)
+         val _ = tracing (Syntax.string_of_typ lthy ty')
        in
          if ty = ty'
          then Const (@{const_name "All"}, ty) $ subtrm
@@ -1313,12 +1322,15 @@
   | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
        let
          val subtrm = apply_subt (REGULARIZE_trm lthy) t t'
+         val _ = tracing "quantor types Ex"
+         val _ = tracing (Syntax.string_of_typ lthy ty)
+         val _ = tracing (Syntax.string_of_typ lthy ty')
        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? *)
+    (* FIXME: should be replaced when fully applied? then 2nd argument *)
   | (Const (@{const_name "op ="}, ty) $ t, Const (@{const_name "op ="}, ty') $ t') =>
        let
          val subtrm = REGULARIZE_trm lthy t t'