1193323Sed(* Subject: Mutually recursive rule induction *)
2193323Sed(* Author: Myra Van Inwegen *)
3193323Sed(* Part of the author's doctoral dissertation *)
4193323Sed
5193323Sedsignature ind_rel =
6193323Sedsig
7193323Sed
8193323Sedval   check_inductive_relations :
9193323Sed         Term.term list ->     (* patterns *)
10193323Sed         Term.term ->          (* term giving rules *)
11193323Sed         Term.term list        (* each term corresponds to a quantified rule *)
12193323Sedval   define_inductive_relations :
13193323Sed         Term.term list ->     (* patterns *)
14193323Sed         Term.term ->          (* term giving rules *)
15193323Sed         Thm.thm * Thm.thm     (* rules_satisfied theorem, induction theorem *)
16193323Sedval   prove_inversion_theorems :
17249423Sdim         Thm.thm ->            (* rules_satisfied theorem *)
18193323Sed         Thm.thm ->            (* induction theorem *)
19224145Sdim         Thm.thm list          (* inversion theorems *)
20221345Sdimval   prove_strong_induction :
21193323Sed         Thm.thm ->            (* rules_satisfied theorem *)
22193323Sed         Thm.thm ->            (* induction theorem *)
23193323Sed         Thm.thm               (* strong induction theorem *)
24210299Sedval   rule_induct :
25193323Sed         Thm.thm ->            (* induction theorem (strong or regular) *)
26193323Sed         Abbrev.tactic         (* sets up induction *)
27203954Srdivacky
28218893Sdimend
29203954Srdivacky