equal
deleted
inserted
replaced
113 |
113 |
114 theorem prefixeq_length_le: "prefixeq xs ys \<Longrightarrow> length xs \<le> length ys" |
114 theorem prefixeq_length_le: "prefixeq xs ys \<Longrightarrow> length xs \<le> length ys" |
115 by (auto simp add: prefixeq_def) |
115 by (auto simp add: prefixeq_def) |
116 |
116 |
117 lemma prefixeq_same_cases: |
117 lemma prefixeq_same_cases: |
118 "prefixeq (xs\<^isub>1::'a list) ys \<Longrightarrow> prefixeq xs\<^isub>2 ys \<Longrightarrow> prefixeq xs\<^isub>1 xs\<^isub>2 \<or> prefixeq xs\<^isub>2 xs\<^isub>1" |
118 "prefixeq (xs\<^sub>1::'a list) ys \<Longrightarrow> prefixeq xs\<^sub>2 ys \<Longrightarrow> prefixeq xs\<^sub>1 xs\<^sub>2 \<or> prefixeq xs\<^sub>2 xs\<^sub>1" |
119 unfolding prefixeq_def by (metis append_eq_append_conv2) |
119 unfolding prefixeq_def by (metis append_eq_append_conv2) |
120 |
120 |
121 lemma set_mono_prefixeq: "prefixeq xs ys \<Longrightarrow> set xs \<subseteq> set ys" |
121 lemma set_mono_prefixeq: "prefixeq xs ys \<Longrightarrow> set xs \<subseteq> set ys" |
122 by (auto simp add: prefixeq_def) |
122 by (auto simp add: prefixeq_def) |
123 |
123 |