rewrite: propagate premises to new subgoals
authornoschinl
Mon Apr 13 12:18:47 2015 +0200 (2015-04-13)
changeset 60050dc6ac152d864
parent 60049 e4a5dfee0f9c
child 60051 2a1cab4c9c9d
rewrite: propagate premises to new subgoals
src/HOL/Library/cconv.ML
src/HOL/Library/rewrite.ML
src/HOL/ex/Rewrite_Examples.thy
     1.1 --- a/src/HOL/Library/cconv.ML	Mon Apr 13 11:58:18 2015 +0200
     1.2 +++ b/src/HOL/Library/cconv.ML	Mon Apr 13 12:18:47 2015 +0200
     1.3 @@ -181,12 +181,14 @@
     1.4            ((if n = 1 then fun_cconv else I) o arg_cconv) (prems_cconv (n-1) cv) ct
     1.5        | _ =>  cv ct)
     1.6  
     1.7 +fun inst_imp_cong ct = Thm.instantiate ([], [(@{cpat "?A :: prop"}, ct)]) Drule.imp_cong
     1.8 +
     1.9  (*rewrite B in A1 \<Longrightarrow> ... \<Longrightarrow> An \<Longrightarrow> B*)
    1.10  fun concl_cconv 0 cv ct = cv ct
    1.11    | concl_cconv n cv ct =
    1.12 -      (case ct |> Thm.term_of of
    1.13 -        (Const (@{const_name "Pure.imp"}, _) $ _) $ _ => arg_cconv (concl_cconv (n-1) cv) ct
    1.14 -      | _ =>  cv ct)
    1.15 +      (case try Thm.dest_implies ct of
    1.16 +        NONE => cv ct
    1.17 +      | SOME (A,B) => (concl_cconv (n-1) cv B) RS inst_imp_cong A)
    1.18  
    1.19  (*forward conversion, cf. FCONV_RULE in LCF*)
    1.20  fun fconv_rule cv th =
     2.1 --- a/src/HOL/Library/rewrite.ML	Mon Apr 13 11:58:18 2015 +0200
     2.2 +++ b/src/HOL/Library/rewrite.ML	Mon Apr 13 12:18:47 2015 +0200
     2.3 @@ -76,6 +76,7 @@
     2.4  
     2.5  val fun_rewr_cconv : subterm_position = fn rewr => CConv.fun_cconv oo rewr
     2.6  val arg_rewr_cconv : subterm_position = fn rewr => CConv.arg_cconv oo rewr
     2.7 +val imp_rewr_cconv : subterm_position = fn rewr => CConv.concl_cconv 1 oo rewr
     2.8  
     2.9  
    2.10  (* focus terms *)
    2.11 @@ -102,9 +103,18 @@
    2.12    | ft_fun ctxt (ft as (_, Abs (_, T, _ $ Bound 0), _)) = (ft_fun ctxt o ft_abs ctxt (NONE, T)) ft
    2.13    | ft_fun _ (_, t, _) = raise TERM ("ft_fun", [t])
    2.14  
    2.15 -fun ft_arg _ (tyenv, _ $ r, pos) = (tyenv, r, pos o arg_rewr_cconv)
    2.16 -  | ft_arg ctxt (ft as (_, Abs (_, T, _ $ Bound 0), _)) = (ft_arg ctxt o ft_abs ctxt (NONE, T)) ft
    2.17 -  | ft_arg _ (_, t, _) = raise TERM ("ft_arg", [t])
    2.18 +local
    2.19 +
    2.20 +fun ft_arg_gen cconv _ (tyenv, _ $ r, pos) = (tyenv, r, pos o cconv)
    2.21 +  | ft_arg_gen cconv ctxt (ft as (_, Abs (_, T, _ $ Bound 0), _)) = (ft_arg_gen cconv ctxt o ft_abs ctxt (NONE, T)) ft
    2.22 +  | ft_arg_gen _ _ (_, t, _) = raise TERM ("ft_arg", [t])
    2.23 +
    2.24 +in
    2.25 +
    2.26 +val ft_arg = ft_arg_gen arg_rewr_cconv
    2.27 +val ft_imp = ft_arg_gen imp_rewr_cconv
    2.28 +
    2.29 +end
    2.30  
    2.31  (* Move to B in !!x_1 ... x_n. B. Do not eta-expand *)
    2.32  fun ft_params ctxt (ft as (_, t, _) : focusterm) =
    2.33 @@ -141,7 +151,7 @@
    2.34  
    2.35  fun ft_concl ctxt (ft as (_, t, _) : focusterm) =
    2.36    case t of
    2.37 -    (Const (@{const_name "Pure.imp"}, _) $ _) $ _ => (ft_concl ctxt o ft_arg ctxt) ft
    2.38 +    (Const (@{const_name "Pure.imp"}, _) $ _) $ _ => (ft_concl ctxt o ft_imp ctxt) ft
    2.39    | _ => ft
    2.40  
    2.41  fun ft_assm ctxt (ft as (_, t, _) : focusterm) =
     3.1 --- a/src/HOL/ex/Rewrite_Examples.thy	Mon Apr 13 11:58:18 2015 +0200
     3.2 +++ b/src/HOL/ex/Rewrite_Examples.thy	Mon Apr 13 12:18:47 2015 +0200
     3.3 @@ -89,15 +89,17 @@
     3.4    shows "x \<le> y \<Longrightarrow> x \<ge> y \<Longrightarrow> x = y"
     3.5    by (rule Orderings.order_antisym)
     3.6  
     3.7 +(* Premises of the conditional rule yield new subgoals. The
     3.8 +   assumptions of the goal are propagated into these subgoals
     3.9 +*)
    3.10  lemma
    3.11 -fixes f :: "nat \<Rightarrow> nat"
    3.12 -  assumes "f x \<le> 0" "f x \<ge> 0"
    3.13 -  shows "f x = 0"
    3.14 +  fixes f :: "nat \<Rightarrow> nat"
    3.15 +  shows "f x \<le> 0 \<Longrightarrow> f x \<ge> 0 \<Longrightarrow> f x = 0"
    3.16    apply (rewrite at "f x" to "0" test_theorem)
    3.17 -  apply fact
    3.18 -  apply fact
    3.19 +  apply assumption
    3.20 +  apply assumption
    3.21    apply (rule refl)
    3.22 -done
    3.23 +  done
    3.24  
    3.25  (*
    3.26     Instantiation.