fixing the cut_tac method to work when there are no instantiations and the
authorpaulson
Thu Oct 17 10:52:59 2002 +0200 (2002-10-17)
changeset 1365031bd2a8cdbe2
parent 13649 0f562a70c07d
child 13651 ac80e101306a
fixing the cut_tac method to work when there are no instantiations and the
supplied theorems have premises
src/Pure/Isar/method.ML
src/Pure/drule.ML
src/Pure/tactic.ML
src/Pure/tctical.ML
     1.1 --- a/src/Pure/Isar/method.ML	Tue Oct 15 15:37:57 2002 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Thu Oct 17 10:52:59 2002 +0200
     1.3 @@ -337,7 +337,7 @@
     1.4  val eres_inst = gen_res_inst Tactic.eres_inst_tac Tactic.eresolve_tac;
     1.5  val dres_inst = gen_res_inst Tactic.dres_inst_tac Tactic.dresolve_tac;
     1.6  val forw_inst = gen_res_inst Tactic.forw_inst_tac Tactic.forward_tac;
     1.7 -val cut_inst = gen_res_inst Tactic.cut_inst_tac Tactic.cut_facts_tac;
     1.8 +val cut_inst = gen_res_inst Tactic.cut_inst_tac Tactic.cut_rules_tac;
     1.9  
    1.10  
    1.11  (* simple Prolog interpreter *)
     2.1 --- a/src/Pure/drule.ML	Tue Oct 15 15:37:57 2002 +0200
     2.2 +++ b/src/Pure/drule.ML	Thu Oct 17 10:52:59 2002 +0200
     2.3 @@ -501,7 +501,10 @@
     2.4  
     2.5  (** theorem equality **)
     2.6  
     2.7 +(*True if the two theorems have the same signature.*)
     2.8  val eq_thm_sg = Sign.eq_sg o pairself Thm.sign_of_thm;
     2.9 +
    2.10 +(*True if the two theorems have the same prop field, ignoring hyps, der, etc.*)
    2.11  val eq_thm_prop = op aconv o pairself Thm.prop_of;
    2.12  
    2.13  (*Useful "distance" function for BEST_FIRST*)
     3.1 --- a/src/Pure/tactic.ML	Tue Oct 15 15:37:57 2002 +0200
     3.2 +++ b/src/Pure/tactic.ML	Thu Oct 17 10:52:59 2002 +0200
     3.3 @@ -29,6 +29,7 @@
     3.4                            int -> tactic
     3.5    val compose_tac       : (bool * thm * int) -> int -> tactic
     3.6    val cut_facts_tac     : thm list -> int -> tactic
     3.7 +  val cut_rules_tac     : thm list -> int -> tactic
     3.8    val cut_inst_tac      : (string*string)list -> thm -> int -> tactic
     3.9    val datac             : thm -> int -> int -> tactic
    3.10    val defer_tac         : int -> tactic
    3.11 @@ -346,9 +347,13 @@
    3.12      case prems_of rl of
    3.13          [] => true  |  _::_ => false;
    3.14  
    3.15 -(*"Cut" all facts from theorem list into the goal as assumptions. *)
    3.16 -fun cut_facts_tac ths i =
    3.17 -    EVERY (map (fn th => metacut_tac th i) (filter is_fact ths));
    3.18 +(*"Cut" a list of rules into the goal.  Their premises will become new
    3.19 +  subgoals.*)
    3.20 +fun cut_rules_tac ths i = EVERY (map (fn th => metacut_tac th i) ths);
    3.21 +
    3.22 +(*As above, but inserts only facts (unconditional theorems);
    3.23 +  generates no additional subgoals. *)
    3.24 +fun cut_facts_tac ths = cut_rules_tac  (filter is_fact ths);
    3.25  
    3.26  (*Introduce the given proposition as a lemma and subgoal*)
    3.27  fun subgoal_tac sprop =
     4.1 --- a/src/Pure/tctical.ML	Tue Oct 15 15:37:57 2002 +0200
     4.2 +++ b/src/Pure/tctical.ML	Thu Oct 17 10:52:59 2002 +0200
     4.3 @@ -291,10 +291,13 @@
     4.4  
     4.5  fun FILTER pred tac st = Seq.filter pred (tac st);
     4.6  
     4.7 +(*Accept only next states that change the theorem somehow*)
     4.8  fun CHANGED tac st =
     4.9    let fun diff st' = not (Thm.eq_thm (st, st'));
    4.10    in Seq.filter diff (tac st) end;
    4.11  
    4.12 +(*Accept only next states that change the theorem's prop field
    4.13 +  (changes to signature, hyps, etc. don't count)*)
    4.14  fun CHANGED_PROP tac st =
    4.15    let fun diff st' = not (Drule.eq_thm_prop (st, st'));
    4.16    in Seq.filter diff (tac st) end;