# HG changeset patch
# User noschinl
# Date 1428920327 -7200
# Node ID dc6ac152d8643c876d0280c0452a101e982f338c
# Parent  e4a5dfee0f9c77183e340c57f6fddddd76078f81
rewrite: propagate premises to new subgoals

diff -r e4a5dfee0f9c -r dc6ac152d864 src/HOL/Library/cconv.ML
--- a/src/HOL/Library/cconv.ML	Mon Apr 13 11:58:18 2015 +0200
+++ b/src/HOL/Library/cconv.ML	Mon Apr 13 12:18:47 2015 +0200
@@ -181,12 +181,14 @@
           ((if n = 1 then fun_cconv else I) o arg_cconv) (prems_cconv (n-1) cv) ct
       | _ =>  cv ct)
 
+fun inst_imp_cong ct = Thm.instantiate ([], [(@{cpat "?A :: prop"}, ct)]) Drule.imp_cong
+
 (*rewrite B in A1 \<Longrightarrow> ... \<Longrightarrow> An \<Longrightarrow> B*)
 fun concl_cconv 0 cv ct = cv ct
   | concl_cconv n cv ct =
-      (case ct |> Thm.term_of of
-        (Const (@{const_name "Pure.imp"}, _) $ _) $ _ => arg_cconv (concl_cconv (n-1) cv) ct
-      | _ =>  cv ct)
+      (case try Thm.dest_implies ct of
+        NONE => cv ct
+      | SOME (A,B) => (concl_cconv (n-1) cv B) RS inst_imp_cong A)
 
 (*forward conversion, cf. FCONV_RULE in LCF*)
 fun fconv_rule cv th =
diff -r e4a5dfee0f9c -r dc6ac152d864 src/HOL/Library/rewrite.ML
--- a/src/HOL/Library/rewrite.ML	Mon Apr 13 11:58:18 2015 +0200
+++ b/src/HOL/Library/rewrite.ML	Mon Apr 13 12:18:47 2015 +0200
@@ -76,6 +76,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
 
 
 (* focus terms *)
@@ -102,9 +103,18 @@
   | ft_fun ctxt (ft as (_, Abs (_, T, _ $ Bound 0), _)) = (ft_fun ctxt o ft_abs ctxt (NONE, T)) ft
   | ft_fun _ (_, t, _) = raise TERM ("ft_fun", [t])
 
-fun ft_arg _ (tyenv, _ $ r, pos) = (tyenv, r, pos o arg_rewr_cconv)
-  | ft_arg ctxt (ft as (_, Abs (_, T, _ $ Bound 0), _)) = (ft_arg ctxt o ft_abs ctxt (NONE, T)) ft
-  | ft_arg _ (_, t, _) = raise TERM ("ft_arg", [t])
+local
+
+fun ft_arg_gen cconv _ (tyenv, _ $ r, pos) = (tyenv, r, pos o cconv)
+  | ft_arg_gen cconv ctxt (ft as (_, Abs (_, T, _ $ Bound 0), _)) = (ft_arg_gen cconv ctxt o ft_abs ctxt (NONE, T)) ft
+  | ft_arg_gen _ _ (_, t, _) = raise TERM ("ft_arg", [t])
+
+in
+
+val ft_arg = ft_arg_gen arg_rewr_cconv
+val ft_imp = ft_arg_gen imp_rewr_cconv
+
+end
 
 (* Move to B in !!x_1 ... x_n. B. Do not eta-expand *)
 fun ft_params ctxt (ft as (_, t, _) : focusterm) =
@@ -141,7 +151,7 @@
 
 fun ft_concl ctxt (ft as (_, t, _) : focusterm) =
   case t of
-    (Const (@{const_name "Pure.imp"}, _) $ _) $ _ => (ft_concl ctxt o ft_arg ctxt) ft
+    (Const (@{const_name "Pure.imp"}, _) $ _) $ _ => (ft_concl ctxt o ft_imp ctxt) ft
   | _ => ft
 
 fun ft_assm ctxt (ft as (_, t, _) : focusterm) =
diff -r e4a5dfee0f9c -r dc6ac152d864 src/HOL/ex/Rewrite_Examples.thy
--- a/src/HOL/ex/Rewrite_Examples.thy	Mon Apr 13 11:58:18 2015 +0200
+++ b/src/HOL/ex/Rewrite_Examples.thy	Mon Apr 13 12:18:47 2015 +0200
@@ -89,15 +89,17 @@
   shows "x \<le> y \<Longrightarrow> x \<ge> y \<Longrightarrow> x = y"
   by (rule Orderings.order_antisym)
 
+(* Premises of the conditional rule yield new subgoals. The
+   assumptions of the goal are propagated into these subgoals
+*)
 lemma
-fixes f :: "nat \<Rightarrow> nat"
-  assumes "f x \<le> 0" "f x \<ge> 0"
-  shows "f x = 0"
+  fixes f :: "nat \<Rightarrow> nat"
+  shows "f x \<le> 0 \<Longrightarrow> f x \<ge> 0 \<Longrightarrow> f x = 0"
   apply (rewrite at "f x" to "0" test_theorem)
-  apply fact
-  apply fact
+  apply assumption
+  apply assumption
   apply (rule refl)
-done
+  done
 
 (*
    Instantiation.