Mercurial Mercurial > hg > isabelle-cookbook / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ProgTutorial/Recipes/Introspection.thy
changeset 562 daf404920ab9
parent 529 13d7ea419c5f
child 565 cecd7a941885
equal deleted inserted replaced
561:aec7073d4645 562:daf404920ab9 
    15   analyse the @{ML_type_ind proof_body} data-structure from the structure 
    15   analyse the @{ML_type_ind proof_body} data-structure from the structure 
    16   @{ML_struct Proofterm}.
 
    16   @{ML_struct Proofterm}.
 
    17 *}
 
    17 *}
 
    18 
    18 
    19 ML %grayML{*fun pthms_of (PBody {thms, ...}) = map #2 thms 
    19 ML %grayML{*fun pthms_of (PBody {thms, ...}) = map #2 thms 
    20 val get_names = map #1 o pthms_of 
    20 val get_names = (map Proofterm.thm_node_name) o pthms_of 
    21 val get_pbodies = map (Future.join o #3) o pthms_of *}
 
    21 val get_pbodies = map (Future.join o Proofterm.thm_node_body) o pthms_of *}
 
    22 
    22 
    23 text {* 
    23 text {* 
    24   To see what their purpose is, consider the following three short proofs.
 
    24   To see what their purpose is, consider the following three short proofs.
 
    25 *}
 
    25 *}
 
    26 
    26 
    55   @{ML_response [display,gray]
 
    55   @{ML_response [display,gray]
 
    56   "@{thm my_conjIa}
 
    56   "@{thm my_conjIa}
 
    57   |> Thm.proof_body_of
 
    57   |> Thm.proof_body_of
 
    58   |> get_names"
 
    58   |> get_names"
 
    59   "[\"Introspection.my_conjIa\"]"}
 
    59   "[\"Introspection.my_conjIa\"]"}
 
    60 
    60 *}
 
       
    61 text {*
 
    61   whereby @{text "Introspection"} refers to the theory name in which
 
    62   whereby @{text "Introspection"} refers to the theory name in which
 
    62   we established the theorem @{thm [source] my_conjIa}. The function @{ML_ind
 
    63   we established the theorem @{thm [source] my_conjIa}. The function @{ML_ind
 
    63   proof_body_of in Thm} returns a part of the data that is stored in a
 
    64   proof_body_of in Thm} returns a part of the data that is stored in a
 
    64   theorem.  Notice that the first proof above references
 
    65   theorem.  Notice that the first proof above references
 
    65   three theorems, namely @{thm [source] conjI}, @{thm [source] conjunct1} 
    66   three theorems, namely @{thm [source] conjI}, @{thm [source] conjunct1} 
    66   and @{thm [source] conjunct2}. We can obtain them by descending into the
 
    67   and @{thm [source] conjunct2}. We can obtain them by descending into the
 
    67   first level of the proof-tree, as follows.
 
    68   first level of the proof-tree, as follows.
 
    68 
    69 
    69   @{ML_response [display,gray]
 
    70   @{ML_response_fake [display,gray]
 
    70   "@{thm my_conjIa}
 
    71   "@{thm my_conjIa}
 
    71   |> Thm.proof_body_of
 
    72   |> Thm.proof_body_of
 
    72   |> get_pbodies
 
    73   |> get_pbodies
 
    73   |> map get_names
 
    74   |> map get_names
 
    74   |> List.concat"
 
    75   |> List.concat"
 
    75   "[\"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.conjI\", \"Pure.protectD\", 
    76   "[\"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.conjI\", \"Pure.protectD\", 
    76   \"Pure.protectI\"]"}
 
    77   \"Pure.protectI\"]"}
 
    77 
    78 *}
 
       
    79 text {*
 
    78   The theorems @{thm [source] protectD} and @{thm [source]
 
    80   The theorems @{thm [source] protectD} and @{thm [source]
 
    79   protectI} that are internal theorems are always part of a
 
    81   protectI} that are internal theorems are always part of a
 
    80   proof in Isabelle. Note also that applications of @{text assumption} do not
 
    82   proof in Isabelle. Note also that applications of @{text assumption} do not
 
    81   count as a separate theorem, as you can see in the following code.
 
    83   count as a separate theorem, as you can see in the following code.
 
    82 
    84 
    83   @{ML_response [display,gray]
 
    85   @{ML_response_fake [display,gray]
 
    84   "@{thm my_conjIb}
 
    86   "@{thm my_conjIb}
 
    85   |> Thm.proof_body_of
 
    87   |> Thm.proof_body_of
 
    86   |> get_pbodies
 
    88   |> get_pbodies
 
    87   |> map get_names
 
    89   |> map get_names
 
    88   |> List.concat"
 
    90   |> List.concat"
 
    89   "[\"Pure.protectD\", \"Pure.protectI\"]"}
 
    91   "[\"Pure.protectD\", \"Pure.protectI\"]"}
 
    90 
    92 *}
 
       
    93 text {*
 
    91   Interestingly, but not surprisingly, the proof of @{thm [source]
 
    94   Interestingly, but not surprisingly, the proof of @{thm [source]
 
    92   my_conjIc} procceeds quite differently from @{thm [source] my_conjIa}
 
    95   my_conjIc} procceeds quite differently from @{thm [source] my_conjIa}
 
    93   and @{thm [source] my_conjIb}, as can be seen by the theorems that
 
    96   and @{thm [source] my_conjIb}, as can be seen by the theorems that
 
    94   are returned for @{thm [source] my_conjIc}.
 
    97   are returned for @{thm [source] my_conjIc}.
 
    95 
    98 
    96   @{ML_response [display,gray]
 
    99   @{ML_response_fake [display,gray]
 
    97   "@{thm my_conjIc}
 
   100   "@{thm my_conjIc}
 
    98   |> Thm.proof_body_of
 
   101   |> Thm.proof_body_of
 
    99   |> get_pbodies
 
   102   |> get_pbodies
 
   100   |> map get_names
 
   103   |> map get_names
 
   101   |> List.concat"
 
   104   |> List.concat"
 
   102   "[\"HOL.Eq_TrueI\", \"HOL.simp_thms_25\", \"HOL.eq_reflection\",
 
   105   "[\"HOL.implies_True_equals\", \"HOL.Eq_TrueI\", \"HOL.simp_thms_25\", \"HOL.eq_reflection\", 
   103   \"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.TrueI\", \"Pure.protectD\",
 
   106     \"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.TrueI\", \"Pure.protectD\",
 
   104   \"Pure.protectI\"]"}
 
   107     \"Pure.protectI\"]"}
 
   105 
   108 *}
 
       
   109 text {*
 
   106   Of course we can also descend into the second level of the tree 
   110   Of course we can also descend into the second level of the tree 
   107   ``behind'' @{thm [source] my_conjIa} say, which
 
   111   ``behind'' @{thm [source] my_conjIa} say, which
 
   108   means we obtain the theorems that are used in order to prove
 
   112   means we obtain the theorems that are used in order to prove
 
   109   @{thm [source] conjunct1}, @{thm [source] conjunct2} and @{thm [source] conjI}.
 
   113   @{thm [source] conjunct1}, @{thm [source] conjunct2} and @{thm [source] conjI}.
 
   110 
   114 
   111   @{ML_response [display, gray]
 
   115   @{ML_response_fake [display, gray]
 
   112   "@{thm my_conjIa}
 
   116   "@{thm my_conjIa}
 
   113   |> Thm.proof_body_of
 
   117   |> Thm.proof_body_of
 
   114   |> get_pbodies
 
   118   |> get_pbodies
 
   115   |> map get_pbodies
 
   119   |> map get_pbodies
 
   116   |> (map o map) get_names
 
   120   |> (map o map) get_names
 
   117   |> List.concat
 
   121   |> List.concat
 
   118   |> List.concat
 
   122   |> List.concat
 
   119   |> duplicates (op=)"
 
   123   |> duplicates (op =)"
 
   120   "[\"HOL.spec\", \"HOL.and_def\", \"HOL.mp\", \"HOL.impI\", \"Pure.protectD\",
 
   124   "[\"\", \"Pure.protectD\",
 
   121   \"Pure.protectI\"]"}
 
   125  \"Pure.protectI\"]"}
 
   122 
   126 *}
 
       
   127 text {*
 
   123   \begin{readmore} 
   128   \begin{readmore} 
   124   The data-structure @{ML_type proof_body} is implemented
 
   129   The data-structure @{ML_type proof_body} is implemented
 
   125   in the file @{ML_file "Pure/proofterm.ML"}. The implementation 
   130   in the file @{ML_file "Pure/proofterm.ML"}. The implementation 
   126   of theorems and related functions are in @{ML_file "Pure/thm.ML"}.  
   131   of theorems and related functions are in @{ML_file "Pure/thm.ML"}.  
   127   \end{readmore}
 
   132   \end{readmore}
isabelle-cookbook