kings-crown/FVELER_Isabelle huggingface dataset:
theory StateTranslation_D

lemma evalMonad_mapM_loadWord_cong:
  "underlying_memory ms = underlying_memory ms' \<Longrightarrow>
   evalMonad (mapM loadWord xs) ms = evalMonad (mapM loadWord xs) ms'" apply (rule evalMonad_mapM_cong) apply (simp cong: evalMonad_loadWord_cong) apply (wp loadWord_inv) apply (rule df_loadWord) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. underlying_memory ms = underlying_memory ms' \<Longrightarrow> evalMonad (mapM loadWord xs) ms = evalMonad (mapM loadWord xs) ms' proof (prove)
goal (3 subgoals):
 1. \<And>x. underlying_memory ms = underlying_memory ms' \<Longrightarrow> evalMonad (loadWord x) ms = evalMonad (loadWord x) ms'
 2. \<And>P x. underlying_memory ms = underlying_memory ms' \<Longrightarrow> \<lbrace>P\<rbrace> loadWord x \<lbrace>\<lambda>_. P\<rbrace>
 3. \<And>x. underlying_memory ms = underlying_memory ms' \<Longrightarrow> det_or_fail (loadWord x) proof (prove)
goal (2 subgoals):
 1. \<And>P x. underlying_memory ms = underlying_memory ms' \<Longrightarrow> \<lbrace>P\<rbrace> loadWord x \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>x. underlying_memory ms = underlying_memory ms' \<Longrightarrow> det_or_fail (loadWord x) proof (prove)
goal (1 subgoal):
 1. \<And>x. underlying_memory ms = underlying_memory ms' \<Longrightarrow> det_or_fail (loadWord x) proof (prove)
goal:
No subgoals!
theory StateTranslation_D

lemma get_tcb_mrs_cong:
  "underlying_memory ms = underlying_memory ms' \<Longrightarrow> get_tcb_mrs ms = get_tcb_mrs ms'" apply (rule ext) apply (simp add: get_tcb_mrs_def Let_def cong: get_ipc_buffer_words_cong) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. underlying_memory ms = underlying_memory ms' \<Longrightarrow> get_tcb_mrs ms = get_tcb_mrs ms' proof (prove)
goal (1 subgoal):
 1. \<And>x. underlying_memory ms = underlying_memory ms' \<Longrightarrow> get_tcb_mrs ms x = get_tcb_mrs ms' x proof (prove)
goal:
No subgoals!
theory StateTranslationProofs_DR

lemma asid_high_bits [simp]:
  "Types_D.asid_high_bits = asid_high_bits" by (simp add:Types_D.asid_high_bits_def asid_high_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Types_D.asid_high_bits = local.asid_high_bits
theory StateTranslationProofs_DR

lemma asid_low_bits [simp]:
  "Types_D.asid_low_bits = asid_low_bits" by (simp add:Types_D.asid_low_bits_def asid_low_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Types_D.asid_low_bits = local.asid_low_bits
theory StateTranslationProofs_DR

lemma asid_bits [simp]:
  "Types_D.asid_bits = asid_bits" by (simp add:Types_D.asid_bits_def asid_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Types_D.asid_bits = local.asid_bits
theory StateTranslationProofs_DR

lemma get_obj_simps [simp]:
  "get_obj (s\<lparr>cur_thread := a\<rparr>) = get_obj s" apply (rule ext) apply (clarsimp simp: get_obj_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. get_obj (s\<lparr>cur_thread := a\<rparr>) = get_obj s proof (prove)
goal (1 subgoal):
 1. \<And>x. get_obj (s\<lparr>cur_thread := a\<rparr>) x = get_obj s x proof (prove)
goal:
No subgoals!
theory StateTranslationProofs_DR

lemma transform_objects_simps [simp]:
  "transform_objects (s\<lparr>cur_thread := a\<rparr>) = transform_objects s" apply (rule ext) apply (clarsimp simp: transform_objects_def transform_object_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transform_objects (s\<lparr>cur_thread := a\<rparr>) = transform_objects s proof (prove)
goal (1 subgoal):
 1. \<And>x. transform_objects (s\<lparr>cur_thread := a\<rparr>) x = transform_objects s x proof (prove)
goal:
No subgoals!
theory StateTranslationProofs_DR

lemma transform_cdt_simps [simp]:
  "transform_cdt (s\<lparr>cur_thread := a\<rparr>) = transform_cdt s" apply (rule ext)+ apply (clarsimp simp: transform_cdt_def split_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transform_cdt (s\<lparr>cur_thread := a\<rparr>) = transform_cdt s proof (prove)
goal (1 subgoal):
 1. \<And>x. transform_cdt (s\<lparr>cur_thread := a\<rparr>) x = transform_cdt s x proof (prove)
goal:
No subgoals!
theory StateTranslationProofs_DR

lemma update_kheap_triv[simp]:
  "kheap s y = Some obj\<Longrightarrow> update_kheap ((kheap s)(y \<mapsto> obj)) s = s" apply (case_tac s,clarsimp) apply (rule ext,clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. kheap s y = Some obj \<Longrightarrow> update_kheap ((kheap s)(y \<mapsto> obj)) s = s proof (prove)
goal (1 subgoal):
 1. \<And>kheap cdt is_original_cap cur_thread idle_thread machine_state interrupt_irq_node interrupt_states arch_state more. \<lbrakk>kheap y = Some obj; s = \<lparr>kheap = kheap, cdt = cdt, is_original_cap = is_original_cap, cur_thread = cur_thread, idle_thread = idle_thread, machine_state = machine_state, interrupt_irq_node = interrupt_irq_node, interrupt_states = interrupt_states, arch_state = arch_state, \<dots> = more\<rparr>\<rbrakk> \<Longrightarrow> kheap(y \<mapsto> obj) = kheap proof (prove)
goal:
No subgoals!
theory StateTranslationProofs_DR

lemma msg_registers_lt_msg_max_length [simp]:
  "length msg_registers < msg_max_length" by (simp add: msg_registers_def msgRegisters_def upto_enum_def
                fromEnum_def enum_register msg_max_length_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length msg_registers < msg_max_length
theory StateTranslationProofs_DR

lemma get_tcb_mrs_update_state :
  "get_tcb_mrs ms (tcb_state_update f tcb) = get_tcb_mrs ms tcb" by (clarsimp simp:get_tcb_mrs_def Suc_le_eq get_tcb_message_info_def get_ipc_buffer_words_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. get_tcb_mrs ms (tcb_state_update f tcb) = get_tcb_mrs ms tcb
theory StateTranslationProofs_DR

lemma badge_cap_register_overlap:
  "badge_register = cap_register" by (clarsimp simp:badge_register_def cap_register_def
                  ARM.badgeRegister_def
                  ARM.capRegister_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. badge_register = cap_register
theory StateTranslationProofs_DR

lemma cap_msg_info_register_no_overlap:
  "cap_register \<noteq> msg_info_register" by (clarsimp simp:msg_info_register_def cap_register_def
                  ARM.msgInfoRegister_def
                  ARM.capRegister_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_register \<noteq> msg_info_register
theory StateTranslationProofs_DR

lemma transform_full_intent_cong:
  "\<lbrakk>ms = ms'; ptr = ptr';
    arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb');
    tcb_ipc_buffer tcb = tcb_ipc_buffer tcb'; tcb_ipcframe tcb = tcb_ipcframe tcb'\<rbrakk>
  \<Longrightarrow> transform_full_intent ms ptr tcb = transform_full_intent ms' ptr' tcb'" by (simp add: transform_full_intent_def get_tcb_message_info_def get_tcb_mrs_def Suc_le_eq get_ipc_buffer_words_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ms = ms'; ptr = ptr'; arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb'); tcb_ipc_buffer tcb = tcb_ipc_buffer tcb'; tcb_ipcframe tcb = tcb_ipcframe tcb'\<rbrakk> \<Longrightarrow> transform_full_intent ms ptr tcb = transform_full_intent ms' ptr' tcb'
theory StateTranslationProofs_DR

lemma caps_of_state_eq_lift:
  "\<forall>cap. cte_wp_at ((=) cap) p s = cte_wp_at ((=) cap) p s' \<Longrightarrow>  caps_of_state s p = caps_of_state s' p" apply (simp add:cte_wp_at_def caps_of_state_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>cap. cte_wp_at ((=) cap) p s = cte_wp_at ((=) cap) p s' \<Longrightarrow> caps_of_state s p = caps_of_state s' p proof (prove)
goal:
No subgoals!
theory StateTranslationProofs_DR

lemma caps_of_state_irrelavent_simp:
  "ref \<noteq> epptr \<Longrightarrow> caps_of_state (update_kheap (kh(epptr \<mapsto> obj)) s) (ref, cref) = caps_of_state (update_kheap kh s) (ref, cref)" apply (rule caps_of_state_eq_lift) apply (clarsimp simp: cte_wp_at_cases) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ref \<noteq> epptr \<Longrightarrow> caps_of_state (update_kheap (kh(epptr \<mapsto> obj)) s) (ref, cref) = caps_of_state (update_kheap kh s) (ref, cref) proof (prove)
goal (1 subgoal):
 1. ref \<noteq> epptr \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) (ref, cref) (update_kheap (kh(epptr \<mapsto> obj)) s) = cte_wp_at ((=) cap) (ref, cref) (update_kheap kh s) proof (prove)
goal:
No subgoals!
theory StateTranslationProofs_DR

lemma caps_of_state_update_same_caps:
  assumes kh: "kh ptr = Some ko"
  and    coo: "caps_of_object ko' = caps_of_object ko"
  shows  "caps_of_state (update_kheap (kh(ptr \<mapsto> ko')) s) = caps_of_state (update_kheap kh s)" using kh coo apply - apply (rule ext) apply (clarsimp simp add: caps_of_state_def2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_of_state (update_kheap (kh(ptr \<mapsto> ko')) s) = caps_of_state (update_kheap kh s) proof (prove)
using this:
kh ptr = Some ko
caps_of_object ko' = caps_of_object ko

goal (1 subgoal):
 1. caps_of_state (update_kheap (kh(ptr \<mapsto> ko')) s) = caps_of_state (update_kheap kh s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kh ptr = Some ko; caps_of_object ko' = caps_of_object ko\<rbrakk> \<Longrightarrow> caps_of_state (update_kheap (kh(ptr \<mapsto> ko')) s) = caps_of_state (update_kheap kh s) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>kh ptr = Some ko; caps_of_object ko' = caps_of_object ko\<rbrakk> \<Longrightarrow> caps_of_state (update_kheap (kh(ptr \<mapsto> ko')) s) x = caps_of_state (update_kheap kh s) x proof (prove)
goal:
No subgoals!
theory StateTranslationProofs_DR

lemma caps_of_state_update_tcb:
  "\<lbrakk> kh thread = Some (TCB tcb);
     (tcb_ctable tcb) =  (tcb_ctable (f tcb));
     (tcb_vtable tcb) =  (tcb_vtable (f tcb));
     (tcb_reply tcb) =  (tcb_reply (f tcb));
     (tcb_caller tcb) =  (tcb_caller (f tcb));
     (tcb_ipcframe tcb) =  (tcb_ipcframe (f tcb)) \<rbrakk>
    \<Longrightarrow>
      caps_of_state (update_kheap (kh(thread \<mapsto> (TCB (f tcb)))) s) =
      caps_of_state (update_kheap kh s)" apply (erule caps_of_state_update_same_caps) apply (rule ext) apply (simp add: tcb_cap_cases_def split: if_split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kh thread = Some (TCB tcb); tcb_ctable tcb = tcb_ctable (f tcb); tcb_vtable tcb = tcb_vtable (f tcb); tcb_reply tcb = tcb_reply (f tcb); tcb_caller tcb = tcb_caller (f tcb); tcb_ipcframe tcb = tcb_ipcframe (f tcb)\<rbrakk> \<Longrightarrow> caps_of_state (update_kheap (kh(thread \<mapsto> TCB (f tcb))) s) = caps_of_state (update_kheap kh s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_ctable tcb = tcb_ctable (f tcb); tcb_vtable tcb = tcb_vtable (f tcb); tcb_reply tcb = tcb_reply (f tcb); tcb_caller tcb = tcb_caller (f tcb); tcb_ipcframe tcb = tcb_ipcframe (f tcb)\<rbrakk> \<Longrightarrow> caps_of_object (TCB (f tcb)) = caps_of_object (TCB tcb) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>tcb_ctable tcb = tcb_ctable (f tcb); tcb_vtable tcb = tcb_vtable (f tcb); tcb_reply tcb = tcb_reply (f tcb); tcb_caller tcb = tcb_caller (f tcb); tcb_ipcframe tcb = tcb_ipcframe (f tcb)\<rbrakk> \<Longrightarrow> caps_of_object (TCB (f tcb)) x = caps_of_object (TCB tcb) x proof (prove)
goal:
No subgoals!
theory StateTranslationProofs_DR

lemma transform_cdt_kheap_update [simp]:
  "transform_cdt (kheap_update f s) = transform_cdt s" by (clarsimp simp: transform_cdt_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transform_cdt (kheap_update f s) = transform_cdt s
theory StateTranslationProofs_DR

lemma transform_cdt_update_original_cap [simp]:
  "transform_cdt (b\<lparr>is_original_cap := x\<rparr>) = transform_cdt b" by (clarsimp simp: transform_cdt_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transform_cdt (b\<lparr>is_original_cap := x\<rparr>) = transform_cdt b
theory StateTranslationProofs_DR

lemma transform_asid_table_kheap_update [simp]:
  "transform_asid_table (kheap_update f s) = transform_asid_table s" by (clarsimp simp: transform_asid_table_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transform_asid_table (kheap_update f s) = transform_asid_table s
theory StateTranslationProofs_DR

lemma transform_asid_table_update_original_cap [simp]:
  "transform_asid_table (b\<lparr>is_original_cap := x\<rparr>) = transform_asid_table b" by (clarsimp simp: transform_asid_table_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. transform_asid_table (b\<lparr>is_original_cap := x\<rparr>) = transform_asid_table b
theory StateTranslationProofs_DR

lemma transform_objects_update_same:
  "\<lbrakk> kheap s ptr = Some ko; transform_object (machine_state s) ptr (ekheap s ptr) ko = ko'; ptr \<noteq> idle_thread s \<rbrakk>
  \<Longrightarrow> (transform_objects s)(ptr \<mapsto> ko') = transform_objects s" unfolding transform_objects_def by (rule ext) (simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s ptr = Some ko; transform_object (machine_state s) ptr (ekheap s ptr) ko = ko'; ptr \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> (transform_objects s)(ptr \<mapsto> ko') = transform_objects s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s ptr = Some ko; transform_object (machine_state s) ptr (ekheap s ptr) ko = ko'; ptr \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> ((\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr)) ((kheap s |` (- {idle_thread s})) ptr)))(ptr \<mapsto> ko') = (\<lambda>ptr. Some cdl_object.Untyped) |` (- {idle_thread s}) ++ (\<lambda>ptr. map_option (transform_object (machine_state s) ptr ((ekheap s |` (- {idle_thread s})) ptr)) ((kheap s |` (- {idle_thread s})) ptr))
theory StateTranslationProofs_DR

lemma map_lift_over_eq_Some:
  "(map_lift_over f m x = Some y)
         = (\<exists>x' y'. x = f x' \<and> y = f y' \<and> inj_on f (dom m \<union> ran m)
                   \<and> m x' = Some y')" proof - have P: "inj_on f (dom m \<union> ran m) \<longrightarrow> inj_on f (dom m)" by (auto elim: subset_inj_on) have Q: "\<And>x y. \<lbrakk> m x = Some y; inj_on f (dom m \<union> ran m) \<rbrakk>
                  \<Longrightarrow> inv_into (dom m) f (f x) = x" using P by (blast intro: inv_into_f_f) show ?thesis by (auto simp add: map_lift_over_def Q) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (map_lift_over f m x = Some y) = (\<exists>x' y'. x = f x' \<and> y = f y' \<and> inj_on f (dom m \<union> ran m) \<and> m x' = Some y') proof (state)
goal (1 subgoal):
 1. (map_lift_over f m x = Some y) = (\<exists>x' y'. x = f x' \<and> y = f y' \<and> inj_on f (dom m \<union> ran m) \<and> m x' = Some y') proof (prove)
goal (1 subgoal):
 1. inj_on f (dom m \<union> ran m) \<longrightarrow> inj_on f (dom m) proof (state)
this:
inj_on f (dom m \<union> ran m) \<longrightarrow> inj_on f (dom m)

goal (1 subgoal):
 1. (map_lift_over f m x = Some y) = (\<exists>x' y'. x = f x' \<and> y = f y' \<and> inj_on f (dom m \<union> ran m) \<and> m x' = Some y') proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>m x = Some y; inj_on f (dom m \<union> ran m)\<rbrakk> \<Longrightarrow> inv_into (dom m) f (f x) = x proof (prove)
using this:
inj_on f (dom m \<union> ran m) \<longrightarrow> inj_on f (dom m)

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>m x = Some y; inj_on f (dom m \<union> ran m)\<rbrakk> \<Longrightarrow> inv_into (dom m) f (f x) = x proof (state)
this:
\<lbrakk>m ?x = Some ?y; inj_on f (dom m \<union> ran m)\<rbrakk> \<Longrightarrow> inv_into (dom m) f (f ?x) = ?x

goal (1 subgoal):
 1. (map_lift_over f m x = Some y) = (\<exists>x' y'. x = f x' \<and> y = f y' \<and> inj_on f (dom m \<union> ran m) \<and> m x' = Some y') proof (prove)
goal (1 subgoal):
 1. (map_lift_over f m x = Some y) = (\<exists>x' y'. x = f x' \<and> y = f y' \<and> inj_on f (dom m \<union> ran m) \<and> m x' = Some y') proof (state)
this:
(map_lift_over f m x = Some y) = (\<exists>x' y'. x = f x' \<and> y = f y' \<and> inj_on f (dom m \<union> ran m) \<and> m x' = Some y')

goal:
No subgoals!
theory StateTranslationProofs_DR

lemma map_lift_over_eq_None:
  "(map_lift_over f m x = None)
         = (inj_on f (dom m \<union> ran m) \<longrightarrow>
                (\<forall>x'. x = f x' \<longrightarrow> m x' = None))" proof - have P: "inj_on f (dom m \<union> ran m) \<Longrightarrow> inj_on f (dom m)" by (auto elim: subset_inj_on) show ?thesis by (auto simp add: map_lift_over_def P[THEN inv_into_f_f] domI
                       inj_on_eq_iff[where f=f]
           | rule ccontr[where P="v = None" for v])+ qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (map_lift_over f m x = None) = (inj_on f (dom m \<union> ran m) \<longrightarrow> (\<forall>x'. x = f x' \<longrightarrow> m x' = None)) proof (state)
goal (1 subgoal):
 1. (map_lift_over f m x = None) = (inj_on f (dom m \<union> ran m) \<longrightarrow> (\<forall>x'. x = f x' \<longrightarrow> m x' = None)) proof (prove)
goal (1 subgoal):
 1. inj_on f (dom m \<union> ran m) \<Longrightarrow> inj_on f (dom m) proof (state)
this:
inj_on f (dom m \<union> ran m) \<Longrightarrow> inj_on f (dom m)

goal (1 subgoal):
 1. (map_lift_over f m x = None) = (inj_on f (dom m \<union> ran m) \<longrightarrow> (\<forall>x'. x = f x' \<longrightarrow> m x' = None)) proof (prove)
goal (1 subgoal):
 1. (map_lift_over f m x = None) = (inj_on f (dom m \<union> ran m) \<longrightarrow> (\<forall>x'. x = f x' \<longrightarrow> m x' = None)) proof (state)
this:
(map_lift_over f m x = None) = (inj_on f (dom m \<union> ran m) \<longrightarrow> (\<forall>x'. x = f x' \<longrightarrow> m x' = None))

goal:
No subgoals!
theory StateTranslationProofs_DR

lemma map_lift_over_f_eq:
  "inj_on f ({x} \<union> dom m \<union> ran m) \<Longrightarrow>
   (map_lift_over f m (f x) = v) = (v = map_option f (m x))" apply (cases v, simp_all add: map_lift_over_eq_None map_lift_over_eq_Some) apply (auto simp: option_map_def split: option.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. inj_on f ({x} \<union> dom m \<union> ran m) \<Longrightarrow> (map_lift_over f m (f x) = v) = (v = map_option f (m x)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>inj_on f (dom m \<union> ran m) \<and> f x \<notin> f ` (dom m \<union> ran m - {x}); v = None\<rbrakk> \<Longrightarrow> (\<forall>x'. f x = f x' \<longrightarrow> m x' = None) = (m x = None)
 2. \<And>a. \<lbrakk>inj_on f (dom m \<union> ran m) \<and> f x \<notin> f ` (dom m \<union> ran m - {x}); v = Some a\<rbrakk> \<Longrightarrow> (\<exists>x'. f x = f x' \<and> (\<exists>y'. a = f y' \<and> m x' = Some y')) = (Some a = map_option f (m x)) proof (prove)
goal:
No subgoals!
theory StateTranslationProofs_DR

lemma map_lift_over_eq_cases[unfolded map_lift_over_eq_None map_lift_over_eq_Some]:
  "(map_lift_over f m x = v)
       = (case v of None \<Rightarrow> map_lift_over f m x = None
                | Some z \<Rightarrow> map_lift_over f m x = Some z)" by (simp split: option.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (map_lift_over f m x = v) = (case v of None \<Rightarrow> map_lift_over f m x = None | Some z \<Rightarrow> map_lift_over f m x = Some z)
theory StateTranslationProofs_DR

lemma map_lift_over_if_eq:
  assumes inj_f: "inj_on f (dom m \<union> ran m \<union> {y} \<union> set_option z)"
  shows
  "map_lift_over f (\<lambda>x. if m x = Some y then z else m x)
       = (\<lambda>x. if map_lift_over f m x = Some (f y) then map_option f z
              else map_lift_over f m x)" using inj_f map_lift_over_if_eq_twice[where f=f and m=m and y=y and z=z and y'=y and z'=z] apply (simp del: inj_on_insert) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map_lift_over f (\<lambda>x. if m x = Some y then z else m x) = (\<lambda>x. if map_lift_over f m x = Some (f y) then map_option f z else map_lift_over f m x) proof (prove)
using this:
inj_on f (dom m \<union> ran m \<union> {y} \<union> set_option z)
inj_on f (dom m \<union> ran m \<union> {y, y} \<union> set_option z \<union> set_option z) \<Longrightarrow> map_lift_over f (\<lambda>x. if m x = Some y then z else if m x = Some y then z else m x) = (\<lambda>x. if map_lift_over f m x = Some (f y) then map_option f z else if map_lift_over f m x = Some (f y) then map_option f z else map_lift_over f m x)

goal (1 subgoal):
 1. map_lift_over f (\<lambda>x. if m x = Some y then z else m x) = (\<lambda>x. if map_lift_over f m x = Some (f y) then map_option f z else map_lift_over f m x) proof (prove)
goal:
No subgoals!
theory Corres_D

lemma truncate_state_unit[simp]: "truncate_state s = s" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. truncate_state s = s
theory Corres_D

lemma select_ext_select[simp]: "select_ext a S = (select S :: ('b, unit) s_monad)" by (rule ext)
     (auto simp: select_ext_def select_switch_unit_def assert_def get_def select_def
                 return_def bind_def fail_def image_def
          split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. select_ext a S = select S
theory Corres_D

lemma OR_choice_OR[simp]: "(OR_choice c (f :: ('a,unit) s_monad) g) = (f \<sqinter> g)" apply (rule ext, rename_tac s) apply (clarsimp simp: OR_choice_def alternative_def get_def select_def return_def bind_def
                        select_f_def mk_ef_def wrap_ext_unit_def wrap_ext_bool_unit_def image_def
                 split: if_split_asm) apply (case_tac "f s") apply (case_tac "g s") by (intro conjI set_eqI; clarsimp?; blast)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. OR_choice c f g = (f \<sqinter> g) proof (prove)
goal (1 subgoal):
 1. \<And>s. OR_choice c f g s = (f \<sqinter> g) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<Union> {y. \<exists>b x. (x \<longrightarrow> (y, b) = f s) \<and> (\<not> x \<longrightarrow> (y, b) = g s)} = fst (f s) \<union> fst (g s) \<and> (\<exists>a x. (x \<longrightarrow> (a, True) = f s) \<and> (\<not> x \<longrightarrow> (a, True) = g s)) = (snd (f s) \<or> snd (g s)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. f s = (a, b) \<Longrightarrow> \<Union> {y. \<exists>b x. (x \<longrightarrow> (y, b) = f s) \<and> (\<not> x \<longrightarrow> (y, b) = g s)} = fst (f s) \<union> fst (g s) \<and> (\<exists>a x. (x \<longrightarrow> (a, True) = f s) \<and> (\<not> x \<longrightarrow> (a, True) = g s)) = (snd (f s) \<or> snd (g s)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b aa ba. \<lbrakk>f s = (a, b); g s = (aa, ba)\<rbrakk> \<Longrightarrow> \<Union> {y. \<exists>b x. (x \<longrightarrow> (y, b) = f s) \<and> (\<not> x \<longrightarrow> (y, b) = g s)} = fst (f s) \<union> fst (g s) \<and> (\<exists>a x. (x \<longrightarrow> (a, True) = f s) \<and> (\<not> x \<longrightarrow> (a, True) = g s)) = (snd (f s) \<or> snd (g s))