(* Subject: Mutually recursive rule induction *)
(* Author: Myra Van Inwegen *)
(* Part of the author's doctoral dissertation *)
signature ind_rel =
sig
val check_inductive_relations :
Term.term list -> (* patterns *)
Term.term -> (* term giving rules *)
Term.term list (* each term corresponds to a quantified rule *)
val define_inductive_relations :
Term.term list -> (* patterns *)
Term.term -> (* term giving rules *)
Thm.thm * Thm.thm (* rules_satisfied theorem, induction theorem *)
val prove_inversion_theorems :
Thm.thm -> (* rules_satisfied theorem *)
Thm.thm -> (* induction theorem *)
Thm.thm list (* inversion theorems *)
val prove_strong_induction :
Thm.thm -> (* rules_satisfied theorem *)
Thm.thm -> (* induction theorem *)
Thm.thm (* strong induction theorem *)
val rule_induct :
Thm.thm -> (* induction theorem (strong or regular) *)
Abbrev.tactic (* sets up induction *)
end;