# HG changeset patch
# User paulson
# Date 1742938476 0
# Node ID 00b59ba22c01ad48c4fa94cf526f9c64cded5f6d
# Parent  04b40cfcebbf4ef0bcdbcc403e5f211630e8f27a# Parent  a854ca7ca7d93056bd9f046fc00863b2bc1d6198
merged

diff -r a854ca7ca7d9 -r 00b59ba22c01 NEWS
--- a/NEWS	Tue Mar 25 21:19:26 2025 +0000
+++ b/NEWS	Tue Mar 25 21:34:36 2025 +0000
@@ -99,6 +99,13 @@
       transp_on_top[simp]
 
 * Theory "HOL.Wellfounded":
+  - Renamed lemmas. Minor INCOMPATIBILITY.
+      wf_on_antimono_stronger ~> wf_on_mono_stronger
+      wf_on_antimono_strong ~> wf_on_mono_strong
+      wf_on_antimono ~> wf_on_mono
+      wfp_on_antimono_stronger ~> wfp_on_mono_stronger
+      wfp_on_antimono_strong ~> wfp_on_mono_strong
+      wfp_on_antimono ~> wfp_on_mono
   - Removed lemmas. Minor INCOMPATIBILITY.
       wf_empty[iff] (use wf_on_bot instead)
   - Added lemmas.
diff -r a854ca7ca7d9 -r 00b59ba22c01 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Tue Mar 25 21:19:26 2025 +0000
+++ b/src/HOL/Nat.thy	Tue Mar 25 21:34:36 2025 +0000
@@ -2300,7 +2300,7 @@
 lemma strict_inc_induct [consumes 1, case_names base step]:
   assumes less: "i < j"
     and base: "\<And>i. j = Suc i \<Longrightarrow> P i"
-    and step: "\<And>i. i < j \<Longrightarrow> P (Suc i) \<Longrightarrow> P i"
+    and step: "\<And>i. Suc i < j \<Longrightarrow> P (Suc i) \<Longrightarrow> P i"
   shows "P i"
 using less proof (induct "j - i - 1" arbitrary: i)
   case (0 i)
@@ -2318,7 +2318,7 @@
   moreover from * have "j - Suc i \<noteq> 0" by auto
   then have "Suc i < j" by (simp add: not_le)
   ultimately have "P (Suc i)" by (rule Suc.hyps)
-  with \<open>i < j\<close> show "P i" by (rule step)
+  with \<open>Suc i < j\<close> show "P i" by (rule step)
 qed
 
 lemma zero_induct_lemma: "P k \<Longrightarrow> (\<And>n. P (Suc n) \<Longrightarrow> P n) \<Longrightarrow> P (k - i)"
diff -r a854ca7ca7d9 -r 00b59ba22c01 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Tue Mar 25 21:19:26 2025 +0000
+++ b/src/HOL/Presburger.thy	Tue Mar 25 21:34:36 2025 +0000
@@ -6,7 +6,6 @@
 
 theory Presburger
 imports Groebner_Basis Set_Interval
-keywords "try0" :: diag
 begin
 
 ML_file \<open>Tools/Qelim/qelim.ML\<close>
@@ -558,9 +557,4 @@
   "n mod 4 = Suc 0 \<Longrightarrow> even ((n - Suc 0) div 2)"
   by presburger
 
-
-subsection \<open>Try0\<close>
-
-ML_file \<open>Tools/try0.ML\<close>
-
 end
diff -r a854ca7ca7d9 -r 00b59ba22c01 src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Tue Mar 25 21:19:26 2025 +0000
+++ b/src/HOL/Relation.thy	Tue Mar 25 21:34:36 2025 +0000
@@ -340,10 +340,10 @@
 lemma irreflp_on_mono[mono]: "A \<subseteq> B \<Longrightarrow> R \<le> Q \<Longrightarrow> irreflp_on B Q \<le> irreflp_on A R"
   by (simp add: irreflp_on_mono_strong le_fun_def)
 
-lemma irrefl_on_subset: "irrefl_on A r \<Longrightarrow> B \<subseteq> A \<Longrightarrow> irrefl_on B r"
+lemma irrefl_on_subset: "irrefl_on B r \<Longrightarrow> A \<subseteq> B \<Longrightarrow> irrefl_on A r"
   by (auto simp: irrefl_on_def)
 
-lemma irreflp_on_subset: "irreflp_on A R \<Longrightarrow> B \<subseteq> A \<Longrightarrow> irreflp_on B R"
+lemma irreflp_on_subset: "irreflp_on B R \<Longrightarrow> A \<subseteq> B \<Longrightarrow> irreflp_on A R"
   using irreflp_on_mono_strong .
 
 lemma irreflp_on_image: "irreflp_on (f ` A) R \<longleftrightarrow> irreflp_on A (\<lambda>a b. R (f a) (f b))"
@@ -417,10 +417,10 @@
 lemma asymp_on_mono[mono]: "A \<subseteq> B \<Longrightarrow> R \<le> Q \<Longrightarrow> asymp_on B Q \<le> asymp_on A R"
   by (simp add: asymp_on_mono_strong le_fun_def)
 
-lemma asym_on_subset: "asym_on A r \<Longrightarrow> B \<subseteq> A \<Longrightarrow> asym_on B r"
+lemma asym_on_subset: "asym_on B r \<Longrightarrow> A \<subseteq> B \<Longrightarrow> asym_on A r"
   by (auto simp: asym_on_def)
 
-lemma asymp_on_subset: "asymp_on A R \<Longrightarrow> B \<subseteq> A \<Longrightarrow> asymp_on B R"
+lemma asymp_on_subset: "asymp_on B R \<Longrightarrow> A \<subseteq> B \<Longrightarrow> asymp_on A R"
   using asymp_on_mono_strong .
 
 lemma asymp_on_image: "asymp_on (f ` A) R \<longleftrightarrow> asymp_on A (\<lambda>a b. R (f a) (f b))"
@@ -512,10 +512,10 @@
 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"
+lemma sym_on_subset: "sym_on B r \<Longrightarrow> A \<subseteq> B \<Longrightarrow> sym_on A r"
   by (auto simp: sym_on_def)
 
-lemma symp_on_subset: "symp_on A R \<Longrightarrow> B \<subseteq> A \<Longrightarrow> symp_on B R"
+lemma symp_on_subset: "symp_on B R \<Longrightarrow> A \<subseteq> B \<Longrightarrow> symp_on A R"
   by (auto simp: symp_on_def)
 
 lemma symp_on_image: "symp_on (f ` A) R \<longleftrightarrow> symp_on A (\<lambda>a b. R (f a) (f b))"
@@ -644,10 +644,10 @@
 lemma antisymp_on_mono[mono]: "A \<subseteq> B \<Longrightarrow> R \<le> Q \<Longrightarrow> antisymp_on B Q \<le> antisymp_on A R"
   by (simp add: antisymp_on_mono_strong le_fun_def)
 
-lemma antisym_on_subset: "antisym_on A r \<Longrightarrow> B \<subseteq> A \<Longrightarrow> antisym_on B r"
+lemma antisym_on_subset: "antisym_on B r \<Longrightarrow> A \<subseteq> B \<Longrightarrow> antisym_on A r"
   by (auto simp: antisym_on_def)
 
-lemma antisymp_on_subset: "antisymp_on A R \<Longrightarrow> B \<subseteq> A \<Longrightarrow> antisymp_on B R"
+lemma antisymp_on_subset: "antisymp_on B R \<Longrightarrow> A \<subseteq> B \<Longrightarrow> antisymp_on A R"
   using antisymp_on_mono_strong .
 
 lemma antisymp_on_image:
@@ -756,10 +756,10 @@
 lemma transpD[dest?]: "transp R \<Longrightarrow> R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
   by (rule transD[to_pred])
 
-lemma trans_on_subset: "trans_on A r \<Longrightarrow> B \<subseteq> A \<Longrightarrow> trans_on B r"
+lemma trans_on_subset: "trans_on B r \<Longrightarrow> A \<subseteq> B \<Longrightarrow> trans_on A r"
   by (auto simp: trans_on_def)
 
-lemma transp_on_subset: "transp_on A R \<Longrightarrow> B \<subseteq> A \<Longrightarrow> transp_on B R"
+lemma transp_on_subset: "transp_on B R \<Longrightarrow> A \<subseteq> B \<Longrightarrow> transp_on A R"
   by (auto simp: transp_on_def)
 
 lemma transp_on_image: "transp_on (f ` A) R \<longleftrightarrow> transp_on A (\<lambda>a b. R (f a) (f b))"
@@ -922,10 +922,10 @@
 lemma totalp_on_mono[mono]: "A \<subseteq> B \<Longrightarrow> Q \<le> R \<Longrightarrow> totalp_on B Q \<le> totalp_on A R"
   by (auto intro: totalp_on_mono_strong)
 
-lemma total_on_subset: "total_on A r \<Longrightarrow> B \<subseteq> A \<Longrightarrow> total_on B r"
+lemma total_on_subset: "total_on B r \<Longrightarrow> A \<subseteq> B \<Longrightarrow> total_on A r"
   by (auto simp: total_on_def)
 
-lemma totalp_on_subset: "totalp_on A R \<Longrightarrow> B \<subseteq> A \<Longrightarrow> totalp_on B R"
+lemma totalp_on_subset: "totalp_on B R \<Longrightarrow> A \<subseteq> B \<Longrightarrow> totalp_on A R"
   using totalp_on_mono_strong .
 
 lemma totalp_on_image:
diff -r a854ca7ca7d9 -r 00b59ba22c01 src/HOL/Sledgehammer.thy
--- a/src/HOL/Sledgehammer.thy	Tue Mar 25 21:19:26 2025 +0000
+++ b/src/HOL/Sledgehammer.thy	Tue Mar 25 21:34:36 2025 +0000
@@ -7,7 +7,7 @@
 section \<open>Sledgehammer: Isabelle--ATP Linkup\<close>
 
 theory Sledgehammer
-imports Presburger SMT
+imports Presburger SMT Try0
 keywords
   "sledgehammer" :: diag and
   "sledgehammer_params" :: thy_decl
diff -r a854ca7ca7d9 -r 00b59ba22c01 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Mar 25 21:19:26 2025 +0000
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Mar 25 21:34:36 2025 +0000
@@ -1935,8 +1935,7 @@
            map_filter (try (specialize_helper t)) types
          else
            [t])
-        |> tag_list 1
-        |> map (fn (k, t) => ((dub needs_sound j k, (Global, status)), t))
+        |> map_index (fn (k, t) => ((dub needs_sound j (k + 1), (Global, status)), t))
       fun make_facts type_enc = map_filter (make_fact ctxt format type_enc false)
       val sound = is_type_enc_sound type_enc
       val could_specialize = could_specialize_helpers type_enc
diff -r a854ca7ca7d9 -r 00b59ba22c01 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Mar 25 21:19:26 2025 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Mar 25 21:34:36 2025 +0000
@@ -175,8 +175,8 @@
         ()
 
     fun print_used_facts used_facts used_from =
-      tag_list 1 used_from
-      |> map (fn (j, fact) => fact |> apsnd (K j))
+      used_from
+      |> map_index (fn (j, fact) => fact |> apsnd (K (j + 1)))
       |> filter_used_facts false used_facts
       |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
       |> commas
@@ -188,8 +188,8 @@
           val num_used_facts = length used_facts
 
           fun find_indices facts =
-            tag_list 1 facts
-            |> map (fn (j, fact) => fact |> apsnd (K j))
+            facts
+            |> map_index (fn (j, fact) => fact |> apsnd (K (j + 1)))
             |> filter_used_facts false used_facts
             |> distinct (eq_fst (op =))
             |> map (prefix "@" o string_of_int o snd)
diff -r a854ca7ca7d9 -r 00b59ba22c01 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Mar 25 21:19:26 2025 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Mar 25 21:34:36 2025 +0000
@@ -370,10 +370,10 @@
   end
 
 fun fact_distinct eq facts =
-  fold (fn (i, fact as (_, th)) =>
+  fold_index (fn (i, fact as (_, th)) =>
       Net.insert_term_safe (eq o apply2 (normalize_eq o Thm.prop_of o snd o snd))
         (normalize_eq (Thm.prop_of th), (i, fact)))
-    (tag_list 0 facts) Net.empty
+    facts Net.empty
   |> Net.entries
   |> sort (int_ord o apply2 fst)
   |> map snd
@@ -452,6 +452,13 @@
       not (member (op aconv) named_locals (normalize_eq (Thm.prop_of th)))
   end
 
+local
+
+type lazy_facts =
+  {singletons : lazy_fact list , dotteds : lazy_fact list, collections : lazy_fact list}
+
+in
+
 fun all_facts ctxt generous keywords add_ths chained css =
   let
     val thy = Proof_Context.theory_of ctxt
@@ -470,7 +477,7 @@
 
     val full_space = Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
 
-    fun add_facts global foldx facts =
+    fun add_facts global foldx facts : 'a -> lazy_facts -> lazy_facts =
       foldx (fn (name0, ths) => fn accum =>
         if name0 <> "" andalso
            (Long_Name.is_hidden (Facts.intern facts name0) orelse
@@ -489,7 +496,7 @@
                 NONE => false
               | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths'))
           in
-            snd (fold_rev (fn th0 => fn (j, accum) =>
+            snd (fold_rev (fn th0 => fn (j, accum as {singletons, dotteds, collections} : lazy_facts) =>
               let val th = transfer th0 in
                 (j - 1,
                  if not (member Thm.eq_thm_prop add_ths th) andalso
@@ -517,21 +524,27 @@
                      val stature = stature_of_thm global assms chained css name0 th
                      val new = ((get_name, stature), th)
                    in
-                     (if collection then apsnd o apsnd
-                      else if dotted_name then apsnd o apfst
-                      else apfst) (cons new) accum
+                     if collection then
+                       {singletons = singletons, dotteds = dotteds, collections = new :: collections}
+                      else if dotted_name then
+                       {singletons = singletons, dotteds = new :: dotteds, collections = collections}
+                      else
+                       {singletons = new :: singletons, dotteds = dotteds, collections = collections}
                    end)
               end) ths (n, accum))
           end)
+      val {singletons, dotteds, collections} =
+        {singletons = [], dotteds = [], collections = []}
+        |> add_facts false fold local_facts (unnamed_locals @ named_locals)
+        |> add_facts true Facts.fold_static global_facts global_facts
   in
     (* Names like "xxx" are preferred to "xxx.yyy", which are preferred to "xxx(666)" and the like.
        "Preferred" means "put to the front of the list". *)
-    ([], ([], []))
-    |> add_facts false fold local_facts (unnamed_locals @ named_locals)
-    |> add_facts true Facts.fold_static global_facts global_facts
-    ||> op @ |> op @
+    singletons @ dotteds @ collections
   end
 
+end
+
 fun nearly_all_facts ctxt inst_inducts {add, del, only} keywords css chained hyp_ts concl_t =
   if only andalso null add then
     []
diff -r a854ca7ca7d9 -r 00b59ba22c01 src/HOL/Try0.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Try0.thy	Tue Mar 25 21:34:36 2025 +0000
@@ -0,0 +1,14 @@
+(* Title:      HOL/Try0.thy
+   Author:     Jasmin Blanchette, LMU Muenchen
+   Author:     Martin Desharnais, LMU Muenchen
+   Author:     Fabian Huch, TU Muenchen
+*)
+
+theory Try0
+  imports Presburger
+  keywords "try0" :: diag
+begin
+
+ML_file \<open>Tools/try0.ML\<close>
+
+end
\ No newline at end of file
diff -r a854ca7ca7d9 -r 00b59ba22c01 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Tue Mar 25 21:19:26 2025 +0000
+++ b/src/HOL/Wellfounded.thy	Tue Mar 25 21:34:36 2025 +0000
@@ -337,7 +337,7 @@
 subsubsection \<open>Antimonotonicity\<close>
 
 
-lemma wfp_on_antimono_stronger:
+lemma wfp_on_mono_stronger:
   fixes
     A :: "'a set" and B :: "'b set" and
     f :: "'a \<Rightarrow> 'b" and
@@ -363,34 +363,34 @@
     using \<open>A' \<subseteq> A\<close> mono by blast
 qed
 
-lemma wf_on_antimono_stronger:
+lemma wf_on_mono_stronger:
   assumes
     "wf_on B r" and
     "f ` A \<subseteq> B" and
     "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> (x, y) \<in> q \<Longrightarrow> (f x, f y) \<in> r)"
   shows "wf_on A q"
-  using assms wfp_on_antimono_stronger[to_set, of B r f A q] by blast
+  using assms wfp_on_mono_stronger[to_set, of B r f A q] by blast
 
-lemma wf_on_antimono_strong:
+lemma wf_on_mono_strong:
   assumes "wf_on B r" and "A \<subseteq> B" and "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> (x, y) \<in> q \<Longrightarrow> (x, y) \<in> r)"
   shows "wf_on A q"
-  using assms wf_on_antimono_stronger[of B r "\<lambda>x. x" A q] by blast
+  using assms wf_on_mono_stronger[of B r "\<lambda>x. x" A q] by blast
 
-lemma wfp_on_antimono_strong:
+lemma wfp_on_mono_strong:
   "wfp_on B R \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> Q x y \<Longrightarrow> R x y) \<Longrightarrow> wfp_on A Q"
-  using wf_on_antimono_strong[of B _ A, to_pred] .
+  using wf_on_mono_strong[of B _ A, to_pred] .
 
-lemma wf_on_antimono: "A \<subseteq> B \<Longrightarrow> q \<subseteq> r \<Longrightarrow> wf_on B r \<le> wf_on A q"
-  using wf_on_antimono_strong[of B r A q] by auto
+lemma wf_on_mono: "A \<subseteq> B \<Longrightarrow> q \<subseteq> r \<Longrightarrow> wf_on B r \<le> wf_on A q"
+  using wf_on_mono_strong[of B r A q] by auto
 
-lemma wfp_on_antimono: "A \<subseteq> B \<Longrightarrow> Q \<le> R \<Longrightarrow> wfp_on B R \<le> wfp_on A Q"
-  using wfp_on_antimono_strong[of B R A Q] by auto
+lemma wfp_on_mono: "A \<subseteq> B \<Longrightarrow> Q \<le> R \<Longrightarrow> wfp_on B R \<le> wfp_on A Q"
+  using wfp_on_mono_strong[of B R A Q] by auto
 
 lemma wf_on_subset: "wf_on B r \<Longrightarrow> A \<subseteq> B \<Longrightarrow> wf_on A r"
-  using wf_on_antimono_strong .
+  using wf_on_mono_strong .
 
 lemma wfp_on_subset: "wfp_on B R \<Longrightarrow> A \<subseteq> B \<Longrightarrow> wfp_on A R"
-  using wfp_on_antimono_strong .
+  using wfp_on_mono_strong .
 
 
 subsubsection \<open>Equivalence between \<^const>\<open>wfp_on\<close> and \<^const>\<open>wfp\<close>\<close>
@@ -405,7 +405,7 @@
 next
   assume ?RHS
   thus ?LHS
-  proof (rule wfp_on_antimono_strong)
+  proof (rule wfp_on_mono_strong)
     show "A \<subseteq> UNIV"
       using subset_UNIV .
   next
@@ -524,7 +524,7 @@
 text \<open>Well-foundedness of subsets\<close>
 
 lemma wf_subset: "wf r \<Longrightarrow> p \<subseteq> r \<Longrightarrow> wf p"
-  using wf_on_antimono[OF subset_UNIV, unfolded le_bool_def] ..
+  using wf_on_mono[OF subset_UNIV, unfolded le_bool_def] ..
 
 lemmas wfp_subset = wf_subset [to_pred]