Structure basicSizeTheory

signature basicSizeTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val bool_size_def : thm
    val full_sum_size_def : thm
    val itself_size_def : thm
    val min_pair_size_def : thm
    val one_size_def : thm
    val option_size_def : thm
    val pair_size_def : thm
    val sum_size_def : thm
  
  (*  Theorems  *)
    val full_sum_size_thm : thm
  
  val basicSize_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [numeral] Parent theory of "basicSize"
   
   [option] Parent theory of "basicSize"
   
   [bool_size_def]  Definition
      
      ⊢ ∀b. bool_size b = 0
   
   [full_sum_size_def]  Definition
      
      ⊢ ∀f g sum. full_sum_size f g sum = 1 + sum_size f g sum
   
   [itself_size_def]  Definition
      
      ⊢ ∀x. itself_size x = 0
   
   [min_pair_size_def]  Definition
      
      ⊢ ∀f g x y. min_pair_size f g (x,y) = f x + g y
   
   [one_size_def]  Definition
      
      ⊢ ∀x. one_size x = 0
   
   [option_size_def]  Definition
      
      ⊢ (∀f. option_size f NONE = 0) ∧
        ∀f x. option_size f (SOME x) = 1 + f x
   
   [pair_size_def]  Definition
      
      ⊢ ∀f g x y. pair_size f g (x,y) = 1 + (f x + g y)
   
   [sum_size_def]  Definition
      
      ⊢ (∀f g x. sum_size f g (INL x) = f x) ∧
        ∀f g y. sum_size f g (INR y) = g y
   
   [full_sum_size_thm]  Theorem
      
      ⊢ full_sum_size f g (INL x) = 1 + f x ∧
        full_sum_size f g (INR y) = 1 + g y
   
   
*)
end

HOL 4, Trindemossen-1