experiment with definitional CNF
authorblanchet
Thu Apr 14 11:24:04 2011 +0200 (2011-04-14)
changeset 42335cb8aa792d138
parent 42334 8e58cc1390c7
child 42336 d63d43e85879
experiment with definitional CNF
src/HOL/Tools/Meson/meson.ML
src/HOL/Tools/Meson/meson_clausify.ML
src/HOL/Tools/cnf_funcs.ML
     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  
     2.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Thu Apr 14 11:24:04 2011 +0200
     2.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Thu Apr 14 11:24:04 2011 +0200
     2.3 @@ -13,7 +13,7 @@
     2.4    val extensionalize_theorem : thm -> thm
     2.5    val introduce_combinators_in_cterm : cterm -> thm
     2.6    val introduce_combinators_in_theorem : thm -> thm
     2.7 -  val to_definitional_cnf_with_quantifiers : theory -> thm -> thm
     2.8 +  val to_definitional_cnf_with_quantifiers : Proof.context -> thm -> thm
     2.9    val cluster_of_zapped_var_name : string -> (int * (int * int)) * bool
    2.10    val cnf_axiom :
    2.11      Proof.context -> bool -> int -> thm -> (thm * term) option * thm list
    2.12 @@ -229,9 +229,9 @@
    2.13      |> Thm.varifyT_global
    2.14    end
    2.15  
    2.16 -fun to_definitional_cnf_with_quantifiers thy th =
    2.17 +fun to_definitional_cnf_with_quantifiers ctxt th =
    2.18    let
    2.19 -    val eqth = cnf.make_cnfx_thm thy (HOLogic.dest_Trueprop (prop_of th))
    2.20 +    val eqth = cnf.make_cnfx_thm ctxt (HOLogic.dest_Trueprop (prop_of th))
    2.21      val eqth = eqth RS @{thm eq_reflection}
    2.22      val eqth = eqth RS @{thm TruepropI}
    2.23    in Thm.equal_elim eqth th end
    2.24 @@ -341,8 +341,8 @@
    2.25                  cterm_of thy)
    2.26            |> zap true
    2.27          val fixes =
    2.28 -          Term.add_free_names (prop_of zapped_th) []
    2.29 -          |> filter is_zapped_var_name
    2.30 +          [] |> Term.add_free_names (prop_of zapped_th)
    2.31 +             |> filter is_zapped_var_name
    2.32          val ctxt' = ctxt |> Variable.add_fixes_direct fixes
    2.33          val fully_skolemized_t =
    2.34            zapped_th |> singleton (Variable.export ctxt' ctxt)
    2.35 @@ -366,6 +366,58 @@
    2.36        (NONE, (th, ctxt))
    2.37    end
    2.38  
    2.39 +val all_out_ss =
    2.40 +  Simplifier.clear_ss HOL_basic_ss addsimps @{thms all_simps[symmetric]}
    2.41 +
    2.42 +val meta_allI = @{lemma "ALL x. P x ==> (!!x. P x)" by auto}
    2.43 +
    2.44 +fun repeat f x =
    2.45 +  case try f x of
    2.46 +    SOME y => repeat f y
    2.47 +  | NONE => x
    2.48 +
    2.49 +fun close_thm thy th =
    2.50 +  fold (Thm.forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of th) []) th
    2.51 +
    2.52 +fun cnf_axiom_xxx ctxt0 new_skolemizer ax_no th =
    2.53 +  let
    2.54 +    val ctxt0 = Variable.global_thm_context th
    2.55 +    val thy = ProofContext.theory_of ctxt0
    2.56 +    val choice_ths = choice_theorems thy
    2.57 +    val (opt, (nnf_th, ctxt)) =
    2.58 +      nnf_axiom choice_ths new_skolemizer ax_no th ctxt0
    2.59 +    val skolem_ths = map (old_skolem_theorem_from_def thy) o old_skolem_defs
    2.60 +    fun make_cnf th = Meson.make_cnf (skolem_ths th) th
    2.61 +    val (cnf_ths, ctxt) =
    2.62 +       make_cnf nnf_th ctxt
    2.63 +       |> (fn (cnf, _) =>
    2.64 +              let
    2.65 +                val _ = tracing ("nondef CNF: " ^ string_of_int (length cnf) ^ " clause(s)")
    2.66 +                val sko_th =
    2.67 +                  nnf_th |> Simplifier.simplify all_out_ss
    2.68 +                         |> repeat (fn th => th RS meta_allI)
    2.69 +                         |> Meson.make_xxx_skolem ctxt (skolem_ths nnf_th)
    2.70 +                         |> close_thm thy
    2.71 +                         |> Conv.fconv_rule Object_Logic.atomize
    2.72 +                         |> to_definitional_cnf_with_quantifiers ctxt
    2.73 +              in make_cnf sko_th ctxt end
    2.74 +           | p => p)
    2.75 +    fun intr_imp ct th =
    2.76 +      Thm.instantiate ([], map (pairself (cterm_of thy))
    2.77 +                               [(Var (("i", 0), @{typ nat}),
    2.78 +                                 HOLogic.mk_nat ax_no)])
    2.79 +                      (zero_var_indexes @{thm skolem_COMBK_D})
    2.80 +      RS Thm.implies_intr ct th
    2.81 +  in
    2.82 +    (NONE (*###*),
    2.83 +     cnf_ths |> map (introduce_combinators_in_theorem
    2.84 +                     #> (case opt of SOME (_, ct) => intr_imp ct | NONE => I))
    2.85 +             |> Variable.export ctxt ctxt0
    2.86 +             |> finish_cnf
    2.87 +             |> map Thm.close_derivation)
    2.88 +  end
    2.89 +
    2.90 +
    2.91  (* Convert a theorem to CNF, with additional premises due to skolemization. *)
    2.92  fun cnf_axiom ctxt0 new_skolemizer ax_no th =
    2.93    let
    2.94 @@ -382,8 +434,23 @@
    2.95      val (cnf_ths, ctxt) =
    2.96        clausify nnf_th
    2.97        |> (fn ([], _) =>
    2.98 -             (* FIXME: This probably doesn't work with the new Skolemizer *)
    2.99 -             clausify (to_definitional_cnf_with_quantifiers thy nnf_th)
   2.100 +             if new_skolemizer then
   2.101 +               let
   2.102 +val _ = tracing ("**** NEW CLAUSIFIER, DEF-CNF: " ^ Display.string_of_thm ctxt (to_definitional_cnf_with_quantifiers ctxt nnf_th)) (*###*)
   2.103 +val _ = tracing (" *** th: " ^ Display.string_of_thm ctxt th) (*###*)
   2.104 +                 val (_, (th1, ctxt)) = nnf_axiom choice_ths true ax_no th ctxt0
   2.105 +val _ = tracing (" *** th1: " ^ Display.string_of_thm ctxt th1) (*###*)
   2.106 +                 val th2 = to_definitional_cnf_with_quantifiers ctxt th1
   2.107 +val _ = tracing (" *** th2: " ^ Display.string_of_thm ctxt th2) (*###*)
   2.108 +                 val (ths3, ctxt) = clausify th2
   2.109 +val _ = tracing (" *** hd ths3: " ^ Display.string_of_thm ctxt (hd ths3)) (*###*)
   2.110 +               in (ths3, ctxt) end
   2.111 +             else
   2.112 +let
   2.113 +val _ = tracing ("**** OLD CLAUSIFIER, DEF-CNF: " ^ Display.string_of_thm ctxt (to_definitional_cnf_with_quantifiers ctxt nnf_th))
   2.114 +(*###*) in
   2.115 +               clausify (to_definitional_cnf_with_quantifiers ctxt nnf_th)
   2.116 +end
   2.117             | p => p)
   2.118      fun intr_imp ct th =
   2.119        Thm.instantiate ([], map (pairself (cterm_of thy))
     3.1 --- a/src/HOL/Tools/cnf_funcs.ML	Thu Apr 14 11:24:04 2011 +0200
     3.2 +++ b/src/HOL/Tools/cnf_funcs.ML	Thu Apr 14 11:24:04 2011 +0200
     3.3 @@ -40,11 +40,12 @@
     3.4    val clause_is_trivial: term -> bool
     3.5  
     3.6    val clause2raw_thm: thm -> thm
     3.7 +  val make_nnf_thm: theory -> term -> thm
     3.8  
     3.9    val weakening_tac: int -> tactic  (* removes the first hypothesis of a subgoal *)
    3.10  
    3.11 -  val make_cnf_thm: theory -> term -> thm
    3.12 -  val make_cnfx_thm: theory -> term -> thm
    3.13 +  val make_cnf_thm: Proof.context -> term -> thm
    3.14 +  val make_cnfx_thm: Proof.context -> term -> thm
    3.15    val cnf_rewrite_tac: Proof.context -> int -> tactic  (* converts all prems of a subgoal to CNF *)
    3.16    val cnfx_rewrite_tac: Proof.context -> int -> tactic
    3.17      (* converts all prems of a subgoal to (almost) definitional CNF *)
    3.18 @@ -252,6 +253,24 @@
    3.19        end
    3.20    | make_nnf_thm thy t = inst_thm thy [t] iff_refl;
    3.21  
    3.22 +val meta_eq_to_obj_eq = @{thm meta_eq_to_obj_eq}
    3.23 +val eq_reflection = @{thm eq_reflection}
    3.24 +
    3.25 +fun make_under_quantifiers ctxt make t =
    3.26 +  let
    3.27 +    val thy = ProofContext.theory_of ctxt
    3.28 +    fun conv ctxt ct =
    3.29 +      case term_of ct of
    3.30 +        (t1 as Const _) $ (t2 as Abs _) =>
    3.31 +        Conv.comb_conv (conv ctxt) ct
    3.32 +      | Abs _ => Conv.abs_conv (conv o snd) ctxt ct
    3.33 +      | Const _ => Conv.all_conv ct
    3.34 +      | t => make t RS eq_reflection
    3.35 +  in conv ctxt (cterm_of thy t) RS meta_eq_to_obj_eq end
    3.36 +
    3.37 +fun make_nnf_thm_under_quantifiers ctxt =
    3.38 +  make_under_quantifiers ctxt (make_nnf_thm (ProofContext.theory_of ctxt))
    3.39 +
    3.40  (* ------------------------------------------------------------------------- *)
    3.41  (* simp_True_False_thm: produces a theorem t = t', where t' is equivalent to *)
    3.42  (*      t, but simplified wrt. the following theorems:                       *)
    3.43 @@ -323,8 +342,9 @@
    3.44  (*      in the length of the term.                                           *)
    3.45  (* ------------------------------------------------------------------------- *)
    3.46  
    3.47 -fun make_cnf_thm thy t =
    3.48 +fun make_cnf_thm ctxt t =
    3.49    let
    3.50 +    val thy = ProofContext.theory_of ctxt
    3.51      fun make_cnf_thm_from_nnf (Const (@{const_name HOL.conj}, _) $ x $ y) =
    3.52            let
    3.53              val thm1 = make_cnf_thm_from_nnf x
    3.54 @@ -361,13 +381,19 @@
    3.55            end
    3.56        | make_cnf_thm_from_nnf t = inst_thm thy [t] iff_refl
    3.57      (* convert 't' to NNF first *)
    3.58 +    val nnf_thm = make_nnf_thm_under_quantifiers ctxt t
    3.59 +(*###
    3.60      val nnf_thm = make_nnf_thm thy t
    3.61 +*)
    3.62      val nnf = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) nnf_thm
    3.63      (* then simplify wrt. True/False (this should preserve NNF) *)
    3.64      val simp_thm = simp_True_False_thm thy nnf
    3.65      val simp = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) simp_thm
    3.66      (* finally, convert to CNF (this should preserve the simplification) *)
    3.67 +    val cnf_thm = make_under_quantifiers ctxt make_cnf_thm_from_nnf simp
    3.68 +(* ###
    3.69      val cnf_thm = make_cnf_thm_from_nnf simp
    3.70 +*)
    3.71    in
    3.72      iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnf_thm]
    3.73    end;
    3.74 @@ -386,8 +412,9 @@
    3.75  (*      in the case of nested equivalences.                                  *)
    3.76  (* ------------------------------------------------------------------------- *)
    3.77  
    3.78 -fun make_cnfx_thm thy t =
    3.79 +fun make_cnfx_thm ctxt t =
    3.80    let
    3.81 +    val thy = ProofContext.theory_of ctxt
    3.82      val var_id = Unsynchronized.ref 0  (* properly initialized below *)
    3.83      fun new_free () =
    3.84        Free ("cnfx_" ^ string_of_int (Unsynchronized.inc var_id), HOLogic.boolT)
    3.85 @@ -465,7 +492,10 @@
    3.86              end
    3.87        | make_cnfx_thm_from_nnf t = inst_thm thy [t] iff_refl
    3.88      (* convert 't' to NNF first *)
    3.89 +    val nnf_thm = make_nnf_thm_under_quantifiers ctxt t
    3.90 +(* ###
    3.91      val nnf_thm = make_nnf_thm thy t
    3.92 +*)
    3.93      val nnf = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) nnf_thm
    3.94      (* then simplify wrt. True/False (this should preserve NNF) *)
    3.95      val simp_thm = simp_True_False_thm thy nnf
    3.96 @@ -483,7 +513,10 @@
    3.97          Int.max (max, the_default 0 idx)
    3.98        end) (OldTerm.term_frees simp) 0)
    3.99      (* finally, convert to definitional CNF (this should preserve the simplification) *)
   3.100 +    val cnfx_thm = make_under_quantifiers ctxt make_cnfx_thm_from_nnf simp
   3.101 +(*###
   3.102      val cnfx_thm = make_cnfx_thm_from_nnf simp
   3.103 +*)
   3.104    in
   3.105      iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnfx_thm]
   3.106    end;
   3.107 @@ -509,8 +542,7 @@
   3.108    (* cut the CNF formulas as new premises *)
   3.109    Subgoal.FOCUS (fn {prems, ...} =>
   3.110      let
   3.111 -      val thy = ProofContext.theory_of ctxt
   3.112 -      val cnf_thms = map (make_cnf_thm thy o HOLogic.dest_Trueprop o Thm.prop_of) prems
   3.113 +      val cnf_thms = map (make_cnf_thm ctxt o HOLogic.dest_Trueprop o Thm.prop_of) prems
   3.114        val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnf_thms ~~ prems)
   3.115      in
   3.116        cut_facts_tac cut_thms 1
   3.117 @@ -532,8 +564,7 @@
   3.118    (* cut the CNF formulas as new premises *)
   3.119    Subgoal.FOCUS (fn {prems, ...} =>
   3.120      let
   3.121 -      val thy = ProofContext.theory_of ctxt;
   3.122 -      val cnfx_thms = map (make_cnfx_thm thy o HOLogic.dest_Trueprop o prop_of) prems
   3.123 +      val cnfx_thms = map (make_cnfx_thm ctxt o HOLogic.dest_Trueprop o prop_of) prems
   3.124        val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnfx_thms ~~ prems)
   3.125      in
   3.126        cut_facts_tac cut_thms 1