ProgTutorial/Recipes/Introspection.thy
author Norbert Schirmer <norbert.schirmer@web.de>
Tue, 14 May 2019 17:45:13 +0200
changeset 566 6103b0eadbf2
parent 565 cecd7a941885
child 567 f7c97e64cc2a
permissions -rw-r--r--
tuned parser for patterns in ML_response... antiquotations
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
525
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     1
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     2
theory Introspection
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     3
imports "../Appendix"
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     4
begin
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     5
565
cecd7a941885 isabelle update_cartouches -t
Norbert Schirmer <norbert.schirmer@web.de>
parents: 562
diff changeset
     6
section \<open>Introspection of Theorems and Proofs \label{rec:introspection}\<close>
525
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     7
565
cecd7a941885 isabelle update_cartouches -t
Norbert Schirmer <norbert.schirmer@web.de>
parents: 562
diff changeset
     8
text\<open>
525
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     9
  {\bf Problem:} 
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    10
  How to obtain all theorems that are used in the proof of a theorem?\smallskip
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    11
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    12
  {\bf Solution:} They can be obtained by introspecting the theorem.\smallskip
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    13
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    14
  To introspect a theorem, let us define the following three functions that 
528
e2c0138b5cea polished
Christian Urban <urbanc@in.tum.de>
parents: 527
diff changeset
    15
  analyse the @{ML_type_ind proof_body} data-structure from the structure 
527
efe63c062e48 polished introspection section
Christian Urban <urbanc@in.tum.de>
parents: 525
diff changeset
    16
  @{ML_struct Proofterm}.
565
cecd7a941885 isabelle update_cartouches -t
Norbert Schirmer <norbert.schirmer@web.de>
parents: 562
diff changeset
    17
\<close>
525
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    18
565
cecd7a941885 isabelle update_cartouches -t
Norbert Schirmer <norbert.schirmer@web.de>
parents: 562
diff changeset
    19
ML %grayML\<open>fun pthms_of (PBody {thms, ...}) = map #2 thms 
562
daf404920ab9 Accomodate to Isabelle 2018
Norbert Schirmer <norbert.schirmer@web.de>
parents: 529
diff changeset
    20
val get_names = (map Proofterm.thm_node_name) o pthms_of 
565
cecd7a941885 isabelle update_cartouches -t
Norbert Schirmer <norbert.schirmer@web.de>
parents: 562
diff changeset
    21
val get_pbodies = map (Future.join o Proofterm.thm_node_body) o pthms_of\<close>
525
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    22
565
cecd7a941885 isabelle update_cartouches -t
Norbert Schirmer <norbert.schirmer@web.de>
parents: 562
diff changeset
    23
text \<open>
527
efe63c062e48 polished introspection section
Christian Urban <urbanc@in.tum.de>
parents: 525
diff changeset
    24
  To see what their purpose is, consider the following three short proofs.
565
cecd7a941885 isabelle update_cartouches -t
Norbert Schirmer <norbert.schirmer@web.de>
parents: 562
diff changeset
    25
\<close>
525
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    26
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    27
lemma my_conjIa:
528
e2c0138b5cea polished
Christian Urban <urbanc@in.tum.de>
parents: 527
diff changeset
    28
shows "A \<and> B \<Longrightarrow> A \<and> B"
525
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    29
apply(rule conjI)
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    30
apply(drule conjunct1)
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    31
apply(assumption)
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    32
apply(drule conjunct2)
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    33
apply(assumption)
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    34
done
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    35
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    36
lemma my_conjIb:
528
e2c0138b5cea polished
Christian Urban <urbanc@in.tum.de>
parents: 527
diff changeset
    37
shows "A \<and> B \<Longrightarrow> A \<and> B"
525
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    38
apply(assumption)
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    39
done
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    40
527
efe63c062e48 polished introspection section
Christian Urban <urbanc@in.tum.de>
parents: 525
diff changeset
    41
lemma my_conjIc:
528
e2c0138b5cea polished
Christian Urban <urbanc@in.tum.de>
parents: 527
diff changeset
    42
shows "A \<and> B \<Longrightarrow> A \<and> B"
527
efe63c062e48 polished introspection section
Christian Urban <urbanc@in.tum.de>
parents: 525
diff changeset
    43
apply(auto)
efe63c062e48 polished introspection section
Christian Urban <urbanc@in.tum.de>
parents: 525
diff changeset
    44
done
efe63c062e48 polished introspection section
Christian Urban <urbanc@in.tum.de>
parents: 525
diff changeset
    45
565
cecd7a941885 isabelle update_cartouches -t
Norbert Schirmer <norbert.schirmer@web.de>
parents: 562
diff changeset
    46
text \<open>
527
efe63c062e48 polished introspection section
Christian Urban <urbanc@in.tum.de>
parents: 525
diff changeset
    47
  While the information about which theorems are used is obvious in
efe63c062e48 polished introspection section
Christian Urban <urbanc@in.tum.de>
parents: 525
diff changeset
    48
  the first two proofs, it is not obvious in the third, because of the
565
cecd7a941885 isabelle update_cartouches -t
Norbert Schirmer <norbert.schirmer@web.de>
parents: 562
diff changeset
    49
  \<open>auto\<close>-step.  Fortunately, ``behind'' every proved theorem is
527
efe63c062e48 polished introspection section
Christian Urban <urbanc@in.tum.de>
parents: 525
diff changeset
    50
  a proof-tree that records all theorems that are employed for
efe63c062e48 polished introspection section
Christian Urban <urbanc@in.tum.de>
parents: 525
diff changeset
    51
  establishing this theorem.  We can traverse this proof-tree
efe63c062e48 polished introspection section
Christian Urban <urbanc@in.tum.de>
parents: 525
diff changeset
    52
  extracting this information.  Let us first extract the name of the
efe63c062e48 polished introspection section
Christian Urban <urbanc@in.tum.de>
parents: 525
diff changeset
    53
  established theorem. This can be done with
525
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    54
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    55
  @{ML_response [display,gray]
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    56
  "@{thm my_conjIa}
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    57
  |> Thm.proof_body_of
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    58
  |> get_names"
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    59
  "[\"Introspection.my_conjIa\"]"}
565
cecd7a941885 isabelle update_cartouches -t
Norbert Schirmer <norbert.schirmer@web.de>
parents: 562
diff changeset
    60
\<close>
cecd7a941885 isabelle update_cartouches -t
Norbert Schirmer <norbert.schirmer@web.de>
parents: 562
diff changeset
    61
text \<open>
cecd7a941885 isabelle update_cartouches -t
Norbert Schirmer <norbert.schirmer@web.de>
parents: 562
diff changeset
    62
  whereby \<open>Introspection\<close> refers to the theory name in which
527
efe63c062e48 polished introspection section
Christian Urban <urbanc@in.tum.de>
parents: 525
diff changeset
    63
  we established the theorem @{thm [source] my_conjIa}. The function @{ML_ind
efe63c062e48 polished introspection section
Christian Urban <urbanc@in.tum.de>
parents: 525
diff changeset
    64
  proof_body_of in Thm} returns a part of the data that is stored in a
529
13d7ea419c5f moved the introspection part into the theorem section
Christian Urban <urbanc@in.tum.de>
parents: 528
diff changeset
    65
  theorem.  Notice that the first proof above references
527
efe63c062e48 polished introspection section
Christian Urban <urbanc@in.tum.de>
parents: 525
diff changeset
    66
  three theorems, namely @{thm [source] conjI}, @{thm [source] conjunct1} 
efe63c062e48 polished introspection section
Christian Urban <urbanc@in.tum.de>
parents: 525
diff changeset
    67
  and @{thm [source] conjunct2}. We can obtain them by descending into the
efe63c062e48 polished introspection section
Christian Urban <urbanc@in.tum.de>
parents: 525
diff changeset
    68
  first level of the proof-tree, as follows.
525
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    69
562
daf404920ab9 Accomodate to Isabelle 2018
Norbert Schirmer <norbert.schirmer@web.de>
parents: 529
diff changeset
    70
  @{ML_response_fake [display,gray]
525
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    71
  "@{thm my_conjIa}
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    72
  |> Thm.proof_body_of
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    73
  |> get_pbodies
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    74
  |> map get_names
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    75
  |> List.concat"
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    76
  "[\"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.conjI\", \"Pure.protectD\", 
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    77
  \"Pure.protectI\"]"}
565
cecd7a941885 isabelle update_cartouches -t
Norbert Schirmer <norbert.schirmer@web.de>
parents: 562
diff changeset
    78
\<close>
cecd7a941885 isabelle update_cartouches -t
Norbert Schirmer <norbert.schirmer@web.de>
parents: 562
diff changeset
    79
text \<open>
529
13d7ea419c5f moved the introspection part into the theorem section
Christian Urban <urbanc@in.tum.de>
parents: 528
diff changeset
    80
  The theorems @{thm [source] protectD} and @{thm [source]
13d7ea419c5f moved the introspection part into the theorem section
Christian Urban <urbanc@in.tum.de>
parents: 528
diff changeset
    81
  protectI} that are internal theorems are always part of a
565
cecd7a941885 isabelle update_cartouches -t
Norbert Schirmer <norbert.schirmer@web.de>
parents: 562
diff changeset
    82
  proof in Isabelle. Note also that applications of \<open>assumption\<close> do not
525
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    83
  count as a separate theorem, as you can see in the following code.
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    84
562
daf404920ab9 Accomodate to Isabelle 2018
Norbert Schirmer <norbert.schirmer@web.de>
parents: 529
diff changeset
    85
  @{ML_response_fake [display,gray]
525
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    86
  "@{thm my_conjIb}
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    87
  |> Thm.proof_body_of
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    88
  |> get_pbodies
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    89
  |> map get_names
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    90
  |> List.concat"
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    91
  "[\"Pure.protectD\", \"Pure.protectI\"]"}
565
cecd7a941885 isabelle update_cartouches -t
Norbert Schirmer <norbert.schirmer@web.de>
parents: 562
diff changeset
    92
\<close>
cecd7a941885 isabelle update_cartouches -t
Norbert Schirmer <norbert.schirmer@web.de>
parents: 562
diff changeset
    93
text \<open>
527
efe63c062e48 polished introspection section
Christian Urban <urbanc@in.tum.de>
parents: 525
diff changeset
    94
  Interestingly, but not surprisingly, the proof of @{thm [source]
efe63c062e48 polished introspection section
Christian Urban <urbanc@in.tum.de>
parents: 525
diff changeset
    95
  my_conjIc} procceeds quite differently from @{thm [source] my_conjIa}
529
13d7ea419c5f moved the introspection part into the theorem section
Christian Urban <urbanc@in.tum.de>
parents: 528
diff changeset
    96
  and @{thm [source] my_conjIb}, as can be seen by the theorems that
13d7ea419c5f moved the introspection part into the theorem section
Christian Urban <urbanc@in.tum.de>
parents: 528
diff changeset
    97
  are returned for @{thm [source] my_conjIc}.
527
efe63c062e48 polished introspection section
Christian Urban <urbanc@in.tum.de>
parents: 525
diff changeset
    98
562
daf404920ab9 Accomodate to Isabelle 2018
Norbert Schirmer <norbert.schirmer@web.de>
parents: 529
diff changeset
    99
  @{ML_response_fake [display,gray]
527
efe63c062e48 polished introspection section
Christian Urban <urbanc@in.tum.de>
parents: 525
diff changeset
   100
  "@{thm my_conjIc}
efe63c062e48 polished introspection section
Christian Urban <urbanc@in.tum.de>
parents: 525
diff changeset
   101
  |> Thm.proof_body_of
efe63c062e48 polished introspection section
Christian Urban <urbanc@in.tum.de>
parents: 525
diff changeset
   102
  |> get_pbodies
efe63c062e48 polished introspection section
Christian Urban <urbanc@in.tum.de>
parents: 525
diff changeset
   103
  |> map get_names
efe63c062e48 polished introspection section
Christian Urban <urbanc@in.tum.de>
parents: 525
diff changeset
   104
  |> List.concat"
562
daf404920ab9 Accomodate to Isabelle 2018
Norbert Schirmer <norbert.schirmer@web.de>
parents: 529
diff changeset
   105
  "[\"HOL.implies_True_equals\", \"HOL.Eq_TrueI\", \"HOL.simp_thms_25\", \"HOL.eq_reflection\", 
daf404920ab9 Accomodate to Isabelle 2018
Norbert Schirmer <norbert.schirmer@web.de>
parents: 529
diff changeset
   106
    \"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.TrueI\", \"Pure.protectD\",
daf404920ab9 Accomodate to Isabelle 2018
Norbert Schirmer <norbert.schirmer@web.de>
parents: 529
diff changeset
   107
    \"Pure.protectI\"]"}
565
cecd7a941885 isabelle update_cartouches -t
Norbert Schirmer <norbert.schirmer@web.de>
parents: 562
diff changeset
   108
\<close>
cecd7a941885 isabelle update_cartouches -t
Norbert Schirmer <norbert.schirmer@web.de>
parents: 562
diff changeset
   109
text \<open>
527
efe63c062e48 polished introspection section
Christian Urban <urbanc@in.tum.de>
parents: 525
diff changeset
   110
  Of course we can also descend into the second level of the tree 
529
13d7ea419c5f moved the introspection part into the theorem section
Christian Urban <urbanc@in.tum.de>
parents: 528
diff changeset
   111
  ``behind'' @{thm [source] my_conjIa} say, which
525
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   112
  means we obtain the theorems that are used in order to prove
527
efe63c062e48 polished introspection section
Christian Urban <urbanc@in.tum.de>
parents: 525
diff changeset
   113
  @{thm [source] conjunct1}, @{thm [source] conjunct2} and @{thm [source] conjI}.
525
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   114
562
daf404920ab9 Accomodate to Isabelle 2018
Norbert Schirmer <norbert.schirmer@web.de>
parents: 529
diff changeset
   115
  @{ML_response_fake [display, gray]
525
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   116
  "@{thm my_conjIa}
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   117
  |> Thm.proof_body_of
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   118
  |> get_pbodies
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   119
  |> map get_pbodies
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   120
  |> (map o map) get_names
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   121
  |> List.concat
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   122
  |> List.concat
562
daf404920ab9 Accomodate to Isabelle 2018
Norbert Schirmer <norbert.schirmer@web.de>
parents: 529
diff changeset
   123
  |> duplicates (op =)"
daf404920ab9 Accomodate to Isabelle 2018
Norbert Schirmer <norbert.schirmer@web.de>
parents: 529
diff changeset
   124
  "[\"\", \"Pure.protectD\",
daf404920ab9 Accomodate to Isabelle 2018
Norbert Schirmer <norbert.schirmer@web.de>
parents: 529
diff changeset
   125
 \"Pure.protectI\"]"}
565
cecd7a941885 isabelle update_cartouches -t
Norbert Schirmer <norbert.schirmer@web.de>
parents: 562
diff changeset
   126
\<close>
cecd7a941885 isabelle update_cartouches -t
Norbert Schirmer <norbert.schirmer@web.de>
parents: 562
diff changeset
   127
text \<open>
525
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   128
  \begin{readmore} 
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   129
  The data-structure @{ML_type proof_body} is implemented
527
efe63c062e48 polished introspection section
Christian Urban <urbanc@in.tum.de>
parents: 525
diff changeset
   130
  in the file @{ML_file "Pure/proofterm.ML"}. The implementation 
efe63c062e48 polished introspection section
Christian Urban <urbanc@in.tum.de>
parents: 525
diff changeset
   131
  of theorems and related functions are in @{ML_file "Pure/thm.ML"}.  
525
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   132
  \end{readmore}
565
cecd7a941885 isabelle update_cartouches -t
Norbert Schirmer <norbert.schirmer@web.de>
parents: 562
diff changeset
   133
\<close>
525
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   134
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   135
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   136
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   137
end
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   138
  
92a3600e50e4 added a new recipe for introspecting theorems (suggested by Lukas and Rafal)
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   139