Structure errorMonadTheory

signature errorMonadTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val bind_def : thm
    val choice_def : thm
    val error_TY_DEF : thm
    val error_case_def : thm
    val error_size_def : thm
    val guard_def : thm
    val try_def : thm
  
  (*  Theorems  *)
    val EXISTS_ERROR : thm
    val FORALL_ERROR : thm
    val bind_EQ_error : thm
    val bind_EQ_return : thm
    val bind_return : thm
    val datatype_error : thm
    val error_11 : thm
    val error_Axiom : thm
    val error_case_cong : thm
    val error_case_eq : thm
    val error_distinct : thm
    val error_induction : thm
    val error_nchotomy : thm
(*
   [hol] Parent theory of "errorMonad"
   
   [bind_def]  Definition
      
      ⊢ (∀v f. bind (return v) f = f v) ∧ ∀e f. bind (error e) f = error e
   
   [choice_def]  Definition
      
      ⊢ (∀v m. choice (return v) m = return v) ∧
        ∀e m. choice (error e) m = m
   
   [error_TY_DEF]  Definition
      
      ⊢ ∃rep.
          TYPE_DEFINITION
            (λa0.
                 ∀ $var$('error').
                   (∀a0.
                      (∃a. a0 =
                           (λa.
                                ind_type$CONSTR 0 (a,ARB)
                                  (λn. ind_type$BOTTOM)) a) ∨
                      (∃a. a0 =
                           (λa.
                                ind_type$CONSTR (SUC 0) (ARB,a)
                                  (λn. ind_type$BOTTOM)) a) ⇒
                      $var$('error') a0) ⇒
                   $var$('error') a0) rep
   
   [error_case_def]  Definition
      
      ⊢ (∀a f f1. error_CASE (return a) f f1 = f a) ∧
        ∀a f f1. error_CASE (error a) f f1 = f1 a
   
   [error_size_def]  Definition
      
      ⊢ (∀f f1 a. error_size f f1 (return a) = 1 + f a) ∧
        ∀f f1 a. error_size f f1 (error a) = 1 + f1 a
   
   [guard_def]  Definition
      
      ⊢ ∀e b. guard e b = if b then return () else error e
   
   [try_def]  Definition
      
      ⊢ (∀v f. try (return v) f = return v) ∧ ∀e f. try (error e) f = f e
   
   [EXISTS_ERROR]  Theorem
      
      ⊢ (∃e. P e) ⇔ (∃a. P (return a)) ∨ ∃e. P (error e)
   
   [FORALL_ERROR]  Theorem
      
      ⊢ (∀e. P e) ⇔ (∀a. P (return a)) ∧ ∀e. P (error e)
   
   [bind_EQ_error]  Theorem
      
      ⊢ bind m f = error e ⇔ m = error e ∨ ∃u. m = return u ∧ f u = error e
   
   [bind_EQ_return]  Theorem
      
      ⊢ bind m f = return v ⇔ ∃u. m = return u ∧ f u = return v
   
   [bind_return]  Theorem
      
      ⊢ bind m return = m
   
   [datatype_error]  Theorem
      
      ⊢ DATATYPE (error return error)
   
   [error_11]  Theorem
      
      ⊢ (∀a a'. return a = return a' ⇔ a = a') ∧
        ∀a a'. error a = error a' ⇔ a = a'
   
   [error_Axiom]  Theorem
      
      ⊢ ∀f0 f1. ∃fn. (∀a. fn (return a) = f0 a) ∧ ∀a. fn (error a) = f1 a
   
   [error_case_cong]  Theorem
      
      ⊢ ∀M M' f f1.
          M = M' ∧ (∀a. M' = return a ⇒ f a = f' a) ∧
          (∀a. M' = error a ⇒ f1 a = f1' a) ⇒
          error_CASE M f f1 = error_CASE M' f' f1'
   
   [error_case_eq]  Theorem
      
      ⊢ error_CASE x f f1 = v ⇔
        (∃a. x = return a ∧ f a = v) ∨ ∃e. x = error e ∧ f1 e = v
   
   [error_distinct]  Theorem
      
      ⊢ ∀a' a. return a ≠ error a'
   
   [error_induction]  Theorem
      
      ⊢ ∀P. (∀a. P (return a)) ∧ (∀e. P (error e)) ⇒ ∀e. P e
   
   [error_nchotomy]  Theorem
      
      ⊢ ∀ee. (∃a. ee = return a) ∨ ∃e. ee = error e
   
   
*)
end

HOL 4, Trindemossen-2