Structure markerTheory

signature markerTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val AC_DEF : thm
    val Abbrev_def : thm
    val Case_def : thm
    val Cong_def : thm
    val Exclude_def : thm
    val IfCases_def : thm
    val Req0_def : thm
    val ReqD_def : thm
    val label_def : thm
    val stmarker_def : thm
    val unint_def : thm
    val usingThm_def : thm
    val using_def : thm
  
  (*  Theorems  *)
    val Abbrev_CONG : thm
    val add_Case : thm
    val elim_Case : thm
    val move_left_conj : thm
    val move_left_disj : thm
    val move_right_conj : thm
    val move_right_disj : thm
  
  val marker_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [bool] Parent theory of "marker"
   
   [AC_DEF]  Definition
      
      ⊢ ∀b1 b2. AC b1 b2 ⇔ b1 ∧ b2
   
   [Abbrev_def]  Definition
      
      ⊢ ∀x. Abbrev x ⇔ x
   
   [Case_def]  Definition
      
      ⊢ ∀X. Case X ⇔ T
   
   [Cong_def]  Definition
      
      ⊢ ∀x. Cong x ⇔ x
   
   [Exclude_def]  Definition
      
      ⊢ ∀x. Exclude x ⇔ T
   
   [IfCases_def]  Definition
      
      ⊢ IfCases ⇔ T
   
   [Req0_def]  Definition
      
      ⊢ Req0 ⇔ T
   
   [ReqD_def]  Definition
      
      ⊢ ReqD ⇔ T
   
   [label_def]  Definition
      
      ⊢ ∀lab argument. (lab :- argument) ⇔ argument
   
   [stmarker_def]  Definition
      
      ⊢ ∀x. stmarker x = x
   
   [unint_def]  Definition
      
      ⊢ ∀x. unint x = x
   
   [usingThm_def]  Definition
      
      ⊢ ∀b. marker$usingThm b ⇔ b
   
   [using_def]  Definition
      
      ⊢ ∀x. marker$using x ⇔ T
   
   [Abbrev_CONG]  Theorem
      
      ⊢ r1 = r2 ⇒ (Abbrev (v = r1) ⇔ Abbrev (v = r2))
   
   [add_Case]  Theorem
      
      ⊢ ∀X. P ⇔ Case X ⇒ P
   
   [elim_Case]  Theorem
      
      ⊢ (Case X ∧ Y ⇔ Y) ∧ (Y ∧ Case X ⇔ Y) ∧ (Case X ⇒ Y ⇔ Y)
   
   [move_left_conj]  Theorem
      
      ⊢ ∀p q m.
          (p ∧ stmarker m ⇔ stmarker m ∧ p) ∧
          ((stmarker m ∧ p) ∧ q ⇔ stmarker m ∧ p ∧ q) ∧
          (p ∧ stmarker m ∧ q ⇔ stmarker m ∧ p ∧ q)
   
   [move_left_disj]  Theorem
      
      ⊢ ∀p q m.
          (p ∨ stmarker m ⇔ stmarker m ∨ p) ∧
          ((stmarker m ∨ p) ∨ q ⇔ stmarker m ∨ p ∨ q) ∧
          (p ∨ stmarker m ∨ q ⇔ stmarker m ∨ p ∨ q)
   
   [move_right_conj]  Theorem
      
      ⊢ ∀p q m.
          (stmarker m ∧ p ⇔ p ∧ stmarker m) ∧
          (p ∧ q ∧ stmarker m ⇔ (p ∧ q) ∧ stmarker m) ∧
          ((p ∧ stmarker m) ∧ q ⇔ (p ∧ q) ∧ stmarker m)
   
   [move_right_disj]  Theorem
      
      ⊢ ∀p q m.
          (stmarker m ∨ p ⇔ p ∨ stmarker m) ∧
          (p ∨ q ∨ stmarker m ⇔ (p ∨ q) ∨ stmarker m) ∧
          ((p ∨ stmarker m) ∨ q ⇔ (p ∨ q) ∨ stmarker m)
   
   
*)
end

HOL 4, Kananaskis-14