theory Noninterference_Refinement

lemma inv_holds_transport:
  "\<lbrakk> A [> Ia; C [> Ic; LI A C R (Ia \<times> Ic) \<rbrakk> \<Longrightarrow> C [> {s'. \<exists>s. (s,s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ic}" apply (clarsimp simp: LI_def inv_holds_def) apply (erule_tac x=j in allE)+ apply (clarsimp simp: rel_semi_def) apply (subgoal_tac "(s,x) \<in> Step A j O R") prefer 2 apply blast apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A [> Ia; C [> Ic; LI A C R (Ia \<times> Ic)\<rbrakk> \<Longrightarrow> C [> {s'. \<exists>s. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ic} proof (prove)
goal (1 subgoal):
 1. \<And>j x xa s. \<lbrakk>\<forall>j. Step A j `` Ia \<subseteq> Ia; \<forall>j. Step C j `` Ic \<subseteq> Ic; (xa, x) \<in> Step C j; \<forall>s. Init C s \<subseteq> R `` Init A s; (s, xa) \<in> R; \<forall>j. R \<inter> Ia \<times> Ic ;;; Step C j \<subseteq> Step A j ;;; R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; s \<in> Ia; xa \<in> Ic\<rbrakk> \<Longrightarrow> \<exists>s. (s, x) \<in> R \<and> s \<in> Ia \<and> x \<in> Ic proof (prove)
goal (1 subgoal):
 1. \<And>j x xa s. \<lbrakk>(xa, x) \<in> Step C j; \<forall>s. Init C s \<subseteq> R `` Init A s; (s, xa) \<in> R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; s \<in> Ia; xa \<in> Ic; Step A j `` Ia \<subseteq> Ia; Step C j `` Ic \<subseteq> Ic; R \<inter> Ia \<times> Ic ;;; Step C j \<subseteq> Step A j ;;; R\<rbrakk> \<Longrightarrow> \<exists>s. (s, x) \<in> R \<and> s \<in> Ia \<and> x \<in> Ic proof (prove)
goal (1 subgoal):
 1. \<And>j x xa s. \<lbrakk>(xa, x) \<in> Step C j; \<forall>s. Init C s \<subseteq> R `` Init A s; (s, xa) \<in> R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; s \<in> Ia; xa \<in> Ic; Step A j `` Ia \<subseteq> Ia; Step C j `` Ic \<subseteq> Ic; (R \<inter> Ia \<times> Ic) O Step C j \<subseteq> Step A j O R\<rbrakk> \<Longrightarrow> \<exists>s. (s, x) \<in> R \<and> s \<in> Ia \<and> x \<in> Ic proof (prove)
goal (2 subgoals):
 1. \<And>j x xa s. \<lbrakk>(xa, x) \<in> Step C j; \<forall>s. Init C s \<subseteq> R `` Init A s; (s, xa) \<in> R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; s \<in> Ia; xa \<in> Ic; Step A j `` Ia \<subseteq> Ia; Step C j `` Ic \<subseteq> Ic; (R \<inter> Ia \<times> Ic) O Step C j \<subseteq> Step A j O R; (s, x) \<in> Step A j O R\<rbrakk> \<Longrightarrow> \<exists>s. (s, x) \<in> R \<and> s \<in> Ia \<and> x \<in> Ic
 2. \<And>j x xa s. \<lbrakk>(xa, x) \<in> Step C j; \<forall>s. Init C s \<subseteq> R `` Init A s; (s, xa) \<in> R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; s \<in> Ia; xa \<in> Ic; Step A j `` Ia \<subseteq> Ia; Step C j `` Ic \<subseteq> Ic; (R \<inter> Ia \<times> Ic) O Step C j \<subseteq> Step A j O R\<rbrakk> \<Longrightarrow> (s, x) \<in> Step A j O R proof (prove)
goal (2 subgoals):
 1. \<And>j x xa s. \<lbrakk>(xa, x) \<in> Step C j; \<forall>s. Init C s \<subseteq> R `` Init A s; (s, xa) \<in> R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; s \<in> Ia; xa \<in> Ic; Step A j `` Ia \<subseteq> Ia; Step C j `` Ic \<subseteq> Ic; (R \<inter> Ia \<times> Ic) O Step C j \<subseteq> Step A j O R\<rbrakk> \<Longrightarrow> (s, x) \<in> Step A j O R
 2. \<And>j x xa s. \<lbrakk>(xa, x) \<in> Step C j; \<forall>s. Init C s \<subseteq> R `` Init A s; (s, xa) \<in> R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; s \<in> Ia; xa \<in> Ic; Step A j `` Ia \<subseteq> Ia; Step C j `` Ic \<subseteq> Ic; (R \<inter> Ia \<times> Ic) O Step C j \<subseteq> Step A j O R; (s, x) \<in> Step A j O R\<rbrakk> \<Longrightarrow> \<exists>s. (s, x) \<in> R \<and> s \<in> Ia \<and> x \<in> Ic proof (prove)
goal (1 subgoal):
 1. \<And>j x xa s. \<lbrakk>(xa, x) \<in> Step C j; \<forall>s. Init C s \<subseteq> R `` Init A s; (s, xa) \<in> R; \<forall>s s'. (s, s') \<in> R \<and> s \<in> Ia \<and> s' \<in> Ic \<longrightarrow> Fin C s' = Fin A s; s \<in> Ia; xa \<in> Ic; Step A j `` Ia \<subseteq> Ia; Step C j `` Ic \<subseteq> Ic; (R \<inter> Ia \<times> Ic) O Step C j \<subseteq> Step A j O R; (s, x) \<in> Step A j O R\<rbrakk> \<Longrightarrow> \<exists>s. (s, x) \<in> R \<and> s \<in> Ia \<and> x \<in> Ic proof (prove)
goal:
No subgoals!