author | wenzelm |
Sat, 01 Dec 2001 18:52:32 +0100 | |
changeset 12338 | de0f4a63baa5 |
parent 9382 | 7cea1cb9703e |
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 |
Also overloads <= and < for lists! |
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 |
Based on Lex/Prefix |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
14 |
*) |
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 |
GenPrefix = Main + |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
17 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
18 |
consts |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
19 |
genPrefix :: "('a * 'a)set => ('a list * 'a list)set" |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
20 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
21 |
inductive "genPrefix(r)" |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
22 |
intrs |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
23 |
Nil "([],[]) : genPrefix(r)" |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
24 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
25 |
prepend "[| (xs,ys) : genPrefix(r); (x,y) : r |] ==> |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
26 |
(x#xs, y#ys) : genPrefix(r)" |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
27 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
28 |
append "(xs,ys) : genPrefix(r) ==> (xs, ys@zs) : genPrefix(r)" |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
29 |
|
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
9382
diff
changeset
|
30 |
instance list :: (type)ord |
6804
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
31 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
32 |
defs |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
33 |
prefix_def "xs <= zs == (xs,zs) : genPrefix Id" |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
34 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
35 |
strict_prefix_def "xs < zs == xs <= zs & xs ~= (zs::'a list)" |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
36 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
37 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
38 |
(*Constants for the <= and >= relations, used below in translations*) |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
39 |
constdefs |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
40 |
Le :: "(nat*nat) set" |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
41 |
"Le == {(x,y). x <= y}" |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
42 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
43 |
Ge :: "(nat*nat) set" |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
44 |
"Ge == {(x,y). y <= x}" |
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
45 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
46 |
syntax |
6824 | 47 |
pfixLe :: [nat list, nat list] => bool (infixl "pfixLe" 50) |
48 |
pfixGe :: [nat list, nat list] => bool (infixl "pfixGe" 50) |
|
6804
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
49 |
|
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
50 |
translations |
6824 | 51 |
"xs pfixLe ys" == "(xs,ys) : genPrefix Le" |
6804
66dc8e62a987
Generalized prefix theory, replacing the reference to directory Lex.
paulson
parents:
diff
changeset
|
52 |
|
6824 | 53 |
"xs pfixGe ys" == "(xs,ys) : genPrefix Ge" |
6804
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 |
end |