# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1736894103 0
# Node ID 6026394145593789bff350d567194cbde41e93b6
# Parent  1655c4a3516be0181827604fae41b31fe7c8e619
Some work on an ancient theory file. And a weird failure in Float.thy

diff -r 1655c4a3516b -r 602639414559 src/HOL/Library/Complete_Partial_Order2.thy
--- a/src/HOL/Library/Complete_Partial_Order2.thy	Tue Jan 14 21:50:44 2025 +0000
+++ b/src/HOL/Library/Complete_Partial_Order2.thy	Tue Jan 14 22:35:03 2025 +0000
@@ -13,48 +13,48 @@
 lemma chain_transfer [transfer_rule]:
   includes lifting_syntax
   shows "((A ===> A ===> (=)) ===> rel_set A ===> (=)) Complete_Partial_Order.chain Complete_Partial_Order.chain"
-unfolding chain_def[abs_def] by transfer_prover
-                             
+  unfolding chain_def[abs_def] by transfer_prover
+
 lemma linorder_chain [simp, intro!]:
   fixes Y :: "_ :: linorder set"
   shows "Complete_Partial_Order.chain (\<le>) Y"
-by(auto intro: chainI)
+  by(auto intro: chainI)
 
 lemma fun_lub_apply: "\<And>Sup. fun_lub Sup Y x = Sup ((\<lambda>f. f x) ` Y)"
-by(simp add: fun_lub_def image_def)
+  by(simp add: fun_lub_def image_def)
 
 lemma fun_lub_empty [simp]: "fun_lub lub {} = (\<lambda>_. lub {})"
-by(rule ext)(simp add: fun_lub_apply)
+  by(rule ext)(simp add: fun_lub_apply)
 
 lemma chain_fun_ordD: 
   assumes "Complete_Partial_Order.chain (fun_ord le) Y"
   shows "Complete_Partial_Order.chain le ((\<lambda>f. f x) ` Y)"
-by(rule chainI)(auto dest: chainD[OF assms] simp add: fun_ord_def)
+  by(rule chainI)(auto dest: chainD[OF assms] simp add: fun_ord_def)
 
 lemma chain_Diff:
   "Complete_Partial_Order.chain ord A
   \<Longrightarrow> Complete_Partial_Order.chain ord (A - B)"
-by(erule chain_subset) blast
+  by(erule chain_subset) blast
 
 lemma chain_rel_prodD1:
   "Complete_Partial_Order.chain (rel_prod orda ordb) Y
   \<Longrightarrow> Complete_Partial_Order.chain orda (fst ` Y)"
-by(auto 4 3 simp add: chain_def)
+  by(auto 4 3 simp add: chain_def)
 
 lemma chain_rel_prodD2:
   "Complete_Partial_Order.chain (rel_prod orda ordb) Y
   \<Longrightarrow> Complete_Partial_Order.chain ordb (snd ` Y)"
-by(auto 4 3 simp add: chain_def)
+  by(auto 4 3 simp add: chain_def)
 
 
 context ccpo begin
 
 lemma ccpo_fun: "class.ccpo (fun_lub Sup) (fun_ord (\<le>)) (mk_less (fun_ord (\<le>)))"
   by standard (auto 4 3 simp add: mk_less_def fun_ord_def fun_lub_apply
-    intro: order.trans order.antisym chain_imageI ccpo_Sup_upper ccpo_Sup_least)
+      intro: order.trans order.antisym chain_imageI ccpo_Sup_upper ccpo_Sup_least)
 
 lemma ccpo_Sup_below_iff: "Complete_Partial_Order.chain (\<le>) Y \<Longrightarrow> Sup Y \<le> x \<longleftrightarrow> (\<forall>y\<in>Y. y \<le> x)"
-by(fast intro: order_trans[OF ccpo_Sup_upper] ccpo_Sup_least)
+  by (meson local.ccpo_Sup_least local.ccpo_Sup_upper local.dual_order.trans)
 
 lemma Sup_minus_bot: 
   assumes chain: "Complete_Partial_Order.chain (\<le>) A"
@@ -152,11 +152,9 @@
   proof(rule ccpo_Sup_least)
     fix y
     assume "y \<in> (\<lambda>x. f x x) ` Y"
-    then obtain x where "x \<in> Y" and "y = f x x" by blast note this(2)
-    also from chain2[OF \<open>x \<in> Y\<close>] have "\<dots> \<le> \<Squnion>(f x ` Y)"
-      by(rule ccpo_Sup_upper)(simp add: \<open>x \<in> Y\<close>)
-    also have "\<dots> \<le> ?lhs" by(rule ccpo_Sup_upper[OF chain1])(simp add: \<open>x \<in> Y\<close>)
-    finally show "y \<le> ?lhs" .
+    then obtain x where "x \<in> Y" and "y = f x x" by blast
+    then show "y \<le> ?lhs"
+      by (metis (no_types, lifting) chain1 chain2 imageI ccpo_Sup_upper order.trans)
   qed
 qed
 
@@ -180,6 +178,7 @@
   finally show "x \<le> \<dots>" .
 qed
 
+
 lemma swap_Sup:
   fixes le_b (infix \<open>\<sqsubseteq>\<close> 60)
   assumes Y: "Complete_Partial_Order.chain (\<sqsubseteq>) Y"
@@ -222,11 +221,10 @@
     proof(rule ccpo_Sup_least)
       fix x'
       assume "x' \<in> (\<lambda>f. f x) ` Z"
-      then obtain f where "f \<in> Z" "x' = f x" by blast note this(2)
-      also have "f x \<le> f y" using \<open>f \<in> Z\<close> \<open>x \<sqsubseteq> y\<close> by(rule monotoneD[OF mono])
-      also have "f y \<le> ?rhs" using chain3
-        by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> Z\<close>)
-      finally show "x' \<le> ?rhs" .
+      then obtain f where "f \<in> Z" "x' = f x" by blast 
+      then show "x' \<le> ?rhs"
+        by (metis (mono_tags, lifting) \<open>x \<sqsubseteq> y\<close> chain3 imageI ccpo_Sup_upper
+            order_trans mono monotoneD)
     qed
   qed
 
@@ -239,11 +237,10 @@
     proof(rule ccpo_Sup_least)
       fix x'
       assume "x' \<in> f ` Y"
-      then obtain y where "y \<in> Y" "x' = f y" by blast note this(2)
-      also have "f y \<le> \<Squnion>((\<lambda>f. f y) ` Z)" using chain3
-        by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> Z\<close>)
-      also have "\<dots> \<le> ?rhs" using chain4 by(rule ccpo_Sup_upper)(simp add: \<open>y \<in> Y\<close>)
-      finally show "x' \<le> ?rhs" .
+      then obtain y where "y \<in> Y" "x' = f y" by blast
+      then show "x' \<le> ?rhs"
+        by (metis (mono_tags, lifting) \<open>f \<in> Z\<close> chain3 chain4 imageI local.ccpo_Sup_upper
+            order.trans)
     qed
     finally show "x \<le> ?rhs" .
   qed
@@ -257,12 +254,10 @@
     proof(rule ccpo_Sup_least)
       fix x'
       assume "x' \<in> (\<lambda>f. f y) ` Z"
-      then obtain f where "f \<in> Z" "x' = f y" by blast note this(2)
-      also have "f y \<le> \<Squnion>(f ` Y)" using chain1[OF \<open>f \<in> Z\<close>]
-        by(rule ccpo_Sup_upper)(simp add: \<open>y \<in> Y\<close>)
-      also have "\<dots> \<le> ?lhs" using chain2
-        by(rule ccpo_Sup_upper)(simp add: \<open>f \<in> Z\<close>)
-      finally show "x' \<le> ?lhs" .
+      then obtain f where "f \<in> Z" "x' = f y" by blast
+      then show "x' \<le> ?lhs"
+        by (metis (mono_tags, lifting) \<open>y \<in> Y\<close> ccpo_Sup_below_iff chain1 chain2 imageI
+            ccpo_Sup_upper)
     qed
     finally show "x \<le> ?lhs" .
   qed
@@ -411,47 +406,47 @@
 declare if_mono[simp]
 
 lemma monotone_id' [cont_intro]: "monotone ord ord (\<lambda>x. x)"
-by(simp add: monotone_def)
+  by(simp add: monotone_def)
 
 lemma monotone_applyI:
   "monotone orda ordb F \<Longrightarrow> monotone (fun_ord orda) ordb (\<lambda>f. F (f x))"
-by(rule monotoneI)(auto simp add: fun_ord_def dest: monotoneD)
+  by(rule monotoneI)(auto simp add: fun_ord_def dest: monotoneD)
 
 lemma monotone_if_fun [partial_function_mono]:
   "\<lbrakk> monotone (fun_ord orda) (fun_ord ordb) F; monotone (fun_ord orda) (fun_ord ordb) G \<rbrakk>
   \<Longrightarrow> monotone (fun_ord orda) (fun_ord ordb) (\<lambda>f n. if c n then F f n else G f n)"
-by(simp add: monotone_def fun_ord_def)
+  by(simp add: monotone_def fun_ord_def)
 
 lemma monotone_fun_apply_fun [partial_function_mono]: 
   "monotone (fun_ord (fun_ord ord)) (fun_ord ord) (\<lambda>f n. f t (g n))"
-by(rule monotoneI)(simp add: fun_ord_def)
+  by(rule monotoneI)(simp add: fun_ord_def)
 
 lemma monotone_fun_ord_apply: 
   "monotone orda (fun_ord ordb) f \<longleftrightarrow> (\<forall>x. monotone orda ordb (\<lambda>y. f y x))"
-by(auto simp add: monotone_def fun_ord_def)
+  by(auto simp add: monotone_def fun_ord_def)
 
 context preorder begin
 
 declare transp_on_le[cont_intro]
 
 lemma monotone_const [simp, cont_intro]: "monotone ord (\<le>) (\<lambda>_. c)"
-by(rule monotoneI) simp
+  by(rule monotoneI) simp
 
 end
 
 lemma transp_le [cont_intro, simp]:
   "class.preorder ord (mk_less ord) \<Longrightarrow> transp ord"
-by(rule preorder.transp_on_le)
+  by(rule preorder.transp_on_le)
 
 context partial_function_definitions begin
 
 declare const_mono [cont_intro, simp]
 
 lemma transp_le [cont_intro, simp]: "transp leq"
-by(rule transpI)(rule leq_trans)
+  by(rule transpI)(rule leq_trans)
 
 lemma preorder [cont_intro, simp]: "class.preorder leq (mk_less leq)"
-by(unfold_locales)(auto simp add: mk_less_def intro: leq_refl leq_trans)
+  by(unfold_locales)(auto simp add: mk_less_def intro: leq_refl leq_trans)
 
 declare ccpo[cont_intro, simp]
 
@@ -460,91 +455,91 @@
 lemma contI [intro?]:
   "(\<And>Y. \<lbrakk> Complete_Partial_Order.chain orda Y; Y \<noteq> {} \<rbrakk> \<Longrightarrow> f (luba Y) = lubb (f ` Y)) 
   \<Longrightarrow> cont luba orda lubb ordb f"
-unfolding cont_def by blast
+  unfolding cont_def by blast
 
 lemma contD:
   "\<lbrakk> cont luba orda lubb ordb f; Complete_Partial_Order.chain orda Y; Y \<noteq> {} \<rbrakk> 
   \<Longrightarrow> f (luba Y) = lubb (f ` Y)"
-unfolding cont_def by blast
+  unfolding cont_def by blast
 
 lemma cont_id [simp, cont_intro]: "\<And>Sup. cont Sup ord Sup ord id"
-by(rule contI) simp
+  by(rule contI) simp
 
 lemma cont_id' [simp, cont_intro]: "\<And>Sup. cont Sup ord Sup ord (\<lambda>x. x)"
-using cont_id[unfolded id_def] .
+  using cont_id[unfolded id_def] .
 
 lemma cont_applyI [cont_intro]:
   assumes cont: "cont luba orda lubb ordb g"
   shows "cont (fun_lub luba) (fun_ord orda) lubb ordb (\<lambda>f. g (f x))"
-by(rule contI)(drule chain_fun_ordD[where x=x], simp add: fun_lub_apply image_image contD[OF cont])
+  by(rule contI)(drule chain_fun_ordD[where x=x], simp add: fun_lub_apply image_image contD[OF cont])
 
 lemma call_cont: "cont (fun_lub lub) (fun_ord ord) lub ord (\<lambda>f. f t)"
-by(simp add: cont_def fun_lub_apply)
+  by(simp add: cont_def fun_lub_apply)
 
 lemma cont_if [cont_intro]:
   "\<lbrakk> cont luba orda lubb ordb f; cont luba orda lubb ordb g \<rbrakk>
   \<Longrightarrow> cont luba orda lubb ordb (\<lambda>x. if c then f x else g x)"
-by(cases c) simp_all
+  by(cases c) simp_all
 
 lemma mcontI [intro?]:
-   "\<lbrakk> monotone orda ordb f; cont luba orda lubb ordb f \<rbrakk> \<Longrightarrow> mcont luba orda lubb ordb f"
-by(simp add: mcont_def)
+  "\<lbrakk> monotone orda ordb f; cont luba orda lubb ordb f \<rbrakk> \<Longrightarrow> mcont luba orda lubb ordb f"
+  by(simp add: mcont_def)
 
 lemma mcont_mono: "mcont luba orda lubb ordb f \<Longrightarrow> monotone orda ordb f"
-by(simp add: mcont_def)
+  by(simp add: mcont_def)
 
 lemma mcont_cont [simp]: "mcont luba orda lubb ordb f \<Longrightarrow> cont luba orda lubb ordb f"
-by(simp add: mcont_def)
+  by(simp add: mcont_def)
 
 lemma mcont_monoD:
   "\<lbrakk> mcont luba orda lubb ordb f; orda x y \<rbrakk> \<Longrightarrow> ordb (f x) (f y)"
-by(auto simp add: mcont_def dest: monotoneD)
+  by(auto simp add: mcont_def dest: monotoneD)
 
 lemma mcont_contD:
   "\<lbrakk> mcont luba orda lubb ordb f; Complete_Partial_Order.chain orda Y; Y \<noteq> {} \<rbrakk>
   \<Longrightarrow> f (luba Y) = lubb (f ` Y)"
-by(auto simp add: mcont_def dest: contD)
+  by(auto simp add: mcont_def dest: contD)
 
 lemma mcont_call [cont_intro, simp]:
   "mcont (fun_lub lub) (fun_ord ord) lub ord (\<lambda>f. f t)"
-by(simp add: mcont_def call_mono call_cont)
+  by(simp add: mcont_def call_mono call_cont)
 
 lemma mcont_id' [cont_intro, simp]: "mcont lub ord lub ord (\<lambda>x. x)"
-by(simp add: mcont_def monotone_id')
+  by(simp add: mcont_def monotone_id')
 
 lemma mcont_applyI:
   "mcont luba orda lubb ordb (\<lambda>x. F x) \<Longrightarrow> mcont (fun_lub luba) (fun_ord orda) lubb ordb (\<lambda>f. F (f x))"
-by(simp add: mcont_def monotone_applyI cont_applyI)
+  by(simp add: mcont_def monotone_applyI cont_applyI)
 
 lemma mcont_if [cont_intro, simp]:
   "\<lbrakk> mcont luba orda lubb ordb (\<lambda>x. f x); mcont luba orda lubb ordb (\<lambda>x. g x) \<rbrakk>
   \<Longrightarrow> mcont luba orda lubb ordb (\<lambda>x. if c then f x else g x)"
-by(simp add: mcont_def cont_if)
+  by(simp add: mcont_def cont_if)
 
 lemma cont_fun_lub_apply: 
   "cont luba orda (fun_lub lubb) (fun_ord ordb) f \<longleftrightarrow> (\<forall>x. cont luba orda lubb ordb (\<lambda>y. f y x))"
-by(simp add: cont_def fun_lub_def fun_eq_iff)(auto simp add: image_def)
+  by(simp add: cont_def fun_lub_def fun_eq_iff)(auto simp add: image_def)
 
 lemma mcont_fun_lub_apply: 
   "mcont luba orda (fun_lub lubb) (fun_ord ordb) f \<longleftrightarrow> (\<forall>x. mcont luba orda lubb ordb (\<lambda>y. f y x))"
-by(auto simp add: monotone_fun_ord_apply cont_fun_lub_apply mcont_def)
+  by(auto simp add: monotone_fun_ord_apply cont_fun_lub_apply mcont_def)
 
 context ccpo begin
 
 lemma cont_const [simp, cont_intro]: "cont luba orda Sup (\<le>) (\<lambda>x. c)"
-by (rule contI) (simp add: image_constant_conv cong del: SUP_cong_simp)
+  by (rule contI) (simp add: image_constant_conv cong del: SUP_cong_simp)
 
 lemma mcont_const [cont_intro, simp]:
   "mcont luba orda Sup (\<le>) (\<lambda>x. c)"
-by(simp add: mcont_def)
+  by(simp add: mcont_def)
 
 lemma cont_apply:
   assumes 2: "\<And>x. cont lubb ordb Sup (\<le>) (\<lambda>y. f x y)"
-  and t: "cont luba orda lubb ordb (\<lambda>x. t x)"
-  and 1: "\<And>y. cont luba orda Sup (\<le>) (\<lambda>x. f x y)"
-  and mono: "monotone orda ordb (\<lambda>x. t x)"
-  and mono2: "\<And>x. monotone ordb (\<le>) (\<lambda>y. f x y)"
-  and mono1: "\<And>y. monotone orda (\<le>) (\<lambda>x. f x y)"
+    and t: "cont luba orda lubb ordb (\<lambda>x. t x)"
+    and 1: "\<And>y. cont luba orda Sup (\<le>) (\<lambda>x. f x y)"
+    and mono: "monotone orda ordb (\<lambda>x. t x)"
+    and mono2: "\<And>x. monotone ordb (\<le>) (\<lambda>y. f x y)"
+    and mono1: "\<And>y. monotone orda (\<le>) (\<lambda>x. f x y)"
   shows "cont luba orda Sup (\<le>) (\<lambda>x. f x (t x))"
 proof
   fix Y
@@ -561,16 +556,16 @@
      \<And>y. mcont lub ord Sup (\<le>) (\<lambda>x. f x y);
      mcont lub ord lub' ord' (\<lambda>y. t y) \<rbrakk>
   \<Longrightarrow> mcont lub ord Sup (\<le>) (\<lambda>x. f x (t x))"
-unfolding mcont_def by(blast intro: transp_on_le monotone2monotone cont_apply)
+  unfolding mcont_def by(blast intro: transp_on_le monotone2monotone cont_apply)
 
 lemma mcont2mcont:
   "\<lbrakk>mcont lub' ord' Sup (\<le>) (\<lambda>x. f x); mcont lub ord lub' ord' (\<lambda>x. t x)\<rbrakk> 
   \<Longrightarrow> mcont lub ord Sup (\<le>) (\<lambda>x. f (t x))"
-by(rule mcont2mcont'[OF _ mcont_const]) 
+  by(rule mcont2mcont'[OF _ mcont_const]) 
 
 context
   fixes ord :: "'b \<Rightarrow> 'b \<Rightarrow> bool" (infix \<open>\<sqsubseteq>\<close> 60) 
-  and lub :: "'b set \<Rightarrow> 'b" (\<open>\<Or>\<close>)
+    and lub :: "'b set \<Rightarrow> 'b" (\<open>\<Or>\<close>)
 begin
 
 lemma cont_fun_lub_Sup:
@@ -818,42 +813,42 @@
 lemma admissible_disj' [simp, cont_intro]:
   "\<lbrakk> class.ccpo lub ord (mk_less ord); ccpo.admissible lub ord P; ccpo.admissible lub ord Q \<rbrakk>
   \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. P x \<or> Q x)"
-by(rule ccpo.admissible_disj)
+  by(rule ccpo.admissible_disj)
 
 lemma admissible_imp' [cont_intro]:
   "\<lbrakk> class.ccpo lub ord (mk_less ord);
      ccpo.admissible lub ord (\<lambda>x. \<not> P x);
      ccpo.admissible lub ord (\<lambda>x. Q x) \<rbrakk>
   \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. P x \<longrightarrow> Q x)"
-unfolding imp_conv_disj by(rule ccpo.admissible_disj)
+  unfolding imp_conv_disj by(rule ccpo.admissible_disj)
 
 lemma admissible_imp [cont_intro]:
   "(Q \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. P x))
   \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. Q \<longrightarrow> P x)"
-by(rule ccpo.admissibleI)(auto dest: ccpo.admissibleD)
+  by(rule ccpo.admissibleI)(auto dest: ccpo.admissibleD)
 
 lemma admissible_not_mem' [THEN admissible_subst, cont_intro, simp]:
   shows admissible_not_mem: "ccpo.admissible Union (\<subseteq>) (\<lambda>A. x \<notin> A)"
-by(rule ccpo.admissibleI) auto
+  by(rule ccpo.admissibleI) auto
 
 lemma admissible_eqI:
   assumes f: "cont luba orda lub ord (\<lambda>x. f x)"
-  and g: "cont luba orda lub ord (\<lambda>x. g x)"
+    and g: "cont luba orda lub ord (\<lambda>x. g x)"
   shows "ccpo.admissible luba orda (\<lambda>x. f x = g x)"
-apply(rule ccpo.admissibleI)
-apply(simp_all add: contD[OF f] contD[OF g] cong: image_cong)
-done
+  apply(rule ccpo.admissibleI)
+  apply(simp_all add: contD[OF f] contD[OF g] cong: image_cong)
+  done
 
 corollary admissible_eq_mcontI [cont_intro]:
   "\<lbrakk> mcont luba orda lub ord (\<lambda>x. f x); 
     mcont luba orda lub ord (\<lambda>x. g x) \<rbrakk>
   \<Longrightarrow> ccpo.admissible luba orda (\<lambda>x. f x = g x)"
-by(rule admissible_eqI)(auto simp add: mcont_def)
+  by(rule admissible_eqI)(auto simp add: mcont_def)
 
 lemma admissible_iff [cont_intro, simp]:
   "\<lbrakk> ccpo.admissible lub ord (\<lambda>x. P x \<longrightarrow> Q x); ccpo.admissible lub ord (\<lambda>x. Q x \<longrightarrow> P x) \<rbrakk>
   \<Longrightarrow> ccpo.admissible lub ord (\<lambda>x. P x \<longleftrightarrow> Q x)"
-by(subst iff_conv_conj_imp)(rule admissible_conj)
+  by(subst iff_conv_conj_imp)(rule admissible_conj)
 
 context ccpo begin
 
@@ -999,35 +994,35 @@
     and bot: "P (\<lambda>_. lub {})"
     and step: "\<And>f'. \<lbrakk> P (U f'); le_fun (U f') (U f) \<rbrakk> \<Longrightarrow> P (U (F f'))"
   shows "P (U f)"
-unfolding eq inverse
-apply (rule ccpo.fixp_strong_induct[OF ccpo adm])
-apply (insert mono, auto simp: monotone_def fun_ord_def bot fun_lub_def)[2]
-apply (rule_tac f'5="C x" in step)
-apply (simp_all add: inverse eq)
-done
+  unfolding eq inverse
+  apply (rule ccpo.fixp_strong_induct[OF ccpo adm])
+    apply (insert mono, auto simp: monotone_def fun_ord_def bot fun_lub_def)[2]
+  apply (rule_tac f'5="C x" in step)
+   apply (simp_all add: inverse eq)
+  done
 
 end
 
 subsection \<open>\<^term>\<open>(=)\<close> as order\<close>
 
 definition lub_singleton :: "('a set \<Rightarrow> 'a) \<Rightarrow> bool"
-where "lub_singleton lub \<longleftrightarrow> (\<forall>a. lub {a} = a)"
+  where "lub_singleton lub \<longleftrightarrow> (\<forall>a. lub {a} = a)"
 
 definition the_Sup :: "'a set \<Rightarrow> 'a"
-where "the_Sup A = (THE a. a \<in> A)"
+  where "the_Sup A = (THE a. a \<in> A)"
 
 lemma lub_singleton_the_Sup [cont_intro, simp]: "lub_singleton the_Sup"
-by(simp add: lub_singleton_def the_Sup_def)
+  by(simp add: lub_singleton_def the_Sup_def)
 
 lemma (in ccpo) lub_singleton: "lub_singleton Sup"
-by(simp add: lub_singleton_def)
+  by(simp add: lub_singleton_def)
 
 lemma (in partial_function_definitions) lub_singleton [cont_intro, simp]: "lub_singleton lub"
-by(rule ccpo.lub_singleton)(rule Partial_Function.ccpo[OF partial_function_definitions_axioms])
+  by(rule ccpo.lub_singleton)(rule Partial_Function.ccpo[OF partial_function_definitions_axioms])
 
 lemma preorder_eq [cont_intro, simp]:
   "class.preorder (=) (mk_less (=))"
-by(unfold_locales)(simp_all add: mk_less_def)
+  by(unfold_locales)(simp_all add: mk_less_def)
 
 lemma monotone_eqI [cont_intro]:
   assumes "class.preorder ord (mk_less ord)"
@@ -1052,23 +1047,23 @@
 lemma mcont_eqI [cont_intro, simp]:
   "\<lbrakk> class.preorder ord (mk_less ord); lub_singleton lub \<rbrakk>
   \<Longrightarrow> mcont the_Sup (=) lub ord f"
-by(simp add: mcont_def cont_eqI monotone_eqI)
+  by(simp add: mcont_def cont_eqI monotone_eqI)
 
 subsection \<open>ccpo for products\<close>
 
 definition prod_lub :: "('a set \<Rightarrow> 'a) \<Rightarrow> ('b set \<Rightarrow> 'b) \<Rightarrow> ('a \<times> 'b) set \<Rightarrow> 'a \<times> 'b"
-where "prod_lub Sup_a Sup_b Y = (Sup_a (fst ` Y), Sup_b (snd ` Y))"
+  where "prod_lub Sup_a Sup_b Y = (Sup_a (fst ` Y), Sup_b (snd ` Y))"
 
 lemma lub_singleton_prod_lub [cont_intro, simp]:
   "\<lbrakk> lub_singleton luba; lub_singleton lubb \<rbrakk> \<Longrightarrow> lub_singleton (prod_lub luba lubb)"
-by(simp add: lub_singleton_def prod_lub_def)
+  by(simp add: lub_singleton_def prod_lub_def)
 
 lemma prod_lub_empty [simp]: "prod_lub luba lubb {} = (luba {}, lubb {})"
-by(simp add: prod_lub_def)
+  by(simp add: prod_lub_def)
 
 lemma preorder_rel_prodI [cont_intro, simp]:
   assumes "class.preorder orda (mk_less orda)"
-  and "class.preorder ordb (mk_less ordb)"
+    and "class.preorder ordb (mk_less ordb)"
   shows "class.preorder (rel_prod orda ordb) (mk_less (rel_prod orda ordb))"
 proof -
   interpret a: preorder orda "mk_less orda" by fact
@@ -1078,9 +1073,9 @@
 
 lemma order_rel_prodI:
   assumes a: "class.order orda (mk_less orda)"
-  and b: "class.order ordb (mk_less ordb)"
+    and b: "class.order ordb (mk_less ordb)"
   shows "class.order (rel_prod orda ordb) (mk_less (rel_prod orda ordb))"
-  (is "class.order ?ord ?ord'")
+    (is "class.order ?ord ?ord'")
 proof(intro class.order.intro class.order_axioms.intro)
   interpret a: order orda "mk_less orda" by(fact a)
   interpret b: order ordb "mk_less ordb" by(fact b)
@@ -1093,10 +1088,10 @@
 
 lemma monotone_rel_prodI:
   assumes mono2: "\<And>a. monotone ordb ordc (\<lambda>b. f (a, b))"
-  and mono1: "\<And>b. monotone orda ordc (\<lambda>a. f (a, b))"
-  and a: "class.preorder orda (mk_less orda)"
-  and b: "class.preorder ordb (mk_less ordb)"
-  and c: "class.preorder ordc (mk_less ordc)"
+    and mono1: "\<And>b. monotone orda ordc (\<lambda>a. f (a, b))"
+    and a: "class.preorder orda (mk_less orda)"
+    and b: "class.preorder ordb (mk_less ordb)"
+    and c: "class.preorder ordc (mk_less ordc)"
   shows "monotone (rel_prod orda ordb) ordc f"
 proof -
   interpret a: preorder orda "mk_less orda" by(rule a)
@@ -1108,7 +1103,7 @@
 
 lemma monotone_rel_prodD1:
   assumes mono: "monotone (rel_prod orda ordb) ordc f"
-  and preorder: "class.preorder ordb (mk_less ordb)"
+    and preorder: "class.preorder ordb (mk_less ordb)"
   shows "monotone orda ordc (\<lambda>a. f (a, b))"
 proof -
   interpret preorder ordb "mk_less ordb" by(rule preorder)
@@ -1117,7 +1112,7 @@
 
 lemma monotone_rel_prodD2:
   assumes mono: "monotone (rel_prod orda ordb) ordc f"
-  and preorder: "class.preorder orda (mk_less orda)"
+    and preorder: "class.preorder orda (mk_less orda)"
   shows "monotone ordb ordc (\<lambda>b. f (a, b))"
 proof -
   interpret preorder orda "mk_less orda" by(rule preorder)
@@ -1129,68 +1124,68 @@
     class.preorder orda (mk_less orda); class.preorder ordb (mk_less ordb);
     class.preorder ordc (mk_less ordc) \<rbrakk>
   \<Longrightarrow> monotone (rel_prod orda ordb) ordc (case_prod f)"
-by(rule monotone_rel_prodI) simp_all
+  by(rule monotone_rel_prodI) simp_all
 
 lemma monotone_case_prodD1:
   assumes mono: "monotone (rel_prod orda ordb) ordc (case_prod f)"
-  and preorder: "class.preorder ordb (mk_less ordb)"
+    and preorder: "class.preorder ordb (mk_less ordb)"
   shows "monotone orda ordc (\<lambda>a. f a b)"
-using monotone_rel_prodD1[OF assms] by simp
+  using monotone_rel_prodD1[OF assms] by simp
 
 lemma monotone_case_prodD2:
   assumes mono: "monotone (rel_prod orda ordb) ordc (case_prod f)"
-  and preorder: "class.preorder orda (mk_less orda)"
+    and preorder: "class.preorder orda (mk_less orda)"
   shows "monotone ordb ordc (f a)"
-using monotone_rel_prodD2[OF assms] by simp
+  using monotone_rel_prodD2[OF assms] by simp
 
 context 
   fixes orda ordb ordc
   assumes a: "class.preorder orda (mk_less orda)"
-  and b: "class.preorder ordb (mk_less ordb)"
-  and c: "class.preorder ordc (mk_less ordc)"
+    and b: "class.preorder ordb (mk_less ordb)"
+    and c: "class.preorder ordc (mk_less ordc)"
 begin
 
 lemma monotone_rel_prod_iff:
   "monotone (rel_prod orda ordb) ordc f \<longleftrightarrow>
    (\<forall>a. monotone ordb ordc (\<lambda>b. f (a, b))) \<and> 
    (\<forall>b. monotone orda ordc (\<lambda>a. f (a, b)))"
-using a b c by(blast intro: monotone_rel_prodI dest: monotone_rel_prodD1 monotone_rel_prodD2)
+  using a b c by(blast intro: monotone_rel_prodI dest: monotone_rel_prodD1 monotone_rel_prodD2)
 
 lemma monotone_case_prod_iff [simp]:
   "monotone (rel_prod orda ordb) ordc (case_prod f) \<longleftrightarrow>
    (\<forall>a. monotone ordb ordc (f a)) \<and> (\<forall>b. monotone orda ordc (\<lambda>a. f a b))"
-by(simp add: monotone_rel_prod_iff)
+  by(simp add: monotone_rel_prod_iff)
 
 end
 
 lemma monotone_case_prod_apply_iff:
   "monotone orda ordb (\<lambda>x. (case_prod f x) y) \<longleftrightarrow> monotone orda ordb (case_prod (\<lambda>a b. f a b y))"
-by(simp add: monotone_def)
+  by(simp add: monotone_def)
 
 lemma monotone_case_prod_applyD:
   "monotone orda ordb (\<lambda>x. (case_prod f x) y)
   \<Longrightarrow> monotone orda ordb (case_prod (\<lambda>a b. f a b y))"
-by(simp add: monotone_case_prod_apply_iff)
+  by(simp add: monotone_case_prod_apply_iff)
 
 lemma monotone_case_prod_applyI:
   "monotone orda ordb (case_prod (\<lambda>a b. f a b y))
   \<Longrightarrow> monotone orda ordb (\<lambda>x. (case_prod f x) y)"
-by(simp add: monotone_case_prod_apply_iff)
+  by(simp add: monotone_case_prod_apply_iff)
 
 
 lemma cont_case_prod_apply_iff:
   "cont luba orda lubb ordb (\<lambda>x. (case_prod f x) y) \<longleftrightarrow> cont luba orda lubb ordb (case_prod (\<lambda>a b. f a b y))"
-by(simp add: cont_def split_def)
+  by(simp add: cont_def split_def)
 
 lemma cont_case_prod_applyI:
   "cont luba orda lubb ordb (case_prod (\<lambda>a b. f a b y))
   \<Longrightarrow> cont luba orda lubb ordb (\<lambda>x. (case_prod f x) y)"
-by(simp add: cont_case_prod_apply_iff)
+  by(simp add: cont_case_prod_apply_iff)
 
 lemma cont_case_prod_applyD:
   "cont luba orda lubb ordb (\<lambda>x. (case_prod f x) y)
   \<Longrightarrow> cont luba orda lubb ordb (case_prod (\<lambda>a b. f a b y))"
-by(simp add: cont_case_prod_apply_iff)
+  by(simp add: cont_case_prod_apply_iff)
 
 lemma mcont_case_prod_apply_iff [simp]:
   "mcont luba orda lubb ordb (\<lambda>x. (case_prod f x) y) \<longleftrightarrow> 
@@ -1307,13 +1302,8 @@
   and t: "monotone orda ordb (\<lambda>x. t x)"
   and t': "monotone orda ordc (\<lambda>x. t' x)"
   shows "monotone orda leq (\<lambda>x. f (t x) (t' x))"
-proof(rule monotoneI)
-  fix x y
-  assume "orda x y"
-  hence "rel_prod ordb ordc (t x, t' x) (t y, t' y)"
-    using t t' by(auto dest: monotoneD)
-  from monotoneD[OF f this] show "leq (f (t x) (t' x)) (f (t y) (t' y))" by simp
-qed
+  by (metis (mono_tags, lifting) case_prod_conv monotoneD monotoneI rel_prod.intros
+      assms)
 
 lemma cont_case_prodI [cont_intro]:
   "\<lbrakk> monotone (rel_prod orda ordb) leq (case_prod f);
@@ -1322,7 +1312,7 @@
     class.preorder orda (mk_less orda);
     class.preorder ordb (mk_less ordb) \<rbrakk>
   \<Longrightarrow> cont (prod_lub luba lubb) (rel_prod orda ordb) lub leq (case_prod f)"
-by(rule ccpo.cont_case_prodI)(rule Partial_Function.ccpo[OF partial_function_definitions_axioms])
+  by(rule ccpo.cont_case_prodI)(rule Partial_Function.ccpo[OF partial_function_definitions_axioms])
 
 lemma cont_case_prod_iff:
   "\<lbrakk> monotone (rel_prod orda ordb) leq (case_prod f);
@@ -1330,39 +1320,39 @@
      class.preorder ordb (mk_less ordb); lub_singleton lubb \<rbrakk>
   \<Longrightarrow> cont (prod_lub luba lubb) (rel_prod orda ordb) lub leq (case_prod f) \<longleftrightarrow>
    (\<forall>x. cont lubb ordb lub leq (\<lambda>y. f x y)) \<and> (\<forall>y. cont luba orda lub leq (\<lambda>x. f x y))"
-by(blast dest: cont_case_prodD1 cont_case_prodD2 intro: cont_case_prodI)
+  by(blast dest: cont_case_prodD1 cont_case_prodD2 intro: cont_case_prodI)
 
 lemma mcont_case_prod_iff [simp]:
   "\<lbrakk> class.preorder orda (mk_less orda); lub_singleton luba;
      class.preorder ordb (mk_less ordb); lub_singleton lubb \<rbrakk>
   \<Longrightarrow> mcont (prod_lub luba lubb) (rel_prod orda ordb) lub leq (case_prod f) \<longleftrightarrow>
    (\<forall>x. mcont lubb ordb lub leq (\<lambda>y. f x y)) \<and> (\<forall>y. mcont luba orda lub leq (\<lambda>x. f x y))"
-unfolding mcont_def by(auto simp add: cont_case_prod_iff)
+  unfolding mcont_def by(auto simp add: cont_case_prod_iff)
 
 end
 
 lemma mono2mono_case_prod [cont_intro]:
   assumes "\<And>x y. monotone orda ordb (\<lambda>f. pair f x y)"
   shows "monotone orda ordb (\<lambda>f. case_prod (pair f) x)"
-by(rule monotoneI)(auto split: prod.split dest: monotoneD[OF assms])
+  by(rule monotoneI)(auto split: prod.split dest: monotoneD[OF assms])
 
 subsection \<open>Complete lattices as ccpo\<close>
 
 context complete_lattice begin
 
 lemma complete_lattice_ccpo: "class.ccpo Sup (\<le>) (<)"
-by(unfold_locales)(fast intro: Sup_upper Sup_least)+
+  by(unfold_locales)(fast intro: Sup_upper Sup_least)+
 
 lemma complete_lattice_ccpo': "class.ccpo Sup (\<le>) (mk_less (\<le>))"
-by(unfold_locales)(auto simp add: mk_less_def intro: Sup_upper Sup_least)
+  by(unfold_locales)(auto simp add: mk_less_def intro: Sup_upper Sup_least)
 
 lemma complete_lattice_partial_function_definitions: 
   "partial_function_definitions (\<le>) Sup"
-by(unfold_locales)(auto intro: Sup_least Sup_upper)
+  by(unfold_locales)(auto intro: Sup_least Sup_upper)
 
 lemma complete_lattice_partial_function_definitions_dual:
   "partial_function_definitions (\<ge>) Inf"
-by(unfold_locales)(auto intro: Inf_lower Inf_greatest)
+  by(unfold_locales)(auto intro: Inf_lower Inf_greatest)
 
 lemmas [cont_intro, simp] =
   Partial_Function.ccpo[OF complete_lattice_partial_function_definitions]
@@ -1370,18 +1360,18 @@
 
 lemma mono2mono_inf:
   assumes f: "monotone ord (\<le>) (\<lambda>x. f x)" 
-  and g: "monotone ord (\<le>) (\<lambda>x. g x)"
+    and g: "monotone ord (\<le>) (\<lambda>x. g x)"
   shows "monotone ord (\<le>) (\<lambda>x. f x \<sqinter> g x)"
-by(auto 4 3 dest: monotoneD[OF f] monotoneD[OF g] intro: le_infI1 le_infI2 intro!: monotoneI)
+  by(auto 4 3 dest: monotoneD[OF f] monotoneD[OF g] intro: le_infI1 le_infI2 intro!: monotoneI)
 
 lemma mcont_const [simp]: "mcont lub ord Sup (\<le>) (\<lambda>_. c)"
-by(rule ccpo.mcont_const[OF complete_lattice_ccpo])
+  by(rule ccpo.mcont_const[OF complete_lattice_ccpo])
 
 lemma mono2mono_sup:
   assumes f: "monotone ord (\<le>) (\<lambda>x. f x)"
-  and g: "monotone ord (\<le>) (\<lambda>x. g x)"
+    and g: "monotone ord (\<le>) (\<lambda>x. g x)"
   shows "monotone ord (\<le>) (\<lambda>x. f x \<squnion> g x)"
-by(auto 4 3 intro!: monotoneI intro: sup.coboundedI1 sup.coboundedI2 dest: monotoneD[OF f] monotoneD[OF g])
+  by(auto 4 3 intro!: monotoneI intro: sup.coboundedI1 sup.coboundedI2 dest: monotoneD[OF f] monotoneD[OF g])
 
 lemma Sup_image_sup: 
   assumes "Y \<noteq> {}"
@@ -1408,16 +1398,16 @@
 qed
 
 lemma mcont_sup1: "mcont Sup (\<le>) Sup (\<le>) (\<lambda>y. x \<squnion> y)"
-by(auto 4 3 simp add: mcont_def sup.coboundedI1 sup.coboundedI2 intro!: monotoneI contI intro: Sup_image_sup[symmetric])
+  by(auto 4 3 simp add: mcont_def sup.coboundedI1 sup.coboundedI2 intro!: monotoneI contI intro: Sup_image_sup[symmetric])
 
 lemma mcont_sup2: "mcont Sup (\<le>) Sup (\<le>) (\<lambda>x. x \<squnion> y)"
-by(subst sup_commute)(rule mcont_sup1)
+  by(subst sup_commute)(rule mcont_sup1)
 
 lemma mcont2mcont_sup [cont_intro, simp]:
   "\<lbrakk> mcont lub ord Sup (\<le>) (\<lambda>x. f x);
      mcont lub ord Sup (\<le>) (\<lambda>x. g x) \<rbrakk>
   \<Longrightarrow> mcont lub ord Sup (\<le>) (\<lambda>x. f x \<squnion> g x)"
-by(best intro: ccpo.mcont2mcont'[OF complete_lattice_ccpo] mcont_sup1 mcont_sup2 ccpo.mcont_const[OF complete_lattice_ccpo])
+  by(best intro: ccpo.mcont2mcont'[OF complete_lattice_ccpo] mcont_sup1 mcont_sup2 ccpo.mcont_const[OF complete_lattice_ccpo])
 
 end
 
@@ -1426,59 +1416,59 @@
 context complete_distrib_lattice begin
 
 lemma mcont_inf1: "mcont Sup (\<le>) Sup (\<le>) (\<lambda>y. x \<sqinter> y)"
-by(auto intro: monotoneI contI simp add: le_infI2 inf_Sup mcont_def)
+  by(auto intro: monotoneI contI simp add: le_infI2 inf_Sup mcont_def)
 
 lemma mcont_inf2: "mcont Sup (\<le>) Sup (\<le>) (\<lambda>x. x \<sqinter> y)"
-by(auto intro: monotoneI contI simp add: le_infI1 Sup_inf mcont_def)
+  by(auto intro: monotoneI contI simp add: le_infI1 Sup_inf mcont_def)
 
 lemma mcont2mcont_inf [cont_intro, simp]:
   "\<lbrakk> mcont lub ord Sup (\<le>) (\<lambda>x. f x);
     mcont lub ord Sup (\<le>) (\<lambda>x. g x) \<rbrakk>
   \<Longrightarrow> mcont lub ord Sup (\<le>) (\<lambda>x. f x \<sqinter> g x)"
-by(best intro: ccpo.mcont2mcont'[OF complete_lattice_ccpo] mcont_inf1 mcont_inf2 ccpo.mcont_const[OF complete_lattice_ccpo])
+  by(best intro: ccpo.mcont2mcont'[OF complete_lattice_ccpo] mcont_inf1 mcont_inf2 ccpo.mcont_const[OF complete_lattice_ccpo])
 
 end
 
 interpretation lfp: partial_function_definitions "(\<le>) :: _ :: complete_lattice \<Rightarrow> _" Sup
-by(rule complete_lattice_partial_function_definitions)
+  by(rule complete_lattice_partial_function_definitions)
 
 declaration \<open>Partial_Function.init "lfp" \<^term>\<open>lfp.fixp_fun\<close> \<^term>\<open>lfp.mono_body\<close>
   @{thm lfp.fixp_rule_uc} @{thm lfp.fixp_induct_uc} NONE\<close>
 
 interpretation gfp: partial_function_definitions "(\<ge>) :: _ :: complete_lattice \<Rightarrow> _" Inf
-by(rule complete_lattice_partial_function_definitions_dual)
+  by(rule complete_lattice_partial_function_definitions_dual)
 
 declaration \<open>Partial_Function.init "gfp" \<^term>\<open>gfp.fixp_fun\<close> \<^term>\<open>gfp.mono_body\<close>
   @{thm gfp.fixp_rule_uc} @{thm gfp.fixp_induct_uc} NONE\<close>
 
 lemma insert_mono [partial_function_mono]:
-   "monotone (fun_ord (\<subseteq>)) (\<subseteq>) A \<Longrightarrow> monotone (fun_ord (\<subseteq>)) (\<subseteq>) (\<lambda>y. insert x (A y))"
-by(rule monotoneI)(auto simp add: fun_ord_def dest: monotoneD)
+  "monotone (fun_ord (\<subseteq>)) (\<subseteq>) A \<Longrightarrow> monotone (fun_ord (\<subseteq>)) (\<subseteq>) (\<lambda>y. insert x (A y))"
+  by(rule monotoneI)(auto simp add: fun_ord_def dest: monotoneD)
 
 lemma mono2mono_insert [THEN lfp.mono2mono, cont_intro, simp]:
   shows monotone_insert: "monotone (\<subseteq>) (\<subseteq>) (insert x)"
-by(rule monotoneI) blast
+  by(rule monotoneI) blast
 
 lemma mcont2mcont_insert[THEN lfp.mcont2mcont, cont_intro, simp]:
   shows mcont_insert: "mcont Union (\<subseteq>) Union (\<subseteq>) (insert x)"
-by(blast intro: mcontI contI monotone_insert)
+  by(blast intro: mcontI contI monotone_insert)
 
 lemma mono2mono_image [THEN lfp.mono2mono, cont_intro, simp]:
   shows monotone_image: "monotone (\<subseteq>) (\<subseteq>) ((`) f)"
-by(rule monotoneI) blast
+  by(rule monotoneI) blast
 
 lemma cont_image: "cont Union (\<subseteq>) Union (\<subseteq>) ((`) f)"
-by(rule contI)(auto)
+  by(rule contI)(auto)
 
 lemma mcont2mcont_image [THEN lfp.mcont2mcont, cont_intro, simp]:
   shows mcont_image: "mcont Union (\<subseteq>) Union (\<subseteq>) ((`) f)"
-by(blast intro: mcontI monotone_image cont_image)
+  by(blast intro: mcontI monotone_image cont_image)
 
 context complete_lattice begin
 
 lemma monotone_Sup [cont_intro, simp]:
   "monotone ord (\<subseteq>) f \<Longrightarrow> monotone ord (\<le>) (\<lambda>x. \<Squnion>f x)"
-by(blast intro: monotoneI Sup_least Sup_upper dest: monotoneD)
+  by(blast intro: monotoneI Sup_least Sup_upper dest: monotoneD)
 
 lemma cont_Sup:
   assumes "cont lub ord Union (\<subseteq>) f"
@@ -1694,21 +1684,21 @@
   for P
 
 lemma monotone_fst: "monotone (rel_prod orda ordb) orda fst"
-by(auto intro: monotoneI)
+  by(auto intro: monotoneI)
 
 lemma mcont_fst: "mcont (prod_lub luba lubb) (rel_prod orda ordb) luba orda fst"
-by(auto intro!: mcontI monotoneI contI simp add: prod_lub_def)
+  by(auto intro!: mcontI monotoneI contI simp add: prod_lub_def)
 
 lemma mcont2mcont_fst [cont_intro, simp]:
   "mcont lub ord (prod_lub luba lubb) (rel_prod orda ordb) t
   \<Longrightarrow> mcont lub ord luba orda (\<lambda>x. fst (t x))"
-by(auto intro!: mcontI monotoneI contI dest: mcont_monoD mcont_contD simp add: rel_prod_sel split_beta prod_lub_def image_image)
+  by(auto intro!: mcontI monotoneI contI dest: mcont_monoD mcont_contD simp add: rel_prod_sel split_beta prod_lub_def image_image)
 
 lemma monotone_snd: "monotone (rel_prod orda ordb) ordb snd"
-by(auto intro: monotoneI)
+  by(auto intro: monotoneI)
 
 lemma mcont_snd: "mcont (prod_lub luba lubb) (rel_prod orda ordb) lubb ordb snd"
-by(auto intro!: mcontI monotoneI contI simp add: prod_lub_def)
+  by(auto intro!: mcontI monotoneI contI simp add: prod_lub_def)
 
 lemma mcont2mcont_snd [cont_intro, simp]:
   "mcont lub ord (prod_lub luba lubb) (rel_prod orda ordb) t
@@ -1718,19 +1708,20 @@
 lemma monotone_Pair:
   "\<lbrakk> monotone ord orda f; monotone ord ordb g \<rbrakk>
   \<Longrightarrow> monotone ord (rel_prod orda ordb) (\<lambda>x. (f x, g x))"
-by(simp add: monotone_def)
+  by(simp add: monotone_def)
 
 lemma cont_Pair:
   "\<lbrakk> cont lub ord luba orda f; cont lub ord lubb ordb g \<rbrakk>
   \<Longrightarrow> cont lub ord (prod_lub luba lubb) (rel_prod orda ordb) (\<lambda>x. (f x, g x))"
-by(rule contI)(auto simp add: prod_lub_def image_image dest!: contD)
+  by(rule contI)(auto simp add: prod_lub_def image_image dest!: contD)
 
 lemma mcont_Pair:
   "\<lbrakk> mcont lub ord luba orda f; mcont lub ord lubb ordb g \<rbrakk>
   \<Longrightarrow> mcont lub ord (prod_lub luba lubb) (rel_prod orda ordb) (\<lambda>x. (f x, g x))"
-by(rule mcontI)(simp_all add: monotone_Pair mcont_mono cont_Pair)
+  by(rule mcontI)(simp_all add: monotone_Pair mcont_mono cont_Pair)
 
-context partial_function_definitions begin
+context partial_function_definitions 
+begin
 text \<open>Specialised versions of @{thm [source] mcont_call} for admissibility proofs for parallel fixpoint inductions\<close>
 lemmas mcont_call_fst [cont_intro] = mcont_call[THEN mcont2mcont, OF mcont_fst]
 lemmas mcont_call_snd [cont_intro] = mcont_call[THEN mcont2mcont, OF mcont_snd]
diff -r 1655c4a3516b -r 602639414559 src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Tue Jan 14 21:50:44 2025 +0000
+++ b/src/HOL/Library/Float.thy	Tue Jan 14 22:35:03 2025 +0000
@@ -1849,7 +1849,7 @@
            (plus_down prec (nprt b * nprt bb)
              (plus_down prec (pprt a * pprt ab)
                (pprt b * nprt ab)))"
-  by (smt (verit, del_insts) mult_mono plus_down_mono add_mono nprt_mono nprt_le_zero zero_le_pprt 
+  by (smt (verit, best) mult_mono plus_down_mono add_mono nprt_mono nprt_le_zero zero_le_pprt 
 pprt_mono mult_mono_nonpos_nonneg mult_mono_nonpos_nonpos mult_mono_nonneg_nonpos)
 
 lemma mult_float_mono2:
@@ -1867,7 +1867,7 @@
            (plus_up prec (pprt aa * nprt bc)
              (plus_up prec (nprt ba * pprt ac)
                (nprt aa * nprt ac)))"
-  by (smt (verit, del_insts) plus_up_mono add_mono mult_mono nprt_mono nprt_le_zero zero_le_pprt pprt_mono 
+  by (smt (verit, best) plus_up_mono add_mono mult_mono nprt_mono nprt_le_zero zero_le_pprt pprt_mono 
       mult_mono_nonpos_nonneg mult_mono_nonpos_nonpos mult_mono_nonneg_nonpos)