Theory Concrete
section ‹Concrete setting›
theory Concrete
imports Syntactic_Criteria After_Execution
begin
lemma (in PL_Indis) WbisT_If_cross:
assumes "c1 ≈wT c2" "c1 ≈wT c1" "c2 ≈wT c2"
shows "(If tst c1 c2) ≈wT (If tst c1 c2)"
proof -
define φ
where "φ c d ⟷ (∃c1' c2'. c = If tst c1' c2' ∧ d = If tst c1' c2' ∧ c1' ≈wT c2' ∧ c1' ≈wT c1' ∧ c2' ≈wT c2')"
for c d
with assms have "φ (If tst c1 c2) (If tst c1 c2)" by auto
then show ?thesis
proof (induct rule: WbisT_coinduct[where φ=φ])
case (cont c s d t c' s')
note cont(2,3)
moreover from cont obtain c1 c2
where φ: "c = If tst c1 c2" "d = If tst c1 c2" "c1 ≈wT c2" "c1 ≈wT c1" "c2 ≈wT c2"
by (auto simp: φ_def)
moreover then have "c2 ≈wT c1"
using WbisT_sym unfolding sym_def by blast
ultimately have "(d, t) →*c (if tval tst t then c1 else c2, t) ∧ s' ≈ t ∧
(φ c' (if tval tst t then c1 else c2) ∨ c' ≈wT (if tval tst t then c1 else c2))"
by (auto simp: φ_def)
then show ?case by auto
qed (auto simp: φ_def)
qed
text‹
We instatiate the following notions, kept generic so far:
\begin{itemize}
\item On the language syntax:
\begin{itemize}
\item atoms, tests and states just like at the possibilistic case;
\item choices, to either if-choices (based on tests) or binary fixed-probability choices;
\item the schedulers, to the uniform one
\end{itemize}
\item On the security semantics, the lattice of levels and the indis relation, again, just like at the possibilistic case.
\end{itemize}
›
datatype level = Lo | Hi
lemma [simp]: "⋀ l. l ≠ Hi ⟷ l = Lo" and
[simp]: "⋀ l. Hi ≠ l ⟷ Lo = l" and
[simp]: "⋀ l. l ≠ Lo ⟷ l = Hi" and
[simp]: "⋀ l. Lo ≠ l ⟷ Hi = l"
by (metis level.exhaust level.simps(2))+
lemma [dest]: "⋀ l A. ⟦l ∈ A; Lo ∉ A⟧ ⟹ l = Hi" and
[dest]: "⋀ l A. ⟦l ∈ A; Hi ∉ A⟧ ⟹ l = Lo"
by (metis level.exhaust)+
declare level.split[split]
instantiation level :: complete_lattice
begin
definition top_level: "top ≡ Hi"
definition bot_level: "bot ≡ Lo"
definition inf_level: "inf l1 l2 ≡ if Lo ∈ {l1,l2} then Lo else Hi"
definition sup_level: "sup l1 l2 ≡ if Hi ∈ {l1,l2} then Hi else Lo"
definition less_eq_level: "less_eq l1 l2 ≡ (l1 = Lo ∨ l2 = Hi)"
definition less_level: "less l1 l2 ≡ l1 = Lo ∧ l2 = Hi"
definition Inf_level: "Inf L ≡ if Lo ∈ L then Lo else Hi"
definition Sup_level: "Sup L ≡ if Hi ∈ L then Hi else Lo"
instance
proof qed (auto simp: top_level bot_level inf_level sup_level
less_eq_level less_level Inf_level Sup_level)
end
lemma sup_eq_Lo[simp]: "sup a b = Lo ⟷ a = Lo ∧ b = Lo"
by (auto simp: sup_level)