theory Noninterference

lemma partitionIntegrity_trans:
  "\<lbrakk> partitionIntegrity aag s t; partitionIntegrity aag t u \<rbrakk>
     \<Longrightarrow> partitionIntegrity aag s u" apply (clarsimp simp: partitionIntegrity_def) apply (rule conjI) apply (blast intro: integrity_trans) apply (fastforce intro: domain_fields_equiv_trans simp: silc_dom_equiv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>partitionIntegrity aag s t; partitionIntegrity aag t u\<rbrakk> \<Longrightarrow> partitionIntegrity aag s u proof (prove)
goal (1 subgoal):
 1. \<lbrakk>integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s t; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} t u; domain_fields_equiv s t; domain_fields_equiv t u; idle_thread s = idle_thread u; idle_thread t = idle_thread u; globals_equiv_scheduler s t; silc_dom_equiv aag s t; globals_equiv_scheduler t u; silc_dom_equiv aag t u\<rbrakk> \<Longrightarrow> integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s u \<and> domain_fields_equiv s u \<and> globals_equiv_scheduler s u \<and> silc_dom_equiv aag s u proof (prove)
goal (2 subgoals):
 1. \<lbrakk>integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s t; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} t u; domain_fields_equiv s t; domain_fields_equiv t u; idle_thread s = idle_thread u; idle_thread t = idle_thread u; globals_equiv_scheduler s t; silc_dom_equiv aag s t; globals_equiv_scheduler t u; silc_dom_equiv aag t u\<rbrakk> \<Longrightarrow> integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s u
 2. \<lbrakk>integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s t; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} t u; domain_fields_equiv s t; domain_fields_equiv t u; idle_thread s = idle_thread u; idle_thread t = idle_thread u; globals_equiv_scheduler s t; silc_dom_equiv aag s t; globals_equiv_scheduler t u; silc_dom_equiv aag t u\<rbrakk> \<Longrightarrow> domain_fields_equiv s u \<and> globals_equiv_scheduler s u \<and> silc_dom_equiv aag s u proof (prove)
goal (1 subgoal):
 1. \<lbrakk>integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} s t; integrity_subjects {pasSubject aag} (aag\<lparr>pasMayActivate := False, pasMayEditReadyQueues := False\<rparr>) False {} t u; domain_fields_equiv s t; domain_fields_equiv t u; idle_thread s = idle_thread u; idle_thread t = idle_thread u; globals_equiv_scheduler s t; silc_dom_equiv aag s t; globals_equiv_scheduler t u; silc_dom_equiv aag t u\<rbrakk> \<Longrightarrow> domain_fields_equiv s u \<and> globals_equiv_scheduler s u \<and> silc_dom_equiv aag s u proof (prove)
goal:
No subgoals!