Email Gateway (Aug 19 2022 at 09:10): Email Gateway (Aug 19 2022 at 09:10):From: Christoph LANGE <c.lange@cs.bham.ac.uk>
2012-11-22 15:59 Christoph LANGE:
Here is another surprise I forgot to mention. If you or anyone else
feel like it, please have a look into the attached file, from which I
removed everything else. (Note that the server where I put our whole
formalisation will be offline until tomorrow morning.)
In the last case of the case distinction, I would like to infer the fact
I call pred_is_component. I need this to continue with the proof.
Now I have been unable to infer pred_is_component directly. But I made
it work with a detour via in_range. (So, don't worry, my proof works –
it's just not _nice_.)
And when I define in_range as "i : {1..n}" instead "1 <= i /\ i <= n",
even that doesn't work.
Cheers,
Christoph
in_range.thy
Last updated: Apr 24 2024 at 04:17 UTC