author  wenzelm 
Mon, 06 Nov 2000 22:56:07 +0100  
changeset 10408  d8b3613158b1 
parent 10389  c7d8901ab269 
child 10512  d34192966cd8 
permissions  rwrr 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

1 
(* Title: HOL/Library/List_Prefix.thy 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

2 
ID: $Id$ 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

3 
Author: Tobias Nipkow and Markus Wenzel, TU Muenchen 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

4 
*) 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

5 

4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

6 
header {* 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

7 
\title{List prefixes} 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

8 
\author{Tobias Nipkow and Markus Wenzel} 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

9 
*} 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

10 

4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

11 
theory List_Prefix = Main: 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

12 

4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

13 
subsection {* Prefix order on lists *} 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

14 

4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

15 
instance list :: ("term") ord .. 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

16 

4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

17 
defs (overloaded) 
10389  18 
prefix_def: "xs \<le> ys == \<exists>zs. ys = xs @ zs" 
19 
strict_prefix_def: "xs < ys == xs \<le> ys \<and> xs \<noteq> (ys::'a list)" 

10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

20 

4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

21 
instance list :: ("term") order 
10389  22 
by intro_classes (auto simp add: prefix_def strict_prefix_def) 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

23 

10389  24 
lemma prefixI [intro?]: "ys = xs @ zs ==> xs \<le> ys" 
25 
by (unfold prefix_def) blast 

10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

26 

10389  27 
lemma prefixE [elim?]: "xs \<le> ys ==> (!!zs. ys = xs @ zs ==> C) ==> C" 
28 
by (unfold prefix_def) blast 

10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

29 

10389  30 
lemma strict_prefixI [intro?]: "xs \<le> ys ==> xs \<noteq> ys ==> xs < (ys::'a list)" 
31 
by (unfold strict_prefix_def) blast 

10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

32 

10389  33 
lemma strict_prefixE [elim?]: 
34 
"xs < ys ==> (xs \<le> ys ==> xs \<noteq> (ys::'a list) ==> C) ==> C" 

35 
by (unfold strict_prefix_def) blast 

10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

36 

4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

37 

10389  38 
subsection {* Basic properties of prefixes *} 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

39 

4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

40 
theorem Nil_prefix [iff]: "[] \<le> xs" 
10389  41 
by (simp add: prefix_def) 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

42 

4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

43 
theorem prefix_Nil [simp]: "(xs \<le> []) = (xs = [])" 
10389  44 
by (induct xs) (simp_all add: prefix_def) 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

45 

4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

46 
lemma prefix_snoc [simp]: "(xs \<le> ys @ [y]) = (xs = ys @ [y] \<or> xs \<le> ys)" 
10389  47 
proof 
48 
assume "xs \<le> ys @ [y]" 

49 
then obtain zs where zs: "ys @ [y] = xs @ zs" .. 

50 
show "xs = ys @ [y] \<or> xs \<le> ys" 

51 
proof (cases zs rule: rev_cases) 

52 
assume "zs = []" 

53 
with zs have "xs = ys @ [y]" by simp 

54 
thus ?thesis .. 

55 
next 

56 
fix z zs' assume "zs = zs' @ [z]" 

57 
with zs have "ys = xs @ zs'" by simp 

58 
hence "xs \<le> ys" .. 

59 
thus ?thesis .. 

60 
qed 

61 
next 

62 
assume "xs = ys @ [y] \<or> xs \<le> ys" 

63 
thus "xs \<le> ys @ [y]" 

64 
proof 

65 
assume "xs = ys @ [y]" 

66 
thus ?thesis by simp 

67 
next 

68 
assume "xs \<le> ys" 

69 
then obtain zs where "ys = xs @ zs" .. 

70 
hence "ys @ [y] = xs @ (zs @ [y])" by simp 

71 
thus ?thesis .. 

72 
qed 

73 
qed 

10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

74 

4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

75 
lemma Cons_prefix_Cons [simp]: "(x # xs \<le> y # ys) = (x = y \<and> xs \<le> ys)" 
10389  76 
by (auto simp add: prefix_def) 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

77 

4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

78 
lemma same_prefix_prefix [simp]: "(xs @ ys \<le> xs @ zs) = (ys \<le> zs)" 
10389  79 
by (induct xs) simp_all 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

80 

10389  81 
lemma same_prefix_nil [iff]: "(xs @ ys \<le> xs) = (ys = [])" 
82 
proof  

83 
have "(xs @ ys \<le> xs @ []) = (ys \<le> [])" by (rule same_prefix_prefix) 

84 
thus ?thesis by simp 

85 
qed 

10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

86 

4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

87 
lemma prefix_prefix [simp]: "xs \<le> ys ==> xs \<le> ys @ zs" 
10389  88 
proof  
89 
assume "xs \<le> ys" 

90 
then obtain us where "ys = xs @ us" .. 

91 
hence "ys @ zs = xs @ (us @ zs)" by simp 

92 
thus ?thesis .. 

93 
qed 

10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

94 

4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

95 
theorem prefix_Cons: "(xs \<le> y # ys) = (xs = [] \<or> (\<exists>zs. xs = y # zs \<and> zs \<le> ys))" 
10389  96 
by (cases xs) (auto simp add: prefix_def) 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

97 

4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

98 
theorem prefix_append: 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

99 
"(xs \<le> ys @ zs) = (xs \<le> ys \<or> (\<exists>us. xs = ys @ us \<and> us \<le> zs))" 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

100 
apply (induct zs rule: rev_induct) 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

101 
apply force 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

102 
apply (simp del: append_assoc add: append_assoc [symmetric]) 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

103 
apply simp 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

104 
apply blast 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

105 
done 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

106 

4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

107 
lemma append_one_prefix: 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

108 
"xs \<le> ys ==> length xs < length ys ==> xs @ [ys ! length xs] \<le> ys" 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

109 
apply (unfold prefix_def) 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

110 
apply (auto simp add: nth_append) 
10389  111 
apply (case_tac zs) 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

112 
apply auto 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

113 
done 
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

114 

4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

115 
theorem prefix_length_le: "xs \<le> ys ==> length xs \<le> length ys" 
10389  116 
by (auto simp add: prefix_def) 
10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

117 

4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

118 

10389  119 
subsection {* Parallel lists *} 
120 

121 
constdefs 

122 
parallel :: "'a list => 'a list => bool" (infixl "\<parallel>" 50) 

123 
"xs \<parallel> ys == \<not> xs \<le> ys \<and> \<not> ys \<le> xs" 

124 

125 
lemma parallelI [intro]: "\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> xs \<parallel> ys" 

126 
by (unfold parallel_def) blast 

10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

127 

10389  128 
lemma parallelE [elim]: 
129 
"xs \<parallel> ys ==> (\<not> xs \<le> ys ==> \<not> ys \<le> xs ==> C) ==> C" 

130 
by (unfold parallel_def) blast 

10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

131 

10389  132 
theorem prefix_cases: 
133 
"(xs \<le> ys ==> C) ==> 

134 
(ys \<le> xs ==> C) ==> 

135 
(xs \<parallel> ys ==> C) ==> C" 

136 
by (unfold parallel_def) blast 

10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

137 

10389  138 
theorem parallel_decomp: 
139 
"xs \<parallel> ys ==> \<exists>as b bs c cs. b \<noteq> c \<and> xs = as @ b # bs \<and> ys = as @ c # cs" 

10408  140 
(is "PROP ?P xs" concl is "?E xs") 
141 
proof (induct xs rule: rev_induct) 

142 
assume "[] \<parallel> ys" hence False by auto 

143 
thus "?E []" .. 

144 
next 

145 
fix x xs 

146 
assume hyp: "PROP ?P xs" 

147 
assume asm: "xs @ [x] \<parallel> ys" 

148 
show "?E (xs @ [x])" 

149 
proof (rule prefix_cases) 

150 
assume le: "xs \<le> ys" 

151 
then obtain ys' where ys: "ys = xs @ ys'" .. 

152 
show ?thesis 

153 
proof (cases ys') 

154 
assume "ys' = []" with ys have "xs = ys" by simp 

155 
with asm have "[x] \<parallel> []" by auto 

156 
hence False by blast 

10389  157 
thus ?thesis .. 
158 
next 

10408  159 
fix c cs assume ys': "ys' = c # cs" 
160 
with asm ys have "xs @ [x] \<parallel> xs @ c # cs" by (simp only:) 

161 
hence "x \<noteq> c" by auto 

162 
moreover have "xs @ [x] = xs @ x # []" by simp 

163 
moreover from ys ys' have "ys = xs @ c # cs" by (simp only:) 

164 
ultimately show ?thesis by blast 

10389  165 
qed 
10408  166 
next 
167 
assume "ys \<le> xs" hence "ys \<le> xs @ [x]" by simp 

168 
with asm have False by blast 

169 
thus ?thesis .. 

170 
next 

171 
assume "xs \<parallel> ys" 

172 
with hyp obtain as b bs c cs where neq: "(b::'a) \<noteq> c" 

173 
and xs: "xs = as @ b # bs" and ys: "ys = as @ c # cs" 

174 
by blast 

175 
from xs have "xs @ [x] = as @ b # (bs @ [x])" by simp 

176 
with neq ys show ?thesis by blast 

10389  177 
qed 
178 
qed 

10330
4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

179 

4362e906b745
"List prefixes" library theory (replaces old Lex/Prefix);
wenzelm
parents:
diff
changeset

180 
end 