# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1259146736 -3600
# Node ID 991db758a72d269ae0a8666cf04058d049b36d93
# Parent  57bde65f6eb23c0bb750339190ff2c1394c465c1
More moving from QuotMain to UnusedQuotMain

diff -r 57bde65f6eb2 -r 991db758a72d QuotMain.thy
--- a/QuotMain.thy	Wed Nov 25 11:41:42 2009 +0100
+++ b/QuotMain.thy	Wed Nov 25 11:58:56 2009 +0100
@@ -158,14 +158,21 @@
 (* lifting of constants *)
 use "quotient_def.ML"
 
+(* TODO: Consider defining it with an "if"; sth like:
+   Babs p m = \<lambda>x. if x \<in> p then m x else undefined
+*)
+definition
+  Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
+where
+  "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
 
 
 section {* ATOMIZE *}
 
-lemma atomize_eqv[atomize]: 
-  shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)" 
+lemma atomize_eqv[atomize]:
+  shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
 proof
-  assume "A \<equiv> B" 
+  assume "A \<equiv> B"
   then show "Trueprop A \<equiv> Trueprop B" by unfold
 next
   assume *: "Trueprop A \<equiv> Trueprop B"
@@ -194,97 +201,9 @@
 
 ML {* atomize_thm @{thm list.induct} *}
 
-section {* REGULARIZE *}
-(*
-
-Regularizing a theorem 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
-
-Regularizing is done in 3 phases:
- - First a regularized term is created
- - Next we prove that the original theorem implies the new one
- - Finally using MP we get the new theorem.
-
-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
-
-*)
-
-definition
-  Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
-where
-  "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
-(* TODO: Consider defining it with an "if"; sth like:
-   Babs p m = \<lambda>x. if x \<in> p then m x else undefined
-*)
-
-ML {*
-fun needs_lift (rty as Type (rty_s, _)) ty =
-  case ty of
-    Type (s, tys) =>
-      (s = rty_s) orelse (exists (needs_lift rty) tys)
-  | _ => false
-
-*}
-
-
-lemma universal_twice:
-  assumes *: "\<And>x. (P x \<longrightarrow> Q x)"
-  shows "(\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x)"
-using * by auto
-
-lemma implication_twice:
-  assumes a: "c \<longrightarrow> a"
-  assumes b: "a \<Longrightarrow> b \<longrightarrow> d"
-  shows "(a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
-using a b by auto
-
 section {* RepAbs injection *}
 (*
 
-RepAbs injection is done in the following phases:
- 1) build_repabs_term inserts rep-abs pairs in the term
- 2) we prove the equality between the original theorem and this one
- 3) we use Pure.equal_elim_rule1 to get the new theorem.
-
-build_repabs_term does:
-
-  For abstractions:
-  * If the type of the abstraction doesn't need lifting we recurse.
-  * If it does we add RepAbs around the whole term and check if the
-    variable needs lifting.
-    * If it doesn't then we recurse
-    * If it does we recurse and put 'RepAbs' around all occurences
-      of the variable in the obtained subterm. This in combination
-      with the RepAbs above will let us change the type of the
-      abstraction with rewriting.
-  For applications:
-  * If the term is 'Respects' applied to anything we leave it unchanged
-  * If the term needs lifting and the head is a constant that we know
-    how to lift, we put a RepAbs and recurse
-  * If the term needs lifting and the head is a free applied to subterms
-    (if it is not applied we treated it in Abs branch) then we
-    put RepAbs and recurse
-  * Otherwise just recurse.
-
-
 To prove that the old theorem implies the new one, we first
 atomize it and then try:
 
@@ -308,6 +227,212 @@
 *)
 
 
+
+(* Need to have a meta-equality *)
+lemma id_def_sym: "(\<lambda>x. x) \<equiv> id"
+by (simp add: id_def)
+(* TODO: can be also obtained with: *)
+ML {* symmetric (eq_reflection OF @{thms id_def}) *}
+
+ML {*
+fun instantiate_tac thm = Subgoal.FOCUS (fn {concl, ...} =>
+  let
+    val pat = Drule.strip_imp_concl (cprop_of thm)
+    val insts = Thm.match (pat, concl)
+  in
+    rtac (Drule.instantiate insts thm) 1
+  end
+  handle _ => no_tac)
+*}
+
+ML {*
+fun CHANGED' tac = (fn i => CHANGED (tac i))
+*}
+
+lemma prod_fun_id: "prod_fun id id \<equiv> id"
+by (rule eq_reflection) (simp add: prod_fun_def)
+
+lemma map_id: "map id \<equiv> id"
+apply (rule eq_reflection)
+apply (rule ext)
+apply (rule_tac list="x" in list.induct)
+apply (simp_all)
+done
+
+ML {*
+fun quotient_tac quot_thm =
+  REPEAT_ALL_NEW (FIRST' [
+    rtac @{thm FUN_QUOTIENT},
+    rtac quot_thm,
+    rtac @{thm IDENTITY_QUOTIENT},
+    (* For functional identity quotients, (op = ---> op =) *)
+    CHANGED' (
+      (simp_tac (HOL_ss addsimps @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id}
+      )))
+  ])
+*}
+
+ML {*
+fun LAMBDA_RES_TAC ctxt i st =
+  (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
+    (_ $ (_ $ (Abs(_, _, _)) $ (Abs(_, _, _)))) =>
+      (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
+      (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
+  | _ => fn _ => no_tac) i st
+*}
+
+ML {*
+fun WEAK_LAMBDA_RES_TAC ctxt i st =
+  (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
+    (_ $ (_ $ _ $ (Abs(_, _, _)))) =>
+      (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
+      (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
+  | (_ $ (_ $ (Abs(_, _, _)) $ _)) =>
+      (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
+      (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
+  | _ => fn _ => no_tac) i st
+*}
+
+ML {* (* Legacy *)
+fun needs_lift (rty as Type (rty_s, _)) ty =
+  case ty of
+    Type (s, tys) =>
+      (s = rty_s) orelse (exists (needs_lift rty) tys)
+  | _ => false
+
+*}
+
+ML {*
+fun APPLY_RSP_TAC rty = Subgoal.FOCUS (fn {concl, ...} =>
+  let
+    val (_ $ (R $ (f $ _) $ (_ $ _))) = term_of concl;
+    val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP});
+    val insts = Thm.match (pat, concl)
+  in
+    if needs_lift rty (type_of f) then
+      rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1
+    else no_tac
+  end
+  handle _ => no_tac)
+*}
+
+ML {*
+val ball_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
+  let
+    val _ $ (_ $ (Const (@{const_name Ball}, _) $ _) $
+                 (Const (@{const_name Ball}, _) $ _)) = term_of concl
+  in
+    ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))
+    THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
+    THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN'
+    (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1
+  end
+  handle _ => no_tac)
+*}
+
+ML {*
+val bex_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
+  let
+    val _ $ (_ $ (Const (@{const_name Bex}, _) $ _) $
+                 (Const (@{const_name Bex}, _) $ _)) = term_of concl
+  in
+    ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))
+    THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
+    THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN'
+    (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1
+  end
+  handle _ => no_tac)
+*}
+
+ML {*
+fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
+*}
+
+ML {*
+fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms =
+  (FIRST' [
+    rtac trans_thm,
+    LAMBDA_RES_TAC ctxt,
+    ball_rsp_tac ctxt,
+    bex_rsp_tac ctxt,
+    FIRST' (map rtac rsp_thms),
+    rtac refl,
+    (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [SOLVES' (quotient_tac quot_thm)])),
+    (APPLY_RSP_TAC rty ctxt THEN' (RANGE [SOLVES' (quotient_tac quot_thm), SOLVES' (quotient_tac quot_thm)])),
+    Cong_Tac.cong_tac @{thm cong},
+    rtac @{thm ext},
+    rtac reflex_thm,
+    atac,
+    SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})),
+    WEAK_LAMBDA_RES_TAC ctxt,
+    CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))
+    ])
+*}
+
+section {* Cleaning the goal *}
+
+
+ML {*
+fun simp_ids lthy thm =
+  MetaSimplifier.rewrite_rule @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id} thm
+*}
+
+text {* Does the same as 'subst' in a given prop or theorem *}
+
+ML {*
+fun eqsubst_thm ctxt thms thm =
+  let
+    val goalstate = Goal.init (Thm.cprop_of thm)
+    val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of
+      NONE => error "eqsubst_thm"
+    | SOME th => cprem_of th 1
+    val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1
+    val goal = Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a');
+    val cgoal = cterm_of (ProofContext.theory_of ctxt) goal
+    val rt = Goal.prove_internal [] cgoal (fn _ => tac);
+  in
+    @{thm Pure.equal_elim_rule1} OF [rt, thm]
+  end
+*}
+
+text {* expects atomized definition *}
+ML {*
+fun add_lower_defs_aux lthy thm =
+  let
+    val e1 = @{thm fun_cong} OF [thm];
+    val f = eqsubst_thm lthy @{thms fun_map.simps} e1;
+    val g = simp_ids lthy f
+  in
+    (simp_ids lthy thm) :: (add_lower_defs_aux lthy g)
+  end
+  handle _ => [simp_ids lthy thm]
+*}
+
+ML {*
+fun add_lower_defs lthy def =
+  let
+    val def_pre_sym = symmetric def
+    val def_atom = atomize_thm def_pre_sym
+    val defs_all = add_lower_defs_aux lthy def_atom
+  in
+    map Thm.varifyT defs_all
+  end
+*}
+
+ML {*
+fun findaps_all rty tm =
+  case tm of
+    Abs(_, T, b) =>
+      findaps_all rty (subst_bound ((Free ("x", T)), b))
+  | (f $ a) => (findaps_all rty f @ findaps_all rty a)
+  | Free (_, (T as (Type ("fun", (_ :: _))))) =>
+      (if needs_lift rty T then [T] else [])
+  | _ => [];
+fun findaps rty tm = distinct (op =) (findaps_all rty tm)
+*}
+
+
+
 (* changes (?'a ?'b raw) (?'a ?'b quo) (int 'b raw \<Rightarrow> bool) to (int 'b quo \<Rightarrow> bool) *)
 ML {*
 fun exchange_ty lthy rty qty ty =
@@ -395,232 +520,6 @@
   end
 *}
 
-text {* Does the same as 'subst' in a given prop or theorem *}
-ML {*
-fun eqsubst_prop ctxt thms t =
-  let
-    val goalstate = Goal.init (cterm_of (ProofContext.theory_of ctxt) t)
-    val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of
-      NONE => error "eqsubst_prop"
-    | SOME th => cprem_of th 1
-  in term_of a' end
-*}
-
-ML {*
-  fun repeat_eqsubst_prop ctxt thms t =
-    repeat_eqsubst_prop ctxt thms (eqsubst_prop ctxt thms t)
-    handle _ => t
-*}
-
-
-ML {*
-fun eqsubst_thm ctxt thms thm =
-  let
-    val goalstate = Goal.init (Thm.cprop_of thm)
-    val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of
-      NONE => error "eqsubst_thm"
-    | SOME th => cprem_of th 1
-    val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1
-    val goal = Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a');
-    val cgoal = cterm_of (ProofContext.theory_of ctxt) goal
-    val rt = Goal.prove_internal [] cgoal (fn _ => tac);
-  in
-    @{thm Pure.equal_elim_rule1} OF [rt, thm]
-  end
-*}
-
-ML {*
-  fun repeat_eqsubst_thm ctxt thms thm =
-    repeat_eqsubst_thm ctxt thms (eqsubst_thm ctxt thms thm)
-    handle _ => thm
-*}
-
-(* Needed to have a meta-equality *)
-lemma id_def_sym: "(\<lambda>x. x) \<equiv> id"
-by (simp add: id_def)
-
-(* TODO: can be also obtained with: *)
-ML {* symmetric (eq_reflection OF @{thms id_def}) *}
-
-ML {*
-fun instantiate_tac thm = Subgoal.FOCUS (fn {concl, ...} =>
-  let
-    val pat = Drule.strip_imp_concl (cprop_of thm)
-    val insts = Thm.match (pat, concl)
-  in
-    rtac (Drule.instantiate insts thm) 1
-  end
-  handle _ => no_tac)
-*}
-
-ML {*
-fun CHANGED' tac = (fn i => CHANGED (tac i))
-*}
-
-lemma prod_fun_id: "prod_fun id id \<equiv> id"
-by (rule eq_reflection) (simp add: prod_fun_def)
-
-lemma map_id: "map id \<equiv> id"
-apply (rule eq_reflection)
-apply (rule ext)
-apply (rule_tac list="x" in list.induct)
-apply (simp_all)
-done
-
-ML {*
-fun quotient_tac quot_thm =
-  REPEAT_ALL_NEW (FIRST' [
-    rtac @{thm FUN_QUOTIENT},
-    rtac quot_thm,
-    rtac @{thm IDENTITY_QUOTIENT},
-    (* For functional identity quotients, (op = ---> op =) *)
-    CHANGED' (
-      (simp_tac (HOL_ss addsimps @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id}
-      )))
-  ])
-*}
-
-ML {*
-fun LAMBDA_RES_TAC ctxt i st =
-  (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
-    (_ $ (_ $ (Abs(_, _, _)) $ (Abs(_, _, _)))) =>
-      (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
-      (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
-  | _ => fn _ => no_tac) i st
-*}
-
-ML {*
-fun WEAK_LAMBDA_RES_TAC ctxt i st =
-  (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
-    (_ $ (_ $ _ $ (Abs(_, _, _)))) =>
-      (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
-      (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
-  | (_ $ (_ $ (Abs(_, _, _)) $ _)) =>
-      (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
-      (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
-  | _ => fn _ => no_tac) i st
-*}
-
-ML {*
-fun APPLY_RSP_TAC rty = Subgoal.FOCUS (fn {concl, ...} =>
-  let
-    val (_ $ (R $ (f $ _) $ (_ $ _))) = term_of concl;
-    val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP});
-    val insts = Thm.match (pat, concl)
-  in
-    if needs_lift rty (type_of f) then
-      rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1
-    else no_tac
-  end
-  handle _ => no_tac)
-*}
-
-ML {*
-val ball_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
-  let
-    val _ $ (_ $ (Const (@{const_name Ball}, _) $ _) $
-                 (Const (@{const_name Ball}, _) $ _)) = term_of concl
-  in
-    ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))
-    THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
-    THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN'
-    (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1
-  end
-  handle _ => no_tac)
-*}
-
-ML {*
-val bex_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
-  let
-    val _ $ (_ $ (Const (@{const_name Bex}, _) $ _) $
-                 (Const (@{const_name Bex}, _) $ _)) = term_of concl
-  in
-    ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))
-    THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI}
-    THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN'
-    (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1
-  end
-  handle _ => no_tac)
-*}
-
-ML {*
-fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
-*}
-
-ML {*
-fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms =
-  (FIRST' [
-    rtac trans_thm,
-    LAMBDA_RES_TAC ctxt,
-    ball_rsp_tac ctxt,
-    bex_rsp_tac ctxt,
-    FIRST' (map rtac rsp_thms),
-    rtac refl,
-    (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [SOLVES' (quotient_tac quot_thm)])),
-    (APPLY_RSP_TAC rty ctxt THEN' (RANGE [SOLVES' (quotient_tac quot_thm), SOLVES' (quotient_tac quot_thm)])),
-    Cong_Tac.cong_tac @{thm cong},
-    rtac @{thm ext},
-    rtac reflex_thm,
-    atac,
-    SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})),
-    WEAK_LAMBDA_RES_TAC ctxt,
-    CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))
-    ])
-*}
-
-section {* Cleaning the goal *}
-
-
-ML {*
-fun simp_ids lthy thm =
-  MetaSimplifier.rewrite_rule @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id} thm
-*}
-
-ML {*
-fun simp_ids_trm trm =
-  trm |>
-  MetaSimplifier.rewrite false @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id}
-  |> cprop_of |> Thm.dest_equals |> snd
-
-*}
-
-text {* expects atomized definition *}
-ML {*
-fun add_lower_defs_aux lthy thm =
-  let
-    val e1 = @{thm fun_cong} OF [thm];
-    val f = eqsubst_thm lthy @{thms fun_map.simps} e1;
-    val g = simp_ids lthy f
-  in
-    (simp_ids lthy thm) :: (add_lower_defs_aux lthy g)
-  end
-  handle _ => [simp_ids lthy thm]
-*}
-
-ML {*
-fun add_lower_defs lthy def =
-  let
-    val def_pre_sym = symmetric def
-    val def_atom = atomize_thm def_pre_sym
-    val defs_all = add_lower_defs_aux lthy def_atom
-  in
-    map Thm.varifyT defs_all
-  end
-*}
-
-ML {*
-fun findaps_all rty tm =
-  case tm of
-    Abs(_, T, b) =>
-      findaps_all rty (subst_bound ((Free ("x", T)), b))
-  | (f $ a) => (findaps_all rty f @ findaps_all rty a)
-  | Free (_, (T as (Type ("fun", (_ :: _))))) =>
-      (if needs_lift rty T then [T] else [])
-  | _ => [];
-fun findaps rty tm = distinct (op =) (findaps_all rty tm)
-*}
-
-
 ML {*
 fun applic_prs lthy rty qty absrep ty =
   let
@@ -703,24 +602,6 @@
 (******************************************)
 (******************************************)
 
-ML {*
-fun atomize_goal thy gl =
-  let
-    val vars = map Free (Term.add_frees gl []);
-    val all = if fastype_of gl = @{typ bool} then HOLogic.all_const else Term.all;
-    fun lambda_all (var as Free(_, T)) trm = (all T) $ lambda var trm;
-    val glv = fold lambda_all vars gl
-    val gla = (term_of o snd o Thm.dest_equals o cprop_of) (ObjectLogic.atomize (cterm_of thy glv))
-    val glf = Type.legacy_freeze gla
-  in
-    if fastype_of gl = @{typ bool} then @{term Trueprop} $ glf else glf
-  end
-*}
-
-
-ML {* atomize_goal @{theory} @{term "x memb [] = False"} *}
-ML {* atomize_goal @{theory} @{term "x = xa \<Longrightarrow> a # x = a # xa"} *}
-
 
 ML {*
 (* builds the relation for respects *)
@@ -901,6 +782,17 @@
 apply(rule b)
 done
 
+lemma universal_twice:
+  assumes *: "\<And>x. (P x \<longrightarrow> Q x)"
+  shows "(\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x)"
+using * by auto
+
+lemma implication_twice:
+  assumes a: "c \<longrightarrow> a"
+  assumes b: "a \<Longrightarrow> b \<longrightarrow> d"
+  shows "(a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
+using a b by auto
+
 ML {*
 (* FIXME: get_rid of rel_refl rel_eqv *)
 fun REGULARIZE_tac lthy rel_refl rel_eqv =
@@ -958,6 +850,28 @@
   end
 *}
 
+(*
+Injecting REPABS means:
+
+  For abstractions:
+  * If the type of the abstraction doesn't need lifting we recurse.
+  * If it does we add RepAbs around the whole term and check if the
+    variable needs lifting.
+    * If it doesn't then we recurse
+    * If it does we recurse and put 'RepAbs' around all occurences
+      of the variable in the obtained subterm. This in combination
+      with the RepAbs above will let us change the type of the
+      abstraction with rewriting.
+  For applications:
+  * If the term is 'Respects' applied to anything we leave it unchanged
+  * If the term needs lifting and the head is a constant that we know
+    how to lift, we put a RepAbs and recurse
+  * If the term needs lifting and the head is a free applied to subterms
+    (if it is not applied we treated it in Abs branch) then we
+    put RepAbs and recurse
+  * Otherwise just recurse.
+*)
+
 (* rep-abs injection *)
 
 ML {*
@@ -1031,7 +945,18 @@
   Logic.mk_equals (rtrm, Syntax.check_term lthy (inj_REPABS lthy (rtrm, qtrm)))
 *}
 
-(* Final wrappers *)
+
+
+(*
+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
+*)
 
 ML {*
 fun regularize_tac ctxt rel_eqv rel_refl =
diff -r 57bde65f6eb2 -r 991db758a72d UnusedQuotMain.thy
--- a/UnusedQuotMain.thy	Wed Nov 25 11:41:42 2009 +0100
+++ b/UnusedQuotMain.thy	Wed Nov 25 11:58:56 2009 +0100
@@ -1,3 +1,26 @@
+ML {*
+fun repeat_eqsubst_thm ctxt thms thm =
+  repeat_eqsubst_thm ctxt thms (eqsubst_thm ctxt thms thm)
+  handle _ => thm
+*}
+
+
+ML {*
+fun eqsubst_prop ctxt thms t =
+  let
+    val goalstate = Goal.init (cterm_of (ProofContext.theory_of ctxt) t)
+    val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of
+      NONE => error "eqsubst_prop"
+    | SOME th => cprem_of th 1
+  in term_of a' end
+*}
+
+ML {*
+  fun repeat_eqsubst_prop ctxt thms t =
+    repeat_eqsubst_prop ctxt thms (eqsubst_prop ctxt thms t)
+    handle _ => t
+*}
+
 
 text {* tyRel takes a type and builds a relation that a quantifier over this
   type needs to respect. *}
@@ -444,6 +467,27 @@
   end
 *}
 
+
+ML {*
+fun atomize_goal thy gl =
+  let
+    val vars = map Free (Term.add_frees gl []);
+    val all = if fastype_of gl = @{typ bool} then HOLogic.all_const else Term.all;
+    fun lambda_all (var as Free(_, T)) trm = (all T) $ lambda var trm;
+    val glv = fold lambda_all vars gl
+    val gla = (term_of o snd o Thm.dest_equals o cprop_of) (ObjectLogic.atomize (cterm_of thy glv))
+    val glf = Type.legacy_freeze gla
+  in
+    if fastype_of gl = @{typ bool} then @{term Trueprop} $ glf else glf
+  end
+*}
+
+
+ML {* atomize_goal @{theory} @{term "x memb [] = False"} *}
+ML {* atomize_goal @{theory} @{term "x = xa ⟹ a # x = a # xa"} *}
+
+
+
 ML {*
 fun lift_thm_goal lthy qty qty_name rsp_thms defs rthm goal =
 let
@@ -484,3 +528,10 @@
   end
 *}
 
+ML {*
+fun simp_ids_trm trm =
+  trm |>
+  MetaSimplifier.rewrite false @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id}
+  |> cprop_of |> Thm.dest_equals |> snd
+
+*}