[isabelle-dev] NEWS: 'consider' command and "cases" method

[Manuel Eberl]

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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev