[isabelle-dev] NEWS: 'consider' command and "cases" method
Manuel Eberl
eberlm at in.tum.de
Wed Sep 23 13:28:33 CEST 2015
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
>>
>>
More information about the isabelle-dev
mailing list