theory Noninterference

lemma relation_preserved_across_sub_big_steps:
  "\<lbrakk> (s', as) \<in> sub_big_steps A R s; (t', as') \<in> sub_big_steps A R t; X s t; as' = as;
     \<forall>sa ta sa' ta'. X sa ta \<and>
       (\<exists>bs. (sa,bs) \<in> sub_big_steps A R s \<and> (sa',bs @ [()]) \<in> sub_big_steps A R s) \<and>
       (\<exists>cs. (ta,cs) \<in> sub_big_steps A R t \<and> (sa',cs @ [()]) \<in> sub_big_steps A R s) \<and>
       (sa,sa') \<in> data_type.Step A () \<and> (ta,ta') \<in> data_type.Step A ()
       \<longrightarrow> X sa' ta' \<rbrakk>
     \<Longrightarrow> X s' t'" apply hypsubst_thin apply (induct as arbitrary: s t s' t' rule: rev_induct) apply (drule sub_big_steps_Nil)+ apply simp apply (frule_tac s=s in sub_big_steps_App) apply (frule_tac s=t in sub_big_steps_App) apply clarify apply (drule_tac x=s in meta_spec) apply (drule_tac x=t in meta_spec) apply (drule_tac x=s'a in meta_spec) apply (drule_tac x=s'aa in meta_spec) apply simp apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s', as) \<in> sub_big_steps A R s; (t', as') \<in> sub_big_steps A R t; X s t; as' = as; \<forall>sa ta sa' ta'. X sa ta \<and> (\<exists>bs. (sa, bs) \<in> sub_big_steps A R s \<and> (sa', bs @ [()]) \<in> sub_big_steps A R s) \<and> (\<exists>cs. (ta, cs) \<in> sub_big_steps A R t \<and> (sa', cs @ [()]) \<in> sub_big_steps A R s) \<and> (sa, sa') \<in> data_type.Step A () \<and> (ta, ta') \<in> data_type.Step A () \<longrightarrow> X sa' ta'\<rbrakk> \<Longrightarrow> X s' t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s', as) \<in> sub_big_steps A R s; (t', as) \<in> sub_big_steps A R t; X s t; \<forall>sa ta sa' ta'. X sa ta \<and> (\<exists>bs. (sa, bs) \<in> sub_big_steps A R s \<and> (sa', bs @ [()]) \<in> sub_big_steps A R s) \<and> (\<exists>cs. (ta, cs) \<in> sub_big_steps A R t \<and> (sa', cs @ [()]) \<in> sub_big_steps A R s) \<and> (sa, sa') \<in> data_type.Step A () \<and> (ta, ta') \<in> data_type.Step A () \<longrightarrow> X sa' ta'\<rbrakk> \<Longrightarrow> X s' t' proof (prove)
goal (2 subgoals):
 1. \<And>s t s' t'. \<lbrakk>(s', []) \<in> sub_big_steps A R s; (t', []) \<in> sub_big_steps A R t; X s t; \<forall>sa ta sa' ta'. X sa ta \<and> (\<exists>bs. (sa, bs) \<in> sub_big_steps A R s \<and> (sa', bs @ [()]) \<in> sub_big_steps A R s) \<and> (\<exists>cs. (ta, cs) \<in> sub_big_steps A R t \<and> (sa', cs @ [()]) \<in> sub_big_steps A R s) \<and> (sa, sa') \<in> data_type.Step A () \<and> (ta, ta') \<in> data_type.Step A () \<longrightarrow> X sa' ta'\<rbrakk> \<Longrightarrow> X s' t'
 2. \<And>x xs s t s' t'. \<lbrakk>\<And>s t s' t'. \<lbrakk>(s', xs) \<in> sub_big_steps A R s; (t', xs) \<in> sub_big_steps A R t; X s t; \<forall>sa ta sa' ta'. X sa ta \<and> (\<exists>bs. (sa, bs) \<in> sub_big_steps A R s \<and> (sa', bs @ [()]) \<in> sub_big_steps A R s) \<and> (\<exists>cs. (ta, cs) \<in> sub_big_steps A R t \<and> (sa', cs @ [()]) \<in> sub_big_steps A R s) \<and> (sa, sa') \<in> data_type.Step A () \<and> (ta, ta') \<in> data_type.Step A () \<longrightarrow> X sa' ta'\<rbrakk> \<Longrightarrow> X s' t'; (s', xs @ [x]) \<in> sub_big_steps A R s; (t', xs @ [x]) \<in> sub_big_steps A R t; X s t; \<forall>sa ta sa' ta'. X sa ta \<and> (\<exists>bs. (sa, bs) \<in> sub_big_steps A R s \<and> (sa', bs @ [()]) \<in> sub_big_steps A R s) \<and> (\<exists>cs. (ta, cs) \<in> sub_big_steps A R t \<and> (sa', cs @ [()]) \<in> sub_big_steps A R s) \<and> (sa, sa') \<in> data_type.Step A () \<and> (ta, ta') \<in> data_type.Step A () \<longrightarrow> X sa' ta'\<rbrakk> \<Longrightarrow> X s' t' proof (prove)
goal (2 subgoals):
 1. \<And>s t s' t'. \<lbrakk>X s t; \<forall>sa ta sa' ta'. X sa ta \<and> (\<exists>bs. (sa, bs) \<in> sub_big_steps A R s \<and> (sa', bs @ [()]) \<in> sub_big_steps A R s) \<and> (\<exists>cs. (ta, cs) \<in> sub_big_steps A R t \<and> (sa', cs @ [()]) \<in> sub_big_steps A R s) \<and> (sa, sa') \<in> data_type.Step A () \<and> (ta, ta') \<in> data_type.Step A () \<longrightarrow> X sa' ta'; s' = s \<and> \<not> R s s; t' = t \<and> \<not> R t t\<rbrakk> \<Longrightarrow> X s' t'
 2. \<And>x xs s t s' t'. \<lbrakk>\<And>s t s' t'. \<lbrakk>(s', xs) \<in> sub_big_steps A R s; (t', xs) \<in> sub_big_steps A R t; X s t; \<forall>sa ta sa' ta'. X sa ta \<and> (\<exists>bs. (sa, bs) \<in> sub_big_steps A R s \<and> (sa', bs @ [()]) \<in> sub_big_steps A R s) \<and> (\<exists>cs. (ta, cs) \<in> sub_big_steps A R t \<and> (sa', cs @ [()]) \<in> sub_big_steps A R s) \<and> (sa, sa') \<in> data_type.Step A () \<and> (ta, ta') \<in> data_type.Step A () \<longrightarrow> X sa' ta'\<rbrakk> \<Longrightarrow> X s' t'; (s', xs @ [x]) \<in> sub_big_steps A R s; (t', xs @ [x]) \<in> sub_big_steps A R t; X s t; \<forall>sa ta sa' ta'. X sa ta \<and> (\<exists>bs. (sa, bs) \<in> sub_big_steps A R s \<and> (sa', bs @ [()]) \<in> sub_big_steps A R s) \<and> (\<exists>cs. (ta, cs) \<in> sub_big_steps A R t \<and> (sa', cs @ [()]) \<in> sub_big_steps A R s) \<and> (sa, sa') \<in> data_type.Step A () \<and> (ta, ta') \<in> data_type.Step A () \<longrightarrow> X sa' ta'\<rbrakk> \<Longrightarrow> X s' t' proof (prove)
goal (1 subgoal):
 1. \<And>x xs s t s' t'. \<lbrakk>\<And>s t s' t'. \<lbrakk>(s', xs) \<in> sub_big_steps A R s; (t', xs) \<in> sub_big_steps A R t; X s t; \<forall>sa ta sa' ta'. X sa ta \<and> (\<exists>bs. (sa, bs) \<in> sub_big_steps A R s \<and> (sa', bs @ [()]) \<in> sub_big_steps A R s) \<and> (\<exists>cs. (ta, cs) \<in> sub_big_steps A R t \<and> (sa', cs @ [()]) \<in> sub_big_steps A R s) \<and> (sa, sa') \<in> data_type.Step A () \<and> (ta, ta') \<in> data_type.Step A () \<longrightarrow> X sa' ta'\<rbrakk> \<Longrightarrow> X s' t'; (s', xs @ [x]) \<in> sub_big_steps A R s; (t', xs @ [x]) \<in> sub_big_steps A R t; X s t; \<forall>sa ta sa' ta'. X sa ta \<and> (\<exists>bs. (sa, bs) \<in> sub_big_steps A R s \<and> (sa', bs @ [()]) \<in> sub_big_steps A R s) \<and> (\<exists>cs. (ta, cs) \<in> sub_big_steps A R t \<and> (sa', cs @ [()]) \<in> sub_big_steps A R s) \<and> (sa, sa') \<in> data_type.Step A () \<and> (ta, ta') \<in> data_type.Step A () \<longrightarrow> X sa' ta'\<rbrakk> \<Longrightarrow> X s' t' proof (prove)
goal (1 subgoal):
 1. \<And>x xs s t s' t'. \<lbrakk>\<And>s t s' t'. \<lbrakk>(s', xs) \<in> sub_big_steps A R s; (t', xs) \<in> sub_big_steps A R t; X s t; \<forall>sa ta sa' ta'. X sa ta \<and> (\<exists>bs. (sa, bs) \<in> sub_big_steps A R s \<and> (sa', bs @ [()]) \<in> sub_big_steps A R s) \<and> (\<exists>cs. (ta, cs) \<in> sub_big_steps A R t \<and> (sa', cs @ [()]) \<in> sub_big_steps A R s) \<and> (sa, sa') \<in> data_type.Step A () \<and> (ta, ta') \<in> data_type.Step A () \<longrightarrow> X sa' ta'\<rbrakk> \<Longrightarrow> X s' t'; (s', xs @ [x]) \<in> sub_big_steps A R s; (t', xs @ [x]) \<in> sub_big_steps A R t; X s t; \<forall>sa ta sa' ta'. X sa ta \<and> (\<exists>bs. (sa, bs) \<in> sub_big_steps A R s \<and> (sa', bs @ [()]) \<in> sub_big_steps A R s) \<and> (\<exists>cs. (ta, cs) \<in> sub_big_steps A R t \<and> (sa', cs @ [()]) \<in> sub_big_steps A R s) \<and> (sa, sa') \<in> data_type.Step A () \<and> (ta, ta') \<in> data_type.Step A () \<longrightarrow> X sa' ta'; \<exists>s'a. (s'a, xs) \<in> sub_big_steps A R s \<and> (s'a, s') \<in> data_type.Step A x \<and> \<not> R s s'\<rbrakk> \<Longrightarrow> X s' t' proof (prove)
goal (1 subgoal):
 1. \<And>x xs s t s' t'. \<lbrakk>\<And>s t s' t'. \<lbrakk>(s', xs) \<in> sub_big_steps A R s; (t', xs) \<in> sub_big_steps A R t; X s t; \<forall>sa ta sa' ta'. X sa ta \<and> (\<exists>bs. (sa, bs) \<in> sub_big_steps A R s \<and> (sa', bs @ [()]) \<in> sub_big_steps A R s) \<and> (\<exists>cs. (ta, cs) \<in> sub_big_steps A R t \<and> (sa', cs @ [()]) \<in> sub_big_steps A R s) \<and> (sa, sa') \<in> data_type.Step A () \<and> (ta, ta') \<in> data_type.Step A () \<longrightarrow> X sa' ta'\<rbrakk> \<Longrightarrow> X s' t'; (s', xs @ [x]) \<in> sub_big_steps A R s; (t', xs @ [x]) \<in> sub_big_steps A R t; X s t; \<forall>sa ta sa' ta'. X sa ta \<and> (\<exists>bs. (sa, bs) \<in> sub_big_steps A R s \<and> (sa', bs @ [()]) \<in> sub_big_steps A R s) \<and> (\<exists>cs. (ta, cs) \<in> sub_big_steps A R t \<and> (sa', cs @ [()]) \<in> sub_big_steps A R s) \<and> (sa, sa') \<in> data_type.Step A () \<and> (ta, ta') \<in> data_type.Step A () \<longrightarrow> X sa' ta'; \<exists>s'a. (s'a, xs) \<in> sub_big_steps A R s \<and> (s'a, s') \<in> data_type.Step A x \<and> \<not> R s s'; \<exists>s'a. (s'a, xs) \<in> sub_big_steps A R t \<and> (s'a, t') \<in> data_type.Step A x \<and> \<not> R t t'\<rbrakk> \<Longrightarrow> X s' t' proof (prove)
goal (1 subgoal):
 1. \<And>x xs s t s' t' s'a s'aa. \<lbrakk>\<And>s t s' t'. \<lbrakk>(s', xs) \<in> sub_big_steps A R s; (t', xs) \<in> sub_big_steps A R t; X s t; \<forall>sa ta sa' ta'. X sa ta \<and> (\<exists>bs. (sa, bs) \<in> sub_big_steps A R s \<and> (sa', bs @ [()]) \<in> sub_big_steps A R s) \<and> (\<exists>cs. (ta, cs) \<in> sub_big_steps A R t \<and> (sa', cs @ [()]) \<in> sub_big_steps A R s) \<and> (sa, sa') \<in> data_type.Step A () \<and> (ta, ta') \<in> data_type.Step A () \<longrightarrow> X sa' ta'\<rbrakk> \<Longrightarrow> X s' t'; (s', xs @ [x]) \<in> sub_big_steps A R s; (t', xs @ [x]) \<in> sub_big_steps A R t; X s t; \<forall>sa ta sa' ta'. X sa ta \<and> (\<exists>bs. (sa, bs) \<in> sub_big_steps A R s \<and> (sa', bs @ [()]) \<in> sub_big_steps A R s) \<and> (\<exists>cs. (ta, cs) \<in> sub_big_steps A R t \<and> (sa', cs @ [()]) \<in> sub_big_steps A R s) \<and> (sa, sa') \<in> data_type.Step A () \<and> (ta, ta') \<in> data_type.Step A () \<longrightarrow> X sa' ta'; (s'a, xs) \<in> sub_big_steps A R s; (s'aa, xs) \<in> sub_big_steps A R t; (s'a, s') \<in> data_type.Step A x; \<not> R s s'; (s'aa, t') \<in> data_type.Step A x; \<not> R t t'\<rbrakk> \<Longrightarrow> X s' t' proof (prove)
goal (1 subgoal):
 1. \<And>x xs s t s' t' s'a s'aa. \<lbrakk>(s', xs @ [x]) \<in> sub_big_steps A R s; (t', xs @ [x]) \<in> sub_big_steps A R t; X s t; \<forall>sa ta sa' ta'. X sa ta \<and> (\<exists>bs. (sa, bs) \<in> sub_big_steps A R s \<and> (sa', bs @ [()]) \<in> sub_big_steps A R s) \<and> (\<exists>cs. (ta, cs) \<in> sub_big_steps A R t \<and> (sa', cs @ [()]) \<in> sub_big_steps A R s) \<and> (sa, sa') \<in> data_type.Step A () \<and> (ta, ta') \<in> data_type.Step A () \<longrightarrow> X sa' ta'; (s'a, xs) \<in> sub_big_steps A R s; (s'aa, xs) \<in> sub_big_steps A R t; (s'a, s') \<in> data_type.Step A x; \<not> R s s'; (s'aa, t') \<in> data_type.Step A x; \<not> R t t'; \<And>t s' t'. \<lbrakk>(s', xs) \<in> sub_big_steps A R s; (t', xs) \<in> sub_big_steps A R t; X s t; \<forall>sa ta sa' ta'. X sa ta \<and> (\<exists>bs. (sa, bs) \<in> sub_big_steps A R s \<and> (sa', bs @ [()]) \<in> sub_big_steps A R s) \<and> (\<exists>cs. (ta, cs) \<in> sub_big_steps A R t \<and> (sa', cs @ [()]) \<in> sub_big_steps A R s) \<and> (sa, sa') \<in> data_type.Step A () \<and> (ta, ta') \<in> data_type.Step A () \<longrightarrow> X sa' ta'\<rbrakk> \<Longrightarrow> X s' t'\<rbrakk> \<Longrightarrow> X s' t' proof (prove)
goal (1 subgoal):
 1. \<And>x xs s t s' t' s'a s'aa. \<lbrakk>(s', xs @ [x]) \<in> sub_big_steps A R s; (t', xs @ [x]) \<in> sub_big_steps A R t; X s t; \<forall>sa ta sa' ta'. X sa ta \<and> (\<exists>bs. (sa, bs) \<in> sub_big_steps A R s \<and> (sa', bs @ [()]) \<in> sub_big_steps A R s) \<and> (\<exists>cs. (ta, cs) \<in> sub_big_steps A R t \<and> (sa', cs @ [()]) \<in> sub_big_steps A R s) \<and> (sa, sa') \<in> data_type.Step A () \<and> (ta, ta') \<in> data_type.Step A () \<longrightarrow> X sa' ta'; (s'a, xs) \<in> sub_big_steps A R s; (s'aa, xs) \<in> sub_big_steps A R t; (s'a, s') \<in> data_type.Step A x; \<not> R s s'; (s'aa, t') \<in> data_type.Step A x; \<not> R t t'; \<And>s' t'. \<lbrakk>(s', xs) \<in> sub_big_steps A R s; (t', xs) \<in> sub_big_steps A R t; X s t; \<forall>sa ta sa' ta'. X sa ta \<and> (\<exists>bs. (sa, bs) \<in> sub_big_steps A R s \<and> (sa', bs @ [()]) \<in> sub_big_steps A R s) \<and> (\<exists>cs. (ta, cs) \<in> sub_big_steps A R t \<and> (sa', cs @ [()]) \<in> sub_big_steps A R s) \<and> (sa, sa') \<in> data_type.Step A () \<and> (ta, ta') \<in> data_type.Step A () \<longrightarrow> X sa' ta'\<rbrakk> \<Longrightarrow> X s' t'\<rbrakk> \<Longrightarrow> X s' t' proof (prove)
goal (1 subgoal):
 1. \<And>x xs s t s' t' s'a s'aa. \<lbrakk>(s', xs @ [x]) \<in> sub_big_steps A R s; (t', xs @ [x]) \<in> sub_big_steps A R t; X s t; \<forall>sa ta sa' ta'. X sa ta \<and> (\<exists>bs. (sa, bs) \<in> sub_big_steps A R s \<and> (sa', bs @ [()]) \<in> sub_big_steps A R s) \<and> (\<exists>cs. (ta, cs) \<in> sub_big_steps A R t \<and> (sa', cs @ [()]) \<in> sub_big_steps A R s) \<and> (sa, sa') \<in> data_type.Step A () \<and> (ta, ta') \<in> data_type.Step A () \<longrightarrow> X sa' ta'; (s'a, xs) \<in> sub_big_steps A R s; (s'aa, xs) \<in> sub_big_steps A R t; (s'a, s') \<in> data_type.Step A x; \<not> R s s'; (s'aa, t') \<in> data_type.Step A x; \<not> R t t'; \<And>t'. \<lbrakk>(s'a, xs) \<in> sub_big_steps A R s; (t', xs) \<in> sub_big_steps A R t; X s t; \<forall>sa ta sa' ta'. X sa ta \<and> (\<exists>bs. (sa, bs) \<in> sub_big_steps A R s \<and> (sa', bs @ [()]) \<in> sub_big_steps A R s) \<and> (\<exists>cs. (ta, cs) \<in> sub_big_steps A R t \<and> (sa', cs @ [()]) \<in> sub_big_steps A R s) \<and> (sa, sa') \<in> data_type.Step A () \<and> (ta, ta') \<in> data_type.Step A () \<longrightarrow> X sa' ta'\<rbrakk> \<Longrightarrow> X s'a t'\<rbrakk> \<Longrightarrow> X s' t' proof (prove)
goal (1 subgoal):
 1. \<And>x xs s t s' t' s'a s'aa. \<lbrakk>(s', xs @ [x]) \<in> sub_big_steps A R s; (t', xs @ [x]) \<in> sub_big_steps A R t; X s t; \<forall>sa ta sa' ta'. X sa ta \<and> (\<exists>bs. (sa, bs) \<in> sub_big_steps A R s \<and> (sa', bs @ [()]) \<in> sub_big_steps A R s) \<and> (\<exists>cs. (ta, cs) \<in> sub_big_steps A R t \<and> (sa', cs @ [()]) \<in> sub_big_steps A R s) \<and> (sa, sa') \<in> data_type.Step A () \<and> (ta, ta') \<in> data_type.Step A () \<longrightarrow> X sa' ta'; (s'a, xs) \<in> sub_big_steps A R s; (s'aa, xs) \<in> sub_big_steps A R t; (s'a, s') \<in> data_type.Step A x; \<not> R s s'; (s'aa, t') \<in> data_type.Step A x; \<not> R t t'; \<lbrakk>(s'a, xs) \<in> sub_big_steps A R s; (s'aa, xs) \<in> sub_big_steps A R t; X s t; \<forall>sa ta sa' ta'. X sa ta \<and> (\<exists>bs. (sa, bs) \<in> sub_big_steps A R s \<and> (sa', bs @ [()]) \<in> sub_big_steps A R s) \<and> (\<exists>cs. (ta, cs) \<in> sub_big_steps A R t \<and> (sa', cs @ [()]) \<in> sub_big_steps A R s) \<and> (sa, sa') \<in> data_type.Step A () \<and> (ta, ta') \<in> data_type.Step A () \<longrightarrow> X sa' ta'\<rbrakk> \<Longrightarrow> X s'a s'aa\<rbrakk> \<Longrightarrow> X s' t' proof (prove)
goal (1 subgoal):
 1. \<And>xs s t s' t' s'a s'aa. \<lbrakk>(s', xs @ [()]) \<in> sub_big_steps A R s; (t', xs @ [()]) \<in> sub_big_steps A R t; X s t; \<forall>sa ta sa' ta'. X sa ta \<and> (\<exists>bs. (sa, bs) \<in> sub_big_steps A R s \<and> (sa', bs @ [()]) \<in> sub_big_steps A R s) \<and> (\<exists>cs. (ta, cs) \<in> sub_big_steps A R t \<and> (sa', cs @ [()]) \<in> sub_big_steps A R s) \<and> (sa, sa') \<in> data_type.Step A () \<and> (ta, ta') \<in> data_type.Step A () \<longrightarrow> X sa' ta'; (s'a, xs) \<in> sub_big_steps A R s; (s'aa, xs) \<in> sub_big_steps A R t; (s'a, s') \<in> data_type.Step A (); \<not> R s s'; (s'aa, t') \<in> data_type.Step A (); \<not> R t t'; X s'a s'aa\<rbrakk> \<Longrightarrow> X s' t' proof (prove)
goal:
No subgoals!