kings-crown/FVELER_Isabelle huggingface dataset:
theory CCorresLemmas

lemma ccorres_symb_exec_l3:
  "\<lbrakk> \<And>rv. ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv) hs (f rv) c;
     \<And>s. \<lbrace>(=) s\<rbrace> m \<lbrace>\<lambda>r. (=) s\<rbrace>; \<lbrace>G\<rbrace> m \<lbrace>Q\<rbrace>; empty_fail m\<rbrakk>
  \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf G {s'. \<forall>rv. s' \<in> Q' rv}
                  hs (m >>= f) c" apply (rule ccorres_guard_imp2, erule ccorres_symb_exec_l) apply assumption+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>rv. ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv) hs (f rv) c; \<And>s. \<lbrace>(=) s\<rbrace> m \<lbrace>\<lambda>r. (=) s\<rbrace>; \<lbrace>G\<rbrace> m \<lbrace>Q\<rbrace>; empty_fail m\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf G {s'. \<forall>rv. s' \<in> Q' rv} hs (m >>= f) c proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> m \<lbrace>\<lambda>r. (=) s\<rbrace>; \<lbrace>G\<rbrace> m \<lbrace>Q\<rbrace>; empty_fail m\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> m \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> m \<lbrace>\<lambda>r. (=) s\<rbrace>; \<lbrace>G\<rbrace> m \<lbrace>Q\<rbrace>; empty_fail m\<rbrakk> \<Longrightarrow> \<lbrace>?Q\<rbrace> m \<lbrace>Q\<rbrace>
 3. \<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> m \<lbrace>\<lambda>r. (=) s\<rbrace>; \<lbrace>G\<rbrace> m \<lbrace>Q\<rbrace>; empty_fail m\<rbrakk> \<Longrightarrow> empty_fail m
 4. \<And>s s'. \<lbrakk>\<And>rv. ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv) hs (f rv) c; \<And>s. \<lbrace>(=) s\<rbrace> m \<lbrace>\<lambda>r. (=) s\<rbrace>; \<lbrace>G\<rbrace> m \<lbrace>Q\<rbrace>; empty_fail m; (s, s') \<in> sr; G s; s' \<in> {s'. \<forall>rv. s' \<in> Q' rv}\<rbrakk> \<Longrightarrow> ?Q s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> sr \<and> Q rv s \<longrightarrow> s' \<in> Q' rv} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>\<And>rv. ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv) hs (f rv) c; \<And>s. \<lbrace>(=) s\<rbrace> m \<lbrace>\<lambda>r. (=) s\<rbrace>; \<lbrace>G\<rbrace> m \<lbrace>Q\<rbrace>; empty_fail m; (s, s') \<in> sr; G s; s' \<in> {s'. \<forall>rv. s' \<in> Q' rv}\<rbrakk> \<Longrightarrow> G s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> sr \<and> Q rv s \<longrightarrow> s' \<in> Q' rv} proof (prove)
goal:
No subgoals!
theory CCorresLemmas

lemma ccorres_add_returnOk:
  "ccorres_underlying Gamm sr rvr xf arrel axf hs P P' (a >>=E returnOk) c
     \<Longrightarrow> ccorres_underlying Gamm sr rvr xf arrel axf hs P P' a c" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying Gamm sr rvr xf arrel axf hs P P' (a >>=E returnOk) c \<Longrightarrow> ccorres_underlying Gamm sr rvr xf arrel axf hs P P' a c
theory CCorresLemmas

lemma ccorres_Guard_True:
  "ccorres_underlying sr \<Gamma> r xf arrel axf A C hs a c
   \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf A C hs a (Guard F \<lbrace>True\<rbrace> c)" by (simp, ccorres_rewrite, assumption)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf A C hs a c \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf A C hs a (Guard F \<lbrace>True\<rbrace> c)
theory CCorresLemmas

lemma ccorres_Guard_True_Seq:
  "ccorres_underlying sr \<Gamma> r xf arrel axf A C hs a (c ;; d)
   \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf A C hs a (Guard F \<lbrace>True\<rbrace> c ;; d)" by (simp, ccorres_rewrite, assumption)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf A C hs a (c;;
d) \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf A C hs a (Guard F \<lbrace>True\<rbrace> c;;
d)
theory CCorresLemmas

lemma ccorres_dc_o_simp[simp]:
  "ccorres_underlying srel \<Gamma> (dc \<circ> f) xf ar axf P Q hs m c
   = ccorres_underlying srel \<Gamma> dc xf ar axf P Q hs m c"
  "ccorres_underlying srel \<Gamma> r xf (dc \<circ> f) axf P Q hs m c
   = ccorres_underlying srel \<Gamma> r xf dc axf P Q hs m c" by (simp cong: ccorres_all_cong)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying srel \<Gamma> (dc \<circ> f) xf ar axf P Q hs m c = ccorres_underlying srel \<Gamma> dc xf ar axf P Q hs m c &&& ccorres_underlying srel \<Gamma> r xf (dc \<circ> f) axf P Q hs m c = ccorres_underlying srel \<Gamma> r xf dc axf P Q hs m c
theory CCorresLemmas

lemma ccorres_inl_rrel_inl_rrel[simp]:
  "ccorres_underlying srel \<Gamma> r xf (inl_rrel (inl_rrel ar)) axf P Q hs m c
   = ccorres_underlying srel \<Gamma> r xf (inl_rrel ar) axf P Q hs m c" by (simp add: inl_rrel_inl_rrel cong: ccorres_all_cong)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying srel \<Gamma> r xf (inl_rrel (inl_rrel ar)) axf P Q hs m c = ccorres_underlying srel \<Gamma> r xf (inl_rrel ar) axf P Q hs m c
theory CCorresLemmas

lemma ccorres_inr_rrel_Inr[simp]:
  "ccorres_underlying srel \<Gamma> (inr_rrel r \<circ> Inr) xf ar axf P Q hs m c
   = ccorres_underlying srel \<Gamma> r xf ar axf P Q hs m c" by (simp cong: ccorres_context_cong)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying srel \<Gamma> (inr_rrel r \<circ> Inr) xf ar axf P Q hs m c = ccorres_underlying srel \<Gamma> r xf ar axf P Q hs m c
theory CCorresLemmas

lemma add_remove_return:
  "getter >>= setter = do (do val \<leftarrow> getter; setter val; return val od); return () od" by (simp add: bind_assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. getter >>= setter = do do val <- getter;
setter val;
return val
od;
return ()
od
theory Move_C

lemma dumb_bool_for_all: "(\<forall>x. x) = False" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<forall>x. x) = False
theory Move_C

lemma (in semigroup) foldl_first:
  "f x (foldl f y zs) = foldl f (f x y) zs" by (induction zs arbitrary: x y) (auto simp: assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<^bold>* foldl (\<^bold>*) y zs = foldl (\<^bold>*) (x \<^bold>* y) zs
theory Move_C

lemma hd_in_zip_set:
   "slots \<noteq> [] \<Longrightarrow> (hd slots, 0) \<in> set (zip slots [0.e.of_nat (length slots - Suc 0)::machine_word])" by (cases slots; simp add: upto_enum_word upto_0_to_n2 del: upt_Suc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. slots \<noteq> [] \<Longrightarrow> (hd slots, 0) \<in> set (zip slots [0 .e. word_of_nat (length slots - Suc 0)])
theory Move_C

lemma last_in_zip_set:
  "\<lbrakk> slots \<noteq> []; length js = length slots \<rbrakk> \<Longrightarrow> (last slots, last js) \<in> set (zip slots js)" apply (simp add: in_set_zip last_conv_nth) apply (rule_tac x="length slots - 1" in exI) apply clarsimp apply (subst last_conv_nth) apply (cases js; simp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>slots \<noteq> []; length js = length slots\<rbrakk> \<Longrightarrow> (last slots, last js) \<in> set (zip slots js) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>slots \<noteq> []; length js = length slots\<rbrakk> \<Longrightarrow> \<exists>n. slots ! n = slots ! (length slots - Suc 0) \<and> js ! n = last js \<and> n < length slots proof (prove)
goal (1 subgoal):
 1. \<lbrakk>slots \<noteq> []; length js = length slots\<rbrakk> \<Longrightarrow> slots ! (length slots - 1) = slots ! (length slots - Suc 0) \<and> js ! (length slots - 1) = last js \<and> length slots - 1 < length slots proof (prove)
goal (1 subgoal):
 1. \<lbrakk>slots \<noteq> []; length js = length slots\<rbrakk> \<Longrightarrow> js ! (length slots - Suc 0) = last js proof (prove)
goal (2 subgoals):
 1. \<lbrakk>slots \<noteq> []; length js = length slots\<rbrakk> \<Longrightarrow> js \<noteq> []
 2. \<lbrakk>slots \<noteq> []; length js = length slots\<rbrakk> \<Longrightarrow> js ! (length slots - Suc 0) = js ! (length js - 1) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>slots \<noteq> []; length js = length slots\<rbrakk> \<Longrightarrow> js ! (length slots - Suc 0) = js ! (length js - 1) proof (prove)
goal:
No subgoals!
theory Move_C

lemma list_length_less:
  "(args = [] \<or> length args \<le> Suc 0) = (length args < 2)" by (case_tac args, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (args = [] \<or> length args \<le> Suc 0) = (length args < 2)
theory Move_C

lemma at_least_2_args:
  "\<not>  length args < 2 \<Longrightarrow> \<exists>a b c. args = a#b#c" apply (case_tac args) apply simp apply (case_tac list) apply simp apply (case_tac lista) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> length args < 2 \<Longrightarrow> \<exists>a b c. args = a # b # c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> length args < 2; args = []\<rbrakk> \<Longrightarrow> \<exists>a b c. args = a # b # c
 2. \<And>a list. \<lbrakk>\<not> length args < 2; args = a # list\<rbrakk> \<Longrightarrow> \<exists>a b c. args = a # b # c proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>\<not> length args < 2; args = a # list\<rbrakk> \<Longrightarrow> \<exists>a b c. args = a # b # c proof (prove)
goal (2 subgoals):
 1. \<And>a list. \<lbrakk>\<not> length args < 2; args = a # list; list = []\<rbrakk> \<Longrightarrow> \<exists>a b c. args = a # b # c
 2. \<And>a list aa lista. \<lbrakk>\<not> length args < 2; args = a # list; list = aa # lista\<rbrakk> \<Longrightarrow> \<exists>a b c. args = a # b # c proof (prove)
goal (1 subgoal):
 1. \<And>a list aa lista. \<lbrakk>\<not> length args < 2; args = a # list; list = aa # lista\<rbrakk> \<Longrightarrow> \<exists>a b c. args = a # b # c proof (prove)
goal (2 subgoals):
 1. \<And>a list aa lista. \<lbrakk>\<not> length args < 2; args = a # list; list = aa # lista; lista = []\<rbrakk> \<Longrightarrow> \<exists>a b c. args = a # b # c
 2. \<And>a list aa lista ab listb. \<lbrakk>\<not> length args < 2; args = a # list; list = aa # lista; lista = ab # listb\<rbrakk> \<Longrightarrow> \<exists>a b c. args = a # b # c proof (prove)
goal (1 subgoal):
 1. \<And>a list aa lista ab listb. \<lbrakk>\<not> length args < 2; args = a # list; list = aa # lista; lista = ab # listb\<rbrakk> \<Longrightarrow> \<exists>a b c. args = a # b # c proof (prove)
goal:
No subgoals!
theory Move_C

lemma rel_option_alt_def:
  "rel_option f a b = (
      (a = None \<and>  b = None)
      \<or> (\<exists>x y. a = Some x \<and>  b = Some y \<and> f x y))" apply (case_tac a, case_tac b, simp, simp, case_tac b, auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rel_option f a b = (a = None \<and> b = None \<or> (\<exists>x y. a = Some x \<and> b = Some y \<and> f x y)) proof (prove)
goal:
No subgoals!
theory Move_C

lemma nat_le_induct [consumes 1, case_names base step]:
  assumes le: "i \<le> (k::nat)" and
        base: "P(k)" and
        step: "\<And>i. \<lbrakk>i \<le> k; P i; 0 < i\<rbrakk> \<Longrightarrow> P(i - 1)"
  shows "P i" proof - obtain j where jk: "j \<le> k" and j_eq: "i = k - j" using le apply (drule_tac x="k - i" in meta_spec) apply simp done have "j \<le> k \<Longrightarrow> P (k - j)" apply (induct j) apply (simp add: base) apply simp apply (drule step[rotated], simp+) done thus "P i" using jk j_eq by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P i proof (state)
goal (1 subgoal):
 1. P i proof (prove)
goal (1 subgoal):
 1. (\<And>j. \<lbrakk>j \<le> k; i = k - j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
i \<le> k

goal (1 subgoal):
 1. (\<And>j. \<lbrakk>j \<le> k; i = k - j\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<le> k; \<lbrakk>k - i \<le> k; i = k - (k - i)\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis proof (prove)
goal:
No subgoals! proof (state)
this:
j \<le> k
i = k - j

goal (1 subgoal):
 1. P i proof (prove)
goal (1 subgoal):
 1. j \<le> k \<Longrightarrow> P (k - j) proof (prove)
goal (2 subgoals):
 1. 0 \<le> k \<Longrightarrow> P (k - 0)
 2. \<And>j. \<lbrakk>j \<le> k \<Longrightarrow> P (k - j); Suc j \<le> k\<rbrakk> \<Longrightarrow> P (k - Suc j) proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>j \<le> k \<Longrightarrow> P (k - j); Suc j \<le> k\<rbrakk> \<Longrightarrow> P (k - Suc j) proof (prove)
goal (1 subgoal):
 1. \<And>j. \<lbrakk>P (k - j); Suc j \<le> k\<rbrakk> \<Longrightarrow> P (k - Suc j) proof (prove)
goal:
No subgoals! proof (state)
this:
j \<le> k \<Longrightarrow> P (k - j)

goal (1 subgoal):
 1. P i proof (prove)
using this:
j \<le> k \<Longrightarrow> P (k - j)

goal (1 subgoal):
 1. P i proof (prove)
using this:
j \<le> k \<Longrightarrow> P (k - j)
j \<le> k
i = k - j

goal (1 subgoal):
 1. P i proof (state)
this:
P i

goal:
No subgoals!
theory Move_C

lemma assumes A: "is_inv f g" shows the_inv_map_eq: "the_inv_map f = g" by (simp add: is_inv_unique[OF A A[THEN is_inv_inj, THEN is_inv_the_inv_map]])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. the_inv_map f = g
theory Move_C

lemma ran_map_comp_subset: "ran (map_comp f g) <= (ran f)" by (fastforce simp: map_comp_def ran_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ran (f \<circ>\<^sub>m g) \<subseteq> ran f
theory Move_C

lemma eq_option_to_0_rev:
  "Some 0 ~: A \<Longrightarrow> \<forall>x. \<forall>y\<in>A.
   ((=) \<circ> option_to_0) y x \<longrightarrow> (if x = 0 then None else Some x) = y" by (clarsimp simp: option_to_0_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Some (0::'a) \<notin> A \<Longrightarrow> \<forall>x. \<forall>y\<in>A. ((=) \<circ> option_to_0) y x \<longrightarrow> (if x = (0::'a) then None else Some x) = y
theory Move_C

lemma inj_image_inv:
  assumes inj_f: "inj f"
  shows "f ` A = B \<Longrightarrow> inv f ` B = A" by (drule sym) (simp add: image_inv_f_f[OF inj_f])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f ` A = B \<Longrightarrow> inv f ` B = A
theory Move_C

lemma Collect_mono2: "Collect P \<subseteq> Collect Q \<longleftrightarrow> (\<forall>x. P x \<longrightarrow> Q x)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (Collect P \<subseteq> Collect Q) = (\<forall>x. P x \<longrightarrow> Q x)
theory Move_C

lemma injection_handler_liftM:
  "injection_handler f
    = liftM (\<lambda>v. case v of Inl ex \<Rightarrow> Inl (f ex) | Inr rv \<Rightarrow> Inr rv)" apply (intro ext, simp add: injection_handler_def liftM_def
                              handleE'_def) apply (rule bind_apply_cong, rule refl) apply (simp add: throwError_def split: sum.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. injection_handler f = liftM (\<lambda>v. case v of Inl ex \<Rightarrow> Inl (f ex) | Inr rv \<Rightarrow> Inr rv) proof (prove)
goal (1 subgoal):
 1. \<And>x xa. (do v <- x;
case v of Inl e \<Rightarrow> throwError (f e) | Inr v' \<Rightarrow> return (Inr v')
od) xa = (do x <- x;
return (case x of Inl ex \<Rightarrow> Inl (f ex) | Inr x \<Rightarrow> Inr x)
od) xa proof (prove)
goal (1 subgoal):
 1. \<And>x xa rv st. (rv, st) \<in> fst (x xa) \<Longrightarrow> (case rv of Inl e \<Rightarrow> throwError (f e) | Inr v' \<Rightarrow> return (Inr v')) st = return (case rv of Inl ex \<Rightarrow> Inl (f ex) | Inr x \<Rightarrow> Inr x) st proof (prove)
goal:
No subgoals!
theory Move_C

lemma option_to_0_simps [simp]:
  "option_to_0 None =  0"
  "option_to_0 (Some x) = x" by (auto simp: option_to_0_def split: option.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. option_to_0 None = (0::'a) &&& option_to_0 (Some x) = x
theory Move_C

lemma of_bool_from_bool: "of_bool = from_bool" by (rule ext, simp add: from_bool_def split: bool.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. of_bool = from_bool
theory Move_C

lemma hoare_vcg_imp_lift_R:
  "\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. \<not> P rv s\<rbrace>, -; \<lbrace>Q'\<rbrace> f \<lbrace>Q\<rbrace>, - \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P' s \<or> Q' s\<rbrace> f \<lbrace>\<lambda>rv s. P rv s \<longrightarrow> Q rv s\<rbrace>, -" by (auto simp add: valid_def validE_R_def validE_def split_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. \<not> P rv s\<rbrace>, -; \<lbrace>Q'\<rbrace> f \<lbrace>Q\<rbrace>, -\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. P' s \<or> Q' s\<rbrace> f \<lbrace>\<lambda>rv s. P rv s \<longrightarrow> Q rv s\<rbrace>, -
theory Move_C

lemma length_Suc_0_conv:
  "length x = Suc 0 = (\<exists>y. x = [y])" by (induct x; clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (length x = Suc 0) = (\<exists>y. x = [y])
theory Move_C

lemma imp_ignore: "B \<Longrightarrow> A \<longrightarrow> B" by blast

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

lemma cteSizeBits_eq:
  "cteSizeBits = cte_level_bits" by (simp add: cte_level_bits_def cteSizeBits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cteSizeBits = cte_level_bits
theory Move_C

lemma cteSizeBits_le_cte_level_bits[simp]:
  "cteSizeBits \<le> cte_level_bits" by (simp add: cte_level_bits_def cteSizeBits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cteSizeBits \<le> cte_level_bits
theory Move_C

lemma msb_le_mono:
  fixes v w :: "'a::len word"
  shows "v \<le> w \<Longrightarrow> msb v \<Longrightarrow> msb w" by (simp add: msb_big)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>v \<le> w; msb v\<rbrakk> \<Longrightarrow> msb w
theory Move_C

lemma neg_msb_le_mono:
  fixes v w :: "'a::len word"
  shows "v \<le> w \<Longrightarrow> \<not> msb w \<Longrightarrow> \<not> msb v" by (simp add: msb_big)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>v \<le> w; \<not> msb w\<rbrakk> \<Longrightarrow> \<not> msb v
theory Move_C

lemma word_sless_iff_less:
  "\<lbrakk> \<not> msb v; \<not> msb w \<rbrakk> \<Longrightarrow> v <s w \<longleftrightarrow> v < w" by (simp add: word_sless_alt sint_eq_uint word_less_alt)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> msb v; \<not> msb w\<rbrakk> \<Longrightarrow> (v <s w) = (v < w)
theory Move_C

lemma word_sle_iff_le:
  "\<lbrakk> \<not> msb v; \<not> msb w \<rbrakk> \<Longrightarrow> v <=s w \<longleftrightarrow> v \<le> w" by (simp add: word_sle_def sint_eq_uint word_le_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> msb v; \<not> msb w\<rbrakk> \<Longrightarrow> (v \<le>s w) = (v \<le> w)
theory Move_C

lemma to_bool_if:
  "(if w \<noteq> 0 then 1 else 0) = (if to_bool w then 1 else 0)" by (auto simp: to_bool_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (if w \<noteq> 0 then 1::'a else (0::'a)) = (if to_bool w then 1::'a else (0::'a))
theory Move_C

lemma word_upcast_shiftr:
  assumes "LENGTH('a::len) \<le> LENGTH('b::len)"
  shows "UCAST('a \<rightarrow> 'b) (w >> n) = UCAST('a \<rightarrow> 'b) w >> n" apply (intro word_eqI impI iffI; clarsimp simp: word_size nth_shiftr nth_ucast) apply (drule test_bit_size) using assms by (simp add: word_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. UCAST('a \<rightarrow> 'b) (w >> n) = UCAST('a \<rightarrow> 'b) w >> n proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>na < LENGTH('b); w !! (n + na)\<rbrakk> \<Longrightarrow> n + na < LENGTH('b) proof (prove)
goal (1 subgoal):
 1. \<And>na. \<lbrakk>na < LENGTH('b); n + na < size w\<rbrakk> \<Longrightarrow> n + na < LENGTH('b) proof (prove)
using this:
LENGTH('a) \<le> LENGTH('b)

goal (1 subgoal):
 1. \<And>na. \<lbrakk>na < LENGTH('b); n + na < size w\<rbrakk> \<Longrightarrow> n + na < LENGTH('b)
theory Move_C

lemma word_upcast_neg_msb:
  "LENGTH('a::len) < LENGTH('b::len) \<Longrightarrow> \<not> msb (UCAST('a \<rightarrow> 'b) w)" unfolding ucast_def msb_word_of_int by clarsimp (metis Suc_pred bit_imp_le_length lens_gt_0(2) not_less_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. LENGTH('a) < LENGTH('b) \<Longrightarrow> \<not> msb (UCAST('a \<rightarrow> 'b) w) proof (prove)
goal (1 subgoal):
 1. LENGTH('a) < LENGTH('b) \<Longrightarrow> \<not> uint w !! (LENGTH('b) - 1)
theory Move_C

lemma word_upcast_0_sle:
  "LENGTH('a::len) < LENGTH('b::len) \<Longrightarrow> 0 <=s UCAST('a \<rightarrow> 'b) w" by (simp add: word_sle_iff_le[OF word_msb_0 word_upcast_neg_msb])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. LENGTH('a) < LENGTH('b) \<Longrightarrow> 0 \<le>s UCAST('a \<rightarrow> 'b) w
theory Move_C

lemma scast_ucast_up_eq_ucast:
  assumes "LENGTH('a::len) < LENGTH('b::len)"
  shows "SCAST('b \<rightarrow> 'c) (UCAST('a \<rightarrow> 'b) w) = UCAST('a \<rightarrow> 'c::len) w" using assms apply (subst scast_eq_ucast; simp) apply (simp only: ucast_def msb_word_of_int) apply (metis bin_nth_uint_imp decr_length_less_iff numeral_nat(7) verit_comp_simplify1(3)) by (metis less_or_eq_imp_le ucast_nat_def unat_ucast_up_simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. SCAST('b \<rightarrow> 'c) (UCAST('a \<rightarrow> 'b) w) = UCAST('a \<rightarrow> 'c) w proof (prove)
using this:
LENGTH('a) < LENGTH('b)

goal (1 subgoal):
 1. SCAST('b \<rightarrow> 'c) (UCAST('a \<rightarrow> 'b) w) = UCAST('a \<rightarrow> 'c) w proof (prove)
goal (2 subgoals):
 1. LENGTH('a) < LENGTH('b) \<Longrightarrow> \<not> msb (UCAST('a \<rightarrow> 'b) w)
 2. LENGTH('a) < LENGTH('b) \<Longrightarrow> UCAST('b \<rightarrow> 'c) (UCAST('a \<rightarrow> 'b) w) = UCAST('a \<rightarrow> 'c) w proof (prove)
goal (2 subgoals):
 1. LENGTH('a) < LENGTH('b) \<Longrightarrow> \<not> uint w !! (LENGTH('b) - 1)
 2. LENGTH('a) < LENGTH('b) \<Longrightarrow> UCAST('b \<rightarrow> 'c) (UCAST('a \<rightarrow> 'b) w) = UCAST('a \<rightarrow> 'c) w proof (prove)
goal (1 subgoal):
 1. LENGTH('a) < LENGTH('b) \<Longrightarrow> UCAST('b \<rightarrow> 'c) (UCAST('a \<rightarrow> 'b) w) = UCAST('a \<rightarrow> 'c) w
theory Move_C

lemma not_max_word_iff_less:
  "w \<noteq> max_word \<longleftrightarrow> w < max_word" by (simp add: order_less_le)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (w \<noteq> - 1) = (w < - 1)
theory Move_C

lemma and_not_max_word:
  "m \<noteq> max_word \<Longrightarrow> w && m \<noteq> max_word" by (simp add: not_max_word_iff_less word_and_less')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m \<noteq> - 1 \<Longrightarrow> w && m \<noteq> - 1
theory Move_C

lemma mask_not_max_word:
  "m < LENGTH('a::len) \<Longrightarrow> mask m \<noteq> (max_word :: 'a word)" by (simp add: mask_eq_exp_minus_1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m < LENGTH('a) \<Longrightarrow> mask m \<noteq> - 1
theory Move_C

lemma shiftr_not_max_word:
  "0 < n \<Longrightarrow> w >> n \<noteq> max_word" by (metis and_mask_eq_iff_shiftr_0 and_mask_not_max_word diff_less len_gt_0 shiftr_le_0 word_shiftr_lt)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> w >> n \<noteq> - 1
theory Move_C

lemma word_sandwich1:
  fixes a b c :: "'a::len word"
  assumes "a < b"
  assumes "b <= c"
  shows "0 < b - a \<and> b - a <= c" using assms diff_add_cancel order_less_irrefl add_0 word_le_imp_diff_le
        word_le_less_eq word_neq_0_conv by metis

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < b - a \<and> b - a \<le> c proof (prove)
using this:
a < b
b \<le> c
?a - ?b + ?b = ?a
\<not> ?x < ?x
(0::?'a) + ?a = ?a
\<lbrakk>?k \<le> ?n; ?n \<le> ?m\<rbrakk> \<Longrightarrow> ?n - ?k \<le> ?m
(?x \<le> ?y) = (?x = ?y \<or> ?x < ?y)
(?w \<noteq> 0) = (0 < ?w)

goal (1 subgoal):
 1. 0 < b - a \<and> b - a \<le> c