diff -r 5305c65dcbb2 -r 1e2a9d2251b0 src/HOL/SMT_Examples/SMT_Examples_Verit.thy
--- a/src/HOL/SMT_Examples/SMT_Examples_Verit.thy	Sun Aug 21 14:01:59 2022 +0000
+++ b/src/HOL/SMT_Examples/SMT_Examples_Verit.thy	Mon Aug 22 06:27:28 2022 +0200
@@ -15,7 +15,7 @@
 external_file \<open>SMT_Examples_Verit.certs\<close>
 
 declare [[smt_certificates = "SMT_Examples_Verit.certs"]]
-declare [[smt_read_only_certificates = true]]
+declare [[smt_read_only_certificates = false]]
 
 
 section \<open>Propositional and first-order logic\<close>
@@ -737,4 +737,82 @@
 
 lemma "g (Some (3::int)) = g (Some True)" by (smt (verit) g1 g2 g3 list.size)
 
+experiment
+begin
+
+lemma duplicate_goal: \<open>A \<Longrightarrow> A \<Longrightarrow> A\<close>
+  by auto
+
+datatype 'a M_nres = is_fail: FAIL | SPEC "'a \<Rightarrow> bool"
+
+definition "is_res m x \<equiv> case m of FAIL \<Rightarrow> True | SPEC P \<Rightarrow> P x"
+
+datatype ('a,'s) M_state = M_STATE (run: "'s \<Rightarrow> ('a\<times>'s) M_nres")
+
+(*Courtesy of Peter Lammich
+https://isabelle.zulipchat.com/#narrow/stream/247541-Mirror.3A-Isabelle-Users-Mailing-List/topic/.5Bisabelle.5D.20smt.20.28verit.29.3A.20exception.20THM.200.20raised.20.28line.20312.20.2E.2E.2E/near/290088165
+*)
+lemma "\<lbrakk>\<forall>x y. (\<forall>xa s. is_fail (run (x xa) s) \<or>
+		   is_fail (run (y xa) s) = is_fail (run (x xa) s) \<and>
+		   (\<forall>a b. is_res (run (y xa) s) (a, b) = is_res (run (x xa) s) (a, b)))
+\<longrightarrow>
+	   (\<forall>s. is_fail (run (B x) s) \<or>
+		is_fail (run (B y) s) = is_fail (run (B x) s) \<and>
+		(\<forall>a b. is_res (run (B y) s) (a, b) = is_res (run (B x) s) (a, b)));
+     \<And>y. \<forall>x ya. (\<forall>xa s. is_fail (run (x xa) s) \<or>
+			 is_fail (run (ya xa) s) = is_fail (run (x xa) s) \<and>
+			 (\<forall>a b. is_res (run (ya xa) s) (a, b) = is_res (run (x xa) s) (a, b)))
+\<longrightarrow>
+		 (\<forall>s. is_fail (run (C y x) s) \<or>
+		      is_fail (run (C y ya) s) = is_fail (run (C y x) s) \<and>
+		      (\<forall>a b. is_res (run (C y ya) s) (a, b) = is_res (run (C y x) s) (a,
+b)))\<rbrakk>
+    \<Longrightarrow> \<forall>x y. (\<forall>xa s.
+		  is_fail (run (x xa) s) \<or>
+		  is_fail (run (y xa) s) = is_fail (run (x xa) s) \<and>
+		  (\<forall>a b. is_res (run (y xa) s) (a, b) = is_res (run (x xa) s) (a, b)))
+\<longrightarrow>
+	      (\<forall>s. is_fail (run (B x) s) \<or>
+		   (\<exists>a b. is_res (run (B x) s) (a, b) \<and> is_fail (run (C a x) b)) \<or>
+		   (is_fail (run (B y) s) \<or> (\<exists>a b. is_res (run (B y) s) (a, b) \<and>
+is_fail (run (C a y) b))) =
+		   (is_fail (run (B x) s) \<or> (\<exists>a b. is_res (run (B x) s) (a, b) \<and>
+is_fail (run (C a x) b))) \<and>
+		   (\<forall>a b. (is_fail (run (B y) s) \<or>
+			   (\<exists>aa ba. is_res (run (B y) s) (aa, ba) \<and> is_res (run (C aa y)
+ba) (a, b))) =
+			  (is_fail (run (B x) s) \<or>
+			   (\<exists>aa ba. is_res (run (B x) s) (aa, ba) \<and> is_res (run (C aa x)
+ba) (a, b)))))"  
+  apply (rule duplicate_goal)
+  subgoal
+    supply [[verit_compress_proofs=true]]
+    by (smt (verit))
+  subgoal
+    supply [[verit_compress_proofs=false]]
+    by (smt (verit))
+  done
+
+(*Example of Reordering in skolemization*)
+lemma
+  fixes Abs_ExpList :: "'freeExp_list \<Rightarrow> 'exp_list" and
+    Abs_Exp:: "'freeExp_set \<Rightarrow> 'exp" and
+    exprel:: "('freeExp \<times> 'freeExp) set" and
+    map2 :: "('freeExp \<Rightarrow> 'exp) \<Rightarrow> 'freeExp_list \<Rightarrow> 'exp_list"
+  assumes "\<And>Xs. Abs_ExpList Xs \<equiv>  map2 (\<lambda>U. Abs_Exp (myImage exprel {U})) Xs"
+    "\<And>P z. (\<And>U. z = Abs_Exp (myImage exprel {U}) \<Longrightarrow> P) \<Longrightarrow> P"
+    "\<And>(ys::'exp_list) (f::'freeExp \<Rightarrow> _). (\<exists>xs. ys = map2 f xs) = (\<forall>y\<in>myset ys. \<exists>x. y = f x)"
+  shows "\<exists>Us. z = Abs_ExpList Us"
+  apply (rule duplicate_goal)
+  subgoal
+    supply [[verit_compress_proofs=true]]
+    using assms
+    by (smt (verit,del_insts))
+  subgoal
+    using assms
+    supply [[verit_compress_proofs=false]]
+    by (smt (verit,del_insts))
+  done
+
+end
 end
\ No newline at end of file