rewrite: do not descend into conclusion of premise with asm pattern
authornoschinl
Mon Apr 13 15:32:32 2015 +0200 (2015-04-13)
changeset 600530e9895ffab1d
parent 60052 616a17640229
child 60054 ef4878146485
rewrite: do not descend into conclusion of premise with asm pattern
src/HOL/Library/rewrite.ML
src/HOL/ex/Rewrite_Examples.thy
     1.1 --- a/src/HOL/Library/rewrite.ML	Mon Apr 13 14:52:40 2015 +0200
     1.2 +++ b/src/HOL/Library/rewrite.ML	Mon Apr 13 15:32:32 2015 +0200
     1.3 @@ -156,7 +156,7 @@
     1.4  
     1.5  fun ft_assm ctxt (ft as (_, t, _) : focusterm) =
     1.6    case t of
     1.7 -    (Const (@{const_name "Pure.imp"}, _) $ _) $ _ => (ft_concl ctxt o ft_arg ctxt o ft_fun ctxt) ft
     1.8 +    (Const (@{const_name "Pure.imp"}, _) $ _) $ _ => (ft_arg ctxt o ft_fun ctxt) ft
     1.9    | _ => raise TERM ("ft_assm", [t])
    1.10  
    1.11  fun ft_judgment ctxt (ft as (_, t, _) : focusterm) =
     2.1 --- a/src/HOL/ex/Rewrite_Examples.thy	Mon Apr 13 14:52:40 2015 +0200
     2.2 +++ b/src/HOL/ex/Rewrite_Examples.thy	Mon Apr 13 15:32:32 2015 +0200
     2.3 @@ -88,6 +88,14 @@
     2.4    shows "PROP R \<Longrightarrow> PROP P \<Longrightarrow> PROP Q"
     2.5      by (rewrite at asm assms)
     2.6  
     2.7 +(* Rewriting "at asm" selects each full assumption, not any parts *)
     2.8 +lemma
     2.9 +  assumes "(PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP S \<Longrightarrow> PROP R)"
    2.10 +  shows "PROP S \<Longrightarrow> (PROP P \<Longrightarrow> PROP Q) \<Longrightarrow> PROP R"
    2.11 +  apply (rewrite at asm assms)
    2.12 +  apply assumption
    2.13 +  done
    2.14 +
    2.15  
    2.16  
    2.17  (* Rewriting with conditional rewriting rules works just as well. *)