# HG changeset patch # User blanchet # Date 1286271910 -7200 # Node ID aa54f347e5e26fd78151d74d033268a35064147c # Parent 7fb79905ed72de37c997c373547702ca72f4dd2a hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names diff -r 7fb79905ed72 -r aa54f347e5e2 src/HOL/Meson.thy --- a/src/HOL/Meson.thy Tue Oct 05 11:14:56 2010 +0200 +++ b/src/HOL/Meson.thy Tue Oct 05 11:45:10 2010 +0200 @@ -18,22 +18,22 @@ text {* de Morgan laws *} -lemma meson_not_conjD: "~(P&Q) ==> ~P | ~Q" - and meson_not_disjD: "~(P|Q) ==> ~P & ~Q" - and meson_not_notD: "~~P ==> P" - and meson_not_allD: "!!P. ~(\x. P(x)) ==> \x. ~P(x)" - and meson_not_exD: "!!P. ~(\x. P(x)) ==> \x. ~P(x)" +lemma not_conjD: "~(P&Q) ==> ~P | ~Q" + and not_disjD: "~(P|Q) ==> ~P & ~Q" + and not_notD: "~~P ==> P" + and not_allD: "!!P. ~(\x. P(x)) ==> \x. ~P(x)" + and not_exD: "!!P. ~(\x. P(x)) ==> \x. ~P(x)" by fast+ text {* Removal of @{text "-->"} and @{text "<->"} (positive and negative occurrences) *} -lemma meson_imp_to_disjD: "P-->Q ==> ~P | Q" - and meson_not_impD: "~(P-->Q) ==> P & ~Q" - and meson_iff_to_disjD: "P=Q ==> (~P | Q) & (~Q | P)" - and meson_not_iffD: "~(P=Q) ==> (P | Q) & (~P | ~Q)" +lemma imp_to_disjD: "P-->Q ==> ~P | Q" + and not_impD: "~(P-->Q) ==> P & ~Q" + and iff_to_disjD: "P=Q ==> (~P | Q) & (~Q | P)" + and not_iffD: "~(P=Q) ==> (P | Q) & (~P | ~Q)" -- {* Much more efficient than @{prop "(P & ~Q) | (Q & ~P)"} for computing CNF *} - and meson_not_refl_disj_D: "x ~= x | P ==> P" + and not_refl_disj_D: "x ~= x | P ==> P" by fast+ @@ -41,24 +41,24 @@ text {* Conjunction *} -lemma meson_conj_exD1: "!!P Q. (\x. P(x)) & Q ==> \x. P(x) & Q" - and meson_conj_exD2: "!!P Q. P & (\x. Q(x)) ==> \x. P & Q(x)" +lemma conj_exD1: "!!P Q. (\x. P(x)) & Q ==> \x. P(x) & Q" + and conj_exD2: "!!P Q. P & (\x. Q(x)) ==> \x. P & Q(x)" by fast+ text {* Disjunction *} -lemma meson_disj_exD: "!!P Q. (\x. P(x)) | (\x. Q(x)) ==> \x. P(x) | Q(x)" +lemma disj_exD: "!!P Q. (\x. P(x)) | (\x. Q(x)) ==> \x. P(x) | Q(x)" -- {* DO NOT USE with forall-Skolemization: makes fewer schematic variables!! *} -- {* With ex-Skolemization, makes fewer Skolem constants *} - and meson_disj_exD1: "!!P Q. (\x. P(x)) | Q ==> \x. P(x) | Q" - and meson_disj_exD2: "!!P Q. P | (\x. Q(x)) ==> \x. P | Q(x)" + and disj_exD1: "!!P Q. (\x. P(x)) | Q ==> \x. P(x) | Q" + and disj_exD2: "!!P Q. P | (\x. Q(x)) ==> \x. P | Q(x)" by fast+ -lemma meson_disj_assoc: "(P|Q)|R ==> P|(Q|R)" - and meson_disj_comm: "P|Q ==> Q|P" - and meson_disj_FalseD1: "False|P ==> P" - and meson_disj_FalseD2: "P|False ==> P" +lemma disj_assoc: "(P|Q)|R ==> P|(Q|R)" + and disj_comm: "P|Q ==> Q|P" + and disj_FalseD1: "False|P ==> P" + and disj_FalseD2: "P|False ==> P" by fast+ @@ -197,4 +197,11 @@ #> Meson_Tactic.setup *} +hide_const (open) COMBI COMBK COMBB COMBC COMBS skolem +hide_fact (open) not_conjD not_disjD not_notD not_allD not_exD imp_to_disjD + not_impD iff_to_disjD not_iffD not_refl_disj_D conj_exD1 conj_exD2 disj_exD + disj_exD1 disj_exD2 disj_assoc disj_comm disj_FalseD1 disj_FalseD2 TruepropI + COMBI_def COMBK_def COMBB_def COMBC_def COMBS_def abs_I abs_K abs_B abs_C + abs_S skolem_def skolem_COMBK_iff skolem_COMBK_I skolem_COMBK_D + end diff -r 7fb79905ed72 -r aa54f347e5e2 src/HOL/Metis.thy --- a/src/HOL/Metis.thy Tue Oct 05 11:14:56 2010 +0200 +++ b/src/HOL/Metis.thy Tue Oct 05 11:45:10 2010 +0200 @@ -31,4 +31,7 @@ use "Tools/Metis/metis_tactics.ML" setup Metis_Tactics.setup +hide_const (open) fequal +hide_fact (open) fequal_imp_equal equal_imp_fequal equal_imp_equal + end diff -r 7fb79905ed72 -r aa54f347e5e2 src/HOL/Tools/Meson/meson.ML --- a/src/HOL/Tools/Meson/meson.ML Tue Oct 05 11:14:56 2010 +0200 +++ b/src/HOL/Tools/Meson/meson.ML Tue Oct 05 11:45:10 2010 +0200 @@ -66,24 +66,24 @@ val all_forward = @{thm all_forward}; val ex_forward = @{thm ex_forward}; -val not_conjD = @{thm meson_not_conjD}; -val not_disjD = @{thm meson_not_disjD}; -val not_notD = @{thm meson_not_notD}; -val not_allD = @{thm meson_not_allD}; -val not_exD = @{thm meson_not_exD}; -val imp_to_disjD = @{thm meson_imp_to_disjD}; -val not_impD = @{thm meson_not_impD}; -val iff_to_disjD = @{thm meson_iff_to_disjD}; -val not_iffD = @{thm meson_not_iffD}; -val conj_exD1 = @{thm meson_conj_exD1}; -val conj_exD2 = @{thm meson_conj_exD2}; -val disj_exD = @{thm meson_disj_exD}; -val disj_exD1 = @{thm meson_disj_exD1}; -val disj_exD2 = @{thm meson_disj_exD2}; -val disj_assoc = @{thm meson_disj_assoc}; -val disj_comm = @{thm meson_disj_comm}; -val disj_FalseD1 = @{thm meson_disj_FalseD1}; -val disj_FalseD2 = @{thm meson_disj_FalseD2}; +val not_conjD = @{thm not_conjD}; +val not_disjD = @{thm not_disjD}; +val not_notD = @{thm not_notD}; +val not_allD = @{thm not_allD}; +val not_exD = @{thm not_exD}; +val imp_to_disjD = @{thm imp_to_disjD}; +val not_impD = @{thm not_impD}; +val iff_to_disjD = @{thm iff_to_disjD}; +val not_iffD = @{thm not_iffD}; +val conj_exD1 = @{thm conj_exD1}; +val conj_exD2 = @{thm conj_exD2}; +val disj_exD = @{thm disj_exD}; +val disj_exD1 = @{thm disj_exD1}; +val disj_exD2 = @{thm disj_exD2}; +val disj_assoc = @{thm disj_assoc}; +val disj_comm = @{thm disj_comm}; +val disj_FalseD1 = @{thm disj_FalseD1}; +val disj_FalseD2 = @{thm disj_FalseD2}; (**** Operators for forward proof ****) @@ -212,7 +212,7 @@ (*They are typically functional reflexivity axioms and are the converses of injectivity equivalences*) -val not_refl_disj_D = @{thm meson_not_refl_disj_D}; +val not_refl_disj_D = @{thm not_refl_disj_D}; (*Is either term a Var that does not properly occur in the other term?*) fun eliminable (t as Var _, u) = t aconv u orelse not (Logic.occs(t,u)) diff -r 7fb79905ed72 -r aa54f347e5e2 src/HOL/Tools/Metis/metis_reconstruct.ML --- a/src/HOL/Tools/Metis/metis_reconstruct.ML Tue Oct 05 11:14:56 2010 +0200 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Tue Oct 05 11:45:10 2010 +0200 @@ -532,7 +532,7 @@ fun is_metis_literal_genuine (_, (s, _)) = not (String.isPrefix class_prefix s) fun is_isabelle_literal_genuine t = - case t of _ $ (Const (@{const_name skolem}, _) $ _) => false | _ => true + case t of _ $ (Const (@{const_name Meson.skolem}, _) $ _) => false | _ => true fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0 diff -r 7fb79905ed72 -r aa54f347e5e2 src/HOL/Tools/Metis/metis_tactics.ML --- a/src/HOL/Tools/Metis/metis_tactics.ML Tue Oct 05 11:14:56 2010 +0200 +++ b/src/HOL/Tools/Metis/metis_tactics.ML Tue Oct 05 11:45:10 2010 +0200 @@ -222,7 +222,7 @@ in (tysubst, tsubst) end fun subst_info_for_prem subgoal_no prem = case prem of - _ $ (Const (@{const_name skolem}, _) $ (_ $ t $ num)) => + _ $ (Const (@{const_name Meson.skolem}, _) $ (_ $ t $ num)) => let val ax_no = HOLogic.dest_nat num in (ax_no, (subgoal_no, match_term (nth axioms ax_no |> the |> snd, t))) @@ -298,7 +298,7 @@ ordered_clusters 1 THEN match_tac [prems_imp_false] 1 THEN ALLGOALS (fn i => - rtac @{thm skolem_COMBK_I} i + rtac @{thm Meson.skolem_COMBK_I} i THEN rotate_tac (rotation_for_subgoal i) i THEN PRIMITIVE (unify_first_prem_with_concl thy i) THEN assume_tac i))) diff -r 7fb79905ed72 -r aa54f347e5e2 src/HOL/Tools/Metis/metis_translate.ML --- a/src/HOL/Tools/Metis/metis_translate.ML Tue Oct 05 11:14:56 2010 +0200 +++ b/src/HOL/Tools/Metis/metis_translate.ML Tue Oct 05 11:45:10 2010 +0200 @@ -112,11 +112,11 @@ (@{const_name HOL.implies}, "implies"), (@{const_name Set.member}, "member"), (@{const_name fequal}, "fequal"), - (@{const_name COMBI}, "COMBI"), - (@{const_name COMBK}, "COMBK"), - (@{const_name COMBB}, "COMBB"), - (@{const_name COMBC}, "COMBC"), - (@{const_name COMBS}, "COMBS"), + (@{const_name Meson.COMBI}, "COMBI"), + (@{const_name Meson.COMBK}, "COMBK"), + (@{const_name Meson.COMBB}, "COMBB"), + (@{const_name Meson.COMBC}, "COMBC"), + (@{const_name Meson.COMBS}, "COMBS"), (@{const_name True}, "True"), (@{const_name False}, "False"), (@{const_name If}, "If")] @@ -463,10 +463,10 @@ (space_implode Long_Name.separator (map Int.toString [i, j, num_T_args])) fun conceal_old_skolem_terms i old_skolems t = - if exists_Const (curry (op =) @{const_name skolem} o fst) t then + if exists_Const (curry (op =) @{const_name Meson.skolem} o fst) t then let fun aux old_skolems - (t as (Const (@{const_name skolem}, Type (_, [_, T])) $ _)) = + (t as (Const (@{const_name Meson.skolem}, Type (_, [_, T])) $ _)) = let val (old_skolems, s) = if i = ~1 then @@ -532,7 +532,7 @@ fun aux (Const x) = fold (fold_type_consts set_insert) (Sign.const_typargs thy x) | aux (Abs (_, _, u)) = aux u - | aux (Const (@{const_name skolem}, _) $ _) = I + | aux (Const (@{const_name Meson.skolem}, _) $ _) = I | aux (t $ u) = aux t #> aux u | aux _ = I in aux end @@ -647,11 +647,11 @@ end; val helpers = - [("c_COMBI", (false, map (`I) @{thms COMBI_def})), - ("c_COMBK", (false, map (`I) @{thms COMBK_def})), - ("c_COMBB", (false, map (`I) @{thms COMBB_def})), - ("c_COMBC", (false, map (`I) @{thms COMBC_def})), - ("c_COMBS", (false, map (`I) @{thms COMBS_def})), + [("c_COMBI", (false, map (`I) @{thms Meson.COMBI_def})), + ("c_COMBK", (false, map (`I) @{thms Meson.COMBK_def})), + ("c_COMBB", (false, map (`I) @{thms Meson.COMBB_def})), + ("c_COMBC", (false, map (`I) @{thms Meson.COMBC_def})), + ("c_COMBS", (false, map (`I) @{thms Meson.COMBS_def})), ("c_fequal", (false, map (rpair @{thm equal_imp_equal}) @{thms fequal_imp_equal equal_imp_fequal})), ("c_True", (true, map (`I) @{thms True_or_False})), diff -r 7fb79905ed72 -r aa54f347e5e2 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Tue Oct 05 11:14:56 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Tue Oct 05 11:45:10 2010 +0200 @@ -370,11 +370,11 @@ pair (raw_term_from_pred thy full_types tfrees u) val combinator_table = - [(@{const_name COMBI}, @{thm COMBI_def_raw}), - (@{const_name COMBK}, @{thm COMBK_def_raw}), - (@{const_name COMBB}, @{thm COMBB_def_raw}), - (@{const_name COMBC}, @{thm COMBC_def_raw}), - (@{const_name COMBS}, @{thm COMBS_def_raw})] + [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def_raw}), + (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def_raw}), + (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def_raw}), + (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def_raw}), + (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def_raw})] fun uncombine_term (t1 $ t2) = betapply (pairself uncombine_term (t1, t2)) | uncombine_term (Abs (s, T, t')) = Abs (s, T, uncombine_term t') diff -r 7fb79905ed72 -r aa54f347e5e2 src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Tue Oct 05 11:14:56 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Tue Oct 05 11:45:10 2010 +0200 @@ -222,11 +222,11 @@ count_combformula combformula val optional_helpers = - [(["c_COMBI"], @{thms COMBI_def}), - (["c_COMBK"], @{thms COMBK_def}), - (["c_COMBB"], @{thms COMBB_def}), - (["c_COMBC"], @{thms COMBC_def}), - (["c_COMBS"], @{thms COMBS_def})] + [(["c_COMBI"], @{thms Meson.COMBI_def}), + (["c_COMBK"], @{thms Meson.COMBK_def}), + (["c_COMBB"], @{thms Meson.COMBB_def}), + (["c_COMBC"], @{thms Meson.COMBC_def}), + (["c_COMBS"], @{thms Meson.COMBS_def})] val optional_typed_helpers = [(["c_True", "c_False", "c_If"], @{thms True_or_False}), (["c_If"], @{thms if_True if_False})]