# HG changeset patch # User Christian Urban # Date 1235563712 0 # Node ID f1ba430a5e7d27e26b39bd2cd0b42bf434c82042 # Parent eaba1442c5161c9077967b0f93449f3bbae58a7d some very slight polishing on the conversion section diff -r eaba1442c516 -r f1ba430a5e7d CookBook/Tactical.thy --- a/CookBook/Tactical.thy Wed Feb 25 11:28:41 2009 +0000 +++ b/CookBook/Tactical.thy Wed Feb 25 12:08:32 2009 +0000 @@ -1318,71 +1318,79 @@ section {* Conversions\label{sec:conversion} *} text {* -Conversions are meta-equalities depending on some input term. Their type is -as follows: + + Conversions are a ``thin'' layer on top of Isabelle's inference kernel, and + may be seen as a controllable, bare-bone version of Isabelle's simplifier. + They are meta-equalities depending on some input term. Their type is + as follows: *} -ML {*type conv = Thm.cterm -> Thm.thm*} +ML{*type conv = Thm.cterm -> Thm.thm*} text {* -The simplest two conversions are @{ML "Conv.all_conv"}, which maps a term to an instance of the reflexivity theorem, and @{ML "Conv.no_conv"}, which always fails: + The simplest two conversions are @{ML "Conv.all_conv"}, which maps a + term to an instance of the reflexivity theorem, and + @{ML "Conv.no_conv"}, which always fails: -@{ML_response_fake "Conv.all_conv @{cterm True}" "True \ True"} - -@{ML_response_fake "Conv.no_conv @{cterm True}" "*** Exception- CTERM (\"no conversion\", []) raised"} + @{ML_response_fake [display,gray] + "Conv.all_conv @{cterm True}" "True \ True"} -A further basic conversion is, for example, @{ML "Thm.beta_conversion"}: + @{ML_response_fake [display,gray] + "Conv.no_conv @{cterm True}" + "*** Exception- CTERM (\"no conversion\", []) raised"} + + A further basic conversion is, for example, @{ML "Thm.beta_conversion"}: -@{ML_response_fake "Thm.beta_conversion true @{cterm \"(\x. x \ False) True\"}" -"(\x. x \ False) True \ True \ False"} + @{ML_response_fake [display,gray] + "Thm.beta_conversion true @{cterm \"(\x. x \ False) True\"}" + "(\x. x \ False) True \ True \ False"} -User-defined rewrite rules can be applied by the conversion -@{ML "Conv.rewr_conv"}. Consider, for example, the following rule: + User-defined rewrite rules can be applied by the conversion + @{ML "Conv.rewr_conv"}. Consider, for example, the following rule: *} lemma true_conj1: "True \ P \ P" by simp text {* -Here is how this rule can be used for rewriting: + Here is how this rule can be used for rewriting: -@{ML_response_fake "Conv.rewr_conv @{thm true_conj1} @{cterm \"True \ False\"}" - "True \ False \ False"} + @{ML_response_fake [display,gray] + "Conv.rewr_conv @{thm true_conj1} @{cterm \"True \ False\"}" + "True \ False \ False"} *} text {* -Basic conversions can be combined with a number of conversionals, i.e. -conversion combinators: + Basic conversions can be combined with a number of conversionals, i.e. + conversion combinators: -@{ML_response_fake -"(Thm.beta_conversion true then_conv Conv.rewr_conv @{thm true_conj1}) + @{ML_response_fake [display,gray] + "(Thm.beta_conversion true then_conv Conv.rewr_conv @{thm true_conj1}) @{cterm \"(\x. x \ False) True\"}" -"(\x. x \ False) True \ False"} + "(\x. x \ False) True \ False"} -@{ML_response_fake -"(Conv.rewr_conv @{thm true_conj1} else_conv Conv.all_conv) + @{ML_response_fake [display,gray] + "(Conv.rewr_conv @{thm true_conj1} else_conv Conv.all_conv) @{cterm \"P \ (True \ Q)\"}" -"P \ (True \ Q) \ P \ (True \ Q)"} + "P \ (True \ Q) \ P \ (True \ Q)"} -@{ML_response_fake -"Conv.arg_conv (Conv.rewr_conv @{thm true_conj1}) + @{ML_response_fake [display,gray] + "Conv.arg_conv (Conv.rewr_conv @{thm true_conj1}) @{cterm \"P \ (True \ Q)\"}" -"P \ (True \ Q) \ P \ Q"} + "P \ (True \ Q) \ P \ Q"} -\begin{readmore} -See @{ML_file "Pure/conv.ML"} for more conversionals. Further basic conversions -can be found in, for example, @{ML_file "Pure/thm.ML"}, -@{ML_file "Pure/drule.ML"}, and @{ML_file "Pure/meta_simplifier.ML"}. -\end{readmore} + \begin{readmore} + See @{ML_file "Pure/conv.ML"} for more conversionals. Further basic conversions + can be found in, for example, @{ML_file "Pure/thm.ML"}, + @{ML_file "Pure/drule.ML"}, and @{ML_file "Pure/meta_simplifier.ML"}. + \end{readmore} -Conversions are a thin layer on top of Isabelle's inference kernel, and may -be seen as a controllable, bare-bone version of Isabelle's simplifier. We -will demonstrate this feature in the following example. + We will demonstrate this feature in the following example. -To begin with, let's assumes we want to simplify with the rewrite rule -@{text true_conj1}. As a conversion, this may look as follows: + To begin with, let's assumes we want to simplify with the rewrite rule + @{text true_conj1}. As a conversion, this may look as follows: *} -ML {*fun all_true1_conv ctxt ct = +ML{*fun all_true1_conv ctxt ct = (case Thm.term_of ct of @{term "op \"} $ @{term True} $ _ => (Conv.arg_conv (all_true1_conv ctxt) then_conv @@ -1393,18 +1401,18 @@ | _ => Conv.all_conv ct)*} text {* -Here is this conversion in action: + Here is this conversion in action: -@{ML_response_fake -"all_true1_conv @{context} + @{ML_response_fake [display,gray] + "all_true1_conv @{context} @{cterm \"distinct [1, x] \ True \ 1 \ x\"}" -"distinct [1, x] \ True \ 1 \ x \ distinct [1, x] \ 1 \ x"} + "distinct [1, x] \ True \ 1 \ x \ distinct [1, x] \ 1 \ x"} -Now, let's complicate the task a bit: Rewrite according to the rule -@{text true_conj1}, but only in the first arguments of @{term If}: + Now, let make the task a bit more complicated by rewrite according to the rule + @{text true_conj1}, but only in the first arguments of @{term If}: *} -ML {*fun if_true1_conv ctxt ct = +ML{*fun if_true1_conv ctxt ct = (case Thm.term_of ct of Const (@{const_name If}, _) $ _ => Conv.arg_conv (all_true1_conv ctxt) ct @@ -1414,30 +1422,30 @@ | _ => Conv.all_conv ct)*} text {* -Here is an application of this conversion: + Here is an application of this conversion: -@{ML_response_fake -"if_true1_conv @{context} + @{ML_response_fake [display,gray] + "if_true1_conv @{context} @{cterm \"if P (True \ 1 \ 2) then True \ True else True \ False\"}" -"if P (True \ 1 \ 2) then True \ True else True \ False \ if P (1 \ 2) then True \ True else True \ False"} + "if P (True \ 1 \ 2) then True \ True else True \ False \ if P (1 \ 2) then True \ True else True \ False"} *} text {* -Conversions can also be turned into a tactic with the @{ML CONVERSION} -tactical, and there are predefined conversionals to traverse a goal state. -Given a state @{term "\x. P \ Q"}, the conversional -@{ML Conv.params_conv} applies a conversion to @{term "P \ Q"}; -given a state @{term "\ P1; P2 \ \ Q"}, -the conversional @{ML Conv.prems_conv} applies a conversion to the premises -@{term P1} and @{term P2}, and @{ML Conv.concl_conv} applies a conversion to -the conclusion @{term Q}. + Conversions can also be turned into a tactic with the @{ML CONVERSION} + tactical, and there are predefined conversionals to traverse a goal state. + Given a state @{term "\x. P \ Q"}, the conversional + @{ML Conv.params_conv} applies a conversion to @{term "P \ Q"}; + given a state @{term "\ P1; P2 \ \ Q"}, + the conversional @{ML Conv.prems_conv} applies a conversion to the premises + @{term P1} and @{term P2}, and @{ML Conv.concl_conv} applies a conversion to + the conclusion @{term Q}. -Assume we want to apply @{ML all_true1_conv} only in the conclusion -of the goal, and @{ML if_true1_conv} should only be applied in the premises. -Here is a tactic doing exactly that: + Assume we want to apply @{ML all_true1_conv} only in the conclusion + of the goal, and @{ML if_true1_conv} should only be applied in the premises. + Here is a tactic doing exactly that: *} -ML {*val true1_tac = CSUBGOAL (fn (goal, i) => +ML{*val true1_tac = CSUBGOAL (fn (goal, i) => let val ctxt = ProofContext.init (Thm.theory_of_cterm goal) in CONVERSION ( @@ -1447,7 +1455,7 @@ end)*} text {* -To demonstrate this tactic, consider the following example: + To demonstrate this tactic, consider the following example: *} lemma @@ -1460,20 +1468,18 @@ (*<*)oops(*>*) text {* -Conversions are not restricted to work on certified terms only, they can also -be lifted to theorem transformers, i.e. functions mapping a theorem to a -theorem, by the help of @{ML Conv.fconv_rule}. As an example, consider the -conversion @{ML all_true1_conv} again: + Conversions are not restricted to work on certified terms only, they can also + be lifted to theorem transformers, i.e. functions mapping a theorem to a + theorem, by the help of @{ML Conv.fconv_rule}. As an example, consider the + conversion @{ML all_true1_conv} again: -@{ML_response_fake -"Conv.fconv_rule (all_true1_conv @{context}) - @{lemma \"P \ (True \ \P)\" by simp}" "P \ \P"} + @{ML_response_fake [display,gray] + "Conv.fconv_rule (all_true1_conv @{context}) @{lemma \"P \ (True \ \P)\" by simp}" + "P \ \P"} *} - - section {* Structured Proofs *} text {* TBD *} diff -r eaba1442c516 -r f1ba430a5e7d cookbook.pdf Binary file cookbook.pdf has changed