Quelle XML_Data.thy

Sprache: Isabelle

(* Title: HOL/Proofs/ex/XML_Data.thy
Author: Makarius
Author: Stefan Berghofer

XML data representation of proof terms.
*)

theory XML_Data
imports "HOL-Examples.Drinker"
begin

subsection ‹Export and re-import of global proof terms›

ML ‹
fun export_proof thy thm = thm
|> Proof_Syntax.standard_proof_of {full = true, expand_name = Thm.expand_name thm}
|> Proofterm.encode thy;

fun import_proof thy xml =
let
val prf = Proofterm.decode thy xml;
val (prf', _) = Proofterm.freeze_thaw_prf prf;
in Drule.export_without_context (Proof_Checker.thm_of_proof thy prf') end;
›

subsection ‹Examples›

ML ‹val thy1 = 🍋›

lemma ex: "A ⟶ A" ..

ML_val ‹
val xml = export_proof thy1 @{thm ex};
val thm = import_proof thy1 xml;
›

ML_val ‹
val xml = export_proof thy1 @{thm de_Morgan};
val thm = import_proof thy1 xml;
›

ML_val ‹
val xml = export_proof thy1 @{thm Drinker's_Principle};
val thm = import_proof thy1 xml;
›

text ‹Some fairly large proof:›

ML_val ‹
val xml = export_proof thy1 @{thm Int.times_int.abs_eq};
val thm = import_proof thy1 xml;

val xml_size = Bytes.size (YXML.bytes_of_body xml);
🍋 (xml_size > 10000000);
›

end

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet am 2026-05-03) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.