--- 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 =