--- a/src/HOL/Inductive.thy Fri Dec 16 12:01:10 2011 +0100
+++ b/src/HOL/Inductive.thy Fri Dec 16 22:07:03 2011 +0100
@@ -116,7 +116,7 @@
to control unfolding*}
lemma def_lfp_unfold: "[| h==lfp(f); mono(f) |] ==> h = f(h)"
-by (auto intro!: lfp_unfold)
+ by (auto intro!: lfp_unfold)
lemma def_lfp_induct:
"[| A == lfp(f); mono(f);
@@ -160,12 +160,12 @@
text{*weak version*}
lemma weak_coinduct: "[| a: X; X \<subseteq> f(X) |] ==> a : gfp(f)"
-by (rule gfp_upperbound [THEN subsetD], auto)
+ by (rule gfp_upperbound [THEN subsetD]) auto
lemma weak_coinduct_image: "!!X. [| a : X; g`X \<subseteq> f (g`X) |] ==> g a : gfp f"
-apply (erule gfp_upperbound [THEN subsetD])
-apply (erule imageI)
-done
+ apply (erule gfp_upperbound [THEN subsetD])
+ apply (erule imageI)
+ done
lemma coinduct_lemma:
"[| X \<le> f (sup X (gfp f)); mono f |] ==> sup X (gfp f) \<le> f (sup X (gfp f))"
@@ -182,7 +182,7 @@
text{*strong version, thanks to Coen and Frost*}
lemma coinduct_set: "[| mono(f); a: X; X \<subseteq> f(X Un gfp(f)) |] ==> a : gfp(f)"
-by (blast intro: weak_coinduct [OF _ coinduct_lemma])
+ by (blast intro: weak_coinduct [OF _ coinduct_lemma])
lemma coinduct: "[| mono(f); X \<le> f (sup X (gfp f)) |] ==> X \<le> gfp(f)"
apply (rule order_trans)
@@ -192,7 +192,7 @@
done
lemma gfp_fun_UnI2: "[| mono(f); a: gfp(f) |] ==> a: f(X Un gfp(f))"
-by (blast dest: gfp_lemma2 mono_Un)
+ by (blast dest: gfp_lemma2 mono_Un)
subsection {* Even Stronger Coinduction Rule, by Martin Coen *}
@@ -227,27 +227,26 @@
to control unfolding*}
lemma def_gfp_unfold: "[| A==gfp(f); mono(f) |] ==> A = f(A)"
-by (auto intro!: gfp_unfold)
+ by (auto intro!: gfp_unfold)
lemma def_coinduct:
"[| A==gfp(f); mono(f); X \<le> f(sup X A) |] ==> X \<le> A"
-by (iprover intro!: coinduct)
+ by (iprover intro!: coinduct)
lemma def_coinduct_set:
"[| A==gfp(f); mono(f); a:X; X \<subseteq> f(X Un A) |] ==> a: A"
-by (auto intro!: coinduct_set)
+ by (auto intro!: coinduct_set)
(*The version used in the induction/coinduction package*)
lemma def_Collect_coinduct:
"[| A == gfp(%w. Collect(P(w))); mono(%w. Collect(P(w)));
a: X; !!z. z: X ==> P (X Un A) z |] ==>
a : A"
-apply (erule def_coinduct_set, auto)
-done
+ by (erule def_coinduct_set) auto
lemma def_coinduct3:
"[| A==gfp(f); mono(f); a:X; X \<subseteq> f(lfp(%x. f(x) Un X Un A)) |] ==> a: A"
-by (auto intro!: coinduct3)
+ by (auto intro!: coinduct3)
text{*Monotonicity of @{term gfp}!*}
lemma gfp_mono: "(!!Z. f Z \<le> g Z) ==> gfp f \<le> gfp g"
@@ -296,8 +295,7 @@
let
fun fun_tr ctxt [cs] =
let
- (* FIXME proper name context!? *)
- val x = Free (singleton (Name.variant_list (Term.add_free_names cs [])) "x", dummyT);
+ val x = Syntax.free (fst (Name.variant "x" (Term.declare_term_frees cs Name.context)));
val ft = Datatype_Case.case_tr true ctxt [x, cs];
in lambda x ft end
in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end
--- a/src/HOL/Tools/Datatype/datatype.ML Fri Dec 16 12:01:10 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML Fri Dec 16 22:07:03 2011 +0100
@@ -644,11 +644,11 @@
DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
(prems ~~ (constr_defs @ map mk_meta_eq iso_char_thms)))]);
- val ([dt_induct'], thy7) =
+ val ([(_, [dt_induct'])], thy7) =
thy6
- |> Global_Theory.add_thms
- [((Binding.qualify true big_name (Binding.name "induct"), dt_induct),
- [case_names_induct])]
+ |> Global_Theory.note_thmss ""
+ [((Binding.qualify true big_name (Binding.name "induct"), [case_names_induct]),
+ [([dt_induct], [])])]
||> Theory.checkpoint;
in
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Fri Dec 16 12:01:10 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Fri Dec 16 22:07:03 2011 +0100
@@ -233,7 +233,7 @@
(if length descr' = 1 then [big_reccomb_name]
else map (prefix (big_reccomb_name ^ "_") o string_of_int) (1 upto length descr'));
val reccombs =
- map (fn ((name, T), T') => list_comb (Const (name, reccomb_fn_Ts @ [T] ---> T'), rec_fns))
+ map (fn ((name, T), T') => Const (name, reccomb_fn_Ts @ [T] ---> T'))
(reccomb_names ~~ recTs ~~ rec_result_Ts);
val (reccomb_defs, thy2) =
@@ -245,9 +245,9 @@
(map
(fn ((((name, comb), set), T), T') =>
(Binding.name (Long_Name.base_name name ^ "_def"),
- Logic.mk_equals (comb, absfree ("x", T)
+ Logic.mk_equals (comb, fold_rev lambda rec_fns (absfree ("x", T)
(Const (@{const_name The}, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T')
- (set $ Free ("x", T) $ Free ("y", T'))))))
+ (set $ Free ("x", T) $ Free ("y", T')))))))
(reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts))
||> Sign.parent_path
||> Theory.checkpoint;
@@ -270,10 +270,11 @@
in
thy2
|> Sign.add_path (space_implode "_" new_type_names)
- |> Global_Theory.add_thmss [((Binding.name "recs", rec_thms), [Nitpick_Simps.add])]
+ |> Global_Theory.note_thmss ""
+ [((Binding.name "recs", [Nitpick_Simps.add]), [(rec_thms, [])])]
||> Sign.parent_path
||> Theory.checkpoint
- |-> (fn thms => pair (reccomb_names, flat thms))
+ |-> (fn thms => pair (reccomb_names, maps #2 thms))
end;
@@ -324,9 +325,10 @@
val decl = ((Binding.name (Long_Name.base_name name), caseT), NoSyn);
val def =
(Binding.name (Long_Name.base_name name ^ "_def"),
- Logic.mk_equals (list_comb (Const (name, caseT), fns1),
- list_comb (reccomb, (flat (take i case_dummy_fns)) @
- fns2 @ (flat (drop (i + 1) case_dummy_fns)))));
+ Logic.mk_equals (Const (name, caseT),
+ fold_rev lambda fns1
+ (list_comb (reccomb,
+ flat (take i case_dummy_fns) @ fns2 @ flat (drop (i + 1) case_dummy_fns)))));
val ([def_thm], thy') =
thy
|> Sign.declare_const_global decl |> snd
--- a/src/HOL/Tools/Datatype/datatype_aux.ML Fri Dec 16 12:01:10 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML Fri Dec 16 22:07:03 2011 +0100
@@ -93,29 +93,29 @@
(* store theorems in theory *)
-fun store_thmss_atts label tnames attss thmss =
+fun store_thmss_atts name tnames attss thmss =
fold_map (fn ((tname, atts), thms) =>
- Global_Theory.add_thmss
- [((Binding.qualify true tname (Binding.name label), thms), atts)]
- #-> (fn thm::_ => pair thm)) (tnames ~~ attss ~~ thmss)
+ Global_Theory.note_thmss ""
+ [((Binding.qualify true tname (Binding.name name), atts), [(thms, [])])]
+ #-> (fn [(_, res)] => pair res)) (tnames ~~ attss ~~ thmss)
##> Theory.checkpoint;
-fun store_thmss label tnames = store_thmss_atts label tnames (replicate (length tnames) []);
+fun store_thmss name tnames = store_thmss_atts name tnames (replicate (length tnames) []);
-fun store_thms_atts label tnames attss thmss =
- fold_map (fn ((tname, atts), thms) =>
- Global_Theory.add_thms
- [((Binding.qualify true tname (Binding.name label), thms), atts)]
- #-> (fn thm::_ => pair thm)) (tnames ~~ attss ~~ thmss)
+fun store_thms_atts name tnames attss thms =
+ fold_map (fn ((tname, atts), thm) =>
+ Global_Theory.note_thmss ""
+ [((Binding.qualify true tname (Binding.name name), atts), [([thm], [])])]
+ #-> (fn [(_, [res])] => pair res)) (tnames ~~ attss ~~ thms)
##> Theory.checkpoint;
-fun store_thms label tnames = store_thms_atts label tnames (replicate (length tnames) []);
+fun store_thms name tnames = store_thms_atts name tnames (replicate (length tnames) []);
(* split theorem thm_1 & ... & thm_n into n theorems *)
fun split_conj_thm th =
- ((th RS conjunct1)::(split_conj_thm (th RS conjunct2))) handle THM _ => [th];
+ ((th RS conjunct1) :: split_conj_thm (th RS conjunct2)) handle THM _ => [th];
val mk_conj = foldr1 (HOLogic.mk_binop @{const_name HOL.conj});
val mk_disj = foldr1 (HOLogic.mk_binop @{const_name HOL.disj});
--- a/src/HOL/Tools/Datatype/rep_datatype.ML Fri Dec 16 12:01:10 2011 +0100
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML Fri Dec 16 22:07:03 2011 +0100
@@ -78,25 +78,26 @@
val dt_names = map fst dt_infos;
val prfx = Binding.qualify true (space_implode "_" new_type_names);
val simps = flat (inject @ distinct @ case_rewrites) @ rec_rewrites;
- val named_rules = flat (map_index (fn (index, tname) =>
- [((Binding.empty, [nth inducts index]), [Induct.induct_type tname]),
- ((Binding.empty, [nth exhaust index]), [Induct.cases_type tname])]) dt_names);
+ val named_rules = flat (map_index (fn (i, tname) =>
+ [((Binding.empty, [Induct.induct_type tname]), [([nth inducts i], [])]),
+ ((Binding.empty, [Induct.cases_type tname]), [([nth exhaust i], [])])]) dt_names);
val unnamed_rules = map (fn induct =>
- ((Binding.empty, [induct]), [Rule_Cases.inner_rule, Induct.induct_type ""]))
+ ((Binding.empty, [Rule_Cases.inner_rule, Induct.induct_type ""]), [([induct], [])]))
(drop (length dt_names) inducts);
in
thy9
- |> Global_Theory.add_thmss ([((prfx (Binding.name "simps"), simps), []),
- ((prfx (Binding.name "inducts"), inducts), []),
- ((prfx (Binding.name "splits"), maps (fn (x, y) => [x, y]) splits), []),
- ((Binding.empty, flat case_rewrites @ flat distinct @ rec_rewrites),
- [Simplifier.simp_add]),
- ((Binding.empty, rec_rewrites), [Code.add_default_eqn_attribute]),
- ((Binding.empty, flat inject), [iff_add]),
- ((Binding.empty, map (fn th => th RS notE) (flat distinct)),
- [Classical.safe_elim NONE]),
- ((Binding.empty, weak_case_congs), [Simplifier.cong_add]),
- ((Binding.empty, flat (distinct @ inject)), [Induct.induct_simp_add])] @
+ |> Global_Theory.note_thmss ""
+ ([((prfx (Binding.name "simps"), []), [(simps, [])]),
+ ((prfx (Binding.name "inducts"), []), [(inducts, [])]),
+ ((prfx (Binding.name "splits"), []), [(maps (fn (x, y) => [x, y]) splits, [])]),
+ ((Binding.empty, [Simplifier.simp_add]),
+ [(flat case_rewrites @ flat distinct @ rec_rewrites, [])]),
+ ((Binding.empty, [Code.add_default_eqn_attribute]), [(rec_rewrites, [])]),
+ ((Binding.empty, [iff_add]), [(flat inject, [])]),
+ ((Binding.empty, [Classical.safe_elim NONE]),
+ [(map (fn th => th RS notE) (flat distinct), [])]),
+ ((Binding.empty, [Simplifier.cong_add]), [(weak_case_congs, [])]),
+ ((Binding.empty, [Induct.induct_simp_add]), [(flat (distinct @ inject), [])])] @
named_rules @ unnamed_rules)
|> snd
|> Datatype_Data.register dt_infos
@@ -116,13 +117,13 @@
val raw_distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct;
val new_type_names = map Long_Name.base_name dt_names;
val prfx = Binding.qualify true (space_implode "_" new_type_names);
- val (((inject, distinct), [induct]), thy2) =
+ val (((inject, distinct), [(_, [induct])]), thy2) =
thy1
|> Datatype_Aux.store_thmss "inject" new_type_names raw_inject
||>> Datatype_Aux.store_thmss "distinct" new_type_names raw_distinct
- ||>> Global_Theory.add_thms
- [((prfx (Binding.name "induct"), raw_induct),
- [Datatype_Data.mk_case_names_induct descr])];
+ ||>> Global_Theory.note_thmss ""
+ [((prfx (Binding.name "induct"), [Datatype_Data.mk_case_names_induct descr]),
+ [([raw_induct], [])])];
in
thy2
|> derive_datatype_props config dt_names [descr] induct inject distinct
--- a/src/HOL/Tools/Function/size.ML Fri Dec 16 12:01:10 2011 +0100
+++ b/src/HOL/Tools/Function/size.ML Fri Dec 16 22:07:03 2011 +0100
@@ -202,12 +202,12 @@
val size_eqns = prove_size_eqs (is_poly thy') size_fns param_size simpset2 @
prove_size_eqs Datatype_Aux.is_rec_type overloaded_size_fns (K NONE) simpset3;
- val ([size_thms], thy'') =
- Global_Theory.add_thmss
- [((Binding.name "size", size_eqns),
- [Simplifier.simp_add, Nitpick_Simps.add,
- Thm.declaration_attribute
- (fn thm => Context.mapping (Code.add_default_eqn thm) I)])] thy';
+ val ([(_, size_thms)], thy'') = thy'
+ |> Global_Theory.note_thmss ""
+ [((Binding.name "size",
+ [Simplifier.simp_add, Nitpick_Simps.add,
+ Thm.declaration_attribute (fn thm => Context.mapping (Code.add_default_eqn thm) I)]),
+ [(size_eqns, [])])];
in
SizeData.map (fold (Symtab.update_new o apsnd (rpair size_thms))
--- a/src/Pure/General/scan.scala Fri Dec 16 12:01:10 2011 +0100
+++ b/src/Pure/General/scan.scala Fri Dec 16 22:07:03 2011 +0100
@@ -79,7 +79,7 @@
/* pseudo Set methods */
- def iterator: Iterator[String] = content(main_tree, Nil).sortWith(_ <= _).iterator
+ def iterator: Iterator[String] = content(main_tree, Nil).sorted.iterator
override def toString: String = iterator.mkString("Lexicon(", ", ", ")")
--- a/src/Pure/PIDE/document.scala Fri Dec 16 12:01:10 2011 +0100
+++ b/src/Pure/PIDE/document.scala Fri Dec 16 22:07:03 2011 +0100
@@ -183,8 +183,7 @@
for (imp <- header.imports; name <- names.get(imp)) yield(name)
case Exn.Exn(_) => Nil
}
- Library.topological_order(next,
- Library.sort_wrt((name: Node.Name) => name.node, nodes.keys.toList))
+ Library.topological_order(next, nodes.keys.toList.sortBy(_.node))
}
}
--- a/src/Pure/System/isabelle_system.scala Fri Dec 16 12:01:10 2011 +0100
+++ b/src/Pure/System/isabelle_system.scala Fri Dec 16 22:07:03 2011 +0100
@@ -297,7 +297,7 @@
for (file <- files if file.isFile) logics += file.getName
}
}
- logics.toList.sortWith(_ < _)
+ logics.toList.sorted
}
--- a/src/Pure/Thy/completion.scala Fri Dec 16 12:01:10 2011 +0100
+++ b/src/Pure/Thy/completion.scala Fri Dec 16 22:07:03 2011 +0100
@@ -96,7 +96,7 @@
case Some(word) =>
words_lex.completions(word).map(words_map(_)) match {
case Nil => None
- case cs => Some(word, cs.sortWith(_ < _))
+ case cs => Some(word, cs.sorted)
}
case None => None
}
--- a/src/Pure/library.scala Fri Dec 16 12:01:10 2011 +0100
+++ b/src/Pure/library.scala Fri Dec 16 22:07:03 2011 +0100
@@ -64,18 +64,6 @@
def split_lines(str: String): List[String] = space_explode('\n', str)
- def sort_wrt[A](key: A => String, args: Seq[A]): List[A] =
- {
- val ordering: Ordering[A] =
- new Ordering[A] { def compare(x: A, y: A): Int = key(x) compare key(y) }
- val a = (new Array[Any](args.length)).asInstanceOf[Array[A]]
- for ((x, i) <- args.iterator zipWithIndex) a(i) = x
- Sorting.quickSort[A](a)(ordering)
- a.toList
- }
-
- def sort_strings(args: Seq[String]): List[String] = sort_wrt((x: String) => x, args)
-
/* iterate over chunks (cf. space_explode) */
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Fri Dec 16 12:01:10 2011 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Fri Dec 16 22:07:03 2011 +0100
@@ -96,7 +96,7 @@
case Some((word, cs)) =>
val ds =
(if (Isabelle_Encoding.is_active(buffer))
- cs.map(Symbol.decode(_)).sortWith(_ < _)
+ cs.map(Symbol.decode(_)).sorted
else cs).filter(_ != word)
if (ds.isEmpty) null
else new SideKickCompletion(
--- a/src/Tools/jEdit/src/plugin.scala Fri Dec 16 12:01:10 2011 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Fri Dec 16 22:07:03 2011 +0100
@@ -379,7 +379,7 @@
filter(file => !loaded_buffer(file) && Isabelle.thy_load.check_file(view, file))
if (!files.isEmpty) {
- val files_list = new ListView(Library.sort_strings(files))
+ val files_list = new ListView(files.sorted)
for (i <- 0 until files.length)
files_list.selection.indices += i