non_type_theorems

EmitTeX.non_type_theorems : string -> (string * thm) list

A versions of theorems that attempts to filter out theorems created by Hol_datatype.

An invocation non_type_theorems thy, where thy is the name of a currently loaded theory segment, will return a list of the theorems stored in that theory. Axioms and definitions are excluded. Each theorem is paired with its name in the result.

Failure

Never fails. If thy is not the name of a currently loaded theory segment, the empty list is returned.

Example

> new_theory "example";
<<HOL message: Restarting theory "example">>
<<HOL warning: Theory.callhooks: Hook Parse.clear_consts_from_grammar failed on event NewTheory{oldseg = "example", newseg = "example"} with problem 
Exception raised at Term.dest_thy_const: not a const
>>
val it = (): unit
> val _ = Hol_datatype `example = First | Second`;
<<HOL message: Defined type: "example">>
> val example_def = Define
   `(example First = Second) /\ (example Second = First)`;
Definition has been stored under "example_def"
val example_def = ⊢ example First = Second ∧ example Second = First: thm
> save_thm("example_thm",
  METIS_PROVE [example_def, theorem "example_nchotomy"]
    ``!x. example (example x) = x``);
metis: r[+0+5]+1+0+0+0+6+2+1+0+1+1#
val it = ⊢ ∀x. example (example x) = x: thm

> theorems "example";
val it =
   [("num2example_thm", ⊢ num2example 0 = First ∧ num2example 1 = Second),
    ("num2example_ONTO", ⊢ ∀a. ∃r. a = num2example r ∧ r < 2),
    ("num2example_example2num", ⊢ ∀a. num2example (example2num a) = a),
    ("num2example_11",
     ⊢ ∀r r'. r < 2 ⇒ r' < 2 ⇒ (num2example r = num2example r' ⇔ r = r')),
    ("example_thm", ⊢ ∀x. example (example x) = x),
    ("example_nchotomy", ⊢ ∀a. a = First ∨ a = Second),
    ("example_induction", ⊢ ∀P. P First ∧ P Second ⇒ ∀a. P a),
    ("example_EQ_example", ⊢ ∀a a'. a = a' ⇔ example2num a = example2num a'),
    ("example_distinct", ⊢ First ≠ Second),
    ("example_case_eq",
     ⊢ (case x of First => v0 | Second => v1) = v ⇔
       x = First ∧ v0 = v ∨ x = Second ∧ v1 = v),
    ("example_case_def",
     ⊢ (∀v0 v1. (case First of First => v0 | Second => v1) = v0) ∧
       ∀v0 v1. (case Second of First => v0 | Second => v1) = v1),
    ("example_case_cong",
     ⊢ ∀M M' v0 v1.
         M = M' ∧ (M' = First ⇒ v0 = v0') ∧ (M' = Second ⇒ v1 = v1') ⇒
         (case M of First => v0 | Second => v1) =
         case M' of First => v0' | Second => v1'),
    ("example_Axiom", ⊢ ∀x0 x1. ∃f. f First = x0 ∧ f Second = x1),
    ("example2num_thm", ⊢ example2num First = 0 ∧ example2num Second = 1),
    ("example2num_ONTO", ⊢ ∀r. r < 2 ⇔ ∃a. r = example2num a),
    ("example2num_num2example",
     ⊢ ∀r. r < 2 ⇔ example2num (num2example r) = r),
    ("example2num_11", ⊢ ∀a a'. example2num a = example2num a' ⇔ a = a'),
    ("datatype_example", ⊢ DATATYPE (example First Second))]:
   (string * thm) list

> EmitTeX.non_type_theorems "example";
val it =
   [("example_case_eq",
     ⊢ (case x of First => v0 | Second => v1) = v ⇔
       x = First ∧ v0 = v ∨ x = Second ∧ v1 = v),
    ("example_thm", ⊢ ∀x. example (example x) = x)]: (string * thm) list

See also

DB.theorems, bossLib.Hol_datatype