192 else list_abs_free (map dest_Free xs, list_comb |
192 else list_abs_free (map dest_Free xs, list_comb |
193 (Free ("r" ^ Sign.base_name (Thm.name_of_thm intr), |
193 (Free ("r" ^ Sign.base_name (Thm.name_of_thm intr), |
194 map fastype_of (rev args) ---> conclT), rev args)) |
194 map fastype_of (rev args) ---> conclT), rev args)) |
195 end |
195 end |
196 |
196 |
197 in fun_of (rev args) [] args' used (Logic.strip_imp_prems rule') end; |
197 in fun_of args' [] (rev args) used (Logic.strip_imp_prems rule') end; |
198 |
198 |
199 fun indrule_realizer thy induct raw_induct rsets params vs rec_names rss intrs dummies = |
199 fun indrule_realizer thy induct raw_induct rsets params vs rec_names rss intrs dummies = |
200 let |
200 let |
201 val concls = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct)); |
201 val concls = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct)); |
202 val premss = mapfilter (fn (s, rs) => if s mem rsets then |
202 val premss = mapfilter (fn (s, rs) => if s mem rsets then |
381 (** realizer for elimination rules **) |
381 (** realizer for elimination rules **) |
382 |
382 |
383 val case_names = map (fst o dest_Const o head_of o fst o HOLogic.dest_eq o |
383 val case_names = map (fst o dest_Const o head_of o fst o HOLogic.dest_eq o |
384 HOLogic.dest_Trueprop o prop_of o hd) (get #case_thms dt_info); |
384 HOLogic.dest_Trueprop o prop_of o hd) (get #case_thms dt_info); |
385 |
385 |
386 fun add_elim_realizer Ps ((((elim, elimR), case_thms), case_name), dummy) thy = |
386 fun add_elim_realizer Ps |
|
387 (((((elim, elimR), intrs), case_thms), case_name), dummy) thy = |
387 let |
388 let |
388 val (prem :: prems) = prems_of elim; |
389 val (prem :: prems) = prems_of elim; |
389 val p = Logic.list_implies (prems @ [prem], concl_of elim); |
390 fun reorder1 (p, intr) = |
|
391 foldl (fn (t, ((s, _), T)) => all T $ lambda (Free (s, T)) t) |
|
392 (strip_all p, Term.add_vars ([], prop_of intr)); |
|
393 fun reorder2 (intr, i) = |
|
394 let |
|
395 val fs1 = term_vars (prop_of intr); |
|
396 val fs2 = Term.add_vars ([], prop_of intr) |
|
397 in foldl (fn (t, x) => lambda (Var x) t) |
|
398 (list_comb (Bound (i + length fs1), fs1), fs2) |
|
399 end; |
|
400 val p = Logic.list_implies |
|
401 (map reorder1 (prems ~~ intrs) @ [prem], concl_of elim); |
390 val T' = Extraction.etype_of thy (vs @ Ps) [] p; |
402 val T' = Extraction.etype_of thy (vs @ Ps) [] p; |
391 val T = if dummy then (HOLogic.unitT --> body_type T') --> T' else T'; |
403 val T = if dummy then (HOLogic.unitT --> body_type T') --> T' else T'; |
392 val Ts = filter_out (equal Extraction.nullT) |
404 val Ts = map (Extraction.etype_of thy (vs @ Ps) []) (prems_of elim); |
393 (map (Extraction.etype_of thy (vs @ Ps) []) (prems_of elim)); |
|
394 val r = if null Ps then Extraction.nullt |
405 val r = if null Ps then Extraction.nullt |
395 else list_abs (map (pair "x") Ts, list_comb (Const (case_name, T), |
406 else list_abs (map (pair "x") Ts, list_comb (Const (case_name, T), |
396 (if dummy then |
407 (if dummy then |
397 [Abs ("x", HOLogic.unitT, Const ("arbitrary", body_type T))] |
408 [Abs ("x", HOLogic.unitT, Const ("arbitrary", body_type T))] |
398 else []) @ |
409 else []) @ |
399 map Bound ((length prems - 1 downto 0) @ [length prems]))); |
410 map reorder2 (intrs ~~ (length prems - 1 downto 0)) @ |
|
411 [Bound (length prems)])); |
400 val rlz = strip_all (Logic.unvarify |
412 val rlz = strip_all (Logic.unvarify |
401 (Extraction.realizes_of thy (vs @ Ps) r (prop_of elim))); |
413 (Extraction.realizes_of thy (vs @ Ps) r (prop_of elim))); |
402 val rews = map mk_meta_eq case_thms; |
414 val rews = map mk_meta_eq case_thms; |
403 val thm = simple_prove_goal_cterm (cterm_of (sign_of thy) rlz) (fn prems => |
415 val thm = simple_prove_goal_cterm (cterm_of (sign_of thy) rlz) (fn prems => |
404 [cut_facts_tac [hd prems] 1, |
416 [cut_facts_tac [hd prems] 1, |
422 val thy5 = Extraction.add_realizers_i |
434 val thy5 = Extraction.add_realizers_i |
423 (map (mk_realizer thy4 vs params') |
435 (map (mk_realizer thy4 vs params') |
424 (map (fn ((rule, rrule), c) => ((rule, rrule), list_comb (c, |
436 (map (fn ((rule, rrule), c) => ((rule, rrule), list_comb (c, |
425 map Var (rev (Term.add_vars ([], prop_of rule)) \\ params')))) |
437 map Var (rev (Term.add_vars ([], prop_of rule)) \\ params')))) |
426 (flat (map snd rss) ~~ rintr_thms ~~ flat constrss))) thy4; |
438 (flat (map snd rss) ~~ rintr_thms ~~ flat constrss))) thy4; |
427 val elimps = mapfilter (fn (s, _) => if s mem rsets then |
439 val elimps = mapfilter (fn (s, intrs) => if s mem rsets then |
428 find_first (fn (thm, _) => s mem term_consts (hd (prems_of thm))) |
440 apsome (rpair intrs) (find_first (fn (thm, _) => |
429 (elims ~~ #elims ind_info) |
441 s mem term_consts (hd (prems_of thm))) (elims ~~ #elims ind_info)) |
430 else None) rss; |
442 else None) rss; |
431 val thy6 = foldl (fn (thy, p as ((((elim, _), _), _), _)) => thy |> |
443 val thy6 = foldl (fn (thy, p as (((((elim, _), _), _), _), _)) => thy |> |
432 add_elim_realizer [] p |> add_elim_realizer [fst (fst (dest_Var |
444 add_elim_realizer [] p |> add_elim_realizer [fst (fst (dest_Var |
433 (HOLogic.dest_Trueprop (concl_of elim))))] p) (thy5, |
445 (HOLogic.dest_Trueprop (concl_of elim))))] p) (thy5, |
434 elimps ~~ get #case_thms dt_info ~~ case_names ~~ dummies) |
446 elimps ~~ get #case_thms dt_info ~~ case_names ~~ dummies) |
435 |
447 |
436 in Theory.add_path (NameSpace.pack (if_none path [])) thy6 end; |
448 in Theory.add_path (NameSpace.pack (if_none path [])) thy6 end; |