# 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.*