author | Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de> |
Mon, 14 Dec 2020 21:02:57 +0100 | |
changeset 72908 | 6a26a955308e |
parent 72513 | 75f5c63f6cfa |
child 75268 | 73650a19591d |
permissions | -rw-r--r-- |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
1 |
(* Title: HOL/Tools/SMT/verit_replay_methods.ML |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
2 |
Author: Mathias Fleury, MPII, JKU |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
3 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
4 |
Proof method for replaying veriT proofs. |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
5 |
*) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
6 |
|
72459
15fc6320da68
reconstruction of veriT proofs in NEWS
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72458
diff
changeset
|
7 |
signature VERIT_REPLAY_METHODS = |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
8 |
sig |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
9 |
(*methods for verit proof rules*) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
10 |
val method_for: string -> Proof.context -> thm list -> term list -> term Symtab.table -> |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
11 |
(string * term) list -> term -> thm |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
12 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
13 |
val requires_subproof_assms : string list -> string -> bool |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
14 |
val requires_local_input: string list -> string -> bool |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
15 |
val eq_congruent_pred: Proof.context -> 'a -> term -> thm |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
16 |
val discharge: Proof.context -> thm list -> term -> thm |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
17 |
end; |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
18 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
19 |
|
72459
15fc6320da68
reconstruction of veriT proofs in NEWS
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72458
diff
changeset
|
20 |
structure Verit_Replay_Methods: VERIT_REPLAY_METHODS = |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
21 |
struct |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
22 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
23 |
(*Some general comments on the proof format: |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
24 |
1. Double negations are not always removed. This means for example that the equivalence rules |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
25 |
cannot assume that the double negations have already been removed. Therefore, we match the |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
26 |
term, instantiate the theorem, then use simp (to remove double negations), and finally use |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
27 |
assumption. |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
28 |
2. The reconstruction for rule forall_inst is buggy and tends to be very fragile, because the rule |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
29 |
is doing much more that is supposed to do. Moreover types can make trivial goals (for the |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
30 |
boolean structure) impossible to prove. |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
31 |
3. Duplicate literals are sometimes removed, mostly by the SAT solver. |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
32 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
33 |
Rules unsupported on purpose: |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
34 |
* Distinct_Elim, XOR, let (we don't need them). |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
35 |
* deep_skolemize (because it is not clear if verit still generates using it). |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
36 |
*) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
37 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
38 |
datatype verit_rule = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
39 |
False | True | |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
40 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
41 |
(*input: a repeated (normalized) assumption of assumption of in a subproof*) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
42 |
Normalized_Input | Local_Input | |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
43 |
(*Subproof:*) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
44 |
Subproof | |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
45 |
(*Conjunction:*) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
46 |
And | Not_And | And_Pos | And_Neg | |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
47 |
(*Disjunction""*) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
48 |
Or | Or_Pos | Not_Or | Or_Neg | |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
49 |
(*Disjunction:*) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
50 |
Implies | Implies_Neg1 | Implies_Neg2 | Implies_Pos | Not_Implies1 | Not_Implies2 | |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
51 |
(*Equivalence:*) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
52 |
Equiv_neg1 | Equiv_pos1 | Equiv_pos2 | Equiv_neg2 | Not_Equiv1 | Not_Equiv2 | Equiv1 | Equiv2 | |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
53 |
(*If-then-else:*) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
54 |
ITE_Pos1 | ITE_Pos2 | ITE_Neg1 | ITE_Neg2 | Not_ITE1 | Not_ITE2 | ITE_Intro | ITE1 | ITE2 | |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
55 |
(*Equality:*) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
56 |
Eq_Congruent | Eq_Reflexive | Eq_Transitive | Eq_Congruent_Pred | Trans | Refl | Cong | |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
57 |
(*Arithmetics:*) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
58 |
LA_Disequality | LA_Generic | LA_Tautology | LIA_Generic | LA_Totality | LA_RW_Eq | |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
59 |
NLA_Generic | |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
60 |
(*Quantifiers:*) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
61 |
Forall_Inst | Qnt_Rm_Unused | Qnt_Join | Onepoint | Bind | Skolem_Forall | Skolem_Ex | |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
62 |
(*Resolution:*) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
63 |
Theory_Resolution | Resolution | |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
64 |
(*Temporary rules, that the verit developpers want to remove:*) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
65 |
AC_Simp | |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
66 |
Bfun_Elim | |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
67 |
Qnt_CNF | |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
68 |
(*Used to introduce skolem constants*) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
69 |
Definition | |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
70 |
(*Former cong rules*) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
71 |
Bool_Simplify | Or_Simplify | Not_Simplify | And_Simplify | Equiv_Simplify | |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
72 |
Implies_Simplify | Connective_Def | Minus_Simplify | Comp_Simplify | |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
73 |
Eq_Simplify | ITE_Simplify | Sum_Simplify | Prod_Simplify | |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
74 |
Qnt_Simplify | Not_Not | Tautological_Clause | Duplicate_Literals | |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
75 |
(*Unsupported rule*) |
72908
6a26a955308e
improve and activate compression for veriT proof reconstruction
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72513
diff
changeset
|
76 |
Unsupported | |
6a26a955308e
improve and activate compression for veriT proof reconstruction
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72513
diff
changeset
|
77 |
(*For compression*) |
6a26a955308e
improve and activate compression for veriT proof reconstruction
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72513
diff
changeset
|
78 |
Theory_Resolution2 |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
79 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
80 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
81 |
fun verit_rule_of "bind" = Bind |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
82 |
| verit_rule_of "cong" = Cong |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
83 |
| verit_rule_of "refl" = Refl |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
84 |
| verit_rule_of "equiv1" = Equiv1 |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
85 |
| verit_rule_of "equiv2" = Equiv2 |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
86 |
| verit_rule_of "equiv_pos1" = Equiv_pos1 |
72908
6a26a955308e
improve and activate compression for veriT proof reconstruction
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72513
diff
changeset
|
87 |
(*Equiv_pos2 covered below*) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
88 |
| verit_rule_of "equiv_neg1" = Equiv_neg1 |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
89 |
| verit_rule_of "equiv_neg2" = Equiv_neg2 |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
90 |
| verit_rule_of "sko_forall" = Skolem_Forall |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
91 |
| verit_rule_of "sko_ex" = Skolem_Ex |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
92 |
| verit_rule_of "eq_reflexive" = Eq_Reflexive |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
93 |
| verit_rule_of "forall_inst" = Forall_Inst |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
94 |
| verit_rule_of "implies_pos" = Implies_Pos |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
95 |
| verit_rule_of "or" = Or |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
96 |
| verit_rule_of "not_or" = Not_Or |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
97 |
| verit_rule_of "resolution" = Resolution |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
98 |
| verit_rule_of "trans" = Trans |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
99 |
| verit_rule_of "false" = False |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
100 |
| verit_rule_of "ac_simp" = AC_Simp |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
101 |
| verit_rule_of "and" = And |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
102 |
| verit_rule_of "not_and" = Not_And |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
103 |
| verit_rule_of "and_pos" = And_Pos |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
104 |
| verit_rule_of "and_neg" = And_Neg |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
105 |
| verit_rule_of "or_pos" = Or_Pos |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
106 |
| verit_rule_of "or_neg" = Or_Neg |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
107 |
| verit_rule_of "not_equiv1" = Not_Equiv1 |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
108 |
| verit_rule_of "not_equiv2" = Not_Equiv2 |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
109 |
| verit_rule_of "not_implies1" = Not_Implies1 |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
110 |
| verit_rule_of "not_implies2" = Not_Implies2 |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
111 |
| verit_rule_of "implies_neg1" = Implies_Neg1 |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
112 |
| verit_rule_of "implies_neg2" = Implies_Neg2 |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
113 |
| verit_rule_of "implies" = Implies |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
114 |
| verit_rule_of "bfun_elim" = Bfun_Elim |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
115 |
| verit_rule_of "ite1" = ITE1 |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
116 |
| verit_rule_of "ite2" = ITE2 |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
117 |
| verit_rule_of "not_ite1" = Not_ITE1 |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
118 |
| verit_rule_of "not_ite2" = Not_ITE2 |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
119 |
| verit_rule_of "ite_pos1" = ITE_Pos1 |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
120 |
| verit_rule_of "ite_pos2" = ITE_Pos2 |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
121 |
| verit_rule_of "ite_neg1" = ITE_Neg1 |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
122 |
| verit_rule_of "ite_neg2" = ITE_Neg2 |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
123 |
| verit_rule_of "la_disequality" = LA_Disequality |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
124 |
| verit_rule_of "lia_generic" = LIA_Generic |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
125 |
| verit_rule_of "la_generic" = LA_Generic |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
126 |
| verit_rule_of "la_tautology" = LA_Tautology |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
127 |
| verit_rule_of "la_totality" = LA_Totality |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
128 |
| verit_rule_of "la_rw_eq"= LA_RW_Eq |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
129 |
| verit_rule_of "nla_generic"= NLA_Generic |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
130 |
| verit_rule_of "eq_transitive" = Eq_Transitive |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
131 |
| verit_rule_of "qnt_rm_unused" = Qnt_Rm_Unused |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
132 |
| verit_rule_of "onepoint" = Onepoint |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
133 |
| verit_rule_of "qnt_join" = Qnt_Join |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
134 |
| verit_rule_of "subproof" = Subproof |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
135 |
| verit_rule_of "bool_simplify" = Bool_Simplify |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
136 |
| verit_rule_of "or_simplify" = Or_Simplify |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
137 |
| verit_rule_of "ite_simplify" = ITE_Simplify |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
138 |
| verit_rule_of "and_simplify" = And_Simplify |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
139 |
| verit_rule_of "not_simplify" = Not_Simplify |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
140 |
| verit_rule_of "equiv_simplify" = Equiv_Simplify |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
141 |
| verit_rule_of "eq_simplify" = Eq_Simplify |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
142 |
| verit_rule_of "implies_simplify" = Implies_Simplify |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
143 |
| verit_rule_of "connective_def" = Connective_Def |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
144 |
| verit_rule_of "minus_simplify" = Minus_Simplify |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
145 |
| verit_rule_of "sum_simplify" = Sum_Simplify |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
146 |
| verit_rule_of "prod_simplify" = Prod_Simplify |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
147 |
| verit_rule_of "comp_simplify" = Comp_Simplify |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
148 |
| verit_rule_of "qnt_simplify" = Qnt_Simplify |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
149 |
| verit_rule_of "tautology" = Tautological_Clause |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
150 |
| verit_rule_of "qnt_cnf" = Qnt_CNF |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
151 |
| verit_rule_of r = |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
152 |
if r = Verit_Proof.normalized_input_rule then Normalized_Input |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
153 |
else if r = Verit_Proof.local_input_rule then Local_Input |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
154 |
else if r = Verit_Proof.veriT_def then Definition |
72513
75f5c63f6cfa
better handling of skolemization for Isar reconstruction in Sledgehammer for veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72459
diff
changeset
|
155 |
else if r = Verit_Proof.not_not_rule then Not_Not |
75f5c63f6cfa
better handling of skolemization for Isar reconstruction in Sledgehammer for veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72459
diff
changeset
|
156 |
else if r = Verit_Proof.contract_rule then Duplicate_Literals |
75f5c63f6cfa
better handling of skolemization for Isar reconstruction in Sledgehammer for veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72459
diff
changeset
|
157 |
else if r = Verit_Proof.ite_intro_rule then ITE_Intro |
75f5c63f6cfa
better handling of skolemization for Isar reconstruction in Sledgehammer for veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72459
diff
changeset
|
158 |
else if r = Verit_Proof.eq_congruent_rule then Eq_Congruent |
75f5c63f6cfa
better handling of skolemization for Isar reconstruction in Sledgehammer for veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72459
diff
changeset
|
159 |
else if r = Verit_Proof.eq_congruent_pred_rule then Eq_Congruent_Pred |
72908
6a26a955308e
improve and activate compression for veriT proof reconstruction
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72513
diff
changeset
|
160 |
else if r = Verit_Proof.theory_resolution2_rule then Theory_Resolution2 |
6a26a955308e
improve and activate compression for veriT proof reconstruction
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72513
diff
changeset
|
161 |
else if r = Verit_Proof.th_resolution_rule then Theory_Resolution |
6a26a955308e
improve and activate compression for veriT proof reconstruction
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72513
diff
changeset
|
162 |
else if r = Verit_Proof.equiv_pos2_rule then Equiv_pos2 |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
163 |
else (@{print} ("Unsupport rule", r); Unsupported) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
164 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
165 |
fun string_of_verit_rule Bind = "Bind" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
166 |
| string_of_verit_rule Cong = "Cong" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
167 |
| string_of_verit_rule Refl = "Refl" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
168 |
| string_of_verit_rule Equiv1 = "Equiv1" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
169 |
| string_of_verit_rule Equiv2 = "Equiv2" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
170 |
| string_of_verit_rule Equiv_pos1 = "Equiv_pos1" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
171 |
| string_of_verit_rule Equiv_pos2 = "Equiv_pos2" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
172 |
| string_of_verit_rule Equiv_neg1 = "Equiv_neg1" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
173 |
| string_of_verit_rule Equiv_neg2 = "Equiv_neg2" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
174 |
| string_of_verit_rule Skolem_Forall = "Skolem_Forall" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
175 |
| string_of_verit_rule Skolem_Ex = "Skolem_Ex" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
176 |
| string_of_verit_rule Eq_Reflexive = "Eq_Reflexive" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
177 |
| string_of_verit_rule Theory_Resolution = "Theory_Resolution" |
72908
6a26a955308e
improve and activate compression for veriT proof reconstruction
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72513
diff
changeset
|
178 |
| string_of_verit_rule Theory_Resolution2 = "Theory_Resolution2" |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
179 |
| string_of_verit_rule Forall_Inst = "forall_inst" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
180 |
| string_of_verit_rule Or = "Or" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
181 |
| string_of_verit_rule Not_Or = "Not_Or" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
182 |
| string_of_verit_rule Resolution = "Resolution" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
183 |
| string_of_verit_rule Eq_Congruent = "eq_congruent" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
184 |
| string_of_verit_rule Trans = "trans" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
185 |
| string_of_verit_rule False = "false" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
186 |
| string_of_verit_rule And = "and" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
187 |
| string_of_verit_rule And_Pos = "and_pos" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
188 |
| string_of_verit_rule Not_And = "not_and" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
189 |
| string_of_verit_rule And_Neg = "and_neg" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
190 |
| string_of_verit_rule Or_Pos = "or_pos" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
191 |
| string_of_verit_rule Or_Neg = "or_neg" |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
192 |
| string_of_verit_rule AC_Simp = "ac_simp" |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
193 |
| string_of_verit_rule Not_Equiv1 = "not_equiv1" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
194 |
| string_of_verit_rule Not_Equiv2 = "not_equiv2" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
195 |
| string_of_verit_rule Not_Implies1 = "not_implies1" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
196 |
| string_of_verit_rule Not_Implies2 = "not_implies2" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
197 |
| string_of_verit_rule Implies_Neg1 = "implies_neg1" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
198 |
| string_of_verit_rule Implies_Neg2 = "implies_neg2" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
199 |
| string_of_verit_rule Implies = "implies" |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
200 |
| string_of_verit_rule Bfun_Elim = "bfun_elim" |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
201 |
| string_of_verit_rule ITE1 = "ite1" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
202 |
| string_of_verit_rule ITE2 = "ite2" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
203 |
| string_of_verit_rule Not_ITE1 = "not_ite1" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
204 |
| string_of_verit_rule Not_ITE2 = "not_ite2" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
205 |
| string_of_verit_rule ITE_Pos1 = "ite_pos1" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
206 |
| string_of_verit_rule ITE_Pos2 = "ite_pos2" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
207 |
| string_of_verit_rule ITE_Neg1 = "ite_neg1" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
208 |
| string_of_verit_rule ITE_Neg2 = "ite_neg2" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
209 |
| string_of_verit_rule ITE_Intro = "ite_intro" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
210 |
| string_of_verit_rule LA_Disequality = "la_disequality" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
211 |
| string_of_verit_rule LA_Generic = "la_generic" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
212 |
| string_of_verit_rule LIA_Generic = "lia_generic" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
213 |
| string_of_verit_rule LA_Tautology = "la_tautology" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
214 |
| string_of_verit_rule LA_RW_Eq = "la_rw_eq" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
215 |
| string_of_verit_rule LA_Totality = "LA_Totality" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
216 |
| string_of_verit_rule NLA_Generic = "nla_generic" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
217 |
| string_of_verit_rule Eq_Transitive = "eq_transitive" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
218 |
| string_of_verit_rule Qnt_Rm_Unused = "qnt_remove_unused" |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
219 |
| string_of_verit_rule Onepoint = "onepoint" |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
220 |
| string_of_verit_rule Qnt_Join = "qnt_join" |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
221 |
| string_of_verit_rule Eq_Congruent_Pred = "eq_congruent_pred" |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
222 |
| string_of_verit_rule Normalized_Input = Verit_Proof.normalized_input_rule |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
223 |
| string_of_verit_rule Local_Input = Verit_Proof.local_input_rule |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
224 |
| string_of_verit_rule Subproof = "subproof" |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
225 |
| string_of_verit_rule Bool_Simplify = "bool_simplify" |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
226 |
| string_of_verit_rule Equiv_Simplify = "equiv_simplify" |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
227 |
| string_of_verit_rule Eq_Simplify = "eq_simplify" |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
228 |
| string_of_verit_rule Not_Simplify = "not_simplify" |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
229 |
| string_of_verit_rule And_Simplify = "and_simplify" |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
230 |
| string_of_verit_rule Or_Simplify = "or_simplify" |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
231 |
| string_of_verit_rule ITE_Simplify = "ite_simplify" |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
232 |
| string_of_verit_rule Implies_Simplify = "implies_simplify" |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
233 |
| string_of_verit_rule Connective_Def = "connective_def" |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
234 |
| string_of_verit_rule Minus_Simplify = "minus_simplify" |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
235 |
| string_of_verit_rule Sum_Simplify = "sum_simplify" |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
236 |
| string_of_verit_rule Prod_Simplify = "prod_simplify" |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
237 |
| string_of_verit_rule Comp_Simplify = "comp_simplify" |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
238 |
| string_of_verit_rule Qnt_Simplify = "qnt_simplify" |
72513
75f5c63f6cfa
better handling of skolemization for Isar reconstruction in Sledgehammer for veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72459
diff
changeset
|
239 |
| string_of_verit_rule Not_Not = Verit_Proof.not_not_rule |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
240 |
| string_of_verit_rule Tautological_Clause = "tautology" |
72513
75f5c63f6cfa
better handling of skolemization for Isar reconstruction in Sledgehammer for veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72459
diff
changeset
|
241 |
| string_of_verit_rule Duplicate_Literals = Verit_Proof.contract_rule |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
242 |
| string_of_verit_rule Qnt_CNF = "qnt_cnf" |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
243 |
| string_of_verit_rule r = "Unknown rule: " ^ \<^make_string> r |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
244 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
245 |
fun replay_error ctxt msg rule thms t = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
246 |
SMT_Replay_Methods.replay_error ctxt msg (string_of_verit_rule rule) thms t |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
247 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
248 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
249 |
(* utility function *) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
250 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
251 |
fun eqsubst_all ctxt thms = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
252 |
K ((REPEAT o HEADGOAL) (EqSubst.eqsubst_asm_tac ctxt [0] thms)) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
253 |
THEN' K ((REPEAT o HEADGOAL) (EqSubst.eqsubst_tac ctxt [0] thms)) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
254 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
255 |
fun simplify_tac ctxt thms = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
256 |
ctxt |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
257 |
|> empty_simpset |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
258 |
|> put_simpset HOL_basic_ss |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
259 |
|> (fn ctxt => ctxt addsimps @{thms simp_thms} addsimps thms) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
260 |
|> Simplifier.asm_full_simp_tac |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
261 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
262 |
(* sko_forall requires the assumptions to be able to prove the equivalence in case of double |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
263 |
skolemization. See comment below. *) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
264 |
fun requires_subproof_assms _ t = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
265 |
member (op =) ["refl", "sko_forall", "sko_ex", "cong"] t |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
266 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
267 |
fun requires_local_input _ t = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
268 |
member (op =) [Verit_Proof.local_input_rule] t |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
269 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
270 |
(*This is a weaker simplification form. It is weaker, but is also less likely to loop*) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
271 |
fun partial_simplify_tac ctxt thms = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
272 |
ctxt |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
273 |
|> empty_simpset |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
274 |
|> put_simpset HOL_basic_ss |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
275 |
|> (fn ctxt => ctxt addsimps @{thms simp_thms} addsimps thms) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
276 |
|> Simplifier.full_simp_tac |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
277 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
278 |
val try_provers = SMT_Replay_Methods.try_provers "verit" |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
279 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
280 |
fun TRY' tac = fn i => TRY (tac i) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
281 |
fun REPEAT' tac = fn i => REPEAT (tac i) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
282 |
fun REPEAT_CHANGED tac = fn i => REPEAT (CHANGED (tac i)) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
283 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
284 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
285 |
(* Bind *) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
286 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
287 |
(*The bind rule is non-obvious due to the handling of quantifiers: |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
288 |
"\<And>x y a. x = y ==> (\<forall>b. P a b x) \<longleftrightarrow> (\<forall>b. P' a b y)" |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
289 |
------------------------------------------------------ |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
290 |
\<forall>a. (\<forall>b x. P a b x) \<longleftrightarrow> (\<forall>b y. P' a b y) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
291 |
is a valid application.*) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
292 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
293 |
val bind_thms = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
294 |
[@{lemma \<open>(\<And>x x'. x = x' \<Longrightarrow> P x = Q x') \<Longrightarrow> (\<forall>x. P x) = (\<forall>y. Q y)\<close> by blast}, |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
295 |
@{lemma \<open>(\<And>x x'. x = x' \<Longrightarrow> P x = Q x') \<Longrightarrow> (\<exists>x. P x) = (\<exists>y. Q y)\<close> by blast}, |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
296 |
@{lemma \<open>(\<And>x x'. x = x' \<Longrightarrow> P x = Q x') \<Longrightarrow> (\<exists>x. P x = Q x)\<close> by blast}, |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
297 |
@{lemma \<open>(\<And>x x'. x = x' \<Longrightarrow> P x = Q x') \<Longrightarrow> (\<forall>x. P x = Q x)\<close> by blast}] |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
298 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
299 |
val bind_thms_same_name = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
300 |
[@{lemma \<open>(\<And>x. P x = Q x) \<Longrightarrow> (\<forall>x. P x) = (\<forall>y. Q y)\<close> by blast}, |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
301 |
@{lemma \<open>(\<And>x. P x = Q x) \<Longrightarrow> (\<exists>x. P x) = (\<exists>y. Q y)\<close> by blast}, |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
302 |
@{lemma \<open>(\<And>x. P x = Q x) \<Longrightarrow> (\<exists>x. P x = Q x)\<close> by blast}, |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
303 |
@{lemma \<open>(\<And>x. P x = Q x) \<Longrightarrow> (\<forall>x. P x = Q x)\<close> by blast}] |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
304 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
305 |
fun extract_quantified_names_q (_ $ Abs (name, _, t)) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
306 |
apfst (curry (op ::) name) (extract_quantified_names_q t) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
307 |
| extract_quantified_names_q t = ([], t) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
308 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
309 |
fun extract_forall_quantified_names_q (Const(\<^const_name>\<open>HOL.All\<close>, _) $ Abs (name, ty, t)) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
310 |
(name, ty) :: (extract_forall_quantified_names_q t) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
311 |
| extract_forall_quantified_names_q _ = [] |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
312 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
313 |
fun extract_all_forall_quantified_names_q (Const(\<^const_name>\<open>HOL.All\<close>, _) $ Abs (name, _, t)) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
314 |
name :: (extract_all_forall_quantified_names_q t) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
315 |
| extract_all_forall_quantified_names_q (t $ u) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
316 |
extract_all_forall_quantified_names_q t @ extract_all_forall_quantified_names_q u |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
317 |
| extract_all_forall_quantified_names_q _ = [] |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
318 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
319 |
val extract_quantified_names_ba = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
320 |
SMT_Replay_Methods.dest_prop |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
321 |
#> extract_quantified_names_q |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
322 |
##> HOLogic.dest_eq |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
323 |
##> fst |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
324 |
##> extract_quantified_names_q |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
325 |
##> fst |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
326 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
327 |
val extract_quantified_names = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
328 |
extract_quantified_names_ba |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
329 |
#> (op @) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
330 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
331 |
val extract_all_forall_quantified_names = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
332 |
SMT_Replay_Methods.dest_prop |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
333 |
#> HOLogic.dest_eq |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
334 |
#> fst |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
335 |
#> extract_all_forall_quantified_names_q |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
336 |
|
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
337 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
338 |
fun extract_all_exists_quantified_names_q (Const(\<^const_name>\<open>HOL.Ex\<close>, _) $ Abs (name, _, t)) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
339 |
name :: (extract_all_exists_quantified_names_q t) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
340 |
| extract_all_exists_quantified_names_q (t $ u) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
341 |
extract_all_exists_quantified_names_q t @ extract_all_exists_quantified_names_q u |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
342 |
| extract_all_exists_quantified_names_q _ = [] |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
343 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
344 |
val extract_all_exists_quantified_names = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
345 |
SMT_Replay_Methods.dest_prop |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
346 |
#> HOLogic.dest_eq |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
347 |
#> fst |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
348 |
#> extract_all_exists_quantified_names_q |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
349 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
350 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
351 |
val extract_bind_names = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
352 |
HOLogic.dest_eq |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
353 |
#> apply2 (fn (Free (name, _)) => name) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
354 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
355 |
fun combine_quant ctxt ((n1, n2) :: bounds) (n1' :: formula) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
356 |
TRY' (if n1 = n1' |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
357 |
then if n1 <> n2 |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
358 |
then |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
359 |
resolve_tac ctxt bind_thms |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
360 |
THEN' TRY'(resolve_tac ctxt [@{thm refl}]) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
361 |
THEN' combine_quant ctxt bounds formula |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
362 |
else resolve_tac ctxt bind_thms_same_name THEN' combine_quant ctxt bounds formula |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
363 |
else resolve_tac ctxt @{thms allI} THEN' combine_quant ctxt ((n1, n2) :: bounds) formula) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
364 |
| combine_quant _ _ _ = K all_tac |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
365 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
366 |
fun bind_quants ctxt args t = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
367 |
combine_quant ctxt (map extract_bind_names args) (extract_quantified_names t) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
368 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
369 |
fun generalize_prems_q [] prems = prems |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
370 |
| generalize_prems_q (_ :: quants) prems = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
371 |
generalize_prems_q quants (@{thm spec} OF [prems]) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
372 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
373 |
fun generalize_prems t = generalize_prems_q (fst (extract_quantified_names_ba t)) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
374 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
375 |
fun bind ctxt [prems] args t = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
376 |
SMT_Replay_Methods.prove ctxt t (fn _ => |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
377 |
bind_quants ctxt args t |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
378 |
THEN' TRY' (SOLVED' (resolve_tac ctxt [generalize_prems t prems] |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
379 |
THEN_ALL_NEW TRY' (assume_tac ctxt ORELSE' resolve_tac ctxt @{thms refl})))) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
380 |
| bind ctxt thms _ t = replay_error ctxt "invalid bind application" Bind thms t |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
381 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
382 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
383 |
(* Congruence/Refl *) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
384 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
385 |
fun cong ctxt thms = try_provers ctxt |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
386 |
(string_of_verit_rule Cong) [ |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
387 |
("basic", SMT_Replay_Methods.cong_basic ctxt thms), |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
388 |
("unfolding then reflexivity", SMT_Replay_Methods.cong_unfolding_trivial ctxt thms), |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
389 |
("unfolding then auto", SMT_Replay_Methods.cong_unfolding_first ctxt thms), |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
390 |
("full", SMT_Replay_Methods.cong_full ctxt thms)] thms |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
391 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
392 |
fun refl ctxt thm t = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
393 |
(case find_first (fn thm => t = Thm.full_prop_of thm) thm of |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
394 |
SOME thm => thm |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
395 |
| NONE => |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
396 |
(case try (fn t => SMT_Replay_Methods.match_instantiate ctxt t @{thm refl}) t of |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
397 |
NONE => cong ctxt thm t |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
398 |
| SOME thm => thm)) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
399 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
400 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
401 |
(* Instantiation *) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
402 |
|
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
403 |
local |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
404 |
fun dropWhile _ [] = [] |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
405 |
| dropWhile f (x :: xs) = if f x then dropWhile f xs else x :: xs |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
406 |
in |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
407 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
408 |
fun forall_inst ctxt _ _ insts t = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
409 |
let |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
410 |
fun instantiate_and_solve i ({context = ctxt, prems = [prem], ...}: Subgoal.focus) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
411 |
let |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
412 |
val t = Thm.prop_of prem |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
413 |
val quants = t |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
414 |
|> SMT_Replay_Methods.dest_prop |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
415 |
|> extract_forall_quantified_names_q |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
416 |
val insts = map (Symtab.lookup insts o fst) (rev quants) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
417 |
|> dropWhile (curry (op =) NONE) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
418 |
|> rev |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
419 |
fun option_map _ NONE = NONE |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
420 |
| option_map f (SOME a) = SOME (f a) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
421 |
fun instantiate_with inst prem = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
422 |
Drule.infer_instantiate' ctxt [NONE, inst] @{thm spec} OF [prem] |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
423 |
val inst_thm = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
424 |
fold instantiate_with |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
425 |
(map (option_map (Thm.cterm_of ctxt)) insts) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
426 |
prem |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
427 |
in |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
428 |
(Method.insert_tac ctxt [inst_thm] |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
429 |
THEN' TRY' (fn i => assume_tac ctxt i) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
430 |
THEN' TRY' (partial_simplify_tac ctxt @{thms eq_commute})) i |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
431 |
end |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
432 |
| instantiate_and_solve _ ({context = ctxt, prems = thms, ...}: Subgoal.focus) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
433 |
replay_error ctxt "invalid application" Forall_Inst thms t |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
434 |
in |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
435 |
SMT_Replay_Methods.prove ctxt t (fn _ => |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
436 |
match_tac ctxt [@{thm disj_not1} RSN (1, @{thm iffD2}) OF [@{thm impI}]] |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
437 |
THEN' (fn i => Subgoal.FOCUS (instantiate_and_solve i) ctxt i)) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
438 |
end |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
439 |
end |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
440 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
441 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
442 |
(* Or *) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
443 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
444 |
fun or _ (thm :: _) _ = thm |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
445 |
| or ctxt thms t = replay_error ctxt "invalid bind application" Or thms t |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
446 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
447 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
448 |
(* Implication *) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
449 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
450 |
val implies_pos_thm = |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
451 |
[@{lemma \<open>\<not>(A \<longrightarrow> B) \<or> \<not>A \<or> B\<close> by blast}, |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
452 |
@{lemma \<open>\<not>(\<not>A \<longrightarrow> B) \<or> A \<or> B\<close> by blast}] |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
453 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
454 |
fun implies_pos ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
455 |
resolve_tac ctxt implies_pos_thm) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
456 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
457 |
fun extract_rewrite_rule_assumption _ thms = |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
458 |
let |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
459 |
fun is_rewrite_rule thm = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
460 |
(case Thm.prop_of thm of |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
461 |
\<^term>\<open>Trueprop\<close> $ (Const(\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ Free(_, _)) => true |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
462 |
| _ => false) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
463 |
fun is_context_rule thm = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
464 |
(case Thm.prop_of thm of |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
465 |
\<^term>\<open>Trueprop\<close> $ (Const(\<^const_name>\<open>HOL.eq\<close>, _) $ Free(_, _) $ Free(_, _)) => true |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
466 |
| _ => false) |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
467 |
val ctxt_eq = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
468 |
thms |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
469 |
|> filter is_context_rule |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
470 |
val rew = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
471 |
thms |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
472 |
|> filter_out is_context_rule |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
473 |
|> filter is_rewrite_rule |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
474 |
in |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
475 |
(ctxt_eq, rew) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
476 |
end |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
477 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
478 |
local |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
479 |
fun rewrite_all_skolems thm_indirect ctxt (SOME thm :: thms) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
480 |
EqSubst.eqsubst_tac ctxt [0] [thm_indirect OF [thm]] |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
481 |
THEN' (partial_simplify_tac ctxt (@{thms eq_commute})) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
482 |
THEN' rewrite_all_skolems thm_indirect ctxt thms |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
483 |
| rewrite_all_skolems thm_indirect ctxt (NONE :: thms) = rewrite_all_skolems thm_indirect ctxt thms |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
484 |
| rewrite_all_skolems _ _ [] = K (all_tac) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
485 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
486 |
fun extract_var_name (thm :: thms) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
487 |
let val name = Thm.concl_of thm |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
488 |
|> SMT_Replay_Methods.dest_prop |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
489 |
|> HOLogic.dest_eq |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
490 |
|> fst |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
491 |
|> (fn Const(_,_) $ Abs(name, _, _) => [(name,@{thm sym} OF [thm])] |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
492 |
| _ => []) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
493 |
in name :: extract_var_name thms end |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
494 |
| extract_var_name [] = [] |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
495 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
496 |
fun skolem_tac extractor thm1 thm2 ctxt thms t = |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
497 |
let |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
498 |
val (ctxt_eq, ts) = extract_rewrite_rule_assumption ctxt thms |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
499 |
fun ordered_definitions () = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
500 |
let |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
501 |
val var_order = extractor t |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
502 |
val thm_names_with_var = extract_var_name ts |> flat |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
503 |
in map (AList.lookup (op =) thm_names_with_var) var_order end |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
504 |
|
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
505 |
in |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
506 |
SMT_Replay_Methods.prove ctxt t (fn _ => |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
507 |
K (unfold_tac ctxt ctxt_eq) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
508 |
THEN' ((SOLVED' (K (unfold_tac ctxt (map (fn thm => thm1 OF [@{thm sym} OF [thm]]) ts)))) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
509 |
ORELSE' |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
510 |
(rewrite_all_skolems thm2 ctxt (ordered_definitions ()) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
511 |
THEN' partial_simplify_tac ctxt @{thms eq_commute}))) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
512 |
end |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
513 |
in |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
514 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
515 |
val skolem_forall = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
516 |
skolem_tac extract_all_forall_quantified_names @{thm verit_sko_forall_indirect} |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
517 |
@{thm verit_sko_forall_indirect2} |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
518 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
519 |
val skolem_ex = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
520 |
skolem_tac extract_all_exists_quantified_names @{thm verit_sko_ex_indirect} |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
521 |
@{thm verit_sko_ex_indirect2} |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
522 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
523 |
end |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
524 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
525 |
fun eq_reflexive ctxt _ t = SMT_Replay_Methods.match_instantiate ctxt t @{thm refl} |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
526 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
527 |
local |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
528 |
fun not_not_prove ctxt _ = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
529 |
K (unfold_tac ctxt @{thms not_not}) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
530 |
THEN' match_tac ctxt @{thms verit_or_simplify_1} |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
531 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
532 |
fun duplicate_literals_prove ctxt prems = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
533 |
Method.insert_tac ctxt prems |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
534 |
THEN' match_tac ctxt @{thms ccontr} |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
535 |
THEN' K (unfold_tac ctxt @{thms de_Morgan_disj not_not}) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
536 |
THEN' TRY o CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac ctxt @{thms conjE}) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
537 |
THEN' CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac ctxt @{thms disjE}) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
538 |
THEN' REPEAT' (ematch_tac ctxt @{thms notE} THEN' TRY' (assume_tac ctxt)) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
539 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
540 |
fun tautological_clause_prove ctxt _ = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
541 |
match_tac ctxt @{thms verit_or_neg} |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
542 |
THEN' K (unfold_tac ctxt @{thms not_not disj_assoc[symmetric]}) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
543 |
THEN' TRY' (match_tac ctxt @{thms notE} THEN_ALL_NEW assume_tac ctxt) |
72908
6a26a955308e
improve and activate compression for veriT proof reconstruction
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72513
diff
changeset
|
544 |
|
6a26a955308e
improve and activate compression for veriT proof reconstruction
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72513
diff
changeset
|
545 |
val theory_resolution2_lemma = @{lemma \<open>a \<Longrightarrow> a = b \<Longrightarrow> b\<close> by blast} |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
546 |
in |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
547 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
548 |
fun prove_abstract abstracter tac ctxt thms t = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
549 |
let |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
550 |
val thms = map (Conv.fconv_rule Thm.eta_long_conversion) thms |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
551 |
val t' = Thm.eta_long_conversion (Object_Logic.dest_judgment ctxt (Thm.cterm_of ctxt t)) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
552 |
val (_, t2) = Logic.dest_equals (Thm.prop_of t') |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
553 |
val thm = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
554 |
SMT_Replay_Methods.prove_abstract ctxt thms t2 tac ( |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
555 |
fold_map (abstracter o SMT_Replay_Methods.dest_thm) thms ##>> |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
556 |
abstracter (SMT_Replay_Methods.dest_prop t2)) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
557 |
in |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
558 |
@{thm verit_Pure_trans} OF [t', thm] |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
559 |
end |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
560 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
561 |
val not_not = prove_abstract SMT_Replay_Methods.abstract_bool_shallow not_not_prove |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
562 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
563 |
val tautological_clause = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
564 |
prove_abstract SMT_Replay_Methods.abstract_bool_shallow tautological_clause_prove |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
565 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
566 |
val duplicate_literals = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
567 |
prove_abstract SMT_Replay_Methods.abstract_bool_shallow duplicate_literals_prove |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
568 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
569 |
val unit_res = prove_abstract SMT_Replay_Methods.abstract_bool_shallow SMT_Replay_Methods.prop_tac |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
570 |
|
72908
6a26a955308e
improve and activate compression for veriT proof reconstruction
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72513
diff
changeset
|
571 |
(*match_instantiate does not work*) |
6a26a955308e
improve and activate compression for veriT proof reconstruction
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72513
diff
changeset
|
572 |
fun theory_resolution2 ctxt prems t = |
6a26a955308e
improve and activate compression for veriT proof reconstruction
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72513
diff
changeset
|
573 |
SMT_Replay_Methods.prove ctxt t (fn _ => match_tac ctxt [theory_resolution2_lemma OF prems]) |
6a26a955308e
improve and activate compression for veriT proof reconstruction
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72513
diff
changeset
|
574 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
575 |
end |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
576 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
577 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
578 |
fun normalized_input ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ => |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
579 |
Method.insert_tac ctxt prems |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
580 |
THEN' TRY' (K (unfold_tac ctxt @{thms SMT.trigger_def})) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
581 |
THEN' TRY' (partial_simplify_tac ctxt @{thms eq_commute})) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
582 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
583 |
val false_rule_thm = @{lemma \<open>\<not>False\<close> by blast} |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
584 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
585 |
fun false_rule ctxt _ t = SMT_Replay_Methods.match_instantiate ctxt t false_rule_thm |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
586 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
587 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
588 |
(* Transitivity *) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
589 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
590 |
val trans_bool_thm = |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
591 |
@{lemma \<open>P = Q \<Longrightarrow> Q \<Longrightarrow> P\<close> by blast} |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
592 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
593 |
fun trans ctxt thms t = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
594 |
let |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
595 |
val prop_of = HOLogic.dest_Trueprop o Thm.full_prop_of |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
596 |
fun combine_thms [thm1, thm2] = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
597 |
(case (prop_of thm1, prop_of thm2) of |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
598 |
((Const(\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2), |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
599 |
(Const(\<^const_name>\<open>HOL.eq\<close>, _) $ t3 $ t4)) => |
72513
75f5c63f6cfa
better handling of skolemization for Isar reconstruction in Sledgehammer for veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72459
diff
changeset
|
600 |
if t2 aconv t3 then thm1 RSN (1, thm2 RSN (2, @{thm trans})) |
75f5c63f6cfa
better handling of skolemization for Isar reconstruction in Sledgehammer for veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72459
diff
changeset
|
601 |
else if t2 aconv t4 then thm1 RSN ((1, ((thm2 RS sym)) RSN (2, @{thm trans}))) |
75f5c63f6cfa
better handling of skolemization for Isar reconstruction in Sledgehammer for veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72459
diff
changeset
|
602 |
else if t1 aconv t4 then thm2 RSN (1, thm1 RSN (2, @{thm trans})) |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
603 |
else raise Fail "invalid trans theorem" |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
604 |
| _ => trans_bool_thm OF [thm1, thm2]) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
605 |
| combine_thms (thm1 :: thm2 :: thms) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
606 |
combine_thms (combine_thms [thm1, thm2] :: thms) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
607 |
| combine_thms thms = replay_error ctxt "invalid bind application" Trans thms t |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
608 |
val t' = Thm.eta_long_conversion (Object_Logic.dest_judgment ctxt (Thm.cterm_of ctxt t)) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
609 |
val (_, t2) = Logic.dest_equals (Thm.prop_of t') |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
610 |
val thms = map (Conv.fconv_rule Thm.eta_long_conversion) thms |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
611 |
val trans_thm = combine_thms thms |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
612 |
in |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
613 |
(case (prop_of trans_thm, t2) of |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
614 |
((Const(\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ _), |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
615 |
(Const(\<^const_name>\<open>HOL.eq\<close>, _) $ t3 $ _)) => |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
616 |
if t1 aconv t3 then trans_thm else trans_thm RS sym |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
617 |
| _ => trans_thm (*to be on the safe side*)) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
618 |
end |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
619 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
620 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
621 |
fun tmp_AC_rule ctxt thms t = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
622 |
SMT_Replay_Methods.prove ctxt t (fn _ => |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
623 |
Method.insert_tac ctxt thms |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
624 |
THEN' REPEAT_ALL_NEW (partial_simplify_tac ctxt @{thms eq_commute} |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
625 |
THEN' TRY' (simplify_tac ctxt @{thms ac_simps conj_ac}) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
626 |
THEN' TRY' (Classical.fast_tac ctxt))) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
627 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
628 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
629 |
(* And/Or *) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
630 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
631 |
local |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
632 |
fun not_and_rule_prove ctxt prems = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
633 |
Method.insert_tac ctxt prems |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
634 |
THEN' K (unfold_tac ctxt @{thms de_Morgan_conj}) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
635 |
THEN_ALL_NEW TRY' (assume_tac ctxt) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
636 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
637 |
fun or_pos_prove ctxt _ = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
638 |
K (unfold_tac ctxt @{thms de_Morgan_disj not_not}) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
639 |
THEN' match_tac ctxt @{thms verit_and_pos} |
72513
75f5c63f6cfa
better handling of skolemization for Isar reconstruction in Sledgehammer for veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72459
diff
changeset
|
640 |
THEN' K (unfold_tac ctxt @{thms de_Morgan_conj de_Morgan_disj not_not}) |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
641 |
THEN' TRY' (assume_tac ctxt) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
642 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
643 |
fun not_or_rule_prove ctxt prems = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
644 |
Method.insert_tac ctxt prems |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
645 |
THEN' K (unfold_tac ctxt @{thms de_Morgan_disj not_not}) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
646 |
THEN' TRY' (REPEAT' (match_tac ctxt @{thms conjI})) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
647 |
THEN_ALL_NEW ((REPEAT' (ematch_tac ctxt @{thms conjE})) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
648 |
THEN' TRY' (assume_tac ctxt)) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
649 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
650 |
fun and_rule_prove ctxt prems = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
651 |
Method.insert_tac ctxt prems |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
652 |
THEN' (fn i => REPEAT (dresolve_tac ctxt @{thms conjE} i THEN assume_tac ctxt (i+1))) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
653 |
THEN' TRY' (assume_tac ctxt) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
654 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
655 |
fun and_neg_rule_prove ctxt _ = |
72513
75f5c63f6cfa
better handling of skolemization for Isar reconstruction in Sledgehammer for veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72459
diff
changeset
|
656 |
match_tac ctxt @{thms verit_and_neg} |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
657 |
THEN' K (unfold_tac ctxt @{thms de_Morgan_conj not_not}) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
658 |
THEN' TRY' (assume_tac ctxt) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
659 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
660 |
fun prover tac = prove_abstract SMT_Replay_Methods.abstract_prop tac |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
661 |
|
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
662 |
in |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
663 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
664 |
val and_rule = prover and_rule_prove |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
665 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
666 |
val not_and_rule = prover not_and_rule_prove |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
667 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
668 |
val not_or_rule = prover not_or_rule_prove |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
669 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
670 |
val or_pos_rule = prover or_pos_prove |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
671 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
672 |
val and_neg_rule = prover and_neg_rule_prove |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
673 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
674 |
val or_neg_rule = prove_abstract SMT_Replay_Methods.abstract_bool (fn ctxt => fn _ => |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
675 |
resolve_tac ctxt @{thms verit_or_neg} |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
676 |
THEN' K (unfold_tac ctxt @{thms not_not}) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
677 |
THEN_ALL_NEW |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
678 |
(REPEAT' |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
679 |
(SOLVED' (match_tac ctxt @{thms disjI1} THEN_ALL_NEW assume_tac ctxt) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
680 |
ORELSE' (match_tac ctxt @{thms disjI2} THEN' TRY' (assume_tac ctxt))))) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
681 |
|
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
682 |
fun and_pos ctxt _ t = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
683 |
SMT_Replay_Methods.prove ctxt t (fn _ => |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
684 |
REPEAT_CHANGED (resolve_tac ctxt @{thms verit_and_pos}) |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
685 |
THEN' TRY' (assume_tac ctxt)) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
686 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
687 |
end |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
688 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
689 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
690 |
(* Equivalence Transformation *) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
691 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
692 |
local |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
693 |
fun prove_equiv equiv_thm ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
694 |
Method.insert_tac ctxt [equiv_thm OF [thm]] |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
695 |
THEN' TRY' (assume_tac ctxt)) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
696 |
| prove_equiv _ ctxt thms t = replay_error ctxt "invalid application in some equiv rule" Unsupported thms t |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
697 |
in |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
698 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
699 |
val not_equiv1 = prove_equiv @{lemma \<open>\<not>(A \<longleftrightarrow> B) \<Longrightarrow> A \<or> B\<close> by blast} |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
700 |
val not_equiv2 = prove_equiv @{lemma \<open>\<not>(A \<longleftrightarrow> B) \<Longrightarrow> \<not>A \<or> \<not>B\<close> by blast} |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
701 |
val equiv1 = prove_equiv @{lemma \<open>(A \<longleftrightarrow> B) \<Longrightarrow> \<not>A \<or> B\<close> by blast} |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
702 |
val equiv2 = prove_equiv @{lemma \<open>(A \<longleftrightarrow> B) \<Longrightarrow> A \<or> \<not>B\<close> by blast} |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
703 |
val not_implies1 = prove_equiv @{lemma \<open>\<not>(A \<longrightarrow> B) \<Longrightarrow> A\<close> by blast} |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
704 |
val not_implies2 = prove_equiv @{lemma \<open>\<not>(A \<longrightarrow>B) \<Longrightarrow> \<not>B\<close> by blast} |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
705 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
706 |
end |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
707 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
708 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
709 |
(* Equivalence Lemma *) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
710 |
(*equiv_pos2 is very important for performance. We have tried various tactics, including |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
711 |
a specialisation of SMT_Replay_Methods.match_instantiate, but there never was a measurable |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
712 |
and consistent gain.*) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
713 |
local |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
714 |
fun prove_equiv_pos_neg2 thm ctxt _ t = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
715 |
SMT_Replay_Methods.match_instantiate ctxt t thm |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
716 |
in |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
717 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
718 |
val equiv_pos1_thm = @{lemma \<open>\<not>(a \<longleftrightarrow> b) \<or> a \<or> \<not>b\<close> by blast+} |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
719 |
val equiv_pos1 = prove_equiv_pos_neg2 equiv_pos1_thm |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
720 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
721 |
val equiv_pos2_thm = @{lemma \<open>\<And>a b. (a \<noteq> b) \<or> \<not>a \<or> b\<close> by blast+} |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
722 |
val equiv_pos2 = prove_equiv_pos_neg2 equiv_pos2_thm |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
723 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
724 |
val equiv_neg1_thm = @{lemma \<open>(a \<longleftrightarrow> b) \<or> \<not>a \<or> \<not>b\<close> by blast+} |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
725 |
val equiv_neg1 = prove_equiv_pos_neg2 equiv_neg1_thm |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
726 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
727 |
val equiv_neg2_thm = @{lemma \<open>(a \<longleftrightarrow> b) \<or> a \<or> b\<close> by blast} |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
728 |
val equiv_neg2 = prove_equiv_pos_neg2 equiv_neg2_thm |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
729 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
730 |
end |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
731 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
732 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
733 |
local |
69593 | 734 |
fun implies_pos_neg_term ctxt thm (\<^term>\<open>Trueprop\<close> $ |
735 |
(\<^term>\<open>HOL.disj\<close> $ (\<^term>\<open>HOL.implies\<close> $ a $ b) $ _)) = |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
736 |
Drule.infer_instantiate' ctxt (map (SOME o Thm.cterm_of ctxt) [a, b]) thm |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
737 |
| implies_pos_neg_term ctxt thm t = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
738 |
replay_error ctxt "invalid application in Implies" Unsupported [thm] t |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
739 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
740 |
fun prove_implies_pos_neg thm ctxt _ t = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
741 |
let val thm = implies_pos_neg_term ctxt thm t |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
742 |
in |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
743 |
SMT_Replay_Methods.prove ctxt t (fn _ => |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
744 |
Method.insert_tac ctxt [thm] |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
745 |
THEN' TRY' (assume_tac ctxt)) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
746 |
end |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
747 |
in |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
748 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
749 |
val implies_neg1_thm = @{lemma \<open>(a \<longrightarrow> b) \<or> a\<close> by blast} |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
750 |
val implies_neg1 = prove_implies_pos_neg implies_neg1_thm |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
751 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
752 |
val implies_neg2_thm = @{lemma \<open>(a \<longrightarrow> b) \<or> \<not>b\<close> by blast} |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
753 |
val implies_neg2 = prove_implies_pos_neg implies_neg2_thm |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
754 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
755 |
val implies_thm = @{lemma \<open>(a \<longrightarrow> b) \<Longrightarrow> \<not>a \<or> b\<close> by blast} |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
756 |
fun implies_rules ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ => |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
757 |
Method.insert_tac ctxt [implies_thm OF prems] |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
758 |
THEN' TRY' (assume_tac ctxt)) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
759 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
760 |
end |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
761 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
762 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
763 |
(* BFun *) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
764 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
765 |
local |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
766 |
val bfun_theorems = @{thms verit_bfun_elim} |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
767 |
in |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
768 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
769 |
fun bfun_elim ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ => |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
770 |
Method.insert_tac ctxt prems |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
771 |
THEN' TRY' (eqsubst_all ctxt bfun_theorems) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
772 |
THEN' TRY' (simplify_tac ctxt @{thms eq_commute all_conj_distrib ex_disj_distrib})) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
773 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
774 |
end |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
775 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
776 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
777 |
(* If-Then-Else *) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
778 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
779 |
local |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
780 |
fun prove_ite ite_thm thm ctxt = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
781 |
resolve_tac ctxt [ite_thm OF [thm]] |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
782 |
THEN' K (unfold_tac ctxt @{thms not_not}) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
783 |
THEN' TRY' (assume_tac ctxt) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
784 |
in |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
785 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
786 |
val ite_pos1_thm = |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
787 |
@{lemma \<open>\<not>(if x then P else Q) \<or> x \<or> Q\<close> by auto} |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
788 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
789 |
fun ite_pos1 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
790 |
resolve_tac ctxt [ite_pos1_thm]) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
791 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
792 |
val ite_pos2_thms = |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
793 |
@{lemma \<open>\<not>(if x then P else Q) \<or> \<not>x \<or> P\<close> \<open>\<not>(if \<not>x then P else Q) \<or> x \<or> P\<close> by auto} |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
794 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
795 |
fun ite_pos2 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => resolve_tac ctxt ite_pos2_thms) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
796 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
797 |
val ite_neg1_thms = |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
798 |
@{lemma \<open>(if x then P else Q) \<or> x \<or> \<not>Q\<close> \<open>(if x then P else \<not>Q) \<or> x \<or> Q\<close> by auto} |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
799 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
800 |
fun ite_neg1 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => resolve_tac ctxt ite_neg1_thms) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
801 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
802 |
val ite_neg2_thms = |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
803 |
@{lemma \<open>(if x then P else Q) \<or> \<not>x \<or> \<not>P\<close> \<open>(if \<not>x then P else Q) \<or> x \<or> \<not>P\<close> |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
804 |
\<open>(if x then \<not>P else Q) \<or> \<not>x \<or> P\<close> \<open>(if \<not>x then \<not>P else Q) \<or> x \<or> P\<close> |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
805 |
by auto} |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
806 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
807 |
fun ite_neg2 ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => resolve_tac ctxt ite_neg2_thms) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
808 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
809 |
val ite1_thm = |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
810 |
@{lemma \<open>(if x then P else Q) \<Longrightarrow> x \<or> Q\<close> by (auto split: if_splits) } |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
811 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
812 |
fun ite1 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => prove_ite ite1_thm thm ctxt) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
813 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
814 |
val ite2_thm = |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
815 |
@{lemma \<open>(if x then P else Q) \<Longrightarrow> \<not>x \<or> P\<close> by (auto split: if_splits) } |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
816 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
817 |
fun ite2 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => prove_ite ite2_thm thm ctxt) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
818 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
819 |
val not_ite1_thm = |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
820 |
@{lemma \<open>\<not>(if x then P else Q) \<Longrightarrow> x \<or> \<not>Q\<close> by (auto split: if_splits) } |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
821 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
822 |
fun not_ite1 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => prove_ite not_ite1_thm thm ctxt) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
823 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
824 |
val not_ite2_thm = |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
825 |
@{lemma \<open>\<not>(if x then P else Q) \<Longrightarrow> \<not>x \<or> \<not>P\<close> by (auto split: if_splits) } |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
826 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
827 |
fun not_ite2 ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => prove_ite not_ite2_thm thm ctxt) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
828 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
829 |
(*ite_intro can introduce new terms that are in the proof exactly the sames as the old one, but are |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
830 |
not internally, hence the possible reordering.*) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
831 |
fun ite_intro ctxt _ t = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
832 |
let |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
833 |
fun simplify_ite ctxt thms = |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
834 |
ctxt |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
835 |
|> empty_simpset |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
836 |
|> put_simpset HOL_basic_ss |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
837 |
|> (fn ctxt => ctxt addsimps thms @ @{thms if_True if_False refl simp_thms if_cancel}) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
838 |
|> Raw_Simplifier.add_eqcong @{thm verit_ite_if_cong} |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
839 |
|> Simplifier.full_simp_tac |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
840 |
in |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
841 |
SMT_Replay_Methods.prove ctxt t (fn _ => simplify_ite ctxt [] |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
842 |
THEN' TRY' (simplify_ite ctxt @{thms eq_commute})) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
843 |
end |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
844 |
end |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
845 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
846 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
847 |
(* Quantifiers *) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
848 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
849 |
local |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
850 |
val rm_unused = @{lemma \<open>(\<forall>x. P) = P\<close> \<open>(\<exists>x. P) = P\<close> by blast+} |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
851 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
852 |
fun qnt_cnf_tac ctxt = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
853 |
simplify_tac ctxt @{thms de_Morgan_conj de_Morgan_disj imp_conv_disj |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
854 |
iff_conv_conj_imp if_bool_eq_disj ex_simps all_simps ex_disj_distrib |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
855 |
verit_connective_def(3) all_conj_distrib} |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
856 |
THEN' TRY' (Blast.blast_tac ctxt) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
857 |
in |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
858 |
fun qnt_rm_unused ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
859 |
K (unfold_tac ctxt rm_unused)) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
860 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
861 |
fun onepoint ctxt prems t = SMT_Replay_Methods.prove ctxt t (fn _ => |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
862 |
Method.insert_tac ctxt prems |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
863 |
THEN' Simplifier.full_simp_tac (put_simpset HOL_basic_ss (empty_simpset ctxt) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
864 |
addsimps @{thms HOL.simp_thms HOL.all_simps} |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
865 |
addsimprocs [@{simproc HOL.defined_All}, @{simproc HOL.defined_Ex}]) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
866 |
THEN' TRY' (Blast.blast_tac ctxt) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
867 |
THEN' TRY' (Metis_Tactic.metis_tac [] ATP_Problem_Generate.combsN ctxt [])) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
868 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
869 |
fun qnt_join ctxt _ t = SMT_Replay_Methods.prove ctxt t Classical.fast_tac |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
870 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
871 |
fun qnt_cnf ctxt _ t = SMT_Replay_Methods.prove ctxt t qnt_cnf_tac |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
872 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
873 |
fun qnt_simplify ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
874 |
partial_simplify_tac ctxt []) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
875 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
876 |
end |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
877 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
878 |
(* Equality *) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
879 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
880 |
fun eq_transitive ctxt _ t = SMT_Replay_Methods.prove ctxt t (fn _ => |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
881 |
REPEAT_CHANGED (resolve_tac ctxt [@{thm disj_not1} RSN (1, @{thm iffD2}) OF @{thms impI}]) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
882 |
THEN' REPEAT' (resolve_tac ctxt @{thms impI}) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
883 |
THEN' REPEAT' (eresolve_tac ctxt @{thms conjI}) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
884 |
THEN' REPEAT' (fn i => dresolve_tac ctxt @{thms verit_eq_transitive} i THEN assume_tac ctxt (i+1)) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
885 |
THEN' resolve_tac ctxt @{thms refl}) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
886 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
887 |
local |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
888 |
fun find_rew rews t t' = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
889 |
(case AList.lookup (op =) rews (t, t') of |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
890 |
SOME thm => SOME (thm COMP @{thm symmetric}) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
891 |
| NONE => |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
892 |
(case AList.lookup (op =) rews (t', t) of |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
893 |
SOME thm => SOME thm |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
894 |
| NONE => NONE)) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
895 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
896 |
fun eq_pred_conv rews t ctxt ctrm = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
897 |
(case find_rew rews t (Thm.term_of ctrm) of |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
898 |
SOME thm => Conv.rewr_conv thm ctrm |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
899 |
| NONE => |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
900 |
(case t of |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
901 |
f $ arg => |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
902 |
(Conv.fun_conv (eq_pred_conv rews f ctxt) then_conv |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
903 |
Conv.arg_conv (eq_pred_conv rews arg ctxt)) ctrm |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
904 |
| _ => Conv.all_conv ctrm)) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
905 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
906 |
fun eq_pred_rewrite_tac ({context = ctxt, prems, concl, ...}: Subgoal.focus) = |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
907 |
let |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
908 |
val rews = prems |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
909 |
|> map_filter (try (apfst (HOLogic.dest_eq o Thm.term_of o Object_Logic.dest_judgment ctxt o |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
910 |
Thm.cconcl_of) o `(fn x => x))) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
911 |
|> map (apsnd (fn x => @{thm eq_reflection} OF [x])) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
912 |
fun conv_left conv = Conv.arg_conv (Conv.arg_conv conv) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
913 |
fun conv_left_neg conv = Conv.arg_conv (Conv.arg_conv (Conv.arg_conv conv)) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
914 |
val (t1, conv_term) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
915 |
(case Thm.term_of (Object_Logic.dest_judgment ctxt concl) of |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
916 |
Const(_, _) $ (Const(\<^const_name>\<open>HOL.Not\<close>, _) $ t1) $ _ => (t1, conv_left) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
917 |
| Const(_, _) $ t1 $ (Const(\<^const_name>\<open>HOL.Not\<close>, _) $ _) => (t1, conv_left_neg) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
918 |
| Const(_, _) $ t1 $ _ => (t1, conv_left) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
919 |
| t1 => (t1, conv_left)) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
920 |
fun throwing_CONVERSION cv i st = Seq.single (Conv.gconv_rule cv i st) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
921 |
in |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
922 |
throwing_CONVERSION (conv_term (eq_pred_conv rews t1 ctxt)) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
923 |
end |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
924 |
in |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
925 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
926 |
fun eq_congruent_pred ctxt _ t = |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
927 |
SMT_Replay_Methods.prove ctxt t (fn _ => |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
928 |
REPEAT' (resolve_tac ctxt [@{thm disj_not1[of \<open>_ = _\<close>]} RSN (1, @{thm iffD2}) OF @{thms impI}]) |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
929 |
THEN' (fn i => Subgoal.FOCUS (fn focus => eq_pred_rewrite_tac focus i) ctxt i) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
930 |
THEN' (resolve_tac ctxt @{thms refl excluded_middle excluded_middle[of \<open>\<not>_\<close>, unfolded not_not]} |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
931 |
ORELSE' assume_tac ctxt)) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
932 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
933 |
val eq_congruent = eq_congruent_pred |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
934 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
935 |
end |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
936 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
937 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
938 |
(* Subproof *) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
939 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
940 |
fun subproof ctxt [prem] t = |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
941 |
SMT_Replay_Methods.prove ctxt t (fn _ => |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
942 |
(resolve_tac ctxt [@{thm disj_not1} RSN (1, @{thm iffD2}) OF [@{thm impI}], |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
943 |
@{thm disj_not1[of \<open>\<not>_\<close>, unfolded not_not]} RSN (1, @{thm iffD2}) OF [@{thm impI}]] |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
944 |
THEN' resolve_tac ctxt [prem] |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
945 |
THEN_ALL_NEW assume_tac ctxt |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
946 |
THEN' TRY' (assume_tac ctxt)) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
947 |
ORELSE' TRY' (Method.insert_tac ctxt [prem] THEN' Blast.blast_tac ctxt)) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
948 |
| subproof ctxt prems t = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
949 |
replay_error ctxt "invalid application, only one assumption expected" Subproof prems t |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
950 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
951 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
952 |
(* Simplifying Steps *) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
953 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
954 |
(* The reconstruction is a bit tricky: At first we only rewrite only based on the rules that are |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
955 |
passed as argument. Then we simply use simp_thms to reconstruct all the proofs (and these theorems |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
956 |
cover all the simplification below). |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
957 |
*) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
958 |
local |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
959 |
fun rewrite_only_thms ctxt thms = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
960 |
ctxt |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
961 |
|> empty_simpset |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
962 |
|> put_simpset HOL_basic_ss |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
963 |
|> (fn ctxt => ctxt addsimps thms) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
964 |
|> Simplifier.full_simp_tac |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
965 |
fun rewrite_thms ctxt thms = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
966 |
ctxt |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
967 |
|> empty_simpset |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
968 |
|> put_simpset HOL_basic_ss |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
969 |
|> Raw_Simplifier.add_eqcong @{thm eq_reflection[OF imp_cong]} |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
970 |
|> (fn ctxt => ctxt addsimps thms addsimps @{thms simp_thms}) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
971 |
|> Simplifier.full_simp_tac |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
972 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
973 |
fun chain_rewrite_thms ctxt thms = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
974 |
TRY' (rewrite_only_thms ctxt thms) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
975 |
THEN' TRY' (rewrite_thms ctxt thms) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
976 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
977 |
fun chain_rewrite_two_step_with_ac_simps ctxt thms1 thms2 = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
978 |
TRY' (rewrite_only_thms ctxt thms1) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
979 |
THEN' TRY' (rewrite_thms ctxt thms2) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
980 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
981 |
fun chain_rewrite_thms_two_step ctxt thms1 thms2 thms3 thms4 = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
982 |
chain_rewrite_two_step_with_ac_simps ctxt thms1 thms2 |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
983 |
THEN' TRY' (chain_rewrite_two_step_with_ac_simps ctxt thms3 thms4) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
984 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
985 |
val imp_refl = @{lemma \<open>(P \<longrightarrow> P) = True\<close> by blast} |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
986 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
987 |
in |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
988 |
fun rewrite_bool_simplify ctxt _ t = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
989 |
SMT_Replay_Methods.prove ctxt t (fn _ => |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
990 |
(chain_rewrite_thms ctxt @{thms verit_bool_simplify})) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
991 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
992 |
fun rewrite_and_simplify ctxt _ t = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
993 |
SMT_Replay_Methods.prove ctxt t (fn _ => |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
994 |
(chain_rewrite_two_step_with_ac_simps ctxt @{thms verit_and_simplify verit_and_simplify1} |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
995 |
@{thms verit_and_simplify})) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
996 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
997 |
fun rewrite_or_simplify ctxt _ t = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
998 |
SMT_Replay_Methods.prove ctxt t (fn _ => |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
999 |
(chain_rewrite_two_step_with_ac_simps ctxt @{thms verit_or_simplify verit_or_simplify_1} |
72513
75f5c63f6cfa
better handling of skolemization for Isar reconstruction in Sledgehammer for veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72459
diff
changeset
|
1000 |
@{thms verit_or_simplify}) |
75f5c63f6cfa
better handling of skolemization for Isar reconstruction in Sledgehammer for veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72459
diff
changeset
|
1001 |
THEN' TRY' (REPEAT' (match_tac ctxt @{thms verit_and_pos}) THEN' assume_tac ctxt)) |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1002 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1003 |
fun rewrite_not_simplify ctxt _ t = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1004 |
SMT_Replay_Methods.prove ctxt t (fn _ => |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1005 |
(rewrite_only_thms ctxt @{thms verit_not_simplify})) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1006 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1007 |
fun rewrite_equiv_simplify ctxt _ t = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1008 |
SMT_Replay_Methods.prove ctxt t (fn _ => |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1009 |
(rewrite_only_thms ctxt @{thms verit_equiv_simplify})) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1010 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1011 |
fun rewrite_eq_simplify ctxt _ t = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1012 |
SMT_Replay_Methods.prove ctxt t (fn _ => |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1013 |
(chain_rewrite_two_step_with_ac_simps ctxt |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1014 |
@{thms verit_eq_simplify} |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1015 |
(Named_Theorems.get ctxt @{named_theorems ac_simps}))) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1016 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1017 |
fun rewrite_implies_simplify ctxt _ t = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1018 |
SMT_Replay_Methods.prove ctxt t (fn _ => |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1019 |
(rewrite_only_thms ctxt @{thms verit_implies_simplify})) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
1020 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1021 |
(* It is more efficient to first fold the implication symbols. |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1022 |
That is however not enough when symbols appears within |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1023 |
expressions, hence we also unfold implications in the |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1024 |
other direction. *) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1025 |
fun rewrite_connective_def ctxt _ t = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1026 |
SMT_Replay_Methods.prove ctxt t (fn _ => |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1027 |
chain_rewrite_thms_two_step ctxt |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1028 |
(imp_refl :: @{thms not_not verit_connective_def[symmetric]}) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1029 |
(@{thms verit_connective_def[symmetric]}) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1030 |
(imp_refl :: @{thms not_not verit_connective_def}) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1031 |
(@{thms verit_connective_def})) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1032 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1033 |
fun rewrite_minus_simplify ctxt _ t = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1034 |
SMT_Replay_Methods.prove ctxt t (fn _ => |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1035 |
chain_rewrite_two_step_with_ac_simps ctxt |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1036 |
@{thms arith_simps verit_minus_simplify} |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1037 |
(Named_Theorems.get ctxt @{named_theorems ac_simps} @ |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1038 |
@{thms numerals arith_simps arith_special |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1039 |
numeral_class.numeral.numeral_One})) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1040 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1041 |
fun rewrite_comp_simplify ctxt _ t = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1042 |
SMT_Replay_Methods.prove ctxt t (fn _ => |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1043 |
chain_rewrite_thms ctxt @{thms verit_comp_simplify}) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1044 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1045 |
fun rewrite_ite_simplify ctxt _ t = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1046 |
SMT_Replay_Methods.prove ctxt t (fn _ => |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1047 |
(rewrite_only_thms ctxt @{thms verit_ite_simplify})) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1048 |
end |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
1049 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
1050 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1051 |
(* Simplifications *) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1052 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1053 |
local |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1054 |
fun simplify_arith ctxt thms = partial_simplify_tac ctxt |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1055 |
(thms @ Named_Theorems.get ctxt @{named_theorems ac_simps} @ @{thms arith_simps}) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1056 |
in |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1057 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1058 |
fun sum_simplify ctxt _ t = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1059 |
SMT_Replay_Methods.prove ctxt t (fn _ => |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1060 |
simplify_arith ctxt @{thms verit_sum_simplify arith_special}) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1061 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1062 |
fun prod_simplify ctxt _ t = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1063 |
SMT_Replay_Methods.prove ctxt t (fn _ => |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1064 |
simplify_arith ctxt @{thms verit_prod_simplify}) |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
1065 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1066 |
end |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1067 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1068 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1069 |
(* Arithmetics *) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1070 |
local |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1071 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1072 |
val la_rw_eq_thm = @{lemma \<open>(a :: nat) = b \<or> (a \<le> b) \<or> (a \<ge> b)\<close> by auto} |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1073 |
in |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1074 |
fun la_rw_eq ctxt _ t = SMT_Replay_Methods.match_instantiate ctxt t la_rw_eq_thm |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1075 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1076 |
fun la_generic_prove args ctxt _ = SMT_Replay_Arith.la_farkas args ctxt |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1077 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1078 |
fun la_generic ctxt _ args = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1079 |
prove_abstract (SMT_Replay_Methods.abstract_arith_shallow ctxt) (la_generic_prove args) ctxt [] |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1080 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1081 |
fun lia_generic ctxt _ t = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1082 |
SMT_Replay_Methods.prove_arith_rewrite SMT_Replay_Methods.abstract_neq ctxt t |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
1083 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1084 |
fun la_disequality ctxt _ t = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1085 |
SMT_Replay_Methods.match_instantiate ctxt t @{thm verit_la_disequality} |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1086 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1087 |
end |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1088 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1089 |
(* Combining all together *) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1090 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1091 |
fun unsupported rule ctxt thms _ _ _ = SMT_Replay_Methods.replay_error ctxt "Unsupported verit rule" |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1092 |
rule thms |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1093 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1094 |
fun ignore_args f ctxt thm _ _ _ t = f ctxt thm t |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1095 |
fun ignore_decls f ctxt thm args insts _ t = f ctxt thm args insts t |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1096 |
fun ignore_insts f ctxt thm args _ _ t = f ctxt thm args t |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1097 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1098 |
fun choose And = ignore_args and_rule |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1099 |
| choose And_Neg = ignore_args and_neg_rule |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
1100 |
| choose And_Pos = ignore_args and_pos |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1101 |
| choose And_Simplify = ignore_args rewrite_and_simplify |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1102 |
| choose Bind = ignore_insts bind |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1103 |
| choose Bool_Simplify = ignore_args rewrite_bool_simplify |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1104 |
| choose Comp_Simplify = ignore_args rewrite_comp_simplify |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
1105 |
| choose Cong = ignore_args cong |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1106 |
| choose Connective_Def = ignore_args rewrite_connective_def |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1107 |
| choose Duplicate_Literals = ignore_args duplicate_literals |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1108 |
| choose Eq_Congruent = ignore_args eq_congruent |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1109 |
| choose Eq_Congruent_Pred = ignore_args eq_congruent_pred |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1110 |
| choose Eq_Reflexive = ignore_args eq_reflexive |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1111 |
| choose Eq_Simplify = ignore_args rewrite_eq_simplify |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1112 |
| choose Eq_Transitive = ignore_args eq_transitive |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1113 |
| choose Equiv1 = ignore_args equiv1 |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1114 |
| choose Equiv2 = ignore_args equiv2 |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1115 |
| choose Equiv_neg1 = ignore_args equiv_neg1 |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1116 |
| choose Equiv_neg2 = ignore_args equiv_neg2 |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
1117 |
| choose Equiv_pos1 = ignore_args equiv_pos1 |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
1118 |
| choose Equiv_pos2 = ignore_args equiv_pos2 |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1119 |
| choose Equiv_Simplify = ignore_args rewrite_equiv_simplify |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1120 |
| choose False = ignore_args false_rule |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1121 |
| choose Forall_Inst = ignore_decls forall_inst |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1122 |
| choose Implies = ignore_args implies_rules |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1123 |
| choose Implies_Neg1 = ignore_args implies_neg1 |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1124 |
| choose Implies_Neg2 = ignore_args implies_neg2 |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1125 |
| choose Implies_Pos = ignore_args implies_pos |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1126 |
| choose Implies_Simplify = ignore_args rewrite_implies_simplify |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1127 |
| choose ITE1 = ignore_args ite1 |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1128 |
| choose ITE2 = ignore_args ite2 |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1129 |
| choose ITE_Intro = ignore_args ite_intro |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1130 |
| choose ITE_Neg1 = ignore_args ite_neg1 |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1131 |
| choose ITE_Neg2 = ignore_args ite_neg2 |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1132 |
| choose ITE_Pos1 = ignore_args ite_pos1 |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1133 |
| choose ITE_Pos2 = ignore_args ite_pos2 |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1134 |
| choose ITE_Simplify = ignore_args rewrite_ite_simplify |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1135 |
| choose LA_Disequality = ignore_args la_disequality |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1136 |
| choose LA_Generic = ignore_insts la_generic |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1137 |
| choose LA_RW_Eq = ignore_args la_rw_eq |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1138 |
| choose LA_Tautology = ignore_args SMT_Replay_Methods.arith_th_lemma_wo_shallow |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1139 |
| choose LA_Totality = ignore_args SMT_Replay_Methods.arith_th_lemma_wo_shallow |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1140 |
| choose LIA_Generic = ignore_args lia_generic |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1141 |
| choose Local_Input = ignore_args refl |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1142 |
| choose Minus_Simplify = ignore_args rewrite_minus_simplify |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1143 |
| choose NLA_Generic = ignore_args SMT_Replay_Methods.arith_th_lemma_wo_shallow |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1144 |
| choose Normalized_Input = ignore_args normalized_input |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1145 |
| choose Not_And = ignore_args not_and_rule |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
1146 |
| choose Not_Equiv1 = ignore_args not_equiv1 |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
1147 |
| choose Not_Equiv2 = ignore_args not_equiv2 |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
1148 |
| choose Not_Implies1 = ignore_args not_implies1 |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
1149 |
| choose Not_Implies2 = ignore_args not_implies2 |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
1150 |
| choose Not_ITE1 = ignore_args not_ite1 |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
1151 |
| choose Not_ITE2 = ignore_args not_ite2 |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1152 |
| choose Not_Not = ignore_args not_not |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1153 |
| choose Not_Or = ignore_args not_or_rule |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1154 |
| choose Not_Simplify = ignore_args rewrite_not_simplify |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1155 |
| choose Or = ignore_args or |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1156 |
| choose Or_Neg = ignore_args or_neg_rule |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1157 |
| choose Or_Pos = ignore_args or_pos_rule |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1158 |
| choose Or_Simplify = ignore_args rewrite_or_simplify |
72908
6a26a955308e
improve and activate compression for veriT proof reconstruction
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72513
diff
changeset
|
1159 |
| choose Theory_Resolution2 = ignore_args theory_resolution2 |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1160 |
| choose Prod_Simplify = ignore_args prod_simplify |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1161 |
| choose Qnt_Join = ignore_args qnt_join |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
1162 |
| choose Qnt_Rm_Unused = ignore_args qnt_rm_unused |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1163 |
| choose Onepoint = ignore_args onepoint |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
1164 |
| choose Qnt_Simplify = ignore_args qnt_simplify |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1165 |
| choose Refl = ignore_args refl |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1166 |
| choose Resolution = ignore_args unit_res |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1167 |
| choose Skolem_Ex = ignore_args skolem_ex |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1168 |
| choose Skolem_Forall = ignore_args skolem_forall |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
1169 |
| choose Subproof = ignore_args subproof |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1170 |
| choose Sum_Simplify = ignore_args sum_simplify |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1171 |
| choose Tautological_Clause = ignore_args tautological_clause |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1172 |
| choose Theory_Resolution = ignore_args unit_res |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1173 |
| choose AC_Simp = ignore_args tmp_AC_rule |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1174 |
| choose Bfun_Elim = ignore_args bfun_elim |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1175 |
| choose Qnt_CNF = ignore_args qnt_cnf |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1176 |
| choose Trans = ignore_args trans |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
1177 |
| choose r = unsupported (string_of_verit_rule r) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
1178 |
|
72459
15fc6320da68
reconstruction of veriT proofs in NEWS
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
72458
diff
changeset
|
1179 |
type verit_method = Proof.context -> thm list -> term -> thm |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
1180 |
type abs_context = int * term Termtab.table |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
1181 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1182 |
fun with_tracing rule method ctxt thms args insts decls t = |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
1183 |
let val _ = SMT_Replay_Methods.trace_goal ctxt rule thms t |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1184 |
in method ctxt thms args insts decls t end |
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
1185 |
|
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
1186 |
fun method_for rule = with_tracing rule (choose (verit_rule_of rule)) |
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
1187 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1188 |
fun discharge ctxt [thm] t = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1189 |
SMT_Replay_Methods.prove ctxt t (fn _ => |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1190 |
resolve_tac ctxt [thm] THEN_ALL_NEW (resolve_tac ctxt @{thms refl})) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69593
diff
changeset
|
1191 |
|
69205
8050734eee3e
add reconstruction by veriT in method smt
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
1192 |
end; |