src/Provers/classical.ML
changeset 8926 0c7f90147f5d
parent 8727 71acc2d8991a
child 9010 ce78dc5e1a73
equal deleted inserted replaced
8925:f4599af94b83 8926:0c7f90147f5d
   323 
   323 
   324 (*Warn if the rule is already present ELSEWHERE in the claset.  The addition
   324 (*Warn if the rule is already present ELSEWHERE in the claset.  The addition
   325   is still allowed.*)
   325   is still allowed.*)
   326 fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, ...}) = 
   326 fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, ...}) = 
   327        if mem_thm (th, safeIs) then 
   327        if mem_thm (th, safeIs) then 
   328 	 warning ("Rule already in claset as Safe Intr\n" ^ string_of_thm th)
   328 	 warning ("Rule already declared as safe introduction (intro)\n" ^ string_of_thm th)
   329   else if mem_thm (th, safeEs) then
   329   else if mem_thm (th, safeEs) then
   330          warning ("Rule already in claset as Safe Elim\n" ^ string_of_thm th)
   330          warning ("Rule already declared as safe elimination (elim)\n" ^ string_of_thm th)
   331   else if mem_thm (th, hazIs) then 
   331   else if mem_thm (th, hazIs) then 
   332          warning ("Rule already in claset as unsafe Intr\n" ^ string_of_thm th)
   332          warning ("Rule already declared as unsafe introduction (intro?)\n" ^ string_of_thm th)
   333   else if mem_thm (th, hazEs) then 
   333   else if mem_thm (th, hazEs) then 
   334          warning ("Rule already in claset as unsafe Elim\n" ^ string_of_thm th)
   334          warning ("Rule already declared as unsafe elimination (elim?)\n" ^ string_of_thm th)
   335   else if mem_thm (th, xtraIs) then 
   335   else if mem_thm (th, xtraIs) then 
   336          warning ("Rule already in claset as extra Intr\n" ^ string_of_thm th)
   336          warning ("Rule already declared as extra introduction (intro??)\n" ^ string_of_thm th)
   337   else if mem_thm (th, xtraEs) then 
   337   else if mem_thm (th, xtraEs) then 
   338          warning ("Rule already in claset as extra Elim\n" ^ string_of_thm th)
   338          warning ("Rule already declared as extra elimination (elim??)\n" ^ string_of_thm th)
   339   else ();
   339   else ();
   340 
   340 
   341 (*** Safe rules ***)
   341 (*** Safe rules ***)
   342 
   342 
   343 fun addSI (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
   343 fun addSI (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, 
   651 fun delrule (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, ...}, th) =
   651 fun delrule (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, ...}, th) =
   652        if mem_thm (th, safeIs) orelse mem_thm (th, safeEs) orelse
   652        if mem_thm (th, safeIs) orelse mem_thm (th, safeEs) orelse
   653 	  mem_thm (th, hazIs)  orelse mem_thm (th, hazEs) orelse
   653 	  mem_thm (th, hazIs)  orelse mem_thm (th, hazEs) orelse
   654           mem_thm (th, xtraIs)  orelse mem_thm (th, xtraEs) 
   654           mem_thm (th, xtraIs)  orelse mem_thm (th, xtraEs) 
   655        then delSI th (delSE th (delI th (delE th (delXI th (delXE th cs)))))
   655        then delSI th (delSE th (delI th (delE th (delXI th (delXE th cs)))))
   656        else (warning ("Rule not in claset\n" ^ (string_of_thm th)); 
   656        else (warning ("Undeclared classical rule\n" ^ (string_of_thm th)); 
   657 	     cs);
   657 	     cs);
   658 
   658 
   659 val op delrules = foldl delrule;
   659 val op delrules = foldl delrule;
   660 
   660 
   661 
   661