# Structure basicSizeTheory

Source File Identifier index Theory binding index

```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

```

Source File Identifier index Theory binding index

HOL 4, Trindemossen-1