hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names

--- 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. ~(\<forall>x. P(x)) ==> \<exists>x. ~P(x)"
-  and meson_not_exD: "!!P. ~(\<exists>x. P(x)) ==> \<forall>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. ~(\<forall>x. P(x)) ==> \<exists>x. ~P(x)"
+  and not_exD: "!!P. ~(\<exists>x. P(x)) ==> \<forall>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. (\<exists>x. P(x)) & Q ==> \<exists>x. P(x) & Q"
-  and meson_conj_exD2: "!!P Q. P & (\<exists>x. Q(x)) ==> \<exists>x. P & Q(x)"
+lemma conj_exD1: "!!P Q. (\<exists>x. P(x)) & Q ==> \<exists>x. P(x) & Q"
+  and conj_exD2: "!!P Q. P & (\<exists>x. Q(x)) ==> \<exists>x. P & Q(x)"
   by fast+
 
 
 text {* Disjunction *}
 
-lemma meson_disj_exD: "!!P Q. (\<exists>x. P(x)) | (\<exists>x. Q(x)) ==> \<exists>x. P(x) | Q(x)"
+lemma disj_exD: "!!P Q. (\<exists>x. P(x)) | (\<exists>x. Q(x)) ==> \<exists>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. (\<exists>x. P(x)) | Q ==> \<exists>x. P(x) | Q"
-  and meson_disj_exD2: "!!P Q. P | (\<exists>x. Q(x)) ==> \<exists>x. P | Q(x)"
+  and disj_exD1: "!!P Q. (\<exists>x. P(x)) | Q ==> \<exists>x. P(x) | Q"
+  and disj_exD2: "!!P Q. P | (\<exists>x. Q(x)) ==> \<exists>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

--- 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

--- 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))

--- 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
 

--- 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)))

--- 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})),

--- 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')

--- 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})]