kings-crown/FVELER_Isabelle huggingface dataset:
theory InvocationLabels_H

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

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

lemma of_nat_size[simp]:
  "of_nat (size x) = (x::'a)" by (cases x rule: Abs_cases) (clarsimp simp: Abs_inverse of_int_eq size_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. of_nat (size x) = x
theory More_Numeral_Type

lemma size_of_nat[simp]:
  "size (of_nat x :: 'a) = nat (int x mod n)" by (simp add: Rep_Abs_mod of_nat_eq size0 size_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. size (of_nat x) = nat (int x mod n)
theory More_Numeral_Type

lemma zero_less_eq[simp]:
  "0 \<le> (x :: 'a)" using Rep by (simp add: less_eq_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> x proof (prove)
using this:
Rep ?x \<in> {0..<n}

goal (1 subgoal):
 1. (0::'a) \<le> x
theory More_Numeral_Type

lemma zero_less_one[simp,intro!]:
  "0 < (1::'a)" by (simp add: less_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (0::'a) < (1::'a)
theory More_Numeral_Type

lemma zero_least[simp,intro]:
  "(x::'a) < y \<Longrightarrow> 0 < y" by (simp add: le_less_trans)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x < y \<Longrightarrow> (0::'a) < y
theory More_Numeral_Type

lemma not_less_zero_bit0[simp]:
  "\<not> (x::'a) < 0" by (simp add: not_less)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> x < (0::'a)
theory More_Numeral_Type

lemma one_leq[simp]:
  "(1 \<le> x) = (0 < (x::'a))" using less_def less_eq_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((1::'a) \<le> x) = ((0::'a) < x) proof (prove)
using this:
(?a < ?b) = (Rep ?a < Rep ?b)
(?a \<le> ?b) = (Rep ?a \<le> Rep ?b)

goal (1 subgoal):
 1. ((1::'a) \<le> x) = ((0::'a) < x)
theory More_Numeral_Type

lemma less_eq_0[simp]:
  "(x \<le> 0) = (x = (0::'a))" by (simp add: antisym)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x \<le> (0::'a)) = (x = (0::'a))
theory More_Numeral_Type

lemma size_less[simp]:
  "(size (x::'a) < size y) = (x < y)" by (cases x rule: Abs_cases, cases y rule: Abs_cases) (auto simp: Abs_inverse definitions)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (size x < size y) = (x < y)
theory More_Numeral_Type

lemma size_inj[simp]:
  "(size (x::'a) = size y) = (x = y)" by (metis of_nat_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (size x = size y) = (x = y)
theory More_Numeral_Type

lemma size_less_eq[simp]:
  "(size (x::'a) \<le> size y) = (x \<le> y)" by (auto simp: le_eq_less_or_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (size x \<le> size y) = (x \<le> y)
theory More_Numeral_Type

lemma size_0[simp]:
  "size (0::'a) = 0" by (simp add: size_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. size (0::'a) = 0
theory More_Numeral_Type

lemma size_1[simp]:
  "size (1::'a) = 1" by (simp add: size_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. size (1::'a) = 1
theory More_Numeral_Type

lemma pred[simp,intro!]:
  "0 < (x::'a) \<Longrightarrow> x - 1 < x" by (auto intro!: minus_less)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (0::'a) < x \<Longrightarrow> x - (1::'a) < x
theory More_Numeral_Type

lemma minus1_leq:
  "\<lbrakk> x - 1 \<le> y; y < x \<rbrakk> \<Longrightarrow> (y::'a) = x-1" by (smt Rep_1 Rep_Abs_mod Rep_less_n less_def diff_def int_mod_ge le_neq_trans)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x - (1::'a) \<le> y; y < x\<rbrakk> \<Longrightarrow> y = x - (1::'a)
theory More_Numeral_Type

lemma max_bound_leq[simp,intro!]:
  "(x::'a) \<le> -1" by (smt Rep_1 Rep_Abs_mod Rep_less_n less_eq_def int_mod_ge' minus_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<le> - (1::'a)
theory More_Numeral_Type

lemma max_bound_neq_conv[simp]:
  "(x \<noteq> -1) = ((x::'a) < -1)" using le_neq_trans by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x \<noteq> - (1::'a)) = (x < - (1::'a)) proof (prove)
using this:
\<lbrakk>?a \<le> ?b; ?a \<noteq> ?b\<rbrakk> \<Longrightarrow> ?a < ?b

goal (1 subgoal):
 1. (x \<noteq> - (1::'a)) = (x < - (1::'a))
theory More_Numeral_Type

lemma max_bound_leq_conv[simp]:
  "(- 1 \<le> (x::'a)) = (x = - 1)" by (simp add: eq_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (- (1::'a) \<le> x) = (x = - (1::'a))
theory More_Numeral_Type

lemma max_bound_not_less[simp]:
  "\<not> -1 < (x::'a)" using minus1_leq by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> - (1::'a) < x proof (prove)
using this:
\<lbrakk>?x - (1::'a) \<le> ?y; ?y < ?x\<rbrakk> \<Longrightarrow> ?y = ?x - (1::'a)

goal (1 subgoal):
 1. \<not> - (1::'a) < x
theory More_Numeral_Type

lemma minus_1_eq:
  "(-1::'a) = of_nat (nat n - 1)" unfolding definitions using Rep_Abs_1 of_nat_eq size1 by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. - (1::'a) = of_nat (nat n - 1) proof (prove)
goal (1 subgoal):
 1. Abs (- Rep (Abs 1) mod n) = of_nat (nat n - 1) proof (prove)
using this:
Rep (Abs 1) = 1
of_nat ?k = Abs (int ?k mod n)
1 < n

goal (1 subgoal):
 1. Abs (- Rep (Abs 1) mod n) = of_nat (nat n - 1)
theory More_Numeral_Type

lemma n_not_less_Rep[simp]:
  "\<not> n < Rep x" using Rep[of x] by (simp add: not_less)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> n < Rep x proof (prove)
using this:
Rep x \<in> {0..<n}

goal (1 subgoal):
 1. \<not> n < Rep x
theory More_Numeral_Type

lemma size_plus:
  "(x::'a) < x + y \<Longrightarrow> size (x + y) = size x + size y" unfolding definitions Rep_Abs_mod using Rep size0 by (simp flip: nat_add_distrib add: eq_nat_nat_iff pos_mod_sign mod_add_if_z split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x < x + y \<Longrightarrow> size (x + y) = size x + size y proof (prove)
goal (1 subgoal):
 1. Rep x < (Rep x + Rep y) mod n \<Longrightarrow> nat ((Rep x + Rep y) mod n) = nat (Rep x) + nat (Rep y) proof (prove)
using this:
Rep ?x \<in> {0..<n}
0 < n

goal (1 subgoal):
 1. Rep x < (Rep x + Rep y) mod n \<Longrightarrow> nat ((Rep x + Rep y) mod n) = nat (Rep x) + nat (Rep y)
theory More_Numeral_Type

lemma Suc_size[simp]:
  "(x::'a) < x + 1 \<Longrightarrow> size (x + 1) = Suc (size x)" by (simp add: size_plus)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x < x + (1::'a) \<Longrightarrow> size (x + (1::'a)) = Suc (size x)
theory More_Numeral_Type

lemma no_overflow_eq_max_bound:
  "((x::'a) < x + 1) = (x < -1)" unfolding definitions by (smt Rep_Abs_mod Rep_Abs_1 Rep_less_n int_mod_ge int_mod_ge' size0)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x < x + (1::'a)) = (x < - (1::'a)) proof (prove)
goal (1 subgoal):
 1. (Rep x < Rep (Abs ((Rep x + Rep (Abs 1)) mod n))) = (Rep x < Rep (Abs (- Rep (Abs 1) mod n)))
theory More_Numeral_Type

lemma plus_one_leq:
  "x < y \<Longrightarrow> x + 1 \<le> (y::'a)" by (metis add_diff_cancel_right' leq_minus1_less not_le zero_least)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x < y \<Longrightarrow> x + (1::'a) \<le> y
theory More_Numeral_Type

lemma less_uminus:
  "\<lbrakk> - x < y; x \<noteq> 0 \<rbrakk> \<Longrightarrow> - y < (x::'a)" unfolding definitions by (smt Rep_inverse Rep_mod Rep_Abs_mod size0 zmod_zminus1_eq_if)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>- x < y; x \<noteq> (0::'a)\<rbrakk> \<Longrightarrow> - y < x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Rep (Abs (- Rep x mod n)) < Rep y; x \<noteq> Abs 0\<rbrakk> \<Longrightarrow> Rep (Abs (- Rep y mod n)) < Rep x
theory More_Numeral_Type

lemma of_nat_cases[case_names of_nat]:
  "(\<And>m. \<lbrakk> (x::'a) = of_nat m; m < nat n \<rbrakk> \<Longrightarrow> P) \<Longrightarrow> P" by (metis mod_type.Rep_less_n mod_type_axioms nat_mono_iff of_nat_size size0 size_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>m. \<lbrakk>x = of_nat m; m < nat n\<rbrakk> \<Longrightarrow> P) \<Longrightarrow> P
theory More_Numeral_Type

lemma plus_induct[case_names 0 plus]:
  assumes "P (0::'a)"
  assumes suc: "\<And>x. \<lbrakk> P x; x < x + 1 \<rbrakk> \<Longrightarrow> P (x + 1)"
  shows "P x" proof (cases x rule: of_nat_cases) case (of_nat m) have "P (of_nat m)" proof (induct m) case 0 then show ?case using `P 0` by simp next case (Suc m) with `P 0` suc show ?case by (metis diff_add_cancel minus_induct pred) qed with of_nat show ?thesis by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P x proof (state)
goal (1 subgoal):
 1. \<And>m. \<lbrakk>x = of_nat m; m < nat n\<rbrakk> \<Longrightarrow> P x proof (state)
this:
x = of_nat m
m < nat n

goal (1 subgoal):
 1. \<And>m. \<lbrakk>x = of_nat m; m < nat n\<rbrakk> \<Longrightarrow> P x proof (prove)
goal (1 subgoal):
 1. P (of_nat m) proof (state)
goal (2 subgoals):
 1. P (of_nat 0)
 2. \<And>m. P (of_nat m) \<Longrightarrow> P (of_nat (Suc m)) proof (state)
this:


goal (2 subgoals):
 1. P (of_nat 0)
 2. \<And>m. P (of_nat m) \<Longrightarrow> P (of_nat (Suc m)) proof (chain)
picking this:
 proof (prove)
goal (1 subgoal):
 1. P (of_nat 0) proof (prove)
using this:
P (0::'a)

goal (1 subgoal):
 1. P (of_nat 0) proof (state)
this:
P (of_nat 0)

goal (1 subgoal):
 1. \<And>m. P (of_nat m) \<Longrightarrow> P (of_nat (Suc m)) proof (state)
goal (1 subgoal):
 1. \<And>m. P (of_nat m) \<Longrightarrow> P (of_nat (Suc m)) proof (state)
this:
P (of_nat m)

goal (1 subgoal):
 1. \<And>m. P (of_nat m) \<Longrightarrow> P (of_nat (Suc m)) proof (chain)
picking this:
P (0::'a)
\<lbrakk>P ?x; ?x < ?x + (1::'a)\<rbrakk> \<Longrightarrow> P (?x + (1::'a))
P (of_nat m) proof (prove)
using this:
P (0::'a)
\<lbrakk>P ?x; ?x < ?x + (1::'a)\<rbrakk> \<Longrightarrow> P (?x + (1::'a))
P (of_nat m)

goal (1 subgoal):
 1. P (of_nat (Suc m)) proof (state)
this:
P (of_nat (Suc m))

goal:
No subgoals! proof (state)
this:
P (of_nat m)

goal (1 subgoal):
 1. \<And>m. \<lbrakk>x = of_nat m; m < nat n\<rbrakk> \<Longrightarrow> P x proof (chain)
picking this:
x = of_nat m
m < nat n
P (of_nat m) proof (prove)
using this:
x = of_nat m
m < nat n
P (of_nat m)

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

goal:
No subgoals!
theory More_Numeral_Type

lemma tranclp_greater: "(>)\<^sup>+\<^sup>+ = ((>) :: 'a \<Rightarrow> 'a \<Rightarrow> bool)" by(auto simp add: fun_eq_iff intro: less_trans elim: tranclp.induct)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x y. y < x)\<^sup>+\<^sup>+ = (\<lambda>x y. y < x)
theory More_Numeral_Type

lemma finite_UNIV[intro!,simp]:
  "finite (UNIV::'a set)" by (rule card_ge_0_finite) (simp add: card_n size0)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. finite UNIV
theory More_Numeral_Type

lemma finite_greater[simp]:
  "finite {(x, y). y < (x::'a)}" by (rule finite_subset[of _ "UNIV \<times> UNIV"], simp)
     (rule finite_cartesian_product; rule finite_UNIV)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. finite {(x, y). y < x}
theory More_Numeral_Type

lemma wf_greater[intro!,simp]:
  "wf {(x,y). x > (y::'a)}" by (auto simp: trancl_def tranclp_greater intro!: finite_acyclic_wf acyclicI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. wf {(x, y). y < x}
theory More_Numeral_Type

lemma greater_induct[case_names greater]:
  "(\<And>x. (\<And>z. x < z \<Longrightarrow> P z) \<Longrightarrow> P x) \<Longrightarrow> P (x::'a)" by (rule wf_induct_rule, rule wf_greater) fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. (\<And>z. x < z \<Longrightarrow> P z) \<Longrightarrow> P x) \<Longrightarrow> P x
theory More_Numeral_Type

lemma from_top_full_induct[case_names top step]:
  assumes top: "\<And>x. y \<le> x \<Longrightarrow> P (x::'a)"
  assumes step: "\<And>x. \<lbrakk>\<forall>z > x. P z; x < y\<rbrakk> \<Longrightarrow> P x"
  shows "P x" proof (induct x rule: greater_induct) case (greater x) show ?case proof (cases "x < y") case True then show ?thesis by (blast intro: step greater) next case False then show ?thesis by (auto simp: not_less intro: top) qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P x proof (state)
goal (1 subgoal):
 1. \<And>x. (\<And>z. x < z \<Longrightarrow> P z) \<Longrightarrow> P x proof (state)
this:
x < ?z \<Longrightarrow> P ?z

goal (1 subgoal):
 1. \<And>x. (\<And>z. x < z \<Longrightarrow> P z) \<Longrightarrow> P x proof (prove)
goal (1 subgoal):
 1. P x proof (state)
goal (2 subgoals):
 1. x < y \<Longrightarrow> P x
 2. \<not> x < y \<Longrightarrow> P x proof (state)
this:
x < y

goal (2 subgoals):
 1. x < y \<Longrightarrow> P x
 2. \<not> x < y \<Longrightarrow> P x proof (chain)
picking this:
x < y proof (prove)
using this:
x < y

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

goal (1 subgoal):
 1. \<not> x < y \<Longrightarrow> P x proof (state)
goal (1 subgoal):
 1. \<not> x < y \<Longrightarrow> P x proof (state)
this:
\<not> x < y

goal (1 subgoal):
 1. \<not> x < y \<Longrightarrow> P x proof (chain)
picking this:
\<not> x < y proof (prove)
using this:
\<not> x < y

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

goal:
No subgoals! proof (state)
this:
P x

goal:
No subgoals!
theory More_Numeral_Type

lemma neq_0_conv:
  "((x::'a) \<noteq> 0) = (0 < x)" by (meson neqE not_less_zero_bit0)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x \<noteq> (0::'a)) = ((0::'a) < x)
theory More_Numeral_Type

lemma minus_one_leq_less: "\<lbrakk> (x::'a) \<le> y; 0 < x \<rbrakk> \<Longrightarrow> x - 1 < y" using pred by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> y; (0::'a) < x\<rbrakk> \<Longrightarrow> x - (1::'a) < y proof (prove)
using this:
(0::'a) < ?x \<Longrightarrow> ?x - (1::'a) < ?x

goal (1 subgoal):
 1. \<lbrakk>x \<le> y; (0::'a) < x\<rbrakk> \<Longrightarrow> x - (1::'a) < y
theory More_Numeral_Type

lemma size_minus:
  "y \<le> (x::'a) \<Longrightarrow> size (x - y) = size x - size y" unfolding definitions Rep_Abs_mod using Rep size0 by (simp flip: nat_diff_distrib add: eq_nat_nat_iff pos_mod_sign mod_sub_if_z split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. y \<le> x \<Longrightarrow> size (x - y) = size x - size y proof (prove)
goal (1 subgoal):
 1. Rep y \<le> Rep x \<Longrightarrow> nat ((Rep x - Rep y) mod n) = nat (Rep x) - nat (Rep y) proof (prove)
using this:
Rep ?x \<in> {0..<n}
0 < n

goal (1 subgoal):
 1. Rep y \<le> Rep x \<Longrightarrow> nat ((Rep x - Rep y) mod n) = nat (Rep x) - nat (Rep y)
theory More_Numeral_Type

lemma fromEnum_size_bit0[simp]:
  "fromEnum (x::'a::finite bit0) = size x" proof - have "enum ! the_index enum x = x" by (auto intro: nth_the_index) moreover have "the_index enum x < length (enum::'a bit0 list)" by (auto intro: the_index_bounded) moreover { fix y assume "Abs_bit0' (int y) = x" moreover assume "y < 2 * CARD('a)" ultimately have "y = nat (Rep_bit0 x)" by (smt Abs_bit0'_code card_bit0 mod_pos_pos_trivial nat_int of_nat_less_0_iff
              zless_nat_eq_int_zless) } ultimately show ?thesis by (simp  add: fromEnum_def enum_bit0_def size_bit0_def) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fromEnum x = size x proof (state)
goal (1 subgoal):
 1. fromEnum x = size x proof (prove)
goal (1 subgoal):
 1. enum ! the_index enum x = x proof (state)
this:
enum ! the_index enum x = x

goal (1 subgoal):
 1. fromEnum x = size x proof (state)
this:
enum ! the_index enum x = x

goal (1 subgoal):
 1. fromEnum x = size x proof (prove)
goal (1 subgoal):
 1. the_index enum x < length enum proof (state)
this:
the_index enum x < length enum

goal (1 subgoal):
 1. fromEnum x = size x proof (state)
this:
the_index enum x < length enum

goal (1 subgoal):
 1. fromEnum x = size x proof (state)
this:
the_index enum x < length enum

goal (1 subgoal):
 1. fromEnum x = size x proof (state)
goal (1 subgoal):
 1. fromEnum x = size x proof (state)
this:
Abs_bit0' (int y) = x

goal (1 subgoal):
 1. fromEnum x = size x proof (state)
this:
Abs_bit0' (int y) = x

goal (1 subgoal):
 1. fromEnum x = size x proof (state)
this:
y < 2 * CARD('a)

goal (1 subgoal):
 1. fromEnum x = size x proof (chain)
picking this:
Abs_bit0' (int y) = x
y < 2 * CARD('a) proof (prove)
using this:
Abs_bit0' (int y) = x
y < 2 * CARD('a)

goal (1 subgoal):
 1. y = nat (Rep_bit0 x) proof (state)
this:
y = nat (Rep_bit0 x)

goal (1 subgoal):
 1. fromEnum x = size x proof (state)
this:
\<lbrakk>Abs_bit0' (int ?y2) = x; ?y2 < 2 * CARD('a)\<rbrakk> \<Longrightarrow> ?y2 = nat (Rep_bit0 x)

goal (1 subgoal):
 1. fromEnum x = size x proof (chain)
picking this:
enum ! the_index enum x = x
the_index enum x < length enum
\<lbrakk>Abs_bit0' (int ?y2) = x; ?y2 < 2 * CARD('a)\<rbrakk> \<Longrightarrow> ?y2 = nat (Rep_bit0 x) proof (prove)
using this:
enum ! the_index enum x = x
the_index enum x < length enum
\<lbrakk>Abs_bit0' (int ?y2) = x; ?y2 < 2 * CARD('a)\<rbrakk> \<Longrightarrow> ?y2 = nat (Rep_bit0 x)

goal (1 subgoal):
 1. fromEnum x = size x proof (state)
this:
fromEnum x = size x

goal:
No subgoals!
theory More_Numeral_Type

lemma fromEnum_size_bitq[simp]:
  "fromEnum (x::'a::finite bit1) = size x" proof - have "enum ! the_index enum x = x" by (auto intro: nth_the_index) moreover have "the_index enum x < length (enum::'a bit1 list)" by (auto intro: the_index_bounded) moreover { fix y assume "Abs_bit1' (int y) = x" moreover assume "y < Suc (2 * CARD('a))" ultimately have "y = nat (Rep_bit1 x)" by (smt Abs_bit1'_code card_bit1 mod_pos_pos_trivial nat_int of_nat_less_0_iff
              zless_nat_eq_int_zless) } ultimately show ?thesis by (simp add: fromEnum_def enum_bit1_def size_bit1_def del: upt_Suc) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fromEnum x = size x proof (state)
goal (1 subgoal):
 1. fromEnum x = size x proof (prove)
goal (1 subgoal):
 1. enum ! the_index enum x = x proof (state)
this:
enum ! the_index enum x = x

goal (1 subgoal):
 1. fromEnum x = size x proof (state)
this:
enum ! the_index enum x = x

goal (1 subgoal):
 1. fromEnum x = size x proof (prove)
goal (1 subgoal):
 1. the_index enum x < length enum proof (state)
this:
the_index enum x < length enum

goal (1 subgoal):
 1. fromEnum x = size x proof (state)
this:
the_index enum x < length enum

goal (1 subgoal):
 1. fromEnum x = size x proof (state)
this:
the_index enum x < length enum

goal (1 subgoal):
 1. fromEnum x = size x proof (state)
goal (1 subgoal):
 1. fromEnum x = size x proof (state)
this:
Abs_bit1' (int y) = x

goal (1 subgoal):
 1. fromEnum x = size x proof (state)
this:
Abs_bit1' (int y) = x

goal (1 subgoal):
 1. fromEnum x = size x proof (state)
this:
y < Suc (2 * CARD('a))

goal (1 subgoal):
 1. fromEnum x = size x proof (chain)
picking this:
Abs_bit1' (int y) = x
y < Suc (2 * CARD('a)) proof (prove)
using this:
Abs_bit1' (int y) = x
y < Suc (2 * CARD('a))

goal (1 subgoal):
 1. y = nat (Rep_bit1 x) proof (state)
this:
y = nat (Rep_bit1 x)

goal (1 subgoal):
 1. fromEnum x = size x proof (state)
this:
\<lbrakk>Abs_bit1' (int ?y2) = x; ?y2 < Suc (2 * CARD('a))\<rbrakk> \<Longrightarrow> ?y2 = nat (Rep_bit1 x)

goal (1 subgoal):
 1. fromEnum x = size x proof (chain)
picking this:
enum ! the_index enum x = x
the_index enum x < length enum
\<lbrakk>Abs_bit1' (int ?y2) = x; ?y2 < Suc (2 * CARD('a))\<rbrakk> \<Longrightarrow> ?y2 = nat (Rep_bit1 x) proof (prove)
using this:
enum ! the_index enum x = x
the_index enum x < length enum
\<lbrakk>Abs_bit1' (int ?y2) = x; ?y2 < Suc (2 * CARD('a))\<rbrakk> \<Longrightarrow> ?y2 = nat (Rep_bit1 x)

goal (1 subgoal):
 1. fromEnum x = size x proof (state)
this:
fromEnum x = size x

goal:
No subgoals!
theory More_Numeral_Type

lemma minBound_size_bit0[simp]:
  "(minBound::'a::finite bit0) = 0" by (simp add: minBound_def hd_map enum_bit0_def Abs_bit0'_def zero_bit0_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. minBound = 0
theory More_Numeral_Type

lemma minBound_size_bit1[simp]:
  "(minBound::'a::finite bit1) = 0" by (simp add: minBound_def hd_map enum_bit1_def Abs_bit1'_def zero_bit1_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. minBound = 0
theory More_Numeral_Type

lemma maxBound_size_bit0:
  "(maxBound::'a::finite bit0) = of_nat (2 * CARD('a) - 1)" by (simp add: maxBound_def enum_bit0_def last_map Abs_bit0'_def bit0.of_nat_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. maxBound = of_nat (2 * CARD('a) - 1)
theory More_Numeral_Type

lemma maxBound_minus_one_bit0:
  "maxBound = (-1 ::'a::finite bit0)" by (simp add: bit0.definitions bit0.of_nat_eq bit0.Rep_Abs_1 maxBound_size_bit0)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. maxBound = - 1
theory More_Numeral_Type

lemma maxBound_minus_one_bit1:
  "maxBound = (-1 ::'a::finite bit1)" by (simp add: bit1.definitions bit1.of_nat_eq bit1.Rep_Abs_1 zmod_minus1 maxBound_size_bit1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. maxBound = - 1
theory HaskellLib_H

lemma bind_drop_test:
  "foldr bind_drop x (return ()) = sequence_x x" by (rule ext, simp add: sequence_x_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. foldr (\<lambda>x y. do x;
y
od) x (return ()) = sequence_x x
theory HaskellLib_H

lemma sassert_cong[fundef_cong]:
 "\<lbrakk> P = P'; P' \<Longrightarrow> s = s' \<rbrakk> \<Longrightarrow> sassert P s = sassert P' s'" apply (simp add: sassert_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P = P'; P' \<Longrightarrow> s = s'\<rbrakk> \<Longrightarrow> sassert P s = sassert P' s' proof (prove)
goal:
No subgoals!
theory HaskellLib_H

lemma split3_simp[simp]: "split3 f (a, b, c) = f a b c" by (simp add: split3_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. split3 f (a, b, c) = f a b c
theory HaskellLib_H

lemma split4_simp[simp]: "split4 f (a, b, c, d) = f a b c d" by (simp add: split4_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. split4 f (a, b, c, d) = f a b c d
theory HaskellLib_H

lemma split5_simp[simp]: "split5 f (a, b, c, d, e) = f a b c d e" by (simp add: split5_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. split5 f (a, b, c, d, e) = f a b c d e
theory HaskellLib_H

lemma insertBy_length [simp]:
  "length (insertBy f a as) = (1 + length as)" by (induct as) simp_all

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length (insertBy f a as) = 1 + length as
theory HaskellLib_H

lemma sortBy_length:
  "length (sortBy f as) = length as" by (induct as) simp_all

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length (sortBy f as) = length as
theory HaskellLib_H

lemma either_simp[simp]: "either = case_sum" apply (rule ext)+ apply (simp add: either_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. either = case_sum proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb. either x xa xb = (case xb of Inl xa \<Rightarrow> x xa | Inr x \<Rightarrow> xa x) proof (prove)
goal:
No subgoals!
theory HaskellLib_H

lemma fromIntegral_simp1[simp]: "(fromIntegral :: nat \<Rightarrow> ('a :: len) word) = of_nat" by (simp add: fromIntegral_def fromInteger_word toInteger_nat)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fromIntegral = word_of_nat
theory HaskellLib_H

lemma fromIntegral_simp2[simp]: "fromIntegral = unat" by (simp add: fromIntegral_def fromInteger_nat toInteger_word)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fromIntegral = unat
theory HaskellLib_H

lemma fromIntegral_simp3[simp]: "fromIntegral = ucast" unfolding fromIntegral_def fromInteger_word toInteger_word by force

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fromIntegral = UCAST('a \<rightarrow> 'b) proof (prove)
goal (1 subgoal):
 1. word_of_nat \<circ> unat = UCAST('a \<rightarrow> 'b)
theory HaskellLib_H

lemma fromIntegral_simp_nat[simp]: "(fromIntegral :: nat \<Rightarrow> nat) = id" by (simp add: fromIntegral_def fromInteger_nat toInteger_nat)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fromIntegral = id