isabelle-cookbook: comparison ProgTutorial/Tactical.thy

equal deleted inserted replaced

-:be23597e81db
+:f875a25aa72d
 text \<open>
 This proof translates to the following ML-code.
 @{ML_matchresult_fake [display,gray]
-"let
+\<open>let
 val ctxt = @{context}
-val goal = @{prop \"P \<or> Q \<Longrightarrow> Q \<or> P\"}
+val goal = @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}
 in
-Goal.prove ctxt [\"P\", \"Q\"] [] goal
+Goal.prove ctxt ["P", "Q"] [] goal
 (fn _ =>  eresolve_tac @{context} [@{thm disjE}] 1
 THEN resolve_tac @{context} [@{thm disjI2}] 1
 THEN assume_tac @{context} 1
 THEN resolve_tac @{context} [@{thm disjI1}] 1
 THEN assume_tac @{context} 1)
-end" "?P \<or> ?Q \<Longrightarrow> ?Q \<or> ?P"}
+end\<close> \<open>?P \<or> ?Q \<Longrightarrow> ?Q \<or> ?P\<close>}
 To start the proof, the function @{ML_ind prove in Goal} sets up a goal
 state for proving the goal @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}. We can give this
 function some assumptions in the third argument (there are no assumption in
 the proof at hand). The second argument stands for a list of variables
 constrained version of the \<open>bspec\<close>-theorem. One way to give such
 constraints is by pre-instantiating theorems with other theorems.
 The function @{ML_ind RS in Drule}, for example, does this.
 @{ML_matchresult_fake [display,gray]
-"@{thm disjI1} RS @{thm conjI}" "\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q"}
+\<open>@{thm disjI1} RS @{thm conjI}\<close> \<open>\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q\<close>}
 In this example it instantiates the first premise of the \<open>conjI\<close>-theorem
 with the theorem \<open>disjI1\<close>. If the instantiation is impossible, as in the
 case of
 @{ML_matchresult_fake_both [display,gray]
-"@{thm conjI} RS @{thm mp}"
+\<open>@{thm conjI} RS @{thm mp}\<close>
-"*** Exception- THM (\"RSN: no unifiers\", 1,
+\<open>*** Exception- THM ("RSN: no unifiers", 1,
-[\"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\", \"\<lbrakk>?P \<longrightarrow> ?Q; ?P\<rbrakk> \<Longrightarrow> ?Q\"]) raised"}
+["\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q", "\<lbrakk>?P \<longrightarrow> ?Q; ?P\<rbrakk> \<Longrightarrow> ?Q"]) raised\<close>}
 then the function raises an exception. The function @{ML_ind  RSN in Drule}
 is similar to @{ML RS}, but takes an additional number as argument. This
 number makes explicit which premise should be instantiated.
 If you want to instantiate more than one premise of a theorem, you can use
 the function @{ML_ind MRS in Drule}:
 @{ML_matchresult_fake [display,gray]
-"[@{thm disjI1}, @{thm disjI2}] MRS @{thm conjI}"
+\<open>[@{thm disjI1}, @{thm disjI2}] MRS @{thm conjI}\<close>
-"\<lbrakk>?P2; ?Q1\<rbrakk> \<Longrightarrow> (?P2 \<or> ?Q2) \<and> (?P1 \<or> ?Q1)"}
+\<open>\<lbrakk>?P2; ?Q1\<rbrakk> \<Longrightarrow> (?P2 \<or> ?Q2) \<and> (?P1 \<or> ?Q1)\<close>}
 If you need to instantiate lists of theorems, you can use the
 functions @{ML_ind RL in Drule} and @{ML_ind OF in Drule}. For
 example in the code below, every theorem in the second list is
 instantiated with every theorem in the first.
 @{ML_matchresult_fake [display,gray]
-"let
+\<open>let
 val list1 = [@{thm impI}, @{thm disjI2}]
 val list2 = [@{thm conjI}, @{thm disjI1}]
 in
 list1 RL list2
-end"
+end\<close>
-"[\<lbrakk>?P1 \<Longrightarrow> ?Q1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<longrightarrow> ?Q1) \<and> ?Q,
+\<open>[\<lbrakk>?P1 \<Longrightarrow> ?Q1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<longrightarrow> ?Q1) \<and> ?Q,
 \<lbrakk>?Q1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q,
 (?P1 \<Longrightarrow> ?Q1) \<Longrightarrow> (?P1 \<longrightarrow> ?Q1) \<or> ?Q,
-?Q1 \<Longrightarrow> (?P1 \<or> ?Q1) \<or> ?Q]"}
+?Q1 \<Longrightarrow> (?P1 \<or> ?Q1) \<or> ?Q]\<close>}
 \begin{readmore}
 The combinators for instantiating theorems with other theorems are
 defined in @{ML_file "Pure/drule.ML"}.
 \end{readmore}
 text \<open>
 There is even another way of implementing this tactic: in automatic proof
 procedures (in contrast to tactics that might be called by the user) there
 are often long lists of tactics that are applied to the first
-subgoal. Instead of writing the code above and then calling @{ML "foo_tac'' @{context} 1"},
+subgoal. Instead of writing the code above and then calling @{ML \<open>foo_tac'' @{context} 1\<close>},
 you can also just write
 \<close>
 ML %grayML\<open>fun foo_tac1 ctxt =
 EVERY1 [eresolve_tac ctxt [@{thm disjE}], resolve_tac ctxt [@{thm disjI2}],
 TRY}, it does not fail anymore. The problem is that for the user there is
 little chance to see whether progress in the proof has been made, or not. By
 convention therefore, tactics visible to the user should either change
 something or fail.
-To comply with this convention, we could simply delete the @{ML "K all_tac"}
+To comply with this convention, we could simply delete the @{ML \<open>K all_tac\<close>}
 in @{ML select_tac'} or delete @{ML TRY} from @{ML select_tac''}. But for
 the sake of argument, let us suppose that this deletion is \emph{not} an
 option. In such cases, you can use the combinator @{ML_ind CHANGED in
 Tactical} to make sure the subgoal has been changed by the tactic. Because
 now
 To see how they work, consider the function in Figure~\ref{fig:printss}, which
 prints out some parts of a simpset. If you use it to print out the components of the
 empty simpset, i.e., @{ML_ind empty_ss in Raw_Simplifier}
 @{ML_matchresult_fake [display,gray]
-"print_ss @{context} empty_ss"
+\<open>print_ss @{context} empty_ss\<close>
-"Simplification rules:
+\<open>Simplification rules:
 Congruences rules:
-Simproc patterns:"}
+Simproc patterns:\<close>}
 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:
 \<close>
 text \<open>
 Printing then out the components of the simpset gives:
 @{ML_matchresult_fake [display,gray]
-"print_ss @{context} (Raw_Simplifier.simpset_of ss1)"
+\<open>print_ss @{context} (Raw_Simplifier.simpset_of ss1)\<close>
-"Simplification rules:
+\<open>Simplification rules:
 ??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)
 Congruences rules:
-Simproc patterns:"}
+Simproc patterns:\<close>}
 \footnote{\bf FIXME: Why does it print out ??.unknown}
 Adding also the congruence rule @{thm [source] strong_INF_cong}
 \<close>
 text \<open>
 gives
 @{ML_matchresult_fake [display,gray]
-"print_ss @{context} (Raw_Simplifier.simpset_of ss2)"
+\<open>print_ss @{context} (Raw_Simplifier.simpset_of ss2)\<close>
-"Simplification rules:
+\<open>Simplification rules:
 ??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)
 Congruences rules:
 Complete_Lattices.Inf_class.INFIMUM:
 \<lbrakk>A1 = B1; \<And>x. x \<in> B1 =simp=> C1 x = D1 x\<rbrakk> \<Longrightarrow> INFIMUM A1 C1 \<equiv> INFIMUM B1 D1
-Simproc patterns:"}
+Simproc patterns:\<close>}
 Notice that we had to add these lemmas as meta-equations. The @{ML empty_ss}
 expects this form of the simplification and congruence rules. This is
 different, if we use for example the simpset @{ML HOL_basic_ss} (see below),
 where rules are usually added as equation. 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_ind
 HOL_basic_ss in Simpdata}. While printing out the components of this simpset
 @{ML_matchresult_fake [display,gray]
-"print_ss @{context} HOL_basic_ss"
+\<open>print_ss @{context} HOL_basic_ss\<close>
-"Simplification rules:
+\<open>Simplification rules:
 Congruences rules:
-Simproc patterns:"}
+Simproc patterns:\<close>}
 also produces ``nothing'', the printout is somewhat misleading. In fact
 the @{ML HOL_basic_ss} is setup so that it can solve goals of the
 form
 The simpset @{ML_ind HOL_ss} is an extension of @{ML HOL_basic_ss} containing
 already many useful simplification and congruence rules for the logical
 connectives in HOL.
 @{ML_matchresult_fake [display,gray]
-"print_ss @{context} HOL_ss"
+\<open>print_ss @{context} HOL_ss\<close>
-"Simplification rules:
+\<open>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'
 Simproc patterns:
-\<dots>"}
+\<dots>\<close>}
 \begin{readmore}
 The simplifier for HOL is set up in @{ML_file "HOL/Tools/simpdata.ML"}.
 The simpset @{ML HOL_ss} is implemented in @{ML_file "HOL/HOL.thy"}.
 \end{readmore}
 (FIXME: What are the second components of the congruence rules---something to
 do with weak congruence constants?)
 (FIXME: what are @{ML mksimps_pairs}; used in Nominal.thy)
-(FIXME: explain @{ML simplify} and @{ML "Simplifier.rewrite_rule"} etc.)
+(FIXME: explain @{ML simplify} and @{ML \<open>Simplifier.rewrite_rule\<close>} etc.)
 \<close>
 section \<open>Simprocs\<close>
 whereby the produced theorem is always a meta-equality. A simple conversion
 is the function @{ML_ind  all_conv in Conv}, which maps a @{ML_type cterm} to an
 instance of the (meta)reflexivity theorem. For example:
 @{ML_matchresult_fake [display,gray]
-"Conv.all_conv @{cterm \"Foo \<or> Bar\"}"
+\<open>Conv.all_conv @{cterm "Foo \<or> Bar"}\<close>
-"Foo \<or> Bar \<equiv> Foo \<or> Bar"}
+\<open>Foo \<or> Bar \<equiv> Foo \<or> Bar\<close>}
 Another simple conversion is @{ML_ind  no_conv in Conv} which always raises the
 exception @{ML CTERM}.
 @{ML_matchresult_fake [display,gray]
-"Conv.no_conv @{cterm True}"
+\<open>Conv.no_conv @{cterm True}\<close>
-"*** Exception- CTERM (\"no conversion\", []) raised"}
+\<open>*** Exception- CTERM ("no conversion", []) raised\<close>}
 A more interesting conversion is the function @{ML_ind  beta_conversion in Thm}: it
 produces a meta-equation between a term and its beta-normal form. For example
 @{ML_matchresult_fake [display,gray]
-"let
+\<open>let
-val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
+val add = @{cterm "\<lambda>x y. x + (y::nat)"}
-val two = @{cterm \"2::nat\"}
+val two = @{cterm "2::nat"}
-val ten = @{cterm \"10::nat\"}
+val ten = @{cterm "10::nat"}
 val ctrm = Thm.apply (Thm.apply add two) ten
 in
 Thm.beta_conversion true ctrm
-end"
+end\<close>
-"((\<lambda>x y. x + y) 2) 10 \<equiv> 2 + 10"}
+\<open>((\<lambda>x y. x + y) 2) 10 \<equiv> 2 + 10\<close>}
 If you run this example, you will notice that the actual response is the
 seemingly nonsensical @{term
 "2 + 10 \<equiv> 2 + (10::nat)"}. The reason is that the pretty-printer for
 @{ML_type cterm}s eta-normalises (sic) terms and therefore produces this output.
 If we get hold of the ``raw'' representation of the produced theorem,
 we obtain the expected result.
 @{ML_matchresult [display,gray]
-"let
+\<open>let
-val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
+val add = @{cterm "\<lambda>x y. x + (y::nat)"}
-val two = @{cterm \"2::nat\"}
+val two = @{cterm "2::nat"}
-val ten = @{cterm \"10::nat\"}
+val ten = @{cterm "10::nat"}
 val ctrm = Thm.apply (Thm.apply add two) ten
 in
 Thm.prop_of (Thm.beta_conversion true ctrm)
-end"
+end\<close>
-"Const (\"Pure.eq\",_) $
+\<open>Const ("Pure.eq",_) $
-(Abs (\"x\",_,Abs (\"y\",_,_)) $_$_) $
+(Abs ("x",_,Abs ("y",_,_)) $_$_) $
-(Const (\"Groups.plus_class.plus\",_) $ _ $ _)"}
+(Const ("Groups.plus_class.plus",_) $ _ $ _)\<close>}
 or in the pretty-printed form
 @{ML_matchresult_fake [display,gray]
-"let
+\<open>let
-val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
+val add = @{cterm "\<lambda>x y. x + (y::nat)"}
-val two = @{cterm \"2::nat\"}
+val two = @{cterm "2::nat"}
-val ten = @{cterm \"10::nat\"}
+val ten = @{cterm "10::nat"}
 val ctrm = Thm.apply (Thm.apply add two) ten
 val ctxt = @{context}
 |> Config.put eta_contract false
 |> Config.put show_abbrevs false
 in
 Thm.prop_of (Thm.beta_conversion true ctrm)
 |> pretty_term ctxt
 |> pwriteln
-end"
+end\<close>
-"(\<lambda>x y. x + y) 2 10 \<equiv> 2 + 10"}
+\<open>(\<lambda>x y. x + y) 2 10 \<equiv> 2 + 10\<close>}
 The argument @{ML true} in @{ML beta_conversion in Thm} indicates that
 the right-hand side should be fully beta-normalised. If instead
 @{ML false} is given, then only a single beta-reduction is performed
 on the outer-most level.
 text \<open>
 It can be used for example to rewrite @{term "True \<and> (Foo \<longrightarrow> Bar)"}
 to @{term "Foo \<longrightarrow> Bar"}. The code is as follows.
 @{ML_matchresult_fake [display,gray]
-"let
+\<open>let
-val ctrm = @{cterm \"True \<and> (Foo \<longrightarrow> Bar)\"}
+val ctrm = @{cterm "True \<and> (Foo \<longrightarrow> Bar)"}
 in
 Conv.rewr_conv @{thm true_conj1} ctrm
-end"
+end\<close>
-"True \<and> (Foo \<longrightarrow> Bar) \<equiv> Foo \<longrightarrow> Bar"}
+\<open>True \<and> (Foo \<longrightarrow> Bar) \<equiv> Foo \<longrightarrow> Bar\<close>}
 Note, however, that the function @{ML_ind  rewr_conv in Conv} only rewrites the
 outer-most level of the @{ML_type cterm}. If the given @{ML_type cterm} does not match
 exactly the
 left-hand side of the theorem, then  @{ML_ind  rewr_conv in Conv} fails, raising
 combining several conversions into one. For this you can use conversion
 combinators. The simplest conversion combinator is @{ML_ind then_conv in Conv},
 which applies one conversion after another. For example
 @{ML_matchresult_fake [display,gray]
-"let
+\<open>let
 val conv1 = Thm.beta_conversion false
 val conv2 = Conv.rewr_conv @{thm true_conj1}
-val ctrm = Thm.apply @{cterm \"\<lambda>x. x \<and> False\"} @{cterm \"True\"}
+val ctrm = Thm.apply @{cterm "\<lambda>x. x \<and> False"} @{cterm "True"}
 in
 (conv1 then_conv conv2) ctrm
-end"
+end\<close>
-"(\<lambda>x. x \<and> False) True \<equiv> False"}
+\<open>(\<lambda>x. x \<and> False) True \<equiv> False\<close>}
 where we first beta-reduce the term and then rewrite according to
 @{thm [source] true_conj1}. (When running this example recall the
 problem with the pretty-printer normalising all terms.)
 The conversion combinator @{ML_ind else_conv in Conv} tries out the
 first one, and if it does not apply, tries the second. For example
 @{ML_matchresult_fake [display,gray]
-"let
+\<open>let
 val conv = Conv.rewr_conv @{thm true_conj1} else_conv Conv.all_conv
-val ctrm1 = @{cterm \"True \<and> Q\"}
+val ctrm1 = @{cterm "True \<and> Q"}
-val ctrm2 = @{cterm \"P \<or> (True \<and> Q)\"}
+val ctrm2 = @{cterm "P \<or> (True \<and> Q)"}
 in
 (conv ctrm1, conv ctrm2)
-end"
+end\<close>
-"(True \<and> Q \<equiv> Q, P \<or> True \<and> Q \<equiv> P \<or> True \<and> Q)"}
+\<open>(True \<and> Q \<equiv> Q, P \<or> True \<and> Q \<equiv> P \<or> True \<and> Q)\<close>}
 Here the conversion @{thm [source] true_conj1} only applies
 in the first case, but fails in the second. The whole conversion
 does not fail, however, because the combinator @{ML else_conv in Conv} will then
 try out @{ML all_conv in Conv}, which always succeeds. The same
 behaviour can also be achieved with conversion combinator @{ML_ind try_conv in Conv}.
 For example
 @{ML_matchresult_fake [display,gray]
-"let
+\<open>let
 val conv = Conv.try_conv (Conv.rewr_conv @{thm true_conj1})
-val ctrm = @{cterm \"True \<or> P\"}
+val ctrm = @{cterm "True \<or> P"}
 in
 conv ctrm
-end"
+end\<close>
-"True \<or> P \<equiv> True \<or> P"}
+\<open>True \<or> P \<equiv> True \<or> P\<close>}
 Rewriting with more than one theorem can be done using the function
 @{ML_ind rewrs_conv in Conv} from the structure @{ML_structure Conv}.
 and @{ML_ind arg_conv in Conv} will apply
 a conversion to the first, respectively second, argument of an application.
 For example
 @{ML_matchresult_fake [display,gray]
-"let
+\<open>let
 val conv = Conv.arg_conv (Conv.rewr_conv @{thm true_conj1})
-val ctrm = @{cterm \"P \<or> (True \<and> Q)\"}
+val ctrm = @{cterm "P \<or> (True \<and> Q)"}
 in
 conv ctrm
-end"
+end\<close>
-"P \<or> (True \<and> Q) \<equiv> P \<or> Q"}
+\<open>P \<or> (True \<and> Q) \<equiv> P \<or> Q\<close>}
 The reason for this behaviour is that \<open>(op \<or>)\<close> expects two
 arguments.  Therefore the term must be of the form \<open>(Const \<dots> $ t1) $ t2\<close>. The
 conversion is then applied to \<open>t2\<close>, which in the example above
 stands for @{term "True \<and> Q"}. The function @{ML fun_conv in Conv} would apply
 The function @{ML_ind  abs_conv in Conv} applies a conversion under an
 abstraction. For example:
 @{ML_matchresult_fake [display,gray]
-"let
+\<open>let
 val conv = Conv.rewr_conv @{thm true_conj1}
-val ctrm = @{cterm \"\<lambda>P. True \<and> (P \<and> Foo)\"}
+val ctrm = @{cterm "\<lambda>P. True \<and> (P \<and> Foo)"}
 in
 Conv.abs_conv (K conv) @{context} ctrm
-end"
+end\<close>
-"\<lambda>P. True \<and> (P \<and> Foo) \<equiv> \<lambda>P. P \<and> Foo"}
+\<open>\<lambda>P. True \<and> (P \<and> Foo) \<equiv> \<lambda>P. P \<and> Foo\<close>}
 Note that this conversion needs a context as an argument. We also give the
 conversion as \<open>(K conv)\<close>, which is a function that ignores its
 argument (the argument being a sufficiently freshened version of the
 variable that is abstracted and a context). The conversion that goes under
 we need to transform the @{ML_type cterm} into a @{ML_type term} in order
 to be able to pattern-match the term. To see this
 conversion in action, consider the following example:
 @{ML_matchresult_fake [display,gray]
-"let
+\<open>let
 val conv = true_conj1_conv @{context}
-val ctrm = @{cterm \"distinct [1::nat, x] \<longrightarrow> True \<and> 1 \<noteq> x\"}
+val ctrm = @{cterm "distinct [1::nat, x] \<longrightarrow> True \<and> 1 \<noteq> x"}
 in
 conv ctrm
-end"
+end\<close>
-"distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x \<equiv> distinct [1, x] \<longrightarrow> 1 \<noteq> x"}
+\<open>distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x \<equiv> distinct [1, x] \<longrightarrow> 1 \<noteq> x\<close>}
 \<close>
 text \<open>
 Conversions that traverse terms, like @{ML true_conj1_conv} above, can be
 implemented more succinctly with the combinators @{ML_ind bottom_conv in
 pause for a moment to be convinced that rewriting top-down and bottom-up
 according to the two meta-equations produces two results. Below these
 two results are calculated.
 @{ML_matchresult_fake [display, gray]
-"let
+\<open>let
 val ctxt = @{context}
 val conv = Conv.try_conv (Conv.rewrs_conv @{thms conj_assoc})
 val conv_top = Conv.top_conv (K conv) ctxt
 val conv_bot = Conv.bottom_conv (K conv) ctxt
-val ctrm = @{cterm \"(a \<and> (b \<and> c)) \<and> d\"}
+val ctrm = @{cterm "(a \<and> (b \<and> c)) \<and> d"}
 in
 (conv_top ctrm, conv_bot ctrm)
-end"
+end\<close>
-"(\"(a \<and> (b \<and> c)) \<and> d \<equiv> a \<and> (b \<and> (c \<and> d))\",
+\<open>("(a \<and> (b \<and> c)) \<and> d \<equiv> a \<and> (b \<and> (c \<and> d))",
-\"(a \<and> (b \<and> c)) \<and> d \<equiv> (a \<and> b) \<and> (c \<and> d)\")"}
+"(a \<and> (b \<and> c)) \<and> d \<equiv> (a \<and> b) \<and> (c \<and> d)")\<close>}
 To see how much control you have over rewriting with conversions, let us
 make the task a bit more complicated by rewriting according to the rule
 \<open>true_conj1\<close>, but only in the first arguments of @{term If}s. Then
 the conversion should be as follows.
 root and applies it to all the redexes on the way, but stops in each branch as
 soon as it found one redex. Here is an example for this conversion:
 @{ML_matchresult_fake [display,gray]
-"let
+\<open>let
-val ctrm = @{cterm \"if P (True \<and> 1 \<noteq> (2::nat))
+val ctrm = @{cterm "if P (True \<and> 1 \<noteq> (2::nat))
-then True \<and> True else True \<and> False\"}
+then True \<and> True else True \<and> False"}
 in
 if_true1_conv @{context} ctrm
-end"
+end\<close>
-"if P (True \<and> 1 \<noteq> 2) then True \<and> True else True \<and> False
+\<open>if P (True \<and> 1 \<noteq> 2) then True \<and> True else True \<and> False
-\<equiv> if P (1 \<noteq> 2) then True \<and> True else True \<and> False"}
+\<equiv> if P (1 \<noteq> 2) then True \<and> True else True \<and> False\<close>}
 \<close>
 text \<open>
 So far we only applied conversions to @{ML_type cterm}s. Conversions can, however,
 also work on theorems using the function @{ML_ind  fconv_rule in Conv}. As an example,
 text \<open>
 Using the conversion you can transform this theorem into a
 new theorem as follows
 @{ML_matchresult_fake [display,gray]
-"let
+\<open>let
 val conv = Conv.fconv_rule (true_conj1_conv @{context})
 val thm = @{thm foo_test}
 in
 conv thm
-end"
+end\<close>
-"?P \<or> \<not> ?P"}
+\<open>?P \<or> \<not> ?P\<close>}
 Finally, Isabelle provides function @{ML_ind CONVERSION in Tactical}
 for turning conversions into tactics. This needs some predefined conversion
 combinators that traverse a goal
 state and can selectively apply the conversion. The combinators for
 (Conv.params_conv ~1 (fn ctxt =>
 (Conv.prems_conv ~1 (if_true1_conv ctxt) then_conv
 Conv.concl_conv ~1 (true_conj1_conv ctxt))) ctxt)\<close>
 text \<open>
-We call the conversions with the argument @{ML "~1"}. By this we
+We call the conversions with the argument @{ML \<open>~1\<close>}. By this we
 analyse all parameters, all premises and the conclusion of a goal
 state. If we call @{ML concl_conv in Conv} with
 a non-negative number, say \<open>n\<close>, then this conversions will
 skip the first \<open>n\<close> premises and applies the conversion to the
 ``rest'' (similar for parameters and conclusions). To test the
 theorem @{thm [source] id1_def}
 into @{thm [source] id2_def} by abstracting all variables on the
 left-hand side in the right-hand side.
 @{ML_matchresult_fake [display,gray]
-"Drule.abs_def @{thm id1_def}"
+\<open>Drule.abs_def @{thm id1_def}\<close>
-"id1 \<equiv> \<lambda>x. x"}
+\<open>id1 \<equiv> \<lambda>x. x\<close>}
 Unfortunately, Isabelle has no built-in function that transforms the
 theorems in the other direction. We can implement one using
 conversions. The feature of conversions we are using is that if we apply a
 @{ML_type cterm} to a conversion we obtain a meta-equality theorem (recall
 theorem we want to construct. As mentioned above, in Line 15 we only have to
 export the context \<open>ctxt'\<close> back to \<open>ctxt\<close> in order to
 produce meta-variables for the theorem.  An example is as follows.
 @{ML_matchresult_fake [display, gray]
-"unabs_def @{context} @{thm id2_def}"
+\<open>unabs_def @{context} @{thm id2_def}\<close>
-"id2 ?x1 \<equiv> ?x1"}
+\<open>id2 ?x1 \<equiv> ?x1\<close>}
 \<close>
 text \<open>
 To sum up this section, conversions are more general than the simplifier
 or simprocs, but you have to do more work yourself. Also conversions are

changeset 569	f875a25aa72d
parent 567	f7c97e64cc2a
child 572	438703674711