List_Prefix.thy
changeset 13 dd1499f296ea
parent 1 dcde836219bc
equal deleted inserted replaced
12:fb962189e921 13:dd1499f296ea
   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