# HG changeset patch # User Norbert Schirmer # Date 1634632898 -7200 # Node ID 3cc363e8bfb27d04a0945fccd360cec463a2284f # Parent ebb0b15c66e1dd94db12b6b0430fc2e45632914c cleanup; add Apple reference diff -r ebb0b15c66e1 -r 3cc363e8bfb2 src/HOL/Statespace/StateSpaceEx.thy --- a/src/HOL/Statespace/StateSpaceEx.thy Thu Jul 15 08:09:10 2021 +0200 +++ b/src/HOL/Statespace/StateSpaceEx.thy Tue Oct 19 10:41:38 2021 +0200 @@ -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 \Examples \label{sec:Examples}\ @@ -32,7 +33,7 @@ text \\noindent This resembles a \<^theory_text>\record\ 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>\n\ and \<^term>\b\ and projection~/ injection functions that convert from abstract values to \<^typ>\nat\ and \bool\. The logical content of the locale is:\ @@ -53,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 @@ -72,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 \s\n\, which is translated to \project_nat (s n)\, and an update as \s\n := 2\\, which is -translated to \s(n := inject_nat 2)\. We can now establish the +can be written as \s\n\, which is translated to \project_nat (s n)\, and an +update as \s\n := 2\\, which is translated to \s(n := inject_nat 2)\. +We can now establish the following lemma:\ lemma (in vars) foo: "s\b = s\b" by simp @@ -92,7 +89,8 @@ \<^typ>\'a\. 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 \distinct [N, B, n, b, x]\, -from this we can derive both \<^term>\distinct [N,B]\ and \<^term>\distinct [n,b]\, the distinction assumptions for the two versions of +from this we can derive both \<^term>\distinct [N,B]\ and \<^term>\distinct [n,b]\, +the distinction assumptions for the two versions of locale \vars\ above. Moreover we have all necessary projection and injection assumptions available. These assumptions together allow us to establish state space \<^term>\varsX\ as an @@ -112,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 @@ -194,7 +192,7 @@ by simp text \There were known problems with syntax-declarations. They only -worked, when the context is already completely built. This is now overcome. e.g.:\ +worked when the context is already completely built. This is now overcome. e.g.:\ locale fooX = foo + assumes "s\b = k" @@ -211,15 +209,15 @@ context side_by_side begin -text \Simplification within on of the statespaces works as expected.\ +text \Simplification within one of the statespaces works as expected.\ lemma "s\C = s\C" by simp lemma "s\b = s\b" by simp -text \In contrast to the statespace @{locale loo} there is no 'inter' statespece distinctness between the -names of @{locale foo} and @{locale bar}. }\ +text \In contrast to the statespace @{locale loo} there is no 'inter' statespace distinctness +between the names of @{locale foo} and @{locale bar}.\ end @@ -252,7 +250,8 @@ context merge_vars1_vars2 begin -text \When defining a statespace instead of a side-by-side locale we get the distinctness of all variables.\ +text \When defining a statespace instead of a side-by-side locale we get the distinctness of +all variables.\ lemma "s\m = s\m" by simp end diff -r ebb0b15c66e1 -r 3cc363e8bfb2 src/HOL/Statespace/distinct_tree_prover.ML --- a/src/HOL/Statespace/distinct_tree_prover.ML Thu Jul 15 08:09:10 2021 +0200 +++ b/src/HOL/Statespace/distinct_tree_prover.ML Tue Oct 19 10:41:38 2021 +0200 @@ -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 = diff -r ebb0b15c66e1 -r 3cc363e8bfb2 src/HOL/Statespace/state_fun.ML --- a/src/HOL/Statespace/state_fun.ML Thu Jul 15 08:09:10 2021 +0200 +++ b/src/HOL/Statespace/state_fun.ML Tue Oct 19 10:41:38 2021 +0200 @@ -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 = diff -r ebb0b15c66e1 -r 3cc363e8bfb2 src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML Thu Jul 15 08:09:10 2021 +0200 +++ b/src/HOL/Statespace/state_space.ML Tue Oct 19 10:41:38 2021 +0200 @@ -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 = @@ -659,8 +660,7 @@ if get_silent (Context.Proof ctxt) then Syntax.const \<^const_name>\StateFun.lookup\ $ Syntax.const \<^const_syntax>\undefined\ $ Syntax.free n $ s - else (trace_name_space_data (Context.Proof ctxt); - raise TERM ("StateSpace.gen_lookup_tr: component " ^ quote n ^ " not defined", []))); + else raise TERM ("StateSpace.gen_lookup_tr: component " ^ quote n ^ " not defined", [])); fun lookup_tr ctxt [s, x] = (case Term_Position.strip_positions x of