merged
authorpaulson
Tue, 18 Mar 2025 18:12:07 +0000
changeset 82303 d546eb345426
parent 82301 bd61b838501c (diff)
parent 82302 19ada02fa486 (current diff)
child 82305 332afbd48bcf
child 82306 c88b27669bfa
merged
--- a/NEWS	Tue Mar 18 18:11:58 2025 +0000
+++ b/NEWS	Tue Mar 18 18:12:07 2025 +0000
@@ -22,31 +22,52 @@
     the formula "r \<subset> A \<times> A \<and> refl_on A r". INCOMPATIBILITY.
   - Removed predicate single_valuedp. Use predicate right_unique instead.
     INCOMPATIBILITY.
+  - Removed lemmas. Minor INCOMPATIBILITY.
+      antisym_empty[simp] (use antisym_on_bot instead)
+      antisym_bot[simp] (use antisymp_on_bot instead)
+      trans_empty[simp] (use trans_on_bot instead)
   - Strengthened lemmas. Minor INCOMPATIBILITY.
       refl_on_empty[simp]
   - Strengthened (and renamed) lemmas. Minor INCOMPATIBILITY.
       antisymp_equality[simp] ~> antisymp_on_equality[simp]
       transp_equality[simp] ~> transp_on_equality[simp]
   - Added lemmas.
+      antisym_on_bot[simp]
       antisymp_on_bot[simp]
+      asym_on_bot[simp]
       asymp_on_bot[simp]
+      irrefl_on_bot[simp]
       irreflp_on_bot[simp]
       left_unique_bot[simp]
       left_unique_iff_Uniq
+      refl_on_top[simp]
       reflp_on_refl_on_eq[pred_set_conv]
+      reflp_on_top[simp]
+      sym_on_bot[simp]
+      sym_on_top[simp]
       symp_on_bot[simp]
       symp_on_equality[simp]
+      symp_on_top[simp]
+      total_on_top[simp]
       totalp_on_mono[mono]
       totalp_on_mono_strong
       totalp_on_mono_stronger
       totalp_on_mono_stronger_alt
+      totalp_on_top[simp]
+      trans_on_bot[simp]
+      trans_on_top[simp]
       transp_on_bot[simp]
+      transp_on_top[simp]
 
 * Theory "HOL.Wellfounded":
+  - Removed lemmas. Minor INCOMPATIBILITY.
+      wf_empty[iff] (use wf_on_bot instead)
   - Added lemmas.
       bex_rtrancl_min_element_if_wf_on
       bex_rtrancl_min_element_if_wfp_on
+      wf_on_bot[simp]
       wf_on_lex_prod[intro]
+      wfp_on_bot[simp]
       wfp_on_iff_wfp
 
 * Theory "HOL.Order_Relation":
--- a/src/HOL/BNF_Wellorder_Constructions.thy	Tue Mar 18 18:11:58 2025 +0000
+++ b/src/HOL/BNF_Wellorder_Constructions.thy	Tue Mar 18 18:12:07 2025 +0000
@@ -847,7 +847,7 @@
     moreover
     {assume Case2: "\<not> Well_order r0"
       hence "?R = {}" unfolding ordLess_def by auto
-      hence "wf ?R" using wf_empty by simp
+      hence "wf ?R" by simp
     }
     ultimately have "wf ?R" by blast
   }
--- a/src/HOL/Library/Extended_Real.thy	Tue Mar 18 18:11:58 2025 +0000
+++ b/src/HOL/Library/Extended_Real.thy	Tue Mar 18 18:12:07 2025 +0000
@@ -298,7 +298,7 @@
 | "real_of_ereal \<infinity> = 0"
 | "real_of_ereal (-\<infinity>) = 0"
   by (auto intro: ereal_cases)
-termination by standard (rule wf_empty)
+termination by standard (rule wf_on_bot)
 
 lemma real_of_ereal[simp]:
   "real_of_ereal (- x :: ereal) = - (real_of_ereal x)"
@@ -327,7 +327,7 @@
 | "\<bar>-\<infinity>\<bar> = (\<infinity>::ereal)"
 | "\<bar>\<infinity>\<bar> = (\<infinity>::ereal)"
 by (auto intro: ereal_cases)
-termination proof qed (rule wf_empty)
+termination proof qed (rule wf_on_bot)
 
 instance ..
 
@@ -377,7 +377,7 @@
   with prems show P
    by (cases rule: ereal2_cases[of a b]) auto
 qed auto
-termination by standard (rule wf_empty)
+termination by standard (rule wf_on_bot)
 
 lemma Infty_neq_0[simp]:
   "(\<infinity>::ereal) \<noteq> 0" "0 \<noteq> (\<infinity>::ereal)"
@@ -852,7 +852,7 @@
 | "sgn (\<infinity>::ereal) = 1"
 | "sgn (-\<infinity>::ereal) = -1"
 by (auto intro: ereal_cases)
-termination by standard (rule wf_empty)
+termination by standard (rule wf_on_bot)
 
 function times_ereal where
   "ereal r * ereal p = ereal (r * p)"
--- a/src/HOL/Library/Old_Recdef.thy	Tue Mar 18 18:11:58 2025 +0000
+++ b/src/HOL/Library/Old_Recdef.thy	Tue Mar 18 18:12:07 2025 +0000
@@ -82,6 +82,6 @@
   wf_measures
   wf_pred_nat
   wf_same_fst
-  wf_empty
+  wf_on_bot
 
 end
--- a/src/HOL/Relation.thy	Tue Mar 18 18:11:58 2025 +0000
+++ b/src/HOL/Relation.thy	Tue Mar 18 18:12:07 2025 +0000
@@ -203,6 +203,12 @@
   obtains "r x x"
   using assms by (auto dest: refl_onD simp add: reflp_def)
 
+lemma refl_on_top[simp]: "refl_on A \<top>"
+  by (simp add: refl_on_def)
+
+lemma reflp_on_top[simp]: "reflp_on A \<top>"
+  by (simp add: reflp_on_def)
+
 lemma reflp_on_subset: "reflp_on A R \<Longrightarrow> B \<subseteq> A \<Longrightarrow> reflp_on B R"
   by (auto intro: reflp_onI dest: reflp_onD)
 
@@ -316,8 +322,11 @@
 lemma irreflpD: "irreflp R \<Longrightarrow> \<not> R x x"
   by (rule irreflD[to_pred])
 
+lemma irrefl_on_bot[simp]: "irrefl_on A \<bottom>"
+  by (simp add: irrefl_on_def)
+
 lemma irreflp_on_bot[simp]: "irreflp_on A \<bottom>"
-  by (simp add: irreflp_on_def)
+  using irrefl_on_bot[to_pred] .
 
 lemma irrefl_on_distinct [code]: "irrefl_on A r \<longleftrightarrow> (\<forall>(a, b) \<in> r. a \<in> A \<longrightarrow> b \<in> A \<longrightarrow> a \<noteq> b)"
   by (auto simp add: irrefl_on_def)
@@ -385,8 +394,11 @@
 lemma asympD: "asymp R \<Longrightarrow> R x y \<Longrightarrow> \<not> R y x"
   by (rule asymD[to_pred])
 
+lemma asym_on_bot[simp]: "asym_on A \<bottom>"
+  by (simp add: asym_on_def)
+
 lemma asymp_on_bot[simp]: "asymp_on A \<bottom>"
-  by (simp add: asymp_on_def)
+  using asym_on_bot[to_pred] .
 
 lemma asym_iff: "asym r \<longleftrightarrow> (\<forall>x y. (x,y) \<in> r \<longrightarrow> (y,x) \<notin> r)"
   by (blast dest: asymD)
@@ -440,7 +452,16 @@
 
 lemmas symp_sym_eq = symp_on_sym_on_eq[of UNIV] \<comment> \<open>For backward compatibility\<close>
 
+lemma sym_on_bot[simp]: "sym_on A \<bottom>"
+  by (simp add: sym_on_def)
+
 lemma symp_on_bot[simp]: "symp_on A \<bottom>"
+  using sym_on_bot[to_pred] .
+
+lemma sym_on_top[simp]: "sym_on A \<top>"
+  by (simp add: sym_on_def)
+
+lemma symp_on_top[simp]: "symp_on A \<top>"
   by (simp add: symp_on_def)
 
 lemma sym_on_subset: "sym_on A r \<Longrightarrow> B \<subseteq> A \<Longrightarrow> sym_on B r"
@@ -542,8 +563,11 @@
 
 lemmas antisymp_antisym_eq = antisymp_on_antisym_on_eq[of UNIV] \<comment> \<open>For backward compatibility\<close>
 
+lemma antisym_on_bot[simp]: "antisym_on A \<bottom>"
+  by (simp add: antisym_on_def)
+
 lemma antisymp_on_bot[simp]: "antisymp_on A \<bottom>"
-  by (simp add: antisymp_on_def)
+  using antisym_on_bot[to_pred] .
 
 lemma antisym_on_subset: "antisym_on A r \<Longrightarrow> B \<subseteq> A \<Longrightarrow> antisym_on B r"
   by (auto simp: antisym_on_def)
@@ -596,14 +620,6 @@
   "r \<le> s \<Longrightarrow> antisymp s \<Longrightarrow> antisymp r"
   by (fact antisym_subset [to_pred])
     
-lemma antisym_empty [simp]:
-  "antisym {}"
-  unfolding antisym_def by blast
-
-lemma antisym_bot [simp]:
-  "antisymp \<bottom>"
-  by (fact antisym_empty [to_pred])
-    
 lemma antisymp_on_equality[simp]: "antisymp_on A (=)"
   by (auto intro: antisymp_onI)
 
@@ -732,10 +748,16 @@
 lemma transp_on_equality[simp]: "transp_on A (=)"
   by (auto intro: transp_onI)
 
-lemma trans_empty [simp]: "trans {}"
-  by (blast intro: transI)
+lemma trans_on_bot[simp]: "trans_on A \<bottom>"
+  by (simp add: trans_on_def)
 
 lemma transp_on_bot[simp]: "transp_on A \<bottom>"
+  using trans_on_bot[to_pred] .
+
+lemma trans_on_top[simp]: "trans_on A \<top>"
+  by (simp add: trans_on_def)
+
+lemma transp_on_top[simp]: "transp_on A \<top>"
   by (simp add: transp_on_def)
 
 lemma transp_empty [simp]: "transp (\<lambda>x y. False)"
@@ -803,6 +825,12 @@
 lemma totalpD: "totalp R \<Longrightarrow> x \<noteq> y \<Longrightarrow> R x y \<or> R y x"
   by (simp add: totalp_onD)
 
+lemma total_on_top[simp]: "total_on A \<top>"
+  by (simp add: total_on_def)
+
+lemma totalp_on_top[simp]: "totalp_on A \<top>"
+  by (simp add: totalp_on_def)
+
 lemma totalp_on_mono_stronger:
   fixes
     A :: "'a set" and R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" and
--- a/src/HOL/Tools/Function/lexicographic_order.ML	Tue Mar 18 18:11:58 2025 +0000
+++ b/src/HOL/Tools/Function/lexicographic_order.ML	Tue Mar 18 18:12:07 2025 +0000
@@ -203,7 +203,7 @@
           st |>
           (PRIMITIVE (infer_instantiate ctxt [(#1 (dest_Var rel), Thm.cterm_of ctxt relation)])
             THEN (REPEAT (resolve_tac ctxt @{thms wf_mlex} 1))
-            THEN (resolve_tac ctxt @{thms wf_empty} 1)
+            THEN (resolve_tac ctxt @{thms wf_on_bot} 1)
             THEN EVERY (map (prove_row_tac ctxt) clean_table))
         end
   end) 1 st;
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Tue Mar 18 18:11:58 2025 +0000
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Tue Mar 18 18:12:07 2025 +0000
@@ -299,7 +299,7 @@
       NONE => no_tac
     | SOME cert =>
         SELECT_GOAL (reconstruct_tac ctxt D cs gp cert) i
-        THEN TRY (resolve_tac ctxt @{thms wf_empty} i))
+        THEN TRY (resolve_tac ctxt @{thms wf_on_bot} i))
   end)
 
 fun gen_decomp_scnp_tac orders autom_tac ctxt =
@@ -314,7 +314,7 @@
 fun gen_sizechange_tac orders autom_tac ctxt =
   TRY (Function_Common.termination_rule_tac ctxt 1)
   THEN TRY (Termination.wf_union_tac ctxt)
-  THEN (resolve_tac ctxt @{thms wf_empty} 1 ORELSE gen_decomp_scnp_tac orders autom_tac ctxt 1)
+  THEN (resolve_tac ctxt @{thms wf_on_bot} 1 ORELSE gen_decomp_scnp_tac orders autom_tac ctxt 1)
 
 fun sizechange_tac ctxt autom_tac =
   gen_sizechange_tac [MAX, MS, MIN] autom_tac ctxt
--- a/src/HOL/Wellfounded.thy	Tue Mar 18 18:11:58 2025 +0000
+++ b/src/HOL/Wellfounded.thy	Tue Mar 18 18:12:07 2025 +0000
@@ -530,16 +530,14 @@
 
 text \<open>Well-foundedness of the empty relation\<close>
 
-lemma wf_empty [iff]: "wf {}"
-  by (simp add: wf_def)
+lemma wf_on_bot[iff]: "wf_on A \<bottom>"
+  by (simp add: wf_on_def)
+
+lemma wfp_on_bot[iff]: "wfp_on A \<bottom>"
+  using wf_on_bot[to_pred] .
 
 lemma wfp_empty [iff]: "wfp (\<lambda>x y. False)"
-proof -
-  have "wfp bot"
-    by (fact wf_empty[to_pred bot_empty_eq2])
-  then show ?thesis
-    by (simp add: bot_fun_def)
-qed
+  using wfp_on_bot by (simp add: bot_fun_def)
 
 lemma wf_Int1: "wf r \<Longrightarrow> wf (r \<inter> r')"
   by (erule wf_subset) (rule Int_lower1)
--- a/src/Pure/Admin/isabelle_cronjob.scala	Tue Mar 18 18:11:58 2025 +0000
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Tue Mar 18 18:12:07 2025 +0000
@@ -353,7 +353,8 @@
             " -e ISABELLE_MLTON=/usr/local/bin/mlton -e ISABELLE_MLTON_OPTIONS=" +
             " -e ISABELLE_SMLNJ=/usr/local/smlnj/bin/sml" +
             " -e ISABELLE_SWIPL=/usr/local/bin/swipl",
-          args = "-a -d '~~/src/Benchmarks'")),
+          args = "-a -d '~~/src/Benchmarks'",
+          count = () => 0)),
       List(
         Remote_Build("AFP macOS (macOS 14 Sonoma, Apple Silicon)", "studio1-sonoma", history = 120,
           history_base = "build_history_base_arm",