author | wenzelm |
Fri, 17 Nov 2000 18:47:33 +0100 | |
changeset 10481 | 9efb2fd5399e |
parent 10408 | d8b3613158b1 |
child 10512 | d34192966cd8 |
permissions | -rw-r--r-- |
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 |