theory ArchUntyped_AI

lemma inj_on_nat_to_cref[Untyped_AI_assms]:
  "bits < 32 \<Longrightarrow> inj_on (nat_to_cref bits) {..< 2 ^ bits}" apply (rule inj_onI) apply (drule arg_cong[where f="\<lambda>x. replicate (32 - bits) False @ x"]) apply (subst(asm) word_bl.Abs_inject[where 'a=32, symmetric]) apply (simp add: nat_to_cref_def word_bits_def) apply (simp add: nat_to_cref_def word_bits_def) apply (simp add: of_bl_rep_False of_bl_nat_to_cref[simplified word_bits_def]) apply (erule word_unat.Abs_eqD) apply (simp only: unats_def mem_simps) apply (erule order_less_le_trans) apply (rule power_increasing, simp+) apply (simp only: unats_def mem_simps) apply (erule order_less_le_trans) apply (rule power_increasing, simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bits < 32 \<Longrightarrow> inj_on (nat_to_cref bits) {..<2 ^ bits} proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>bits < 32; x \<in> {..<2 ^ bits}; y \<in> {..<2 ^ bits}; nat_to_cref bits x = nat_to_cref bits y\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>bits < 32; x \<in> {..<2 ^ bits}; y \<in> {..<2 ^ bits}; replicate (32 - bits) False @ nat_to_cref bits x = replicate (32 - bits) False @ nat_to_cref bits y\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>bits < 32; x \<in> {..<2 ^ bits}; y \<in> {..<2 ^ bits}\<rbrakk> \<Longrightarrow> replicate (32 - bits) False @ nat_to_cref bits x \<in> {bl. length bl = LENGTH(32)}
 2. \<And>x y. \<lbrakk>bits < 32; x \<in> {..<2 ^ bits}; y \<in> {..<2 ^ bits}\<rbrakk> \<Longrightarrow> replicate (32 - bits) False @ nat_to_cref bits y \<in> {bl. length bl = LENGTH(32)}
 3. \<And>x y. \<lbrakk>bits < 32; x \<in> {..<2 ^ bits}; y \<in> {..<2 ^ bits}; of_bl (replicate (32 - bits) False @ nat_to_cref bits x) = of_bl (replicate (32 - bits) False @ nat_to_cref bits y)\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>bits < 32; x \<in> {..<2 ^ bits}; y \<in> {..<2 ^ bits}\<rbrakk> \<Longrightarrow> replicate (32 - bits) False @ nat_to_cref bits y \<in> {bl. length bl = LENGTH(32)}
 2. \<And>x y. \<lbrakk>bits < 32; x \<in> {..<2 ^ bits}; y \<in> {..<2 ^ bits}; of_bl (replicate (32 - bits) False @ nat_to_cref bits x) = of_bl (replicate (32 - bits) False @ nat_to_cref bits y)\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>bits < 32; x \<in> {..<2 ^ bits}; y \<in> {..<2 ^ bits}; of_bl (replicate (32 - bits) False @ nat_to_cref bits x) = of_bl (replicate (32 - bits) False @ nat_to_cref bits y)\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>bits < 32; x < 2 ^ bits; y < 2 ^ bits; word_of_nat x = word_of_nat y\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>bits < 32; x < 2 ^ bits; y < 2 ^ bits\<rbrakk> \<Longrightarrow> x \<in> unats LENGTH(32)
 2. \<And>x y. \<lbrakk>bits < 32; x < 2 ^ bits; y < 2 ^ bits\<rbrakk> \<Longrightarrow> y \<in> unats LENGTH(32) proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>bits < 32; x < 2 ^ bits; y < 2 ^ bits\<rbrakk> \<Longrightarrow> x < 2 ^ LENGTH(32)
 2. \<And>x y. \<lbrakk>bits < 32; x < 2 ^ bits; y < 2 ^ bits\<rbrakk> \<Longrightarrow> y \<in> unats LENGTH(32) proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>bits < 32; y < 2 ^ bits\<rbrakk> \<Longrightarrow> 2 ^ bits \<le> 2 ^ LENGTH(32)
 2. \<And>x y. \<lbrakk>bits < 32; x < 2 ^ bits; y < 2 ^ bits\<rbrakk> \<Longrightarrow> y \<in> unats LENGTH(32) proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>bits < 32; x < 2 ^ bits; y < 2 ^ bits\<rbrakk> \<Longrightarrow> y \<in> unats 32 proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>bits < 32; x < 2 ^ bits; y < 2 ^ bits\<rbrakk> \<Longrightarrow> y < 2 ^ 32 proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>bits < 32; x < 2 ^ bits\<rbrakk> \<Longrightarrow> 2 ^ bits \<le> 2 ^ 32 proof (prove)
goal:
No subgoals!