theory Bits_Int

lemma bin_rsplit_aux_len_le [rule_format] :
  "\<forall>ws m. n \<noteq> 0 \<longrightarrow> ws = bin_rsplit_aux n nw w bs \<longrightarrow>
    length ws \<le> m \<longleftrightarrow> nw + length bs * n \<le> m * n" proof - have *: R
    if d: "i \<le> j \<or> m < j'"
    and R1: "i * k \<le> j * k \<Longrightarrow> R"
    and R2: "Suc m * k' \<le> j' * k' \<Longrightarrow> R"
    for i j j' k k' m :: nat and R using d apply safe apply (rule R1, erule mult_le_mono1) apply (rule R2, erule Suc_le_eq [THEN iffD2 [THEN mult_le_mono1]]) done have **: "0 < sc \<Longrightarrow> sc - n + (n + lb * n) \<le> m * n \<longleftrightarrow> sc + lb * n \<le> m * n"
    for sc m n lb :: nat apply safe apply arith apply (case_tac "sc \<ge> n") apply arith apply (insert linorder_le_less_linear [of m lb]) apply (erule_tac k=n and k'=n in *) apply arith apply simp done show ?thesis apply (induct n nw w bs rule: bin_rsplit_aux.induct) apply (subst bin_rsplit_aux.simps) apply (simp add: ** Let_def split: prod.split) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>ws m. n \<noteq> 0 \<longrightarrow> ws = bin_rsplit_aux n nw w bs \<longrightarrow> (length ws \<le> m) = (nw + length bs * n \<le> m * n) proof (state)
goal (1 subgoal):
 1. \<forall>ws m. n \<noteq> 0 \<longrightarrow> ws = bin_rsplit_aux n nw w bs \<longrightarrow> (length ws \<le> m) = (nw + length bs * n \<le> m * n) proof (prove)
goal (1 subgoal):
 1. R proof (prove)
using this:
i \<le> j \<or> m < j'

goal (1 subgoal):
 1. R proof (prove)
goal (2 subgoals):
 1. i \<le> j \<Longrightarrow> R
 2. m < j' \<Longrightarrow> R proof (prove)
goal (1 subgoal):
 1. m < j' \<Longrightarrow> R proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrakk>?i \<le> ?j \<or> ?m < ?j'; ?i * ?k \<le> ?j * ?k \<Longrightarrow> ?R; Suc ?m * ?k' \<le> ?j' * ?k' \<Longrightarrow> ?R\<rbrakk> \<Longrightarrow> ?R

goal (1 subgoal):
 1. \<forall>ws m. n \<noteq> 0 \<longrightarrow> ws = bin_rsplit_aux n nw w bs \<longrightarrow> (length ws \<le> m) = (nw + length bs * n \<le> m * n) proof (prove)
goal (1 subgoal):
 1. 0 < sc \<Longrightarrow> (sc - n + (n + lb * n) \<le> m * n) = (sc + lb * n \<le> m * n) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < sc; sc - n + (n + lb * n) \<le> m * n\<rbrakk> \<Longrightarrow> sc + lb * n \<le> m * n
 2. \<lbrakk>0 < sc; sc + lb * n \<le> m * n\<rbrakk> \<Longrightarrow> sc - n + (n + lb * n) \<le> m * n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < sc; sc + lb * n \<le> m * n\<rbrakk> \<Longrightarrow> sc - n + (n + lb * n) \<le> m * n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < sc; sc + lb * n \<le> m * n; n \<le> sc\<rbrakk> \<Longrightarrow> sc - n + (n + lb * n) \<le> m * n
 2. \<lbrakk>0 < sc; sc + lb * n \<le> m * n; \<not> n \<le> sc\<rbrakk> \<Longrightarrow> sc - n + (n + lb * n) \<le> m * n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < sc; sc + lb * n \<le> m * n; \<not> n \<le> sc\<rbrakk> \<Longrightarrow> sc - n + (n + lb * n) \<le> m * n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < sc; sc + lb * n \<le> m * n; \<not> n \<le> sc; m \<le> lb \<or> lb < m\<rbrakk> \<Longrightarrow> sc - n + (n + lb * n) \<le> m * n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < sc; sc + lb * n \<le> m * n; \<not> n \<le> sc; m * n \<le> lb * n\<rbrakk> \<Longrightarrow> sc - n + (n + lb * n) \<le> m * n
 2. \<lbrakk>0 < sc; sc + lb * n \<le> m * n; \<not> n \<le> sc; Suc lb * n \<le> m * n\<rbrakk> \<Longrightarrow> sc - n + (n + lb * n) \<le> m * n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < sc; sc + lb * n \<le> m * n; \<not> n \<le> sc; Suc lb * n \<le> m * n\<rbrakk> \<Longrightarrow> sc - n + (n + lb * n) \<le> m * n proof (prove)
goal:
No subgoals! proof (state)
this:
0 < ?sc \<Longrightarrow> (?sc - ?n + (?n + ?lb * ?n) \<le> ?m * ?n) = (?sc + ?lb * ?n \<le> ?m * ?n)

goal (1 subgoal):
 1. \<forall>ws m. n \<noteq> 0 \<longrightarrow> ws = bin_rsplit_aux n nw w bs \<longrightarrow> (length ws \<le> m) = (nw + length bs * n \<le> m * n) proof (prove)
goal (1 subgoal):
 1. \<forall>ws m. n \<noteq> 0 \<longrightarrow> ws = bin_rsplit_aux n nw w bs \<longrightarrow> (length ws \<le> m) = (nw + length bs * n \<le> m * n) proof (prove)
goal (1 subgoal):
 1. \<And>n m c bs. (\<And>x xa y. \<lbrakk>\<not> (m = 0 \<or> n = 0); x = bin_split n c; (xa, y) = x\<rbrakk> \<Longrightarrow> \<forall>ws ma. n \<noteq> 0 \<longrightarrow> ws = bin_rsplit_aux n (m - n) xa (y # bs) \<longrightarrow> (length ws \<le> ma) = (m - n + length (y # bs) * n \<le> ma * n)) \<Longrightarrow> \<forall>ws ma. n \<noteq> 0 \<longrightarrow> ws = bin_rsplit_aux n m c bs \<longrightarrow> (length ws \<le> ma) = (m + length bs * n \<le> ma * n) proof (prove)
goal (1 subgoal):
 1. \<And>n m c bs. (\<And>x xa y. \<lbrakk>\<not> (m = 0 \<or> n = 0); x = bin_split n c; (xa, y) = x\<rbrakk> \<Longrightarrow> \<forall>ws ma. n \<noteq> 0 \<longrightarrow> ws = bin_rsplit_aux n (m - n) xa (y # bs) \<longrightarrow> (length ws \<le> ma) = (m - n + length (y # bs) * n \<le> ma * n)) \<Longrightarrow> \<forall>ws ma. n \<noteq> 0 \<longrightarrow> ws = (if m = 0 \<or> n = 0 then bs else let (a, b) = bin_split n c in bin_rsplit_aux n (m - n) a (b # bs)) \<longrightarrow> (length ws \<le> ma) = (m + length bs * n \<le> ma * n) proof (prove)
goal:
No subgoals! proof (state)
this:
\<forall>ws m. n \<noteq> 0 \<longrightarrow> ws = bin_rsplit_aux n nw w bs \<longrightarrow> (length ws \<le> m) = (nw + length bs * n \<le> m * n)

goal:
No subgoals!