1structure IndDefLib :> IndDefLib = 2struct 3 4local open IndDefRules in end; 5 6open HolKernel Abbrev; 7 8type monoset = InductiveDefinition.monoset; 9 10val ERR = mk_HOL_ERR "IndDefLib"; 11val ERRloc = mk_HOL_ERRloc "IndDefLib"; 12 13local open Absyn 14 fun head clause = 15 let val appl = last (strip_imp (snd(strip_forall clause))) 16 in fst(strip_app appl) 17 end 18 fun determ M = 19 fst(Term.dest_var M handle HOL_ERR _ => Term.dest_const M) 20 handle HOL_ERR _ => raise ERR "determ" "Non-atom in antiquote" 21 fun dest (AQ (_,tm)) = determ tm 22 | dest (IDENT (_,s)) = s 23 | dest other = raise ERRloc "names_of.reln_names.dest" 24 (locn_of_absyn other) "Unexpected structure" 25in 26fun term_of_absyn absyn = let 27 val clauses = strip_conj absyn 28 fun checkcl a = let 29 val nm = dest (head a) 30 in 31 if mem nm ["/\\", "\\/", "!", "?", "LET", 32 UnicodeChars.conj, UnicodeChars.disj, UnicodeChars.forall, 33 UnicodeChars.exists] 34 then 35 raise ERRloc "term_of_absyn" (locn_of_absyn a) 36 ("Abstract syntax looks to be trying to redefine "^nm^". "^ 37 "\nThis is probably an error.\nIf you must, define with \ 38 \another name and use overload_on") 39 else nm 40 end 41 val names = mk_set (map checkcl clauses) 42 val resdata = List.map (fn s => (s, Parse.hide s)) names 43 fun restore() = 44 List.app (fn (s,d) => Parse.update_overload_maps s d) resdata 45 val tm = 46 Parse.absyn_to_term (Parse.term_grammar()) absyn 47 handle e => (restore(); raise e) 48in 49 restore(); 50 (tm, map locn_of_absyn clauses) 51end 52 53fun term_of q = term_of_absyn (Parse.Absyn q) 54 55end; 56 57(* ---------------------------------------------------------------------- 58 Store all rule inductions 59 ---------------------------------------------------------------------- *) 60 61val term_rule_map : ({Name:string,Thy:string},thm list)Binarymap.dict ref = 62 ref (Binarymap.mkDict KernelSig.name_compare) 63 64fun listdict_add (d, k, e) = 65 case Binarymap.peek(d, k) of 66 NONE => Binarymap.insert(d,k,[e]) 67 | SOME l => Binarymap.insert(d,k,e::l) 68 69fun rule_induction_map() = !term_rule_map 70 71fun ind_thm_to_consts thm = let 72 open boolSyntax 73 val c = concl thm 74 val (_, bod) = strip_forall c 75 val (_, con) = dest_imp bod 76 val cons = strip_conj con 77 fun to_kname {Name,Thy,...} = {Name = Name, Thy = Thy} 78in 79 map (fn t => t |> strip_forall |> #2 |> dest_imp |> #1 |> strip_comb |> #1 80 |> dest_thy_const |> to_kname) 81 cons 82end 83 84fun add_rule_induction th = let 85 val nm = current_theory() 86 val ts = ind_thm_to_consts th 87in 88 term_rule_map := List.foldl (fn (t,d) => listdict_add(d,t,th)) 89 (!term_rule_map) 90 ts 91end 92 93(* making it exportable *) 94val {export = export_rule_induction, dest, ...} = 95 ThmSetData.new_exporter "rule_induction" (K (app (add_rule_induction o #2))) 96 97fun thy_rule_inductions thyname = let 98 val segdata = 99 LoadableThyData.segment_data {thy = thyname, thydataty = "rule_induction"} 100in 101 case segdata of 102 NONE => [] 103 | SOME d => map #2 (valOf (dest d)) 104end 105 106(* ---------------------------------------------------------------------- 107 the built-in monoset, that users can update as they prove new 108 monotonicity results about their constants 109 ---------------------------------------------------------------------- *) 110 111val the_monoset = ref InductiveDefinition.bool_monoset 112 113fun mono_name th = let 114 open boolLib 115 val (_, con) = dest_imp (concl th) 116in 117 #1 (dest_const (#1 (strip_comb (#1 (dest_imp con))))) 118end 119 120fun add_mono_thm th = the_monoset := (mono_name th, th) :: (!the_monoset) 121 122(* making it exportable *) 123val {export = export_mono, dest, ...} = 124 ThmSetData.new_exporter "mono" (K (app (add_mono_thm o #2))) 125 126fun thy_monos thyname = 127 case LoadableThyData.segment_data {thy = thyname, thydataty = "mono"} of 128 NONE => [] 129 | SOME d => map #2 (valOf (dest d)) 130 131(*--------------------------------------------------------------------------- 132 given a case theorem of the sort returned by new_inductive_definition 133 return the name of the first new constant mentioned 134 form is 135 (!x y z. (C x y z = ...)) /\ 136 (!u v w. (D u v w = ...)) 137 in which case we return ["C", "D"] 138 ---------------------------------------------------------------------------*) 139 140open InductiveDefinition 141 142fun names_from_casethm thm = let 143 open HolKernel boolSyntax 144 val forallbod = #2 o strip_forall 145 val eqns = thm |> concl |> forallbod |> strip_conj |> map forallbod 146 val cnsts = map (#1 o strip_comb o lhs) eqns 147in 148 map (#1 o dest_const) cnsts 149end 150 151val derive_mono_strong_induction = IndDefRules.derive_mono_strong_induction; 152fun derive_strong_induction (rules,ind) = 153 IndDefRules.derive_mono_strong_induction (!the_monoset) (rules, ind) 154 155fun save_theorems name (rules, indn, strong_ind, cases) = let 156in 157 save_thm(name^"_rules", rules); 158 save_thm(name^"_ind", indn); 159 save_thm(name^"_strongind", strong_ind); 160 save_thm(name^"_cases", cases); 161 export_rule_induction (name ^ "_strongind") 162end 163 164fun Hol_mono_reln name monoset tm = let 165 val _ = Lexis.ok_sml_identifier (name ^ !boolLib.def_suffix) orelse 166 raise ERR "Hol_mono_reln" 167 ("Bad name for definition: "^ Lib.mlquote name^ 168 " (use xHol_reln to specify a better)") 169 val (rules, indn, cases) = new_inductive_definition monoset name tm 170 (* not! InductiveDefinition.bool_monoset tm *) 171 val strong_ind = derive_strong_induction (rules, indn) 172in 173 save_theorems name (rules, indn, strong_ind, cases); 174 (rules, indn, cases) 175end 176handle e => raise (wrap_exn "IndDefLib" "Hol_mono_reln" e); 177 178 179(* ---------------------------------------------------------------------- 180 the standard entry-points 181 ---------------------------------------------------------------------- *) 182 183fun xHol_reln name q = Hol_mono_reln name (!the_monoset) (term_of q) 184 185fun name_from_def t = let 186 open boolSyntax 187 val cs = strip_conj t 188in 189 hd cs |> strip_forall |> #2 |> strip_imp |> #2 |> strip_comb |> #1 |> 190 dest_var |> #1 191end 192 193fun Hol_reln q = let 194 val parse = term_of |> trace ("syntax_error", 0) 195 |> trace ("show_typecheck_errors", 0) 196 (* turn off verbiage because the Raise below will redisplay any 197 exceptions *) 198 val def as (def_t,_) = parse q 199 val name = name_from_def def_t 200in 201 Hol_mono_reln name (!the_monoset) def 202end handle e => Raise (wrap_exn "IndDefLib" "Hol_reln" e); 203 204end 205