author | wenzelm |
Mon, 21 Jul 2025 16:21:37 +0200 | |
changeset 82892 | 45107da819fc |
parent 76183 | 8089593a364a |
permissions | -rw-r--r-- |
76183 | 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; |