general type of delete_tagged_brl;
authorwenzelm
Thu Nov 29 00:44:34 2001 +0100 (2001-11-29)
changeset 123206e70d870ddf0
parent 12319 cb3ea5750c3b
child 12321 3b31490191d8
general type of delete_tagged_brl;
tuned;
src/Pure/tactic.ML
     1.1 --- a/src/Pure/tactic.ML	Thu Nov 29 00:43:39 2001 +0100
     1.2 +++ b/src/Pure/tactic.ML	Thu Nov 29 00:44:34 2001 +0100
     1.3 @@ -54,12 +54,12 @@
     1.4    val forward_tac       : thm list -> int -> tactic
     1.5    val forw_inst_tac     : (string*string)list -> thm -> int -> tactic
     1.6    val ftac              : thm -> int ->tactic
     1.7 -  val insert_tagged_brl : ('a*(bool*thm)) *
     1.8 -                          (('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net) ->
     1.9 -                          ('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net
    1.10 -  val delete_tagged_brl : (bool*thm) *
    1.11 -                         ((int*(bool*thm))Net.net * (int*(bool*thm))Net.net) ->
    1.12 -                    (int*(bool*thm))Net.net * (int*(bool*thm))Net.net
    1.13 +  val insert_tagged_brl : ('a * (bool * thm)) *
    1.14 +    (('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net) ->
    1.15 +      ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net
    1.16 +  val delete_tagged_brl : (bool * thm) *
    1.17 +    (('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net) ->
    1.18 +      ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net
    1.19    val is_fact           : thm -> bool
    1.20    val lessb             : (bool * thm) * (bool * thm) -> bool
    1.21    val lift_inst_rule    : thm * int * (string*string)list * thm -> thm
    1.22 @@ -399,28 +399,27 @@
    1.23  fun orderlist kbrls = untaglist (sort (int_ord o pairself fst) kbrls);
    1.24  
    1.25  (*insert one tagged brl into the pair of nets*)
    1.26 -fun insert_tagged_brl (kbrl as (k,(eres,th)), (inet,enet)) =
    1.27 -    if eres then
    1.28 -        case prems_of th of
    1.29 -            prem::_ => (inet, Net.insert_term ((prem,kbrl), enet, K false))
    1.30 -          | [] => error"insert_tagged_brl: elimination rule with no premises"
    1.31 -    else (Net.insert_term ((concl_of th, kbrl), inet, K false), enet);
    1.32 +fun insert_tagged_brl (kbrl as (k, (eres, th)), (inet, enet)) =
    1.33 +  if eres then
    1.34 +    (case try Thm.major_prem_of th of
    1.35 +      Some prem => (inet, Net.insert_term ((prem, kbrl), enet, K false))
    1.36 +    | None => error "insert_tagged_brl: elimination rule with no premises")
    1.37 +  else (Net.insert_term ((concl_of th, kbrl), inet, K false), enet);
    1.38  
    1.39  (*build a pair of nets for biresolution*)
    1.40  fun build_netpair netpair brls =
    1.41      foldr insert_tagged_brl (taglist 1 brls, netpair);
    1.42  
    1.43 -(*delete one kbrl from the pair of nets;
    1.44 -  we don't know the value of k, so we use 0 and ignore it in the comparison*)
    1.45 +(*delete one kbrl from the pair of nets*)
    1.46  local
    1.47 -  fun eq_kbrl ((k,(eres,th)), (k',(eres',th'))) = eq_thm (th,th')
    1.48 +  fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = eq_thm (th, th')
    1.49  in
    1.50 -fun delete_tagged_brl (brl as (eres,th), (inet,enet)) =
    1.51 -    if eres then
    1.52 -        case prems_of th of
    1.53 -            prem::_ => (inet, Net.delete_term ((prem, (0,brl)), enet, eq_kbrl))
    1.54 -          | []      => (inet,enet)     (*no major premise: ignore*)
    1.55 -    else (Net.delete_term ((concl_of th, (0,brl)), inet, eq_kbrl), enet);
    1.56 +fun delete_tagged_brl (brl as (eres, th), (inet, enet)) =
    1.57 +  if eres then
    1.58 +    (case try Thm.major_prem_of th of
    1.59 +      Some prem => (inet, Net.delete_term ((prem, ((), brl)), enet, eq_kbrl))
    1.60 +    | None => (inet, enet))  (*no major premise: ignore*)
    1.61 +  else (Net.delete_term ((Thm.concl_of th, ((), brl)), inet, eq_kbrl), enet);
    1.62  end;
    1.63  
    1.64