--- 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);
--- a/src/HOL/Tools/Meson/meson_clausify.ML Thu Apr 14 11:24:04 2011 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Thu Apr 14 11:24:04 2011 +0200
@@ -13,7 +13,7 @@
val extensionalize_theorem : thm -> thm
val introduce_combinators_in_cterm : cterm -> thm
val introduce_combinators_in_theorem : thm -> thm
- val to_definitional_cnf_with_quantifiers : theory -> thm -> thm
+ val to_definitional_cnf_with_quantifiers : Proof.context -> thm -> thm
val cluster_of_zapped_var_name : string -> (int * (int * int)) * bool
val cnf_axiom :
Proof.context -> bool -> int -> thm -> (thm * term) option * thm list
@@ -229,9 +229,9 @@
|> Thm.varifyT_global
end
-fun to_definitional_cnf_with_quantifiers thy th =
+fun to_definitional_cnf_with_quantifiers ctxt th =
let
- val eqth = cnf.make_cnfx_thm thy (HOLogic.dest_Trueprop (prop_of th))
+ val eqth = cnf.make_cnfx_thm ctxt (HOLogic.dest_Trueprop (prop_of th))
val eqth = eqth RS @{thm eq_reflection}
val eqth = eqth RS @{thm TruepropI}
in Thm.equal_elim eqth th end
@@ -341,8 +341,8 @@
cterm_of thy)
|> zap true
val fixes =
- Term.add_free_names (prop_of zapped_th) []
- |> filter is_zapped_var_name
+ [] |> Term.add_free_names (prop_of zapped_th)
+ |> filter is_zapped_var_name
val ctxt' = ctxt |> Variable.add_fixes_direct fixes
val fully_skolemized_t =
zapped_th |> singleton (Variable.export ctxt' ctxt)
@@ -366,6 +366,58 @@
(NONE, (th, ctxt))
end
+val all_out_ss =
+ Simplifier.clear_ss HOL_basic_ss addsimps @{thms all_simps[symmetric]}
+
+val meta_allI = @{lemma "ALL x. P x ==> (!!x. P x)" by auto}
+
+fun repeat f x =
+ case try f x of
+ SOME y => repeat f y
+ | NONE => x
+
+fun close_thm thy th =
+ fold (Thm.forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of th) []) th
+
+fun cnf_axiom_xxx ctxt0 new_skolemizer ax_no th =
+ let
+ val ctxt0 = Variable.global_thm_context th
+ val thy = ProofContext.theory_of ctxt0
+ val choice_ths = choice_theorems thy
+ val (opt, (nnf_th, ctxt)) =
+ nnf_axiom choice_ths new_skolemizer ax_no th ctxt0
+ val skolem_ths = map (old_skolem_theorem_from_def thy) o old_skolem_defs
+ fun make_cnf th = Meson.make_cnf (skolem_ths th) th
+ val (cnf_ths, ctxt) =
+ make_cnf nnf_th ctxt
+ |> (fn (cnf, _) =>
+ let
+ val _ = tracing ("nondef CNF: " ^ string_of_int (length cnf) ^ " clause(s)")
+ val sko_th =
+ nnf_th |> Simplifier.simplify all_out_ss
+ |> repeat (fn th => th RS meta_allI)
+ |> Meson.make_xxx_skolem ctxt (skolem_ths nnf_th)
+ |> close_thm thy
+ |> Conv.fconv_rule Object_Logic.atomize
+ |> to_definitional_cnf_with_quantifiers ctxt
+ in make_cnf sko_th ctxt end
+ | p => p)
+ fun intr_imp ct th =
+ Thm.instantiate ([], map (pairself (cterm_of thy))
+ [(Var (("i", 0), @{typ nat}),
+ HOLogic.mk_nat ax_no)])
+ (zero_var_indexes @{thm skolem_COMBK_D})
+ RS Thm.implies_intr ct th
+ in
+ (NONE (*###*),
+ cnf_ths |> map (introduce_combinators_in_theorem
+ #> (case opt of SOME (_, ct) => intr_imp ct | NONE => I))
+ |> Variable.export ctxt ctxt0
+ |> finish_cnf
+ |> map Thm.close_derivation)
+ end
+
+
(* Convert a theorem to CNF, with additional premises due to skolemization. *)
fun cnf_axiom ctxt0 new_skolemizer ax_no th =
let
@@ -382,8 +434,23 @@
val (cnf_ths, ctxt) =
clausify nnf_th
|> (fn ([], _) =>
- (* FIXME: This probably doesn't work with the new Skolemizer *)
- clausify (to_definitional_cnf_with_quantifiers thy nnf_th)
+ if new_skolemizer then
+ let
+val _ = tracing ("**** NEW CLAUSIFIER, DEF-CNF: " ^ Display.string_of_thm ctxt (to_definitional_cnf_with_quantifiers ctxt nnf_th)) (*###*)
+val _ = tracing (" *** th: " ^ Display.string_of_thm ctxt th) (*###*)
+ val (_, (th1, ctxt)) = nnf_axiom choice_ths true ax_no th ctxt0
+val _ = tracing (" *** th1: " ^ Display.string_of_thm ctxt th1) (*###*)
+ val th2 = to_definitional_cnf_with_quantifiers ctxt th1
+val _ = tracing (" *** th2: " ^ Display.string_of_thm ctxt th2) (*###*)
+ val (ths3, ctxt) = clausify th2
+val _ = tracing (" *** hd ths3: " ^ Display.string_of_thm ctxt (hd ths3)) (*###*)
+ in (ths3, ctxt) end
+ else
+let
+val _ = tracing ("**** OLD CLAUSIFIER, DEF-CNF: " ^ Display.string_of_thm ctxt (to_definitional_cnf_with_quantifiers ctxt nnf_th))
+(*###*) in
+ clausify (to_definitional_cnf_with_quantifiers ctxt nnf_th)
+end
| p => p)
fun intr_imp ct th =
Thm.instantiate ([], map (pairself (cterm_of thy))
--- a/src/HOL/Tools/cnf_funcs.ML Thu Apr 14 11:24:04 2011 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML Thu Apr 14 11:24:04 2011 +0200
@@ -40,11 +40,12 @@
val clause_is_trivial: term -> bool
val clause2raw_thm: thm -> thm
+ val make_nnf_thm: theory -> term -> thm
val weakening_tac: int -> tactic (* removes the first hypothesis of a subgoal *)
- val make_cnf_thm: theory -> term -> thm
- val make_cnfx_thm: theory -> term -> thm
+ val make_cnf_thm: Proof.context -> term -> thm
+ val make_cnfx_thm: Proof.context -> term -> thm
val cnf_rewrite_tac: Proof.context -> int -> tactic (* converts all prems of a subgoal to CNF *)
val cnfx_rewrite_tac: Proof.context -> int -> tactic
(* converts all prems of a subgoal to (almost) definitional CNF *)
@@ -252,6 +253,24 @@
end
| make_nnf_thm thy t = inst_thm thy [t] iff_refl;
+val meta_eq_to_obj_eq = @{thm meta_eq_to_obj_eq}
+val eq_reflection = @{thm eq_reflection}
+
+fun make_under_quantifiers ctxt make t =
+ let
+ val thy = ProofContext.theory_of ctxt
+ fun conv ctxt ct =
+ case term_of ct of
+ (t1 as Const _) $ (t2 as Abs _) =>
+ Conv.comb_conv (conv ctxt) ct
+ | Abs _ => Conv.abs_conv (conv o snd) ctxt ct
+ | Const _ => Conv.all_conv ct
+ | t => make t RS eq_reflection
+ in conv ctxt (cterm_of thy t) RS meta_eq_to_obj_eq end
+
+fun make_nnf_thm_under_quantifiers ctxt =
+ make_under_quantifiers ctxt (make_nnf_thm (ProofContext.theory_of ctxt))
+
(* ------------------------------------------------------------------------- *)
(* simp_True_False_thm: produces a theorem t = t', where t' is equivalent to *)
(* t, but simplified wrt. the following theorems: *)
@@ -323,8 +342,9 @@
(* in the length of the term. *)
(* ------------------------------------------------------------------------- *)
-fun make_cnf_thm thy t =
+fun make_cnf_thm ctxt t =
let
+ val thy = ProofContext.theory_of ctxt
fun make_cnf_thm_from_nnf (Const (@{const_name HOL.conj}, _) $ x $ y) =
let
val thm1 = make_cnf_thm_from_nnf x
@@ -361,13 +381,19 @@
end
| make_cnf_thm_from_nnf t = inst_thm thy [t] iff_refl
(* convert 't' to NNF first *)
+ val nnf_thm = make_nnf_thm_under_quantifiers ctxt t
+(*###
val nnf_thm = make_nnf_thm thy t
+*)
val nnf = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) nnf_thm
(* then simplify wrt. True/False (this should preserve NNF) *)
val simp_thm = simp_True_False_thm thy nnf
val simp = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) simp_thm
(* finally, convert to CNF (this should preserve the simplification) *)
+ val cnf_thm = make_under_quantifiers ctxt make_cnf_thm_from_nnf simp
+(* ###
val cnf_thm = make_cnf_thm_from_nnf simp
+*)
in
iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnf_thm]
end;
@@ -386,8 +412,9 @@
(* in the case of nested equivalences. *)
(* ------------------------------------------------------------------------- *)
-fun make_cnfx_thm thy t =
+fun make_cnfx_thm ctxt t =
let
+ val thy = ProofContext.theory_of ctxt
val var_id = Unsynchronized.ref 0 (* properly initialized below *)
fun new_free () =
Free ("cnfx_" ^ string_of_int (Unsynchronized.inc var_id), HOLogic.boolT)
@@ -465,7 +492,10 @@
end
| make_cnfx_thm_from_nnf t = inst_thm thy [t] iff_refl
(* convert 't' to NNF first *)
+ val nnf_thm = make_nnf_thm_under_quantifiers ctxt t
+(* ###
val nnf_thm = make_nnf_thm thy t
+*)
val nnf = (snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) nnf_thm
(* then simplify wrt. True/False (this should preserve NNF) *)
val simp_thm = simp_True_False_thm thy nnf
@@ -483,7 +513,10 @@
Int.max (max, the_default 0 idx)
end) (OldTerm.term_frees simp) 0)
(* finally, convert to definitional CNF (this should preserve the simplification) *)
+ val cnfx_thm = make_under_quantifiers ctxt make_cnfx_thm_from_nnf simp
+(*###
val cnfx_thm = make_cnfx_thm_from_nnf simp
+*)
in
iff_trans OF [iff_trans OF [nnf_thm, simp_thm], cnfx_thm]
end;
@@ -509,8 +542,7 @@
(* cut the CNF formulas as new premises *)
Subgoal.FOCUS (fn {prems, ...} =>
let
- val thy = ProofContext.theory_of ctxt
- val cnf_thms = map (make_cnf_thm thy o HOLogic.dest_Trueprop o Thm.prop_of) prems
+ val cnf_thms = map (make_cnf_thm ctxt o HOLogic.dest_Trueprop o Thm.prop_of) prems
val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnf_thms ~~ prems)
in
cut_facts_tac cut_thms 1
@@ -532,8 +564,7 @@
(* cut the CNF formulas as new premises *)
Subgoal.FOCUS (fn {prems, ...} =>
let
- val thy = ProofContext.theory_of ctxt;
- val cnfx_thms = map (make_cnfx_thm thy o HOLogic.dest_Trueprop o prop_of) prems
+ val cnfx_thms = map (make_cnfx_thm ctxt o HOLogic.dest_Trueprop o prop_of) prems
val cut_thms = map (fn (th, pr) => cnftac_eq_imp OF [th, pr]) (cnfx_thms ~~ prems)
in
cut_facts_tac cut_thms 1