--- a/src/FOL/ex/LocaleTest.thy Thu Jan 15 12:55:38 2009 +0000
+++ b/src/FOL/ex/LocaleTest.thy Thu Jan 15 14:52:35 2009 +0100
@@ -1,7 +1,7 @@
(* Title: FOL/ex/NewLocaleTest.thy
Author: Clemens Ballarin, TU Muenchen
-Testing environment for locale expressions --- experimental.
+Testing environment for locale expressions.
*)
theory LocaleTest
@@ -483,4 +483,6 @@
thm local_free.lone [where ?zero = 0]
qed
+ML_val {* reset Toplevel.debug *}
+
end
--- a/src/HOL/Library/LaTeXsugar.thy Thu Jan 15 12:55:38 2009 +0000
+++ b/src/HOL/Library/LaTeXsugar.thy Thu Jan 15 14:52:35 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Library/LaTeXsugar.thy
- ID: $Id$
Author: Gerwin Klain, Tobias Nipkow, Norbert Schirmer
Copyright 2005 NICTA and TUM
*)
--- a/src/HOL/Library/OptionalSugar.thy Thu Jan 15 12:55:38 2009 +0000
+++ b/src/HOL/Library/OptionalSugar.thy Thu Jan 15 14:52:35 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Library/OptionalSugar.thy
- ID: $Id$
Author: Gerwin Klain, Tobias Nipkow
Copyright 2005 NICTA and TUM
*)
@@ -37,6 +36,36 @@
"_bind (p#DUMMY) e" <= "_bind p (hd e)"
"_bind (DUMMY#p) e" <= "_bind p (tl e)"
+(* type constraints with spacing *)
+setup {*
+let
+ val typ = SimpleSyntax.read_typ;
+ val typeT = Syntax.typeT;
+ val spropT = Syntax.spropT;
+in
+ Sign.del_modesyntax_i (Symbol.xsymbolsN, false) [
+ ("_constrain", typ "logic => type => logic", Mixfix ("_\<Colon>_", [4, 0], 3)),
+ ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_\<Colon>_", [4, 0], 3))]
+ #> Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [
+ ("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon> _", [4, 0], 3)),
+ ("_constrain", [spropT, typeT] ---> spropT, Mixfix ("_ \<Colon> _", [4, 0], 3))]
+end
+*}
+
+(* sorts as intersections *)
+setup {*
+let
+ val sortT = Type ("sort", []); (*FIXME*)
+ val classesT = Type ("classes", []); (*FIXME*)
+in
+ Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [
+ ("_topsort", sortT, Mixfix ("\<top>", [], Syntax.max_pri)),
+ ("_sort", classesT --> sortT, Mixfix ("'(_')", [], Syntax.max_pri)),
+ ("_classes", Lexicon.idT --> classesT --> classesT, Mixfix ("_ \<inter> _", [], Syntax.max_pri)),
+ ("_classes", Lexicon.longidT --> classesT --> classesT, Mixfix ("_ \<inter> _", [], Syntax.max_pri))
+ ]
+end
+*}
end
(*>*)
--- a/src/HOL/Tools/function_package/size.ML Thu Jan 15 12:55:38 2009 +0000
+++ b/src/HOL/Tools/function_package/size.ML Thu Jan 15 14:52:35 2009 +0100
@@ -1,6 +1,5 @@
(* Title: HOL/Tools/function_package/size.ML
- ID: $Id$
- Author: Stefan Berghofer, Florian Haftmann, TU Muenchen
+ Author: Stefan Berghofer, Florian Haftmann & Alexander Krauss, TU Muenchen
Size functions for datatypes.
*)
@@ -81,7 +80,7 @@
val param_size = AList.lookup op = param_size_fs;
val extra_rewrites = descr |> map (#1 o snd) |> distinct op = |>
- List.mapPartial (Option.map snd o lookup_size thy) |> flat;
+ map_filter (Option.map snd o lookup_size thy) |> flat;
val extra_size = Option.map fst o lookup_size thy;
val (((size_names, size_fns), def_names), def_names') =
@@ -180,7 +179,7 @@
let
val Ts = map (typ_of_dtyp descr sorts) cargs;
val tnames = Name.variant_list f_names (DatatypeProp.make_tnames Ts);
- val ts = List.mapPartial (fn (sT as (s, T), dt) =>
+ val ts = map_filter (fn (sT as (s, T), dt) =>
Option.map (fn sz => sz $ Free sT)
(if p dt then size_of_type size_of extra_size size_ofp T
else NONE)) (tnames ~~ Ts ~~ cargs)
--- a/src/Pure/Isar/expression.ML Thu Jan 15 12:55:38 2009 +0000
+++ b/src/Pure/Isar/expression.ML Thu Jan 15 14:52:35 2009 +0100
@@ -26,6 +26,8 @@
(* Interpretation *)
val cert_goal_expression: expression_i -> Proof.context ->
(term list list * (string * morphism) list * morphism) * Proof.context;
+ val read_goal_expression: expression -> Proof.context ->
+ (term list list * (string * morphism) list * morphism) * Proof.context;
val sublocale: string -> expression_i -> theory -> Proof.state;
val sublocale_cmd: string -> expression -> theory -> Proof.state;
@@ -812,21 +814,17 @@
local
-datatype goal = Reg of string * Morphism.morphism | Eqns of Attrib.binding list;
-
fun gen_interpretation prep_expr parse_prop prep_attr
- expression equations thy =
+ expression equations theory =
let
- val ctxt = ProofContext.init thy;
-
- val ((propss, regs, export), expr_ctxt) = prep_expr expression ctxt;
+ val ((propss, regs, export), expr_ctxt) = ProofContext.init theory
+ |> prep_expr expression;
val eqns = map (parse_prop expr_ctxt o snd) equations |> Syntax.check_terms expr_ctxt;
- val eq_attns = map ((apsnd o map) (prep_attr thy) o fst) equations;
+ val eq_attns = map ((apsnd o map) (prep_attr theory) o fst) equations;
val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt;
val export' = Variable.export_morphism goal_ctxt expr_ctxt;
- (*** alternative code -- unclear why it does not work yet ***)
fun store_reg ((name, morph), thms) thy =
let
val thms' = map (Element.morph_witness export') thms;
@@ -841,7 +839,7 @@
thy
|> fold (fn (name, morph) =>
Locale.activate_global_facts (name, morph $> export)) regs
- | store_eqns_activate regs thms thys =
+ | store_eqns_activate regs thms thy =
let
val thms' = thms |> map (Element.conclude_witness #>
Morphism.thm (export' $> export) #>
@@ -866,40 +864,7 @@
in ProofContext.theory (fold_map store_reg (regs ~~ wits_reg)
#-> (fn regs => store_eqns_activate regs wits_eq))
end;
- (*** alternative code end ***)
- fun store (Reg (name, morph), thms) (regs, thy) =
- let
- val thms' = map (Element.morph_witness export') thms;
- val morph' = morph $> Element.satisfy_morphism thms';
- val add = Locale.add_registration (name, (morph', export));
- in ((name, morph') :: regs, add thy) end
- | store (Eqns [], []) (regs, thy) =
- let val add = fold_rev (fn (name, morph) =>
- Locale.activate_global_facts (name, morph $> export)) regs;
- in (regs, add thy) end
- | store (Eqns attns, thms) (regs, thy) =
- let
- val thms' = thms |> map (Element.conclude_witness #>
- Morphism.thm (export' $> export) #>
- LocalDefs.meta_rewrite_rule (ProofContext.init thy) #>
- Drule.abs_def);
- val eq_morph =
- Morphism.term_morphism (MetaSimplifier.rewrite_term thy thms' []) $>
- Morphism.thm_morphism (MetaSimplifier.rewrite_rule thms');
- val attns' = map ((apsnd o map) (Attrib.attribute_i thy)) attns;
- val add =
- fold_rev (fn (name, morph) =>
- Locale.amend_registration eq_morph (name, morph) #>
- Locale.activate_global_facts (name, morph $> eq_morph $> export)) regs #>
- PureThy.note_thmss Thm.lemmaK (attns' ~~ map (fn th => [([th], [])]) thms') #>
- snd
- in (regs, add thy) end;
-
- fun after_qed results =
- ProofContext.theory (fn thy =>
- fold store (map Reg regs @ [Eqns eq_attns] ~~
- prep_result (propss @ [eqns]) results) ([], thy) |> snd);
in
goal_ctxt |>
Proof.theorem_i NONE after_qed (prep_propp (propss @ [eqns])) |>
--- a/src/Pure/Thy/present.ML Thu Jan 15 12:55:38 2009 +0000
+++ b/src/Pure/Thy/present.ML Thu Jan 15 14:52:35 2009 +0100
@@ -467,7 +467,7 @@
val _ = add_file (Path.append html_prefix base_html,
HTML.ml_file (Url.File base) (File.read path));
in (Url.File base_html, Url.File raw_path, loadit) end
- | NONE => error ("Browser info: expected to find ML file" ^ quote (Path.implode raw_path)));
+ | NONE => error ("Browser info: expected to find ML file " ^ quote (Path.implode raw_path)));
val files_html = map prep_file files;