Structure ringTheory


Source File Identifier index Theory binding index

signature ringTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val is_ring_def : thm
    val ring_R0 : thm
    val ring_R0_fupd : thm
    val ring_R1 : thm
    val ring_R1_fupd : thm
    val ring_RM : thm
    val ring_RM_fupd : thm
    val ring_RN : thm
    val ring_RN_fupd : thm
    val ring_RP : thm
    val ring_RP_fupd : thm
    val ring_TY_DEF : thm
    val ring_case_def : thm
    val ring_size_def : thm
    val semi_ring_of_def : thm
  
  (*  Theorems  *)
    val EXISTS_ring : thm
    val FORALL_ring : thm
    val datatype_ring : thm
    val distr_left : thm
    val mult_assoc : thm
    val mult_one_left : thm
    val mult_one_right : thm
    val mult_sym : thm
    val mult_zero_left : thm
    val mult_zero_right : thm
    val neg_mult : thm
    val opp_def : thm
    val plus_assoc : thm
    val plus_sym : thm
    val plus_zero_left : thm
    val plus_zero_right : thm
    val ring_11 : thm
    val ring_Axiom : thm
    val ring_accessors : thm
    val ring_accfupds : thm
    val ring_case_cong : thm
    val ring_case_eq : thm
    val ring_component_equality : thm
    val ring_fn_updates : thm
    val ring_fupdcanon : thm
    val ring_fupdcanon_comp : thm
    val ring_fupdfupds : thm
    val ring_fupdfupds_comp : thm
    val ring_induction : thm
    val ring_is_semi_ring : thm
    val ring_literal_11 : thm
    val ring_literal_nchotomy : thm
    val ring_nchotomy : thm
    val ring_updates_eq_literal : thm
  
  val ring_grammars : type_grammar.grammar * term_grammar.grammar
  
  val IMPORT : abstraction.inst_infos ->
    { is_ring_def : thm,
  ring_case_def : thm,
  ring_R0 : thm,
  ring_R0_fupd : thm,
  ring_R1 : thm,
  ring_R1_fupd : thm,
  ring_RM : thm,
  ring_RM_fupd : thm,
  ring_RN : thm,
  ring_RN_fupd : thm,
  ring_RP : thm,
  ring_RP_fupd : thm,
  ring_size_def : thm,
  ring_TY_DEF : thm,
  semi_ring_of_def : thm,
  datatype_ring : thm,
  distr_left : thm,
  EXISTS_ring : thm,
  FORALL_ring : thm,
  mult_assoc : thm,
  mult_one_left : thm,
  mult_one_right : thm,
  mult_sym : thm,
  mult_zero_left : thm,
  mult_zero_right : thm,
  neg_mult : thm,
  opp_def : thm,
  plus_assoc : thm,
  plus_sym : thm,
  plus_zero_left : thm,
  plus_zero_right : thm,
  ring_11 : thm,
  ring_accessors : thm,
  ring_accfupds : thm,
  ring_Axiom : thm,
  ring_case_cong : thm,
  ring_case_eq : thm,
  ring_component_equality : thm,
  ring_fn_updates : thm,
  ring_fupdcanon : thm,
  ring_fupdcanon_comp : thm,
  ring_fupdfupds : thm,
  ring_fupdfupds_comp : thm,
  ring_induction : thm,
  ring_is_semi_ring : thm,
  ring_literal_11 : thm,
  ring_literal_nchotomy : thm,
  ring_nchotomy : thm,
  ring_updates_eq_literal : thm }
  
(*
   [semi_ring] Parent theory of "ring"
   
   [is_ring_def]  Definition
      
      ⊢ ∀r. is_ring r ⇔
            (∀n m. r.RP n m = r.RP m n) ∧
            (∀n m p. r.RP n (r.RP m p) = r.RP (r.RP n m) p) ∧
            (∀n m. r.RM n m = r.RM m n) ∧
            (∀n m p. r.RM n (r.RM m p) = r.RM (r.RM n m) p) ∧
            (∀n. r.RP r.R0 n = n) ∧ (∀n. r.RM r.R1 n = n) ∧
            (∀n. r.RP n (r.RN n) = r.R0) ∧
            ∀n m p. r.RM (r.RP n m) p = r.RP (r.RM n p) (r.RM m p)
   
   [ring_R0]  Definition
      
      ⊢ ∀a a0 f f0 f1. (ring a a0 f f0 f1).R0 = a
   
   [ring_R0_fupd]  Definition
      
      ⊢ ∀f2 a a0 f f0 f1.
          ring a a0 f f0 f1 with R0 updated_by f2 = ring (f2 a) a0 f f0 f1
   
   [ring_R1]  Definition
      
      ⊢ ∀a a0 f f0 f1. (ring a a0 f f0 f1).R1 = a0
   
   [ring_R1_fupd]  Definition
      
      ⊢ ∀f2 a a0 f f0 f1.
          ring a a0 f f0 f1 with R1 updated_by f2 = ring a (f2 a0) f f0 f1
   
   [ring_RM]  Definition
      
      ⊢ ∀a a0 f f0 f1. (ring a a0 f f0 f1).RM = f0
   
   [ring_RM_fupd]  Definition
      
      ⊢ ∀f2 a a0 f f0 f1.
          ring a a0 f f0 f1 with RM updated_by f2 = ring a a0 f (f2 f0) f1
   
   [ring_RN]  Definition
      
      ⊢ ∀a a0 f f0 f1. (ring a a0 f f0 f1).RN = f1
   
   [ring_RN_fupd]  Definition
      
      ⊢ ∀f2 a a0 f f0 f1.
          ring a a0 f f0 f1 with RN updated_by f2 = ring a a0 f f0 (f2 f1)
   
   [ring_RP]  Definition
      
      ⊢ ∀a a0 f f0 f1. (ring a a0 f f0 f1).RP = f
   
   [ring_RP_fupd]  Definition
      
      ⊢ ∀f2 a a0 f f0 f1.
          ring a a0 f f0 f1 with RP updated_by f2 = ring a a0 (f2 f) f0 f1
   
   [ring_TY_DEF]  Definition
      
      ⊢ ∃rep.
          TYPE_DEFINITION
            (λa0'.
                 ∀ $var$('ring').
                   (∀a0'.
                      (∃a0 a1 a2 a3 a4.
                         a0' =
                         (λa0 a1 a2 a3 a4.
                              ind_type$CONSTR 0 (a0,a1,a2,a3,a4)
                                (λn. ind_type$BOTTOM)) a0 a1 a2 a3 a4) ⇒
                      $var$('ring') a0') ⇒
                   $var$('ring') a0') rep
   
   [ring_case_def]  Definition
      
      ⊢ ∀a0 a1 a2 a3 a4 f.
          ring_CASE (ring a0 a1 a2 a3 a4) f = f a0 a1 a2 a3 a4
   
   [ring_size_def]  Definition
      
      ⊢ ∀f a0 a1 a2 a3 a4.
          ring_size f (ring a0 a1 a2 a3 a4) = 1 + (f a0 + f a1)
   
   [semi_ring_of_def]  Definition
      
      ⊢ ∀r. semi_ring_of r = semi_ring r.R0 r.R1 r.RP r.RM
   
   [EXISTS_ring]  Theorem
      
      ⊢ ∀P. (∃r. P r) ⇔
            ∃a0 a f1 f0 f.
              P <|R0 := a0; R1 := a; RP := f1; RM := f0; RN := f|>
   
   [FORALL_ring]  Theorem
      
      ⊢ ∀P. (∀r. P r) ⇔
            ∀a0 a f1 f0 f.
              P <|R0 := a0; R1 := a; RP := f1; RM := f0; RN := f|>
   
   [datatype_ring]  Theorem
      
      ⊢ DATATYPE (record ring R0 R1 RP RM RN)
   
   [distr_left]  Theorem
      
      ⊢ ∀r. is_ring r ⇒
            ∀n m p. r.RM (r.RP n m) p = r.RP (r.RM n p) (r.RM m p)
   
   [mult_assoc]  Theorem
      
      ⊢ ∀r. is_ring r ⇒ ∀n m p. r.RM n (r.RM m p) = r.RM (r.RM n m) p
   
   [mult_one_left]  Theorem
      
      ⊢ ∀r. is_ring r ⇒ ∀n. r.RM r.R1 n = n
   
   [mult_one_right]  Theorem
      
      ⊢ ∀r. is_ring r ⇒ ∀n. r.RM n r.R1 = n
   
   [mult_sym]  Theorem
      
      ⊢ ∀r. is_ring r ⇒ ∀n m. r.RM n m = r.RM m n
   
   [mult_zero_left]  Theorem
      
      ⊢ ∀r. is_ring r ⇒ ∀n. r.RM r.R0 n = r.R0
   
   [mult_zero_right]  Theorem
      
      ⊢ ∀r. is_ring r ⇒ ∀n. r.RM n r.R0 = r.R0
   
   [neg_mult]  Theorem
      
      ⊢ ∀r. is_ring r ⇒ ∀a b. r.RM (r.RN a) b = r.RN (r.RM a b)
   
   [opp_def]  Theorem
      
      ⊢ ∀r. is_ring r ⇒ ∀n. r.RP n (r.RN n) = r.R0
   
   [plus_assoc]  Theorem
      
      ⊢ ∀r. is_ring r ⇒ ∀n m p. r.RP n (r.RP m p) = r.RP (r.RP n m) p
   
   [plus_sym]  Theorem
      
      ⊢ ∀r. is_ring r ⇒ ∀n m. r.RP n m = r.RP m n
   
   [plus_zero_left]  Theorem
      
      ⊢ ∀r. is_ring r ⇒ ∀n. r.RP r.R0 n = n
   
   [plus_zero_right]  Theorem
      
      ⊢ ∀r. is_ring r ⇒ ∀n. r.RP n r.R0 = n
   
   [ring_11]  Theorem
      
      ⊢ ∀a0 a1 a2 a3 a4 a0' a1' a2' a3' a4'.
          ring a0 a1 a2 a3 a4 = ring a0' a1' a2' a3' a4' ⇔
          a0 = a0' ∧ a1 = a1' ∧ a2 = a2' ∧ a3 = a3' ∧ a4 = a4'
   
   [ring_Axiom]  Theorem
      
      ⊢ ∀f. ∃fn. ∀a0 a1 a2 a3 a4.
          fn (ring a0 a1 a2 a3 a4) = f a0 a1 a2 a3 a4
   
   [ring_accessors]  Theorem
      
      ⊢ (∀a a0 f f0 f1. (ring a a0 f f0 f1).R0 = a) ∧
        (∀a a0 f f0 f1. (ring a a0 f f0 f1).R1 = a0) ∧
        (∀a a0 f f0 f1. (ring a a0 f f0 f1).RP = f) ∧
        (∀a a0 f f0 f1. (ring a a0 f f0 f1).RM = f0) ∧
        ∀a a0 f f0 f1. (ring a a0 f f0 f1).RN = f1
   
   [ring_accfupds]  Theorem
      
      ⊢ (∀r f. (r with R1 updated_by f).R0 = r.R0) ∧
        (∀r f. (r with RP updated_by f).R0 = r.R0) ∧
        (∀r f. (r with RM updated_by f).R0 = r.R0) ∧
        (∀r f. (r with RN updated_by f).R0 = r.R0) ∧
        (∀r f. (r with R0 updated_by f).R1 = r.R1) ∧
        (∀r f. (r with RP updated_by f).R1 = r.R1) ∧
        (∀r f. (r with RM updated_by f).R1 = r.R1) ∧
        (∀r f. (r with RN updated_by f).R1 = r.R1) ∧
        (∀r f. (r with R0 updated_by f).RP = r.RP) ∧
        (∀r f. (r with R1 updated_by f).RP = r.RP) ∧
        (∀r f. (r with RM updated_by f).RP = r.RP) ∧
        (∀r f. (r with RN updated_by f).RP = r.RP) ∧
        (∀r f. (r with R0 updated_by f).RM = r.RM) ∧
        (∀r f. (r with R1 updated_by f).RM = r.RM) ∧
        (∀r f. (r with RP updated_by f).RM = r.RM) ∧
        (∀r f. (r with RN updated_by f).RM = r.RM) ∧
        (∀r f. (r with R0 updated_by f).RN = r.RN) ∧
        (∀r f. (r with R1 updated_by f).RN = r.RN) ∧
        (∀r f. (r with RP updated_by f).RN = r.RN) ∧
        (∀r f. (r with RM updated_by f).RN = r.RN) ∧
        (∀r f. (r with R0 updated_by f).R0 = f r.R0) ∧
        (∀r f. (r with R1 updated_by f).R1 = f r.R1) ∧
        (∀r f. (r with RP updated_by f).RP = f r.RP) ∧
        (∀r f. (r with RM updated_by f).RM = f r.RM) ∧
        ∀r f. (r with RN updated_by f).RN = f r.RN
   
   [ring_case_cong]  Theorem
      
      ⊢ ∀M M' f.
          M = M' ∧
          (∀a0 a1 a2 a3 a4.
             M' = ring a0 a1 a2 a3 a4 ⇒
             f a0 a1 a2 a3 a4 = f' a0 a1 a2 a3 a4) ⇒
          ring_CASE M f = ring_CASE M' f'
   
   [ring_case_eq]  Theorem
      
      ⊢ ring_CASE x f = v ⇔
        ∃a a0 f' f0 f1. x = ring a a0 f' f0 f1 ∧ f a a0 f' f0 f1 = v
   
   [ring_component_equality]  Theorem
      
      ⊢ ∀r1 r2.
          r1 = r2 ⇔
          r1.R0 = r2.R0 ∧ r1.R1 = r2.R1 ∧ r1.RP = r2.RP ∧ r1.RM = r2.RM ∧
          r1.RN = r2.RN
   
   [ring_fn_updates]  Theorem
      
      ⊢ (∀f2 a a0 f f0 f1.
           ring a a0 f f0 f1 with R0 updated_by f2 = ring (f2 a) a0 f f0 f1) ∧
        (∀f2 a a0 f f0 f1.
           ring a a0 f f0 f1 with R1 updated_by f2 = ring a (f2 a0) f f0 f1) ∧
        (∀f2 a a0 f f0 f1.
           ring a a0 f f0 f1 with RP updated_by f2 = ring a a0 (f2 f) f0 f1) ∧
        (∀f2 a a0 f f0 f1.
           ring a a0 f f0 f1 with RM updated_by f2 = ring a a0 f (f2 f0) f1) ∧
        ∀f2 a a0 f f0 f1.
          ring a a0 f f0 f1 with RN updated_by f2 = ring a a0 f f0 (f2 f1)
   
   [ring_fupdcanon]  Theorem
      
      ⊢ (∀r g f.
           r with <|R1 updated_by f; R0 updated_by g|> =
           r with <|R0 updated_by g; R1 updated_by f|>) ∧
        (∀r g f.
           r with <|RP updated_by f; R0 updated_by g|> =
           r with <|R0 updated_by g; RP updated_by f|>) ∧
        (∀r g f.
           r with <|RP updated_by f; R1 updated_by g|> =
           r with <|R1 updated_by g; RP updated_by f|>) ∧
        (∀r g f.
           r with <|RM updated_by f; R0 updated_by g|> =
           r with <|R0 updated_by g; RM updated_by f|>) ∧
        (∀r g f.
           r with <|RM updated_by f; R1 updated_by g|> =
           r with <|R1 updated_by g; RM updated_by f|>) ∧
        (∀r g f.
           r with <|RM updated_by f; RP updated_by g|> =
           r with <|RP updated_by g; RM updated_by f|>) ∧
        (∀r g f.
           r with <|RN updated_by f; R0 updated_by g|> =
           r with <|R0 updated_by g; RN updated_by f|>) ∧
        (∀r g f.
           r with <|RN updated_by f; R1 updated_by g|> =
           r with <|R1 updated_by g; RN updated_by f|>) ∧
        (∀r g f.
           r with <|RN updated_by f; RP updated_by g|> =
           r with <|RP updated_by g; RN updated_by f|>) ∧
        ∀r g f.
          r with <|RN updated_by f; RM updated_by g|> =
          r with <|RM updated_by g; RN updated_by f|>
   
   [ring_fupdcanon_comp]  Theorem
      
      ⊢ ((∀g f. R1_fupd f ∘ R0_fupd g = R0_fupd g ∘ R1_fupd f) ∧
         ∀h g f. R1_fupd f ∘ R0_fupd g ∘ h = R0_fupd g ∘ R1_fupd f ∘ h) ∧
        ((∀g f. RP_fupd f ∘ R0_fupd g = R0_fupd g ∘ RP_fupd f) ∧
         ∀h g f. RP_fupd f ∘ R0_fupd g ∘ h = R0_fupd g ∘ RP_fupd f ∘ h) ∧
        ((∀g f. RP_fupd f ∘ R1_fupd g = R1_fupd g ∘ RP_fupd f) ∧
         ∀h g f. RP_fupd f ∘ R1_fupd g ∘ h = R1_fupd g ∘ RP_fupd f ∘ h) ∧
        ((∀g f. RM_fupd f ∘ R0_fupd g = R0_fupd g ∘ RM_fupd f) ∧
         ∀h g f. RM_fupd f ∘ R0_fupd g ∘ h = R0_fupd g ∘ RM_fupd f ∘ h) ∧
        ((∀g f. RM_fupd f ∘ R1_fupd g = R1_fupd g ∘ RM_fupd f) ∧
         ∀h g f. RM_fupd f ∘ R1_fupd g ∘ h = R1_fupd g ∘ RM_fupd f ∘ h) ∧
        ((∀g f. RM_fupd f ∘ RP_fupd g = RP_fupd g ∘ RM_fupd f) ∧
         ∀h g f. RM_fupd f ∘ RP_fupd g ∘ h = RP_fupd g ∘ RM_fupd f ∘ h) ∧
        ((∀g f. RN_fupd f ∘ R0_fupd g = R0_fupd g ∘ RN_fupd f) ∧
         ∀h g f. RN_fupd f ∘ R0_fupd g ∘ h = R0_fupd g ∘ RN_fupd f ∘ h) ∧
        ((∀g f. RN_fupd f ∘ R1_fupd g = R1_fupd g ∘ RN_fupd f) ∧
         ∀h g f. RN_fupd f ∘ R1_fupd g ∘ h = R1_fupd g ∘ RN_fupd f ∘ h) ∧
        ((∀g f. RN_fupd f ∘ RP_fupd g = RP_fupd g ∘ RN_fupd f) ∧
         ∀h g f. RN_fupd f ∘ RP_fupd g ∘ h = RP_fupd g ∘ RN_fupd f ∘ h) ∧
        (∀g f. RN_fupd f ∘ RM_fupd g = RM_fupd g ∘ RN_fupd f) ∧
        ∀h g f. RN_fupd f ∘ RM_fupd g ∘ h = RM_fupd g ∘ RN_fupd f ∘ h
   
   [ring_fupdfupds]  Theorem
      
      ⊢ (∀r g f.
           r with <|R0 updated_by f; R0 updated_by g|> =
           r with R0 updated_by f ∘ g) ∧
        (∀r g f.
           r with <|R1 updated_by f; R1 updated_by g|> =
           r with R1 updated_by f ∘ g) ∧
        (∀r g f.
           r with <|RP updated_by f; RP updated_by g|> =
           r with RP updated_by f ∘ g) ∧
        (∀r g f.
           r with <|RM updated_by f; RM updated_by g|> =
           r with RM updated_by f ∘ g) ∧
        ∀r g f.
          r with <|RN updated_by f; RN updated_by g|> =
          r with RN updated_by f ∘ g
   
   [ring_fupdfupds_comp]  Theorem
      
      ⊢ ((∀g f. R0_fupd f ∘ R0_fupd g = R0_fupd (f ∘ g)) ∧
         ∀h g f. R0_fupd f ∘ R0_fupd g ∘ h = R0_fupd (f ∘ g) ∘ h) ∧
        ((∀g f. R1_fupd f ∘ R1_fupd g = R1_fupd (f ∘ g)) ∧
         ∀h g f. R1_fupd f ∘ R1_fupd g ∘ h = R1_fupd (f ∘ g) ∘ h) ∧
        ((∀g f. RP_fupd f ∘ RP_fupd g = RP_fupd (f ∘ g)) ∧
         ∀h g f. RP_fupd f ∘ RP_fupd g ∘ h = RP_fupd (f ∘ g) ∘ h) ∧
        ((∀g f. RM_fupd f ∘ RM_fupd g = RM_fupd (f ∘ g)) ∧
         ∀h g f. RM_fupd f ∘ RM_fupd g ∘ h = RM_fupd (f ∘ g) ∘ h) ∧
        (∀g f. RN_fupd f ∘ RN_fupd g = RN_fupd (f ∘ g)) ∧
        ∀h g f. RN_fupd f ∘ RN_fupd g ∘ h = RN_fupd (f ∘ g) ∘ h
   
   [ring_induction]  Theorem
      
      ⊢ ∀P. (∀a a0 f f0 f1. P (ring a a0 f f0 f1)) ⇒ ∀r. P r
   
   [ring_is_semi_ring]  Theorem
      
      ⊢ ∀r. is_ring r ⇒ is_semi_ring (semi_ring_of r)
   
   [ring_literal_11]  Theorem
      
      ⊢ ∀a01 a1 f11 f01 f1 a02 a2 f12 f02 f2.
          <|R0 := a01; R1 := a1; RP := f11; RM := f01; RN := f1|> =
          <|R0 := a02; R1 := a2; RP := f12; RM := f02; RN := f2|> ⇔
          a01 = a02 ∧ a1 = a2 ∧ f11 = f12 ∧ f01 = f02 ∧ f1 = f2
   
   [ring_literal_nchotomy]  Theorem
      
      ⊢ ∀r. ∃a0 a f1 f0 f.
          r = <|R0 := a0; R1 := a; RP := f1; RM := f0; RN := f|>
   
   [ring_nchotomy]  Theorem
      
      ⊢ ∀rr. ∃a a0 f f0 f1. rr = ring a a0 f f0 f1
   
   [ring_updates_eq_literal]  Theorem
      
      ⊢ ∀r a0 a f1 f0 f.
          r with <|R0 := a0; R1 := a; RP := f1; RM := f0; RN := f|> =
          <|R0 := a0; R1 := a; RP := f1; RM := f0; RN := f|>
   
   
*)
end


Source File Identifier index Theory binding index

HOL 4, Kananaskis-14