more uniform use of Reconstruct.clean_proof_of;
authorwenzelm
Sat Feb 04 21:15:11 2017 +0100 (2017-02-04 ago)
changeset 64986b81a048960a3
parent 64985 69592ac04836
child 64987 1985502518ce
more uniform use of Reconstruct.clean_proof_of;
NEWS
src/HOL/Proofs/ex/Proof_Terms.thy
src/HOL/Proofs/ex/XML_Data.thy
src/Pure/Isar/isar_cmd.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/Proof/reconstruct.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/NEWS	Sat Feb 04 20:12:27 2017 +0100
     1.2 +++ b/NEWS	Sat Feb 04 21:15:11 2017 +0100
     1.3 @@ -7,6 +7,12 @@
     1.4  New in this Isabelle version
     1.5  ----------------------------
     1.6  
     1.7 +*** General ***
     1.8 +
     1.9 +* Document antiquotations @{prf} and @{full_prf} output proof terms
    1.10 +(again) in the same way as commands 'prf' and 'full_prf'.
    1.11 +
    1.12 +
    1.13  *** Prover IDE -- Isabelle/Scala/jEdit ***
    1.14  
    1.15  * Command-line invocation "isabelle jedit -R -l LOGIC" opens the ROOT
     2.1 --- a/src/HOL/Proofs/ex/Proof_Terms.thy	Sat Feb 04 20:12:27 2017 +0100
     2.2 +++ b/src/HOL/Proofs/ex/Proof_Terms.thy	Sat Feb 04 21:15:11 2017 +0100
     2.3 @@ -20,12 +20,17 @@
     2.4  qed
     2.5  
     2.6  ML_val \<open>
     2.7 +  val thm = @{thm ex};
     2.8 +
     2.9    (*proof body with digest*)
    2.10 -  val body = Proofterm.strip_thm (Thm.proof_body_of @{thm ex});
    2.11 +  val body = Proofterm.strip_thm (Thm.proof_body_of thm);
    2.12  
    2.13    (*proof term only*)
    2.14    val prf = Proofterm.proof_of body;
    2.15 -  Pretty.writeln (Proof_Syntax.pretty_proof @{context} prf);
    2.16 +
    2.17 +  (*clean output*)
    2.18 +  Pretty.writeln (Proof_Syntax.pretty_clean_proof_of @{context} false thm);
    2.19 +  Pretty.writeln (Proof_Syntax.pretty_clean_proof_of @{context} true thm);
    2.20  
    2.21    (*all theorems used in the graph of nested proofs*)
    2.22    val all_thms =
     3.1 --- a/src/HOL/Proofs/ex/XML_Data.thy	Sat Feb 04 20:12:27 2017 +0100
     3.2 +++ b/src/HOL/Proofs/ex/XML_Data.thy	Sat Feb 04 21:15:11 2017 +0100
     3.3 @@ -6,25 +6,14 @@
     3.4  *)
     3.5  
     3.6  theory XML_Data
     3.7 -imports "~~/src/HOL/Isar_Examples/Drinker"
     3.8 +  imports "~~/src/HOL/Isar_Examples/Drinker"
     3.9  begin
    3.10  
    3.11  subsection \<open>Export and re-import of global proof terms\<close>
    3.12  
    3.13  ML \<open>
    3.14    fun export_proof ctxt thm =
    3.15 -    let
    3.16 -      val thy = Proof_Context.theory_of ctxt;
    3.17 -      val (_, prop) =
    3.18 -        Logic.unconstrainT (Thm.shyps_of thm)
    3.19 -          (Logic.list_implies (Thm.hyps_of thm, Thm.prop_of thm));
    3.20 -      val prf =
    3.21 -        Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of thm)) |>
    3.22 -        Reconstruct.reconstruct_proof ctxt prop |>
    3.23 -        Reconstruct.expand_proof ctxt [("", NONE)] |>
    3.24 -        Proofterm.rew_proof thy |>
    3.25 -        Proofterm.no_thm_proofs;
    3.26 -    in Proofterm.encode prf end;
    3.27 +    Proofterm.encode (Reconstruct.clean_proof_of ctxt true thm);
    3.28  
    3.29    fun import_proof thy xml =
    3.30      let
     4.1 --- a/src/Pure/Isar/isar_cmd.ML	Sat Feb 04 20:12:27 2017 +0100
     4.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sat Feb 04 21:15:11 2017 +0100
     4.3 @@ -260,21 +260,7 @@
     4.4      | SOME srcs =>
     4.5          let
     4.6            val ctxt = Toplevel.context_of state;
     4.7 -          val thy = Proof_Context.theory_of ctxt;
     4.8 -          fun pretty_proof thm =
     4.9 -            let
    4.10 -              val (_, prop) =
    4.11 -                Logic.unconstrainT (Thm.shyps_of thm)
    4.12 -                  (Logic.list_implies (Thm.hyps_of thm, Thm.prop_of thm));
    4.13 -            in
    4.14 -              Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of thm))
    4.15 -              |> Reconstruct.reconstruct_proof ctxt prop
    4.16 -              |> Reconstruct.expand_proof ctxt [("", NONE)]
    4.17 -              |> Proofterm.rew_proof thy
    4.18 -              |> Proofterm.no_thm_proofs
    4.19 -              |> not full ? Proofterm.shrink_proof
    4.20 -              |> Proof_Syntax.pretty_proof ctxt
    4.21 -            end;
    4.22 +          val pretty_proof = Proof_Syntax.pretty_clean_proof_of ctxt full;
    4.23          in Pretty.chunks (map pretty_proof (Attrib.eval_thms ctxt srcs)) end);
    4.24  
    4.25  fun string_of_prop ctxt s =
     5.1 --- a/src/Pure/Proof/proof_syntax.ML	Sat Feb 04 20:12:27 2017 +0100
     5.2 +++ b/src/Pure/Proof/proof_syntax.ML	Sat Feb 04 21:15:11 2017 +0100
     5.3 @@ -16,7 +16,7 @@
     5.4    val proof_syntax: Proofterm.proof -> theory -> theory
     5.5    val proof_of: Proof.context -> bool -> thm -> Proofterm.proof
     5.6    val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T
     5.7 -  val pretty_proof_of: Proof.context -> bool -> thm -> Pretty.T
     5.8 +  val pretty_clean_proof_of: Proof.context -> bool -> thm -> Pretty.T
     5.9  end;
    5.10  
    5.11  structure Proof_Syntax : PROOF_SYNTAX =
    5.12 @@ -259,7 +259,7 @@
    5.13      (Proof_Context.transfer (proof_syntax prf (Proof_Context.theory_of ctxt)) ctxt)
    5.14      (term_of_proof prf);
    5.15  
    5.16 -fun pretty_proof_of ctxt full th =
    5.17 -  pretty_proof ctxt (proof_of ctxt full th);
    5.18 +fun pretty_clean_proof_of ctxt full thm =
    5.19 +  pretty_proof ctxt (Reconstruct.clean_proof_of ctxt full thm);
    5.20  
    5.21  end;
     6.1 --- a/src/Pure/Proof/reconstruct.ML	Sat Feb 04 20:12:27 2017 +0100
     6.2 +++ b/src/Pure/Proof/reconstruct.ML	Sat Feb 04 21:15:11 2017 +0100
     6.3 @@ -13,6 +13,7 @@
     6.4    val proof_of : Proof.context -> thm -> Proofterm.proof
     6.5    val expand_proof : Proof.context -> (string * term option) list ->
     6.6      Proofterm.proof -> Proofterm.proof
     6.7 +  val clean_proof_of : Proof.context -> bool -> thm -> Proofterm.proof
     6.8  end;
     6.9  
    6.10  structure Reconstruct : RECONSTRUCT =
    6.11 @@ -388,4 +389,21 @@
    6.12  
    6.13    in #3 (expand (Proofterm.maxidx_proof prf ~1) [] prf) end;
    6.14  
    6.15 +
    6.16 +(* cleanup for output etc. *)
    6.17 +
    6.18 +fun clean_proof_of ctxt full thm =
    6.19 +  let
    6.20 +    val (_, prop) =
    6.21 +      Logic.unconstrainT (Thm.shyps_of thm)
    6.22 +        (Logic.list_implies (Thm.hyps_of thm, Thm.prop_of thm));
    6.23 +  in
    6.24 +    Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of thm))
    6.25 +    |> reconstruct_proof ctxt prop
    6.26 +    |> expand_proof ctxt [("", NONE)]
    6.27 +    |> Proofterm.rew_proof (Proof_Context.theory_of ctxt)
    6.28 +    |> Proofterm.no_thm_proofs
    6.29 +    |> not full ? Proofterm.shrink_proof
    6.30 +  end;
    6.31 +
    6.32  end;
     7.1 --- a/src/Pure/Thy/thy_output.ML	Sat Feb 04 20:12:27 2017 +0100
     7.2 +++ b/src/Pure/Thy/thy_output.ML	Sat Feb 04 21:15:11 2017 +0100
     7.3 @@ -584,7 +584,7 @@
     7.4    let val Type (name, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s
     7.5    in Pretty.str (Proof_Context.extern_type ctxt name) end;
     7.6  
     7.7 -fun pretty_prf full ctxt = Proof_Syntax.pretty_proof_of ctxt full;
     7.8 +fun pretty_prf full ctxt = Proof_Syntax.pretty_clean_proof_of ctxt full;
     7.9  
    7.10  fun pretty_theory ctxt (name, pos) = (Theory.check ctxt (name, pos); Pretty.str name);
    7.11