hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
authorblanchet
Tue Oct 05 11:45:10 2010 +0200 (2010-10-05)
changeset 39953aa54f347e5e2
parent 39952 7fb79905ed72
child 39954 1a908a35920b
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
src/HOL/Meson.thy
src/HOL/Metis.thy
src/HOL/Tools/Meson/meson.ML
src/HOL/Tools/Metis/metis_reconstruct.ML
src/HOL/Tools/Metis/metis_tactics.ML
src/HOL/Tools/Metis/metis_translate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
     1.1 --- a/src/HOL/Meson.thy	Tue Oct 05 11:14:56 2010 +0200
     1.2 +++ b/src/HOL/Meson.thy	Tue Oct 05 11:45:10 2010 +0200
     1.3 @@ -18,22 +18,22 @@
     1.4  
     1.5  text {* de Morgan laws *}
     1.6  
     1.7 -lemma meson_not_conjD: "~(P&Q) ==> ~P | ~Q"
     1.8 -  and meson_not_disjD: "~(P|Q) ==> ~P & ~Q"
     1.9 -  and meson_not_notD: "~~P ==> P"
    1.10 -  and meson_not_allD: "!!P. ~(\<forall>x. P(x)) ==> \<exists>x. ~P(x)"
    1.11 -  and meson_not_exD: "!!P. ~(\<exists>x. P(x)) ==> \<forall>x. ~P(x)"
    1.12 +lemma not_conjD: "~(P&Q) ==> ~P | ~Q"
    1.13 +  and not_disjD: "~(P|Q) ==> ~P & ~Q"
    1.14 +  and not_notD: "~~P ==> P"
    1.15 +  and not_allD: "!!P. ~(\<forall>x. P(x)) ==> \<exists>x. ~P(x)"
    1.16 +  and not_exD: "!!P. ~(\<exists>x. P(x)) ==> \<forall>x. ~P(x)"
    1.17    by fast+
    1.18  
    1.19  text {* Removal of @{text "-->"} and @{text "<->"} (positive and
    1.20  negative occurrences) *}
    1.21  
    1.22 -lemma meson_imp_to_disjD: "P-->Q ==> ~P | Q"
    1.23 -  and meson_not_impD: "~(P-->Q) ==> P & ~Q"
    1.24 -  and meson_iff_to_disjD: "P=Q ==> (~P | Q) & (~Q | P)"
    1.25 -  and meson_not_iffD: "~(P=Q) ==> (P | Q) & (~P | ~Q)"
    1.26 +lemma imp_to_disjD: "P-->Q ==> ~P | Q"
    1.27 +  and not_impD: "~(P-->Q) ==> P & ~Q"
    1.28 +  and iff_to_disjD: "P=Q ==> (~P | Q) & (~Q | P)"
    1.29 +  and not_iffD: "~(P=Q) ==> (P | Q) & (~P | ~Q)"
    1.30      -- {* Much more efficient than @{prop "(P & ~Q) | (Q & ~P)"} for computing CNF *}
    1.31 -  and meson_not_refl_disj_D: "x ~= x | P ==> P"
    1.32 +  and not_refl_disj_D: "x ~= x | P ==> P"
    1.33    by fast+
    1.34  
    1.35  
    1.36 @@ -41,24 +41,24 @@
    1.37  
    1.38  text {* Conjunction *}
    1.39  
    1.40 -lemma meson_conj_exD1: "!!P Q. (\<exists>x. P(x)) & Q ==> \<exists>x. P(x) & Q"
    1.41 -  and meson_conj_exD2: "!!P Q. P & (\<exists>x. Q(x)) ==> \<exists>x. P & Q(x)"
    1.42 +lemma conj_exD1: "!!P Q. (\<exists>x. P(x)) & Q ==> \<exists>x. P(x) & Q"
    1.43 +  and conj_exD2: "!!P Q. P & (\<exists>x. Q(x)) ==> \<exists>x. P & Q(x)"
    1.44    by fast+
    1.45  
    1.46  
    1.47  text {* Disjunction *}
    1.48  
    1.49 -lemma meson_disj_exD: "!!P Q. (\<exists>x. P(x)) | (\<exists>x. Q(x)) ==> \<exists>x. P(x) | Q(x)"
    1.50 +lemma disj_exD: "!!P Q. (\<exists>x. P(x)) | (\<exists>x. Q(x)) ==> \<exists>x. P(x) | Q(x)"
    1.51    -- {* DO NOT USE with forall-Skolemization: makes fewer schematic variables!! *}
    1.52    -- {* With ex-Skolemization, makes fewer Skolem constants *}
    1.53 -  and meson_disj_exD1: "!!P Q. (\<exists>x. P(x)) | Q ==> \<exists>x. P(x) | Q"
    1.54 -  and meson_disj_exD2: "!!P Q. P | (\<exists>x. Q(x)) ==> \<exists>x. P | Q(x)"
    1.55 +  and disj_exD1: "!!P Q. (\<exists>x. P(x)) | Q ==> \<exists>x. P(x) | Q"
    1.56 +  and disj_exD2: "!!P Q. P | (\<exists>x. Q(x)) ==> \<exists>x. P | Q(x)"
    1.57    by fast+
    1.58  
    1.59 -lemma meson_disj_assoc: "(P|Q)|R ==> P|(Q|R)"
    1.60 -  and meson_disj_comm: "P|Q ==> Q|P"
    1.61 -  and meson_disj_FalseD1: "False|P ==> P"
    1.62 -  and meson_disj_FalseD2: "P|False ==> P"
    1.63 +lemma disj_assoc: "(P|Q)|R ==> P|(Q|R)"
    1.64 +  and disj_comm: "P|Q ==> Q|P"
    1.65 +  and disj_FalseD1: "False|P ==> P"
    1.66 +  and disj_FalseD2: "P|False ==> P"
    1.67    by fast+
    1.68  
    1.69  
    1.70 @@ -197,4 +197,11 @@
    1.71    #> Meson_Tactic.setup
    1.72  *}
    1.73  
    1.74 +hide_const (open) COMBI COMBK COMBB COMBC COMBS skolem
    1.75 +hide_fact (open) not_conjD not_disjD not_notD not_allD not_exD imp_to_disjD
    1.76 +    not_impD iff_to_disjD not_iffD not_refl_disj_D conj_exD1 conj_exD2 disj_exD
    1.77 +    disj_exD1 disj_exD2 disj_assoc disj_comm disj_FalseD1 disj_FalseD2 TruepropI
    1.78 +    COMBI_def COMBK_def COMBB_def COMBC_def COMBS_def abs_I abs_K abs_B abs_C
    1.79 +    abs_S skolem_def skolem_COMBK_iff skolem_COMBK_I skolem_COMBK_D
    1.80 +
    1.81  end
     2.1 --- a/src/HOL/Metis.thy	Tue Oct 05 11:14:56 2010 +0200
     2.2 +++ b/src/HOL/Metis.thy	Tue Oct 05 11:45:10 2010 +0200
     2.3 @@ -31,4 +31,7 @@
     2.4  use "Tools/Metis/metis_tactics.ML"
     2.5  setup Metis_Tactics.setup
     2.6  
     2.7 +hide_const (open) fequal
     2.8 +hide_fact (open) fequal_imp_equal equal_imp_fequal equal_imp_equal
     2.9 +
    2.10  end
     3.1 --- a/src/HOL/Tools/Meson/meson.ML	Tue Oct 05 11:14:56 2010 +0200
     3.2 +++ b/src/HOL/Tools/Meson/meson.ML	Tue Oct 05 11:45:10 2010 +0200
     3.3 @@ -66,24 +66,24 @@
     3.4  val all_forward = @{thm all_forward};
     3.5  val ex_forward = @{thm ex_forward};
     3.6  
     3.7 -val not_conjD = @{thm meson_not_conjD};
     3.8 -val not_disjD = @{thm meson_not_disjD};
     3.9 -val not_notD = @{thm meson_not_notD};
    3.10 -val not_allD = @{thm meson_not_allD};
    3.11 -val not_exD = @{thm meson_not_exD};
    3.12 -val imp_to_disjD = @{thm meson_imp_to_disjD};
    3.13 -val not_impD = @{thm meson_not_impD};
    3.14 -val iff_to_disjD = @{thm meson_iff_to_disjD};
    3.15 -val not_iffD = @{thm meson_not_iffD};
    3.16 -val conj_exD1 = @{thm meson_conj_exD1};
    3.17 -val conj_exD2 = @{thm meson_conj_exD2};
    3.18 -val disj_exD = @{thm meson_disj_exD};
    3.19 -val disj_exD1 = @{thm meson_disj_exD1};
    3.20 -val disj_exD2 = @{thm meson_disj_exD2};
    3.21 -val disj_assoc = @{thm meson_disj_assoc};
    3.22 -val disj_comm = @{thm meson_disj_comm};
    3.23 -val disj_FalseD1 = @{thm meson_disj_FalseD1};
    3.24 -val disj_FalseD2 = @{thm meson_disj_FalseD2};
    3.25 +val not_conjD = @{thm not_conjD};
    3.26 +val not_disjD = @{thm not_disjD};
    3.27 +val not_notD = @{thm not_notD};
    3.28 +val not_allD = @{thm not_allD};
    3.29 +val not_exD = @{thm not_exD};
    3.30 +val imp_to_disjD = @{thm imp_to_disjD};
    3.31 +val not_impD = @{thm not_impD};
    3.32 +val iff_to_disjD = @{thm iff_to_disjD};
    3.33 +val not_iffD = @{thm not_iffD};
    3.34 +val conj_exD1 = @{thm conj_exD1};
    3.35 +val conj_exD2 = @{thm conj_exD2};
    3.36 +val disj_exD = @{thm disj_exD};
    3.37 +val disj_exD1 = @{thm disj_exD1};
    3.38 +val disj_exD2 = @{thm disj_exD2};
    3.39 +val disj_assoc = @{thm disj_assoc};
    3.40 +val disj_comm = @{thm disj_comm};
    3.41 +val disj_FalseD1 = @{thm disj_FalseD1};
    3.42 +val disj_FalseD2 = @{thm disj_FalseD2};
    3.43  
    3.44  
    3.45  (**** Operators for forward proof ****)
    3.46 @@ -212,7 +212,7 @@
    3.47  (*They are typically functional reflexivity axioms and are the converses of
    3.48    injectivity equivalences*)
    3.49  
    3.50 -val not_refl_disj_D = @{thm meson_not_refl_disj_D};
    3.51 +val not_refl_disj_D = @{thm not_refl_disj_D};
    3.52  
    3.53  (*Is either term a Var that does not properly occur in the other term?*)
    3.54  fun eliminable (t as Var _, u) = t aconv u orelse not (Logic.occs(t,u))
     4.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Tue Oct 05 11:14:56 2010 +0200
     4.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Tue Oct 05 11:45:10 2010 +0200
     4.3 @@ -532,7 +532,7 @@
     4.4  
     4.5  fun is_metis_literal_genuine (_, (s, _)) = not (String.isPrefix class_prefix s)
     4.6  fun is_isabelle_literal_genuine t =
     4.7 -  case t of _ $ (Const (@{const_name skolem}, _) $ _) => false | _ => true
     4.8 +  case t of _ $ (Const (@{const_name Meson.skolem}, _) $ _) => false | _ => true
     4.9  
    4.10  fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0
    4.11  
     5.1 --- a/src/HOL/Tools/Metis/metis_tactics.ML	Tue Oct 05 11:14:56 2010 +0200
     5.2 +++ b/src/HOL/Tools/Metis/metis_tactics.ML	Tue Oct 05 11:45:10 2010 +0200
     5.3 @@ -222,7 +222,7 @@
     5.4          in (tysubst, tsubst) end
     5.5        fun subst_info_for_prem subgoal_no prem =
     5.6          case prem of
     5.7 -          _ $ (Const (@{const_name skolem}, _) $ (_ $ t $ num)) =>
     5.8 +          _ $ (Const (@{const_name Meson.skolem}, _) $ (_ $ t $ num)) =>
     5.9            let val ax_no = HOLogic.dest_nat num in
    5.10              (ax_no, (subgoal_no,
    5.11                       match_term (nth axioms ax_no |> the |> snd, t)))
    5.12 @@ -298,7 +298,7 @@
    5.13                                          ordered_clusters 1
    5.14                THEN match_tac [prems_imp_false] 1
    5.15                THEN ALLGOALS (fn i =>
    5.16 -                       rtac @{thm skolem_COMBK_I} i
    5.17 +                       rtac @{thm Meson.skolem_COMBK_I} i
    5.18                         THEN rotate_tac (rotation_for_subgoal i) i
    5.19                         THEN PRIMITIVE (unify_first_prem_with_concl thy i)
    5.20                         THEN assume_tac i)))
     6.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Tue Oct 05 11:14:56 2010 +0200
     6.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Tue Oct 05 11:45:10 2010 +0200
     6.3 @@ -112,11 +112,11 @@
     6.4                 (@{const_name HOL.implies}, "implies"),
     6.5                 (@{const_name Set.member}, "member"),
     6.6                 (@{const_name fequal}, "fequal"),
     6.7 -               (@{const_name COMBI}, "COMBI"),
     6.8 -               (@{const_name COMBK}, "COMBK"),
     6.9 -               (@{const_name COMBB}, "COMBB"),
    6.10 -               (@{const_name COMBC}, "COMBC"),
    6.11 -               (@{const_name COMBS}, "COMBS"),
    6.12 +               (@{const_name Meson.COMBI}, "COMBI"),
    6.13 +               (@{const_name Meson.COMBK}, "COMBK"),
    6.14 +               (@{const_name Meson.COMBB}, "COMBB"),
    6.15 +               (@{const_name Meson.COMBC}, "COMBC"),
    6.16 +               (@{const_name Meson.COMBS}, "COMBS"),
    6.17                 (@{const_name True}, "True"),
    6.18                 (@{const_name False}, "False"),
    6.19                 (@{const_name If}, "If")]
    6.20 @@ -463,10 +463,10 @@
    6.21    (space_implode Long_Name.separator (map Int.toString [i, j, num_T_args]))
    6.22  
    6.23  fun conceal_old_skolem_terms i old_skolems t =
    6.24 -  if exists_Const (curry (op =) @{const_name skolem} o fst) t then
    6.25 +  if exists_Const (curry (op =) @{const_name Meson.skolem} o fst) t then
    6.26      let
    6.27        fun aux old_skolems
    6.28 -              (t as (Const (@{const_name skolem}, Type (_, [_, T])) $ _)) =
    6.29 +             (t as (Const (@{const_name Meson.skolem}, Type (_, [_, T])) $ _)) =
    6.30            let
    6.31              val (old_skolems, s) =
    6.32                if i = ~1 then
    6.33 @@ -532,7 +532,7 @@
    6.34      fun aux (Const x) =
    6.35          fold (fold_type_consts set_insert) (Sign.const_typargs thy x)
    6.36        | aux (Abs (_, _, u)) = aux u
    6.37 -      | aux (Const (@{const_name skolem}, _) $ _) = I
    6.38 +      | aux (Const (@{const_name Meson.skolem}, _) $ _) = I
    6.39        | aux (t $ u) = aux t #> aux u
    6.40        | aux _ = I
    6.41    in aux end
    6.42 @@ -647,11 +647,11 @@
    6.43    end;
    6.44  
    6.45  val helpers =
    6.46 -  [("c_COMBI", (false, map (`I) @{thms COMBI_def})),
    6.47 -   ("c_COMBK", (false, map (`I) @{thms COMBK_def})),
    6.48 -   ("c_COMBB", (false, map (`I) @{thms COMBB_def})),
    6.49 -   ("c_COMBC", (false, map (`I) @{thms COMBC_def})),
    6.50 -   ("c_COMBS", (false, map (`I) @{thms COMBS_def})),
    6.51 +  [("c_COMBI", (false, map (`I) @{thms Meson.COMBI_def})),
    6.52 +   ("c_COMBK", (false, map (`I) @{thms Meson.COMBK_def})),
    6.53 +   ("c_COMBB", (false, map (`I) @{thms Meson.COMBB_def})),
    6.54 +   ("c_COMBC", (false, map (`I) @{thms Meson.COMBC_def})),
    6.55 +   ("c_COMBS", (false, map (`I) @{thms Meson.COMBS_def})),
    6.56     ("c_fequal", (false, map (rpair @{thm equal_imp_equal})
    6.57                              @{thms fequal_imp_equal equal_imp_fequal})),
    6.58     ("c_True", (true, map (`I) @{thms True_or_False})),
     7.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Oct 05 11:14:56 2010 +0200
     7.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Oct 05 11:45:10 2010 +0200
     7.3 @@ -370,11 +370,11 @@
     7.4      pair (raw_term_from_pred thy full_types tfrees u)
     7.5  
     7.6  val combinator_table =
     7.7 -  [(@{const_name COMBI}, @{thm COMBI_def_raw}),
     7.8 -   (@{const_name COMBK}, @{thm COMBK_def_raw}),
     7.9 -   (@{const_name COMBB}, @{thm COMBB_def_raw}),
    7.10 -   (@{const_name COMBC}, @{thm COMBC_def_raw}),
    7.11 -   (@{const_name COMBS}, @{thm COMBS_def_raw})]
    7.12 +  [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def_raw}),
    7.13 +   (@{const_name Meson.COMBK}, @{thm Meson.COMBK_def_raw}),
    7.14 +   (@{const_name Meson.COMBB}, @{thm Meson.COMBB_def_raw}),
    7.15 +   (@{const_name Meson.COMBC}, @{thm Meson.COMBC_def_raw}),
    7.16 +   (@{const_name Meson.COMBS}, @{thm Meson.COMBS_def_raw})]
    7.17  
    7.18  fun uncombine_term (t1 $ t2) = betapply (pairself uncombine_term (t1, t2))
    7.19    | uncombine_term (Abs (s, T, t')) = Abs (s, T, uncombine_term t')
     8.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Tue Oct 05 11:14:56 2010 +0200
     8.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Tue Oct 05 11:45:10 2010 +0200
     8.3 @@ -222,11 +222,11 @@
     8.4    count_combformula combformula
     8.5  
     8.6  val optional_helpers =
     8.7 -  [(["c_COMBI"], @{thms COMBI_def}),
     8.8 -   (["c_COMBK"], @{thms COMBK_def}),
     8.9 -   (["c_COMBB"], @{thms COMBB_def}),
    8.10 -   (["c_COMBC"], @{thms COMBC_def}),
    8.11 -   (["c_COMBS"], @{thms COMBS_def})]
    8.12 +  [(["c_COMBI"], @{thms Meson.COMBI_def}),
    8.13 +   (["c_COMBK"], @{thms Meson.COMBK_def}),
    8.14 +   (["c_COMBB"], @{thms Meson.COMBB_def}),
    8.15 +   (["c_COMBC"], @{thms Meson.COMBC_def}),
    8.16 +   (["c_COMBS"], @{thms Meson.COMBS_def})]
    8.17  val optional_typed_helpers =
    8.18    [(["c_True", "c_False", "c_If"], @{thms True_or_False}),
    8.19     (["c_If"], @{thms if_True if_False})]