193 map fastype_of (rev args) ---> conclT), rev args)) |
193 map fastype_of (rev args) ---> conclT), rev args)) |
194 end |
194 end |
195 |
195 |
196 in fun_of args' [] (rev args) used (Logic.strip_imp_prems rule') end; |
196 in fun_of args' [] (rev args) used (Logic.strip_imp_prems rule') end; |
197 |
197 |
|
198 fun find_first f = Library.find_first f; |
|
199 |
198 fun indrule_realizer thy induct raw_induct rsets params vs rec_names rss intrs dummies = |
200 fun indrule_realizer thy induct raw_induct rsets params vs rec_names rss intrs dummies = |
199 let |
201 let |
200 val concls = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct)); |
202 val concls = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct)); |
201 val premss = List.mapPartial (fn (s, rs) => if s mem rsets then |
203 val premss = List.mapPartial (fn (s, rs) => if s mem rsets then |
202 SOME (map (fn r => List.nth (prems_of raw_induct, |
204 SOME (map (fn r => List.nth (prems_of raw_induct, |
306 val dts = List.mapPartial (fn (s, rs) => if s mem rsets then |
308 val dts = List.mapPartial (fn (s, rs) => if s mem rsets then |
307 SOME (dt_of_intrs thy1' vs rs) else NONE) rss; |
309 SOME (dt_of_intrs thy1' vs rs) else NONE) rss; |
308 |
310 |
309 (** datatype representing computational content of inductive set **) |
311 (** datatype representing computational content of inductive set **) |
310 |
312 |
311 val (thy2, (dummies, dt_info)) = thy1 |> |
313 val (thy2, (dummies, dt_info)) = |
312 (if null dts then rpair ([], NONE) else |
314 thy1 |
313 apsnd (apsnd SOME) o add_dummies (DatatypePackage.add_datatype_i false false |
315 |> (if null dts |
314 (map #2 dts)) (map (pair false) dts) []) |>> |
316 then rpair ([], NONE) |
315 Extraction.add_typeof_eqns_i ty_eqs |>> |
317 else add_dummies (DatatypePackage.add_datatype_i false false |
316 Extraction.add_realizes_eqns_i rlz_eqs; |
318 (map #2 dts)) (map (pair false) dts) [] #> (fn (v, (b, thy)) => (thy, (b, SOME v)))) |
|
319 |>> Extraction.add_typeof_eqns_i ty_eqs |
|
320 |>> Extraction.add_realizes_eqns_i rlz_eqs; |
317 fun get f x = getOpt (Option.map f x, []); |
321 fun get f x = getOpt (Option.map f x, []); |
318 val rec_names = distinct (map (fst o dest_Const o head_of o fst o |
322 val rec_names = distinct (map (fst o dest_Const o head_of o fst o |
319 HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) (get #rec_thms dt_info)); |
323 HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) (get #rec_thms dt_info)); |
320 val (_, constrss) = foldl_map (fn ((recs, dummies), (s, rs)) => |
324 val (_, constrss) = foldl_map (fn ((recs, dummies), (s, rs)) => |
321 if s mem rsets then |
325 if s mem rsets then |