# HG changeset patch
# User desharna
# Date 1657007078 -7200
# Node ID 6d4fb57eb66c80f87f60b7c51ae584cc240833e1
# Parent  7afb6628ab866fc65e83ba41ae294e8851ae77d1
fixed diverging simproc cont_intro

diff -r 7afb6628ab86 -r 6d4fb57eb66c src/HOL/Library/Complete_Partial_Order2.thy
--- a/src/HOL/Library/Complete_Partial_Order2.thy	Mon Jul 04 10:08:10 2022 +0000
+++ b/src/HOL/Library/Complete_Partial_Order2.thy	Tue Jul 05 09:44:38 2022 +0200
@@ -368,14 +368,17 @@
       |> Thm.cterm_of ctxt
       |> Goal.init
     fun mk_thm t =
-      case SINGLE (cont_intro_tac ctxt 1) (mk_stmt t) of
-        SOME thm => SOME (Goal.finish ctxt thm RS @{thm Eq_TrueI})
-      | NONE => NONE
+      if exists_subterm Term.is_Var t then
+        NONE
+      else
+        case SINGLE (cont_intro_tac ctxt 1) (mk_stmt t) of
+          SOME thm => SOME (Goal.finish ctxt thm RS @{thm Eq_TrueI})
+        | NONE => NONE
   in
     case Thm.term_of ct of
       t as \<^Const_>\<open>ccpo.admissible _ for _ _ _\<close> => mk_thm t
     | t as \<^Const_>\<open>mcont _ _ for _ _ _ _ _\<close> => mk_thm t
-    | t as \<^Const_>\<open>monotone_on _ _ for \<^Const_>\<open>Orderings.top _\<close> _ _ _\<close> => mk_thm t
+    | t as \<^Const_>\<open>monotone_on _ _ for _ _ _ _\<close> => mk_thm t
     | _ => NONE
   end
   handle THM _ => NONE 
@@ -396,6 +399,15 @@
   tailrec.const_mono
   bind_mono
 
+experiment begin
+
+text \<open>The following proof by simplification diverges if variables are not handled properly.\<close>
+
+lemma "(\<And>f. monotone R S f \<Longrightarrow> thesis) \<Longrightarrow> monotone R S g \<Longrightarrow> thesis"
+  by simp
+
+end
+
 declare if_mono[simp]
 
 lemma monotone_id' [cont_intro]: "monotone ord ord (\<lambda>x. x)"