1signature permLib =
2sig
3  include Abbrev
4
5  (* Syntax *)
6  val PERM_tm   : term
7  val dest_PERM : term -> term * term
8  val is_PERM   : term -> bool
9
10
11
12  (* Given a term of the form "PERM l1 l2" this
13     conversion tries to eliminate common parts of
14     l1 and l2. It knows about APPEND and CONS.
15
16     Example:
17
18     PERM_ELIM_DUPLICATES_CONV ``PERM (x::l1++y::l2++l3) (y::l3++z::l2++l4)``
19
20     |- PERM (x::l1 ++ y::l2 ++ l3) (y::l3 ++ z::l2 ++ l4) <=>
21        PERM (x::l1) ([z] ++ l4)
22  *)
23  val PERM_ELIM_DUPLICATES_CONV : term -> thm
24
25  (* Given a term of the form "PERM l1 l2" this
26     conversion tries to combine TAKE and DROP parts of
27     l1 and l2. It uses that resorting is allowed inside permutations.
28
29     Example:
30
31     PERM_TAKE_DROP_CONV ``PERM (DROP n l1++l2++TAKE n l1) (l1++TAKE n l2++DROP n l2)``
32
33     |- PERM (DROP n l1 ++ l2 ++ TAKE n l1) (l1 ++ TAKE n l2 ++ DROP n l2) <=>
34        PERM (l1 ++ l2) (l2 ++ l1)
35  *)
36  val PERM_TAKE_DROP_CONV : term -> thm
37
38  (* Given a term ``PERM l1 l2`` this conversions sorts the lists l1 and l2.
39
40     Example:
41
42     PERM_NO_ELIM_NORMALISE_CONV ``PERM (x::l1++y::l2++l3) (y::l3++z::l2++l4)``
43
44     |- PERM (x::l1++y::l2++l3) (y::l3++z::l2++l4) <=>
45        PERM (x::y::(l1 ++ l2 ++ l3)) (y::z::(l2 ++ l3 ++ l4))
46  )*
47  val PERM_NO_ELIM_NORMALISE_CONV = fn : term -> thm
48
49
50  (* Turns ``PERM l1 l2`` into ``PERM l2 l1`` iff l1 is in some sence
51     smaller than l2. This is useful in combination with PERM_REWR_CONV.
52
53     Exmaple:
54
55     PERM_TURN_CONV ``PERM (x::l1) (y::z::l1 ++ l2 ++ l3)``
56
57     |- PERM (x::l1) (y::z::l1 ++ l2 ++ l3) <=>
58        PERM (y::z::l1 ++ l2 ++ l3) (x::l1)
59  *)
60  val PERM_TURN_CONV : term -> thm
61
62
63  (* Combines PERM_ELIM_DUPLICATES_CONV, PERM_NO_ELIM_NORMALISE_CONV and
64     PERM_TURN_CONV *)
65
66
67     Example:
68
69     PERM_NORMALISE_CONV ``PERM (x::l1++y::l2++l3) (y::l3++z::l2++l4)``
70
71     |- PERM (x::l1++y::l2++l3) (y::l3++z::l2++l4) <=>
72        PERM (z::l4) (x::l1)
73  *)
74  val PERM_NORMALISE_CONV : term -> thm
75
76  (* Given two terms l1 and l2. PERM_SPLIT l1 l2 tries to find
77     a l2' such that PERM l2 (l1 ++ l2') holds.
78
79     Example:
80
81     PERM_SPLIT ``(y::l4)`` ``(y::l3++z::l2++l4)``
82
83     |- PERM (y::l3++z::l2++l4) (y::l4 ++ (l3 ++ z::l2)
84  *)
85  val PERM_SPLIT : term -> term -> thm
86
87
88  (* Given a theorem |- PERM l r and a term
89     PERM l1 l2 then
90     PERM_REWR_CONV tries to replace l in l1 or l2 with r.
91     Afterwards PERM_NORMALISE_CONV is used.
92
93     Example:
94     PERM_REWR_CONV (ASSUME ``PERM l1 [x;y;z]``) ``PERM (z::y::x'::l2) (l3++x'::l1)``
95
96     [PERM l1 [x; y; z]]
97       |- PERM (z::y::x'::l2) (l3 ++ x'::l1) <=> PERM (x::l3) l2 : thm
98  *)
99  val PERM_REWR_CONV : thm -> term -> thm
100
101
102  (* A SSFRAG to use these PERM tools with the simplifier *)
103  val PERM_ss        : simpLib.ssfrag
104  val PERM_SIMPLE_ss : simpLib.ssfrag
105
106  (* brings the permutation assumptions in normal form *)
107  val NORMALISE_ASM_PERM_TAC : tactic
108
109  (* Prove `ALL_DISTINCT xs = T` by permuting to a sorted list
110     (using theorems ALL_DISTINCT_PERM and SORTED_ALL_DISTINCT).
111
112     Requires a relation R, a theorem `irreflexive R /\ transitive R`
113     a sorting function f which sorts the terms of xs in ML, and a
114     conversion that shows `R x y = T` whenever f `x` `y`.
115  *)
116  val ALL_DISTINCT_CONV : thm -> (term -> term -> bool) -> conv -> conv
117
118end
119