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-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
