kings-crown/FVELER_Isabelle huggingface dataset:
theory TailrecPre

lemma short_tailrec_pair_single_step:
  "\<forall>v. \<not> isLeft (fst (f v))
    \<Longrightarrow> short_tailrec_pair f = (\<lambda>v. let (rv, b) = (f v) in (b, theRight rv))" apply (rule ext) apply (simp add: short_tailrec_pair_def split_def Let_def) apply (simp add: short_tailrec_thm cong: imp_cong[OF _ refl] if_weak_cong) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>v. isRight (fst (f v)) \<Longrightarrow> short_tailrec_pair f = (\<lambda>v. let (rv, b) = f v in (b, theRight rv)) proof (prove)
goal (1 subgoal):
 1. \<And>v. \<forall>v. isRight (fst (f v)) \<Longrightarrow> short_tailrec_pair f v = (let (rv, b) = f v in (b, theRight rv)) proof (prove)
goal (1 subgoal):
 1. \<And>v. \<forall>v. isRight (fst (f v)) \<Longrightarrow> short_tailrec_pre f v = snd (f v) \<and> short_tailrec f v = theRight (fst (f v)) proof (prove)
goal:
No subgoals!
theory TailrecPre

lemma eq_true_imp:
  "(x ==  Trueprop True) ==> PROP x" apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. PROP x \<equiv> True \<Longrightarrow> PROP x proof (prove)
goal:
No subgoals!
theory GraphLang

lemma relpow_Suc_simp2:
  "R ^^ Suc n = R O R ^^ n" apply safe apply (erule relpow_Suc_E2, blast) apply (blast intro: relpow_Suc_I2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. R ^^ Suc n = R O R ^^ n proof (prove)
goal (2 subgoals):
 1. \<And>a b. (a, b) \<in> R ^^ Suc n \<Longrightarrow> (a, b) \<in> R O R ^^ n
 2. \<And>a b x y z. \<lbrakk>(x, y) \<in> R; (y, z) \<in> R ^^ n\<rbrakk> \<Longrightarrow> (x, z) \<in> R ^^ Suc n proof (prove)
goal (1 subgoal):
 1. \<And>a b x y z. \<lbrakk>(x, y) \<in> R; (y, z) \<in> R ^^ n\<rbrakk> \<Longrightarrow> (x, z) \<in> R ^^ Suc n proof (prove)
goal:
No subgoals!
theory GraphLang

lemma exec_graph_n_take_step:
  "\<lbrakk> (stack, stack') \<in> exec_graph_n GGamma n;
    \<lbrakk> n = 0; stack' = stack \<rbrakk> \<Longrightarrow> P;
    \<And>stack''. \<lbrakk> n > 0; (stack, stack'') \<in> exec_graph_step GGamma;
            (stack'', stack') \<in> exec_graph_n GGamma (n - 1) \<rbrakk>
        \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" apply (cases n, simp_all only: exec_graph_n_def relpow_Suc_simp2) apply simp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(stack, stack') \<in> exec_graph_n GGamma n; \<lbrakk>n = 0; stack' = stack\<rbrakk> \<Longrightarrow> P; \<And>stack''. \<lbrakk>0 < n; (stack, stack'') \<in> exec_graph_step GGamma; (stack'', stack') \<in> exec_graph_n GGamma (n - 1)\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(stack, stack') \<in> exec_graph_step GGamma ^^ 0; \<lbrakk>0 = 0; stack' = stack\<rbrakk> \<Longrightarrow> P; \<And>stack''. \<lbrakk>0 < 0; (stack, stack'') \<in> exec_graph_step GGamma; (stack'', stack') \<in> exec_graph_step GGamma ^^ (0 - 1)\<rbrakk> \<Longrightarrow> True; n = 0\<rbrakk> \<Longrightarrow> P
 2. \<And>nat. \<lbrakk>(stack, stack') \<in> exec_graph_step GGamma O exec_graph_step GGamma ^^ nat; \<lbrakk>Suc nat = 0; stack' = stack\<rbrakk> \<Longrightarrow> True; \<And>stack''. \<lbrakk>0 < Suc nat; (stack, stack'') \<in> exec_graph_step GGamma; (stack'', stack') \<in> exec_graph_step GGamma ^^ (Suc nat - 1)\<rbrakk> \<Longrightarrow> P; n = Suc nat\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>(stack, stack') \<in> exec_graph_step GGamma O exec_graph_step GGamma ^^ nat; \<lbrakk>Suc nat = 0; stack' = stack\<rbrakk> \<Longrightarrow> True; \<And>stack''. \<lbrakk>0 < Suc nat; (stack, stack'') \<in> exec_graph_step GGamma; (stack'', stack') \<in> exec_graph_step GGamma ^^ (Suc nat - 1)\<rbrakk> \<Longrightarrow> P; n = Suc nat\<rbrakk> \<Longrightarrow> P proof (prove)
goal:
No subgoals!
theory GraphLang

lemma exec_graph_take_step:
  "\<lbrakk> ((NextNode m, gst, fname) # stack, stack') \<in> exec_graph_n GGamma n;
            GGamma fname = Some gf; function_graph gf m = Some node \<rbrakk>
    \<Longrightarrow> (n = 0 \<and> stack' = (NextNode m, gst, fname) # stack)
    \<or> (\<exists>stack''. n \<ge> 1
            \<and> stack'' \<in> exec_node GGamma gst node
                    ((NextNode m, gst, fname) # stack)
            \<and> (stack'', stack') \<in> exec_graph_n GGamma (n - 1))" apply (erule exec_graph_n_take_step) apply simp apply (clarsimp simp: exec_graph_step_def split: graph_function.split_asm) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>((NextNode m, gst, fname) # stack, stack') \<in> exec_graph_n GGamma n; GGamma fname = Some gf; function_graph gf m = Some node\<rbrakk> \<Longrightarrow> n = 0 \<and> stack' = (NextNode m, gst, fname) # stack \<or> (\<exists>stack''. 1 \<le> n \<and> stack'' \<in> exec_node GGamma gst node ((NextNode m, gst, fname) # stack) \<and> (stack'', stack') \<in> exec_graph_n GGamma (n - 1)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>GGamma fname = Some gf; function_graph gf m = Some node; n = 0; stack' = (NextNode m, gst, fname) # stack\<rbrakk> \<Longrightarrow> n = 0 \<and> stack' = (NextNode m, gst, fname) # stack \<or> (\<exists>stack''. 1 \<le> n \<and> stack'' \<in> exec_node GGamma gst node ((NextNode m, gst, fname) # stack) \<and> (stack'', stack') \<in> exec_graph_n GGamma (n - 1))
 2. \<And>stack''. \<lbrakk>GGamma fname = Some gf; function_graph gf m = Some node; 0 < n; ((NextNode m, gst, fname) # stack, stack'') \<in> exec_graph_step GGamma; (stack'', stack') \<in> exec_graph_n GGamma (n - 1)\<rbrakk> \<Longrightarrow> n = 0 \<and> stack' = (NextNode m, gst, fname) # stack \<or> (\<exists>stack''. 1 \<le> n \<and> stack'' \<in> exec_node GGamma gst node ((NextNode m, gst, fname) # stack) \<and> (stack'', stack') \<in> exec_graph_n GGamma (n - 1)) proof (prove)
goal (1 subgoal):
 1. \<And>stack''. \<lbrakk>GGamma fname = Some gf; function_graph gf m = Some node; 0 < n; ((NextNode m, gst, fname) # stack, stack'') \<in> exec_graph_step GGamma; (stack'', stack') \<in> exec_graph_n GGamma (n - 1)\<rbrakk> \<Longrightarrow> n = 0 \<and> stack' = (NextNode m, gst, fname) # stack \<or> (\<exists>stack''. 1 \<le> n \<and> stack'' \<in> exec_node GGamma gst node ((NextNode m, gst, fname) # stack) \<and> (stack'', stack') \<in> exec_graph_n GGamma (n - 1)) proof (prove)
goal (1 subgoal):
 1. \<And>stack'' x1 x2 x3 x4. \<lbrakk>(stack'', stack') \<in> exec_graph_n GGamma (n - Suc 0); GGamma fname = Some (GraphFunction x1 x2 x3 x4); x3 m = Some node; 0 < n; gf = GraphFunction x1 x2 x3 x4; stack'' \<in> exec_node GGamma gst node ((NextNode m, gst, fname) # stack)\<rbrakk> \<Longrightarrow> \<exists>stack''. stack'' \<in> exec_node GGamma gst node ((NextNode m, gst, fname) # stack) \<and> (stack'', stack') \<in> exec_graph_n GGamma (n - Suc 0) proof (prove)
goal:
No subgoals!
theory GraphLang

lemma continuing_simps[simp]:
  "\<not> continuing []"
  "continuing [(unn, st, g)] = (unn \<noteq> Ret \<and> unn \<noteq> Err)"
  "continuing ((Ret, st, g) # stk) = (stk \<noteq> [])"
  "continuing (stf # stf' # stk)"
  "continuing ((NextNode nn, st, g) # stk)"
  "continuing ((Err, st, g) # stk) = (stk \<noteq> [])" by (simp_all add: continuing_def split: next_node.split list.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<not> continuing [] &&& continuing [(unn, st, g)] = (unn \<noteq> Ret \<and> unn \<noteq> Err) &&& continuing ((Ret, st, g) # stk) = (stk \<noteq> [])) &&& continuing (stf # stf' # stk) &&& continuing ((NextNode nn, st, g) # stk) &&& continuing ((Err, st, g) # stk) = (stk \<noteq> [])
theory GraphLang

lemma consume_Not_eq:
  "(\<not> P) = Q \<Longrightarrow> P = (\<not> Q)" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<not> P) = Q \<Longrightarrow> P = (\<not> Q)
theory GraphLang

lemma exec_node_case_helper:
  "(stk' \<in> exec_node Gamma st node stk)
    = (case node of Basic _ _ \<Rightarrow> stk' \<in> id (exec_node Gamma) st node stk
        | _ \<Rightarrow> stk' \<in> id (exec_node Gamma) st node stk)"
  "(stk' \<in> exec_node_return Gamma st node stk)
    = (case node of Basic _ _ \<Rightarrow> stk' \<in> id (exec_node_return Gamma) st node stk
        | _ \<Rightarrow> stk' \<in> id (exec_node_return Gamma) st node stk)" by (simp_all split: node.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (stk' \<in> exec_node Gamma st node stk) = (case node of node.Basic x xa \<Rightarrow> stk' \<in> id (exec_node Gamma) st node stk | _ \<Rightarrow> stk' \<in> id (exec_node Gamma) st node stk) &&& (stk' \<in> exec_node_return Gamma st node stk) = (case node of node.Basic x xa \<Rightarrow> stk' \<in> id (exec_node_return Gamma) st node stk | _ \<Rightarrow> stk' \<in> id (exec_node_return Gamma) st node stk)
theory GraphLang

lemma exec_graph_step_nonempty:
  "\<lbrakk> (stack, stack') \<in> exec_graph_step Gamma ^^ n; stack \<noteq> [] \<rbrakk>
    \<Longrightarrow> stack' \<noteq> []" by (cases n, auto simp: all_exec_graph_step_cases
                   split: graph_function.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(stack, stack') \<in> exec_graph_step Gamma ^^ n; stack \<noteq> []\<rbrakk> \<Longrightarrow> stack' \<noteq> []
theory GraphLang

lemma relpow_mono:
  "\<lbrakk> R \<subseteq> (S :: ('a \<times> 'a) set) \<rbrakk> \<Longrightarrow> R ^^ n \<subseteq> S ^^ n" by (induct n, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. R \<subseteq> S \<Longrightarrow> R ^^ n \<subseteq> S ^^ n
theory GraphLang

lemma drop_eq_Cons:
  "(drop n xs = x # ys) = (\<exists>zs. length zs = n \<and> xs = zs @ x # ys)" apply (induct n arbitrary: xs) apply simp apply (case_tac xs, auto simp add: length_Suc_conv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (drop n xs = x # ys) = (\<exists>zs. length zs = n \<and> xs = zs @ x # ys) proof (prove)
goal (2 subgoals):
 1. \<And>xs. (drop 0 xs = x # ys) = (\<exists>zs. length zs = 0 \<and> xs = zs @ x # ys)
 2. \<And>n xs. (\<And>xs. (drop n xs = x # ys) = (\<exists>zs. length zs = n \<and> xs = zs @ x # ys)) \<Longrightarrow> (drop (Suc n) xs = x # ys) = (\<exists>zs. length zs = Suc n \<and> xs = zs @ x # ys) proof (prove)
goal (1 subgoal):
 1. \<And>n xs. (\<And>xs. (drop n xs = x # ys) = (\<exists>zs. length zs = n \<and> xs = zs @ x # ys)) \<Longrightarrow> (drop (Suc n) xs = x # ys) = (\<exists>zs. length zs = Suc n \<and> xs = zs @ x # ys) proof (prove)
goal:
No subgoals!
theory GraphLang

lemma nat_trace_rel_Some_range:
  "tr \<in> nat_trace_rel cont r \<Longrightarrow> tr n = Some v
    \<Longrightarrow> \<forall>i \<le> n. \<exists>v'. tr i = Some v'" apply (induct n arbitrary: v, simp_all) apply (simp add: nat_trace_rel_def le_Suc_eq) apply (drule_tac x=n in spec, clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> nat_trace_rel cont r; tr n = Some v\<rbrakk> \<Longrightarrow> \<forall>i\<le>n. \<exists>v'. tr i = Some v' proof (prove)
goal (1 subgoal):
 1. \<And>n v. \<lbrakk>\<And>v. tr n = Some v \<Longrightarrow> \<forall>i\<le>n. \<exists>v'. tr i = Some v'; tr \<in> nat_trace_rel cont r; tr (Suc n) = Some v\<rbrakk> \<Longrightarrow> \<forall>i\<le>Suc n. \<exists>v'. tr i = Some v' proof (prove)
goal (1 subgoal):
 1. \<And>n v. \<lbrakk>\<And>v. tr n = Some v \<Longrightarrow> \<forall>i\<le>n. \<exists>v'. tr i = Some v'; \<forall>n. (tr n = None \<longrightarrow> tr (Suc n) = None) \<and> ((\<exists>y. tr (Suc n) = Some y) \<longrightarrow> (the (tr n), the (tr (Suc n))) \<in> r) \<and> ((\<exists>y. tr n = Some y) \<and> cont (the (tr n)) \<longrightarrow> (\<exists>y. tr (Suc n) = Some y)); tr (Suc n) = Some v\<rbrakk> \<Longrightarrow> \<forall>i\<le>n. \<exists>v'. tr i = Some v' proof (prove)
goal:
No subgoals!
theory GraphLang

lemma trace_None_dom_subset:
  "tr n = None \<Longrightarrow> tr \<in> nat_trace_rel cont R
    \<Longrightarrow> dom tr \<subseteq> {..< n}" apply clarsimp apply (drule_tac n=x in nat_trace_rel_Some_range, simp+) apply (drule_tac x="n" in spec) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr n = None; tr \<in> nat_trace_rel cont R\<rbrakk> \<Longrightarrow> dom tr \<subseteq> {..<n} proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>tr n = None; tr \<in> nat_trace_rel cont R; tr x = Some y\<rbrakk> \<Longrightarrow> x < n proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>tr n = None; tr x = Some y; \<forall>i\<le>x. \<exists>v'. tr i = Some v'\<rbrakk> \<Longrightarrow> x < n proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>tr n = None; tr x = Some y; n \<le> x \<longrightarrow> (\<exists>v'. tr n = Some v')\<rbrakk> \<Longrightarrow> x < n proof (prove)
goal:
No subgoals!
theory GraphLang

lemma nat_trace_Max_dom_None:
  "tr \<in> nat_trace_rel cont R \<Longrightarrow> tr n \<noteq> None \<Longrightarrow> (tr (Max (dom tr)) \<noteq> None)" apply (rule notI) apply (frule(1) trace_None_dom_subset) apply (cases "dom tr = {}") apply clarsimp apply (drule Max_in[rotated]) apply (simp add: finite_subset) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> nat_trace_rel cont R; tr n \<noteq> None\<rbrakk> \<Longrightarrow> tr (Max (dom tr)) \<noteq> None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> nat_trace_rel cont R; tr n \<noteq> None; tr (Max (dom tr)) = None\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> nat_trace_rel cont R; tr n \<noteq> None; tr (Max (dom tr)) = None; dom tr \<subseteq> {..<Max (dom tr)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>tr \<in> nat_trace_rel cont R; tr n \<noteq> None; tr (Max (dom tr)) = None; dom tr \<subseteq> {..<Max (dom tr)}; dom tr = {}\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>tr \<in> nat_trace_rel cont R; tr n \<noteq> None; tr (Max (dom tr)) = None; dom tr \<subseteq> {..<Max (dom tr)}; dom tr \<noteq> {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> nat_trace_rel cont R; tr n \<noteq> None; tr (Max (dom tr)) = None; dom tr \<subseteq> {..<Max (dom tr)}; dom tr \<noteq> {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>tr \<in> nat_trace_rel cont R; tr n \<noteq> None; tr (Max (dom tr)) = None; dom tr \<subseteq> {..<Max (dom tr)}\<rbrakk> \<Longrightarrow> finite (dom tr)
 2. \<lbrakk>tr \<in> nat_trace_rel cont R; tr n \<noteq> None; tr (Max (dom tr)) = None; dom tr \<subseteq> {..<Max (dom tr)}; Max (dom tr) \<in> dom tr\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tr \<in> nat_trace_rel cont R; tr n \<noteq> None; tr (Max (dom tr)) = None; dom tr \<subseteq> {..<Max (dom tr)}; Max (dom tr) \<in> dom tr\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory GraphLang

lemma trace_end_NoneD:
  "trace_end tr = None \<Longrightarrow> tr \<in> nat_trace_rel cont r
    \<Longrightarrow> tr = (\<lambda>_. None) \<or> (\<exists>f. tr = Some o f)" apply (subst disj_commute, rule disjCI) apply (clarsimp simp: fun_eq_iff) apply (simp add: trace_end_def split: if_split_asm) apply (metis nat_trace_Max_dom_None not_None_eq) apply (rule_tac x="the o tr" in exI, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trace_end tr = None; tr \<in> nat_trace_rel cont r\<rbrakk> \<Longrightarrow> tr = (\<lambda>_. None) \<or> (\<exists>f. tr = Some \<circ> f) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>trace_end tr = None; tr \<in> nat_trace_rel cont r; tr \<noteq> (\<lambda>_. None)\<rbrakk> \<Longrightarrow> \<exists>f. tr = Some \<circ> f proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>trace_end tr = None; tr \<in> nat_trace_rel cont r; tr x = Some y\<rbrakk> \<Longrightarrow> \<exists>f. \<forall>x. tr x = Some (f x) proof (prove)
goal (2 subgoals):
 1. \<And>x y n. \<lbrakk>tr \<in> nat_trace_rel cont r; tr x = Some y; tr n = None; tr (Max (dom tr)) = None\<rbrakk> \<Longrightarrow> \<exists>f. \<forall>x. tr x = Some (f x)
 2. \<And>x y. \<lbrakk>tr \<in> nat_trace_rel cont r; tr x = Some y; \<forall>n. \<exists>y. tr n = Some y\<rbrakk> \<Longrightarrow> \<exists>f. \<forall>x. tr x = Some (f x) proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>tr \<in> nat_trace_rel cont r; tr x = Some y; \<forall>n. \<exists>y. tr n = Some y\<rbrakk> \<Longrightarrow> \<exists>f. \<forall>x. tr x = Some (f x) proof (prove)
goal:
No subgoals!
theory CommonOpsLemmas

lemma fold_all_htd_updates':
  "ptr_retyp (p :: ('a :: c_type) ptr)
    = all_htd_updates TYPE('a) 1 (ptr_val p) 1"
  "(if P then (f :: heap_typ_desc \<Rightarrow> heap_typ_desc) else g) s
    = (if P then f s else g s)"
  "\<lbrakk> n < 2 ^ word_bits \<rbrakk> \<Longrightarrow>
    ptr_retyps n p = all_htd_updates TYPE('a) 1 (ptr_val p) (of_nat n)"
  "\<lbrakk> n < 2 ^ word_bits \<rbrakk> \<Longrightarrow>
    ptr_retyps (2 ^ n) p = all_htd_updates TYPE('a) 3 (ptr_val p) (of_nat n)"
  "n < 2 ^ word_bits \<Longrightarrow> typ_clear_region x n = all_htd_updates TYPE(machine_word) 0 x (of_nat n)"
  "n < 2 ^ word_bits \<Longrightarrow> typ_region_bytes x n = all_htd_updates TYPE(machine_word) 2 x (of_nat n)"
  "\<lbrakk> n < 2 ^ word_bits \<rbrakk> \<Longrightarrow>
    ptr_arr_retyps n p = all_htd_updates TYPE('a) 4 (ptr_val p) (of_nat n)"
  "\<lbrakk> n < 2 ^ word_bits \<rbrakk> \<Longrightarrow>
    ptr_arr_retyps (2 ^ n) p = all_htd_updates TYPE('a) 5 (ptr_val p) (of_nat n)" by (simp_all add: all_htd_updates_def fun_eq_iff word_bits_conv take_bit_nat_eq_self unat_of_nat)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((ptr_retyp p = all_htd_updates TYPE('a) 1 (ptr_val p) 1 &&& (if P then f else g) s = (if P then f s else g s)) &&& (n < 2 ^ word_bits \<Longrightarrow> ptr_retyps n p = all_htd_updates TYPE('a) 1 (ptr_val p) (word_of_nat n)) &&& (n < 2 ^ word_bits \<Longrightarrow> ptr_retyps (2 ^ n) p = all_htd_updates TYPE('a) 3 (ptr_val p) (word_of_nat n))) &&& ((n < 2 ^ word_bits \<Longrightarrow> typ_clear_region x n = all_htd_updates TYPE(32 word) 0 x (word_of_nat n)) &&& (n < 2 ^ word_bits \<Longrightarrow> typ_region_bytes x n = all_htd_updates TYPE(32 word) 2 x (word_of_nat n))) &&& (n < 2 ^ word_bits \<Longrightarrow> ptr_arr_retyps n p = all_htd_updates TYPE('a) 4 (ptr_val p) (word_of_nat n)) &&& (n < 2 ^ word_bits \<Longrightarrow> ptr_arr_retyps (2 ^ n) p = all_htd_updates TYPE('a) 5 (ptr_val p) (word_of_nat n))
theory CommonOpsLemmas

lemma upcast_unat_less_2p_length:
    "is_up UCAST('a :: len \<rightarrow> 'b :: len) \<Longrightarrow> unat (x :: 'a word) < 2 ^ LENGTH('b)" by (simp add: is_up unat_pow_le_intro)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_up UCAST('a \<rightarrow> 'b) \<Longrightarrow> unat x < 2 ^ LENGTH('b)
theory CommonOpsLemmas

lemma is_up_u32_word_size: "is_up UCAST(32 \<rightarrow> machine_word_len)" by (clarsimp simp add: is_up_def source_size target_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_up UCAST(32 \<rightarrow> 32)
theory CommonOpsLemmas

lemma is_up_i32_word_size: "is_up UCAST(32 signed \<rightarrow> machine_word_len)" by (clarsimp simp add: is_up_def source_size target_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_up UCAST(32 signed \<rightarrow> 32)
theory CommonOpsLemmas

lemma unat_word32_less_2p_word_bits: "unat (x :: 32 word) < 2 ^ word_bits" unfolding word_bits_def by (rule upcast_unat_less_2p_length, rule is_up_u32_word_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat x < 2 ^ word_bits proof (prove)
goal (1 subgoal):
 1. unat x < 2 ^ LENGTH(32)
theory CommonOpsLemmas

lemma unat_sword32_less_2p_word_bits: "unat (x :: 32 signed word) < 2 ^ word_bits" by (rule upcast_unat_less_2p_length[OF is_up_i32_word_size, simplified word_bits_def[symmetric]])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat x < 2 ^ word_bits
theory CommonOpsLemmas

lemma ptr_add_assertion_uintD:
  "ptr_add_assertion ptr (uint (x :: ('a :: len) word)) strong htd
    \<longrightarrow> (x = 0 \<or> array_assertion ptr (if strong then unat (x + 1) else unat x) htd)" by (auto simp: unat_plus_if_size intro: array_assertion_shrink_right)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptr_add_assertion ptr (uint x) strong htd \<longrightarrow> x = 0 \<or> array_assertion ptr (if strong then unat (x + 1) else unat x) htd
theory CommonOpsLemmas

lemma sint_uint_sless_0_if:
  "sint x = (if x <s 0 then - uint (- x) else uint (x :: ('a :: len) word))" apply (simp add: word_sint_msb_eq word_sless_alt
                   word_size uint_word_ariths) apply (clarsimp simp: zmod_zminus1_eq_if uint_0_iff) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sint x = (if x <s 0 then - uint (- x) else uint x) proof (prove)
goal (1 subgoal):
 1. msb x \<longrightarrow> uint x - 2 ^ LENGTH('a) = - (- uint x mod 2 ^ LENGTH('a)) proof (prove)
goal:
No subgoals!
theory CommonOpsLemmas

lemma ptr_add_assertion_sintD:
  "ptr_add_assertion ptr (sint (x :: ('a :: len) word)) strong htd
    \<longrightarrow> (x = 0 \<or> (x <s 0 \<and> array_assertion (ptr +\<^sub>p sint x)
            (unat (- x)) htd)
        \<or> (x \<noteq> 0 \<and> \<not> x <s 0 \<and> array_assertion ptr (if strong then unat (x + 1) else unat x) htd))" apply (simp add: ptr_add_assertion_def word_sless_alt
                   sint_uint_sless_0_if[THEN arg_cong[where f="\<lambda>x. - x"]]
                   sint_uint_sless_0_if[THEN arg_cong[where f=nat]]
                   unat_plus_if_size) apply (simp add: array_assertion_shrink_right) apply (auto simp: linorder_not_less) done

\<comment> \<open>
  Some lemmas used by both SimplExport and ProveGraphRefine.
\<close>

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptr_add_assertion ptr (sint x) strong htd \<longrightarrow> x = 0 \<or> x <s 0 \<and> array_assertion (ptr +\<^sub>p sint x) (unat (- x)) htd \<or> x \<noteq> 0 \<and> \<not> x <s 0 \<and> array_assertion ptr (if strong then unat (x + 1) else unat x) htd proof (prove)
goal (1 subgoal):
 1. (Suc (unat x) < 2 ^ size x \<longrightarrow> (strong \<longrightarrow> \<not> sint x < 0 \<longrightarrow> array_assertion ptr (Suc (unat x)) htd \<longrightarrow> x = 0 \<or> 0 < x) \<and> (\<not> strong \<longrightarrow> \<not> sint x < 0 \<longrightarrow> array_assertion ptr (unat x) htd \<longrightarrow> x = 0 \<or> 0 < x)) \<and> (\<not> Suc (unat x) < 2 ^ size x \<longrightarrow> (strong \<longrightarrow> \<not> sint x < 0 \<longrightarrow> array_assertion ptr (Suc (unat x)) htd \<longrightarrow> x = 0 \<or> 0 < x \<and> array_assertion ptr (Suc (unat x) - 2 ^ size x) htd) \<and> (\<not> strong \<longrightarrow> \<not> sint x < 0 \<longrightarrow> array_assertion ptr (unat x) htd \<longrightarrow> x = 0 \<or> 0 < x)) proof (prove)
goal (1 subgoal):
 1. (strong \<longrightarrow> \<not> sint x < 0 \<longrightarrow> array_assertion ptr (Suc (unat x)) htd \<longrightarrow> x = 0 \<or> 0 < x) \<and> (\<not> strong \<longrightarrow> \<not> sint x < 0 \<longrightarrow> array_assertion ptr (unat x) htd \<longrightarrow> x = 0 \<or> 0 < x) proof (prove)
goal:
No subgoals!
theory CommonOpsLemmas

lemma word32_31_less:
  "31 < len_of TYPE (32 signed)" "31 > (0 :: nat)"
  "31 < len_of TYPE (32)" "31 > (0 :: nat)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (31 < LENGTH(32 signed) &&& 0 < 31) &&& 31 < LENGTH(32) &&& 0 < 31
theory CommonOpsLemmas

lemma word64_31_less:
  "31 < len_of TYPE (64 signed)" "31 > (0 :: nat)"
  "31 < len_of TYPE (64)" "31 > (0 :: nat)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (31 < LENGTH(64 signed) &&& 0 < 31) &&& 31 < LENGTH(64) &&& 0 < 31