kings-crown/FVELER_Isabelle huggingface dataset:
theory Finalise_DR

lemma imp_strength:
  "(A \<and> (B\<longrightarrow>C)) \<longrightarrow> (B \<longrightarrow> (A\<and>C))" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. A \<and> (B \<longrightarrow> C) \<longrightarrow> B \<longrightarrow> A \<and> C
theory Finalise_DR

lemma valid_pde_pt_at:
  "\<lbrakk>valid_pde (ARM_A.pde.PageTablePDE word1 se word2) s \<and> pspace_aligned s\<rbrakk>
  \<Longrightarrow> (ptrFromPAddr word1, unat ((vaddr >> 12) && 0xFF)) =
  transform_pt_slot_ref (ptrFromPAddr word1 + ((vaddr >> 12) && 0xFF << 2))" apply (clarsimp simp :transform_pt_slot_ref_def ) apply (drule(1) pt_aligned) apply (simp add:vaddr_segment_nonsense3
    vaddr_segment_nonsense4) apply (subst shiftl_shiftr_id) apply simp apply (rule le_less_trans[OF word_and_le1]) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_pde (PageTablePDE word1 se word2) s \<and> pspace_aligned s \<Longrightarrow> (ptrFromPAddr word1, unat ((vaddr >> 12) && 0xFF)) = transform_pt_slot_ref (ptrFromPAddr word1 + ((vaddr >> 12) && 0xFF << 2)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>typ_at (AArch APageTable) (ptrFromPAddr word1) s; pspace_aligned s\<rbrakk> \<Longrightarrow> ptrFromPAddr word1 = ptrFromPAddr word1 + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits \<and> (vaddr >> 12) && 0xFF = ptrFromPAddr word1 + ((vaddr >> 12) && 0xFF << 2) && mask pt_bits >> 2 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_aligned s; is_aligned (ptrFromPAddr word1) 10\<rbrakk> \<Longrightarrow> ptrFromPAddr word1 = ptrFromPAddr word1 + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits \<and> (vaddr >> 12) && 0xFF = ptrFromPAddr word1 + ((vaddr >> 12) && 0xFF << 2) && mask pt_bits >> 2 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_aligned s; is_aligned (ptrFromPAddr word1) 10\<rbrakk> \<Longrightarrow> (vaddr >> 12) && 0xFF = (vaddr >> 12) && 0xFF << 2 >> 2 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>pspace_aligned s; is_aligned (ptrFromPAddr word1) 10\<rbrakk> \<Longrightarrow> 2 < LENGTH(32)
 2. \<lbrakk>pspace_aligned s; is_aligned (ptrFromPAddr word1) 10\<rbrakk> \<Longrightarrow> (vaddr >> 12) && 0xFF < 2 ^ (LENGTH(32) - 2)
 3. \<lbrakk>pspace_aligned s; is_aligned (ptrFromPAddr word1) 10\<rbrakk> \<Longrightarrow> (vaddr >> 12) && 0xFF = (vaddr >> 12) && 0xFF proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pspace_aligned s; is_aligned (ptrFromPAddr word1) 10\<rbrakk> \<Longrightarrow> (vaddr >> 12) && 0xFF < 2 ^ (LENGTH(32) - 2)
 2. \<lbrakk>pspace_aligned s; is_aligned (ptrFromPAddr word1) 10\<rbrakk> \<Longrightarrow> (vaddr >> 12) && 0xFF = (vaddr >> 12) && 0xFF proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pspace_aligned s; is_aligned (ptrFromPAddr word1) 10\<rbrakk> \<Longrightarrow> 0xFF < 2 ^ (LENGTH(32) - 2)
 2. \<lbrakk>pspace_aligned s; is_aligned (ptrFromPAddr word1) 10\<rbrakk> \<Longrightarrow> (vaddr >> 12) && 0xFF = (vaddr >> 12) && 0xFF proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_aligned s; is_aligned (ptrFromPAddr word1) 10\<rbrakk> \<Longrightarrow> (vaddr >> 12) && 0xFF = (vaddr >> 12) && 0xFF proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma find_pd_for_asid_kernel_mapping_help:
  "\<lbrace>pspace_aligned and valid_vspace_objs and K (v<kernel_base) \<rbrace> find_pd_for_asid a
   \<lbrace>\<lambda>rv s. ucast (lookup_pd_slot rv v && mask pd_bits >> 2) \<notin> kernel_mapping_slots \<rbrace>,-" apply (rule hoare_gen_asmE) apply (rule hoare_post_imp_R) apply (rule find_pd_for_asid_aligned_pd_bits) apply simp apply (rule less_kernel_base_mapping_slots) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned and valid_vspace_objs and K (v < kernel_base)\<rbrace> find_pd_for_asid a \<lbrace>\<lambda>rv s. UCAST(32 \<rightarrow> 12) (lookup_pd_slot rv v && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. v < kernel_base \<Longrightarrow> \<lbrace>pspace_aligned and valid_vspace_objs\<rbrace> find_pd_for_asid a \<lbrace>\<lambda>rv s. UCAST(32 \<rightarrow> 12) (lookup_pd_slot rv v && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. v < kernel_base \<Longrightarrow> \<lbrace>pspace_aligned and valid_vspace_objs\<rbrace> find_pd_for_asid a \<lbrace>?Q'2\<rbrace>, -
 2. \<And>rv s. \<lbrakk>v < kernel_base; ?Q'2 rv s\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (lookup_pd_slot rv v && mask pd_bits >> 2) \<notin> kernel_mapping_slots proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>v < kernel_base; is_aligned rv pd_bits\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (lookup_pd_slot rv v && mask pd_bits >> 2) \<notin> kernel_mapping_slots proof (prove)
goal (1 subgoal):
 1. \<And>rv. \<lbrakk>v < kernel_base; is_aligned rv pd_bits\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (lookup_pd_slot rv v && mask pd_bits >> 2) \<notin> kernel_mapping_slots proof (prove)
goal (2 subgoals):
 1. \<And>rv. \<lbrakk>v < kernel_base; is_aligned rv pd_bits\<rbrakk> \<Longrightarrow> v < kernel_base
 2. \<And>rv. \<lbrakk>v < kernel_base; is_aligned rv pd_bits\<rbrakk> \<Longrightarrow> is_aligned rv pd_bits proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma corres_dummy_returnOk_l:
  "dcorres cr P P' (f >>=E returnOk) g \<Longrightarrow> dcorres cr P P' f g" by (simp add:liftE_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres cr P P' (f >>=E returnOk) g \<Longrightarrow> dcorres cr P P' f g
theory Finalise_DR

lemma dcorres_delete_asid_none:
  "dcorres dc \<top> \<top> (CSpace_D.delete_asid x word) (return ())" apply (clarsimp simp:CSpace_D.delete_asid_def) apply (rule corres_alternate2) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>_. True) (CSpace_D.delete_asid x word) (return ()) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>_. True) (do asid_table <- gets cdl_asid_table;
case asid_table (fst x) of None \<Rightarrow> fail | Some cdl_cap.NullCap \<Rightarrow> return () | Some (AsidPoolCap p xa) \<Rightarrow> KHeap_D.set_cap (p, snd x) cdl_cap.NullCap | Some _ \<Rightarrow> fail
od \<sqinter> return ()) (return ()) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (return ()) proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma asid_table_transform:
  "cdl_asid_table (transform s) slot =
   unat_map (Some \<circ> transform_asid_table_entry \<circ> arm_asid_table (arch_state s)) slot" apply (simp add:transform_def transform_asid_table_def transform_asid_table_entry_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cdl_asid_table (transform s) slot = unat_map (Some \<circ> transform_asid_table_entry \<circ> asid_table s) slot proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma thread_in_thread_cap_not_idle:
 "\<lbrakk>valid_global_refs s;cte_wp_at ((=) (cap.ThreadCap ptr)) slot s\<rbrakk>
  \<Longrightarrow> not_idle_thread ptr s" apply (rule ccontr) apply (clarsimp simp:valid_cap_def valid_global_refs_def valid_refs_def) apply (case_tac slot) apply (drule_tac x = a in spec) apply (drule_tac x = b in spec) apply (clarsimp simp:cte_wp_at_def not_idle_thread_def) apply (simp add:cap_range_def global_refs_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_global_refs s; cte_wp_at ((=) (ThreadCap ptr)) slot s\<rbrakk> \<Longrightarrow> not_idle_thread ptr s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_global_refs s; cte_wp_at ((=) (ThreadCap ptr)) slot s; \<not> not_idle_thread ptr s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>a b. \<not> cte_wp_at (\<lambda>c. global_refs s \<inter> cap_range c \<noteq> {}) (a, b) s; cte_wp_at ((=) (ThreadCap ptr)) slot s; \<not> not_idle_thread ptr s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>a b. \<not> cte_wp_at (\<lambda>c. global_refs s \<inter> cap_range c \<noteq> {}) (a, b) s; cte_wp_at ((=) (ThreadCap ptr)) slot s; \<not> not_idle_thread ptr s; slot = (a, b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>cte_wp_at ((=) (ThreadCap ptr)) slot s; \<not> not_idle_thread ptr s; slot = (a, b); \<forall>b. \<not> cte_wp_at (\<lambda>c. global_refs s \<inter> cap_range c \<noteq> {}) (a, b) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>cte_wp_at ((=) (ThreadCap ptr)) slot s; \<not> not_idle_thread ptr s; slot = (a, b); \<not> cte_wp_at (\<lambda>c. global_refs s \<inter> cap_range c \<noteq> {}) (a, b) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>fst (CSpaceAcc_A.get_cap (a, b) s) = {(ThreadCap (idle_thread s), s)}; ptr = idle_thread s; slot = (a, b); global_refs s \<inter> cap_range (ThreadCap (idle_thread s)) = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma prepare_thread_delete_dcorres: "dcorres dc P P' (CSpace_D.prepare_thread_delete t) (prepare_thread_delete t)" apply (clarsimp simp: CSpace_D.prepare_thread_delete_def prepare_thread_delete_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc P P' (CSpace_D.prepare_thread_delete t) (local.prepare_thread_delete t) proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma dcorres_splits:
  "\<lbrakk> T a \<Longrightarrow> dcorres r P (Q a) f (g a);
    \<not> T a \<Longrightarrow> dcorres r P (Q' a) f (g a)\<rbrakk>\<Longrightarrow>
    dcorres r P ( (\<lambda>s. (T a) \<longrightarrow> (Q a s)) and (\<lambda>s. (\<not> (T a)) \<longrightarrow> (Q' a s)) ) f (g a)" apply (case_tac "T a") apply clarsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>T a \<Longrightarrow> dcorres r P (Q a) f (g a); \<not> T a \<Longrightarrow> dcorres r P (Q' a) f (g a)\<rbrakk> \<Longrightarrow> dcorres r P ((\<lambda>s. T a \<longrightarrow> Q a s) and (\<lambda>s. \<not> T a \<longrightarrow> Q' a s)) f (g a) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>T a \<Longrightarrow> dcorres r P (Q a) f (g a); \<not> T a \<Longrightarrow> dcorres r P (Q' a) f (g a); T a\<rbrakk> \<Longrightarrow> dcorres r P ((\<lambda>s. T a \<longrightarrow> Q a s) and (\<lambda>s. \<not> T a \<longrightarrow> Q' a s)) f (g a)
 2. \<lbrakk>T a \<Longrightarrow> dcorres r P (Q a) f (g a); \<not> T a \<Longrightarrow> dcorres r P (Q' a) f (g a); \<not> T a\<rbrakk> \<Longrightarrow> dcorres r P ((\<lambda>s. T a \<longrightarrow> Q a s) and (\<lambda>s. \<not> T a \<longrightarrow> Q' a s)) f (g a) proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma get_cap_weak_wp:
  "\<lbrace>cte_wp_at Q slot\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>rv s. Q rv\<rbrace>" by (clarsimp simp:valid_def cte_wp_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at Q slot\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>rv s. Q rv\<rbrace>
theory Finalise_DR

lemma obj_ref_not_idle:
  "\<lbrakk>valid_objs s;valid_global_refs s;cte_at slot s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. \<forall>x\<in>obj_refs cap. not_idle_thread x s) slot s" apply (simp add:valid_global_refs_def valid_refs_def) apply (case_tac slot) apply clarsimp apply (drule_tac x = a in spec) apply (drule_tac x = b in spec) apply (clarsimp simp:cte_wp_at_def not_idle_thread_def cap_range_def global_refs_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; valid_global_refs s; cte_wp_at (\<lambda>_. True) slot s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. \<forall>x\<in>obj_refs cap. not_idle_thread x s) slot s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; \<forall>a b. \<not> cte_wp_at (\<lambda>c. global_refs s \<inter> cap_range c \<noteq> {}) (a, b) s; cte_wp_at (\<lambda>_. True) slot s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. \<forall>x\<in>obj_refs cap. not_idle_thread x s) slot s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>valid_objs s; \<forall>a b. \<not> cte_wp_at (\<lambda>c. global_refs s \<inter> cap_range c \<noteq> {}) (a, b) s; cte_wp_at (\<lambda>_. True) slot s; slot = (a, b)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. \<forall>x\<in>obj_refs cap. not_idle_thread x s) slot s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>valid_objs s; \<forall>a b. \<not> cte_wp_at (\<lambda>c. global_refs s \<inter> cap_range c \<noteq> {}) (a, b) s; cte_wp_at (\<lambda>_. True) (a, b) s; slot = (a, b)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. \<forall>x\<in>obj_refs cap. not_idle_thread x s) (a, b) s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>valid_objs s; cte_wp_at (\<lambda>_. True) (a, b) s; slot = (a, b); \<forall>b. \<not> cte_wp_at (\<lambda>c. global_refs s \<inter> cap_range c \<noteq> {}) (a, b) s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. \<forall>x\<in>obj_refs cap. not_idle_thread x s) (a, b) s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>valid_objs s; cte_wp_at (\<lambda>_. True) (a, b) s; slot = (a, b); \<not> cte_wp_at (\<lambda>c. global_refs s \<inter> cap_range c \<noteq> {}) (a, b) s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. \<forall>x\<in>obj_refs cap. not_idle_thread x s) (a, b) s proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma singleton_set_eq:
  "\<lbrakk>x = {a}; b\<in> x\<rbrakk>\<Longrightarrow> b = a" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = {a}; b \<in> x\<rbrakk> \<Longrightarrow> b = a
theory Finalise_DR

lemma monadic_trancl_steps:
  "monadic_rewrite False False \<top>
     (monadic_trancl f x)
     (do y \<leftarrow> monadic_trancl f x;
           monadic_trancl f y od)" apply (simp add: monadic_rewrite_def monadic_trancl_def
                   bind_def split_def monadic_option_dest_def) apply (safe, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite False False (\<lambda>_. True) (monadic_trancl f x) (monadic_trancl f x >>= monadic_trancl f) proof (prove)
goal (1 subgoal):
 1. \<forall>s. (\<Union>x\<in>Some -` (monadic_rel_optionation_form f)\<^sup>* `` {Some (x, s)}. Some -` (monadic_rel_optionation_form f)\<^sup>* `` {Some x}) \<subseteq> Some -` (monadic_rel_optionation_form f)\<^sup>* `` {Some (x, s)} \<and> ((\<exists>x\<in>Some -` (monadic_rel_optionation_form f)\<^sup>* `` {Some (x, s)}. (Some x, None) \<in> (monadic_rel_optionation_form f)\<^sup>*) \<longrightarrow> (Some (x, s), None) \<in> (monadic_rel_optionation_form f)\<^sup>*) proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma monadic_trancl_f:
  "monadic_rewrite False False \<top>
     (monadic_trancl f x) (f x)" apply (simp add: monadic_rewrite_def monadic_trancl_def
                   bind_def split_def monadic_option_dest_def) apply (safe, simp_all) apply (simp add: r_into_rtrancl monadic_rel_optionation_form_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite False False (\<lambda>_. True) (monadic_trancl f x) (f x) proof (prove)
goal (1 subgoal):
 1. \<forall>s. fst (f x s) \<subseteq> Some -` (monadic_rel_optionation_form f)\<^sup>* `` {Some (x, s)} \<and> (snd (f x s) \<longrightarrow> (Some (x, s), None) \<in> (monadic_rel_optionation_form f)\<^sup>*) proof (prove)
goal (2 subgoals):
 1. \<And>s a b. (a, b) \<in> fst (f x s) \<Longrightarrow> (Some (x, s), Some (a, b)) \<in> (monadic_rel_optionation_form f)\<^sup>*
 2. \<And>s. snd (f x s) \<Longrightarrow> (Some (x, s), None) \<in> (monadic_rel_optionation_form f)\<^sup>* proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma monadic_trancl_step:
  "monadic_rewrite False False \<top>
       (monadic_trancl f x) (do y \<leftarrow> f x; monadic_trancl f y od)" apply (monadic_rewrite_l monadic_trancl_steps) apply (monadic_rewrite_l monadic_trancl_f) apply (rule monadic_rewrite_refl) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite False False (\<lambda>_. True) (monadic_trancl f x) (f x >>= monadic_trancl f) proof (prove)
goal (2 subgoals):
 1. monadic_rewrite False False ?Q1 (monadic_trancl f x >>= monadic_trancl f) (f x >>= monadic_trancl f)
 2. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q1) s proof (prove)
goal (2 subgoals):
 1. monadic_rewrite False False ?Q9 (f x >>= monadic_trancl f) (f x >>= monadic_trancl f)
 2. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ((\<lambda>_. True) and ?Q9)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ((\<lambda>_. True) and (\<lambda>_. True))) s proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma monadic_trancl_return:
  "monadic_rewrite False False \<top>
          (monadic_trancl f x) (return x)" by (simp add: monadic_rewrite_def monadic_trancl_def
                monadic_option_dest_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite False False (\<lambda>_. True) (monadic_trancl f x) (return x)
theory Finalise_DR

lemma rtrancl_idem:
  assumes S: "S `` T = T"
       shows "S\<^sup>* `` T = T" proof - note P = eqset_imp_iff[OF S, THEN iffD1, OF ImageI] have Q: "\<And>x y. (x, y) \<in> S\<^sup>* \<Longrightarrow> x \<in> T \<longrightarrow> y \<in> T" by (erule rtrancl.induct, auto dest: P) thus ?thesis by auto qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. S\<^sup>* `` T = T proof (state)
goal (1 subgoal):
 1. S\<^sup>* `` T = T proof (state)
this:
\<lbrakk>(?a2, ?x1) \<in> S; ?a2 \<in> T\<rbrakk> \<Longrightarrow> ?x1 \<in> T

goal (1 subgoal):
 1. S\<^sup>* `` T = T proof (prove)
goal (1 subgoal):
 1. \<And>x y. (x, y) \<in> S\<^sup>* \<Longrightarrow> x \<in> T \<longrightarrow> y \<in> T proof (state)
this:
(?x, ?y) \<in> S\<^sup>* \<Longrightarrow> ?x \<in> T \<longrightarrow> ?y \<in> T

goal (1 subgoal):
 1. S\<^sup>* `` T = T proof (prove)
using this:
(?x, ?y) \<in> S\<^sup>* \<Longrightarrow> ?x \<in> T \<longrightarrow> ?y \<in> T

goal (1 subgoal):
 1. S\<^sup>* `` T = T proof (state)
this:
S\<^sup>* `` T = T

goal:
No subgoals!
theory Finalise_DR

lemma monadic_trancl_lift_Inl:
  "monadic_trancl (lift f) (Inl err) = throwError err" apply (rule ext) apply (simp add: throwError_def return_def monadic_trancl_def) apply (subst rtrancl_idem) apply (auto simp: monadic_rel_optionation_form_def lift_def
                     throwError_def return_def monadic_option_dest_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_trancl (lift f) (Inl err) = throwError err proof (prove)
goal (1 subgoal):
 1. \<And>x. monadic_trancl (lift f) (Inl err) x = throwError err x proof (prove)
goal (1 subgoal):
 1. \<And>x. monadic_option_dest ((monadic_rel_optionation_form (lift f))\<^sup>* `` {Some (Inl err, x)}) = ({(Inl err, x)}, False) proof (prove)
goal (2 subgoals):
 1. \<And>x. monadic_rel_optionation_form (lift f) `` {Some (Inl err, x)} = {Some (Inl err, x)}
 2. \<And>x. monadic_option_dest {Some (Inl err, x)} = ({(Inl err, x)}, False) proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma monadic_trancl_preemptible_steps:
  "monadic_rewrite False False \<top>
      (monadic_trancl_preemptible f x)
      (doE y \<leftarrow> monadic_trancl_preemptible f x;
              monadic_trancl_preemptible f y odE)" unfolding monadic_trancl_preemptible_def bindE_def apply (monadic_rewrite_l monadic_trancl_steps) apply (rule monadic_rewrite_bind_tail) apply (case_tac y; simp add: lift_def monadic_trancl_lift_Inl) apply (rule monadic_rewrite_refl)+ apply wpsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite False False (\<lambda>_. True) (monadic_trancl_preemptible f x) (monadic_trancl_preemptible f x >>=E monadic_trancl_preemptible f) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite False False (\<lambda>_. True) (monadic_trancl (lift f) (Inr x)) (monadic_trancl (lift f) (Inr x) >>= lift (\<lambda>y. monadic_trancl (lift f) (Inr y))) proof (prove)
goal (2 subgoals):
 1. monadic_rewrite False False ?Q1 (monadic_trancl (lift f) (Inr x) >>= monadic_trancl (lift f)) (monadic_trancl (lift f) (Inr x) >>= lift (\<lambda>y. monadic_trancl (lift f) (Inr y)))
 2. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q1) s proof (prove)
goal (3 subgoals):
 1. \<And>y. monadic_rewrite False False (?Q9 y) (monadic_trancl (lift f) y) (lift (\<lambda>y. monadic_trancl (lift f) (Inr y)) y)
 2. \<lbrace>?Q1\<rbrace> monadic_trancl (lift f) (Inr x) \<lbrace>?Q9\<rbrace>
 3. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q1) s proof (prove)
goal (4 subgoals):
 1. \<And>y a. y = Inl a \<Longrightarrow> monadic_rewrite False False (?Q9 (Inl a)) (throwError a) (throwError a)
 2. \<And>y b. y = Inr b \<Longrightarrow> monadic_rewrite False False (?Q9 (Inr b)) (monadic_trancl (lift f) (Inr b)) (monadic_trancl (lift f) (Inr b))
 3. \<lbrace>?Q1\<rbrace> monadic_trancl (lift f) (Inr x) \<lbrace>?Q9\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q1) s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q1\<rbrace> monadic_trancl (lift f) (Inr x) \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q1) s proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma monadic_trancl_preemptible_f:
  "monadic_rewrite False False (\<lambda>_. True)
     (monadic_trancl_preemptible f x) (f x)" unfolding monadic_trancl_preemptible_def apply (monadic_rewrite_l monadic_trancl_f) apply (fastforce simp: lift_def intro!: monadic_rewrite_refl)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite False False (\<lambda>_. True) (monadic_trancl_preemptible f x) (f x) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite False False (\<lambda>_. True) (monadic_trancl (lift f) (Inr x)) (f x) proof (prove)
goal (2 subgoals):
 1. monadic_rewrite False False ?Q1 (lift f (Inr x)) (f x)
 2. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q1) s proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma monadic_trancl_preemptible_step:
  "monadic_rewrite False False \<top>
      (monadic_trancl_preemptible f x)
      (doE y \<leftarrow> f x;
            monadic_trancl_preemptible f y odE)" apply (monadic_rewrite_l monadic_trancl_preemptible_steps) apply (monadic_rewrite_l monadic_trancl_preemptible_f) apply (fastforce intro!: monadic_rewrite_refl)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite False False (\<lambda>_. True) (monadic_trancl_preemptible f x) (f x >>=E monadic_trancl_preemptible f) proof (prove)
goal (2 subgoals):
 1. monadic_rewrite False False ?Q1 (monadic_trancl_preemptible f x >>=E monadic_trancl_preemptible f) (f x >>=E monadic_trancl_preemptible f)
 2. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q1) s proof (prove)
goal (2 subgoals):
 1. monadic_rewrite False False ?Q9 (f x >>=E monadic_trancl_preemptible f) (f x >>=E monadic_trancl_preemptible f)
 2. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ((\<lambda>_. True) and (\<lambda>s. True) and ?Q9)) s proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma monadic_trancl_preemptible_return:
  "monadic_rewrite False False (\<lambda>_. True)
     (monadic_trancl_preemptible f x) (returnOk x)" unfolding monadic_trancl_preemptible_def apply (monadic_rewrite_l monadic_trancl_return) apply (fastforce simp: returnOk_def intro!: monadic_rewrite_refl)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite False False (\<lambda>_. True) (monadic_trancl_preemptible f x) (returnOk x) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite False False (\<lambda>_. True) (monadic_trancl (lift f) (Inr x)) (returnOk x) proof (prove)
goal (2 subgoals):
 1. monadic_rewrite False False ?Q1 (return (Inr x)) (returnOk x)
 2. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q1) s proof (prove)
goal:
No subgoals!
theory Finalise_DR

lemma set_cdt_modify:
  "set_cdt c = modify (\<lambda>s. s \<lparr> cdt := c \<rparr>)" by (simp add: set_cdt_def modify_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set_cdt c = modify (cdt_update (\<lambda>_. c))