# HG changeset patch # User wenzelm # Date 968773129 -7200 # Node ID cb6a7572d0a13543fdf55cdab18c939424b8064f # Parent 431c96ac997ee2945929c69808bc7a42898a575a delrule: handle dest rules as well; replaced "delrule" by "rule del"; diff -r 431c96ac997e -r cb6a7572d0a1 src/Provers/classical.ML --- a/src/Provers/classical.ML Tue Sep 12 17:35:09 2000 +0200 +++ b/src/Provers/classical.ML Tue Sep 12 17:38:49 2000 +0200 @@ -1,6 +1,6 @@ -(* Title: Provers/classical.ML +(* Title: Provers/classical.ML ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1992 University of Cambridge Theorem prover for classical reasoning, including predicate calculus, set @@ -28,10 +28,10 @@ signature CLASSICAL_DATA = sig val make_elim : thm -> thm (* Tactic.make_elim or a classical version*) - val mp : thm (* [| P-->Q; P |] ==> Q *) - val not_elim : thm (* [| ~P; P |] ==> R *) - val classical : thm (* (~P ==> P) ==> P *) - val sizef : thm -> int (* size function for BEST_FIRST *) + val mp : thm (* [| P-->Q; P |] ==> Q *) + val not_elim : thm (* [| ~P; P |] ==> R *) + val classical : thm (* (~P ==> P) ==> P *) + val sizef : thm -> int (* size function for BEST_FIRST *) val hyp_subst_tacs: (int -> tactic) list end; @@ -43,35 +43,35 @@ val print_claset: theory -> unit val rep_cs: (* BLAST_DATA in blast.ML dependent on this *) claset -> {safeIs: thm list, safeEs: thm list, - hazIs: thm list, hazEs: thm list, - xtraIs: thm list, xtraEs: thm list, - swrappers: (string * wrapper) list, - uwrappers: (string * wrapper) list, - safe0_netpair: netpair, safep_netpair: netpair, - haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: netpair} - val merge_cs : claset * claset -> claset - val addDs : claset * thm list -> claset - val addEs : claset * thm list -> claset - val addIs : claset * thm list -> claset - val addSDs : claset * thm list -> claset - val addSEs : claset * thm list -> claset - val addSIs : claset * thm list -> claset - val delrules : claset * thm list -> claset - val addSWrapper : claset * (string * wrapper) -> claset - val delSWrapper : claset * string -> claset - val addWrapper : claset * (string * wrapper) -> claset - val delWrapper : claset * string -> claset - val addSbefore : claset * (string * (int -> tactic)) -> claset - val addSaltern : claset * (string * (int -> tactic)) -> claset - val addbefore : claset * (string * (int -> tactic)) -> claset - val addaltern : claset * (string * (int -> tactic)) -> claset + hazIs: thm list, hazEs: thm list, + xtraIs: thm list, xtraEs: thm list, + swrappers: (string * wrapper) list, + uwrappers: (string * wrapper) list, + safe0_netpair: netpair, safep_netpair: netpair, + haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: netpair} + val merge_cs : claset * claset -> claset + val addDs : claset * thm list -> claset + val addEs : claset * thm list -> claset + val addIs : claset * thm list -> claset + val addSDs : claset * thm list -> claset + val addSEs : claset * thm list -> claset + val addSIs : claset * thm list -> claset + val delrules : claset * thm list -> claset + val addSWrapper : claset * (string * wrapper) -> claset + val delSWrapper : claset * string -> claset + val addWrapper : claset * (string * wrapper) -> claset + val delWrapper : claset * string -> claset + val addSbefore : claset * (string * (int -> tactic)) -> claset + val addSaltern : claset * (string * (int -> tactic)) -> claset + val addbefore : claset * (string * (int -> tactic)) -> claset + val addaltern : claset * (string * (int -> tactic)) -> claset val addD2 : claset * (string * thm) -> claset val addE2 : claset * (string * thm) -> claset val addSD2 : claset * (string * thm) -> claset val addSE2 : claset * (string * thm) -> claset - val appSWrappers : claset -> wrapper - val appWrappers : claset -> wrapper - val trace_rules : bool ref + val appSWrappers : claset -> wrapper + val appWrappers : claset -> wrapper + val trace_rules : bool ref val claset_ref_of_sg: Sign.sg -> claset ref val claset_ref_of: theory -> claset ref @@ -82,59 +82,59 @@ val claset: unit -> claset val claset_ref: unit -> claset ref - val fast_tac : claset -> int -> tactic - val slow_tac : claset -> int -> tactic - val weight_ASTAR : int ref - val astar_tac : claset -> int -> tactic - val slow_astar_tac : claset -> int -> tactic - val best_tac : claset -> int -> tactic - val first_best_tac : claset -> int -> tactic - val slow_best_tac : claset -> int -> tactic - val depth_tac : claset -> int -> int -> tactic - val deepen_tac : claset -> int -> int -> tactic + val fast_tac : claset -> int -> tactic + val slow_tac : claset -> int -> tactic + val weight_ASTAR : int ref + val astar_tac : claset -> int -> tactic + val slow_astar_tac : claset -> int -> tactic + val best_tac : claset -> int -> tactic + val first_best_tac : claset -> int -> tactic + val slow_best_tac : claset -> int -> tactic + val depth_tac : claset -> int -> int -> tactic + val deepen_tac : claset -> int -> int -> tactic - val contr_tac : int -> tactic - val dup_elim : thm -> thm - val dup_intr : thm -> thm - val dup_step_tac : claset -> int -> tactic - val eq_mp_tac : int -> tactic - val haz_step_tac : claset -> int -> tactic - val joinrules : thm list * thm list -> (bool * thm) list - val mp_tac : int -> tactic - val safe_tac : claset -> tactic - val safe_steps_tac : claset -> int -> tactic - val safe_step_tac : claset -> int -> tactic - val clarify_tac : claset -> int -> tactic - val clarify_step_tac : claset -> int -> tactic - val step_tac : claset -> int -> tactic - val slow_step_tac : claset -> int -> tactic - val swap : thm (* ~P ==> (~Q ==> P) ==> Q *) - val swapify : thm list -> thm list - val swap_res_tac : thm list -> int -> tactic - val inst_step_tac : claset -> int -> tactic - val inst0_step_tac : claset -> int -> tactic - val instp_step_tac : claset -> int -> tactic + val contr_tac : int -> tactic + val dup_elim : thm -> thm + val dup_intr : thm -> thm + val dup_step_tac : claset -> int -> tactic + val eq_mp_tac : int -> tactic + val haz_step_tac : claset -> int -> tactic + val joinrules : thm list * thm list -> (bool * thm) list + val mp_tac : int -> tactic + val safe_tac : claset -> tactic + val safe_steps_tac : claset -> int -> tactic + val safe_step_tac : claset -> int -> tactic + val clarify_tac : claset -> int -> tactic + val clarify_step_tac : claset -> int -> tactic + val step_tac : claset -> int -> tactic + val slow_step_tac : claset -> int -> tactic + val swap : thm (* ~P ==> (~Q ==> P) ==> Q *) + val swapify : thm list -> thm list + val swap_res_tac : thm list -> int -> tactic + val inst_step_tac : claset -> int -> tactic + val inst0_step_tac : claset -> int -> tactic + val instp_step_tac : claset -> int -> tactic - val AddDs : thm list -> unit - val AddEs : thm list -> unit - val AddIs : thm list -> unit - val AddSDs : thm list -> unit - val AddSEs : thm list -> unit - val AddSIs : thm list -> unit - val AddXDs : thm list -> unit - val AddXEs : thm list -> unit - val AddXIs : thm list -> unit - val Delrules : thm list -> unit - val Safe_tac : tactic - val Safe_step_tac : int -> tactic - val Clarify_tac : int -> tactic - val Clarify_step_tac : int -> tactic - val Step_tac : int -> tactic - val Fast_tac : int -> tactic - val Best_tac : int -> tactic - val Slow_tac : int -> tactic + val AddDs : thm list -> unit + val AddEs : thm list -> unit + val AddIs : thm list -> unit + val AddSDs : thm list -> unit + val AddSEs : thm list -> unit + val AddSIs : thm list -> unit + val AddXDs : thm list -> unit + val AddXEs : thm list -> unit + val AddXIs : thm list -> unit + val Delrules : thm list -> unit + val Safe_tac : tactic + val Safe_step_tac : int -> tactic + val Clarify_tac : int -> tactic + val Clarify_step_tac : int -> tactic + val Step_tac : int -> tactic + val Fast_tac : int -> tactic + val Best_tac : int -> tactic + val Slow_tac : int -> tactic val Slow_best_tac : int -> tactic - val Deepen_tac : int -> int -> tactic + val Deepen_tac : int -> int -> tactic end; signature CLASSICAL = @@ -152,7 +152,7 @@ val xtra_dest_global: theory attribute val xtra_elim_global: theory attribute val xtra_intro_global: theory attribute - val delrule_global: theory attribute + val rule_del_global: theory attribute val safe_dest_local: Proof.context attribute val safe_elim_local: Proof.context attribute val safe_intro_local: Proof.context attribute @@ -162,7 +162,7 @@ val xtra_dest_local: Proof.context attribute val xtra_elim_local: Proof.context attribute val xtra_intro_local: Proof.context attribute - val delrule_local: Proof.context attribute + val rule_del_local: Proof.context attribute val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list val cla_meth: (claset -> tactic) -> thm list -> Proof.context -> Proof.method val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method @@ -180,7 +180,7 @@ (*** Useful tactics for classical reasoning ***) val imp_elim = (*cannot use bind_thm within a structure!*) - store_thm ("imp_elim", make_elim mp); + store_thm ("imp_elim", Data.make_elim mp); (*Prove goal that assumes both P and ~P. No backtracking if it finds an equal assumption. Perhaps should call @@ -205,8 +205,8 @@ trying rules in order. *) fun swap_res_tac rls = let fun addrl (rl,brls) = (false, rl) :: (true, rl RSN (2,swap)) :: brls - in assume_tac ORELSE' - contr_tac ORELSE' + in assume_tac ORELSE' + contr_tac ORELSE' biresolve_tac (foldr addrl (rls,[])) end; @@ -224,27 +224,27 @@ (**** Classical rule sets ****) datatype claset = - CS of {safeIs : thm list, (*safe introduction rules*) - safeEs : thm list, (*safe elimination rules*) - hazIs : thm list, (*unsafe introduction rules*) - hazEs : thm list, (*unsafe elimination rules*) - xtraIs : thm list, (*extra introduction rules*) - xtraEs : thm list, (*extra elimination rules*) - swrappers : (string * wrapper) list, (*for transf. safe_step_tac*) - uwrappers : (string * wrapper) list, (*for transforming step_tac*) - safe0_netpair : netpair, (*nets for trivial cases*) - safep_netpair : netpair, (*nets for >0 subgoals*) - haz_netpair : netpair, (*nets for unsafe rules*) - dup_netpair : netpair, (*nets for duplication*) - xtra_netpair : netpair}; (*nets for extra rules*) + CS of {safeIs : thm list, (*safe introduction rules*) + safeEs : thm list, (*safe elimination rules*) + hazIs : thm list, (*unsafe introduction rules*) + hazEs : thm list, (*unsafe elimination rules*) + xtraIs : thm list, (*extra introduction rules*) + xtraEs : thm list, (*extra elimination rules*) + swrappers : (string * wrapper) list, (*for transf. safe_step_tac*) + uwrappers : (string * wrapper) list, (*for transforming step_tac*) + safe0_netpair : netpair, (*nets for trivial cases*) + safep_netpair : netpair, (*nets for >0 subgoals*) + haz_netpair : netpair, (*nets for unsafe rules*) + dup_netpair : netpair, (*nets for duplication*) + xtra_netpair : netpair}; (*nets for extra rules*) (*Desired invariants are - safe0_netpair = build safe0_brls, - safep_netpair = build safep_brls, - haz_netpair = build (joinrules(hazIs, hazEs)), - dup_netpair = build (joinrules(map dup_intr hazIs, - map dup_elim hazEs)), - xtra_netpair = build (joinrules(xtraIs, xtraEs))} + safe0_netpair = build safe0_brls, + safep_netpair = build safep_brls, + haz_netpair = build (joinrules(hazIs, hazEs)), + dup_netpair = build (joinrules(map dup_intr hazIs, + map dup_elim hazEs)), + xtra_netpair = build (joinrules(xtraIs, xtraEs))} where build = build_netpair(Net.empty,Net.empty), safe0_brls contains all brules that solve the subgoal, and @@ -256,12 +256,12 @@ val empty_netpair = (Net.empty, Net.empty); val empty_cs = - CS{safeIs = [], - safeEs = [], - hazIs = [], - hazEs = [], - xtraIs = [], - xtraEs = [], + CS{safeIs = [], + safeEs = [], + hazIs = [], + hazEs = [], + xtraIs = [], + xtraEs = [], swrappers = [], uwrappers = [], safe0_netpair = empty_netpair, @@ -327,7 +327,7 @@ is still allowed.*) fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, ...}) = if mem_thm (th, safeIs) then - warning ("Rule already declared as safe introduction (intro!)\n" ^ string_of_thm th) + warning ("Rule already declared as safe introduction (intro!)\n" ^ string_of_thm th) else if mem_thm (th, safeEs) then warning ("Rule already declared as safe elimination (elim!)\n" ^ string_of_thm th) else if mem_thm (th, hazIs) then @@ -343,57 +343,57 @@ (*** Safe rules ***) fun addSI (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, - th) = + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, + th) = if mem_thm (th, safeIs) then - (warning ("Ignoring duplicate safe introduction (intro!)\n" ^ string_of_thm th); - cs) + (warning ("Ignoring duplicate safe introduction (intro!)\n" ^ string_of_thm th); + cs) else let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) partition Thm.no_prems [th] val nI = length safeIs + 1 and nE = length safeEs in warn_dup th cs; - CS{safeIs = th::safeIs, + CS{safeIs = th::safeIs, safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair, - safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair, - safeEs = safeEs, - hazIs = hazIs, - hazEs = hazEs, - xtraIs = xtraIs, - xtraEs = xtraEs, - swrappers = swrappers, - uwrappers = uwrappers, - haz_netpair = haz_netpair, - dup_netpair = dup_netpair, - xtra_netpair = xtra_netpair} + safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair, + safeEs = safeEs, + hazIs = hazIs, + hazEs = hazEs, + xtraIs = xtraIs, + xtraEs = xtraEs, + swrappers = swrappers, + uwrappers = uwrappers, + haz_netpair = haz_netpair, + dup_netpair = dup_netpair, + xtra_netpair = xtra_netpair} end; fun addSE (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, - th) = + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, + th) = if mem_thm (th, safeEs) then - (warning ("Ignoring duplicate safe elimination (elim!)\n" ^ string_of_thm th); - cs) + (warning ("Ignoring duplicate safe elimination (elim!)\n" ^ string_of_thm th); + cs) else let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) partition (fn rl => nprems_of rl=1) [th] val nI = length safeIs and nE = length safeEs + 1 in warn_dup th cs; - CS{safeEs = th::safeEs, + CS{safeEs = th::safeEs, safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair, - safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair, - safeIs = safeIs, - hazIs = hazIs, - hazEs = hazEs, - xtraIs = xtraIs, - xtraEs = xtraEs, - swrappers = swrappers, - uwrappers = uwrappers, - haz_netpair = haz_netpair, - dup_netpair = dup_netpair, - xtra_netpair = xtra_netpair} + safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair, + safeIs = safeIs, + hazIs = hazIs, + hazEs = hazEs, + xtraIs = xtraIs, + xtraEs = xtraEs, + swrappers = swrappers, + uwrappers = uwrappers, + haz_netpair = haz_netpair, + dup_netpair = dup_netpair, + xtra_netpair = xtra_netpair} end; fun rev_foldl f (e, l) = foldl f (e, rev l); @@ -401,117 +401,117 @@ val op addSIs = rev_foldl addSI; val op addSEs = rev_foldl addSE; -fun cs addSDs ths = cs addSEs (map make_elim ths); +fun cs addSDs ths = cs addSEs (map Data.make_elim ths); (*** Hazardous (unsafe) rules ***) fun addI (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, - th)= + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, + th)= if mem_thm (th, hazIs) then - (warning ("Ignoring duplicate introduction (intro)\n" ^ string_of_thm th); - cs) + (warning ("Ignoring duplicate introduction (intro)\n" ^ string_of_thm th); + cs) else let val nI = length hazIs + 1 and nE = length hazEs in warn_dup th cs; - CS{hazIs = th::hazIs, - haz_netpair = insert (nI,nE) ([th], []) haz_netpair, - dup_netpair = insert (nI,nE) (map dup_intr [th], []) dup_netpair, - safeIs = safeIs, - safeEs = safeEs, - hazEs = hazEs, - xtraIs = xtraIs, - xtraEs = xtraEs, - swrappers = swrappers, - uwrappers = uwrappers, - safe0_netpair = safe0_netpair, - safep_netpair = safep_netpair, - xtra_netpair = xtra_netpair} + CS{hazIs = th::hazIs, + haz_netpair = insert (nI,nE) ([th], []) haz_netpair, + dup_netpair = insert (nI,nE) (map dup_intr [th], []) dup_netpair, + safeIs = safeIs, + safeEs = safeEs, + hazEs = hazEs, + xtraIs = xtraIs, + xtraEs = xtraEs, + swrappers = swrappers, + uwrappers = uwrappers, + safe0_netpair = safe0_netpair, + safep_netpair = safep_netpair, + xtra_netpair = xtra_netpair} end; fun addE (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, - th) = + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, + th) = if mem_thm (th, hazEs) then - (warning ("Ignoring duplicate elimination (elim)\n" ^ string_of_thm th); - cs) + (warning ("Ignoring duplicate elimination (elim)\n" ^ string_of_thm th); + cs) else let val nI = length hazIs and nE = length hazEs + 1 in warn_dup th cs; - CS{hazEs = th::hazEs, - haz_netpair = insert (nI,nE) ([], [th]) haz_netpair, - dup_netpair = insert (nI,nE) ([], map dup_elim [th]) dup_netpair, - safeIs = safeIs, - safeEs = safeEs, - hazIs = hazIs, - xtraIs = xtraIs, - xtraEs = xtraEs, - swrappers = swrappers, - uwrappers = uwrappers, - safe0_netpair = safe0_netpair, - safep_netpair = safep_netpair, - xtra_netpair = xtra_netpair} + CS{hazEs = th::hazEs, + haz_netpair = insert (nI,nE) ([], [th]) haz_netpair, + dup_netpair = insert (nI,nE) ([], map dup_elim [th]) dup_netpair, + safeIs = safeIs, + safeEs = safeEs, + hazIs = hazIs, + xtraIs = xtraIs, + xtraEs = xtraEs, + swrappers = swrappers, + uwrappers = uwrappers, + safe0_netpair = safe0_netpair, + safep_netpair = safep_netpair, + xtra_netpair = xtra_netpair} end; val op addIs = rev_foldl addI; val op addEs = rev_foldl addE; -fun cs addDs ths = cs addEs (map make_elim ths); +fun cs addDs ths = cs addEs (map Data.make_elim ths); (*** Extra (single step) rules ***) fun addXI (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, - th)= + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, + th)= if mem_thm (th, xtraIs) then - (warning ("Ignoring duplicate extra introduction (intro?)\n" ^ string_of_thm th); - cs) + (warning ("Ignoring duplicate extra introduction (intro?)\n" ^ string_of_thm th); + cs) else let val nI = length xtraIs + 1 and nE = length xtraEs in warn_dup th cs; - CS{xtraIs = th::xtraIs, - xtra_netpair = insert (nI,nE) ([th], []) xtra_netpair, - safeIs = safeIs, - safeEs = safeEs, - hazIs = hazIs, - hazEs = hazEs, - xtraEs = xtraEs, - swrappers = swrappers, - uwrappers = uwrappers, - safe0_netpair = safe0_netpair, - safep_netpair = safep_netpair, - haz_netpair = haz_netpair, - dup_netpair = dup_netpair} + CS{xtraIs = th::xtraIs, + xtra_netpair = insert (nI,nE) ([th], []) xtra_netpair, + safeIs = safeIs, + safeEs = safeEs, + hazIs = hazIs, + hazEs = hazEs, + xtraEs = xtraEs, + swrappers = swrappers, + uwrappers = uwrappers, + safe0_netpair = safe0_netpair, + safep_netpair = safep_netpair, + haz_netpair = haz_netpair, + dup_netpair = dup_netpair} end; fun addXE (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, - th) = + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}, + th) = if mem_thm (th, xtraEs) then - (warning ("Ignoring duplicate extra elimination (elim?)\n" ^ string_of_thm th); - cs) + (warning ("Ignoring duplicate extra elimination (elim?)\n" ^ string_of_thm th); + cs) else let val nI = length xtraIs and nE = length xtraEs + 1 in warn_dup th cs; - CS{xtraEs = th::xtraEs, - xtra_netpair = insert (nI,nE) ([], [th]) xtra_netpair, - safeIs = safeIs, - safeEs = safeEs, - hazIs = hazIs, - hazEs = hazEs, - xtraIs = xtraIs, - swrappers = swrappers, - uwrappers = uwrappers, - safe0_netpair = safe0_netpair, - safep_netpair = safep_netpair, - haz_netpair = haz_netpair, - dup_netpair = dup_netpair} + CS{xtraEs = th::xtraEs, + xtra_netpair = insert (nI,nE) ([], [th]) xtra_netpair, + safeIs = safeIs, + safeEs = safeEs, + hazIs = hazIs, + hazEs = hazEs, + xtraIs = xtraIs, + swrappers = swrappers, + uwrappers = uwrappers, + safe0_netpair = safe0_netpair, + safep_netpair = safep_netpair, + haz_netpair = haz_netpair, + dup_netpair = dup_netpair} end; infix 4 addXIs addXEs addXDs; @@ -519,144 +519,147 @@ val op addXIs = rev_foldl addXI; val op addXEs = rev_foldl addXE; -fun cs addXDs ths = cs addXEs (map make_elim ths); +fun cs addXDs ths = cs addXEs (map Data.make_elim ths); (*** Deletion of rules Working out what to delete, requires repeating much of the code used - to insert. + to insert. Separate functions delSI, etc., are not exported; instead delrules searches in all the lists and chooses the relevant delXX functions. ***) fun delSI th (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = if mem_thm (th, safeIs) then let val (safe0_rls, safep_rls) = partition Thm.no_prems [th] in CS{safe0_netpair = delete (safe0_rls, []) safe0_netpair, - safep_netpair = delete (safep_rls, []) safep_netpair, - safeIs = rem_thm (safeIs,th), - safeEs = safeEs, - hazIs = hazIs, - hazEs = hazEs, - xtraIs = xtraIs, - xtraEs = xtraEs, - swrappers = swrappers, - uwrappers = uwrappers, - haz_netpair = haz_netpair, - dup_netpair = dup_netpair, - xtra_netpair = xtra_netpair} + safep_netpair = delete (safep_rls, []) safep_netpair, + safeIs = rem_thm (safeIs,th), + safeEs = safeEs, + hazIs = hazIs, + hazEs = hazEs, + xtraIs = xtraIs, + xtraEs = xtraEs, + swrappers = swrappers, + uwrappers = uwrappers, + haz_netpair = haz_netpair, + dup_netpair = dup_netpair, + xtra_netpair = xtra_netpair} end else cs; fun delSE th (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = if mem_thm (th, safeEs) then let val (safe0_rls, safep_rls) = partition (fn rl => nprems_of rl=1) [th] in CS{safe0_netpair = delete ([], safe0_rls) safe0_netpair, - safep_netpair = delete ([], safep_rls) safep_netpair, - safeIs = safeIs, - safeEs = rem_thm (safeEs,th), - hazIs = hazIs, - hazEs = hazEs, - xtraIs = xtraIs, - xtraEs = xtraEs, - swrappers = swrappers, - uwrappers = uwrappers, - haz_netpair = haz_netpair, - dup_netpair = dup_netpair, - xtra_netpair = xtra_netpair} + safep_netpair = delete ([], safep_rls) safep_netpair, + safeIs = safeIs, + safeEs = rem_thm (safeEs,th), + hazIs = hazIs, + hazEs = hazEs, + xtraIs = xtraIs, + xtraEs = xtraEs, + swrappers = swrappers, + uwrappers = uwrappers, + haz_netpair = haz_netpair, + dup_netpair = dup_netpair, + xtra_netpair = xtra_netpair} end else cs; fun delI th (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = if mem_thm (th, hazIs) then CS{haz_netpair = delete ([th], []) haz_netpair, - dup_netpair = delete ([dup_intr th], []) dup_netpair, - safeIs = safeIs, - safeEs = safeEs, - hazIs = rem_thm (hazIs,th), - hazEs = hazEs, - xtraIs = xtraIs, - xtraEs = xtraEs, - swrappers = swrappers, - uwrappers = uwrappers, - safe0_netpair = safe0_netpair, - safep_netpair = safep_netpair, - xtra_netpair = xtra_netpair} + dup_netpair = delete ([dup_intr th], []) dup_netpair, + safeIs = safeIs, + safeEs = safeEs, + hazIs = rem_thm (hazIs,th), + hazEs = hazEs, + xtraIs = xtraIs, + xtraEs = xtraEs, + swrappers = swrappers, + uwrappers = uwrappers, + safe0_netpair = safe0_netpair, + safep_netpair = safep_netpair, + xtra_netpair = xtra_netpair} else cs; fun delE th - (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = + (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = if mem_thm (th, hazEs) then CS{haz_netpair = delete ([], [th]) haz_netpair, - dup_netpair = delete ([], [dup_elim th]) dup_netpair, - safeIs = safeIs, - safeEs = safeEs, - hazIs = hazIs, - hazEs = rem_thm (hazEs,th), - xtraIs = xtraIs, - xtraEs = xtraEs, - swrappers = swrappers, - uwrappers = uwrappers, - safe0_netpair = safe0_netpair, - safep_netpair = safep_netpair, - xtra_netpair = xtra_netpair} + dup_netpair = delete ([], [dup_elim th]) dup_netpair, + safeIs = safeIs, + safeEs = safeEs, + hazIs = hazIs, + hazEs = rem_thm (hazEs,th), + xtraIs = xtraIs, + xtraEs = xtraEs, + swrappers = swrappers, + uwrappers = uwrappers, + safe0_netpair = safe0_netpair, + safep_netpair = safep_netpair, + xtra_netpair = xtra_netpair} else cs; fun delXI th (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = if mem_thm (th, xtraIs) then CS{xtra_netpair = delete ([th], []) xtra_netpair, - safeIs = safeIs, - safeEs = safeEs, - hazIs = hazIs, - hazEs = hazEs, - xtraIs = rem_thm (xtraIs,th), - xtraEs = xtraEs, - swrappers = swrappers, - uwrappers = uwrappers, - safe0_netpair = safe0_netpair, - safep_netpair = safep_netpair, - haz_netpair = haz_netpair, - dup_netpair = dup_netpair} + safeIs = safeIs, + safeEs = safeEs, + hazIs = hazIs, + hazEs = hazEs, + xtraIs = rem_thm (xtraIs,th), + xtraEs = xtraEs, + swrappers = swrappers, + uwrappers = uwrappers, + safe0_netpair = safe0_netpair, + safep_netpair = safep_netpair, + haz_netpair = haz_netpair, + dup_netpair = dup_netpair} else cs; fun delXE th - (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = + (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers, + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = if mem_thm (th, xtraEs) then CS{xtra_netpair = delete ([], [th]) xtra_netpair, - safeIs = safeIs, - safeEs = safeEs, - hazIs = hazIs, - hazEs = hazEs, - xtraIs = xtraIs, - xtraEs = rem_thm (xtraEs,th), - swrappers = swrappers, - uwrappers = uwrappers, - safe0_netpair = safe0_netpair, - safep_netpair = safep_netpair, - haz_netpair = haz_netpair, - dup_netpair = dup_netpair} + safeIs = safeIs, + safeEs = safeEs, + hazIs = hazIs, + hazEs = hazEs, + xtraIs = xtraIs, + xtraEs = rem_thm (xtraEs,th), + swrappers = swrappers, + uwrappers = uwrappers, + safe0_netpair = safe0_netpair, + safep_netpair = safep_netpair, + haz_netpair = haz_netpair, + dup_netpair = dup_netpair} else cs; (*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*) fun delrule (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, ...}, th) = - if mem_thm (th, safeIs) orelse mem_thm (th, safeEs) orelse - mem_thm (th, hazIs) orelse mem_thm (th, hazEs) orelse - mem_thm (th, xtraIs) orelse mem_thm (th, xtraEs) - then delSI th (delSE th (delI th (delE th (delXI th (delXE th cs))))) - else (warning ("Undeclared classical rule\n" ^ (string_of_thm th)); - cs); + let val th' = Data.make_elim th in + if mem_thm (th, safeIs) orelse mem_thm (th, safeEs) orelse + mem_thm (th, hazIs) orelse mem_thm (th, hazEs) orelse + mem_thm (th, xtraIs) orelse mem_thm (th, xtraEs) orelse + mem_thm (th', safeEs) orelse mem_thm (th', hazEs) orelse mem_thm (th', xtraEs) + then delSI th (delSE th (delI th (delE th (delXI th (delXE th + (delSE th' (delE th' (delXE th' cs)))))))) + else (warning ("Undeclared classical rule\n" ^ (string_of_thm th)); cs) + end; val op delrules = foldl delrule; @@ -689,13 +692,13 @@ (*Add/replace an unsafe wrapper*) fun cs addWrapper new_uwrapper = update_uwrappers cs (fn uwrappers => overwrite_warn (uwrappers, new_uwrapper) - ("Overwriting unsafe wrapper "^fst new_uwrapper)); + ("Overwriting unsafe wrapper "^fst new_uwrapper)); (*Remove a safe wrapper*) fun cs delSWrapper name = update_swrappers cs (fn swrappers => let val (del,rest) = partition (fn (n,_) => n=name) swrappers in if null del then (warning ("No such safe wrapper in claset: "^ name); - swrappers) else rest end); + swrappers) else rest end); (*Remove an unsafe wrapper*) fun cs delWrapper name = update_uwrappers cs (fn uwrappers => @@ -730,7 +733,7 @@ fun merge_cs (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, ...}, CS{safeIs=safeIs2, safeEs=safeEs2, hazIs=hazIs2, hazEs=hazEs2, - xtraIs=xtraIs2, xtraEs=xtraEs2, swrappers, uwrappers, ...}) = + xtraIs=xtraIs2, xtraEs=xtraEs2, swrappers, uwrappers, ...}) = let val safeIs' = gen_rems eq_thm (safeIs2,safeIs) val safeEs' = gen_rems eq_thm (safeEs2,safeEs) val hazIs' = gen_rems eq_thm ( hazIs2, hazIs) @@ -738,11 +741,11 @@ val xtraIs' = gen_rems eq_thm (xtraIs2, xtraIs) val xtraEs' = gen_rems eq_thm (xtraEs2, xtraEs) val cs1 = cs addSIs safeIs' - addSEs safeEs' - addIs hazIs' - addEs hazEs' - addXIs xtraIs' - addXEs xtraEs' + addSEs safeEs' + addIs hazIs' + addEs hazEs' + addXIs xtraIs' + addXEs xtraEs' val cs2 = update_swrappers cs1 (fn ws => merge_alists ws swrappers); val cs3 = update_uwrappers cs2 (fn ws => merge_alists ws uwrappers); in cs3 @@ -754,15 +757,15 @@ (*Attack subgoals using safe inferences -- matching, not resolution*) fun safe_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = appSWrappers cs (FIRST' [ - eq_assume_tac, - eq_mp_tac, - bimatch_from_nets_tac safe0_netpair, - FIRST' hyp_subst_tacs, - bimatch_from_nets_tac safep_netpair]); + eq_assume_tac, + eq_mp_tac, + bimatch_from_nets_tac safe0_netpair, + FIRST' hyp_subst_tacs, + bimatch_from_nets_tac safep_netpair]); (*Repeatedly attack a subgoal using safe inferences -- it's deterministic!*) fun safe_steps_tac cs = REPEAT_DETERM1 o - (fn i => COND (has_fewer_prems i) no_tac (safe_step_tac cs i)); + (fn i => COND (has_fewer_prems i) no_tac (safe_step_tac cs i)); (*Repeatedly attack subgoals using safe inferences -- it's deterministic!*) fun safe_tac cs = REPEAT_DETERM1 (FIRSTGOAL (safe_steps_tac cs)); @@ -788,10 +791,10 @@ (*Attack subgoals using safe inferences -- matching, not resolution*) fun clarify_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = appSWrappers cs (FIRST' [ - eq_assume_contr_tac, - bimatch_from_nets_tac safe0_netpair, - FIRST' hyp_subst_tacs, - n_bimatch_from_nets_tac 1 safep_netpair, + eq_assume_contr_tac, + bimatch_from_nets_tac safe0_netpair, + FIRST' hyp_subst_tacs, + n_bimatch_from_nets_tac 1 safep_netpair, bimatch2_tac safep_netpair]); fun clarify_tac cs = SELECT_GOAL (REPEAT_DETERM (clarify_step_tac cs 1)); @@ -802,8 +805,8 @@ (*Backtracking is allowed among the various these unsafe ways of proving a subgoal. *) fun inst0_step_tac (CS{safe0_netpair,safep_netpair,...}) = - assume_tac APPEND' - contr_tac APPEND' + assume_tac APPEND' + contr_tac APPEND' biresolve_from_nets_tac safe0_netpair; (*These unsafe steps could generate more subgoals.*) @@ -818,12 +821,12 @@ (*Single step for the prover. FAILS unless it makes progress. *) fun step_tac cs i = safe_tac cs ORELSE appWrappers cs - (inst_step_tac cs ORELSE' haz_step_tac cs) i; + (inst_step_tac cs ORELSE' haz_step_tac cs) i; (*Using a "safe" rule to instantiate variables is unsafe. This tactic allows backtracking from "safe" rules to "unsafe" rules here.*) fun slow_step_tac cs i = safe_tac cs ORELSE appWrappers cs - (inst_step_tac cs APPEND' haz_step_tac cs) i; + (inst_step_tac cs APPEND' haz_step_tac cs) i; (**** The following tactics all fail unless they solve one goal ****) @@ -849,13 +852,13 @@ fun astar_tac cs = SELECT_GOAL ( ASTAR (has_fewer_prems 1 - , fn level =>(fn thm =>size_of_thm thm + !weight_ASTAR *level)) - (step_tac cs 1)); + , fn level =>(fn thm =>size_of_thm thm + !weight_ASTAR *level)) + (step_tac cs 1)); fun slow_astar_tac cs = SELECT_GOAL ( ASTAR (has_fewer_prems 1 - , fn level =>(fn thm =>size_of_thm thm + !weight_ASTAR *level)) - (slow_step_tac cs 1)); + , fn level =>(fn thm =>size_of_thm thm + !weight_ASTAR *level)) + (slow_step_tac cs 1)); (**** Complete tactic, loosely based upon LeanTaP. This tactic is the outcome of much experimentation! Changing APPEND to ORELSE below would prove @@ -871,12 +874,12 @@ (*Searching to depth m. A variant called nodup_depth_tac appears in clasimp.ML*) local fun slow_step_tac' cs = appWrappers cs - (instp_step_tac cs APPEND' dup_step_tac cs); + (instp_step_tac cs APPEND' dup_step_tac cs); in fun depth_tac cs m i state = SELECT_GOAL (safe_steps_tac cs 1 THEN_ELSE - (DEPTH_SOLVE (depth_tac cs m 1), - inst0_step_tac cs 1 APPEND COND (K (m=0)) no_tac - (slow_step_tac' cs 1 THEN DEPTH_SOLVE (depth_tac cs (m-1) 1)) + (DEPTH_SOLVE (depth_tac cs m 1), + inst0_step_tac cs 1 APPEND COND (K (m=0)) no_tac + (slow_step_tac' cs 1 THEN DEPTH_SOLVE (depth_tac cs (m-1) 1)) )) i state; end; @@ -886,12 +889,12 @@ SUBGOAL (fn (prem,i) => let val deti = - (*No Vars in the goal? No need to backtrack between goals.*) - case term_vars prem of - [] => DETERM - | _::_ => I + (*No Vars in the goal? No need to backtrack between goals.*) + case term_vars prem of + [] => DETERM + | _::_ => I in SELECT_GOAL (TRY (safe_tac cs) THEN - DEPTH_SOLVE (deti (depth_tac cs m 1))) i + DEPTH_SOLVE (deti (depth_tac cs m 1))) i end); fun deepen_tac cs = DEEPEN (2,10) (safe_depth_tac cs); @@ -983,7 +986,7 @@ val xtra_dest_global = change_global_cs (op addXDs); val xtra_elim_global = change_global_cs (op addXEs); val xtra_intro_global = change_global_cs (op addXIs); -val delrule_global = change_global_cs (op delrules); +val rule_del_global = change_global_cs (op delrules); val safe_dest_local = change_local_cs (op addSDs); val safe_elim_local = change_local_cs (op addSEs); @@ -994,22 +997,22 @@ val xtra_dest_local = change_local_cs (op addXDs); val xtra_elim_local = change_local_cs (op addXEs); val xtra_intro_local = change_local_cs (op addXIs); -val delrule_local = change_local_cs (op delrules); +val rule_del_local = change_local_cs (op delrules); (* tactics referring to the implicit claset *) (*the abstraction over the proof state delays the dereferencing*) -fun Safe_tac st = safe_tac (claset()) st; -fun Safe_step_tac i st = safe_step_tac (claset()) i st; +fun Safe_tac st = safe_tac (claset()) st; +fun Safe_step_tac i st = safe_step_tac (claset()) i st; fun Clarify_step_tac i st = clarify_step_tac (claset()) i st; -fun Clarify_tac i st = clarify_tac (claset()) i st; -fun Step_tac i st = step_tac (claset()) i st; -fun Fast_tac i st = fast_tac (claset()) i st; -fun Best_tac i st = best_tac (claset()) i st; -fun Slow_tac i st = slow_tac (claset()) i st; -fun Slow_best_tac i st = slow_best_tac (claset()) i st; -fun Deepen_tac m = deepen_tac (claset()) m; +fun Clarify_tac i st = clarify_tac (claset()) i st; +fun Step_tac i st = step_tac (claset()) i st; +fun Fast_tac i st = fast_tac (claset()) i st; +fun Best_tac i st = best_tac (claset()) i st; +fun Slow_tac i st = slow_tac (claset()) i st; +fun Slow_best_tac i st = slow_best_tac (claset()) i st; +fun Deepen_tac m = deepen_tac (claset()) m; end; @@ -1023,8 +1026,8 @@ val introN = "intro"; val elimN = "elim"; val destN = "dest"; +val ruleN = "rule"; val delN = "del"; -val delruleN = "delrule"; val colon = Args.$$$ ":"; val query = Args.$$$ "?"; @@ -1036,19 +1039,21 @@ (Scan.lift ((query >> K xtra || bang >> K safe || Scan.succeed haz) >> change)); fun cla_attr f g h = (cla_att change_global_cs f g h, cla_att change_local_cs f g h); -val del_attr = (Attrib.no_args delrule_global, Attrib.no_args delrule_local); + +fun del_args att = Attrib.syntax (Scan.lift (Args.$$$ delN) >> K att); +val rule_del_attr = (del_args rule_del_global, del_args rule_del_local); (* setup_attrs *) -fun elimified x = Attrib.no_args (Drule.rule_attribute (K make_elim)) x; +fun elimified x = Attrib.no_args (Drule.rule_attribute (K Data.make_elim)) x; val setup_attrs = Attrib.add_attributes [("elimified", (elimified, elimified), "destruct rule turned into elimination rule (classical)"), (destN, cla_attr (op addXDs) (op addDs) (op addSDs), "declaration of destruction rule"), (elimN, cla_attr (op addXEs) (op addEs) (op addSEs), "declaration of elimination rule"), (introN, cla_attr (op addXIs) (op addIs) (op addSIs), "declaration of introduction rule"), - (delruleN, del_attr, "remove declaration of elim/intro rule")]; + (ruleN, rule_del_attr, "remove declaration of intro/elim/dest rule")]; @@ -1153,7 +1158,7 @@ Args.$$$ introN -- query_colon >> K (I, xtra_intro_local), Args.$$$ introN -- bang_colon >> K (I, safe_intro_local), Args.$$$ introN -- colon >> K (I, haz_intro_local), - Args.$$$ delN -- colon >> K (I, delrule_local)]; + Args.$$$ delN -- colon >> K (I, rule_del_local)]; fun cla_meth tac prems ctxt = Method.METHOD (fn facts => ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_claset ctxt)); diff -r 431c96ac997e -r cb6a7572d0a1 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Tue Sep 12 17:35:09 2000 +0200 +++ b/src/Pure/Isar/method.ML Tue Sep 12 17:38:49 2000 +0200 @@ -20,11 +20,11 @@ val dest_global: theory attribute val elim_global: theory attribute val intro_global: theory attribute - val delrule_global: theory attribute + val rule_del_global: theory attribute val dest_local: Proof.context attribute val elim_local: Proof.context attribute val intro_local: Proof.context attribute - val delrule_local: Proof.context attribute + val rule_del_local: Proof.context attribute val METHOD: (thm list -> tactic) -> Proof.method val METHOD_CASES: (thm list -> thm -> (thm * (string * RuleCases.T) list) Seq.seq) -> Proof.method @@ -175,27 +175,31 @@ local -fun add_rule thm rules = Library.gen_ins Thm.eq_thm (thm, rules); -fun del_rule thm rules = Library.gen_rem Thm.eq_thm (rules, thm); +fun add_dest th (intro, elim) = (intro, Drule.add_rules [Tactic.make_elim th] elim); +fun add_elim th (intro, elim) = (intro, Drule.add_rules [th] elim); +fun add_intro th (intro, elim) = (Drule.add_rules [th] intro, elim); -fun add_dest thm (intro, elim) = (intro, add_rule (Tactic.make_elim thm) elim); -fun add_elim thm (intro, elim) = (intro, add_rule thm elim); -fun add_intro thm (intro, elim) = (add_rule thm intro, elim); -fun delrule thm (intro, elim) = (del_rule thm intro, del_rule thm elim); +fun del_rule th (intro, elim) = + let + val th' = Tactic.make_elim th; + val del = Drule.del_rules [th'] o Drule.del_rules [th]; + in (del intro, del elim) end; -fun mk_att f g (x, thm) = (f (g thm) x, thm); +fun mk_att f g (x, th) = (f (g th) x, th); in val dest_global = mk_att GlobalRules.map add_dest; val elim_global = mk_att GlobalRules.map add_elim; val intro_global = mk_att GlobalRules.map add_intro; -val delrule_global = mk_att GlobalRules.map delrule; +val rule_del_global = mk_att GlobalRules.map del_rule; val dest_local = mk_att LocalRules.map add_dest; val elim_local = mk_att LocalRules.map add_elim; val intro_local = mk_att LocalRules.map add_intro; -val delrule_local = mk_att LocalRules.map delrule; +val rule_del_local = mk_att LocalRules.map del_rule; + +fun del_args att = Attrib.syntax (Scan.lift (Args.$$$ "del") >> K att); end; @@ -209,7 +213,7 @@ "declaration of elimination rule"), ("intro", (Attrib.no_args intro_global, Attrib.no_args intro_local), "declaration of introduction rule"), - ("delrule", (Attrib.no_args delrule_global, Attrib.no_args delrule_local), + ("rule", (del_args rule_del_global, del_args rule_del_local), "remove declaration of elim/intro rule")];