more informative 'prf' and 'full_prf', based on HOL/Proofs/ex/XML_Data.thy;
authorwenzelm
Sat Aug 06 18:14:59 2016 +0200 (2016-08-06 ago)
changeset 63624994d1a1105ef
parent 63623 1a38142e1172
child 63625 1e7c5bbea36d
more informative 'prf' and 'full_prf', based on HOL/Proofs/ex/XML_Data.thy;
NEWS
src/Doc/Isar_Ref/Inner_Syntax.thy
src/Pure/Isar/isar_cmd.ML
     1.1 --- a/NEWS	Sat Aug 06 17:39:21 2016 +0200
     1.2 +++ b/NEWS	Sat Aug 06 18:14:59 2016 +0200
     1.3 @@ -57,6 +57,9 @@
     1.4  theory imports that merge Pure with e.g. Main of Isabelle/HOL: the order
     1.5  is relevant to avoid confusion of Pure.simp vs. HOL.simp.
     1.6  
     1.7 +* Commands 'prf' and 'full_prf' are somewhat more informative (again):
     1.8 +proof terms are reconstructed and cleaned from administrative thm nodes.
     1.9 +
    1.10  
    1.11  *** Prover IDE -- Isabelle/Scala/jEdit ***
    1.12  
     2.1 --- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Sat Aug 06 17:39:21 2016 +0200
     2.2 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Sat Aug 06 18:14:59 2016 +0200
     2.3 @@ -84,10 +84,8 @@
     2.4      \<open>a\<^sub>1, \<dots>, a\<^sub>n\<close> do not have any permanent effect.
     2.5  
     2.6      \<^descr> @{command "prf"} displays the (compact) proof term of the current proof
     2.7 -    state (if present), or of the given theorems. Note that this requires
     2.8 -    proof terms to be switched on for the current object logic (see the
     2.9 -    ``Proof terms'' section of the Isabelle reference manual for information
    2.10 -    on how to do this).
    2.11 +    state (if present), or of the given theorems. Note that this requires an
    2.12 +    underlying logic image with proof terms enabled, e.g. \<open>HOL-Proofs\<close>.
    2.13  
    2.14      \<^descr> @{command "full_prf"} is like @{command "prf"}, but displays the full
    2.15      proof term, i.e.\ also displays information omitted in the compact proof
     3.1 --- a/src/Pure/Isar/isar_cmd.ML	Sat Aug 06 17:39:21 2016 +0200
     3.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sat Aug 06 18:14:59 2016 +0200
     3.3 @@ -258,9 +258,24 @@
     3.4              (if full then Reconstruct.reconstruct_proof ctxt prop prf' else prf')
     3.5          end
     3.6      | SOME srcs =>
     3.7 -        let val ctxt = Toplevel.context_of state
     3.8 -        in map (Proof_Syntax.pretty_proof_of ctxt full) (Attrib.eval_thms ctxt srcs) end
     3.9 -        |> Pretty.chunks);
    3.10 +        let
    3.11 +          val ctxt = Toplevel.context_of state;
    3.12 +          val thy = Proof_Context.theory_of ctxt;
    3.13 +          fun pretty_proof thm =
    3.14 +            let
    3.15 +              val (_, prop) =
    3.16 +                Logic.unconstrainT (Thm.shyps_of thm)
    3.17 +                  (Logic.list_implies (Thm.hyps_of thm, Thm.prop_of thm));
    3.18 +            in
    3.19 +              Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of thm))
    3.20 +              |> Reconstruct.reconstruct_proof ctxt prop
    3.21 +              |> Reconstruct.expand_proof ctxt [("", NONE)]
    3.22 +              |> Proofterm.rew_proof thy
    3.23 +              |> Proofterm.no_thm_proofs
    3.24 +              |> not full ? Proofterm.shrink_proof
    3.25 +              |> Proof_Syntax.pretty_proof ctxt
    3.26 +            end;
    3.27 +        in Pretty.chunks (map pretty_proof (Attrib.eval_thms ctxt srcs)) end);
    3.28  
    3.29  fun string_of_prop ctxt s =
    3.30    let