[isabelle-dev] Isabelle_10-Sep-2013

[Tobias Nipkow]

You mean parentheses, not braces. This is an intentional change. See the NEWS:

* Weaker precendence of syntax for big intersection and union on sets,
in accordance with corresponding lattice operations.  INCOMPATIBILITY.

Tobias


Am 11/09/2013 11:31, schrieb C. Diekmann:
> Hi,
> 
> I just downloaded the compiled binary for Linux and wanted to share my
> experience. It seems there are some issues with braces. My thy files
> work fine with the release, however, in the AFP Collections entry, I
> had to make the following changes:
> In Collections/spec/SetSpec.thy:
>  locale set_Union_image = set α1 invar1 + set α2 invar2 + set α3 invar3
>    for α1 :: "'s1 ⇒ 'a set" and invar1
>    and α2 :: "'s2 ⇒ 'b set" and invar2
>    and α3 :: "'s3 ⇒ 'b set" and invar3
>    + (*<-- not a diff plus*)
>    fixes Union_image :: "('a ⇒ 's2) ⇒ 's1 ⇒ 's3"
>    assumes Union_image_correct:
> -    "⟦ invar1 s; !!x. x∈α1 s ⟹ invar2 (f x) ⟧ ⟹ α3 (Union_image f s)
> = ⋃α2`f`α1 s"
> +   "⟦ invar1 s; !!x. x∈α1 s ⟹ invar2 (f x) ⟧ ⟹ α3 (Union_image f s) =
> ⋃(α2`f`α1 s)"
>      "⟦ invar1 s; !!x. x∈α1 s ⟹ invar2 (f x) ⟧ ⟹ invar3 (Union_image f s)"
> 
> In Collections/gen_algo/SetGA.thy:
>  lemma it_Union_image_correct:
>    assumes "set_iteratei α1 invar1 iti1"
>    assumes "set_empty α3 invar3 em3"
>    assumes "set_union α2 invar2 α3 invar3 α3 invar3 un233"
>    shows "set_Union_image α1 invar1 α2 invar2 α3 invar3
> (it_Union_image iti1 em3 un233)"
>  proof -
>    interpret set_iteratei α1 invar1 iti1 by fact
>    interpret set_empty α3 invar3 em3 by fact
>    interpret set_union α2 invar2 α3 invar3 α3 invar3 un233 by fact
> 
>    {
>      fix s f
> -       α3 (it_Union_image iti1 em3 un233 f s) = ⋃α2 ` f ` α1 s
> +       α3 (it_Union_image iti1 em3 un233 f s) = ⋃(α2 ` f ` α1 s)
>        ∧ invar3 (it_Union_image iti1 em3 un233 f s)"
>        apply (unfold it_Union_image_def)
> -       apply (rule_tac I="λit res. invar3 res ∧ α3 res = ⋃α2`f`(α1 s
> - it)" in iterate_rule_P)
> +      apply (rule_tac I="λit res. invar3 res ∧ α3 res = ⋃(α2`f`(α1 s
> - it))" in iterate_rule_P)
>        apply (fastforce simp add: empty_correct union_correct)+
>        done
>    }
>    thus ?thesis
>      apply unfold_locales
>      apply auto
>      done
>  qed
> 
> Also, but this might be due to my stupidity, when I select something
> in jedit with the mouse, it gets green and I cannot deselect it.
> 
> Finally, the following imports are no longer available:
> "~~/src/HOL/Library/Code_Char_chr"
> "~~/src/HOL/Library/Efficient_Nat"
> "~~/src/HOL/Library/Code_Char_ord"
> Something was already mentioned about this (I will investigate later).
> I cannot give feedback about the generated Scala code now as the
> change to the generated code is too huge because of this.
> 
> Cheers
>   Cornelius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>