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