theory Noninterference_Refinement

lemma ADT_C_if_Init_Fin_serial:
  "Init_Fin_serial (ADT_C_if fp utf) s {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'}" apply (unfold_locales) apply (subgoal_tac "ADT_C_if fp utf \<Turnstile> P" for P) prefer 2 apply (rule fw_inv_transport) apply (rule global_automaton_invs.ADT_invs) apply (rule haskell_invs) apply (rule invariant_T) apply (rule global_automata_refine.fw_sim_abs_conc) apply (rule c_to_haskell) apply (rule uop_nonempty) apply simp apply (rule ADT_C_if_serial[rule_format]) apply simp apply (clarsimp simp: ADT_C_if_def lift_fst_rel_def lift_snd_rel_def) apply blast apply (clarsimp simp: lift_fst_rel_def lift_snd_rel_def ADT_C_if_def) apply (rule_tac x=bb in exI) apply (clarsimp simp: full_invs_if'_def) apply (case_tac "sys_mode_of s", simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Init_Fin_serial (ADT_C_if fp utf) s {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} proof (prove)
goal (4 subgoals):
 1. ADT_C_if fp utf \<Turnstile> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'}
 2. \<And>s' a. s' \<in> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} \<Longrightarrow> \<exists>t. (s', t) \<in> data_type.Step (ADT_C_if fp utf) a
 3. \<And>s'. s' \<in> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} \<Longrightarrow> s' \<in> Init (ADT_C_if fp utf) (Fin (ADT_C_if fp utf) s')
 4. Init (ADT_C_if fp utf) s \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} proof (prove)
goal (5 subgoals):
 1. ADT_C_if fp utf \<Turnstile> ?P6 \<Longrightarrow> ADT_C_if fp utf \<Turnstile> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'}
 2. ADT_C_if fp utf \<Turnstile> ?P6
 3. \<And>s' a. s' \<in> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} \<Longrightarrow> \<exists>t. (s', t) \<in> data_type.Step (ADT_C_if fp utf) a
 4. \<And>s'. s' \<in> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} \<Longrightarrow> s' \<in> Init (ADT_C_if fp utf) (Fin (ADT_C_if fp utf) s')
 5. Init (ADT_C_if fp utf) s \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} proof (prove)
goal (5 subgoals):
 1. ADT_C_if fp utf \<Turnstile> ?P6
 2. ADT_C_if fp utf \<Turnstile> ?P6 \<Longrightarrow> ADT_C_if fp utf \<Turnstile> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'}
 3. \<And>s' a. s' \<in> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} \<Longrightarrow> \<exists>t. (s', t) \<in> data_type.Step (ADT_C_if fp utf) a
 4. \<And>s'. s' \<in> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} \<Longrightarrow> s' \<in> Init (ADT_C_if fp utf) (Fin (ADT_C_if fp utf) s')
 5. Init (ADT_C_if fp utf) s \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} proof (prove)
goal (7 subgoals):
 1. ?A7 \<Turnstile> ?I\<^sub>a7
 2. ADT_C_if fp utf \<Turnstile> ?I\<^sub>c7
 3. LI ?A7 (ADT_C_if fp utf) ?R7 (?I\<^sub>a7 \<times> ?I\<^sub>c7)
 4. ADT_C_if fp utf \<Turnstile> {s'. \<exists>s. (s, s') \<in> ?R7 \<and> s \<in> ?I\<^sub>a7 \<and> s' \<in> ?I\<^sub>c7} \<Longrightarrow> ADT_C_if fp utf \<Turnstile> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'}
 5. \<And>s' a. s' \<in> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} \<Longrightarrow> \<exists>t. (s', t) \<in> data_type.Step (ADT_C_if fp utf) a
 6. \<And>s'. s' \<in> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} \<Longrightarrow> s' \<in> Init (ADT_C_if fp utf) (Fin (ADT_C_if fp utf) s')
 7. Init (ADT_C_if fp utf) s \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} proof (prove)
goal (7 subgoals):
 1. global_automaton_invs ?check_active_irq11 ?do_user_op11 ?kernel_call11 ?handle_preemption11 ?schedule11 ?kernel_exit11 ?I\<^sub>a7 ?A7 ?extras11
 2. ADT_C_if fp utf \<Turnstile> ?I\<^sub>c7
 3. LI ?A7 (ADT_C_if fp utf) ?R7 (?I\<^sub>a7 \<times> ?I\<^sub>c7)
 4. ADT_C_if fp utf \<Turnstile> {s'. \<exists>s. (s, s') \<in> ?R7 \<and> s \<in> ?I\<^sub>a7 \<and> s' \<in> ?I\<^sub>c7} \<Longrightarrow> ADT_C_if fp utf \<Turnstile> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'}
 5. \<And>s' a. s' \<in> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} \<Longrightarrow> \<exists>t. (s', t) \<in> data_type.Step (ADT_C_if fp utf) a
 6. \<And>s'. s' \<in> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} \<Longrightarrow> s' \<in> Init (ADT_C_if fp utf) (Fin (ADT_C_if fp utf) s')
 7. Init (ADT_C_if fp utf) s \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} proof (prove)
goal (6 subgoals):
 1. ADT_C_if fp utf \<Turnstile> ?I\<^sub>c7
 2. LI (valid_initial_state_noenabled.ADT_H_if ?uop13) (ADT_C_if fp utf) ?R7 (full_invs_if' \<times> ?I\<^sub>c7)
 3. ADT_C_if fp utf \<Turnstile> {s'. \<exists>s. (s, s') \<in> ?R7 \<and> s \<in> full_invs_if' \<and> s' \<in> ?I\<^sub>c7} \<Longrightarrow> ADT_C_if fp utf \<Turnstile> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'}
 4. \<And>s' a. s' \<in> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} \<Longrightarrow> \<exists>t. (s', t) \<in> data_type.Step (ADT_C_if fp utf) a
 5. \<And>s'. s' \<in> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} \<Longrightarrow> s' \<in> Init (ADT_C_if fp utf) (Fin (ADT_C_if fp utf) s')
 6. Init (ADT_C_if fp utf) s \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} proof (prove)
goal (5 subgoals):
 1. LI (valid_initial_state_noenabled.ADT_H_if ?uop13) (ADT_C_if fp utf) ?R7 (full_invs_if' \<times> UNIV)
 2. ADT_C_if fp utf \<Turnstile> {s'. \<exists>s. (s, s') \<in> ?R7 \<and> s \<in> full_invs_if' \<and> s' \<in> UNIV} \<Longrightarrow> ADT_C_if fp utf \<Turnstile> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'}
 3. \<And>s' a. s' \<in> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} \<Longrightarrow> \<exists>t. (s', t) \<in> data_type.Step (ADT_C_if fp utf) a
 4. \<And>s'. s' \<in> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} \<Longrightarrow> s' \<in> Init (ADT_C_if fp utf) (Fin (ADT_C_if fp utf) s')
 5. Init (ADT_C_if fp utf) s \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} proof (prove)
goal (5 subgoals):
 1. global_automata_refine ?check_active_irq_abs15 ?do_user_op_abs15 ?kernel_call_abs15 ?handle_preemption_abs15 ?schedule_abs15 ?kernel_exit_abs15 full_invs_if' (valid_initial_state_noenabled.ADT_H_if ?uop13) ?extras_abs15 ?check_active_irq_conc15 ?do_user_op_conc15 ?kernel_call_conc15 ?handle_preemption_conc15 ?schedule_conc15 ?kernel_exit_conc15 UNIV (ADT_C_if fp utf) ?srel15 ?nf15
 2. ADT_C_if fp utf \<Turnstile> {s'. \<exists>s. (s, s') \<in> lift_fst_rel ?srel15 \<and> s \<in> full_invs_if' \<and> s' \<in> UNIV} \<Longrightarrow> ADT_C_if fp utf \<Turnstile> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'}
 3. \<And>s' a. s' \<in> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} \<Longrightarrow> \<exists>t. (s', t) \<in> data_type.Step (ADT_C_if fp utf) a
 4. \<And>s'. s' \<in> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} \<Longrightarrow> s' \<in> Init (ADT_C_if fp utf) (Fin (ADT_C_if fp utf) s')
 5. Init (ADT_C_if fp utf) s \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} proof (prove)
goal (5 subgoals):
 1. uop_nonempty utf
 2. ADT_C_if fp utf \<Turnstile> {s'. \<exists>s. (s, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> s \<in> full_invs_if' \<and> s' \<in> UNIV} \<Longrightarrow> ADT_C_if fp utf \<Turnstile> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'}
 3. \<And>s' a. s' \<in> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} \<Longrightarrow> \<exists>t. (s', t) \<in> data_type.Step (ADT_C_if fp utf) a
 4. \<And>s'. s' \<in> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} \<Longrightarrow> s' \<in> Init (ADT_C_if fp utf) (Fin (ADT_C_if fp utf) s')
 5. Init (ADT_C_if fp utf) s \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} proof (prove)
goal (4 subgoals):
 1. ADT_C_if fp utf \<Turnstile> {s'. \<exists>s. (s, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> s \<in> full_invs_if' \<and> s' \<in> UNIV} \<Longrightarrow> ADT_C_if fp utf \<Turnstile> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'}
 2. \<And>s' a. s' \<in> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} \<Longrightarrow> \<exists>t. (s', t) \<in> data_type.Step (ADT_C_if fp utf) a
 3. \<And>s'. s' \<in> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} \<Longrightarrow> s' \<in> Init (ADT_C_if fp utf) (Fin (ADT_C_if fp utf) s')
 4. Init (ADT_C_if fp utf) s \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} proof (prove)
goal (3 subgoals):
 1. \<And>s' a. s' \<in> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} \<Longrightarrow> \<exists>t. (s', t) \<in> data_type.Step (ADT_C_if fp utf) a
 2. \<And>s'. s' \<in> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} \<Longrightarrow> s' \<in> Init (ADT_C_if fp utf) (Fin (ADT_C_if fp utf) s')
 3. Init (ADT_C_if fp utf) s \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} proof (prove)
goal (3 subgoals):
 1. \<And>s' a. s' \<in> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} \<Longrightarrow> \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'
 2. \<And>s'. s' \<in> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} \<Longrightarrow> s' \<in> Init (ADT_C_if fp utf) (Fin (ADT_C_if fp utf) s')
 3. Init (ADT_C_if fp utf) s \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} proof (prove)
goal (2 subgoals):
 1. \<And>s'. s' \<in> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} \<Longrightarrow> s' \<in> Init (ADT_C_if fp utf) (Fin (ADT_C_if fp utf) s')
 2. Init (ADT_C_if fp utf) s \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} proof (prove)
goal (2 subgoals):
 1. \<And>a b ba bb. \<lbrakk>(bb, b) \<in> rf_sr; ((a, bb), ba) \<in> full_invs_if'\<rbrakk> \<Longrightarrow> \<exists>a bb. (bb, b) \<in> rf_sr \<and> ((a, bb), ba) \<in> full_invs_if'
 2. Init (ADT_C_if fp utf) s \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} proof (prove)
goal (1 subgoal):
 1. Init (ADT_C_if fp utf) s \<subseteq> {s'. \<exists>hs. (hs, s') \<in> lift_fst_rel (lift_snd_rel rf_sr) \<and> hs \<in> full_invs_if'} proof (prove)
goal (1 subgoal):
 1. \<And>b aa bb. \<lbrakk>(bb, b) \<in> rf_sr; ((aa, bb), sys_mode_of s) \<in> full_invs_if'; cstate_to_A b = internal_state_if s\<rbrakk> \<Longrightarrow> \<exists>ba. (ba, b) \<in> rf_sr \<and> ((user_context_of s, ba), sys_mode_of s) \<in> full_invs_if' proof (prove)
goal (1 subgoal):
 1. \<And>b aa bb. \<lbrakk>(bb, b) \<in> rf_sr; ((aa, bb), sys_mode_of s) \<in> full_invs_if'; cstate_to_A b = internal_state_if s\<rbrakk> \<Longrightarrow> (bb, b) \<in> rf_sr \<and> ((user_context_of s, bb), sys_mode_of s) \<in> full_invs_if' proof (prove)
goal (1 subgoal):
 1. \<And>b aa bb. \<lbrakk>(bb, b) \<in> rf_sr; cstate_to_A b = internal_state_if s; invs' bb; ex_abs einvs bb; vs_valid_duplicates' (ksPSpace bb); sys_mode_of s \<noteq> KernelSchedule True \<longrightarrow> 0 < ksDomainTime bb; ksDomainTime bb = 0 \<longrightarrow> ksSchedulerAction bb = ChooseNewThread; valid_domain_list' bb; case sys_mode_of s of InUserMode \<Rightarrow> ct_running' (internal_state_if ((aa, bb), sys_mode_of s)) \<and> ksSchedulerAction (internal_state_if ((aa, bb), sys_mode_of s)) = ResumeCurrentThread | InIdleMode \<Rightarrow> ct_idle' (internal_state_if ((aa, bb), sys_mode_of s)) \<and> ksSchedulerAction (internal_state_if ((aa, bb), sys_mode_of s)) = ResumeCurrentThread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running' (internal_state_if ((aa, bb), sys_mode_of s)) \<and> ksDomainTime (internal_state_if ((aa, bb), sys_mode_of s)) \<noteq> 0) \<and> (ct_running' (internal_state_if ((aa, bb), sys_mode_of s)) \<or> ct_idle' (internal_state_if ((aa, bb), sys_mode_of s))) \<and> ksSchedulerAction (internal_state_if ((aa, bb), sys_mode_of s)) = ResumeCurrentThread | KernelExit \<Rightarrow> (ct_running' (internal_state_if ((aa, bb), sys_mode_of s)) \<or> ct_idle' (internal_state_if ((aa, bb), sys_mode_of s))) \<and> ksSchedulerAction (internal_state_if ((aa, bb), sys_mode_of s)) = ResumeCurrentThread \<and> ksDomainTime (internal_state_if ((aa, bb), sys_mode_of s)) \<noteq> 0 | _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> case sys_mode_of s of InUserMode \<Rightarrow> ct_running' (internal_state_if ((user_context_of s, bb), sys_mode_of s)) \<and> ksSchedulerAction (internal_state_if ((user_context_of s, bb), sys_mode_of s)) = ResumeCurrentThread | InIdleMode \<Rightarrow> ct_idle' (internal_state_if ((user_context_of s, bb), sys_mode_of s)) \<and> ksSchedulerAction (internal_state_if ((user_context_of s, bb), sys_mode_of s)) = ResumeCurrentThread | KernelEntry e \<Rightarrow> (e \<noteq> Interrupt \<longrightarrow> ct_running' (internal_state_if ((user_context_of s, bb), sys_mode_of s)) \<and> ksDomainTime (internal_state_if ((user_context_of s, bb), sys_mode_of s)) \<noteq> 0) \<and> (ct_running' (internal_state_if ((user_context_of s, bb), sys_mode_of s)) \<or> ct_idle' (internal_state_if ((user_context_of s, bb), sys_mode_of s))) \<and> ksSchedulerAction (internal_state_if ((user_context_of s, bb), sys_mode_of s)) = ResumeCurrentThread | KernelExit \<Rightarrow> (ct_running' (internal_state_if ((user_context_of s, bb), sys_mode_of s)) \<or> ct_idle' (internal_state_if ((user_context_of s, bb), sys_mode_of s))) \<and> ksSchedulerAction (internal_state_if ((user_context_of s, bb), sys_mode_of s)) = ResumeCurrentThread \<and> ksDomainTime (internal_state_if ((user_context_of s, bb), sys_mode_of s)) \<noteq> 0 | _ \<Rightarrow> True proof (prove)
goal:
No subgoals!