4780 ci (layout_of ap) (start_of (layout_of ap) k) (ap ! k)" |
4780 ci (layout_of ap) (start_of (layout_of ap) k) (ap ! k)" |
4781 apply(simp add: tms_of.simps tpairs_of.simps) |
4781 apply(simp add: tms_of.simps tpairs_of.simps) |
4782 done |
4782 done |
4783 |
4783 |
4784 lemma [elim]: "\<lbrakk>k < length ap; ap ! k = Inc n; |
4784 lemma [elim]: "\<lbrakk>k < length ap; ap ! k = Inc n; |
4785 (a, b) \<in> set (abacus.tshift (abacus.tshift tinc_b (2 * n)) |
4785 (a, b) \<in> set (tshift (tshift tinc_b (2 * n)) |
4786 (start_of (layout_of ap) k - Suc 0))\<rbrakk> |
4786 (start_of (layout_of ap) k - Suc 0))\<rbrakk> |
4787 \<Longrightarrow> b \<le> start_of (layout_of ap) (length ap)" |
4787 \<Longrightarrow> b \<le> start_of (layout_of ap) (length ap)" |
4788 apply(subgoal_tac "b \<le> start_of (layout_of ap) (Suc k)") |
4788 apply(subgoal_tac "b \<le> start_of (layout_of ap) (Suc k)") |
4789 apply(subgoal_tac "start_of (layout_of ap) (Suc k) \<le> start_of (layout_of ap) (length ap) ") |
4789 apply(subgoal_tac "start_of (layout_of ap) (Suc k) \<le> start_of (layout_of ap) (length ap) ") |
4790 apply(arith) |
4790 apply(arith) |
4792 apply(rule_tac start_of_le, simp) |
4792 apply(rule_tac start_of_le, simp) |
4793 apply(auto simp: tinc_b_def tshift.simps start_of.simps |
4793 apply(auto simp: tinc_b_def tshift.simps start_of.simps |
4794 layout_of.simps length_of.simps startof_not0) |
4794 layout_of.simps length_of.simps startof_not0) |
4795 done |
4795 done |
4796 |
4796 |
4797 lemma findnth_le[elim]: "(a, b) \<in> set (abacus.tshift (findnth n) (start_of (layout_of ap) k - Suc 0)) |
4797 lemma findnth_le[elim]: "(a, b) \<in> set (tshift (findnth n) (start_of (layout_of ap) k - Suc 0)) |
4798 \<Longrightarrow> b \<le> Suc (start_of (layout_of ap) k + 2 * n)" |
4798 \<Longrightarrow> b \<le> Suc (start_of (layout_of ap) k + 2 * n)" |
4799 apply(induct n, simp add: findnth.simps tshift.simps) |
4799 apply(induct n, simp add: findnth.simps tshift.simps) |
4800 apply(simp add: findnth.simps tshift_append, auto) |
4800 apply(simp add: findnth.simps tshift_append, auto) |
4801 apply(auto simp: tshift.simps) |
4801 apply(auto simp: tshift.simps) |
4802 done |
4802 done |
4803 |
4803 |
4804 |
4804 |
4805 lemma [elim]: "\<lbrakk>k < length ap; ap ! k = Inc n; (a, b) \<in> |
4805 lemma [elim]: "\<lbrakk>k < length ap; ap ! k = Inc n; (a, b) \<in> |
4806 set (abacus.tshift (findnth n) (start_of (layout_of ap) k - Suc 0))\<rbrakk> |
4806 set (tshift (findnth n) (start_of (layout_of ap) k - Suc 0))\<rbrakk> |
4807 \<Longrightarrow> b \<le> start_of (layout_of ap) (length ap)" |
4807 \<Longrightarrow> b \<le> start_of (layout_of ap) (length ap)" |
4808 apply(subgoal_tac "b \<le> start_of (layout_of ap) (Suc k)") |
4808 apply(subgoal_tac "b \<le> start_of (layout_of ap) (Suc k)") |
4809 apply(subgoal_tac "start_of (layout_of ap) (Suc k) \<le> start_of (layout_of ap) (length ap) ") |
4809 apply(subgoal_tac "start_of (layout_of ap) (Suc k) \<le> start_of (layout_of ap) (length ap) ") |
4810 apply(arith) |
4810 apply(arith) |
4811 apply(case_tac "Suc k = length ap", simp) |
4811 apply(case_tac "Suc k = length ap", simp) |
4829 auto simp: start_of_eq start_of_le) |
4829 auto simp: start_of_eq start_of_le) |
4830 done |
4830 done |
4831 |
4831 |
4832 lemma [elim]: "\<lbrakk>k < length ap; |
4832 lemma [elim]: "\<lbrakk>k < length ap; |
4833 ap ! k = Dec n e; |
4833 ap ! k = Dec n e; |
4834 (a, b) \<in> set (abacus.tshift (findnth n) (start_of (layout_of ap) k - Suc 0))\<rbrakk> |
4834 (a, b) \<in> set (tshift (findnth n) (start_of (layout_of ap) k - Suc 0))\<rbrakk> |
4835 \<Longrightarrow> b \<le> start_of (layout_of ap) (length ap)" |
4835 \<Longrightarrow> b \<le> start_of (layout_of ap) (length ap)" |
4836 apply(subgoal_tac "b \<le> start_of (layout_of ap) k + 2*n + 1 \<and> |
4836 apply(subgoal_tac "b \<le> start_of (layout_of ap) k + 2*n + 1 \<and> |
4837 start_of (layout_of ap) k + 2*n + 1 \<le> start_of (layout_of ap) (Suc k) \<and> |
4837 start_of (layout_of ap) k + 2*n + 1 \<le> start_of (layout_of ap) (Suc k) \<and> |
4838 start_of (layout_of ap) (Suc k) \<le> start_of (layout_of ap) (length ap)", auto) |
4838 start_of (layout_of ap) (Suc k) \<le> start_of (layout_of ap) (length ap)", auto) |
4839 apply(simp add: tshift.simps start_of.simps |
4839 apply(simp add: tshift.simps start_of.simps |
4840 layout_of.simps length_of.simps startof_not0) |
4840 layout_of.simps length_of.simps startof_not0) |
4841 apply(rule_tac start_of_all_le) |
4841 apply(rule_tac start_of_all_le) |
4842 done |
4842 done |
4843 |
4843 |
4844 thm length_of.simps |
4844 thm length_of.simps |
4845 lemma [elim]: "\<lbrakk>k < length ap; ap ! k = Dec n e; (a, b) \<in> set (abacus.tshift (abacus.tshift tdec_b (2 * n)) |
4845 lemma [elim]: "\<lbrakk>k < length ap; ap ! k = Dec n e; (a, b) \<in> set (tshift (tshift tdec_b (2 * n)) |
4846 (start_of (layout_of ap) k - Suc 0))\<rbrakk> |
4846 (start_of (layout_of ap) k - Suc 0))\<rbrakk> |
4847 \<Longrightarrow> b \<le> start_of (layout_of ap) (length ap)" |
4847 \<Longrightarrow> b \<le> start_of (layout_of ap) (length ap)" |
4848 apply(subgoal_tac "2*n + start_of (layout_of ap) k + 16 \<le> start_of (layout_of ap) (length ap) \<and> start_of (layout_of ap) k > 0") |
4848 apply(subgoal_tac "2*n + start_of (layout_of ap) k + 16 \<le> start_of (layout_of ap) (length ap) \<and> start_of (layout_of ap) k > 0") |
4849 prefer 2 |
4849 prefer 2 |
4850 apply(subgoal_tac "2 * n + start_of (layout_of ap) k + 16 = start_of (layout_of ap) (Suc k) |
4850 apply(subgoal_tac "2 * n + start_of (layout_of ap) k + 16 = start_of (layout_of ap) (Suc k) |