--- a/src/HOL/Tools/Meson/meson.ML Thu Apr 14 11:24:04 2011 +0200
+++ b/src/HOL/Tools/Meson/meson.ML Thu Apr 14 11:24:04 2011 +0200
@@ -14,6 +14,7 @@
val size_of_subgoals: thm -> int
val has_too_many_clauses: Proof.context -> term -> bool
val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
+ val make_xxx_skolem: Proof.context -> thm list -> thm -> thm
val finish_cnf: thm list -> thm list
val presimplify: thm -> thm
val make_nnf: Proof.context -> thm -> thm
@@ -393,6 +394,48 @@
fun make_cnf old_skolem_ths th ctxt = cnf old_skolem_ths ctxt (th, [])
+val disj_imp_cong =
+ @{lemma "[| P --> P'; Q --> Q'; P | Q |] ==> P' | Q'" by auto}
+
+val impI = @{thm impI}
+
+(* ### *)
+(* Match untyped terms. *)
+fun untyped_aconv (Const (a, _)) (Const(b, _)) = (a = b)
+ | untyped_aconv (Free (a, _)) (Free (b, _)) = (a = b)
+ | untyped_aconv (Var ((a, _), _)) (Var ((b, _), _)) = true
+ | untyped_aconv (Free (a, _)) (Var ((b, _), _)) = true
+ | untyped_aconv (Var ((a, _), _)) (Free (b, _)) = true
+ | untyped_aconv (Bound i) (Bound j) = (i = j)
+ | untyped_aconv (Abs (_, _, t)) (Abs (_, _, u)) = untyped_aconv t u
+ | untyped_aconv (t1 $ t2) (u1 $ u2) =
+ untyped_aconv t1 u1 andalso untyped_aconv t2 u2
+ | untyped_aconv _ _ = false
+
+fun make_xxx_skolem ctxt skolem_ths th =
+ let
+ val thy = ProofContext.theory_of ctxt
+ fun do_connective fwd_thm t1 t2 =
+ do_formula t1
+ COMP rotate_prems 1 (do_formula t2 COMP (rotate_prems 2 fwd_thm))
+ and do_formula t =
+ case t of
+ @{const Trueprop} $ t' => do_formula t'
+ | @{const conj} $ t1 $ t2 => do_connective @{thm conj_forward} t1 t2
+ | @{const disj} $ t1 $ t2 => do_connective @{thm disj_forward} t1 t2
+ | Const (@{const_name Ex}, _) $ Abs _ =>
+ let
+ val th =
+ find_first (fn sko_th => (untyped_aconv (Logic.nth_prem (1, prop_of sko_th)) (HOLogic.mk_Trueprop t)))
+ skolem_ths |> the
+ in
+ th
+ RS
+ do_formula (Logic.strip_imp_concl (prop_of th))
+ end
+ | _ => Thm.trivial (cterm_of thy (HOLogic.mk_Trueprop t))
+ in th COMP do_formula (HOLogic.dest_Trueprop (prop_of th)) end
+
(*Generalization, removal of redundant equalities, removal of tautologies.*)
fun finish_cnf ths = filter (not o is_taut) (map refl_clause ths);