1open HolKernel Parse boolLib
2
3val _ = new_theory "ndatatype_ind0";
4
5(* set up a type (that is a copy of lists, basically), with an
6   induction and cases theorems, and register this type in the TypeBase.
7
8   Check that this type supports various forms of Induct_on and Induct.
9*)
10
11val _ = new_type ("foo", 1)
12
13val _ = new_constant("foonil", ``:'a foo``)
14val _ = new_constant("foocons", ``:'a -> 'a foo -> 'a foo``)
15
16val foo_ind = new_axiom (
17  "foo_ind",
18  ``!P. P foonil /\ (!t. P t ==> !a. P (foocons a t)) ==> !x. P x``);
19
20val foo_cases = new_axiom (
21  "foo_cases",
22  ``!x. (x = foonil) \/ ?a t. x = foocons a t``);
23
24val _ = TypeBase.write [
25  TypeBasePure.mk_nondatatype_info
26          (``:'a foo``,
27           {encode = NONE, induction = SOME foo_ind,
28            nchotomy = SOME foo_cases, size = NONE})
29]
30
31val c = ref 0
32fun check (tac, t) = (tac([], t) before ignore (save_thm(
33  "OK" ^ Int.toString (!c) before c := !c + 1,
34  TRUTH)))
35
36open BasicProvers
37val _ = map check [
38  (Induct_on `t`, ``foonil <> foocons (a:'a) t``),
39  (Induct_on `t`, ``!t. foonil <> foocons (a:'a) t``),
40  (Induct_on `foocons a t`, ``foonil <> foocons (a:'a) t``),
41  (Induct, ``!t. foonil <> foocons (a:'a) t``)
42]
43
44val _ = export_theory();
45