--- a/CONTRIBUTORS Tue Oct 26 11:15:40 2021 +0100
+++ b/CONTRIBUTORS Tue Oct 26 16:22:03 2021 +0100
@@ -22,6 +22,9 @@
complex numbers (theory HOL-Library.Complex_Order), and products of uniform
spaces (theory HOL-Analysis.Product_Vector).
+* November 2020 / July 2021: Norbert Schirmer, Apple
+ Various improvements and cleanup of session "HOL-Statespace".
+
* July 2021: Florian Haftmann
Further consolidation of bit operations and word types.
--- a/NEWS Tue Oct 26 11:15:40 2021 +0100
+++ b/NEWS Tue Oct 26 16:22:03 2021 +0100
@@ -287,6 +287,8 @@
* Theory "HOL-Combinatorics.Transposition" provides elementary swap
operation "transpose".
+* Session "HOL-Statespace": various improvements and cleanup.
+
*** ML ***
--- a/src/HOL/Statespace/StateSpaceEx.thy Tue Oct 26 11:15:40 2021 +0100
+++ b/src/HOL/Statespace/StateSpaceEx.thy Tue Oct 26 16:22:03 2021 +0100
@@ -1,5 +1,6 @@
(* Title: HOL/Statespace/StateSpaceEx.thy
- Author: Norbert Schirmer, TU Muenchen
+ Author: Norbert Schirmer, TU Muenchen, 2007
+ Author: Norbert Schirmer, Apple, 2021
*)
section \<open>Examples \label{sec:Examples}\<close>
@@ -12,6 +13,7 @@
"_statespace_updates" :: "('a \<Rightarrow> 'b) \<Rightarrow> updbinds \<Rightarrow> ('a \<Rightarrow> 'b)" ("_\<langle>_\<rangle>" [900,0] 900)
(*>*)
+
text \<open>Did you ever dream about records with multiple inheritance?
Then you should definitely have a look at statespaces. They may be
what you are dreaming of. Or at least almost \dots\<close>
@@ -31,7 +33,7 @@
text \<open>\noindent This resembles a \<^theory_text>\<open>record\<close> definition,
but introduces sophisticated locale
-infrastructure instead of HOL type schemes. The resulting context
+infrastructure instead of HOL type schemes. The resulting context
postulates two distinct names \<^term>\<open>n\<close> and \<^term>\<open>b\<close> and
projection~/ injection functions that convert from abstract values to
\<^typ>\<open>nat\<close> and \<open>bool\<close>. The logical content of the locale is:\<close>
@@ -52,17 +54,12 @@
locale. We also maintain non-logical context information to support
the user:
-\begin{itemize}
-
-\item Syntax for state lookup and updates that automatically inserts
+\<^item> Syntax for state lookup and updates that automatically inserts
the corresponding projection and injection functions.
-
-\item Setup for the proof tools that exploit the distinctness
+\<^item> Setup for the proof tools that exploit the distinctness
information and the cancellation of projections and injections in
deductions and simplifications.
-\end{itemize}
-
This extra-logical information is added to the locale in form of
declarations, which associate the name of a variable to the
corresponding projection and injection functions to handle the syntax
@@ -71,8 +68,9 @@
extended there are multiple distinctness theorems in the context. Our
declarations take care that the link always points to the strongest
distinctness assumption. With these declarations in place, a lookup
-can be written as \<open>s\<cdot>n\<close>, which is translated to \<open>project_nat (s n)\<close>, and an update as \<open>s\<langle>n := 2\<rangle>\<close>, which is
-translated to \<open>s(n := inject_nat 2)\<close>. We can now establish the
+can be written as \<open>s\<cdot>n\<close>, which is translated to \<open>project_nat (s n)\<close>, and an
+update as \<open>s\<langle>n := 2\<rangle>\<close>, which is translated to \<open>s(n := inject_nat 2)\<close>.
+We can now establish the
following lemma:\<close>
lemma (in vars) foo: "s<n := 2>\<cdot>b = s\<cdot>b" by simp
@@ -91,7 +89,8 @@
\<^typ>\<open>'a\<close>. This type is fixed inside the state space but may get
instantiated later on, analogous to type parameters of an ML-functor.
The distinctness assumption is now \<open>distinct [N, B, n, b, x]\<close>,
-from this we can derive both \<^term>\<open>distinct [N,B]\<close> and \<^term>\<open>distinct [n,b]\<close>, the distinction assumptions for the two versions of
+from this we can derive both \<^term>\<open>distinct [N,B]\<close> and \<^term>\<open>distinct [n,b]\<close>,
+the distinction assumptions for the two versions of
locale \<open>vars\<close> above. Moreover we have all necessary
projection and injection assumptions available. These assumptions
together allow us to establish state space \<^term>\<open>varsX\<close> as an
@@ -111,8 +110,8 @@
we get logarithmic certificates for the distinctness of two names by
the distinctness of the paths in the tree. Asked for the distinctness
of two names, our tool produces the paths of the variables in the tree
-(this is implemented in SML, outside the logic) and returns a
-certificate corresponding to the different paths. Merging state
+(this is implemented in Isabelle/ML, outside the logic) and returns a
+certificate corresponding to the different paths. Merging state
spaces requires to prove that the combined distinctness assumption
implies the distinctness assumptions of the components. Such a proof
is of the order $m \cdot \log n$, where $n$ and $m$ are the number of
@@ -192,39 +191,70 @@
shows "s<A := i>\<cdot>x = s\<cdot>x"
by simp
-
-(*
-text "Hmm, I hoped this would work now..."
+text \<open>There were known problems with syntax-declarations. They only
+worked when the context is already completely built. This is now overcome. e.g.:\<close>
locale fooX = foo +
assumes "s<a:=i>\<cdot>b = k"
-*)
+
+
+
+text \<open>
+We can also put statespaces side-by-side by using ordinary @{command locale} expressions
+(instead of the @{command statespace}).
+\<close>
+
+
+locale side_by_side = foo + bar where b="B::'a" and c=C for B C
-(* ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ *)
-text \<open>There are known problems with syntax-declarations. They currently
-only work, when the context is already built. Hopefully this will be
-implemented correctly in future Isabelle versions.\<close>
+context side_by_side
+begin
+text \<open>Simplification within one of the statespaces works as expected.\<close>
+lemma "s<B := i>\<cdot>C = s\<cdot>C"
+ by simp
+
+lemma "s<a := i>\<cdot>b = s\<cdot>b"
+ by simp
+
+text \<open>In contrast to the statespace @{locale loo} there is no 'inter' statespace distinctness
+between the names of @{locale foo} and @{locale bar}.\<close>
+end
+
+
+text \<open>Sharing of names in side-by-side statespaces is also possible as long as they are mapped
+to the same type.}\<close>
-(*
-lemma
- assumes "foo f a b c p1 i1 p2 i2 p3 i3 p4 i4"
- shows True
-proof
- interpret foo [f a b c p1 i1 p2 i2 p3 i3 p4 i4] by fact
- term "s<a := i>\<cdot>a = i"
-qed
-*)
-(*
-lemma
- includes foo
- shows "s<a := i>\<cdot>a = i"
-*)
+statespace vars1 = n::nat m::nat
+statespace vars2 = n::nat k::nat
+
+locale vars1_vars2 = vars1 + vars2
+
+context vars1_vars2
+begin
+
+text \<open>Note that the distinctness theorem for @{locale vars1} is selected here to do the proof.\<close>
+lemma "s<n := i>\<cdot>m = s\<cdot>m"
+ by simp
+
+text \<open>Note that the distinctness theorem for @{locale vars2} is selected here to do the proof.\<close>
+lemma "s<n := i>\<cdot>k = s\<cdot>k"
+ by simp
-text \<open>It would be nice to have nested state spaces. This is
-logically no problem. From the locale-implementation side this may be
-something like an 'includes' into a locale. When there is a more
-elaborate locale infrastructure in place this may be an easy exercise.
-\<close>
+text \<open>Still there is no inter-statespace distinctness.\<close>
+lemma "s<k := i>\<cdot>m = s\<cdot>m"
+ (* apply simp *)
+ oops
+end
+
+statespace merge_vars1_vars2 = vars1 + vars2
+
+context merge_vars1_vars2
+begin
+text \<open>When defining a statespace instead of a side-by-side locale we get the distinctness of
+all variables.\<close>
+lemma "s<k := i>\<cdot>m = s\<cdot>m"
+ by simp
+end
subsection \<open>Benchmarks\<close>
--- a/src/HOL/Statespace/distinct_tree_prover.ML Tue Oct 26 11:15:40 2021 +0100
+++ b/src/HOL/Statespace/distinct_tree_prover.ML Tue Oct 26 16:22:03 2021 +0100
@@ -1,5 +1,6 @@
(* Title: HOL/Statespace/distinct_tree_prover.ML
- Author: Norbert Schirmer, TU Muenchen
+ Author: Norbert Schirmer, TU Muenchen, 2007
+ Author: Norbert Schirmer, Apple, 2021
*)
signature DISTINCT_TREE_PROVER =
@@ -9,6 +10,8 @@
val dest_tree : term -> term list
val find_tree : term -> term -> direction list option
+ val in_set: Proof.context -> direction list -> cterm -> thm
+ val find_in_set: Proof.context -> term -> cterm -> thm
val neq_to_eq_False : thm
val distinctTreeProver : Proof.context -> thm -> direction list -> direction list -> thm
val neq_x_y : Proof.context -> term -> term -> string -> thm option
@@ -188,6 +191,41 @@
in (x, l) end;
in
+
+fun in_set ctxt ps tree =
+ let
+ val in_set = in_set ctxt
+ val (_, [l, x, _, r]) = Drule.strip_comb tree;
+ val xT = Thm.ctyp_of_cterm x;
+ in
+ (case ps of
+ [] =>
+ instantiate ctxt
+ [(Thm.ctyp_of_cterm x_in_set_root, xT)]
+ [(l_in_set_root, l), (x_in_set_root, x), (r_in_set_root, r)] @{thm in_set_root}
+ | Left :: ps' =>
+ let
+ val in_set_l = in_set ps' l;
+ val in_set_left' =
+ instantiate ctxt
+ [(Thm.ctyp_of_cterm x_in_set_left, xT)]
+ [(x_in_set_left, x), (r_in_set_left, r)] @{thm in_set_left};
+ in discharge ctxt [in_set_l] in_set_left' end
+ | Right :: ps' =>
+ let
+ val in_set_r = in_set ps' r;
+ val in_set_right' =
+ instantiate ctxt
+ [(Thm.ctyp_of_cterm x_in_set_right, xT)]
+ [(x_in_set_right, x), (l_in_set_right, l)] @{thm in_set_right};
+ in discharge ctxt [in_set_r] in_set_right' end)
+ end;
+
+fun find_in_set ctxt t ct =
+ case find_tree t (Thm.term_of ct) of
+ SOME ps => in_set ctxt ps ct
+ | NONE => raise TERM ("find_in_set", [t, Thm.term_of ct])
+
(*
1. First get paths x_path y_path of x and y in the tree.
2. For the common prefix descend into the tree according to the path
@@ -210,34 +248,7 @@
val subtree = Thm.cprop_of dist_subtree_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
val (_, [l, _, _, r]) = Drule.strip_comb subtree;
- fun in_set ps tree =
- let
- val (_, [l, x, _, r]) = Drule.strip_comb tree;
- val xT = Thm.ctyp_of_cterm x;
- in
- (case ps of
- [] =>
- instantiate ctxt
- [(Thm.ctyp_of_cterm x_in_set_root, xT)]
- [(l_in_set_root, l), (x_in_set_root, x), (r_in_set_root, r)] @{thm in_set_root}
- | Left :: ps' =>
- let
- val in_set_l = in_set ps' l;
- val in_set_left' =
- instantiate ctxt
- [(Thm.ctyp_of_cterm x_in_set_left, xT)]
- [(x_in_set_left, x), (r_in_set_left, r)] @{thm in_set_left};
- in discharge ctxt [in_set_l] in_set_left' end
- | Right :: ps' =>
- let
- val in_set_r = in_set ps' r;
- val in_set_right' =
- instantiate ctxt
- [(Thm.ctyp_of_cterm x_in_set_right, xT)]
- [(x_in_set_right, x), (l_in_set_right, l)] @{thm in_set_right};
- in discharge ctxt [in_set_r] in_set_right' end)
- end;
-
+ val in_set = in_set ctxt
fun in_set' [] = raise TERM ("distinctTreeProver", [])
| in_set' (Left :: ps) = in_set ps l
| in_set' (Right :: ps) = in_set ps r;
--- a/src/HOL/Statespace/state_fun.ML Tue Oct 26 11:15:40 2021 +0100
+++ b/src/HOL/Statespace/state_fun.ML Tue Oct 26 16:22:03 2021 +0100
@@ -1,5 +1,6 @@
(* Title: HOL/Statespace/state_fun.ML
- Author: Norbert Schirmer, TU Muenchen
+ Author: Norbert Schirmer, TU Muenchen, 2007
+ Author: Norbert Schirmer, Apple, 2021
*)
signature STATE_FUN =
@@ -16,6 +17,8 @@
val ex_lookup_ss : simpset
val lazy_conj_simproc : simproc
val string_eq_simp_tac : Proof.context -> int -> tactic
+
+ val trace_data : Context.generic -> unit
end;
structure StateFun: STATE_FUN =
@@ -105,6 +108,17 @@
(merge_ss (ss1, ss2), merge_ss (ex_ss1, ex_ss2), b1 orelse b2);
);
+fun trace_data context =
+ let
+ val (lookup_ss, ex_ss, active) = Data.get context
+ val pretty_ex_ss = Simplifier.pretty_simpset true (put_simpset ex_ss (Context.proof_of context))
+ val pretty_lookup_ss = Simplifier.pretty_simpset true (put_simpset lookup_ss (Context.proof_of context))
+ in
+ tracing ("state_fun ex_ss: " ^ Pretty.string_of pretty_ex_ss ^
+ "\n ================= \n lookup_ss: " ^ Pretty.string_of pretty_lookup_ss ^ "\n " ^
+ "active: " ^ @{make_string} active)
+ end
+
val _ = Theory.setup (Context.theory_map (Data.put (lookup_ss, ex_lookup_ss, false)));
val lookup_simproc =
--- a/src/HOL/Statespace/state_space.ML Tue Oct 26 11:15:40 2021 +0100
+++ b/src/HOL/Statespace/state_space.ML Tue Oct 26 16:22:03 2021 +0100
@@ -1,5 +1,6 @@
(* Title: HOL/Statespace/state_space.ML
- Author: Norbert Schirmer, TU Muenchen
+ Author: Norbert Schirmer, TU Muenchen, 2007
+ Author: Norbert Schirmer, Apple, 2021
*)
signature STATE_SPACE =
@@ -42,19 +43,31 @@
val distinct_simproc : Simplifier.simproc
- val get_comp : Context.generic -> string -> (typ * string) option
+ val is_statespace : Context.generic -> xstring -> bool
+
+ val get_comp' : Context.generic -> string -> (typ * string list) option
+ val get_comp : Context.generic -> string -> (typ * string) option (* legacy wrapper, eventually replace by primed version *)
+ val get_comps : Context.generic -> (typ * string list) Termtab.table
+
val get_silent : Context.generic -> bool
val set_silent : bool -> Context.generic -> Context.generic
+
val gen_lookup_tr : Proof.context -> term -> string -> term
val lookup_swap_tr : Proof.context -> term list -> term
val lookup_tr : Proof.context -> term list -> term
val lookup_tr' : Proof.context -> term list -> term
- val gen_update_tr :
- bool -> Proof.context -> string -> term -> term -> term
+ val gen'_update_tr :
+ bool -> bool -> Proof.context -> string -> term -> term -> term
+ val gen_update_tr : (* legacy wrapper, eventually replace by primed version *)
+ bool -> Proof.context -> string -> term -> term -> term
+
val update_tr : Proof.context -> term list -> term
val update_tr' : Proof.context -> term list -> term
+
+ val trace_name_space_data: Context.generic -> unit
+ val trace_state_space_data: Context.generic -> unit
end;
structure StateSpace : STATE_SPACE =
@@ -83,11 +96,66 @@
| sorted_subset eq (x::xs) (y::ys) = if eq (x,y) then sorted_subset eq xs ys
else sorted_subset eq (x::xs) ys;
+fun comps_of_distinct_thm thm = Thm.prop_of thm
+ |> (fn (_$(_$t)) => DistinctTreeProver.dest_tree t) |> map (fst o dest_Free) |> sort_strings;
+
+fun insert_tagged_distinct_thms tagged_thm tagged_thms =
+ let
+ fun ins t1 [] = [t1]
+ | ins (t1 as (names1, _)) ((t2 as (names2, _))::thms) =
+ if Ord_List.subset string_ord (names1, names2) then t2::thms
+ else if Ord_List.subset string_ord (names2, names1) then ins t1 thms
+ else t2 :: ins t1 thms
+ in
+ ins tagged_thm tagged_thms
+ end
+
+fun join_tagged_distinct_thms tagged_thms1 tagged_thms2 =
+ tagged_thms1 |> fold insert_tagged_distinct_thms tagged_thms2
+
+fun tag_distinct_thm thm = (comps_of_distinct_thm thm, thm)
+val tag_distinct_thms = map tag_distinct_thm
+
+fun join_distinct_thms thms1 thms2 =
+ if pointer_eq (thms1, thms2) then thms1
+ else join_tagged_distinct_thms (tag_distinct_thms thms1) (tag_distinct_thms thms2)
+ |> map snd
+
+fun insert_distinct_thm thm thms = join_distinct_thms thms [thm]
+
+val join_distinctthm_tab = Symtab.join (fn name => fn (thms1, thms2) => join_distinct_thms thms1 thms2)
+fun join_declinfo_entry name (T1:typ, names1:string list) (T2, names2) =
+ let
+ fun typ_info T names = @{make_string} T ^ " " ^ Pretty.string_of (Pretty.str_list "(" ")" names);
+ in
+ if T1 = T2 then (T1, distinct (op =) (names1 @ names2))
+ else error ("statespace component '" ^ name ^ "' disagrees on type:\n " ^
+ typ_info T1 names1 ^ " vs. " ^ typ_info T2 names2
+ )
+ end
+fun guess_name (Free (x,_)) = x
+ | guess_name _ = "unknown"
+
+val join_declinfo = Termtab.join (fn trm => uncurry (join_declinfo_entry (guess_name trm)))
+
+
+(*
+ A component might appear in *different* statespaces within the same context. However, it must
+ be mapped to the same type. Note that this information is currently only properly maintained
+ within contexts where all components are actually "fixes" and not arbitrary terms. Moreover, on
+ the theory level the info stays empty.
+
+ This means that on the theory level we do not make use of the syntax and the tree-based distinct simprocs.
+ N.B: It might still make sense (from a performance perspective) to overcome this limitation
+ and even use the simprocs when a statespace is interpreted for concrete names like HOL-strings.
+ Once the distinct-theorem is proven by the interpretation the simproc can use the positions in
+ the tree to derive distinctness of two strings vs. HOL-string comparison.
+ *)
type namespace_info =
- {declinfo: (typ*string) Termtab.table, (* type, name of statespace *)
- distinctthm: thm Symtab.table,
+ {declinfo: (typ * string list) Termtab.table, (* type, names of statespaces of component *)
+ distinctthm: thm list Symtab.table, (* minimal list of maximal distinctness-assumptions for a component name *)
silent: bool
};
@@ -98,19 +166,24 @@
fun merge
({declinfo=declinfo1, distinctthm=distinctthm1, silent=silent1},
{declinfo=declinfo2, distinctthm=distinctthm2, silent=silent2}) : T =
- {declinfo = Termtab.merge (K true) (declinfo1, declinfo2),
- distinctthm = Symtab.merge (K true) (distinctthm1, distinctthm2),
+ {declinfo = join_declinfo (declinfo1, declinfo2),
+ distinctthm = join_distinctthm_tab (distinctthm1, distinctthm2),
silent = silent1 andalso silent2 (* FIXME odd merge *)}
);
+fun trace_name_space_data context =
+ tracing ("NameSpaceData: " ^ @{make_string} (NameSpaceData.get context))
+
fun make_namespace_data declinfo distinctthm silent =
{declinfo=declinfo,distinctthm=distinctthm,silent=silent};
fun update_declinfo (n,v) ctxt =
- let val {declinfo,distinctthm,silent} = NameSpaceData.get ctxt;
+ let
+ val {declinfo,distinctthm,silent} = NameSpaceData.get ctxt;
+ val v = apsnd single v
in NameSpaceData.put
- (make_namespace_data (Termtab.update (n,v) declinfo) distinctthm silent) ctxt
+ (make_namespace_data (Termtab.map_default (n,v) (join_declinfo_entry (guess_name n) v) declinfo) distinctthm silent) ctxt
end;
fun set_silent silent ctxt =
@@ -158,6 +231,12 @@
fun merge data : T = Symtab.merge (K true) data;
);
+fun is_statespace context name =
+ Symtab.defined (StateSpaceData.get context) (Locale.intern (Context.theory_of context) name)
+
+fun trace_state_space_data context =
+ tracing ("StateSpaceData: " ^ @{make_string} (StateSpaceData.get context))
+
fun add_statespace name args parents components types ctxt =
StateSpaceData.put
(Symtab.update_new (name, {args=args,parents=parents,
@@ -171,27 +250,58 @@
fun mk_free ctxt name =
if Variable.is_fixed ctxt name orelse Variable.is_declared ctxt name
then
- let val n' = Variable.intern_fixed ctxt name |> perhaps Long_Name.dest_hidden;
- in SOME (Free (n', Proof_Context.infer_type ctxt (n', dummyT))) end
- else NONE
+ let
+ val n' = Variable.intern_fixed ctxt name |> perhaps Long_Name.dest_hidden;
+ val free = Free (n', Proof_Context.infer_type ctxt (n', dummyT))
+ in SOME (free) end
+ else (tracing ("variable not fixed or declared: " ^ name); NONE)
fun get_dist_thm ctxt name = Symtab.lookup (#distinctthm (NameSpaceData.get ctxt)) name;
+
+fun get_dist_thm2 ctxt x y =
+ (let
+ val dist_thms = [x, y] |> map (#1 o dest_Free)
+ |> map (these o get_dist_thm (Context.Proof ctxt)) |> flat;
+
+ fun get_paths dist_thm =
+ let
+ val ctree = Thm.cprop_of dist_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
+ val tree = Thm.term_of ctree;
+ val x_path = the (DistinctTreeProver.find_tree x tree);
+ val y_path = the (DistinctTreeProver.find_tree y tree);
+ in SOME (dist_thm, x_path, y_path) end
+ handle Option.Option => NONE
+
+ val result = get_first get_paths dist_thms
+ in
+ result
+ end)
+
+
+fun get_comp' ctxt name =
+ mk_free (Context.proof_of ctxt) name
+ |> Option.mapPartial (fn t =>
+ let
+ val declinfo = #declinfo (NameSpaceData.get ctxt)
+ in
+ case Termtab.lookup declinfo t of
+ NONE => (* during syntax phase, types of fixes might not yet be constrained completely *)
+ AList.lookup (fn (x, Free (n,_)) => n = x | _ => false) (Termtab.dest declinfo) name
+ | some => some
+ end)
+
+(* legacy wrapper *)
fun get_comp ctxt name =
- Option.mapPartial
- (Termtab.lookup (#declinfo (NameSpaceData.get ctxt)))
- (mk_free (Context.proof_of ctxt) name);
+ get_comp' ctxt name |> Option.map (apsnd (fn ns => if null ns then "" else hd ns))
+fun get_comps ctxt = #declinfo (NameSpaceData.get ctxt)
(*** Tactics ***)
fun neq_x_y ctxt x y =
(let
- val dist_thm = the (get_dist_thm (Context.Proof ctxt) (#1 (dest_Free x)));
- val ctree = Thm.cprop_of dist_thm |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
- val tree = Thm.term_of ctree;
- val x_path = the (DistinctTreeProver.find_tree x tree);
- val y_path = the (DistinctTreeProver.find_tree y tree);
+ val (dist_thm, x_path, y_path) = the (get_dist_thm2 ctxt x y);
val thm = DistinctTreeProver.distinctTreeProver ctxt dist_thm x_path y_path;
in SOME thm
end handle Option.Option => NONE)
@@ -240,8 +350,6 @@
val dist_thm_name = distinct_compsN;
val dist_thm_full_name = dist_thm_name;
- fun comps_of_thm thm = Thm.prop_of thm
- |> (fn (_$(_$t)) => DistinctTreeProver.dest_tree t) |> map (fst o dest_Free);
fun type_attr phi = Thm.declaration_attribute (fn thm => fn context =>
(case context of
@@ -249,12 +357,8 @@
| Context.Proof ctxt =>
let
val {declinfo,distinctthm=tt,silent} = NameSpaceData.get context;
- val all_names = comps_of_thm thm;
- fun upd name tt =
- (case Symtab.lookup tt name of
- SOME dthm => if sorted_subset (op =) (comps_of_thm dthm) all_names
- then Symtab.update (name,thm) tt else tt
- | NONE => Symtab.update (name,thm) tt)
+ val all_names = comps_of_distinct_thm thm;
+ fun upd name = Symtab.map_default (name, [thm]) (fn thms => insert_distinct_thm thm thms)
val tt' = tt |> fold upd all_names;
val context' =
@@ -377,7 +481,8 @@
in Context.proof_map
(update_declinfo (Morphism.term phi (Free (n,nT)),v))
end;
- in ctxt |> fold upd updates end;
+ val ctxt' = ctxt |> fold upd updates
+ in ctxt' end;
in Context.mapping I upd_prf ctxt end;
@@ -545,20 +650,9 @@
(*** parse/print - translations ***)
-local
-
-fun map_get_comp f ctxt (Free (name,_)) =
- (case (get_comp ctxt name) of
- SOME (T,_) => f T T dummyT
- | NONE => (Syntax.free "arbitrary"(*; error "context not ready"*)))
- | map_get_comp _ _ _ = Syntax.free "arbitrary";
-
-fun name_of (Free (n,_)) = n;
-
-in
fun gen_lookup_tr ctxt s n =
- (case get_comp (Context.Proof ctxt) n of
+ (case get_comp' (Context.Proof ctxt) n of
SOME (T, _) =>
Syntax.const \<^const_name>\<open>StateFun.lookup\<close> $
Syntax.free (project_name T) $ Syntax.free n $ s
@@ -576,7 +670,7 @@
fun lookup_swap_tr ctxt [Free (n,_),s] = gen_lookup_tr ctxt s n;
fun lookup_tr' ctxt [_ $ Free (prj, _), n as (_ $ Free (name, _)), s] =
- (case get_comp (Context.Proof ctxt) name of
+ (case get_comp' (Context.Proof ctxt) name of
SOME (T, _) =>
if prj = project_name T
then Syntax.const "_statespace_lookup" $ s $ n
@@ -584,33 +678,36 @@
| NONE => raise Match)
| lookup_tr' _ _ = raise Match;
-fun gen_update_tr id ctxt n v s =
+fun gen'_update_tr const_val id ctxt n v s =
let
fun pname T = if id then \<^const_name>\<open>Fun.id\<close> else project_name T;
fun iname T = if id then \<^const_name>\<open>Fun.id\<close> else inject_name T;
+ val v = if const_val then (Syntax.const \<^const_name>\<open>K_statefun\<close> $ v) else v
in
- (case get_comp (Context.Proof ctxt) n of
+ (case get_comp' (Context.Proof ctxt) n of
SOME (T, _) =>
Syntax.const \<^const_name>\<open>StateFun.update\<close> $
Syntax.free (pname T) $ Syntax.free (iname T) $
- Syntax.free n $ (Syntax.const \<^const_name>\<open>K_statefun\<close> $ v) $ s
+ Syntax.free n $ v $ s
| NONE =>
if get_silent (Context.Proof ctxt) then
Syntax.const \<^const_name>\<open>StateFun.update\<close> $
Syntax.const \<^const_syntax>\<open>undefined\<close> $ Syntax.const \<^const_syntax>\<open>undefined\<close> $
- Syntax.free n $ (Syntax.const \<^const_name>\<open>K_statefun\<close> $ v) $ s
+ Syntax.free n $ v $ s
else raise TERM ("StateSpace.gen_update_tr: component " ^ n ^ " not defined", []))
end;
+val gen_update_tr = gen'_update_tr true
+
fun update_tr ctxt [s, x, v] =
(case Term_Position.strip_positions x of
- Free (n, _) => gen_update_tr false ctxt n v s
+ Free (n, _) => gen'_update_tr true false ctxt n v s
| _ => raise Match);
fun update_tr' ctxt
[_ $ Free (prj, _), _ $ Free (inj, _), n as (_ $ Free (name, _)), (Const (k, _) $ v), s] =
if Long_Name.base_name k = Long_Name.base_name \<^const_name>\<open>K_statefun\<close> then
- (case get_comp (Context.Proof ctxt) name of
+ (case get_comp' (Context.Proof ctxt) name of
SOME (T, _) =>
if inj = inject_name T andalso prj = project_name T then
Syntax.const "_statespace_update" $ s $ n $ v
@@ -619,7 +716,7 @@
else raise Match
| update_tr' _ _ = raise Match;
-end;
+
(*** outer syntax *)