kings-crown/FVELER_Isabelle huggingface dataset:
theory Many_More

lemma if_Not_x: "(if p then \<not> x else x) = (p = (\<not> x))" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (if p then \<not> x else x) = (p = (\<not> x))
theory Many_More

lemma if_x_Not: "(if p then x else \<not> x) = (p = x)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (if p then x else \<not> x) = (p = x)
theory Many_More

lemma if_same_and: "(If p x y \<and> If p u v) = (if p then x \<and> u else y \<and> v)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((if p then x else y) \<and> (if p then u else v)) = (if p then x \<and> u else y \<and> v)
theory Many_More

lemma if_same_eq: "(If p x y  = (If p u v)) = (if p then x = u else y = v)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((if p then x else y) = (if p then u else v)) = (if p then x = u else y = v)
theory Many_More

lemma if_same_eq_not: "(If p x y = (\<not> If p u v)) = (if p then x = (\<not> u) else y = (\<not> v))" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((if p then x else y) = (\<not> (if p then u else v))) = (if p then x = (\<not> u) else y = (\<not> v))
theory Many_More

lemma the_elemI: "y = {x} \<Longrightarrow> the_elem y = x" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. y = {x} \<Longrightarrow> the_elem y = x
theory Many_More

lemma nonemptyE: "S \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> S \<Longrightarrow> R) \<Longrightarrow> R" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>S \<noteq> {}; \<And>x. x \<in> S \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
theory Many_More

lemma not_empty_eq:
  "(S \<noteq> {}) = (\<exists>x. x \<in> S)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (S \<noteq> {}) = (\<exists>x. x \<in> S)
theory Many_More

lemma range_subset_lower:
  fixes c :: "'a ::linorder"
  shows "\<lbrakk> {a..b} \<subseteq> {c..d}; x \<in> {a..b} \<rbrakk> \<Longrightarrow> c \<le> a" apply (frule (1) subsetD) apply (rule classical) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{a..b} \<subseteq> {c..d}; x \<in> {a..b}\<rbrakk> \<Longrightarrow> c \<le> a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{a..b} \<subseteq> {c..d}; x \<in> {a..b}; x \<in> {c..d}\<rbrakk> \<Longrightarrow> c \<le> a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{a..b} \<subseteq> {c..d}; x \<in> {a..b}; x \<in> {c..d}; \<not> c \<le> a\<rbrakk> \<Longrightarrow> c \<le> a proof (prove)
goal:
No subgoals!
theory Many_More

lemma range_subset_upper:
  fixes c :: "'a ::linorder"
  shows "\<lbrakk> {a..b} \<subseteq> {c..d}; x \<in> {a..b} \<rbrakk> \<Longrightarrow> b \<le> d" apply (frule (1) subsetD) apply (rule classical) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{a..b} \<subseteq> {c..d}; x \<in> {a..b}\<rbrakk> \<Longrightarrow> b \<le> d proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{a..b} \<subseteq> {c..d}; x \<in> {a..b}; x \<in> {c..d}\<rbrakk> \<Longrightarrow> b \<le> d proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{a..b} \<subseteq> {c..d}; x \<in> {a..b}; x \<in> {c..d}; \<not> b \<le> d\<rbrakk> \<Longrightarrow> b \<le> d proof (prove)
goal:
No subgoals!
theory Many_More

lemma range_subset_eq:
  fixes a::"'a::linorder"
  assumes non_empty: "a \<le> b"
  shows "({a..b} \<subseteq> {c..d}) = (c \<le> a \<and> b \<le> d)" apply (insert non_empty) apply (rule iffI) apply (frule range_subset_lower [where x=a], simp) apply (drule range_subset_upper [where x=a], simp) apply simp apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ({a..b} \<subseteq> {c..d}) = (c \<le> a \<and> b \<le> d) proof (prove)
goal (1 subgoal):
 1. a \<le> b \<Longrightarrow> ({a..b} \<subseteq> {c..d}) = (c \<le> a \<and> b \<le> d) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<le> b; {a..b} \<subseteq> {c..d}\<rbrakk> \<Longrightarrow> c \<le> a \<and> b \<le> d
 2. \<lbrakk>a \<le> b; c \<le> a \<and> b \<le> d\<rbrakk> \<Longrightarrow> {a..b} \<subseteq> {c..d} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<le> b; {a..b} \<subseteq> {c..d}; c \<le> a\<rbrakk> \<Longrightarrow> c \<le> a \<and> b \<le> d
 2. \<lbrakk>a \<le> b; c \<le> a \<and> b \<le> d\<rbrakk> \<Longrightarrow> {a..b} \<subseteq> {c..d} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<le> b; c \<le> a; b \<le> d\<rbrakk> \<Longrightarrow> c \<le> a \<and> b \<le> d
 2. \<lbrakk>a \<le> b; c \<le> a \<and> b \<le> d\<rbrakk> \<Longrightarrow> {a..b} \<subseteq> {c..d} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<le> b; c \<le> a \<and> b \<le> d\<rbrakk> \<Longrightarrow> {a..b} \<subseteq> {c..d} proof (prove)
goal:
No subgoals!
theory Many_More

lemma range_eq:
  fixes a::"'a::linorder"
  assumes non_empty: "a \<le> b"
  shows "({a..b} = {c..d}) = (a = c \<and> b = d)" by (metis atLeastatMost_subset_iff eq_iff non_empty)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ({a..b} = {c..d}) = (a = c \<and> b = d)
theory Many_More

lemma range_subsetI:
  fixes x :: "'a :: order"
  assumes xX: "X \<le> x"
  and     yY: "y \<le> Y"
  shows   "{x .. y} \<subseteq> {X .. Y}" using xX yY by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {x..y} \<subseteq> {X..Y} proof (prove)
using this:
X \<le> x
y \<le> Y

goal (1 subgoal):
 1. {x..y} \<subseteq> {X..Y}
theory Many_More

lemma int_not_emptyD:
  "A \<inter> B \<noteq> {} \<Longrightarrow> \<exists>x. x \<in> A \<and> x \<in> B" by (erule contrapos_np, clarsimp simp: disjoint_iff_not_equal)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. A \<inter> B \<noteq> {} \<Longrightarrow> \<exists>x. x \<in> A \<and> x \<in> B
theory Many_More

lemma sum_map_simps[simp]:
  "sum_map f g (Inl v) = Inl (f v)"
  "sum_map f g (Inr w) = Inr (g w)" by (simp add: sum_map_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sum_map f g (Inl v) = Inl (f v) &&& sum_map f g (Inr w) = Inr (g w)
theory Many_More

lemma CollectPairFalse [iff]:
  "{(a,b). False} = {}" by (simp add: split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {(a, b). False} = {}
theory Many_More

lemma if_conj_dist:
  "((if b then w else x) \<and> (if b then y else z) \<and> X) =
  ((if b then w \<and> y else x \<and> z) \<and> X)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((if b then w else x) \<and> (if b then y else z) \<and> X) = ((if b then w \<and> y else x \<and> z) \<and> X)
theory Many_More

lemma if_P_True1:
  "Q \<Longrightarrow> (if P then True else Q)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Q \<Longrightarrow> if P then True else Q
theory Many_More

lemma if_P_True2:
  "Q \<Longrightarrow> (if P then Q else True)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Q \<Longrightarrow> if P then Q else True
theory Many_More

lemma nat_min_simps:
  "(a::nat) \<le> b \<Longrightarrow> min b a = a"
  "a \<le> b \<Longrightarrow> min a b = a" by simp_all

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (a \<le> b \<Longrightarrow> min b a = a) &&& (a \<le> b \<Longrightarrow> min a b = a)
theory Many_More

lemma pl_pl_rels: "a + b = c + d \<Longrightarrow> a \<ge> c \<and> b \<le> d \<or> a \<le> c \<and> b \<ge> d"
  for a b c d :: nat by arith

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a + b = c + d \<Longrightarrow> c \<le> a \<and> b \<le> d \<or> a \<le> c \<and> d \<le> b
theory Many_More

lemma diff_le_eq': "a - b \<le> c \<longleftrightarrow> a \<le> b + c"
  for a b c :: int by arith

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (a - b \<le> c) = (a \<le> b + c)
theory Many_More

lemma zless2: "0 < (2 :: int)" by (fact zero_less_numeral)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < 2
theory Many_More

lemma zless2p: "0 < (2 ^ n :: int)" by arith

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < 2 ^ n
theory Many_More

lemma zle2p: "0 \<le> (2 ^ n :: int)" by arith

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 \<le> 2 ^ n
theory Many_More

lemma ex_eq_or: "(\<exists>m. n = Suc m \<and> (m = k \<or> P m)) \<longleftrightarrow> n = Suc k \<or> (\<exists>m. n = Suc m \<and> P m)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<exists>m. n = Suc m \<and> (m = k \<or> P m)) = (n = Suc k \<or> (\<exists>m. n = Suc m \<and> P m))
theory Many_More

lemma power_minus_simp: "0 < n \<Longrightarrow> a ^ n = a * a ^ (n - 1)" by (auto dest: gr0_implies_Suc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> a ^ n = a * a ^ (n - 1)
theory Many_More

lemma n2s_ths:
  \<open>2 + n = Suc (Suc n)\<close>
  \<open>n + 2 = Suc (Suc n)\<close> by (fact add_2_eq_Suc add_2_eq_Suc')+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 2 + n = Suc (Suc n) &&& n + 2 = Suc (Suc n)
theory Many_More

lemma s2n_ths:
  \<open>Suc (Suc n) = 2 + n\<close>
  \<open>Suc (Suc n) = n + 2\<close> by simp_all

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Suc (Suc n) = 2 + n &&& Suc (Suc n) = n + 2
theory Many_More

lemma gt_or_eq_0: "0 < y \<or> 0 = y"
  for y :: nat by arith

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < y \<or> 0 = y
theory Many_More

lemma sum_imp_diff: "j = k + i \<Longrightarrow> j - i = k"
  for k :: nat by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. j = k + i \<Longrightarrow> j - i = k
theory Many_More

lemma le_diff_eq': "a \<le> c - b \<longleftrightarrow> b + a \<le> c"
  for a b c :: int by arith

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (a \<le> c - b) = (b + a \<le> c)
theory Many_More

lemma less_diff_eq': "a < c - b \<longleftrightarrow> b + a < c"
  for a b c :: int by arith

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (a < c - b) = (b + a < c)
theory Many_More

lemma diff_less_eq': "a - b < c \<longleftrightarrow> a < b + c"
  for a b c :: int by arith

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (a - b < c) = (a < b + c)
theory Many_More

lemma minus_eq: "m - k = m \<longleftrightarrow> k = 0 \<or> m = 0"
  for k m :: nat by arith

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (m - k = m) = (k = 0 \<or> m = 0)
theory Many_More

lemma pl_pl_mm: "a + b = c + d \<Longrightarrow> a - c = d - b"
  for a b c d :: nat by arith

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a + b = c + d \<Longrightarrow> a - c = d - b
theory Many_More

lemma less_le_mult': "w * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> (w + 1) * c \<le> b * c"
  for b c w :: int apply (rule mult_right_mono) apply (rule zless_imp_add1_zle) apply (erule (1) mult_right_less_imp_less) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w * c < b * c; 0 \<le> c\<rbrakk> \<Longrightarrow> (w + 1) * c \<le> b * c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>w * c < b * c; 0 \<le> c\<rbrakk> \<Longrightarrow> w + 1 \<le> b
 2. \<lbrakk>w * c < b * c; 0 \<le> c\<rbrakk> \<Longrightarrow> 0 \<le> c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>w * c < b * c; 0 \<le> c\<rbrakk> \<Longrightarrow> w < b
 2. \<lbrakk>w * c < b * c; 0 \<le> c\<rbrakk> \<Longrightarrow> 0 \<le> c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w * c < b * c; 0 \<le> c\<rbrakk> \<Longrightarrow> 0 \<le> c proof (prove)
goal:
No subgoals!
theory Many_More

lemma less_le_mult: "w * c < b * c \<Longrightarrow> 0 \<le> c \<Longrightarrow> w * c + c \<le> b * c"
  for b c w :: int using less_le_mult' [of w c b] by (simp add: algebra_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w * c < b * c; 0 \<le> c\<rbrakk> \<Longrightarrow> w * c + c \<le> b * c proof (prove)
using this:
\<lbrakk>w * c < b * c; 0 \<le> c\<rbrakk> \<Longrightarrow> (w + 1) * c \<le> b * c

goal (1 subgoal):
 1. \<lbrakk>w * c < b * c; 0 \<le> c\<rbrakk> \<Longrightarrow> w * c + c \<le> b * c
theory Many_More

lemma gen_minus: "0 < n \<Longrightarrow> f n = f (Suc (n - 1))" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> f n = f (Suc (n - 1))
theory Many_More

lemma mpl_lem: "j \<le> i \<Longrightarrow> k < j \<Longrightarrow> i - j + k < i"
  for i j k :: nat by arith

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>j \<le> i; k < j\<rbrakk> \<Longrightarrow> i - j + k < i
theory Many_More

lemma given_quot: "f > 0 \<Longrightarrow> (f * l + (f - 1)) div f = l"
  for f l :: nat by (rule div_nat_eqI) (simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < f \<Longrightarrow> (f * l + (f - 1)) div f = l
theory Many_More

lemma given_quot_alt: "f > 0 \<Longrightarrow> (l * f + f - Suc 0) div f = l"
  for f l :: nat apply (frule given_quot) apply (rule trans) prefer 2 apply (erule asm_rl) apply (rule_tac f="\<lambda>n. n div f" in arg_cong) apply (simp add : ac_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < f \<Longrightarrow> (l * f + f - Suc 0) div f = l proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < f; (f * ?l + (f - 1)) div f = ?l\<rbrakk> \<Longrightarrow> (l * f + f - Suc 0) div f = l proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < f; (f * ?l + (f - 1)) div f = ?l\<rbrakk> \<Longrightarrow> (l * f + f - Suc 0) div f = ?s2
 2. \<lbrakk>0 < f; (f * ?l + (f - 1)) div f = ?l\<rbrakk> \<Longrightarrow> ?s2 = l proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < f; (f * ?l + (f - 1)) div f = ?l\<rbrakk> \<Longrightarrow> ?s2 = l
 2. \<lbrakk>0 < f; (f * ?l + (f - 1)) div f = ?l\<rbrakk> \<Longrightarrow> (l * f + f - Suc 0) div f = ?s2 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < f; (f * l + (f - 1)) div f = l\<rbrakk> \<Longrightarrow> (l * f + f - Suc 0) div f = (f * l + (f - 1)) div f proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < f; (f * l + (f - 1)) div f = l\<rbrakk> \<Longrightarrow> l * f + f - Suc 0 = f * l + (f - 1) proof (prove)
goal:
No subgoals!
theory Many_More

lemma x_power_minus_1:
  fixes x :: "'a :: {ab_group_add, power, numeral, one}"
  shows "x + (2::'a) ^ n - (1::'a) = x + (2 ^ n - 1)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x + (2::'a) ^ n - (1::'a) = x + ((2::'a) ^ n - (1::'a))
theory Many_More

lemma nat_diff_add:
  fixes i :: nat
  shows "\<lbrakk> i + j = k \<rbrakk> \<Longrightarrow> i = k - j" by arith

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. i + j = k \<Longrightarrow> i = k - j
theory Many_More

lemma pow_2_gt: "n \<ge> 2 \<Longrightarrow> (2::int) < 2 ^ n" by (induct n) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 2 \<le> n \<Longrightarrow> 2 < 2 ^ n
theory Many_More

lemma sum_to_zero:
  "(a :: 'a :: ring) + b = 0 \<Longrightarrow> a = (- b)" by (drule arg_cong[where f="\<lambda> x. x - a"], simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a + b = (0::'a) \<Longrightarrow> a = - b
theory Many_More

lemma arith_is_1:
  "\<lbrakk> x \<le> Suc 0; x > 0 \<rbrakk> \<Longrightarrow> x = 1" by arith

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> Suc 0; 0 < x\<rbrakk> \<Longrightarrow> x = 1
theory Many_More

lemma suc_le_pow_2:
  "1 < (n::nat) \<Longrightarrow> Suc n < 2 ^ n" by (induct n; clarsimp)
     (case_tac "n = 1"; clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 1 < n \<Longrightarrow> Suc n < 2 ^ n
theory Many_More

lemma nat_le_Suc_less_imp:
  "x < y \<Longrightarrow> x \<le> y - Suc 0" by arith

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x < y \<Longrightarrow> x \<le> y - Suc 0
theory Many_More

lemma power_sub_int:
  "\<lbrakk> m \<le> n; 0 < b \<rbrakk> \<Longrightarrow> b ^ n div b ^ m = (b ^ (n - m) :: int)" apply (subgoal_tac "\<exists>n'. n = m + n'") apply (clarsimp simp: power_add) apply (rule exI[where x="n - m"]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<le> n; 0 < b\<rbrakk> \<Longrightarrow> b ^ n div b ^ m = b ^ (n - m) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m \<le> n; 0 < b; \<exists>n'. n = m + n'\<rbrakk> \<Longrightarrow> b ^ n div b ^ m = b ^ (n - m)
 2. \<lbrakk>m \<le> n; 0 < b\<rbrakk> \<Longrightarrow> \<exists>n'. n = m + n' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<le> n; 0 < b\<rbrakk> \<Longrightarrow> \<exists>n'. n = m + n' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<le> n; 0 < b\<rbrakk> \<Longrightarrow> n = m + (n - m) proof (prove)
goal:
No subgoals!
theory Many_More

lemma nat_Suc_less_le_imp:
  "(k::nat) < Suc n \<Longrightarrow> k \<le> n" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. k < Suc n \<Longrightarrow> k \<le> n
theory Many_More

lemma nat_add_less_by_max:
  "\<lbrakk> (x::nat) \<le> xmax ; y < k - xmax \<rbrakk> \<Longrightarrow> x + y < k" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> xmax; y < k - xmax\<rbrakk> \<Longrightarrow> x + y < k
theory Many_More

lemma nat_le_Suc_less:
  "0 < y \<Longrightarrow> (x \<le> y - Suc 0) = (x < y)" by arith

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < y \<Longrightarrow> (x \<le> y - Suc 0) = (x < y)
theory Many_More

lemma nat_power_minus_less:
  "a < 2 ^ (x - n) \<Longrightarrow> (a :: nat) < 2 ^ x" by (erule order_less_le_trans) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a < 2 ^ (x - n) \<Longrightarrow> a < 2 ^ x
theory Many_More

lemma less_le_mult_nat':
  "w * c < b * c ==> 0 \<le> c ==> Suc w * c \<le> b * (c::nat)" apply (rule mult_right_mono) apply (rule Suc_leI) apply (erule (1) mult_right_less_imp_less) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w * c < b * c; 0 \<le> c\<rbrakk> \<Longrightarrow> Suc w * c \<le> b * c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>w * c < b * c; 0 \<le> c\<rbrakk> \<Longrightarrow> Suc w \<le> b
 2. \<lbrakk>w * c < b * c; 0 \<le> c\<rbrakk> \<Longrightarrow> 0 \<le> c proof (prove)
goal (2 subgoals):
 1. \<lbrakk>w * c < b * c; 0 \<le> c\<rbrakk> \<Longrightarrow> w < b
 2. \<lbrakk>w * c < b * c; 0 \<le> c\<rbrakk> \<Longrightarrow> 0 \<le> c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w * c < b * c; 0 \<le> c\<rbrakk> \<Longrightarrow> 0 \<le> c proof (prove)
goal:
No subgoals!
theory Many_More

lemma less_le_mult_nat:
  \<open>0 < c \<and> w < b \<Longrightarrow> c + w * c \<le> b * c\<close> for b c w :: nat using less_le_mult_nat' [of w c b] by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < c \<and> w < b \<Longrightarrow> c + w * c \<le> b * c proof (prove)
using this:
\<lbrakk>w * c < b * c; 0 \<le> c\<rbrakk> \<Longrightarrow> Suc w * c \<le> b * c

goal (1 subgoal):
 1. 0 < c \<and> w < b \<Longrightarrow> c + w * c \<le> b * c
theory Many_More

lemma p_assoc_help:
  fixes p :: "'a::{ring,power,numeral,one}"
  shows "p + 2^sz - 1 = p + (2^sz - 1)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. p + (2::'a) ^ sz - (1::'a) = p + ((2::'a) ^ sz - (1::'a))
theory Many_More

lemma pow_mono_leq_imp_lt:
  "x \<le> y \<Longrightarrow> x < 2 ^ y" by (simp add: le_less_trans)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> x < 2 ^ y
theory Many_More

lemma small_powers_of_2:
  "x \<ge> 3 \<Longrightarrow> x < 2 ^ (x - 1)" by (induct x; simp add: suc_le_pow_2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 3 \<le> x \<Longrightarrow> x < 2 ^ (x - 1)
theory Many_More

lemma nat_less_power_trans2:
  fixes n :: nat
  shows "\<lbrakk>n < 2 ^ (m - k); k \<le> m\<rbrakk> \<Longrightarrow> n * 2 ^ k  < 2 ^ m" by (subst mult.commute, erule (1) nat_less_power_trans)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 2 ^ (m - k); k \<le> m\<rbrakk> \<Longrightarrow> n * 2 ^ k < 2 ^ m
theory Many_More

lemma nat_move_sub_le: "(a::nat) + b \<le> c \<Longrightarrow> a \<le> c - b" by arith

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a + b \<le> c \<Longrightarrow> a \<le> c - b
theory Many_More

lemma plus_minus_one_rewrite:
  "v + (- 1 :: ('a :: {ring, one, uminus})) \<equiv> v - 1" by (simp add: field_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. v + - (1::'a) \<equiv> v - (1::'a)
theory Many_More

lemma Suc_0_lt_2p_len_of: "Suc 0 < 2 ^ LENGTH('a :: len)" by (metis One_nat_def len_gt_0 lessI numeral_2_eq_2 one_less_power)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Suc 0 < 2 ^ LENGTH('a)
theory Many_More

lemma bin_rest_code: "i div 2 = drop_bit 1 i" for i :: int by (simp add: drop_bit_eq_div)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. i div 2 = drop_bit 1 i
theory More_Word_Operations

lemma alignUp_unfold:
  \<open>alignUp w n = (w + mask n) AND NOT (mask n)\<close> by (simp add: alignUp_def mask_eq_exp_minus_1 add_mask_fold)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. alignUp w n = w + mask n AND NOT (mask n)
theory More_Word_Operations

lemma word_ctz_unfold:
  \<open>word_ctz w = length (takeWhile (Not \<circ> bit w) [0..<LENGTH('a)])\<close> for w :: \<open>'a::len word\<close> by (simp add: word_ctz_def rev_to_bl_eq takeWhile_map)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_ctz w = length (takeWhile (Not \<circ> bit w) [0..<LENGTH('a)])
theory More_Word_Operations

lemma word_ctz_less:
  "w \<noteq> 0 \<Longrightarrow> word_ctz (w :: ('a::len word)) < LENGTH('a)" apply (clarsimp simp: word_ctz_def eq_zero_set_bl) using length_takeWhile_less apply (rule less_le_trans) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. w \<noteq> 0 \<Longrightarrow> word_ctz w < LENGTH('a) proof (prove)
goal (1 subgoal):
 1. True \<in> set (to_bl w) \<Longrightarrow> length (takeWhile Not (rev (to_bl w))) < LENGTH('a) proof (prove)
using this:
\<exists>x\<in>set ?xs. \<not> ?P x \<Longrightarrow> length (takeWhile ?P ?xs) < length ?xs

goal (1 subgoal):
 1. True \<in> set (to_bl w) \<Longrightarrow> length (takeWhile Not (rev (to_bl w))) < LENGTH('a) proof (prove)
goal (2 subgoals):
 1. True \<in> set (to_bl w) \<Longrightarrow> \<exists>x\<in>set (rev (to_bl w)). \<not> \<not> x
 2. True \<in> set (to_bl w) \<Longrightarrow> length (rev (to_bl w)) \<le> LENGTH('a) proof (prove)
goal:
No subgoals!
theory More_Word_Operations

lemma take_bit_word_ctz_eq [simp]:
  \<open>take_bit LENGTH('a) (word_ctz w) = word_ctz w\<close>
  for w :: \<open>'a::len word\<close> apply (simp add: take_bit_nat_eq_self_iff word_ctz_def to_bl_unfold) using length_takeWhile_le apply (rule le_less_trans) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. take_bit LENGTH('a) (word_ctz w) = word_ctz w proof (prove)
goal (1 subgoal):
 1. length (takeWhile Not (map (bit w) [0..<LENGTH('a)])) < 2 ^ LENGTH('a) proof (prove)
using this:
length (takeWhile ?P ?xs) \<le> length ?xs

goal (1 subgoal):
 1. length (takeWhile Not (map (bit w) [0..<LENGTH('a)])) < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. length (map (bit w) [0..<LENGTH('a)]) < 2 ^ LENGTH('a) proof (prove)
goal:
No subgoals!