theory Word_Lemmas

lemma word_enum_prefix:
  "[x .e. (y ::'a::len word)] = as @ a # bs \<Longrightarrow> as = (if x < a then [x .e. a - 1] else [])" apply (induct as arbitrary: x; clarsimp) apply (case_tac "x < y") prefer 2 apply (case_tac "x = y", simp) apply (simp add: not_less) apply (drule (1) dual_order.not_eq_order_implies_strict) apply (simp add: word_upto_Nil) apply (simp add: word_upto_Cons_eq) apply (case_tac "x < y") prefer 2 apply (case_tac "x = y", simp) apply (simp add: not_less) apply (drule (1) dual_order.not_eq_order_implies_strict) apply (simp add: word_upto_Nil) apply (clarsimp simp: word_upto_Cons_eq) apply (frule word_enum_decomp_elem) apply clarsimp apply (rule conjI) prefer 2 apply (subst word_Suc_le[symmetric]; clarsimp) apply (drule meta_spec) apply (drule (1) meta_mp) apply clarsimp apply (rule conjI; clarsimp) apply (subst (2) word_upto_Cons_eq) apply unat_arith apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. [x .e. y] = as @ a # bs \<Longrightarrow> as = (if x < a then [x .e. a - 1] else []) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>[x .e. y] = a # bs; x < a\<rbrakk> \<Longrightarrow> [] = [x .e. a - 1]
 2. \<And>aa as x. \<lbrakk>\<And>x. [x .e. y] = as @ a # bs \<Longrightarrow> as = (if x < a then [x .e. a - 1] else []); [x .e. y] = aa # as @ a # bs\<rbrakk> \<Longrightarrow> (x < a \<longrightarrow> aa # as = [x .e. a - 1]) \<and> x < a proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>[x .e. y] = a # bs; x < a; x < y\<rbrakk> \<Longrightarrow> [] = [x .e. a - 1]
 2. \<And>x. \<lbrakk>[x .e. y] = a # bs; x < a; \<not> x < y\<rbrakk> \<Longrightarrow> [] = [x .e. a - 1]
 3. \<And>aa as x. \<lbrakk>\<And>x. [x .e. y] = as @ a # bs \<Longrightarrow> as = (if x < a then [x .e. a - 1] else []); [x .e. y] = aa # as @ a # bs\<rbrakk> \<Longrightarrow> (x < a \<longrightarrow> aa # as = [x .e. a - 1]) \<and> x < a proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>[x .e. y] = a # bs; x < a; \<not> x < y\<rbrakk> \<Longrightarrow> [] = [x .e. a - 1]
 2. \<And>x. \<lbrakk>[x .e. y] = a # bs; x < a; x < y\<rbrakk> \<Longrightarrow> [] = [x .e. a - 1]
 3. \<And>aa as x. \<lbrakk>\<And>x. [x .e. y] = as @ a # bs \<Longrightarrow> as = (if x < a then [x .e. a - 1] else []); [x .e. y] = aa # as @ a # bs\<rbrakk> \<Longrightarrow> (x < a \<longrightarrow> aa # as = [x .e. a - 1]) \<and> x < a proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>[x .e. y] = a # bs; x < a; \<not> x < y; x \<noteq> y\<rbrakk> \<Longrightarrow> [] = [x .e. a - 1]
 2. \<And>x. \<lbrakk>[x .e. y] = a # bs; x < a; x < y\<rbrakk> \<Longrightarrow> [] = [x .e. a - 1]
 3. \<And>aa as x. \<lbrakk>\<And>x. [x .e. y] = as @ a # bs \<Longrightarrow> as = (if x < a then [x .e. a - 1] else []); [x .e. y] = aa # as @ a # bs\<rbrakk> \<Longrightarrow> (x < a \<longrightarrow> aa # as = [x .e. a - 1]) \<and> x < a proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>[x .e. y] = a # bs; x < a; y \<le> x; x \<noteq> y\<rbrakk> \<Longrightarrow> [] = [x .e. a - 1]
 2. \<And>x. \<lbrakk>[x .e. y] = a # bs; x < a; x < y\<rbrakk> \<Longrightarrow> [] = [x .e. a - 1]
 3. \<And>aa as x. \<lbrakk>\<And>x. [x .e. y] = as @ a # bs \<Longrightarrow> as = (if x < a then [x .e. a - 1] else []); [x .e. y] = aa # as @ a # bs\<rbrakk> \<Longrightarrow> (x < a \<longrightarrow> aa # as = [x .e. a - 1]) \<and> x < a proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>[x .e. y] = a # bs; x < a; y \<le> x; y < x\<rbrakk> \<Longrightarrow> [] = [x .e. a - 1]
 2. \<And>x. \<lbrakk>[x .e. y] = a # bs; x < a; x < y\<rbrakk> \<Longrightarrow> [] = [x .e. a - 1]
 3. \<And>aa as x. \<lbrakk>\<And>x. [x .e. y] = as @ a # bs \<Longrightarrow> as = (if x < a then [x .e. a - 1] else []); [x .e. y] = aa # as @ a # bs\<rbrakk> \<Longrightarrow> (x < a \<longrightarrow> aa # as = [x .e. a - 1]) \<and> x < a proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>[x .e. y] = a # bs; x < a; x < y\<rbrakk> \<Longrightarrow> [] = [x .e. a - 1]
 2. \<And>aa as x. \<lbrakk>\<And>x. [x .e. y] = as @ a # bs \<Longrightarrow> as = (if x < a then [x .e. a - 1] else []); [x .e. y] = aa # as @ a # bs\<rbrakk> \<Longrightarrow> (x < a \<longrightarrow> aa # as = [x .e. a - 1]) \<and> x < a proof (prove)
goal (1 subgoal):
 1. \<And>aa as x. \<lbrakk>\<And>x. [x .e. y] = as @ a # bs \<Longrightarrow> as = (if x < a then [x .e. a - 1] else []); [x .e. y] = aa # as @ a # bs\<rbrakk> \<Longrightarrow> (x < a \<longrightarrow> aa # as = [x .e. a - 1]) \<and> x < a proof (prove)
goal (2 subgoals):
 1. \<And>aa as x. \<lbrakk>\<And>x. [x .e. y] = as @ a # bs \<Longrightarrow> as = (if x < a then [x .e. a - 1] else []); [x .e. y] = aa # as @ a # bs; x < y\<rbrakk> \<Longrightarrow> (x < a \<longrightarrow> aa # as = [x .e. a - 1]) \<and> x < a
 2. \<And>aa as x. \<lbrakk>\<And>x. [x .e. y] = as @ a # bs \<Longrightarrow> as = (if x < a then [x .e. a - 1] else []); [x .e. y] = aa # as @ a # bs; \<not> x < y\<rbrakk> \<Longrightarrow> (x < a \<longrightarrow> aa # as = [x .e. a - 1]) \<and> x < a proof (prove)
goal (2 subgoals):
 1. \<And>aa as x. \<lbrakk>\<And>x. [x .e. y] = as @ a # bs \<Longrightarrow> as = (if x < a then [x .e. a - 1] else []); [x .e. y] = aa # as @ a # bs; \<not> x < y\<rbrakk> \<Longrightarrow> (x < a \<longrightarrow> aa # as = [x .e. a - 1]) \<and> x < a
 2. \<And>aa as x. \<lbrakk>\<And>x. [x .e. y] = as @ a # bs \<Longrightarrow> as = (if x < a then [x .e. a - 1] else []); [x .e. y] = aa # as @ a # bs; x < y\<rbrakk> \<Longrightarrow> (x < a \<longrightarrow> aa # as = [x .e. a - 1]) \<and> x < a proof (prove)
goal (2 subgoals):
 1. \<And>aa as x. \<lbrakk>\<And>x. [x .e. y] = as @ a # bs \<Longrightarrow> as = (if x < a then [x .e. a - 1] else []); [x .e. y] = aa # as @ a # bs; \<not> x < y; x \<noteq> y\<rbrakk> \<Longrightarrow> (x < a \<longrightarrow> aa # as = [x .e. a - 1]) \<and> x < a
 2. \<And>aa as x. \<lbrakk>\<And>x. [x .e. y] = as @ a # bs \<Longrightarrow> as = (if x < a then [x .e. a - 1] else []); [x .e. y] = aa # as @ a # bs; x < y\<rbrakk> \<Longrightarrow> (x < a \<longrightarrow> aa # as = [x .e. a - 1]) \<and> x < a proof (prove)
goal (2 subgoals):
 1. \<And>aa as x. \<lbrakk>\<And>x. [x .e. y] = as @ a # bs \<Longrightarrow> as = (if x < a then [x .e. a - 1] else []); [x .e. y] = aa # as @ a # bs; y \<le> x; x \<noteq> y\<rbrakk> \<Longrightarrow> (x < a \<longrightarrow> aa # as = [x .e. a - 1]) \<and> x < a
 2. \<And>aa as x. \<lbrakk>\<And>x. [x .e. y] = as @ a # bs \<Longrightarrow> as = (if x < a then [x .e. a - 1] else []); [x .e. y] = aa # as @ a # bs; x < y\<rbrakk> \<Longrightarrow> (x < a \<longrightarrow> aa # as = [x .e. a - 1]) \<and> x < a proof (prove)
goal (2 subgoals):
 1. \<And>aa as x. \<lbrakk>\<And>x. [x .e. y] = as @ a # bs \<Longrightarrow> as = (if x < a then [x .e. a - 1] else []); [x .e. y] = aa # as @ a # bs; y \<le> x; y < x\<rbrakk> \<Longrightarrow> (x < a \<longrightarrow> aa # as = [x .e. a - 1]) \<and> x < a
 2. \<And>aa as x. \<lbrakk>\<And>x. [x .e. y] = as @ a # bs \<Longrightarrow> as = (if x < a then [x .e. a - 1] else []); [x .e. y] = aa # as @ a # bs; x < y\<rbrakk> \<Longrightarrow> (x < a \<longrightarrow> aa # as = [x .e. a - 1]) \<and> x < a proof (prove)
goal (1 subgoal):
 1. \<And>aa as x. \<lbrakk>\<And>x. [x .e. y] = as @ a # bs \<Longrightarrow> as = (if x < a then [x .e. a - 1] else []); [x .e. y] = aa # as @ a # bs; x < y\<rbrakk> \<Longrightarrow> (x < a \<longrightarrow> aa # as = [x .e. a - 1]) \<and> x < a proof (prove)
goal (1 subgoal):
 1. \<And>aa as. \<lbrakk>\<And>x. [x .e. y] = as @ a # bs \<Longrightarrow> as = (if x < a then [x .e. a - 1] else []); [aa + 1 .e. y] = as @ a # bs; aa < y\<rbrakk> \<Longrightarrow> (aa < a \<longrightarrow> aa # as = [aa .e. a - 1]) \<and> aa < a proof (prove)
goal (1 subgoal):
 1. \<And>aa as. \<lbrakk>\<And>x. [x .e. y] = as @ a # bs \<Longrightarrow> as = (if x < a then [x .e. a - 1] else []); [aa + 1 .e. y] = as @ a # bs; aa < y; aa + 1 \<le> a \<and> a \<le> y\<rbrakk> \<Longrightarrow> (aa < a \<longrightarrow> aa # as = [aa .e. a - 1]) \<and> aa < a proof (prove)
goal (1 subgoal):
 1. \<And>aa as. \<lbrakk>\<And>x. [x .e. y] = as @ a # bs \<Longrightarrow> as = (if x < a then [x .e. a - 1] else []); [aa + 1 .e. y] = as @ a # bs; aa < y; aa + 1 \<le> a; a \<le> y\<rbrakk> \<Longrightarrow> (aa < a \<longrightarrow> aa # as = [aa .e. a - 1]) \<and> aa < a proof (prove)
goal (2 subgoals):
 1. \<And>aa as. \<lbrakk>\<And>x. [x .e. y] = as @ a # bs \<Longrightarrow> as = (if x < a then [x .e. a - 1] else []); [aa + 1 .e. y] = as @ a # bs; aa < y; aa + 1 \<le> a; a \<le> y\<rbrakk> \<Longrightarrow> aa < a \<longrightarrow> aa # as = [aa .e. a - 1]
 2. \<And>aa as. \<lbrakk>\<And>x. [x .e. y] = as @ a # bs \<Longrightarrow> as = (if x < a then [x .e. a - 1] else []); [aa + 1 .e. y] = as @ a # bs; aa < y; aa + 1 \<le> a; a \<le> y\<rbrakk> \<Longrightarrow> aa < a proof (prove)
goal (2 subgoals):
 1. \<And>aa as. \<lbrakk>\<And>x. [x .e. y] = as @ a # bs \<Longrightarrow> as = (if x < a then [x .e. a - 1] else []); [aa + 1 .e. y] = as @ a # bs; aa < y; aa + 1 \<le> a; a \<le> y\<rbrakk> \<Longrightarrow> aa < a
 2. \<And>aa as. \<lbrakk>\<And>x. [x .e. y] = as @ a # bs \<Longrightarrow> as = (if x < a then [x .e. a - 1] else []); [aa + 1 .e. y] = as @ a # bs; aa < y; aa + 1 \<le> a; a \<le> y\<rbrakk> \<Longrightarrow> aa < a \<longrightarrow> aa # as = [aa .e. a - 1] proof (prove)
goal (1 subgoal):
 1. \<And>aa as. \<lbrakk>\<And>x. [x .e. y] = as @ a # bs \<Longrightarrow> as = (if x < a then [x .e. a - 1] else []); [aa + 1 .e. y] = as @ a # bs; aa < y; aa + 1 \<le> a; a \<le> y\<rbrakk> \<Longrightarrow> aa < a \<longrightarrow> aa # as = [aa .e. a - 1] proof (prove)
goal (1 subgoal):
 1. \<And>aa as. \<lbrakk>[aa + 1 .e. y] = as @ a # bs; aa < y; aa + 1 \<le> a; a \<le> y; [?x41 aa as .e. y] = as @ a # bs \<Longrightarrow> as = (if ?x41 aa as < a then [?x41 aa as .e. a - 1] else [])\<rbrakk> \<Longrightarrow> aa < a \<longrightarrow> aa # as = [aa .e. a - 1] proof (prove)
goal (1 subgoal):
 1. \<And>aa as. \<lbrakk>[aa + 1 .e. y] = as @ a # bs; aa < y; aa + 1 \<le> a; a \<le> y; as = (if aa + 1 < a then [aa + 1 .e. a - 1] else [])\<rbrakk> \<Longrightarrow> aa < a \<longrightarrow> aa # as = [aa .e. a - 1] proof (prove)
goal (1 subgoal):
 1. \<And>aa. \<lbrakk>[aa + 1 .e. y] = (if aa + 1 < a then [aa + 1 .e. a - 1] else []) @ a # bs; aa < y; aa + 1 \<le> a; a \<le> y\<rbrakk> \<Longrightarrow> (aa + 1 < a \<longrightarrow> aa < a \<longrightarrow> aa # [aa + 1 .e. a - 1] = [aa .e. a - 1]) \<and> (aa + 1 = a \<longrightarrow> aa < a \<longrightarrow> [aa] = [aa .e. a - 1]) proof (prove)
goal (1 subgoal):
 1. \<And>aa. \<lbrakk>[aa + 1 .e. y] = [aa + 1 .e. a - 1] @ a # bs; aa < y; aa + 1 \<le> a; a \<le> y; aa + 1 < a; aa < a\<rbrakk> \<Longrightarrow> aa # [aa + 1 .e. a - 1] = [aa .e. a - 1] proof (prove)
goal (2 subgoals):
 1. \<And>aa. \<lbrakk>[aa + 1 .e. y] = [aa + 1 .e. a - 1] @ a # bs; aa < y; aa + 1 \<le> a; a \<le> y; aa + 1 < a; aa < a\<rbrakk> \<Longrightarrow> aa < a - 1
 2. \<And>aa. \<lbrakk>[aa + 1 .e. y] = [aa + 1 .e. a - 1] @ a # bs; aa < y; aa + 1 \<le> a; a \<le> y; aa + 1 < a; aa < a\<rbrakk> \<Longrightarrow> aa # [aa + 1 .e. a - 1] = aa # [aa + 1 .e. a - 1] proof (prove)
goal (1 subgoal):
 1. \<And>aa. \<lbrakk>[aa + 1 .e. y] = [aa + 1 .e. a - 1] @ a # bs; aa < y; aa + 1 \<le> a; a \<le> y; aa + 1 < a; aa < a\<rbrakk> \<Longrightarrow> aa # [aa + 1 .e. a - 1] = aa # [aa + 1 .e. a - 1] proof (prove)
goal:
No subgoals!