Email Gateway (Aug 22 2022 at 17:02): Email Gateway (Aug 22 2022 at 17:02):From: Bertram Felgenhauer via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi,
I'm playing with the automatic refinement framework, trying to obtain
partially correct code. To this end, I found it convenient to assume
(not assert) that a certain set is finite. As an artificial example,
definition
"assume_test X ≡ do { ASSUME (finite X); RETURN X }"
Next, I want to do a data refinement from sets to lists. This implies
that the finiteness assumption is always satisfied:
lemma [simp]:
"(X', X) ∈ ⟨Id⟩list_set_rel ⟹ finite X"
by (auto simp: list_set_rel_def br_def)
That in turns means that the assumption can be omitted in the refined
implementation:
lemma assume_test_refine:
assumes "(X', X) ∈ ⟨Id⟩list_set_rel"
shows "(RETURN X', assume_test X) ∈ ⟨⟨Id⟩list_set_rel⟩nres_rel"
using assms
unfolding nres_rel_def assume_test_def
by (auto simp: assume_test_def)
My question, now, is whether this can be automated, which would allow
this idea to be applied in the middle of a larger refinement that is
otherwise automatic. I tried this:
schematic_goal assume_test_refine:
assumes [autoref_rules]: "(X', X) ∈ ⟨Id⟩list_set_rel"
shows "(?f, assume_test X) ∈ ⟨⟨Id⟩list_set_rel⟩nres_rel"
unfolding assume_test_def
using [[autoref_trace_failed_id]]
apply (autoref (keep_goal))
(* some goal involving op_nres_ASSUME_bnd remains *)
oops
Can this work? I suspect that it is a matter of adding a suitable rule
to [autoref_rules], but my two attempts (see the attached theory) failed.
Cheers,
Bertram
Scratch.thy
Email Gateway (Aug 22 2022 at 17:05):From: Peter Lammich <lammich@in.tum.de>
Hi Bertram,
find attached my commented debugging session that shows how to find and
fix the problem.
In short: When trying to show "finite X", Autoref knows nothing about
the refinement of X to X', and you have to manually add this fact to
the simpset.
I have never used assumptions too much, I only added them because they
are the natural dual to assertions. Thus, I don't have too much
experience where they are actually useful. What is your actual
example?
Scratch1.thy
Last updated: Apr 20 2024 at 04:19 UTC