# HG changeset patch # User blanchet # Date 1307385395 -7200 # Node ID 4ca344fe0aca75525dce65d3d8610d0381d2c7d2 # Parent f497a1e97d375b03f0f52d1210db6cf5acfe3b6f properly locate helpers whose constants have several entries in the helper table diff -r f497a1e97d37 -r 4ca344fe0aca src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Mon Jun 06 20:36:35 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_translate.ML Mon Jun 06 20:36:35 2011 +0200 @@ -1266,7 +1266,9 @@ (** Helper facts **) -(* The Boolean indicates that a fairly sound type encoding is needed. *) +(* The Boolean indicates that a fairly sound type encoding is needed. + "false" must precede "true" to ensure consistent numbering and a correct + mapping in Metis. *) val helper_table = [("COMBI", (false, @{thms Meson.COMBI_def})), ("COMBK", (false, @{thms Meson.COMBK_def})), @@ -1279,10 +1281,10 @@ equality helpers by default in Metis breaks a few existing proofs. *) (true, @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1] fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]})), + ("fFalse", (false, [@{lemma "~ fFalse" by (unfold fFalse_def) fast}])), ("fFalse", (true, @{thms True_or_False})), - ("fFalse", (false, [@{lemma "~ fFalse" by (unfold fFalse_def) fast}])), + ("fTrue", (false, [@{lemma "fTrue" by (unfold fTrue_def) fast}])), ("fTrue", (true, @{thms True_or_False})), - ("fTrue", (false, [@{lemma "fTrue" by (unfold fTrue_def) fast}])), ("fNot", (false, @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1] fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]})), diff -r f497a1e97d37 -r 4ca344fe0aca src/HOL/Tools/Metis/metis_translate.ML --- a/src/HOL/Tools/Metis/metis_translate.ML Mon Jun 06 20:36:35 2011 +0200 +++ b/src/HOL/Tools/Metis/metis_translate.ML Mon Jun 06 20:36:35 2011 +0200 @@ -329,7 +329,8 @@ else if String.isPrefix helper_prefix ident then case space_explode "_" ident of _ :: const :: j :: _ => - nth (AList.lookup (op =) helper_table const |> the |> snd) + nth (helper_table |> filter (curry (op =) const o fst) + |> maps (snd o snd)) (the (Int.fromString j) - 1) |> prepare_helper |> Isa_Raw |> some | _ => raise Fail ("malformed helper identifier " ^ quote ident)