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 |
(* Junk: *)
|
3842
|
8 |
val [maj,min] = goal Prefix.thy "[| Q([]); !! y ys. Q(y#ys) |] ==> ! l. Q(l)";
|
1465
|
9 |
by (rtac allI 1);
|
1344
|
10 |
by (list.induct_tac "l" 1);
|
1465
|
11 |
by (rtac maj 1);
|
|
12 |
by (rtac min 1);
|
1344
|
13 |
val list_cases = result();
|
|
14 |
|
4643
|
15 |
(** <= is a partial order: **)
|
|
16 |
|
5069
|
17 |
Goalw [prefix_def] "xs <= (xs::'a list)";
|
4643
|
18 |
by(Simp_tac 1);
|
|
19 |
qed "prefix_refl";
|
4647
|
20 |
AddIffs[prefix_refl];
|
4643
|
21 |
|
5069
|
22 |
Goalw [prefix_def] "!!xs::'a list. [| xs <= ys; ys <= zs |] ==> xs <= zs";
|
4643
|
23 |
by(Clarify_tac 1);
|
|
24 |
by(Simp_tac 1);
|
|
25 |
qed "prefix_trans";
|
|
26 |
|
5069
|
27 |
Goalw [prefix_def] "!!xs::'a list. [| xs <= ys; ys <= xs |] ==> xs = ys";
|
4643
|
28 |
by(Clarify_tac 1);
|
|
29 |
by(Asm_full_simp_tac 1);
|
|
30 |
qed "prefix_antisym";
|
|
31 |
|
|
32 |
(** recursion equations **)
|
|
33 |
|
5069
|
34 |
Goalw [prefix_def] "[] <= xs";
|
4089
|
35 |
by (simp_tac (simpset() addsimps [eq_sym_conv]) 1);
|
1344
|
36 |
qed "Nil_prefix";
|
4647
|
37 |
AddIffs[Nil_prefix];
|
1344
|
38 |
|
5069
|
39 |
Goalw [prefix_def] "(xs <= []) = (xs = [])";
|
1344
|
40 |
by (list.induct_tac "xs" 1);
|
|
41 |
by (Simp_tac 1);
|
|
42 |
by (Simp_tac 1);
|
|
43 |
qed "prefix_Nil";
|
|
44 |
Addsimps [prefix_Nil];
|
|
45 |
|
5069
|
46 |
Goalw [prefix_def] "(xs <= ys@[y]) = (xs = ys@[y] | xs <= ys)";
|
4643
|
47 |
br iffI 1;
|
|
48 |
be exE 1;
|
|
49 |
by(rename_tac "zs" 1);
|
4936
|
50 |
by(res_inst_tac [("xs","zs")] rev_exhaust 1);
|
4643
|
51 |
by(Asm_full_simp_tac 1);
|
|
52 |
by(hyp_subst_tac 1);
|
|
53 |
by(asm_full_simp_tac (simpset() delsimps [append_assoc]
|
|
54 |
addsimps [append_assoc RS sym])1);
|
|
55 |
be disjE 1;
|
|
56 |
by(Asm_simp_tac 1);
|
|
57 |
by(Clarify_tac 1);
|
|
58 |
by (Simp_tac 1);
|
|
59 |
qed "prefix_snoc";
|
|
60 |
Addsimps [prefix_snoc];
|
|
61 |
|
5069
|
62 |
Goalw [prefix_def] "(x#xs <= y#ys) = (x=y & xs<=ys)";
|
4643
|
63 |
by (Simp_tac 1);
|
|
64 |
by (Fast_tac 1);
|
|
65 |
qed"Cons_prefix_Cons";
|
|
66 |
Addsimps [Cons_prefix_Cons];
|
|
67 |
|
5069
|
68 |
Goal "(xs@ys <= xs@zs) = (ys <= zs)";
|
4647
|
69 |
by (induct_tac "xs" 1);
|
|
70 |
by(ALLGOALS Asm_simp_tac);
|
|
71 |
qed "same_prefix_prefix";
|
|
72 |
Addsimps [same_prefix_prefix];
|
|
73 |
|
|
74 |
AddIffs
|
|
75 |
[simplify (simpset()) (read_instantiate [("zs","[]")] same_prefix_prefix)];
|
|
76 |
|
5069
|
77 |
Goalw [prefix_def] "!!xs. xs <= ys ==> xs <= ys@zs";
|
4643
|
78 |
by(Clarify_tac 1);
|
|
79 |
by (Simp_tac 1);
|
|
80 |
qed "prefix_prefix";
|
|
81 |
Addsimps [prefix_prefix];
|
|
82 |
|
1344
|
83 |
(* nicht sehr elegant bewiesen - Induktion eigentlich ueberfluessig *)
|
5069
|
84 |
Goalw [prefix_def]
|
1344
|
85 |
"(xs <= y#ys) = (xs=[] | (? zs. xs=y#zs & zs <= ys))";
|
|
86 |
by (list.induct_tac "xs" 1);
|
|
87 |
by (Simp_tac 1);
|
|
88 |
by (Simp_tac 1);
|
1894
|
89 |
by (Fast_tac 1);
|
1344
|
90 |
qed "prefix_Cons";
|
4647
|
91 |
|
5069
|
92 |
Goal "(xs <= ys@zs) = (xs <= ys | (? us. xs = ys@us & us <= zs))";
|
4936
|
93 |
by(res_inst_tac [("xs","zs")] rev_induct 1);
|
4647
|
94 |
by(Simp_tac 1);
|
|
95 |
by(Blast_tac 1);
|
|
96 |
by(asm_full_simp_tac (simpset() delsimps [append_assoc]
|
|
97 |
addsimps [append_assoc RS sym])1);
|
|
98 |
by(Simp_tac 1);
|
|
99 |
by(Blast_tac 1);
|
|
100 |
qed "prefix_append";
|