isabelle-cookbook: comparison CookBook/Tactical.thy

equal deleted inserted replaced

-:3fb9f820a294
+:2319cff107f0
 *}
 text_raw {*
 \begin{figure}[tp]
 \begin{isabelle}*}
-ML{*fun get_parts ss =
+ML{*fun print_ss ctxt ss =
-let
-val ({rules, ...}, {congs, procs, ...}) = MetaSimplifier.rep_ss ss
-val rules_list = Net.entries rules
-val rnames = map #name rules_list
-val rthms =  map #thm rules_list
-val congs_list = fst congs
-val cnames = map fst congs_list
-val cthms = map (#thm o snd) congs_list
-val proc_list = Net.entries procs
-in
-(rnames ~~ rthms, cnames ~~ cthms)
-end
-fun print_parts ctxt ss =
 let
-val (simps, congs) = get_parts ss
+val {simps, congs, procs, ...} = MetaSimplifier.dest_ss ss
 fun name_thm (nm, thm) =
 "  " ^ nm ^ ": " ^ (str_of_thm ctxt thm)
+fun name_ctrm (nm, ctrm) =
+"  " ^ nm ^ ": " ^ (str_of_cterms ctxt ctrm)
 val s1 = ["Simplification rules:"]
 val s2 = map name_thm simps
 val s3 = ["Congruences rules:"]
 val s4 = map name_thm congs
+val s5 = ["Simproc patterns:"]
+val s6 = map name_ctrm procs
 in
-(s1 @ s2 @ s3 @ s4)
+(s1 @ s2 @ s3 @ s4 @ s5 @ s6)
 |> separate "\n"
 |> implode
 |> warning
 end*}
 text_raw {*
 \end{isabelle}
-\caption{The function @{ML MetaSimplifier.rep_ss} returns a record containing
+\caption{The function @{ML MetaSimplifier.dest_ss} returns a record containing
-a simpset. We are here only interested in the simplifcation rules, congruence rules and
+all printable information stored in a simpset. We are here only interested in the
-simprocs. The first and third are discrimination nets, which from which we extract
+simplifcation rules, congruence rules and simprocs.\label{fig:printss}}
-lists using @{ML Net.entries}. The congruence rules are stored in
-an association list, associating a constant with a rule.\label{fig:prettyss}}
 \end{figure} *}
 text {*
-To see how they work, consider the two functions in Figure~\ref{fig:prettyss}, which
+To see how they work, consider the two functions in Figure~\ref{fig:printss}, which
 print out some parts of a simpset. If you use them to print out the components of the
 empty simpset, in ML @{ML empty_ss} and the most primitive simpset
 @{ML_response_fake [display,gray]
-"print_parts @{context} empty_ss"
+"print_ss @{context} empty_ss"
 "Simplification rules:
-Congruences rules:"}
+Congruences rules:
+Simproc patterns:"}
 you can see it contains nothing. This simpset is usually not useful, except as a
 building block to build bigger simpsets. For example you can add to @{ML empty_ss}
 the simplification rule @{thm [source] Diff_Int} as follows:
 *}
 text {*
 Printing then out the components of the simpset gives:
 @{ML_response_fake [display,gray]
-"print_parts @{context} ss1"
+"print_ss @{context} ss1"
-"Simplification rules:
-??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)
-Congruences rules:"}
-(FIXME: Why does it print out ??.unknown)
-Adding also the congruence rule @{thm [source] UN_cong}
-*}
-ML{*val ss2 = ss1 addcongs [@{thm UN_cong} RS @{thm eq_reflection}] *}
-text {*
-gives
-@{ML_response_fake [display,gray]
-"print_parts @{context} ss2"
 "Simplification rules:
 ??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)
 Congruences rules:
-UNION: \<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> C x = D x\<rbrakk> \<Longrightarrow> \<Union>x\<in>A. C x \<equiv> \<Union>x\<in>B. D x"}
+Simproc patterns:"}
+(FIXME: Why does it print out ??.unknown)
+Adding also the congruence rule @{thm [source] UN_cong}
+*}
+ML{*val ss2 = ss1 addcongs [@{thm UN_cong} RS @{thm eq_reflection}] *}
+text {*
+gives
+@{ML_response_fake [display,gray]
+"print_ss @{context} ss2"
+"Simplification rules:
+??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)
+Congruences rules:
+UNION: \<lbrakk>A = B; \<And>x. x \<in> B \<Longrightarrow> C x = D x\<rbrakk> \<Longrightarrow> \<Union>x\<in>A. C x \<equiv> \<Union>x\<in>B. D x
+Simproc patterns:"}
 Notice that we had to add these lemmas as meta-equations. The @{ML empty_ss}
 expects this form of the simplification and congruence rules. However, even
 when adding these lemmas to @{ML empty_ss} we do not end up with anything useful yet.
 In the context of HOL, the first really useful simpset is @{ML HOL_basic_ss}. While
 printing out the components of this simpset
 @{ML_response_fake [display,gray]
-"print_parts @{context} HOL_basic_ss"
+"print_ss @{context} HOL_basic_ss"
 "Simplification rules:
-Congruences rules:"}
+Congruences rules:
+Simproc patterns:"}
 also produces ``nothing'', the printout is misleading. In fact
 the @{ML HOL_basic_ss} is setup so that it can solve goals of the
 form  @{thm TrueI}, @{thm refl[no_vars]}, @{term "t \<equiv> t"} and @{thm FalseE[no_vars]};
 and also resolve with assumptions. For example:
 The simpset @{ML HOL_ss} is an extention of @{ML HOL_basic_ss} containing
 already many useful simplification and congruence rules for the logical
 connectives in HOL.
 @{ML_response_fake [display,gray]
-"print_parts @{context} HOL_ss"
+"print_ss @{context} HOL_ss"
 "Simplification rules:
 Pure.triv_forall_equality: (\<And>x. PROP V) \<equiv> PROP V
 HOL.the_eq_trivial: THE x. x = y \<equiv> y
 HOL.the_sym_eq_trivial: THE ya. y = ya \<equiv> y
 \<dots>
 Congruences rules:
 HOL.simp_implies: \<dots>
 \<Longrightarrow> (PROP P =simp=> PROP Q) \<equiv> (PROP P' =simp=> PROP Q')
-op -->: \<lbrakk>P \<equiv> P'; P' \<Longrightarrow> Q \<equiv> Q'\<rbrakk> \<Longrightarrow> P \<longrightarrow> Q \<equiv> P' \<longrightarrow> Q'"}
+op -->: \<lbrakk>P \<equiv> P'; P' \<Longrightarrow> Q \<equiv> Q'\<rbrakk> \<Longrightarrow> P \<longrightarrow> Q \<equiv> P' \<longrightarrow> Q'
+Simproc patterns:
+\<dots>"}
 The simplifier is often used to unfold definitions in a proof. For this the
 simplifier contains the @{ML rewrite_goals_tac}. Suppose for example the
 definition
 often be done easier by implementing a simproc or a conversion. Both will be
 explained in the next two chapters.
 (FIXME: Is it interesting to say something about @{term "op =simp=>"}?)
-(FIXME: Unfortunately one cannot access any simproc, as there is
-no @{text rep_proc} in function @{ML get_parts}.)
 (FIXME: What are the second components of the congruence rules---something to
 do with weak congruence constants?)
 (FIXME: Anything interesting to say about @{ML Simplifier.clear_ss}?)

changeset 163	2319cff107f0
parent 162	3fb9f820a294
child 166	00d153e32a53