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

author | noschinl |

Mon, 13 Apr 2015 15:32:32 +0200 | |

changeset 60053 | 0e9895ffab1d |

parent 60052 | 616a17640229 |

child 60054 | ef4878146485 |

rewrite: do not descend into conclusion of premise with asm pattern

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:52:40 2015 +0200 +++ b/src/HOL/Library/rewrite.ML Mon Apr 13 15:32:32 2015 +0200 @@ -156,7 +156,7 @@ fun ft_assm ctxt (ft as (_, t, _) : focusterm) = case t of - (Const (@{const_name "Pure.imp"}, _) $ _) $ _ => (ft_concl ctxt o ft_arg ctxt o ft_fun ctxt) ft + (Const (@{const_name "Pure.imp"}, _) $ _) $ _ => (ft_arg ctxt o ft_fun ctxt) ft | _ => raise TERM ("ft_assm", [t]) fun ft_judgment ctxt (ft as (_, t, _) : focusterm) =

--- a/src/HOL/ex/Rewrite_Examples.thy Mon Apr 13 14:52:40 2015 +0200 +++ b/src/HOL/ex/Rewrite_Examples.thy Mon Apr 13 15:32:32 2015 +0200 @@ -88,6 +88,14 @@ shows "PROP R \<Longrightarrow> PROP P \<Longrightarrow> PROP Q" by (rewrite at asm assms) +(* Rewriting "at asm" selects each full assumption, not any parts *) +lemma + assumes "(PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP S \<Longrightarrow> PROP R)" + shows "PROP S \<Longrightarrow> (PROP P \<Longrightarrow> PROP Q) \<Longrightarrow> PROP R" + apply (rewrite at asm assms) + apply assumption + done + (* Rewriting with conditional rewriting rules works just as well. *)