kings-crown/FVELER_Isabelle huggingface dataset:
theory ADT_IF_Refine_C

lemma cur_thread_of_absKState[simp]:
   "cur_thread (absKState s) = (ksCurThread s)" by (clarsimp simp: cstate_relation_def Let_def absKState_def cstate_to_H_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cur_thread (absKState s) = ksCurThread s
theory ADT_IF_Refine_C

lemma handlePreemption_if_def2:
  "handlePreemption_if tc = do
     r \<leftarrow> handleEvent Interrupt;
          stateAssert (\<lambda>s. (ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<and>
                            valid_domain_list' s) [];
          return tc
   od" apply (clarsimp simp add: handlePreemption_if_def handleEvent_def liftE_def
                   bind_assoc) apply (rule bind_eqI) apply (rule ext) apply (clarsimp split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. handlePreemption_if tc = do r <- handleEvent Interrupt;
stateAssert (\<lambda>s. (ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<and> valid_domain_list' s) [];
return tc
od proof (prove)
goal (1 subgoal):
 1. do irq <- doMachineOp (getActiveIRQ False);
y <- when (\<exists>y. irq = Some y) (handleInterrupt (the irq));
y <- stateAssert (\<lambda>s. (ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<and> valid_domain_list' s) [];
return tc
od = do x <- doMachineOp (getActiveIRQ False);
r <- case x of None \<Rightarrow> return () | Some x \<Rightarrow> handleInterrupt x;
y <- stateAssert (\<lambda>s. (ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<and> valid_domain_list' s) [];
return tc
od proof (prove)
goal (1 subgoal):
 1. (\<lambda>irq. do y <- when (\<exists>y. irq = Some y) (handleInterrupt (the irq));
y <- stateAssert (\<lambda>s. (ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<and> valid_domain_list' s) [];
return tc
od) = (\<lambda>x. do r <- case x of None \<Rightarrow> return () | Some x \<Rightarrow> handleInterrupt x;
y <- stateAssert (\<lambda>s. (ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<and> valid_domain_list' s) [];
return tc
od) proof (prove)
goal (1 subgoal):
 1. \<And>irq. do y <- when (\<exists>y. irq = Some y) (handleInterrupt (the irq));
y <- stateAssert (\<lambda>s. (ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<and> valid_domain_list' s) [];
return tc
od = do r <- case irq of None \<Rightarrow> return () | Some x \<Rightarrow> handleInterrupt x;
y <- stateAssert (\<lambda>s. (ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<and> valid_domain_list' s) [];
return tc
od proof (prove)
goal:
No subgoals!
theory ADT_IF_Refine_C

lemma handleInterrupt_no_fail:
  "no_fail (ex_abs (einvs) and invs'
                           and (\<lambda>s. intStateIRQTable (ksInterruptState s) a \<noteq> irqstate.IRQInactive))
           (handleInterrupt a)" apply (rule no_fail_pre) apply (rule corres_nofail) apply (rule handleInterrupt_corres) apply (erule FalseE) apply (fastforce simp: ex_abs_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (ex_abs einvs and invs' and (\<lambda>s. intStateIRQTable (ksInterruptState s) a \<noteq> irqstate.IRQInactive)) (handleInterrupt a) proof (prove)
goal (2 subgoals):
 1. no_fail ?P (handleInterrupt a)
 2. \<And>s. (ex_abs einvs and invs' and (\<lambda>s. intStateIRQTable (ksInterruptState s) a \<noteq> irqstate.IRQInactive)) s \<Longrightarrow> ?P s proof (prove)
goal (3 subgoals):
 1. corres_underlying ?state_relation3 ?nf3 True ?r3 ?P3 ?P'3 ?f3 (handleInterrupt a)
 2. ?nf3 \<Longrightarrow> no_fail ?P3 ?f3
 3. \<And>s. (ex_abs einvs and invs' and (\<lambda>s. intStateIRQTable (ksInterruptState s) a \<noteq> irqstate.IRQInactive)) s \<Longrightarrow> \<exists>sa. (sa, s) \<in> ?state_relation3 \<and> ?P3 sa \<and> ?P'3 s proof (prove)
goal (2 subgoals):
 1. False \<Longrightarrow> no_fail einvs (handle_interrupt a)
 2. \<And>s. (ex_abs einvs and invs' and (\<lambda>s. intStateIRQTable (ksInterruptState s) a \<noteq> irqstate.IRQInactive)) s \<Longrightarrow> \<exists>sa. (sa, s) \<in> state_relation \<and> einvs sa \<and> (invs' and (\<lambda>s. intStateIRQTable (ksInterruptState s) a \<noteq> irqstate.IRQInactive)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (ex_abs einvs and invs' and (\<lambda>s. intStateIRQTable (ksInterruptState s) a \<noteq> irqstate.IRQInactive)) s \<Longrightarrow> \<exists>sa. (sa, s) \<in> state_relation \<and> einvs sa \<and> (invs' and (\<lambda>s. intStateIRQTable (ksInterruptState s) a \<noteq> irqstate.IRQInactive)) s proof (prove)
goal:
No subgoals!
theory ADT_IF_Refine_C

lemma ccorres_corres_u':
  "\<lbrakk> ccorres dc xfdc P' Q' [] H C; no_fail P'' H; (\<And>s. P s \<Longrightarrow> P' s \<and> P'' s); (Collect Q) \<subseteq> Q' \<rbrakk>
     \<Longrightarrow> corres_underlying rf_sr nf nf' dc P Q H (exec_C \<Gamma> C)" apply (rule ccorres_corres_u) apply (rule ccorres_guard_imp) apply assumption apply simp apply blast apply (rule no_fail_pre,simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccorres dc xfdc P' Q' [] H C; no_fail P'' H; \<And>s. P s \<Longrightarrow> P' s \<and> P'' s; Collect Q \<subseteq> Q'\<rbrakk> \<Longrightarrow> corres_underlying rf_sr nf nf' dc P Q H (exec_C \<Gamma> C) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ccorres dc xfdc P' Q' [] H C; no_fail P'' H; \<And>s. P s \<Longrightarrow> P' s \<and> P'' s; Collect Q \<subseteq> Q'\<rbrakk> \<Longrightarrow> ccorres dc xfdc P (Collect Q) [] H C
 2. \<lbrakk>ccorres dc xfdc P' Q' [] H C; no_fail P'' H; \<And>s. P s \<Longrightarrow> P' s \<and> P'' s; Collect Q \<subseteq> Q'\<rbrakk> \<Longrightarrow> no_fail P H proof (prove)
goal (4 subgoals):
 1. \<lbrakk>ccorres dc xfdc P' Q' [] H C; no_fail P'' H; \<And>s. P s \<Longrightarrow> P' s \<and> P'' s; Collect Q \<subseteq> Q'\<rbrakk> \<Longrightarrow> ccorres dc xfdc ?Q3 ?Q'3 [] H C
 2. \<And>s. \<lbrakk>ccorres dc xfdc P' Q' [] H C; no_fail P'' H; \<And>s. P s \<Longrightarrow> P' s \<and> P'' s; Collect Q \<subseteq> Q'; P s\<rbrakk> \<Longrightarrow> ?Q3 s
 3. \<And>s. \<lbrakk>ccorres dc xfdc P' Q' [] H C; no_fail P'' H; \<And>s. P s \<Longrightarrow> P' s \<and> P'' s; Collect Q \<subseteq> Q'; s \<in> Collect Q\<rbrakk> \<Longrightarrow> s \<in> ?Q'3
 4. \<lbrakk>ccorres dc xfdc P' Q' [] H C; no_fail P'' H; \<And>s. P s \<Longrightarrow> P' s \<and> P'' s; Collect Q \<subseteq> Q'\<rbrakk> \<Longrightarrow> no_fail P H proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>ccorres dc xfdc P' Q' [] H C; no_fail P'' H; \<And>s. P s \<Longrightarrow> P' s \<and> P'' s; Collect Q \<subseteq> Q'; P s\<rbrakk> \<Longrightarrow> P' s
 2. \<And>s. \<lbrakk>ccorres dc xfdc P' Q' [] H C; no_fail P'' H; \<And>s. P s \<Longrightarrow> P' s \<and> P'' s; Collect Q \<subseteq> Q'; s \<in> Collect Q\<rbrakk> \<Longrightarrow> s \<in> Q'
 3. \<lbrakk>ccorres dc xfdc P' Q' [] H C; no_fail P'' H; \<And>s. P s \<Longrightarrow> P' s \<and> P'' s; Collect Q \<subseteq> Q'\<rbrakk> \<Longrightarrow> no_fail P H proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>ccorres dc xfdc P' Q' [] H C; no_fail P'' H; \<And>s. P s \<Longrightarrow> P' s \<and> P'' s; Collect Q \<subseteq> Q'; s \<in> Collect Q\<rbrakk> \<Longrightarrow> s \<in> Q'
 2. \<lbrakk>ccorres dc xfdc P' Q' [] H C; no_fail P'' H; \<And>s. P s \<Longrightarrow> P' s \<and> P'' s; Collect Q \<subseteq> Q'\<rbrakk> \<Longrightarrow> no_fail P H proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccorres dc xfdc P' Q' [] H C; no_fail P'' H; \<And>s. P s \<Longrightarrow> P' s \<and> P'' s; Collect Q \<subseteq> Q'\<rbrakk> \<Longrightarrow> no_fail P H proof (prove)
goal:
No subgoals!
theory ADT_IF_Refine_C

lemma preserves_trivial: "preserves mode mode' UNIV f" apply (simp add: preserves_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. preserves mode mode' UNIV f proof (prove)
goal:
No subgoals!
theory ADT_IF_Refine_C

lemma preserves'_trivial: "preserves' mode UNIV f" apply (simp add: preserves'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. preserves' mode UNIV f proof (prove)
goal:
No subgoals!
theory ADT_IF_Refine_C

lemma full_invs_all_invs[simp]:
  "((tc,s),KernelEntry e) \<in> full_invs_if' \<Longrightarrow> all_invs' e s" apply (clarsimp simp: full_invs_if'_def all_invs'_def ex_abs_def) apply (rule_tac x=sa in exI) by (auto simp: ct_running_related ct_idle_related schedaction_related
                 domain_time_rel_eq domain_list_rel_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((tc, s), KernelEntry e) \<in> full_invs_if' \<Longrightarrow> all_invs' e s proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>invs' s; vs_valid_duplicates' (ksPSpace s); (sa, s) \<in> state_relation; 0 < ksDomainTime s; invs sa; ksDomainTime s \<noteq> 0; valid_list sa; valid_sched sa; valid_domain_list' s; e \<noteq> Interrupt \<longrightarrow> ct_running' s; ct_running' s \<or> ct_idle' s; ksSchedulerAction s = ResumeCurrentThread\<rbrakk> \<Longrightarrow> \<exists>sa. (sa, s) \<in> state_relation \<and> invs sa \<and> valid_list sa \<and> valid_sched sa \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running sa) \<and> (ct_running sa \<or> ct_idle sa) \<and> scheduler_action sa = resume_cur_thread \<and> 0 < domain_time sa \<and> valid_domain_list sa proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>invs' s; vs_valid_duplicates' (ksPSpace s); (sa, s) \<in> state_relation; 0 < ksDomainTime s; invs sa; ksDomainTime s \<noteq> 0; valid_list sa; valid_sched sa; valid_domain_list' s; e \<noteq> Interrupt \<longrightarrow> ct_running' s; ct_running' s \<or> ct_idle' s; ksSchedulerAction s = ResumeCurrentThread\<rbrakk> \<Longrightarrow> (sa, s) \<in> state_relation \<and> invs sa \<and> valid_list sa \<and> valid_sched sa \<and> (e \<noteq> Interrupt \<longrightarrow> ct_running sa) \<and> (ct_running sa \<or> ct_idle sa) \<and> scheduler_action sa = resume_cur_thread \<and> 0 < domain_time sa \<and> valid_domain_list sa
theory ADT_IF_Refine_C

lemma obs_cpspace_device_data_relation:
  "\<lbrakk> pspace_aligned' bd; pspace_distinct' bd;
     cpspace_device_data_relation (ksPSpace bd) (underlying_memory (ksMachineState bd)) hgs \<rbrakk>
     \<Longrightarrow> cpspace_device_data_relation (ksPSpace bd)
           (underlying_memory (observable_memory (ksMachineState bd) (user_mem' bd))) hgs" apply (clarsimp simp: cmap_relation_def dom_heap_to_device_data) apply (drule bspec,fastforce) apply (clarsimp simp: cuser_user_data_device_relation_def observable_memory_def
                         heap_to_user_data_def  map_comp_def Let_def
                  split: option.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_aligned' bd; pspace_distinct' bd; cpspace_device_data_relation (ksPSpace bd) (underlying_memory (ksMachineState bd)) hgs\<rbrakk> \<Longrightarrow> cpspace_device_data_relation (ksPSpace bd) (underlying_memory (observable_memory (ksMachineState bd) (user_mem' bd))) hgs proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>pspace_aligned' bd; pspace_distinct' bd; map_to_user_data_device (ksPSpace bd) x = Some y; PTR(user_data_device_C) ` dom (map_to_user_data_device (ksPSpace bd)) = dom (clift hgs); \<forall>x\<in>dom (map_to_user_data_device (ksPSpace bd)). cuser_user_data_device_relation (the (heap_to_device_data (ksPSpace bd) (underlying_memory (ksMachineState bd)) x)) (the (clift hgs (PTR(user_data_device_C) x)))\<rbrakk> \<Longrightarrow> cuser_user_data_device_relation (the (heap_to_device_data (ksPSpace bd) (underlying_memory (observable_memory (ksMachineState bd) (user_mem' bd))) x)) (the (clift hgs (PTR(user_data_device_C) x))) proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>pspace_aligned' bd; pspace_distinct' bd; map_to_user_data_device (ksPSpace bd) x = Some y; PTR(user_data_device_C) ` dom (map_to_user_data_device (ksPSpace bd)) = dom (clift hgs); cuser_user_data_device_relation (the (heap_to_device_data (ksPSpace bd) (underlying_memory (ksMachineState bd)) x)) (the (clift hgs (PTR(user_data_device_C) x)))\<rbrakk> \<Longrightarrow> cuser_user_data_device_relation (the (heap_to_device_data (ksPSpace bd) (underlying_memory (observable_memory (ksMachineState bd) (user_mem' bd))) x)) (the (clift hgs (PTR(user_data_device_C) x))) proof (prove)
goal:
No subgoals!
theory ADT_IF_Refine_C

lemma cstate_relation_observable_memory:
  "\<lbrakk> invs' bs; cstate_relation bs gs \<rbrakk>
     \<Longrightarrow> cstate_relation (bs\<lparr>ksMachineState := observable_memory (ksMachineState bs) (user_mem' bs)\<rparr>) gs" by (clarsimp simp: cstate_relation_def Let_def obs_cpspace_user_data_relation
                     obs_cpspace_device_data_relation cpspace_relation_def invs'_def
                     valid_state'_def valid_pspace'_def
                     cmachine_state_relation_def observable_memory_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs' bs; cstate_relation bs gs\<rbrakk> \<Longrightarrow> cstate_relation (bs\<lparr>ksMachineState := observable_memory (ksMachineState bs) (user_mem' bs)\<rparr>) gs
theory ADT_IF_Refine_C

lemma infoflow_fw_sim_H: "uop_nonempty uop \<Longrightarrow> ADT_C_if fp uop \<sqsubseteq>\<^sub>F ADT_H_if uop" apply (erule global_automata_refine.fw_simulates[OF c_to_haskell]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. uop_nonempty uop \<Longrightarrow> ADT_C_if fp uop \<sqsubseteq>\<^sub>F ADT_H_if uop proof (prove)
goal:
No subgoals!
theory ADT_IF_Refine_C

lemma infoflow_fw_sim_A: "uop_nonempty uop \<Longrightarrow> ADT_C_if fp uop \<sqsubseteq>\<^sub>F ADT_A_if uop" apply (rule fw_simulates_trans) apply (rule infoflow_fw_sim_H) apply simp+ apply (erule global_automata_refine.fw_simulates[OF haskell_to_abs]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. uop_nonempty uop \<Longrightarrow> ADT_C_if fp uop \<sqsubseteq>\<^sub>F ADT_A_if uop proof (prove)
goal (2 subgoals):
 1. uop_nonempty uop \<Longrightarrow> ADT_C_if fp uop \<sqsubseteq>\<^sub>F ?B
 2. uop_nonempty uop \<Longrightarrow> ?B \<sqsubseteq>\<^sub>F ADT_A_if uop proof (prove)
goal (2 subgoals):
 1. uop_nonempty uop \<Longrightarrow> uop_nonempty uop
 2. uop_nonempty uop \<Longrightarrow> ADT_H_if uop \<sqsubseteq>\<^sub>F ADT_A_if uop proof (prove)
goal (1 subgoal):
 1. uop_nonempty uop \<Longrightarrow> ADT_H_if uop \<sqsubseteq>\<^sub>F ADT_A_if uop proof (prove)
goal:
No subgoals!
theory ADT_IF_Refine_C

theorem infoflow_refinement_H: "uop_nonempty uop \<Longrightarrow> ADT_C_if fp uop \<sqsubseteq> ADT_H_if uop" apply (erule sim_imp_refines[OF infoflow_fw_sim_H]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. uop_nonempty uop \<Longrightarrow> ADT_C_if fp uop \<sqsubseteq> ADT_H_if uop proof (prove)
goal:
No subgoals!
theory ADT_IF_Refine_C

theorem infoflow_refinement_A: "uop_nonempty uop \<Longrightarrow> ADT_C_if fp uop \<sqsubseteq> ADT_A_if uop" apply (erule sim_imp_refines[OF infoflow_fw_sim_A]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. uop_nonempty uop \<Longrightarrow> ADT_C_if fp uop \<sqsubseteq> ADT_A_if uop proof (prove)
goal:
No subgoals!
theory ArchADT_IF_Refine_C

lemma irqInvalid_def2:
  "irqInvalid = 0xFFFF" by (clarsimp simp: irqInvalid_def mask_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. kernel_all_global_addresses.irqInvalid = 0xFFFF
theory ArchADT_IF_Refine_C

lemma handleInvocation_ccorres'[ADT_IF_Refine_assms]:
  "ccorres (K dc \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
       (invs' and arch_extras and
        ct_active' and sch_act_simple and
        (\<lambda>s. \<forall>x. ksCurThread s \<notin> set (ksReadyQueues s x)))
       (UNIV \<inter> {s. isCall_' s = from_bool isCall}
             \<inter> {s. isBlocking_' s = from_bool isBlocking}) []
       (handleInvocation isCall isBlocking) (Call handleInvocation_'proc)" apply (simp only: arch_extras_def) apply (rule handleInvocation_ccorres) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (K dc \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (invs' and arch_extras and ct_active' and sch_act_simple and (\<lambda>s. \<forall>x. ksCurThread s \<notin> set (ksReadyQueues s x))) (UNIV \<inter> \<lbrace>\<acute>isCall = from_bool isCall\<rbrace> \<inter> \<lbrace>\<acute>isBlocking = from_bool isBlocking\<rbrace>) [] (handleInvocation isCall isBlocking) (com.Call handleInvocation_'proc) proof (prove)
goal (1 subgoal):
 1. ccorres (K dc \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and ct_active' and sch_act_simple and (\<lambda>s. \<forall>x. ksCurThread s \<notin> set (ksReadyQueues s x))) (UNIV \<inter> \<lbrace>\<acute>isCall = from_bool isCall\<rbrace> \<inter> \<lbrace>\<acute>isBlocking = from_bool isBlocking\<rbrace>) [] (handleInvocation isCall isBlocking) (com.Call handleInvocation_'proc) proof (prove)
goal:
No subgoals!
theory ArchADT_IF_Refine_C

lemma corres_underlying_split5:
  "(\<And>a b c d e. corres_underlying srel nf nf' rrel (Q a b c d e) (Q' a b c d e) (f a b c d e) (f' a b c d e))
   \<Longrightarrow> corres_underlying srel nf nf' rrel (case x of (a,b,c,d,e) \<Rightarrow> Q a b c d e)
                                          (case x of (a,b,c,d,e) \<Rightarrow> Q' a b c d e)
                                          (case x of (a,b,c,d,e) \<Rightarrow> f a b c d e)
                                          (case x of (a,b,c,d,e) \<Rightarrow> f' a b c d e)" by (cases x; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>a b c d e. corres_underlying srel nf nf' rrel (Q a b c d e) (Q' a b c d e) (f a b c d e) (f' a b c d e)) \<Longrightarrow> corres_underlying srel nf nf' rrel (case x of (a, b, c, d, e) \<Rightarrow> Q a b c d e) (case x of (a, b, c, d, e) \<Rightarrow> Q' a b c d e) (case x of (a, b, c, d, e) \<Rightarrow> f a b c d e) (case x of (a, b, c, d, e) \<Rightarrow> f' a b c d e)
theory Noninterference_Refinement

lemma internal_R_ADT_A_if:
  "internal_R (ADT_A_if uop) R = R" apply (rule ext, rule ext) apply (simp add: internal_R_def ADT_A_if_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. internal_R (ADT_A_if uop) R = R proof (prove)
goal (1 subgoal):
 1. \<And>x xa. internal_R (ADT_A_if uop) R x xa = R x xa proof (prove)
goal:
No subgoals!
theory Noninterference_Refinement

lemma big_step_ADT_C_if_big_step_ADT_A_if_refines:
  "uop_nonempty utf \<Longrightarrow> refines (big_step_ADT_C_if utf) (big_step_ADT_A_if utf) " apply (simp add: big_step_ADT_A_if_def big_step_ADT_C_if_def) apply (rule big_step_adt_refines[where A="ADT_A_if utf", simplified internal_R_ADT_A_if]) apply (rule LI_trans) apply (erule global_automata_refine.fw_sim_abs_conc[OF haskell_to_abs]) apply (erule global_automata_refine.fw_sim_abs_conc[OF c_to_haskell]) apply (rule global_automaton_invs.ADT_invs[OF haskell_invs]) apply (rule global_automaton_invs.ADT_invs[OF abstract_invs]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. uop_nonempty utf \<Longrightarrow> big_step_ADT_C_if utf \<sqsubseteq> big_step_ADT_A_if utf proof (prove)
goal (1 subgoal):
 1. uop_nonempty utf \<Longrightarrow> big_step_adt (ADT_C_if fp utf) (internal_R (ADT_C_if fp utf) big_step_R) big_step_evmap \<sqsubseteq> big_step_adt (ADT_A_if utf) big_step_R big_step_evmap proof (prove)
goal (3 subgoals):
 1. uop_nonempty utf \<Longrightarrow> LI (ADT_A_if utf) (ADT_C_if fp utf) ?S (?Ia \<times> ?Ic)
 2. uop_nonempty utf \<Longrightarrow> ADT_A_if utf \<Turnstile> ?Ia
 3. uop_nonempty utf \<Longrightarrow> ADT_C_if fp utf \<Turnstile> ?Ic proof (prove)
goal (5 subgoals):
 1. uop_nonempty utf \<Longrightarrow> LI (ADT_A_if utf) ?H4 ?R4 (?Ia \<times> ?Ih4)
 2. uop_nonempty utf \<Longrightarrow> LI ?H4 (ADT_C_if fp utf) ?S4 (?Ih4 \<times> ?Ic)
 3. uop_nonempty utf \<Longrightarrow> ?H4 \<Turnstile> ?Ih4
 4. uop_nonempty utf \<Longrightarrow> ADT_A_if utf \<Turnstile> ?Ia
 5. uop_nonempty utf \<Longrightarrow> ADT_C_if fp utf \<Turnstile> ?Ic proof (prove)
goal (4 subgoals):
 1. uop_nonempty utf \<Longrightarrow> LI (ADT_H_if utf) (ADT_C_if fp utf) ?S4 (full_invs_if' \<times> ?Ic)
 2. uop_nonempty utf \<Longrightarrow> ADT_H_if utf \<Turnstile> full_invs_if'
 3. uop_nonempty utf \<Longrightarrow> ADT_A_if utf \<Turnstile> full_invs_if
 4. uop_nonempty utf \<Longrightarrow> ADT_C_if fp utf \<Turnstile> ?Ic proof (prove)
goal (3 subgoals):
 1. uop_nonempty utf \<Longrightarrow> ADT_H_if utf \<Turnstile> full_invs_if'
 2. uop_nonempty utf \<Longrightarrow> ADT_A_if utf \<Turnstile> full_invs_if
 3. uop_nonempty utf \<Longrightarrow> ADT_C_if fp utf \<Turnstile> UNIV proof (prove)
goal (2 subgoals):
 1. uop_nonempty utf \<Longrightarrow> ADT_A_if utf \<Turnstile> full_invs_if
 2. uop_nonempty utf \<Longrightarrow> ADT_C_if fp utf \<Turnstile> UNIV proof (prove)
goal (1 subgoal):
 1. uop_nonempty utf \<Longrightarrow> ADT_C_if fp utf \<Turnstile> UNIV proof (prove)
goal:
No subgoals!
theory Noninterference_Refinement

lemma internal_R_tranclp:
  "(internal_R A R)\<^sup>+\<^sup>+ s s' \<Longrightarrow> R\<^sup>+\<^sup>+ (Fin A s) (Fin A s')" apply (induct rule: tranclp.induct) apply (simp add: internal_R_def) apply (simp add: internal_R_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (internal_R A R)\<^sup>+\<^sup>+ s s' \<Longrightarrow> R\<^sup>+\<^sup>+ (Fin A s) (Fin A s') proof (prove)
goal (2 subgoals):
 1. \<And>a b. internal_R A R a b \<Longrightarrow> R\<^sup>+\<^sup>+ (Fin A a) (Fin A b)
 2. \<And>a b c. \<lbrakk>(internal_R A R)\<^sup>+\<^sup>+ a b; R\<^sup>+\<^sup>+ (Fin A a) (Fin A b); internal_R A R b c\<rbrakk> \<Longrightarrow> R\<^sup>+\<^sup>+ (Fin A a) (Fin A c) proof (prove)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>(internal_R A R)\<^sup>+\<^sup>+ a b; R\<^sup>+\<^sup>+ (Fin A a) (Fin A b); internal_R A R b c\<rbrakk> \<Longrightarrow> R\<^sup>+\<^sup>+ (Fin A a) (Fin A c) proof (prove)
goal:
No subgoals!
theory Noninterference_Refinement

lemma inv_holds_T: "A [> UNIV" by (simp add: inv_holds_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. A [> UNIV
theory Noninterference_Refinement

lemma LI_abs_to_c:
  "LI (ADT_A_if utf) (ADT_C_if fp utf)
   (((lift_fst_rel (lift_snd_rel state_relation)))
     O ((lift_fst_rel (lift_snd_rel rf_sr)) \<inter> {(h, c). h \<in> full_invs_if'}))
   (full_invs_if \<times> UNIV)" apply (rule LI_trans) apply (rule global_automata_refine.fw_sim_abs_conc[OF haskell_to_abs]) apply (rule uop_nonempty) apply (rule global_automata_refine.fw_sim_abs_conc[OF c_to_haskell]) apply (rule uop_nonempty) apply (rule global_automaton_invs.ADT_invs[OF haskell_invs]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. LI (ADT_A_if utf) (ADT_C_if fp utf) (lift_fst_rel (lift_snd_rel state_relation) O (lift_fst_rel (lift_snd_rel rf_sr) \<inter> {(h, c). h \<in> full_invs_if'})) (full_invs_if \<times> UNIV) proof (prove)
goal (3 subgoals):
 1. LI (ADT_A_if utf) ?H (lift_fst_rel (lift_snd_rel state_relation)) (full_invs_if \<times> full_invs_if')
 2. LI ?H (ADT_C_if fp utf) (lift_fst_rel (lift_snd_rel rf_sr)) (full_invs_if' \<times> UNIV)
 3. ?H \<Turnstile> full_invs_if' proof (prove)
goal (3 subgoals):
 1. uop_nonempty utf
 2. LI (valid_initial_state_noenabled.ADT_H_if utf) (ADT_C_if fp utf) (lift_fst_rel (lift_snd_rel rf_sr)) (full_invs_if' \<times> UNIV)
 3. valid_initial_state_noenabled.ADT_H_if utf \<Turnstile> full_invs_if' proof (prove)
goal (2 subgoals):
 1. LI (valid_initial_state_noenabled.ADT_H_if utf) (ADT_C_if fp utf) (lift_fst_rel (lift_snd_rel rf_sr)) (full_invs_if' \<times> UNIV)
 2. valid_initial_state_noenabled.ADT_H_if utf \<Turnstile> full_invs_if' proof (prove)
goal (2 subgoals):
 1. uop_nonempty utf
 2. valid_initial_state_noenabled.ADT_H_if utf \<Turnstile> full_invs_if' proof (prove)
goal (1 subgoal):
 1. valid_initial_state_noenabled.ADT_H_if utf \<Turnstile> full_invs_if' proof (prove)
goal:
No subgoals!