theory Noninterference_Base

lemma integrity_u_and_single_event_systems:
  "\<lbrakk> integrity_u; reachable s; dom a s \<noteq> schedDomain; s' \<in> execution A s as; \<forall>y. y = a \<rbrakk>
     \<Longrightarrow> dom e s' \<noteq> schedDomain" apply (frule_tac x=e in spec) apply (erule ssubst) apply (rule_tac P="\<lambda>x. x \<noteq> schedDomain" in subst[rotated]) apply assumption apply (induct as arbitrary: s s' a rule: rev_induct) apply (simp add: execution_Run) apply (simp add: execution_Run) apply (drule Run_mid) apply (erule exE, rename_tac t) apply (drule_tac x=s in meta_spec) apply (drule_tac x=t in meta_spec) apply (drule_tac x=a in meta_spec) apply simp apply (rule schedIncludesCurrentDom) apply (rule non_sched_doms_cannot_schedule) apply assumption apply (rule reachable_execution) apply assumption apply (fastforce simp: execution_Run) apply assumption apply (drule_tac x=x in spec) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>integrity_u; reachable s; dom a s \<noteq> schedDomain; s' \<in> execution A s as; \<forall>y. y = a\<rbrakk> \<Longrightarrow> dom e s' \<noteq> schedDomain proof (prove)
goal (1 subgoal):
 1. \<lbrakk>integrity_u; reachable s; dom a s \<noteq> schedDomain; s' \<in> execution A s as; \<forall>y. y = a; e = a\<rbrakk> \<Longrightarrow> dom e s' \<noteq> schedDomain proof (prove)
goal (1 subgoal):
 1. \<lbrakk>integrity_u; reachable s; dom a s \<noteq> schedDomain; s' \<in> execution A s as; \<forall>y. y = a\<rbrakk> \<Longrightarrow> dom a s' \<noteq> schedDomain proof (prove)
goal (2 subgoals):
 1. \<lbrakk>integrity_u; reachable s; dom a s \<noteq> schedDomain; s' \<in> execution A s as; \<forall>y. y = a\<rbrakk> \<Longrightarrow> ?s4 \<noteq> schedDomain
 2. \<lbrakk>integrity_u; reachable s; dom a s \<noteq> schedDomain; s' \<in> execution A s as; \<forall>y. y = a\<rbrakk> \<Longrightarrow> ?s4 = dom a s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>integrity_u; reachable s; dom a s \<noteq> schedDomain; s' \<in> execution A s as; \<forall>y. y = a\<rbrakk> \<Longrightarrow> dom a s = dom a s' proof (prove)
goal (2 subgoals):
 1. \<And>s s' a. \<lbrakk>integrity_u; reachable s; dom a s \<noteq> schedDomain; s' \<in> execution A s []; \<forall>y. y = a\<rbrakk> \<Longrightarrow> dom a s = dom a s'
 2. \<And>x xs s s' a. \<lbrakk>\<And>s s' a. \<lbrakk>integrity_u; reachable s; dom a s \<noteq> schedDomain; s' \<in> execution A s xs; \<forall>y. y = a\<rbrakk> \<Longrightarrow> dom a s = dom a s'; integrity_u; reachable s; dom a s \<noteq> schedDomain; s' \<in> execution A s (xs @ [x]); \<forall>y. y = a\<rbrakk> \<Longrightarrow> dom a s = dom a s' proof (prove)
goal (1 subgoal):
 1. \<And>x xs s s' a. \<lbrakk>\<And>s s' a. \<lbrakk>integrity_u; reachable s; dom a s \<noteq> schedDomain; s' \<in> execution A s xs; \<forall>y. y = a\<rbrakk> \<Longrightarrow> dom a s = dom a s'; integrity_u; reachable s; dom a s \<noteq> schedDomain; s' \<in> execution A s (xs @ [x]); \<forall>y. y = a\<rbrakk> \<Longrightarrow> dom a s = dom a s' proof (prove)
goal (1 subgoal):
 1. \<And>x xs s s' a. \<lbrakk>\<And>s s' a. \<lbrakk>reachable s; dom a s \<noteq> schedDomain; (s, s') \<in> Run local.Step xs; \<forall>y. y = a\<rbrakk> \<Longrightarrow> dom a s = dom a s'; integrity_u; reachable s; dom a s \<noteq> schedDomain; (s, s') \<in> Run local.Step (xs @ [x]); \<forall>y. y = a\<rbrakk> \<Longrightarrow> dom a s = dom a s' proof (prove)
goal (1 subgoal):
 1. \<And>x xs s s' a. \<lbrakk>\<And>s s' a. \<lbrakk>reachable s; dom a s \<noteq> schedDomain; (s, s') \<in> Run local.Step xs; \<forall>y. y = a\<rbrakk> \<Longrightarrow> dom a s = dom a s'; integrity_u; reachable s; dom a s \<noteq> schedDomain; \<forall>y. y = a; \<exists>t. (s, t) \<in> Run local.Step xs \<and> (t, s') \<in> Run local.Step [x]\<rbrakk> \<Longrightarrow> dom a s = dom a s' proof (prove)
goal (1 subgoal):
 1. \<And>x xs s s' a t. \<lbrakk>\<And>s s' a. \<lbrakk>reachable s; dom a s \<noteq> schedDomain; (s, s') \<in> Run local.Step xs; \<forall>y. y = a\<rbrakk> \<Longrightarrow> dom a s = dom a s'; integrity_u; reachable s; dom a s \<noteq> schedDomain; \<forall>y. y = a; (s, t) \<in> Run local.Step xs \<and> (t, s') \<in> Run local.Step [x]\<rbrakk> \<Longrightarrow> dom a s = dom a s' proof (prove)
goal (1 subgoal):
 1. \<And>x xs s s' a t. \<lbrakk>integrity_u; reachable s; dom a s \<noteq> schedDomain; \<forall>y. y = a; (s, t) \<in> Run local.Step xs \<and> (t, s') \<in> Run local.Step [x]; \<And>s' a. \<lbrakk>reachable s; dom a s \<noteq> schedDomain; (s, s') \<in> Run local.Step xs; \<forall>y. y = a\<rbrakk> \<Longrightarrow> dom a s = dom a s'\<rbrakk> \<Longrightarrow> dom a s = dom a s' proof (prove)
goal (1 subgoal):
 1. \<And>x xs s s' a t. \<lbrakk>integrity_u; reachable s; dom a s \<noteq> schedDomain; \<forall>y. y = a; (s, t) \<in> Run local.Step xs \<and> (t, s') \<in> Run local.Step [x]; \<And>a. \<lbrakk>reachable s; dom a s \<noteq> schedDomain; (s, t) \<in> Run local.Step xs; \<forall>y. y = a\<rbrakk> \<Longrightarrow> dom a s = dom a t\<rbrakk> \<Longrightarrow> dom a s = dom a s' proof (prove)
goal (1 subgoal):
 1. \<And>x xs s s' a t. \<lbrakk>integrity_u; reachable s; dom a s \<noteq> schedDomain; \<forall>y. y = a; (s, t) \<in> Run local.Step xs \<and> (t, s') \<in> Run local.Step [x]; \<lbrakk>reachable s; dom a s \<noteq> schedDomain; (s, t) \<in> Run local.Step xs; \<forall>y. y = a\<rbrakk> \<Longrightarrow> dom a s = dom a t\<rbrakk> \<Longrightarrow> dom a s = dom a s' proof (prove)
goal (1 subgoal):
 1. \<And>x xs s s' a t. \<lbrakk>integrity_u; reachable s; dom a t \<noteq> schedDomain; \<forall>y. y = a; (s, t) \<in> Run local.Step xs \<and> (t, s') \<in> local.Step x; dom a s = dom a t\<rbrakk> \<Longrightarrow> dom a t = dom a s' proof (prove)
goal (1 subgoal):
 1. \<And>x xs s s' a t. \<lbrakk>integrity_u; reachable s; dom a t \<noteq> schedDomain; \<forall>y. y = a; (s, t) \<in> Run local.Step xs \<and> (t, s') \<in> local.Step x; dom a s = dom a t\<rbrakk> \<Longrightarrow> t \<sim>schedDomain\<sim> s' proof (prove)
goal (4 subgoals):
 1. \<And>x xs s s' a t. \<lbrakk>integrity_u; reachable s; dom a t \<noteq> schedDomain; \<forall>y. y = a; (s, t) \<in> Run local.Step xs \<and> (t, s') \<in> local.Step x; dom a s = dom a t\<rbrakk> \<Longrightarrow> integrity_u
 2. \<And>x xs s s' a t. \<lbrakk>integrity_u; reachable s; dom a t \<noteq> schedDomain; \<forall>y. y = a; (s, t) \<in> Run local.Step xs \<and> (t, s') \<in> local.Step x; dom a s = dom a t\<rbrakk> \<Longrightarrow> reachable t
 3. \<And>x xs s s' a t. \<lbrakk>integrity_u; reachable s; dom a t \<noteq> schedDomain; \<forall>y. y = a; (s, t) \<in> Run local.Step xs \<and> (t, s') \<in> local.Step x; dom a s = dom a t\<rbrakk> \<Longrightarrow> dom (?a14 x xs s s' a t) t \<noteq> schedDomain
 4. \<And>x xs s s' a t. \<lbrakk>integrity_u; reachable s; dom a t \<noteq> schedDomain; \<forall>y. y = a; (s, t) \<in> Run local.Step xs \<and> (t, s') \<in> local.Step x; dom a s = dom a t\<rbrakk> \<Longrightarrow> (t, s') \<in> local.Step (?a14 x xs s s' a t) proof (prove)
goal (3 subgoals):
 1. \<And>x xs s s' a t. \<lbrakk>integrity_u; reachable s; dom a t \<noteq> schedDomain; \<forall>y. y = a; (s, t) \<in> Run local.Step xs \<and> (t, s') \<in> local.Step x; dom a s = dom a t\<rbrakk> \<Longrightarrow> reachable t
 2. \<And>x xs s s' a t. \<lbrakk>integrity_u; reachable s; dom a t \<noteq> schedDomain; \<forall>y. y = a; (s, t) \<in> Run local.Step xs \<and> (t, s') \<in> local.Step x; dom a s = dom a t\<rbrakk> \<Longrightarrow> dom (?a14 x xs s s' a t) t \<noteq> schedDomain
 3. \<And>x xs s s' a t. \<lbrakk>integrity_u; reachable s; dom a t \<noteq> schedDomain; \<forall>y. y = a; (s, t) \<in> Run local.Step xs \<and> (t, s') \<in> local.Step x; dom a s = dom a t\<rbrakk> \<Longrightarrow> (t, s') \<in> local.Step (?a14 x xs s s' a t) proof (prove)
goal (4 subgoals):
 1. \<And>x xs s s' a t. \<lbrakk>integrity_u; reachable s; dom a t \<noteq> schedDomain; \<forall>y. y = a; (s, t) \<in> Run local.Step xs \<and> (t, s') \<in> local.Step x; dom a s = dom a t\<rbrakk> \<Longrightarrow> reachable (?s19 x xs s s' a t)
 2. \<And>x xs s s' a t. \<lbrakk>integrity_u; reachable s; dom a t \<noteq> schedDomain; \<forall>y. y = a; (s, t) \<in> Run local.Step xs \<and> (t, s') \<in> local.Step x; dom a s = dom a t\<rbrakk> \<Longrightarrow> t \<in> execution A (?s19 x xs s s' a t) (?js19 x xs s s' a t)
 3. \<And>x xs s s' a t. \<lbrakk>integrity_u; reachable s; dom a t \<noteq> schedDomain; \<forall>y. y = a; (s, t) \<in> Run local.Step xs \<and> (t, s') \<in> local.Step x; dom a s = dom a t\<rbrakk> \<Longrightarrow> dom (?a14 x xs s s' a t) t \<noteq> schedDomain
 4. \<And>x xs s s' a t. \<lbrakk>integrity_u; reachable s; dom a t \<noteq> schedDomain; \<forall>y. y = a; (s, t) \<in> Run local.Step xs \<and> (t, s') \<in> local.Step x; dom a s = dom a t\<rbrakk> \<Longrightarrow> (t, s') \<in> local.Step (?a14 x xs s s' a t) proof (prove)
goal (3 subgoals):
 1. \<And>x xs s s' a t. \<lbrakk>integrity_u; reachable s; dom a t \<noteq> schedDomain; \<forall>y. y = a; (s, t) \<in> Run local.Step xs \<and> (t, s') \<in> local.Step x; dom a s = dom a t\<rbrakk> \<Longrightarrow> t \<in> execution A s (?js19 x xs s s' a t)
 2. \<And>x xs s s' a t. \<lbrakk>integrity_u; reachable s; dom a t \<noteq> schedDomain; \<forall>y. y = a; (s, t) \<in> Run local.Step xs \<and> (t, s') \<in> local.Step x; dom a s = dom a t\<rbrakk> \<Longrightarrow> dom (?a14 x xs s s' a t) t \<noteq> schedDomain
 3. \<And>x xs s s' a t. \<lbrakk>integrity_u; reachable s; dom a t \<noteq> schedDomain; \<forall>y. y = a; (s, t) \<in> Run local.Step xs \<and> (t, s') \<in> local.Step x; dom a s = dom a t\<rbrakk> \<Longrightarrow> (t, s') \<in> local.Step (?a14 x xs s s' a t) proof (prove)
goal (2 subgoals):
 1. \<And>x xs s s' a t. \<lbrakk>integrity_u; reachable s; dom a t \<noteq> schedDomain; \<forall>y. y = a; (s, t) \<in> Run local.Step xs \<and> (t, s') \<in> local.Step x; dom a s = dom a t\<rbrakk> \<Longrightarrow> dom (?a14 x xs s s' a t) t \<noteq> schedDomain
 2. \<And>x xs s s' a t. \<lbrakk>integrity_u; reachable s; dom a t \<noteq> schedDomain; \<forall>y. y = a; (s, t) \<in> Run local.Step xs \<and> (t, s') \<in> local.Step x; dom a s = dom a t\<rbrakk> \<Longrightarrow> (t, s') \<in> local.Step (?a14 x xs s s' a t) proof (prove)
goal (1 subgoal):
 1. \<And>x xs s s' a t. \<lbrakk>integrity_u; reachable s; dom a t \<noteq> schedDomain; \<forall>y. y = a; (s, t) \<in> Run local.Step xs \<and> (t, s') \<in> local.Step x; dom a s = dom a t\<rbrakk> \<Longrightarrow> (t, s') \<in> local.Step a proof (prove)
goal (1 subgoal):
 1. \<And>x xs s s' a t. \<lbrakk>integrity_u; reachable s; dom a t \<noteq> schedDomain; (s, t) \<in> Run local.Step xs \<and> (t, s') \<in> local.Step x; dom a s = dom a t; x = a\<rbrakk> \<Longrightarrow> (t, s') \<in> local.Step a proof (prove)
goal:
No subgoals!