nicolas.meric
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

syntactic massage of an interface description.

This commit is contained in:
Burkhart Wolff 2022-08-03 11:44:33 +02:00
parent 07a9c10001
commit bba7d9d5c5
1 changed files with 10 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
examples/CENELEC_50128/mini_odo/mini_odo.thy
View File

@ -222,7 +222,11 @@ text\<open>
type_synonym distance_function = "real[s] \<Rightarrow> real[m]"
consts Speed::"distance_function \<Rightarrow> real[s] \<Rightarrow> real[m\<cdot>s\<^sup>-\<^sup>1]"
consts Accel::"distance_function \<Rightarrow> real[s] \<Rightarrow> real[m\<cdot>s\<^sup>-\<^sup>2]"
definition "kilohertz = kilo *\<^sub>Q hertz"
consts Speed\<^sub>M\<^sub>a\<^sub>x::"real[m\<cdot>s\<^sup>-\<^sup>1]"
(* Non - SI conform common abrbreviations *)
definition "kmh \<equiv> kilo *\<^sub>Q metre \<^bold>/ hour :: real[m\<cdot>s\<^sup>-\<^sup>1]"
definition "kHz \<equiv> kilo *\<^sub>Q hertz :: real[s\<^sup>-\<^sup>1]"
(*>*)
text\<open>
@ -290,13 +294,13 @@ and the global model parameters such as wheel diameter, the number of teeth per
sampling frequency etc., we can infer the maximal time of service as well the maximum distance
the device can measure. As an example configuration, choosing:
\<^item> \<^term>\<open>(1 *\<^sub>Q metre)::real[m]\<close> for \<^term>\<open>w\<^sub>d\<close>,
\<^item> \<^term>\<open>100 :: real\<close> for \<^term>\<open>tpw\<close>,
\<^item> \<^term>\<open>80 *\<^sub>Q kilo *\<^sub>Q metre \<^bold>/ hour :: real[m\<cdot>s\<^sup>-\<^sup>1] \<close> for \<^term>\<open>Speed\<^sub>M\<^sub>a\<^sub>x\<close>,
\<^item> \<^term>\<open>14.4 *\<^sub>Q kilo *\<^sub>Q hertz\<close> for the sampling frequency,
\<^item> \<^term>\<open>(1 *\<^sub>Q metre)::real[m]\<close> for \<^term>\<open>w\<^sub>d\<close> (wheel-diameter),
\<^item> \<^term>\<open>100 :: real\<close> for \<^term>\<open>tpw\<close> (teeth per wheel),
\<^item> \<^term>\<open>80 *\<^sub>Q kmh :: real[m\<cdot>s\<^sup>-\<^sup>1]\<close> for \<^term>\<open>Speed\<^sub>M\<^sub>a\<^sub>x\<close>,
\<^item> \<^term>\<open>14.4 *\<^sub>Q kHz :: real[s\<^sup>-\<^sup>1]\<close> for the sampling frequency,
results in an odometer resolution of \<^term>\<open>2.3 *\<^sub>Q milli *\<^sub>Q metre\<close>, a maximum distance of
\<^term>\<open>9878*\<^sub>Q kilo *\<^sub>Q metre\<close>, and a maximal system up-time of \<^term>\<open>123.4 *\<^sub>Q hour\<close>s.
\<^term>\<open>9878 *\<^sub>Q kilo *\<^sub>Q metre\<close>, and a maximal system up-time of \<^term>\<open>123.4 *\<^sub>Q hour\<close>s.
The required precision of an odometer can be defined by a constant describing
the maximally allowed difference between \<open>df(n*\<delta>t)\<close> and
\<open>sampling df init\<^sub>p\<^sub>o\<^sub>s \<delta>t n\<close> for all \<open>init\<^sub>p\<^sub>o\<^sub>s \<in>{0..5}\<close>.