
diff -r 86fba2c4eeef -r 57bde65f6eb2 QuotMain.thy
--- a/QuotMain.thy	Wed Nov 25 10:52:21 2009 +0100
+++ b/QuotMain.thy	Wed Nov 25 11:41:42 2009 +0100
@@ -227,35 +227,6 @@
 
 *)
 
-text {* tyRel takes a type and builds a relation that a quantifier over this
-  type needs to respect. *}
-ML {*
-fun tyRel ty rty rel lthy =
-  if Sign.typ_instance (ProofContext.theory_of lthy) (ty, rty)
-  then rel
-  else (case ty of
-          Type (s, tys) =>
-            let
-              val tys_rel = map (fn ty => ty --> ty --> @{typ bool}) tys;
-              val ty_out = ty --> ty --> @{typ bool};
-              val tys_out = tys_rel ---> ty_out;
-            in
-            (case (maps_lookup (ProofContext.theory_of lthy) s) of
-               SOME (info) => list_comb (Const (#relfun info, tys_out),
-                              map (fn ty => tyRel ty rty rel lthy) tys)
-             | NONE  => HOLogic.eq_const ty
-            )
-            end
-        | _ => HOLogic.eq_const ty)
-*}
-
-(* 
-ML {* cterm_of @{theory} 
-  (tyRel @{typ "'a \<Rightarrow> 'a list \<Rightarrow> 't \<Rightarrow> 't"} (Logic.varifyT @{typ "'a list"}) 
-         @{term "f::('a list \<Rightarrow> 'a list \<Rightarrow> bool)"} @{context}) 
-*} 
-*)
-
 definition
   Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
 where
@@ -273,94 +244,6 @@
 
 *}
 
-ML {*
-fun mk_babs ty ty' = Const (@{const_name "Babs"}, [ty' --> @{typ bool}, ty] ---> ty)
-fun mk_ball ty = Const (@{const_name "Ball"}, [ty, ty] ---> @{typ bool})
-fun mk_bex ty = Const (@{const_name "Bex"}, [ty, ty] ---> @{typ bool})
-fun mk_resp ty = Const (@{const_name Respects}, [[ty, ty] ---> @{typ bool}, ty] ---> @{typ bool})
-*}
-
-(* applies f to the subterm of an abstractions, otherwise to the given term *)
-ML {*
-fun apply_subt f trm =
-  case trm of
-    Abs (x, T, t) => 
-       let 
-         val (x', t') = Term.dest_abs (x, T, t)
-       in
-         Term.absfree (x', T, f t') 
-       end
-  | _ => f trm
-*}
-
-(* FIXME: if there are more than one quotient, then you have to look up the relation *)
-ML {*
-fun my_reg lthy rel rty trm =
-  case trm of
-    Abs (x, T, t) =>
-       if (needs_lift rty T) then
-         let
-            val rrel = tyRel T rty rel lthy
-         in
-           (mk_babs (fastype_of trm) T) $ (mk_resp T $ rrel) $ (apply_subt (my_reg lthy rel rty) trm)
-         end
-       else
-         Abs(x, T, (apply_subt (my_reg lthy rel rty) t))
-  | Const (@{const_name "All"}, ty) $ (t as Abs (x, T, _)) =>
-       let
-          val ty1 = domain_type ty
-          val ty2 = domain_type ty1
-          val rrel = tyRel T rty rel lthy
-       in
-         if (needs_lift rty T) then
-           (mk_ball ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t)
-         else
-           Const (@{const_name "All"}, ty) $ apply_subt (my_reg lthy rel rty) t
-       end
-  | Const (@{const_name "Ex"}, ty) $ (t as Abs (x, T, _)) =>
-       let
-          val ty1 = domain_type ty
-          val ty2 = domain_type ty1
-          val rrel = tyRel T rty rel lthy
-       in
-         if (needs_lift rty T) then
-           (mk_bex ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t)
-         else
-           Const (@{const_name "Ex"}, ty) $ apply_subt (my_reg lthy rel rty) t
-       end
-  | Const (@{const_name "op ="}, ty) $ t =>
-      if needs_lift rty (fastype_of t) then
-        (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
-*}
-
-(* For polymorphic types we need to find the type of the Relation term. *)
-(* TODO: we assume that the relation is a Constant. Is this always true? *)
-ML {*
-fun my_reg_inst lthy rel rty trm =
-  case rel of
-    Const (n, _) => Syntax.check_term lthy
-      (my_reg lthy (Const (n, dummyT)) (Logic.varifyT rty) trm)
-*}
-
-(*
-ML {*
-  val r = Free ("R", dummyT);
-  val t = (my_reg_inst @{context} r @{typ "'a list"} @{term "\<forall>(x::'b list). P x"});
-  val t2 = Syntax.check_term @{context} t;
-  cterm_of @{theory} t2
-*}
-*)
-
-text {* Assumes that the given theorem is atomized *}
-ML {*
-  fun build_regularize_goal thm rty rel lthy =
-     Logic.mk_implies
-       ((prop_of thm),
-       (my_reg_inst lthy rel rty (prop_of thm)))
-*}
 
 lemma universal_twice:
   assumes *: "\<And>x. (P x \<longrightarrow> Q x)"
@@ -373,32 +256,6 @@
   shows "(a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
 using a b by auto
 
-ML {*
-fun regularize thm rty rel rel_eqv rel_refl lthy =
-  let
-    val goal = build_regularize_goal thm rty rel lthy;
-    fun tac ctxt =
-      (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},
-        EqSubst.eqsubst_tac ctxt [0]
-          [(@{thm equiv_res_forall} OF [rel_eqv]),
-           (@{thm equiv_res_exists} OF [rel_eqv])],
-        (* 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})
-      ]);
-    val cthm = Goal.prove lthy [] [] goal
-      (fn {context, ...} => tac context 1);
-  in
-    cthm OF [thm]
-  end
-*}
-
 section {* RepAbs injection *}
 (*
 
@@ -473,16 +330,6 @@
   handle TYPE _ => ty (* for dest_Type *)
 *}
 
-(*consts Rl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
-axioms Rl_eq: "EQUIV Rl"
-
-quotient ql = "'a list" / "Rl"
-  by (rule Rl_eq)
-ML {*
-  ctyp_of @{theory} (exchange_ty @{context} (Logic.varifyT @{typ "'a list"}) (Logic.varifyT @{typ "'a ql"}) @{typ "nat list \<Rightarrow> (nat \<times> nat) list"});
-  ctyp_of @{theory} (exchange_ty @{context} (Logic.varifyT @{typ "nat \<times> nat"}) (Logic.varifyT @{typ "int"}) @{typ "nat list \<Rightarrow> (nat \<times> nat) list"})
-*}
-*)
 
 ML {*
 fun find_matching_types rty ty =
@@ -535,19 +382,6 @@
         | 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 {*
@@ -609,73 +443,6 @@
 ML {* symmetric (eq_reflection OF @{thms id_def}) *}
 
 ML {*
-fun build_repabs_term lthy thm consts rty qty =
-  let
-    (* TODO: The rty and qty stored in the quotient_info should
-       be varified, so this will soon not be needed *)
-    val rty = Logic.varifyT rty;
-    val qty = Logic.varifyT qty;
-
-  fun mk_abs tm =
-    let
-      val ty = fastype_of tm
-    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_OLD repF (rty, qty) lthy ty) $ (mk_abs tm)) end
-
-    fun is_lifted_const (Const (x, _)) = member (op =) consts x
-      | is_lifted_const _ = false;
-
-    fun build_aux lthy tm =
-      case tm of
-        Abs (a as (_, vty, _)) =>
-          let
-            val (vs, t) = Term.dest_abs a;
-            val v = Free(vs, vty);
-            val t' = lambda v (build_aux lthy t)
-          in
-            if (not (needs_lift rty (fastype_of tm))) then t'
-            else mk_repabs (
-              if not (needs_lift rty vty) then t'
-              else
-                let
-                  val v' = mk_repabs v;
-                  (* TODO: I believe 'beta' is not needed any more *)
-                  val t1 = (* Envir.beta_norm *) (t' $ v')
-                in
-                  lambda v t1
-                end)
-          end
-      | x =>
-        case Term.strip_comb tm of
-          (Const(@{const_name Respects}, _), _) => tm
-        | (opp, tms0) =>
-          let
-            val tms = map (build_aux lthy) tms0
-            val ty = fastype_of tm
-          in
-            if (is_lifted_const opp andalso needs_lift rty ty) then
-            mk_repabs (list_comb (opp, tms))
-            else if ((Term.is_Free opp) andalso (length tms > 0) andalso (needs_lift rty ty)) then
-              mk_repabs (list_comb (opp, tms))
-            else if tms = [] then opp
-            else list_comb(opp, tms)
-          end
-  in
-    repeat_eqsubst_prop lthy @{thms id_def_sym}
-      (build_aux lthy (Thm.prop_of thm))
-  end
-*}
-
-text {* Builds provable goals for regularized theorems *}
-ML {*
-fun build_repabs_goal ctxt thm cons rty qty =
-  Logic.mk_equals ((Thm.prop_of thm), (build_repabs_term ctxt thm cons rty qty))
-*}
-
-ML {*
 fun instantiate_tac thm = Subgoal.FOCUS (fn {concl, ...} =>
   let
     val pat = Drule.strip_imp_concl (cprop_of thm)
@@ -801,19 +568,6 @@
     ])
 *}
 
-ML {*
-fun repabs lthy thm consts rty qty quot_thm reflex_thm trans_thm rsp_thms =
-  let
-    val rt = build_repabs_term lthy thm consts rty qty;
-    val rg = Logic.mk_equals ((Thm.prop_of thm), rt);
-    fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN'
-      (REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms));
-    val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1);
-  in
-    @{thm Pure.equal_elim_rule1} OF [cthm, thm]
-  end
-*}
-
 section {* Cleaning the goal *}
 
 
@@ -854,22 +608,6 @@
   end
 *}
 
-(* TODO: Check if it behaves properly with varifyed rty *)
-ML {*
-fun findabs_all rty tm =
-  case tm of
-    Abs(_, T, b) =>
-      let
-        val b' = subst_bound ((Free ("x", T)), b);
-        val tys = findabs_all rty b'
-        val ty = fastype_of tm
-      in if needs_lift rty ty then (ty :: tys) else tys
-      end
-  | f $ a => (findabs_all rty f) @ (findabs_all rty a)
-  | _ => [];
-fun findabs rty tm = distinct (op =) (findabs_all rty tm)
-*}
-
 ML {*
 fun findaps_all rty tm =
   case tm of
@@ -882,83 +620,6 @@
 fun findaps rty tm = distinct (op =) (findaps_all rty tm)
 *}
 
-(* Currently useful only for LAMBDA_PRS *)
-ML {*
-fun make_simp_prs_thm lthy quot_thm thm typ =
-  let
-    val (_, [lty, rty]) = dest_Type typ;
-    val thy = ProofContext.theory_of lthy;
-    val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty)
-    val inst = [SOME lcty, NONE, SOME rcty];
-    val lpi = Drule.instantiate' inst [] thm;
-    val tac =
-      (compose_tac (false, lpi, 2)) THEN_ALL_NEW
-      (quotient_tac quot_thm);
-    val gc = Drule.strip_imp_concl (cprop_of lpi);
-    val t = Goal.prove_internal [] gc (fn _ => tac 1)
-  in
-    MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t
-  end
-*}
-
-ML {*
-fun findallex_all rty qty tm =
-  case tm of
-    Const (@{const_name All}, T) $ (s as (Abs(_, _, b))) =>
-      let
-        val (tya, tye) = findallex_all rty qty s
-      in if needs_lift rty T then
-        ((T :: tya), tye)
-      else (tya, tye) end
-  | Const (@{const_name Ex}, T) $ (s as (Abs(_, _, b))) =>
-      let
-        val (tya, tye) = findallex_all rty qty s
-      in if needs_lift rty T then
-        (tya, (T :: tye))
-      else (tya, tye) end
-  | Abs(_, T, b) =>
-      findallex_all rty qty (subst_bound ((Free ("x", T)), b))
-  | f $ a =>
-      let
-        val (a1, e1) = findallex_all rty qty f;
-        val (a2, e2) = findallex_all rty qty a;
-      in (a1 @ a2, e1 @ e2) end
-  | _ => ([], []);
-*}
-
-ML {*
-fun findallex lthy rty qty tm =
-  let
-    val (a, e) = findallex_all rty qty tm;
-    val (ad, ed) = (map domain_type a, map domain_type e);
-    val (au, eu) = (distinct (op =) ad, distinct (op =) ed);
-    val (rty, qty) = (Logic.varifyT rty, Logic.varifyT qty)
-  in
-    (map (exchange_ty lthy rty qty) au, map (exchange_ty lthy rty qty) eu)
-  end
-*}
-
-ML {*
-fun make_allex_prs_thm lthy quot_thm thm typ =
-  let
-    val (_, [lty, rty]) = dest_Type typ;
-    val thy = ProofContext.theory_of lthy;
-    val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty)
-    val inst = [NONE, SOME lcty];
-    val lpi = Drule.instantiate' inst [] thm;
-    val tac =
-      (compose_tac (false, lpi, 1)) THEN_ALL_NEW
-      (quotient_tac quot_thm);
-    val gc = Drule.strip_imp_concl (cprop_of lpi);
-    val t = Goal.prove_internal [] gc (fn _ => tac 1)
-    val t_noid = MetaSimplifier.rewrite_rule
-      [@{thm eq_reflection} OF @{thms id_apply}] t;
-    val t_sym = @{thm "HOL.sym"} OF [t_noid];
-    val t_eq = @{thm "eq_reflection"} OF [t_sym]
-  in
-    t_eq
-  end
-*}
 
 ML {*
 fun applic_prs lthy rty qty absrep ty =
@@ -1035,76 +696,6 @@
 *}
 
 
-ML {*
-fun lift_thm lthy qty qty_name rsp_thms defs rthm = 
-let
-  val _ = tracing ("raw theorem:\n" ^ Syntax.string_of_term lthy (prop_of rthm))
-
-  val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty;
-  val (trans2, reps_same, absrep, quot) = lookup_quot_thms lthy qty_name;
-  val consts = lookup_quot_consts defs;
-  val t_a = atomize_thm rthm;
-
-  val _ = tracing ("raw atomized theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_a))
-
-  val t_r = regularize t_a rty rel rel_eqv rel_refl lthy;
-
-  val _ = tracing ("regularised theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_r))
-
-  val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms;
-
-  val _ = tracing ("rep/abs injected theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_t))
-
-  val (alls, exs) = findallex lthy rty qty (prop_of t_a);
-  val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls
-  val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs
-  val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t
-
-  val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_a))
-
-  val abs = findabs rty (prop_of t_a);
-  val aps = findaps rty (prop_of t_a);
-  val app_prs_thms = map (applic_prs lthy rty qty absrep) aps;
-  val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs;
-  val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a;
-  
-  val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_l))
-
-  val defs_sym = flat (map (add_lower_defs lthy) defs);
-  val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym;
-  val t_id = simp_ids lthy t_l;
-
-  val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_id))
-
-  val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_id;
-
-  val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_d0))
-
-  val t_d = repeat_eqsubst_thm lthy defs_sym t_d0;
-
-  val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_d))
-
-  val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d;
-
-  val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_r))
-
-  val t_rv = ObjectLogic.rulify t_r
-
-  val _ = tracing ("lifted theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_rv))
-in
-  Thm.varifyT t_rv
-end
-*}
-
-ML {*
-fun lift_thm_note qty qty_name rsp_thms defs thm name lthy =
-  let
-    val lifted_thm = lift_thm lthy qty qty_name rsp_thms defs thm;
-    val (_, lthy2) = note (name, lifted_thm) lthy;
-  in
-    lthy2
-  end
-*}
 
 (******************************************)
 (******************************************)
@@ -1461,70 +1052,6 @@
 *}
 
 ML {*
-fun regularize_goal lthy thm rel_eqv rel_refl qtrm =
-  let
-    val reg_trm = mk_REGULARIZE_goal lthy (prop_of thm) qtrm;
-    fun tac lthy = regularize_tac lthy rel_eqv rel_refl;
-    val cthm = Goal.prove lthy [] [] reg_trm
-      (fn {context, ...} => tac context 1);
-  in
-    cthm OF [thm]
-  end
-*}
-
-ML {*
-fun repabs_goal lthy thm rty quot_thm reflex_thm trans_thm rsp_thms qtrm =
-  let
-    val rg = Syntax.check_term lthy (mk_inj_REPABS_goal lthy ((prop_of thm), qtrm));
-    fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN'
-      (REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms));
-    val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1);
-  in
-    @{thm Pure.equal_elim_rule1} OF [cthm, thm]
-  end
-*}
-
-ML {*
-fun lift_thm_goal lthy qty qty_name rsp_thms defs rthm goal =
-let
-  val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty;
-  val (trans2, reps_same, absrep, quot) = lookup_quot_thms lthy qty_name;
-  val t_a = atomize_thm rthm;
-  val goal_a = atomize_goal (ProofContext.theory_of lthy) goal;
-  val t_r = regularize_goal lthy t_a rel_eqv rel_refl goal_a;
-  val t_t = repabs_goal lthy t_r rty quot rel_refl trans2 rsp_thms goal_a;
-  val (alls, exs) = findallex lthy rty qty (prop_of t_a);
-  val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls
-  val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs
-  val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t
-  val abs = findabs rty (prop_of t_a);
-  val aps = findaps rty (prop_of t_a);
-  val app_prs_thms = map (applic_prs lthy rty qty absrep) aps;
-  val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs;
-  val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a;
-  val defs_sym = flat (map (add_lower_defs lthy) defs);
-  val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym;
-  val t_id = simp_ids lthy t_l;
-  val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_id;
-  val t_d = repeat_eqsubst_thm lthy defs_sym t_d0;
-  val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d;
-  val t_rv = ObjectLogic.rulify t_r
-in
-  Thm.varifyT t_rv
-end
-*}
-
-ML {*
-fun lift_thm_goal_note lthy qty qty_name rsp_thms defs thm name goal =
-  let
-    val lifted_thm = lift_thm_goal lthy qty qty_name rsp_thms defs thm goal;
-    val (_, lthy2) = note (name, lifted_thm) lthy;
-  in
-    lthy2
-  end
-*}
-
-ML {*
 fun inst_spec ctrm =
 let
    val cty = ctyp_of_term ctrm




