Structure optionTheory

signature optionTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val NONE_DEF : thm
    val OPTION_ALL_def : thm
    val OPTION_APPLY_def : thm
    val OPTION_BIND_def : thm
    val OPTION_CHOICE_def : thm
    val OPTION_GUARD_def : thm
    val OPTION_IGNORE_BIND_def : thm
    val OPTION_MAP2_DEF : thm
    val OPTION_MAP_DEF : thm
    val OPTION_MCOMP_def : thm
    val OPTREL_def : thm
    val SOME_DEF : thm
    val option_REP_ABS_DEF : thm
    val option_TY_DEF : thm
    val option_case_def : thm
    val some_def : thm
  
  (*  Theorems  *)
    val EXISTS_OPTION : thm
    val FORALL_OPTION : thm
    val IF_EQUALS_OPTION : thm
    val IF_NONE_EQUALS_OPTION : thm
    val IS_NONE_DEF : thm
    val IS_NONE_EQ_NONE : thm
    val IS_SOME_BIND : thm
    val IS_SOME_DEF : thm
    val IS_SOME_EXISTS : thm
    val IS_SOME_MAP : thm
    val NOT_IS_SOME_EQ_NONE : thm
    val NOT_NONE_SOME : thm
    val NOT_SOME_NONE : thm
    val OPTION_ALL_CONG : thm
    val OPTION_ALL_MONO : thm
    val OPTION_APPLY_MAP2 : thm
    val OPTION_APPLY_o : thm
    val OPTION_BIND_EQUALS_OPTION : thm
    val OPTION_BIND_SOME : thm
    val OPTION_BIND_cong : thm
    val OPTION_CHOICE_EQ_NONE : thm
    val OPTION_CHOICE_NONE : thm
    val OPTION_GUARD_COND : thm
    val OPTION_GUARD_EQ_THM : thm
    val OPTION_IGNORE_BIND_EQUALS_OPTION : thm
    val OPTION_IGNORE_BIND_cong : thm
    val OPTION_IGNORE_BIND_thm : thm
    val OPTION_JOIN_DEF : thm
    val OPTION_JOIN_EQ_SOME : thm
    val OPTION_MAP2_NONE : thm
    val OPTION_MAP2_SOME : thm
    val OPTION_MAP2_THM : thm
    val OPTION_MAP2_cong : thm
    val OPTION_MAP_CASE : thm
    val OPTION_MAP_COMPOSE : thm
    val OPTION_MAP_CONG : thm
    val OPTION_MAP_EQ_NONE : thm
    val OPTION_MAP_EQ_NONE_both_ways : thm
    val OPTION_MAP_EQ_SOME : thm
    val OPTION_MAP_id : thm
    val OPTION_MCOMP_ASSOC : thm
    val OPTION_MCOMP_ID : thm
    val OPTREL_CONG : thm
    val OPTREL_MONO : thm
    val OPTREL_NONE : thm
    val OPTREL_O : thm
    val OPTREL_SOME : thm
    val OPTREL_THM : thm
    val OPTREL_eq : thm
    val OPTREL_refl : thm
    val SOME_11 : thm
    val SOME_APPLY_PERMUTE : thm
    val SOME_SOME_APPLY : thm
    val THE_DEF : thm
    val datatype_option : thm
    val option_Axiom : thm
    val option_CASES : thm
    val option_CLAUSES : thm
    val option_Induct : thm
    val option_case_ID : thm
    val option_case_SOME_ID : thm
    val option_case_compute : thm
    val option_case_cong : thm
    val option_case_eq : thm
    val option_case_eq' : thm
    val option_case_lazily : thm
    val option_imp_elim : thm
    val option_induction : thm
    val option_nchotomy : thm
    val some_EQ : thm
    val some_F : thm
    val some_elim : thm
    val some_intro : thm
  
  val option_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [one] Parent theory of "option"
   
   [sum] Parent theory of "option"
   
   [NONE_DEF]  Definition
      
      ⊢ NONE = option_ABS (INR ())
   
   [OPTION_ALL_def]  Definition
      
      ⊢ (∀P. OPTION_ALL P NONE ⇔ T) ∧ ∀P x. OPTION_ALL P (SOME x) ⇔ P x
   
   [OPTION_APPLY_def]  Definition
      
      ⊢ (∀x. NONE <*> x = NONE) ∧ ∀f x. SOME f <*> x = OPTION_MAP f x
   
   [OPTION_BIND_def]  Definition
      
      ⊢ (∀f. OPTION_BIND NONE f = NONE) ∧
        ∀x f. OPTION_BIND (SOME x) f = f x
   
   [OPTION_CHOICE_def]  Definition
      
      ⊢ (∀m2. OPTION_CHOICE NONE m2 = m2) ∧
        ∀x m2. OPTION_CHOICE (SOME x) m2 = SOME x
   
   [OPTION_GUARD_def]  Definition
      
      ⊢ OPTION_GUARD T = SOME () ∧ OPTION_GUARD F = NONE
   
   [OPTION_IGNORE_BIND_def]  Definition
      
      ⊢ ∀m1 m2. OPTION_IGNORE_BIND m1 m2 = OPTION_BIND m1 (K m2)
   
   [OPTION_MAP2_DEF]  Definition
      
      ⊢ ∀f x y.
          OPTION_MAP2 f x y =
          if IS_SOME x ∧ IS_SOME y then SOME (f (THE x) (THE y)) else NONE
   
   [OPTION_MAP_DEF]  Definition
      
      ⊢ (∀f x. OPTION_MAP f (SOME x) = SOME (f x)) ∧
        ∀f. OPTION_MAP f NONE = NONE
   
   [OPTION_MCOMP_def]  Definition
      
      ⊢ ∀g f m. OPTION_MCOMP g f m = OPTION_BIND (f m) g
   
   [OPTREL_def]  Definition
      
      ⊢ ∀R x y.
          OPTREL R x y ⇔
          x = NONE ∧ y = NONE ∨ ∃x0 y0. x = SOME x0 ∧ y = SOME y0 ∧ R x0 y0
   
   [SOME_DEF]  Definition
      
      ⊢ ∀x. SOME x = option_ABS (INL x)
   
   [option_REP_ABS_DEF]  Definition
      
      ⊢ (∀a. option_ABS (option_REP a) = a) ∧
        ∀r. (λx. T) r ⇔ option_REP (option_ABS r) = r
   
   [option_TY_DEF]  Definition
      
      ⊢ ∃rep. TYPE_DEFINITION (λx. T) rep
   
   [option_case_def]  Definition
      
      ⊢ (∀v f. option_CASE NONE v f = v) ∧
        ∀x v f. option_CASE (SOME x) v f = f x
   
   [some_def]  Definition
      
      ⊢ ∀P. $some P = if ∃x. P x then SOME (@x. P x) else NONE
   
   [EXISTS_OPTION]  Theorem
      
      ⊢ (∃opt. P opt) ⇔ P NONE ∨ ∃x. P (SOME x)
   
   [FORALL_OPTION]  Theorem
      
      ⊢ (∀opt. P opt) ⇔ P NONE ∧ ∀x. P (SOME x)
   
   [IF_EQUALS_OPTION]  Theorem
      
      ⊢ ((if P then SOME x else NONE) = NONE ⇔ ¬P) ∧
        ((if P then NONE else SOME x) = NONE ⇔ P) ∧
        ((if P then SOME x else NONE) = SOME y ⇔ P ∧ x = y) ∧
        ((if P then NONE else SOME x) = SOME y ⇔ ¬P ∧ x = y)
   
   [IF_NONE_EQUALS_OPTION]  Theorem
      
      ⊢ ((if P then X else NONE) = NONE ⇔ P ⇒ IS_NONE X) ∧
        ((if P then NONE else X) = NONE ⇔ IS_SOME X ⇒ P) ∧
        ((if P then X else NONE) = SOME x ⇔ P ∧ X = SOME x) ∧
        ((if P then NONE else X) = SOME x ⇔ ¬P ∧ X = SOME x)
   
   [IS_NONE_DEF]  Theorem
      
      ⊢ (∀x. IS_NONE (SOME x) ⇔ F) ∧ (IS_NONE NONE ⇔ T)
   
   [IS_NONE_EQ_NONE]  Theorem
      
      ⊢ ∀x. IS_NONE x ⇔ x = NONE
   
   [IS_SOME_BIND]  Theorem
      
      ⊢ IS_SOME (OPTION_BIND x g) ⇒ IS_SOME x
   
   [IS_SOME_DEF]  Theorem
      
      ⊢ (∀x. IS_SOME (SOME x) ⇔ T) ∧ (IS_SOME NONE ⇔ F)
   
   [IS_SOME_EXISTS]  Theorem
      
      ⊢ ∀opt. IS_SOME opt ⇔ ∃x. opt = SOME x
   
   [IS_SOME_MAP]  Theorem
      
      ⊢ IS_SOME (OPTION_MAP f x) ⇔ IS_SOME x
   
   [NOT_IS_SOME_EQ_NONE]  Theorem
      
      ⊢ ∀x. ¬IS_SOME x ⇔ x = NONE
   
   [NOT_NONE_SOME]  Theorem
      
      ⊢ ∀x. NONE ≠ SOME x
   
   [NOT_SOME_NONE]  Theorem
      
      ⊢ ∀x. SOME x ≠ NONE
   
   [OPTION_ALL_CONG]  Theorem
      
      ⊢ ∀opt opt' P P'.
          opt = opt' ∧ (∀x. opt' = SOME x ⇒ (P x ⇔ P' x)) ⇒
          (OPTION_ALL P opt ⇔ OPTION_ALL P' opt')
   
   [OPTION_ALL_MONO]  Theorem
      
      ⊢ (∀x. P x ⇒ P' x) ⇒ OPTION_ALL P opt ⇒ OPTION_ALL P' opt
   
   [OPTION_APPLY_MAP2]  Theorem
      
      ⊢ OPTION_MAP f x <*> y = OPTION_MAP2 f x y
   
   [OPTION_APPLY_o]  Theorem
      
      ⊢ SOME $o <*> f <*> g <*> x = f <*> (g <*> x)
   
   [OPTION_BIND_EQUALS_OPTION]  Theorem
      
      ⊢ (OPTION_BIND p f = NONE ⇔ p = NONE ∨ ∃x. p = SOME x ∧ f x = NONE) ∧
        (OPTION_BIND p f = SOME y ⇔ ∃x. p = SOME x ∧ f x = SOME y)
   
   [OPTION_BIND_SOME]  Theorem
      
      ⊢ ∀opt. OPTION_BIND opt SOME = opt
   
   [OPTION_BIND_cong]  Theorem
      
      ⊢ ∀o1 o2 f1 f2.
          o1 = o2 ∧ (∀x. o2 = SOME x ⇒ f1 x = f2 x) ⇒
          OPTION_BIND o1 f1 = OPTION_BIND o2 f2
   
   [OPTION_CHOICE_EQ_NONE]  Theorem
      
      ⊢ OPTION_CHOICE m1 m2 = NONE ⇔ m1 = NONE ∧ m2 = NONE
   
   [OPTION_CHOICE_NONE]  Theorem
      
      ⊢ OPTION_CHOICE m1 NONE = m1
   
   [OPTION_GUARD_COND]  Theorem
      
      ⊢ OPTION_GUARD b = if b then SOME () else NONE
   
   [OPTION_GUARD_EQ_THM]  Theorem
      
      ⊢ (OPTION_GUARD b = SOME () ⇔ b) ∧ (OPTION_GUARD b = NONE ⇔ ¬b)
   
   [OPTION_IGNORE_BIND_EQUALS_OPTION]  Theorem
      
      ⊢ (OPTION_IGNORE_BIND m1 m2 = NONE ⇔ m1 = NONE ∨ m2 = NONE) ∧
        (OPTION_IGNORE_BIND m1 m2 = SOME y ⇔ ∃x. m1 = SOME x ∧ m2 = SOME y)
   
   [OPTION_IGNORE_BIND_cong]  Theorem
      
      ⊢ o1 = o2 ∧ (∀v. o2 = SOME v ⇒ p1 = p2) ⇒
        OPTION_IGNORE_BIND o1 p1 = OPTION_IGNORE_BIND o2 p2
   
   [OPTION_IGNORE_BIND_thm]  Theorem
      
      ⊢ OPTION_IGNORE_BIND NONE m = NONE ∧
        OPTION_IGNORE_BIND (SOME v) m = m
   
   [OPTION_JOIN_DEF]  Theorem
      
      ⊢ OPTION_JOIN NONE = NONE ∧ ∀x. OPTION_JOIN (SOME x) = x
   
   [OPTION_JOIN_EQ_SOME]  Theorem
      
      ⊢ ∀x y. OPTION_JOIN x = SOME y ⇔ x = SOME (SOME y)
   
   [OPTION_MAP2_NONE]  Theorem
      
      ⊢ OPTION_MAP2 f o1 o2 = NONE ⇔ o1 = NONE ∨ o2 = NONE
   
   [OPTION_MAP2_SOME]  Theorem
      
      ⊢ OPTION_MAP2 f o1 o2 = SOME v ⇔
        ∃x1 x2. o1 = SOME x1 ∧ o2 = SOME x2 ∧ v = f x1 x2
   
   [OPTION_MAP2_THM]  Theorem
      
      ⊢ OPTION_MAP2 f (SOME x) (SOME y) = SOME (f x y) ∧
        OPTION_MAP2 f (SOME x) NONE = NONE ∧
        OPTION_MAP2 f NONE (SOME y) = NONE ∧ OPTION_MAP2 f NONE NONE = NONE
   
   [OPTION_MAP2_cong]  Theorem
      
      ⊢ ∀x1 x2 y1 y2 f1 f2.
          x1 = x2 ∧ y1 = y2 ∧
          (∀x y. x2 = SOME x ∧ y2 = SOME y ⇒ f1 x y = f2 x y) ⇒
          OPTION_MAP2 f1 x1 y1 = OPTION_MAP2 f2 x2 y2
   
   [OPTION_MAP_CASE]  Theorem
      
      ⊢ OPTION_MAP f x = option_CASE x NONE (SOME ∘ f)
   
   [OPTION_MAP_COMPOSE]  Theorem
      
      ⊢ OPTION_MAP f (OPTION_MAP g x) = OPTION_MAP (f ∘ g) x
   
   [OPTION_MAP_CONG]  Theorem
      
      ⊢ ∀opt1 opt2 f1 f2.
          opt1 = opt2 ∧ (∀x. opt2 = SOME x ⇒ f1 x = f2 x) ⇒
          OPTION_MAP f1 opt1 = OPTION_MAP f2 opt2
   
   [OPTION_MAP_EQ_NONE]  Theorem
      
      ⊢ ∀f x. OPTION_MAP f x = NONE ⇔ x = NONE
   
   [OPTION_MAP_EQ_NONE_both_ways]  Theorem
      
      ⊢ (OPTION_MAP f x = NONE ⇔ x = NONE) ∧
        (NONE = OPTION_MAP f x ⇔ x = NONE)
   
   [OPTION_MAP_EQ_SOME]  Theorem
      
      ⊢ ∀f x y. OPTION_MAP f x = SOME y ⇔ ∃z. x = SOME z ∧ y = f z
   
   [OPTION_MAP_id]  Theorem
      
      ⊢ OPTION_MAP I x = x ∧ OPTION_MAP (λx. x) x = x
   
   [OPTION_MCOMP_ASSOC]  Theorem
      
      ⊢ OPTION_MCOMP f (OPTION_MCOMP g h) =
        OPTION_MCOMP (OPTION_MCOMP f g) h
   
   [OPTION_MCOMP_ID]  Theorem
      
      ⊢ OPTION_MCOMP g SOME = g ∧ OPTION_MCOMP SOME f = f
   
   [OPTREL_CONG]  Theorem
      
      ⊢ ∀opt1 opt2 opt1' opt2' R R'.
          opt1 = opt1' ∧ opt2 = opt2' ∧
          (∀x y. opt1' = SOME x ∧ opt2' = SOME y ⇒ (R x y ⇔ R' x y)) ⇒
          (OPTREL R opt1 opt2 ⇔ OPTREL R' opt1' opt2')
   
   [OPTREL_MONO]  Theorem
      
      ⊢ (∀x y. P x y ⇒ Q x y) ⇒ OPTREL P x y ⇒ OPTREL Q x y
   
   [OPTREL_NONE]  Theorem
      
      ⊢ (OPTREL R NONE y ⇔ y = NONE) ∧ (OPTREL R x NONE ⇔ x = NONE)
   
   [OPTREL_O]  Theorem
      
      ⊢ ∀R1 R2. OPTREL (R1 ∘ᵣ R2) = OPTREL R1 ∘ᵣ OPTREL R2
   
   [OPTREL_SOME]  Theorem
      
      ⊢ (∀R x y. OPTREL R (SOME x) y ⇔ ∃z. y = SOME z ∧ R x z) ∧
        ∀R x y. OPTREL R x (SOME y) ⇔ ∃z. x = SOME z ∧ R z y
   
   [OPTREL_THM]  Theorem
      
      ⊢ (OPTREL R (SOME x) NONE ⇔ F) ∧ (OPTREL R NONE (SOME y) ⇔ F) ∧
        (OPTREL R NONE NONE ⇔ T) ∧ (OPTREL R (SOME x) (SOME y) ⇔ R x y)
   
   [OPTREL_eq]  Theorem
      
      ⊢ OPTREL $= = $=
   
   [OPTREL_refl]  Theorem
      
      ⊢ (∀x. R x x) ⇒ ∀x. OPTREL R x x
   
   [SOME_11]  Theorem
      
      ⊢ ∀x y. SOME x = SOME y ⇔ x = y
   
   [SOME_APPLY_PERMUTE]  Theorem
      
      ⊢ f <*> SOME x = SOME (λf. f x) <*> f
   
   [SOME_SOME_APPLY]  Theorem
      
      ⊢ SOME f <*> SOME x = SOME (f x)
   
   [THE_DEF]  Theorem
      
      ⊢ ∀x. THE (SOME x) = x
   
   [datatype_option]  Theorem
      
      ⊢ DATATYPE (option NONE SOME)
   
   [option_Axiom]  Theorem
      
      ⊢ ∀e f. ∃fn. fn NONE = e ∧ ∀x. fn (SOME x) = f x
   
   [option_CASES]  Theorem
      
      ⊢ ∀opt. (∃x. opt = SOME x) ∨ opt = NONE
   
   [option_CLAUSES]  Theorem
      
      ⊢ (∀x y. SOME x = SOME y ⇔ x = y) ∧ (∀x. THE (SOME x) = x) ∧
        (∀x. NONE ≠ SOME x) ∧ (∀x. SOME x ≠ NONE) ∧
        (∀x. IS_SOME (SOME x) ⇔ T) ∧ (IS_SOME NONE ⇔ F) ∧
        (∀x. IS_NONE x ⇔ x = NONE) ∧ (∀x. ¬IS_SOME x ⇔ x = NONE) ∧
        (∀x. IS_SOME x ⇒ SOME (THE x) = x) ∧
        (∀x. option_CASE x NONE SOME = x) ∧
        (∀x. option_CASE x x SOME = x) ∧
        (∀x. IS_NONE x ⇒ option_CASE x e f = e) ∧
        (∀x. IS_SOME x ⇒ option_CASE x e f = f (THE x)) ∧
        (∀x. IS_SOME x ⇒ option_CASE x e SOME = x) ∧
        (∀v f. option_CASE NONE v f = v) ∧
        (∀x v f. option_CASE (SOME x) v f = f x) ∧
        (∀f x. OPTION_MAP f (SOME x) = SOME (f x)) ∧
        (∀f. OPTION_MAP f NONE = NONE) ∧ OPTION_JOIN NONE = NONE ∧
        ∀x. OPTION_JOIN (SOME x) = x
   
   [option_Induct]  Theorem
      
      ⊢ ∀P. (∀a. P (SOME a)) ∧ P NONE ⇒ ∀x. P x
   
   [option_case_ID]  Theorem
      
      ⊢ ∀x. option_CASE x NONE SOME = x
   
   [option_case_SOME_ID]  Theorem
      
      ⊢ ∀x. option_CASE x x SOME = x
   
   [option_case_compute]  Theorem
      
      ⊢ option_CASE x e f = if IS_SOME x then f (THE x) else e
   
   [option_case_cong]  Theorem
      
      ⊢ ∀M M' v f.
          M = M' ∧ (M' = NONE ⇒ v = v') ∧ (∀x. M' = SOME x ⇒ f x = f' x) ⇒
          option_CASE M v f = option_CASE M' v' f'
   
   [option_case_eq]  Theorem
      
      ⊢ option_CASE opt nc sc = v ⇔
        opt = NONE ∧ nc = v ∨ ∃x. opt = SOME x ∧ sc x = v
   
   [option_case_eq']  Theorem
      
      ⊢ option_CASE x v f = v' ⇔
        x = NONE ∧ v = v' ∨ ∃a. x = SOME a ∧ f a = v'
   
   [option_case_lazily]  Theorem
      
      ⊢ option_CASE NONE = (λv f. v) ∧ option_CASE (SOME x) = (λv f. f x)
   
   [option_imp_elim]  Theorem
      
      ⊢ option_CASE x v f ⇔ (x = NONE ⇒ v) ∧ ∀x'. x = SOME x' ⇒ f x'
   
   [option_induction]  Theorem
      
      ⊢ ∀P. P NONE ∧ (∀a. P (SOME a)) ⇒ ∀x. P x
   
   [option_nchotomy]  Theorem
      
      ⊢ ∀opt. opt = NONE ∨ ∃x. opt = SOME x
   
   [some_EQ]  Theorem
      
      ⊢ (some x. x = y) = SOME y ∧ (some x. y = x) = SOME y
   
   [some_F]  Theorem
      
      ⊢ (some x. F) = NONE
   
   [some_elim]  Theorem
      
      ⊢ Q ($some P) ⇒ (∃x. P x ∧ Q (SOME x)) ∨ (∀x. ¬P x) ∧ Q NONE
   
   [some_intro]  Theorem
      
      ⊢ (∀x. P x ⇒ Q (SOME x)) ∧ ((∀x. ¬P x) ⇒ Q NONE) ⇒ Q ($some P)
   
   
*)
end

HOL 4, Trindemossen-1