theory Bits_Int

lemma bin_sign_cat: "bin_sign ((\<lambda>k n l. concat_bit n l k) x n y) = bin_sign x" proof - have \<open>0 \<le> x\<close> if \<open>0 \<le> x * 2 ^ n + y mod 2 ^ n\<close> proof - have \<open>y mod 2 ^ n < 2 ^ n\<close> using pos_mod_bound [of \<open>2 ^ n\<close> y] by simp then have \<open>\<not> y mod 2 ^ n \<ge> 2 ^ n\<close> by (simp add: less_le) with that have \<open>x \<noteq> - 1\<close> by auto have *: \<open>- 1 \<le> (- (y mod 2 ^ n)) div 2 ^ n\<close> by (simp add: zdiv_zminus1_eq_if) from that have \<open>- (y mod 2 ^ n) \<le> x * 2 ^ n\<close> by simp then have \<open>(- (y mod 2 ^ n)) div 2 ^ n \<le> (x * 2 ^ n) div 2 ^ n\<close> using zdiv_mono1 zero_less_numeral zero_less_power by blast with * have \<open>- 1 \<le> x * 2 ^ n div 2 ^ n\<close> by simp with \<open>x \<noteq> - 1\<close> show ?thesis by simp qed then show ?thesis by (simp add: bin_sign_def not_le not_less bin_cat_eq_push_bit_add_take_bit push_bit_eq_mult take_bit_eq_mod) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bin_sign (concat_bit n y x) = bin_sign x proof (state)
goal (1 subgoal):
 1. bin_sign (concat_bit n y x) = bin_sign x proof (prove)
goal (1 subgoal):
 1. 0 \<le> x proof (state)
goal (1 subgoal):
 1. 0 \<le> x proof (prove)
goal (1 subgoal):
 1. y mod 2 ^ n < 2 ^ n proof (prove)
using this:
0 < 2 ^ n \<Longrightarrow> y mod 2 ^ n < 2 ^ n

goal (1 subgoal):
 1. y mod 2 ^ n < 2 ^ n proof (state)
this:
y mod 2 ^ n < 2 ^ n

goal (1 subgoal):
 1. 0 \<le> x proof (chain)
picking this:
y mod 2 ^ n < 2 ^ n proof (prove)
using this:
y mod 2 ^ n < 2 ^ n

goal (1 subgoal):
 1. \<not> 2 ^ n \<le> y mod 2 ^ n proof (state)
this:
\<not> 2 ^ n \<le> y mod 2 ^ n

goal (1 subgoal):
 1. 0 \<le> x proof (chain)
picking this:
0 \<le> x * 2 ^ n + y mod 2 ^ n
\<not> 2 ^ n \<le> y mod 2 ^ n proof (prove)
using this:
0 \<le> x * 2 ^ n + y mod 2 ^ n
\<not> 2 ^ n \<le> y mod 2 ^ n

goal (1 subgoal):
 1. x \<noteq> - 1 proof (state)
this:
x \<noteq> - 1

goal (1 subgoal):
 1. 0 \<le> x proof (prove)
goal (1 subgoal):
 1. - 1 \<le> - (y mod 2 ^ n) div 2 ^ n proof (state)
this:
- 1 \<le> - (y mod 2 ^ n) div 2 ^ n

goal (1 subgoal):
 1. 0 \<le> x proof (chain)
picking this:
0 \<le> x * 2 ^ n + y mod 2 ^ n proof (prove)
using this:
0 \<le> x * 2 ^ n + y mod 2 ^ n

goal (1 subgoal):
 1. - (y mod 2 ^ n) \<le> x * 2 ^ n proof (state)
this:
- (y mod 2 ^ n) \<le> x * 2 ^ n

goal (1 subgoal):
 1. 0 \<le> x proof (chain)
picking this:
- (y mod 2 ^ n) \<le> x * 2 ^ n proof (prove)
using this:
- (y mod 2 ^ n) \<le> x * 2 ^ n

goal (1 subgoal):
 1. - (y mod 2 ^ n) div 2 ^ n \<le> x * 2 ^ n div 2 ^ n proof (prove)
using this:
- (y mod 2 ^ n) \<le> x * 2 ^ n
\<lbrakk>?a \<le> ?a'; 0 < ?b\<rbrakk> \<Longrightarrow> ?a div ?b \<le> ?a' div ?b
(0::?'a) < numeral ?n
(0::?'a) < ?a \<Longrightarrow> (0::?'a) < ?a ^ ?n

goal (1 subgoal):
 1. - (y mod 2 ^ n) div 2 ^ n \<le> x * 2 ^ n div 2 ^ n proof (state)
this:
- (y mod 2 ^ n) div 2 ^ n \<le> x * 2 ^ n div 2 ^ n

goal (1 subgoal):
 1. 0 \<le> x proof (chain)
picking this:
- 1 \<le> - (y mod 2 ^ n) div 2 ^ n
- (y mod 2 ^ n) div 2 ^ n \<le> x * 2 ^ n div 2 ^ n proof (prove)
using this:
- 1 \<le> - (y mod 2 ^ n) div 2 ^ n
- (y mod 2 ^ n) div 2 ^ n \<le> x * 2 ^ n div 2 ^ n

goal (1 subgoal):
 1. - 1 \<le> x * 2 ^ n div 2 ^ n proof (state)
this:
- 1 \<le> x * 2 ^ n div 2 ^ n

goal (1 subgoal):
 1. 0 \<le> x proof (chain)
picking this:
x \<noteq> - 1
- 1 \<le> x * 2 ^ n div 2 ^ n proof (prove)
using this:
x \<noteq> - 1
- 1 \<le> x * 2 ^ n div 2 ^ n

goal (1 subgoal):
 1. 0 \<le> x proof (state)
this:
0 \<le> x

goal:
No subgoals! proof (state)
this:
0 \<le> x * 2 ^ n + y mod 2 ^ n \<Longrightarrow> 0 \<le> x

goal (1 subgoal):
 1. bin_sign (concat_bit n y x) = bin_sign x proof (chain)
picking this:
0 \<le> x * 2 ^ n + y mod 2 ^ n \<Longrightarrow> 0 \<le> x proof (prove)
using this:
0 \<le> x * 2 ^ n + y mod 2 ^ n \<Longrightarrow> 0 \<le> x

goal (1 subgoal):
 1. bin_sign (concat_bit n y x) = bin_sign x proof (state)
this:
bin_sign (concat_bit n y x) = bin_sign x

goal:
No subgoals!