summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Library/List_Prefix.thy

changeset 10389 | c7d8901ab269 |

parent 10330 | 4362e906b745 |

child 10408 | d8b3613158b1 |

1.1 --- a/src/HOL/Library/List_Prefix.thy Fri Nov 03 21:34:22 2000 +0100 1.2 +++ b/src/HOL/Library/List_Prefix.thy Fri Nov 03 21:35:36 2000 +0100 1.3 @@ -15,86 +15,85 @@ 1.4 instance list :: ("term") ord .. 1.5 1.6 defs (overloaded) 1.7 - prefix_def: "xs \<le> zs == \<exists>ys. zs = xs @ ys" 1.8 - strict_prefix_def: "xs < zs == xs \<le> zs \<and> xs \<noteq> (zs::'a list)" 1.9 + prefix_def: "xs \<le> ys == \<exists>zs. ys = xs @ zs" 1.10 + strict_prefix_def: "xs < ys == xs \<le> ys \<and> xs \<noteq> (ys::'a list)" 1.11 1.12 instance list :: ("term") order 1.13 -proof 1.14 - fix xs ys zs :: "'a list" 1.15 - show "xs \<le> xs" by (simp add: prefix_def) 1.16 - { assume "xs \<le> ys" and "ys \<le> zs" thus "xs \<le> zs" by (auto simp add: prefix_def) } 1.17 - { assume "xs \<le> ys" and "ys \<le> xs" thus "xs = ys" by (auto simp add: prefix_def) } 1.18 - show "(xs < zs) = (xs \<le> zs \<and> xs \<noteq> zs)" by (simp only: strict_prefix_def) 1.19 -qed 1.20 + by intro_classes (auto simp add: prefix_def strict_prefix_def) 1.21 1.22 -constdefs 1.23 - parallel :: "'a list => 'a list => bool" (infixl "\<parallel>" 50) 1.24 - "xs \<parallel> ys == \<not> (xs \<le> ys) \<and> \<not> (ys \<le> xs)" 1.25 +lemma prefixI [intro?]: "ys = xs @ zs ==> xs \<le> ys" 1.26 + by (unfold prefix_def) blast 1.27 1.28 -lemma parallelI [intro]: "\<not> (xs \<le> ys) ==> \<not> (ys \<le> xs) ==> xs \<parallel> ys" 1.29 - by (unfold parallel_def) blast 1.30 +lemma prefixE [elim?]: "xs \<le> ys ==> (!!zs. ys = xs @ zs ==> C) ==> C" 1.31 + by (unfold prefix_def) blast 1.32 1.33 -lemma parellelE [elim]: 1.34 - "xs \<parallel> ys ==> (\<not> (xs \<le> ys) ==> \<not> (ys \<le> xs) ==> C) ==> C" 1.35 - by (unfold parallel_def) blast 1.36 +lemma strict_prefixI [intro?]: "xs \<le> ys ==> xs \<noteq> ys ==> xs < (ys::'a list)" 1.37 + by (unfold strict_prefix_def) blast 1.38 1.39 -theorem prefix_cases: 1.40 - "(xs \<le> ys ==> C) ==> 1.41 - (ys \<le> xs ==> C) ==> 1.42 - (xs \<parallel> ys ==> C) ==> C" 1.43 - by (unfold parallel_def) blast 1.44 +lemma strict_prefixE [elim?]: 1.45 + "xs < ys ==> (xs \<le> ys ==> xs \<noteq> (ys::'a list) ==> C) ==> C" 1.46 + by (unfold strict_prefix_def) blast 1.47 1.48 1.49 -subsection {* Recursion equations *} 1.50 +subsection {* Basic properties of prefixes *} 1.51 1.52 theorem Nil_prefix [iff]: "[] \<le> xs" 1.53 - apply (simp add: prefix_def) 1.54 - done 1.55 + by (simp add: prefix_def) 1.56 1.57 theorem prefix_Nil [simp]: "(xs \<le> []) = (xs = [])" 1.58 - apply (induct_tac xs) 1.59 - apply simp 1.60 - apply (simp add: prefix_def) 1.61 - done 1.62 + by (induct xs) (simp_all add: prefix_def) 1.63 1.64 lemma prefix_snoc [simp]: "(xs \<le> ys @ [y]) = (xs = ys @ [y] \<or> xs \<le> ys)" 1.65 - apply (unfold prefix_def) 1.66 - apply (rule iffI) 1.67 - apply (erule exE) 1.68 - apply (rename_tac zs) 1.69 - apply (rule_tac xs = zs in rev_exhaust) 1.70 - apply simp 1.71 - apply hypsubst 1.72 - apply (simp del: append_assoc add: append_assoc [symmetric]) 1.73 - apply force 1.74 - done 1.75 +proof 1.76 + assume "xs \<le> ys @ [y]" 1.77 + then obtain zs where zs: "ys @ [y] = xs @ zs" .. 1.78 + show "xs = ys @ [y] \<or> xs \<le> ys" 1.79 + proof (cases zs rule: rev_cases) 1.80 + assume "zs = []" 1.81 + with zs have "xs = ys @ [y]" by simp 1.82 + thus ?thesis .. 1.83 + next 1.84 + fix z zs' assume "zs = zs' @ [z]" 1.85 + with zs have "ys = xs @ zs'" by simp 1.86 + hence "xs \<le> ys" .. 1.87 + thus ?thesis .. 1.88 + qed 1.89 +next 1.90 + assume "xs = ys @ [y] \<or> xs \<le> ys" 1.91 + thus "xs \<le> ys @ [y]" 1.92 + proof 1.93 + assume "xs = ys @ [y]" 1.94 + thus ?thesis by simp 1.95 + next 1.96 + assume "xs \<le> ys" 1.97 + then obtain zs where "ys = xs @ zs" .. 1.98 + hence "ys @ [y] = xs @ (zs @ [y])" by simp 1.99 + thus ?thesis .. 1.100 + qed 1.101 +qed 1.102 1.103 lemma Cons_prefix_Cons [simp]: "(x # xs \<le> y # ys) = (x = y \<and> xs \<le> ys)" 1.104 - apply (auto simp add: prefix_def) 1.105 - done 1.106 + by (auto simp add: prefix_def) 1.107 1.108 lemma same_prefix_prefix [simp]: "(xs @ ys \<le> xs @ zs) = (ys \<le> zs)" 1.109 - apply (induct_tac xs) 1.110 - apply simp_all 1.111 - done 1.112 + by (induct xs) simp_all 1.113 1.114 -lemma [iff]: "(xs @ ys \<le> xs) = (ys = [])" 1.115 - apply (insert same_prefix_prefix [where ?zs = "[]"]) 1.116 - apply simp 1.117 - apply blast 1.118 - done 1.119 +lemma same_prefix_nil [iff]: "(xs @ ys \<le> xs) = (ys = [])" 1.120 +proof - 1.121 + have "(xs @ ys \<le> xs @ []) = (ys \<le> [])" by (rule same_prefix_prefix) 1.122 + thus ?thesis by simp 1.123 +qed 1.124 1.125 lemma prefix_prefix [simp]: "xs \<le> ys ==> xs \<le> ys @ zs" 1.126 - apply (unfold prefix_def) 1.127 - apply clarify 1.128 - apply simp 1.129 - done 1.130 +proof - 1.131 + assume "xs \<le> ys" 1.132 + then obtain us where "ys = xs @ us" .. 1.133 + hence "ys @ zs = xs @ (us @ zs)" by simp 1.134 + thus ?thesis .. 1.135 +qed 1.136 1.137 theorem prefix_Cons: "(xs \<le> y # ys) = (xs = [] \<or> (\<exists>zs. xs = y # zs \<and> zs \<le> ys))" 1.138 - apply (unfold prefix_def) 1.139 - apply (case_tac xs) 1.140 - apply auto 1.141 - done 1.142 + by (cases xs) (auto simp add: prefix_def) 1.143 1.144 theorem prefix_append: 1.145 "(xs \<le> ys @ zs) = (xs \<le> ys \<or> (\<exists>us. xs = ys @ us \<and> us \<le> zs))" 1.146 @@ -109,42 +108,78 @@ 1.147 "xs \<le> ys ==> length xs < length ys ==> xs @ [ys ! length xs] \<le> ys" 1.148 apply (unfold prefix_def) 1.149 apply (auto simp add: nth_append) 1.150 - apply (case_tac ys) 1.151 + apply (case_tac zs) 1.152 apply auto 1.153 done 1.154 1.155 theorem prefix_length_le: "xs \<le> ys ==> length xs \<le> length ys" 1.156 - apply (auto simp add: prefix_def) 1.157 - done 1.158 + by (auto simp add: prefix_def) 1.159 1.160 1.161 -subsection {* Prefix cases *} 1.162 +subsection {* Parallel lists *} 1.163 + 1.164 +constdefs 1.165 + parallel :: "'a list => 'a list => bool" (infixl "\<parallel>" 50) 1.166 + "xs \<parallel> ys == \<not> xs \<le> ys \<and> \<not> ys \<le> xs" 1.167 + 1.168 +lemma parallelI [intro]: "\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> xs \<parallel> ys" 1.169 + by (unfold parallel_def) blast 1.170 1.171 -lemma prefix_Nil_cases [case_names Nil]: 1.172 - "xs \<le> [] ==> 1.173 - (xs = [] ==> C) ==> C" 1.174 - by simp 1.175 +lemma parallelE [elim]: 1.176 + "xs \<parallel> ys ==> (\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> C) ==> C" 1.177 + by (unfold parallel_def) blast 1.178 1.179 -lemma prefix_Cons_cases [case_names Nil Cons]: 1.180 - "xs \<le> y # ys ==> 1.181 - (xs = [] ==> C) ==> 1.182 - (!!zs. xs = y # zs ==> zs \<le> ys ==> C) ==> C" 1.183 - by (simp only: prefix_Cons) blast 1.184 +theorem prefix_cases: 1.185 + "(xs \<le> ys ==> C) ==> 1.186 + (ys \<le> xs ==> C) ==> 1.187 + (xs \<parallel> ys ==> C) ==> C" 1.188 + by (unfold parallel_def) blast 1.189 1.190 -lemma prefix_snoc_cases [case_names prefix snoc]: 1.191 - "xs \<le> ys @ [y] ==> 1.192 - (xs \<le> ys ==> C) ==> 1.193 - (xs = ys @ [y] ==> C) ==> C" 1.194 - by (simp only: prefix_snoc) blast 1.195 - 1.196 -lemma prefix_append_cases [case_names prefix append]: 1.197 - "xs \<le> ys @ zs ==> 1.198 - (xs \<le> ys ==> C) ==> 1.199 - (!!us. xs = ys @ us ==> us \<le> zs ==> C) ==> C" 1.200 - by (simp only: prefix_append) blast 1.201 - 1.202 -lemmas prefix_any_cases [cases set: prefix] = (*dummy set name*) 1.203 - prefix_Nil_cases prefix_Cons_cases 1.204 - prefix_snoc_cases prefix_append_cases 1.205 +theorem parallel_decomp: 1.206 + "xs \<parallel> ys ==> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs" 1.207 + (concl is "?E xs") 1.208 +proof - 1.209 + assume "xs \<parallel> ys" 1.210 + have "?this --> ?E xs" (is "?P xs") 1.211 + proof (induct (stripped) xs rule: rev_induct) 1.212 + assume "[] \<parallel> ys" hence False by auto 1.213 + thus "?E []" .. 1.214 + next 1.215 + fix x xs 1.216 + assume hyp: "?P xs" 1.217 + assume asm: "xs @ [x] \<parallel> ys" 1.218 + show "?E (xs @ [x])" 1.219 + proof (rule prefix_cases) 1.220 + assume le: "xs \<le> ys" 1.221 + then obtain ys' where ys: "ys = xs @ ys'" .. 1.222 + show ?thesis 1.223 + proof (cases ys') 1.224 + assume "ys' = []" with ys have "xs = ys" by simp 1.225 + with asm have "[x] \<parallel> []" by auto 1.226 + hence False by blast 1.227 + thus ?thesis .. 1.228 + next 1.229 + fix c cs assume ys': "ys' = c # cs" 1.230 + with asm ys have "xs @ [x] \<parallel> xs @ c # cs" by (simp only:) 1.231 + hence "x \<noteq> c" by auto 1.232 + moreover have "xs @ [x] = xs @ x # []" by simp 1.233 + moreover from ys ys' have "ys = xs @ c # cs" by (simp only:) 1.234 + ultimately show ?thesis by blast 1.235 + qed 1.236 + next 1.237 + assume "ys \<le> xs" hence "ys \<le> xs @ [x]" by simp 1.238 + with asm have False by blast 1.239 + thus ?thesis .. 1.240 + next 1.241 + assume "xs \<parallel> ys" 1.242 + with hyp obtain as b bs c cs where neq: "(b::'a) \<noteq> c" 1.243 + and xs: "xs = as @ b # bs" and ys: "ys = as @ c # cs" 1.244 + by blast 1.245 + from xs have "xs @ [x] = as @ b # (bs @ [x])" by simp 1.246 + with neq ys show ?thesis by blast 1.247 + qed 1.248 + qed 1.249 + thus ?thesis .. 1.250 +qed 1.251 1.252 end