src/Pure/Proof/proof_syntax.ML
changeset 71286 4b45d592ce29
parent 71206 be689b7d81fd
child 71288 06c6495fb1d0
equal deleted inserted replaced
71285:77580c977e0c 71286:4b45d592ce29
    12   val read_term: theory -> bool -> typ -> string -> term
    12   val read_term: theory -> bool -> typ -> string -> term
    13   val read_proof: theory -> bool -> bool -> string -> Proofterm.proof
    13   val read_proof: theory -> bool -> bool -> string -> Proofterm.proof
    14   val proof_syntax: Proofterm.proof -> theory -> theory
    14   val proof_syntax: Proofterm.proof -> theory -> theory
    15   val proof_of: bool -> thm -> Proofterm.proof
    15   val proof_of: bool -> thm -> Proofterm.proof
    16   val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T
    16   val pretty_proof: Proof.context -> Proofterm.proof -> Pretty.T
    17   val pretty_standard_proof_of: Proof.context -> bool -> thm -> Pretty.T
       
    18   val pretty_proof_boxes_of: Proof.context ->
    17   val pretty_proof_boxes_of: Proof.context ->
    19     {full: bool, preproc: theory -> proof -> proof} -> thm -> Pretty.T
    18     {full: bool, preproc: theory -> proof -> proof} -> thm -> Pretty.T
       
    19   val standard_proof_of: {full: bool, expand_name: Proofterm.thm_header -> string option} ->
       
    20     thm -> Proofterm.proof
       
    21   val pretty_standard_proof_of: Proof.context -> bool -> thm -> Pretty.T
    20 end;
    22 end;
    21 
    23 
    22 structure Proof_Syntax : PROOF_SYNTAX =
    24 structure Proof_Syntax : PROOF_SYNTAX =
    23 struct
    25 struct
    24 
    26 
   249 fun pretty_proof ctxt prf =
   251 fun pretty_proof ctxt prf =
   250   Proof_Context.pretty_term_abbrev
   252   Proof_Context.pretty_term_abbrev
   251     (Proof_Context.transfer (proof_syntax prf (Proof_Context.theory_of ctxt)) ctxt)
   253     (Proof_Context.transfer (proof_syntax prf (Proof_Context.theory_of ctxt)) ctxt)
   252     (term_of_proof prf);
   254     (term_of_proof prf);
   253 
   255 
   254 fun pretty_standard_proof_of ctxt full thm =
       
   255   pretty_proof ctxt (Thm.standard_proof_of {full = full, expand_name = Thm.expand_name thm} thm);
       
   256 
       
   257 fun pretty_proof_boxes_of ctxt {full, preproc} thm =
   256 fun pretty_proof_boxes_of ctxt {full, preproc} thm =
   258   let
   257   let
   259     val thy = Proof_Context.theory_of ctxt;
   258     val thy = Proof_Context.theory_of ctxt;
   260     val selection =
   259     val selection =
   261       {included = Proofterm.this_id (Thm.derivation_id thm),
   260       {included = Proofterm.this_id (Thm.derivation_id thm),
   278             Syntax.pretty_term ctxt prop', Pretty.fbrk, pretty_proof ctxt proof']
   277             Syntax.pretty_term ctxt prop', Pretty.fbrk, pretty_proof ctxt proof']
   279         end)
   278         end)
   280     |> Pretty.chunks
   279     |> Pretty.chunks
   281   end;
   280   end;
   282 
   281 
   283 end;
   282 
       
   283 (* standardized proofs *)
       
   284 
       
   285 fun standard_proof_of {full, expand_name} thm =
       
   286   let val thy = Thm.theory_of_thm thm in
       
   287     Thm.reconstruct_proof_of thm
       
   288     |> Proofterm.expand_proof thy expand_name
       
   289     |> Proofterm.rew_proof thy
       
   290     |> Proofterm.no_thm_proofs
       
   291     |> not full ? Proofterm.shrink_proof
       
   292   end;
       
   293 
       
   294 fun pretty_standard_proof_of ctxt full thm =
       
   295   pretty_proof ctxt (standard_proof_of {full = full, expand_name = Thm.expand_name thm} thm);
       
   296 
       
   297 end;