author | wenzelm |
Thu, 26 Aug 2021 14:45:19 +0200 | |
changeset 74200 | 17090e27aae9 |
parent 72458 | b44e894796d5 |
child 74266 | 612b7e0d6721 |
permissions | -rw-r--r-- |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
1 |
(* Title: HOL/Tools/SMT/smt_replay_methods.ML |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
2 |
Author: Sascha Boehme, TU Muenchen |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
3 |
Author: Jasmin Blanchette, TU Muenchen |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
4 |
Author: Mathias Fleury, MPII |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
5 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
6 |
Proof methods for replaying SMT proofs. |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
7 |
*) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
8 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
9 |
signature SMT_REPLAY_METHODS = |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
10 |
sig |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
11 |
(*Printing*) |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
12 |
val pretty_goal: Proof.context -> string -> string -> thm list -> term -> Pretty.T |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
13 |
val trace_goal: Proof.context -> string -> thm list -> term -> unit |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
14 |
val trace: Proof.context -> (unit -> string) -> unit |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
15 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
16 |
(*Replaying*) |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
17 |
val replay_error: Proof.context -> string -> string -> thm list -> term -> 'a |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
18 |
val replay_rule_error: string -> Proof.context -> string -> thm list -> term -> 'a |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
19 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
20 |
(*theory lemma methods*) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
21 |
type th_lemma_method = Proof.context -> thm list -> term -> thm |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
22 |
val add_th_lemma_method: string * th_lemma_method -> Context.generic -> |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
23 |
Context.generic |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
24 |
val get_th_lemma_method: Proof.context -> th_lemma_method Symtab.table |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
25 |
val discharge: int -> thm list -> thm -> thm |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
26 |
val match_instantiate: Proof.context -> term -> thm -> thm |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
27 |
val prove: Proof.context -> term -> (Proof.context -> int -> tactic) -> thm |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
28 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
29 |
val prove_arith_rewrite: ((term -> int * term Termtab.table -> |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
30 |
term * (int * term Termtab.table)) -> term -> int * term Termtab.table -> |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
31 |
term * (int * term Termtab.table)) -> Proof.context -> term -> thm |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
32 |
|
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
33 |
(*abstraction*) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
34 |
type abs_context = int * term Termtab.table |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
35 |
type 'a abstracter = term -> abs_context -> 'a * abs_context |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
36 |
val add_arith_abstracter: (term abstracter -> term option abstracter) -> |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
37 |
Context.generic -> Context.generic |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
38 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
39 |
val abstract_lit: term -> abs_context -> term * abs_context |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
40 |
val abstract_conj: term -> abs_context -> term * abs_context |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
41 |
val abstract_disj: term -> abs_context -> term * abs_context |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
42 |
val abstract_not: (term -> abs_context -> term * abs_context) -> |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
43 |
term -> abs_context -> term * abs_context |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
44 |
val abstract_unit: term -> abs_context -> term * abs_context |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
45 |
val abstract_bool: term -> abs_context -> term * abs_context |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
46 |
(* also abstracts over equivalences and conjunction and implication*) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
47 |
val abstract_bool_shallow: term -> abs_context -> term * abs_context |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
48 |
(* abstracts down to equivalence symbols *) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
49 |
val abstract_bool_shallow_equivalence: term -> abs_context -> term * abs_context |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
50 |
val abstract_prop: term -> abs_context -> term * abs_context |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
51 |
val abstract_term: term -> abs_context -> term * abs_context |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
52 |
val abstract_eq: (term -> int * term Termtab.table -> term * (int * term Termtab.table)) -> |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
53 |
term -> int * term Termtab.table -> term * (int * term Termtab.table) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
54 |
val abstract_neq: (term -> int * term Termtab.table -> term * (int * term Termtab.table)) -> |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
55 |
term -> int * term Termtab.table -> term * (int * term Termtab.table) |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
56 |
val abstract_arith: Proof.context -> term -> abs_context -> term * abs_context |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
57 |
(* also abstracts over if-then-else *) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
58 |
val abstract_arith_shallow: Proof.context -> term -> abs_context -> term * abs_context |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
59 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
60 |
val prove_abstract: Proof.context -> thm list -> term -> |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
61 |
(Proof.context -> thm list -> int -> tactic) -> |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
62 |
(abs_context -> (term list * term) * abs_context) -> thm |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
63 |
val prove_abstract': Proof.context -> term -> (Proof.context -> thm list -> int -> tactic) -> |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
64 |
(abs_context -> term * abs_context) -> thm |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
65 |
val try_provers: string -> Proof.context -> string -> (string * (term -> 'a)) list -> thm list -> |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
66 |
term -> 'a |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
67 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
68 |
(*shared tactics*) |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
69 |
val cong_unfolding_trivial: Proof.context -> thm list -> term -> thm |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
70 |
val cong_basic: Proof.context -> thm list -> term -> thm |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
71 |
val cong_full: Proof.context -> thm list -> term -> thm |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
72 |
val cong_unfolding_first: Proof.context -> thm list -> term -> thm |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
73 |
val arith_th_lemma: Proof.context -> thm list -> term -> thm |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
74 |
val arith_th_lemma_wo: Proof.context -> thm list -> term -> thm |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
75 |
val arith_th_lemma_wo_shallow: Proof.context -> thm list -> term -> thm |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
76 |
val arith_th_lemma_tac_with_wo: Proof.context -> thm list -> int -> tactic |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
77 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
78 |
val dest_thm: thm -> term |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
79 |
val prop_tac: Proof.context -> thm list -> int -> tactic |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
80 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
81 |
val certify_prop: Proof.context -> term -> cterm |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
82 |
val dest_prop: term -> term |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
83 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
84 |
end; |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
85 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
86 |
structure SMT_Replay_Methods: SMT_REPLAY_METHODS = |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
87 |
struct |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
88 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
89 |
(* utility functions *) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
90 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
91 |
fun trace ctxt f = SMT_Config.trace_msg ctxt f () |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
92 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
93 |
fun pretty_thm ctxt thm = Syntax.pretty_term ctxt (Thm.concl_of thm) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
94 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
95 |
fun pretty_goal ctxt msg rule thms t = |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
96 |
let |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
97 |
val full_msg = msg ^ ": " ^ quote rule |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
98 |
val assms = |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
99 |
if null thms then [] |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
100 |
else [Pretty.big_list "assumptions:" (map (pretty_thm ctxt) thms)] |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
101 |
val concl = Pretty.big_list "proposition:" [Syntax.pretty_term ctxt t] |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
102 |
in Pretty.big_list full_msg (assms @ [concl]) end |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
103 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
104 |
fun replay_error ctxt msg rule thms t = error (Pretty.string_of (pretty_goal ctxt msg rule thms t)) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
105 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
106 |
fun replay_rule_error name ctxt = replay_error ctxt ("Failed to replay" ^ name ^ " proof step") |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
107 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
108 |
fun trace_goal ctxt rule thms t = |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
109 |
trace ctxt (fn () => Pretty.string_of (pretty_goal ctxt "Goal" rule thms t)) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
110 |
|
69593 | 111 |
fun as_prop (t as Const (\<^const_name>\<open>Trueprop\<close>, _) $ _) = t |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
112 |
| as_prop t = HOLogic.mk_Trueprop t |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
113 |
|
69593 | 114 |
fun dest_prop (Const (\<^const_name>\<open>Trueprop\<close>, _) $ t) = t |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
115 |
| dest_prop t = t |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
116 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
117 |
fun dest_thm thm = dest_prop (Thm.concl_of thm) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
118 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
119 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
120 |
(* plug-ins *) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
121 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
122 |
type abs_context = int * term Termtab.table |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
123 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
124 |
type 'a abstracter = term -> abs_context -> 'a * abs_context |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
125 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
126 |
type th_lemma_method = Proof.context -> thm list -> term -> thm |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
127 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
128 |
fun id_ord ((id1, _), (id2, _)) = int_ord (id1, id2) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
129 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
130 |
structure Plugins = Generic_Data |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
131 |
( |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
132 |
type T = |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
133 |
(int * (term abstracter -> term option abstracter)) list * |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
134 |
th_lemma_method Symtab.table |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
135 |
val empty = ([], Symtab.empty) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
136 |
val extend = I |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
137 |
fun merge ((abss1, ths1), (abss2, ths2)) = ( |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
138 |
Ord_List.merge id_ord (abss1, abss2), |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
139 |
Symtab.merge (K true) (ths1, ths2)) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
140 |
) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
141 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
142 |
fun add_arith_abstracter abs = Plugins.map (apfst (Ord_List.insert id_ord (serial (), abs))) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
143 |
fun get_arith_abstracters ctxt = map snd (fst (Plugins.get (Context.Proof ctxt))) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
144 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
145 |
fun add_th_lemma_method method = Plugins.map (apsnd (Symtab.update_new method)) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
146 |
fun get_th_lemma_method ctxt = snd (Plugins.get (Context.Proof ctxt)) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
147 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
148 |
fun match ctxt pat t = |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
149 |
(Vartab.empty, Vartab.empty) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
150 |
|> Pattern.first_order_match (Proof_Context.theory_of ctxt) (pat, t) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
151 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
152 |
fun gen_certify_inst sel cert ctxt thm t = |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
153 |
let |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
154 |
val inst = match ctxt (dest_thm thm) (dest_prop t) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
155 |
fun cert_inst (ix, (a, b)) = ((ix, a), cert b) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
156 |
in Vartab.fold (cons o cert_inst) (sel inst) [] end |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
157 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
158 |
fun match_instantiateT ctxt t thm = |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
159 |
if Term.exists_type (Term.exists_subtype Term.is_TVar) (dest_thm thm) then |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
160 |
Thm.instantiate (gen_certify_inst fst (Thm.ctyp_of ctxt) ctxt thm t, []) thm |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
161 |
else thm |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
162 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
163 |
fun match_instantiate ctxt t thm = |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
164 |
let val thm' = match_instantiateT ctxt t thm in |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
165 |
Thm.instantiate ([], gen_certify_inst snd (Thm.cterm_of ctxt) ctxt thm' t) thm' |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
166 |
end |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
167 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
168 |
fun discharge _ [] thm = thm |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
169 |
| discharge i (rule :: rules) thm = discharge (i + Thm.nprems_of rule) rules (rule RSN (i, thm)) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
170 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
171 |
fun by_tac ctxt thms ns ts t tac = |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
172 |
Goal.prove ctxt [] (map as_prop ts) (as_prop t) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
173 |
(fn {context, prems} => HEADGOAL (tac context prems)) |
74200
17090e27aae9
more scalable data structure (but: rarely used with > 5 arguments);
wenzelm
parents:
72458
diff
changeset
|
174 |
|> Drule.generalize (Symtab.empty, Symtab.make_set ns) |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
175 |
|> discharge 1 thms |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
176 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
177 |
fun prove ctxt t tac = by_tac ctxt [] [] [] t (K o tac) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
178 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
179 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
180 |
(* abstraction *) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
181 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
182 |
fun prove_abstract ctxt thms t tac f = |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
183 |
let |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
184 |
val ((prems, concl), (_, ts)) = f (1, Termtab.empty) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
185 |
val ns = Termtab.fold (fn (_, v) => cons (fst (Term.dest_Free v))) ts [] |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
186 |
in |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
187 |
by_tac ctxt [] ns prems concl tac |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
188 |
|> match_instantiate ctxt t |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
189 |
|> discharge 1 thms |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
190 |
end |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
191 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
192 |
fun prove_abstract' ctxt t tac f = |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
193 |
prove_abstract ctxt [] t tac (f #>> pair []) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
194 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
195 |
fun lookup_term (_, terms) t = Termtab.lookup terms t |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
196 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
197 |
fun abstract_sub t f cx = |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
198 |
(case lookup_term cx t of |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
199 |
SOME v => (v, cx) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
200 |
| NONE => f cx) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
201 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
202 |
fun mk_fresh_free t (i, terms) = |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
203 |
let val v = Free ("t" ^ string_of_int i, fastype_of t) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
204 |
in (v, (i + 1, Termtab.update (t, v) terms)) end |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
205 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
206 |
fun apply_abstracters _ [] _ cx = (NONE, cx) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
207 |
| apply_abstracters abs (abstracter :: abstracters) t cx = |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
208 |
(case abstracter abs t cx of |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
209 |
(NONE, _) => apply_abstracters abs abstracters t cx |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
210 |
| x as (SOME _, _) => x) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
211 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
212 |
fun abstract_term (t as _ $ _) = abstract_sub t (mk_fresh_free t) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
213 |
| abstract_term (t as Abs _) = abstract_sub t (mk_fresh_free t) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
214 |
| abstract_term t = pair t |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
215 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
216 |
fun abstract_bin abs f t t1 t2 = abstract_sub t (abs t1 ##>> abs t2 #>> f) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
217 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
218 |
fun abstract_ter abs f t t1 t2 t3 = |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
219 |
abstract_sub t (abs t1 ##>> abs t2 ##>> abs t3 #>> (Scan.triple1 #> f)) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
220 |
|
69597 | 221 |
fun abstract_lit (\<^const>\<open>HOL.Not\<close> $ t) = abstract_term t #>> HOLogic.mk_not |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
222 |
| abstract_lit t = abstract_term t |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
223 |
|
69597 | 224 |
fun abstract_not abs (t as \<^const>\<open>HOL.Not\<close> $ t1) = |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
225 |
abstract_sub t (abs t1 #>> HOLogic.mk_not) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
226 |
| abstract_not _ t = abstract_lit t |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
227 |
|
69597 | 228 |
fun abstract_conj (t as \<^const>\<open>HOL.conj\<close> $ t1 $ t2) = |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
229 |
abstract_bin abstract_conj HOLogic.mk_conj t t1 t2 |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
230 |
| abstract_conj t = abstract_lit t |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
231 |
|
69597 | 232 |
fun abstract_disj (t as \<^const>\<open>HOL.disj\<close> $ t1 $ t2) = |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
233 |
abstract_bin abstract_disj HOLogic.mk_disj t t1 t2 |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
234 |
| abstract_disj t = abstract_lit t |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
235 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
236 |
fun abstract_prop (t as (c as @{const If (bool)}) $ t1 $ t2 $ t3) = |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
237 |
abstract_ter abstract_prop (fn (t1, t2, t3) => c $ t1 $ t2 $ t3) t t1 t2 t3 |
69597 | 238 |
| abstract_prop (t as \<^const>\<open>HOL.disj\<close> $ t1 $ t2) = |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
239 |
abstract_bin abstract_prop HOLogic.mk_disj t t1 t2 |
69597 | 240 |
| abstract_prop (t as \<^const>\<open>HOL.conj\<close> $ t1 $ t2) = |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
241 |
abstract_bin abstract_prop HOLogic.mk_conj t t1 t2 |
69597 | 242 |
| abstract_prop (t as \<^const>\<open>HOL.implies\<close> $ t1 $ t2) = |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
243 |
abstract_bin abstract_prop HOLogic.mk_imp t t1 t2 |
69593 | 244 |
| abstract_prop (t as \<^term>\<open>HOL.eq :: bool => _\<close> $ t1 $ t2) = |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
245 |
abstract_bin abstract_prop HOLogic.mk_eq t t1 t2 |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
246 |
| abstract_prop t = abstract_not abstract_prop t |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
247 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
248 |
fun abstract_arith ctxt u = |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
249 |
let |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
250 |
fun abs (t as (Const (\<^const_name>\<open>HOL.The\<close>, _) $ Abs (_, _, _))) = |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
251 |
abstract_sub t (abstract_term t) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
252 |
| abs (t as (c as Const _) $ Abs (s, T, t')) = |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
253 |
abstract_sub t (abs t' #>> (fn u' => c $ Abs (s, T, u'))) |
69593 | 254 |
| abs (t as (c as Const (\<^const_name>\<open>If\<close>, _)) $ t1 $ t2 $ t3) = |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
255 |
abstract_ter abs (fn (t1, t2, t3) => c $ t1 $ t2 $ t3) t t1 t2 t3 |
69597 | 256 |
| abs (t as \<^const>\<open>HOL.Not\<close> $ t1) = abstract_sub t (abs t1 #>> HOLogic.mk_not) |
257 |
| abs (t as \<^const>\<open>HOL.disj\<close> $ t1 $ t2) = |
|
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
258 |
abstract_sub t (abs t1 ##>> abs t2 #>> HOLogic.mk_disj) |
69593 | 259 |
| abs (t as (c as Const (\<^const_name>\<open>uminus_class.uminus\<close>, _)) $ t1) = |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
260 |
abstract_sub t (abs t1 #>> (fn u => c $ u)) |
69593 | 261 |
| abs (t as (c as Const (\<^const_name>\<open>plus_class.plus\<close>, _)) $ t1 $ t2) = |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
262 |
abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2)) |
69593 | 263 |
| abs (t as (c as Const (\<^const_name>\<open>minus_class.minus\<close>, _)) $ t1 $ t2) = |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
264 |
abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2)) |
69593 | 265 |
| abs (t as (c as Const (\<^const_name>\<open>times_class.times\<close>, _)) $ t1 $ t2) = |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
266 |
abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2)) |
69593 | 267 |
| abs (t as (c as Const (\<^const_name>\<open>z3div\<close>, _)) $ t1 $ t2) = |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
268 |
abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2)) |
69593 | 269 |
| abs (t as (c as Const (\<^const_name>\<open>z3mod\<close>, _)) $ t1 $ t2) = |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
270 |
abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2)) |
69593 | 271 |
| abs (t as (c as Const (\<^const_name>\<open>HOL.eq\<close>, _)) $ t1 $ t2) = |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
272 |
abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2)) |
69593 | 273 |
| abs (t as (c as Const (\<^const_name>\<open>ord_class.less\<close>, _)) $ t1 $ t2) = |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
274 |
abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2)) |
69593 | 275 |
| abs (t as (c as Const (\<^const_name>\<open>ord_class.less_eq\<close>, _)) $ t1 $ t2) = |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
276 |
abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2)) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
277 |
| abs t = abstract_sub t (fn cx => |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
278 |
if can HOLogic.dest_number t then (t, cx) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
279 |
else |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
280 |
(case apply_abstracters abs (get_arith_abstracters ctxt) t cx of |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
281 |
(SOME u, cx') => (u, cx') |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
282 |
| (NONE, _) => abstract_term t cx)) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
283 |
in abs u end |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
284 |
|
69597 | 285 |
fun abstract_unit (t as (\<^const>\<open>HOL.Not\<close> $ (\<^const>\<open>HOL.disj\<close> $ t1 $ t2))) = |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
286 |
abstract_sub t (abstract_unit t1 ##>> abstract_unit t2 #>> |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
287 |
HOLogic.mk_not o HOLogic.mk_disj) |
69597 | 288 |
| abstract_unit (t as (\<^const>\<open>HOL.disj\<close> $ t1 $ t2)) = |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
289 |
abstract_sub t (abstract_unit t1 ##>> abstract_unit t2 #>> |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
290 |
HOLogic.mk_disj) |
69593 | 291 |
| abstract_unit (t as (Const(\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2)) = |
292 |
if fastype_of t1 = \<^typ>\<open>bool\<close> then |
|
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
293 |
abstract_sub t (abstract_unit t1 ##>> abstract_unit t2 #>> |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
294 |
HOLogic.mk_eq) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
295 |
else abstract_lit t |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
296 |
| abstract_unit (t as (\<^const>\<open>HOL.Not\<close> $ (Const(\<^const_name>\<open>HOL.eq\<close>, _) $ t1 $ t2))) = |
69593 | 297 |
if fastype_of t1 = \<^typ>\<open>bool\<close> then |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
298 |
abstract_sub t (abstract_unit t1 ##>> abstract_unit t2 #>> |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
299 |
HOLogic.mk_eq #>> HOLogic.mk_not) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
300 |
else abstract_lit t |
69597 | 301 |
| abstract_unit (t as (\<^const>\<open>HOL.Not\<close> $ t1)) = |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
302 |
abstract_sub t (abstract_unit t1 #>> HOLogic.mk_not) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
303 |
| abstract_unit t = abstract_lit t |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
304 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
305 |
fun abstract_bool (t as (@{const HOL.disj} $ t1 $ t2)) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
306 |
abstract_sub t (abstract_bool t1 ##>> abstract_bool t2 #>> |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
307 |
HOLogic.mk_disj) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
308 |
| abstract_bool (t as (@{const HOL.conj} $ t1 $ t2)) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
309 |
abstract_sub t (abstract_bool t1 ##>> abstract_bool t2 #>> |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
310 |
HOLogic.mk_conj) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
311 |
| abstract_bool (t as (Const(@{const_name HOL.eq}, _) $ t1 $ t2)) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
312 |
if fastype_of t1 = @{typ bool} then |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
313 |
abstract_sub t (abstract_bool t1 ##>> abstract_bool t2 #>> |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
314 |
HOLogic.mk_eq) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
315 |
else abstract_lit t |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
316 |
| abstract_bool (t as (@{const HOL.Not} $ t1)) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
317 |
abstract_sub t (abstract_bool t1 #>> HOLogic.mk_not) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
318 |
| abstract_bool (t as (@{const HOL.implies} $ t1 $ t2)) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
319 |
abstract_sub t (abstract_bool t1 ##>> abstract_bool t2 #>> |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
320 |
HOLogic.mk_imp) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
321 |
| abstract_bool t = abstract_lit t |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
322 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
323 |
fun abstract_bool_shallow (t as (@{const HOL.disj} $ t1 $ t2)) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
324 |
abstract_sub t (abstract_bool_shallow t1 ##>> abstract_bool_shallow t2 #>> |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
325 |
HOLogic.mk_disj) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
326 |
| abstract_bool_shallow (t as (@{const HOL.Not} $ t1)) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
327 |
abstract_sub t (abstract_bool_shallow t1 #>> HOLogic.mk_not) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
328 |
| abstract_bool_shallow t = abstract_term t |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
329 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
330 |
fun abstract_bool_shallow_equivalence (t as (@{const HOL.disj} $ t1 $ t2)) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
331 |
abstract_sub t (abstract_bool_shallow_equivalence t1 ##>> abstract_bool_shallow_equivalence t2 #>> |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
332 |
HOLogic.mk_disj) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
333 |
| abstract_bool_shallow_equivalence (t as (Const(@{const_name HOL.eq}, _) $ t1 $ t2)) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
334 |
if fastype_of t1 = @{typ bool} then |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
335 |
abstract_sub t (abstract_lit t1 ##>> abstract_lit t2 #>> |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
336 |
HOLogic.mk_eq) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
337 |
else abstract_lit t |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
338 |
| abstract_bool_shallow_equivalence (t as (@{const HOL.Not} $ t1)) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
339 |
abstract_sub t (abstract_bool_shallow_equivalence t1 #>> HOLogic.mk_not) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
340 |
| abstract_bool_shallow_equivalence t = abstract_lit t |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
341 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
342 |
fun abstract_arith_shallow ctxt u = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
343 |
let |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
344 |
fun abs (t as (Const (\<^const_name>\<open>HOL.The\<close>, _) $ Abs (_, _, _))) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
345 |
abstract_sub t (abstract_term t) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
346 |
| abs (t as (c as Const _) $ Abs (s, T, t')) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
347 |
abstract_sub t (abs t' #>> (fn u' => c $ Abs (s, T, u'))) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
348 |
| abs (t as (Const (\<^const_name>\<open>If\<close>, _)) $ _ $ _ $ _) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
349 |
abstract_sub t (abstract_term t) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
350 |
| abs (t as \<^const>\<open>HOL.Not\<close> $ t1) = abstract_sub t (abs t1 #>> HOLogic.mk_not) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
351 |
| abs (t as \<^const>\<open>HOL.disj\<close> $ t1 $ t2) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
352 |
abstract_sub t (abs t1 ##>> abs t2 #>> HOLogic.mk_disj) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
353 |
| abs (t as (c as Const (\<^const_name>\<open>uminus_class.uminus\<close>, _)) $ t1) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
354 |
abstract_sub t (abs t1 #>> (fn u => c $ u)) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
355 |
| abs (t as (c as Const (\<^const_name>\<open>plus_class.plus\<close>, _)) $ t1 $ t2) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
356 |
abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2)) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
357 |
| abs (t as (c as Const (\<^const_name>\<open>minus_class.minus\<close>, _)) $ t1 $ t2) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
358 |
abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2)) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
359 |
| abs (t as (c as Const (\<^const_name>\<open>times_class.times\<close>, _)) $ t1 $ t2) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
360 |
abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2)) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
361 |
| abs (t as (Const (\<^const_name>\<open>z3div\<close>, _)) $ _ $ _) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
362 |
abstract_sub t (abstract_term t) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
363 |
| abs (t as (Const (\<^const_name>\<open>z3mod\<close>, _)) $ _ $ _) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
364 |
abstract_sub t (abstract_term t) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
365 |
| abs (t as (c as 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:
69597
diff
changeset
|
366 |
abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2)) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
367 |
| abs (t as (c as Const (\<^const_name>\<open>ord_class.less\<close>, _)) $ t1 $ t2) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
368 |
abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2)) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
369 |
| abs (t as (c as Const (\<^const_name>\<open>ord_class.less_eq\<close>, _)) $ t1 $ t2) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
370 |
abstract_sub t (abs t1 ##>> abs t2 #>> (fn (u1, u2) => c $ u1 $ u2)) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
371 |
| abs t = abstract_sub t (fn cx => |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
372 |
if can HOLogic.dest_number t then (t, cx) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
373 |
else |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
374 |
(case apply_abstracters abs (get_arith_abstracters ctxt) t cx of |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
375 |
(SOME u, cx') => (u, cx') |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
376 |
| (NONE, _) => abstract_term t cx)) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
377 |
in abs u end |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
378 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
379 |
(* theory lemmas *) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
380 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
381 |
fun try_provers prover_name ctxt rule [] thms t = replay_rule_error prover_name ctxt rule thms t |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
382 |
| try_provers prover_name ctxt rule ((name, prover) :: named_provers) thms t = |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
383 |
(case (trace ctxt (K ("Trying prover " ^ quote name)); try prover t) of |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
384 |
SOME thm => thm |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
385 |
| NONE => try_provers prover_name ctxt rule named_provers thms t) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
386 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
387 |
(*theory-lemma*) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
388 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
389 |
fun arith_th_lemma_tac ctxt prems = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
390 |
Method.insert_tac ctxt prems |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
391 |
THEN' SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms z3div_def z3mod_def}) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
392 |
THEN' Arith_Data.arith_tac ctxt |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
393 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
394 |
fun arith_th_lemma ctxt thms t = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
395 |
prove_abstract ctxt thms t arith_th_lemma_tac ( |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
396 |
fold_map (abstract_arith ctxt o dest_thm) thms ##>> |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
397 |
abstract_arith ctxt (dest_prop t)) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
398 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
399 |
fun arith_th_lemma_tac_with_wo ctxt prems = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
400 |
Method.insert_tac ctxt prems |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
401 |
THEN' SELECT_GOAL (Local_Defs.unfold0_tac ctxt @{thms z3div_def z3mod_def int_distrib}) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
402 |
THEN' Simplifier.asm_full_simp_tac |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
403 |
(empty_simpset ctxt addsimprocs [(*@{simproc linordered_ring_strict_eq_cancel_factor_poly}, |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
404 |
@{simproc linordered_ring_strict_le_cancel_factor_poly}, |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
405 |
@{simproc linordered_ring_strict_less_cancel_factor_poly}, |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
406 |
@{simproc nat_eq_cancel_factor_poly}, |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
407 |
@{simproc nat_le_cancel_factor_poly}, |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
408 |
@{simproc nat_less_cancel_factor_poly}*)]) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
409 |
THEN' (fn i => TRY (Arith_Data.arith_tac ctxt i)) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
410 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
411 |
fun arith_th_lemma_wo ctxt thms t = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
412 |
prove_abstract ctxt thms t arith_th_lemma_tac_with_wo ( |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
413 |
fold_map (abstract_arith ctxt o dest_thm) thms ##>> |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
414 |
abstract_arith ctxt (dest_prop t)) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
415 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
416 |
fun arith_th_lemma_wo_shallow ctxt thms t = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
417 |
prove_abstract ctxt thms t arith_th_lemma_tac_with_wo ( |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
418 |
fold_map (abstract_arith_shallow ctxt o dest_thm) thms ##>> |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
419 |
abstract_arith_shallow ctxt (dest_prop t)) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
420 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
421 |
val _ = Theory.setup (Context.theory_map (add_th_lemma_method ("arith", arith_th_lemma))) |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
422 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
423 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
424 |
(* congruence *) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
425 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
426 |
fun certify_prop ctxt t = Thm.cterm_of ctxt (as_prop t) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
427 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
428 |
fun ctac ctxt prems i st = st |> ( |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
429 |
resolve_tac ctxt (@{thm refl} :: prems) i |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
430 |
ORELSE (cong_tac ctxt i THEN ctac ctxt prems (i + 1) THEN ctac ctxt prems i)) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
431 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
432 |
fun cong_basic ctxt thms t = |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
433 |
let val st = Thm.trivial (certify_prop ctxt t) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
434 |
in |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
435 |
(case Seq.pull (ctac ctxt thms 1 st) of |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
436 |
SOME (thm, _) => thm |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
437 |
| NONE => raise THM ("cong", 0, thms @ [st])) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
438 |
end |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
439 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
440 |
val cong_dest_rules = @{lemma |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
441 |
"(\<not> P \<or> Q) \<and> (P \<or> \<not> Q) \<Longrightarrow> P = Q" |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
442 |
"(P \<or> \<not> Q) \<and> (\<not> P \<or> Q) \<Longrightarrow> P = Q" |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
443 |
by fast+} |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
444 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
445 |
fun cong_full_core_tac ctxt = |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
446 |
eresolve_tac ctxt @{thms subst} |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
447 |
THEN' resolve_tac ctxt @{thms refl} |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
448 |
ORELSE' Classical.fast_tac ctxt |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
449 |
|
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
450 |
fun cong_full ctxt thms t = prove ctxt t (fn ctxt' => |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
451 |
Method.insert_tac ctxt thms |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
452 |
THEN' (cong_full_core_tac ctxt' |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
453 |
ORELSE' dresolve_tac ctxt cong_dest_rules |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
454 |
THEN' cong_full_core_tac ctxt')) |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
455 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
456 |
local |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
457 |
val reorder_for_simp = try (fn thm => |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
458 |
let val t = Thm.prop_of (@{thm eq_reflection} OF [thm]) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
459 |
val thm = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
460 |
(case Logic.dest_equals t of |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
461 |
(t1, t2) => |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
462 |
if t1 aconv t2 then raise TERM("identical terms", [t1, t2]) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
463 |
else if Term.size_of_term t1 > Term.size_of_term t2 then @{thm eq_reflection} OF [thm] |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
464 |
else @{thm eq_reflection} OF [@{thm sym} OF [thm]]) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
465 |
handle TERM("dest_equals", _) => @{thm eq_reflection} OF [thm] |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
466 |
in thm end) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
467 |
in |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
468 |
fun cong_unfolding_trivial ctxt thms t = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
469 |
prove ctxt t (fn _ => |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
470 |
EVERY' (map (fn thm => K (unfold_tac ctxt [thm])) ((map_filter reorder_for_simp thms))) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
471 |
THEN' (fn i => TRY (resolve_tac ctxt @{thms refl} i))) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
472 |
|
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
473 |
fun cong_unfolding_first ctxt thms t = |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
474 |
let val ctxt = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
475 |
ctxt |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
476 |
|> empty_simpset |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
477 |
|> put_simpset HOL_basic_ss |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
478 |
|> (fn ctxt => ctxt addsimps @{thms not_not eq_commute}) |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
479 |
in |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
480 |
prove ctxt t (fn _ => |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
481 |
EVERY' (map (fn thm => K (unfold_tac ctxt [thm])) ((map_filter reorder_for_simp thms))) |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
482 |
THEN' Method.insert_tac ctxt thms |
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
483 |
THEN' (full_simp_tac ctxt) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
484 |
THEN' K (ALLGOALS (K (Clasimp.auto_tac ctxt)))) |
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
485 |
end |
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
486 |
|
72458
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
487 |
end |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
488 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
489 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
490 |
fun arith_rewrite_tac ctxt _ = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
491 |
let val backup_tac = Arith_Data.arith_tac ctxt ORELSE' Clasimp.force_tac ctxt in |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
492 |
(TRY o Simplifier.simp_tac ctxt) THEN_ALL_NEW backup_tac |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
493 |
ORELSE' backup_tac |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
494 |
end |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
495 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
496 |
fun abstract_eq f (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:
69597
diff
changeset
|
497 |
f t1 ##>> f t2 #>> HOLogic.mk_eq |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
498 |
| abstract_eq _ t = abstract_term t |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
499 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
500 |
fun abstract_neq f (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:
69597
diff
changeset
|
501 |
f t1 ##>> f t2 #>> HOLogic.mk_eq |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
502 |
| abstract_neq f (Const (\<^const_name>\<open>HOL.Not\<close>, _) $ (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:
69597
diff
changeset
|
503 |
f t1 ##>> f t2 #>> HOLogic.mk_eq #>> curry (op $) HOLogic.Not |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
504 |
| abstract_neq f (Const (\<^const_name>\<open>HOL.disj\<close>, _) $ t1 $ t2) = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
505 |
f t1 ##>> f t2 #>> HOLogic.mk_disj |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
506 |
| abstract_neq _ t = abstract_term t |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
507 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
508 |
fun prove_arith_rewrite abstracter ctxt t = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
509 |
prove_abstract' ctxt t arith_rewrite_tac ( |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
510 |
abstracter (abstract_arith ctxt) (dest_prop t)) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
511 |
|
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
512 |
fun prop_tac ctxt prems = |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
513 |
Method.insert_tac ctxt prems |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
514 |
THEN' SUBGOAL (fn (prop, i) => |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
515 |
if Term.size_of_term prop > 100 then SAT.satx_tac ctxt i |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
516 |
else (Classical.fast_tac ctxt ORELSE' Clasimp.force_tac ctxt) i) |
b44e894796d5
add reconstruction for the SMT solver veriT
Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
69597
diff
changeset
|
517 |
|
69204
d5ab1636660b
split SMT reconstruction into library
fleury <Mathias.Fleury@mpi-inf.mpg.de>
parents:
diff
changeset
|
518 |
end; |