576 val corr_prop = Reconstruct.prop_of corr_prf; |
576 val corr_prop = Reconstruct.prop_of corr_prf; |
577 val corr_prf' = foldr forall_intr_prf |
577 val corr_prf' = foldr forall_intr_prf |
578 (proof_combt |
578 (proof_combt |
579 (PThm (corr_name name vs', corr_prf, corr_prop, |
579 (PThm (corr_name name vs', corr_prf, corr_prop, |
580 SOME (map TVar (term_tvars corr_prop))), vfs_of corr_prop)) |
580 SOME (map TVar (term_tvars corr_prop))), vfs_of corr_prop)) |
581 (map (get_var_type corr_prop) (vfs_of prop)) |
581 (map (get_var_type corr_prop) (vfs_of prop)) |
582 in |
582 in |
583 ((name, (vs', ((nullt, nullt), (corr_prf, corr_prf')))) :: defs'', |
583 ((name, (vs', ((nullt, nullt), (corr_prf, corr_prf')))) :: defs'', |
584 prf_subst_TVars tye' corr_prf') |
584 prf_subst_TVars tye' corr_prf') |
585 end |
585 end |
586 | SOME (_, (_, prf')) => (defs', prf_subst_TVars tye' prf')) |
586 | SOME (_, (_, prf')) => (defs', prf_subst_TVars tye' prf')) |
685 val corr_prop = Reconstruct.prop_of corr_prf'; |
685 val corr_prop = Reconstruct.prop_of corr_prf'; |
686 val corr_prf'' = foldr forall_intr_prf |
686 val corr_prf'' = foldr forall_intr_prf |
687 (proof_combt |
687 (proof_combt |
688 (PThm (corr_name s vs', corr_prf', corr_prop, |
688 (PThm (corr_name s vs', corr_prf', corr_prop, |
689 SOME (map TVar (term_tvars corr_prop))), vfs_of corr_prop)) |
689 SOME (map TVar (term_tvars corr_prop))), vfs_of corr_prop)) |
690 (map (get_var_type corr_prop) (vfs_of prop)); |
690 (map (get_var_type corr_prop) (vfs_of prop)); |
691 in |
691 in |
692 ((s, (vs', ((t', u), (corr_prf', corr_prf'')))) :: defs'', |
692 ((s, (vs', ((t', u), (corr_prf', corr_prf'')))) :: defs'', |
693 subst_TVars tye' u) |
693 subst_TVars tye' u) |
694 end |
694 end |
695 | SOME ((_, u), _) => (defs, subst_TVars tye' u)) |
695 | SOME ((_, u), _) => (defs, subst_TVars tye' u)) |
731 NONE => |
731 NONE => |
732 let |
732 let |
733 val corr_prop = Reconstruct.prop_of prf; |
733 val corr_prop = Reconstruct.prop_of prf; |
734 val ft = Type.freeze t; |
734 val ft = Type.freeze t; |
735 val fu = Type.freeze u; |
735 val fu = Type.freeze u; |
736 val thy' = if t = nullt then thy else thy |> |
736 val (def_thms, thy') = if t = nullt then ([], thy) else |
737 Theory.add_consts_i [(extr_name s vs, fastype_of ft, NoSyn)] |> |
737 thy |
738 snd o PureThy.add_defs_i false [((extr_name s vs ^ "_def", |
738 |> Theory.add_consts_i [(extr_name s vs, fastype_of ft, NoSyn)] |
739 Logic.mk_equals (head_of (strip_abs_body fu), ft)), [])]; |
739 |> PureThy.add_defs_i false [((extr_name s vs ^ "_def", |
|
740 Logic.mk_equals (head_of (strip_abs_body fu), ft)), [])] |
740 in |
741 in |
741 snd (PureThy.store_thm ((corr_name s vs, |
742 thy' |
742 Thm.varifyT (funpow (length (term_vars corr_prop)) |
743 |> PureThy.store_thm ((corr_name s vs, |
743 (forall_elim_var 0) (forall_intr_frees |
744 Thm.varifyT (funpow (length (term_vars corr_prop)) |
744 (ProofChecker.thm_of_proof thy' |
745 (forall_elim_var 0) (forall_intr_frees |
745 (fst (Proofterm.freeze_thaw_prf prf)))))), []) thy') |
746 (ProofChecker.thm_of_proof thy' |
|
747 (fst (Proofterm.freeze_thaw_prf prf)))))), []) |
|
748 |> snd |
|
749 |> fold (CodegenData.add_func false) def_thms |
746 end |
750 end |
747 | SOME _ => thy); |
751 | SOME _ => thy); |
748 |
752 |
749 in |
753 in |
750 thy |
754 thy |