theory Noninterference_Base

lemma Noninfluence_Noninfluence_strong:
  "\<lbrakk> confidentiality_u; Noninfluence \<rbrakk> \<Longrightarrow> Noninfluence_strong" apply (clarsimp simp: Noninfluence_def Noninfluence_strong_def) apply (frule_tac s=s and t=t and as=as and u=u in ipurge_eq) apply assumption+ apply (frule_tac s=s and t=t and as=bs and u=u in ipurge_eq) apply assumption+ apply clarsimp apply (drule_tac x=u in spec) apply (frule_tac x=as in spec) apply (drule_tac x=s in spec, drule_tac x=t in spec) apply (drule_tac x=bs in spec) apply (drule_tac x=t in spec, drule_tac x=t in spec) apply clarsimp apply (rule_tac t=t in obs_equiv_trans) apply assumption apply assumption apply (rule obs_equiv_sym) apply (clarsimp simp: sameFor_dom_def uwr_refl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>confidentiality_u; Noninfluence\<rbrakk> \<Longrightarrow> Noninfluence_strong proof (prove)
goal (1 subgoal):
 1. \<And>u as bs s t. \<lbrakk>confidentiality_u; \<forall>u as s t. reachable s \<and> reachable t \<longrightarrow> s \<approx>sources as s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> obs_equiv s as t (ipurge u as {t}) u; reachable s; reachable t; s \<approx>sources as s u\<approx> t; s \<sim>schedDomain\<sim> t; ipurge u as {s} = ipurge u bs {s}\<rbrakk> \<Longrightarrow> obs_equiv s as t bs u proof (prove)
goal (4 subgoals):
 1. \<And>u as bs s t. \<lbrakk>confidentiality_u; \<forall>u as s t. reachable s \<and> reachable t \<longrightarrow> s \<approx>sources as s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> obs_equiv s as t (ipurge u as {t}) u; reachable s; reachable t; s \<approx>sources as s u\<approx> t; s \<sim>schedDomain\<sim> t; ipurge u as {s} = ipurge u bs {s}\<rbrakk> \<Longrightarrow> reachable s
 2. \<And>u as bs s t. \<lbrakk>confidentiality_u; \<forall>u as s t. reachable s \<and> reachable t \<longrightarrow> s \<approx>sources as s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> obs_equiv s as t (ipurge u as {t}) u; reachable s; reachable t; s \<approx>sources as s u\<approx> t; s \<sim>schedDomain\<sim> t; ipurge u as {s} = ipurge u bs {s}\<rbrakk> \<Longrightarrow> reachable t
 3. \<And>u as bs s t. \<lbrakk>confidentiality_u; \<forall>u as s t. reachable s \<and> reachable t \<longrightarrow> s \<approx>sources as s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> obs_equiv s as t (ipurge u as {t}) u; reachable s; reachable t; s \<approx>sources as s u\<approx> t; s \<sim>schedDomain\<sim> t; ipurge u as {s} = ipurge u bs {s}\<rbrakk> \<Longrightarrow> confidentiality_u
 4. \<And>u as bs s t. \<lbrakk>confidentiality_u; \<forall>u as s t. reachable s \<and> reachable t \<longrightarrow> s \<approx>sources as s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> obs_equiv s as t (ipurge u as {t}) u; reachable s; reachable t; s \<approx>sources as s u\<approx> t; s \<sim>schedDomain\<sim> t; ipurge u as {s} = ipurge u bs {s}; ipurge u as {s} = ipurge u as {t}\<rbrakk> \<Longrightarrow> obs_equiv s as t bs u proof (prove)
goal (1 subgoal):
 1. \<And>u as bs s t. \<lbrakk>confidentiality_u; \<forall>u as s t. reachable s \<and> reachable t \<longrightarrow> s \<approx>sources as s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> obs_equiv s as t (ipurge u as {t}) u; reachable s; reachable t; s \<approx>sources as s u\<approx> t; s \<sim>schedDomain\<sim> t; ipurge u as {s} = ipurge u bs {s}; ipurge u as {s} = ipurge u as {t}\<rbrakk> \<Longrightarrow> obs_equiv s as t bs u proof (prove)
goal (4 subgoals):
 1. \<And>u as bs s t. \<lbrakk>confidentiality_u; \<forall>u as s t. reachable s \<and> reachable t \<longrightarrow> s \<approx>sources as s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> obs_equiv s as t (ipurge u as {t}) u; reachable s; reachable t; s \<approx>sources as s u\<approx> t; s \<sim>schedDomain\<sim> t; ipurge u as {s} = ipurge u bs {s}; ipurge u as {s} = ipurge u as {t}\<rbrakk> \<Longrightarrow> reachable s
 2. \<And>u as bs s t. \<lbrakk>confidentiality_u; \<forall>u as s t. reachable s \<and> reachable t \<longrightarrow> s \<approx>sources as s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> obs_equiv s as t (ipurge u as {t}) u; reachable s; reachable t; s \<approx>sources as s u\<approx> t; s \<sim>schedDomain\<sim> t; ipurge u as {s} = ipurge u bs {s}; ipurge u as {s} = ipurge u as {t}\<rbrakk> \<Longrightarrow> reachable t
 3. \<And>u as bs s t. \<lbrakk>confidentiality_u; \<forall>u as s t. reachable s \<and> reachable t \<longrightarrow> s \<approx>sources as s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> obs_equiv s as t (ipurge u as {t}) u; reachable s; reachable t; s \<approx>sources as s u\<approx> t; s \<sim>schedDomain\<sim> t; ipurge u as {s} = ipurge u bs {s}; ipurge u as {s} = ipurge u as {t}\<rbrakk> \<Longrightarrow> confidentiality_u
 4. \<And>u as bs s t. \<lbrakk>confidentiality_u; \<forall>u as s t. reachable s \<and> reachable t \<longrightarrow> s \<approx>sources as s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> obs_equiv s as t (ipurge u as {t}) u; reachable s; reachable t; s \<approx>sources as s u\<approx> t; s \<sim>schedDomain\<sim> t; ipurge u as {s} = ipurge u bs {s}; ipurge u as {s} = ipurge u as {t}; ipurge u bs {s} = ipurge u bs {t}\<rbrakk> \<Longrightarrow> obs_equiv s as t bs u proof (prove)
goal (1 subgoal):
 1. \<And>u as bs s t. \<lbrakk>confidentiality_u; \<forall>u as s t. reachable s \<and> reachable t \<longrightarrow> s \<approx>sources as s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> obs_equiv s as t (ipurge u as {t}) u; reachable s; reachable t; s \<approx>sources as s u\<approx> t; s \<sim>schedDomain\<sim> t; ipurge u as {s} = ipurge u bs {s}; ipurge u as {s} = ipurge u as {t}; ipurge u bs {s} = ipurge u bs {t}\<rbrakk> \<Longrightarrow> obs_equiv s as t bs u proof (prove)
goal (1 subgoal):
 1. \<And>u as bs s t. \<lbrakk>confidentiality_u; \<forall>u as s t. reachable s \<and> reachable t \<longrightarrow> s \<approx>sources as s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> obs_equiv s as t (ipurge u as {t}) u; reachable s; reachable t; s \<approx>sources as s u\<approx> t; s \<sim>schedDomain\<sim> t; ipurge u as {t} = ipurge u bs {t}; ipurge u as {s} = ipurge u bs {t}; ipurge u bs {s} = ipurge u bs {t}\<rbrakk> \<Longrightarrow> obs_equiv s as t bs u proof (prove)
goal (1 subgoal):
 1. \<And>u as bs s t. \<lbrakk>confidentiality_u; reachable s; reachable t; s \<approx>sources as s u\<approx> t; s \<sim>schedDomain\<sim> t; ipurge u as {t} = ipurge u bs {t}; ipurge u as {s} = ipurge u bs {t}; ipurge u bs {s} = ipurge u bs {t}; \<forall>as s t. reachable s \<and> reachable t \<longrightarrow> s \<approx>sources as s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> obs_equiv s as t (ipurge u as {t}) u\<rbrakk> \<Longrightarrow> obs_equiv s as t bs u proof (prove)
goal (1 subgoal):
 1. \<And>u as bs s t. \<lbrakk>confidentiality_u; reachable s; reachable t; s \<approx>sources as s u\<approx> t; s \<sim>schedDomain\<sim> t; ipurge u as {t} = ipurge u bs {t}; ipurge u as {s} = ipurge u bs {t}; ipurge u bs {s} = ipurge u bs {t}; \<forall>as s t. reachable s \<and> reachable t \<longrightarrow> s \<approx>sources as s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> obs_equiv s as t (ipurge u as {t}) u; \<forall>s t. reachable s \<and> reachable t \<longrightarrow> s \<approx>sources as s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> obs_equiv s as t (ipurge u as {t}) u\<rbrakk> \<Longrightarrow> obs_equiv s as t bs u proof (prove)
goal (1 subgoal):
 1. \<And>u as bs s t. \<lbrakk>confidentiality_u; reachable s; reachable t; s \<approx>sources as s u\<approx> t; s \<sim>schedDomain\<sim> t; ipurge u as {t} = ipurge u bs {t}; ipurge u as {s} = ipurge u bs {t}; ipurge u bs {s} = ipurge u bs {t}; \<forall>as s t. reachable s \<and> reachable t \<longrightarrow> s \<approx>sources as s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> obs_equiv s as t (ipurge u as {t}) u; reachable s \<and> reachable t \<longrightarrow> s \<approx>sources as s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> obs_equiv s as t (ipurge u as {t}) u\<rbrakk> \<Longrightarrow> obs_equiv s as t bs u proof (prove)
goal (1 subgoal):
 1. \<And>u as bs s t. \<lbrakk>confidentiality_u; reachable s; reachable t; s \<approx>sources as s u\<approx> t; s \<sim>schedDomain\<sim> t; ipurge u as {t} = ipurge u bs {t}; ipurge u as {s} = ipurge u bs {t}; ipurge u bs {s} = ipurge u bs {t}; reachable s \<and> reachable t \<longrightarrow> s \<approx>sources as s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> obs_equiv s as t (ipurge u as {t}) u; \<forall>s t. reachable s \<and> reachable t \<longrightarrow> s \<approx>sources bs s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> obs_equiv s bs t (ipurge u bs {t}) u\<rbrakk> \<Longrightarrow> obs_equiv s as t bs u proof (prove)
goal (1 subgoal):
 1. \<And>u as bs s t. \<lbrakk>confidentiality_u; reachable s; reachable t; s \<approx>sources as s u\<approx> t; s \<sim>schedDomain\<sim> t; ipurge u as {t} = ipurge u bs {t}; ipurge u as {s} = ipurge u bs {t}; ipurge u bs {s} = ipurge u bs {t}; reachable s \<and> reachable t \<longrightarrow> s \<approx>sources as s u\<approx> t \<longrightarrow> s \<sim>schedDomain\<sim> t \<longrightarrow> obs_equiv s as t (ipurge u as {t}) u; reachable t \<and> reachable t \<longrightarrow> t \<approx>sources bs t u\<approx> t \<longrightarrow> t \<sim>schedDomain\<sim> t \<longrightarrow> obs_equiv t bs t (ipurge u bs {t}) u\<rbrakk> \<Longrightarrow> obs_equiv s as t bs u proof (prove)
goal (1 subgoal):
 1. \<And>u as bs s t. \<lbrakk>confidentiality_u; reachable s; reachable t; s \<approx>sources as s u\<approx> t; s \<sim>schedDomain\<sim> t; ipurge u as {t} = ipurge u bs {t}; ipurge u as {s} = ipurge u bs {t}; ipurge u bs {s} = ipurge u bs {t}; obs_equiv s as t (ipurge u bs {t}) u; t \<approx>sources bs t u\<approx> t \<longrightarrow> t \<sim>schedDomain\<sim> t \<longrightarrow> obs_equiv t bs t (ipurge u bs {t}) u\<rbrakk> \<Longrightarrow> obs_equiv s as t bs u proof (prove)
goal (3 subgoals):
 1. \<And>u as bs s t. \<lbrakk>confidentiality_u; reachable s; reachable t; s \<approx>sources as s u\<approx> t; s \<sim>schedDomain\<sim> t; ipurge u as {t} = ipurge u bs {t}; ipurge u as {s} = ipurge u bs {t}; ipurge u bs {s} = ipurge u bs {t}; obs_equiv s as t (ipurge u bs {t}) u; t \<approx>sources bs t u\<approx> t \<longrightarrow> t \<sim>schedDomain\<sim> t \<longrightarrow> obs_equiv t bs t (ipurge u bs {t}) u\<rbrakk> \<Longrightarrow> reachable t
 2. \<And>u as bs s t. \<lbrakk>confidentiality_u; reachable s; reachable t; s \<approx>sources as s u\<approx> t; s \<sim>schedDomain\<sim> t; ipurge u as {t} = ipurge u bs {t}; ipurge u as {s} = ipurge u bs {t}; ipurge u bs {s} = ipurge u bs {t}; obs_equiv s as t (ipurge u bs {t}) u; t \<approx>sources bs t u\<approx> t \<longrightarrow> t \<sim>schedDomain\<sim> t \<longrightarrow> obs_equiv t bs t (ipurge u bs {t}) u\<rbrakk> \<Longrightarrow> obs_equiv s as t (?bs28 u as bs s t) u
 3. \<And>u as bs s t. \<lbrakk>confidentiality_u; reachable s; reachable t; s \<approx>sources as s u\<approx> t; s \<sim>schedDomain\<sim> t; ipurge u as {t} = ipurge u bs {t}; ipurge u as {s} = ipurge u bs {t}; ipurge u bs {s} = ipurge u bs {t}; obs_equiv s as t (ipurge u bs {t}) u; t \<approx>sources bs t u\<approx> t \<longrightarrow> t \<sim>schedDomain\<sim> t \<longrightarrow> obs_equiv t bs t (ipurge u bs {t}) u\<rbrakk> \<Longrightarrow> obs_equiv t (?bs28 u as bs s t) t bs u proof (prove)
goal (2 subgoals):
 1. \<And>u as bs s t. \<lbrakk>confidentiality_u; reachable s; reachable t; s \<approx>sources as s u\<approx> t; s \<sim>schedDomain\<sim> t; ipurge u as {t} = ipurge u bs {t}; ipurge u as {s} = ipurge u bs {t}; ipurge u bs {s} = ipurge u bs {t}; obs_equiv s as t (ipurge u bs {t}) u; t \<approx>sources bs t u\<approx> t \<longrightarrow> t \<sim>schedDomain\<sim> t \<longrightarrow> obs_equiv t bs t (ipurge u bs {t}) u\<rbrakk> \<Longrightarrow> obs_equiv s as t (?bs28 u as bs s t) u
 2. \<And>u as bs s t. \<lbrakk>confidentiality_u; reachable s; reachable t; s \<approx>sources as s u\<approx> t; s \<sim>schedDomain\<sim> t; ipurge u as {t} = ipurge u bs {t}; ipurge u as {s} = ipurge u bs {t}; ipurge u bs {s} = ipurge u bs {t}; obs_equiv s as t (ipurge u bs {t}) u; t \<approx>sources bs t u\<approx> t \<longrightarrow> t \<sim>schedDomain\<sim> t \<longrightarrow> obs_equiv t bs t (ipurge u bs {t}) u\<rbrakk> \<Longrightarrow> obs_equiv t (?bs28 u as bs s t) t bs u proof (prove)
goal (1 subgoal):
 1. \<And>u as bs s t. \<lbrakk>confidentiality_u; reachable s; reachable t; s \<approx>sources as s u\<approx> t; s \<sim>schedDomain\<sim> t; ipurge u as {t} = ipurge u bs {t}; ipurge u as {s} = ipurge u bs {t}; ipurge u bs {s} = ipurge u bs {t}; obs_equiv s as t (ipurge u bs {t}) u; t \<approx>sources bs t u\<approx> t \<longrightarrow> t \<sim>schedDomain\<sim> t \<longrightarrow> obs_equiv t bs t (ipurge u bs {t}) u\<rbrakk> \<Longrightarrow> obs_equiv t (ipurge u bs {t}) t bs u proof (prove)
goal (1 subgoal):
 1. \<And>u as bs s t. \<lbrakk>confidentiality_u; reachable s; reachable t; s \<approx>sources as s u\<approx> t; s \<sim>schedDomain\<sim> t; ipurge u as {t} = ipurge u bs {t}; ipurge u as {s} = ipurge u bs {t}; ipurge u bs {s} = ipurge u bs {t}; obs_equiv s as t (ipurge u bs {t}) u; t \<approx>sources bs t u\<approx> t \<longrightarrow> t \<sim>schedDomain\<sim> t \<longrightarrow> obs_equiv t bs t (ipurge u bs {t}) u\<rbrakk> \<Longrightarrow> obs_equiv t bs t (ipurge u bs {t}) u proof (prove)
goal:
No subgoals!