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

[Manuel Eberl]

Ah, interesting. Thanks!

On 23/09/15 08:47, Andreas Lochbihler wrote:
> Dear Manuel,
> 
> consider supports the same syntax as obtains, i.e., you can use "where"
> as in
> 
>   consider "x = ∞" | "x = -∞" | y where "x = ereal y"
> 
> Andreas
> 
> On 23/09/15 08:41, Manuel Eberl wrote:
>> 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
>>>
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>
>>