theory Untyped_AI

lemma inj_bits:
  "\<lbrakk> of_nat x * 2^bits = of_nat y * (2^bits :: machine_word);
     x < bnd; y < bnd; bits \<le> word_bits; bnd \<le> 2 ^ (word_bits - bits) \<rbrakk>
     \<Longrightarrow> of_nat x = (of_nat y :: machine_word)" apply (cases "bits = 0", simp) apply (fold shiftl_t2n [where n=bits, simplified, simplified mult.commute]) apply (simp only: word_bl.Rep_inject[symmetric]
                    bl_shiftl) apply (drule(1) order_less_le_trans)+ apply (drule of_nat_mono_maybe[rotated, where 'a=machine_word_len]) apply (rule power_strict_increasing) apply (simp add: word_bits_def) apply simp apply (drule of_nat_mono_maybe[rotated, where 'a=machine_word_len]) apply (rule power_strict_increasing) apply (simp add: word_bits_def) apply simp apply (simp only: word_unat_power[symmetric]) apply (erule ssubst [OF less_is_drop_replicate])+ apply (simp add: word_bits_def word_size) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>word_of_nat x * 2 ^ bits = word_of_nat y * 2 ^ bits; x < bnd; y < bnd; bits \<le> word_bits; bnd \<le> 2 ^ (word_bits - bits)\<rbrakk> \<Longrightarrow> word_of_nat x = word_of_nat y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>word_of_nat x * 2 ^ bits = word_of_nat y * 2 ^ bits; x < bnd; y < bnd; bits \<le> word_bits; bnd \<le> 2 ^ (word_bits - bits); bits \<noteq> 0\<rbrakk> \<Longrightarrow> word_of_nat x = word_of_nat y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>word_of_nat x << bits = word_of_nat y << bits; x < bnd; y < bnd; bits \<le> word_bits; bnd \<le> 2 ^ (word_bits - bits); bits \<noteq> 0\<rbrakk> \<Longrightarrow> word_of_nat x = word_of_nat y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>drop bits (to_bl (word_of_nat x)) @ replicate (min (size (word_of_nat x)) bits) False = drop bits (to_bl (word_of_nat y)) @ replicate (min (size (word_of_nat y)) bits) False; x < bnd; y < bnd; bits \<le> word_bits; bnd \<le> 2 ^ (word_bits - bits); bits \<noteq> 0\<rbrakk> \<Longrightarrow> to_bl (word_of_nat x) = to_bl (word_of_nat y) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>drop bits (to_bl (word_of_nat x)) @ replicate (min (size (word_of_nat x)) bits) False = drop bits (to_bl (word_of_nat y)) @ replicate (min (size (word_of_nat y)) bits) False; bits \<le> word_bits; bnd \<le> 2 ^ (word_bits - bits); bits \<noteq> 0; x < 2 ^ (word_bits - bits); y < 2 ^ (word_bits - bits)\<rbrakk> \<Longrightarrow> to_bl (word_of_nat x) = to_bl (word_of_nat y) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>drop bits (to_bl (word_of_nat x)) @ replicate (min (size (word_of_nat x)) bits) False = drop bits (to_bl (word_of_nat y)) @ replicate (min (size (word_of_nat y)) bits) False; bits \<le> word_bits; bnd \<le> 2 ^ (word_bits - bits); bits \<noteq> 0; y < 2 ^ (word_bits - bits)\<rbrakk> \<Longrightarrow> 2 ^ (word_bits - bits) < 2 ^ LENGTH(32)
 2. \<lbrakk>drop bits (to_bl (word_of_nat x)) @ replicate (min (size (word_of_nat x)) bits) False = drop bits (to_bl (word_of_nat y)) @ replicate (min (size (word_of_nat y)) bits) False; bits \<le> word_bits; bnd \<le> 2 ^ (word_bits - bits); bits \<noteq> 0; y < 2 ^ (word_bits - bits); word_of_nat x < word_of_nat (2 ^ (word_bits - bits))\<rbrakk> \<Longrightarrow> to_bl (word_of_nat x) = to_bl (word_of_nat y) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>drop bits (to_bl (word_of_nat x)) @ replicate (min (size (word_of_nat x)) bits) False = drop bits (to_bl (word_of_nat y)) @ replicate (min (size (word_of_nat y)) bits) False; bits \<le> word_bits; bnd \<le> 2 ^ (word_bits - bits); bits \<noteq> 0; y < 2 ^ (word_bits - bits)\<rbrakk> \<Longrightarrow> word_bits - bits < LENGTH(32)
 2. \<lbrakk>drop bits (to_bl (word_of_nat x)) @ replicate (min (size (word_of_nat x)) bits) False = drop bits (to_bl (word_of_nat y)) @ replicate (min (size (word_of_nat y)) bits) False; bits \<le> word_bits; bnd \<le> 2 ^ (word_bits - bits); bits \<noteq> 0; y < 2 ^ (word_bits - bits)\<rbrakk> \<Longrightarrow> 1 < 2
 3. \<lbrakk>drop bits (to_bl (word_of_nat x)) @ replicate (min (size (word_of_nat x)) bits) False = drop bits (to_bl (word_of_nat y)) @ replicate (min (size (word_of_nat y)) bits) False; bits \<le> word_bits; bnd \<le> 2 ^ (word_bits - bits); bits \<noteq> 0; y < 2 ^ (word_bits - bits); word_of_nat x < word_of_nat (2 ^ (word_bits - bits))\<rbrakk> \<Longrightarrow> to_bl (word_of_nat x) = to_bl (word_of_nat y) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>drop bits (to_bl (word_of_nat x)) @ replicate (min (size (word_of_nat x)) bits) False = drop bits (to_bl (word_of_nat y)) @ replicate (min (size (word_of_nat y)) bits) False; bits \<le> word_bits; bnd \<le> 2 ^ (word_bits - bits); bits \<noteq> 0; y < 2 ^ (word_bits - bits)\<rbrakk> \<Longrightarrow> 1 < 2
 2. \<lbrakk>drop bits (to_bl (word_of_nat x)) @ replicate (min (size (word_of_nat x)) bits) False = drop bits (to_bl (word_of_nat y)) @ replicate (min (size (word_of_nat y)) bits) False; bits \<le> word_bits; bnd \<le> 2 ^ (word_bits - bits); bits \<noteq> 0; y < 2 ^ (word_bits - bits); word_of_nat x < word_of_nat (2 ^ (word_bits - bits))\<rbrakk> \<Longrightarrow> to_bl (word_of_nat x) = to_bl (word_of_nat y) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>drop bits (to_bl (word_of_nat x)) @ replicate (min (size (word_of_nat x)) bits) False = drop bits (to_bl (word_of_nat y)) @ replicate (min (size (word_of_nat y)) bits) False; bits \<le> word_bits; bnd \<le> 2 ^ (word_bits - bits); bits \<noteq> 0; y < 2 ^ (word_bits - bits); word_of_nat x < word_of_nat (2 ^ (word_bits - bits))\<rbrakk> \<Longrightarrow> to_bl (word_of_nat x) = to_bl (word_of_nat y) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>drop bits (to_bl (word_of_nat x)) @ replicate (min (size (word_of_nat x)) bits) False = drop bits (to_bl (word_of_nat y)) @ replicate (min (size (word_of_nat y)) bits) False; bits \<le> word_bits; bnd \<le> 2 ^ (word_bits - bits); bits \<noteq> 0; word_of_nat x < word_of_nat (2 ^ (word_bits - bits))\<rbrakk> \<Longrightarrow> 2 ^ (word_bits - bits) < 2 ^ LENGTH(32)
 2. \<lbrakk>drop bits (to_bl (word_of_nat x)) @ replicate (min (size (word_of_nat x)) bits) False = drop bits (to_bl (word_of_nat y)) @ replicate (min (size (word_of_nat y)) bits) False; bits \<le> word_bits; bnd \<le> 2 ^ (word_bits - bits); bits \<noteq> 0; word_of_nat x < word_of_nat (2 ^ (word_bits - bits)); word_of_nat y < word_of_nat (2 ^ (word_bits - bits))\<rbrakk> \<Longrightarrow> to_bl (word_of_nat x) = to_bl (word_of_nat y) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>drop bits (to_bl (word_of_nat x)) @ replicate (min (size (word_of_nat x)) bits) False = drop bits (to_bl (word_of_nat y)) @ replicate (min (size (word_of_nat y)) bits) False; bits \<le> word_bits; bnd \<le> 2 ^ (word_bits - bits); bits \<noteq> 0; word_of_nat x < word_of_nat (2 ^ (word_bits - bits))\<rbrakk> \<Longrightarrow> word_bits - bits < LENGTH(32)
 2. \<lbrakk>drop bits (to_bl (word_of_nat x)) @ replicate (min (size (word_of_nat x)) bits) False = drop bits (to_bl (word_of_nat y)) @ replicate (min (size (word_of_nat y)) bits) False; bits \<le> word_bits; bnd \<le> 2 ^ (word_bits - bits); bits \<noteq> 0; word_of_nat x < word_of_nat (2 ^ (word_bits - bits))\<rbrakk> \<Longrightarrow> 1 < 2
 3. \<lbrakk>drop bits (to_bl (word_of_nat x)) @ replicate (min (size (word_of_nat x)) bits) False = drop bits (to_bl (word_of_nat y)) @ replicate (min (size (word_of_nat y)) bits) False; bits \<le> word_bits; bnd \<le> 2 ^ (word_bits - bits); bits \<noteq> 0; word_of_nat x < word_of_nat (2 ^ (word_bits - bits)); word_of_nat y < word_of_nat (2 ^ (word_bits - bits))\<rbrakk> \<Longrightarrow> to_bl (word_of_nat x) = to_bl (word_of_nat y) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>drop bits (to_bl (word_of_nat x)) @ replicate (min (size (word_of_nat x)) bits) False = drop bits (to_bl (word_of_nat y)) @ replicate (min (size (word_of_nat y)) bits) False; bits \<le> word_bits; bnd \<le> 2 ^ (word_bits - bits); bits \<noteq> 0; word_of_nat x < word_of_nat (2 ^ (word_bits - bits))\<rbrakk> \<Longrightarrow> 1 < 2
 2. \<lbrakk>drop bits (to_bl (word_of_nat x)) @ replicate (min (size (word_of_nat x)) bits) False = drop bits (to_bl (word_of_nat y)) @ replicate (min (size (word_of_nat y)) bits) False; bits \<le> word_bits; bnd \<le> 2 ^ (word_bits - bits); bits \<noteq> 0; word_of_nat x < word_of_nat (2 ^ (word_bits - bits)); word_of_nat y < word_of_nat (2 ^ (word_bits - bits))\<rbrakk> \<Longrightarrow> to_bl (word_of_nat x) = to_bl (word_of_nat y) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>drop bits (to_bl (word_of_nat x)) @ replicate (min (size (word_of_nat x)) bits) False = drop bits (to_bl (word_of_nat y)) @ replicate (min (size (word_of_nat y)) bits) False; bits \<le> word_bits; bnd \<le> 2 ^ (word_bits - bits); bits \<noteq> 0; word_of_nat x < word_of_nat (2 ^ (word_bits - bits)); word_of_nat y < word_of_nat (2 ^ (word_bits - bits))\<rbrakk> \<Longrightarrow> to_bl (word_of_nat x) = to_bl (word_of_nat y) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>drop bits (to_bl (word_of_nat x)) @ replicate (min (size (word_of_nat x)) bits) False = drop bits (to_bl (word_of_nat y)) @ replicate (min (size (word_of_nat y)) bits) False; bits \<le> word_bits; bnd \<le> 2 ^ (word_bits - bits); bits \<noteq> 0; word_of_nat x < 2 ^ (word_bits - bits); word_of_nat y < 2 ^ (word_bits - bits)\<rbrakk> \<Longrightarrow> to_bl (word_of_nat x) = to_bl (word_of_nat y) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>drop bits (to_bl (word_of_nat x)) @ replicate (min (size (word_of_nat x)) bits) False = drop bits (to_bl (word_of_nat y)) @ replicate (min (size (word_of_nat y)) bits) False; bits \<le> word_bits; bnd \<le> 2 ^ (word_bits - bits); bits \<noteq> 0\<rbrakk> \<Longrightarrow> replicate (LENGTH(32) - (word_bits - bits)) False @ drop (LENGTH(32) - (word_bits - bits)) (to_bl (word_of_nat x)) = replicate (LENGTH(32) - (word_bits - bits)) False @ drop (LENGTH(32) - (word_bits - bits)) (to_bl (word_of_nat y)) proof (prove)
goal:
No subgoals!