rewrite: with asm pattern, try all premises for rewriting, not only the first
authornoschinl
Mon Apr 13 14:52:40 2015 +0200 (2015-04-13)
changeset 60052616a17640229
parent 60051 2a1cab4c9c9d
child 60053 0e9895ffab1d
rewrite: with asm pattern, try all premises for rewriting, not only the first
src/HOL/Library/rewrite.ML
src/HOL/ex/Rewrite_Examples.thy
     1.1 --- a/src/HOL/Library/rewrite.ML	Mon Apr 13 14:45:44 2015 +0200
     1.2 +++ b/src/HOL/Library/rewrite.ML	Mon Apr 13 14:52:40 2015 +0200
     1.3 @@ -253,14 +253,16 @@
     1.4              | SOME ft => SOME ft
     1.5        in desc eta_expands ft end
     1.6  
     1.7 -    fun seq_unfold f ft =
     1.8 -      case f ft of
     1.9 -        NONE => Seq.empty
    1.10 -      | SOME ft' => Seq.cons ft' (seq_unfold f ft')
    1.11 +    fun move_assms ctxt (ft: focusterm) =
    1.12 +      let
    1.13 +        fun f () = case try (ft_assm ctxt) ft of
    1.14 +            NONE => NONE
    1.15 +          | SOME ft' => SOME (ft', move_assms ctxt (ft_imp ctxt ft))
    1.16 +      in Seq.make f end
    1.17  
    1.18      fun apply_pat At = Seq.map (ft_judgment ctxt)
    1.19        | apply_pat In = Seq.maps (valid_match_points ctxt)
    1.20 -      | apply_pat Asm = Seq.maps (seq_unfold (try (ft_assm ctxt)) o ft_params ctxt)
    1.21 +      | apply_pat Asm = Seq.maps (move_assms ctxt o ft_params ctxt)
    1.22        | apply_pat Concl = Seq.map (ft_concl ctxt o ft_params ctxt)
    1.23        | apply_pat (For idents) = Seq.map_filter ((ft_for ctxt (map (apfst SOME) idents)))
    1.24        | apply_pat (Term x) = Seq.map_filter ( (move_term ctxt x))
     2.1 --- a/src/HOL/ex/Rewrite_Examples.thy	Mon Apr 13 14:45:44 2015 +0200
     2.2 +++ b/src/HOL/ex/Rewrite_Examples.thy	Mon Apr 13 14:52:40 2015 +0200
     2.3 @@ -82,6 +82,13 @@
     2.4    shows   "P {(x::nat, y::nat, z). x + z * 3 = Q (\<lambda>s t. y + s * t - 3)}"
     2.5    by (rewrite at "b + d * e" in "\<lambda>(a, b, c). _ = Q (\<lambda>d e. \<hole>)" add.commute) fact
     2.6  
     2.7 +(* This is not limited to the first assumption *)
     2.8 +lemma
     2.9 +  assumes "PROP P \<equiv> PROP Q"
    2.10 +  shows "PROP R \<Longrightarrow> PROP P \<Longrightarrow> PROP Q"
    2.11 +    by (rewrite at asm assms)
    2.12 +
    2.13 +
    2.14  
    2.15  (* Rewriting with conditional rewriting rules works just as well. *)
    2.16  lemma test_theorem: