1signature DefnBase = 2sig 3 type term = Term.term 4 type thm = Thm.thm 5 6 datatype defn 7 = ABBREV of {eqn:thm, bind:string} 8 | PRIMREC of {eqs:thm, ind:thm, bind:string} 9 | NONREC of {eqs:thm, ind:thm, SV:term list, stem:string} 10 | STDREC of {eqs:thm list, ind:thm, R:term,SV:term list,stem:string} 11 | MUTREC of {eqs:thm list, ind:thm, R:term,SV:term list, 12 stem:string,union:defn} 13 | NESTREC of {eqs:thm list, ind:thm, R:term,SV:term list, 14 stem:string,aux:defn} 15 | TAILREC of {eqs:thm list, ind:thm, R:term, SV:term list, stem:string} 16 17 18 val pp_defn : defn Parse.pprinter 19 val all_terms : defn -> term list 20 (* conclusions of theorems, SV variables, R *) 21 22 (* Used to control context tracking during termination 23 condition extraction *) 24 25 val read_congs : unit -> thm list 26 val write_congs : thm list -> unit 27 val add_cong : thm -> unit 28 val drop_cong : term -> thm 29 30 val export_cong : string -> unit 31 32 (* record various flavours of definition, keyed by constant and a 33 "tag", which is a user-choosable string. Assume that "user" and 34 "compute" exist for example. 35 36 Another might be "PMATCH", which would be the definition with 37 case constants translated into PMATCH versions. 38 *) 39 val register_defn : string -> thm -> unit 40 val lookup_defn : term -> string -> thm option 41 42 val register_indn : thm * term list -> unit 43 val lookup_indn : term -> (thm * term list) option 44 45 (* register_defn is given a tag and a theorem which is a conjunction of 46 possibly universally quantified equations. The machinery here 47 will create a sub-conjunction of the clauses per constant (and this is 48 what is returned by lookup_defn). 49 50 Induction theorems have some number of induction variables (P1, 51 P2, ..) where each corresponds to a defined constant. This list 52 of constants is what is passed into register_indn alongside the 53 induction theorem. When a term is looked up, if lookup_indn t 54 returns SOME (th, ts), then t will be among the ts. 55 *) 56 57 val const_eq_ref : Abbrev.conv ref 58 val elim_triv_literal_CONV : Abbrev.conv 59 val one_line_ify : PmatchHeuristics.pmatch_heuristic option -> thm -> thm 60 61end 62