# HG changeset patch
# User nipkow
# Date 1316556756 -7200
# Node ID a5d43ffc95eb13d62fdaebb9f204fb1c1c07cf04
# Parent  05031b71a89a1ea9ef698e238113c0bfe241abce# Parent  fdac1e9880eb0664402e2c82793d54b82ea82170
merged

diff -r fdac1e9880eb -r a5d43ffc95eb NEWS
--- a/NEWS	Tue Sep 20 05:48:23 2011 +0200
+++ b/NEWS	Wed Sep 21 00:12:36 2011 +0200
@@ -96,8 +96,7 @@
 Redundant lemmas Inf_singleton, Sup_singleton, Inf_binary, Sup_binary,
 INF_eq, SUP_eq, INF_UNIV_range, SUP_UNIV_range, Int_eq_Inter,
 INTER_eq_Inter_image, Inter_def, INT_eq, Un_eq_Union, INF_subset,
-UNION_eq_Union_image, Union_def, UN_singleton, UN_eq have been
-discarded.
+UNION_eq_Union_image, Union_def, UN_eq have been discarded.
 
 More consistent and comprehensive names:
 
diff -r fdac1e9880eb -r a5d43ffc95eb src/CCL/ex/List.thy
--- a/src/CCL/ex/List.thy	Tue Sep 20 05:48:23 2011 +0200
+++ b/src/CCL/ex/List.thy	Wed Sep 21 00:12:36 2011 +0200
@@ -19,7 +19,7 @@
   where "l @ m == lrec(l,m,%x xs g. x$g)"
 
 axiomatization member :: "[i,i]=>i"  (infixr "mem" 55)  (* FIXME dangling eq *)
-  where "a mem l == lrec(l,false,%h t g. if eq(a,h) then true else g)"
+  where member_ax: "a mem l == lrec(l,false,%h t g. if eq(a,h) then true else g)"
 
 definition filter :: "[i,i]=>i"
   where "filter(f,l) == lrec(l,[],%x xs g. if f`x then x$g else g)"
diff -r fdac1e9880eb -r a5d43ffc95eb src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Tue Sep 20 05:48:23 2011 +0200
+++ b/src/HOL/Complete_Lattices.thy	Wed Sep 21 00:12:36 2011 +0200
@@ -1012,6 +1012,9 @@
 lemma image_UN: "f ` UNION A B = (\<Union>x\<in>A. f ` B x)"
   by blast
 
+lemma UN_singleton [simp]: "(\<Union>x\<in>A. {x}) = A"
+  by blast
+
 
 subsection {* Distributive laws *}
 
@@ -1131,11 +1134,6 @@
   "\<And>A B f. (\<Inter>a\<in>A. B (f a)) = (\<Inter>x\<in>f`A. B x)"
   by auto
 
-text {* Legacy names *}
-
-lemma UN_singleton [simp]: "(\<Union>x\<in>A. {x}) = A"
-  by blast
-
 text {* Finally *}
 
 no_notation
diff -r fdac1e9880eb -r a5d43ffc95eb src/HOL/Library/Executable_Set.thy
--- a/src/HOL/Library/Executable_Set.thy	Tue Sep 20 05:48:23 2011 +0200
+++ b/src/HOL/Library/Executable_Set.thy	Wed Sep 21 00:12:36 2011 +0200
@@ -101,12 +101,12 @@
 lemma insert_Set [code]:
   "insert x (Set xs) = Set (List.insert x xs)"
   "insert x (Coset xs) = Coset (removeAll x xs)"
-  by (simp_all add: set_insert)
+  by simp_all
 
 lemma remove_Set [code]:
   "remove x (Set xs) = Set (removeAll x xs)"
   "remove x (Coset xs) = Coset (List.insert x xs)"
-  by (auto simp add: set_insert remove_def)
+  by (auto simp add: remove_def)
 
 lemma image_Set [code]:
   "image f (Set xs) = Set (remdups (map f xs))"
@@ -254,12 +254,12 @@
 lemma Inf_inf [code]:
   "Inf (Set xs) = foldr inf xs (top :: 'a::complete_lattice)"
   "Inf (Coset []) = (bot :: 'a::complete_lattice)"
-  by (simp_all add: Inf_UNIV Inf_set_foldr)
+  by (simp_all add: Inf_set_foldr)
 
 lemma Sup_sup [code]:
   "Sup (Set xs) = foldr sup xs (bot :: 'a::complete_lattice)"
   "Sup (Coset []) = (top :: 'a::complete_lattice)"
-  by (simp_all add: Sup_UNIV Sup_set_foldr)
+  by (simp_all add: Sup_set_foldr)
 
 lemma Inter_inter [code]:
   "Inter (Set xs) = foldr inter xs (Coset [])"
@@ -279,50 +279,40 @@
 
 text {* Initially contributed by Tjark Weber. *}
 
-lemma bounded_Collect_code [code_unfold]:
-  "{x\<in>S. P x} = project P S"
-  by (auto simp add: project_def)
-
-lemma Id_on_code [code]:
-  "Id_on (Set xs) = Set [(x,x). x \<leftarrow> xs]"
-  by (auto simp add: Id_on_def)
-
-lemma Domain_fst [code]:
+lemma [code]:
   "Domain r = fst ` r"
-  by (auto simp add: image_def Bex_def)
+  by (fact Domain_fst)
 
-lemma Range_snd [code]:
+lemma [code]:
   "Range r = snd ` r"
-  by (auto simp add: image_def Bex_def)
+  by (fact Range_snd)
 
-lemma irrefl_code [code]:
-  "irrefl r \<longleftrightarrow> (\<forall>(x, y)\<in>r. x \<noteq> y)"
-  by (auto simp add: irrefl_def)
+lemma [code]:
+  "trans r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. \<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> (x, z) \<in> r)"
+  by (fact trans_join)
+
+lemma [code]:
+  "irrefl r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<noteq> y)"
+  by (fact irrefl_distinct)
 
-lemma trans_def [code]:
-  "trans r \<longleftrightarrow> (\<forall>(x, y1)\<in>r. \<forall>(y2, z)\<in>r. y1 = y2 \<longrightarrow> (x, z)\<in>r)"
-  by (auto simp add: trans_def)
+lemma [code]:
+  "acyclic r \<longleftrightarrow> irrefl (r^+)"
+  by (fact acyclic_irrefl)
 
-definition "exTimes A B = Sigma A (%_. B)"
-
-lemma [code_unfold]:
-  "Sigma A (%_. B) = exTimes A B"
-  by (simp add: exTimes_def)
+lemma [code]:
+  "More_Set.product (Set xs) (Set ys) = Set [(x, y). x \<leftarrow> xs, y \<leftarrow> ys]"
+  by (unfold Set_def) (fact product_code)
 
-lemma exTimes_code [code]:
-  "exTimes (Set xs) (Set ys) = Set [(x,y). x \<leftarrow> xs, y \<leftarrow> ys]"
-  by (auto simp add: exTimes_def)
-
-lemma rel_comp_code [code]:
-  "(Set xys) O (Set yzs) = Set (remdups [(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
- by (auto simp add: Bex_def)
+lemma [code]:
+  "Id_on (Set xs) = Set [(x, x). x \<leftarrow> xs]"
+  by (unfold Set_def) (fact Id_on_set)
 
-lemma acyclic_code [code]:
-  "acyclic r = irrefl (r^+)"
-  by (simp add: acyclic_def irrefl_def)
+lemma [code]:
+  "Set xys O Set yzs = Set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
+  by (unfold Set_def) (fact set_rel_comp)
 
-lemma wf_code [code]:
+lemma [code]:
   "wf (Set xs) = acyclic (Set xs)"
-  by (simp add: wf_iff_acyclic_if_finite)
+  by (unfold Set_def) (fact wf_set)
 
 end
diff -r fdac1e9880eb -r a5d43ffc95eb src/HOL/Library/More_Set.thy
--- a/src/HOL/Library/More_Set.thy	Tue Sep 20 05:48:23 2011 +0200
+++ b/src/HOL/Library/More_Set.thy	Wed Sep 21 00:12:36 2011 +0200
@@ -31,7 +31,20 @@
 qed
 
 definition project :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
-  "project P A = {a\<in>A. P a}"
+  "project P A = {a \<in> A. P a}"
+
+lemma bounded_Collect_code [code_unfold_post]:
+  "{x \<in> A. P x} = project P A"
+  by (simp add: project_def)
+
+definition product :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where
+  "product A B = Sigma A (\<lambda>_. B)"
+
+hide_const (open) product
+
+lemma [code_unfold_post]:
+  "Sigma A (\<lambda>_. B) = More_Set.product A B"
+  by (simp add: product_def)
 
 
 subsection {* Basic set operations *}
@@ -75,7 +88,7 @@
   "set xs \<union> A = foldr Set.insert xs A"
 proof -
   have "\<And>x y :: 'a. insert y \<circ> insert x = insert x \<circ> insert y"
-    by (auto intro: ext)
+    by auto
   then show ?thesis by (simp add: union_set foldr_fold)
 qed
 
@@ -92,7 +105,7 @@
   "A - set xs = foldr remove xs A"
 proof -
   have "\<And>x y :: 'a. remove y \<circ> remove x = remove x \<circ> remove y"
-    by (auto simp add: remove_def intro: ext)
+    by (auto simp add: remove_def)
   then show ?thesis by (simp add: minus_set foldr_fold)
 qed
 
@@ -120,10 +133,22 @@
   by (auto simp add: project_def)
 
 
-subsection {* Various lemmas *}
+subsection {* Theorems on relations *}
+
+lemma product_code:
+  "More_Set.product (set xs) (set ys) = set [(x, y). x \<leftarrow> xs, y \<leftarrow> ys]"
+  by (auto simp add: product_def)
 
-lemma not_set_compl:
-  "Not \<circ> set xs = - set xs"
-  by (simp add: fun_Compl_def comp_def fun_eq_iff)
+lemma Id_on_set:
+  "Id_on (set xs) = set [(x, x). x \<leftarrow> xs]"
+  by (auto simp add: Id_on_def)
+
+lemma set_rel_comp:
+  "set xys O set yzs = set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
+  by (auto simp add: Bex_def)
+
+lemma wf_set:
+  "wf (set xs) = acyclic (set xs)"
+  by (simp add: wf_iff_acyclic_if_finite)
 
 end
diff -r fdac1e9880eb -r a5d43ffc95eb src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Tue Sep 20 05:48:23 2011 +0200
+++ b/src/HOL/Relation.thy	Wed Sep 21 00:12:36 2011 +0200
@@ -275,6 +275,10 @@
 
 subsection {* Transitivity *}
 
+lemma trans_join:
+  "trans r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. \<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> (x, z) \<in> r)"
+  by (auto simp add: trans_def)
+
 lemma transI:
   "(!!x y z. (x, y) : r ==> (y, z) : r ==> (x, z) : r) ==> trans r"
 by (unfold trans_def) iprover
@@ -296,6 +300,10 @@
 
 subsection {* Irreflexivity *}
 
+lemma irrefl_distinct:
+  "irrefl r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<noteq> y)"
+  by (auto simp add: irrefl_def)
+
 lemma irrefl_diff_Id[simp]: "irrefl(r-Id)"
 by(simp add:irrefl_def)
 
@@ -386,6 +394,10 @@
   "a : Domain r ==> (!!y. (a, y) : r ==> P) ==> P"
 by (iprover dest!: iffD1 [OF Domain_iff])
 
+lemma Domain_fst:
+  "Domain r = fst ` r"
+  by (auto simp add: image_def Bex_def)
+
 lemma Domain_empty [simp]: "Domain {} = {}"
 by blast
 
@@ -440,6 +452,10 @@
 lemma RangeE [elim!]: "b : Range r ==> (!!x. (x, b) : r ==> P) ==> P"
 by (unfold Range_def) (iprover elim!: DomainE dest!: converseD)
 
+lemma Range_snd:
+  "Range r = snd ` r"
+  by (auto simp add: image_def Bex_def)
+
 lemma Range_empty [simp]: "Range {} = {}"
 by blast
 
diff -r fdac1e9880eb -r a5d43ffc95eb src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Tue Sep 20 05:48:23 2011 +0200
+++ b/src/HOL/Wellfounded.thy	Wed Sep 21 00:12:36 2011 +0200
@@ -387,6 +387,10 @@
 abbreviation acyclicP :: "('a => 'a => bool) => bool" where
   "acyclicP r == acyclic {(x, y). r x y}"
 
+lemma acyclic_irrefl:
+  "acyclic r \<longleftrightarrow> irrefl (r^+)"
+  by (simp add: acyclic_def irrefl_def)
+
 lemma acyclicI: "ALL x. (x, x) ~: r^+ ==> acyclic r"
   by (simp add: acyclic_def)
 
diff -r fdac1e9880eb -r a5d43ffc95eb src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Tue Sep 20 05:48:23 2011 +0200
+++ b/src/Tools/Code/code_haskell.ML	Wed Sep 21 00:12:36 2011 +0200
@@ -85,13 +85,16 @@
                 then print_case tyvars some_thm vars fxy cases
                 else print_app tyvars some_thm vars fxy c_ts
             | NONE => print_case tyvars some_thm vars fxy cases)
-    and print_app_expr tyvars some_thm vars ((c, ((_, (function_typs, body_typ)), annotate)), ts) =
+    and print_app_expr tyvars some_thm vars ((c, ((_, (arg_tys, result_ty)), annotate)), ts) =
       let
-        val ty = Library.foldr (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (function_typs, body_typ)
-        fun put_annotation c = brackets [c, str "::", print_typ tyvars NOBR ty]
+        val ty = Library.foldr (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (arg_tys, result_ty)
+        val printed_const =
+          if annotate then
+            brackets [(str o deresolve) c, str "::", print_typ tyvars NOBR ty]
+          else
+            (str o deresolve) c
       in 
-        ((if annotate then put_annotation else I)
-          ((str o deresolve) c)) :: map (print_term tyvars some_thm vars BR) ts
+        printed_const :: map (print_term tyvars some_thm vars BR) ts
       end
     and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) const_syntax
     and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p
@@ -234,15 +237,16 @@
                     ]
                 | SOME k =>
                     let
-                      val (c, ((_, tys), _)) = const; (* FIXME: pass around the need annotation flag here? *)
+                      val (c, ((_, tys), _)) = const;
                       val (vs, rhs) = (apfst o map) fst
                         (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
                       val s = if (is_some o const_syntax) c
                         then NONE else (SOME o Long_Name.base_name o deresolve) c;
                       val vars = reserved
                         |> intro_vars (map_filter I (s :: vs));
-                      val lhs = IConst (classparam, ((([], []), tys), false (* FIXME *))) `$$ map IVar vs;
-                        (*dictionaries are not relevant at this late stage*)
+                      val lhs = IConst (classparam, ((([], []), tys), false)) `$$ map IVar vs;
+                        (*dictionaries are not relevant at this late stage,
+                          and these consts never need type annotations for disambiguation *)
                     in
                       semicolon [
                         print_term tyvars (SOME thm) vars NOBR lhs,
@@ -323,8 +327,7 @@
       in deriv [] tyco end;
     fun print_stmt deresolve = print_haskell_stmt labelled_name
       class_syntax tyco_syntax const_syntax (make_vars reserved)
-      deresolve
-      (if string_classes then deriving_show else K false);
+      deresolve (if string_classes then deriving_show else K false);
 
     (* print modules *)
     val import_includes_ps =
diff -r fdac1e9880eb -r a5d43ffc95eb src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Tue Sep 20 05:48:23 2011 +0200
+++ b/src/Tools/Code/code_ml.ML	Wed Sep 21 00:12:36 2011 +0200
@@ -117,9 +117,9 @@
                 then print_case is_pseudo_fun some_thm vars fxy cases
                 else print_app is_pseudo_fun some_thm vars fxy c_ts
             | NONE => print_case is_pseudo_fun some_thm vars fxy cases)
-    and print_app_expr is_pseudo_fun some_thm vars (app as ((c, (((_, iss), (function_typs, _)), _)), ts)) =
+    and print_app_expr is_pseudo_fun some_thm vars (app as ((c, (((_, iss), (arg_tys, _)), _)), ts)) =
       if is_cons c then
-        let val k = length function_typs in
+        let val k = length arg_tys in
           if k < 2 orelse length ts = k
           then (str o deresolve) c
             :: the_list (tuplify (print_term is_pseudo_fun some_thm vars) BR ts)
diff -r fdac1e9880eb -r a5d43ffc95eb src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Tue Sep 20 05:48:23 2011 +0200
+++ b/src/Tools/Code/code_printer.ML	Wed Sep 21 00:12:36 2011 +0200
@@ -315,7 +315,7 @@
       |-> (fn cs' => pair (Complex_const_syntax (n, f literals cs')));
 
 fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy
-    (app as ((c, ((_, (function_typs, _)), _)), ts)) =
+    (app as ((c, ((_, (arg_tys, _)), _)), ts)) =
   case const_syntax c of
     NONE => brackify fxy (print_app_expr some_thm vars app)
   | SOME (Plain_const_syntax (_, s)) =>
@@ -323,7 +323,7 @@
   | SOME (Complex_const_syntax (k, print)) =>
       let
         fun print' fxy ts =
-          print (print_term some_thm) some_thm vars fxy (ts ~~ take k function_typs);
+          print (print_term some_thm) some_thm vars fxy (ts ~~ take k arg_tys);
       in
         if k = length ts
         then print' fxy ts
diff -r fdac1e9880eb -r a5d43ffc95eb src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Tue Sep 20 05:48:23 2011 +0200
+++ b/src/Tools/Code/code_scala.ML	Wed Sep 21 00:12:36 2011 +0200
@@ -72,23 +72,23 @@
                 else print_app tyvars is_pat some_thm vars fxy c_ts
             | NONE => print_case tyvars some_thm vars fxy cases)
     and print_app tyvars is_pat some_thm vars fxy
-        (app as ((c, (((arg_typs, _), (function_typs, _)), _)), ts)) =
+        (app as ((c, (((tys, _), (arg_tys, _)), _)), ts)) =
       let
         val k = length ts;
-        val arg_typs' = if is_pat orelse
-          (is_none (const_syntax c) andalso is_singleton_constr c) then [] else arg_typs;
+        val tys' = if is_pat orelse
+          (is_none (const_syntax c) andalso is_singleton_constr c) then [] else tys;
         val (l, print') = case const_syntax c
          of NONE => (args_num c, fn fxy => fn ts => applify "(" ")"
               (print_term tyvars is_pat some_thm vars NOBR) fxy
                 (applify "[" "]" (print_typ tyvars NOBR)
-                  NOBR ((str o deresolve) c) arg_typs') ts)
+                  NOBR ((str o deresolve) c) tys') ts)
           | SOME (Plain_const_syntax (k, s)) => (k, fn fxy => fn ts => applify "(" ")"
               (print_term tyvars is_pat some_thm vars NOBR) fxy
                 (applify "[" "]" (print_typ tyvars NOBR)
-                  NOBR (str s) arg_typs') ts)
+                  NOBR (str s) tys') ts)
           | SOME (Complex_const_syntax (k, print)) =>
               (k, fn fxy => fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy
-                (ts ~~ take k function_typs))
+                (ts ~~ take k arg_tys))
       in if k = l then print' fxy ts
       else if k < l then
         print_term tyvars is_pat some_thm vars fxy (Code_Thingol.eta_expand l app)
diff -r fdac1e9880eb -r a5d43ffc95eb src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Tue Sep 20 05:48:23 2011 +0200
+++ b/src/Tools/Code/code_thingol.ML	Wed Sep 21 00:12:36 2011 +0200
@@ -23,7 +23,7 @@
       `%% of string * itype list
     | ITyVar of vname;
   type const = string * (((itype list * dict list list) * (itype list * itype)) * bool)
-    (* f [T1..Tn] {dicts} (_::S1) .. (_..Sm) =^= (f, (([T1..Tn], dicts), [S1..Sm]) *)
+    (* (f [T1..Tn] {dicts} (_::S1) .. (_::Sm)) :: S =^= (f, ((([T1..Tn], dicts), ([S1..Sm], S)), ambiguous)) *)
   datatype iterm =
       IConst of const
     | IVar of vname option
@@ -144,7 +144,7 @@
   | ITyVar of vname;
 
 type const = string * (((itype list * dict list list) *
-  (itype list (*types of arguments*) * itype (*body type*))) * bool (*requires type annotation*))
+  (itype list (*types of arguments*) * itype (*result type*))) * bool (*requires type annotation*))
 
 datatype iterm =
     IConst of const
diff -r fdac1e9880eb -r a5d43ffc95eb src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Tue Sep 20 05:48:23 2011 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala	Wed Sep 21 00:12:36 2011 +0200
@@ -139,15 +139,15 @@
   }
   status.renderer = new Node_Renderer
 
-  private def handle_changed(changed_nodes: Set[Document.Node.Name])
+  private def handle_update(restriction: Option[Set[Document.Node.Name]] = None)
   {
     Swing_Thread.now {
-      // FIXME correlation to changed_nodes!?
       val snapshot = Isabelle.session.snapshot()
+      val nodes = restriction getOrElse snapshot.version.nodes.keySet
 
       var nodes_status1 = nodes_status
       for {
-        name <- changed_nodes
+        name <- nodes
         node <- snapshot.version.nodes.get(name)
         val status = Isar_Document.node_status(snapshot.state, snapshot.version, node)
       } nodes_status1 += (name -> status)
@@ -179,7 +179,7 @@
         case phase: Session.Phase =>
           Swing_Thread.now { session_phase.text = " " + phase.toString + " " }
 
-        case changed: Session.Commands_Changed => handle_changed(changed.nodes)
+        case changed: Session.Commands_Changed => handle_update(Some(changed.nodes))
 
         case bad => System.err.println("Session_Dockable: ignoring bad message " + bad)
       }
@@ -197,4 +197,6 @@
     Isabelle.session.phase_changed -= main_actor
     Isabelle.session.commands_changed -= main_actor
   }
+
+  handle_update()
 }