Is there a way to use ‘consider’ with fixed variables?
E.g. if I have a rule like ereal_cases:
(⋀r. x = ereal r ⟹ thesis) ⟹
(x = ∞ ⟹ thesis) ⟹
(x = - ∞ ⟹ thesis) ⟹ thesis
I would like to write
consider "x = ∞" | "x = -∞" | "x = ereal x'" for x'
But that syntax is not supported. Is there another way except the rather
clumsy
consider "x = ∞" | "x = -∞" | "∃x'. x = ereal x'"
?
Cheers,
Manuel
On 15/06/15 00:11, Makarius wrote:
> * New command 'consider' states rules for generalized elimination and
> case splitting. This is like a toplevel statement "theorem obtains" used
> within a proof body; or like a multi-branch 'obtain' without activation
> of the local context elements yet.
>
> * Proof method "cases" allows to specify the rule as first entry of
> chained facts. This is particularly useful with 'consider':
>
> consider (a) A | (b) B | (c) C <proof>
> then have something
> proof cases
> case a
> then show ?thesis <proof>
> next
> case b
> then show ?thesis <proof>
> next
> case c
> then show ?thesis <proof>
> qed
>
>
> This refers e.g. to Isabelle/051b200f7578. Some examples are in
> ~~/src/HOL/Isar_Examples/Structured_Statements.thy
>
> It may be seen as an answer to the open problem of section 5.5.3
> "Generalized case-splitting" from my Ph.D. thesis. There is no need to
> support non-linear proof processing in the Isar/VM: 'consider' merely
> states and proves the rule, and the "cases" method does the splitting in
> a normal backwards proof (with case names).
>
> This means that awkward use of raw proof blocks with "big-bang
> integration" by blast is no longer required. General case-splitting can
> now be written explicitly and robustly.
>
>
> Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
