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

Manuel Eberl eberlm at in.tum.de
Wed Sep 23 08:41:10 CEST 2015

```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
```