theory Noninterference_Base

lemma Noninterference_Noninterference_strong:
  "Noninterference \<Longrightarrow> Noninterference_strong" apply (clarsimp simp: Noninterference_def Noninterference_strong_def) apply (drule_tac x=u in spec) apply (frule_tac x=as in spec, drule_tac x=s in spec) apply (drule_tac x=bs in spec, drule_tac x=s in spec) apply clarsimp apply (rule obs_equiv_trans) apply assumption apply assumption apply (erule obs_equiv_sym) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Noninterference \<Longrightarrow> Noninterference_strong proof (prove)
goal (1 subgoal):
 1. \<And>u as bs s. \<lbrakk>\<forall>u as s. reachable s \<longrightarrow> obs_equiv s as s (ipurge u as {s}) u; reachable s; ipurge u as {s} = ipurge u bs {s}\<rbrakk> \<Longrightarrow> obs_equiv s as s bs u proof (prove)
goal (1 subgoal):
 1. \<And>u as bs s. \<lbrakk>reachable s; ipurge u as {s} = ipurge u bs {s}; \<forall>as s. reachable s \<longrightarrow> obs_equiv s as s (ipurge u as {s}) u\<rbrakk> \<Longrightarrow> obs_equiv s as s bs u proof (prove)
goal (1 subgoal):
 1. \<And>u as bs s. \<lbrakk>reachable s; ipurge u as {s} = ipurge u bs {s}; \<forall>as s. reachable s \<longrightarrow> obs_equiv s as s (ipurge u as {s}) u; reachable s \<longrightarrow> obs_equiv s as s (ipurge u as {s}) u\<rbrakk> \<Longrightarrow> obs_equiv s as s bs u proof (prove)
goal (1 subgoal):
 1. \<And>u as bs s. \<lbrakk>reachable s; ipurge u as {s} = ipurge u bs {s}; reachable s \<longrightarrow> obs_equiv s as s (ipurge u as {s}) u; reachable s \<longrightarrow> obs_equiv s bs s (ipurge u bs {s}) u\<rbrakk> \<Longrightarrow> obs_equiv s as s bs u proof (prove)
goal (1 subgoal):
 1. \<And>u as bs s. \<lbrakk>reachable s; ipurge u as {s} = ipurge u bs {s}; obs_equiv s as s (ipurge u bs {s}) u; obs_equiv s bs s (ipurge u bs {s}) u\<rbrakk> \<Longrightarrow> obs_equiv s as s bs u proof (prove)
goal (3 subgoals):
 1. \<And>u as bs s. \<lbrakk>reachable s; ipurge u as {s} = ipurge u bs {s}; obs_equiv s as s (ipurge u bs {s}) u; obs_equiv s bs s (ipurge u bs {s}) u\<rbrakk> \<Longrightarrow> reachable (?t16 u as bs s)
 2. \<And>u as bs s. \<lbrakk>reachable s; ipurge u as {s} = ipurge u bs {s}; obs_equiv s as s (ipurge u bs {s}) u; obs_equiv s bs s (ipurge u bs {s}) u\<rbrakk> \<Longrightarrow> obs_equiv s as (?t16 u as bs s) (?bs16 u as bs s) u
 3. \<And>u as bs s. \<lbrakk>reachable s; ipurge u as {s} = ipurge u bs {s}; obs_equiv s as s (ipurge u bs {s}) u; obs_equiv s bs s (ipurge u bs {s}) u\<rbrakk> \<Longrightarrow> obs_equiv (?t16 u as bs s) (?bs16 u as bs s) s bs u proof (prove)
goal (2 subgoals):
 1. \<And>u as bs s. \<lbrakk>reachable s; ipurge u as {s} = ipurge u bs {s}; obs_equiv s as s (ipurge u bs {s}) u; obs_equiv s bs s (ipurge u bs {s}) u\<rbrakk> \<Longrightarrow> obs_equiv s as s (?bs16 u as bs s) u
 2. \<And>u as bs s. \<lbrakk>reachable s; ipurge u as {s} = ipurge u bs {s}; obs_equiv s as s (ipurge u bs {s}) u; obs_equiv s bs s (ipurge u bs {s}) u\<rbrakk> \<Longrightarrow> obs_equiv s (?bs16 u as bs s) s bs u proof (prove)
goal (1 subgoal):
 1. \<And>u as bs s. \<lbrakk>reachable s; ipurge u as {s} = ipurge u bs {s}; obs_equiv s as s (ipurge u bs {s}) u; obs_equiv s bs s (ipurge u bs {s}) u\<rbrakk> \<Longrightarrow> obs_equiv s (ipurge u bs {s}) s bs u proof (prove)
goal:
No subgoals!