Email Gateway (Aug 18 2022 at 16:30): Email Gateway (Aug 18 2022 at 16:30):From: Nils Jähnig <jaehnig@mi.fu-berlin.de>
Hello Norbert,
We recently asked a question about state spaces on the mailing list
that you kindly answered, but still questions arise :-)
We are working on a formalization of a low-level language with a proof
calculus in Isabelle/HOL. So far this formalization was defined
concrete, i.e. the operational semantics were defined as inductive
function of type "record => instruction => record => bool". Currently
it is our goal to make the formalization more abstract, i.e. as an
abstract base function " 's => instruction =>' s => bool" and to
define the concrete semantics of a command (e.g. "s (add VX VY VZ) t")
by reducing to the abstract definition (rather like in Simpl, e.g. "s
(Basic f) t"). We still want to use statespace construct.
The problem we're facing now is how we can quantify over variables
within a specific statespace environment (e.g. statespace st = VX::nat
VY::nat VZ::nat) . For example, if we want to show the lemma (in st)
"Opsem s (add VX VY VZ) t", we want to reduce the semantics of add to
the general rule that represents the relationship between the states s
and t (the equivalent of [ta = sb + sc ] ==> Opsem s (add a b c) t).
As variables in statespace are distinguished according to their
abstract names, we could not come up with a solution. It seems as if
this happens in Simpl in the ML code. do we have to learn ML to do
this?
For ideas or suggestions where we might find this a starting point, we
would be very grateful.
Thank you and best regards,
Nils and Björn
Email Gateway (Aug 18 2022 at 16:30):From: Norbert Schirmer <schirmer@in.tum.de>
Hi Nils and Björn,
well it depends. The art of HOL style theorem proving is a lot about choice. And this is especially true for Isabelle / HOL. There are a lot of choices:
And which choice to take depends on what you want to achieve with your theory. Is it biased towards meta-theory of a language or is it creating a tool to prove properties about a concrete program in that language.
To be more concrete in your example what do you want to prove about "add VX VY VZ" and how do you want to further use the result within the theorem prover? Do you want to use the result at all, or is this already the final result?
For example in your case you could aim at:
(1) "forall sates s where I have three distinct variables vx, vy, vz, then in state t we have vz t = vx t + vy t ..."
(2) symbolic evaluation of a concrete program which happens to have those three variables among others, and continue 'calculation' to prove something about the outcome in the end
The good thing about using locales and statespaces here in particular is that you can get both:
You prove the concrete (in an abstract context -- the statespace) and Isabelle gives you the generalized version for free.
While being inside of the statespace / locale you just have those 3 distinct fixed variables with the 'obvious' properties and can easily prove or symbolically evaluate your programs.
But under the hood you also get a generalized version of the theorem which you can use outside of the statespace / locale.
This theorem basically states:
For all states which have at least 3 distinct variables say vx, vy,vz we have ...
So in theory this is all you need. The question is how handy these theorems are for you to use in practice for your further theory development. Maybe the locale / statespace infrastructure already provides the tools you need (e.g. merging locales). But maybe there are obvious extensions that you (and probably others) would like to have. Thats where you should start using ML and try to develop the tools that other will enjoy to use.
I suggest to start with the locale documentation, understanding the difference of being 'inside the locale' and outside. Look at the theorems that are generated after proving a lemma, the internal variant and the generalized variant. Think about how you could use those theorems.
Hope this helps,
Norbert
Last updated: Apr 24 2024 at 04:17 UTC