theory Test imports Noninfluence begin

primrec
"dom (INPUTHIGH x) = H"
"dom (INPUTLOW x) = L"
"dom OUTPUTHIGH = H"
"dom OUTPUTLOW = L"

primrec
"step (INPUTHIGH x) S = S\<lparr> HighData := x \<rparr>"
"step (INPUTLOW x) S = S\<lparr> LowData := x \<rparr>"
"step OUTPUTHIGH S = S"
"step OUTPUTLOW S = S"

primrec
"output H s = {HighData s, LowData s}"
"output L s = {LowData s}"

(* Information may flow from Low to High *)

recdef policy "measure (\<lambda> x. 0)"
"policy x = (if x = L then (\<lambda> y. True) else (\<lambda> y. x=y))"

primrec
"uwr s1 H s2 = (s1=s2)"
"uwr s1 L s2 = ((LowData s1) = (LowData s2))"

lemma wsc: "weakly_step_consistent"
apply(simp add:weakly_step_consistent_def)
apply(auto)
apply(case_tac a)
apply(auto)
apply(case_tac u)
apply(auto)
apply(case_tac a)
by(auto)

lemma sr: "step_respect"
apply(simp add:step_respect_def)
apply(auto)
apply(case_tac a, auto)
by(case_tac u, auto)


lemma oc: "output_consistent"
apply(simp add:output_consistent_def)
apply(auto)
apply(case_tac u, auto)
by(case_tac u, auto)

theorem "nonleakage"
by(insert nonleakage wsc oc sr, simp)

lemma lr: "local_respect"
apply(simp only:local_respect_def local_respect_left_def local_respect_right_def)
apply(simp)
apply(auto)
apply(case_tac u, auto)
apply(case_tac a, auto)
apply(case_tac a, auto)
apply(case_tac a, auto)
by(case_tac u, auto)

theorem "noninterference"
by(insert noninterference wsc oc sr lr,simp)

end