summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | noschinl |

Mon, 13 Apr 2015 14:52:40 +0200 | |

changeset 60052 | 616a17640229 |

parent 60051 | 2a1cab4c9c9d |

child 60053 | 0e9895ffab1d |

rewrite: with asm pattern, try all premises for rewriting, not only the first

src/HOL/Library/rewrite.ML | file | annotate | diff | comparison | revisions | |

src/HOL/ex/Rewrite_Examples.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Library/rewrite.ML Mon Apr 13 14:45:44 2015 +0200 +++ b/src/HOL/Library/rewrite.ML Mon Apr 13 14:52:40 2015 +0200 @@ -253,14 +253,16 @@ | SOME ft => SOME ft in desc eta_expands ft end - fun seq_unfold f ft = - case f ft of - NONE => Seq.empty - | SOME ft' => Seq.cons ft' (seq_unfold f ft') + fun move_assms ctxt (ft: focusterm) = + let + fun f () = case try (ft_assm ctxt) ft of + NONE => NONE + | SOME ft' => SOME (ft', move_assms ctxt (ft_imp ctxt ft)) + in Seq.make f end fun apply_pat At = Seq.map (ft_judgment ctxt) | apply_pat In = Seq.maps (valid_match_points ctxt) - | apply_pat Asm = Seq.maps (seq_unfold (try (ft_assm ctxt)) o ft_params ctxt) + | apply_pat Asm = Seq.maps (move_assms ctxt o ft_params ctxt) | apply_pat Concl = Seq.map (ft_concl ctxt o ft_params ctxt) | apply_pat (For idents) = Seq.map_filter ((ft_for ctxt (map (apfst SOME) idents))) | apply_pat (Term x) = Seq.map_filter ( (move_term ctxt x))

--- a/src/HOL/ex/Rewrite_Examples.thy Mon Apr 13 14:45:44 2015 +0200 +++ b/src/HOL/ex/Rewrite_Examples.thy Mon Apr 13 14:52:40 2015 +0200 @@ -82,6 +82,13 @@ shows "P {(x::nat, y::nat, z). x + z * 3 = Q (\<lambda>s t. y + s * t - 3)}" by (rewrite at "b + d * e" in "\<lambda>(a, b, c). _ = Q (\<lambda>d e. \<hole>)" add.commute) fact +(* This is not limited to the first assumption *) +lemma + assumes "PROP P \<equiv> PROP Q" + shows "PROP R \<Longrightarrow> PROP P \<Longrightarrow> PROP Q" + by (rewrite at asm assms) + + (* Rewriting with conditional rewriting rules works just as well. *) lemma test_theorem: