
diff -r 7d3d86beacd6 -r f46dc0ca08c3 QuotMain.thy
--- a/QuotMain.thy	Fri Nov 20 13:03:01 2009 +0100
+++ b/QuotMain.thy	Sat Nov 21 02:49:39 2009 +0100
@@ -557,7 +557,62 @@
 *}
 
 ML {*
-fun get_fun_new flag (rty, qty) lthy ty =
+fun negF absF = repF
+  | negF repF = absF
+
+fun get_fun flag qenv lthy ty =
+let
+  
+  fun get_fun_aux s fs =
+   (case (maps_lookup (ProofContext.theory_of lthy) s) of
+      SOME info => list_comb (Const (#mapfun info, dummyT), fs)
+    | NONE      => error ("no map association for type " ^ s))
+
+  fun get_const flag qty =
+  let 
+    val thy = ProofContext.theory_of lthy
+    val qty_name = Long_Name.base_name (fst (dest_Type qty))
+  in
+    case flag of
+      absF => Const (Sign.full_bname thy ("ABS_" ^ qty_name), dummyT)
+    | repF => Const (Sign.full_bname thy ("REP_" ^ qty_name), dummyT)
+  end
+
+  fun mk_identity ty = Abs ("", ty, Bound 0)
+
+in
+  if (AList.defined (op=) qenv ty)
+  then (get_const flag ty)
+  else (case ty of
+          TFree _ => mk_identity ty
+        | Type (_, []) => mk_identity ty 
+        | Type ("fun" , [ty1, ty2]) => 
+            let
+              val fs_ty1 = get_fun (negF flag) qenv lthy ty1
+              val fs_ty2 = get_fun flag qenv lthy ty2
+            in  
+              get_fun_aux "fun" [fs_ty1, fs_ty2]
+            end 
+        | Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys)
+        | _ => error ("no type variables allowed"))
+end
+
+(* returns all subterms where two types differ *)
+fun diff (T, S) Ds =
+  case (T, S) of
+    (TVar v, TVar u) => if v = u then Ds else (T, S)::Ds 
+  | (TFree x, TFree y) => if x = y then Ds else (T, S)::Ds
+  | (Type (a, Ts), Type (b, Us)) => 
+      if a = b then diffs (Ts, Us) Ds else (T, S)::Ds
+  | _ => (T, S)::Ds
+and diffs (T::Ts, U::Us) Ds = diffs (Ts, Us) (diff (T, U) Ds)
+  | diffs ([], []) Ds = Ds
+  | diffs _ _ = error "Unequal length of type arguments"
+
+*}
+
+ML {*
+fun get_fun_OLD flag (rty, qty) lthy ty =
   let
     val tys = find_matching_types rty ty;
     val qenv = map (fn t => (exchange_ty lthy rty qty t, t)) tys;
@@ -657,11 +712,11 @@
   fun mk_abs tm =
     let
       val ty = fastype_of tm
-    in Syntax.check_term lthy ((get_fun_new absF (rty, qty) lthy ty) $ tm) end
+    in Syntax.check_term lthy ((get_fun_OLD absF (rty, qty) lthy ty) $ tm) end
   fun mk_repabs tm =
     let
       val ty = fastype_of tm
-    in Syntax.check_term lthy ((get_fun_new repF (rty, qty) lthy ty) $ (mk_abs tm)) end
+    in Syntax.check_term lthy ((get_fun_OLD repF (rty, qty) lthy ty) $ (mk_abs tm)) end
 
     fun is_lifted_const (Const (x, _)) = member (op =) consts x
       | is_lifted_const _ = false;
@@ -1008,11 +1063,11 @@
     fun mk_rep tm =
       let
         val ty = exchange_ty lthy qty rty (fastype_of tm)
-      in Syntax.check_term lthy ((get_fun_new repF (rty, qty) lthy ty) $ tm) end;
+      in Syntax.check_term lthy ((get_fun_OLD repF (rty, qty) lthy ty) $ tm) end;
     fun mk_abs tm =
       let
         val ty = fastype_of tm
-      in Syntax.check_term lthy ((get_fun_new absF (rty, qty) lthy ty) $ tm) end
+      in Syntax.check_term lthy ((get_fun_OLD absF (rty, qty) lthy ty) $ tm) end
     val (l, ltl) = Term.strip_type ty;
     val nl = map absty l;
     val vs = map (fn _ => "x") l;
@@ -1149,7 +1204,6 @@
 (******************************************)
 
 (* exception for when qtrm and rtrm do not match *)
-ML {* exception LIFT_MATCH of string *}
 
 ML {*
 fun mk_resp_arg lthy (rty, qty) =
@@ -1161,7 +1215,7 @@
        if s = s' 
        then let
               val SOME map_info = maps_lookup thy s
-              val args = map (mk_resp_arg lthy) (tys ~~tys')
+              val args = map (mk_resp_arg lthy) (tys ~~ tys')
             in
               list_comb (Const (#relfun map_info, dummyT), args) 
             end  
@@ -1192,12 +1246,28 @@
 fun qnt_typ ty = domain_type (domain_type ty)
 *}
 
+(*
+Regularizing an rterm means:
+ - Quantifiers over a type that needs lifting are replaced by
+   bounded quantifiers, for example:
+      \<forall>x. P     \<Longrightarrow>     \<forall>x\<in>(Respects R). P
+ - Abstractions over a type that needs lifting are replaced
+   by bounded abstractions:
+      \<lambda>x. P     \<Longrightarrow>     Ball (Respects R) (\<lambda>x. P)
+
+ - Equalities over the type being lifted are replaced by
+   appropriate relations:
+      A = B     \<Longrightarrow>     A \<approx> B
+   Example with more complicated types of A, B:
+      A = B     \<Longrightarrow>     (op = \<Longrightarrow> op \<approx>) A B
+*)
+
 ML {*
-fun REGULARIZE_aux lthy rtrm qtrm =
+fun REGULARIZE_trm lthy rtrm qtrm =
   case (rtrm, qtrm) of
     (Abs (x, T, t), Abs (x', T', t')) =>
        let
-         val subtrm = REGULARIZE_aux lthy t t'
+         val subtrm = REGULARIZE_trm lthy t t'
        in     
          if T = T'
          then Abs (x, T, subtrm)
@@ -1205,7 +1275,7 @@
        end
   | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
        let
-         val subtrm = apply_subt (REGULARIZE_aux lthy) t t'
+         val subtrm = apply_subt (REGULARIZE_trm lthy) t t'
        in
          if ty = ty'
          then Const (@{const_name "All"}, ty) $ subtrm
@@ -1213,7 +1283,7 @@
        end
   | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
        let
-         val subtrm = apply_subt (REGULARIZE_aux lthy) t t'
+         val subtrm = apply_subt (REGULARIZE_trm lthy) t t'
        in
          if ty = ty'
          then Const (@{const_name "Ex"}, ty) $ subtrm
@@ -1222,14 +1292,14 @@
   (* 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'
+         val subtrm = REGULARIZE_trm 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')
+       (REGULARIZE_trm lthy t1 t1') $ (REGULARIZE_trm lthy t2 t2')
   | (Free (x, ty), Free (x', ty')) =>
        if x = x' 
        then rtrm 
@@ -1246,11 +1316,98 @@
 *}
 
 ML {*
-fun REGULARIZE_trm lthy rtrm qtrm =
-  REGULARIZE_aux lthy rtrm qtrm
-  |> Syntax.check_term lthy
-  
+fun mk_REGULARIZE_goal lthy rtrm qtrm =
+      Logic.mk_implies (rtrm, REGULARIZE_trm lthy rtrm qtrm |> Syntax.check_term lthy)
 *}
 
+(*
+To prove that the old theorem implies the new one, we first
+atomize it and then try:
+ - Reflexivity of the relation
+ - Assumption
+ - Elimnating quantifiers on both sides of toplevel implication
+ - Simplifying implications on both sides of toplevel implication
+ - Ball (Respects ?E) ?P = All ?P
+ - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q
+
+*)
+
+lemma my_equiv_res_forall2:
+  fixes P::"'a \<Rightarrow> bool"
+  fixes Q::"'b \<Rightarrow> bool"
+  assumes a: "(All Q) \<longrightarrow> (All P)"
+  shows "(All Q) \<longrightarrow> Ball (Respects E) P"
+using a by auto
+
+lemma my_equiv_res_exists:
+  fixes P::"'a \<Rightarrow> bool"
+  fixes Q::"'b \<Rightarrow> bool"
+  assumes a: "EQUIV E"
+  and     b: "(Ex Q) \<longrightarrow> (Ex P)"
+  shows "(Ex Q) \<longrightarrow> Bex (Respects E) P"
+apply(subst equiv_res_exists)
+apply(rule a)
+apply(rule b)
+done
+
+ML {*
+fun REGULARIZE_tac lthy rel_refl rel_eqv =
+  ObjectLogic.full_atomize_tac THEN'
+   REPEAT_ALL_NEW (FIRST' 
+     [rtac rel_refl,
+      atac,
+      rtac @{thm universal_twice},
+      rtac @{thm impI} THEN' atac,
+      rtac @{thm implication_twice},
+      rtac @{thm my_equiv_res_forall2},
+      rtac (rel_eqv RS @{thm my_equiv_res_exists}),
+      (* For a = b \<longrightarrow> a \<approx> b *)
+      rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl,
+      rtac @{thm RIGHT_RES_FORALL_REGULAR}])
+*}
+
+(* same version including debugging information *)
+ML {*
+fun my_print_tac ctxt s thm =
+let
+  val prems_str = prems_of thm
+                  |> map (Syntax.string_of_term ctxt)
+                  |> cat_lines
+  val _ = tracing (s ^ "\n" ^ prems_str)
+in
+  Seq.single thm
+end
+ 
+fun DT ctxt s tac = EVERY' [tac, K (my_print_tac ctxt ("after " ^ s))]
+*}
+
+ML {*
+fun REGULARIZE_tac' lthy rel_refl rel_eqv =
+   (REPEAT1 o FIRST1) 
+     [(K (print_tac "start")) THEN' (K no_tac), 
+      DT lthy "1" (rtac rel_refl),
+      DT lthy "2" atac,
+      DT lthy "3" (rtac @{thm universal_twice}),
+      DT lthy "4" (rtac @{thm impI} THEN' atac),
+      DT lthy "5" (rtac @{thm implication_twice}),
+      DT lthy "6" (rtac @{thm my_equiv_res_forall2}),
+      DT lthy "7" (rtac (rel_eqv RS @{thm my_equiv_res_exists})),
+      (* For a = b \<longrightarrow> a \<approx> b *)
+      DT lthy "8" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl),
+      DT lthy "9" (rtac @{thm RIGHT_RES_FORALL_REGULAR})]
+*}
+
+ML {*
+fun REGULARIZE_prove rtrm qtrm rel_eqv rel_refl lthy =
+  let
+    val goal = mk_REGULARIZE_goal lthy rtrm qtrm
+    val cthm = Goal.prove lthy [] [] goal 
+      (fn {context, ...} => REGULARIZE_tac context rel_refl rel_eqv 1)
+  in
+    cthm 
+  end
+*}
+
+
 end
 




