Quelle lethe_isar.ML Sprache: SML

(*  Title:      HOL/Tools/SMT/lethe_isar.ML
    Author:     Mathias Fleury, TU Muenchen
    Author:     Jasmin Blanchette, TU Muenchen

LETHE proofs as generic ATP proofs for Isar proof reconstruction.
*)

signature LETHE_ISAR =
sig
  type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step
  val atp_proof_of_veriT_proof: Proof.context -> term list -> thm list -> term list -> term ->
    (string * term) list -> int list -> int -> (int * string) list -> Lethe_Proof.lethe_step list ->
    (term, string) ATP_Proof.atp_step list
end;

structure Lethe_Isar: LETHE_ISAR =
struct

open ATP_Util
open ATP_Problem
open ATP_Proof
open ATP_Proof_Reconstruct
open SMTLIB_Interface
open SMTLIB_Isar
open Lethe_Proof

fun atp_proof_of_veriT_proof ctxt ll_defs rewrite_rules hyp_ts concl_t fact_helper_ts prem_ids
    conjecture_id fact_helper_ids =
  let
    fun steps_of (Lethe_Proof.Lethe_Step {id, rule, prems, concl, ...}) =
      let
        val concl' = postprocess_step_conclusion ctxt rewrite_rules ll_defs concl
        fun standard_step role = ((id, []), role, concl', rule, map (rpair []) prems)
      in
        if rule = input_rule then
          let
            val (_, id_num) = SMTLIB_Interface.role_and_index_of_assert_name id
            val ss = the_list (AList.lookup (op =) fact_helper_ids id_num)
          in
            (case distinguish_conjecture_and_hypothesis ss id_num conjecture_id prem_ids
                fact_helper_ts hyp_ts concl_t of
              NONE => []
            | SOME (role0, concl00) =>
              let
                val name0 = (id ^ "a", ss)
                val concl0 = unskolemize_names ctxt concl00
              in
                [(name0, role0, concl0, rule, []),
                 ((id, []), Plain, concl', rewrite_rule,
                  name0 :: normalizing_prems ctxt concl0)]
              end)
          end
        else
          [standard_step (if null prems then Lemma else Plain)]
      end
  in
    maps steps_of
  end

end;

quality100%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.