Email Gateway (Jul 21 2025 at 15:46): Email Gateway (Jul 21 2025 at 15:46):From: Makarius <makarius@sketis.net>
* General *
This refers to Isabelle/372273ab6ebb and AFP/eae86974a665.
That is the notable point, where all Isabelle + AFP applications essentially
work unchanged. Intermediately, in my desparation to get it done, I had
adjusted a few odd proofs. See this already backed-out changeset:
changeset: 15842:d06954e7388a
user: wenzelm
date: Sun Jul 13 04:21:58 2025 +0200
files: thys/Buchi_Complementation/Complementation_Implement.thy
thys/Tree_Enumeration/Rooted_Tree.thy
description:
adapted proofs to Isabelle/df2d774bcf21: spurious failures due to unclear reasons;
diff -r ba30fe0ad97c -r d06954e7388a
thys/Buchi_Complementation/Complementation_Implement.thy
--- a/thys/Buchi_Complementation/Complementation_Implement.thy Fri Jul 11
15:02:29 2025 +0200
+++ b/thys/Buchi_Complementation/Complementation_Implement.thy Sun Jul 13
04:21:58 2025 +0200
@@ -597,7 +597,9 @@
fix a f g
assume "g \<in> expand_map (get_4 A (bounds_3 A a (refresh_1 f)))"
then show "g \<in> expand_map (get_3 A (bounds_3 A a (refresh_1 f)))"
unfolding get_4_def get_3_def items_4_def items_3_def
expand_map_alt_def by blast
unfolding get_4_def get_3_def items_4_def items_3_def
expand_map_alt_def mem_Collect_eq
supply not_None_eq [iff del] by blast
+
qed
lemma complement_4_language_2: "language (complement_4 A) \<subseteq>
language (complement_3 A)"
using language_mono complement_4_less by (auto dest: monoD)
diff -r ba30fe0ad97c -r d06954e7388a thys/Tree_Enumeration/Rooted_Tree.thy
--- a/thys/Tree_Enumeration/Rooted_Tree.thy Fri Jul 11 15:02:29 2025 +0200
+++ b/thys/Tree_Enumeration/Rooted_Tree.thy Sun Jul 13 04:21:58 2025 +0200
@@ -554,7 +554,7 @@
abbreviation "ltree_stree_subtrees ts \<equiv> SOME xs. fset_of_list xs =
ltree_stree |`| ts \<and> distinct xs \<and> sorted_wrt (\<lambda>t s.
tree_ltree t \<le> tree_ltree s) xs"
lemma fset_of_list_ltree_stree_subtrees[simp]: "fset_of_list
(ltree_stree_subtrees ts) = ltree_stree |`| ts"
using someI_ex[OF distinct_sorted_wrt_list] by fast
using someI_ex[OF distinct_sorted_wrt_list] by force
lemma set_ltree_stree_subtrees[simp]: "set (ltree_stree_subtrees ts) =
ltree_stree ` fset ts"
using fset_of_list_ltree_stree_subtrees by (metis (mono_tags, lifting)
fset.set_map fset_of_list.rep_eq)
A bit later, the hidden failure of smt proof reconstruction prompted me to
revisit the whole affair once again, comparing netpair content more carefully,
and reconstructing/eliminating reasons for remaining deviations.
Some of these oddities had been around for approx. 30 years: Delicate
diversions from the intention written as prose comments wrt. the actual
implementation in ML. I made the mistake to take the prose text more seriously
than the formal ML text. Ultimately, real-world applications found in AFP
determine what is right or wrong, and don't care about good intentions written
as comments.
Here are some notable points in history, together with my present
interpretation of the archeological findings. This is going back to the depths
of time, when Isabelle was still an odd research experiment.
That is an early attempt to make things scale better. That version is notable
to assign integer "tags" for sorting rules according to the following
calculation of the length of intro vs. elim rules:
fun insert (nI,nE) = insert_tagged_list o (tag_brls (~(2*nI+nE))) o joinrules;
Still a bit inefficient (based on list length) and not quite correct, as
explained below.
Here the comment says:
(*Merge works by adding all new rules of the 2nd claset into the 1st claset.
Merging the term nets may look more efficient, but the rather delicate
treatment of priority might get muddled up.*)
But the ML source says something different: It effectively orders all
declarations from the RHS of the merge according to their "rule kind" (using
current terminology). That is no problem for disjoint netpairs, but within a
single netpair, newly introduced elim rules now take precedence over intro rules.
That odd ordering from 1996 made smt reconstruction fail now, because I
reimplemented the prose specification instead of the actual ML story.
Further note that we still see quadratic complexity for the merge, because it
is based on plain lists (which implicitly retains the order of declarations).
That was my attempt to address the complexity of extending/merging claset rule
declarations, but not a fully successful one. Its use of Item_Net.T instead of
a plain list was fine, because that is a scalable data structure with n*log(n)
complexity instead of n^2. My oversight in 2011 was the remaining linear
operation Item_Net.length to imitate the allocation of a "fresh" declaration
index for each rule.
Approx. 2 weeks ago, I realized the core problem of inefficiency of the
claset, only after cleaning up the sources and saying clearly in ML what
really happens, instead of trusting odd comments. Apart from inefficiency of
length-based allocation of a "fresh" index, it was also wrong due to the
presence of "rule del" declarations: thus an old index could have been reused
later on --- it is not really fresh. Luckily, the more correct implementation
in this changeset did not affect any applications in Isabelle + AFP. So
ca600cbfd4bf remained the "stable status-quo" in subsequent struggles to
finish this renovation project.
This is where I switched over to a quite different background store for the
claset rules, with subtle differences in ordering of declarations (and a few
other problems that I introduced on the spot). The idea is plain and simple:
all rules are maintained in one scalable data structure Bires.decls, and the
netpairs derived from it can count on precise weight and index information for
the ordering. The reality turned out rather ugly, though: applications from
AFP that did not quite work yet.
All these problems are resolved in Isabelle/372273ab6ebb and AFP/eae86974a665,
as far as I can tell. It recovers all visible applications, without odd
changes of proofs.
We could still be a bit more ambitious, though, and eliminate the strange
Bires.decl_merge_ord that is there to imitate the merge ordering from 30 years
ago. Changing that would mean to take the user-provided declaration order
seriously, even for newly added rules in a merge.
That further detail would require to go into the smt proof reconstruction, to
see where its invocations of fast_tac/blast_tac/auto_tac etc. actually fail,
or rather consume much more time than before --- and thus break (line 6705 of
"$AFP/Modular_arithmetic_LLL_and_HNF_algorithms/HNF_Mod_Det_Soundness.thy"),
for example.
Makarius
Email Gateway (Jul 24 2025 at 14:26):From: Florian Haftmann <florian.haftmann@cit.tum.de>
Just a side-remark:
That further detail would require to go into the smt proof
reconstruction, to see where its invocations of fast_tac/blast_tac/
auto_tac etc. actually fail, or rather consume much more time than
before --- and thus break (line 6705 of "$AFP/
Modular_arithmetic_LLL_and_HNF_algorithms/HNF_Mod_Det_Soundness.thy"),
for example.
I also stumbled over that proof and it can be dramatically simplified:
- have "A (0, 0)"
- by (smt (verit) add_gr_0 append_rows_def A_def A'' carrier_matD index_mat_four_block(1) mn n0 nat_SN.compat)
- from \<open>0 < n\<close> \<open>0 < m\<close> A'' have \<open>A (0, 0)\<close>
- by (simp add: A_def append_rows_def)
I will leave it »as it is« for the moment as long as it serves as an
important indicator for smt proof reconstruction.
Florian
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Email Gateway (Jul 26 2025 at 15:11):From: Makarius <makarius@sketis.net>
On 21/07/2025 17:45, Makarius wrote:
* General *
- Declarations of intro/elim/dest rules for Pure and the Classical
Reasoner (e.g. HOL) are handled more uniformly and efficiently: the
order of rule declarations is maintained accurately, regardless of
intermediate [rule del] declarations. Furthermore, [dest] is now a
proper declaration on its own account, instead of the former expansion
[elim_format, elim]. Consequently, [rule del] no longer deletes the
[elim_format] of the given rule, only the original rule. Very rare
INCOMPATIBILITY: tools like "blast" and "auto" may fail in unusual
situations.This refers to Isabelle/372273ab6ebb and AFP/eae86974a665.
After a few days of accumulating Isabelle + AFP "flight telemetry data", I
have inspected
https://isatest.sketis.net/devel/build_status/AFP_macOS_(macOS_14_Sonoma_Apple_Silicon)/index.html
closely, if anything good or bad is to be seen there.
Conclusion: this change has now overall measurable effect on Isabelle/AFP,
despite significant lack of scalability.
I found other performance changes elsewhere, and will report them separately.
Makarius
Last updated: Aug 31 2025 at 20:21 UTC