[isabelle-dev] RE: Isabelle_10-Sep-2013

[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