--- 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:
--- 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)"
--- 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
--- 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
--- 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
--- 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
--- 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)
--- 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 =
--- 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)
--- 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
--- 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)
--- 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
--- 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()
}