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