equal
deleted
inserted
replaced
117 |
117 |
118 theorem prefix_length_le: "xs \<le> ys ==> length xs \<le> length ys" |
118 theorem prefix_length_le: "xs \<le> ys ==> length xs \<le> length ys" |
119 by (auto simp add: prefix_def) |
119 by (auto simp add: prefix_def) |
120 |
120 |
121 lemma prefix_same_cases: |
121 lemma prefix_same_cases: |
122 "(xs\<^isub>1::'a list) \<le> ys \<Longrightarrow> xs\<^isub>2 \<le> ys \<Longrightarrow> xs\<^isub>1 \<le> xs\<^isub>2 \<or> xs\<^isub>2 \<le> xs\<^isub>1" |
122 "(xs\<^sub>1::'a list) \<le> ys \<Longrightarrow> xs\<^sub>2 \<le> ys \<Longrightarrow> xs\<^sub>1 \<le> xs\<^sub>2 \<or> xs\<^sub>2 \<le> xs\<^sub>1" |
123 unfolding prefix_def by (metis append_eq_append_conv2) |
123 unfolding prefix_def by (metis append_eq_append_conv2) |
124 |
124 |
125 lemma set_mono_prefix: "xs \<le> ys \<Longrightarrow> set xs \<subseteq> set ys" |
125 lemma set_mono_prefix: "xs \<le> ys \<Longrightarrow> set xs \<subseteq> set ys" |
126 by (auto simp add: prefix_def) |
126 by (auto simp add: prefix_def) |
127 |
127 |