--- a/src/HOL/SMT_Examples/SMT_Tests_Verit.thy Mon Jun 13 20:02:00 2022 +0200
+++ b/src/HOL/SMT_Examples/SMT_Tests_Verit.thy Tue Jun 14 16:14:28 2022 +0200
@@ -717,4 +717,20 @@
"{x. x \<in> P} = {y. y \<in> P}"
by (smt smt_sets)+
+
+context
+ fixes in_multiset :: "'d \<Rightarrow> 'd_multiset \<Rightarrow> bool" and
+ add_mset :: "'d \<Rightarrow> 'd_multiset \<Rightarrow> 'd_multiset" and
+ set_mset :: "'d_multiset \<Rightarrow> 'd set"
+begin
+lemma
+ assumes "\<And>a b A. ((a::'d) \<in> insert b A) = (a = b \<or> a \<in> A)"
+ "\<And>a A. set_mset (add_mset (a::'d) A) = insert a (set_mset A)"
+ "\<And>r. transp (r::'d \<Rightarrow> 'd \<Rightarrow> bool) = (\<forall>x y z. r x y \<longrightarrow> r y z \<longrightarrow> r x z)"
+ shows
+ "transp (\<lambda>x y. (x::'d) \<in> set_mset (add_mset m M) \<and> y \<in> set_mset (add_mset m M) \<and> R x y) \<Longrightarrow>
+ transp (\<lambda>x y. x \<in> set_mset M \<and> y \<in> set_mset M \<and> R x y)"
+ by (smt (verit) assms)
end
+
+end
--- a/src/HOL/Tools/SMT/lethe_proof.ML Mon Jun 13 20:02:00 2022 +0200
+++ b/src/HOL/Tools/SMT/lethe_proof.ML Tue Jun 14 16:14:28 2022 +0200
@@ -58,6 +58,7 @@
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
@@ -142,11 +143,12 @@
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
--- a/src/HOL/Tools/SMT/verit_proof.ML Mon Jun 13 20:02:00 2022 +0200
+++ b/src/HOL/Tools/SMT/verit_proof.ML Tue Jun 14 16:14:28 2022 +0200
@@ -55,6 +55,7 @@
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
@@ -248,11 +249,12 @@
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
--- a/src/HOL/Tools/SMT/verit_replay_methods.ML Mon Jun 13 20:02:00 2022 +0200
+++ b/src/HOL/Tools/SMT/verit_replay_methods.ML Tue Jun 14 16:14:28 2022 +0200
@@ -41,7 +41,6 @@
| 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
@@ -101,6 +100,7 @@
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)