789 |
789 |
790 fun OfClasst (T, c) = |
790 fun OfClasst (T, c) = |
791 let val U = Term.itselfT T --> propT |
791 let val U = Term.itselfT T --> propT |
792 in Const ("Pure.OfClass", U --> proofT) $ Const (Logic.const_of_class c, U) end; |
792 in Const ("Pure.OfClass", U --> proofT) $ Const (Logic.const_of_class c, U) end; |
793 |
793 |
794 fun term_of _ (PThm (_, ((name, _, Ts, _), _))) = |
|
795 fold AppT (these Ts) (Const (Long_Name.append "thm" name, proofT)) |
|
796 | term_of _ (PAxm (name, _, Ts)) = |
|
797 fold AppT (these Ts) (Const (Long_Name.append "axm" name, proofT)) |
|
798 | term_of _ (OfClass (T, c)) = AppT T (OfClasst (T, c)) |
|
799 | term_of _ (PBound i) = Bound i |
|
800 | term_of Ts (Abst (s, opT, prf)) = |
|
801 let val T = the_default dummyT opT in |
|
802 Const ("Pure.Abst", (T --> proofT) --> proofT) $ |
|
803 Abs (s, T, term_of (T::Ts) (incr_pboundvars 1 0 prf)) |
|
804 end |
|
805 | term_of Ts (AbsP (s, t, prf)) = |
|
806 AbsPt $ the_default Term.dummy_prop t $ |
|
807 Abs (s, proofT, term_of (proofT::Ts) (incr_pboundvars 0 1 prf)) |
|
808 | term_of Ts (prf1 %% prf2) = |
|
809 AppPt $ term_of Ts prf1 $ term_of Ts prf2 |
|
810 | term_of Ts (prf % opt) = |
|
811 let |
|
812 val t = the_default Term.dummy opt; |
|
813 val T = fastype_of1 (Ts, t) handle TERM _ => dummyT; |
|
814 in Const ("Pure.Appt", proofT --> T --> proofT) $ term_of Ts prf $ t end |
|
815 | term_of _ (Hyp t) = Hypt $ t |
|
816 | term_of _ (Oracle (_, t, _)) = Oraclet $ t |
|
817 | term_of _ MinProof = MinProoft; |
|
818 |
|
819 in |
794 in |
820 |
795 |
821 val term_of_proof = term_of []; |
796 fun thm_const_default (_: proof_serial) name = Long_Name.append "thm" name; |
|
797 fun axm_const_default name = Long_Name.append "axm" name; |
|
798 |
|
799 fun term_of |
|
800 {thm_const: proof_serial -> string -> string, |
|
801 axm_const: string -> string} = |
|
802 let |
|
803 fun term _ (PThm (i, ((name, _, Ts, _), _))) = |
|
804 fold AppT (these Ts) (Const (thm_const i name, proofT)) |
|
805 | term _ (PAxm (name, _, Ts)) = |
|
806 fold AppT (these Ts) (Const (axm_const name, proofT)) |
|
807 | term _ (OfClass (T, c)) = AppT T (OfClasst (T, c)) |
|
808 | term _ (PBound i) = Bound i |
|
809 | term Ts (Abst (s, opT, prf)) = |
|
810 let val T = the_default dummyT opT in |
|
811 Const ("Pure.Abst", (T --> proofT) --> proofT) $ |
|
812 Abs (s, T, term (T::Ts) (incr_pboundvars 1 0 prf)) |
|
813 end |
|
814 | term Ts (AbsP (s, t, prf)) = |
|
815 AbsPt $ the_default Term.dummy_prop t $ |
|
816 Abs (s, proofT, term (proofT::Ts) (incr_pboundvars 0 1 prf)) |
|
817 | term Ts (prf1 %% prf2) = |
|
818 AppPt $ term Ts prf1 $ term Ts prf2 |
|
819 | term Ts (prf % opt) = |
|
820 let |
|
821 val t = the_default Term.dummy opt; |
|
822 val T = fastype_of1 (Ts, t) handle TERM _ => dummyT; |
|
823 in Const ("Pure.Appt", proofT --> T --> proofT) $ term Ts prf $ t end |
|
824 | term _ (Hyp t) = Hypt $ t |
|
825 | term _ (Oracle (_, t, _)) = Oraclet $ t |
|
826 | term _ MinProof = MinProoft; |
|
827 in term [] end; |
|
828 |
|
829 val term_of_proof = term_of {thm_const = thm_const_default, axm_const = axm_const_default}; |
822 |
830 |
823 end; |
831 end; |
824 |
832 |
825 |
833 |
826 |
834 |
2014 #> fold_rev (implies_intr_proof o snd) (#constraints ucontext) |
2022 #> fold_rev (implies_intr_proof o snd) (#constraints ucontext) |
2015 end; |
2023 end; |
2016 |
2024 |
2017 fun clean_proof thy = rew_proof thy #> shrink_proof; |
2025 fun clean_proof thy = rew_proof thy #> shrink_proof; |
2018 |
2026 |
|
2027 val export_proof_term = |
|
2028 term_of {thm_const = K o string_of_int, axm_const = axm_const_default}; |
|
2029 |
|
2030 fun export_proof thy main_prop main_proof = |
|
2031 let |
|
2032 fun add_proof_boxes (AbsP (_, _, prf)) = add_proof_boxes prf |
|
2033 | add_proof_boxes (Abst (_, _, prf)) = add_proof_boxes prf |
|
2034 | add_proof_boxes (prf1 %% prf2) = add_proof_boxes prf1 #> add_proof_boxes prf2 |
|
2035 | add_proof_boxes (prf % _) = add_proof_boxes prf |
|
2036 | add_proof_boxes (PThm (i, (("", prop, _, open_proof), body))) = |
|
2037 (fn boxes => |
|
2038 if Inttab.defined boxes i then boxes |
|
2039 else |
|
2040 let val prf = open_proof (join_proof body) |> reconstruct_proof thy prop; |
|
2041 in add_proof_boxes prf boxes |> Inttab.update (i, prf) end) |
|
2042 | add_proof_boxes _ = I; |
|
2043 |
|
2044 val proof = reconstruct_proof thy main_prop main_proof; |
|
2045 val proof_boxes = |
|
2046 (proof, Inttab.empty) |-> add_proof_boxes |> Inttab.dest |
|
2047 |> map (apsnd export_proof_term); |
|
2048 in (proof_boxes, export_proof_term proof) end; |
|
2049 |
2019 fun export thy i prop proof = |
2050 fun export thy i prop proof = |
2020 if Options.default_bool "export_proofs" then |
2051 if Options.default_bool "export_proofs" then |
2021 let |
2052 let |
2022 val xml = |
2053 val xml = export_proof thy prop proof |
2023 reconstruct_proof thy prop proof |
2054 |> let open XML.Encode Term_XML.Encode in pair (list (pair int term)) term end; |
2024 |> expand_proof thy [("", NONE)] |
|
2025 |> term_of_proof |
|
2026 |> Term_XML.Encode.term; |
|
2027 in |
2055 in |
2028 Export.export thy (Path.binding0 (Path.make ["proofs", string_of_int i])) |
2056 Export.export thy (Path.binding0 (Path.make ["proofs", string_of_int i])) |
2029 (Buffer.chunks (YXML.buffer_body xml Buffer.empty)) |
2057 (Buffer.chunks (YXML.buffer_body xml Buffer.empty)) |
2030 end |
2058 end |
2031 else (); |
2059 else (); |