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