--- a/Paper.thy Sun Jun 23 03:55:49 2013 +0100
+++ b/Paper.thy Fri Sep 06 12:55:12 2013 +0100
@@ -91,9 +91,9 @@
InheritParent_file_type ("InheritPatentType") and
NormalFile_type ("NormalFileType") and
deleted ("deleted _ _" [50, 100] 100) and
- taintable_s ("taintable\<^isup>s") and
- tainted_s ("tainted\<^isup>s") and
- all_sobjs ("reachable\<^isup>s") and
+ taintable_s ("taintable\<^sup>s") and
+ tainted_s ("tainted\<^sup>s") and
+ all_sobjs ("reachable\<^sup>s") and
init_obj2sobj ("\<lbrakk>_\<rbrakk>") and
erole_functor ("erole'_aux") --"I have a erole_functor and etype_aux to handle
efficient, but their name not same, so ..., but don't work"
@@ -773,7 +773,7 @@
potentially infinitely many of them and therefore the search space would be
infinite. For example starting from an
initial state containing a process @{text p} and a file @{text pf},
- we can create files @{text "f\<^isub>1"}, @{text "f\<^isub>2"}, @{text "..."}
+ we can create files @{text "f\<^sub>1"}, @{text "f\<^sub>2"}, @{text "..."}
via @{text "CreateFile"}-events. This can be pictured roughly as follows:
\begin{center}
@@ -785,23 +785,23 @@
\begin{tabular}[t]{c}
\\
@{text "\<Longrightarrow>"}\\[2mm]
- {\small@{term "CreateFile p (f\<^isub>1#pf)"}}
+ {\small@{term "CreateFile p (f\<^sub>1#pf)"}}
\end{tabular}
&
\begin{tabular}[t]{c}
\\
- @{term "{p, pf, f\<^isub>1#pf}"}
+ @{term "{p, pf, f\<^sub>1#pf}"}
\end{tabular}
&
\begin{tabular}[t]{c}
\\
@{text "\<Longrightarrow>"}\\[2mm]
- {\small@{term "CreateFile p (f\<^isub>2#f\<^isub>1#pf)"}}
+ {\small@{term "CreateFile p (f\<^sub>2#f\<^sub>1#pf)"}}
\end{tabular}
&
\begin{tabular}[t]{c}
\\
- @{term "{p, pf, f\<^isub>1#pf, f\<^isub>2#f\<^isub>1#pf}"}
+ @{term "{p, pf, f\<^sub>1#pf, f\<^sub>2#f\<^sub>1#pf}"}
\end{tabular} &
\begin{tabular}[t]{c}
\\
@@ -1035,34 +1035,34 @@
is that there can be infinitely many valid states, but assuming the initial
state contains only finitely many objects, then also @{term "all_sobjs"} will
be finite. To see the difference, consider the infinite ``chain'' of events
- just cloning a process @{text "p\<^isub>0"}:
+ just cloning a process @{text "p\<^sub>0"}:
\begin{center}
\begin{tabular}[t]{c@ {\hspace{-2mm}}c@ {\hspace{-2mm}}c@ {\hspace{-2mm}}c@ {\hspace{-2mm}}cc}
\begin{tabular}[t]{c}
Initial state:\\
- @{term "{p\<^isub>0}"}
+ @{term "{p\<^sub>0}"}
\end{tabular} &
\begin{tabular}[t]{c}
\\
@{text "\<Longrightarrow>"}\\[2mm]
- {\small@{term "Clone p\<^isub>0 p\<^isub>1"}}
+ {\small@{term "Clone p\<^sub>0 p\<^sub>1"}}
\end{tabular}
&
\begin{tabular}[t]{c}
\\
- @{term "{p\<^isub>0, p\<^isub>1}"}
+ @{term "{p\<^sub>0, p\<^sub>1}"}
\end{tabular}
&
\begin{tabular}[t]{c}
\\
@{text "\<Longrightarrow>"}\\[2mm]
- {\small@{term "Clone p\<^isub>0 p\<^isub>2"}}
+ {\small@{term "Clone p\<^sub>0 p\<^sub>2"}}
\end{tabular}
&
\begin{tabular}[t]{c}
\\
- @{term "{p\<^isub>0, p\<^isub>1, p\<^isub>2}"}
+ @{term "{p\<^sub>0, p\<^sub>1, p\<^sub>2}"}
\end{tabular} &
\begin{tabular}[t]{c}
\\
@@ -1077,22 +1077,22 @@
\begin{center}
\begin{tabular}[t]{cccc}
\begin{tabular}[t]{c}
- @{text "{P(r, dr, t, u)\<^bsup>Some (p\<^isub>0)\<^esup>}"}
+ @{text "{P(r, dr, t, u)\<^bsup>Some (p\<^sub>0)\<^esup>}"}
\end{tabular} &
\begin{tabular}[t]{c}
@{text "\<Longrightarrow>"}
\end{tabular}
&
\begin{tabular}[t]{c}
- @{text "{P(r, dr, t, u)\<^bsup>Some (p\<^isub>0)\<^esup>, P(r, dr, t, u)\<^bsup>None\<^esup>}"}
+ @{text "{P(r, dr, t, u)\<^bsup>Some (p\<^sub>0)\<^esup>, P(r, dr, t, u)\<^bsup>None\<^esup>}"}
\end{tabular}
\end{tabular}
\end{center}
\noindent
where no further progress can be made because the information
- recorded about @{text "p\<^isub>2"}, @{text "p\<^isub>3"} and so on is just the same
- as for @{text "p\<^isub>1"}, namely @{text "P(r, dr, t, u)\<^bsup>None\<^esup>"}. Indeed we
+ recorded about @{text "p\<^sub>2"}, @{text "p\<^sub>3"} and so on is just the same
+ as for @{text "p\<^sub>1"}, namely @{text "P(r, dr, t, u)\<^bsup>None\<^esup>"}. Indeed we
can prove the lemma:
\begin{lemma}\label{finite}
@@ -1159,7 +1159,7 @@
is that every tainted object is also reachable:
\begin{lemma}
- @{text "tainted\<^isup>s \<subseteq> reachable\<^isup>s"}
+ @{text "tainted\<^sup>s \<subseteq> reachable\<^sup>s"}
\end{lemma}
\noindent
@@ -1188,7 +1188,7 @@
\begin{isabelle}\ \ \ \ \ %%%
\mbox{\begin{tabular}{lcl}
- @{thm (lhs) taintable_s_def} & @{text "\<equiv>"} & @{text "\<exists>item. item \<in> tainted\<^isup>s \<and> |item| = Some obj"}
+ @{thm (lhs) taintable_s_def} & @{text "\<equiv>"} & @{text "\<exists>item. item \<in> tainted\<^sup>s \<and> |item| = Some obj"}
\end{tabular}}
\end{isabelle}