1(* Subject: Mutually recursive rule induction *)
2(* Author: Myra Van Inwegen *)
3(* Part of the author's doctoral dissertation *)
4
5signature ind_rel =
6sig
7
8val   check_inductive_relations :
9         Term.term list ->     (* patterns *)
10         Term.term ->          (* term giving rules *)
11         Term.term list        (* each term corresponds to a quantified rule *)
12val   define_inductive_relations :
13         Term.term list ->     (* patterns *)
14         Term.term ->          (* term giving rules *)
15         Thm.thm * Thm.thm     (* rules_satisfied theorem, induction theorem *)
16val   prove_inversion_theorems :
17         Thm.thm ->            (* rules_satisfied theorem *)
18         Thm.thm ->            (* induction theorem *)
19         Thm.thm list          (* inversion theorems *)
20val   prove_strong_induction :
21         Thm.thm ->            (* rules_satisfied theorem *)
22         Thm.thm ->            (* induction theorem *)
23         Thm.thm               (* strong induction theorem *)
24val   rule_induct :
25         Thm.thm ->            (* induction theorem (strong or regular) *)
26         Abbrev.tactic         (* sets up induction *)
27
28end
29