Email Gateway (Aug 22 2022 at 16:04): Email Gateway (Aug 22 2022 at 16:04):From: Mark Wassell <mpwassell@gmail.com>
Hello,
I am having a problem invoking code_pred on an inductive predicate that is
ultimately defined in a locale that has an assumption.
I am following the steps outlined in a previous post on this [1] but my
locale has an assumption so I don't know if defining this is at all
possible.
Cheers
Mark
[1]
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2017-January/msg00064.html
locale mylocale =
fixes P :: "'a set ⇒ bool"
assumes "P {}"
begin
inductive test :: "'a ⇒ 'a ⇒ bool" where
"P {a,b} ⟹ test a b" (*|
"test a b ⟹ P {a,b,c} ⟹ test a c" *)
end
definition "foo P = mylocale.test P"
lemma [code_pred_intro]:
"mylocale P ⟹ P {a,b} ⟹ foo P a b"
unfolding foo_def using mylocale.test.intros by metis
code_pred foo unfolding foo_def
proof -
assume a1: "mylocale.test x xa xb" and "(⋀P a b. x = P ⟹ xa = a ⟹ xb = b
⟹ mylocale P ⟹ P {a, b} ⟹ thesis)"
show thesis using mylocale.test.cases[of x xa xb thesis,OF _ a1] (* Seem
to have the right bits, in particular 'mylocale P', but in the wrong
'order' *)
oops
Email Gateway (Aug 22 2022 at 16:05):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Mark,
This is not going to work in this way. In principle, if you could phrase the locale
assumptions as an executable test, then it would work, but every call to the inductive
predicate would re-evaluate this test, and this can get pretty computationally expensive
if you have a recursive inductive predicate.
What I would recommend is that you only make it executable for interpretations that have
discharged the assumptions. For example:
locale mylocale =
fixes P :: "'a set ⇒ bool"
assumes "P {}"
begin
inductive test :: "'a ⇒ 'a ⇒ bool" where
"P {a,b} ⟹ test a b" (*|
"test a b ⟹ P {a,b,c} ⟹ test a c" *)
end
consts P :: "nat set ⇒ bool"
global_interpretation foo: mylocale P
defines foo_test = "foo.test"
sorry
declare foo.test.intros [code_pred_intro]
code_pred foo_test by(rule foo.test.cases)
This works if there are only a few interpretations of your locale. If you have many of
them, it might be useful to restructure your locale hierarchy such that you can move the
definition to a place without assumptions. (In all my years of using Isabelle, I've never
seen an inductive definition for which you needed a locale assumption to prove its
consistency, i.e., monotonicity of the associated functional.)
Andreas
Last updated: Apr 19 2024 at 16:20 UTC