Re: [isabelle] statespace again

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: 
 * shallow vs. deep embedding,
 * abstract (e.g. using locales) vs. concrete definitions (e.g. using records)
 * an general theorem vs. solving instances on the fly in ML.

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,


On 19.11.2010, at 16:14, Nils Jähnig wrote:

> 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

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.