improved rewrite_thm / rewrite_goals to handle conditional eqns;
authorwenzelm
Fri Jul 25 11:47:09 1997 +0200 (1997-07-25)
changeset 35754e9beacb5339
parent 3574 5995ab73d790
child 3576 9cd0a0919ba0
improved rewrite_thm / rewrite_goals to handle conditional eqns;
src/Pure/drule.ML
src/Pure/tactic.ML
     1.1 --- a/src/Pure/drule.ML	Thu Jul 24 15:25:29 1997 +0200
     1.2 +++ b/src/Pure/drule.ML	Fri Jul 25 11:47:09 1997 +0200
     1.3 @@ -48,8 +48,8 @@
     1.4    val revcut_rl		: thm
     1.5    val rewrite_goal_rule	: bool * bool -> (meta_simpset -> thm -> thm option)
     1.6          -> meta_simpset -> int -> thm -> thm
     1.7 -  val rewrite_goals_rule: thm list -> thm -> thm
     1.8 -  val rewrite_rule	: thm list -> thm -> thm
     1.9 +  val rewrite_goals_rule_aux: (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
    1.10 +  val rewrite_rule_aux	: (meta_simpset -> thm -> thm option) -> thm list -> thm -> thm
    1.11    val rewrite_thm	: bool * bool -> (meta_simpset -> thm -> thm option)
    1.12  	-> meta_simpset -> thm -> thm
    1.13    val RS		: thm * thm -> thm
    1.14 @@ -548,19 +548,17 @@
    1.15  fun rew_conv mode prover mss = rewrite_cterm mode mss prover;
    1.16  
    1.17  (*Rewrite a theorem*)
    1.18 -fun rewrite_rule []   th = th
    1.19 -  | rewrite_rule thms th =
    1.20 -	fconv_rule (rew_conv (true,false) (K(K None)) (Thm.mss_of thms)) th;
    1.21 +fun rewrite_rule_aux _ []   th = th
    1.22 +  | rewrite_rule_aux prover thms th =
    1.23 +      fconv_rule (rew_conv (true,false) prover (Thm.mss_of thms)) th;
    1.24  
    1.25  fun rewrite_thm mode prover mss = fconv_rule (rew_conv mode prover mss);
    1.26  
    1.27  (*Rewrite the subgoals of a proof state (represented by a theorem) *)
    1.28 -fun rewrite_goals_rule []   th = th
    1.29 -  | rewrite_goals_rule thms th =
    1.30 -	fconv_rule (goals_conv (K true) 
    1.31 -		    (rew_conv (true,false) (K(K None))
    1.32 -		     (Thm.mss_of thms))) 
    1.33 -	           th;
    1.34 +fun rewrite_goals_rule_aux _ []   th = th
    1.35 +  | rewrite_goals_rule_aux prover thms th =
    1.36 +      fconv_rule (goals_conv (K true) (rew_conv (true, true) prover
    1.37 +        (Thm.mss_of thms))) th;
    1.38  
    1.39  (*Rewrite the subgoal of a proof state (represented by a theorem) *)
    1.40  fun rewrite_goal_rule mode prover mss i thm =
     2.1 --- a/src/Pure/tactic.ML	Thu Jul 24 15:25:29 1997 +0200
     2.2 +++ b/src/Pure/tactic.ML	Fri Jul 25 11:47:09 1997 +0200
     2.3 @@ -1,4 +1,4 @@
     2.4 -(*  Title: 	tactic
     2.5 +(*  Title: 	Pure/tactic.ML
     2.6      ID:         $Id$
     2.7      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     2.8      Copyright   1991  University of Cambridge
     2.9 @@ -72,6 +72,8 @@
    2.10    val resolve_from_net_tac	: (int*thm) Net.net -> int -> tactic
    2.11    val resolve_tac	: thm list -> int -> tactic
    2.12    val res_inst_tac	: (string*string)list -> thm -> int -> tactic   
    2.13 +  val rewrite_goals_rule: thm list -> thm -> thm
    2.14 +  val rewrite_rule	: thm list -> thm -> thm
    2.15    val rewrite_goals_tac	: thm list -> tactic
    2.16    val rewrite_tac	: thm list -> tactic
    2.17    val rewtac		: thm -> tactic
    2.18 @@ -473,6 +475,13 @@
    2.19  fun result1 tacf mss thm =
    2.20    apsome fst (Sequence.pull (tacf mss thm));
    2.21  
    2.22 +val simple_prover =
    2.23 +  result1 (fn mss => ALLGOALS (resolve_tac (prems_of_mss mss)));
    2.24 +
    2.25 +val rewrite_rule = Drule.rewrite_rule_aux simple_prover;
    2.26 +val rewrite_goals_rule = Drule.rewrite_goals_rule_aux simple_prover;
    2.27 +
    2.28 +
    2.29  (*Rewrite subgoal i only.  SELECT_GOAL avoids inefficiencies in goals_conv.*)
    2.30  fun asm_rewrite_goal_tac mode prover_tac mss =
    2.31        SELECT_GOAL