Structure permutesTheory

signature permutesTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val evenperm : thm
    val inverse : thm
    val permutation : thm
    val permutes : thm
    val swap_def : thm
  
  (*  Theorems  *)
    val CARD_PERMUTATIONS : thm
    val EVENPERM_COMPOSE : thm
    val EVENPERM_I : thm
    val EVENPERM_INVERSE : thm
    val EVENPERM_SWAP : thm
    val EVENPERM_UNIQUE : thm
    val FINITE_PERMUTATIONS : thm
    val FIXING_SWAPSEQ_DECREASE : thm
    val HAS_SIZE_PERMUTATIONS : thm
    val IMAGE_COMPOSE_PERMUTATIONS_L : thm
    val IMAGE_COMPOSE_PERMUTATIONS_R : thm
    val IMAGE_INVERSE_PERMUTATIONS : thm
    val INJECTIVE_INVERSE : thm
    val INJECTIVE_INVERSE_o : thm
    val INVERSE_I : thm
    val INVERSE_SWAP : thm
    val INVERSE_UNIQUE_o : thm
    val PERMUTATION : thm
    val PERMUTATION_BIJECTIVE : thm
    val PERMUTATION_COMPOSE : thm
    val PERMUTATION_COMPOSE_EQ : thm
    val PERMUTATION_COMPOSE_SWAP : thm
    val PERMUTATION_FINITE_SUPPORT : thm
    val PERMUTATION_I : thm
    val PERMUTATION_INVERSE : thm
    val PERMUTATION_INVERSE_COMPOSE : thm
    val PERMUTATION_INVERSE_WORKS : thm
    val PERMUTATION_LEMMA : thm
    val PERMUTATION_PERMUTES : thm
    val PERMUTATION_SWAP : thm
    val PERMUTES_COMPOSE : thm
    val PERMUTES_EMPTY : thm
    val PERMUTES_FINITE_INJECTIVE : thm
    val PERMUTES_FINITE_SURJECTIVE : thm
    val PERMUTES_I : thm
    val PERMUTES_IMAGE : thm
    val PERMUTES_INDUCT : thm
    val PERMUTES_INJECTIVE : thm
    val PERMUTES_INSERT : thm
    val PERMUTES_INSERT_LEMMA : thm
    val PERMUTES_INVERSE : thm
    val PERMUTES_INVERSES : thm
    val PERMUTES_INVERSES_o : thm
    val PERMUTES_INVERSE_EQ : thm
    val PERMUTES_INVERSE_INVERSE : thm
    val PERMUTES_IN_COUNT : thm
    val PERMUTES_IN_IMAGE : thm
    val PERMUTES_NUMSET_GE : thm
    val PERMUTES_NUMSET_LE : thm
    val PERMUTES_SING : thm
    val PERMUTES_SUBSET : thm
    val PERMUTES_SUPERSET : thm
    val PERMUTES_SURJECTIVE : thm
    val PERMUTES_SWAP : thm
    val PERMUTES_UNIV : thm
    val SURJECTIVE_INVERSE : thm
    val SURJECTIVE_INVERSE_o : thm
    val SWAPSEQ_COMPOSE : thm
    val SWAPSEQ_ENDSWAP : thm
    val SWAPSEQ_EVEN_EVEN : thm
    val SWAPSEQ_I : thm
    val SWAPSEQ_IDENTITY_EVEN : thm
    val SWAPSEQ_INVERSE : thm
    val SWAPSEQ_INVERSE_EXISTS : thm
    val SWAPSEQ_SWAP : thm
    val SWAP_COMMON : thm
    val SWAP_COMMON' : thm
    val SWAP_GALOIS : thm
    val SWAP_GENERAL : thm
    val SWAP_IDEMPOTENT : thm
    val SWAP_INDEPENDENT : thm
    val SWAP_REFL : thm
    val SWAP_SYM : thm
    val inverse_alt_LINV : thm
    val permutes_alt : thm
    val permutes_alt_univ : thm
    val permutes_bijn : thm
    val permutes_imp : thm
    val swapseq_cases : thm
    val swapseq_ind : thm
    val swapseq_rules : thm
    val swapseq_strongind : thm
  
  val permutes_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [cardinal] Parent theory of "permutes"
   
   [res_quan] Parent theory of "permutes"
   
   [evenperm]  Definition
      
      ⊢ ∀p. evenperm p ⇔ EVEN (@n. swapseq n p)
   
   [inverse]  Definition
      
      ⊢ ∀f. inverse f = (λy. @x. f x = y)
   
   [permutation]  Definition
      
      ⊢ ∀p. permutation p ⇔ ∃n. swapseq n p
   
   [permutes]  Definition
      
      ⊢ ∀p s. p permutes s ⇔ (∀x. x ∉ s ⇒ p x = x) ∧ ∀y. ∃!x. p x = y
   
   [swap_def]  Definition
      
      ⊢ ∀i j k. swap (i,j) k = if k = i then j else if k = j then i else k
   
   [CARD_PERMUTATIONS]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ CARD {p | p permutes s} = FACT (CARD s)
   
   [EVENPERM_COMPOSE]  Theorem
      
      ⊢ ∀p q.
          permutation p ∧ permutation q ⇒
          (evenperm (p ∘ q) ⇔ (evenperm p ⇔ evenperm q))
   
   [EVENPERM_I]  Theorem
      
      ⊢ evenperm I ⇔ T
   
   [EVENPERM_INVERSE]  Theorem
      
      ⊢ ∀p. permutation p ⇒ (evenperm (inverse p) ⇔ evenperm p)
   
   [EVENPERM_SWAP]  Theorem
      
      ⊢ ∀a b. evenperm (swap (a,b)) ⇔ a = b
   
   [EVENPERM_UNIQUE]  Theorem
      
      ⊢ ∀n p b. swapseq n p ∧ (EVEN n ⇔ b) ⇒ (evenperm p ⇔ b)
   
   [FINITE_PERMUTATIONS]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ FINITE {p | p permutes s}
   
   [FIXING_SWAPSEQ_DECREASE]  Theorem
      
      ⊢ ∀n p a b.
          swapseq n p ∧ a ≠ b ∧ (swap (a,b) ∘ p) a = a ⇒
          n ≠ 0 ∧ swapseq (n − 1) (swap (a,b) ∘ p)
   
   [HAS_SIZE_PERMUTATIONS]  Theorem
      
      ⊢ ∀s n. s HAS_SIZE n ⇒ {p | p permutes s} HAS_SIZE FACT n
   
   [IMAGE_COMPOSE_PERMUTATIONS_L]  Theorem
      
      ⊢ ∀s q. q permutes s ⇒ {q ∘ p | p permutes s} = {p | p permutes s}
   
   [IMAGE_COMPOSE_PERMUTATIONS_R]  Theorem
      
      ⊢ ∀s q. q permutes s ⇒ {p ∘ q | p permutes s} = {p | p permutes s}
   
   [IMAGE_INVERSE_PERMUTATIONS]  Theorem
      
      ⊢ ∀s. {inverse p | p permutes s} = {p | p permutes s}
   
   [INJECTIVE_INVERSE]  Theorem
      
      ⊢ ∀f. (∀x y. f x = f y ⇒ x = y) ⇔ ∀x. inverse f (f x) = x
   
   [INJECTIVE_INVERSE_o]  Theorem
      
      ⊢ ∀f. (∀x y. f x = f y ⇒ x = y) ⇔ inverse f ∘ f = I
   
   [INVERSE_I]  Theorem
      
      ⊢ inverse I = I
   
   [INVERSE_SWAP]  Theorem
      
      ⊢ ∀a b. inverse (swap (a,b)) = swap (a,b)
   
   [INVERSE_UNIQUE_o]  Theorem
      
      ⊢ ∀f g. f ∘ g = I ∧ g ∘ f = I ⇒ inverse f = g
   
   [PERMUTATION]  Theorem
      
      ⊢ ∀p. permutation p ⇔ (∀y. ∃!x. p x = y) ∧ FINITE {x | p x ≠ x}
   
   [PERMUTATION_BIJECTIVE]  Theorem
      
      ⊢ ∀p. permutation p ⇒ ∀y. ∃!x. p x = y
   
   [PERMUTATION_COMPOSE]  Theorem
      
      ⊢ ∀p q. permutation p ∧ permutation q ⇒ permutation (p ∘ q)
   
   [PERMUTATION_COMPOSE_EQ]  Theorem
      
      ⊢ (∀p q. permutation p ⇒ (permutation (p ∘ q) ⇔ permutation q)) ∧
        ∀p q. permutation q ⇒ (permutation (p ∘ q) ⇔ permutation p)
   
   [PERMUTATION_COMPOSE_SWAP]  Theorem
      
      ⊢ (∀p a b. permutation (swap (a,b) ∘ p) ⇔ permutation p) ∧
        ∀p a b. permutation (p ∘ swap (a,b)) ⇔ permutation p
   
   [PERMUTATION_FINITE_SUPPORT]  Theorem
      
      ⊢ ∀p. permutation p ⇒ FINITE {x | p x ≠ x}
   
   [PERMUTATION_I]  Theorem
      
      ⊢ permutation I
   
   [PERMUTATION_INVERSE]  Theorem
      
      ⊢ ∀p. permutation p ⇒ permutation (inverse p)
   
   [PERMUTATION_INVERSE_COMPOSE]  Theorem
      
      ⊢ ∀p q.
          permutation p ∧ permutation q ⇒
          inverse (p ∘ q) = inverse q ∘ inverse p
   
   [PERMUTATION_INVERSE_WORKS]  Theorem
      
      ⊢ ∀p. permutation p ⇒ inverse p ∘ p = I ∧ p ∘ inverse p = I
   
   [PERMUTATION_LEMMA]  Theorem
      
      ⊢ ∀s p.
          FINITE s ∧ (∀y. ∃!x. p x = y) ∧ (∀x. x ∉ s ⇒ p x = x) ⇒
          permutation p
   
   [PERMUTATION_PERMUTES]  Theorem
      
      ⊢ ∀p. permutation p ⇔ ∃s. FINITE s ∧ p permutes s
   
   [PERMUTATION_SWAP]  Theorem
      
      ⊢ ∀a b. permutation (swap (a,b))
   
   [PERMUTES_COMPOSE]  Theorem
      
      ⊢ ∀p q s x. p permutes s ∧ q permutes s ⇒ q ∘ p permutes s
   
   [PERMUTES_EMPTY]  Theorem
      
      ⊢ ∀p. p permutes ∅ ⇔ p = I
   
   [PERMUTES_FINITE_INJECTIVE]  Theorem
      
      ⊢ ∀s p.
          FINITE s ⇒
          (p permutes s ⇔
           (∀x. x ∉ s ⇒ p x = x) ∧ (∀x. x ∈ s ⇒ p x ∈ s) ∧
           ∀x y. x ∈ s ∧ y ∈ s ∧ p x = p y ⇒ x = y)
   
   [PERMUTES_FINITE_SURJECTIVE]  Theorem
      
      ⊢ ∀s p.
          FINITE s ⇒
          (p permutes s ⇔
           (∀x. x ∉ s ⇒ p x = x) ∧ (∀x. x ∈ s ⇒ p x ∈ s) ∧
           ∀y. y ∈ s ⇒ ∃x. x ∈ s ∧ p x = y)
   
   [PERMUTES_I]  Theorem
      
      ⊢ ∀s. I permutes s
   
   [PERMUTES_IMAGE]  Theorem
      
      ⊢ ∀p s. p permutes s ⇒ IMAGE p s = s
   
   [PERMUTES_INDUCT]  Theorem
      
      ⊢ ∀P s.
          FINITE s ∧ P I ∧
          (∀a b p. a ∈ s ∧ b ∈ s ∧ P p ∧ permutation p ⇒ P (swap (a,b) ∘ p)) ⇒
          ∀p. p permutes s ⇒ P p
   
   [PERMUTES_INJECTIVE]  Theorem
      
      ⊢ ∀p s. p permutes s ⇒ ∀x y. p x = p y ⇔ x = y
   
   [PERMUTES_INSERT]  Theorem
      
      ⊢ {p | p permutes a INSERT s} =
        IMAGE (λ(b,p). swap (a,b) ∘ p)
          {(b,p) | b ∈ a INSERT s ∧ p ∈ {p | p permutes s}}
   
   [PERMUTES_INSERT_LEMMA]  Theorem
      
      ⊢ ∀p a s. p permutes a INSERT s ⇒ swap (a,p a) ∘ p permutes s
   
   [PERMUTES_INVERSE]  Theorem
      
      ⊢ ∀p s. p permutes s ⇒ inverse p permutes s
   
   [PERMUTES_INVERSES]  Theorem
      
      ⊢ ∀p s.
          p permutes s ⇒
          (∀x. p (inverse p x) = x) ∧ ∀x. inverse p (p x) = x
   
   [PERMUTES_INVERSES_o]  Theorem
      
      ⊢ ∀p s. p permutes s ⇒ p ∘ inverse p = I ∧ inverse p ∘ p = I
   
   [PERMUTES_INVERSE_EQ]  Theorem
      
      ⊢ ∀p s. p permutes s ⇒ ∀x y. inverse p y = x ⇔ p x = y
   
   [PERMUTES_INVERSE_INVERSE]  Theorem
      
      ⊢ ∀p s. p permutes s ⇒ inverse (inverse p) = p
   
   [PERMUTES_IN_COUNT]  Theorem
      
      ⊢ ∀p n i. p permutes count n ∧ i ∈ count n ⇒ p i < n
   
   [PERMUTES_IN_IMAGE]  Theorem
      
      ⊢ ∀p s x. p permutes s ⇒ (p x ∈ s ⇔ x ∈ s)
   
   [PERMUTES_NUMSET_GE]  Theorem
      
      ⊢ ∀p s. p permutes s ∧ (∀i. i ∈ s ⇒ i ≤ p i) ⇒ p = I
   
   [PERMUTES_NUMSET_LE]  Theorem
      
      ⊢ ∀p s. p permutes s ∧ (∀i. i ∈ s ⇒ p i ≤ i) ⇒ p = I
   
   [PERMUTES_SING]  Theorem
      
      ⊢ ∀p a. p permutes {a} ⇔ p = I
   
   [PERMUTES_SUBSET]  Theorem
      
      ⊢ ∀p s t. p permutes s ∧ s ⊆ t ⇒ p permutes t
   
   [PERMUTES_SUPERSET]  Theorem
      
      ⊢ ∀p s t. p permutes s ∧ (∀x. x ∈ s DIFF t ⇒ p x = x) ⇒ p permutes t
   
   [PERMUTES_SURJECTIVE]  Theorem
      
      ⊢ ∀p s. p permutes s ⇒ ∀y. ∃x. p x = y
   
   [PERMUTES_SWAP]  Theorem
      
      ⊢ ∀a b s. a ∈ s ∧ b ∈ s ⇒ swap (a,b) permutes s
   
   [PERMUTES_UNIV]  Theorem
      
      ⊢ ∀p. p permutes 𝕌(:α) ⇔ ∀y. ∃!x. p x = y
   
   [SURJECTIVE_INVERSE]  Theorem
      
      ⊢ ∀f. (∀y. ∃x. f x = y) ⇔ ∀y. f (inverse f y) = y
   
   [SURJECTIVE_INVERSE_o]  Theorem
      
      ⊢ ∀f. (∀y. ∃x. f x = y) ⇔ f ∘ inverse f = I
   
   [SWAPSEQ_COMPOSE]  Theorem
      
      ⊢ ∀n p m q. swapseq n p ∧ swapseq m q ⇒ swapseq (n + m) (p ∘ q)
   
   [SWAPSEQ_ENDSWAP]  Theorem
      
      ⊢ ∀n p a b. swapseq n p ∧ a ≠ b ⇒ swapseq (SUC n) (p ∘ swap (a,b))
   
   [SWAPSEQ_EVEN_EVEN]  Theorem
      
      ⊢ ∀m n p. swapseq m p ∧ swapseq n p ⇒ (EVEN m ⇔ EVEN n)
   
   [SWAPSEQ_I]  Theorem
      
      ⊢ swapseq 0 I
   
   [SWAPSEQ_IDENTITY_EVEN]  Theorem
      
      ⊢ ∀n. swapseq n I ⇒ EVEN n
   
   [SWAPSEQ_INVERSE]  Theorem
      
      ⊢ ∀n p. swapseq n p ⇒ swapseq n (inverse p)
   
   [SWAPSEQ_INVERSE_EXISTS]  Theorem
      
      ⊢ ∀n p. swapseq n p ⇒ ∃q. swapseq n q ∧ p ∘ q = I ∧ q ∘ p = I
   
   [SWAPSEQ_SWAP]  Theorem
      
      ⊢ ∀a b. swapseq (if a = b then 0 else 1) (swap (a,b))
   
   [SWAP_COMMON]  Theorem
      
      ⊢ ∀a b c.
          a ≠ c ∧ b ≠ c ⇒ swap (a,b) ∘ swap (a,c) = swap (b,c) ∘ swap (a,b)
   
   [SWAP_COMMON']  Theorem
      
      ⊢ ∀a b c.
          a ≠ b ∧ a ≠ c ⇒ swap (a,c) ∘ swap (b,c) = swap (b,c) ∘ swap (a,b)
   
   [SWAP_GALOIS]  Theorem
      
      ⊢ ∀a b x y. x = swap (a,b) y ⇔ y = swap (a,b) x
   
   [SWAP_GENERAL]  Theorem
      
      ⊢ ∀a b c d.
          a ≠ b ∧ c ≠ d ⇒
          swap (a,b) ∘ swap (c,d) = I ∨
          ∃x y z.
            x ≠ a ∧ y ≠ a ∧ z ≠ a ∧ x ≠ y ∧
            swap (a,b) ∘ swap (c,d) = swap (x,y) ∘ swap (a,z)
   
   [SWAP_IDEMPOTENT]  Theorem
      
      ⊢ ∀a b. swap (a,b) ∘ swap (a,b) = I
   
   [SWAP_INDEPENDENT]  Theorem
      
      ⊢ ∀a b c d.
          a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ⇒
          swap (a,b) ∘ swap (c,d) = swap (c,d) ∘ swap (a,b)
   
   [SWAP_REFL]  Theorem
      
      ⊢ ∀a. swap (a,a) = I
   
   [SWAP_SYM]  Theorem
      
      ⊢ ∀a b. swap (a,b) = swap (b,a)
   
   [inverse_alt_LINV]  Theorem
      
      ⊢ ∀f. (∀y. ∃x. f x = y) ∧ (∀x y. f x = f y ⇒ x = y) ⇒
            inverse f = LINV f 𝕌(:α)
   
   [permutes_alt]  Theorem
      
      ⊢ ∀f s. f permutes s ⇔ f PERMUTES s ∧ ∀x. x ∉ s ⇒ f x = x
   
   [permutes_alt_univ]  Theorem
      
      ⊢ ∀f. f permutes 𝕌(:α) ⇔ f PERMUTES 𝕌(:α)
   
   [permutes_bijn]  Theorem
      
      ⊢ f permutes s ⇔ f ∈ bijns s
   
   [permutes_imp]  Theorem
      
      ⊢ ∀f s. f permutes s ⇒ f PERMUTES s
   
   [swapseq_cases]  Theorem
      
      ⊢ ∀a0 a1.
          swapseq a0 a1 ⇔
          a0 = 0 ∧ a1 = I ∨
          ∃a b p n. a0 = SUC n ∧ a1 = swap (a,b) ∘ p ∧ swapseq n p ∧ a ≠ b
   
   [swapseq_ind]  Theorem
      
      ⊢ ∀swapseq'.
          swapseq' 0 I ∧
          (∀a b p n.
             swapseq' n p ∧ a ≠ b ⇒ swapseq' (SUC n) (swap (a,b) ∘ p)) ⇒
          ∀a0 a1. swapseq a0 a1 ⇒ swapseq' a0 a1
   
   [swapseq_rules]  Theorem
      
      ⊢ swapseq 0 I ∧
        ∀a b p n. swapseq n p ∧ a ≠ b ⇒ swapseq (SUC n) (swap (a,b) ∘ p)
   
   [swapseq_strongind]  Theorem
      
      ⊢ ∀swapseq'.
          swapseq' 0 I ∧
          (∀a b p n.
             swapseq n p ∧ swapseq' n p ∧ a ≠ b ⇒
             swapseq' (SUC n) (swap (a,b) ∘ p)) ⇒
          ∀a0 a1. swapseq a0 a1 ⇒ swapseq' a0 a1
   
   
*)
end

HOL 4, Trindemossen-1