src/HOL/Tools/Meson/meson.ML
changeset 42346 be52d9bed9f6
parent 42335 cb8aa792d138
child 42361 23f352990944
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Thu Apr 14 11:24:05 2011 +0200
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Thu Apr 14 11:24:05 2011 +0200
     1.3 @@ -14,7 +14,6 @@
     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 @@ -394,48 +393,6 @@
    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