Added delete function for brls
authorpaulson
Fri Jun 14 12:27:11 1996 +0200 (1996-06-14)
changeset 1801927a31ba4346
parent 1800 3d9d2ef0cd3b
child 1802 d2f07baaf776
Added delete function for brls
src/Pure/tactic.ML
     1.1 --- a/src/Pure/tactic.ML	Fri Jun 14 12:26:06 1996 +0200
     1.2 +++ b/src/Pure/tactic.ML	Fri Jun 14 12:27:11 1996 +0200
     1.3 @@ -46,6 +46,9 @@
     1.4    val insert_tagged_brl:  ('a*(bool*thm)) * 
     1.5                      (('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net) ->
     1.6                      ('a*(bool*thm))Net.net * ('a*(bool*thm))Net.net
     1.7 +  val delete_tagged_brl:  (bool*thm) * 
     1.8 +                    ((int*(bool*thm))Net.net * (int*(bool*thm))Net.net) ->
     1.9 +                    (int*(bool*thm))Net.net * (int*(bool*thm))Net.net
    1.10    val is_fact: thm -> bool
    1.11    val lessb: (bool * thm) * (bool * thm) -> bool
    1.12    val lift_inst_rule: thm * int * (string*string)list * thm -> thm
    1.13 @@ -315,6 +318,20 @@
    1.14  fun build_netpair netpair brls = 
    1.15      foldr insert_tagged_brl (taglist 1 brls, netpair);
    1.16  
    1.17 +(*delete one kbrl from the pair of nets;
    1.18 +  we don't know the value of k, so we use 0 and ignore it in the comparison*)
    1.19 +local
    1.20 +  fun eq_kbrl ((k,(eres,th)), (k',(eres',th'))) = eq_thm (th,th')
    1.21 +in
    1.22 +fun delete_tagged_brl (brl as (eres,th), (inet,enet)) =
    1.23 +    if eres then 
    1.24 +	case prems_of th of
    1.25 +	    prem::_ => (inet, Net.delete_term ((prem, (0,brl)), enet, eq_kbrl))
    1.26 +	  | [] => error"delete_brl: elimination rule with no premises"
    1.27 +    else (Net.delete_term ((concl_of th, (0,brl)), inet, eq_kbrl), enet);
    1.28 +end;
    1.29 +
    1.30 +
    1.31  (*biresolution using a pair of nets rather than rules*)
    1.32  fun biresolution_from_nets_tac match (inet,enet) =
    1.33    SUBGOAL