author wenzelm Sat, 10 Mar 2012 23:00:32 +0100 changeset 46864 6eb62a79d02a parent 46863 56376f6be74f (current diff) parent 46862 ef45df55127d (diff) child 46865 659dcbafe4bf
merged
--- a/doc-src/Locales/Locales/Examples.thy	Sat Mar 10 16:39:55 2012 +0100
+++ b/doc-src/Locales/Locales/Examples.thy	Sat Mar 10 23:00:32 2012 +0100
@@ -193,7 +193,8 @@
notions of infimum and supremum for partial orders are introduced,
together with theorems about their uniqueness.  *}

-  context partial_order begin
+  context partial_order
+  begin

definition
is_inf where "is_inf x y i =
--- a/doc-src/Locales/Locales/Examples3.thy	Sat Mar 10 16:39:55 2012 +0100
+++ b/doc-src/Locales/Locales/Examples3.thy	Sat Mar 10 23:00:32 2012 +0100
@@ -10,8 +10,8 @@
discharge the premise in the definition of @{text "op \<sqsubset>"}.  In
general, proofs of the equations not only may involve definitions
from the interpreted locale but arbitrarily complex arguments in the
-  context of the locale.  Therefore is would be convenient to have the
-  interpreted locale conclusions temporary available in the proof.
+  context of the locale.  Therefore it would be convenient to have the
+  interpreted locale conclusions temporarily available in the proof.
This can be achieved by a locale interpretation in the proof body.
The command for local interpretations is \isakeyword{interpret}.  We
repeat the example from the previous section to illustrate this. *}
@@ -304,7 +304,8 @@
second lattice.
*}

-  context lattice_hom begin
+  context lattice_hom
+  begin
abbreviation meet' (infixl "\<sqinter>''" 50) where "meet' \<equiv> le'.meet"
abbreviation join' (infixl "\<squnion>''" 50) where "join' \<equiv> le'.join"
end
@@ -369,7 +370,8 @@
preserving.  As the final example of this section, a locale
interpretation is used to assert this: *}

-  sublocale lattice_hom \<subseteq> order_preserving proof unfold_locales
+  sublocale lattice_hom \<subseteq> order_preserving
+  proof unfold_locales
fix x y
assume "x \<sqsubseteq> y"
then have "y = (x \<squnion> y)" by (simp add: le.join_connection)
@@ -481,7 +483,7 @@
locale fun_lattice = fun_partial_order + lattice

sublocale fun_lattice \<subseteq> f: lattice "\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x"
-    proof unfold_locales
+  proof unfold_locales
fix f g
have "partial_order.is_inf (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x) f g (\<lambda>x. f x \<sqinter> g x)"
apply (rule is_infI) apply rule+ apply (drule spec, assumption)+ done
--- a/doc-src/Locales/Locales/document/Examples.tex	Sat Mar 10 16:39:55 2012 +0100
+++ b/doc-src/Locales/Locales/document/Examples.tex	Sat Mar 10 23:00:32 2012 +0100
@@ -253,7 +253,8 @@
\end{isamarkuptext}%
\isamarkuptrue%
\ \ \isacommand{context}\isamarkupfalse%
-\ partial{\isaliteral{5F}{\isacharunderscore}}order\ \isakeyword{begin}\isanewline
+\ partial{\isaliteral{5F}{\isacharunderscore}}order\isanewline
+\ \ \isakeyword{begin}\isanewline
\isanewline
\ \ \isacommand{definition}\isamarkupfalse%
\isanewline
--- a/doc-src/Locales/Locales/document/Examples3.tex	Sat Mar 10 16:39:55 2012 +0100
+++ b/doc-src/Locales/Locales/document/Examples3.tex	Sat Mar 10 23:00:32 2012 +0100
@@ -34,8 +34,8 @@
discharge the premise in the definition of \isa{op\ {\isaliteral{5C3C73717375627365743E}{\isasymsqsubset}}}.  In
general, proofs of the equations not only may involve definitions
from the interpreted locale but arbitrarily complex arguments in the
-  context of the locale.  Therefore is would be convenient to have the
-  interpreted locale conclusions temporary available in the proof.
+  context of the locale.  Therefore it would be convenient to have the
+  interpreted locale conclusions temporarily available in the proof.
This can be achieved by a locale interpretation in the proof body.
The command for local interpretations is \isakeyword{interpret}.  We
repeat the example from the previous section to illustrate this.%
@@ -439,7 +439,8 @@
\end{isamarkuptext}%
\isamarkuptrue%
\ \ \isacommand{context}\isamarkupfalse%
-\ lattice{\isaliteral{5F}{\isacharunderscore}}hom\ \isakeyword{begin}\isanewline
+\ lattice{\isaliteral{5F}{\isacharunderscore}}hom\isanewline
+\ \ \isakeyword{begin}\isanewline
\ \ \isacommand{abbreviation}\isamarkupfalse%
\ \ \isacommand{abbreviation}\isamarkupfalse%
@@ -513,9 +514,10 @@
\end{isamarkuptext}%
\isamarkuptrue%
\ \ \isacommand{sublocale}\isamarkupfalse%
-\ lattice{\isaliteral{5F}{\isacharunderscore}}hom\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ order{\isaliteral{5F}{\isacharunderscore}}preserving%
+\ lattice{\isaliteral{5F}{\isacharunderscore}}hom\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ order{\isaliteral{5F}{\isacharunderscore}}preserving\isanewline
+%
-\ %
+\ \ %
%
\isatagproof
@@ -738,7 +740,7 @@
\ fun{\isaliteral{5F}{\isacharunderscore}}lattice\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ f{\isaliteral{3A}{\isacharcolon}}\ lattice\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}f\ g{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ f\ x\ {\isaliteral{5C3C737173756273657465713E}{\isasymsqsubseteq}}\ g\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
%
-\ \ \ \ %
+\ \ %
%
\isatagproof
--- a/src/Pure/Isar/class_declaration.ML	Sat Mar 10 16:39:55 2012 +0100
+++ b/src/Pure/Isar/class_declaration.ML	Sat Mar 10 23:00:32 2012 +0100
@@ -74,13 +74,12 @@
val ((_, [thm']), _) = Variable.import true [thm] empty_ctxt;
val const_eq_morph =
(case eq_morph of
-             SOME eq_morph => const_morph $> eq_morph + SOME eq_morph => const_morph$> eq_morph
| NONE => const_morph);
val thm'' = Morphism.thm const_eq_morph thm';
val tac = ALLGOALS (Proof_Context.fact_tac [thm'']);
in Skip_Proof.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end;
-    val assm_intro = Option.map prove_assm_intro
-      (fst (Locale.intros_of thy class));
+    val assm_intro = Option.map prove_assm_intro (fst (Locale.intros_of thy class));

(* of_class *)
val of_class_prop_concl = Logic.mk_of_class (aT, class);
--- a/src/Pure/Isar/element.ML	Sat Mar 10 16:39:55 2012 +0100
+++ b/src/Pure/Isar/element.ML	Sat Mar 10 23:00:32 2012 +0100
@@ -461,11 +461,13 @@

(* rewriting with equalities *)

-fun eq_morphism thy thms = if null thms then NONE else SOME (Morphism.morphism
- {binding = [],
-  typ = [],
-  term = [Raw_Simplifier.rewrite_term thy thms []],
-  fact = [map (Raw_Simplifier.rewrite_rule thms)]});
+fun eq_morphism _ [] = NONE
+  | eq_morphism thy thms =
+      SOME (Morphism.morphism
+       {binding = [],
+        typ = [],
+        term = [Raw_Simplifier.rewrite_term thy thms []],
+        fact = [map (Raw_Simplifier.rewrite_rule thms)]});

(* transfer to theory using closure *)
--- a/src/Pure/Isar/expression.ML	Sat Mar 10 16:39:55 2012 +0100
+++ b/src/Pure/Isar/expression.ML	Sat Mar 10 23:00:32 2012 +0100
@@ -814,17 +814,15 @@

local

-fun note_eqns_register deps witss attrss eqns export export' context =
-  context
-  |> Element.generic_note_thmss Thm.lemmaK
+fun note_eqns_register deps witss attrss eqns export export' =
+  Element.generic_note_thmss Thm.lemmaK
(attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns) - |-> (fn facts => (fn context => meta_rewrite (Context.proof_of context) (maps snd facts))) - |-> (fn eqns => fold (fn ((dep, morph), wits) => + #-> (fn facts => (fn context => meta_rewrite (Context.proof_of context) (maps snd facts))) + #-> (fn eqns => fold (fn ((dep, morph), wits) => fn context => - Locale.add_registration (dep, morph$> Element.satisfy_morphism
-          (map (Element.transform_witness export') wits))
-        (Element.eq_morphism (Context.theory_of context) eqns |>
-          Option.map (rpair true))
+        (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits)) + (Element.eq_morphism (Context.theory_of context) eqns |> Option.map (rpair true)) export context) (deps ~~ witss)); fun gen_interpretation prep_expr parse_prop prep_attr @@ -899,8 +897,7 @@ |> Proof_Context.background_theory (fold (fn ((dep, morph), wits) => fn thy => Locale.add_dependency target - (dep, morph$> Element.satisfy_morphism
-            (map (Element.transform_witness export') wits))
+          (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits)) (Element.eq_morphism thy eqns' |> Option.map (rpair true)) export thy) (deps ~~ witss)) end; --- a/src/Pure/Isar/locale.ML Sat Mar 10 16:39:55 2012 +0100 +++ b/src/Pure/Isar/locale.ML Sat Mar 10 23:00:32 2012 +0100 @@ -99,17 +99,16 @@ lists indexed by registration/dependency serial, entries for empty lists may be omitted *) -fun lookup_mixins serial' mixins = the_default [] (Inttab.lookup mixins serial'); +fun lookup_mixins serial' mixins = Inttab.lookup_list mixins serial'; -fun merge_mixins (mix1, mix2) = Inttab.join (K (Library.merge (eq_snd op =))) (mix1, mix2); +fun merge_mixins mixs : mixins = Inttab.merge_list (eq_snd op =) mixs; -fun insert_mixin serial' mixin = - Inttab.map_default (serial', []) (cons (mixin, serial ())); +fun insert_mixin serial' mixin = Inttab.cons_list (serial', (mixin, serial ())); fun rename_mixin (old, new) mix = - case Inttab.lookup mix old of - NONE => mix | - SOME mxs => Inttab.delete old mix |> Inttab.update_new (new, mxs); + (case Inttab.lookup mix old of + NONE => mix + | SOME mxs => Inttab.delete old mix |> Inttab.update_new (new, mxs)); fun compose_mixins mixins = fold_rev Morphism.compose (map (fst o fst) mixins) Morphism.identity; @@ -241,43 +240,23 @@ (*** Identifiers: activated locales in theory or proof context ***) -(* subsumption *) -fun ident_le thy ((n: string, ts), (m, ss)) = (m = n) andalso Pattern.matchess thy (ss, ts); - (* smaller term is more general *) +type idents = term list list Symtab.table; (* name ~> instance (grouped by name) *) -(* total order *) -fun ident_ord ((n: string, ts), (m, ss)) = - (case fast_string_ord (m, n) of - EQUAL => list_ord Term_Ord.fast_term_ord (ts, ss) - | ord => ord); +val empty_idents : idents = Symtab.empty; +val insert_idents = Symtab.insert_list (eq_list (op aconv)); +val merge_idents = Symtab.merge_list (eq_list (op aconv)); -local +fun redundant_ident thy idents (name, instance) = + exists (fn pat => Pattern.matchess thy (pat, instance)) (Symtab.lookup_list idents name); -datatype 'a delayed = Ready of 'a | ToDo of 'a delayed * 'a delayed; - -structure Identifiers = Generic_Data +structure Idents = Generic_Data ( - type T = (string * term list) list delayed; - val empty = Ready []; + type T = idents; + val empty = empty_idents; val extend = I; - val merge = ToDo; + val merge = merge_idents; ); -fun finish thy (ToDo (i1, i2)) = merge (ident_le thy) (finish thy i1, finish thy i2) - | finish _ (Ready ids) = ids; - -val _ = Context.>> (Context.map_theory (Theory.at_begin (fn thy => - (case Identifiers.get (Context.Theory thy) of - Ready _ => NONE - | ids => SOME (Context.theory_map (Identifiers.put (Ready (finish thy ids))) thy))))); - -in - -val get_idents = (fn Ready ids => ids) o Identifiers.get; -val put_idents = Identifiers.put o Ready; - -end; - (** Resolve locale dependencies in a depth-first fashion **) @@ -292,8 +271,7 @@ let val instance = instance_of thy name (morph$> stem $> export); in - if member (ident_le thy) marked (name, instance) - then (deps, marked) + if redundant_ident thy marked (name, instance) then (deps, marked) else let val full_morph = morph$> compose_mixins mixins $> stem; @@ -301,7 +279,7 @@ val dependencies = dependencies_of thy name |> map (fn ((name', (morph', export')), serial') => (name', morph'$> export', mixins_of thy name serial'));
-          val marked' = (name, instance) :: marked;
+          val marked' = insert_idents (name, instance) marked;
val (deps', marked'') =
fold_rev (add thy (depth + 1) full_morph export) dependencies
([], marked');
@@ -320,12 +298,12 @@
(* Find all dependencies including new ones (which are dependencies enriching
existing registrations). *)
val (dependencies, marked') =
-      add thy 0 Morphism.identity export (name, morph, []) ([], []);
+      add thy 0 Morphism.identity export (name, morph, []) ([], empty_idents);
(* Filter out fragments from marked; these won't be activated. *)
val dependencies' = filter_out (fn (name, morph) =>
-      member (ident_le thy) marked (name, instance_of thy name (morph $> export))) dependencies; + redundant_ident thy marked (name, instance_of thy name (morph$> export))) dependencies;
in
-    (merge (ident_le thy) (marked, marked'), input |> fold_rev activate_dep dependencies')
+    (merge_idents (marked, marked'), input |> fold_rev activate_dep dependencies')
end;

end;
@@ -333,7 +311,9 @@

(*** Registrations: interpretations in theories or proof contexts ***)

-structure Idtab = Table(type key = string * term list val ord = ident_ord);
+val total_ident_ord = prod_ord fast_string_ord (list_ord Term_Ord.fast_term_ord);
+
+structure Idtab = Table(type key = string * term list val ord = total_ident_ord);

structure Registrations = Generic_Data
(
@@ -385,13 +365,15 @@
val thy = Context.theory_of context;
in
roundup thy (fn dep => fn mixins => merge (eq_snd op =) (mixins, get_mixins context dep))
-      Morphism.identity (name, morph) ([(name, instance_of thy name morph)], [])
+      Morphism.identity (name, morph)
+      (insert_idents (name, instance_of thy name morph) empty_idents, [])
|> snd |> filter (snd o fst)  (* only inheritable mixins *)
|> (fn x => merge (eq_snd op =) (x, get_mixins context (name, morph)))
|> compose_mixins
end;

-fun get_registrations context select = Registrations.get context
+fun get_registrations context select =
+  Registrations.get context
|>> Idtab.dest |>> select
(* with inherited mixins *)
|-> (fn regs => fn _ => map (fn ((name, _), ((base, export) ,_)) =>
@@ -454,8 +436,8 @@
let
val thy = Context.theory_of context;
in
-    roundup thy activate_syntax_decls Morphism.identity dep (get_idents context, context)
-    |-> put_idents
+    roundup thy activate_syntax_decls Morphism.identity dep (Idents.get context, context)
+    |-> Idents.put
end);

fun activate_facts export dep context =
@@ -464,14 +446,14 @@
val activate =
activate_notes Element.init (Element.transfer_morphism o Context.theory_of) context export;
in
-    roundup thy activate (case export of NONE => Morphism.identity | SOME export => export)
-      dep (get_idents context, context)
-    |-> put_idents
+    roundup thy activate (the_default Morphism.identity export) dep (Idents.get context, context)
+    |-> Idents.put
end;

fun init name thy =
activate_all name thy Element.init (Element.transfer_morphism o Context.theory_of)
-    ([], Context.Proof (Proof_Context.init_global thy)) |-> put_idents |> Context.proof_of;
+    (empty_idents, Context.Proof (Proof_Context.init_global thy))
+  |-> Idents.put |> Context.proof_of;

(*** Add and extend registrations ***)
@@ -501,10 +483,10 @@
val morph = base_morph $> mix; val inst = instance_of thy name morph; in - if member (ident_le thy) (get_idents context) (name, inst) + if redundant_ident thy (Idents.get context) (name, inst) then context (* FIXME amend mixins? *) else - (get_idents context, context) + (Idents.get context, context) (* add new registrations with inherited mixins *) |> roundup thy (add_reg thy export) export (name, morph) |> snd @@ -526,7 +508,7 @@ val deps = dependencies_of thy loc; in case AList.lookup (fn ((name, morph), ((name', (morph', _)), _)) => - ident_ord ((name, instance_of thy name morph), (name', instance_of thy name' morph')) = EQUAL) deps (name, morph) of + total_ident_ord ((name, instance_of thy name morph), (name', instance_of thy name' morph')) = EQUAL) deps (name, morph) of NONE => error ("Locale " ^ quote (extern thy name) ^ " with\parameter instantiation " ^ space_implode " " (map (quote o Syntax.string_of_term_global thy) morph) ^ @@ -543,8 +525,9 @@ (apfst (cons ((name, (morph, export)), serial')) #> apsnd (case mixin of NONE => I | SOME mixin => insert_mixin serial' mixin)); val context' = Context.Theory thy'; - val (_, regs) = fold_rev (roundup thy' cons export) - (registrations_of context' loc) (get_idents (context'), []); + val (_, regs) = + fold_rev (roundup thy' cons export) + (registrations_of context' loc) (Idents.get context', []); in thy' |> fold_rev (fn dep => Context.theory_map (add_registration dep NONE export)) regs @@ -644,7 +627,7 @@ fun cons_elem (elem as Notes _) = show_facts ? cons elem | cons_elem elem = cons elem; val elems = - activate_all name thy cons_elem (K (Element.transfer_morphism thy)) ([], []) + activate_all name thy cons_elem (K (Element.transfer_morphism thy)) (empty_idents, []) |> snd |> rev; in Pretty.big_list "locale elements:" (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems) @@ -658,23 +641,23 @@ val _ = the_locale thy name; (* error if locale unknown *) in (case registrations_of (Context.Proof ctxt) (* FIXME *) name of - [] => Pretty.str ("no interpretations") + [] => Pretty.str "no interpretations" | regs => Pretty.big_list "interpretations:" (map (pretty_reg ctxt) (rev regs))) end |> Pretty.writeln; fun print_dependencies ctxt clean export insts = let val thy = Proof_Context.theory_of ctxt; - val idents = if clean then [] else get_idents (Context.Proof ctxt); + val idents = if clean then empty_idents else Idents.get (Context.Proof ctxt); in (case fold (roundup thy cons export) insts (idents, []) |> snd of - [] => Pretty.str ("no dependencies") + [] => Pretty.str "no dependencies" | deps => Pretty.big_list "dependencies:" (map (pretty_reg ctxt) (rev deps))) end |> Pretty.writeln; fun locale_deps thy = let - val names = all_locales thy + val names = all_locales thy; fun add_locale_node name = let val params = params_of thy name; @@ -690,7 +673,8 @@ val dependencies = map (apsnd (instance_of thy name o op$>) o fst) (dependencies_of thy name);
in
-        fold (fn (super, ts) => fn (gr, deps) => (gr |> Graph.add_edge (super, name),
+        fold (fn (super, ts) => fn (gr, deps) =>
+         (gr |> Graph.add_edge (super, name),
deps |> Symtab.map_default (super, Symtab.empty) (Symtab.cons_list (name, ts))))
dependencies
end;
--- a/src/Pure/more_thm.ML	Sat Mar 10 16:39:55 2012 +0100
+++ b/src/Pure/more_thm.ML	Sat Mar 10 23:00:32 2012 +0100
@@ -37,7 +37,6 @@
val thm_cache: (thm -> 'a) -> thm -> 'a
val is_reflexive: thm -> bool
val eq_thm: thm * thm -> bool
-  val eq_thms: thm list * thm list -> bool
val eq_thm_thy: thm * thm -> bool
val eq_thm_prop: thm * thm -> bool
val equiv_thm: thm * thm -> bool
@@ -188,8 +187,6 @@
Context.joinable (pairself Thm.theory_of_thm ths) andalso
is_equal (thm_ord ths);

-val eq_thms = eq_list eq_thm;
-
val eq_thm_thy = Theory.eq_thy o pairself Thm.theory_of_thm;
val eq_thm_prop = op aconv o pairself Thm.full_prop_of;

--- a/src/Pure/pattern.ML	Sat Mar 10 16:39:55 2012 +0100
+++ b/src/Pure/pattern.ML	Sat Mar 10 23:00:32 2012 +0100
@@ -399,7 +399,9 @@

fun matches thy po = (match thy po (Vartab.empty, Vartab.empty); true) handle MATCH => false;

-fun matchess thy pos = (fold (match thy) (op ~~ pos) (Vartab.empty, Vartab.empty); true) handle MATCH => false;
+fun matchess thy (ps, os) =
+  length ps = length os andalso
+    ((fold (match thy) (ps ~~ os) (Vartab.empty, Vartab.empty); true) handle MATCH => false);

fun equiv thy (t, u) = matches thy (t, u) andalso matches thy (u, t);

--- a/src/Tools/interpretation_with_defs.ML	Sat Mar 10 16:39:55 2012 +0100
+++ b/src/Tools/interpretation_with_defs.ML	Sat Mar 10 23:00:32 2012 +0100
@@ -17,20 +17,19 @@
structure Interpretation_With_Defs : INTERPRETATION_WITH_DEFS =
struct

-fun note_eqns_register deps witss def_eqns attrss eqns export export' context =
+fun note_eqns_register deps witss def_eqns attrss eqns export export' =
let
fun meta_rewrite context =
map (Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def) o
maps snd;
in
-    context
-    |> Element.generic_note_thmss Thm.lemmaK
+    Element.generic_note_thmss Thm.lemmaK
(attrss ~~ map (fn eqn => [([Morphism.thm (export' $> export) eqn], [])]) eqns) - |-> (fn facts => (fn context => meta_rewrite context facts)) - |-> (fn eqns => fold (fn ((dep, morph), wits) => + #-> (fn facts => (fn context => meta_rewrite context facts)) + #-> (fn eqns => fold (fn ((dep, morph), wits) => fn context => - Locale.add_registration (dep, morph$> Element.satisfy_morphism
-            (map (Element.transform_witness export') wits))
export context) (deps ~~ witss))