rewrite: with asm pattern, propagate also remaining assumptions to new subgoals

--- a/src/HOL/Library/Rewrite.thy	Mon Apr 13 15:32:32 2015 +0200
+++ b/src/HOL/Library/Rewrite.thy	Mon Apr 13 20:11:12 2015 +0200
@@ -16,6 +16,21 @@
   fixes f :: "'a::{} \<Rightarrow> 'b::{}"
   shows "f \<equiv> \<lambda>x. f x" .
 
+lemma rewr_imp:
+  assumes "PROP A \<equiv> PROP B"
+  shows "(PROP A \<Longrightarrow> PROP C) \<equiv> (PROP B \<Longrightarrow> PROP C)"
+  apply (rule Pure.equal_intr_rule)
+  apply (drule equal_elim_rule2[OF assms]; assumption)
+  apply (drule equal_elim_rule1[OF assms]; assumption)
+  done
+
+lemma imp_cong_eq:
+  "(PROP A \<Longrightarrow> (PROP B \<Longrightarrow> PROP C) \<equiv> (PROP B' \<Longrightarrow> PROP C')) \<equiv> ((PROP B \<Longrightarrow> PROP A \<Longrightarrow> PROP C) \<equiv> (PROP B' \<Longrightarrow> PROP A \<Longrightarrow> PROP C'))"
+  apply (intro Pure.equal_intr_rule)
+     apply (drule (1) cut_rl; drule Pure.equal_elim_rule1 Pure.equal_elim_rule2; assumption)+
+   apply (drule Pure.equal_elim_rule1 Pure.equal_elim_rule2; assumption)+
+  done
+
 ML_file "cconv.ML"
 ML_file "rewrite.ML"
 

--- a/src/HOL/Library/cconv.ML	Mon Apr 13 15:32:32 2015 +0200
+++ b/src/HOL/Library/cconv.ML	Mon Apr 13 20:11:12 2015 +0200
@@ -33,6 +33,7 @@
   val rewrs_cconv: thm list -> cconv
   val params_cconv: int -> (Proof.context -> cconv) -> Proof.context -> cconv
   val prems_cconv: int -> cconv -> cconv
+  val with_prems_cconv: int -> cconv -> cconv
   val concl_cconv: int -> cconv -> cconv
   val fconv_rule: cconv -> thm -> thm
   val gconv_rule: cconv -> int -> thm -> thm
@@ -190,6 +191,25 @@
         NONE => cv ct
       | SOME (A,B) => (concl_cconv (n-1) cv B) RS inst_imp_cong A)
 
+(* Rewrites A in A \<Longrightarrow> A1 \<Longrightarrow> An \<Longrightarrow> B.
+   The premises of the resulting theorem assume A1, ..., An
+   *)
+fun with_prems_cconv n cv ct =
+  let
+    fun strip_prems 0 As B = (As, B)
+      | strip_prems i As B =
+          case try Thm.dest_implies B of
+            NONE => (As, B)
+          | SOME (A,B) => strip_prems (i - 1) (A::As) B
+    val (prem, (prems, concl)) = ct |> Thm.dest_implies ||> strip_prems n [] 
+    val rewr_imp_concl = Thm.instantiate ([], [(@{cpat "?C :: prop"}, concl)]) @{thm rewr_imp}
+    val th1 = cv prem RS rewr_imp_concl
+    val nprems = Thm.nprems_of th1
+    fun inst_cut_rl ct = Thm.instantiate ([], [(@{cpat "?psi :: prop"}, ct)]) cut_rl
+    fun f p th = (th RS inst_cut_rl p)
+      |> Conv.fconv_rule (Conv.concl_conv nprems (Conv.rewr_conv @{thm imp_cong_eq}))
+  in fold f prems th1 end
+
 (*forward conversion, cf. FCONV_RULE in LCF*)
 fun fconv_rule cv th =
   let

--- a/src/HOL/Library/rewrite.ML	Mon Apr 13 15:32:32 2015 +0200
+++ b/src/HOL/Library/rewrite.ML	Mon Apr 13 20:11:12 2015 +0200
@@ -77,6 +77,7 @@
 val fun_rewr_cconv : subterm_position = fn rewr => CConv.fun_cconv oo rewr
 val arg_rewr_cconv : subterm_position = fn rewr => CConv.arg_cconv oo rewr
 val imp_rewr_cconv : subterm_position = fn rewr => CConv.concl_cconv 1 oo rewr
+val with_prems_rewr_cconv : subterm_position = fn rewr => CConv.with_prems_cconv ~1 oo rewr
 
 
 (* focus terms *)
@@ -154,10 +155,9 @@
     (Const (@{const_name "Pure.imp"}, _) $ _) $ _ => (ft_concl ctxt o ft_imp ctxt) ft
   | _ => ft
 
-fun ft_assm ctxt (ft as (_, t, _) : focusterm) =
-  case t of
-    (Const (@{const_name "Pure.imp"}, _) $ _) $ _ => (ft_arg ctxt o ft_fun ctxt) ft
-  | _ => raise TERM ("ft_assm", [t])
+fun ft_assm _ (tyenv, (Const (@{const_name "Pure.imp"}, _) $ l) $ _, pos) =
+      (tyenv, l, pos o with_prems_rewr_cconv)
+  | ft_assm _ (_, t, _) = raise TERM ("ft_assm", [t])
 
 fun ft_judgment ctxt (ft as (_, t, _) : focusterm) =
   if Object_Logic.is_judgment ctxt t

--- a/src/HOL/ex/Rewrite_Examples.thy	Mon Apr 13 15:32:32 2015 +0200
+++ b/src/HOL/ex/Rewrite_Examples.thy	Mon Apr 13 20:11:12 2015 +0200
@@ -116,6 +116,20 @@
   apply (rule refl)
   done
 
+(* This holds also for rewriting in assumptions. The order of assumptions is preserved *)
+lemma
+  assumes rewr: "PROP P \<Longrightarrow> PROP Q \<Longrightarrow> PROP R \<equiv> PROP R'"
+  assumes A1: "PROP S \<Longrightarrow> PROP T \<Longrightarrow> PROP U \<Longrightarrow> PROP P"
+  assumes A2: "PROP S \<Longrightarrow> PROP T \<Longrightarrow> PROP U \<Longrightarrow> PROP Q"
+  assumes C: "PROP S \<Longrightarrow> PROP R' \<Longrightarrow> PROP T \<Longrightarrow> PROP U \<Longrightarrow> PROP V"
+  shows "PROP S \<Longrightarrow> PROP R \<Longrightarrow> PROP T \<Longrightarrow> PROP U \<Longrightarrow> PROP V"
+  apply (rewrite at asm rewr)
+  apply (fact A1)
+  apply (fact A2)
+  apply (fact C)
+  done
+
+
 (*
    Instantiation.