kings-crown/FVELER_Isabelle huggingface dataset:
theory ADT_IF_Refine

lemma preserves'E:
  assumes preserves: "preserves' mode P f"
  assumes inf: "(s,e,s') \<in> f"
  assumes P: "(s,mode) \<in> P"
  assumes a: "(s',e) \<in> P \<Longrightarrow> Q"
  shows "Q" apply (rule a) apply (insert preserves inf P) apply (clarsimp simp: preserves'_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Q proof (prove)
goal (1 subgoal):
 1. (s', e) \<in> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>preserves' mode P f; (s, e, s') \<in> f; (s, mode) \<in> P\<rbrakk> \<Longrightarrow> (s', e) \<in> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>f. case x of (s, e, s') \<Rightarrow> (s, mode) \<in> P \<longrightarrow> (s', e) \<in> P; (s, e, s') \<in> f; (s, mode) \<in> P\<rbrakk> \<Longrightarrow> (s', e) \<in> P proof (prove)
goal:
No subgoals!
theory ADT_IF_Refine

lemma ADT_extras: "ADT \<Turnstile> extras" apply (rule invariantI) apply (clarsimp simp: init_extras) apply (clarsimp simp: step_adt) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ADT \<Turnstile> extras proof (prove)
goal (2 subgoals):
 1. \<forall>s. Init ADT s \<subseteq> extras
 2. \<forall>j. Step ADT j `` extras \<subseteq> extras proof (prove)
goal (1 subgoal):
 1. \<forall>j. Step ADT j `` extras \<subseteq> extras proof (prove)
goal:
No subgoals!
theory ADT_IF_Refine

lemma invariant_holds_inter:
  "A \<Turnstile> I \<Longrightarrow> A \<Turnstile> S \<Longrightarrow> A \<Turnstile> (I \<inter> S)" apply (clarsimp simp: invariant_holds_def) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<Turnstile> I; A \<Turnstile> S\<rbrakk> \<Longrightarrow> A \<Turnstile> I \<inter> S proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>\<forall>s. Init A s \<subseteq> I; \<forall>j. Step A j `` I \<subseteq> I; \<forall>s. Init A s \<subseteq> S; \<forall>j. Step A j `` S \<subseteq> S\<rbrakk> \<Longrightarrow> Step A j `` (I \<inter> S) \<subseteq> I \<and> Step A j `` (I \<inter> S) \<subseteq> S proof (prove)
goal:
No subgoals!
theory ADT_IF_Refine

lemma preserves_lift_ret:
  "(\<And>tc. \<lbrace>\<lambda>s. ((tc,s),mode) \<in> P\<rbrace> f tc \<lbrace>\<lambda>tc' s'. ((snd tc',s'),mode') \<in> P\<rbrace>)
   \<Longrightarrow> preserves mode mode' P {((tc, s), irq, tc', s'). ((irq, tc'), s') \<in> fst (f tc s)}" by (fastforce simp: preserves_def valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>tc. \<lbrace>\<lambda>s. ((tc, s), mode) \<in> P\<rbrace> f tc \<lbrace>\<lambda>tc' s'. ((snd tc', s'), mode') \<in> P\<rbrace>) \<Longrightarrow> preserves mode mode' P {((tc, s), irq, tc', s'). ((irq, tc'), s') \<in> fst (f tc s)}
theory ADT_IF_Refine

lemma preserves_lift:
  "(\<And>tc. \<lbrace>\<lambda>s. ((tc,s),mode) \<in> P\<rbrace> f tc \<lbrace>\<lambda>tc' s'. ((tc',s'),mode') \<in> P\<rbrace>)
   \<Longrightarrow> preserves mode mode' P {((tc, s), irq, tc', s'). (tc', s') \<in> fst (f tc s)}" by (clarsimp simp: preserves_def valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>tc. \<lbrace>\<lambda>s. ((tc, s), mode) \<in> P\<rbrace> f tc \<lbrace>\<lambda>tc' s'. ((tc', s'), mode') \<in> P\<rbrace>) \<Longrightarrow> preserves mode mode' P {((tc, s), irq, tc', s'). (tc', s') \<in> fst (f tc s)}
theory ADT_IF_Refine

lemma preserves_lift':
  "(\<And>tc. \<lbrace>\<lambda>s. ((tc,s),mode) \<in> P\<rbrace> f uop tc \<lbrace>\<lambda>tc' s'. ((snd tc',s'),mode') \<in> P\<rbrace>)
   \<Longrightarrow> preserves mode mode' P {((a, b), e, tc, s') | a b e tc s'. ((e, tc), s') \<in> fst (f uop a b)}" by (fastforce simp: preserves_def valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>tc. \<lbrace>\<lambda>s. ((tc, s), mode) \<in> P\<rbrace> f uop tc \<lbrace>\<lambda>tc' s'. ((snd tc', s'), mode') \<in> P\<rbrace>) \<Longrightarrow> preserves mode mode' P {((a, b), e, tc, s') |a b e tc s'. ((e, tc), s') \<in> fst (f uop a b)}
theory ADT_IF_Refine

lemma preserves_lift'':
   "(\<And>tc. \<lbrace>\<lambda>s. ((tc,s),mode) \<in> P\<rbrace> f e tc \<lbrace>\<lambda>tc' s'. ((snd tc',s'),mode') \<in> P\<rbrace>)
    \<Longrightarrow> preserves mode mode' P
         {((a, b), ba, tc, s') | a b ba tc s'.
                                 \<exists>r. ((r, tc), s') \<in> fst (f e a b) \<and> ba = (r \<noteq> Inr ())}" by (fastforce simp: preserves_def valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>tc. \<lbrace>\<lambda>s. ((tc, s), mode) \<in> P\<rbrace> f e tc \<lbrace>\<lambda>tc' s'. ((snd tc', s'), mode') \<in> P\<rbrace>) \<Longrightarrow> preserves mode mode' P {((a, b), ba, tc, s') |a b ba tc s'. \<exists>r. ((r, tc), s') \<in> fst (f e a b) \<and> ba = (r \<noteq> Inr ())}
theory ADT_IF_Refine

lemma preserves_lift''':
  "(\<And>tc. \<lbrace>\<lambda>s. ((tc,s),mode) \<in> P\<rbrace> f tc \<lbrace>\<lambda>tc' s'. ((tc',s'),mode') \<in> P\<rbrace>)
   \<Longrightarrow> preserves mode mode' P {(s, u, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> f x xa)}" by (clarsimp simp: preserves_def valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>tc. \<lbrace>\<lambda>s. ((tc, s), mode) \<in> P\<rbrace> f tc \<lbrace>\<lambda>tc' s'. ((tc', s'), mode') \<in> P\<rbrace>) \<Longrightarrow> preserves mode mode' P {(s, u, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> f x xa)}
theory ADT_IF_Refine

lemma preserves'_lift:
  "(\<And>tc. \<lbrace>\<lambda>s. ((tc,s),mode) \<in> P\<rbrace> f tc \<lbrace>\<lambda>tc' s'. ((tc',s'),y s') \<in> P\<rbrace>)
   \<Longrightarrow> preserves' mode P {(s, m, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> f x xa) \<and>
                                      m = (y (snd s'))}" by (fastforce simp: preserves'_def valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>tc. \<lbrace>\<lambda>s. ((tc, s), mode) \<in> P\<rbrace> f tc \<lbrace>\<lambda>tc' s'. ((tc', s'), y s') \<in> P\<rbrace>) \<Longrightarrow> preserves' mode P {(s, m, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> f x xa) \<and> m = y (snd s')}
theory ADT_IF_Refine

lemma kernelEntry_if_valid_domain_time:
  "e \<noteq> Interrupt \<Longrightarrow> \<lbrace>\<top>\<rbrace> kernelEntry_if e tc \<lbrace>\<lambda>_ s. 0 < ksDomainTime s \<and> valid_domain_list' s\<rbrace>"
  "\<lbrace>\<top>\<rbrace>
   kernelEntry_if Interrupt tc
   \<lbrace>\<lambda>_ s. (ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<and> valid_domain_list' s\<rbrace>" unfolding kernelEntry_if_def by wpsimp+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (e \<noteq> Interrupt \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> kernelEntry_if e tc \<lbrace>\<lambda>_ s. 0 < ksDomainTime s \<and> valid_domain_list' s\<rbrace>) &&& \<lbrace>\<lambda>_. True\<rbrace> kernelEntry_if Interrupt tc \<lbrace>\<lambda>_ s. (ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<and> valid_domain_list' s\<rbrace> proof (prove)
goal (1 subgoal):
 1. (e \<noteq> Interrupt \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do t <- getCurThread;
threadSet (tcbArch_update (atcbContextSet tc)) t;
r <- handleEvent e;
stateAssert (\<lambda>s. valid_domain_list' s \<and> (e \<noteq> Interrupt \<longrightarrow> 0 < ksDomainTime s) \<and> (e = Interrupt \<longrightarrow> ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) [];
return (r, tc)
od \<lbrace>\<lambda>_ s. 0 < ksDomainTime s \<and> valid_domain_list' s\<rbrace>) &&& \<lbrace>\<lambda>_. True\<rbrace> do t <- getCurThread;
threadSet (tcbArch_update (atcbContextSet tc)) t;
r <- handleEvent Interrupt;
stateAssert (\<lambda>s. valid_domain_list' s \<and> (Interrupt \<noteq> Interrupt \<longrightarrow> 0 < ksDomainTime s) \<and> (Interrupt = Interrupt \<longrightarrow> ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) [];
return (r, tc)
od \<lbrace>\<lambda>_ s. (ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<and> valid_domain_list' s\<rbrace>
theory ADT_IF_Refine

lemma handlePreemption_if_valid_domain_time:
  "\<lbrace>\<top>\<rbrace>
   handlePreemption_if tc
   \<lbrace>\<lambda>_ s. (ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<and> valid_domain_list' s\<rbrace>" unfolding handlePreemption_if_def by (wpsimp cong: if_cong)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> handlePreemption_if tc \<lbrace>\<lambda>_ s. (ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<and> valid_domain_list' s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do irq <- doMachineOp (getActiveIRQ False);
when (irq \<noteq> None) $ handleInterrupt (the irq);
stateAssert (\<lambda>s. (ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<and> valid_domain_list' s) [];
return tc
od \<lbrace>\<lambda>_ s. (ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<and> valid_domain_list' s\<rbrace>
theory ADT_IF_Refine

lemma schedule'_if_valid_domain_time:
  "\<lbrace>\<top>\<rbrace> schedule'_if tc \<lbrace>\<lambda>_ s. 0 < ksDomainTime s\<rbrace>"
  "\<lbrace>\<top>\<rbrace> schedule'_if tc \<lbrace>\<lambda>_. valid_domain_list'\<rbrace>" unfolding schedule'_if_def by wpsimp+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> schedule'_if tc \<lbrace>\<lambda>_ s. 0 < ksDomainTime s\<rbrace> &&& \<lbrace>\<lambda>_. True\<rbrace> schedule'_if tc \<lbrace>\<lambda>_. valid_domain_list'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do ThreadDecls_H.schedule;
activateThread;
stateAssert (\<lambda>s. 0 < ksDomainTime s \<and> valid_domain_list' s) [];
return tc
od \<lbrace>\<lambda>_ s. 0 < ksDomainTime s\<rbrace> &&& \<lbrace>\<lambda>_. True\<rbrace> do ThreadDecls_H.schedule;
activateThread;
stateAssert (\<lambda>s. 0 < ksDomainTime s \<and> valid_domain_list' s) [];
return tc
od \<lbrace>\<lambda>_. valid_domain_list'\<rbrace>
theory ADT_IF_Refine

lemma kernelEntry_if_no_preempt:
  "\<lbrace>\<top>\<rbrace> kernelEntry_if Interrupt ctx \<lbrace>\<lambda>(interrupt,_) _. interrupt = Inr () \<rbrace>" unfolding kernelEntry_if_def handleEvent_def by (wp | clarsimp intro!: validE_cases_valid)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> kernelEntry_if Interrupt ctx \<lbrace>\<lambda>(interrupt, uu_) _. interrupt = Inr ()\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do t <- getCurThread;
threadSet (tcbArch_update (atcbContextSet ctx)) t;
r <- case Interrupt of SyscallEvent SysCall \<Rightarrow> handleCall | SyscallEvent SysReplyRecv \<Rightarrow> withoutPreemption $ do handleReply;
handleRecv True
od | SyscallEvent SysSend \<Rightarrow> handleSend True | SyscallEvent SysNBSend \<Rightarrow> handleSend False | SyscallEvent SysRecv \<Rightarrow> withoutPreemption $ handleRecv True | SyscallEvent SysReply \<Rightarrow> withoutPreemption handleReply | SyscallEvent SysYield \<Rightarrow> withoutPreemption handleYield | SyscallEvent SysNBRecv \<Rightarrow> withoutPreemption $ handleRecv False | UnknownSyscall n \<Rightarrow> withoutPreemption $ do thread <- getCurThread;
handleFault thread $ Fault_H.fault.UnknownSyscallException $ fromIntegral n;
return ()
od | UserLevelFault w1 w2 \<Rightarrow> withoutPreemption $ do thread <- getCurThread;
handleFault thread $ Fault_H.fault.UserException (w1 && mask 32) (w2 && mask 28);
return ()
od | Interrupt \<Rightarrow> withoutPreemption $ do active <- doMachineOp (getActiveIRQ False);
case active of None \<Rightarrow> doMachineOp $ debugPrint [] | Some irq \<Rightarrow> handleInterrupt irq
od | VMFaultEvent faultType \<Rightarrow> withoutPreemption $ do thread <- getCurThread;
handleVMFault thread faultType `~catchFailure~` handleFault thread;
return ()
od | HypervisorEvent hypType \<Rightarrow> withoutPreemption $ do thread <- getCurThread;
handleHypervisorFault thread hypType
od;
stateAssert (\<lambda>s. valid_domain_list' s \<and> (Interrupt \<noteq> Interrupt \<longrightarrow> 0 < ksDomainTime s) \<and> (Interrupt = Interrupt \<longrightarrow> ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread)) [];
return (r, ctx)
od \<lbrace>\<lambda>(interrupt, uu_) _. interrupt = Inr ()\<rbrace>
theory ADT_IF_Refine

lemma Init_Fin_ADT_H:
  "s' \<in> full_invs_if'
   \<Longrightarrow> s' \<in> Init (ADT_H_if uop) (Fin (ADT_H_if uop) s')" apply (clarsimp simp: ADT_H_if_def) apply (case_tac s') apply simp apply (case_tac a) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s' \<in> full_invs_if' \<Longrightarrow> s' \<in> Init (ADT_H_if uop) (Fin (ADT_H_if uop) s') proof (prove)
goal (1 subgoal):
 1. s' \<in> full_invs_if' \<Longrightarrow> s' \<in> ({user_context_of (case s' of (x, xa) \<Rightarrow> (case x of (uc, s) \<Rightarrow> Pair (uc, absKState s)) xa)} \<times> {s'a. absKState s'a = internal_state_if (case s' of (x, xa) \<Rightarrow> (case x of (uc, s) \<Rightarrow> Pair (uc, absKState s)) xa)}) \<times> {sys_mode_of (case s' of (x, xa) \<Rightarrow> (case x of (uc, s) \<Rightarrow> Pair (uc, absKState s)) xa)} proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>s' \<in> full_invs_if'; s' = (a, b)\<rbrakk> \<Longrightarrow> s' \<in> ({user_context_of (case s' of (x, xa) \<Rightarrow> (case x of (uc, s) \<Rightarrow> Pair (uc, absKState s)) xa)} \<times> {s'a. absKState s'a = internal_state_if (case s' of (x, xa) \<Rightarrow> (case x of (uc, s) \<Rightarrow> Pair (uc, absKState s)) xa)}) \<times> {sys_mode_of (case s' of (x, xa) \<Rightarrow> (case x of (uc, s) \<Rightarrow> Pair (uc, absKState s)) xa)} proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> full_invs_if'; s' = (a, b)\<rbrakk> \<Longrightarrow> a \<in> {user_context_of ((case a of (uc, s) \<Rightarrow> Pair (uc, absKState s)) b)} \<times> {s'. absKState s' = internal_state_if ((case a of (uc, s) \<Rightarrow> Pair (uc, absKState s)) b)} \<and> b = sys_mode_of ((case a of (uc, s) \<Rightarrow> Pair (uc, absKState s)) b) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>(a, b) \<in> full_invs_if'; s' = (a, b); a = (aa, ba)\<rbrakk> \<Longrightarrow> a \<in> {user_context_of ((case a of (uc, s) \<Rightarrow> Pair (uc, absKState s)) b)} \<times> {s'. absKState s' = internal_state_if ((case a of (uc, s) \<Rightarrow> Pair (uc, absKState s)) b)} \<and> b = sys_mode_of ((case a of (uc, s) \<Rightarrow> Pair (uc, absKState s)) b) proof (prove)
goal:
No subgoals!
theory ADT_IF_Refine

lemma extras_inter'[dest!]:
   "(t,mode) \<in> has_srel_state (lift_fst_rel srel) invs_conc \<Longrightarrow> (t,mode) \<in> extras_abs" apply (rule set_mp) apply (rule extras_abs_intro) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (t, mode) \<in> has_srel_state (lift_fst_rel srel) invs_conc \<Longrightarrow> (t, mode) \<in> extras_abs proof (prove)
goal (2 subgoals):
 1. (t, mode) \<in> has_srel_state (lift_fst_rel srel) invs_conc \<Longrightarrow> ?A \<subseteq> extras_abs
 2. (t, mode) \<in> has_srel_state (lift_fst_rel srel) invs_conc \<Longrightarrow> (t, mode) \<in> ?A proof (prove)
goal (1 subgoal):
 1. (t, mode) \<in> has_srel_state (lift_fst_rel srel) invs_conc \<Longrightarrow> (t, mode) \<in> has_srel_state (lift_fst_rel srel) invs_conc proof (prove)
goal:
No subgoals!
theory ADT_IF_Refine

lemma fw_simulates: "ADT_conc \<sqsubseteq>\<^sub>F ADT_abs" apply (rule L_invariantI) apply (rule abs.ADT_invs) apply (rule conc.ADT_invs) apply (rule fw_sim_abs_conc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ADT_conc \<sqsubseteq>\<^sub>F ADT_abs proof (prove)
goal (3 subgoals):
 1. ADT_abs \<Turnstile> ?I\<^sub>a
 2. ADT_conc \<Turnstile> ?I\<^sub>c
 3. LI ADT_abs ADT_conc ?r (?I\<^sub>a \<times> ?I\<^sub>c) proof (prove)
goal (2 subgoals):
 1. ADT_conc \<Turnstile> ?I\<^sub>c
 2. LI ADT_abs ADT_conc ?r (invs_abs \<times> ?I\<^sub>c) proof (prove)
goal (1 subgoal):
 1. LI ADT_abs ADT_conc ?r (invs_abs \<times> invs_conc) proof (prove)
goal:
No subgoals!
theory ADT_IF_Refine

lemma refinement: "ADT_conc \<sqsubseteq> ADT_abs" by (rule sim_imp_refines[OF fw_simulates])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ADT_conc \<sqsubseteq> ADT_abs
theory ADT_IF_Refine

lemma step_corres_lift:
  "\<lbrakk> \<And>tc. corres_underlying srel False nf (=) (\<lambda>s. ((tc,s),mode) \<in> P) (\<lambda>s'. ((tc,s'),mode) \<in> P')
                            (f tc) (f' tc);
     \<And>tc. nf \<Longrightarrow> empty_fail (f' tc) \<rbrakk>
     \<Longrightarrow> step_corres nf (lift_snd_rel srel) mode P P'
           {((tc, s), irq, tc', s'). ((irq, tc'), s') \<in> fst (f tc s)}
           {((tc, s), irq, tc', s'). ((irq, tc'), s') \<in> fst (f' tc s)}" by (fastforce simp: corres_underlying_def step_corres_def lift_snd_rel_def empty_fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>tc. corres_underlying srel False nf (=) (\<lambda>s. ((tc, s), mode) \<in> P) (\<lambda>s'. ((tc, s'), mode) \<in> P') (f tc) (f' tc); \<And>tc. nf \<Longrightarrow> empty_fail (f' tc)\<rbrakk> \<Longrightarrow> step_corres nf (lift_snd_rel srel) mode P P' {((tc, s), irq, tc', s'). ((irq, tc'), s') \<in> fst (f tc s)} {((tc, s), irq, tc', s'). ((irq, tc'), s') \<in> fst (f' tc s)}
theory ADT_IF_Refine

lemma step_corres_lift':
  "(\<And>tc. corres_underlying srel False nf (=)
            (\<lambda>s. ((tc,s),mode) \<in> P) (\<lambda>s'. ((tc,s'),mode) \<in> P') (f u tc) (f' u tc)) \<Longrightarrow>
   (\<And>tc. nf \<Longrightarrow> empty_fail (f' u tc)) \<Longrightarrow>
   step_corres nf (lift_snd_rel srel) mode
         P P'
         {((a, b), e, tc, s') |a b e tc s'.
          ((e, tc), s') \<in> fst (f u a b)}
         {((a, b), e, tc, s') |a b e tc s'.
          ((e, tc), s') \<in> fst (f' u a b)}" by (fastforce simp: corres_underlying_def step_corres_def lift_snd_rel_def empty_fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>tc. corres_underlying srel False nf (=) (\<lambda>s. ((tc, s), mode) \<in> P) (\<lambda>s'. ((tc, s'), mode) \<in> P') (f u tc) (f' u tc); \<And>tc. nf \<Longrightarrow> empty_fail (f' u tc)\<rbrakk> \<Longrightarrow> step_corres nf (lift_snd_rel srel) mode P P' {((a, b), e, tc, s') |a b e tc s'. ((e, tc), s') \<in> fst (f u a b)} {((a, b), e, tc, s') |a b e tc s'. ((e, tc), s') \<in> fst (f' u a b)}
theory ADT_IF_Refine

lemma step_corres_lift'':
  "\<lbrakk> \<And>tc. corres_underlying srel False nf
            (\<lambda>r r'. ((fst r) = Inr ()) = ((fst r') = Inr ()) \<and> (snd r) = (snd r'))
            (\<lambda>s. ((tc,s),mode) \<in> P) (\<lambda>s'. ((tc,s'),mode) \<in> P') (f e tc) (f' e tc);
     \<And>tc. nf \<Longrightarrow> empty_fail (f' e tc) \<rbrakk>
     \<Longrightarrow> step_corres nf (lift_snd_rel srel) mode P P'
           {((a, b), ba, tc, s') |a b ba tc s'. \<exists>r. ((r, tc), s') \<in> fst (f e a b) \<and>
                                                    ba = (r \<noteq> Inr ())}
           {((a, b), ba, tc, s') |a b ba tc s'. \<exists>r. ((r, tc), s') \<in> fst (f' e a b) \<and>
                                                    ba = (r \<noteq> Inr ())}" by (fastforce simp: corres_underlying_def step_corres_def lift_snd_rel_def empty_fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>tc. corres_underlying srel False nf (\<lambda>r r'. (fst r = Inr ()) = (fst r' = Inr ()) \<and> snd r = snd r') (\<lambda>s. ((tc, s), mode) \<in> P) (\<lambda>s'. ((tc, s'), mode) \<in> P') (f e tc) (f' e tc); \<And>tc. nf \<Longrightarrow> empty_fail (f' e tc)\<rbrakk> \<Longrightarrow> step_corres nf (lift_snd_rel srel) mode P P' {((a, b), ba, tc, s') |a b ba tc s'. \<exists>r. ((r, tc), s') \<in> fst (f e a b) \<and> ba = (r \<noteq> Inr ())} {((a, b), ba, tc, s') |a b ba tc s'. \<exists>r. ((r, tc), s') \<in> fst (f' e a b) \<and> ba = (r \<noteq> Inr ())}
theory ADT_IF_Refine

lemma step_corres_lift''':
  "\<lbrakk> \<And>tc. corres_underlying srel False nf (=) (\<lambda>s. ((tc,s),mode) \<in> P)
                            (\<lambda>s'. ((tc,s'),mode) \<in> P') (f tc) (f' tc);
     \<And>tc. nf \<Longrightarrow> empty_fail (f' tc) \<rbrakk>
     \<Longrightarrow> step_corres nf (lift_snd_rel srel) mode P P'
           {(s, u, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> f x xa)}
           {(s, u, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> f' x xa)}" by (fastforce simp: corres_underlying_def step_corres_def lift_snd_rel_def empty_fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>tc. corres_underlying srel False nf (=) (\<lambda>s. ((tc, s), mode) \<in> P) (\<lambda>s'. ((tc, s'), mode) \<in> P') (f tc) (f' tc); \<And>tc. nf \<Longrightarrow> empty_fail (f' tc)\<rbrakk> \<Longrightarrow> step_corres nf (lift_snd_rel srel) mode P P' {(s, u, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> f x xa)} {(s, u, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> f' x xa)}
theory ADT_IF_Refine

lemma ct_running'_related:
  "\<lbrakk> (a, c) \<in> state_relation; invs' c; ct_running a \<rbrakk>
     \<Longrightarrow> ct_running' c" apply (clarsimp simp: ct_in_state_def ct_in_state'_def
                        curthread_relation) apply (frule(1) st_tcb_at_coerce_haskell) apply (simp add: invs'_def cur_tcb'_def curthread_relation) apply (erule pred_tcb'_weakenE) apply (case_tac st, simp_all)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(a, c) \<in> state_relation; invs' c; ct_running a\<rbrakk> \<Longrightarrow> ct_running' c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(a, c) \<in> state_relation; invs' c; st_tcb_at (\<lambda>st. st = Structures_A.thread_state.Running) (cur_thread a) a\<rbrakk> \<Longrightarrow> st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) (cur_thread a) c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(a, c) \<in> state_relation; invs' c; st_tcb_at (\<lambda>st. st = Structures_A.thread_state.Running) (cur_thread a) a\<rbrakk> \<Longrightarrow> tcb_at' (cur_thread a) c
 2. \<lbrakk>(a, c) \<in> state_relation; invs' c; st_tcb_at (\<lambda>st. st = Structures_A.thread_state.Running) (cur_thread a) a; st_tcb_at' (\<lambda>st'. \<exists>st. thread_state_relation st st' \<and> st = Structures_A.thread_state.Running) (cur_thread a) c\<rbrakk> \<Longrightarrow> st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) (cur_thread a) c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(a, c) \<in> state_relation; invs' c; st_tcb_at (\<lambda>st. st = Structures_A.thread_state.Running) (cur_thread a) a; st_tcb_at' (\<lambda>st'. \<exists>st. thread_state_relation st st' \<and> st = Structures_A.thread_state.Running) (cur_thread a) c\<rbrakk> \<Longrightarrow> st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) (cur_thread a) c proof (prove)
goal (1 subgoal):
 1. \<And>st. \<lbrakk>(a, c) \<in> state_relation; invs' c; st_tcb_at (\<lambda>st. st = Structures_A.thread_state.Running) (cur_thread a) a; \<exists>sta. thread_state_relation sta st \<and> sta = Structures_A.thread_state.Running\<rbrakk> \<Longrightarrow> st = Structures_H.thread_state.Running proof (prove)
goal:
No subgoals!
theory ADT_IF_Refine

lemma invs_machine_state:
  "invs s \<Longrightarrow> valid_machine_state s" by (clarsimp simp: invs_def valid_state_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs s \<Longrightarrow> valid_machine_state s
theory ADT_IF_Refine

lemma sched_act_cnt_related:
  "\<lbrakk> (a, c) \<in> state_relation; ksSchedulerAction c = ChooseNewThread \<rbrakk>
     \<Longrightarrow> scheduler_action a = choose_new_thread" by (case_tac "scheduler_action a", simp_all add: state_relation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(a, c) \<in> state_relation; ksSchedulerAction c = ChooseNewThread\<rbrakk> \<Longrightarrow> scheduler_action a = choose_new_thread