theory Noninterference

lemma dmo_device_update_respects_Write:
  "\<lbrace>integrity aag X st and K (\<forall>p \<in> dom um'. aag_has_auth_to aag Write p)\<rbrace>
   do_machine_op (device_memory_update um')
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: device_memory_update_def) apply (rule hoare_pre) apply (wp dmo_wp) apply clarsimp apply (simp cong: abstract_state.fold_congs) apply (rule integrity_device_state_update) apply simp apply clarify apply (drule (1) bspec) apply simp apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and K (\<forall>p\<in>dom um'. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag)\<rbrace> do_machine_op (device_memory_update um') \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and (\<lambda>y. \<forall>p\<in>dom um'. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag)\<rbrace> do_machine_op (modify (\<lambda>ms. ms\<lparr>device_state := device_state ms ++ um'\<rparr>)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do_machine_op (modify (\<lambda>ms. ms\<lparr>device_state := device_state ms ++ um'\<rparr>)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>s. (integrity aag X st and (\<lambda>y. \<forall>p\<in>dom um'. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag)) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (integrity aag X st and (\<lambda>y. \<forall>p\<in>dom um'. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag)) s \<Longrightarrow> integrity aag X st (s\<lparr>machine_state := machine_state s\<lparr>device_state := device_state (machine_state s) ++ um'\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>integrity aag X st s; \<forall>p\<in>dom um'. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> integrity aag X st (s\<lparr>machine_state := machine_state s\<lparr>device_state := device_state (machine_state s) ++ um'\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>integrity aag X st s; \<forall>p\<in>dom um'. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> integrity aag X st (machine_state_update (\<lambda>a. a\<lparr>device_state := device_state a ++ um'\<rparr>) s) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>integrity aag X st s; \<forall>p\<in>dom um'. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> integrity aag X st s
 2. \<And>s. \<lbrakk>integrity aag X st s; \<forall>p\<in>dom um'. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> \<forall>x\<in>?xs8 s. (pasSubject aag, Write, pasObjectAbs aag x) \<in> pasPolicy aag
 3. \<And>s. \<lbrakk>integrity aag X st s; \<forall>p\<in>dom um'. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> \<forall>x\<in>- ?xs8 s. um' x = None proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>integrity aag X st s; \<forall>p\<in>dom um'. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> \<forall>x\<in>?xs8 s. (pasSubject aag, Write, pasObjectAbs aag x) \<in> pasPolicy aag
 2. \<And>s. \<lbrakk>integrity aag X st s; \<forall>p\<in>dom um'. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> \<forall>x\<in>- ?xs8 s. um' x = None proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>integrity aag X st s; \<forall>p\<in>dom um'. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag; x \<in> ?xs8 s\<rbrakk> \<Longrightarrow> (pasSubject aag, Write, pasObjectAbs aag x) \<in> pasPolicy aag
 2. \<And>s. \<lbrakk>integrity aag X st s; \<forall>p\<in>dom um'. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> \<forall>x\<in>- ?xs8 s. um' x = None proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>integrity aag X st s; x \<in> dom um'; (pasSubject aag, Write, pasObjectAbs aag x) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasSubject aag, Write, pasObjectAbs aag x) \<in> pasPolicy aag
 2. \<And>s. \<lbrakk>integrity aag X st s; \<forall>p\<in>dom um'. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> \<forall>x\<in>- dom um'. um' x = None proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>integrity aag X st s; \<forall>p\<in>dom um'. (pasSubject aag, Write, pasObjectAbs aag p) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> \<forall>x\<in>- dom um'. um' x = None proof (prove)
goal:
No subgoals!