kings-crown/FVELER_Isabelle huggingface dataset:
theory Bits_Int

lemma eq_mod_iff: "0 < n \<Longrightarrow> b = b mod n \<longleftrightarrow> 0 \<le> b \<and> b < n"
  for b n :: int using pos_mod_sign [of n b] pos_mod_bound [of n b] by (safe, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> (b = b mod n) = (0 \<le> b \<and> b < n) proof (prove)
using this:
0 < n \<Longrightarrow> 0 \<le> b mod n
0 < n \<Longrightarrow> b mod n < n

goal (1 subgoal):
 1. 0 < n \<Longrightarrow> (b = b mod n) = (0 \<le> b \<and> b < n)
theory Bits_Int

lemma split_uint_lem: "bin_split n (uint w) = (a, b) \<Longrightarrow>
    a = take_bit (LENGTH('a) - n) a \<and> b = take_bit (LENGTH('a)) b"
  for w :: "'a::len word" by transfer (simp add: drop_bit_take_bit ac_simps)

\<comment> \<open>limited hom result\<close>

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bin_split n (uint w) = (a, b) \<Longrightarrow> a = take_bit (LENGTH('a) - n) a \<and> b = take_bit LENGTH('a) b
theory Bits_Int

lemma word_cat_hom:
  "LENGTH('a::len) \<le> LENGTH('b::len) + LENGTH('c::len) \<Longrightarrow>
    (word_cat (word_of_int w :: 'b word) (b :: 'c word) :: 'a word) =
    word_of_int ((\<lambda>k n l. concat_bit n l k) w (size b) (uint b))" by transfer (simp add: take_bit_concat_bit_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. LENGTH('a) \<le> LENGTH('b) + LENGTH('c) \<Longrightarrow> word_cat (word_of_int w) b = word_of_int (concat_bit (size b) (uint b) w)
theory Bits_Int

lemma uint_shiftl:
  "uint (push_bit i n) = take_bit (size n) (push_bit i (uint n))" by (simp add: unsigned_push_bit_eq word_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. uint (push_bit i n) = take_bit (size n) (push_bit i (uint n))
theory Bits_Int

lemma bin_mask_conv_pow2:
  "mask n = 2 ^ n - (1 :: int)" by (fact mask_eq_exp_minus_1)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mask n = 2 ^ n - 1
theory Bits_Int

lemma bin_mask_ge0: "mask n \<ge> (0 :: int)" by (fact mask_nonnegative_int)

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

lemma and_bin_mask_conv_mod: "x AND mask n = x mod 2 ^ n"
  for x :: int by (simp flip: take_bit_eq_mod add: take_bit_eq_mask)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x AND mask n = x mod 2 ^ n
theory Bits_Int

lemma bin_mask_numeral:
  "mask (numeral n) = (1 :: int) + 2 * mask (pred_numeral n)" by (fact mask_numeral)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mask (numeral n) = 1 + 2 * mask (pred_numeral n)
theory Bits_Int

lemma bin_sign_mask [simp]: "bin_sign (mask n) = 0" by (simp add: bin_sign_def bin_mask_conv_pow2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bin_sign (mask n) = 0
theory Bits_Int

lemma bin_mask_p1_conv_shift: "mask n + 1 = push_bit n (1 :: int)" by (simp add: bin_mask_conv_pow2 shiftl_int_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mask n + 1 = push_bit n 1
theory Bits_Int

lemma sbintrunc_eq_in_range:
  "((signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n x = x) = (x \<in> range ((signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n))"
  "(x = (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n x) = (x \<in> range ((signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n))" apply (simp_all add: image_def) apply (metis sbintrunc_sbintrunc)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (signed_take_bit n x = x) = (x \<in> range (signed_take_bit n)) &&& (x = signed_take_bit n x) = (x \<in> range (signed_take_bit n)) proof (prove)
goal (2 subgoals):
 1. (signed_take_bit n x = x) = (\<exists>xa. x = signed_take_bit n xa)
 2. (x = signed_take_bit n x) = (\<exists>xa. x = signed_take_bit n xa) proof (prove)
goal:
No subgoals!
theory Bits_Int

lemma sbintrunc_If:
  "- 3 * (2 ^ n) \<le> x \<and> x < 3 * (2 ^ n)
    \<Longrightarrow> (signed_take_bit :: nat \<Rightarrow> int \<Rightarrow> int) n x = (if x < - (2 ^ n) then x + 2 * (2 ^ n)
        else if x \<ge> 2 ^ n then x - 2 * (2 ^ n) else x)" apply (simp add: no_sbintr_alt2, safe) apply (simp add: mod_pos_geq) apply (subst mod_add_self1[symmetric], simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. - 3 * 2 ^ n \<le> x \<and> x < 3 * 2 ^ n \<Longrightarrow> signed_take_bit n x = (if x < - (2 ^ n) then x + 2 * 2 ^ n else if 2 ^ n \<le> x then x - 2 * 2 ^ n else x) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>- (3 * 2 ^ n) \<le> x; x < 3 * 2 ^ n; 2 ^ n \<le> x\<rbrakk> \<Longrightarrow> 2 ^ n + (x + 2 ^ n) mod (2 * 2 ^ n) = x
 2. \<lbrakk>- (3 * 2 ^ n) \<le> x; x < 3 * 2 ^ n; \<not> 2 ^ n \<le> x; x < - (2 ^ n)\<rbrakk> \<Longrightarrow> (x + 2 ^ n) mod (2 * 2 ^ n) = 3 * 2 ^ n + x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>- (3 * 2 ^ n) \<le> x; x < 3 * 2 ^ n; \<not> 2 ^ n \<le> x; x < - (2 ^ n)\<rbrakk> \<Longrightarrow> (x + 2 ^ n) mod (2 * 2 ^ n) = 3 * 2 ^ n + x proof (prove)
goal:
No subgoals!
theory Bits_Int

lemma sint_range':
  \<open>- (2 ^ (LENGTH('a) - Suc 0)) \<le> sint x \<and> sint x < 2 ^ (LENGTH('a) - Suc 0)\<close>
  for x :: \<open>'a::len word\<close> apply transfer using sbintr_ge sbintr_lt apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. - (2 ^ (LENGTH('a) - Suc 0)) \<le> sint x \<and> sint x < 2 ^ (LENGTH('a) - Suc 0) proof (prove)
goal (1 subgoal):
 1. \<And>x. - (2 ^ (LENGTH('a) - Suc 0)) \<le> signed_take_bit (LENGTH('a) - Suc 0) x \<and> signed_take_bit (LENGTH('a) - Suc 0) x < 2 ^ (LENGTH('a) - Suc 0) proof (prove)
using this:
- (2 ^ ?n) \<le> signed_take_bit ?n ?w
signed_take_bit ?n ?w < 2 ^ ?n

goal (1 subgoal):
 1. \<And>x. - (2 ^ (LENGTH('a) - Suc 0)) \<le> signed_take_bit (LENGTH('a) - Suc 0) x \<and> signed_take_bit (LENGTH('a) - Suc 0) x < 2 ^ (LENGTH('a) - Suc 0) proof (prove)
goal:
No subgoals!
theory Bits_Int

lemma signed_arith_eq_checks_to_ord:
  "(sint a + sint b = sint (a + b ))
    = ((a <=s a + b) = (0 <=s b))"
  "(sint a - sint b = sint (a - b ))
    = ((0 <=s a - b) = (b <=s a))"
  "(- sint a = sint (- a)) = (0 <=s (- a) = (a <=s 0))" using sint_range'[where x=a] sint_range'[where x=b] by (simp_all add: sint_word_ariths word_sle_eq word_sless_alt sbintrunc_If)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (sint a + sint b = sint (a + b)) = ((a \<le>s a + b) = (0 \<le>s b)) &&& (sint a - sint b = sint (a - b)) = ((0 \<le>s a - b) = (b \<le>s a)) &&& (- sint a = sint (- a)) = ((0 \<le>s - a) = (a \<le>s 0)) proof (prove)
using this:
- (2 ^ (LENGTH('a) - Suc 0)) \<le> sint a \<and> sint a < 2 ^ (LENGTH('a) - Suc 0)
- (2 ^ (LENGTH('a) - Suc 0)) \<le> sint b \<and> sint b < 2 ^ (LENGTH('a) - Suc 0)

goal (1 subgoal):
 1. (sint a + sint b = sint (a + b)) = ((a \<le>s a + b) = (0 \<le>s b)) &&& (sint a - sint b = sint (a - b)) = ((0 \<le>s a - b) = (b \<le>s a)) &&& (- sint a = sint (- a)) = ((0 \<le>s - a) = (a \<le>s 0))
theory Bits_Int

lemma bintrunc_id:
  "\<lbrakk>m \<le> int n; 0 < m\<rbrakk> \<Longrightarrow> take_bit n m = m" by (simp add: take_bit_int_eq_self_iff le_less_trans)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m \<le> int n; 0 < m\<rbrakk> \<Longrightarrow> take_bit n m = m
theory Bits_Int

lemma bin_cat_cong: "concat_bit n b a = concat_bit m d c"
  if "n = m" "a = c" "take_bit m b = take_bit m d" using that(3) unfolding that(1,2) by (simp add: bin_cat_eq_push_bit_add_take_bit)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. concat_bit n b a = concat_bit m d c proof (prove)
using this:
take_bit m b = take_bit m d

goal (1 subgoal):
 1. concat_bit n b a = concat_bit m d c proof (prove)
using this:
take_bit m b = take_bit m d

goal (1 subgoal):
 1. concat_bit m b c = concat_bit m d c
theory Bits_Int

lemma bin_cat_eqD1: "concat_bit n b a = concat_bit n d c \<Longrightarrow> a = c" by (metis drop_bit_bin_cat_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. concat_bit n b a = concat_bit n d c \<Longrightarrow> a = c
theory Bits_Int

lemma bin_cat_eqD2: "concat_bit n b a = concat_bit n d c \<Longrightarrow> take_bit n b = take_bit n d" by (metis take_bit_bin_cat_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. concat_bit n b a = concat_bit n d c \<Longrightarrow> take_bit n b = take_bit n d
theory Bits_Int

lemma bin_cat_inj: "(concat_bit n b a) = concat_bit n d c \<longleftrightarrow> a = c \<and> take_bit n b = take_bit n d" by (auto intro: bin_cat_cong bin_cat_eqD1 bin_cat_eqD2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (concat_bit n b a = concat_bit n d c) = (a = c \<and> take_bit n b = take_bit n d)
theory Bits_Int

lemma bin_sc_pos:
  "0 \<le> i \<Longrightarrow> 0 \<le> bin_sc n b i" by (metis bin_sign_sc sign_Pls_ge_0)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 \<le> i \<Longrightarrow> 0 \<le> set_bit_class.set_bit i n b
theory Typedef_Morphisms

lemma tdD1: "type_definition Rep Abs A \<Longrightarrow> \<forall>x. Rep x \<in> A"
  and tdD2: "type_definition Rep Abs A \<Longrightarrow> \<forall>x. Abs (Rep x) = x"
  and tdD3: "type_definition Rep Abs A \<Longrightarrow> \<forall>y. y \<in> A \<longrightarrow> Rep (Abs y) = y" by (auto simp: type_definition_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (type_definition Rep Abs A \<Longrightarrow> \<forall>x. Rep x \<in> A) &&& (type_definition Rep Abs A \<Longrightarrow> \<forall>x. Abs (Rep x) = x) &&& (type_definition Rep Abs A \<Longrightarrow> \<forall>y. y \<in> A \<longrightarrow> Rep (Abs y) = y)
theory Typedef_Morphisms

lemma td_nat_int: "type_definition int nat (Collect ((\<le>) 0))" unfolding type_definition_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. type_definition int nat (Collect ((\<le>) 0)) proof (prove)
goal (1 subgoal):
 1. (\<forall>x. int x \<in> Collect ((\<le>) 0)) \<and> (\<forall>x. nat (int x) = x) \<and> (\<forall>y. y \<in> Collect ((\<le>) 0) \<longrightarrow> int (nat y) = y)
theory Typedef_Morphisms

lemma Abs_inverse': "r \<in> A \<Longrightarrow> Abs r = a \<Longrightarrow> Rep a = r" by (safe elim!: Abs_inverse)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>r \<in> A; Abs r = a\<rbrakk> \<Longrightarrow> Rep a = r
theory Typedef_Morphisms

lemma Rep_comp_inverse: "Rep \<circ> f = g \<Longrightarrow> Abs \<circ> g = f" using Rep_inverse by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Rep \<circ> f = g \<Longrightarrow> Abs \<circ> g = f proof (prove)
using this:
Abs (Rep ?x) = ?x

goal (1 subgoal):
 1. Rep \<circ> f = g \<Longrightarrow> Abs \<circ> g = f
theory Typedef_Morphisms

lemma Rep_eqD [elim!]: "Rep x = Rep y \<Longrightarrow> x = y" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Rep x = Rep y \<Longrightarrow> x = y
theory Typedef_Morphisms

lemma Rep_inverse': "Rep a = r \<Longrightarrow> Abs r = a" by (safe intro!: Rep_inverse)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Rep a = r \<Longrightarrow> Abs r = a
theory Typedef_Morphisms

lemma comp_Abs_inverse: "f \<circ> Abs = g \<Longrightarrow> g \<circ> Rep = f" using Rep_inverse by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f \<circ> Abs = g \<Longrightarrow> g \<circ> Rep = f proof (prove)
using this:
Abs (Rep ?x) = ?x

goal (1 subgoal):
 1. f \<circ> Abs = g \<Longrightarrow> g \<circ> Rep = f
theory Typedef_Morphisms

lemma set_Rep_Abs: "A = range (Rep \<circ> Abs)" proof (rule set_eqI) show "x \<in> A \<longleftrightarrow> x \<in> range (Rep \<circ> Abs)" for x by (auto dest: Abs_inverse [of x, symmetric]) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. A = range (Rep \<circ> Abs) proof (state)
goal (1 subgoal):
 1. \<And>x. (x \<in> A) = (x \<in> range (Rep \<circ> Abs)) proof (prove)
goal (1 subgoal):
 1. (x \<in> A) = (x \<in> range (Rep \<circ> Abs)) proof (state)
this:
(?x \<in> A) = (?x \<in> range (Rep \<circ> Abs))

goal:
No subgoals!
theory Typedef_Morphisms

lemma Abs_inj_on: "inj_on Abs A" unfolding inj_on_def by (auto dest: Abs_inject [THEN iffD1])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. inj_on Abs A proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>A. \<forall>y\<in>A. Abs x = Abs y \<longrightarrow> x = y
theory Typedef_Morphisms

lemma image: "Abs ` A = UNIV" by (fact Abs_image)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Abs ` A = UNIV
theory Typedef_Morphisms

lemma fns1: "Rep \<circ> fa = fr \<circ> Rep \<or> fa \<circ> Abs = Abs \<circ> fr \<Longrightarrow> Abs \<circ> fr \<circ> Rep = fa" by (auto dest: Rep_comp_inverse elim: comp_Abs_inverse simp: o_assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Rep \<circ> fa = fr \<circ> Rep \<or> fa \<circ> Abs = Abs \<circ> fr \<Longrightarrow> Abs \<circ> fr \<circ> Rep = fa
theory Typedef_Morphisms

lemma fns4: "Rep \<circ> fa \<circ> Abs = fr \<Longrightarrow> Rep \<circ> fa = fr \<circ> Rep \<and> fa \<circ> Abs = Abs \<circ> fr" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Rep \<circ> fa \<circ> Abs = fr \<Longrightarrow> Rep \<circ> fa = fr \<circ> Rep \<and> fa \<circ> Abs = Abs \<circ> fr
theory Typedef_Morphisms

lemma td_conds:
  "norm \<circ> norm = norm \<Longrightarrow>
    fr \<circ> norm = norm \<circ> fr \<longleftrightarrow> norm \<circ> fr \<circ> norm = fr \<circ> norm \<and> norm \<circ> fr \<circ> norm = norm \<circ> fr" apply safe apply (simp_all add: comp_assoc) apply (simp_all add: o_assoc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. norm \<circ> norm = norm \<Longrightarrow> (fr \<circ> norm = norm \<circ> fr) = (norm \<circ> fr \<circ> norm = fr \<circ> norm \<and> norm \<circ> fr \<circ> norm = norm \<circ> fr) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>norm \<circ> norm = norm; fr \<circ> norm = norm \<circ> fr\<rbrakk> \<Longrightarrow> norm \<circ> fr \<circ> norm = fr \<circ> norm
 2. \<lbrakk>norm \<circ> norm = norm; fr \<circ> norm = norm \<circ> fr\<rbrakk> \<Longrightarrow> norm \<circ> fr \<circ> norm = norm \<circ> fr
 3. \<lbrakk>norm \<circ> norm = norm; norm \<circ> fr \<circ> norm = fr \<circ> norm; norm \<circ> fr \<circ> norm = norm \<circ> fr\<rbrakk> \<Longrightarrow> fr \<circ> norm = norm \<circ> fr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>norm \<circ> norm = norm; fr \<circ> norm = norm \<circ> fr\<rbrakk> \<Longrightarrow> norm \<circ> (norm \<circ> fr) = norm \<circ> fr
 2. \<lbrakk>norm \<circ> norm = norm; fr \<circ> norm = norm \<circ> fr\<rbrakk> \<Longrightarrow> norm \<circ> (norm \<circ> fr) = norm \<circ> fr proof (prove)
goal:
No subgoals!
theory Typedef_Morphisms

lemma fn_comm_power: "fa \<circ> tr = tr \<circ> fr \<Longrightarrow> fa ^^ n \<circ> tr = tr \<circ> fr ^^ n" apply (rule ext) apply (induct n) apply (auto dest: fun_cong) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fa \<circ> tr = tr \<circ> fr \<Longrightarrow> fa ^^ n \<circ> tr = tr \<circ> fr ^^ n proof (prove)
goal (1 subgoal):
 1. \<And>x. fa \<circ> tr = tr \<circ> fr \<Longrightarrow> (fa ^^ n \<circ> tr) x = (tr \<circ> fr ^^ n) x proof (prove)
goal (2 subgoals):
 1. \<And>x. fa \<circ> tr = tr \<circ> fr \<Longrightarrow> (fa ^^ 0 \<circ> tr) x = (tr \<circ> fr ^^ 0) x
 2. \<And>n x. \<lbrakk>\<And>x. fa \<circ> tr = tr \<circ> fr \<Longrightarrow> (fa ^^ n \<circ> tr) x = (tr \<circ> fr ^^ n) x; fa \<circ> tr = tr \<circ> fr\<rbrakk> \<Longrightarrow> (fa ^^ Suc n \<circ> tr) x = (tr \<circ> fr ^^ Suc n) x proof (prove)
goal:
No subgoals!
theory Typedef_Morphisms

lemma Abs_norm [simp]: "Abs (norm x) = Abs x" using eq_norm [of x] by (auto elim: Rep_inverse')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Abs (norm x) = Abs x proof (prove)
using this:
Rep (Abs x) = norm x

goal (1 subgoal):
 1. Abs (norm x) = Abs x
theory Typedef_Morphisms

lemma eq_norm': "Rep \<circ> Abs = norm" by (auto simp: eq_norm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Rep \<circ> Abs = norm
theory Typedef_Morphisms

lemma norm_Rep [simp]: "norm (Rep x) = Rep x" by (auto simp: eq_norm' intro: td_th)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. norm (Rep x) = Rep x
theory Typedef_Morphisms

lemma set_iff_norm: "w \<in> A \<longleftrightarrow> w = norm w" by (auto simp: set_Rep_Abs eq_norm' eq_norm [symmetric])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (w \<in> A) = (w = norm w)
theory Typedef_Morphisms

lemma inverse_norm: "Abs n = w \<longleftrightarrow> Rep w = norm n" apply (rule iffI) apply (clarsimp simp add: eq_norm) apply (simp add: eq_norm' [symmetric]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (Abs n = w) = (Rep w = norm n) proof (prove)
goal (2 subgoals):
 1. Abs n = w \<Longrightarrow> Rep w = norm n
 2. Rep w = norm n \<Longrightarrow> Abs n = w proof (prove)
goal (1 subgoal):
 1. Rep w = norm n \<Longrightarrow> Abs n = w proof (prove)
goal:
No subgoals!
theory Typedef_Morphisms

lemma fns5: "Rep \<circ> fa \<circ> Abs = fr \<Longrightarrow> fr \<circ> norm = fr \<and> norm \<circ> fr = fr" by (fold eq_norm') auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Rep \<circ> fa \<circ> Abs = fr \<Longrightarrow> fr \<circ> norm = fr \<and> norm \<circ> fr = fr
theory Typedef_Morphisms

lemma fns2: "Abs \<circ> fr \<circ> Rep = fa \<Longrightarrow> norm \<circ> fr \<circ> norm = fr \<circ> norm \<longleftrightarrow> Rep \<circ> fa = fr \<circ> Rep" apply (fold eq_norm') apply safe prefer 2 apply (simp add: o_assoc) apply (rule ext) apply (drule_tac x="Rep x" in fun_cong) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Abs \<circ> fr \<circ> Rep = fa \<Longrightarrow> (norm \<circ> fr \<circ> norm = fr \<circ> norm) = (Rep \<circ> fa = fr \<circ> Rep) proof (prove)
goal (1 subgoal):
 1. Abs \<circ> fr \<circ> Rep = fa \<Longrightarrow> (Rep \<circ> Abs \<circ> fr \<circ> (Rep \<circ> Abs) = fr \<circ> (Rep \<circ> Abs)) = (Rep \<circ> fa = fr \<circ> Rep) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>fa = Abs \<circ> fr \<circ> Rep; Rep \<circ> Abs \<circ> fr \<circ> (Rep \<circ> Abs) = fr \<circ> (Rep \<circ> Abs)\<rbrakk> \<Longrightarrow> Rep \<circ> (Abs \<circ> fr \<circ> Rep) = fr \<circ> Rep
 2. \<lbrakk>fa = Abs \<circ> fr \<circ> Rep; Rep \<circ> (Abs \<circ> fr \<circ> Rep) = fr \<circ> Rep\<rbrakk> \<Longrightarrow> Rep \<circ> Abs \<circ> fr \<circ> (Rep \<circ> Abs) = fr \<circ> (Rep \<circ> Abs) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>fa = Abs \<circ> fr \<circ> Rep; Rep \<circ> (Abs \<circ> fr \<circ> Rep) = fr \<circ> Rep\<rbrakk> \<Longrightarrow> Rep \<circ> Abs \<circ> fr \<circ> (Rep \<circ> Abs) = fr \<circ> (Rep \<circ> Abs)
 2. \<lbrakk>fa = Abs \<circ> fr \<circ> Rep; Rep \<circ> Abs \<circ> fr \<circ> (Rep \<circ> Abs) = fr \<circ> (Rep \<circ> Abs)\<rbrakk> \<Longrightarrow> Rep \<circ> (Abs \<circ> fr \<circ> Rep) = fr \<circ> Rep proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fa = Abs \<circ> fr \<circ> Rep; Rep \<circ> Abs \<circ> fr \<circ> (Rep \<circ> Abs) = fr \<circ> (Rep \<circ> Abs)\<rbrakk> \<Longrightarrow> Rep \<circ> (Abs \<circ> fr \<circ> Rep) = fr \<circ> Rep proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>fa = Abs \<circ> fr \<circ> Rep; Rep \<circ> Abs \<circ> fr \<circ> (Rep \<circ> Abs) = fr \<circ> (Rep \<circ> Abs)\<rbrakk> \<Longrightarrow> (Rep \<circ> (Abs \<circ> fr \<circ> Rep)) x = (fr \<circ> Rep) x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>fa = Abs \<circ> fr \<circ> Rep; (Rep \<circ> Abs \<circ> fr \<circ> (Rep \<circ> Abs)) (Rep x) = (fr \<circ> (Rep \<circ> Abs)) (Rep x)\<rbrakk> \<Longrightarrow> (Rep \<circ> (Abs \<circ> fr \<circ> Rep)) x = (fr \<circ> Rep) x proof (prove)
goal:
No subgoals!
theory Typedef_Morphisms

lemma fns3: "Abs \<circ> fr \<circ> Rep = fa \<Longrightarrow> norm \<circ> fr \<circ> norm = norm \<circ> fr \<longleftrightarrow> fa \<circ> Abs = Abs \<circ> fr" apply (fold eq_norm') apply safe prefer 2 apply (simp add: comp_assoc) apply (rule ext) apply (drule_tac f="a \<circ> b" for a b in fun_cong) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Abs \<circ> fr \<circ> Rep = fa \<Longrightarrow> (norm \<circ> fr \<circ> norm = norm \<circ> fr) = (fa \<circ> Abs = Abs \<circ> fr) proof (prove)
goal (1 subgoal):
 1. Abs \<circ> fr \<circ> Rep = fa \<Longrightarrow> (Rep \<circ> Abs \<circ> fr \<circ> (Rep \<circ> Abs) = Rep \<circ> Abs \<circ> fr) = (fa \<circ> Abs = Abs \<circ> fr) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>fa = Abs \<circ> fr \<circ> Rep; Rep \<circ> Abs \<circ> fr \<circ> (Rep \<circ> Abs) = Rep \<circ> Abs \<circ> fr\<rbrakk> \<Longrightarrow> Abs \<circ> fr \<circ> Rep \<circ> Abs = Abs \<circ> fr
 2. \<lbrakk>fa = Abs \<circ> fr \<circ> Rep; Abs \<circ> fr \<circ> Rep \<circ> Abs = Abs \<circ> fr\<rbrakk> \<Longrightarrow> Rep \<circ> Abs \<circ> fr \<circ> (Rep \<circ> Abs) = Rep \<circ> Abs \<circ> fr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>fa = Abs \<circ> fr \<circ> Rep; Abs \<circ> fr \<circ> Rep \<circ> Abs = Abs \<circ> fr\<rbrakk> \<Longrightarrow> Rep \<circ> Abs \<circ> fr \<circ> (Rep \<circ> Abs) = Rep \<circ> Abs \<circ> fr
 2. \<lbrakk>fa = Abs \<circ> fr \<circ> Rep; Rep \<circ> Abs \<circ> fr \<circ> (Rep \<circ> Abs) = Rep \<circ> Abs \<circ> fr\<rbrakk> \<Longrightarrow> Abs \<circ> fr \<circ> Rep \<circ> Abs = Abs \<circ> fr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fa = Abs \<circ> fr \<circ> Rep; Rep \<circ> Abs \<circ> fr \<circ> (Rep \<circ> Abs) = Rep \<circ> Abs \<circ> fr\<rbrakk> \<Longrightarrow> Abs \<circ> fr \<circ> Rep \<circ> Abs = Abs \<circ> fr proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>fa = Abs \<circ> fr \<circ> Rep; Rep \<circ> Abs \<circ> fr \<circ> (Rep \<circ> Abs) = Rep \<circ> Abs \<circ> fr\<rbrakk> \<Longrightarrow> (Abs \<circ> fr \<circ> Rep \<circ> Abs) x = (Abs \<circ> fr) x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>fa = Abs \<circ> fr \<circ> Rep; (Rep \<circ> Abs \<circ> fr \<circ> (Rep \<circ> Abs)) (?x7 x) = (Rep \<circ> Abs \<circ> fr) (?x7 x)\<rbrakk> \<Longrightarrow> (Abs \<circ> fr \<circ> Rep \<circ> Abs) x = (Abs \<circ> fr) x proof (prove)
goal:
No subgoals!
theory Typedef_Morphisms

lemma range_norm: "range (Rep \<circ> Abs) = A" by (simp add: set_Rep_Abs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. range (Rep \<circ> Abs) = A
theory Typedef_Morphisms

lemma uints_num: "uints n = {i. 0 \<le> i \<and> i < 2 ^ n}" by (simp add: uints_def range_bintrunc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. uints n = {i. 0 \<le> i \<and> i < 2 ^ n}
theory Typedef_Morphisms

lemma sints_num: "sints n = {i. - (2 ^ (n - 1)) \<le> i \<and> i < 2 ^ (n - 1)}" by (simp add: sints_def range_sbintrunc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sints n = {i. - (2 ^ (n - 1)) \<le> i \<and> i < 2 ^ (n - 1)}
theory Typedef_Morphisms

lemma unats_uints: "unats n = nat ` uints n" by (auto simp: uints_unats image_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unats n = nat ` uints n
theory Typedef_Morphisms

lemma td_ext_uint:
  "td_ext (uint :: 'a word \<Rightarrow> int) word_of_int (uints (LENGTH('a::len)))
    (\<lambda>w::int. w mod 2 ^ LENGTH('a))" apply (unfold td_ext_def') apply transfer apply (simp add: uints_num take_bit_eq_mod) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. td_ext uint word_of_int (uints LENGTH('a)) (\<lambda>w. w mod 2 ^ LENGTH('a)) proof (prove)
goal (1 subgoal):
 1. ((\<forall>x. uint x \<in> uints LENGTH('a)) \<and> (\<forall>x. word_of_int (uint x) = x) \<and> (\<forall>y. y \<in> uints LENGTH('a) \<longrightarrow> uint (word_of_int y) = y)) \<and> (\<forall>x. uint (word_of_int x) = x mod 2 ^ LENGTH('a)) proof (prove)
goal (1 subgoal):
 1. ((\<forall>x. take_bit LENGTH('a) x \<in> uints LENGTH('a)) \<and> (\<forall>x. take_bit LENGTH('a) (take_bit LENGTH('a) x) = take_bit LENGTH('a) x) \<and> (\<forall>y. y \<in> uints LENGTH('a) \<longrightarrow> take_bit LENGTH('a) y = y)) \<and> (\<forall>x. take_bit LENGTH('a) x = x mod 2 ^ LENGTH('a)) proof (prove)
goal:
No subgoals!