--- 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>.)