src/Doc/IsarImplementation/Logic.thy
 changeset 52410 fb1fb867c146 parent 52408 fa2dc6c6c94f child 52411 f192c4ea5b17
     1.1 --- a/src/Doc/IsarImplementation/Logic.thy	Sat Jun 15 21:07:32 2013 +0200
1.2 +++ b/src/Doc/IsarImplementation/Logic.thy	Mon Jun 17 19:30:41 2013 +0200
1.3 @@ -1314,4 +1314,107 @@
1.4    \end{description}
1.5  *}
1.6
1.7 +text %mlex {* Detailed proof information of a theorem may be retrieved
1.8 +  as follows: *}
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 {*
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 +*}
1.30 +
1.31 +text {* The result refers to various basic facts of Isabelle/HOL:
1.32 +  @{thm [source] HOL.impI}, @{thm [source] HOL.conjE}, @{thm [source]
1.33 +  HOL.conjI} etc.  The combinator @{ML Proofterm.fold_body_thms}
1.34 +  recursively explores the graph of the proofs of all theorems being
1.35 +  used here.
1.36 +
1.37 +  \medskip Alternatively, we may produce a proof term manually, and
1.38 +  turn it into a theorem as follows: *}
1.39 +
1.40 +ML_val {*
1.41 +  val thy = @{theory};
1.42 +  val prf =
1.43 +    Proof_Syntax.read_proof thy true false
1.44 +      "impI \<cdot> _ \<cdot> _ \<bullet> \
1.45 +      \   (Lam H: _. \
1.46 +      \     conjE \<cdot> _ \<cdot> _ \<cdot> _ \<bullet> H \<bullet> \
1.47 +      \       (Lam (H: _) Ha: _. conjI \<cdot> _ \<cdot> _ \<bullet> Ha \<bullet> H))";
1.48 +  val thm =
1.49 +    prf
1.50 +    |> Reconstruct.reconstruct_proof thy @{prop "A \<and> B \<longrightarrow> B \<and> A"}
1.51 +    |> Proof_Checker.thm_of_proof thy
1.52 +    |> Drule.export_without_context;
1.53 +*}
1.54 +
1.55 +text {* \medskip The subsequent example illustrates the use of various
1.56 +  key operations on proof terms: the proof term of an existing theorem
1.57 +  is reconstructed and turned again into a theorem using the proof
1.58 +  checker; some informative output is printed as well.  *}
1.59 +
1.60 +ML {*
1.61 +  fun recheck ctxt0 thm0 =
1.62 +    let
1.63 +      (*formal transfer and import -- avoid schematic variables*)
1.64 +      val thy = Proof_Context.theory_of ctxt0;
1.65 +      val ((_, [thm]), ctxt) =
1.66 +        Variable.import true [Thm.transfer thy thm0] ctxt0;
1.67 +
1.68 +      (*main proof information*)
1.69 +      val prop = Thm.prop_of thm;
1.70 +      val prf =
1.71 +        Proofterm.proof_of
1.72 +          (Proofterm.strip_thm (Thm.proof_body_of thm));
1.73 +      val full_prf = Reconstruct.reconstruct_proof thy prop prf;
1.74 +
1.75 +      (*informative output*)
1.76 +      fun pretty_item name prt =
1.77 +        Pretty.block [Pretty.str name, Pretty.brk 1, prt];
1.78 +      val _ =
1.79 +        [pretty_item "proposition:" (Syntax.pretty_term ctxt prop),
1.80 +         pretty_item "proof:" (Proof_Syntax.pretty_proof ctxt prf),
1.81 +         pretty_item "full proof:"
1.82 +          (Proof_Syntax.pretty_proof ctxt full_prf)]
1.83 +        |> Pretty.chunks |> Pretty.writeln;
1.84 +
1.85 +      (*rechecked theorem*)
1.86 +      val thm' =
1.87 +        Proof_Checker.thm_of_proof thy full_prf
1.88 +        |> singleton (Proof_Context.export ctxt ctxt0);
1.89 +    in thm' end;
1.90 +*}
1.91 +
1.92 +text {* As anticipated, the rechecked theorem establishes the same
1.93 +  proposition: *}
1.94 +
1.95 +ML_val {*
1.96 +  val thm = @{thm ex};
1.97 +  val thm' = recheck @{context} thm;
1.98 +  @{assert} (Thm.eq_thm_prop (thm, thm'));
1.99 +*}
1.100 +
1.101 +text {* More precise theorem equality is achieved by adjusting a few
1.102 +  accidental details of the theorems involved here: *}
1.103 +
1.104 +ML_val {*
1.105 +  val thm = Thm.map_tags (K []) @{thm ex};
1.106 +  val thm' = Thm.strip_shyps (recheck @{context} thm);
1.107 +  @{assert} (Thm.eq_thm (thm, thm'));
1.108 +*}
1.109 +
1.110  end