Next: UTac Up: LEGO Release 1.3 Documentation Previous: Then

LEGO Version 1.3: Theorems and Configure Theorems

Simple inductive datatypes can be equipped with useful gadgets by the new version of the Theorems switch, in accordance with the parameters set up by the Configure Theorems command. This configuration can work in one of two ways:

  Inductive [simple:SET] Theorems

will build for each constructor coni a function simple_is_coni

acting like

  fun simple_is_coni (coni xi1 .. xiji) = true_type or true_value
    | simple_is_coni _ = absurd_type or false_value

These functions can then be used, with eq_subst or true_not_false according to the configuration, to synthesise constructor conflict theorems as required.

Also constructed where possible are the injectivity theorems:

  simple_coni_injective : {xi1,yi1|Ti1}..{xiji,yiji|Tiji}
                              (Eq (coni xi1 .. xiji) (coni yi1 .. yiji))->
                              {P|subst_univ} ((Eq xi1 yi1)->..->(Eq xiji yiji)->P)->P

where subst_univ is the universe over which eq_subst substitutes.

At present, LEGO fails to generate an injectivity theorem for any constructor whose arguments contain type dependencies such that the injected equalities are not well-typed. In these circumstances, the user is informed of the omission, but the inductive definition goes though anyway, along with those injectivity theorems which can be generated.

Note that the Theorems package uses the equality set up by Configure Equality. The library's default equality comes with an appropriate Theorems configuration.

The Qnify tactic uses the facilities generated by Theorems to solve first-order unification problems involving constructors and variables expressed as equational premises in the goal.