1structure DefnBase :> DefnBase = 2struct 3 4open HolKernel 5 6val ERR = mk_HOL_ERR "DefnBase"; 7 8(*--------------------------------------------------------------------------- 9 The type of definitions. This is an attempt to gather all the 10 information about a definition in one place. 11 ---------------------------------------------------------------------------*) 12 13datatype defn 14 = ABBREV of {eqn:thm, bind:string} 15 | PRIMREC of {eqs:thm, ind:thm, bind:string} 16 | NONREC of {eqs:thm, ind:thm, SV:term list, stem:string} 17 | STDREC of {eqs:thm list, ind:thm, R:term,SV:term list,stem:string} 18 | MUTREC of {eqs:thm list, ind:thm, R:term, SV:term list, 19 stem:string,union:defn} 20 | NESTREC of {eqs:thm list, ind:thm, R:term, SV:term list, 21 stem:string, aux:defn} 22 | TAILREC of {eqs:thm list, ind:thm, R:term, SV:term list, stem:string} 23 24fun all_terms d = 25 case d of 26 ABBREV{eqn,...} => [concl eqn] 27 | PRIMREC {eqs,ind,...} => [concl eqs, concl ind] 28 | NONREC {eqs,ind,SV,...} => concl eqs::concl ind::SV 29 | STDREC {eqs,ind,R,SV,...} => R :: concl ind :: map concl eqs @ SV 30 | MUTREC {eqs,ind,R,SV,union,...} => 31 R :: concl ind :: map concl eqs @ SV @ all_terms union 32 | NESTREC {eqs,ind,R,SV,aux,...} => 33 R :: concl ind :: map concl eqs @ SV @ all_terms aux 34 | TAILREC {eqs,ind,R,SV,...} => R :: concl ind :: map concl eqs @ SV 35 36local open Portable 37 fun kind (ABBREV _) = "abbreviation" 38 | kind (NONREC _) = "non-recursive" 39 | kind (STDREC _) = "recursive" 40 | kind (PRIMREC _) = "primitive recursion" 41 | kind (MUTREC _) = "mutual recursion" 42 | kind (NESTREC _) = "nested recursion" 43 | kind (TAILREC _) = "nonterminating tail recursion" 44 fun hyps thl = HOLset.listItems 45 (foldl (fn (th,s) => HOLset.union(hypset th, s)) 46 empty_tmset thl) 47in 48fun pp_defn d = 49 let open smpp 50 val pp_term = lift Parse.pp_term 51 val pp_thm = lift Parse.pp_thm 52 fun pp_rec (eqs,ind,tcs) = 53 block CONSISTENT 0 ( 54 add_string "Equation(s) :" >> 55 add_break(1,0) >> 56 pr_list pp_thm add_newline eqs >> 57 add_newline >> add_newline >> 58 add_string "Induction :" >> 59 add_break(1,0) >> 60 pp_thm ind >> 61 (if null tcs then nothing 62 else 63 (add_newline >> add_newline >> 64 add_string "Termination conditions :" >> 65 add_break(1,2) >> 66 block CONSISTENT 0 ( 67 pr_list (fn (n,tm) => 68 block CONSISTENT 3 ( 69 add_string (Lib.int_to_string n^". ") >> 70 pp_term tm 71 ) 72 ) 73 add_newline 74 (Lib.enumerate 0 tcs) 75 )) 76 ) 77 ) 78 fun pp (ABBREV {eqn, ...}) = 79 block CONSISTENT 0 ( 80 add_string "Equation :" >> 81 add_break(1,0) >> 82 pp_thm eqn 83 ) 84 | pp (PRIMREC{eqs, ind, bind}) = 85 block CONSISTENT 0 ( 86 add_string "Equation(s) :" >> 87 add_break(1,0) >> 88 pp_thm eqs 89 ) 90 | pp (NONREC {eqs, ind, SV, stem}) = 91 block CONSISTENT 0 ( 92 add_string "Equation(s) :" >> 93 add_break(1,0) >> 94 pp_thm eqs >> 95 add_newline >> add_newline >> 96 add_string "Case analysis:" >> 97 add_break(1,0) >> pp_thm ind 98 ) 99 | pp (STDREC {eqs, ind, R, SV, stem}) = pp_rec(eqs,ind, hyps eqs) 100 | pp (NESTREC{eqs, ind, R, SV, aux, stem}) = pp_rec(eqs,ind, hyps eqs) 101 | pp (MUTREC {eqs, ind, R, SV, union, stem}) = pp_rec(eqs,ind, hyps eqs) 102 | pp (TAILREC{eqs, ind, R, SV, stem}) = pp_rec(eqs,ind, hyps eqs) 103 val m = 104 block CONSISTENT 0 ( 105 add_string "HOL function definition " >> 106 add_string (String.concat ["(",kind d,")"]) >> 107 add_newline >> add_newline >> 108 pp d 109 ) 110 in 111 Parse.mlower m 112 end 113end; 114 115 116(*--------------------------------------------------------------------------- 117 Congruence rules for termination condition extraction. Before 118 t.c. extraction is performed, the theorems in "non_datatype_congs" 119 are added to the congruence rules arising from datatype definitions, 120 which are held in the TypeBase. 121 ---------------------------------------------------------------------------*) 122 123 124local open boolTheory 125 val non_datatype_congs = 126 ref [LET_CONG, COND_CONG, IMP_CONG, literal_case_CONG] 127in 128 fun read_congs() = !non_datatype_congs 129 fun write_congs L = (non_datatype_congs := L) 130end; 131 132fun add_cong thm = write_congs (thm :: read_congs()); 133 134fun drop_cong c = 135 let open boolSyntax 136 val P = same_const c 137 val (cong,rst) = 138 pluck (fn th => P (fst(strip_comb(lhs(snd 139 (strip_imp(snd(strip_forall(concl th))))))))) 140 (read_congs()) 141 val _ = write_congs rst 142 in 143 cong 144 end 145 handle e => raise wrap_exn "DefnBase.drop_cong" 146 (case total dest_thy_const c 147 of NONE => "expected a constant" 148 | SOME{Thy,Name,...} => 149 ("congruence rule for " 150 ^Lib.quote(Thy^"$"^Name) 151 ^" was not found")) e; 152 153val {export = export_cong,...} = 154 ThmSetData.new_exporter "defncong" 155 (fn _ (* thy *) => fn namedthms => 156 app (add_cong o #2) namedthms) 157 158end 159