theory Move_C

lemma reset_name_seq_bound_helper:
  fixes sz
  fixes v :: "('a :: len) word"
  defines "CP \<equiv> (\<lambda>n. ~ (v && ~~ mask sz) + of_nat n * (-1 << sz) =
                          ((-1 :: 'a word) << sz))"
      and "n \<equiv> Suc (unat (shiftR v sz))"
  assumes vsz: "v + 1 < 2 ^ (len_of TYPE('a) - 1)" "2 ^ sz \<noteq> (0 :: 'a word)"
    and vless: "v < v'"
  shows "(\<not> CP n \<and> (\<forall>n' < n. CP n'))" apply (clarsimp simp: shiftl_t2n field_simps less_Suc_eq_le CP_def n_def) apply (simp add: shiftr_shiftl1[where b=sz and c=sz, simplified, symmetric]
                   shiftl_t2n) apply (clarsimp simp: word_sle_msb_le shiftl_t2n[symmetric]) apply (case_tac n', simp_all) apply (cut_tac vsz(1) order_less_le_trans[OF vless max_word_max]) apply (clarsimp simp: shiftr_shiftl1 dest!: word_add_no_overflow) apply (drule_tac f="\<lambda>x. x - 2 ^ sz" in arg_cong, simp) apply (metis less_irrefl order_le_less_trans order_less_trans
                word_and_le2[where a=v and y="~~ mask sz"]
                word_two_power_neg_ineq[OF vsz(2)]) apply (clarsimp simp add: field_simps) apply (drule_tac f="\<lambda>x. shiftr x sz" in arg_cong) apply simp apply (simp add: shiftr_div_2n') apply (simp only: linorder_not_less[symmetric], erule notE) apply (rule order_le_less_trans[OF div_le_mono]) apply (rule_tac b="v * 2 ^ sz" for v in word_unat_less_le,
     simp, rule order_refl) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> CP n \<and> (\<forall>n'<n. CP n') proof (prove)
goal (1 subgoal):
 1. v && ~~ mask sz = (v >> sz) * 2 ^ sz \<and> (\<forall>n'\<le>unat (v >> sz). (v && ~~ mask sz) + 2 ^ sz \<noteq> word_of_nat n' * 2 ^ sz) proof (prove)
goal (1 subgoal):
 1. \<forall>n'\<le>unat (v >> sz). 2 ^ sz * (v >> sz) + 2 ^ sz \<noteq> word_of_nat n' * 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<And>n'. \<lbrakk>n' \<le> unat (v >> sz); (v >> sz << sz) + 2 ^ sz = word_of_nat n' * 2 ^ sz\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>n'. \<lbrakk>(v >> sz << sz) + 2 ^ sz = 0; n' = 0\<rbrakk> \<Longrightarrow> False
 2. \<And>n' nat. \<lbrakk>Suc nat \<le> unat (v >> sz); (v >> sz << sz) + 2 ^ sz = (1 + word_of_nat nat) * 2 ^ sz; n' = Suc nat\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>n'. \<lbrakk>(v >> sz << sz) + 2 ^ sz = 0; n' = 0; v + 1 < 2 ^ (LENGTH('a) - 1); v < - 1\<rbrakk> \<Longrightarrow> False
 2. \<And>n' nat. \<lbrakk>Suc nat \<le> unat (v >> sz); (v >> sz << sz) + 2 ^ sz = (1 + word_of_nat nat) * 2 ^ sz; n' = Suc nat\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(v && ~~ mask sz) + 2 ^ sz = 0; v + 1 < 2 ^ (LENGTH('a) - Suc 0); v < v + 1\<rbrakk> \<Longrightarrow> False
 2. \<And>n' nat. \<lbrakk>Suc nat \<le> unat (v >> sz); (v >> sz << sz) + 2 ^ sz = (1 + word_of_nat nat) * 2 ^ sz; n' = Suc nat\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>v + 1 < 2 ^ (LENGTH('a) - Suc 0); v < v + 1; v && ~~ mask sz = - (2 ^ sz)\<rbrakk> \<Longrightarrow> False
 2. \<And>n' nat. \<lbrakk>Suc nat \<le> unat (v >> sz); (v >> sz << sz) + 2 ^ sz = (1 + word_of_nat nat) * 2 ^ sz; n' = Suc nat\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>n' nat. \<lbrakk>Suc nat \<le> unat (v >> sz); (v >> sz << sz) + 2 ^ sz = (1 + word_of_nat nat) * 2 ^ sz; n' = Suc nat\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>Suc nat \<le> unat (v >> sz); v >> sz << sz = word_of_nat nat * 2 ^ sz\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>Suc nat \<le> unat (v >> sz); v >> sz << sz >> sz = word_of_nat nat * 2 ^ sz >> sz\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>Suc nat \<le> unat (word_of_nat nat * 2 ^ sz >> sz); v >> sz = word_of_nat nat * 2 ^ sz >> sz\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>nat. \<lbrakk>Suc nat \<le> unat (word_of_nat nat * 2 ^ sz) div 2 ^ sz; v >> sz = word_of_nat nat * 2 ^ sz >> sz\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>nat. v >> sz = word_of_nat nat * 2 ^ sz >> sz \<Longrightarrow> unat (word_of_nat nat * 2 ^ sz) div 2 ^ sz < Suc nat proof (prove)
goal (2 subgoals):
 1. \<And>nat. v >> sz = word_of_nat nat * 2 ^ sz >> sz \<Longrightarrow> unat (word_of_nat nat * 2 ^ sz) \<le> ?n29 nat
 2. \<And>nat. v >> sz = word_of_nat nat * 2 ^ sz >> sz \<Longrightarrow> ?n29 nat div 2 ^ sz < Suc nat proof (prove)
goal (1 subgoal):
 1. \<And>nat. v >> sz = word_of_nat nat * 2 ^ sz >> sz \<Longrightarrow> nat * 2 ^ sz div 2 ^ sz < Suc nat proof (prove)
goal:
No subgoals!