Re: [isabelle] SOME simplification
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
not depend on e.
Yes, probably the problem is here!
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.
Ok, thank you very much for your help.
This archive was generated by a fusion of
Pipermail (Mailman edition) and