theory More_Word

lemma word_subset_less:
  "\<lbrakk> {x .. x + r - 1} \<subseteq> {y .. y + s - 1};
     x \<le> x + r - 1; y \<le> y + (s :: 'a :: len word) - 1;
     s \<noteq> 0 \<rbrakk>
     \<Longrightarrow> r \<le> s" apply (frule subsetD[where c=x]) apply simp apply (drule subsetD[where c="x + r - 1"]) apply simp apply (clarsimp simp: add_diff_eq[symmetric]) apply (drule(1) word_sub_mono2) apply (simp_all add: olen_add_eqv[symmetric]) apply (erule word_le_minus_cancel) apply (rule ccontr) apply (simp add: word_not_le) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{x..x + r - 1} \<subseteq> {y..y + s - 1}; x \<le> x + r - 1; y \<le> y + s - 1; s \<noteq> 0\<rbrakk> \<Longrightarrow> r \<le> s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>{x..x + r - 1} \<subseteq> {y..y + s - 1}; x \<le> x + r - 1; y \<le> y + s - 1; s \<noteq> 0\<rbrakk> \<Longrightarrow> x \<in> {x..x + r - 1}
 2. \<lbrakk>{x..x + r - 1} \<subseteq> {y..y + s - 1}; x \<le> x + r - 1; y \<le> y + s - 1; s \<noteq> 0; x \<in> {y..y + s - 1}\<rbrakk> \<Longrightarrow> r \<le> s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{x..x + r - 1} \<subseteq> {y..y + s - 1}; x \<le> x + r - 1; y \<le> y + s - 1; s \<noteq> 0; x \<in> {y..y + s - 1}\<rbrakk> \<Longrightarrow> r \<le> s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>x \<le> x + r - 1; y \<le> y + s - 1; s \<noteq> 0; x \<in> {y..y + s - 1}\<rbrakk> \<Longrightarrow> x + r - 1 \<in> {x..x + r - 1}
 2. \<lbrakk>x \<le> x + r - 1; y \<le> y + s - 1; s \<noteq> 0; x \<in> {y..y + s - 1}; x + r - 1 \<in> {y..y + s - 1}\<rbrakk> \<Longrightarrow> r \<le> s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> x + r - 1; y \<le> y + s - 1; s \<noteq> 0; x \<in> {y..y + s - 1}; x + r - 1 \<in> {y..y + s - 1}\<rbrakk> \<Longrightarrow> r \<le> s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> x + (r - 1); y \<le> y + (s - 1); s \<noteq> 0; y \<le> x; x \<le> y + (s - 1); y \<le> x + (r - 1); x + (r - 1) \<le> y + (s - 1)\<rbrakk> \<Longrightarrow> r \<le> s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>x \<le> x + (r - 1); y \<le> y + (s - 1); s \<noteq> 0; y \<le> x; x \<le> y + (s - 1); y \<le> x + (r - 1)\<rbrakk> \<Longrightarrow> r - 1 \<le> x + (r - 1)
 2. \<lbrakk>x \<le> x + (r - 1); y \<le> y + (s - 1); s \<noteq> 0; y \<le> x; x \<le> y + (s - 1); y \<le> x + (r - 1)\<rbrakk> \<Longrightarrow> s - 1 \<le> y + (s - 1)
 3. \<lbrakk>x \<le> x + (r - 1); y \<le> y + (s - 1); s \<noteq> 0; y \<le> x; x \<le> y + (s - 1); y \<le> x + (r - 1); r - 1 \<le> s - 1\<rbrakk> \<Longrightarrow> r \<le> s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> x + (r - 1); y \<le> y + (s - 1); s \<noteq> 0; y \<le> x; x \<le> y + (s - 1); y \<le> x + (r - 1); r - 1 \<le> s - 1\<rbrakk> \<Longrightarrow> r \<le> s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> x + (r - 1); y \<le> y + (s - 1); s \<noteq> 0; y \<le> x; x \<le> y + (s - 1); y \<le> x + (r - 1)\<rbrakk> \<Longrightarrow> 1 \<le> s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> x + (r - 1); y \<le> y + (s - 1); s \<noteq> 0; y \<le> x; x \<le> y + (s - 1); y \<le> x + (r - 1); \<not> 1 \<le> s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!