Structure basis_emitTheory

signature basis_emitTheory =
sig
  type thm = Thm.thm
  
  (*  Axioms  *)
    val EXPi : thm
    val MULi : thm
    val SUMi : thm
    val dimindexi : thm
  
  (*  Definitions  *)
    val FCPi_def_primitive : thm
    val IS_EMPTY_def : thm
    val i2w_itself_def_primitive : thm
    val mk_fcp_def : thm
    val neg_int_of_num_def : thm
  
  (*  Theorems  *)
    val FCPi_def : thm
    val FCPi_ind : thm
    val IS_EMPTY_REWRITE : thm
    val i2w_itself_def : thm
    val i2w_itself_ind : thm
(*
   [finite_map] Parent theory of "basis_emit"
   
   [integer_word] Parent theory of "basis_emit"
   
   [pre_emit] Parent theory of "basis_emit"
   
   [EXPi]  Axiom
      
      [oracles: ] [axioms: EXPi] []
      ⊢ EXPi (ITSELF a,ITSELF b) = ITSELF (a ** b)
   
   [MULi]  Axiom
      
      [oracles: ] [axioms: MULi] []
      ⊢ MULi (ITSELF a,ITSELF b) = ITSELF (a * b)
   
   [SUMi]  Axiom
      
      [oracles: ] [axioms: SUMi] []
      ⊢ SUMi (ITSELF a,ITSELF b) = ITSELF (a + b)
   
   [dimindexi]  Axiom
      
      [oracles: ] [axioms: dimindexi] [] ⊢ dimindex (ITSELF a) = a
   
   [FCPi_def_primitive]  Definition
      
      ⊢ FCPi = WFREC (@R. WF R) (λFCPi a. case a of (v,v1) => I ($FCP v))
   
   [IS_EMPTY_def]  Definition
      
      ⊢ ∀s. IS_EMPTY s ⇔ if s = ∅ then T else F
   
   [i2w_itself_def_primitive]  Definition
      
      ⊢ i2w_itself =
        WFREC (@R. WF R) (λi2w_itself a. case a of (v,v1) => I (i2w v))
   
   [mk_fcp_def]  Definition
      
      ⊢ mk_fcp = FCPi
   
   [neg_int_of_num_def]  Definition
      
      ⊢ ∀n. neg_int_of_num n = -int_of_num (n + 1)
   
   [FCPi_def]  Theorem
      
      ⊢ FCPi (f,(:β)) = $FCP f
   
   [FCPi_ind]  Theorem
      
      ⊢ ∀P. (∀f. P (f,(:β))) ⇒ ∀v v1. P (v,v1)
   
   [IS_EMPTY_REWRITE]  Theorem
      
      ⊢ (s = ∅ ⇔ IS_EMPTY s) ∧ (∅ = s ⇔ IS_EMPTY s)
   
   [i2w_itself_def]  Theorem
      
      ⊢ i2w_itself (i,(:α)) = i2w i
   
   [i2w_itself_ind]  Theorem
      
      ⊢ ∀P. (∀i. P (i,(:α))) ⇒ ∀v v1. P (v,v1)
   
   
*)
end

HOL 4, Trindemossen-2