theory Arch_AI

lemma ucast_assocs:
  "LENGTH('a) < LENGTH('b) \<Longrightarrow>
   assocs (fn o (ucast :: 'a :: len word \<Rightarrow> 'b :: len word))
     = map (\<lambda>(x, y). (ucast x, y)) (filter (\<lambda>(x, y). x < 2 ^ LENGTH('a)) (assocs fn))" apply (simp add: assocs_def enum_word_def split_def filter_map) apply (rule map_cong) apply (simp add: o_def) apply (rule trans [OF _ filter_cong [OF refl]],
          rule sym, rule filter_to_shorter_upto) apply simp apply (rule iffI) apply (subst word_unat_power, rule of_nat_mono_maybe) apply simp apply assumption apply (simp add: word_less_nat_alt word_unat.Abs_inverse unats_def) apply clarsimp apply (simp add: word_less_nat_alt word_unat.Abs_inverse unats_def) apply (simp add: ucast_of_nat_small) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. LENGTH('a) < LENGTH('b) \<Longrightarrow> assocs (fn \<circ> UCAST('a \<rightarrow> 'b)) = map (\<lambda>(x, y). (UCAST('b \<rightarrow> 'a) x, y)) (filter (\<lambda>(x, y). x < 2 ^ LENGTH('a)) (assocs fn)) proof (prove)
goal (1 subgoal):
 1. LENGTH('a) < LENGTH('b) \<Longrightarrow> map ((\<lambda>x. (x, fn (UCAST('a \<rightarrow> 'b) x))) \<circ> word_of_nat) [0..<2 ^ LENGTH('a)] = map ((\<lambda>p. (UCAST('b \<rightarrow> 'a) (fst p), snd p)) \<circ> ((\<lambda>x. (x, fn x)) \<circ> word_of_nat)) (filter ((\<lambda>p. fst p < 2 ^ LENGTH('a)) \<circ> ((\<lambda>x. (x, fn x)) \<circ> word_of_nat)) [0..<2 ^ LENGTH('b)]) proof (prove)
goal (2 subgoals):
 1. LENGTH('a) < LENGTH('b) \<Longrightarrow> [0..<2 ^ LENGTH('a)] = filter ((\<lambda>p. fst p < 2 ^ LENGTH('a)) \<circ> ((\<lambda>x. (x, fn x)) \<circ> word_of_nat)) [0..<2 ^ LENGTH('b)]
 2. \<And>x. \<lbrakk>LENGTH('a) < LENGTH('b); x \<in> set (filter ((\<lambda>p. fst p < 2 ^ LENGTH('a)) \<circ> ((\<lambda>x. (x, fn x)) \<circ> word_of_nat)) [0..<2 ^ LENGTH('b)])\<rbrakk> \<Longrightarrow> ((\<lambda>x. (x, fn (UCAST('a \<rightarrow> 'b) x))) \<circ> word_of_nat) x = ((\<lambda>p. (UCAST('b \<rightarrow> 'a) (fst p), snd p)) \<circ> ((\<lambda>x. (x, fn x)) \<circ> word_of_nat)) x proof (prove)
goal (2 subgoals):
 1. LENGTH('a) < LENGTH('b) \<Longrightarrow> [0..<2 ^ LENGTH('a)] = filter (\<lambda>x. word_of_nat x < 2 ^ LENGTH('a)) [0..<2 ^ LENGTH('b)]
 2. \<And>x. \<lbrakk>LENGTH('a) < LENGTH('b); x \<in> set (filter ((\<lambda>p. fst p < 2 ^ LENGTH('a)) \<circ> ((\<lambda>x. (x, fn x)) \<circ> word_of_nat)) [0..<2 ^ LENGTH('b)])\<rbrakk> \<Longrightarrow> ((\<lambda>x. (x, fn (UCAST('a \<rightarrow> 'b) x))) \<circ> word_of_nat) x = ((\<lambda>p. (UCAST('b \<rightarrow> 'a) (fst p), snd p)) \<circ> ((\<lambda>x. (x, fn x)) \<circ> word_of_nat)) x proof (prove)
goal (3 subgoals):
 1. LENGTH('a) < LENGTH('b) \<Longrightarrow> 2 ^ LENGTH('a) \<le> 2 ^ LENGTH('b)
 2. \<And>x. \<lbrakk>LENGTH('a) < LENGTH('b); x \<in> set [0..<2 ^ LENGTH('b)]\<rbrakk> \<Longrightarrow> (x < 2 ^ LENGTH('a)) = (word_of_nat x < 2 ^ LENGTH('a))
 3. \<And>x. \<lbrakk>LENGTH('a) < LENGTH('b); x \<in> set (filter ((\<lambda>p. fst p < 2 ^ LENGTH('a)) \<circ> ((\<lambda>x. (x, fn x)) \<circ> word_of_nat)) [0..<2 ^ LENGTH('b)])\<rbrakk> \<Longrightarrow> ((\<lambda>x. (x, fn (UCAST('a \<rightarrow> 'b) x))) \<circ> word_of_nat) x = ((\<lambda>p. (UCAST('b \<rightarrow> 'a) (fst p), snd p)) \<circ> ((\<lambda>x. (x, fn x)) \<circ> word_of_nat)) x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>LENGTH('a) < LENGTH('b); x \<in> set [0..<2 ^ LENGTH('b)]\<rbrakk> \<Longrightarrow> (x < 2 ^ LENGTH('a)) = (word_of_nat x < 2 ^ LENGTH('a))
 2. \<And>x. \<lbrakk>LENGTH('a) < LENGTH('b); x \<in> set (filter ((\<lambda>p. fst p < 2 ^ LENGTH('a)) \<circ> ((\<lambda>x. (x, fn x)) \<circ> word_of_nat)) [0..<2 ^ LENGTH('b)])\<rbrakk> \<Longrightarrow> ((\<lambda>x. (x, fn (UCAST('a \<rightarrow> 'b) x))) \<circ> word_of_nat) x = ((\<lambda>p. (UCAST('b \<rightarrow> 'a) (fst p), snd p)) \<circ> ((\<lambda>x. (x, fn x)) \<circ> word_of_nat)) x proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>LENGTH('a) < LENGTH('b); x \<in> set [0..<2 ^ LENGTH('b)]; x < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> word_of_nat x < 2 ^ LENGTH('a)
 2. \<And>x. \<lbrakk>LENGTH('a) < LENGTH('b); x \<in> set [0..<2 ^ LENGTH('b)]; word_of_nat x < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> x < 2 ^ LENGTH('a)
 3. \<And>x. \<lbrakk>LENGTH('a) < LENGTH('b); x \<in> set (filter ((\<lambda>p. fst p < 2 ^ LENGTH('a)) \<circ> ((\<lambda>x. (x, fn x)) \<circ> word_of_nat)) [0..<2 ^ LENGTH('b)])\<rbrakk> \<Longrightarrow> ((\<lambda>x. (x, fn (UCAST('a \<rightarrow> 'b) x))) \<circ> word_of_nat) x = ((\<lambda>p. (UCAST('b \<rightarrow> 'a) (fst p), snd p)) \<circ> ((\<lambda>x. (x, fn x)) \<circ> word_of_nat)) x proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>LENGTH('a) < LENGTH('b); x \<in> set [0..<2 ^ LENGTH('b)]; x < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> 2 ^ LENGTH('a) < 2 ^ LENGTH('b)
 2. \<And>x. \<lbrakk>LENGTH('a) < LENGTH('b); x \<in> set [0..<2 ^ LENGTH('b)]; x < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> x < 2 ^ LENGTH('a)
 3. \<And>x. \<lbrakk>LENGTH('a) < LENGTH('b); x \<in> set [0..<2 ^ LENGTH('b)]; word_of_nat x < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> x < 2 ^ LENGTH('a)
 4. \<And>x. \<lbrakk>LENGTH('a) < LENGTH('b); x \<in> set (filter ((\<lambda>p. fst p < 2 ^ LENGTH('a)) \<circ> ((\<lambda>x. (x, fn x)) \<circ> word_of_nat)) [0..<2 ^ LENGTH('b)])\<rbrakk> \<Longrightarrow> ((\<lambda>x. (x, fn (UCAST('a \<rightarrow> 'b) x))) \<circ> word_of_nat) x = ((\<lambda>p. (UCAST('b \<rightarrow> 'a) (fst p), snd p)) \<circ> ((\<lambda>x. (x, fn x)) \<circ> word_of_nat)) x proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>LENGTH('a) < LENGTH('b); x \<in> set [0..<2 ^ LENGTH('b)]; x < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> x < 2 ^ LENGTH('a)
 2. \<And>x. \<lbrakk>LENGTH('a) < LENGTH('b); x \<in> set [0..<2 ^ LENGTH('b)]; word_of_nat x < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> x < 2 ^ LENGTH('a)
 3. \<And>x. \<lbrakk>LENGTH('a) < LENGTH('b); x \<in> set (filter ((\<lambda>p. fst p < 2 ^ LENGTH('a)) \<circ> ((\<lambda>x. (x, fn x)) \<circ> word_of_nat)) [0..<2 ^ LENGTH('b)])\<rbrakk> \<Longrightarrow> ((\<lambda>x. (x, fn (UCAST('a \<rightarrow> 'b) x))) \<circ> word_of_nat) x = ((\<lambda>p. (UCAST('b \<rightarrow> 'a) (fst p), snd p)) \<circ> ((\<lambda>x. (x, fn x)) \<circ> word_of_nat)) x proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>LENGTH('a) < LENGTH('b); x \<in> set [0..<2 ^ LENGTH('b)]; word_of_nat x < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> x < 2 ^ LENGTH('a)
 2. \<And>x. \<lbrakk>LENGTH('a) < LENGTH('b); x \<in> set (filter ((\<lambda>p. fst p < 2 ^ LENGTH('a)) \<circ> ((\<lambda>x. (x, fn x)) \<circ> word_of_nat)) [0..<2 ^ LENGTH('b)])\<rbrakk> \<Longrightarrow> ((\<lambda>x. (x, fn (UCAST('a \<rightarrow> 'b) x))) \<circ> word_of_nat) x = ((\<lambda>p. (UCAST('b \<rightarrow> 'a) (fst p), snd p)) \<circ> ((\<lambda>x. (x, fn x)) \<circ> word_of_nat)) x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>LENGTH('a) < LENGTH('b); x \<in> set (filter ((\<lambda>p. fst p < 2 ^ LENGTH('a)) \<circ> ((\<lambda>x. (x, fn x)) \<circ> word_of_nat)) [0..<2 ^ LENGTH('b)])\<rbrakk> \<Longrightarrow> ((\<lambda>x. (x, fn (UCAST('a \<rightarrow> 'b) x))) \<circ> word_of_nat) x = ((\<lambda>p. (UCAST('b \<rightarrow> 'a) (fst p), snd p)) \<circ> ((\<lambda>x. (x, fn x)) \<circ> word_of_nat)) x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>LENGTH('a) < LENGTH('b); x < 2 ^ LENGTH('b); word_of_nat x < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> word_of_nat x = UCAST('b \<rightarrow> 'a) (word_of_nat x) \<and> fn (UCAST('a \<rightarrow> 'b) (word_of_nat x)) = fn (word_of_nat x) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>LENGTH('a) < LENGTH('b); x < 2 ^ LENGTH('b); x < 2 ^ LENGTH('a)\<rbrakk> \<Longrightarrow> word_of_nat x = UCAST('b \<rightarrow> 'a) (word_of_nat x) \<and> fn (UCAST('a \<rightarrow> 'b) (word_of_nat x)) = fn (word_of_nat x) proof (prove)
goal:
No subgoals!