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