fixed type helper indices in new Metis
authorblanchet
Mon Jun 06 20:36:35 2011 +0200 (2011-06-06)
changeset 43194ef3ff8856245
parent 43193 e11bd628f1a5
child 43195 6dc58b3b73b5
fixed type helper indices in new Metis
src/HOL/Tools/ATP/atp_translate.ML
src/HOL/Tools/Metis/metis_tactics.ML
src/HOL/Tools/Metis/metis_translate.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Jun 06 20:36:35 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Mon Jun 06 20:36:35 2011 +0200
     1.3 @@ -127,7 +127,7 @@
     1.4    val translate_atp_fact :
     1.5      Proof.context -> format -> type_sys -> bool -> (string * locality) * thm
     1.6      -> translated_formula option * ((string * locality) * thm)
     1.7 -  val helper_table : (string * (bool * thm list)) list
     1.8 +  val helper_table : ((string * bool) * thm list) list
     1.9    val should_specialize_helper : type_sys -> term -> bool
    1.10    val tfree_classes_of_terms : term list -> string list
    1.11    val tvar_classes_of_terms : term list -> string list
    1.12 @@ -1253,42 +1253,38 @@
    1.13  
    1.14  (** Helper facts **)
    1.15  
    1.16 -(* The Boolean indicates that a fairly sound type encoding is needed.
    1.17 -   "false" must precede "true" to ensure consistent numbering and a correct
    1.18 -   mapping in Metis. *)
    1.19 +(* The Boolean indicates that a fairly sound type encoding is needed. *)
    1.20  val helper_table =
    1.21 -  [("COMBI", (false, @{thms Meson.COMBI_def})),
    1.22 -   ("COMBK", (false, @{thms Meson.COMBK_def})),
    1.23 -   ("COMBB", (false, @{thms Meson.COMBB_def})),
    1.24 -   ("COMBC", (false, @{thms Meson.COMBC_def})),
    1.25 -   ("COMBS", (false, @{thms Meson.COMBS_def})),
    1.26 -   ("fequal",
    1.27 +  [(("COMBI", false), @{thms Meson.COMBI_def}),
    1.28 +   (("COMBK", false), @{thms Meson.COMBK_def}),
    1.29 +   (("COMBB", false), @{thms Meson.COMBB_def}),
    1.30 +   (("COMBC", false), @{thms Meson.COMBC_def}),
    1.31 +   (("COMBS", false), @{thms Meson.COMBS_def}),
    1.32 +   (("fequal", true),
    1.33      (* This is a lie: Higher-order equality doesn't need a sound type encoding.
    1.34         However, this is done so for backward compatibility: Including the
    1.35         equality helpers by default in Metis breaks a few existing proofs. *)
    1.36 -    (true, @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
    1.37 -                  fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]})),
    1.38 -   ("fFalse", (false, [@{lemma "~ fFalse" by (unfold fFalse_def) fast}])),
    1.39 -   ("fFalse", (true, @{thms True_or_False})),
    1.40 -   ("fTrue", (false, [@{lemma "fTrue" by (unfold fTrue_def) fast}])),
    1.41 -   ("fTrue", (true, @{thms True_or_False})),
    1.42 -   ("fNot",
    1.43 -    (false, @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
    1.44 -                   fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]})),
    1.45 -   ("fconj",
    1.46 -    (false,
    1.47 -     @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q"
    1.48 -         by (unfold fconj_def) fast+})),
    1.49 -   ("fdisj",
    1.50 -    (false,
    1.51 -     @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q"
    1.52 -         by (unfold fdisj_def) fast+})),
    1.53 -   ("fimplies",
    1.54 -    (false, @{lemma "P | fimplies P Q" "~ Q | fimplies P Q"
    1.55 -                    "~ fimplies P Q | ~ P | Q"
    1.56 -                by (unfold fimplies_def) fast+})),
    1.57 -   ("If", (true, @{thms if_True if_False True_or_False}))]
    1.58 -  |> map (apsnd (apsnd (map zero_var_indexes)))
    1.59 +    @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
    1.60 +           fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
    1.61 +   (("fFalse", false), [@{lemma "~ fFalse" by (unfold fFalse_def) fast}]),
    1.62 +   (("fFalse", true), @{thms True_or_False}),
    1.63 +   (("fTrue", false), [@{lemma "fTrue" by (unfold fTrue_def) fast}]),
    1.64 +   (("fTrue", true), @{thms True_or_False}),
    1.65 +   (("fNot", false),
    1.66 +    @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
    1.67 +           fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
    1.68 +   (("fconj", false),
    1.69 +    @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q"
    1.70 +        by (unfold fconj_def) fast+}),
    1.71 +   (("fdisj", false),
    1.72 +    @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q"
    1.73 +        by (unfold fdisj_def) fast+}),
    1.74 +   (("fimplies", false),
    1.75 +    @{lemma "P | fimplies P Q" "~ Q | fimplies P Q"
    1.76 +            "~ fimplies P Q | ~ P | Q"
    1.77 +        by (unfold fimplies_def) fast+}),
    1.78 +   (("If", true), @{thms if_True if_False True_or_False})]
    1.79 +  |> map (apsnd (map zero_var_indexes))
    1.80  
    1.81  val type_tag = `make_fixed_const type_tag_name
    1.82  
    1.83 @@ -1331,7 +1327,7 @@
    1.84        val fairly_sound = is_type_sys_fairly_sound type_sys
    1.85      in
    1.86        helper_table
    1.87 -      |> maps (fn (helper_s, (needs_fairly_sound, ths)) =>
    1.88 +      |> maps (fn ((helper_s, needs_fairly_sound), ths) =>
    1.89                    if helper_s <> unmangled_s orelse
    1.90                       (needs_fairly_sound andalso not fairly_sound) then
    1.91                      []
     2.1 --- a/src/HOL/Tools/Metis/metis_tactics.ML	Mon Jun 06 20:36:35 2011 +0200
     2.2 +++ b/src/HOL/Tools/Metis/metis_tactics.ML	Mon Jun 06 20:36:35 2011 +0200
     2.3 @@ -195,7 +195,7 @@
     2.4  fun generic_metis_tac modes type_sys ctxt ths i st0 =
     2.5    let
     2.6      val _ = trace_msg ctxt (fn () =>
     2.7 -        "Metis called with theorems " ^
     2.8 +        "Metis called with theorems\n" ^
     2.9          cat_lines (map (Display.string_of_thm ctxt) ths))
    2.10      fun tac clause = resolve_tac (FOL_SOLVE type_sys modes ctxt clause ths) 1
    2.11    in
     3.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Mon Jun 06 20:36:35 2011 +0200
     3.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Mon Jun 06 20:36:35 2011 +0200
     3.3 @@ -327,12 +327,14 @@
     3.4           String.isPrefix lightweight_tags_sym_formula_prefix ident then
     3.5          Isa_Reflexive_or_Trivial |> some
     3.6        else if String.isPrefix helper_prefix ident then
     3.7 -        case space_explode "_" ident  of
     3.8 -          _ :: const :: j :: _ =>
     3.9 -          nth (helper_table |> filter (curry (op =) const o fst)
    3.10 -                            |> maps (snd o snd))
    3.11 +        case (String.isSuffix typed_helper_suffix ident,
    3.12 +              space_explode "_" ident) of
    3.13 +          (needs_fairly_sound, _ :: const :: j :: _) =>
    3.14 +          nth ((const, needs_fairly_sound)
    3.15 +               |> AList.lookup (op =) helper_table |> the)
    3.16                (the (Int.fromString j) - 1)
    3.17 -          |> prepare_helper |> Isa_Raw |> some
    3.18 +          |> prepare_helper
    3.19 +          |> Isa_Raw |> some
    3.20          | _ => raise Fail ("malformed helper identifier " ^ quote ident)
    3.21        else case try (unprefix conjecture_prefix) ident of
    3.22          SOME s =>
    3.23 @@ -424,8 +426,8 @@
    3.24            let
    3.25              val helper_ths =
    3.26                helper_table
    3.27 -              |> filter (is_used o prefix const_prefix o fst)
    3.28 -              |> maps (fn (_, (needs_full_types, thms)) =>
    3.29 +              |> filter (is_used o prefix const_prefix o fst o fst)
    3.30 +              |> maps (fn ((_, needs_full_types), thms) =>
    3.31                            if needs_full_types andalso mode <> FT then []
    3.32                            else map (`prepare_helper) thms)
    3.33            in problem |> fold (add_thm false) helper_ths end