theory KHeap_DR

lemma nat_to_bl_dest:
  "b\<in>Collect (%x. length x= n)\<Longrightarrow> nat_to_bl n (nat (bl_to_bin b)) = Some b" apply (unfold nat_to_bl_def) apply (subgoal_tac "0 \<le> bl_to_bin b") apply (subst nat_0_le) apply simp apply (subgoal_tac "length b = n") apply (erule subst[where s="length b" and t=n]) apply (subst bl_bin_bl) apply (simp add: not_le) apply (clarsimp simp: bl_to_bin_lt2p) apply clarsimp apply (simp add:not_less) apply (rule bl_to_bin_ge0) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. b \<in> {x. length x = n} \<Longrightarrow> nat_to_bl n (nat (bl_to_bin b)) = Some b proof (prove)
goal (1 subgoal):
 1. b \<in> {x. length x = n} \<Longrightarrow> (if 2 ^ n \<le> nat (bl_to_bin b) then None else Some $ bin_to_bl n (int (nat (bl_to_bin b)))) = Some b proof (prove)
goal (2 subgoals):
 1. \<lbrakk>b \<in> {x. length x = n}; 0 \<le> bl_to_bin b\<rbrakk> \<Longrightarrow> (if 2 ^ n \<le> nat (bl_to_bin b) then None else Some $ bin_to_bl n (int (nat (bl_to_bin b)))) = Some b
 2. b \<in> {x. length x = n} \<Longrightarrow> 0 \<le> bl_to_bin b proof (prove)
goal (3 subgoals):
 1. \<lbrakk>b \<in> {x. length x = n}; 0 \<le> bl_to_bin b\<rbrakk> \<Longrightarrow> 0 \<le> bl_to_bin b
 2. \<lbrakk>b \<in> {x. length x = n}; 0 \<le> bl_to_bin b\<rbrakk> \<Longrightarrow> (if 2 ^ n \<le> nat (bl_to_bin b) then None else Some $ bin_to_bl n (bl_to_bin b)) = Some b
 3. b \<in> {x. length x = n} \<Longrightarrow> 0 \<le> bl_to_bin b proof (prove)
goal (2 subgoals):
 1. \<lbrakk>b \<in> {x. length x = n}; 0 \<le> bl_to_bin b\<rbrakk> \<Longrightarrow> (if 2 ^ n \<le> nat (bl_to_bin b) then None else Some $ bin_to_bl n (bl_to_bin b)) = Some b
 2. b \<in> {x. length x = n} \<Longrightarrow> 0 \<le> bl_to_bin b proof (prove)
goal (3 subgoals):
 1. \<lbrakk>b \<in> {x. length x = n}; 0 \<le> bl_to_bin b; length b = n\<rbrakk> \<Longrightarrow> (if 2 ^ n \<le> nat (bl_to_bin b) then None else Some $ bin_to_bl n (bl_to_bin b)) = Some b
 2. \<lbrakk>b \<in> {x. length x = n}; 0 \<le> bl_to_bin b\<rbrakk> \<Longrightarrow> length b = n
 3. b \<in> {x. length x = n} \<Longrightarrow> 0 \<le> bl_to_bin b proof (prove)
goal (3 subgoals):
 1. \<lbrakk>b \<in> {x. length x = n}; 0 \<le> bl_to_bin b\<rbrakk> \<Longrightarrow> (if 2 ^ length b \<le> nat (bl_to_bin b) then None else Some $ bin_to_bl (length b) (bl_to_bin b)) = Some b
 2. \<lbrakk>b \<in> {x. length x = n}; 0 \<le> bl_to_bin b\<rbrakk> \<Longrightarrow> length b = n
 3. b \<in> {x. length x = n} \<Longrightarrow> 0 \<le> bl_to_bin b proof (prove)
goal (3 subgoals):
 1. \<lbrakk>b \<in> {x. length x = n}; 0 \<le> bl_to_bin b\<rbrakk> \<Longrightarrow> (if 2 ^ length b \<le> nat (bl_to_bin b) then None else Some $ b) = Some b
 2. \<lbrakk>b \<in> {x. length x = n}; 0 \<le> bl_to_bin b\<rbrakk> \<Longrightarrow> length b = n
 3. b \<in> {x. length x = n} \<Longrightarrow> 0 \<le> bl_to_bin b proof (prove)
goal (3 subgoals):
 1. \<lbrakk>length b = n; 0 \<le> bl_to_bin b\<rbrakk> \<Longrightarrow> bl_to_bin b < 2 ^ n
 2. \<lbrakk>b \<in> {x. length x = n}; 0 \<le> bl_to_bin b\<rbrakk> \<Longrightarrow> length b = n
 3. b \<in> {x. length x = n} \<Longrightarrow> 0 \<le> bl_to_bin b proof (prove)
goal (2 subgoals):
 1. \<lbrakk>b \<in> {x. length x = n}; 0 \<le> bl_to_bin b\<rbrakk> \<Longrightarrow> length b = n
 2. b \<in> {x. length x = n} \<Longrightarrow> 0 \<le> bl_to_bin b proof (prove)
goal (1 subgoal):
 1. b \<in> {x. length x = n} \<Longrightarrow> 0 \<le> bl_to_bin b proof (prove)
goal (1 subgoal):
 1. length b = n \<Longrightarrow> 0 \<le> bl_to_bin b proof (prove)
goal:
No subgoals!