theory Example_Valid_State

lemma nat_to_bl_eq:
  assumes "a < 2 ^ n \<or> b < 2 ^ n"
  shows "nat_to_bl n a = nat_to_bl n b \<longleftrightarrow> a = b" using assms apply - apply (erule disjE_R) apply (clarsimp simp: nat_to_bl_def) apply (case_tac "a \<ge> 2 ^ n") apply (clarsimp simp: nat_to_bl_def) apply (clarsimp simp: not_le) apply (induct n arbitrary: a b) apply (clarsimp simp: nat_to_bl_def) apply atomize apply (clarsimp simp: nat_to_bl_def) apply (erule_tac x="a div 2" in allE) apply (erule_tac x="b div 2" in allE) apply (erule impE) apply (metis power_commutes td_gal_lt zero_less_numeral) apply (clarsimp simp: bin_last_def zdiv_int) apply (rule iffI [rotated], clarsimp) apply (subst (asm) (1 2 3 4) bin_to_bl_aux_alt) apply (clarsimp simp: mod_eq_dvd_iff) apply (subst split_div_mod [where k=2]) apply clarsimp apply presburger done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (nat_to_bl n a = nat_to_bl n b) = (a = b) proof (prove)
using this:
a < 2 ^ n \<or> b < 2 ^ n

goal (1 subgoal):
 1. (nat_to_bl n a = nat_to_bl n b) = (a = b) proof (prove)
goal (1 subgoal):
 1. a < 2 ^ n \<or> b < 2 ^ n \<Longrightarrow> (nat_to_bl n a = nat_to_bl n b) = (a = b) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<not> b < 2 ^ n; a < 2 ^ n\<rbrakk> \<Longrightarrow> (nat_to_bl n a = nat_to_bl n b) = (a = b)
 2. b < 2 ^ n \<Longrightarrow> (nat_to_bl n a = nat_to_bl n b) = (a = b) proof (prove)
goal (1 subgoal):
 1. b < 2 ^ n \<Longrightarrow> (nat_to_bl n a = nat_to_bl n b) = (a = b) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>b < 2 ^ n; 2 ^ n \<le> a\<rbrakk> \<Longrightarrow> (nat_to_bl n a = nat_to_bl n b) = (a = b)
 2. \<lbrakk>b < 2 ^ n; \<not> 2 ^ n \<le> a\<rbrakk> \<Longrightarrow> (nat_to_bl n a = nat_to_bl n b) = (a = b) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b < 2 ^ n; \<not> 2 ^ n \<le> a\<rbrakk> \<Longrightarrow> (nat_to_bl n a = nat_to_bl n b) = (a = b) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b < 2 ^ n; a < 2 ^ n\<rbrakk> \<Longrightarrow> (nat_to_bl n a = nat_to_bl n b) = (a = b) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>b < 2 ^ 0; a < 2 ^ 0\<rbrakk> \<Longrightarrow> (nat_to_bl 0 a = nat_to_bl 0 b) = (a = b)
 2. \<And>n a b. \<lbrakk>\<And>a b. \<lbrakk>b < 2 ^ n; a < 2 ^ n\<rbrakk> \<Longrightarrow> (nat_to_bl n a = nat_to_bl n b) = (a = b); b < 2 ^ Suc n; a < 2 ^ Suc n\<rbrakk> \<Longrightarrow> (nat_to_bl (Suc n) a = nat_to_bl (Suc n) b) = (a = b) proof (prove)
goal (1 subgoal):
 1. \<And>n a b. \<lbrakk>\<And>a b. \<lbrakk>b < 2 ^ n; a < 2 ^ n\<rbrakk> \<Longrightarrow> (nat_to_bl n a = nat_to_bl n b) = (a = b); b < 2 ^ Suc n; a < 2 ^ Suc n\<rbrakk> \<Longrightarrow> (nat_to_bl (Suc n) a = nat_to_bl (Suc n) b) = (a = b) proof (prove)
goal (1 subgoal):
 1. \<And>n a b. \<lbrakk>\<forall>a b. b < 2 ^ n \<longrightarrow> a < 2 ^ n \<longrightarrow> (nat_to_bl n a = nat_to_bl n b) = (a = b); b < 2 ^ Suc n; a < 2 ^ Suc n\<rbrakk> \<Longrightarrow> (nat_to_bl (Suc n) a = nat_to_bl (Suc n) b) = (a = b) proof (prove)
goal (1 subgoal):
 1. \<And>n a b. \<lbrakk>\<forall>a b. b < 2 ^ n \<longrightarrow> a < 2 ^ n \<longrightarrow> (bin_to_bl_aux n (int a) [] = bin_to_bl_aux n (int b) []) = (a = b); b < 2 * 2 ^ n; a < 2 * 2 ^ n\<rbrakk> \<Longrightarrow> (bin_to_bl_aux n (int a div 2) [odd a] = bin_to_bl_aux n (int b div 2) [odd b]) = (a = b) proof (prove)
goal (1 subgoal):
 1. \<And>n a b. \<lbrakk>b < 2 * 2 ^ n; a < 2 * 2 ^ n; \<forall>b<2 ^ n. a div 2 < 2 ^ n \<longrightarrow> (bin_to_bl_aux n (int (a div 2)) [] = bin_to_bl_aux n (int b) []) = (a div 2 = b)\<rbrakk> \<Longrightarrow> (bin_to_bl_aux n (int a div 2) [odd a] = bin_to_bl_aux n (int b div 2) [odd b]) = (a = b) proof (prove)
goal (1 subgoal):
 1. \<And>n a b. \<lbrakk>b < 2 * 2 ^ n; a < 2 * 2 ^ n; b div 2 < 2 ^ n \<longrightarrow> a div 2 < 2 ^ n \<longrightarrow> (bin_to_bl_aux n (int (a div 2)) [] = bin_to_bl_aux n (int (b div 2)) []) = (a div 2 = b div 2)\<rbrakk> \<Longrightarrow> (bin_to_bl_aux n (int a div 2) [odd a] = bin_to_bl_aux n (int b div 2) [odd b]) = (a = b) proof (prove)
goal (2 subgoals):
 1. \<And>n a b. \<lbrakk>b < 2 * 2 ^ n; a < 2 * 2 ^ n\<rbrakk> \<Longrightarrow> b div 2 < 2 ^ n
 2. \<And>n a b. \<lbrakk>b < 2 * 2 ^ n; a < 2 * 2 ^ n; a div 2 < 2 ^ n \<longrightarrow> (bin_to_bl_aux n (int (a div 2)) [] = bin_to_bl_aux n (int (b div 2)) []) = (a div 2 = b div 2)\<rbrakk> \<Longrightarrow> (bin_to_bl_aux n (int a div 2) [odd a] = bin_to_bl_aux n (int b div 2) [odd b]) = (a = b) proof (prove)
goal (1 subgoal):
 1. \<And>n a b. \<lbrakk>b < 2 * 2 ^ n; a < 2 * 2 ^ n; a div 2 < 2 ^ n \<longrightarrow> (bin_to_bl_aux n (int (a div 2)) [] = bin_to_bl_aux n (int (b div 2)) []) = (a div 2 = b div 2)\<rbrakk> \<Longrightarrow> (bin_to_bl_aux n (int a div 2) [odd a] = bin_to_bl_aux n (int b div 2) [odd b]) = (a = b) proof (prove)
goal (1 subgoal):
 1. \<And>n a b. \<lbrakk>b < 2 * 2 ^ n; a < 2 * 2 ^ n; a div 2 < 2 ^ n \<longrightarrow> (bin_to_bl_aux n (int a div 2) [] = bin_to_bl_aux n (int b div 2) []) = (a div 2 = b div 2)\<rbrakk> \<Longrightarrow> (bin_to_bl_aux n (int a div 2) [odd a] = bin_to_bl_aux n (int b div 2) [odd b]) = (a = b) proof (prove)
goal (1 subgoal):
 1. \<And>n a b. \<lbrakk>b < 2 * 2 ^ n; a < 2 * 2 ^ n; a div 2 < 2 ^ n \<longrightarrow> (bin_to_bl_aux n (int a div 2) [] = bin_to_bl_aux n (int b div 2) []) = (a div 2 = b div 2); bin_to_bl_aux n (int a div 2) [odd a] = bin_to_bl_aux n (int b div 2) [odd b]\<rbrakk> \<Longrightarrow> a = b proof (prove)
goal (1 subgoal):
 1. \<And>n a b. \<lbrakk>b < 2 * 2 ^ n; a < 2 * 2 ^ n; a div 2 < 2 ^ n \<longrightarrow> (bin_to_bl n (int a div 2) @ [] = bin_to_bl n (int b div 2) @ []) = (a div 2 = b div 2); bin_to_bl n (int a div 2) @ [odd a] = bin_to_bl n (int b div 2) @ [odd b]\<rbrakk> \<Longrightarrow> a = b proof (prove)
goal (1 subgoal):
 1. \<And>n a b. \<lbrakk>b < 2 * 2 ^ n; a < 2 * 2 ^ n; b div 2 < 2 ^ n \<longrightarrow> bin_to_bl_aux n (int a div 2) [] = bin_to_bl_aux n (int b div 2) []; a div 2 = b div 2; even a = even b\<rbrakk> \<Longrightarrow> a = b proof (prove)
goal (1 subgoal):
 1. \<And>n a b. \<lbrakk>b < 2 * 2 ^ n; a < 2 * 2 ^ n; b div 2 < 2 ^ n \<longrightarrow> bin_to_bl_aux n (int a div 2) [] = bin_to_bl_aux n (int b div 2) []; a div 2 = b div 2; even a = even b\<rbrakk> \<Longrightarrow> a div 2 = b div 2 \<and> a mod 2 = b mod 2 proof (prove)
goal (1 subgoal):
 1. \<And>n a b. \<lbrakk>b < 2 * 2 ^ n; a < 2 * 2 ^ n; b div 2 < 2 ^ n \<longrightarrow> bin_to_bl_aux n (int a div 2) [] = bin_to_bl_aux n (int b div 2) []; a div 2 = b div 2; even a = even b\<rbrakk> \<Longrightarrow> a mod 2 = b mod 2 proof (prove)
goal:
No subgoals!