moved examples to avoid dependency on bulky HOL-Proofs session, e.g. relevant for "isabelle makedist";
authorwenzelm
Fri Feb 19 15:01:38 2016 +0100 (2016-02-19)
changeset 623637b5468422352
parent 62362 e4119d366ab0
child 62364 9209770bdcdf
moved examples to avoid dependency on bulky HOL-Proofs session, e.g. relevant for "isabelle makedist";
src/Doc/Implementation/Logic.thy
src/Doc/ROOT
src/HOL/Proofs/ex/Proof_Terms.thy
src/HOL/ROOT
     1.1 --- a/src/Doc/Implementation/Logic.thy	Fri Feb 19 14:50:12 2016 +0100
     1.2 +++ b/src/Doc/Implementation/Logic.thy	Fri Feb 19 15:01:38 2016 +0100
     1.3 @@ -1248,60 +1248,11 @@
     1.4  \<close>
     1.5  
     1.6  text %mlex \<open>
     1.7 -  Detailed proof information of a theorem may be retrieved as follows:
     1.8 -\<close>
     1.9 -
    1.10 -lemma ex: "A \<and> B \<longrightarrow> B \<and> A"
    1.11 -proof
    1.12 -  assume "A \<and> B"
    1.13 -  then obtain B and A ..
    1.14 -  then show "B \<and> A" ..
    1.15 -qed
    1.16 -
    1.17 -ML_val \<open>
    1.18 -  (*proof body with digest*)
    1.19 -  val body = Proofterm.strip_thm (Thm.proof_body_of @{thm ex});
    1.20 -
    1.21 -  (*proof term only*)
    1.22 -  val prf = Proofterm.proof_of body;
    1.23 -  Pretty.writeln (Proof_Syntax.pretty_proof @{context} prf);
    1.24 -
    1.25 -  (*all theorems used in the graph of nested proofs*)
    1.26 -  val all_thms =
    1.27 -    Proofterm.fold_body_thms
    1.28 -      (fn (name, _, _) => insert (op =) name) [body] [];
    1.29 -\<close>
    1.30 +  \<^item> @{file "~~/src/HOL/Proofs/ex/Proof_Terms.thy"} provides basic examples
    1.31 +  involving proof terms.
    1.32  
    1.33 -text \<open>
    1.34 -  The result refers to various basic facts of Isabelle/HOL: @{thm [source]
    1.35 -  HOL.impI}, @{thm [source] HOL.conjE}, @{thm [source] HOL.conjI} etc. The
    1.36 -  combinator @{ML Proofterm.fold_body_thms} recursively explores the graph of
    1.37 -  the proofs of all theorems being used here.
    1.38 -
    1.39 -  \<^medskip>
    1.40 -  Alternatively, we may produce a proof term manually, and turn it into a
    1.41 -  theorem as follows:
    1.42 -\<close>
    1.43 -
    1.44 -ML_val \<open>
    1.45 -  val thy = @{theory};
    1.46 -  val prf =
    1.47 -    Proof_Syntax.read_proof thy true false
    1.48 -      "impI \<cdot> _ \<cdot> _ \<bullet> \
    1.49 -      \   (\<^bold>\<lambda>H: _. \
    1.50 -      \     conjE \<cdot> _ \<cdot> _ \<cdot> _ \<bullet> H \<bullet> \
    1.51 -      \       (\<^bold>\<lambda>(H: _) Ha: _. conjI \<cdot> _ \<cdot> _ \<bullet> Ha \<bullet> H))";
    1.52 -  val thm =
    1.53 -    prf
    1.54 -    |> Reconstruct.reconstruct_proof thy @{prop "A \<and> B \<longrightarrow> B \<and> A"}
    1.55 -    |> Proof_Checker.thm_of_proof thy
    1.56 -    |> Drule.export_without_context;
    1.57 -\<close>
    1.58 -
    1.59 -text \<open>
    1.60 -  \<^medskip>
    1.61 -  See also @{file "~~/src/HOL/Proofs/ex/XML_Data.thy"} for further examples,
    1.62 -  with export and import of proof terms via XML/ML data representation.
    1.63 +  \<^item> @{file "~~/src/HOL/Proofs/ex/XML_Data.thy"} demonstrates export and import
    1.64 +  of proof terms via XML/ML data representation.
    1.65  \<close>
    1.66  
    1.67  end
     2.1 --- a/src/Doc/ROOT	Fri Feb 19 14:50:12 2016 +0100
     2.2 +++ b/src/Doc/ROOT	Fri Feb 19 15:01:38 2016 +0100
     2.3 @@ -125,7 +125,7 @@
     2.4      "getting.tex"
     2.5      "root.tex"
     2.6  
     2.7 -session Implementation (doc) in "Implementation" = "HOL-Proofs" +
     2.8 +session Implementation (doc) in "Implementation" = "HOL" +
     2.9    options [document_variants = "implementation", quick_and_dirty]
    2.10    theories
    2.11      Eq
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Proofs/ex/Proof_Terms.thy	Fri Feb 19 15:01:38 2016 +0100
     3.3 @@ -0,0 +1,62 @@
     3.4 +(*  Title:      HOL/Proofs/ex/Proof_Terms.thy
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Basic examples involving proof terms.
     3.8 +*)
     3.9 +
    3.10 +theory Proof_Terms
    3.11 +imports Main
    3.12 +begin
    3.13 +
    3.14 +text \<open>
    3.15 +  Detailed proof information of a theorem may be retrieved as follows:
    3.16 +\<close>
    3.17 +
    3.18 +lemma ex: "A \<and> B \<longrightarrow> B \<and> A"
    3.19 +proof
    3.20 +  assume "A \<and> B"
    3.21 +  then obtain B and A ..
    3.22 +  then show "B \<and> A" ..
    3.23 +qed
    3.24 +
    3.25 +ML_val \<open>
    3.26 +  (*proof body with digest*)
    3.27 +  val body = Proofterm.strip_thm (Thm.proof_body_of @{thm ex});
    3.28 +
    3.29 +  (*proof term only*)
    3.30 +  val prf = Proofterm.proof_of body;
    3.31 +  Pretty.writeln (Proof_Syntax.pretty_proof @{context} prf);
    3.32 +
    3.33 +  (*all theorems used in the graph of nested proofs*)
    3.34 +  val all_thms =
    3.35 +    Proofterm.fold_body_thms
    3.36 +      (fn (name, _, _) => insert (op =) name) [body] [];
    3.37 +\<close>
    3.38 +
    3.39 +text \<open>
    3.40 +  The result refers to various basic facts of Isabelle/HOL: @{thm [source]
    3.41 +  HOL.impI}, @{thm [source] HOL.conjE}, @{thm [source] HOL.conjI} etc. The
    3.42 +  combinator @{ML Proofterm.fold_body_thms} recursively explores the graph of
    3.43 +  the proofs of all theorems being used here.
    3.44 +
    3.45 +  \<^medskip>
    3.46 +  Alternatively, we may produce a proof term manually, and turn it into a
    3.47 +  theorem as follows:
    3.48 +\<close>
    3.49 +
    3.50 +ML_val \<open>
    3.51 +  val thy = @{theory};
    3.52 +  val prf =
    3.53 +    Proof_Syntax.read_proof thy true false
    3.54 +      "impI \<cdot> _ \<cdot> _ \<bullet> \
    3.55 +      \   (\<^bold>\<lambda>H: _. \
    3.56 +      \     conjE \<cdot> _ \<cdot> _ \<cdot> _ \<bullet> H \<bullet> \
    3.57 +      \       (\<^bold>\<lambda>(H: _) Ha: _. conjI \<cdot> _ \<cdot> _ \<bullet> Ha \<bullet> H))";
    3.58 +  val thm =
    3.59 +    prf
    3.60 +    |> Reconstruct.reconstruct_proof thy @{prop "A \<and> B \<longrightarrow> B \<and> A"}
    3.61 +    |> Proof_Checker.thm_of_proof thy
    3.62 +    |> Drule.export_without_context;
    3.63 +\<close>
    3.64 +
    3.65 +end
     4.1 --- a/src/HOL/ROOT	Fri Feb 19 14:50:12 2016 +0100
     4.2 +++ b/src/HOL/ROOT	Fri Feb 19 15:01:38 2016 +0100
     4.3 @@ -402,6 +402,7 @@
     4.4    options [document = false, parallel_proofs = 0]
     4.5    theories
     4.6      Hilbert_Classical
     4.7 +    Proof_Terms
     4.8      XML_Data
     4.9  
    4.10  session "HOL-Proofs-Extraction" in "Proofs/Extraction" = "HOL-Proofs" +