kings-crown/FVELER_Isabelle huggingface dataset:
theory Refine_C

lemma monadic_rewrite_\<Gamma>:
  "monadic_rewrite True False \<top>
    (exec_C \<Gamma> c)
    (exec_C (kernel_all_global_addresses.\<Gamma> symbol_table) c)" using spec_refine [of symbol_table domain] using spec_simulates_to_exec_simulates apply (clarsimp simp: spec_statefn_simulates_via_statefn
                        o_def map_option_case monadic_rewrite_def exec_C_def
                   split: option.splits
                   cong: option.case_cong) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True False (\<lambda>_. True) (exec_C \<Gamma> c) (exec_C (kernel_all_global_addresses.\<Gamma> symbol_table) c) proof (prove)
using this:
spec_statefn_simulates id (kernel_all_global_addresses.\<Gamma> symbol_table) \<Gamma>

goal (1 subgoal):
 1. monadic_rewrite True False (\<lambda>_. True) (exec_C \<Gamma> c) (exec_C (kernel_all_global_addresses.\<Gamma> symbol_table) c) proof (prove)
using this:
spec_statefn_simulates id (kernel_all_global_addresses.\<Gamma> symbol_table) \<Gamma>
\<lbrakk>?G\<turnstile> \<langle>?a,?xs\<rangle> \<Rightarrow> ?t; spec_simulates ?G ?G'\<rbrakk> \<Longrightarrow> ?G'\<turnstile> \<langle>?a,?xs\<rangle> \<Rightarrow> ?t \<or> (\<exists>ft. ?G'\<turnstile> \<langle>?a,?xs\<rangle> \<Rightarrow> Fault ft)

goal (1 subgoal):
 1. monadic_rewrite True False (\<lambda>_. True) (exec_C \<Gamma> c) (exec_C (kernel_all_global_addresses.\<Gamma> symbol_table) c) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>spec_simulates (kernel_all_global_addresses.\<Gamma> symbol_table) \<Gamma>; \<And>G a xs t G'. \<lbrakk>G\<turnstile> \<langle>a,xs\<rangle> \<Rightarrow> t; spec_simulates G G'\<rbrakk> \<Longrightarrow> G'\<turnstile> \<langle>a,xs\<rangle> \<Rightarrow> t \<or> (\<exists>ft. G'\<turnstile> \<langle>a,xs\<rangle> \<Rightarrow> Fault ft); \<forall>xs. xs \<in> range Normal \<or> \<not> \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> xs\<rbrakk> \<Longrightarrow> {()} \<times> {s'. kernel_all_global_addresses.\<Gamma> symbol_table\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Normal s'} \<subseteq> {()} \<times> {s'. \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Normal s'} \<and> ((\<exists>xs. xs \<notin> range Normal \<and> kernel_all_global_addresses.\<Gamma> symbol_table\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> xs) \<longrightarrow> (\<exists>xs. xs \<notin> range Normal \<and> \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> xs)) proof (prove)
goal:
No subgoals!
theory Refine_C

theorem true_refinement:
  "kernel_global.ADT_C symbol_table armKSKernelVSpace_C uop
   \<sqsubseteq> ADT_H uop" apply (rule refinement_trans[OF _ refinement2]) apply (simp add: kernel_global.ADT_C_def ADT_C_def) apply (rule sim_imp_refines) apply (clarsimp simp: fw_simulates_def) apply (rule_tac x=Id in exI) using kernel_all_subset_kernel apply (simp add: fw_sim_def rel_semi_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. kernel_global.ADT_C symbol_table armKSKernelVSpace_C uop \<sqsubseteq> ADT_H uop proof (prove)
goal (1 subgoal):
 1. kernel_global.ADT_C symbol_table armKSKernelVSpace_C uop \<sqsubseteq> ADT_C uop proof (prove)
goal (1 subgoal):
 1. \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton (kernel_global.check_active_irq_C symbol_table) (do_user_op_C uop) (kernel_global.kernel_call_C symbol_table False)\<rparr> \<sqsubseteq> \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C False)\<rparr> proof (prove)
goal (1 subgoal):
 1. \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton (kernel_global.check_active_irq_C symbol_table) (do_user_op_C uop) (kernel_global.kernel_call_C symbol_table False)\<rparr> \<sqsubseteq>\<^sub>F \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C False)\<rparr> proof (prove)
goal (1 subgoal):
 1. \<exists>R. fw_sim R \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton (kernel_global.check_active_irq_C symbol_table) (do_user_op_C uop) (kernel_global.kernel_call_C symbol_table False)\<rparr> \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C False)\<rparr> proof (prove)
goal (1 subgoal):
 1. fw_sim Id \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton (kernel_global.check_active_irq_C symbol_table) (do_user_op_C uop) (kernel_global.kernel_call_C symbol_table False)\<rparr> \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C False)\<rparr> proof (prove)
using this:
global_automaton (kernel_global.check_active_irq_C symbol_table) (do_user_op_C ?uop) (kernel_global.kernel_call_C symbol_table ?fp) \<subseteq> global_automaton check_active_irq_C (do_user_op_C ?uop) (kernel_call_C ?fp)

goal (1 subgoal):
 1. fw_sim Id \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton (kernel_global.check_active_irq_C symbol_table) (do_user_op_C uop) (kernel_global.kernel_call_C symbol_table False)\<rparr> \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C False)\<rparr> proof (prove)
goal:
No subgoals!
theory Refine_C

theorem true_fp_refinement:
  "kernel_global.ADT_FP_C symbol_table armKSKernelVSpace_C uop
   \<sqsubseteq> ADT_H uop" apply (rule refinement_trans[OF _ fp_refinement]) apply (simp add: kernel_global.ADT_FP_C_def ADT_FP_C_def) apply (rule sim_imp_refines) apply (clarsimp simp: fw_simulates_def) apply (rule_tac x=Id in exI) using kernel_all_subset_kernel apply (simp add: fw_sim_def rel_semi_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. kernel_global.ADT_FP_C symbol_table armKSKernelVSpace_C uop \<sqsubseteq> ADT_H uop proof (prove)
goal (1 subgoal):
 1. kernel_global.ADT_FP_C symbol_table armKSKernelVSpace_C uop \<sqsubseteq> ADT_FP_C uop proof (prove)
goal (1 subgoal):
 1. \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton (kernel_global.check_active_irq_C symbol_table) (do_user_op_C uop) (kernel_global.kernel_call_C symbol_table True)\<rparr> \<sqsubseteq> \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C True)\<rparr> proof (prove)
goal (1 subgoal):
 1. \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton (kernel_global.check_active_irq_C symbol_table) (do_user_op_C uop) (kernel_global.kernel_call_C symbol_table True)\<rparr> \<sqsubseteq>\<^sub>F \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C True)\<rparr> proof (prove)
goal (1 subgoal):
 1. \<exists>R. fw_sim R \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton (kernel_global.check_active_irq_C symbol_table) (do_user_op_C uop) (kernel_global.kernel_call_C symbol_table True)\<rparr> \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C True)\<rparr> proof (prove)
goal (1 subgoal):
 1. fw_sim Id \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton (kernel_global.check_active_irq_C symbol_table) (do_user_op_C uop) (kernel_global.kernel_call_C symbol_table True)\<rparr> \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C True)\<rparr> proof (prove)
using this:
global_automaton (kernel_global.check_active_irq_C symbol_table) (do_user_op_C ?uop) (kernel_global.kernel_call_C symbol_table ?fp) \<subseteq> global_automaton check_active_irq_C (do_user_op_C ?uop) (kernel_call_C ?fp)

goal (1 subgoal):
 1. fw_sim Id \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton (kernel_global.check_active_irq_C symbol_table) (do_user_op_C uop) (kernel_global.kernel_call_C symbol_table True)\<rparr> \<lparr>Init = Init_C, Fin = Fin_C, Step = \<lambda>u. global_automaton check_active_irq_C (do_user_op_C uop) (kernel_call_C True)\<rparr> proof (prove)
goal:
No subgoals!
theory MoreHOL

lemma tuple_relation_to_function [simp]: "((a, b) \<in> {(s, s'). f s' = s}) = (a = f b)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((a, b) \<in> {(s, s'). f s' = s}) = (a = f b)
theory MoreCorres

lemma corres_select_equiv:
  "\<lbrakk> \<forall>a' \<in> A'. \<exists>a \<in> A. r a a' \<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r \<top> \<top> (select A) (select A')" apply (clarsimp simp: corres_underlying_def) apply (clarsimp simp: split_def) apply (clarsimp simp: select_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>a'\<in>A'. \<exists>a\<in>A. r a a' \<Longrightarrow> corres_underlying sr nf nf' r (\<lambda>_. True) (\<lambda>_. True) (select A) (select A') proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>a'\<in>A'. \<exists>a\<in>A. r a a'; (a, b) \<in> sr; nf \<longrightarrow> \<not> snd (select A a)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst (select A' b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (select A a). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (select A' b)) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>a'\<in>A'. \<exists>a\<in>A. r a a'; (a, b) \<in> sr; nf \<longrightarrow> \<not> snd (select A a)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst (select A' b). \<exists>xa\<in>fst (select A a). (snd xa, snd x) \<in> sr \<and> r (fst xa) (fst x)) \<and> (nf' \<longrightarrow> \<not> snd (select A' b)) proof (prove)
goal:
No subgoals!
theory MoreCorres

lemma corres_if_rhs:
  "\<lbrakk>  G \<Longrightarrow> corres_underlying sr nf nf' rvr P  Q  a b;
     \<not>G \<Longrightarrow> corres_underlying sr nf nf' rvr P' Q' a c \<rbrakk> \<Longrightarrow>
   corres_underlying sr nf nf' rvr
       (\<lambda>s. (G \<longrightarrow> P s) \<and> (\<not>G \<longrightarrow> P' s)) (\<lambda>s. (G \<longrightarrow> Q s) \<and> (\<not>G \<longrightarrow> Q' s))
       a (if G then b else c)" by (auto elim: corres_guard_imp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>G \<Longrightarrow> corres_underlying sr nf nf' rvr P Q a b; \<not> G \<Longrightarrow> corres_underlying sr nf nf' rvr P' Q' a c\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' rvr (\<lambda>s. (G \<longrightarrow> P s) \<and> (\<not> G \<longrightarrow> P' s)) (\<lambda>s. (G \<longrightarrow> Q s) \<and> (\<not> G \<longrightarrow> Q' s)) a (if G then b else c)
theory MoreCorres

lemma alternative_bind_distrib: "((f \<sqinter> g) >>= h) = ((f >>= h) \<sqinter> (g >>= h))" apply (auto simp: alternative_def bind_def split_def intro!: prod_eqI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (f \<sqinter> g) >>= h = (f >>= h \<sqinter> g >>= h) proof (prove)
goal:
No subgoals!
theory MoreCorres

lemma alternative_bind_distrib_2: "(do f; (a \<sqinter> b) od) = ((do f; a od) \<sqinter> (do f; b od))" apply (auto simp: alternative_def bind_def split_def intro!: prod_eqI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do f;
a \<sqinter> b
od = (do f;
a
od \<sqinter> do f;
b
od) proof (prove)
goal:
No subgoals!
theory MoreCorres

lemma alternative_bindE_distrib: "((f \<sqinter> g) >>=E h) = ((f >>=E h) \<sqinter> (g >>=E h))" by (simp add: bindE_def alternative_bind_distrib)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (f \<sqinter> g) >>=E h = (f >>=E h \<sqinter> g >>=E h)
theory MoreCorres

lemma corres_return_dc [simp]:
  "corres_underlying sr nf nf' dc \<top> \<top> (return a) (return b)" apply (clarsimp simp: corres_underlying_def dc_def return_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' dc (\<lambda>_. True) (\<lambda>_. True) (return a) (return b) proof (prove)
goal:
No subgoals!
theory MoreCorres

lemma corres_return_dc_rhs:
  "corres_underlying sr nf nf' dc G G' P P' \<Longrightarrow> corres_underlying sr nf nf' dc G G' P (do P'; return a od)" by (fastforce simp: corres_underlying_def dc_def return_def bind_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' dc G G' P P' \<Longrightarrow> corres_underlying sr nf nf' dc G G' P (do P';
return a
od)
theory MoreCorres

lemma corres_return_dc_lhs:
  "corres_underlying sr nf nf' dc G G' P P'
    \<Longrightarrow> corres_underlying sr nf nf' dc G G' (do P; return a od) P'" by (simp add: liftM_def[symmetric])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' dc G G' P P' \<Longrightarrow> corres_underlying sr nf nf' dc G G' (do P;
return a
od) P'
theory MoreCorres

lemma liftE_distrib: "(liftE (A >>= (\<lambda>_. B))) = ((liftE A) >>=E (\<lambda>x. (liftE B)))" apply (clarsimp simp: liftE_def bindE_def) apply (subst bind_assoc)+ apply (clarsimp simp: bind_def lift_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. liftE (do _ <- A;
B
od) = doE x <- liftE A;
liftE B
odE proof (prove)
goal (1 subgoal):
 1. do r <- do _ <- A;
B
od;
return (Inr r)
od = do r <- A;
r <- B;
return (Inr r)
od proof (prove)
goal (1 subgoal):
 1. do x <- A;
r <- B;
return (Inr r)
od = do r <- A;
r <- B;
return (Inr r)
od proof (prove)
goal:
No subgoals!
theory MoreCorres

lemma liftE_alternative_distrib: "(liftE (a \<sqinter> b)) = ((liftE a) \<sqinter> (liftE b))" by (metis alternative_bind_distrib bindE_returnOk liftE_bindE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. liftE (a \<sqinter> b) = (liftE a \<sqinter> liftE b)
theory MoreCorres

lemma corres_skip_catch:
  "corres_underlying sr nf nf' dc P P' f g \<Longrightarrow>
   corres_underlying sr nf nf' dc P P' f (g <catch> (\<lambda>_. return x))" by (clarsimp simp: corres_underlying_def catch_def return_def bind_def
                     split_def
               split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' dc P P' f g \<Longrightarrow> corres_underlying sr nf nf' dc P P' f (g <catch> (\<lambda>_. return x))
theory Lemmas_D

lemma nonempty_pick_in:
  "a \<noteq> {} \<Longrightarrow> pick a \<in> a" by (metis all_not_in_conv someI_ex)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a \<noteq> {} \<Longrightarrow> pick a \<in> a
theory Lemmas_D

lemma pick_singleton[simp]:
  "pick {a} = a" apply (rule ccontr) apply (cut_tac nonempty_pick_in) apply fastforce apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pick {a} = a proof (prove)
goal (1 subgoal):
 1. pick {a} \<noteq> a \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pick {a} \<noteq> a; pick ?a3 \<in> ?a3\<rbrakk> \<Longrightarrow> False
 2. pick {a} \<noteq> a \<Longrightarrow> ?a3 \<noteq> {} proof (prove)
goal (1 subgoal):
 1. pick {a} \<noteq> a \<Longrightarrow> ?a3 \<noteq> {} proof (prove)
goal:
No subgoals!
theory Lemmas_D

lemma is_tcb_TCB[simp]: "is_tcb (TCB t)" by (simp add: is_tcb)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_tcb (TCB t)
theory StateTranslation_D

lemma transform_cnode_index_and_depth_success:
       "(\<exists>ci. Some (C ci) =
            map_option C
             (transform_cnode_index_and_depth C2 args)) =
       (\<not> length args < 2)" apply(rule iffI) apply(unfold option_map_def transform_cnode_index_and_depth_def) apply(case_tac args) apply(auto split: list.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<exists>ci. Some (C ci) = map_option C (transform_cnode_index_and_depth C2 args)) = (\<not> length args < 2) proof (prove)
goal (2 subgoals):
 1. \<exists>ci. Some (C ci) = map_option C (transform_cnode_index_and_depth C2 args) \<Longrightarrow> \<not> length args < 2
 2. \<not> length args < 2 \<Longrightarrow> \<exists>ci. Some (C ci) = map_option C (transform_cnode_index_and_depth C2 args) proof (prove)
goal (2 subgoals):
 1. \<exists>ci. Some (C ci) = (case case args of [] \<Rightarrow> None | [index] \<Rightarrow> None | index # depth # xa \<Rightarrow> Some (C2 index depth) of None \<Rightarrow> None | Some x \<Rightarrow> Some (C x)) \<Longrightarrow> \<not> length args < 2
 2. \<not> length args < 2 \<Longrightarrow> \<exists>ci. Some (C ci) = (case case args of [] \<Rightarrow> None | [index] \<Rightarrow> None | index # depth # xa \<Rightarrow> Some (C2 index depth) of None \<Rightarrow> None | Some x \<Rightarrow> Some (C x)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<exists>ci. Some (C ci) = (case case args of [] \<Rightarrow> None | [index] \<Rightarrow> None | index # depth # xa \<Rightarrow> Some (C2 index depth) of None \<Rightarrow> None | Some x \<Rightarrow> Some (C x)); args = []\<rbrakk> \<Longrightarrow> \<not> length args < 2
 2. \<And>a list. \<lbrakk>\<exists>ci. Some (C ci) = (case case args of [] \<Rightarrow> None | [index] \<Rightarrow> None | index # depth # xa \<Rightarrow> Some (C2 index depth) of None \<Rightarrow> None | Some x \<Rightarrow> Some (C x)); args = a # list\<rbrakk> \<Longrightarrow> \<not> length args < 2
 3. \<not> length args < 2 \<Longrightarrow> \<exists>ci. Some (C ci) = (case case args of [] \<Rightarrow> None | [index] \<Rightarrow> None | index # depth # xa \<Rightarrow> Some (C2 index depth) of None \<Rightarrow> None | Some x \<Rightarrow> Some (C x)) proof (prove)
goal:
No subgoals!
theory StateTranslation_D

lemma unat_map_unat [simp]: "(unat_map p) (unat x) = p x" by (clarsimp simp: unat_map_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat_map p (unat x) = p x
theory StateTranslation_D

lemma nat_to_bl_id [simp]: "nat_to_bl (size (x :: (('a::len) word))) (unat x) = Some (to_bl x)" by (clarsimp simp: nat_to_bl_def to_bl_def le_def word_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. nat_to_bl (size x) (unat x) = Some (to_bl x)
theory StateTranslation_D

lemma invocation_type0:
  "invocation_type 0 = GenInvocationLabel InvalidInvocation" by (clarsimp simp: invocation_type_def toEnum_def enum_invocation_label enum_gen_invocation_labels)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invocation_type 0 = GenInvocationLabel InvalidInvocation
theory StateTranslation_D

lemma evalMonad_return [simp]:
  "evalMonad (return x) s = Some x" by (simp add: evalMonad_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. evalMonad (return x) s = Some x
theory StateTranslation_D

lemma bind_dfI:
  "\<lbrakk> det_or_fail f; \<And>x. det_or_fail (g x) \<rbrakk> \<Longrightarrow> det_or_fail (f >>= g)" apply (auto simp: det_or_fail_def bind_def split_def) apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>det_or_fail f; \<And>x. det_or_fail (g x)\<rbrakk> \<Longrightarrow> det_or_fail (f >>= g) proof (prove)
goal (1 subgoal):
 1. \<And>s a b aa ba. \<lbrakk>\<forall>s. fst (f s) = {} \<or> (\<exists>a b. fst (f s) = {(a, b)}); \<And>x. \<forall>s. fst (g x s) = {} \<or> (\<exists>a b. fst (g x s) = {(a, b)}); \<forall>a b. (\<Union>x\<in>fst (f s). fst (g (fst x) (snd x))) \<noteq> {(a, b)}; (a, b) \<in> fst (f s); (aa, ba) \<in> fst (g a b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory StateTranslation_D

lemma return_df:
  "det_or_fail (return x)" by (simp add: det_or_fail_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det_or_fail (return x)
theory StateTranslation_D

lemma assert_df:
  "det_or_fail (assert P)" by (simp add: assert_def fail_def det_or_fail_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det_or_fail (assert P)
theory StateTranslation_D

lemma mapM_df:
  "(\<And>x. det_or_fail (f x)) \<Longrightarrow> det_or_fail (mapM f xs)" apply (induct xs) apply (simp add: mapM_Nil return_df) apply (simp add: mapM_Cons) apply (rule bind_dfI, assumption) apply (rule bind_dfI, assumption) apply (rule return_df) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. det_or_fail (f x)) \<Longrightarrow> det_or_fail (mapM f xs) proof (prove)
goal (2 subgoals):
 1. (\<And>x. det_or_fail (f x)) \<Longrightarrow> det_or_fail (mapM f [])
 2. \<And>a xs. \<lbrakk>(\<And>x. det_or_fail (f x)) \<Longrightarrow> det_or_fail (mapM f xs); \<And>x. det_or_fail (f x)\<rbrakk> \<Longrightarrow> det_or_fail (mapM f (a # xs)) proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>(\<And>x. det_or_fail (f x)) \<Longrightarrow> det_or_fail (mapM f xs); \<And>x. det_or_fail (f x)\<rbrakk> \<Longrightarrow> det_or_fail (mapM f (a # xs)) proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>det_or_fail (mapM f xs); \<And>x. det_or_fail (f x)\<rbrakk> \<Longrightarrow> det_or_fail (do y <- f a;
ys <- mapM f xs;
return (y # ys)
od) proof (prove)
goal (1 subgoal):
 1. \<And>a xs x. \<lbrakk>det_or_fail (mapM f xs); \<And>x. det_or_fail (f x)\<rbrakk> \<Longrightarrow> det_or_fail (do ys <- mapM f xs;
return (x # ys)
od) proof (prove)
goal (1 subgoal):
 1. \<And>a xs x xa. \<lbrakk>det_or_fail (mapM f xs); \<And>x. det_or_fail (f x)\<rbrakk> \<Longrightarrow> det_or_fail (return (x # xa)) proof (prove)
goal:
No subgoals!
theory StateTranslation_D

lemma df_loadWord: "det_or_fail (loadWord x)" apply (unfold loadWord_def) apply (rule bind_dfI) apply (simp add: simpler_gets_def det_or_fail_def) apply clarsimp apply (rule bind_dfI) apply (rule assert_df) apply (rule return_df) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det_or_fail (loadWord x) proof (prove)
goal (1 subgoal):
 1. det_or_fail (do m <- gets underlying_memory;
assert (x && mask 2 = 0);
return (word_rcat [m (x + 3), m (x + 2), m (x + 1), m x])
od) proof (prove)
goal (2 subgoals):
 1. det_or_fail (gets underlying_memory)
 2. \<And>xa. det_or_fail (do assert (x && mask 2 = 0);
return (word_rcat [xa (x + 3), xa (x + 2), xa (x + 1), xa x])
od) proof (prove)
goal (1 subgoal):
 1. \<And>xa. det_or_fail (do assert (x && mask 2 = 0);
return (word_rcat [xa (x + 3), xa (x + 2), xa (x + 1), xa x])
od) proof (prove)
goal (1 subgoal):
 1. \<And>xa. det_or_fail (do y <- assert (x && mask 2 = 0);
return (word_rcat [xa (x + 3), xa (x + 2), xa (x + 1), xa x])
od) proof (prove)
goal (2 subgoals):
 1. \<And>xa. det_or_fail (assert (x && mask 2 = 0))
 2. \<And>xa xaa. det_or_fail (return (word_rcat [xa (x + 3), xa (x + 2), xa (x + 1), xa x])) proof (prove)
goal (1 subgoal):
 1. \<And>xa xaa. det_or_fail (return (word_rcat [xa (x + 3), xa (x + 2), xa (x + 1), xa x])) proof (prove)
goal:
No subgoals!
theory StateTranslation_D

lemma evalMonad_loadWord_cong:
  "underlying_memory ms = underlying_memory ms' \<Longrightarrow>
  evalMonad (loadWord x) ms = evalMonad (loadWord x) ms'" by (simp add: loadWord_def bind_def simpler_gets_def assert_def
                return_def fail_def evalMonad_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. underlying_memory ms = underlying_memory ms' \<Longrightarrow> evalMonad (loadWord x) ms = evalMonad (loadWord x) ms'