1.1 --- a/src/HOL/Tools/Meson/meson.ML	Thu Apr 14 11:24:04 2011 +0200
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Thu Apr 14 11:24:04 2011 +0200
     1.3 @@ -14,6 +14,7 @@
     1.4    val size_of_subgoals: thm -> int
     1.5    val has_too_many_clauses: Proof.context -> term -> bool
     1.6    val make_cnf: thm list -> thm -> Proof.context -> thm list * Proof.context
     1.7 +  val make_xxx_skolem: Proof.context -> thm list -> thm -> thm
     1.8    val finish_cnf: thm list -> thm list
     1.9    val presimplify: thm -> thm
    1.10    val make_nnf: Proof.context -> thm -> thm
    1.11 @@ -393,6 +394,48 @@
    1.12  
    1.13  fun make_cnf old_skolem_ths th ctxt = cnf old_skolem_ths ctxt (th, [])
    1.14  
    1.15 +val disj_imp_cong =
    1.16 +  @{lemma "[| P --> P'; Q --> Q'; P | Q |] ==> P' | Q'" by auto}
    1.17 +
    1.18 +val impI = @{thm impI}
    1.19 +
    1.20 +(* ### *)
    1.21 +(* Match untyped terms. *)
    1.22 +fun untyped_aconv (Const (a, _)) (Const(b, _)) = (a = b)
    1.23 +  | untyped_aconv (Free (a, _)) (Free (b, _)) = (a = b)
    1.24 +  | untyped_aconv (Var ((a, _), _)) (Var ((b, _), _)) = true
    1.25 +  | untyped_aconv (Free (a, _)) (Var ((b, _), _)) = true
    1.26 +  | untyped_aconv (Var ((a, _), _)) (Free (b, _)) = true
    1.27 +  | untyped_aconv (Bound i) (Bound j) = (i = j)
    1.28 +  | untyped_aconv (Abs (_, _, t)) (Abs (_, _, u)) = untyped_aconv t u
    1.29 +  | untyped_aconv (t1 $ t2) (u1 $ u2) =
    1.30 +    untyped_aconv t1 u1 andalso untyped_aconv t2 u2
    1.31 +  | untyped_aconv _ _ = false
    1.32 +
    1.33 +fun make_xxx_skolem ctxt skolem_ths th =
    1.34 +  let
    1.35 +    val thy = ProofContext.theory_of ctxt
    1.36 +    fun do_connective fwd_thm t1 t2 =
    1.37 +      do_formula t1
    1.38 +      COMP rotate_prems 1 (do_formula t2 COMP (rotate_prems 2 fwd_thm))
    1.39 +    and do_formula t =
    1.40 +      case t of
    1.41 +        @{const Trueprop} $ t' => do_formula t'
    1.42 +      | @{const conj} $ t1 $ t2 => do_connective @{thm conj_forward} t1 t2
    1.43 +      | @{const disj} $ t1 $ t2 => do_connective @{thm disj_forward} t1 t2
    1.44 +      | Const (@{const_name Ex}, _) $ Abs _ =>
    1.45 +        let
    1.46 +          val th =
    1.47 +            find_first (fn sko_th => (untyped_aconv (Logic.nth_prem (1, prop_of sko_th)) (HOLogic.mk_Trueprop t)))
    1.48 +                       skolem_ths |> the
    1.49 +        in
    1.50 +          th
    1.51 +          RS
    1.52 +          do_formula (Logic.strip_imp_concl (prop_of th))
    1.53 +        end
    1.54 +      | _ => Thm.trivial (cterm_of thy (HOLogic.mk_Trueprop t))
    1.55 +  in th COMP do_formula (HOLogic.dest_Trueprop (prop_of th)) end
    1.56 +
    1.57  (*Generalization, removal of redundant equalities, removal of tautologies.*)
    1.58  fun finish_cnf ths = filter (not o is_taut) (map refl_clause ths);
    1.59