# HG changeset patch
# User Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
# Date 1655216068 -7200
# Node ID b6239ed66b948515b5ac651ee72c44d17470fc4a
# Parent  aeb797356de06ce8242b8d06957261404fe05899
fix veriT reconstruction for and_pos and lambda-lifting

diff -r aeb797356de0 -r b6239ed66b94 src/HOL/SMT_Examples/SMT_Tests_Verit.thy
--- 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
diff -r aeb797356de0 -r b6239ed66b94 src/HOL/Tools/SMT/lethe_proof.ML
--- 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
diff -r aeb797356de0 -r b6239ed66b94 src/HOL/Tools/SMT/verit_proof.ML
--- 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
diff -r aeb797356de0 -r b6239ed66b94 src/HOL/Tools/SMT/verit_replay_methods.ML
--- 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)