theory Structures_A

lemma msg_align_bits':
  "msg_align_bits = word_size_bits + 7" proof - have "(LEAST n. (cap_transfer_data_size + msg_max_length + msg_max_extra_caps + 2) \<le> 2 ^ n) = 7" proof (rule Least_equality) show "(cap_transfer_data_size + msg_max_length + msg_max_extra_caps + 2)  \<le> 2 ^ 7" by (simp add: cap_transfer_data_size_def msg_max_length_def msg_max_extra_caps_def) next fix y assume "(cap_transfer_data_size + msg_max_length + msg_max_extra_caps + 2) \<le> 2 ^ y" hence "(2 :: nat) ^ 7 \<le> 2 ^ y" by (simp add: cap_transfer_data_size_def msg_max_length_def msg_max_extra_caps_def) thus "7 \<le> y" by (rule power_le_imp_le_exp [rotated], simp) qed thus ?thesis unfolding msg_align_bits_def max_ipc_length_def by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. msg_align_bits = word_size_bits + 7 proof (state)
goal (1 subgoal):
 1. msg_align_bits = word_size_bits + 7 proof (prove)
goal (1 subgoal):
 1. (LEAST n. cap_transfer_data_size + msg_max_length + msg_max_extra_caps + 2 \<le> 2 ^ n) = 7 proof (state)
goal (2 subgoals):
 1. cap_transfer_data_size + msg_max_length + msg_max_extra_caps + 2 \<le> 2 ^ 7
 2. \<And>y. cap_transfer_data_size + msg_max_length + msg_max_extra_caps + 2 \<le> 2 ^ y \<Longrightarrow> 7 \<le> y proof (prove)
goal (1 subgoal):
 1. cap_transfer_data_size + msg_max_length + msg_max_extra_caps + 2 \<le> 2 ^ 7 proof (state)
this:
cap_transfer_data_size + msg_max_length + msg_max_extra_caps + 2 \<le> 2 ^ 7

goal (1 subgoal):
 1. \<And>y. cap_transfer_data_size + msg_max_length + msg_max_extra_caps + 2 \<le> 2 ^ y \<Longrightarrow> 7 \<le> y proof (state)
goal (1 subgoal):
 1. \<And>y. cap_transfer_data_size + msg_max_length + msg_max_extra_caps + 2 \<le> 2 ^ y \<Longrightarrow> 7 \<le> y proof (state)
goal (1 subgoal):
 1. \<And>y. cap_transfer_data_size + msg_max_length + msg_max_extra_caps + 2 \<le> 2 ^ y \<Longrightarrow> 7 \<le> y proof (state)
this:
cap_transfer_data_size + msg_max_length + msg_max_extra_caps + 2 \<le> 2 ^ y

goal (1 subgoal):
 1. \<And>y. cap_transfer_data_size + msg_max_length + msg_max_extra_caps + 2 \<le> 2 ^ y \<Longrightarrow> 7 \<le> y proof (prove)
using this:
cap_transfer_data_size + msg_max_length + msg_max_extra_caps + 2 \<le> 2 ^ y

goal (1 subgoal):
 1. 2 ^ 7 \<le> 2 ^ y proof (state)
this:
2 ^ 7 \<le> 2 ^ y

goal (1 subgoal):
 1. \<And>y. cap_transfer_data_size + msg_max_length + msg_max_extra_caps + 2 \<le> 2 ^ y \<Longrightarrow> 7 \<le> y proof (prove)
using this:
2 ^ 7 \<le> 2 ^ y

goal (1 subgoal):
 1. 7 \<le> y proof (state)
this:
7 \<le> y

goal:
No subgoals! proof (state)
this:
(LEAST n. cap_transfer_data_size + msg_max_length + msg_max_extra_caps + 2 \<le> 2 ^ n) = 7

goal (1 subgoal):
 1. msg_align_bits = word_size_bits + 7 proof (prove)
using this:
(LEAST n. cap_transfer_data_size + msg_max_length + msg_max_extra_caps + 2 \<le> 2 ^ n) = 7

goal (1 subgoal):
 1. msg_align_bits = word_size_bits + 7 proof (prove)
using this:
(LEAST n. cap_transfer_data_size + msg_max_length + msg_max_extra_caps + 2 \<le> 2 ^ n) = 7

goal (1 subgoal):
 1. word_size_bits + (LEAST n. cap_transfer_data_size + msg_max_length + msg_max_extra_caps + 2 \<le> 2 ^ n) = word_size_bits + 7 proof (state)
this:
msg_align_bits = word_size_bits + 7

goal:
No subgoals!