kings-crown/FVELER_Isabelle huggingface dataset:
theory Lib

lemma prefix_induct [consumes 1, case_names Nil Cons]:
  fixes prefix
  assumes np: "prefix \<le> lst"
  and base:   "\<And>xs. P [] xs"
  and rl:     "\<And>x xs y ys. \<lbrakk> x = y; xs \<le> ys; P xs ys \<rbrakk> \<Longrightarrow> P (x#xs) (y#ys)"
  shows "P prefix lst" using np proof (induct prefix arbitrary: lst) case Nil show ?case by fact next case (Cons x xs) have prem: "(x # xs) \<le> lst" by fact then obtain y ys where lv: "lst = y # ys" by (rule prefixE, auto) have ih: "\<And>lst. xs \<le> lst \<Longrightarrow> P xs lst" by fact show ?case using prem by (auto simp: lv intro!: rl ih) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P prefix lst proof (prove)
using this:
prefix \<le> lst

goal (1 subgoal):
 1. P prefix lst proof (state)
goal (2 subgoals):
 1. \<And>lst. [] \<le> lst \<Longrightarrow> P [] lst
 2. \<And>a prefix lst. \<lbrakk>\<And>lst. prefix \<le> lst \<Longrightarrow> P prefix lst; a # prefix \<le> lst\<rbrakk> \<Longrightarrow> P (a # prefix) lst proof (state)
this:
[] \<le> lst

goal (2 subgoals):
 1. \<And>lst. [] \<le> lst \<Longrightarrow> P [] lst
 2. \<And>a prefix lst. \<lbrakk>\<And>lst. prefix \<le> lst \<Longrightarrow> P prefix lst; a # prefix \<le> lst\<rbrakk> \<Longrightarrow> P (a # prefix) lst proof (prove)
goal (1 subgoal):
 1. P [] lst proof (state)
this:
P [] lst

goal (1 subgoal):
 1. \<And>a prefix lst. \<lbrakk>\<And>lst. prefix \<le> lst \<Longrightarrow> P prefix lst; a # prefix \<le> lst\<rbrakk> \<Longrightarrow> P (a # prefix) lst proof (state)
goal (1 subgoal):
 1. \<And>a prefix lst. \<lbrakk>\<And>lst. prefix \<le> lst \<Longrightarrow> P prefix lst; a # prefix \<le> lst\<rbrakk> \<Longrightarrow> P (a # prefix) lst proof (state)
this:
xs \<le> ?lst \<Longrightarrow> P xs ?lst
x # xs \<le> lst

goal (1 subgoal):
 1. \<And>a prefix lst. \<lbrakk>\<And>lst. prefix \<le> lst \<Longrightarrow> P prefix lst; a # prefix \<le> lst\<rbrakk> \<Longrightarrow> P (a # prefix) lst proof (prove)
goal (1 subgoal):
 1. x # xs \<le> lst proof (state)
this:
x # xs \<le> lst

goal (1 subgoal):
 1. \<And>a prefix lst. \<lbrakk>\<And>lst. prefix \<le> lst \<Longrightarrow> P prefix lst; a # prefix \<le> lst\<rbrakk> \<Longrightarrow> P (a # prefix) lst proof (chain)
picking this:
x # xs \<le> lst proof (prove)
using this:
x # xs \<le> lst

goal (1 subgoal):
 1. (\<And>y ys. lst = y # ys \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
lst = y # ys

goal (1 subgoal):
 1. \<And>a prefix lst. \<lbrakk>\<And>lst. prefix \<le> lst \<Longrightarrow> P prefix lst; a # prefix \<le> lst\<rbrakk> \<Longrightarrow> P (a # prefix) lst proof (prove)
goal (1 subgoal):
 1. \<And>lst. xs \<le> lst \<Longrightarrow> P xs lst proof (state)
this:
xs \<le> ?lst \<Longrightarrow> P xs ?lst

goal (1 subgoal):
 1. \<And>a prefix lst. \<lbrakk>\<And>lst. prefix \<le> lst \<Longrightarrow> P prefix lst; a # prefix \<le> lst\<rbrakk> \<Longrightarrow> P (a # prefix) lst proof (prove)
goal (1 subgoal):
 1. P (x # xs) lst proof (prove)
using this:
x # xs \<le> lst

goal (1 subgoal):
 1. P (x # xs) lst proof (state)
this:
P (x # xs) lst

goal:
No subgoals!
theory Lib

lemma rsubst:
  "\<lbrakk> P s; s = t \<rbrakk> \<Longrightarrow> P t" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P s; s = t\<rbrakk> \<Longrightarrow> P t
theory Lib

lemma ex_impE: "((\<exists>x. P x) \<longrightarrow> Q) \<Longrightarrow> P x \<Longrightarrow> Q" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<exists>x. P x) \<longrightarrow> Q; P x\<rbrakk> \<Longrightarrow> Q
theory Lib

lemma option_Some_value_independent:
  "\<lbrakk> f x = Some v; \<And>v'. f x = Some v' \<Longrightarrow> f y = Some v' \<rbrakk> \<Longrightarrow> f y = Some v" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f x = Some v; \<And>v'. f x = Some v' \<Longrightarrow> f y = Some v'\<rbrakk> \<Longrightarrow> f y = Some v
theory Lib

lemma distinct_map_enum:
  "\<lbrakk> (\<forall> x y. (F x = F y \<longrightarrow> x = y )) \<rbrakk>
   \<Longrightarrow> distinct (map F (enum_class.enum :: 'a :: enum list))" by (simp add: distinct_map inj_onI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>x y. F x = F y \<longrightarrow> x = y \<Longrightarrow> distinct (map F enum)
theory Lib

lemma if_option_Some:
  "((if P then None else Some x) = Some y) = (\<not>P \<and> x = y)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((if P then None else Some x) = Some y) = (\<not> P \<and> x = y)
theory Lib

lemma if_option_Some2:
  "((if P then Some x else None) = Some y) = (P \<and> x = y)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((if P then Some x else None) = Some y) = (P \<and> x = y)
theory Lib

lemma if_option_Some_eq:
  "((if P then None else Some x) = Some x) = (\<not>P)"
  "((if P then Some x else None) = Some x) = P" by simp+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((if P then None else Some x) = Some x) = (\<not> P) &&& ((if P then Some x else None) = Some x) = P
theory Lib

lemma if_option_None_eq:
  "((if P then None else Some x) = None) = P"
  "((if P then Some x else None) = None) = (\<not>P)" by simp+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((if P then None else Some x) = None) = P &&& ((if P then Some x else None) = None) = (\<not> P)
theory Lib

lemma option_case_all_conv:
  "(case x of None \<Rightarrow> True | Some v \<Rightarrow> P v) = (\<forall>v. x = Some v \<longrightarrow> P v)" by (auto split: option.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case x of None \<Rightarrow> True | Some v \<Rightarrow> P v) = (\<forall>v. x = Some v \<longrightarrow> P v)
theory Lib

lemma prod_o_comp:
  "(case x of (a, b) \<Rightarrow> f a b) \<circ> g = (case x of (a, b) \<Rightarrow> f a b \<circ> g)" by (auto simp: split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case x of (a, b) \<Rightarrow> f a b) \<circ> g = (case x of (a, b) \<Rightarrow> f a b \<circ> g)
theory Lib

lemma lhs_sym_eq:
  "(a = b) = x \<longleftrightarrow> (b = a) = x" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((a = b) = x) = ((b = a) = x)
theory Lib

lemma not_in_ran_None_upd:
  "x \<notin> ran m \<Longrightarrow> x \<notin> ran (m(y := None))" by (auto simp: ran_def split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<notin> ran m \<Longrightarrow> x \<notin> ran (m(y := None))
theory Lib

lemma ranD:
  "v \<in> ran f \<Longrightarrow> \<exists>x. f x = Some v" by (auto simp: ran_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. v \<in> ran f \<Longrightarrow> \<exists>x. f x = Some v
theory Lib

lemma fun_upd_swap:
  "a \<noteq> c \<Longrightarrow>  hp(c := d, a := b) = hp(a := b, c := d)" by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a \<noteq> c \<Longrightarrow> hp(c := d, a := b) = hp(a := b, c := d)
theory Lib

lemma list_not_head:
  "Suc 0 < length ls \<Longrightarrow> ls \<noteq> [hd ls]" by (cases ls; clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Suc 0 < length ls \<Longrightarrow> ls \<noteq> [hd ls]
theory Lib

lemma list_not_last:
  "Suc 0 < length ls \<Longrightarrow> ls \<noteq> [last ls]" by (cases ls; clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Suc 0 < length ls \<Longrightarrow> ls \<noteq> [last ls]
theory Lib

lemma length_tail_nonempty:
  "Suc 0 < length list \<Longrightarrow> tl list \<noteq> []" by (cases list, simp, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Suc 0 < length list \<Longrightarrow> tl list \<noteq> []
theory MachineMonad

lemma failure_consistent:
  "\<lbrakk> empty_fail f; no_fail \<top> f \<rbrakk> \<Longrightarrow> ignore_failure f = f" apply (simp add: ignore_failure_def empty_fail_def no_fail_def) apply (rule ext) apply (auto intro: prod_eqI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>empty_fail f; no_fail (\<lambda>_. True) f\<rbrakk> \<Longrightarrow> ignore_failure f = f proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. fst (f s) \<noteq> {}; \<forall>s. \<not> snd (f s)\<rbrakk> \<Longrightarrow> (\<lambda>s. (fst (f s), False)) = f proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>s. fst (f s) \<noteq> {}; \<forall>s. \<not> snd (f s)\<rbrakk> \<Longrightarrow> (fst (f s), False) = f s proof (prove)
goal:
No subgoals!
theory MachineMonad

lemma ef_ignore_failure [simp]:
  "empty_fail (ignore_failure f)" by (simp add: empty_fail_def ignore_failure_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (ignore_failure f)
theory MachineMonad

lemma no_fail_ignore_failure [simp, intro!]:
  "no_fail \<top> (ignore_failure f)" by (simp add: no_fail_def ignore_failure_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (ignore_failure f)
theory MachineMonad

lemma ef_machine_rest_lift [simp, intro!]:
  "empty_fail f \<Longrightarrow> empty_fail (machine_rest_lift f)" apply (clarsimp simp: empty_fail_def machine_rest_lift_def simpler_gets_def
                        select_f_def bind_def simpler_modify_def return_def) apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail f \<Longrightarrow> empty_fail (machine_rest_lift f) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>s. fst (f s) = {} \<longrightarrow> snd (f s); \<forall>x\<in>fst (f (machine_state_rest s)). fst ((case x of (r, mr') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state_rest := mr'\<rparr>)}, False)) s) = {}; \<not> snd (f (machine_state_rest s))\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f (machine_state_rest s)). snd ((case x of (r, mr') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state_rest := mr'\<rparr>)}, False)) s) proof (prove)
goal:
No subgoals!
theory MachineMonad

lemma no_fail_machine_state_rest [intro!]:
  "no_fail P f \<Longrightarrow> no_fail (P o machine_state_rest) (machine_rest_lift f)" apply (simp add: no_fail_def machine_rest_lift_def simpler_gets_def
                        select_f_def bind_def simpler_modify_def return_def) apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail P f \<Longrightarrow> no_fail (P \<circ> machine_state_rest) (machine_rest_lift f) proof (prove)
goal (1 subgoal):
 1. \<forall>s. P s \<longrightarrow> \<not> snd (f s) \<Longrightarrow> \<forall>s. P (machine_state_rest s) \<longrightarrow> (\<forall>x\<in>fst (f (machine_state_rest s)). \<not> snd ((case x of (r, mr') \<Rightarrow> \<lambda>s. ({(r, s\<lparr>machine_state_rest := mr'\<rparr>)}, False)) s)) proof (prove)
goal:
No subgoals!
theory MachineMonad

lemma no_fail_machine_state_rest_T [simp, intro!]:
  "no_fail \<top> f \<Longrightarrow> no_fail \<top> (machine_rest_lift f)" apply (drule no_fail_machine_state_rest) apply (simp add: o_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) f \<Longrightarrow> no_fail (\<lambda>_. True) (machine_rest_lift f) proof (prove)
goal (1 subgoal):
 1. no_fail ((\<lambda>_. True) \<circ> machine_state_rest) (machine_rest_lift f) \<Longrightarrow> no_fail (\<lambda>_. True) (machine_rest_lift f) proof (prove)
goal:
No subgoals!
theory MachineOps

lemma loadWord_storeWord_is_return:
  "p && mask 2 = 0 \<Longrightarrow> (do w \<leftarrow> loadWord p; storeWord p w od) = return ()" apply (rule ext) apply (simp add: loadWord_def storeWord_def bind_def assert_def return_def
    modify_def gets_def get_def eval_nat_numeral put_def) apply (simp add: word_rsplit_rcat_size word_size) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. p && mask 2 = 0 \<Longrightarrow> loadWord p >>= storeWord p = return () proof (prove)
goal (1 subgoal):
 1. \<And>x. p && mask 2 = 0 \<Longrightarrow> (loadWord p >>= storeWord p) x = return () x proof (prove)
goal (1 subgoal):
 1. \<And>x. p && mask (Suc (Suc 0)) = 0 \<Longrightarrow> underlying_memory_update (\<lambda>m. m(p := word_rsplit (word_rcat [underlying_memory x (p + 3), underlying_memory x (p + 2), underlying_memory x (p + 1), underlying_memory x p]) ! Suc (Suc (Suc 0)), p + 1 := word_rsplit (word_rcat [underlying_memory x (p + 3), underlying_memory x (p + 2), underlying_memory x (p + 1), underlying_memory x p]) ! Suc (Suc 0), p + 2 := word_rsplit (word_rcat [underlying_memory x (p + 3), underlying_memory x (p + 2), underlying_memory x (p + 1), underlying_memory x p]) ! Suc 0, p + 3 := word_rsplit (word_rcat [underlying_memory x (p + 3), underlying_memory x (p + 2), underlying_memory x (p + 1), underlying_memory x p]) ! 0)) x = x proof (prove)
goal:
No subgoals!
theory MachineExports

lemma Suc_unat_mask_div_obfuscated:
  "Suc (unat (mask sz div (word_size::machine_word))) = 2 ^ (min sz word_bits - word_size_bits)" by (rule Suc_unat_mask_div)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Suc (unat (mask sz div word_size)) = 2 ^ (min sz word_bits - word_size_bits)
theory MachineExports

lemma word_size_size_bits_nat:
  "2^word_size_bits = (word_size :: nat)" by (simp add: word_size_bits_def word_size_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 2 ^ word_size_bits = word_size
theory MachineExports

lemma word_size_size_bits_word:
  "2^word_size_bits = (word_size :: 'a :: len word)" by (simp add: word_size_bits_def word_size_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 2 ^ word_size_bits = word_size
theory MiscMachine_A

lemma asid_bits_len_checks:
  "asid_bits = asid_high_bits + asid_low_bits"
  "asid_bits \<le> LENGTH(asid_rep_len)" unfolding asid_bits_defs by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. asid_bits = asid_high_bits + asid_low_bits &&& asid_bits \<le> LENGTH(32) proof (prove)
goal (1 subgoal):
 1. LENGTH(17) = LENGTH(7) + LENGTH(10) &&& LENGTH(17) \<le> LENGTH(32)
theory Kernel_Config_Lemmas

lemma numDomains_not_zero:
  "numDomains > 0" unfolding Kernel_Config.numDomains_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < numDomains proof (prove)
goal (1 subgoal):
 1. 0 < 16
theory Kernel_Config_Lemmas

lemma numDomains_machine_word_safe:
  "unat (of_nat numDomains :: machine_word) = numDomains" unfolding Kernel_Config.numDomains_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (word_of_nat numDomains) = numDomains proof (prove)
goal (1 subgoal):
 1. unat (word_of_nat 16) = 16
theory Arch_Kernel_Config_Lemmas

lemma physBase_aligned:
  "is_aligned physBase 24" by (simp add: is_aligned_def Kernel_Config.physBase_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned physBase 24
theory Structures_A

lemma zombie_cte_bits_simps[simp]:
 "zombie_cte_bits (Some n) = n"
 "zombie_cte_bits None     = 3" by (simp add: zombie_cte_bits_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. zombie_cte_bits (Some n) = n &&& zombie_cte_bits None = 3
theory List_Lib

lemma zip_take1:
  "zip (take n xs) ys = take n (zip xs ys)" apply (induct xs arbitrary: n ys) apply simp_all apply (case_tac n, simp_all) apply (case_tac ys, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. zip (take n xs) ys = take n (zip xs ys) proof (prove)
goal (2 subgoals):
 1. \<And>n ys. zip (take n []) ys = take n (zip [] ys)
 2. \<And>a xs n ys. (\<And>n ys. zip (take n xs) ys = take n (zip xs ys)) \<Longrightarrow> zip (take n (a # xs)) ys = take n (zip (a # xs) ys) proof (prove)
goal (1 subgoal):
 1. \<And>a xs n ys. (\<And>n ys. zip (take n xs) ys = take n (zip xs ys)) \<Longrightarrow> zip (take n (a # xs)) ys = take n (zip (a # xs) ys) proof (prove)
goal (1 subgoal):
 1. \<And>a xs n ys nat. \<lbrakk>\<And>n ys. zip (take n xs) ys = take n (zip xs ys); n = Suc nat\<rbrakk> \<Longrightarrow> zip (a # take nat xs) ys = take (Suc nat) (zip (a # xs) ys) proof (prove)
goal:
No subgoals!
theory List_Lib

lemma zip_take2:
  "zip xs (take n ys) = take n (zip xs ys)" apply (induct xs arbitrary: n ys) apply simp_all apply (case_tac n, simp_all) apply (case_tac ys, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. zip xs (take n ys) = take n (zip xs ys) proof (prove)
goal (2 subgoals):
 1. \<And>n ys. zip [] (take n ys) = take n (zip [] ys)
 2. \<And>a xs n ys. (\<And>n ys. zip xs (take n ys) = take n (zip xs ys)) \<Longrightarrow> zip (a # xs) (take n ys) = take n (zip (a # xs) ys) proof (prove)
goal (1 subgoal):
 1. \<And>a xs n ys. (\<And>n ys. zip xs (take n ys) = take n (zip xs ys)) \<Longrightarrow> zip (a # xs) (take n ys) = take n (zip (a # xs) ys) proof (prove)
goal (1 subgoal):
 1. \<And>a xs n ys nat. \<lbrakk>\<And>n ys. zip xs (take n ys) = take n (zip xs ys); n = Suc nat\<rbrakk> \<Longrightarrow> zip (a # xs) (take (Suc nat) ys) = take (Suc nat) (zip (a # xs) ys) proof (prove)
goal:
No subgoals!
theory List_Lib

lemma replicate_append: "replicate n x @ (x # xs) = replicate (n + 1) x @ xs" by (induct n, simp+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. replicate n x @ x # xs = replicate (n + 1) x @ xs
theory Deterministic_A

lemma trans_state[simp]: "kheap (trans_state t s) = kheap s"
                            "cdt (trans_state t s) = cdt s"
                            "is_original_cap (trans_state t s) = is_original_cap s"
                            "cur_thread (trans_state t s) = cur_thread s"
                            "idle_thread (trans_state t s) = idle_thread s"
                            "machine_state (trans_state t s) = machine_state s"
                            "interrupt_irq_node (trans_state t s) = interrupt_irq_node s"
                           "interrupt_states (trans_state t s) = interrupt_states s"
                            "arch_state (trans_state t s) = arch_state s"
                            "exst (trans_state t s) = (t (exst s))"
                            "exst (trans_state (\<lambda>_. e) s) = e" apply (simp add: trans_state_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((kheap (trans_state t s) = kheap s &&& cdt (trans_state t s) = cdt s) &&& is_original_cap (trans_state t s) = is_original_cap s &&& cur_thread (trans_state t s) = cur_thread s &&& idle_thread (trans_state t s) = idle_thread s) &&& (machine_state (trans_state t s) = machine_state s &&& interrupt_irq_node (trans_state t s) = interrupt_irq_node s &&& interrupt_states (trans_state t s) = interrupt_states s) &&& arch_state (trans_state t s) = arch_state s &&& exst (trans_state t s) = t (exst s) &&& exst (trans_state (\<lambda>_. e) s) = e proof (prove)
goal:
No subgoals!
theory Deterministic_A

lemma trans_state_update[simp]:
 "trans_state t (kheap_update f s) = kheap_update f (trans_state t s)"
 "trans_state t (cdt_update g s) = cdt_update g (trans_state t s)"
 "trans_state t (is_original_cap_update h s) = is_original_cap_update h (trans_state t s)"
 "trans_state t (cur_thread_update i s) = cur_thread_update i (trans_state t s)"
 "trans_state t (idle_thread_update j s) = idle_thread_update j (trans_state t s)"
 "trans_state t (machine_state_update k s) = machine_state_update k (trans_state t s)"
 "trans_state t (interrupt_irq_node_update l s) = interrupt_irq_node_update l (trans_state t s)"
 "trans_state t (arch_state_update m s) = arch_state_update m (trans_state t s)"
 "trans_state t (interrupt_states_update p s) = interrupt_states_update p (trans_state t s)" apply (simp add: trans_state_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((trans_state t (kheap_update f s) = kheap_update f (trans_state t s) &&& trans_state t (cdt_update g s) = cdt_update g (trans_state t s)) &&& trans_state t (is_original_cap_update h s) = is_original_cap_update h (trans_state t s) &&& trans_state t (cur_thread_update i s) = cur_thread_update i (trans_state t s)) &&& (trans_state t (idle_thread_update j s) = idle_thread_update j (trans_state t s) &&& trans_state t (machine_state_update k s) = machine_state_update k (trans_state t s)) &&& trans_state t (interrupt_irq_node_update l s) = interrupt_irq_node_update l (trans_state t s) &&& trans_state t (arch_state_update m s) = arch_state_update m (trans_state t s) &&& trans_state t (interrupt_states_update p s) = interrupt_states_update p (trans_state t s) proof (prove)
goal:
No subgoals!
theory Deterministic_A

lemma trans_state_update':
  "trans_state f = exst_update f" apply (rule ext) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. trans_state f = exst_update f proof (prove)
goal (1 subgoal):
 1. \<And>x. trans_state f x = exst_update f x proof (prove)
goal:
No subgoals!
theory Deterministic_A

lemma trans_state_update''[simp]:
  "trans_state t' (trans_state t s) = trans_state (\<lambda>e. t' (t e)) s" apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. trans_state t' (trans_state t s) = trans_state (\<lambda>e. t' (t e)) s proof (prove)
goal:
No subgoals!
theory KHeap_A

lemma proj_inj: "inj f \<Longrightarrow> (partial_inv f ko = Some v) = (f v = ko)" by (auto simp: partial_inv_def the_equality injD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. inj f \<Longrightarrow> (partial_inv f ko = Some v) = (f v = ko)
theory KHeap_A

lemma inj_Endpoint: "inj Endpoint" by (auto intro: injI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. inj Endpoint
theory KHeap_A

lemma proj_ko_type_ep[simp]: "(\<exists>v. partial_inv Endpoint  ko = Some (v::endpoint)) = (a_type ko = AEndpoint)" by (cases ko; auto simp: partial_inv_def a_type_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<exists>v. partial_inv Endpoint ko = Some v) = (a_type ko = AEndpoint)
theory KHeap_A

lemma proj_ko_type_ntfn[simp]:
  "(\<exists>v. partial_inv Notification  ko = Some (v::notification)) = (a_type ko = ANTFN)" by (cases ko; auto simp: partial_inv_def a_type_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<exists>v. partial_inv Notification ko = Some v) = (a_type ko = ANTFN)
theory CSpace_A

lemma rab_termination:
  "\<forall>cref guard radix_bits.
    \<not> length cref \<le> radix_bits + length guard \<and>
    (0 < radix_bits \<or> guard \<noteq> []) \<longrightarrow>
      length cref - (radix_bits + length guard) < length cref" apply clarsimp apply (erule disjE) apply arith apply (clarsimp simp: neq_Nil_conv) apply arith done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>cref guard radix_bits. \<not> length cref \<le> radix_bits + length guard \<and> (0 < radix_bits \<or> guard \<noteq> []) \<longrightarrow> length cref - (radix_bits + length guard) < length cref proof (prove)
goal (1 subgoal):
 1. \<And>cref guard radix_bits. \<lbrakk>\<not> length cref \<le> radix_bits + length guard; 0 < radix_bits \<or> guard \<noteq> []\<rbrakk> \<Longrightarrow> length cref - (radix_bits + length guard) < length cref proof (prove)
goal (2 subgoals):
 1. \<And>cref guard radix_bits. \<lbrakk>\<not> length cref \<le> radix_bits + length guard; 0 < radix_bits\<rbrakk> \<Longrightarrow> length cref - (radix_bits + length guard) < length cref
 2. \<And>cref guard radix_bits. \<lbrakk>\<not> length cref \<le> radix_bits + length guard; guard \<noteq> []\<rbrakk> \<Longrightarrow> length cref - (radix_bits + length guard) < length cref proof (prove)
goal (1 subgoal):
 1. \<And>cref guard radix_bits. \<lbrakk>\<not> length cref \<le> radix_bits + length guard; guard \<noteq> []\<rbrakk> \<Longrightarrow> length cref - (radix_bits + length guard) < length cref proof (prove)
goal (1 subgoal):
 1. \<And>cref radix_bits ys. \<not> length cref \<le> Suc (radix_bits + length ys) \<Longrightarrow> length cref - Suc (radix_bits + length ys) < length cref proof (prove)
goal:
No subgoals!
theory InvocationLabels_H

lemma GenInvocationLabel_map_distinct[simp]: "distinct (map GenInvocationLabel enum)" apply (simp add: distinct_map) by (meson injI invocation_label.inject)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct (map GenInvocationLabel enum) proof (prove)
goal (1 subgoal):
 1. inj GenInvocationLabel