Re: [isabelle] SOME simplification

Gabriele,

On Wednesday 20 December 2006 15:48, Gabriele Pozzani wrote:
> Hello everybody,
> in IOA logic I want to demonstrate:
> a: "prob((%e. (L (SOME i. (L i e)) e)) ~> Q, q)"
>  knowing:
> g: "FORALL i::nat. prob (%e. (L i e) ~> Q,  q)"
>  where "~>" is the Leadsto operator of TLS, the temporal logic of step
> developed in Muller's PhD thesis.
> L and Q are predicates of type " 'a Seq => bool ", while prob is a function
> of type " ('a Seq => bool) x fraction => bool ".
>
> Knowing from "g" that the result is true for every natural number I'm not
> able to demonstrate "a", but I think it's correct because "(SOME i. (L i
> e))" is just a particular natural number.
> I tried using spec theorem but it don't work.

I'm not familiar with the IOA theory, but it seems the problem is that

"SOME i. L i e"

is a particular natural number only after e has been fixed.  In your
assumption g however, i is quantified at the outermost level, and hence may
not depend on e.

One possible solution is to modify your assumption g:

g': "ALL (i'::('a Seq => bool)=>nat). prob (%e. (L (i' e) e) ~> Q,  q)"

Now you can instantiate i' in g' with "%e. SOME i. L i e" to show a.

Best,
Tjark

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