# Structure oneTheory

Source File Identifier index Theory binding index

```signature oneTheory =
sig
type thm = Thm.thm

(*  Definitions  *)
val one_DEF : thm
val one_TY_DEF : thm
val one_case_def : thm

(*  Theorems  *)
val EXISTS_ONE_FN : thm
val FORALL_ONE : thm
val FORALL_ONE_FN : thm
val one : thm
val one_Axiom : thm
val one_axiom : thm
val one_case_thm : thm
val one_induction : thm
val one_prim_rec : thm

val one_grammars : type_grammar.grammar * term_grammar.grammar
(*
[combin] Parent theory of "one"

[sat] Parent theory of "one"

[one_DEF]  Definition

⊢ () = @x. T

[one_TY_DEF]  Definition

⊢ ∃rep. TYPE_DEFINITION (λb. b) rep

[one_case_def]  Definition

⊢ ∀u x. one_CASE u x = x

[EXISTS_ONE_FN]  Theorem

⊢ (∃f. P f) ⇔ ∃f. P (λx u. f x)

[FORALL_ONE]  Theorem

⊢ (∀x. P x) ⇔ P ()

[FORALL_ONE_FN]  Theorem

⊢ (∀uf. P uf) ⇔ ∀a. P (λu. a)

[one]  Theorem

⊢ ∀v. v = ()

[one_Axiom]  Theorem

⊢ ∀e. ∃!fn. fn () = e

[one_axiom]  Theorem

⊢ ∀f g. f = g

[one_case_thm]  Theorem

⊢ ∀x. one_CASE () x = x

[one_induction]  Theorem

⊢ ∀P. P () ⇒ ∀x. P x

[one_prim_rec]  Theorem

⊢ ∀e. ∃fn. fn () = e

*)
end

```

Source File Identifier index Theory binding index

HOL 4, Trindemossen-1