--- a/QuotMain.thy Tue Nov 03 14:04:45 2009 +0100
+++ b/QuotMain.thy Tue Nov 03 16:17:19 2009 +0100
@@ -538,12 +538,13 @@
*}
lemma universal_twice: "(\<And>x. (P x \<longrightarrow> Q x)) \<Longrightarrow> ((\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x))"
-apply (auto)
-done
+by auto
lemma implication_twice: "(c \<longrightarrow> a) \<Longrightarrow> (a \<Longrightarrow> b \<longrightarrow> d) \<Longrightarrow> (a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
-apply (auto)
-done
+by auto
+
+(*lemma equality_twice: "a = c \<Longrightarrow> b = d \<Longrightarrow> (a = b \<longrightarrow> c = d)"
+by auto*)
ML {*
fun regularize thm rty rel rel_eqv rel_refl lthy =
@@ -557,6 +558,7 @@
rtac @{thm universal_twice},
(rtac @{thm impI} THEN' atac),
rtac @{thm implication_twice},
+ (*rtac @{thm equality_twice},*)
EqSubst.eqsubst_tac ctxt [0]
[(@{thm equiv_res_forall} OF [rel_eqv]),
(@{thm equiv_res_exists} OF [rel_eqv])],
@@ -708,21 +710,6 @@
)
*}
-ML {*
-fun res_forall_rsp_tac ctxt =
- (simp_tac ((Simplifier.context ctxt 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 ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
-*}
-
-ML {*
-fun res_exists_rsp_tac ctxt =
- (simp_tac ((Simplifier.context ctxt 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 ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))
-*}
ML {*
@@ -770,6 +757,34 @@
*}
ML {*
+val res_forall_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
+ let
+ val _ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ (Const (@{const_name Ball}, _) $ _)) = term_of concl
+ in
+ ((simp_tac ((Simplifier.context ctxt 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 ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))) 1
+ end
+ handle _ => no_tac
+ )
+*}
+
+ML {*
+val res_exists_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
+ let
+ val _ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ (Const (@{const_name Bex}, _) $ _)) = term_of concl
+ in
+ ((simp_tac ((Simplifier.context ctxt 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 ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps}))) 1
+ end
+ handle _ => no_tac
+ )
+*}
+
+ML {*
fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms =
(FIRST' [
(* rtac @{thm FUN_QUOTIENT},
@@ -779,10 +794,7 @@
LAMBDA_RES_TAC ctxt,
res_forall_rsp_tac ctxt,
res_exists_rsp_tac ctxt,
- (
- (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps rsp_thms))
- THEN_ALL_NEW (fn _ => no_tac)
- ),
+ FIRST' (map rtac rsp_thms),
(instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),
rtac refl,
(* rtac @{thm arg_cong2[of _ _ _ _ "op ="]},*)
@@ -893,17 +905,63 @@
*}
ML {*
- fun simp_allex_prs quot thms thm =
+ 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 rty qty tm =
let
- val ts = [@{thm FORALL_PRS} OF [quot], @{thm EXISTS_PRS} OF [quot]] @ thms
- val sym_ts = map (fn x => @{thm "HOL.sym"} OF [x]) ts;
- val eq_ts = map (fn x => @{thm "eq_reflection"} OF [x]) sym_ts
+ 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)
in
- MetaSimplifier.rewrite_rule eq_ts thm
+ (map (old_exchange_ty rty qty) au, map (old_exchange_ty 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 lookup_quot_data lthy qty =
let
val SOME quotdata = find_first (fn x => matches ((#qtyp x), qty)) (quotdata_lookup lthy)
@@ -947,11 +1005,14 @@
val t_a = atomize_thm t;
val t_r = regularize t_a rty rel rel_eqv rel_refl lthy;
val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms;
+ val (alls, exs) = findallex 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 (make_simp_prs_thm lthy quot @{thm APP_PRS}) aps;
val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs;
- val t_a = simp_allex_prs quot [] t_t;
val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a;
val defs_sym = add_lower_defs lthy defs;
val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym;