misc lemmas about prefix, postfix, and parallel
authorkleing
Mon Nov 05 22:51:16 2007 +0100 (2007-11-05)
changeset 25299c3542f70b0fd
parent 25298 63f6d969253e
child 25300 bc3a1c964704
misc lemmas about prefix, postfix, and parallel
src/HOL/Library/List_Prefix.thy
     1.1 --- a/src/HOL/Library/List_Prefix.thy	Mon Nov 05 22:50:48 2007 +0100
     1.2 +++ b/src/HOL/Library/List_Prefix.thy	Mon Nov 05 22:51:16 2007 +0100
     1.3 @@ -155,6 +155,91 @@
     1.4      "xs \<le> ys \<Longrightarrow> set xs \<subseteq> set ys"
     1.5    by (auto simp add: prefix_def)
     1.6  
     1.7 +lemma take_is_prefix:
     1.8 +  "take n xs \<le> xs"
     1.9 +  apply (simp add: prefix_def)
    1.10 +  apply (rule_tac x="drop n xs" in exI)
    1.11 +  apply simp
    1.12 +  done
    1.13 +
    1.14 +lemma prefix_length_less:
    1.15 +  "xs < ys \<Longrightarrow> length xs < length ys"
    1.16 +  apply (clarsimp simp: strict_prefix_def)
    1.17 +  apply (frule prefix_length_le)
    1.18 +  apply (rule ccontr, simp)
    1.19 +  apply (clarsimp simp: prefix_def)
    1.20 +  done
    1.21 +
    1.22 +lemma strict_prefix_simps [simp]:
    1.23 +  "xs < [] = False"
    1.24 +  "[] < (x # xs) = True"
    1.25 +  "(x # xs) < (y # ys) = (x = y \<and> xs < ys)"
    1.26 +  by (simp_all add: strict_prefix_def cong: conj_cong)
    1.27 +
    1.28 +lemma take_strict_prefix:
    1.29 +  "xs < ys \<Longrightarrow> take n xs < ys"
    1.30 +  apply (induct n arbitrary: xs ys)
    1.31 +   apply (case_tac ys, simp_all)[1]
    1.32 +  apply (case_tac xs, simp)
    1.33 +  apply (case_tac ys, simp_all)
    1.34 +  done
    1.35 +
    1.36 +lemma not_prefix_cases: 
    1.37 +  assumes pfx: "\<not> ps \<le> ls"
    1.38 +  and c1: "\<lbrakk> ps \<noteq> []; ls = [] \<rbrakk> \<Longrightarrow> R"
    1.39 +  and c2: "\<And>a as x xs. \<lbrakk> ps = a#as; ls = x#xs; x = a; \<not> as \<le> xs\<rbrakk> \<Longrightarrow> R"
    1.40 +  and c3: "\<And>a as x xs. \<lbrakk> ps = a#as; ls = x#xs; x \<noteq> a\<rbrakk> \<Longrightarrow> R"
    1.41 +  shows "R"  
    1.42 +proof (cases ps)
    1.43 +  case Nil thus ?thesis using pfx by simp
    1.44 +next
    1.45 +  case (Cons a as)
    1.46 +  
    1.47 +  hence c: "ps = a#as" .
    1.48 +  
    1.49 +  show ?thesis
    1.50 +  proof (cases ls)
    1.51 +    case Nil thus ?thesis 
    1.52 +      by (intro c1, simp add: Cons)
    1.53 +  next
    1.54 +    case (Cons x xs)
    1.55 +    show ?thesis
    1.56 +    proof (cases "x = a")
    1.57 +      case True 
    1.58 +      show ?thesis 
    1.59 +      proof (intro c2) 
    1.60 +     	  show "\<not> as \<le> xs" using pfx c Cons True
    1.61 +	        by simp
    1.62 +      qed
    1.63 +    next 
    1.64 +      case False 
    1.65 +      show ?thesis by (rule c3)
    1.66 +    qed
    1.67 +  qed
    1.68 +qed
    1.69 +
    1.70 +lemma not_prefix_induct [consumes 1, case_names Nil Neq Eq]:
    1.71 +  assumes np: "\<not> ps \<le> ls"
    1.72 +  and base:   "\<And>x xs. P (x#xs) []"
    1.73 +  and r1:     "\<And>x xs y ys. x \<noteq> y \<Longrightarrow> P (x#xs) (y#ys)"
    1.74 +  and r2:     "\<And>x xs y ys. \<lbrakk> x = y; \<not> xs \<le> ys; P xs ys \<rbrakk> \<Longrightarrow> P (x#xs) (y#ys)"
    1.75 +  shows "P ps ls"
    1.76 +  using np
    1.77 +proof (induct ls arbitrary: ps)
    1.78 +  case Nil thus ?case  
    1.79 +    by (auto simp: neq_Nil_conv elim!: not_prefix_cases intro!: base)
    1.80 +next
    1.81 +  case (Cons y ys)  
    1.82 +  hence npfx: "\<not> ps \<le> (y # ys)" by simp
    1.83 +  then obtain x xs where pv: "ps = x # xs" 
    1.84 +    by (rule not_prefix_cases) auto
    1.85 +
    1.86 +  from Cons
    1.87 +  have ih: "\<And>ps. \<not>ps \<le> ys \<Longrightarrow> P ps ys" by simp
    1.88 +  
    1.89 +  show ?case using npfx
    1.90 +    by (simp only: pv) (erule not_prefix_cases, auto intro: r1 r2 ih)
    1.91 +qed
    1.92  
    1.93  subsection {* Parallel lists *}
    1.94  
    1.95 @@ -214,6 +299,19 @@
    1.96    qed
    1.97  qed
    1.98  
    1.99 +lemma parallel_append:
   1.100 +  "a \<parallel> b \<Longrightarrow> a @ c \<parallel> b @ d"
   1.101 +  by (rule parallelI) 
   1.102 +     (erule parallelE, erule conjE, 
   1.103 +            induct rule: not_prefix_induct, simp+)+
   1.104 +
   1.105 +lemma parallel_appendI: 
   1.106 +  "\<lbrakk> xs \<parallel> ys; x = xs @ xs' ; y = ys @ ys' \<rbrakk> \<Longrightarrow> x \<parallel> y"
   1.107 +  by simp (rule parallel_append)
   1.108 +
   1.109 +lemma parallel_commute:
   1.110 +  "(a \<parallel> b) = (b \<parallel> a)" 
   1.111 +  unfolding parallel_def by auto
   1.112  
   1.113  subsection {* Postfix order on lists *}
   1.114  
   1.115 @@ -280,6 +378,74 @@
   1.116    then show "xs >>= ys" ..
   1.117  qed
   1.118  
   1.119 +lemma distinct_postfix:
   1.120 +  assumes dx: "distinct xs"
   1.121 +  and     pf: "xs >>= ys"
   1.122 +  shows   "distinct ys"
   1.123 +  using dx pf by (clarsimp elim!: postfixE)
   1.124 +
   1.125 +lemma postfix_map:
   1.126 +  assumes pf: "xs >>= ys" 
   1.127 +  shows   "map f xs >>= map f ys"
   1.128 +  using pf by (auto elim!: postfixE intro: postfixI)
   1.129 +
   1.130 +lemma postfix_drop:
   1.131 +  "as >>= drop n as"
   1.132 +  unfolding postfix_def
   1.133 +  by (rule exI [where x = "take n as"]) simp
   1.134 +
   1.135 +lemma postfix_take:
   1.136 +  "xs >>= ys \<Longrightarrow> xs = take (length xs - length ys) xs @ ys"
   1.137 +  by (clarsimp elim!: postfixE)
   1.138 +
   1.139 +lemma parallelD1: 
   1.140 +  "x \<parallel> y \<Longrightarrow> \<not> x \<le> y" by blast
   1.141 +
   1.142 +lemma parallelD2: 
   1.143 +  "x \<parallel> y \<Longrightarrow> \<not> y \<le> x" by blast
   1.144 +  
   1.145 +lemma parallel_Nil1 [simp]: "\<not> x \<parallel> []" 
   1.146 +  unfolding parallel_def by simp
   1.147 +  
   1.148 +lemma parallel_Nil2 [simp]: "\<not> [] \<parallel> x"
   1.149 +  unfolding parallel_def by simp
   1.150 +
   1.151 +lemma Cons_parallelI1:
   1.152 +  "a \<noteq> b \<Longrightarrow> a # as \<parallel> b # bs" by auto
   1.153 +
   1.154 +lemma Cons_parallelI2:
   1.155 +  "\<lbrakk> a = b; as \<parallel> bs \<rbrakk> \<Longrightarrow> a # as \<parallel> b # bs" 
   1.156 +  apply simp
   1.157 +  apply (rule parallelI)
   1.158 +   apply simp
   1.159 +   apply (erule parallelD1)
   1.160 +  apply simp
   1.161 +  apply (erule parallelD2)
   1.162 + done
   1.163 +
   1.164 +lemma not_equal_is_parallel:
   1.165 +  assumes neq: "xs \<noteq> ys"
   1.166 +  and     len: "length xs = length ys"
   1.167 +  shows   "xs \<parallel> ys"
   1.168 +  using len neq
   1.169 +proof (induct rule: list_induct2) 
   1.170 +  case 1 thus ?case by simp
   1.171 +next
   1.172 +  case (2 a as b bs)
   1.173 +
   1.174 +  have ih: "as \<noteq> bs \<Longrightarrow> as \<parallel> bs" .
   1.175 +  
   1.176 +  show ?case
   1.177 +  proof (cases "a = b")
   1.178 +    case True 
   1.179 +    hence "as \<noteq> bs" using 2 by simp
   1.180 +   
   1.181 +    thus ?thesis by (rule Cons_parallelI2 [OF True ih])
   1.182 +  next
   1.183 +    case False
   1.184 +    thus ?thesis by (rule Cons_parallelI1)
   1.185 +  qed
   1.186 +qed
   1.187  
   1.188  subsection {* Exeuctable code *}
   1.189