author | paulson |
Thu, 10 Jun 1999 10:37:29 +0200 | |
changeset 6808 | d5dfe040c183 |
parent 6675 | 63e53327f5e5 |
child 8423 | 3c19160b6432 |
permissions | -rw-r--r-- |
1465 | 1 |
(* Title: HOL/Lex/Prefix.thy |
1344 | 2 |
ID: $Id$ |
1465 | 3 |
Author: Richard Mayr & Tobias Nipkow |
1344 | 4 |
Copyright 1995 TUM |
5 |
*) |
|
6 |
||
4643 | 7 |
(** <= is a partial order: **) |
8 |
||
5069 | 9 |
Goalw [prefix_def] "xs <= (xs::'a list)"; |
5132 | 10 |
by (Simp_tac 1); |
4643 | 11 |
qed "prefix_refl"; |
4647 | 12 |
AddIffs[prefix_refl]; |
4643 | 13 |
|
5069 | 14 |
Goalw [prefix_def] "!!xs::'a list. [| xs <= ys; ys <= zs |] ==> xs <= zs"; |
5132 | 15 |
by (Clarify_tac 1); |
16 |
by (Simp_tac 1); |
|
4643 | 17 |
qed "prefix_trans"; |
18 |
||
5069 | 19 |
Goalw [prefix_def] "!!xs::'a list. [| xs <= ys; ys <= xs |] ==> xs = ys"; |
5132 | 20 |
by (Clarify_tac 1); |
21 |
by (Asm_full_simp_tac 1); |
|
4643 | 22 |
qed "prefix_antisym"; |
23 |
||
6675
63e53327f5e5
changes to show that Lists are partially ordered by the prefix relation
paulson
parents:
5619
diff
changeset
|
24 |
Goalw [strict_prefix_def] "!!xs::'a list. (xs < zs) = (xs <= zs & xs ~= zs)"; |
63e53327f5e5
changes to show that Lists are partially ordered by the prefix relation
paulson
parents:
5619
diff
changeset
|
25 |
by Auto_tac; |
63e53327f5e5
changes to show that Lists are partially ordered by the prefix relation
paulson
parents:
5619
diff
changeset
|
26 |
qed "prefix_less_le"; |
63e53327f5e5
changes to show that Lists are partially ordered by the prefix relation
paulson
parents:
5619
diff
changeset
|
27 |
|
63e53327f5e5
changes to show that Lists are partially ordered by the prefix relation
paulson
parents:
5619
diff
changeset
|
28 |
|
4643 | 29 |
(** recursion equations **) |
30 |
||
5069 | 31 |
Goalw [prefix_def] "[] <= xs"; |
4089 | 32 |
by (simp_tac (simpset() addsimps [eq_sym_conv]) 1); |
1344 | 33 |
qed "Nil_prefix"; |
4647 | 34 |
AddIffs[Nil_prefix]; |
1344 | 35 |
|
5069 | 36 |
Goalw [prefix_def] "(xs <= []) = (xs = [])"; |
5184 | 37 |
by (induct_tac "xs" 1); |
1344 | 38 |
by (Simp_tac 1); |
39 |
by (Simp_tac 1); |
|
40 |
qed "prefix_Nil"; |
|
41 |
Addsimps [prefix_Nil]; |
|
42 |
||
5069 | 43 |
Goalw [prefix_def] "(xs <= ys@[y]) = (xs = ys@[y] | xs <= ys)"; |
5132 | 44 |
by (rtac iffI 1); |
45 |
by (etac exE 1); |
|
46 |
by (rename_tac "zs" 1); |
|
47 |
by (res_inst_tac [("xs","zs")] rev_exhaust 1); |
|
48 |
by (Asm_full_simp_tac 1); |
|
49 |
by (hyp_subst_tac 1); |
|
50 |
by (asm_full_simp_tac (simpset() delsimps [append_assoc] |
|
4643 | 51 |
addsimps [append_assoc RS sym])1); |
6808 | 52 |
by (Force_tac 1); |
4643 | 53 |
qed "prefix_snoc"; |
54 |
Addsimps [prefix_snoc]; |
|
55 |
||
5069 | 56 |
Goalw [prefix_def] "(x#xs <= y#ys) = (x=y & xs<=ys)"; |
4643 | 57 |
by (Simp_tac 1); |
58 |
by (Fast_tac 1); |
|
59 |
qed"Cons_prefix_Cons"; |
|
60 |
Addsimps [Cons_prefix_Cons]; |
|
61 |
||
5069 | 62 |
Goal "(xs@ys <= xs@zs) = (ys <= zs)"; |
4647 | 63 |
by (induct_tac "xs" 1); |
5132 | 64 |
by (ALLGOALS Asm_simp_tac); |
4647 | 65 |
qed "same_prefix_prefix"; |
66 |
Addsimps [same_prefix_prefix]; |
|
67 |
||
5456 | 68 |
AddIffs (* (xs@ys <= xs) = (ys <= []) *) |
4647 | 69 |
[simplify (simpset()) (read_instantiate [("zs","[]")] same_prefix_prefix)]; |
70 |
||
5118 | 71 |
Goalw [prefix_def] "xs <= ys ==> xs <= ys@zs"; |
5132 | 72 |
by (Clarify_tac 1); |
4643 | 73 |
by (Simp_tac 1); |
74 |
qed "prefix_prefix"; |
|
75 |
Addsimps [prefix_prefix]; |
|
76 |
||
5069 | 77 |
Goalw [prefix_def] |
1344 | 78 |
"(xs <= y#ys) = (xs=[] | (? zs. xs=y#zs & zs <= ys))"; |
5456 | 79 |
by (exhaust_tac "xs" 1); |
80 |
by Auto_tac; |
|
1344 | 81 |
qed "prefix_Cons"; |
4647 | 82 |
|
5069 | 83 |
Goal "(xs <= ys@zs) = (xs <= ys | (? us. xs = ys@us & us <= zs))"; |
5132 | 84 |
by (res_inst_tac [("xs","zs")] rev_induct 1); |
6808 | 85 |
by (Force_tac 1); |
5132 | 86 |
by (asm_full_simp_tac (simpset() delsimps [append_assoc] |
5456 | 87 |
addsimps [append_assoc RS sym])1); |
5132 | 88 |
by (Simp_tac 1); |
89 |
by (Blast_tac 1); |
|
4647 | 90 |
qed "prefix_append"; |
5619 | 91 |
|
92 |
Goalw [prefix_def] |
|
93 |
"[| xs <= ys; length xs < length ys |] ==> xs @ [ys ! length xs] <= ys"; |
|
94 |
by (auto_tac(claset(), simpset() addsimps [nth_append])); |
|
95 |
by (exhaust_tac "ys" 1); |
|
96 |
by Auto_tac; |
|
97 |
qed "append_one_prefix"; |
|
98 |
||
99 |
Goalw [prefix_def] "xs <= ys ==> length xs <= length ys"; |
|
100 |
by Auto_tac; |
|
101 |
qed "prefix_length_le"; |
|
6675
63e53327f5e5
changes to show that Lists are partially ordered by the prefix relation
paulson
parents:
5619
diff
changeset
|
102 |
|
63e53327f5e5
changes to show that Lists are partially ordered by the prefix relation
paulson
parents:
5619
diff
changeset
|
103 |
Goal "mono length"; |
63e53327f5e5
changes to show that Lists are partially ordered by the prefix relation
paulson
parents:
5619
diff
changeset
|
104 |
by (blast_tac (claset() addIs [monoI, prefix_length_le]) 1); |
63e53327f5e5
changes to show that Lists are partially ordered by the prefix relation
paulson
parents:
5619
diff
changeset
|
105 |
qed "mono_length"; |