new_type_definition : string * thm -> thm

- STRUCTURE
- SYNOPSIS
- Defines a new type constant or type operator.
- DESCRIPTION
- The ML function new_type_definition implements the primitive HOL rule of definition for introducing new type constants or type operators into the logic. If t is a term of type ty->bool containing n distinct type variables, then evaluating:results in tyop being declared as a new n-ary type operator in the current theory and returned by the call to new_type_definition. This new type operator is characterized by a definitional axiom of the form:
new_type_definition (tyop, |- ?x. t x)

which is stored as a definition in the current theory segment under the automatically-generated name op_TY_DEF. The arguments to the new type operator occur in the order given by an alphabetic ordering of the name of the corresponding type variables. The constant TYPE_DEFINITION in this axiomatic characterization of tyop is defined by:|- ?rep:('a,...,'n)op->tyop. TYPE_DEFINITION t rep

Thus |- ?rep. TYPE_DEFINITION P rep asserts that there is a bijection between the newly defined type ('a,...,'n)tyop and the set of values of type ty that satisfy P.|- TYPE_DEFINITION (P:'a->bool) (rep:'b->'a) = (!x' x''. (rep x' = rep x'') ==> (x' = x'')) /\ (!x. P x = (?x'. x = rep x'))

- FAILURE
- Executing new_type_definition(tyop,th) fails if th is not an assumption-free theorem of the form |- ?x. t x, if the type of t is not of the form ty->bool, or if there are free variables in the term t.
- EXAMPLE
- In this example, a type containing three elements is defined. The predicate defining the type is over the type bool # bool.
app load ["PairedLambda", "Q"]; open PairedLambda pairTheory; - val tyax = new_type_definition ("three", Q.prove(`?p. (\(x,y). ~(x /\ y)) p`, Q.EXISTS_TAC `(F,F)` THEN GEN_BETA_TAC THEN REWRITE_TAC [])); > val tyax = |- ?rep. TYPE_DEFINITION (\(x,y). ~(x /\ y)) rep : thm

- COMMENTS
- Usually, once a type has been defined, maps between the representation type and the new type need to be proved. This may be accomplished using define_new_type_bijections. In the example, the two functions are named abs3 and rep3.Properties of the maps may be conveniently proved with prove_abs_fn_one_one, prove_abs_fn_onto, prove_rep_fn_one_one, and prove_rep_fn_onto. In this case, we need only prove_abs_fn_one_one.
- val three_bij = define_new_type_bijections {name="three_tybij", ABS="abs3", REP="rep3", tyax=tyax}; > val three_bij = |- (!a. abs3 (rep3 a) = a) /\ (!r. (\(x,y). ~(x /\ y)) r = (rep3 (abs3 r) = r))

Now we address how to define constants designating the three elements of our example type. We will use new_specification to create these constants (say e1, e2, and e3) and their characterizing property, which is- val abs_11 = GEN_BETA_RULE (prove_abs_fn_one_one three_bij); > val abs_11 = |- !r r'. ~(FST r /\ SND r) ==> ~(FST r' /\ SND r') ==> ((abs3 r = abs3 r') = (r = r')) : thm

A simple lemma stating that the abstraction function doesn’t confuse any of the representations is required:~(e1 = e2) /\ ~(e2 = e3) /\ ~(e3 = e1)

Finally, we can introduce the constants and their property.- val abs_distinct = REWRITE_RULE (PAIR_EQ::pair_rws) (LIST_CONJ (map (C Q.SPECL abs_11) [[`(F,F)`,`(F,T)`], [`(F,T)`,`(T,F)`], [`(T,F)`,`(F,F)`]])); > val abs_distinct = |- ~(abs3 (F,F) = abs3 (F,T)) /\ ~(abs3 (F,T) = abs3 (T,F)) /\ ~(abs3 (T,F) = abs3 (F,F)) : thm

- val THREE = new_specification ("THREE", ["e1", "e2", "e3"], PROVE [abs_distinct] (Term`?x y z:three. ~(x=y) /\ ~(y=z) /\ ~(z=x)`)); > val THREE = |- ~(e1 = e2) /\ ~(e2 = e3) /\ ~(e3 = e1) : thm

- SEEALSO

HOL Kananaskis-14