isabelle-cookbook: comparison ProgTutorial/Tactical.thy

equal deleted inserted replaced

-:cd28458c2add
+:501491d56798
 sometimes useful during the development of tactics.
 *}
 lemma
 shows "False" and "Goldbach_conjecture"
-apply(tactic {* Skip_Proof.cheat_tac @{theory} *})
+apply(tactic {* Skip_Proof.cheat_tac 1 *})
 txt{*\begin{minipage}{\textwidth}
 @{subgoals [display]}
 \end{minipage}*}
 (*<*)oops(*>*)
 corresponds on the ML-level to the tactic
 *}
 lemma
 shows "Suc (1 + 2) < 3 + 2"
-apply(tactic {* asm_full_simp_tac @{simpset} 1 *})
+apply(tactic {* asm_full_simp_tac @{context} 1 *})
 done
 text {*
 If the simplifier cannot make any progress, then it leaves the goal unchanged,
 i.e., does not raise any error message. That means if you use it to unfold a
 \begin{isabelle}*}
 ML %grayML{*fun print_ss ctxt ss =
 let
 val {simps, congs, procs, ...} = Raw_Simplifier.dest_ss ss
-fun name_thm (nm, thm) =
+fun name_sthm (nm, thm) =
+Pretty.enclose (nm ^ ": ") "" [pretty_thm_no_vars ctxt thm]
+fun name_cthm ((_, nm), thm) =
 Pretty.enclose (nm ^ ": ") "" [pretty_thm_no_vars ctxt thm]
 fun name_ctrm (nm, ctrm) =
 Pretty.enclose (nm ^ ": ") "" [pretty_cterms ctxt ctrm]
-val pps = [Pretty.big_list "Simplification rules:" (map name_thm simps),
+val pps = [Pretty.big_list "Simplification rules:" (map name_sthm simps),
-Pretty.big_list "Congruences rules:" (map name_thm congs),
+Pretty.big_list "Congruences rules:" (map name_cthm congs),
 Pretty.big_list "Simproc patterns:" (map name_ctrm procs)]
 in
 pps |> Pretty.chunks
 |> pwriteln
 end*}
 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:
 *}
-ML %grayML{*val ss1 = empty_ss addsimps [@{thm Diff_Int} RS @{thm eq_reflection}] *}
+ML %grayML{*val ss1 = put_simpset empty_ss @{context} addsimps [@{thm Diff_Int} RS @{thm eq_reflection}] *}
 text {*
 Printing then out the components of the simpset gives:
 @{ML_response_fake [display,gray]
-"print_ss @{context} ss1"
+"print_ss @{context} (Raw_Simplifier.simpset_of ss1)"
 "Simplification rules:
 ??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)
 Congruences rules:
 Simproc patterns:"}
 \footnote{\bf FIXME: Why does it print out ??.unknown}
 Adding also the congruence rule @{thm [source] UN_cong}
 *}
-ML %grayML{*val ss2 = Simplifier.add_cong (@{thm UN_cong} RS @{thm eq_reflection}) ss1 *}
+ML %grayML{*val ss2 = ss1 |> Simplifier.add_cong (@{thm UN_cong} RS @{thm eq_reflection}) *}
 text {*
 gives
 @{ML_response_fake [display,gray]
-"print_ss @{context} ss2"
+"print_ss @{context} (Raw_Simplifier.simpset_of 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:"}
 shows "True"
 and  "t = t"
 and  "t \<equiv> t"
 and  "False \<Longrightarrow> Foo"
 and  "\<lbrakk>A; B; C\<rbrakk> \<Longrightarrow> A"
-apply(tactic {* ALLGOALS (simp_tac HOL_basic_ss) *})
+apply(tactic {* ALLGOALS (simp_tac (put_simpset HOL_basic_ss @{context})) *})
 done
 text {*
 This behaviour is not because of simplification rules, but how the subgoaler, solver
 and looper are set up in @{ML HOL_basic_ss}.
 other permutations by rule @{thm [source] perm_compose_aux} (Line 10); and
 finally ``unfreeze'' all instances of permutation compositions by unfolding
 the definition of the auxiliary constant.
 *}
-ML %linenosgray{*val perm_simp_tac =
+ML %linenosgray{*fun perm_simp_tac ctxt =
 let
 val thms1 = [@{thm perm_aux_expand}]
 val thms2 = [@{thm perm_append}, @{thm perm_bij}, @{thm perm_rev},
 @{thm perm_compose_aux}] @ @{thms perm_prod.simps} @
 @{thms perm_list.simps} @ @{thms perm_nat.simps}
 val thms3 = [@{thm perm_aux_def}]
+val ss = put_simpset HOL_basic_ss ctxt
 in
-simp_tac (HOL_basic_ss addsimps thms1)
+simp_tac (ss addsimps thms1)
-THEN' simp_tac (HOL_basic_ss addsimps thms2)
+THEN' simp_tac (ss addsimps thms2)
-THEN' simp_tac (HOL_basic_ss addsimps thms3)
+THEN' simp_tac (ss addsimps thms3)
 end*}
 text {*
 For all three phases we have to build simpsets adding specific lemmas. As is sufficient
 for our purposes here, we can add these lemmas to @{ML HOL_basic_ss} in order to obtain
 *}
 lemma
 fixes c d::"nat" and pi\<^isub>1 pi\<^isub>2::"prm"
 shows "pi\<^isub>1\<bullet>(c, pi\<^isub>2\<bullet>((rev pi\<^isub>1)\<bullet>d)) = (pi\<^isub>1\<bullet>c, (pi\<^isub>1\<bullet>pi\<^isub>2)\<bullet>d)"
-apply(tactic {* perm_simp_tac 1 *})
+apply(tactic {* perm_simp_tac @{context} 1 *})
 done
 text {*
 in one step. This tactic can deal with most instances of normalising permutations.
 (FIXME: Is it interesting to say something about @{term "op =simp=>"}?)
 (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}?)
 (FIXME: what are @{ML mksimps_pairs}; used in Nominal.thy)
 (FIXME: explain @{ML simplify} and @{ML "Simplifier.rewrite_rule"} etc.)
 *}
 To see how simprocs work, let us first write a simproc that just prints out
 the pattern which triggers it and otherwise does nothing. For this
 you can use the function:
 *}
-ML %linenosgray{*fun fail_simproc simpset redex =
+ML %linenosgray{*fun fail_simproc ctxt redex =
 let
-val ctxt = Simplifier.the_context simpset
 val _ = pwriteln (Pretty.block
 [Pretty.str "The redex: ", pretty_cterm ctxt redex])
 in
 NONE
 end*}
 as follows:
 *}
 lemma
 shows "Suc 0 = 1"
-apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [@{simproc fail}]) 1*})
+apply(tactic {* simp_tac (put_simpset
+HOL_basic_ss @{context} addsimprocs [@{simproc fail}]) 1*})
 (*<*)oops(*>*)
 text {*
 Now the message shows up only once since the term @{term "1::nat"} is
 left unchanged.
 want this, then you have to use a slightly different method for setting
 up the simproc. First the function @{ML fail_simproc} needs to be modified
 to
 *}
-ML %grayML{*fun fail_simproc' simpset redex =
+ML %grayML{*fun fail_simproc' ctxt redex =
 let
-val ctxt = Simplifier.the_context simpset
 val _ = pwriteln (Pretty.block
 [Pretty.str "The redex:", pretty_term ctxt redex])
 in
 NONE
 end*}
 We can turn this function into a proper simproc using the function
 @{ML Simplifier.simproc_global_i}:
 *}
-ML %grayML{*val fail' =
+ML %grayML{*fun fail' ctxt =
 let
 val thy = @{theory}
 val pat = [@{term "Suc n"}]
 in
-Simplifier.simproc_global_i thy "fail_simproc'" pat (K fail_simproc')
+Simplifier.simproc_global_i thy "fail_simproc'" pat (K fail_simproc' ctxt)
 end*}
 text {*
 Here the pattern is given as @{ML_type term} (instead of @{ML_type cterm}).
 The function also takes a list of patterns that can trigger the simproc.
 see this in the proof
 *}
 lemma
 shows "Suc (Suc 0) = (Suc 1)"
-apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [fail']) 1*})
+apply(tactic {* simp_tac ((put_simpset HOL_basic_ss @{context}) addsimprocs [fail' @{context}]) 1*})
 (*<*)oops(*>*)
 text {*
 The simproc @{ML fail'} prints out the sequence
 the rewriting with simprocs, let us further assume we want that the simproc
 only rewrites terms ``greater'' than @{term "Suc 0"}. For this we can write
 *}
-ML %grayML{*fun plus_one_simproc ss redex =
+ML %grayML{*fun plus_one_simproc ctxt redex =
 case redex of
 @{term "Suc 0"} => NONE
 | _ => SOME @{thm plus_one}*}
 text {*
 and set up the simproc as follows.
 *}
-ML %grayML{*val plus_one =
+ML %grayML{*fun plus_one ctxt =
 let
 val thy = @{theory}
 val pat = [@{term "Suc n"}]
 in
-Simplifier.simproc_global_i thy "sproc +1" pat (K plus_one_simproc)
+Simplifier.simproc_global_i thy "sproc +1" pat (K plus_one_simproc ctxt)
 end*}
 text {*
 Now the simproc is set up so that it is triggered by terms
 of the form @{term "Suc n"}, but inside the simproc we only produce
 in the following proof
 *}
 lemma
 shows "P (Suc (Suc (Suc 0))) (Suc 0)"
-apply(tactic {* simp_tac (HOL_basic_ss addsimprocs [plus_one]) 1*})
+apply(tactic {* simp_tac (put_simpset HOL_basic_ss @{context} addsimprocs [plus_one @{context}]) 1*})
 txt{*
 where the simproc produces the goal state
 \begin{isabelle}
 @{subgoals[display]}
 \end{isabelle}
 ML %grayML{*fun get_thm_alt ctxt (t, n) =
 let
 val num = HOLogic.mk_number @{typ "nat"} n
 val goal = Logic.mk_equals (t, num)
-val num_ss = HOL_ss addsimps @{thms semiring_norm}
+val num_ss = put_simpset HOL_ss ctxt addsimps @{thms semiring_norm}
 in
 Goal.prove ctxt [] [] goal (K (simp_tac num_ss 1))
 end*}
 text {*
 Anyway, either version can be used in the function that produces the actual
 theorem for the simproc.
 *}
-ML %grayML{*fun nat_number_simproc ss t =
+ML %grayML{*fun nat_number_simproc ctxt t =
-let
-val ctxt = Simplifier.the_context ss
-in
 SOME (get_thm_alt ctxt (t, dest_suc_trm t))
-handle TERM _ => NONE
+handle TERM _ => NONE *}
-end*}
 text {*
 This function uses the fact that @{ML dest_suc_trm} might raise an exception
 @{ML TERM}. In this case there is nothing that can be rewritten and therefore no
 theorem is produced (i.e.~the function returns @{ML NONE}). To try out the simproc
 on an example, you can set it up as follows:
 *}
-ML %grayML{*val nat_number =
+ML %grayML{*fun nat_number ctxt =
 let
 val thy = @{theory}
 val pat = [@{term "Suc n"}]
 in
-Simplifier.simproc_global_i thy "nat_number" pat (K nat_number_simproc)
+Simplifier.simproc_global_i thy "nat_number" pat (K nat_number_simproc ctxt)
 end*}
 text {*
 Now in the lemma
 *}
 lemma
 shows "P (Suc (Suc 2)) (Suc 99) (0::nat) (Suc 4 + Suc 0) (Suc (0 + 0))"
-apply(tactic {* simp_tac (HOL_ss addsimprocs [nat_number]) 1*})
+apply(tactic {* simp_tac (put_simpset HOL_ss @{context} addsimprocs [nat_number @{context}]) 1*})
 txt {*
 you obtain the more legible goal state
 \begin{isabelle}
 @{subgoals [display]}
 \end{isabelle}*}

changeset 544	501491d56798
parent 543	cd28458c2add
child 551	be361e980acf