|
1 (* Title: HOL/UNITY/GenPrefix.thy |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1999 University of Cambridge |
|
5 |
|
6 Charpentier's Generalized Prefix Relation |
|
7 (xs,ys) : genPrefix(r) |
|
8 if ys = xs' @ zs where length xs = length xs' |
|
9 and corresponding elements of xs, xs' are pairwise related by r |
|
10 |
|
11 Also overloads <= and < for lists! |
|
12 |
|
13 Based on Lex/Prefix |
|
14 *) |
|
15 |
|
16 GenPrefix = Main + |
|
17 |
|
18 consts |
|
19 genPrefix :: "('a * 'a)set => ('a list * 'a list)set" |
|
20 |
|
21 inductive "genPrefix(r)" |
|
22 intrs |
|
23 Nil "([],[]) : genPrefix(r)" |
|
24 |
|
25 prepend "[| (xs,ys) : genPrefix(r); (x,y) : r |] ==> |
|
26 (x#xs, y#ys) : genPrefix(r)" |
|
27 |
|
28 append "(xs,ys) : genPrefix(r) ==> (xs, ys@zs) : genPrefix(r)" |
|
29 |
|
30 arities list :: (term)ord |
|
31 |
|
32 defs |
|
33 prefix_def "xs <= zs == (xs,zs) : genPrefix Id" |
|
34 |
|
35 strict_prefix_def "xs < zs == xs <= zs & xs ~= (zs::'a list)" |
|
36 |
|
37 |
|
38 (*Constants for the <= and >= relations, used below in translations*) |
|
39 constdefs |
|
40 Le :: "(nat*nat) set" |
|
41 "Le == {(x,y). x <= y}" |
|
42 |
|
43 Ge :: "(nat*nat) set" |
|
44 "Ge == {(x,y). y <= x}" |
|
45 |
|
46 syntax |
|
47 pfixLe :: [nat list, nat list] => bool (infixl "pfix'_le" 50) |
|
48 pfixGe :: [nat list, nat list] => bool (infixl "pfix'_ge" 50) |
|
49 |
|
50 translations |
|
51 "xs pfix_le ys" == "(xs,ys) : genPrefix Le" |
|
52 |
|
53 "xs pfix_ge ys" == "(xs,ys) : genPrefix Ge" |
|
54 |
|
55 end |