Structure gcdsetTheory

signature gcdsetTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val big_gcd_def : thm
    val big_lcm_def : thm
    val coprimes_def : thm
    val gcdset_def : thm
  
  (*  Theorems  *)
    val big_gcd_empty : thm
    val big_gcd_insert : thm
    val big_gcd_is_common_divisor : thm
    val big_gcd_is_greatest_common_divisor : thm
    val big_gcd_map_times : thm
    val big_gcd_positive : thm
    val big_gcd_reduction : thm
    val big_gcd_sing : thm
    val big_gcd_two : thm
    val big_lcm_empty : thm
    val big_lcm_insert : thm
    val big_lcm_is_common_multiple : thm
    val big_lcm_is_least_common_multiple : thm
    val big_lcm_map_times : thm
    val big_lcm_positive : thm
    val big_lcm_reduction : thm
    val big_lcm_sing : thm
    val big_lcm_two : thm
    val coprimes_0 : thm
    val coprimes_1 : thm
    val coprimes_alt : thm
    val coprimes_element : thm
    val coprimes_element_alt : thm
    val coprimes_element_less : thm
    val coprimes_eq_empty : thm
    val coprimes_finite : thm
    val coprimes_has_1 : thm
    val coprimes_has_last_but_1 : thm
    val coprimes_max : thm
    val coprimes_no_0 : thm
    val coprimes_subset : thm
    val coprimes_with_last : thm
    val coprimes_without_last : thm
    val gcdset_EMPTY : thm
    val gcdset_INSERT : thm
    val gcdset_divides : thm
    val gcdset_greatest : thm
    val natural_0 : thm
    val natural_1 : thm
    val natural_card : thm
    val natural_cofactor_natural : thm
    val natural_cofactor_natural_reduced : thm
    val natural_divisor_natural : thm
    val natural_element : thm
    val natural_finite : thm
    val natural_has_1 : thm
    val natural_has_last : thm
    val natural_not_0 : thm
    val natural_property : thm
    val natural_suc : thm
(*
   [gcd] Parent theory of "gcdset"
   
   [pred_set] Parent theory of "gcdset"
   
   [big_gcd_def]  Definition
      
      ⊢ ∀s. big_gcd s = ITSET gcd s 0
   
   [big_lcm_def]  Definition
      
      ⊢ ∀s. big_lcm s = ITSET lcm s 1
   
   [coprimes_def]  Definition
      
      ⊢ ∀n. coprimes n = {j | j ∈ natural n ∧ coprime j n}
   
   [gcdset_def]  Definition
      
      ⊢ ∀s. gcdset s =
            if s = ∅ ∨ s = {0} then 0
            else
              MAX_SET
                ({n | n ≤ MIN_SET (s DELETE 0)} ∩
                 {d | ∀e. e ∈ s ⇒ d divides e})
   
   [big_gcd_empty]  Theorem
      
      ⊢ big_gcd ∅ = 0
   
   [big_gcd_insert]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ ∀x. big_gcd (x INSERT s) = gcd x (big_gcd s)
   
   [big_gcd_is_common_divisor]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ ∀x. x ∈ s ⇒ big_gcd s divides x
   
   [big_gcd_is_greatest_common_divisor]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ ∀m. (∀x. x ∈ s ⇒ m divides x) ⇒ m divides big_gcd s
   
   [big_gcd_map_times]  Theorem
      
      ⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ ∀k. big_gcd (IMAGE ($* k) s) = k * big_gcd s
   
   [big_gcd_positive]  Theorem
      
      ⊢ ∀s. FINITE s ∧ s ≠ ∅ ∧ (∀x. x ∈ s ⇒ 0 < x) ⇒ 0 < big_gcd s
   
   [big_gcd_reduction]  Theorem
      
      ⊢ ∀s x. FINITE s ∧ x ∉ s ⇒ big_gcd (x INSERT s) = gcd x (big_gcd s)
   
   [big_gcd_sing]  Theorem
      
      ⊢ ∀x. big_gcd {x} = x
   
   [big_gcd_two]  Theorem
      
      ⊢ ∀x y. big_gcd {x; y} = gcd x y
   
   [big_lcm_empty]  Theorem
      
      ⊢ big_lcm ∅ = 1
   
   [big_lcm_insert]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ ∀x. big_lcm (x INSERT s) = lcm x (big_lcm s)
   
   [big_lcm_is_common_multiple]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ ∀x. x ∈ s ⇒ x divides big_lcm s
   
   [big_lcm_is_least_common_multiple]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ ∀m. (∀x. x ∈ s ⇒ x divides m) ⇒ big_lcm s divides m
   
   [big_lcm_map_times]  Theorem
      
      ⊢ ∀s. FINITE s ∧ s ≠ ∅ ⇒ ∀k. big_lcm (IMAGE ($* k) s) = k * big_lcm s
   
   [big_lcm_positive]  Theorem
      
      ⊢ ∀s. FINITE s ⇒ (∀x. x ∈ s ⇒ 0 < x) ⇒ 0 < big_lcm s
   
   [big_lcm_reduction]  Theorem
      
      ⊢ ∀s x. FINITE s ∧ x ∉ s ⇒ big_lcm (x INSERT s) = lcm x (big_lcm s)
   
   [big_lcm_sing]  Theorem
      
      ⊢ ∀x. big_lcm {x} = x
   
   [big_lcm_two]  Theorem
      
      ⊢ ∀x y. big_lcm {x; y} = lcm x y
   
   [coprimes_0]  Theorem
      
      ⊢ coprimes 0 = ∅
   
   [coprimes_1]  Theorem
      
      ⊢ coprimes 1 = {1}
   
   [coprimes_alt]  Theorem
      
      ⊢ ∀n. coprimes n = natural n ∩ {j | coprime j n}
   
   [coprimes_element]  Theorem
      
      ⊢ ∀n j. j ∈ coprimes n ⇔ 0 < j ∧ j ≤ n ∧ coprime j n
   
   [coprimes_element_alt]  Theorem
      
      ⊢ ∀n. 1 < n ⇒ ∀j. j ∈ coprimes n ⇔ j < n ∧ coprime j n
   
   [coprimes_element_less]  Theorem
      
      ⊢ ∀n. 1 < n ⇒ ∀j. j ∈ coprimes n ⇒ j < n
   
   [coprimes_eq_empty]  Theorem
      
      ⊢ ∀n. coprimes n = ∅ ⇔ n = 0
   
   [coprimes_finite]  Theorem
      
      ⊢ ∀n. FINITE (coprimes n)
   
   [coprimes_has_1]  Theorem
      
      ⊢ ∀n. 0 < n ⇒ 1 ∈ coprimes n
   
   [coprimes_has_last_but_1]  Theorem
      
      ⊢ ∀n. 1 < n ⇒ n − 1 ∈ coprimes n
   
   [coprimes_max]  Theorem
      
      ⊢ ∀n. 1 < n ⇒ MAX_SET (coprimes n) = n − 1
   
   [coprimes_no_0]  Theorem
      
      ⊢ ∀n. 0 ∉ coprimes n
   
   [coprimes_subset]  Theorem
      
      ⊢ ∀n. coprimes n ⊆ natural n
   
   [coprimes_with_last]  Theorem
      
      ⊢ ∀n. n ∈ coprimes n ⇔ n = 1
   
   [coprimes_without_last]  Theorem
      
      ⊢ ∀n. 1 < n ⇒ n ∉ coprimes n
   
   [gcdset_EMPTY]  Theorem
      
      ⊢ gcdset ∅ = 0
   
   [gcdset_INSERT]  Theorem
      
      ⊢ gcdset (x INSERT s) = gcd x (gcdset s)
   
   [gcdset_divides]  Theorem
      
      ⊢ ∀e. e ∈ s ⇒ gcdset s divides e
   
   [gcdset_greatest]  Theorem
      
      ⊢ (∀e. e ∈ s ⇒ g divides e) ⇒ g divides gcdset s
   
   [natural_0]  Theorem
      
      ⊢ natural 0 = ∅
   
   [natural_1]  Theorem
      
      ⊢ natural 1 = {1}
   
   [natural_card]  Theorem
      
      ⊢ ∀n. CARD (natural n) = n
   
   [natural_cofactor_natural]  Theorem
      
      ⊢ ∀n a b.
          0 < n ∧ 0 < a ∧ b ∈ natural n ∧ a divides b ⇒ b DIV a ∈ natural n
   
   [natural_cofactor_natural_reduced]  Theorem
      
      ⊢ ∀n a b.
          0 < n ∧ a divides n ∧ b ∈ natural n ∧ a divides b ⇒
          b DIV a ∈ natural (n DIV a)
   
   [natural_divisor_natural]  Theorem
      
      ⊢ ∀n a b. 0 < n ∧ a ∈ natural n ∧ b divides a ⇒ b ∈ natural n
   
   [natural_element]  Theorem
      
      ⊢ ∀n j. j ∈ natural n ⇔ 0 < j ∧ j ≤ n
   
   [natural_finite]  Theorem
      
      ⊢ ∀n. FINITE (natural n)
   
   [natural_has_1]  Theorem
      
      ⊢ ∀n. 0 < n ⇒ 1 ∈ natural n
   
   [natural_has_last]  Theorem
      
      ⊢ ∀n. 0 < n ⇒ n ∈ natural n
   
   [natural_not_0]  Theorem
      
      ⊢ ∀n. 0 ∉ natural n
   
   [natural_property]  Theorem
      
      ⊢ ∀n. natural n = {j | 0 < j ∧ j ≤ n}
   
   [natural_suc]  Theorem
      
      ⊢ ∀n. natural (SUC n) = SUC n INSERT natural n
   
   
*)
end

HOL 4, Trindemossen-2