author | nipkow |
Mon, 13 May 2002 15:27:28 +0200 | |
changeset 13145 | 59bc43b51aa2 |
parent 9747 | 043098ba5098 |
permissions | -rw-r--r-- |
6804
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
1 |
(* Title: HOL/UNITY/GenPrefix.thy |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
4 |
Copyright 1999 University of Cambridge |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
5 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
6 |
Charpentier's Generalized Prefix Relation |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
7 |
(xs,ys) : genPrefix r |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
8 |
if ys = xs' @ zs where length xs = length xs' |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
9 |
and corresponding elements of xs, xs' are pairwise related by r |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
10 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
11 |
Based on Lex/Prefix |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
12 |
*) |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
13 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
14 |
(*** preliminary lemmas ***) |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
15 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
16 |
Goal "([], xs) : genPrefix r"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
17 |
by (cut_facts_tac [genPrefix.Nil RS genPrefix.append] 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
18 |
by Auto_tac; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
19 |
qed "Nil_genPrefix"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
20 |
AddIffs[Nil_genPrefix]; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
21 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
22 |
Goal "(xs,ys) : genPrefix r ==> length xs <= length ys"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
23 |
by (etac genPrefix.induct 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
24 |
by Auto_tac; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
25 |
qed "genPrefix_length_le"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
26 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
27 |
Goal "[| (xs', ys'): genPrefix r |] \ |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
28 |
\ ==> (ALL x xs. xs' = x#xs --> (EX y ys. ys' = y#ys & (x,y) : r & (xs, ys) : genPrefix r))"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
29 |
by (etac genPrefix.induct 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
30 |
by (Blast_tac 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
31 |
by (Blast_tac 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
32 |
by (force_tac (claset() addIs [genPrefix.append], |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
33 |
simpset()) 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
34 |
val lemma = result(); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
35 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
36 |
(*As usual converting it to an elimination rule is tiresome*) |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
37 |
val major::prems = |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
38 |
Goal "[| (x#xs, zs): genPrefix r; \ |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
39 |
\ !!y ys. [| zs = y#ys; (x,y) : r; (xs, ys) : genPrefix r |] ==> P \ |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
40 |
\ |] ==> P"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
41 |
by (cut_facts_tac [major RS lemma] 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
42 |
by (Full_simp_tac 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
43 |
by (REPEAT (eresolve_tac [exE, conjE] 1)); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
44 |
by (REPEAT (ares_tac prems 1)); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
45 |
qed "cons_genPrefixE"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
46 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
47 |
AddSEs [cons_genPrefixE]; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
48 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
49 |
Goal "((x#xs,y#ys) : genPrefix r) = ((x,y) : r & (xs,ys) : genPrefix r)"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
50 |
by (blast_tac (claset() addIs [genPrefix.prepend]) 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
51 |
qed"Cons_genPrefix_Cons"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
52 |
AddIffs [Cons_genPrefix_Cons]; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
53 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
54 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
55 |
(*** genPrefix is a partial order ***) |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
56 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
57 |
Goalw [refl_def] "reflexive r ==> reflexive (genPrefix r)"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
58 |
by Auto_tac; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
59 |
by (induct_tac "x" 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
60 |
by (blast_tac (claset() addIs [genPrefix.prepend]) 2); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
61 |
by (blast_tac (claset() addIs [genPrefix.Nil]) 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
62 |
qed "refl_genPrefix"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
63 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
64 |
Goal "reflexive r ==> (l,l) : genPrefix r"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
65 |
by (etac ([refl_genPrefix,UNIV_I] MRS reflD) 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
66 |
qed "genPrefix_refl"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
67 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
68 |
Addsimps [genPrefix_refl]; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
69 |
|
9111 | 70 |
Goal "r<=s ==> genPrefix r <= genPrefix s"; |
71 |
by (Clarify_tac 1); |
|
72 |
by (etac genPrefix.induct 1); |
|
73 |
by (auto_tac (claset() addIs [genPrefix.append], simpset())); |
|
74 |
qed "genPrefix_mono"; |
|
75 |
||
6804
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
76 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
77 |
(** Transitivity **) |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
78 |
|
9111 | 79 |
(*A lemma for proving genPrefix_trans_O*) |
6804
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
80 |
Goal "ALL zs. (xs @ ys, zs) : genPrefix r --> (xs, zs) : genPrefix r"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
81 |
by (induct_tac "xs" 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
82 |
by Auto_tac; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
83 |
qed_spec_mp "append_genPrefix"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
84 |
|
9111 | 85 |
(*Lemma proving transitivity and more*) |
86 |
Goalw [prefix_def] |
|
87 |
"(x, y) : genPrefix r \ |
|
88 |
\ ==> ALL z. (y,z) : genPrefix s --> (x, z) : genPrefix (s O r)"; |
|
6804
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
89 |
by (etac genPrefix.induct 1); |
9111 | 90 |
by (blast_tac (claset() addDs [append_genPrefix]) 3); |
91 |
by (blast_tac (claset() addIs [genPrefix.prepend]) 2); |
|
6804
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
92 |
by (Blast_tac 1); |
9111 | 93 |
qed_spec_mp "genPrefix_trans_O"; |
94 |
||
95 |
Goal "[| (x,y) : genPrefix r; (y,z) : genPrefix r; trans r |] \ |
|
96 |
\ ==> (x,z) : genPrefix r"; |
|
97 |
by (rtac (impOfSubs (trans_O_subset RS genPrefix_mono)) 1); |
|
98 |
by (assume_tac 2); |
|
99 |
by (blast_tac (claset() addIs [genPrefix_trans_O]) 1); |
|
6804
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
100 |
qed_spec_mp "genPrefix_trans"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
101 |
|
9111 | 102 |
Goalw [prefix_def] |
103 |
"[| x<=y; (y,z) : genPrefix r |] ==> (x, z) : genPrefix r"; |
|
104 |
by (stac (R_O_Id RS sym) 1 THEN etac genPrefix_trans_O 1); |
|
105 |
by (assume_tac 1); |
|
106 |
qed_spec_mp "prefix_genPrefix_trans"; |
|
107 |
||
108 |
Goalw [prefix_def] |
|
109 |
"[| (x,y) : genPrefix r; y<=z |] ==> (x,z) : genPrefix r"; |
|
110 |
by (stac (Id_O_R RS sym) 1 THEN etac genPrefix_trans_O 1); |
|
111 |
by (assume_tac 1); |
|
112 |
qed_spec_mp "genPrefix_prefix_trans"; |
|
113 |
||
6804
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
114 |
Goal "trans r ==> trans (genPrefix r)"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
115 |
by (blast_tac (claset() addIs [transI, genPrefix_trans]) 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
116 |
qed "trans_genPrefix"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
117 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
118 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
119 |
(** Antisymmetry **) |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
120 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
121 |
Goal "[| (xs,ys) : genPrefix r; antisym r |] \ |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
122 |
\ ==> (ys,xs) : genPrefix r --> xs = ys"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
123 |
by (etac genPrefix.induct 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
124 |
by (full_simp_tac (simpset() addsimps [antisym_def]) 2); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
125 |
by (Blast_tac 2); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
126 |
by (Blast_tac 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
127 |
(*append case is hardest*) |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
128 |
by (Clarify_tac 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
129 |
by (subgoal_tac "length zs = 0" 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
130 |
by (Force_tac 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
131 |
by (REPEAT (dtac genPrefix_length_le 1)); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
132 |
by (full_simp_tac (simpset() delsimps [length_0_conv]) 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
133 |
qed_spec_mp "genPrefix_antisym"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
134 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
135 |
Goal "antisym r ==> antisym (genPrefix r)"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
136 |
by (blast_tac (claset() addIs [antisymI, genPrefix_antisym]) 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
137 |
qed "antisym_genPrefix"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
138 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
139 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
140 |
(*** recursion equations ***) |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
141 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
142 |
Goal "((xs, []) : genPrefix r) = (xs = [])"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
143 |
by (induct_tac "xs" 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
144 |
by (Blast_tac 2); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
145 |
by (Simp_tac 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
146 |
qed "genPrefix_Nil"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
147 |
Addsimps [genPrefix_Nil]; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
148 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
149 |
Goalw [refl_def] |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
150 |
"reflexive r ==> ((xs@ys, xs@zs) : genPrefix r) = ((ys,zs) : genPrefix r)"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
151 |
by (induct_tac "xs" 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
152 |
by (ALLGOALS Asm_simp_tac); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
153 |
qed "same_genPrefix_genPrefix"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
154 |
Addsimps [same_genPrefix_genPrefix]; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
155 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
156 |
Goal "((xs, y#ys) : genPrefix r) = \ |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
157 |
\ (xs=[] | (EX z zs. xs=z#zs & (z,y) : r & (zs,ys) : genPrefix r))"; |
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset
|
158 |
by (case_tac "xs" 1); |
6804
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
159 |
by Auto_tac; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
160 |
qed "genPrefix_Cons"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
161 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
162 |
Goal "[| reflexive r; (xs,ys) : genPrefix r |] \ |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
163 |
\ ==> (xs@zs, take (length xs) ys @ zs) : genPrefix r"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
164 |
by (etac genPrefix.induct 1); |
7499 | 165 |
by (ftac genPrefix_length_le 3); |
7053
8f246bc87ab2
tweaked proof after removal of diff_is_0_eq RS iffD2
paulson
parents:
6824
diff
changeset
|
166 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_is_0_eq RS iffD2]))); |
6804
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
167 |
qed "genPrefix_take_append"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
168 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
169 |
Goal "[| reflexive r; (xs,ys) : genPrefix r; length xs = length ys |] \ |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
170 |
\ ==> (xs@zs, ys @ zs) : genPrefix r"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
171 |
by (dtac genPrefix_take_append 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
172 |
by (assume_tac 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
173 |
by (asm_full_simp_tac (simpset() addsimps [take_all]) 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
174 |
qed "genPrefix_append_both"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
175 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
176 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
177 |
(*NOT suitable for rewriting since [y] has the form y#ys*) |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
178 |
Goal "xs @ y # ys = (xs @ [y]) @ ys"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
179 |
by Auto_tac; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
180 |
qed "append_cons_eq"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
181 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
182 |
Goal "[| (xs,ys) : genPrefix r; reflexive r |] \ |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
183 |
\ ==> length xs < length ys --> (xs @ [ys ! length xs], ys) : genPrefix r"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
184 |
by (etac genPrefix.induct 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
185 |
by (Blast_tac 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
186 |
by (Asm_simp_tac 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
187 |
(*Append case is hardest*) |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
188 |
by (Asm_simp_tac 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
189 |
by (forward_tac [genPrefix_length_le RS le_imp_less_or_eq] 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
190 |
by (etac disjE 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
191 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [neq_Nil_conv, nth_append]))); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
192 |
by (blast_tac (claset() addIs [genPrefix.append]) 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
193 |
by Auto_tac; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
194 |
by (stac append_cons_eq 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
195 |
by (blast_tac (claset() addIs [genPrefix_append_both, genPrefix.append]) 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
196 |
val lemma = result() RS mp; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
197 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
198 |
Goal "[| (xs,ys) : genPrefix r; length xs < length ys; reflexive r |] \ |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
199 |
\ ==> (xs @ [ys ! length xs], ys) : genPrefix r"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
200 |
by (blast_tac (claset() addIs [lemma]) 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
201 |
qed "append_one_genPrefix"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
202 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
203 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
204 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
205 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
206 |
(** Proving the equivalence with Charpentier's definition **) |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
207 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
208 |
Goal "ALL i ys. i < length xs \ |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
209 |
\ --> (xs, ys) : genPrefix r --> (xs ! i, ys ! i) : r"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
210 |
by (induct_tac "xs" 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
211 |
by Auto_tac; |
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset
|
212 |
by (case_tac "i" 1); |
6804
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
213 |
by Auto_tac; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
214 |
qed_spec_mp "genPrefix_imp_nth"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
215 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
216 |
Goal "ALL ys. length xs <= length ys \ |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
217 |
\ --> (ALL i. i < length xs --> (xs ! i, ys ! i) : r) \ |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
218 |
\ --> (xs, ys) : genPrefix r"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
219 |
by (induct_tac "xs" 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
220 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq_0_disj, |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
221 |
all_conj_distrib]))); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
222 |
by (Clarify_tac 1); |
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset
|
223 |
by (case_tac "ys" 1); |
6804
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
224 |
by (ALLGOALS Force_tac); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
225 |
qed_spec_mp "nth_imp_genPrefix"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
226 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
227 |
Goal "((xs,ys) : genPrefix r) = \ |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
228 |
\ (length xs <= length ys & (ALL i. i < length xs --> (xs!i, ys!i) : r))"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
229 |
by (blast_tac (claset() addIs [genPrefix_length_le, genPrefix_imp_nth, |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
230 |
nth_imp_genPrefix]) 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
231 |
qed "genPrefix_iff_nth"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
232 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
233 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
234 |
(** <= is a partial order: **) |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
235 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
236 |
AddIffs [reflexive_Id, antisym_Id, trans_Id]; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
237 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
238 |
Goalw [prefix_def] "xs <= (xs::'a list)"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
239 |
by (Simp_tac 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
240 |
qed "prefix_refl"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
241 |
AddIffs[prefix_refl]; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
242 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
243 |
Goalw [prefix_def] "!!xs::'a list. [| xs <= ys; ys <= zs |] ==> xs <= zs"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
244 |
by (blast_tac (claset() addIs [genPrefix_trans]) 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
245 |
qed "prefix_trans"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
246 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
247 |
Goalw [prefix_def] "!!xs::'a list. [| xs <= ys; ys <= xs |] ==> xs = ys"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
248 |
by (blast_tac (claset() addIs [genPrefix_antisym]) 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
249 |
qed "prefix_antisym"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
250 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
251 |
Goalw [strict_prefix_def] "!!xs::'a list. (xs < zs) = (xs <= zs & xs ~= zs)"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
252 |
by Auto_tac; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
253 |
qed "prefix_less_le"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
254 |
|
7839 | 255 |
(*Monotonicity of "set" operator WRT prefix*) |
256 |
Goalw [prefix_def] "xs <= ys ==> set xs <= set ys"; |
|
257 |
by (etac genPrefix.induct 1); |
|
258 |
by Auto_tac; |
|
259 |
qed "set_mono"; |
|
260 |
||
6804
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
261 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
262 |
(** recursion equations **) |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
263 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
264 |
Goalw [prefix_def] "[] <= xs"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
265 |
by (simp_tac (simpset() addsimps [Nil_genPrefix]) 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
266 |
qed "Nil_prefix"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
267 |
AddIffs[Nil_prefix]; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
268 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
269 |
Goalw [prefix_def] "(xs <= []) = (xs = [])"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
270 |
by (simp_tac (simpset() addsimps [genPrefix_Nil]) 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
271 |
qed "prefix_Nil"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
272 |
Addsimps [prefix_Nil]; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
273 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
274 |
Goalw [prefix_def] "(x#xs <= y#ys) = (x=y & xs<=ys)"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
275 |
by (Simp_tac 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
276 |
qed"Cons_prefix_Cons"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
277 |
Addsimps [Cons_prefix_Cons]; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
278 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
279 |
Goalw [prefix_def] "(xs@ys <= xs@zs) = (ys <= zs)"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
280 |
by (Simp_tac 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
281 |
qed "same_prefix_prefix"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
282 |
Addsimps [same_prefix_prefix]; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
283 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
284 |
AddIffs (* (xs@ys <= xs) = (ys <= []) *) |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
285 |
[simplify (simpset()) (read_instantiate [("zs","[]")] same_prefix_prefix)]; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
286 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
287 |
Goalw [prefix_def] "xs <= ys ==> xs <= ys@zs"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
288 |
by (etac genPrefix.append 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
289 |
qed "prefix_appendI"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
290 |
Addsimps [prefix_appendI]; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
291 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
292 |
Goalw [prefix_def] |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
293 |
"(xs <= y#ys) = (xs=[] | (? zs. xs=y#zs & zs <= ys))"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
294 |
by (simp_tac (simpset() addsimps [genPrefix_Cons]) 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
295 |
by Auto_tac; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
296 |
qed "prefix_Cons"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
297 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
298 |
Goalw [prefix_def] |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
299 |
"[| xs <= ys; length xs < length ys |] ==> xs @ [ys ! length xs] <= ys"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
300 |
by (asm_simp_tac (simpset() addsimps [append_one_genPrefix]) 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
301 |
qed "append_one_prefix"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
302 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
303 |
Goalw [prefix_def] "xs <= ys ==> length xs <= length ys"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
304 |
by (etac genPrefix_length_le 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
305 |
qed "prefix_length_le"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
306 |
|
8216 | 307 |
Goalw [prefix_def] "xs<=ys ==> xs~=ys --> length xs < length ys"; |
308 |
by (etac genPrefix.induct 1); |
|
309 |
by Auto_tac; |
|
310 |
val lemma = result(); |
|
311 |
||
312 |
Goalw [strict_prefix_def] "xs < ys ==> length xs < length ys"; |
|
313 |
by (blast_tac (claset() addIs [lemma RS mp]) 1); |
|
314 |
qed "strict_prefix_length_less"; |
|
315 |
||
6804
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
316 |
Goal "mono length"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
317 |
by (blast_tac (claset() addIs [monoI, prefix_length_le]) 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
318 |
qed "mono_length"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
319 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
320 |
(*Equivalence to the definition used in Lex/Prefix.thy*) |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
321 |
Goalw [prefix_def] "(xs <= zs) = (EX ys. zs = xs@ys)"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
322 |
by (auto_tac (claset(), |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
323 |
simpset() addsimps [genPrefix_iff_nth, nth_append])); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
324 |
by (res_inst_tac [("x", "drop (length xs) zs")] exI 1); |
6824 | 325 |
by (rtac nth_equalityI 1); |
6804
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
326 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [nth_append]))); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
327 |
qed "prefix_iff"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
328 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
329 |
Goal "(xs <= ys@[y]) = (xs = ys@[y] | xs <= ys)"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
330 |
by (simp_tac (simpset() addsimps [prefix_iff]) 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
331 |
by (rtac iffI 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
332 |
by (etac exE 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
333 |
by (rename_tac "zs" 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
334 |
by (res_inst_tac [("xs","zs")] rev_exhaust 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
335 |
by (Asm_full_simp_tac 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
336 |
by (hyp_subst_tac 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
337 |
by (asm_full_simp_tac (simpset() delsimps [append_assoc] |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
338 |
addsimps [append_assoc RS sym])1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
339 |
by (Force_tac 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
340 |
qed "prefix_snoc"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
341 |
Addsimps [prefix_snoc]; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
342 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
343 |
Goal "(xs <= ys@zs) = (xs <= ys | (? us. xs = ys@us & us <= zs))"; |
13145 | 344 |
by (res_inst_tac [("xs","zs")] rev_induct 1); |
6804
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
345 |
by (Force_tac 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
346 |
by (asm_full_simp_tac (simpset() delsimps [append_assoc] |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
347 |
addsimps [append_assoc RS sym])1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
348 |
by (Force_tac 1); |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
349 |
qed "prefix_append_iff"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
350 |
|
8216 | 351 |
(*Although the prefix ordering is not linear, the prefixes of a list |
352 |
are linearly ordered.*) |
|
353 |
Goal "!!zs::'a list. xs <= zs --> ys <= zs --> xs <= ys | ys <= xs"; |
|
13145 | 354 |
by (res_inst_tac [("xs","zs")] rev_induct 1); |
8216 | 355 |
by Auto_tac; |
356 |
qed_spec_mp "common_prefix_linear"; |
|
357 |
||
6804
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
358 |
|
6824 | 359 |
(*** pfixLe, pfixGe: properties inherited from the translations ***) |
6804
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
360 |
|
8128 | 361 |
(** pfixLe **) |
362 |
||
6804
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
363 |
Goalw [refl_def, Le_def] "reflexive Le"; |
6824 | 364 |
by Auto_tac; |
6804
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
365 |
qed "reflexive_Le"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
366 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
367 |
Goalw [antisym_def, Le_def] "antisym Le"; |
6824 | 368 |
by Auto_tac; |
6804
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
369 |
qed "antisym_Le"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
370 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
371 |
Goalw [trans_def, Le_def] "trans Le"; |
6824 | 372 |
by Auto_tac; |
6804
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
373 |
qed "trans_Le"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
374 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
375 |
AddIffs [reflexive_Le, antisym_Le, trans_Le]; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
376 |
|
8128 | 377 |
Goal "x pfixLe x"; |
378 |
by (Simp_tac 1); |
|
379 |
qed "pfixLe_refl"; |
|
380 |
AddIffs[pfixLe_refl]; |
|
381 |
||
382 |
Goal "[| x pfixLe y; y pfixLe z |] ==> x pfixLe z"; |
|
383 |
by (blast_tac (claset() addIs [genPrefix_trans]) 1); |
|
384 |
qed "pfixLe_trans"; |
|
385 |
||
386 |
Goal "[| x pfixLe y; y pfixLe x |] ==> x = y"; |
|
387 |
by (blast_tac (claset() addIs [genPrefix_antisym]) 1); |
|
388 |
qed "pfixLe_antisym"; |
|
389 |
||
390 |
Goalw [prefix_def, Le_def] "xs<=ys ==> xs pfixLe ys"; |
|
391 |
by (blast_tac (claset() addIs [impOfSubs genPrefix_mono]) 1); |
|
392 |
qed "prefix_imp_pfixLe"; |
|
393 |
||
6804
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
394 |
Goalw [refl_def, Ge_def] "reflexive Ge"; |
6824 | 395 |
by Auto_tac; |
6804
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
396 |
qed "reflexive_Ge"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
397 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
398 |
Goalw [antisym_def, Ge_def] "antisym Ge"; |
6824 | 399 |
by Auto_tac; |
6804
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
400 |
qed "antisym_Ge"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
401 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
402 |
Goalw [trans_def, Ge_def] "trans Ge"; |
6824 | 403 |
by Auto_tac; |
6804
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
404 |
qed "trans_Ge"; |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
405 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
406 |
AddIffs [reflexive_Ge, antisym_Ge, trans_Ge]; |
8067 | 407 |
|
8128 | 408 |
Goal "x pfixGe x"; |
409 |
by (Simp_tac 1); |
|
410 |
qed "pfixGe_refl"; |
|
411 |
AddIffs[pfixGe_refl]; |
|
8067 | 412 |
|
8128 | 413 |
Goal "[| x pfixGe y; y pfixGe z |] ==> x pfixGe z"; |
414 |
by (blast_tac (claset() addIs [genPrefix_trans]) 1); |
|
415 |
qed "pfixGe_trans"; |
|
416 |
||
417 |
Goal "[| x pfixGe y; y pfixGe x |] ==> x = y"; |
|
418 |
by (blast_tac (claset() addIs [genPrefix_antisym]) 1); |
|
419 |
qed "pfixGe_antisym"; |
|
8067 | 420 |
|
421 |
Goalw [prefix_def, Ge_def] "xs<=ys ==> xs pfixGe ys"; |
|
422 |
by (blast_tac (claset() addIs [impOfSubs genPrefix_mono]) 1); |
|
423 |
qed "prefix_imp_pfixGe"; |
|
424 |