Re: [isabelle-dev] NEWS: clarified 'case' command
On Wed, 24 Jun 2015, Makarius wrote: After seeing too many "case 1", "case 2", "case 3" and corresponding facts "1", "2", "3" I've now pushed this trivial change through, really with rare incompatibilities. Here is an example changeset that illustrates the reduction of odd digits and redundancy in the source, for better proof mainainability: http://isabelle.in.tum.de/repos/isabelle/rev/19c277ea65ae I had already adapted these theories from HOL-Library and HOL-Decision_Procs earlier, to make use of 'consider' and statements with 'if' / 'for'. Thus raw proof blocks with big-bang integration by blast are mostly eliminated, and replaced by explicit proof structure. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] NEWS: clarified 'case' command
* Command 'case' allows fact name and attribute specification like this: case a: (c xs) case a [attributes]: (c xs) Facts that are introduced by invoking the case context are uniformly qualified by "a"; the same name is used for the cumulative fact. The old form "case (c xs) [attributes]" is no longer supported. Rare INCOMPATIBILITY, need to adapt uses of case facts in exotic situations, and always put attributes in front. This refers to Isabelle/b7ee41f72add. The inability to name the case facts was just a very old omission that never got beyond a certain critical mass of pain to do something about it. After seeing too many "case 1", "case 2", "case 3" and corresponding facts "1", "2", "3" I've now pushed this trivial change through, really with rare incompatibilities. (See also AFP/16e7d42ef7f4.) Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: structured Isar goal statements (update)
* Local goals ('have', 'show', 'hence', 'thus') allow structured
statements like fixes/assumes/shows in theorem specifications, but the
notation is postfix with keywords 'if' (or 'when') and 'for'. For
example:
have result: "C x y"
if "A x" and "B y"
for x :: 'a and y :: 'a
The local assumptions are bound to the name "that". The result is
exported from context of the statement as usual. The above roughly
corresponds to a raw proof block like this:
{
fix x :: 'a and y :: 'a
assume that: "A x" "B y"
have "C x y"
}
note result = this
The keyword 'when' may be used instead of 'if', to indicate 'presume'
instead of 'assume' above.
This refers to Isabelle/51a6997b1384.
The 'presume' element is rarely used, and the 'when' eigen-context is
mainly an exercise in orthogonality of the language. There might be useful
applications nonetheless, e.g. see the examples about "suffices-to-show"
in ~~/src/HOL/Isar_Examples/Structured_Statements.thy
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] NEWS: proof method "sleep"
* Method "sleep" succeeds after a real-time delay (in seconds). This is occasionally useful for demonstration and testing purposes. This refers to Isabelle/c0e1c121c7c0. Maybe a bit silly, but in experimentation with Eisbach and parallel evaluation, it turned out surprisingly difficult to get this right on the spot. So the result is made publicly available here. The key point is the use of the new Method.RUNTIME combinator (see Isabelle/86fc6652c4df). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] NEWS: nesting of Isar goal structure
* Nesting of Isar goal structure has been clarified: the context after the initial backwards refinement is retained for the whole proof, within all its context sections (as indicated via 'next'). This is e.g. relevant for 'using', 'including', 'supply': have "A ∧ A" if a: A for A supply [simp] = a proof show A by simp next show A by simp qed This refers to Isabelle/2b8342b0d98c. The block structure now conforms better to contemporay Isar, with its various ways to operate in the backwards refinement are, which is sometimes used for "proof scripting". Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] »real« considered harmful
On Wed, 24 Jun 2015, Larry Paulson wrote: This may be the problem. I don’t remember exactly what I was trying to do, only that it was very difficult. Of course nobody uses show_types any more. Larry On 24 Jun 2015, at 15:13, Dmitriy Traytel wrote: You can hover in the output panel, but you won't see types of constants there. Input and output of terms have always been slightly asymmetric, despite attempts to make them agree as much as feasible over the decades. The type annotations for certain term items in the PIDE document markup is only half finished. It was considered impossible over many years, and getting it to the still current state was so difficult, that I did not revisit it again. It needs to be done one day, nonetheless. Note that show_types is actually related to PIDE type markup: roughly speaking, in places where show_types could work, the markup can be provided as well. Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] »real« considered harmful
This may be the problem. I don’t remember exactly what I was trying to do, only that it was very difficult. Of course nobody uses show_types any more. Larry > On 24 Jun 2015, at 15:13, Dmitriy Traytel wrote: > > You can hover in the output panel, but you won't see types of constants there. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] »real« considered harmful
On 24.06.2015 16:29, Larry Paulson wrote: > This may be the problem. I don’t remember exactly what I was trying to do, > only that it was very difficult. Of course nobody uses show_types any more. At least this was the problem for me. A notorious instance of the same problem are the functions in HOL-Word, e.g. "ucast :: 'a word => 'b word" and "uint :: 'a word => int". Getting at the types of things like "uint (ucast 4)" in some big term happens often when verifying C programs and is pretty annoying. Such things need a disambiguating output syntax (at least as long as hovering in the output buffer doesn't show the types, maybe even then). ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] »real« considered harmful
Ah, I see the problem. In that case, one could still hover over the "of_nat" in the output window, but it is perhaps not ideal. On 24/06/15 16:08, Dmitriy Traytel wrote: I guess what Larry means is there is no way to see a type of a constant that is not there in the source. Consider e.g. declare [[coercion "of_nat :: nat ⇒ real"]] term "sqrt (2 :: nat)" Today the output says "sqrt (real_of_nat 2)". But if there would be no abbreviation for "of_nat :: nat ⇒ real", how would you deduce the type of the coercion. Dmitriy On 24.06.2015 16:01, Manuel Eberl wrote: On 24/06/15 15:55, Larry Paulson wrote: A more appropriate point is that it can be tricky in Isabelle/jEdit to determine the type of an expression such as “of_nat k”, as there is nothing to click on. When I type ‘term "sqrt (of_nat 2)"’ and hover over the ‘of_nat’, it says ‘constant "Nat.semiring_1_class.of_nat" :: nat ⇒ real’. ___ 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] »real« considered harmful
You can hover in the output panel, but you won't see types of constants there. Dmitriy On 24.06.2015 16:09, Manuel Eberl wrote: Ah, I see the problem. In that case, one could still hover over the "of_nat" in the output window, but it is perhaps not ideal. On 24/06/15 16:08, Dmitriy Traytel wrote: I guess what Larry means is there is no way to see a type of a constant that is not there in the source. Consider e.g. declare [[coercion "of_nat :: nat ⇒ real"]] term "sqrt (2 :: nat)" Today the output says "sqrt (real_of_nat 2)". But if there would be no abbreviation for "of_nat :: nat ⇒ real", how would you deduce the type of the coercion. Dmitriy On 24.06.2015 16:01, Manuel Eberl wrote: On 24/06/15 15:55, Larry Paulson wrote: A more appropriate point is that it can be tricky in Isabelle/jEdit to determine the type of an expression such as “of_nat k”, as there is nothing to click on. When I type ‘term "sqrt (of_nat 2)"’ and hover over the ‘of_nat’, it says ‘constant "Nat.semiring_1_class.of_nat" :: nat ⇒ real’. ___ 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] »real« considered harmful
I guess what Larry means is there is no way to see a type of a constant that is not there in the source. Consider e.g. declare [[coercion "of_nat :: nat ⇒ real"]] term "sqrt (2 :: nat)" Today the output says "sqrt (real_of_nat 2)". But if there would be no abbreviation for "of_nat :: nat ⇒ real", how would you deduce the type of the coercion. Dmitriy On 24.06.2015 16:01, Manuel Eberl wrote: On 24/06/15 15:55, Larry Paulson wrote: A more appropriate point is that it can be tricky in Isabelle/jEdit to determine the type of an expression such as “of_nat k”, as there is nothing to click on. When I type ‘term "sqrt (of_nat 2)"’ and hover over the ‘of_nat’, it says ‘constant "Nat.semiring_1_class.of_nat" :: nat ⇒ real’. ___ 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] »real« considered harmful
On 24/06/15 15:55, Larry Paulson wrote: A more appropriate point is that it can be tricky in Isabelle/jEdit to determine the type of an expression such as “of_nat k”, as there is nothing to click on. When I type ‘term "sqrt (of_nat 2)"’ and hover over the ‘of_nat’, it says ‘constant "Nat.semiring_1_class.of_nat" :: nat ⇒ real’. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] »real« considered harmful
The first question is, do we need a prefix syntax for type constraints? My point was that the ability to write [:real:]of_nat k might be better than having to introduce and abbreviations such as real_of_nat, but this is not clear. The latter has the advantage that it is automatically introduced when the term has the matching type, and we would not want the pretty printer to insert [:real:] all over the place, but only when it is necessary. A more appropriate point is that it can be tricky in Isabelle/jEdit to determine the type of an expression such as “of_nat k”, as there is nothing to click on. Larry > On 23 Jun 2015, at 21:42, Makarius wrote: > > On Sat, 6 Jun 2015, Florian Haftmann wrote: > >>> Conceivably we could introduce a prefix syntax for type constraints, e.g. >>> >>> [:real:]of_nat k >>> >>> I’d find such a thing useful from time to time. >> >> My personal favourite would be System-F-style type instantiation >> >> of_nat [real] k >> >> instead of type annotations but there are hardly any brackets left which >> could serve here. > > In theory we have an infinite store of Isabelle symbols, and many usable > Unicode points for rendering. Here is a list of funny brackets to consider: > http://stackoverflow.com/questions/13535172/list-of-all-unicodes-open-close-brackets > > For example: > > U+2772 Ps LIGHT LEFT TORTOISE SHELL BRACKET ORNAMENT ❲ > U+2773 Pe LIGHT RIGHT TORTOISE SHELL BRACKET ORNAMENT ❳ > U+3014 Ps LEFT TORTOISE SHELL BRACKET 〔 > U+3015 Pe RIGHT TORTOISE SHELL BRACKET 〕 > > > In practice this also needs a LaTeX macro, and maybe some ASCII abbreviation > for input in the Prover IDE. > > > 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
