support for XML data representation of proof terms;
authorwenzelm
Sun Jun 23 16:47:45 2013 +0200 (2013-06-23)
changeset 5242477075c576d4c
parent 52423 bc5c96c74514
child 52425 de8a85aad216
support for XML data representation of proof terms;
src/HOL/Proofs/ex/XML_Data.thy
src/HOL/ROOT
src/Pure/proofterm.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Proofs/ex/XML_Data.thy	Sun Jun 23 16:47:45 2013 +0200
     1.3 @@ -0,0 +1,47 @@
     1.4 +(*  Title:      HOL/Proofs/ex/XML_Data.thy
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +XML data representation of proof terms.
     1.8 +*)
     1.9 +
    1.10 +theory XML_Data
    1.11 +imports Main
    1.12 +begin
    1.13 +
    1.14 +subsection {* Export and re-import of global proof terms *}
    1.15 +
    1.16 +ML {*
    1.17 +  fun export_proof thm0 =
    1.18 +    let
    1.19 +      val thy = Thm.theory_of_thm thm0;
    1.20 +      val ctxt0 = Proof_Context.init_global thy;
    1.21 +      val thy = Proof_Context.theory_of ctxt0;
    1.22 +      val ((_, [thm]), ctxt) = Variable.import true [Thm.transfer thy thm0] ctxt0;
    1.23 +
    1.24 +      val prop = Thm.prop_of thm;  (* FIXME proper prop (wrt. import / strip) (!??) *)
    1.25 +      val prf =
    1.26 +        Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of thm))
    1.27 +        |> Proofterm.no_thm_proofs;
    1.28 +    in XML.Encode.pair Term_XML.Encode.term Proofterm.encode (prop, prf) end;
    1.29 +
    1.30 +  fun import_proof thy xml =
    1.31 +    let
    1.32 +      val (prop, prf) = XML.Decode.pair Term_XML.Decode.term Proofterm.decode xml;
    1.33 +      val full_prf = Reconstruct.reconstruct_proof thy prop prf;
    1.34 +    in Drule.export_without_context (Proof_Checker.thm_of_proof thy full_prf) end;
    1.35 +*}
    1.36 +
    1.37 +
    1.38 +subsection {* Example *}
    1.39 +
    1.40 +ML {* val thy1 = @{theory} *}
    1.41 +
    1.42 +lemma ex: "A \<longrightarrow> A" ..
    1.43 +
    1.44 +ML {*
    1.45 +  val xml = export_proof @{thm ex};
    1.46 +  val thm = import_proof thy1 xml;
    1.47 +*}
    1.48 +
    1.49 +end
    1.50 +
     2.1 --- a/src/HOL/ROOT	Sun Jun 23 14:26:49 2013 +0200
     2.2 +++ b/src/HOL/ROOT	Sun Jun 23 16:47:45 2013 +0200
     2.3 @@ -357,7 +357,9 @@
     2.4  
     2.5  session "HOL-Proofs-ex" in "Proofs/ex" = "HOL-Proofs" +
     2.6    options [document = false, proofs = 2, skip_proofs = false, parallel_proofs = 0]
     2.7 -  theories Hilbert_Classical
     2.8 +  theories
     2.9 +    Hilbert_Classical
    2.10 +    XML_Data
    2.11  
    2.12  session "HOL-Proofs-Extraction" in "Proofs/Extraction" = "HOL-Proofs" +
    2.13    description {*
     3.1 --- a/src/Pure/proofterm.ML	Sun Jun 23 14:26:49 2013 +0200
     3.2 +++ b/src/Pure/proofterm.ML	Sun Jun 23 16:47:45 2013 +0200
     3.3 @@ -50,6 +50,13 @@
     3.4    val unions_thms: pthm Ord_List.T list -> pthm Ord_List.T
     3.5    val all_oracles_of: proof_body -> oracle Ord_List.T
     3.6    val approximate_proof_body: proof -> proof_body
     3.7 +  val no_proof_body: proof_body
     3.8 +  val no_thm_proofs: proof -> proof
     3.9 +
    3.10 +  val encode: proof XML.Encode.T
    3.11 +  val encode_body: proof_body XML.Encode.T
    3.12 +  val decode: proof XML.Decode.T
    3.13 +  val decode_body: proof_body XML.Decode.T
    3.14  
    3.15    (** primitive operations **)
    3.16    val proofs_enabled: unit -> bool
    3.17 @@ -265,6 +272,87 @@
    3.18        proof = prf}
    3.19    end;
    3.20  
    3.21 +val no_proof_body = PBody {oracles = [], thms = [], proof = MinProof};
    3.22 +val no_body = Future.value no_proof_body;
    3.23 +
    3.24 +fun no_thm_proofs (PThm (i, (a, _))) = PThm (i, (a, no_body))
    3.25 +  | no_thm_proofs (Abst (x, T, prf)) = Abst (x, T, no_thm_proofs prf)
    3.26 +  | no_thm_proofs (AbsP (x, t, prf)) = AbsP (x, t, no_thm_proofs prf)
    3.27 +  | no_thm_proofs (prf % t) = no_thm_proofs prf % t
    3.28 +  | no_thm_proofs (prf1 %% prf2) = no_thm_proofs prf1 %% no_thm_proofs prf2
    3.29 +  | no_thm_proofs a = a;
    3.30 +
    3.31 +
    3.32 +(***** XML data representation *****)
    3.33 +
    3.34 +(* encode *)
    3.35 +
    3.36 +local
    3.37 +
    3.38 +open XML.Encode Term_XML.Encode;
    3.39 +
    3.40 +fun proof prf = prf |> variant
    3.41 + [fn MinProof => ([], []),
    3.42 +  fn PBound a => ([int_atom a], []),
    3.43 +  fn Abst (a, b, c) => ([a], pair (option typ) proof (b, c)),
    3.44 +  fn AbsP (a, b, c) => ([a], pair (option term) proof (b, c)),
    3.45 +  fn a % b => ([], pair proof (option term) (a, b)),
    3.46 +  fn a %% b => ([], pair proof proof (a, b)),
    3.47 +  fn Hyp a => ([], term a),
    3.48 +  fn PAxm (a, b, c) => ([a], pair term (option (list typ)) (b, c)),
    3.49 +  fn OfClass (a, b) => ([b], typ a),
    3.50 +  fn Oracle (a, b, c) => ([a], pair term (option (list typ)) (b, c)),
    3.51 +  fn Promise (a, b, c) => ([int_atom a], pair term (list typ) (b, c)),
    3.52 +  fn PThm (a, ((b, c, d), body)) =>
    3.53 +    ([int_atom a, b], triple term (option (list typ)) proof_body (c, d, Future.join body))]
    3.54 +and proof_body (PBody {oracles, thms, proof = prf}) =
    3.55 +  triple (list (pair string term)) (list pthm) proof (oracles, thms, prf)
    3.56 +and pthm (a, (b, c, body)) =
    3.57 +  pair int (triple string term proof_body) (a, (b, c, Future.join body));
    3.58 +
    3.59 +in
    3.60 +
    3.61 +val encode = proof;
    3.62 +val encode_body = proof_body;
    3.63 +
    3.64 +end;
    3.65 +
    3.66 +
    3.67 +(* decode *)
    3.68 +
    3.69 +local
    3.70 +
    3.71 +open XML.Decode Term_XML.Decode;
    3.72 +
    3.73 +fun proof prf = prf |> variant
    3.74 + [fn ([], []) => MinProof,
    3.75 +  fn ([a], []) => PBound (int_atom a),
    3.76 +  fn ([a], b) => let val (c, d) = pair (option typ) proof b in Abst (a, c, d) end,
    3.77 +  fn ([a], b) => let val (c, d) = pair (option term) proof b in AbsP (a, c, d) end,
    3.78 +  fn ([], a) => op % (pair proof (option term) a),
    3.79 +  fn ([], a) => op %% (pair proof proof a),
    3.80 +  fn ([], a) => Hyp (term a),
    3.81 +  fn ([a], b) => let val (c, d) = pair term (option (list typ)) b in PAxm (a, c, d) end,
    3.82 +  fn ([b], a) => OfClass (typ a, b),
    3.83 +  fn ([a], b) => let val (c, d) = pair term (option (list typ)) b in Oracle (a, c, d) end,
    3.84 +  fn ([a], b) => let val (c, d) = pair term (list typ) b in Promise (int_atom a, c, d) end,
    3.85 +  fn ([a, b], c) =>
    3.86 +    let val (d, e, f) = triple term (option (list typ)) proof_body c
    3.87 +    in PThm (int_atom a, ((b, d, e), Future.value f)) end]
    3.88 +and proof_body x =
    3.89 +  let val (a, b, c) = triple (list (pair string term)) (list pthm) proof x
    3.90 +  in PBody {oracles = a, thms = b, proof = c} end
    3.91 +and pthm x =
    3.92 +  let val (a, (b, c, d)) = pair int (triple string term proof_body) x
    3.93 +  in (a, (b, c, Future.value d)) end;
    3.94 +
    3.95 +in
    3.96 +
    3.97 +val decode = proof;
    3.98 +val decode_body = proof_body;
    3.99 +
   3.100 +end;
   3.101 +
   3.102  
   3.103  (***** proof objects with different levels of detail *****)
   3.104