src/HOL/Tools/SMT/lethe_isar.ML
author wenzelm
Mon, 21 Jul 2025 16:21:37 +0200
changeset 82892 45107da819fc
parent 76183 8089593a364a
permissions -rw-r--r--
eliminate odd Unicode characters (amending e9f3b94eb6a0, b69e4da2604b, 8f0b2daa7eaa, 8d1e295aab70);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
76183
8089593a364a proper file headers;
wenzelm
parents: 75299
diff changeset
     1
(*  Title:      HOL/Tools/SMT/lethe_isar.ML
75299
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
     2
    Author:     Mathias Fleury, TU Muenchen
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
     3
    Author:     Jasmin Blanchette, TU Muenchen
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
     4
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
     5
LETHE proofs as generic ATP proofs for Isar proof reconstruction.
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
     6
*)
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
     7
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
     8
signature LETHE_ISAR =
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
     9
sig
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    10
  type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    11
  val atp_proof_of_veriT_proof: Proof.context -> term list -> thm list -> term list -> term ->
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    12
    (string * term) list -> int list -> int -> (int * string) list -> Lethe_Proof.lethe_step list ->
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    13
    (term, string) ATP_Proof.atp_step list
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    14
end;
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    15
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    16
structure Lethe_Isar: LETHE_ISAR =
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    17
struct
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    18
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    19
open ATP_Util
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    20
open ATP_Problem
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    21
open ATP_Proof
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    22
open ATP_Proof_Reconstruct
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    23
open SMTLIB_Interface
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    24
open SMTLIB_Isar
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    25
open Lethe_Proof
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    26
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    27
fun atp_proof_of_veriT_proof ctxt ll_defs rewrite_rules hyp_ts concl_t fact_helper_ts prem_ids
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    28
    conjecture_id fact_helper_ids =
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    29
  let
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    30
    fun steps_of (Lethe_Proof.Lethe_Step {id, rule, prems, concl, ...}) =
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    31
      let
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    32
        val concl' = postprocess_step_conclusion ctxt rewrite_rules ll_defs concl
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    33
        fun standard_step role = ((id, []), role, concl', rule, map (rpair []) prems)
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    34
      in
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    35
        if rule = input_rule then
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    36
          let
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    37
            val (_, id_num) = SMTLIB_Interface.role_and_index_of_assert_name id
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    38
            val ss = the_list (AList.lookup (op =) fact_helper_ids id_num)
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    39
          in
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    40
            (case distinguish_conjecture_and_hypothesis ss id_num conjecture_id prem_ids
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    41
                fact_helper_ts hyp_ts concl_t of
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    42
              NONE => []
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    43
            | SOME (role0, concl00) =>
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    44
              let
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    45
                val name0 = (id ^ "a", ss)
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    46
                val concl0 = unskolemize_names ctxt concl00
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    47
              in
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    48
                [(name0, role0, concl0, rule, []),
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    49
                 ((id, []), Plain, concl', rewrite_rule,
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    50
                  name0 :: normalizing_prems ctxt concl0)]
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    51
              end)
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    52
          end
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    53
        else
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    54
          [standard_step (if null prems then Lemma else Plain)]
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    55
      end
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    56
  in
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    57
    maps steps_of
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    58
  end
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    59
da591621d6ae split veriT reconstruction into Lethe and veriT part
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff changeset
    60
end;