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-...@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