support lightweight tags in new Metis
authorblanchet
Wed Jun 01 10:29:43 2011 +0200 (2011-06-01)
changeset 431294301f1c123d6
parent 43128 a19826080596
child 43130 d73fc2e55308
support lightweight tags 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	Wed Jun 01 10:29:43 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Jun 01 10:29:43 2011 +0200
     1.3 @@ -66,7 +66,7 @@
     1.4    val type_decl_prefix : string
     1.5    val sym_decl_prefix : string
     1.6    val preds_sym_formula_prefix : string
     1.7 -  val tags_sym_formula_prefix : string
     1.8 +  val lightweight_tags_sym_formula_prefix : string
     1.9    val fact_prefix : string
    1.10    val conjecture_prefix : string
    1.11    val helper_prefix : string
    1.12 @@ -172,7 +172,7 @@
    1.13  val type_decl_prefix = "ty_"
    1.14  val sym_decl_prefix = "sy_"
    1.15  val preds_sym_formula_prefix = "psy_"
    1.16 -val tags_sym_formula_prefix = "tsy_"
    1.17 +val lightweight_tags_sym_formula_prefix = "tsy_"
    1.18  val fact_prefix = "fact_"
    1.19  val conjecture_prefix = "conj_"
    1.20  val helper_prefix = "help_"
    1.21 @@ -1665,11 +1665,11 @@
    1.22               intro_info, NONE)
    1.23    end
    1.24  
    1.25 -fun formula_lines_for_tags_sym_decl ctxt format conj_sym_kind nonmono_Ts
    1.26 -        type_sys n s (j, (s', T_args, T, pred_sym, ary, in_conj)) =
    1.27 +fun formula_lines_for_lightweight_tags_sym_decl ctxt format conj_sym_kind
    1.28 +        nonmono_Ts type_sys n s (j, (s', T_args, T, pred_sym, ary, in_conj)) =
    1.29    let
    1.30      val ident_base =
    1.31 -      tags_sym_formula_prefix ^ s ^
    1.32 +      lightweight_tags_sym_formula_prefix ^ s ^
    1.33        (if n > 1 then "_" ^ string_of_int j else "")
    1.34      val (kind, maybe_negate) =
    1.35        if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
    1.36 @@ -1749,8 +1749,8 @@
    1.37       | Lightweight =>
    1.38         let val n = length decls in
    1.39           (0 upto n - 1 ~~ decls)
    1.40 -         |> maps (formula_lines_for_tags_sym_decl ctxt format conj_sym_kind
    1.41 -                                                  nonmono_Ts type_sys n s)
    1.42 +         |> maps (formula_lines_for_lightweight_tags_sym_decl ctxt format
    1.43 +                      conj_sym_kind nonmono_Ts type_sys n s)
    1.44         end)
    1.45  
    1.46  fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
     2.1 --- a/src/HOL/Tools/Metis/metis_tactics.ML	Wed Jun 01 10:29:43 2011 +0200
     2.2 +++ b/src/HOL/Tools/Metis/metis_tactics.ML	Wed Jun 01 10:29:43 2011 +0200
     2.3 @@ -55,6 +55,28 @@
     2.4  fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th)
     2.5    | used_axioms _ _ = NONE
     2.6  
     2.7 +fun cterm_from_metis ctxt sym_tab tm =
     2.8 +  let val thy = Proof_Context.theory_of ctxt in
     2.9 +    tm |> hol_term_from_metis MX sym_tab ctxt
    2.10 +       |> Syntax.check_term
    2.11 +              (Proof_Context.set_mode Proof_Context.mode_schematic ctxt)
    2.12 +       |> cterm_of thy
    2.13 +  end
    2.14 +
    2.15 +(* Lightweight predicate type information comes in two flavors, "t = t'" and
    2.16 +   "t => t'", where "t" and "t'" are the same term modulo type tags.
    2.17 +   In Isabelle, type tags are stripped away, so we are left with "t = t" or
    2.18 +   "t => t". *)
    2.19 +fun lightweight_tags_sym_theorem_from_metis ctxt sym_tab mth =
    2.20 +  (case Metis_LiteralSet.toList (Metis_Thm.clause mth) of
    2.21 +     [(true, (_, [_, tm]))] =>
    2.22 +     tm |> cterm_from_metis ctxt sym_tab |> Thm.reflexive
    2.23 +     RS @{thm meta_eq_to_obj_eq}
    2.24 +   | [_, (_, tm)] =>
    2.25 +     tm |> Metis_Term.Fn |> cterm_from_metis ctxt sym_tab |> Thm.assume
    2.26 +   | _ => raise Fail "unexpected tags sym clause")
    2.27 +  |> Meson.make_meta_clause
    2.28 +
    2.29  val clause_params =
    2.30    {ordering = Metis_KnuthBendixOrder.default,
    2.31     orderLiterals = Metis_Clause.UnsignedLiteralOrder,
    2.32 @@ -88,6 +110,11 @@
    2.33        val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) ths
    2.34        val (mode, sym_tab, {axioms, old_skolems, ...}) =
    2.35          prepare_metis_problem ctxt mode type_sys cls ths
    2.36 +      val axioms =
    2.37 +        axioms |> map
    2.38 +            (fn (mth, SOME th) => (mth, th)
    2.39 +              | (mth, NONE) =>
    2.40 +                (mth, lightweight_tags_sym_theorem_from_metis ctxt sym_tab mth))
    2.41        val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS")
    2.42        val thms = map #1 axioms
    2.43        val _ = app (fn th => trace_msg ctxt (fn () => Metis_Thm.toString th)) thms
     3.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Wed Jun 01 10:29:43 2011 +0200
     3.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Wed Jun 01 10:29:43 2011 +0200
     3.3 @@ -15,7 +15,7 @@
     3.4    datatype mode = FO | HO | FT | MX
     3.5  
     3.6    type metis_problem =
     3.7 -    {axioms : (Metis_Thm.thm * thm) list,
     3.8 +    {axioms : (Metis_Thm.thm * thm option) list,
     3.9       tfrees : type_literal list,
    3.10       old_skolems : (string * term) list}
    3.11  
    3.12 @@ -236,7 +236,7 @@
    3.13  (* ------------------------------------------------------------------------- *)
    3.14  
    3.15  type metis_problem =
    3.16 -  {axioms : (Metis_Thm.thm * thm) list,
    3.17 +  {axioms : (Metis_Thm.thm * thm option) list,
    3.18     tfrees : type_literal list,
    3.19     old_skolems : (string * term) list}
    3.20  
    3.21 @@ -309,14 +309,17 @@
    3.22      (phi |> metis_literals_from_atp |> Metis_LiteralSet.fromList
    3.23           |> Metis_Thm.axiom,
    3.24       case try (unprefix conjecture_prefix) ident of
    3.25 -       SOME s => Meson.make_meta_clause (nth clauses (the (Int.fromString s)))
    3.26 +       SOME s =>
    3.27 +       SOME (Meson.make_meta_clause (nth clauses (the (Int.fromString s))))
    3.28       | NONE =>
    3.29 +       if String.isPrefix lightweight_tags_sym_formula_prefix ident then
    3.30 +         NONE
    3.31  (* FIXME: missing:
    3.32 -       if String.isPrefix helper_prefix then
    3.33 +       else if String.isPrefix helper_prefix then
    3.34           ...
    3.35 +*)
    3.36         else
    3.37 -*)
    3.38 -       TrueI)
    3.39 +         SOME TrueI)
    3.40    | metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula"
    3.41  
    3.42  val default_type_sys = Preds (Polymorphic, Nonmonotonic_Types, Lightweight)
    3.43 @@ -363,15 +366,15 @@
    3.44              hol_thm_to_fol is_conjecture ctxt mode (length axioms) old_skolems
    3.45                             metis_ith
    3.46          in
    3.47 -          {axioms = (mth, isa_ith) :: axioms,
    3.48 +          {axioms = (mth, SOME isa_ith) :: axioms,
    3.49             tfrees = union (op =) tfree_lits tfrees, old_skolems = old_skolems}
    3.50          end;
    3.51        fun add_type_thm (ith, mth) {axioms, tfrees, old_skolems} =
    3.52 -        {axioms = (mth, ith) :: axioms, tfrees = tfrees,
    3.53 +        {axioms = (mth, SOME ith) :: axioms, tfrees = tfrees,
    3.54           old_skolems = old_skolems}
    3.55        fun add_tfrees {axioms, tfrees, old_skolems} =
    3.56 -        {axioms =
    3.57 -           map (rpair TrueI o metis_of_tfree) (distinct (op =) tfrees) @ axioms,
    3.58 +        {axioms = map (rpair (SOME TrueI) o metis_of_tfree)
    3.59 +                      (distinct (op =) tfrees) @ axioms,
    3.60           tfrees = tfrees, old_skolems = old_skolems}
    3.61        val problem =
    3.62          {axioms = [], tfrees = init_tfrees ctxt, old_skolems = []}