# HG changeset patch
# User wenzelm
# Date 1747828240 -7200
# Node ID c994245a696588a479607c5890a03acd313a9790
# Parent  54d6ea1ebbf65a5c5d00f8cdb908aaa55d8fed62
more concise Isabelle/ML;
some examples to test the simproc;

diff -r 54d6ea1ebbf6 -r c994245a6965 src/HOL/HOLCF/Cpo.thy
--- a/src/HOL/HOLCF/Cpo.thy	Wed May 21 10:30:35 2025 +0200
+++ b/src/HOL/HOLCF/Cpo.thy	Wed May 21 13:50:40 2025 +0200
@@ -1105,25 +1105,25 @@
   using cont_id by (rule cont2cont_fun)
 
 simproc_setup apply_cont (\<open>cont (\<lambda>f. E f)\<close>) = \<open>
-  K (fn ctxt => fn ct =>
-     let val t = Thm.term_of ct
-         val foo = case t of _ $ foo => foo
-     in  case foo of Abs (_, _, expr) =>
-              if   fst (strip_comb expr) = Bound 0
-              (* since \<open>\<lambda>f. E f\<close> is too permissive, we ensure that the term is of the
-                 form \<open>\<lambda>f. f ...\<close> (for example \<open>\<lambda>f. f x\<close>, or \<open>\<lambda>f. f x y\<close>, etc.) *)
-              then let val tac = Metis_Tactic.metis_tac ["no_types"] "combs" ctxt
-                                 @{thms cont2cont_fun cont_id}
-                       val rwrt_ct  = HOLogic.mk_judgment (Thm.apply \<^cterm>\<open>\<lambda>lhs. lhs = True\<close> ct)
-                       val rwrt_thm = Goal.prove_internal ctxt [] rwrt_ct (fn _ => tac 1)
-                   in  SOME (mk_meta_eq rwrt_thm)
-                   end
-              else NONE
-            | _ => NONE
-     end
-    )
+  fn _ => fn ctxt => fn ct =>
+    (case Thm.term_of ct of
+      \<^Const_>\<open>cont _ _ for \<open>Abs (_, _, expr)\<close>\<close> =>
+        if Term.head_of expr = Bound 0
+        (* since \<open>\<lambda>f. E f\<close> is too permissive, we ensure that the term is of the
+           form \<open>\<lambda>f. f ...\<close> (for example \<open>\<lambda>f. f x\<close>, or \<open>\<lambda>f. f x y\<close>, etc.) *)
+        then
+          let
+            val tac = Metis_Tactic.metis_tac ["no_types"] "combs" ctxt @{thms cont2cont_fun cont_id}
+            val rwrt_ct  = HOLogic.mk_judgment (Thm.apply \<^cterm>\<open>\<lambda>lhs. lhs = True\<close> ct)
+            val rwrt_thm = Goal.prove_internal ctxt [] rwrt_ct (fn _ => tac 1)
+          in SOME (mk_meta_eq rwrt_thm) end
+        else NONE
+    | _ => NONE)
 \<close>
 
+lemma "cont (\<lambda>f. f x)" and "cont (\<lambda>f. f x y)" and "cont (\<lambda>f. f x y z)"
+  by simp_all
+
 text \<open>
   Lambda abstraction preserves monotonicity and continuity.
   (Note \<open>(\<lambda>x. \<lambda>y. f x y) = f\<close>.)