# HG changeset patch # User Christian Urban # Date 1235556790 0 # Node ID f7cf072e72d6a1281aa5b506da8e5d07691bf15f # Parent e4d8dfb7e34ae815c5b588e3194af84931fab870# Parent c06885c3657527a93c250b365cc0813335990f57 merged with Sascha diff -r e4d8dfb7e34a -r f7cf072e72d6 CookBook/Tactical.thy --- a/CookBook/Tactical.thy Wed Feb 25 10:09:18 2009 +0000 +++ b/CookBook/Tactical.thy Wed Feb 25 10:13:10 2009 +0000 @@ -1,5 +1,6 @@ theory Tactical imports Base FirstSteps +uses "infix_conv.ML" begin chapter {* Tactical Reasoning\label{chp:tactical} *} @@ -1317,96 +1318,157 @@ section {* Conversions\label{sec:conversion} *} text {* -conversions: core of the simplifier - -see: Pure/conv.ML -*} - -ML {* type conv = Thm.cterm -> Thm.thm *} - -text {* -simple example: -*} - -lemma true_conj_1: "True \ P \ P" by simp - -ML {* -val true1_conv = Conv.rewr_conv @{thm true_conj_1} -*} - -ML {* -true1_conv @{cterm "True \ False"} +Conversions are meta-equalities depending on some input term. Their type is +as follows: *} -text {* -@{ML_response_fake "true1_conv @{cterm \"True \ False\"}" - "True \ False \ False"} -*} +ML {*type conv = Thm.cterm -> Thm.thm*} text {* -how to extend rewriting to more complex cases? e.g.: +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"} + +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"} + +User-defined rewrite rules can be applied by the conversion +@{ML "Conv.rewr_conv"}. Consider, for example, the following rule: *} -ML {* -val complex = @{cterm "distinct [1, x] \ True \ 1 \ (x::int)"} -*} - -text {* conversionals: basically a count-down version of MetaSimplifier.rewrite *} +lemma true_conj1: "True \ P \ P" by simp -ML {* -fun all_true1_conv ctxt ct = - (case Thm.term_of ct of - @{term "op \"} $ @{term True} $ _ => true1_conv ct - | _ $ _ => Conv.combination_conv (all_true1_conv ctxt) (all_true1_conv ctxt) ct - | Abs _ => Conv.abs_conv (fn (_, cx) => all_true1_conv cx) ctxt ct) +text {* +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"} *} text {* -@{ML_response_fake "all_true1_conv @{context} complex" - "distinct [1, x] \ True \ 1 \ x \ distinct [1, x] \ 1 \ x"} +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}) + @{cterm \"(\x. x \ False) True\"}" +"(\x. x \ False) True \ False"} + +@{ML_response_fake +"(Conv.rewr_conv @{thm true_conj1} else_conv Conv.all_conv) + @{cterm \"P \ (True \ Q)\"}" +"P \ (True \ Q) \ P \ (True \ Q)"} + +@{ML_response_fake +"Conv.arg_conv (Conv.rewr_conv @{thm true_conj1}) + @{cterm \"P \ (True \ 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} + +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. + +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 = + (case Thm.term_of ct of + @{term "op \"} $ @{term True} $ _ => + (Conv.arg_conv (all_true1_conv ctxt) then_conv + Conv.rewr_conv @{thm true_conj1}) ct + | _ $ _ => Conv.combination_conv (all_true1_conv ctxt) + (all_true1_conv ctxt) ct + | Abs _ => Conv.abs_conv (fn (_, cx) => all_true1_conv cx) ctxt ct + | _ => Conv.all_conv ct)*} text {* -transforming theorems: @{ML "Conv.fconv_rule"} (give type) - -example: -*} +Here is this conversion in action: -lemma foo: "True \ (P \ \P)" by simp +@{ML_response_fake +"all_true1_conv @{context} + @{cterm \"distinct [1, x] \ True \ 1 \ x\"}" +"distinct [1, x] \ True \ 1 \ x \ distinct [1, x] \ 1 \ x"} -text {* -@{ML_response_fake "Conv.fconv_rule (Conv.arg_conv (all_true1_conv @{context})) @{thm foo}" "P \ \P"} +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}: *} -text {* now, replace "True and P" with "P" if it occurs inside an 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 - | _ $ _ => Conv.combination_conv (if_true1_conv ctxt) (if_true1_conv ctxt) ct - | Abs _ => Conv.abs_conv (fn (_, cx) => if_true1_conv cx) ctxt ct) + Const (@{const_name If}, _) $ _ => + Conv.arg_conv (all_true1_conv ctxt) ct + | _ $ _ => Conv.combination_conv (if_true1_conv ctxt) + (if_true1_conv ctxt) ct + | Abs _ => Conv.abs_conv (fn (_, cx) => if_true1_conv cx) ctxt ct + | _ => Conv.all_conv ct)*} + +text {* +Here is an application of this conversion: + +@{ML_response_fake +"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"} *} -text {* show example *} - text {* -conversions inside a tactic: replace "true" in conclusion, "if true" in assumptions +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: *} -ML {* -local open Conv -in -fun true1_tac ctxt = - CONVERSION ( - Conv.params_conv ~1 (fn cx => - (Conv.prems_conv ~1 (if_true1_conv cx)) then_conv - (Conv.concl_conv ~1 (all_true1_conv cx))) ctxt) -end +ML {*val true1_tac = CSUBGOAL (fn (goal, i) => + let val ctxt = ProofContext.init (Thm.theory_of_cterm goal) + in + CONVERSION ( + Conv.params_conv ~1 (fn cx => + (Conv.prems_conv ~1 (if_true1_conv cx)) then_conv + Conv.concl_conv ~1 (all_true1_conv cx)) ctxt) i + end)*} + +text {* +To demonstrate this tactic, consider the following example: *} -text {* give example, show that the conditional rewriting works *} +lemma + "if True \ P then P else True \ False \ + (if True \ Q then Q else P) \ True \ (True \ Q)" +apply(tactic {* true1_tac 1 *}) +txt {* \begin{minipage}{\textwidth} + @{subgoals [display]} + \end{minipage} *} +(*<*)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: + +@{ML_response_fake +"Conv.fconv_rule (all_true1_conv @{context}) + @{lemma \"P \ (True \ \P)\" by simp}" "P \ \P"} +*} @@ -1453,4 +1515,4 @@ -end \ No newline at end of file +end diff -r e4d8dfb7e34a -r f7cf072e72d6 CookBook/infix_conv.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/CookBook/infix_conv.ML Wed Feb 25 10:13:10 2009 +0000 @@ -0,0 +1,9 @@ +signature INFIX_CONV = +sig + val then_conv : Thm.conv * Thm.conv -> Thm.conv + val else_conv : Thm.conv * Thm.conv -> Thm.conv +end + +structure InfixConv : INFIX_CONV = Conv + +open InfixConv diff -r e4d8dfb7e34a -r f7cf072e72d6 cookbook.pdf Binary file cookbook.pdf has changed