diff --git a/src/HOL/SMT_Examples/SMT_Tests_Verit.thy b/src/HOL/SMT_Examples/SMT_Tests_Verit.thy --- a/src/HOL/SMT_Examples/SMT_Tests_Verit.thy +++ b/src/HOL/SMT_Examples/SMT_Tests_Verit.thy @@ -1,720 +1,736 @@ (* Title: HOL/SMT_Examples/SMT_Tests.thy Author: Sascha Boehme, TU Muenchen Author: Mathias Fleury, MPII, JKU *) section \Tests for the SMT binding\ theory SMT_Tests_Verit imports Complex_Main begin declare [[smt_solver=verit]] smt_status text \Most examples are taken from the equivalent Z3 theory called \<^file>\SMT_Tests.thy\, and have been taken from various Isabelle and HOL4 developments.\ section \Propositional logic\ lemma "True" "\ False" "\ \ True" "True \ True" "True \ False" "False \ True" "\ (False \ True)" by smt+ lemma "P \ \ P" "\ (P \ \ P)" "(True \ P) \ \ P \ (False \ P) \ P" "P \ P" "P \ \ P \ False" "P \ Q \ Q \ P" "P \ Q \ Q \ P" "P \ Q \ P \ Q" "\ (P \ Q) \ \ P" "\ (P \ Q) \ \ Q" "\ P \ \ (P \ Q)" "\ Q \ \ (P \ Q)" "(P \ Q) \ (\ (\ P \ \ Q))" "(P \ Q) \ R \ P \ (Q \ R)" "(P \ Q) \ R \ P \ (Q \ R)" "(P \ Q) \ R \ (P \ R) \ (Q \ R)" "(P \ R) \ (Q \ R) \ (P \ Q) \ R" "(P \ Q) \ R \ (P \ R) \ (Q \ R)" "(P \ R) \ (Q \ R) \ (P \ Q) \ R" "((P \ Q) \ P) \ P" "(P \ R) \ (Q \ R) \ (P \ Q \ R)" "(P \ Q \ R) \ (P \ (Q \ R))" "((P \ R) \ R) \ ((Q \ R) \ R) \ (P \ Q \ R) \ R" "\ (P \ R) \ \ (Q \ R) \ \ (P \ Q \ R)" "(P \ Q \ R) \ (P \ Q) \ (P \ R)" "P \ (Q \ P)" "(P \ Q \ R) \ (P \ Q)\ (P \ R)" "(P \ Q) \ (P \ R) \ (P \ Q \ R)" "((((P \ Q) \ P) \ P) \ Q) \ Q" "(P \ Q) \ (\ Q \ \ P)" "(P \ Q \ R) \ (P \ Q) \ (P \ R)" "(P \ Q) \ (Q \ P) \ (P \ Q)" "(P \ Q) \ (Q \ P)" "\ (P \ \ P)" "(P \ Q) \ (\ Q \ \ P)" "P \ P \ P \ P \ P \ P \ P \ P \ P \ P" by smt+ lemma "(if P then Q1 else Q2) \ ((P \ Q1) \ (\ P \ Q2))" "if P then (Q \ P) else (P \ Q)" "(if P1 \ P2 then Q1 else Q2) \ (if P1 then Q1 else if P2 then Q1 else Q2)" "(if P1 \ P2 then Q1 else Q2) \ (if P1 then if P2 then Q1 else Q2 else Q2)" "(P1 \ (if P2 then Q1 else Q2)) \ (if P1 \ P2 then P1 \ Q1 else P1 \ Q2)" by smt+ lemma "case P of True \ P | False \ \ P" "case P of False \ \ P | True \ P" "case \ P of True \ \ P | False \ P" "case P of True \ (Q \ P) | False \ (P \ Q)" by smt+ section \First-order logic with equality\ lemma "x = x" "x = y \ y = x" "x = y \ y = z \ x = z" "x = y \ f x = f y" "x = y \ g x y = g y x" "f (f x) = x \ f (f (f (f (f x)))) = x \ f x = x" "((if a then b else c) = d) = ((a \ (b = d)) \ (\ a \ (c = d)))" by smt+ lemma "\x. x = x" "(\x. P x) \ (\y. P y)" "\x. P x \ (\y. P x \ P y)" "(\x. P x \ Q x) \ (\x. P x) \ (\x. Q x)" "(\x. P x) \ R \ (\x. P x \ R)" "(\x y z. S x z) \ (\x z. S x z)" "(\x y. S x y \ S y x) \ (\x. S x y) \ S y x" "(\x. P x \ P (f x)) \ P d \ P (f(f(f(d))))" "(\x y. s x y = s y x) \ a = a \ s a b = s b a" "(\s. q s \ r s) \ \ r s \ (\s. \ r s \ \ q s \ p t \ q t) \ p t \ r t" by smt+ lemma "(\x. P x) \ R \ (\x. P x \ R)" by smt lemma "\x. x = x" "(\x. P x) \ (\y. P y)" "(\x. P x \ Q x) \ (\x. P x) \ (\x. Q x)" "(\x. P x) \ R \ (\x. P x \ R)" "(\x y z. S x z) \ (\x z. S x z)" "\ ((\x. \ P x) \ ((\x. P x) \ (\x. P x \ Q x)) \ \ (\x. P x))" by smt+ lemma "\x y. x = y" "(\x. P x) \ R \ (\x. P x \ R)" "\x. P x \ P a \ P b" "(\x. Q \ P x) \ (Q \ (\x. P x))" by smt+ lemma "(P False \ P True) \ \ P False" by smt lemma "(\ (\x. P x)) \ (\x. \ P x)" "(\x. P x \ Q) \ (\x. P x) \ Q" "(\x y. R x y = x) \ (\y. R x y) = R x c" "(if P x then \ (\y. P y) else (\y. \ P y)) \ P x \ P y" "(\x y. R x y = x) \ (\x. \y. R x y) = (\x. R x c) \ (\y. R x y) = R x c" by smt+ lemma "\x. \y. f x y = f x (g x)" "(\ \ (\x. P x)) \ (\ (\x. \ P x))" "\u. \v. \w. \x. f u v w x = f u (g u) w (h u w)" "\x. if x = y then (\y. y = x \ y \ x) else (\y. y = (x, x) \ y \ (x, x))" "\x. if x = y then (\y. y = x \ y \ x) else (\y. y = (x, x) \ y \ (x, x))" "(\x. \y. P x \ P y) \ ((\x. P x) \ (\y. P y))" "(\y. \x. R x y) \ (\x. \y. R x y)" by smt+ lemma "(\!x. P x) \ (\x. P x)" "(\!x. P x) \ (\x. P x \ (\y. y \ x \ \ P y))" "P a \ (\x. P x \ x = a) \ (\!x. P x)" "(\x. P x) \ (\x y. P x \ P y \ x = y) \ (\!x. P x)" "(\!x. P x) \ (\x. P x \ (\y. P y \ y = x) \ R) \ R" by smt+ lemma "(\x\M. P x) \ c \ M \ P c" "(\x\M. P x) \ \ (P c \ c \ M)" by smt+ lemma "let P = True in P" "let P = P1 \ P2 in P \ \ P" "let P1 = True; P2 = False in P1 \ P2 \ P2 \ P1" "(let x = y in x) = y" "(let x = y in Q x) \ (let z = y in Q z)" "(let x = y1; z = y2 in R x z) \ (let z = y2; x = y1 in R x z)" "(let x = y1; z = y2 in R x z) \ (let z = y1; x = y2 in R z x)" "let P = (\x. Q x) in if P then P else \ P" by smt+ lemma "a \ b \ a \ c \ b \ c \ (\x y. f x = f y \ y = x) \ f a \ f b" by smt lemma "(\x y z. f x y = f x z \ y = z) \ b \ c \ f a b \ f a c" "(\x y z. f x y = f z y \ x = z) \ a \ d \ f a b \ f d b" by smt+ section \Guidance for quantifier heuristics: patterns\ lemma assumes "\x. SMT.trigger (SMT.Symb_Cons (SMT.Symb_Cons (SMT.pat (f x)) SMT.Symb_Nil) SMT.Symb_Nil) (f x = x)" shows "f 1 = 1" using assms by smt lemma assumes "\x y. SMT.trigger (SMT.Symb_Cons (SMT.Symb_Cons (SMT.pat (f x)) (SMT.Symb_Cons (SMT.pat (g y)) SMT.Symb_Nil)) SMT.Symb_Nil) (f x = g y)" shows "f a = g b" using assms by smt section \Meta-logical connectives\ lemma "True \ True" "False \ True" "False \ False" "P' x \ P' x" "P \ P \ Q" "Q \ P \ Q" "\ P \ P \ Q" "Q \ P \ Q" "\P; \ Q\ \ \ (P \ Q)" "P' x \ P' x" "P' x \ Q' x \ P' x = Q' x" "P' x = Q' x \ P' x \ Q' x" "x \ y \ y \ z \ x \ (z::'a::type)" "x \ y \ (f x :: 'b::type) \ f y" "(\x. g x) \ g a \ a" "(\x y. h x y \ h y x) \ \x. h x x" "(p \ q) \ \ p \ q" "(a \ b) \ (c \ d) \ (a \ b) \ (c \ d)" by smt+ section \Natural numbers\ declare [[smt_nat_as_int]] lemma "(0::nat) = 0" "(1::nat) = 1" "(0::nat) < 1" "(0::nat) \ 1" "(123456789::nat) < 2345678901" by smt+ lemma "Suc 0 = 1" "Suc x = x + 1" "x < Suc x" "(Suc x = Suc y) = (x = y)" "Suc (x + y) < Suc x + Suc y" by smt+ lemma "(x::nat) + 0 = x" "0 + x = x" "x + y = y + x" "x + (y + z) = (x + y) + z" "(x + y = 0) = (x = 0 \ y = 0)" by smt+ lemma "(x::nat) - 0 = x" "x < y \ x - y = 0" "x - y = 0 \ y - x = 0" "(x - y) + y = (if x < y then y else x)" "x - y - z = x - (y + z)" by smt+ lemma "(x::nat) * 0 = 0" "0 * x = 0" "x * 1 = x" "1 * x = x" "3 * x = x * 3" by smt+ lemma "min (x::nat) y \ x" "min x y \ y" "min x y \ x + y" "z < x \ z < y \ z < min x y" "min x y = min y x" "min x 0 = 0" by smt+ lemma "max (x::nat) y \ x" "max x y \ y" "max x y \ (x - y) + (y - x)" "z > x \ z > y \ z > max x y" "max x y = max y x" "max x 0 = x" by smt+ lemma "0 \ (x::nat)" "0 < x \ x \ 1 \ x = 1" "x \ x" "x \ y \ 3 * x \ 3 * y" "x < y \ 3 * x < 3 * y" "x < y \ x \ y" "(x < y) = (x + 1 \ y)" "\ (x < x)" "x \ y \ y \ z \ x \ z" "x < y \ y \ z \ x \ z" "x \ y \ y < z \ x \ z" "x < y \ y < z \ x < z" "x < y \ y < z \ \ (z < x)" by smt+ declare [[smt_nat_as_int = false]] section \Integers\ lemma "(0::int) = 0" "(0::int) = (- 0)" "(1::int) = 1" "\ (-1 = (1::int))" "(0::int) < 1" "(0::int) \ 1" "-123 + 345 < (567::int)" "(123456789::int) < 2345678901" "(-123456789::int) < 2345678901" by smt+ lemma "(x::int) + 0 = x" "0 + x = x" "x + y = y + x" "x + (y + z) = (x + y) + z" "(x + y = 0) = (x = -y)" by smt+ lemma "(-1::int) = - 1" "(-3::int) = - 3" "-(x::int) < 0 \ x > 0" "x > 0 \ -x < 0" "x < 0 \ -x > 0" by smt+ lemma "(x::int) - 0 = x" "0 - x = -x" "x < y \ x - y < 0" "x - y = -(y - x)" "x - y = -y + x" "x - y - z = x - (y + z)" by smt+ lemma "(x::int) * 0 = 0" "0 * x = 0" "x * 1 = x" "1 * x = x" "x * -1 = -x" "-1 * x = -x" "3 * x = x * 3" by smt+ lemma "\x::int\ \ 0" "(\x\ = 0) = (x = 0)" "(x \ 0) = (\x\ = x)" "(x \ 0) = (\x\ = -x)" "\\x\\ = \x\" by smt+ lemma "min (x::int) y \ x" "min x y \ y" "z < x \ z < y \ z < min x y" "min x y = min y x" "x \ 0 \ min x 0 = 0" "min x y \ \x + y\" by smt+ lemma "max (x::int) y \ x" "max x y \ y" "z > x \ z > y \ z > max x y" "max x y = max y x" "x \ 0 \ max x 0 = x" "max x y \ - \x\ - \y\" by smt+ lemma "0 < (x::int) \ x \ 1 \ x = 1" "x \ x" "x \ y \ 3 * x \ 3 * y" "x < y \ 3 * x < 3 * y" "x < y \ x \ y" "(x < y) = (x + 1 \ y)" "\ (x < x)" "x \ y \ y \ z \ x \ z" "x < y \ y \ z \ x \ z" "x \ y \ y < z \ x \ z" "x < y \ y < z \ x < z" "x < y \ y < z \ \ (z < x)" by smt+ section \Reals\ lemma "(0::real) = 0" "(0::real) = -0" "(0::real) = (- 0)" "(1::real) = 1" "\ (-1 = (1::real))" "(0::real) < 1" "(0::real) \ 1" "-123 + 345 < (567::real)" "(123456789::real) < 2345678901" "(-123456789::real) < 2345678901" by smt+ lemma "(x::real) + 0 = x" "0 + x = x" "x + y = y + x" "x + (y + z) = (x + y) + z" "(x + y = 0) = (x = -y)" by smt+ lemma "(-1::real) = - 1" "(-3::real) = - 3" "-(x::real) < 0 \ x > 0" "x > 0 \ -x < 0" "x < 0 \ -x > 0" by smt+ lemma "(x::real) - 0 = x" "0 - x = -x" "x < y \ x - y < 0" "x - y = -(y - x)" "x - y = -y + x" "x - y - z = x - (y + z)" by smt+ lemma "(x::real) * 0 = 0" "0 * x = 0" "x * 1 = x" "1 * x = x" "x * -1 = -x" "-1 * x = -x" "3 * x = x * 3" by smt+ lemma "\x::real\ \ 0" "(\x\ = 0) = (x = 0)" "(x \ 0) = (\x\ = x)" "(x \ 0) = (\x\ = -x)" "\\x\\ = \x\" by smt+ lemma "min (x::real) y \ x" "min x y \ y" "z < x \ z < y \ z < min x y" "min x y = min y x" "x \ 0 \ min x 0 = 0" "min x y \ \x + y\" by smt+ lemma "max (x::real) y \ x" "max x y \ y" "z > x \ z > y \ z > max x y" "max x y = max y x" "x \ 0 \ max x 0 = x" "max x y \ - \x\ - \y\" by smt+ lemma "x \ (x::real)" "x \ y \ 3 * x \ 3 * y" "x < y \ 3 * x < 3 * y" "x < y \ x \ y" "\ (x < x)" "x \ y \ y \ z \ x \ z" "x < y \ y \ z \ x \ z" "x \ y \ y < z \ x \ z" "x < y \ y < z \ x < z" "x < y \ y < z \ \ (z < x)" by smt+ section \Datatypes, records, and typedefs\ subsection \Without support by the SMT solver\ subsubsection \Algebraic datatypes\ lemma "x = fst (x, y)" "y = snd (x, y)" "((x, y) = (y, x)) = (x = y)" "((x, y) = (u, v)) = (x = u \ y = v)" "(fst (x, y, z) = fst (u, v, w)) = (x = u)" "(snd (x, y, z) = snd (u, v, w)) = (y = v \ z = w)" "(fst (snd (x, y, z)) = fst (snd (u, v, w))) = (y = v)" "(snd (snd (x, y, z)) = snd (snd (u, v, w))) = (z = w)" "(fst (x, y) = snd (x, y)) = (x = y)" "p1 = (x, y) \ p2 = (y, x) \ fst p1 = snd p2" "(fst (x, y) = snd (x, y)) = (x = y)" "(fst p = snd p) = (p = (snd p, fst p))" using fst_conv snd_conv prod.collapse by smt+ lemma "[x] \ Nil" "[x, y] \ Nil" "x \ y \ [x] \ [y]" "hd (x # xs) = x" "tl (x # xs) = xs" "hd [x, y, z] = x" "tl [x, y, z] = [y, z]" "hd (tl [x, y, z]) = y" "tl (tl [x, y, z]) = [z]" using list.sel(1,3) list.simps by smt+ lemma "fst (hd [(a, b)]) = a" "snd (hd [(a, b)]) = b" using fst_conv snd_conv prod.collapse list.sel(1,3) list.simps by smt+ subsubsection \Records\ record point = cx :: int cy :: int record bw_point = point + black :: bool lemma "\cx = x, cy = y\ = \cx = x', cy = y'\ \ x = x' \ y = y'" using point.simps by smt lemma "cx \ cx = 3, cy = 4 \ = 3" "cy \ cx = 3, cy = 4 \ = 4" "cx \ cx = 3, cy = 4 \ \ cy \ cx = 3, cy = 4 \" "\ cx = 3, cy = 4 \ \ cx := 5 \ = \ cx = 5, cy = 4 \" "\ cx = 3, cy = 4 \ \ cy := 6 \ = \ cx = 3, cy = 6 \" "p = \ cx = 3, cy = 4 \ \ p \ cx := 3 \ \ cy := 4 \ = p" "p = \ cx = 3, cy = 4 \ \ p \ cy := 4 \ \ cx := 3 \ = p" using point.simps by smt+ lemma "\cx = x, cy = y, black = b\ = \cx = x', cy = y', black = b'\ \ x = x' \ y = y' \ b = b'" using point.simps bw_point.simps by smt lemma "cx \ cx = 3, cy = 4, black = b \ = 3" "cy \ cx = 3, cy = 4, black = b \ = 4" "black \ cx = 3, cy = 4, black = b \ = b" "cx \ cx = 3, cy = 4, black = b \ \ cy \ cx = 3, cy = 4, black = b \" "\ cx = 3, cy = 4, black = b \ \ cx := 5 \ = \ cx = 5, cy = 4, black = b \" "\ cx = 3, cy = 4, black = b \ \ cy := 6 \ = \ cx = 3, cy = 6, black = b \" "p = \ cx = 3, cy = 4, black = True \ \ p \ cx := 3 \ \ cy := 4 \ \ black := True \ = p" "p = \ cx = 3, cy = 4, black = True \ \ p \ cy := 4 \ \ black := True \ \ cx := 3 \ = p" "p = \ cx = 3, cy = 4, black = True \ \ p \ black := True \ \ cx := 3 \ \ cy := 4 \ = p" using point.simps bw_point.simps by smt+ lemma "\ cx = 3, cy = 4, black = b \ \ black := w \ = \ cx = 3, cy = 4, black = w \" "\ cx = 3, cy = 4, black = True \ \ black := False \ = \ cx = 3, cy = 4, black = False \" "p \ cx := 3 \ \ cy := 4 \ \ black := True \ = p \ black := True \ \ cy := 4 \ \ cx := 3 \" apply (smt add_One add_inc bw_point.update_convs(1) default_unit_def inc.simps(2) one_plus_BitM semiring_norm(6,26)) apply (smt bw_point.update_convs(1)) apply (smt bw_point.cases_scheme bw_point.update_convs(1) point.update_convs(1,2)) done subsubsection \Type definitions\ typedef int' = "UNIV::int set" by (rule UNIV_witness) definition n0 where "n0 = Abs_int' 0" definition n1 where "n1 = Abs_int' 1" definition n2 where "n2 = Abs_int' 2" definition plus' where "plus' n m = Abs_int' (Rep_int' n + Rep_int' m)" lemma "n0 \ n1" "plus' n1 n1 = n2" "plus' n0 n2 = n2" by (smt n0_def n1_def n2_def plus'_def Abs_int'_inverse Rep_int'_inverse UNIV_I)+ subsection \With support by the SMT solver (but without proofs)\ subsubsection \Algebraic datatypes\ lemma "x = fst (x, y)" "y = snd (x, y)" "((x, y) = (y, x)) = (x = y)" "((x, y) = (u, v)) = (x = u \ y = v)" "(fst (x, y, z) = fst (u, v, w)) = (x = u)" "(snd (x, y, z) = snd (u, v, w)) = (y = v \ z = w)" "(fst (snd (x, y, z)) = fst (snd (u, v, w))) = (y = v)" "(snd (snd (x, y, z)) = snd (snd (u, v, w))) = (z = w)" "(fst (x, y) = snd (x, y)) = (x = y)" "p1 = (x, y) \ p2 = (y, x) \ fst p1 = snd p2" "(fst (x, y) = snd (x, y)) = (x = y)" "(fst p = snd p) = (p = (snd p, fst p))" using fst_conv snd_conv prod.collapse by smt+ lemma "x \ y \ [x] \ [y]" "hd (x # xs) = x" "tl (x # xs) = xs" "hd [x, y, z] = x" "tl [x, y, z] = [y, z]" "hd (tl [x, y, z]) = y" "tl (tl [x, y, z]) = [z]" using list.sel(1,3) by smt+ lemma "fst (hd [(a, b)]) = a" "snd (hd [(a, b)]) = b" using fst_conv snd_conv prod.collapse list.sel(1,3) by smt+ subsubsection \Records\ text \The equivalent theory for Z3 contains more example, but unlike Z3, we are able to reconstruct the proofs.\ lemma "cx \ cx = 3, cy = 4 \ = 3" "cy \ cx = 3, cy = 4 \ = 4" "cx \ cx = 3, cy = 4 \ \ cy \ cx = 3, cy = 4 \" "\ cx = 3, cy = 4 \ \ cx := 5 \ = \ cx = 5, cy = 4 \" "\ cx = 3, cy = 4 \ \ cy := 6 \ = \ cx = 3, cy = 6 \" "p = \ cx = 3, cy = 4 \ \ p \ cx := 3 \ \ cy := 4 \ = p" "p = \ cx = 3, cy = 4 \ \ p \ cy := 4 \ \ cx := 3 \ = p" using point.simps by smt+ lemma "cx \ cx = 3, cy = 4, black = b \ = 3" "cy \ cx = 3, cy = 4, black = b \ = 4" "black \ cx = 3, cy = 4, black = b \ = b" "cx \ cx = 3, cy = 4, black = b \ \ cy \ cx = 3, cy = 4, black = b \" "\ cx = 3, cy = 4, black = b \ \ cx := 5 \ = \ cx = 5, cy = 4, black = b \" "\ cx = 3, cy = 4, black = b \ \ cy := 6 \ = \ cx = 3, cy = 6, black = b \" "p = \ cx = 3, cy = 4, black = True \ \ p \ cx := 3 \ \ cy := 4 \ \ black := True \ = p" "p = \ cx = 3, cy = 4, black = True \ \ p \ cy := 4 \ \ black := True \ \ cx := 3 \ = p" "p = \ cx = 3, cy = 4, black = True \ \ p \ black := True \ \ cx := 3 \ \ cy := 4 \ = p" using point.simps bw_point.simps by smt+ section \Functions\ lemma "\f. map_option f (Some x) = Some (y + x)" by (smt option.map(2)) lemma "(f (i := v)) i = v" "i1 \ i2 \ (f (i1 := v)) i2 = f i2" "i1 \ i2 \ (f (i1 := v1, i2 := v2)) i1 = v1" "i1 \ i2 \ (f (i1 := v1, i2 := v2)) i2 = v2" "i1 = i2 \ (f (i1 := v1, i2 := v2)) i1 = v2" "i1 = i2 \ (f (i1 := v1, i2 := v2)) i1 = v2" "i1 \ i2 \i1 \ i3 \ i2 \ i3 \ (f (i1 := v1, i2 := v2)) i3 = f i3" using fun_upd_same fun_upd_apply by smt+ section \Sets\ lemma Empty: "x \ {}" by simp lemmas smt_sets = Empty UNIV_I Un_iff Int_iff lemma "x \ {}" "x \ UNIV" "x \ A \ B \ x \ A \ x \ B" "x \ P \ {} \ x \ P" "x \ P \ UNIV" "x \ P \ Q \ x \ Q \ P" "x \ P \ P \ x \ P" "x \ P \ (Q \ R) \ x \ (P \ Q) \ R" "x \ A \ B \ x \ A \ x \ B" "x \ P \ {}" "x \ P \ UNIV \ x \ P" "x \ P \ Q \ x \ Q \ P" "x \ P \ P \ x \ P" "x \ P \ (Q \ R) \ x \ (P \ Q) \ R" "{x. x \ P} = {y. y \ P}" by (smt smt_sets)+ + +context + fixes in_multiset :: "'d \ 'd_multiset \ bool" and + add_mset :: "'d \ 'd_multiset \ 'd_multiset" and + set_mset :: "'d_multiset \ 'd set" +begin +lemma + assumes "\a b A. ((a::'d) \ insert b A) = (a = b \ a \ A)" + "\a A. set_mset (add_mset (a::'d) A) = insert a (set_mset A)" + "\r. transp (r::'d \ 'd \ bool) = (\x y z. r x y \ r y z \ r x z)" + shows + "transp (\x y. (x::'d) \ set_mset (add_mset m M) \ y \ set_mset (add_mset m M) \ R x y) \ + transp (\x y. x \ set_mset M \ y \ set_mset M \ R x y)" + by (smt (verit) assms) end + +end diff --git a/src/HOL/Tools/SMT/lethe_proof.ML b/src/HOL/Tools/SMT/lethe_proof.ML --- a/src/HOL/Tools/SMT/lethe_proof.ML +++ b/src/HOL/Tools/SMT/lethe_proof.ML @@ -1,785 +1,787 @@ (* Title: HOL/Tools/SMT/Lethe_Proof.ML Author: Mathias Fleury, ENS Rennes Author: Sascha Boehme, TU Muenchen Lethe proofs: parsing and abstract syntax tree. *) signature LETHE_PROOF = sig (*proofs*) datatype lethe_step = Lethe_Step of { id: string, rule: string, prems: string list, proof_ctxt: term list, concl: term, fixes: string list} datatype lethe_replay_node = Lethe_Replay_Node of { id: string, rule: string, args: term list, prems: string list, proof_ctxt: term list, concl: term, bounds: (string * typ) list, declarations: (string * term) list, insts: term Symtab.table, subproof: (string * typ) list * term list * term list * lethe_replay_node list} val mk_replay_node: string -> string -> term list -> string list -> term list -> term -> (string * typ) list -> term Symtab.table -> (string * term) list -> (string * typ) list * term list * term list * lethe_replay_node list -> lethe_replay_node (*proof parser*) val parse: typ Symtab.table -> term Symtab.table -> string list -> Proof.context -> lethe_step list * Proof.context val parse_replay: typ Symtab.table -> term Symtab.table -> string list -> Proof.context -> lethe_replay_node list * Proof.context val step_prefix : string val input_rule: string val keep_app_symbols: string -> bool val keep_raw_lifting: string -> bool val normalized_input_rule: string val la_generic_rule : string val rewrite_rule : string val simp_arith_rule : string val lethe_deep_skolemize_rule : string val lethe_def : string val subproof_rule : string val local_input_rule : string val not_not_rule : string val contract_rule : string val ite_intro_rule : string val eq_congruent_rule : string val eq_congruent_pred_rule : string val skolemization_steps : string list val theory_resolution2_rule: string val equiv_pos2_rule: string + val and_pos_rule: string val th_resolution_rule: string val is_skolemization: string -> bool val is_skolemization_step: lethe_replay_node -> bool val number_of_steps: lethe_replay_node list -> int end; structure Lethe_Proof: LETHE_PROOF = struct open SMTLIB_Proof datatype raw_lethe_node = Raw_Lethe_Node of { id: string, rule: string, args: SMTLIB.tree, prems: string list, concl: SMTLIB.tree, declarations: (string * SMTLIB.tree) list, subproof: raw_lethe_node list} fun mk_raw_node id rule args prems declarations concl subproof = Raw_Lethe_Node {id = id, rule = rule, args = args, prems = prems, declarations = declarations, concl = concl, subproof = subproof} datatype lethe_node = Lethe_Node of { id: string, rule: string, prems: string list, proof_ctxt: term list, concl: term} fun mk_node id rule prems proof_ctxt concl = Lethe_Node {id = id, rule = rule, prems = prems, proof_ctxt = proof_ctxt, concl = concl} datatype lethe_replay_node = Lethe_Replay_Node of { id: string, rule: string, args: term list, prems: string list, proof_ctxt: term list, concl: term, bounds: (string * typ) list, insts: term Symtab.table, declarations: (string * term) list, subproof: (string * typ) list * term list * term list * lethe_replay_node list} fun mk_replay_node id rule args prems proof_ctxt concl bounds insts declarations subproof = Lethe_Replay_Node {id = id, rule = rule, args = args, prems = prems, proof_ctxt = proof_ctxt, concl = concl, bounds = bounds, insts = insts, declarations = declarations, subproof = subproof} datatype lethe_step = Lethe_Step of { id: string, rule: string, prems: string list, proof_ctxt: term list, concl: term, fixes: string list} fun mk_step id rule prems proof_ctxt concl fixes = Lethe_Step {id = id, rule = rule, prems = prems, proof_ctxt = proof_ctxt, concl = concl, fixes = fixes} val step_prefix = ".c" val input_rule = "input" val la_generic_rule = "la_generic" val normalized_input_rule = "__normalized_input" (*arbitrary*) val rewrite_rule = "__rewrite" (*arbitrary*) val subproof_rule = "subproof" val local_input_rule = "__local_input" (*arbitrary*) val simp_arith_rule = "simp_arith" val lethe_def = "__skolem_definition" (*arbitrary*) val not_not_rule = "not_not" val contract_rule = "contraction" val eq_congruent_pred_rule = "eq_congruent_pred" val eq_congruent_rule = "eq_congruent" val ite_intro_rule = "ite_intro" val default_skolem_rule = "sko_forall" (*arbitrary, but must be one of the skolems*) val theory_resolution2_rule = "__theory_resolution2" (*arbitrary*) val equiv_pos2_rule = "equiv_pos2" val th_resolution_rule = "th_resolution" +val and_pos_rule = "and_pos" val skolemization_steps = ["sko_forall", "sko_ex"] val is_skolemization = member (op =) skolemization_steps -val keep_app_symbols = member (op =) [eq_congruent_pred_rule, eq_congruent_rule, ite_intro_rule] -val keep_raw_lifting = member (op =) [eq_congruent_pred_rule, eq_congruent_rule, ite_intro_rule] +val keep_app_symbols = member (op =) [eq_congruent_pred_rule, eq_congruent_rule, ite_intro_rule, and_pos_rule] +val keep_raw_lifting = member (op =) [eq_congruent_pred_rule, eq_congruent_rule, ite_intro_rule, and_pos_rule] val is_SH_trivial = member (op =) [not_not_rule, contract_rule] fun is_skolemization_step (Lethe_Replay_Node {id, ...}) = is_skolemization id (* Even the lethe developers do not know if the following rule can still appear in proofs: *) val lethe_deep_skolemize_rule = "deep_skolemize" fun number_of_steps [] = 0 | number_of_steps ((Lethe_Replay_Node {subproof = (_, _, _, subproof), ...}) :: pf) = 1 + number_of_steps subproof + number_of_steps pf (* proof parser *) fun node_of p cx = ([], cx) ||>> `(with_fresh_names (term_of p)) |>> snd fun synctactic_var_subst old_name new_name (u $ v) = (synctactic_var_subst old_name new_name u $ synctactic_var_subst old_name new_name v) | synctactic_var_subst old_name new_name (Abs (v, T, u)) = Abs (if String.isPrefix old_name v then new_name else v, T, synctactic_var_subst old_name new_name u) | synctactic_var_subst old_name new_name (Free (v, T)) = if String.isPrefix old_name v then Free (new_name, T) else Free (v, T) | synctactic_var_subst _ _ t = t fun synctatic_rew_in_lhs_subst old_name new_name (Const(\<^const_name>\HOL.eq\, T) $ t1 $ t2) = Const(\<^const_name>\HOL.eq\, T) $ synctactic_var_subst old_name new_name t1 $ t2 | synctatic_rew_in_lhs_subst old_name new_name (Const(\<^const_name>\Trueprop\, T) $ t1) = Const(\<^const_name>\Trueprop\, T) $ (synctatic_rew_in_lhs_subst old_name new_name t1) | synctatic_rew_in_lhs_subst _ _ t = t fun add_bound_variables_to_ctxt cx = fold (update_binding o (fn (s, SOME typ) => (s, Term (Free (s, type_of cx typ))))) local fun extract_symbols bds = bds |> map (fn (SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym x, SMTLIB.Sym y], typ) => [([x, y], typ)] | t => raise (Fail ("match error " ^ @{make_string} t))) |> flat (* onepoint can bind a variable to another variable or to a constant *) fun extract_qnt_symbols cx bds = bds |> map (fn (SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym x, SMTLIB.Sym y], typ) => (case node_of (SMTLIB.Sym y) cx of ((_, []), _) => [([x], typ)] | _ => [([x, y], typ)]) | (SMTLIB.S (SMTLIB.Sym "=" :: SMTLIB.Sym x :: _), typ) => [([x], typ)] | t => raise (Fail ("match error " ^ @{make_string} t))) |> flat fun extract_symbols_map bds = bds |> map (fn (SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym x, _], typ) => [([x], typ)]) |> flat in fun declared_csts _ "__skolem_definition" [(SMTLIB.S [SMTLIB.Sym x, typ, _], _)] = [(x, typ)] | declared_csts _ "__skolem_definition" t = raise (Fail ("unrecognized skolem_definition " ^ @{make_string} t)) | declared_csts _ _ _ = [] fun skolems_introduced_by_rule (SMTLIB.S bds) = fold (fn (SMTLIB.S [SMTLIB.Sym "=", _, SMTLIB.Sym y]) => curry (op ::) y) bds [] (*FIXME there is probably a way to use the information given by onepoint*) fun bound_vars_by_rule _ "bind" (bds) = extract_symbols bds | bound_vars_by_rule cx "onepoint" bds = extract_qnt_symbols cx bds | bound_vars_by_rule _ "sko_forall" bds = extract_symbols_map bds | bound_vars_by_rule _ "sko_ex" bds = extract_symbols_map bds | bound_vars_by_rule _ "__skolem_definition" [(SMTLIB.S [SMTLIB.Sym x, typ, _], _)] = [([x], SOME typ)] | bound_vars_by_rule _ "__skolem_definition" [(SMTLIB.S [_, SMTLIB.Sym x, _], _)] = [([x], NONE)] | bound_vars_by_rule _ _ _ = [] (* Lethe adds "?" before some variables. *) fun remove_all_qm (SMTLIB.Sym v :: l) = SMTLIB.Sym (perhaps (try (unprefix "?")) v) :: remove_all_qm l | remove_all_qm (SMTLIB.S l :: l') = SMTLIB.S (remove_all_qm l) :: remove_all_qm l' | remove_all_qm (SMTLIB.Key v :: l) = SMTLIB.Key v :: remove_all_qm l | remove_all_qm (v :: l) = v :: remove_all_qm l | remove_all_qm [] = [] fun remove_all_qm2 (SMTLIB.Sym v) = SMTLIB.Sym (perhaps (try (unprefix "?")) v) | remove_all_qm2 (SMTLIB.S l) = SMTLIB.S (remove_all_qm l) | remove_all_qm2 (SMTLIB.Key v) = SMTLIB.Key v | remove_all_qm2 v = v end datatype step_kind = ASSUME | ANCHOR | NO_STEP | NORMAL_STEP | SKOLEM fun parse_raw_proof_steps (limit : string option) (ls : SMTLIB.tree list) (cx : name_bindings) : (raw_lethe_node list * SMTLIB.tree list * name_bindings) = let fun rotate_pair (a, (b, c)) = ((a, b), c) fun step_kind [] = (NO_STEP, SMTLIB.S [], []) | step_kind ((p as SMTLIB.S (SMTLIB.Sym "anchor" :: _)) :: l) = (ANCHOR, p, l) | step_kind ((p as SMTLIB.S (SMTLIB.Sym "assume" :: _)) :: l) = (ASSUME, p, l) | step_kind ((p as SMTLIB.S (SMTLIB.Sym "step" :: _)) :: l) = (NORMAL_STEP, p, l) | step_kind ((p as SMTLIB.S (SMTLIB.Sym "define-fun" :: _)) :: l) = (SKOLEM, p, l) | step_kind p = raise (Fail ("step_kind unrec: " ^ @{make_string} p)) fun parse_skolem (SMTLIB.S [SMTLIB.Sym "define-fun", SMTLIB.Sym id, _, typ, SMTLIB.S (SMTLIB.Sym "!" :: t :: [SMTLIB.Key _, SMTLIB.Sym name])]) cx = (*replace the name binding by the constant instead of the full term in order to reduce the size of the generated terms and therefore the reconstruction time*) let val (l, cx) = (fst oo SMTLIB_Proof.extract_and_update_name_bindings) t cx |> apsnd (SMTLIB_Proof.update_name_binding (name, SMTLIB.Sym id)) in (mk_raw_node (id ^ lethe_def) lethe_def (SMTLIB.S [SMTLIB.Sym id, typ, l]) [] [] (SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym id, l]) [], cx) end | parse_skolem (SMTLIB.S [SMTLIB.Sym "define-fun", SMTLIB.Sym id, _, typ, SMTLIB.S l]) cx = let val (l, cx) = (fst oo SMTLIB_Proof.extract_and_update_name_bindings) (SMTLIB.S l ) cx in (mk_raw_node (id ^ lethe_def) lethe_def (SMTLIB.S [SMTLIB.Sym id, typ, l]) [] [] (SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym id, l]) [], cx) end | parse_skolem t _ = raise Fail ("unrecognized Lethe proof " ^ \<^make_string> t) fun get_id_cx (SMTLIB.S ((SMTLIB.Sym _) :: (SMTLIB.Sym id) :: l), cx) = (id, (l, cx)) | get_id_cx t = raise Fail ("unrecognized Lethe proof " ^ \<^make_string> t) fun get_id (SMTLIB.S ((SMTLIB.Sym _) :: (SMTLIB.Sym id) :: l)) = (id, l) | get_id t = raise Fail ("unrecognized Lethe proof " ^ \<^make_string> t) fun parse_source (SMTLIB.Key "premises" :: SMTLIB.S source ::l, cx) = (SOME (map (fn (SMTLIB.Sym id) => id) source), (l, cx)) | parse_source (l, cx) = (NONE, (l, cx)) fun parse_rule (SMTLIB.Key "rule" :: SMTLIB.Sym r :: l, cx) = (r, (l, cx)) | parse_rule t = raise Fail ("unrecognized Lethe proof " ^ \<^make_string> t) fun parse_anchor_step (SMTLIB.S (SMTLIB.Sym "anchor" :: SMTLIB.Key "step" :: SMTLIB.Sym r :: l), cx) = (r, (l, cx)) | parse_anchor_step t = raise Fail ("unrecognized Lethe proof " ^ \<^make_string> t) fun parse_args (SMTLIB.Key "args" :: args :: l, cx) = let val ((args, cx), _) = SMTLIB_Proof.extract_and_update_name_bindings args cx in (args, (l, cx)) end | parse_args (l, cx) = (SMTLIB.S [], (l, cx)) fun parse_and_clausify_conclusion (SMTLIB.S (SMTLIB.Sym "cl" :: []) :: l, cx) = (SMTLIB.Sym "false", (l, cx)) | parse_and_clausify_conclusion (SMTLIB.S (SMTLIB.Sym "cl" :: concl) :: l, cx) = let val (concl, cx) = fold_map (fst oo SMTLIB_Proof.extract_and_update_name_bindings) concl cx in (SMTLIB.S (SMTLIB.Sym "or" :: concl), (l, cx)) end | parse_and_clausify_conclusion t = raise Fail ("unrecognized Lethe proof " ^ \<^make_string> t) val parse_normal_step = get_id_cx ##> parse_and_clausify_conclusion #> rotate_pair ##> parse_rule #> rotate_pair ##> parse_source #> rotate_pair ##> parse_args #> rotate_pair fun to_raw_node subproof ((((id, concl), rule), prems), args) = mk_raw_node id rule args (the_default [] prems) [] concl subproof fun at_discharge NONE _ = false | at_discharge (SOME id) p = p |> get_id |> fst |> (fn id2 => id = id2) in case step_kind ls of (NO_STEP, _, _) => ([],[], cx) | (NORMAL_STEP, p, l) => if at_discharge limit p then ([], ls, cx) else let (*ignores content of "discharge": Isabelle is keeping track of it via the context*) val (s, (_, cx)) = (p, cx) |> parse_normal_step |>> (to_raw_node []) val (rp, rl, cx) = parse_raw_proof_steps limit l cx in (s :: rp, rl, cx) end | (ASSUME, p, l) => let val (id, t :: []) = p |> get_id val ((t, cx), _) = SMTLIB_Proof.extract_and_update_name_bindings t cx val s = mk_raw_node id input_rule (SMTLIB.S []) [] [] t [] val (rp, rl, cx) = parse_raw_proof_steps limit l cx in (s :: rp, rl, cx) end | (ANCHOR, p, l) => let val (anchor_id, (anchor_args, (_, cx))) = (p, cx) |> (parse_anchor_step ##> parse_args) val (subproof, discharge_step :: remaining_proof, cx) = parse_raw_proof_steps (SOME anchor_id) l cx val (curss, (_, cx)) = parse_normal_step (discharge_step, cx) val s = to_raw_node subproof (fst curss, anchor_args) val (rp, rl, cx) = parse_raw_proof_steps limit remaining_proof cx in (s :: rp, rl, cx) end | (SKOLEM, p, l) => let val (s, cx) = parse_skolem p cx val (rp, rl, cx) = parse_raw_proof_steps limit l cx in (s :: rp, rl, cx) end end fun proof_ctxt_of_rule "bind" t = t | proof_ctxt_of_rule "sko_forall" t = t | proof_ctxt_of_rule "sko_ex" t = t | proof_ctxt_of_rule "let" t = t | proof_ctxt_of_rule "onepoint" t = t | proof_ctxt_of_rule _ _ = [] fun args_of_rule "bind" t = t | args_of_rule "la_generic" t = t | args_of_rule _ _ = [] fun insts_of_forall_inst "forall_inst" t = map (fn SMTLIB.S [_, SMTLIB.Sym x, a] => (x, a)) t | insts_of_forall_inst _ _ = [] fun id_of_last_step prems = if null prems then [] else let val Lethe_Replay_Node {id, ...} = List.last prems in [id] end fun extract_assumptions_from_subproof subproof = let fun extract_assumptions_from_subproof (Lethe_Replay_Node {rule, concl, ...}) assms = if rule = local_input_rule then concl :: assms else assms in fold extract_assumptions_from_subproof subproof [] end fun normalized_rule_name id rule = (case (rule = input_rule, can SMTLIB_Interface.role_and_index_of_assert_name id) of (true, true) => normalized_input_rule | (true, _) => local_input_rule | _ => rule) fun is_assm_repetition id rule = rule = input_rule andalso can SMTLIB_Interface.role_and_index_of_assert_name id fun extract_skolem ([SMTLIB.Sym var, typ, choice]) = (var, typ, choice) | extract_skolem t = raise Fail ("fail to parse type" ^ @{make_string} t) (* The preprocessing takes care of: 1. unfolding the shared terms 2. extract the declarations of skolems to make sure that there are not unfolded *) fun preprocess compress step = let fun expand_assms cs = map (fn t => case AList.lookup (op =) cs t of NONE => t | SOME a => a) fun expand_lonely_arguments (args as SMTLIB.S [SMTLIB.Sym "=", _, _]) = [args] | expand_lonely_arguments (x as SMTLIB.S [SMTLIB.Sym var, _]) = [SMTLIB.S [SMTLIB.Sym "=", x, SMTLIB.Sym var]] fun preprocess (Raw_Lethe_Node {id, rule, args, prems, concl, subproof, ...}) (cx, remap_assms) = let val (skolem_names, stripped_args) = args |> (fn SMTLIB.S args => args) |> map (fn SMTLIB.S [SMTLIB.Key "=", x, y] => SMTLIB.S [SMTLIB.Sym "=", x, y] | x => x) |> (rule = "bind" orelse rule = "onepoint") ? flat o (map expand_lonely_arguments) |> `(if rule = lethe_def then single o extract_skolem else K []) ||> SMTLIB.S val (subproof, (cx, _)) = fold_map preprocess subproof (cx, remap_assms) |> apfst flat val remap_assms = (if rule = "or" then (id, hd prems) :: remap_assms else remap_assms) (* declare variables in the context *) val declarations = if rule = lethe_def then skolem_names |> map (fn (name, _, choice) => (name, choice)) else [] in if compress andalso rule = "or" then ([], (cx, remap_assms)) else ([Raw_Lethe_Node {id = id, rule = rule, args = stripped_args, prems = expand_assms remap_assms prems, declarations = declarations, concl = concl, subproof = subproof}], (cx, remap_assms)) end in preprocess step end fun filter_split _ [] = ([], []) | filter_split f (a :: xs) = (if f a then apfst (curry op :: a) else apsnd (curry op :: a)) (filter_split f xs) fun extract_types_of_args (SMTLIB.S [var, typ, t as SMTLIB.S [SMTLIB.Sym "choice", _, _]]) = (SMTLIB.S [var, typ, t], SOME typ) |> single | extract_types_of_args (SMTLIB.S t) = let fun extract_types_of_arg (SMTLIB.S [eq, SMTLIB.S [var, typ], t]) = (SMTLIB.S [eq, var, t], SOME typ) | extract_types_of_arg t = (t, NONE) in t |> map extract_types_of_arg end fun collect_skolem_defs (Raw_Lethe_Node {rule, subproof = subproof, args, ...}) = (if is_skolemization rule then map (fn id => id ^ lethe_def) (skolems_introduced_by_rule args) else []) @ flat (map collect_skolem_defs subproof) (*The postprocessing does: 1. translate the terms to Isabelle syntax, taking care of free variables 2. remove the ambiguity in the proof terms: x \ y |- x = x means y = x. To remove ambiguity, we use the fact that y is a free variable and replace the term by: xy \ y |- xy = x. This is now does not have an ambiguity and we can safely move the "xy \ y" to the proof assumptions. *) fun postprocess_proof compress ctxt step cx = let fun postprocess (Raw_Lethe_Node {id, rule, args, prems, declarations, concl, subproof}) (cx, rew) = let val _ = (SMT_Config.verit_msg ctxt) (fn () => @{print} ("id =", id, "concl =", concl)) val args = extract_types_of_args args val globally_bound_vars = declared_csts cx rule args val cx = fold (update_binding o (fn (s, typ) => (s, Term (Free (s, type_of cx typ))))) globally_bound_vars cx (*find rebound variables specific to the LHS of the equivalence symbol*) val bound_vars = bound_vars_by_rule cx rule args val bound_vars_no_typ = map fst bound_vars val rhs_vars = fold (fn [t', t] => t <> t' ? (curry (op ::) t) | _ => fn x => x) bound_vars_no_typ [] fun not_already_bound cx t = SMTLIB_Proof.lookup_binding cx t = None andalso not (member (op =) rhs_vars t) val (shadowing_vars, rebound_lhs_vars) = bound_vars |> filter_split (fn ([t, _], typ) => not_already_bound cx t | _ => true) |>> map (apfst (hd)) |>> (fn vars => vars @ flat (map (fn ([_, t], typ) => [(t, typ)] | _ => []) bound_vars)) val subproof_rew = fold (fn [t, t'] => curry (op ::) (t, t ^ t')) (map fst rebound_lhs_vars) rew val subproof_rewriter = fold (fn (t, t') => synctatic_rew_in_lhs_subst t t') subproof_rew val ((concl, bounds), cx') = node_of concl cx val extra_lhs_vars = map (fn ([a,b], typ) => (a, a^b, typ)) rebound_lhs_vars val old_lhs_vars = map (fn (a, _, typ) => (a, typ)) extra_lhs_vars val new_lhs_vars = map (fn (_, newvar, typ) => (newvar, typ)) extra_lhs_vars (* postprocess conclusion *) val concl = SMTLIB_Isar.unskolemize_names ctxt (subproof_rewriter concl) val _ = (SMT_Config.verit_msg ctxt) (fn () => \<^print> ("id =", id, "concl =", concl)) val _ = (SMT_Config.verit_msg ctxt) (fn () => \<^print> ("id =", id, "cx' =", cx', "bound_vars =", bound_vars)) val bound_tvars = map (fn (s, SOME typ) => (s, type_of cx typ)) (shadowing_vars @ new_lhs_vars) val subproof_cx = add_bound_variables_to_ctxt cx (shadowing_vars @ new_lhs_vars) cx fun could_unify (Bound i, Bound j) = i = j | could_unify (Var v, Var v') = v = v' | could_unify (Free v, Free v') = v = v' | could_unify (Const (v, ty), Const (v', ty')) = v = v' andalso ty = ty' | could_unify (Abs (_, ty, bdy), Abs (_, ty', bdy')) = ty = ty' andalso could_unify (bdy, bdy') | could_unify (u $ v, u' $ v') = could_unify (u, u') andalso could_unify (v, v') | could_unify _ = false fun is_alpha_renaming t = t |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> could_unify handle TERM _ => false val alpha_conversion = rule = "bind" andalso is_alpha_renaming concl val can_remove_subproof = compress andalso (is_skolemization rule orelse alpha_conversion) val (fixed_subproof : lethe_replay_node list, _) = fold_map postprocess (if can_remove_subproof then [] else subproof) (subproof_cx, subproof_rew) val unsk_and_rewrite = SMTLIB_Isar.unskolemize_names ctxt o subproof_rewriter (* postprocess assms *) val stripped_args = map fst args val sanitized_args = proof_ctxt_of_rule rule stripped_args val arg_cx = add_bound_variables_to_ctxt cx (shadowing_vars @ old_lhs_vars) subproof_cx val (termified_args, _) = fold_map node_of sanitized_args arg_cx |> apfst (map fst) val normalized_args = map unsk_and_rewrite termified_args val subproof_assms = proof_ctxt_of_rule rule normalized_args (* postprocess arguments *) val rule_args = args_of_rule rule stripped_args val (termified_args, _) = fold_map term_of rule_args subproof_cx val normalized_args = map unsk_and_rewrite termified_args val rule_args = map subproof_rewriter normalized_args val raw_insts = insts_of_forall_inst rule stripped_args fun termify_term (x, t) cx = let val (t, cx) = term_of t cx in ((x, t), cx) end val (termified_args, _) = fold_map termify_term raw_insts subproof_cx val insts = Symtab.empty |> fold (fn (x, t) => fn insts => Symtab.update_new (x, t) insts) termified_args |> Symtab.map (K unsk_and_rewrite) (* declarations *) val (declarations, _) = fold_map termify_term declarations cx |> apfst (map (apsnd unsk_and_rewrite)) (* fix step *) val _ = if bounds <> [] then raise (Fail "found dangling variable in concl") else () val skolem_defs = (if is_skolemization rule then map (fn id => id ^ lethe_def) (skolems_introduced_by_rule (SMTLIB.S (map fst args))) else []) val skolems_of_subproof = (if is_skolemization rule then flat (map collect_skolem_defs subproof) else []) val fixed_prems = prems @ (if is_assm_repetition id rule then [id] else []) @ skolem_defs @ skolems_of_subproof @ (id_of_last_step fixed_subproof) (* fix subproof *) val normalized_rule = normalized_rule_name id rule |> (if compress andalso alpha_conversion then K "refl" else I) val extra_assms2 = (if rule = subproof_rule then extract_assumptions_from_subproof fixed_subproof else []) val step = mk_replay_node id normalized_rule rule_args fixed_prems subproof_assms concl [] insts declarations (bound_tvars, subproof_assms, extra_assms2, fixed_subproof) in (step, (cx', rew)) end in postprocess step (cx, []) |> (fn (step, (cx, _)) => (step, cx)) end fun combine_proof_steps ((step1 : lethe_replay_node) :: step2 :: steps) = let val (Lethe_Replay_Node {id = id1, rule = rule1, args = args1, prems = prems1, proof_ctxt = proof_ctxt1, concl = concl1, bounds = bounds1, insts = insts1, declarations = declarations1, subproof = (bound_sub1, assms_sub1, assms_extra1, subproof1)}) = step1 val (Lethe_Replay_Node {id = id2, rule = rule2, args = args2, prems = prems2, proof_ctxt = proof_ctxt2, concl = concl2, bounds = bounds2, insts = insts2, declarations = declarations2, subproof = (bound_sub2, assms_sub2, assms_extra2, subproof2)}) = step2 val goals1 = (case concl1 of _ $ (Const (\<^const_name>\HOL.disj\, _) $ _ $ (Const (\<^const_name>\HOL.disj\, _) $ (Const (\<^const_name>\HOL.Not\, _) $a) $ b)) => [a,b] | _ => []) val goal2 = (case concl2 of _ $ a => a) in if rule1 = equiv_pos2_rule andalso rule2 = th_resolution_rule andalso member (op =) prems2 id1 andalso member (op =) goals1 goal2 then mk_replay_node id2 theory_resolution2_rule args2 (filter_out (curry (op =) id1) prems2) proof_ctxt2 concl2 bounds2 insts2 declarations2 (bound_sub2, assms_sub2, assms_extra2, combine_proof_steps subproof2) :: combine_proof_steps steps else mk_replay_node id1 rule1 args1 prems1 proof_ctxt1 concl1 bounds1 insts1 declarations1 (bound_sub1, assms_sub1, assms_extra1, combine_proof_steps subproof1) :: combine_proof_steps (step2 :: steps) end | combine_proof_steps steps = steps val linearize_proof = let fun map_node_concl f (Lethe_Node {id, rule, prems, proof_ctxt, concl}) = mk_node id rule prems proof_ctxt (f concl) fun linearize (Lethe_Replay_Node {id = id, rule = rule, args = _, prems = prems, proof_ctxt = proof_ctxt, concl = concl, bounds = bounds, insts = _, declarations = _, subproof = (bounds', assms, inputs, subproof)}) = let val bounds = distinct (op =) bounds val bounds' = distinct (op =) bounds' fun mk_prop_of_term concl = concl |> fastype_of concl = \<^typ>\bool\ ? curry (op $) \<^term>\Trueprop\ fun remove_assumption_id assumption_id prems = filter_out (curry (op =) assumption_id) prems fun add_assumption assumption concl = \<^Const>\Pure.imp for \mk_prop_of_term assumption\ \mk_prop_of_term concl\\ fun inline_assumption assumption assumption_id (Lethe_Node {id, rule, prems, proof_ctxt, concl}) = mk_node id rule (remove_assumption_id assumption_id prems) proof_ctxt (add_assumption assumption concl) fun find_input_steps_and_inline [] = [] | find_input_steps_and_inline (Lethe_Node {id = id', rule, prems, concl, ...} :: steps) = if rule = input_rule then find_input_steps_and_inline (map (inline_assumption concl id') steps) else mk_node (id') rule prems [] concl :: find_input_steps_and_inline steps fun free_bounds bounds (concl) = fold (fn (var, typ) => fn t => Logic.all (Free (var, typ)) t) bounds concl val subproof = subproof |> flat o map linearize |> map (map_node_concl (fold add_assumption (assms @ inputs))) |> map (map_node_concl (free_bounds (bounds @ bounds'))) |> find_input_steps_and_inline val concl = free_bounds bounds concl in subproof @ [mk_node id rule prems proof_ctxt concl] end in linearize end fun rule_of (Lethe_Replay_Node {rule,...}) = rule fun subproof_of (Lethe_Replay_Node {subproof = (_, _, _, subproof),...}) = subproof (* Massage Skolems for Sledgehammer. We have to make sure that there is an "arrow" in the graph for skolemization steps. A. The normal easy case This function detects the steps of the form P \ Q :skolemization Q :resolution with P and replace them by Q :skolemization Throwing away the step "P \ Q" completely. This throws away a lot of information, but it does not matter too much for Sledgehammer. B. Skolems in subproofs Supporting this is more or less hopeless as long as the Isar reconstruction of Sledgehammer does not support more features like definitions. lethe is able to generate proofs with skolemization happening in subproofs inside the formula. (assume "A \ P" ... P \ Q :skolemization in the subproof ...) hence A \ P \ A \ Q :lemma ... R :something with some rule and replace them by R :skolemization with some rule Without any subproof *) fun remove_skolem_definitions_proof steps = let fun replace_equivalent_by_imp (judgement $ ((Const(\<^const_name>\HOL.eq\, typ) $ arg1) $ arg2)) = judgement $ ((Const(\<^const_name>\HOL.implies\, typ) $ arg1) $ arg2) | replace_equivalent_by_imp a = a (*This case is probably wrong*) fun remove_skolem_definitions (Lethe_Replay_Node {id = id, rule = rule, args = args, prems = prems, proof_ctxt = proof_ctxt, concl = concl, bounds = bounds, insts = insts, declarations = declarations, subproof = (vars, assms', extra_assms', subproof)}) (prems_to_remove, skolems) = let val prems = prems |> filter_out (member (op =) prems_to_remove) val trivial_step = is_SH_trivial rule fun has_skolem_substep st NONE = if is_skolemization (rule_of st) then SOME (rule_of st) else fold has_skolem_substep (subproof_of st) NONE | has_skolem_substep _ a = a val promote_to_skolem = exists (fn t => member (op =) skolems t) prems val promote_from_assms = fold has_skolem_substep subproof NONE <> NONE val promote_step = promote_to_skolem orelse promote_from_assms val skolem_step_to_skip = is_skolemization rule orelse (promote_from_assms andalso length prems > 1) val is_skolem = is_skolemization rule orelse promote_step val prems = prems |> filter_out (fn t => member (op =) skolems t) |> is_skolem ? filter_out (String.isPrefix id) val rule = (if promote_step then default_skolem_rule else rule) val subproof = subproof |> (is_skolem ? K []) (*subproofs of skolemization steps are useless for SH*) |> map (fst o (fn st => remove_skolem_definitions st (prems_to_remove, skolems))) (*no new definitions in subproofs*) |> flat val concl = concl |> is_skolem ? replace_equivalent_by_imp val step = (if skolem_step_to_skip orelse rule = lethe_def orelse trivial_step then [] else mk_replay_node id rule args prems proof_ctxt concl bounds insts declarations (vars, assms', extra_assms', subproof) |> single) val defs = (if rule = lethe_def orelse trivial_step then id :: prems_to_remove else prems_to_remove) val skolems = (if skolem_step_to_skip then id :: skolems else skolems) in (step, (defs, skolems)) end in fold_map remove_skolem_definitions steps ([], []) |> fst |> flat end local (*TODO useful?*) fun remove_pattern (SMTLIB.S (SMTLIB.Sym "!" :: t :: [SMTLIB.Key _, SMTLIB.S _])) = t | remove_pattern (SMTLIB.S xs) = SMTLIB.S (map remove_pattern xs) | remove_pattern p = p fun import_proof_and_post_process typs funs lines ctxt = let val compress = SMT_Config.compress_verit_proofs ctxt val smtlib_lines_without_qm = lines |> map single |> map SMTLIB.parse |> map remove_all_qm2 |> map remove_pattern val (raw_steps, _, _) = parse_raw_proof_steps NONE smtlib_lines_without_qm SMTLIB_Proof.empty_name_binding fun process step (cx, cx') = let fun postprocess step (cx, cx') = let val (step, cx) = postprocess_proof compress ctxt step cx in (step, (cx, cx')) end in uncurry (fold_map postprocess) (preprocess compress step (cx, cx')) end val step = (empty_context ctxt typs funs, []) |> fold_map process raw_steps |> (fn (steps, (cx, _)) => (flat steps, cx)) |> compress? apfst combine_proof_steps in step end in fun parse typs funs lines ctxt = let val (u, env) = import_proof_and_post_process typs funs lines ctxt val t = u |> remove_skolem_definitions_proof |> flat o (map linearize_proof) fun node_to_step (Lethe_Node {id, rule, prems, concl, ...}) = mk_step id rule prems [] concl [] in (map node_to_step t, ctxt_of env) end fun parse_replay typs funs lines ctxt = let val (u, env) = import_proof_and_post_process typs funs lines ctxt val _ = (SMT_Config.verit_msg ctxt) (fn () => \<^print> u) in (u, ctxt_of env) end end end; diff --git a/src/HOL/Tools/SMT/verit_proof.ML b/src/HOL/Tools/SMT/verit_proof.ML --- a/src/HOL/Tools/SMT/verit_proof.ML +++ b/src/HOL/Tools/SMT/verit_proof.ML @@ -1,893 +1,895 @@ (* Title: HOL/Tools/SMT/Verit_Proof.ML Author: Mathias Fleury, ENS Rennes Author: Sascha Boehme, TU Muenchen VeriT proofs: parsing and abstract syntax tree. *) signature VERIT_PROOF = sig (*proofs*) datatype veriT_step = VeriT_Step of { id: string, rule: string, prems: string list, proof_ctxt: term list, concl: term, fixes: string list} datatype veriT_replay_node = VeriT_Replay_Node of { id: string, rule: string, args: term list, prems: string list, proof_ctxt: term list, concl: term, bounds: (string * typ) list, declarations: (string * term) list, insts: term Symtab.table, subproof: (string * typ) list * term list * term list * veriT_replay_node list} (*proof parser*) val parse: typ Symtab.table -> term Symtab.table -> string list -> Proof.context -> veriT_step list * Proof.context val parse_replay: typ Symtab.table -> term Symtab.table -> string list -> Proof.context -> veriT_replay_node list * Proof.context val step_prefix : string val input_rule: string val keep_app_symbols: string -> bool val keep_raw_lifting: string -> bool val normalized_input_rule: string val la_generic_rule : string val rewrite_rule : string val simp_arith_rule : string val veriT_deep_skolemize_rule : string val veriT_def : string val subproof_rule : string val local_input_rule : string val not_not_rule : string val contract_rule : string val ite_intro_rule : string val eq_congruent_rule : string val eq_congruent_pred_rule : string val skolemization_steps : string list val theory_resolution2_rule: string val equiv_pos2_rule: string val th_resolution_rule: string + val and_pos_rule: string val is_skolemization: string -> bool val is_skolemization_step: veriT_replay_node -> bool val number_of_steps: veriT_replay_node list -> int (*Strategy related*) val veriT_strategy : string Config.T val veriT_current_strategy : Context.generic -> string list val all_veriT_stgies: Context.generic -> string list; val select_veriT_stgy: string -> Context.generic -> Context.generic; val valid_veriT_stgy: string -> Context.generic -> bool; val verit_add_stgy: string * string list -> Context.generic -> Context.generic val verit_rm_stgy: string -> Context.generic -> Context.generic (*Global tactic*) val verit_tac: Proof.context -> thm list -> int -> tactic val verit_tac_stgy: string -> Proof.context -> thm list -> int -> tactic end; structure Verit_Proof: VERIT_PROOF = struct open SMTLIB_Proof val veriT_strategy_default_name = "default"; (*FUDGE*) val veriT_strategy_del_insts_name = "del_insts"; (*FUDGE*) val veriT_strategy_rm_insts_name = "ccfv_SIG"; (*FUDGE*) val veriT_strategy_ccfv_insts_name = "ccfv_threshold"; (*FUDGE*) val veriT_strategy_best_name = "best"; (*FUDGE*) val veriT_strategy_best = ["--index-sorts", "--index-fresh-sorts", "--triggers-new", "--triggers-sel-rm-specific"]; val veriT_strategy_del_insts = ["--index-sorts", "--index-fresh-sorts", "--ccfv-breadth", "--inst-deletion", "--index-SAT-triggers", "--inst-deletion-loops", "--inst-deletion-track-vars", "--inst-deletion", "--index-SAT-triggers"]; val veriT_strategy_rm_insts = ["--index-SIG", "--triggers-new", "--triggers-sel-rm-specific"]; val veriT_strategy_ccfv_insts = ["--index-sorts", "--index-fresh-sorts", "--triggers-new", "--triggers-sel-rm-specific", "--triggers-restrict-combine", "--inst-deletion", "--index-SAT-triggers", "--inst-deletion-loops", "--inst-deletion-track-vars", "--inst-deletion", "--index-SAT-triggers", "--inst-sorts-threshold=100000", "--ematch-exp=10000000", "--ccfv-index=100000", "--ccfv-index-full=1000"] val veriT_strategy_default = []; type verit_strategy = {default_strategy: string, strategies: (string * string list) list} fun mk_verit_strategy default_strategy strategies : verit_strategy = {default_strategy=default_strategy,strategies=strategies} val empty_data = mk_verit_strategy veriT_strategy_best_name [(veriT_strategy_default_name, veriT_strategy_default), (veriT_strategy_del_insts_name, veriT_strategy_del_insts), (veriT_strategy_rm_insts_name, veriT_strategy_rm_insts), (veriT_strategy_ccfv_insts_name, veriT_strategy_ccfv_insts), (veriT_strategy_best_name, veriT_strategy_best)] fun merge_data ({strategies=strategies1,...}:verit_strategy, {default_strategy,strategies=strategies2}:verit_strategy) : verit_strategy = mk_verit_strategy default_strategy (AList.merge (op =) (op =) (strategies1, strategies2)) structure Data = Generic_Data ( type T = verit_strategy val empty = empty_data val merge = merge_data ) fun veriT_current_strategy ctxt = let val {default_strategy,strategies} = (Data.get ctxt) in AList.lookup (op=) strategies default_strategy |> the end val veriT_strategy = Attrib.setup_config_string \<^binding>\smt_verit_strategy\ (K veriT_strategy_best_name); fun valid_veriT_stgy stgy context = let val {strategies,...} = Data.get context in AList.defined (op =) strategies stgy end fun select_veriT_stgy stgy context = let val {strategies,...} = Data.get context val upd = Data.map (K (mk_verit_strategy stgy strategies)) in if not (AList.defined (op =) strategies stgy) then error ("Trying to select unknown veriT strategy: " ^ quote stgy) else upd context end fun verit_add_stgy stgy context = let val {default_strategy,strategies} = Data.get context in Data.map (K (mk_verit_strategy default_strategy (AList.update (op =) stgy strategies))) context end fun verit_rm_stgy stgy context = let val {default_strategy,strategies} = Data.get context in Data.map (K (mk_verit_strategy default_strategy (AList.delete (op =) stgy strategies))) context end fun all_veriT_stgies context = let val {strategies,...} = Data.get context in map fst strategies end val select_verit = SMT_Config.select_solver "verit" fun verit_tac ctxt = SMT_Solver.smt_tac (Config.put SMT_Config.native_bv false ((Context.proof_map select_verit ctxt))) fun verit_tac_stgy stgy ctxt = verit_tac (Context.proof_of (select_veriT_stgy stgy (Context.Proof ctxt))) datatype raw_veriT_node = Raw_VeriT_Node of { id: string, rule: string, args: SMTLIB.tree, prems: string list, concl: SMTLIB.tree, declarations: (string * SMTLIB.tree) list, subproof: raw_veriT_node list} fun mk_raw_node id rule args prems declarations concl subproof = Raw_VeriT_Node {id = id, rule = rule, args = args, prems = prems, declarations = declarations, concl = concl, subproof = subproof} datatype veriT_node = VeriT_Node of { id: string, rule: string, prems: string list, proof_ctxt: term list, concl: term} fun mk_node id rule prems proof_ctxt concl = VeriT_Node {id = id, rule = rule, prems = prems, proof_ctxt = proof_ctxt, concl = concl} datatype veriT_replay_node = VeriT_Replay_Node of { id: string, rule: string, args: term list, prems: string list, proof_ctxt: term list, concl: term, bounds: (string * typ) list, insts: term Symtab.table, declarations: (string * term) list, subproof: (string * typ) list * term list * term list * veriT_replay_node list} fun mk_replay_node id rule args prems proof_ctxt concl bounds insts declarations subproof = VeriT_Replay_Node {id = id, rule = rule, args = args, prems = prems, proof_ctxt = proof_ctxt, concl = concl, bounds = bounds, insts = insts, declarations = declarations, subproof = subproof} datatype veriT_step = VeriT_Step of { id: string, rule: string, prems: string list, proof_ctxt: term list, concl: term, fixes: string list} fun mk_step id rule prems proof_ctxt concl fixes = VeriT_Step {id = id, rule = rule, prems = prems, proof_ctxt = proof_ctxt, concl = concl, fixes = fixes} val step_prefix = ".c" val input_rule = "input" val la_generic_rule = "la_generic" val normalized_input_rule = "__normalized_input" (*arbitrary*) val rewrite_rule = "__rewrite" (*arbitrary*) val subproof_rule = "subproof" val local_input_rule = "__local_input" (*arbitrary*) val simp_arith_rule = "simp_arith" val veriT_def = "__skolem_definition" (*arbitrary*) val not_not_rule = "not_not" val contract_rule = "contraction" val eq_congruent_pred_rule = "eq_congruent_pred" val eq_congruent_rule = "eq_congruent" val ite_intro_rule = "ite_intro" val default_skolem_rule = "sko_forall" (*arbitrary, but must be one of the skolems*) val theory_resolution2_rule = "__theory_resolution2" (*arbitrary*) val equiv_pos2_rule = "equiv_pos2" val th_resolution_rule = "th_resolution" +val and_pos_rule = "and_pos" val skolemization_steps = ["sko_forall", "sko_ex"] val is_skolemization = member (op =) skolemization_steps -val keep_app_symbols = member (op =) [eq_congruent_pred_rule, eq_congruent_rule, ite_intro_rule] -val keep_raw_lifting = member (op =) [eq_congruent_pred_rule, eq_congruent_rule, ite_intro_rule] +val keep_app_symbols = member (op =) [eq_congruent_pred_rule, eq_congruent_rule, ite_intro_rule, and_pos_rule] +val keep_raw_lifting = member (op =) [eq_congruent_pred_rule, eq_congruent_rule, ite_intro_rule, and_pos_rule] val is_SH_trivial = member (op =) [not_not_rule, contract_rule] fun is_skolemization_step (VeriT_Replay_Node {id, ...}) = is_skolemization id (* Even the veriT developers do not know if the following rule can still appear in proofs: *) val veriT_deep_skolemize_rule = "deep_skolemize" fun number_of_steps [] = 0 | number_of_steps ((VeriT_Replay_Node {subproof = (_, _, _, subproof), ...}) :: pf) = 1 + number_of_steps subproof + number_of_steps pf (* proof parser *) fun node_of p cx = ([], cx) ||>> `(with_fresh_names (term_of p)) |>> snd fun find_type_in_formula (Abs (v, T, u)) var_name = if String.isPrefix var_name v then SOME T else find_type_in_formula u var_name | find_type_in_formula (u $ v) var_name = (case find_type_in_formula u var_name of NONE => find_type_in_formula v var_name | some_T => some_T) | find_type_in_formula (Free(v, T)) var_name = if String.isPrefix var_name v then SOME T else NONE | find_type_in_formula _ _ = NONE fun synctactic_var_subst old_name new_name (u $ v) = (synctactic_var_subst old_name new_name u $ synctactic_var_subst old_name new_name v) | synctactic_var_subst old_name new_name (Abs (v, T, u)) = Abs (if String.isPrefix old_name v then new_name else v, T, synctactic_var_subst old_name new_name u) | synctactic_var_subst old_name new_name (Free (v, T)) = if String.isPrefix old_name v then Free (new_name, T) else Free (v, T) | synctactic_var_subst _ _ t = t fun synctatic_rew_in_lhs_subst old_name new_name (Const(\<^const_name>\HOL.eq\, T) $ t1 $ t2) = Const(\<^const_name>\HOL.eq\, T) $ synctactic_var_subst old_name new_name t1 $ t2 | synctatic_rew_in_lhs_subst old_name new_name (Const(\<^const_name>\Trueprop\, T) $ t1) = Const(\<^const_name>\Trueprop\, T) $ (synctatic_rew_in_lhs_subst old_name new_name t1) | synctatic_rew_in_lhs_subst _ _ t = t fun add_bound_variables_to_ctxt cx = fold (update_binding o (fn (s, SOME typ) => (s, Term (Free (s, type_of cx typ))))) local fun extract_symbols bds = bds |> map (fn (SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym x, SMTLIB.Sym y], typ) => [([x, y], typ)] | t => raise (Fail ("match error " ^ @{make_string} t))) |> flat (* onepoint can bind a variable to another variable or to a constant *) fun extract_qnt_symbols cx bds = bds |> map (fn (SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym x, SMTLIB.Sym y], typ) => (case node_of (SMTLIB.Sym y) cx of ((_, []), _) => [([x], typ)] | _ => [([x, y], typ)]) | (SMTLIB.S (SMTLIB.Sym "=" :: SMTLIB.Sym x :: _), typ) => [([x], typ)] | t => raise (Fail ("match error " ^ @{make_string} t))) |> flat fun extract_symbols_map bds = bds |> map (fn (SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym x, _], typ) => [([x], typ)]) |> flat in fun declared_csts _ "__skolem_definition" [(SMTLIB.S [SMTLIB.Sym x, typ, _], _)] = [(x, typ)] | declared_csts _ "__skolem_definition" t = raise (Fail ("unrecognized skolem_definition " ^ @{make_string} t)) | declared_csts _ _ _ = [] fun skolems_introduced_by_rule (SMTLIB.S bds) = fold (fn (SMTLIB.S [SMTLIB.Sym "=", _, SMTLIB.Sym y]) => curry (op ::) y) bds [] (*FIXME there is probably a way to use the information given by onepoint*) fun bound_vars_by_rule _ "bind" (bds) = extract_symbols bds | bound_vars_by_rule cx "onepoint" bds = extract_qnt_symbols cx bds | bound_vars_by_rule _ "sko_forall" bds = extract_symbols_map bds | bound_vars_by_rule _ "sko_ex" bds = extract_symbols_map bds | bound_vars_by_rule _ "__skolem_definition" [(SMTLIB.S [SMTLIB.Sym x, typ, _], _)] = [([x], SOME typ)] | bound_vars_by_rule _ "__skolem_definition" [(SMTLIB.S [_, SMTLIB.Sym x, _], _)] = [([x], NONE)] | bound_vars_by_rule _ _ _ = [] (* VeriT adds "?" before some variables. *) fun remove_all_qm (SMTLIB.Sym v :: l) = SMTLIB.Sym (perhaps (try (unprefix "?")) v) :: remove_all_qm l | remove_all_qm (SMTLIB.S l :: l') = SMTLIB.S (remove_all_qm l) :: remove_all_qm l' | remove_all_qm (SMTLIB.Key v :: l) = SMTLIB.Key v :: remove_all_qm l | remove_all_qm (v :: l) = v :: remove_all_qm l | remove_all_qm [] = [] fun remove_all_qm2 (SMTLIB.Sym v) = SMTLIB.Sym (perhaps (try (unprefix "?")) v) | remove_all_qm2 (SMTLIB.S l) = SMTLIB.S (remove_all_qm l) | remove_all_qm2 (SMTLIB.Key v) = SMTLIB.Key v | remove_all_qm2 v = v end datatype step_kind = ASSUME | ANCHOR | NO_STEP | NORMAL_STEP | SKOLEM fun parse_raw_proof_steps (limit : string option) (ls : SMTLIB.tree list) (cx : name_bindings) : (raw_veriT_node list * SMTLIB.tree list * name_bindings) = let fun rotate_pair (a, (b, c)) = ((a, b), c) fun step_kind [] = (NO_STEP, SMTLIB.S [], []) | step_kind ((p as SMTLIB.S (SMTLIB.Sym "anchor" :: _)) :: l) = (ANCHOR, p, l) | step_kind ((p as SMTLIB.S (SMTLIB.Sym "assume" :: _)) :: l) = (ASSUME, p, l) | step_kind ((p as SMTLIB.S (SMTLIB.Sym "step" :: _)) :: l) = (NORMAL_STEP, p, l) | step_kind ((p as SMTLIB.S (SMTLIB.Sym "define-fun" :: _)) :: l) = (SKOLEM, p, l) fun parse_skolem (SMTLIB.S [SMTLIB.Sym "define-fun", SMTLIB.Sym id, _, typ, SMTLIB.S (SMTLIB.Sym "!" :: t :: [SMTLIB.Key _, SMTLIB.Sym name])]) cx = (*replace the name binding by the constant instead of the full term in order to reduce the size of the generated terms and therefore the reconstruction time*) let val (l, cx) = (fst oo SMTLIB_Proof.extract_and_update_name_bindings) t cx |> apsnd (SMTLIB_Proof.update_name_binding (name, SMTLIB.Sym id)) in (mk_raw_node (id ^ veriT_def) veriT_def (SMTLIB.S [SMTLIB.Sym id, typ, l]) [] [] (SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym id, l]) [], cx) end | parse_skolem (SMTLIB.S [SMTLIB.Sym "define-fun", SMTLIB.Sym id, _, typ, SMTLIB.S l]) cx = let val (l, cx) = (fst oo SMTLIB_Proof.extract_and_update_name_bindings) (SMTLIB.S l ) cx in (mk_raw_node (id ^ veriT_def) veriT_def (SMTLIB.S [SMTLIB.Sym id, typ, l]) [] [] (SMTLIB.S [SMTLIB.Sym "=", SMTLIB.Sym id, l]) [], cx) end | parse_skolem t _ = raise Fail ("unrecognized VeriT proof " ^ \<^make_string> t) fun get_id_cx (SMTLIB.S ((SMTLIB.Sym _) :: (SMTLIB.Sym id) :: l), cx) = (id, (l, cx)) | get_id_cx t = raise Fail ("unrecognized VeriT proof " ^ \<^make_string> t) fun get_id (SMTLIB.S ((SMTLIB.Sym _) :: (SMTLIB.Sym id) :: l)) = (id, l) | get_id t = raise Fail ("unrecognized VeriT proof " ^ \<^make_string> t) fun parse_source (SMTLIB.Key "premises" :: SMTLIB.S source ::l, cx) = (SOME (map (fn (SMTLIB.Sym id) => id) source), (l, cx)) | parse_source (l, cx) = (NONE, (l, cx)) fun parse_rule (SMTLIB.Key "rule" :: SMTLIB.Sym r :: l, cx) = (r, (l, cx)) | parse_rule t = raise Fail ("unrecognized VeriT proof " ^ \<^make_string> t) fun parse_anchor_step (SMTLIB.S (SMTLIB.Sym "anchor" :: SMTLIB.Key "step" :: SMTLIB.Sym r :: l), cx) = (r, (l, cx)) | parse_anchor_step t = raise Fail ("unrecognized VeriT proof " ^ \<^make_string> t) fun parse_args (SMTLIB.Key "args" :: args :: l, cx) = let val ((args, cx), _) = SMTLIB_Proof.extract_and_update_name_bindings args cx in (args, (l, cx)) end | parse_args (l, cx) = (SMTLIB.S [], (l, cx)) fun parse_and_clausify_conclusion (SMTLIB.S (SMTLIB.Sym "cl" :: []) :: l, cx) = (SMTLIB.Sym "false", (l, cx)) | parse_and_clausify_conclusion (SMTLIB.S (SMTLIB.Sym "cl" :: concl) :: l, cx) = let val (concl, cx) = fold_map (fst oo SMTLIB_Proof.extract_and_update_name_bindings) concl cx in (SMTLIB.S (SMTLIB.Sym "or" :: concl), (l, cx)) end | parse_and_clausify_conclusion t = raise Fail ("unrecognized VeriT proof " ^ \<^make_string> t) val parse_normal_step = get_id_cx ##> parse_and_clausify_conclusion #> rotate_pair ##> parse_rule #> rotate_pair ##> parse_source #> rotate_pair ##> parse_args #> rotate_pair fun to_raw_node subproof ((((id, concl), rule), prems), args) = mk_raw_node id rule args (the_default [] prems) [] concl subproof fun at_discharge NONE _ = false | at_discharge (SOME id) p = p |> get_id |> fst |> (fn id2 => id = id2) in case step_kind ls of (NO_STEP, _, _) => ([],[], cx) | (NORMAL_STEP, p, l) => if at_discharge limit p then ([], ls, cx) else let val (s, (_, cx)) = (p, cx) |> parse_normal_step ||> (fn i => i) |>> (to_raw_node []) val (rp, rl, cx) = parse_raw_proof_steps limit l cx in (s :: rp, rl, cx) end | (ASSUME, p, l) => let val (id, t :: []) = p |> get_id val ((t, cx), _) = SMTLIB_Proof.extract_and_update_name_bindings t cx val s = mk_raw_node id input_rule (SMTLIB.S []) [] [] t [] val (rp, rl, cx) = parse_raw_proof_steps limit l cx in (s :: rp, rl, cx) end | (ANCHOR, p, l) => let val (anchor_id, (anchor_args, (_, cx))) = (p, cx) |> (parse_anchor_step ##> parse_args) val (subproof, discharge_step :: remaining_proof, cx) = parse_raw_proof_steps (SOME anchor_id) l cx val (curss, (_, cx)) = parse_normal_step (discharge_step, cx) val s = to_raw_node subproof (fst curss, anchor_args) val (rp, rl, cx) = parse_raw_proof_steps limit remaining_proof cx in (s :: rp, rl, cx) end | (SKOLEM, p, l) => let val (s, cx) = parse_skolem p cx val (rp, rl, cx) = parse_raw_proof_steps limit l cx in (s :: rp, rl, cx) end end fun proof_ctxt_of_rule "bind" t = t | proof_ctxt_of_rule "sko_forall" t = t | proof_ctxt_of_rule "sko_ex" t = t | proof_ctxt_of_rule "let" t = t | proof_ctxt_of_rule "onepoint" t = t | proof_ctxt_of_rule _ _ = [] fun args_of_rule "bind" t = t | args_of_rule "la_generic" t = t | args_of_rule "lia_generic" t = t | args_of_rule _ _ = [] fun insts_of_forall_inst "forall_inst" t = map (fn SMTLIB.S [_, SMTLIB.Sym x, a] => (x, a)) t | insts_of_forall_inst _ _ = [] fun id_of_last_step prems = if null prems then [] else let val VeriT_Replay_Node {id, ...} = List.last prems in [id] end fun extract_assumptions_from_subproof subproof = let fun extract_assumptions_from_subproof (VeriT_Replay_Node {rule, concl, ...}) assms = if rule = local_input_rule then concl :: assms else assms in fold extract_assumptions_from_subproof subproof [] end fun normalized_rule_name id rule = (case (rule = input_rule, can SMTLIB_Interface.role_and_index_of_assert_name id) of (true, true) => normalized_input_rule | (true, _) => local_input_rule | _ => rule) fun is_assm_repetition id rule = rule = input_rule andalso can SMTLIB_Interface.role_and_index_of_assert_name id fun extract_skolem ([SMTLIB.Sym var, typ, choice]) = (var, typ, choice) | extract_skolem t = raise Fail ("fail to parse type" ^ @{make_string} t) (* The preprocessing takes care of: 1. unfolding the shared terms 2. extract the declarations of skolems to make sure that there are not unfolded *) fun preprocess compress step = let fun expand_assms cs = map (fn t => case AList.lookup (op =) cs t of NONE => t | SOME a => a) fun expand_lonely_arguments (args as SMTLIB.S [SMTLIB.Sym "=", _, _]) = [args] | expand_lonely_arguments (x as SMTLIB.S [SMTLIB.Sym var, _]) = [SMTLIB.S [SMTLIB.Sym "=", x, SMTLIB.Sym var]] fun preprocess (Raw_VeriT_Node {id, rule, args, prems, concl, subproof, ...}) (cx, remap_assms) = let val (skolem_names, stripped_args) = args |> (fn SMTLIB.S args => args) |> map (fn SMTLIB.S [SMTLIB.Key "=", x, y] => SMTLIB.S [SMTLIB.Sym "=", x, y] | x => x) |> (rule = "bind" orelse rule = "onepoint") ? flat o (map expand_lonely_arguments) |> `(if rule = veriT_def then single o extract_skolem else K []) ||> SMTLIB.S val (subproof, (cx, _)) = fold_map preprocess subproof (cx, remap_assms) |> apfst flat val remap_assms = (if rule = "or" then (id, hd prems) :: remap_assms else remap_assms) (* declare variables in the context *) val declarations = if rule = veriT_def then skolem_names |> map (fn (name, _, choice) => (name, choice)) else [] in if compress andalso rule = "or" then ([], (cx, remap_assms)) else ([Raw_VeriT_Node {id = id, rule = rule, args = stripped_args, prems = expand_assms remap_assms prems, declarations = declarations, concl = concl, subproof = subproof}], (cx, remap_assms)) end in preprocess step end fun filter_split _ [] = ([], []) | filter_split f (a :: xs) = (if f a then apfst (curry op :: a) else apsnd (curry op :: a)) (filter_split f xs) fun collect_skolem_defs (Raw_VeriT_Node {rule, subproof = subproof, args, ...}) = (if is_skolemization rule then map (fn id => id ^ veriT_def) (skolems_introduced_by_rule args) else []) @ flat (map collect_skolem_defs subproof) fun extract_types_of_args (SMTLIB.S [var, typ, t as SMTLIB.S [SMTLIB.Sym "choice", _, _]]) = (SMTLIB.S [var, typ, t], SOME typ) |> single | extract_types_of_args (SMTLIB.S t) = let fun extract_types_of_arg (SMTLIB.S [eq, SMTLIB.S [var, typ], t]) = (SMTLIB.S [eq, var, t], SOME typ) | extract_types_of_arg t = (t, NONE) in t |> map extract_types_of_arg end (*The postprocessing does: 1. translate the terms to Isabelle syntax, taking care of free variables 2. remove the ambiguity in the proof terms: x \ y |- x = x means y = x. To remove ambiguity, we use the fact that y is a free variable and replace the term by: xy \ y |- xy = x. This is now does not have an ambiguity and we can safely move the "xy \ y" to the proof assumptions. *) fun postprocess_proof compress ctxt step cx = let fun postprocess (Raw_VeriT_Node {id, rule, args, prems, declarations, concl, subproof}) (cx, rew) = let val _ = (SMT_Config.verit_msg ctxt) (fn () => @{print} ("id =", id, "concl =", concl)) val (args) = extract_types_of_args args val globally_bound_vars = declared_csts cx rule args val cx = fold (update_binding o (fn (s, typ) => (s, Term (Free (s, type_of cx typ))))) globally_bound_vars cx (*find rebound variables specific to the LHS of the equivalence symbol*) val bound_vars = bound_vars_by_rule cx rule args val bound_vars_no_typ = map fst bound_vars val rhs_vars = fold (fn [t', t] => t <> t' ? (curry (op ::) t) | _ => fn x => x) bound_vars_no_typ [] fun not_already_bound cx t = SMTLIB_Proof.lookup_binding cx t = None andalso not (member (op =) rhs_vars t) val (shadowing_vars, rebound_lhs_vars) = bound_vars |> filter_split (fn ([t, _], typ) => not_already_bound cx t | _ => true) |>> map (apfst (hd)) |>> (fn vars => vars @ flat (map (fn ([_, t], typ) => [(t, typ)] | _ => []) bound_vars)) val subproof_rew = fold (fn [t, t'] => curry (op ::) (t, t ^ t')) (map fst rebound_lhs_vars) rew val subproof_rewriter = fold (fn (t, t') => synctatic_rew_in_lhs_subst t t') subproof_rew val ((concl, bounds), cx') = node_of concl cx val extra_lhs_vars = map (fn ([a,b], typ) => (a, a^b, typ)) rebound_lhs_vars val old_lhs_vars = map (fn (a, _, typ) => (a, typ)) extra_lhs_vars val new_lhs_vars = map (fn (_, newvar, typ) => (newvar, typ)) extra_lhs_vars (* postprocess conclusion *) val concl = SMTLIB_Isar.unskolemize_names ctxt (subproof_rewriter concl) val _ = (SMT_Config.verit_msg ctxt) (fn () => \<^print> ("id =", id, "concl =", concl)) val _ = (SMT_Config.verit_msg ctxt) (fn () => \<^print> ("id =", id, "cx' =", cx', "bound_vars =", bound_vars)) val bound_tvars = map (fn (s, SOME typ) => (s, type_of cx typ)) (shadowing_vars @ new_lhs_vars) val subproof_cx = add_bound_variables_to_ctxt cx (shadowing_vars @ new_lhs_vars) cx fun could_unify (Bound i, Bound j) = i = j | could_unify (Var v, Var v') = v = v' | could_unify (Free v, Free v') = v = v' | could_unify (Const (v, ty), Const (v', ty')) = v = v' andalso ty = ty' | could_unify (Abs (_, ty, bdy), Abs (_, ty', bdy')) = ty = ty' andalso could_unify (bdy, bdy') | could_unify (u $ v, u' $ v') = could_unify (u, u') andalso could_unify (v, v') | could_unify _ = false fun is_alpha_renaming t = t |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> could_unify handle TERM _ => false val alpha_conversion = rule = "bind" andalso is_alpha_renaming concl val can_remove_subproof = compress andalso (is_skolemization rule orelse alpha_conversion) val (fixed_subproof : veriT_replay_node list, _) = fold_map postprocess (if can_remove_subproof then [] else subproof) (subproof_cx, subproof_rew) val unsk_and_rewrite = SMTLIB_Isar.unskolemize_names ctxt o subproof_rewriter (* postprocess assms *) val stripped_args = map fst args val sanitized_args = proof_ctxt_of_rule rule stripped_args val arg_cx = add_bound_variables_to_ctxt cx (shadowing_vars @ old_lhs_vars) subproof_cx val (termified_args, _) = fold_map node_of sanitized_args arg_cx |> apfst (map fst) val normalized_args = map unsk_and_rewrite termified_args val subproof_assms = proof_ctxt_of_rule rule normalized_args (* postprocess arguments *) val rule_args = args_of_rule rule stripped_args val (termified_args, _) = fold_map term_of rule_args subproof_cx val normalized_args = map unsk_and_rewrite termified_args val rule_args = map subproof_rewriter normalized_args val raw_insts = insts_of_forall_inst rule stripped_args fun termify_term (x, t) cx = let val (t, cx) = term_of t cx in ((x, t), cx) end val (termified_args, _) = fold_map termify_term raw_insts subproof_cx val insts = Symtab.empty |> fold (fn (x, t) => fn insts => Symtab.update_new (x, t) insts) termified_args |> Symtab.map (K unsk_and_rewrite) (* declarations *) val (declarations, _) = fold_map termify_term declarations cx |> apfst (map (apsnd unsk_and_rewrite)) (* fix step *) val _ = if bounds <> [] then raise (Fail "found dangling variable in concl") else () val skolem_defs = (if is_skolemization rule then map (fn id => id ^ veriT_def) (skolems_introduced_by_rule (SMTLIB.S (map fst args))) else []) val skolems_of_subproof = (if is_skolemization rule then flat (map collect_skolem_defs subproof) else []) val fixed_prems = prems @ (if is_assm_repetition id rule then [id] else []) @ skolem_defs @ skolems_of_subproof @ (id_of_last_step fixed_subproof) (* fix subproof *) val normalized_rule = normalized_rule_name id rule |> (if compress andalso alpha_conversion then K "refl" else I) val extra_assms2 = (if rule = subproof_rule then extract_assumptions_from_subproof fixed_subproof else []) val step = mk_replay_node id normalized_rule rule_args fixed_prems subproof_assms concl [] insts declarations (bound_tvars, subproof_assms, extra_assms2, fixed_subproof) in (step, (cx', rew)) end in postprocess step (cx, []) |> (fn (step, (cx, _)) => (step, cx)) end fun combine_proof_steps ((step1 : veriT_replay_node) :: step2 :: steps) = let val (VeriT_Replay_Node {id = id1, rule = rule1, args = args1, prems = prems1, proof_ctxt = proof_ctxt1, concl = concl1, bounds = bounds1, insts = insts1, declarations = declarations1, subproof = (bound_sub1, assms_sub1, assms_extra1, subproof1)}) = step1 val (VeriT_Replay_Node {id = id2, rule = rule2, args = args2, prems = prems2, proof_ctxt = proof_ctxt2, concl = concl2, bounds = bounds2, insts = insts2, declarations = declarations2, subproof = (bound_sub2, assms_sub2, assms_extra2, subproof2)}) = step2 val goals1 = (case concl1 of _ $ (Const (\<^const_name>\HOL.disj\, _) $ _ $ (Const (\<^const_name>\HOL.disj\, _) $ (Const (\<^const_name>\HOL.Not\, _) $a) $ b)) => [a,b] | _ => []) val goal2 = (case concl2 of _ $ a => a) in if rule1 = equiv_pos2_rule andalso rule2 = th_resolution_rule andalso member (op =) prems2 id1 andalso member (op =) goals1 goal2 then mk_replay_node id2 theory_resolution2_rule args2 (filter_out (curry (op =) id1) prems2) proof_ctxt2 concl2 bounds2 insts2 declarations2 (bound_sub2, assms_sub2, assms_extra2, combine_proof_steps subproof2) :: combine_proof_steps steps else mk_replay_node id1 rule1 args1 prems1 proof_ctxt1 concl1 bounds1 insts1 declarations1 (bound_sub1, assms_sub1, assms_extra1, combine_proof_steps subproof1) :: combine_proof_steps (step2 :: steps) end | combine_proof_steps steps = steps val linearize_proof = let fun map_node_concl f (VeriT_Node {id, rule, prems, proof_ctxt, concl}) = mk_node id rule prems proof_ctxt (f concl) fun linearize (VeriT_Replay_Node {id = id, rule = rule, args = _, prems = prems, proof_ctxt = proof_ctxt, concl = concl, bounds = bounds, insts = _, declarations = _, subproof = (bounds', assms, inputs, subproof)}) = let val bounds = distinct (op =) bounds val bounds' = distinct (op =) bounds' fun mk_prop_of_term concl = concl |> fastype_of concl = \<^typ>\bool\ ? curry (op $) \<^term>\Trueprop\ fun remove_assumption_id assumption_id prems = filter_out (curry (op =) assumption_id) prems fun add_assumption assumption concl = \<^Const>\Pure.imp for \mk_prop_of_term assumption\ \mk_prop_of_term concl\\ fun inline_assumption assumption assumption_id (VeriT_Node {id, rule, prems, proof_ctxt, concl}) = mk_node id rule (remove_assumption_id assumption_id prems) proof_ctxt (add_assumption assumption concl) fun find_input_steps_and_inline [] = [] | find_input_steps_and_inline (VeriT_Node {id = id', rule, prems, concl, ...} :: steps) = if rule = input_rule then find_input_steps_and_inline (map (inline_assumption concl id') steps) else mk_node (id') rule prems [] concl :: find_input_steps_and_inline steps fun free_bounds bounds (concl) = fold (fn (var, typ) => fn t => Logic.all (Free (var, typ)) t) bounds concl val subproof = subproof |> flat o map linearize |> map (map_node_concl (fold add_assumption (assms @ inputs))) |> map (map_node_concl (free_bounds (bounds @ bounds'))) |> find_input_steps_and_inline val concl = free_bounds bounds concl in subproof @ [mk_node id rule prems proof_ctxt concl] end in linearize end fun rule_of (VeriT_Replay_Node {rule,...}) = rule fun subproof_of (VeriT_Replay_Node {subproof = (_, _, _, subproof),...}) = subproof (* Massage Skolems for Sledgehammer. We have to make sure that there is an "arrow" in the graph for skolemization steps. A. The normal easy case This function detects the steps of the form P \ Q :skolemization Q :resolution with P and replace them by Q :skolemization Throwing away the step "P \ Q" completely. This throws away a lot of information, but it does not matter too much for Sledgehammer. B. Skolems in subproofs Supporting this is more or less hopeless as long as the Isar reconstruction of Sledgehammer does not support more features like definitions. veriT is able to generate proofs with skolemization happening in subproofs inside the formula. (assume "A \ P" ... P \ Q :skolemization in the subproof ...) hence A \ P \ A \ Q :lemma ... R :something with some rule and replace them by R :skolemization with some rule Without any subproof *) fun remove_skolem_definitions_proof steps = let fun replace_equivalent_by_imp (judgement $ ((Const(\<^const_name>\HOL.eq\, typ) $ arg1) $ arg2)) = judgement $ ((Const(\<^const_name>\HOL.implies\, typ) $ arg1) $ arg2) | replace_equivalent_by_imp a = a (*This case is probably wrong*) fun remove_skolem_definitions (VeriT_Replay_Node {id = id, rule = rule, args = args, prems = prems, proof_ctxt = proof_ctxt, concl = concl, bounds = bounds, insts = insts, declarations = declarations, subproof = (vars, assms', extra_assms', subproof)}) (prems_to_remove, skolems) = let val prems = prems |> filter_out (member (op =) prems_to_remove) val trivial_step = is_SH_trivial rule fun has_skolem_substep st NONE = if is_skolemization (rule_of st) then SOME (rule_of st) else fold has_skolem_substep (subproof_of st) NONE | has_skolem_substep _ a = a val promote_to_skolem = exists (fn t => member (op =) skolems t) prems val promote_from_assms = fold has_skolem_substep subproof NONE <> NONE val promote_step = promote_to_skolem orelse promote_from_assms val skolem_step_to_skip = is_skolemization rule orelse (promote_from_assms andalso length prems > 1) val is_skolem = is_skolemization rule orelse promote_step val prems = prems |> filter_out (fn t => member (op =) skolems t) |> is_skolem ? filter_out (String.isPrefix id) val rule = (if promote_step then default_skolem_rule else rule) val subproof = subproof |> (is_skolem ? K []) (*subproofs of skolemization steps are useless for SH*) |> map (fst o (fn st => remove_skolem_definitions st (prems_to_remove, skolems))) (*no new definitions in subproofs*) |> flat val concl = concl |> is_skolem ? replace_equivalent_by_imp val step = (if skolem_step_to_skip orelse rule = veriT_def orelse trivial_step then [] else mk_replay_node id rule args prems proof_ctxt concl bounds insts declarations (vars, assms', extra_assms', subproof) |> single) val defs = (if rule = veriT_def orelse trivial_step then id :: prems_to_remove else prems_to_remove) val skolems = (if skolem_step_to_skip then id :: skolems else skolems) in (step, (defs, skolems)) end in fold_map remove_skolem_definitions steps ([], []) |> fst |> flat end local fun import_proof_and_post_process typs funs lines ctxt = let val compress = SMT_Config.compress_verit_proofs ctxt val smtlib_lines_without_qm = lines |> map single |> map SMTLIB.parse |> map remove_all_qm2 val (raw_steps, _, _) = parse_raw_proof_steps NONE smtlib_lines_without_qm SMTLIB_Proof.empty_name_binding fun process step (cx, cx') = let fun postprocess step (cx, cx') = let val (step, cx) = postprocess_proof compress ctxt step cx in (step, (cx, cx')) end in uncurry (fold_map postprocess) (preprocess compress step (cx, cx')) end val step = (empty_context ctxt typs funs, []) |> fold_map process raw_steps |> (fn (steps, (cx, _)) => (flat steps, cx)) |> compress? apfst combine_proof_steps in step end in fun parse typs funs lines ctxt = let val (u, env) = import_proof_and_post_process typs funs lines ctxt val t = u |> remove_skolem_definitions_proof |> flat o (map linearize_proof) fun node_to_step (VeriT_Node {id, rule, prems, concl, ...}) = mk_step id rule prems [] concl [] in (map node_to_step t, ctxt_of env) end fun parse_replay typs funs lines ctxt = let val (u, env) = import_proof_and_post_process typs funs lines ctxt val _ = (SMT_Config.verit_msg ctxt) (fn () => \<^print> u) in (u, ctxt_of env) end end end; diff --git a/src/HOL/Tools/SMT/verit_replay_methods.ML b/src/HOL/Tools/SMT/verit_replay_methods.ML --- a/src/HOL/Tools/SMT/verit_replay_methods.ML +++ b/src/HOL/Tools/SMT/verit_replay_methods.ML @@ -1,210 +1,210 @@ (* Title: HOL/Tools/SMT/verit_replay_methods.ML Author: Mathias Fleury, MPII, JKU Proof method for replaying veriT proofs. *) signature VERIT_REPLAY_METHODS = sig (*methods for verit proof rules*) val method_for: string -> Proof.context -> thm list -> term list -> term Symtab.table -> (string * term) list -> term -> thm val discharge: Proof.context -> thm list -> term -> thm end; structure Verit_Replay_Methods: VERIT_REPLAY_METHODS = struct open Lethe_Replay_Methods fun verit_rule_of "bind" = Bind | verit_rule_of "cong" = Cong | verit_rule_of "refl" = Refl | verit_rule_of "equiv1" = Equiv1 | verit_rule_of "equiv2" = Equiv2 | verit_rule_of "equiv_pos1" = Equiv_pos1 (*Equiv_pos2 covered below*) | verit_rule_of "equiv_neg1" = Equiv_neg1 | verit_rule_of "equiv_neg2" = Equiv_neg2 | verit_rule_of "sko_forall" = Skolem_Forall | verit_rule_of "sko_ex" = Skolem_Ex | verit_rule_of "eq_reflexive" = Eq_Reflexive | verit_rule_of "forall_inst" = Forall_Inst | verit_rule_of "implies_pos" = Implies_Pos | verit_rule_of "or" = Or | verit_rule_of "not_or" = Not_Or | verit_rule_of "resolution" = Resolution | verit_rule_of "trans" = Trans | verit_rule_of "false" = False | verit_rule_of "ac_simp" = AC_Simp | verit_rule_of "and" = And | verit_rule_of "not_and" = Not_And - | verit_rule_of "and_pos" = And_Pos | verit_rule_of "and_neg" = And_Neg | verit_rule_of "or_pos" = Or_Pos | verit_rule_of "or_neg" = Or_Neg | verit_rule_of "not_equiv1" = Not_Equiv1 | verit_rule_of "not_equiv2" = Not_Equiv2 | verit_rule_of "not_implies1" = Not_Implies1 | verit_rule_of "not_implies2" = Not_Implies2 | verit_rule_of "implies_neg1" = Implies_Neg1 | verit_rule_of "implies_neg2" = Implies_Neg2 | verit_rule_of "implies" = Implies | verit_rule_of "bfun_elim" = Bfun_Elim | verit_rule_of "ite1" = ITE1 | verit_rule_of "ite2" = ITE2 | verit_rule_of "not_ite1" = Not_ITE1 | verit_rule_of "not_ite2" = Not_ITE2 | verit_rule_of "ite_pos1" = ITE_Pos1 | verit_rule_of "ite_pos2" = ITE_Pos2 | verit_rule_of "ite_neg1" = ITE_Neg1 | verit_rule_of "ite_neg2" = ITE_Neg2 | verit_rule_of "la_disequality" = LA_Disequality | verit_rule_of "lia_generic" = LIA_Generic | verit_rule_of "la_generic" = LA_Generic | verit_rule_of "la_tautology" = LA_Tautology | verit_rule_of "la_totality" = LA_Totality | verit_rule_of "la_rw_eq"= LA_RW_Eq | verit_rule_of "nla_generic"= NLA_Generic | verit_rule_of "eq_transitive" = Eq_Transitive | verit_rule_of "qnt_rm_unused" = Qnt_Rm_Unused | verit_rule_of "onepoint" = Onepoint | verit_rule_of "qnt_join" = Qnt_Join | verit_rule_of "subproof" = Subproof | verit_rule_of "bool_simplify" = Bool_Simplify | verit_rule_of "or_simplify" = Or_Simplify | verit_rule_of "ite_simplify" = ITE_Simplify | verit_rule_of "and_simplify" = And_Simplify | verit_rule_of "not_simplify" = Not_Simplify | verit_rule_of "equiv_simplify" = Equiv_Simplify | verit_rule_of "eq_simplify" = Eq_Simplify | verit_rule_of "implies_simplify" = Implies_Simplify | verit_rule_of "connective_def" = Connective_Def | verit_rule_of "minus_simplify" = Minus_Simplify | verit_rule_of "sum_simplify" = Sum_Simplify | verit_rule_of "prod_simplify" = Prod_Simplify | verit_rule_of "comp_simplify" = Comp_Simplify | verit_rule_of "qnt_simplify" = Qnt_Simplify | verit_rule_of "tautology" = Tautological_Clause | verit_rule_of "qnt_cnf" = Qnt_CNF | verit_rule_of r = if r = Lethe_Proof.normalized_input_rule then Normalized_Input else if r = Lethe_Proof.local_input_rule then Local_Input else if r = Lethe_Proof.lethe_def then Definition else if r = Lethe_Proof.not_not_rule then Not_Not else if r = Lethe_Proof.contract_rule then Duplicate_Literals else if r = Lethe_Proof.ite_intro_rule then ITE_Intro else if r = Lethe_Proof.eq_congruent_rule then Eq_Congruent else if r = Lethe_Proof.eq_congruent_pred_rule then Eq_Congruent_Pred else if r = Lethe_Proof.theory_resolution2_rule then Theory_Resolution2 else if r = Lethe_Proof.th_resolution_rule then Theory_Resolution else if r = Lethe_Proof.equiv_pos2_rule then Equiv_pos2 + else if r = Lethe_Proof.and_pos_rule then And_Pos else (@{print} ("Unsupport rule", r); Unsupported) (* Combining all together *) fun unsupported rule ctxt thms _ _ _ = SMT_Replay_Methods.replay_error ctxt "Unsupported verit rule" rule thms fun ignore_args f ctxt thm _ _ _ t = f ctxt thm t fun ignore_decls f ctxt thm args insts _ t = f ctxt thm args insts t fun ignore_insts f ctxt thm args _ _ t = f ctxt thm args t fun choose And = ignore_args and_rule | choose And_Neg = ignore_args and_neg_rule | choose And_Pos = ignore_args and_pos | choose And_Simplify = ignore_args rewrite_and_simplify | choose Bind = ignore_insts bind | choose Bool_Simplify = ignore_args rewrite_bool_simplify | choose Comp_Simplify = ignore_args rewrite_comp_simplify | choose Cong = ignore_args cong | choose Connective_Def = ignore_args rewrite_connective_def | choose Duplicate_Literals = ignore_args duplicate_literals | choose Eq_Congruent = ignore_args eq_congruent | choose Eq_Congruent_Pred = ignore_args eq_congruent_pred | choose Eq_Reflexive = ignore_args eq_reflexive | choose Eq_Simplify = ignore_args rewrite_eq_simplify | choose Eq_Transitive = ignore_args eq_transitive | choose Equiv1 = ignore_args equiv1 | choose Equiv2 = ignore_args equiv2 | choose Equiv_neg1 = ignore_args equiv_neg1 | choose Equiv_neg2 = ignore_args equiv_neg2 | choose Equiv_pos1 = ignore_args equiv_pos1 | choose Equiv_pos2 = ignore_args equiv_pos2 | choose Equiv_Simplify = ignore_args rewrite_equiv_simplify | choose False = ignore_args false_rule | choose Forall_Inst = ignore_decls forall_inst | choose Implies = ignore_args implies_rules | choose Implies_Neg1 = ignore_args implies_neg1 | choose Implies_Neg2 = ignore_args implies_neg2 | choose Implies_Pos = ignore_args implies_pos | choose Implies_Simplify = ignore_args rewrite_implies_simplify | choose ITE1 = ignore_args ite1 | choose ITE2 = ignore_args ite2 | choose ITE_Intro = ignore_args ite_intro | choose ITE_Neg1 = ignore_args ite_neg1 | choose ITE_Neg2 = ignore_args ite_neg2 | choose ITE_Pos1 = ignore_args ite_pos1 | choose ITE_Pos2 = ignore_args ite_pos2 | choose ITE_Simplify = ignore_args rewrite_ite_simplify | choose LA_Disequality = ignore_args la_disequality | choose LA_Generic = ignore_insts la_generic | choose LA_RW_Eq = ignore_args la_rw_eq | choose LA_Tautology = ignore_args SMT_Replay_Methods.arith_th_lemma_wo_shallow | choose LA_Totality = ignore_args SMT_Replay_Methods.arith_th_lemma_wo_shallow | choose LIA_Generic = ignore_args lia_generic | choose Local_Input = ignore_args refl | choose Minus_Simplify = ignore_args rewrite_minus_simplify | choose NLA_Generic = ignore_args SMT_Replay_Methods.arith_th_lemma_wo_shallow | choose Normalized_Input = ignore_args normalized_input | choose Not_And = ignore_args not_and_rule | choose Not_Equiv1 = ignore_args not_equiv1 | choose Not_Equiv2 = ignore_args not_equiv2 | choose Not_Implies1 = ignore_args not_implies1 | choose Not_Implies2 = ignore_args not_implies2 | choose Not_ITE1 = ignore_args not_ite1 | choose Not_ITE2 = ignore_args not_ite2 | choose Not_Not = ignore_args not_not | choose Not_Or = ignore_args not_or_rule | choose Not_Simplify = ignore_args rewrite_not_simplify | choose Or = ignore_args or | choose Or_Neg = ignore_args or_neg_rule | choose Or_Pos = ignore_args or_pos_rule | choose Or_Simplify = ignore_args rewrite_or_simplify | choose Theory_Resolution2 = ignore_args theory_resolution2 | choose Prod_Simplify = ignore_args prod_simplify | choose Qnt_Join = ignore_args qnt_join | choose Qnt_Rm_Unused = ignore_args qnt_rm_unused | choose Onepoint = ignore_args onepoint | choose Qnt_Simplify = ignore_args qnt_simplify | choose Refl = ignore_args refl | choose Resolution = ignore_args unit_res | choose Skolem_Ex = ignore_args skolem_ex | choose Skolem_Forall = ignore_args skolem_forall | choose Subproof = ignore_args subproof | choose Sum_Simplify = ignore_args sum_simplify | choose Tautological_Clause = ignore_args tautological_clause | choose Theory_Resolution = ignore_args unit_res | choose AC_Simp = ignore_args tmp_AC_rule | choose Bfun_Elim = ignore_args bfun_elim | choose Qnt_CNF = ignore_args qnt_cnf | choose Trans = ignore_args trans | choose r = unsupported (string_of_verit_rule r) type verit_method = Proof.context -> thm list -> term -> thm type abs_context = int * term Termtab.table fun with_tracing rule method ctxt thms args insts decls t = let val _ = SMT_Replay_Methods.trace_goal ctxt rule thms t in method ctxt thms args insts decls t end fun method_for rule = with_tracing rule (choose (verit_rule_of rule)) fun discharge ctxt [thm] t = SMT_Replay_Methods.prove ctxt t (fn _ => resolve_tac ctxt [thm] THEN_ALL_NEW (resolve_tac ctxt @{thms refl})) end;