streamlined addIffs/delIffs, added warnings
authoroheimb
Thu May 31 16:52:02 2001 +0200 (2001-05-31)
changeset 1134457b7ad51971c
parent 11343 d5f1b482bfbf
child 11345 cd605c85e421
streamlined addIffs/delIffs, added warnings
src/FOL/simpdata.ML
src/HOL/simpdata.ML
src/Provers/clasimp.ML
     1.1 --- a/src/FOL/simpdata.ML	Thu May 31 16:51:26 2001 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Thu May 31 16:52:02 2001 +0200
     1.3 @@ -359,9 +359,7 @@
     1.4  structure Clasimp = ClasimpFun
     1.5   (structure Simplifier = Simplifier and Splitter = Splitter
     1.6    and Classical  = Cla and Blast = Blast
     1.7 -  val dest_Trueprop = FOLogic.dest_Trueprop
     1.8 -  val iff_const = FOLogic.iff val not_const = FOLogic.not
     1.9 -  val notE = notE val iffD1 = iffD1 val iffD2 = iffD2
    1.10 +  val iffD1 = iffD1 val iffD2 = iffD2 val notE = notE
    1.11    val cla_make_elim = cla_make_elim);
    1.12  open Clasimp;
    1.13  
     2.1 --- a/src/HOL/simpdata.ML	Thu May 31 16:51:26 2001 +0200
     2.2 +++ b/src/HOL/simpdata.ML	Thu May 31 16:52:02 2001 +0200
     2.3 @@ -454,10 +454,7 @@
     2.4  structure Clasimp = ClasimpFun
     2.5   (structure Simplifier = Simplifier and Splitter = Splitter
     2.6    and Classical  = Classical and Blast = Blast
     2.7 -  val dest_Trueprop = HOLogic.dest_Trueprop
     2.8 -  val iff_const = HOLogic.eq_const HOLogic.boolT
     2.9 -  val not_const = HOLogic.not_const
    2.10 -  val notE = notE val iffD1 = iffD1 val iffD2 = iffD2
    2.11 +  val iffD1 = iffD1 val iffD2 = iffD2 val notE = notE
    2.12    val cla_make_elim = cla_make_elim);
    2.13  open Clasimp;
    2.14  
     3.1 --- a/src/Provers/clasimp.ML	Thu May 31 16:51:26 2001 +0200
     3.2 +++ b/src/Provers/clasimp.ML	Thu May 31 16:52:02 2001 +0200
     3.3 @@ -16,9 +16,6 @@
     3.4    structure Classical: CLASSICAL
     3.5    structure Blast: BLAST
     3.6    sharing type Classical.claset = Blast.claset
     3.7 -  val dest_Trueprop: term -> term
     3.8 -  val not_const: term
     3.9 -  val iff_const: term
    3.10    val notE: thm
    3.11    val iffD1: thm
    3.12    val iffD2: thm
    3.13 @@ -116,39 +113,30 @@
    3.14  
    3.15  (* iffs: addition of rules to simpsets and clasets simultaneously *)
    3.16  
    3.17 -(*Takes UNCONDITIONAL theorems of the form A<->B to
    3.18 +(*Takes (possibly conditional) theorems of the form A<->B to
    3.19          the Safe Intr     rule B==>A and
    3.20          the Safe Destruct rule A==>B.
    3.21    Also ~A goes to the Safe Elim rule A ==> ?R
    3.22 -  Failing other cases, A is added as a Safe Intr rule*)
    3.23 +  Failing other cases, A is added as a Safe Intr rule and a warning is issued *)
    3.24  local
    3.25  
    3.26  fun addIff dest elim intro simp ((cs, ss), th) =
    3.27 -  (case dest_Trueprop (#prop (Thm.rep_thm th)) of
    3.28 -    con $ _ $ _ =>
    3.29 -      if con = Data.iff_const then
    3.30 -        dest (intro (cs, [zero_var_indexes (th RS Data.iffD2)]),
    3.31 -          [zero_var_indexes (th RS Data.iffD1)])
    3.32 -      else intro (cs, [th])
    3.33 -  | con $ A =>
    3.34 -      if con = Data.not_const then elim (cs, [zero_var_indexes (th RS Data.notE)])
    3.35 -      else intro (cs, [th])
    3.36 -  | _ => intro (cs, [th]), simp (ss, [th]))
    3.37 -  handle TERM _ => error ("iff add: theorem must be unconditional\n" ^ Display.string_of_thm th);
    3.38 +  (          dest (intro (cs, [zero_var_indexes (th RS Data.iffD2)]),
    3.39 +                              [zero_var_indexes (th RS Data.iffD1)])
    3.40 +   handle THM _ => (warning ("iff add: theorem is not an equivalence\n" 
    3.41 +                  ^ Display.string_of_thm th);
    3.42 +                    elim (cs, [zero_var_indexes (th RS Data.notE )])
    3.43 +   handle THM _ => intro (cs, [th])),
    3.44 +   simp (ss, [th]));
    3.45  
    3.46  fun delIff ((cs, ss), th) =
    3.47 -  (case dest_Trueprop (#prop (Thm.rep_thm th)) of
    3.48 -    con $ _ $ _ =>
    3.49 -      if con = Data.iff_const then
    3.50 -        Classical.delrules (cs, [zero_var_indexes (th RS Data.iffD2),
    3.51 -          Data.cla_make_elim (zero_var_indexes (th RS Data.iffD1))])
    3.52 -      else Classical.delrules (cs, [th])
    3.53 -  | con $ A =>
    3.54 -      if con = Data.not_const then Classical.delrules (cs, [zero_var_indexes (th RS Data.notE)])
    3.55 -      else Classical.delrules (cs, [th])
    3.56 -  | _ => Classical.delrules (cs, [th]), Simplifier.delsimps (ss, [th]))
    3.57 -  handle TERM _ =>
    3.58 -    (warning ("iff del: ignoring conditional theorem\n" ^ string_of_thm th); (cs, ss));
    3.59 +(                Classical.delrules (cs, [zero_var_indexes (th RS Data.iffD2),
    3.60 +                      Data.cla_make_elim (zero_var_indexes (th RS Data.iffD1))])
    3.61 + handle THM _ => (warning ("iff del: theorem is not an equivalence\n" 
    3.62 +                  ^ Display.string_of_thm th);
    3.63 +                 Classical.delrules (cs, [zero_var_indexes (th RS Data.notE)])
    3.64 + handle THM _ => Classical.delrules (cs, [th])), 
    3.65 + Simplifier.delsimps (ss, [th]));
    3.66  
    3.67  fun store_clasimp (cs, ss) =
    3.68    (Classical.claset_ref () := cs; Simplifier.simpset_ref () := ss);