Re: [isabelle-dev] NEWS: 'consider' command and "cases" method
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 >>>then have something >>>proof cases >>> case a >>> then show ?thesis >>>next >>> case b >>> then show ?thesis >>>next >>> case c >>> then show ?thesis >>>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
Re: [isabelle-dev] NEWS: 'consider' command and "cases" method
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 then have something proof cases case a then show ?thesis next case b then show ?thesis next case c then show ?thesis 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
[isabelle-dev] NEWS: 'consider' command and cases method
* 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
