equal
deleted
inserted
replaced
4907 done |
4907 done |
4908 |
4908 |
4909 lemma tms_any_less: |
4909 lemma tms_any_less: |
4910 "\<lbrakk>k < length ap; (a, b) \<in> set (tms_of ap ! k)\<rbrakk> \<Longrightarrow> |
4910 "\<lbrakk>k < length ap; (a, b) \<in> set (tms_of ap ! k)\<rbrakk> \<Longrightarrow> |
4911 b \<le> start_of (layout_of ap) (length ap)" |
4911 b \<le> start_of (layout_of ap) (length ap)" |
4912 apply(case_tac "ap!k", auto simp: tms_of.simps tpairs_of.simps ci.simps shift_append sete.simps) |
4912 apply(case_tac "ap!k", auto simp: tms_of.simps tpairs_of.simps ci.simps shift_append adjust.simps) |
4913 apply(erule_tac findnth_state_all_le1, simp_all) |
4913 apply(erule_tac findnth_state_all_le1, simp_all) |
4914 apply(erule_tac inc_state_all_le, simp_all) |
4914 apply(erule_tac inc_state_all_le, simp_all) |
4915 apply(erule_tac findnth_state_all_le2, simp_all) |
4915 apply(erule_tac findnth_state_all_le2, simp_all) |
4916 apply(rule_tac start_of_all_le) |
4916 apply(rule_tac start_of_all_le) |
4917 apply(rule_tac dec_state_all_le, simp_all) |
4917 apply(rule_tac dec_state_all_le, simp_all) |
4949 lemma length_ci: |
4949 lemma length_ci: |
4950 "\<lbrakk>k < length ap; length (ci ly y (ap ! k)) = 2 * qa\<rbrakk> |
4950 "\<lbrakk>k < length ap; length (ci ly y (ap ! k)) = 2 * qa\<rbrakk> |
4951 \<Longrightarrow> layout_of ap ! k = qa" |
4951 \<Longrightarrow> layout_of ap ! k = qa" |
4952 apply(case_tac "ap ! k") |
4952 apply(case_tac "ap ! k") |
4953 apply(auto simp: layout_of.simps ci.simps |
4953 apply(auto simp: layout_of.simps ci.simps |
4954 length_of.simps tinc_b_def tdec_b_def length_findnth sete.simps) |
4954 length_of.simps tinc_b_def tdec_b_def length_findnth adjust.simps) |
4955 done |
4955 done |
4956 |
4956 |
4957 lemma [intro]: "length (ci ly y i) mod 2 = 0" |
4957 lemma [intro]: "length (ci ly y i) mod 2 = 0" |
4958 apply(case_tac i, auto simp: ci.simps length_findnth |
4958 apply(case_tac i, auto simp: ci.simps length_findnth |
4959 tinc_b_def sete.simps tdec_b_def) |
4959 tinc_b_def adjust.simps tdec_b_def) |
4960 done |
4960 done |
4961 |
4961 |
4962 lemma [intro]: "listsum (map (length \<circ> (\<lambda>(x, y). ci ly x y)) zs) mod 2 = 0" |
4962 lemma [intro]: "listsum (map (length \<circ> (\<lambda>(x, y). ci ly x y)) zs) mod 2 = 0" |
4963 apply(induct zs rule: list_tl_induct, simp) |
4963 apply(induct zs rule: list_tl_induct, simp) |
4964 apply(case_tac a, simp) |
4964 apply(case_tac a, simp) |