1344
|
1 |
(* Title: HOL/Lex/Prefix.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Richard Mayr & Tobias Nipkow
|
|
4 |
Copyright 1995 TUM
|
|
5 |
*)
|
|
6 |
|
|
7 |
open Prefix;
|
|
8 |
|
|
9 |
val [maj,min] = goal Prefix.thy "[| Q([]); !! y ys. Q(y#ys) |] ==> ! l.Q(l)";
|
|
10 |
br allI 1;
|
|
11 |
by (list.induct_tac "l" 1);
|
|
12 |
br maj 1;
|
|
13 |
br min 1;
|
|
14 |
val list_cases = result();
|
|
15 |
|
|
16 |
goalw Prefix.thy [prefix_def] "[] <= xs";
|
|
17 |
by (simp_tac (!simpset addsimps [eq_sym_conv]) 1);
|
|
18 |
qed "Nil_prefix";
|
|
19 |
Addsimps[Nil_prefix];
|
|
20 |
|
|
21 |
goalw Prefix.thy [prefix_def] "(xs <= []) = (xs = [])";
|
|
22 |
by (list.induct_tac "xs" 1);
|
|
23 |
by (Simp_tac 1);
|
|
24 |
by (fast_tac HOL_cs 1);
|
|
25 |
by (Simp_tac 1);
|
|
26 |
qed "prefix_Nil";
|
|
27 |
Addsimps [prefix_Nil];
|
|
28 |
|
|
29 |
(* nicht sehr elegant bewiesen - Induktion eigentlich ueberfluessig *)
|
|
30 |
goalw Prefix.thy [prefix_def]
|
|
31 |
"(xs <= y#ys) = (xs=[] | (? zs. xs=y#zs & zs <= ys))";
|
|
32 |
by (list.induct_tac "xs" 1);
|
|
33 |
by (Simp_tac 1);
|
|
34 |
by (fast_tac HOL_cs 1);
|
|
35 |
by (Simp_tac 1);
|
|
36 |
by (fast_tac HOL_cs 1);
|
|
37 |
qed "prefix_Cons";
|
|
38 |
|
|
39 |
goalw Prefix.thy [prefix_def] "(x#xs <= y#ys) = (x=y & xs<=ys)";
|
|
40 |
by(Simp_tac 1);
|
|
41 |
by (fast_tac HOL_cs 1);
|
|
42 |
qed"Cons_prefix_Cons";
|
|
43 |
Addsimps [Cons_prefix_Cons];
|