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

[Andreas Lochbihler]

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
>