author | wenzelm |

Sat Nov 11 16:11:42 2006 +0100 (2006-11-11) | |

changeset 21305 | d41eddfd2b66 |

parent 21304 | 01968a336533 |

child 21306 | 7ab6e95e6b0b |

tuned proofs;

1.1 --- a/src/HOL/Library/List_Prefix.thy Sat Nov 11 16:11:41 2006 +0100 1.2 +++ b/src/HOL/Library/List_Prefix.thy Sat Nov 11 16:11:42 2006 +0100 1.3 @@ -23,28 +23,31 @@ 1.4 lemma prefixI [intro?]: "ys = xs @ zs ==> xs \<le> ys" 1.5 unfolding prefix_def by blast 1.6 1.7 -lemma prefixE [elim?]: "xs \<le> ys ==> (!!zs. ys = xs @ zs ==> C) ==> C" 1.8 - unfolding prefix_def by blast 1.9 +lemma prefixE [elim?]: 1.10 + assumes "xs \<le> ys" 1.11 + obtains zs where "ys = xs @ zs" 1.12 + using prems unfolding prefix_def by blast 1.13 1.14 lemma strict_prefixI' [intro?]: "ys = xs @ z # zs ==> xs < ys" 1.15 unfolding strict_prefix_def prefix_def by blast 1.16 1.17 lemma strict_prefixE' [elim?]: 1.18 - assumes lt: "xs < ys" 1.19 - and r: "!!z zs. ys = xs @ z # zs ==> C" 1.20 - shows C 1.21 + assumes "xs < ys" 1.22 + obtains z zs where "ys = xs @ z # zs" 1.23 proof - 1.24 - from lt obtain us where "ys = xs @ us" and "xs \<noteq> ys" 1.25 + from `xs < ys` obtain us where "ys = xs @ us" and "xs \<noteq> ys" 1.26 unfolding strict_prefix_def prefix_def by blast 1.27 - with r show ?thesis by (auto simp add: neq_Nil_conv) 1.28 + with that show ?thesis by (auto simp add: neq_Nil_conv) 1.29 qed 1.30 1.31 lemma strict_prefixI [intro?]: "xs \<le> ys ==> xs \<noteq> ys ==> xs < (ys::'a list)" 1.32 unfolding strict_prefix_def by blast 1.33 1.34 lemma strict_prefixE [elim?]: 1.35 - "xs < ys ==> (xs \<le> ys ==> xs \<noteq> (ys::'a list) ==> C) ==> C" 1.36 - unfolding strict_prefix_def by blast 1.37 + fixes xs ys :: "'a list" 1.38 + assumes "xs < ys" 1.39 + obtains "xs \<le> ys" and "xs \<noteq> ys" 1.40 + using prems unfolding strict_prefix_def by blast 1.41 1.42 1.43 subsection {* Basic properties of prefixes *} 1.44 @@ -163,13 +166,12 @@ 1.45 unfolding parallel_def by blast 1.46 1.47 lemma parallelE [elim]: 1.48 - "xs \<parallel> ys ==> (\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> C) ==> C" 1.49 - unfolding parallel_def by blast 1.50 + assumes "xs \<parallel> ys" 1.51 + obtains "\<not> xs \<le> ys \<and> \<not> ys \<le> xs" 1.52 + using prems unfolding parallel_def by blast 1.53 1.54 theorem prefix_cases: 1.55 - "(xs \<le> ys ==> C) ==> 1.56 - (ys < xs ==> C) ==> 1.57 - (xs \<parallel> ys ==> C) ==> C" 1.58 + obtains "xs \<le> ys" | "ys < xs" | "xs \<parallel> ys" 1.59 unfolding parallel_def strict_prefix_def by blast 1.60 1.61 theorem parallel_decomp: 1.62 @@ -219,7 +221,15 @@ 1.63 postfix :: "'a list => 'a list => bool" ("(_/ >>= _)" [51, 50] 50) 1.64 "(xs >>= ys) = (\<exists>zs. xs = zs @ ys)" 1.65 1.66 -lemma postfix_refl [simp, intro!]: "xs >>= xs" 1.67 +lemma postfixI [intro?]: "xs = zs @ ys ==> xs >>= ys" 1.68 + unfolding postfix_def by blast 1.69 + 1.70 +lemma postfixE [elim?]: 1.71 + assumes "xs >>= ys" 1.72 + obtains zs where "xs = zs @ ys" 1.73 + using prems unfolding postfix_def by blast 1.74 + 1.75 +lemma postfix_refl [iff]: "xs >>= xs" 1.76 by (auto simp add: postfix_def) 1.77 lemma postfix_trans: "\<lbrakk>xs >>= ys; ys >>= zs\<rbrakk> \<Longrightarrow> xs >>= zs" 1.78 by (auto simp add: postfix_def) 1.79 @@ -229,7 +239,7 @@ 1.80 lemma Nil_postfix [iff]: "xs >>= []" 1.81 by (simp add: postfix_def) 1.82 lemma postfix_Nil [simp]: "([] >>= xs) = (xs = [])" 1.83 - by (auto simp add:postfix_def) 1.84 + by (auto simp add: postfix_def) 1.85 1.86 lemma postfix_ConsI: "xs >>= ys \<Longrightarrow> x#xs >>= ys" 1.87 by (auto simp add: postfix_def) 1.88 @@ -239,23 +249,35 @@ 1.89 lemma postfix_appendI: "xs >>= ys \<Longrightarrow> zs @ xs >>= ys" 1.90 by (auto simp add: postfix_def) 1.91 lemma postfix_appendD: "xs >>= zs @ ys \<Longrightarrow> xs >>= ys" 1.92 - by(auto simp add: postfix_def) 1.93 + by (auto simp add: postfix_def) 1.94 1.95 -lemma postfix_is_subset_lemma: "xs = zs @ ys \<Longrightarrow> set ys \<subseteq> set xs" 1.96 - by (induct zs) auto 1.97 -lemma postfix_is_subset: "xs >>= ys \<Longrightarrow> set ys \<subseteq> set xs" 1.98 - by (unfold postfix_def, erule exE, erule postfix_is_subset_lemma) 1.99 +lemma postfix_is_subset: "xs >>= ys ==> set ys \<subseteq> set xs" 1.100 +proof - 1.101 + assume "xs >>= ys" 1.102 + then obtain zs where "xs = zs @ ys" .. 1.103 + then show ?thesis by (induct zs) auto 1.104 +qed 1.105 1.106 -lemma postfix_ConsD2_lemma: "x#xs = zs @ y#ys \<Longrightarrow> xs >>= ys" 1.107 - by (induct zs) (auto intro!: postfix_appendI postfix_ConsI) 1.108 -lemma postfix_ConsD2: "x#xs >>= y#ys \<Longrightarrow> xs >>= ys" 1.109 - by (auto simp add: postfix_def dest!: postfix_ConsD2_lemma) 1.110 +lemma postfix_ConsD2: "x#xs >>= y#ys ==> xs >>= ys" 1.111 +proof - 1.112 + assume "x#xs >>= y#ys" 1.113 + then obtain zs where "x#xs = zs @ y#ys" .. 1.114 + then show ?thesis 1.115 + by (induct zs) (auto intro!: postfix_appendI postfix_ConsI) 1.116 +qed 1.117 1.118 -lemma postfix2prefix: "(xs >>= ys) = (rev ys <= rev xs)" 1.119 - apply (unfold prefix_def postfix_def, safe) 1.120 - apply (rule_tac x = "rev zs" in exI, simp) 1.121 - apply (rule_tac x = "rev zs" in exI) 1.122 - apply (rule rev_is_rev_conv [THEN iffD1], simp) 1.123 - done 1.124 +lemma postfix_to_prefix: "xs >>= ys \<longleftrightarrow> rev ys \<le> rev xs" 1.125 +proof 1.126 + assume "xs >>= ys" 1.127 + then obtain zs where "xs = zs @ ys" .. 1.128 + then have "rev xs = rev ys @ rev zs" by simp 1.129 + then show "rev ys <= rev xs" .. 1.130 +next 1.131 + assume "rev ys <= rev xs" 1.132 + then obtain zs where "rev xs = rev ys @ zs" .. 1.133 + then have "rev (rev xs) = rev zs @ rev (rev ys)" by simp 1.134 + then have "xs = rev zs @ ys" by simp 1.135 + then show "xs >>= ys" .. 1.136 +qed 1.137 1.138 end