theory Untyped_AI

lemma upt_mult_lt_prop:
  assumes n: "n \<le> 2 ^ a"
  assumes b: "b \<le> a"
  shows "\<exists>bd. [i\<leftarrow>[0..<2 ^ (a - b)]. i * 2 ^ b < n]
        = [0 ..< bd] \<and> n \<le> bd * 2 ^ b \<and> bd * 2 ^ b \<le> 2 ^ a
          \<and> (bd - 1) * 2 ^ b \<le> n" proof - let ?al = "(n + (2 ^ b - 1)) div 2 ^ b" have sub1: "0 < n \<Longrightarrow> (?al - 1) * 2 ^ b < n" apply (cases "?al = 0") apply simp apply (simp add: diff_mult_distrib) apply (rule nat_diff_less2, simp_all) apply (rule order_le_less_trans, rule div_mult_le) apply simp done have le1: "(n + 2 ^ b - Suc 0) div 2 ^ b * 2 ^ b \<le> 2 ^ a" apply (rule alignUp_le_nat[simplified], simp_all add: n) apply (simp add: b le_imp_power_dvd) done note le2 = div_le_mono[OF le1, where k="2 ^ b", simplified] show ?thesis apply (cases "n = 0") apply (simp add: exI[where x=0]) apply (rule exI[where x="?al"]) apply (strengthen filter_upt_eq) apply (simp add: linorder_not_less conj.commute) apply (simp add: alignUp_ge_nat[simplified] sub1[simplified]
                     sub1[THEN order_less_imp_le, simplified]
                     power_minus_is_div[OF b] le1 le2) apply (auto elim: order_le_less_trans[rotated]) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>bd. filter (\<lambda>i. i * 2 ^ b < n) [0..<2 ^ (a - b)] = [0..<bd] \<and> n \<le> bd * 2 ^ b \<and> bd * 2 ^ b \<le> 2 ^ a \<and> (bd - 1) * 2 ^ b \<le> n proof (state)
goal (1 subgoal):
 1. \<exists>bd. filter (\<lambda>i. i * 2 ^ b < n) [0..<2 ^ (a - b)] = [0..<bd] \<and> n \<le> bd * 2 ^ b \<and> bd * 2 ^ b \<le> 2 ^ a \<and> (bd - 1) * 2 ^ b \<le> n proof (state)
goal (1 subgoal):
 1. \<exists>bd. filter (\<lambda>i. i * 2 ^ b < n) [0..<2 ^ (a - b)] = [0..<bd] \<and> n \<le> bd * 2 ^ b \<and> bd * 2 ^ b \<le> 2 ^ a \<and> (bd - 1) * 2 ^ b \<le> n proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> ((n + (2 ^ b - 1)) div 2 ^ b - 1) * 2 ^ b < n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < n; (n + (2 ^ b - 1)) div 2 ^ b = 0\<rbrakk> \<Longrightarrow> ((n + (2 ^ b - 1)) div 2 ^ b - 1) * 2 ^ b < n
 2. \<lbrakk>0 < n; (n + (2 ^ b - 1)) div 2 ^ b \<noteq> 0\<rbrakk> \<Longrightarrow> ((n + (2 ^ b - 1)) div 2 ^ b - 1) * 2 ^ b < n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; (n + (2 ^ b - 1)) div 2 ^ b \<noteq> 0\<rbrakk> \<Longrightarrow> ((n + (2 ^ b - 1)) div 2 ^ b - 1) * 2 ^ b < n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; 0 < (n + 2 ^ b - Suc 0) div 2 ^ b\<rbrakk> \<Longrightarrow> (n + 2 ^ b - Suc 0) div 2 ^ b * 2 ^ b - 2 ^ b < n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; 0 < (n + 2 ^ b - Suc 0) div 2 ^ b\<rbrakk> \<Longrightarrow> (n + 2 ^ b - Suc 0) div 2 ^ b * 2 ^ b < n + 2 ^ b proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < n; 0 < (n + 2 ^ b - Suc 0) div 2 ^ b\<rbrakk> \<Longrightarrow> n + 2 ^ b - Suc 0 < n + 2 ^ b proof (prove)
goal:
No subgoals! proof (state)
this:
0 < n \<Longrightarrow> ((n + (2 ^ b - 1)) div 2 ^ b - 1) * 2 ^ b < n

goal (1 subgoal):
 1. \<exists>bd. filter (\<lambda>i. i * 2 ^ b < n) [0..<2 ^ (a - b)] = [0..<bd] \<and> n \<le> bd * 2 ^ b \<and> bd * 2 ^ b \<le> 2 ^ a \<and> (bd - 1) * 2 ^ b \<le> n proof (prove)
goal (1 subgoal):
 1. (n + 2 ^ b - Suc 0) div 2 ^ b * 2 ^ b \<le> 2 ^ a proof (prove)
goal (1 subgoal):
 1. 2 ^ b dvd 2 ^ a proof (prove)
goal:
No subgoals! proof (state)
this:
(n + 2 ^ b - Suc 0) div 2 ^ b * 2 ^ b \<le> 2 ^ a

goal (1 subgoal):
 1. \<exists>bd. filter (\<lambda>i. i * 2 ^ b < n) [0..<2 ^ (a - b)] = [0..<bd] \<and> n \<le> bd * 2 ^ b \<and> bd * 2 ^ b \<le> 2 ^ a \<and> (bd - 1) * 2 ^ b \<le> n proof (state)
this:
(n + 2 ^ b - Suc 0) div 2 ^ b \<le> 2 ^ a div 2 ^ b

goal (1 subgoal):
 1. \<exists>bd. filter (\<lambda>i. i * 2 ^ b < n) [0..<2 ^ (a - b)] = [0..<bd] \<and> n \<le> bd * 2 ^ b \<and> bd * 2 ^ b \<le> 2 ^ a \<and> (bd - 1) * 2 ^ b \<le> n proof (prove)
goal (1 subgoal):
 1. \<exists>bd. filter (\<lambda>i. i * 2 ^ b < n) [0..<2 ^ (a - b)] = [0..<bd] \<and> n \<le> bd * 2 ^ b \<and> bd * 2 ^ b \<le> 2 ^ a \<and> (bd - 1) * 2 ^ b \<le> n proof (prove)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> \<exists>bd. filter (\<lambda>i. i * 2 ^ b < n) [0..<2 ^ (a - b)] = [0..<bd] \<and> n \<le> bd * 2 ^ b \<and> bd * 2 ^ b \<le> 2 ^ a \<and> (bd - 1) * 2 ^ b \<le> n
 2. n \<noteq> 0 \<Longrightarrow> \<exists>bd. filter (\<lambda>i. i * 2 ^ b < n) [0..<2 ^ (a - b)] = [0..<bd] \<and> n \<le> bd * 2 ^ b \<and> bd * 2 ^ b \<le> 2 ^ a \<and> (bd - 1) * 2 ^ b \<le> n proof (prove)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> \<exists>bd. filter (\<lambda>i. i * 2 ^ b < n) [0..<2 ^ (a - b)] = [0..<bd] \<and> n \<le> bd * 2 ^ b \<and> bd * 2 ^ b \<le> 2 ^ a \<and> (bd - 1) * 2 ^ b \<le> n proof (prove)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> filter (\<lambda>i. i * 2 ^ b < n) [0..<2 ^ (a - b)] = [0..<(n + (2 ^ b - 1)) div 2 ^ b] \<and> n \<le> (n + (2 ^ b - 1)) div 2 ^ b * 2 ^ b \<and> (n + (2 ^ b - 1)) div 2 ^ b * 2 ^ b \<le> 2 ^ a \<and> ((n + (2 ^ b - 1)) div 2 ^ b - 1) * 2 ^ b \<le> n proof (prove)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> ((\<forall>a ba. a \<le> ba \<longrightarrow> ba * 2 ^ b < n \<longrightarrow> a * 2 ^ b < n) \<and> \<not> (n + (2 ^ b - 1)) div 2 ^ b * 2 ^ b < n \<and> ((n + (2 ^ b - 1)) div 2 ^ b \<noteq> 0 \<longrightarrow> ((n + (2 ^ b - 1)) div 2 ^ b - 1) * 2 ^ b < n) \<and> (n + (2 ^ b - 1)) div 2 ^ b \<le> 2 ^ (a - b)) \<and> n \<le> (n + (2 ^ b - 1)) div 2 ^ b * 2 ^ b \<and> (n + (2 ^ b - 1)) div 2 ^ b * 2 ^ b \<le> 2 ^ a \<and> ((n + (2 ^ b - 1)) div 2 ^ b - 1) * 2 ^ b \<le> n proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> n \<le> (n + 2 ^ b - Suc 0) div 2 ^ b * 2 ^ b \<and> ((n + 2 ^ b - Suc 0) div 2 ^ b - Suc 0) * 2 ^ b \<le> n \<and> (n + 2 ^ b - Suc 0) div 2 ^ b * 2 ^ b \<le> 2 ^ a \<and> (\<forall>a ba. a \<le> ba \<longrightarrow> ba * 2 ^ b < n \<longrightarrow> a * 2 ^ b < n) \<and> n \<le> (n + 2 ^ b - Suc 0) div 2 ^ b * 2 ^ b \<and> (n + 2 ^ b - Suc 0) div 2 ^ b \<le> 2 ^ (a - b) \<and> (0 < (n + 2 ^ b - Suc 0) div 2 ^ b \<longrightarrow> ((n + 2 ^ b - Suc 0) div 2 ^ b - Suc 0) * 2 ^ b < n) proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> \<forall>a ba. a \<le> ba \<longrightarrow> ba * 2 ^ b < n \<longrightarrow> a * 2 ^ b < n proof (prove)
goal:
No subgoals! proof (state)
this:
\<exists>bd. filter (\<lambda>i. i * 2 ^ b < n) [0..<2 ^ (a - b)] = [0..<bd] \<and> n \<le> bd * 2 ^ b \<and> bd * 2 ^ b \<le> 2 ^ a \<and> (bd - 1) * 2 ^ b \<le> n

goal:
No subgoals!