--- 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.
--- 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)"
--- 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
--- 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:
--- 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
--- 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
--- 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)
--- 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
[]
--- /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
--- 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]