--- 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 =
--- 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) =
--- 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.