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 MHonArc.