# HG changeset patch # User wenzelm # Date 1305294474 -7200 # Node ID e07e56300faaf5988017c73182ee3d338dfaf846 # Parent 3a84b69479325fcb3983fb0cc7a964df6d5efbe1 misc tuning and simplification; diff -r 3a84b6947932 -r e07e56300faa src/Provers/classical.ML --- a/src/Provers/classical.ML Fri May 13 14:39:55 2011 +0200 +++ b/src/Provers/classical.ML Fri May 13 15:47:54 2011 +0200 @@ -25,11 +25,11 @@ signature CLASSICAL_DATA = sig - val imp_elim : thm (* P --> Q ==> (~ R ==> P) ==> (Q ==> R) ==> R *) - val not_elim : thm (* ~P ==> P ==> R *) - val swap : thm (* ~ P ==> (~ R ==> P) ==> R *) - val classical : thm (* (~ P ==> P) ==> P *) - val sizef : thm -> int (* size function for BEST_FIRST *) + val imp_elim: thm (* P --> Q ==> (~ R ==> P) ==> (Q ==> R) ==> R *) + val not_elim: thm (* ~P ==> P ==> R *) + val swap: thm (* ~ P ==> (~ R ==> 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; @@ -38,71 +38,75 @@ type claset val empty_cs: claset val print_cs: Proof.context -> claset -> unit - val rep_cs: - claset -> {safeIs: thm list, safeEs: thm list, - hazIs: thm list, hazEs: thm list, - swrappers: (string * wrapper) list, - uwrappers: (string * wrapper) list, - safe0_netpair: netpair, safep_netpair: netpair, - haz_netpair: netpair, dup_netpair: netpair, - xtra_netpair: Context_Rules.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 addSafter : claset * (string * (int -> tactic)) -> claset - val addbefore : claset * (string * (int -> tactic)) -> claset - val addafter : 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 rep_cs: claset -> + {safeIs: thm list, + safeEs: thm list, + hazIs: thm list, + hazEs: thm list, + swrappers: (string * wrapper) list, + uwrappers: (string * wrapper) list, + safe0_netpair: netpair, + safep_netpair: netpair, + haz_netpair: netpair, + dup_netpair: netpair, + xtra_netpair: Context_Rules.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 addSafter: claset * (string * (int -> tactic)) -> claset + val addbefore: claset * (string * (int -> tactic)) -> claset + val addafter: 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 global_claset_of : theory -> claset - val claset_of : Proof.context -> claset + val global_claset_of: theory -> claset + val claset_of: Proof.context -> claset - val fast_tac : claset -> int -> tactic - val slow_tac : claset -> int -> tactic - val weight_ASTAR : int Unsynchronized.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 Unsynchronized.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 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 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 end; signature CLASSICAL = @@ -313,151 +317,131 @@ val mem_thm = member Thm.eq_thm_prop and rem_thm = remove Thm.eq_thm_prop; -(*Warn if the rule is already present ELSEWHERE in the claset. The addition - is still allowed.*) -fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, ...}) = - if mem_thm safeIs th then - warning ("Rule already declared as safe introduction (intro!)\n" ^ - Display.string_of_thm_without_context th) - else if mem_thm safeEs th then - warning ("Rule already declared as safe elimination (elim!)\n" ^ - Display.string_of_thm_without_context th) - else if mem_thm hazIs th then - warning ("Rule already declared as introduction (intro)\n" ^ - Display.string_of_thm_without_context th) - else if mem_thm hazEs th then - warning ("Rule already declared as elimination (elim)\n" ^ - Display.string_of_thm_without_context th) - else (); +fun warn msg rules th = + mem_thm rules th andalso (warning (msg ^ Display.string_of_thm_without_context th); true); + +fun warn_other th (CS{safeIs, safeEs, hazIs, hazEs, ...}) = + warn "Rule already declared as safe introduction (intro!)\n" safeIs th orelse + warn "Rule already declared as safe elimination (elim!)\n" safeEs th orelse + warn "Rule already declared as introduction (intro)\n" hazIs th orelse + warn "Rule already declared as elimination (elim)\n" hazEs th; (*** Safe rules ***) fun addSI w th - (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = - if mem_thm safeIs th then - (warning ("Ignoring duplicate safe introduction (intro!)\n" ^ - Display.string_of_thm_without_context th); cs) + (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = + if warn "Ignoring duplicate safe introduction (intro!)\n" safeIs th then cs else - let val th' = flat_rule th + let + val th' = flat_rule th; val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) - List.partition Thm.no_prems [th'] - val nI = length safeIs + 1 - and nE = length safeEs - in warn_dup th cs; - CS{safeIs = th::safeIs, + List.partition Thm.no_prems [th']; + val nI = length safeIs + 1; + val nE = length safeEs; + val _ = warn_other th cs; + in + 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, - swrappers = swrappers, - uwrappers = uwrappers, - haz_netpair = haz_netpair, - dup_netpair = dup_netpair, + safeEs = safeEs, + hazIs = hazIs, + hazEs = hazEs, + swrappers = swrappers, + uwrappers = uwrappers, + haz_netpair = haz_netpair, + dup_netpair = dup_netpair, xtra_netpair = insert' (the_default 0 w) (nI,nE) ([th], []) xtra_netpair} - end; + end; fun addSE w th - (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = - if mem_thm safeEs th then - (warning ("Ignoring duplicate safe elimination (elim!)\n" ^ - Display.string_of_thm_without_context th); cs) + (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = + if warn "Ignoring duplicate safe elimination (elim!)\n" safeEs th then cs else if has_fewer_prems 1 th then - error ("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th) + error ("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th) else - let - val th' = classical_rule (flat_rule th) + let + val th' = classical_rule (flat_rule th); val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*) - List.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, + List.partition (fn rl => nprems_of rl=1) [th']; + val nI = length safeIs; + val nE = length safeEs + 1; + val _ = warn_other th cs; + in + 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, - swrappers = swrappers, - uwrappers = uwrappers, - haz_netpair = haz_netpair, - dup_netpair = dup_netpair, + safeIs = safeIs, + hazIs = hazIs, + hazEs = hazEs, + swrappers = swrappers, + uwrappers = uwrappers, + haz_netpair = haz_netpair, + dup_netpair = dup_netpair, xtra_netpair = insert' (the_default 0 w) (nI,nE) ([], [th]) xtra_netpair} - end; - -fun cs addSIs ths = fold_rev (addSI NONE) ths cs; -fun cs addSEs ths = fold_rev (addSE NONE) ths cs; - -fun make_elim th = - if has_fewer_prems 1 th then - error ("Ill-formed destruction rule\n" ^ Display.string_of_thm_without_context th) - else Tactic.make_elim th; - -fun cs addSDs ths = cs addSEs (map make_elim ths); + end; (*** Hazardous (unsafe) rules ***) fun addI w th - (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = - if mem_thm hazIs th then - (warning ("Ignoring duplicate introduction (intro)\n" ^ - Display.string_of_thm_without_context th); cs) + (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = + if warn "Ignoring duplicate introduction (intro)\n" hazIs th then cs else - let val th' = flat_rule th - 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, - swrappers = swrappers, - uwrappers = uwrappers, + let + val th' = flat_rule th; + val nI = length hazIs + 1; + val nE = length hazEs; + val _ = warn_other th cs; + in + CS + {hazIs = th :: hazIs, + haz_netpair = insert (nI, nE) ([th'], []) haz_netpair, + dup_netpair = insert (nI, nE) ([dup_intr th'], []) dup_netpair, + safeIs = safeIs, + safeEs = safeEs, + hazEs = hazEs, + swrappers = swrappers, + uwrappers = uwrappers, safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, - xtra_netpair = insert' (the_default 1 w) (nI,nE) ([th], []) xtra_netpair} - end - handle THM("RSN: no unifiers",_,_) => (*from dup_intr*) - error ("Ill-formed introduction rule\n" ^ Display.string_of_thm_without_context th); + xtra_netpair = insert' (the_default 1 w) (nI, nE) ([th], []) xtra_netpair} + end + handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*) (* FIXME !? *) + error ("Ill-formed introduction rule\n" ^ Display.string_of_thm_without_context th); fun addE w th - (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = - if mem_thm hazEs th then - (warning ("Ignoring duplicate elimination (elim)\n" ^ - Display.string_of_thm_without_context th); cs) + (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = + if warn "Ignoring duplicate elimination (elim)\n" hazEs th then cs else if has_fewer_prems 1 th then - error("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th) + error ("Ill-formed elimination rule\n" ^ Display.string_of_thm_without_context th) else - let - val th' = classical_rule (flat_rule th) - 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, - swrappers = swrappers, - uwrappers = uwrappers, + let + val th' = classical_rule (flat_rule th); + val nI = length hazIs; + val nE = length hazEs + 1; + val _ = warn_other th cs; + in + CS + {hazEs = th :: hazEs, + haz_netpair = insert (nI, nE) ([], [th']) haz_netpair, + dup_netpair = insert (nI, nE) ([], [dup_elim th']) dup_netpair, + safeIs = safeIs, + safeEs = safeEs, + hazIs = hazIs, + swrappers = swrappers, + uwrappers = uwrappers, safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, - xtra_netpair = insert' (the_default 1 w) (nI,nE) ([], [th]) xtra_netpair} - end; + xtra_netpair = insert' (the_default 1 w) (nI, nE) ([], [th]) xtra_netpair} + end; -fun cs addIs ths = fold_rev (addI NONE) ths cs; -fun cs addEs ths = fold_rev (addE NONE) ths cs; - -fun cs addDs ths = cs addEs (map make_elim ths); (*** Deletion of rules @@ -466,91 +450,96 @@ ***) fun delSI th - (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = - if mem_thm safeIs th then - let val th' = flat_rule th - val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th'] - in CS{safe0_netpair = delete (safe0_rls, []) safe0_netpair, - safep_netpair = delete (safep_rls, []) safep_netpair, - safeIs = rem_thm th safeIs, - safeEs = safeEs, - hazIs = hazIs, - hazEs = hazEs, - swrappers = swrappers, - uwrappers = uwrappers, - haz_netpair = haz_netpair, - dup_netpair = dup_netpair, - xtra_netpair = delete' ([th], []) xtra_netpair} - end - else cs; - -fun delSE th - (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = - if mem_thm safeEs th then + (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = + if mem_thm safeIs th then let - val th' = classical_rule (flat_rule th) - val (safe0_rls, safep_rls) = List.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 th safeEs, - hazIs = hazIs, - hazEs = hazEs, - swrappers = swrappers, - uwrappers = uwrappers, - haz_netpair = haz_netpair, - dup_netpair = dup_netpair, - xtra_netpair = delete' ([], [th]) xtra_netpair} + val th' = flat_rule th; + val (safe0_rls, safep_rls) = List.partition Thm.no_prems [th']; + in + CS + {safe0_netpair = delete (safe0_rls, []) safe0_netpair, + safep_netpair = delete (safep_rls, []) safep_netpair, + safeIs = rem_thm th safeIs, + safeEs = safeEs, + hazIs = hazIs, + hazEs = hazEs, + swrappers = swrappers, + uwrappers = uwrappers, + haz_netpair = haz_netpair, + dup_netpair = dup_netpair, + xtra_netpair = delete' ([th], []) xtra_netpair} end else cs; +fun delSE th + (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = + if mem_thm safeEs th then + let + val th' = classical_rule (flat_rule th); + val (safe0_rls, safep_rls) = List.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 th safeEs, + hazIs = hazIs, + hazEs = hazEs, + swrappers = swrappers, + uwrappers = uwrappers, + haz_netpair = haz_netpair, + dup_netpair = dup_netpair, + xtra_netpair = delete' ([], [th]) xtra_netpair} + end + else cs; fun delI th - (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = - if mem_thm hazIs th then - let val th' = flat_rule th - in CS{haz_netpair = delete ([th'], []) haz_netpair, + (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = + if mem_thm hazIs th then + let val th' = flat_rule th in + CS + {haz_netpair = delete ([th'], []) haz_netpair, dup_netpair = delete ([dup_intr th'], []) dup_netpair, - safeIs = safeIs, - safeEs = safeEs, - hazIs = rem_thm th hazIs, - hazEs = hazEs, - swrappers = swrappers, - uwrappers = uwrappers, + safeIs = safeIs, + safeEs = safeEs, + hazIs = rem_thm th hazIs, + hazEs = hazEs, + swrappers = swrappers, + uwrappers = uwrappers, safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, xtra_netpair = delete' ([th], []) xtra_netpair} end - else cs - handle THM("RSN: no unifiers",_,_) => (*from dup_intr*) - error ("Ill-formed introduction rule\n" ^ Display.string_of_thm_without_context th); - + else cs + handle THM ("RSN: no unifiers", _, _) => (*from dup_intr*) (* FIXME !? *) + error ("Ill-formed introduction rule\n" ^ Display.string_of_thm_without_context th); fun delE th - (cs as CS{safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = - if mem_thm hazEs th then - let val th' = classical_rule (flat_rule th) - in CS{haz_netpair = delete ([], [th']) haz_netpair, + (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, + safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) = + if mem_thm hazEs th then + let val th' = classical_rule (flat_rule th) in + CS + {haz_netpair = delete ([], [th']) haz_netpair, dup_netpair = delete ([], [dup_elim th']) dup_netpair, - safeIs = safeIs, - safeEs = safeEs, - hazIs = hazIs, - hazEs = rem_thm th hazEs, - swrappers = swrappers, - uwrappers = uwrappers, + safeIs = safeIs, + safeEs = safeEs, + hazIs = hazIs, + hazEs = rem_thm th hazEs, + swrappers = swrappers, + uwrappers = uwrappers, safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, xtra_netpair = delete' ([], [th]) xtra_netpair} - end - else cs; + end + else cs; (*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*) fun delrule th (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}) = - let val th' = Tactic.make_elim th in + let val th' = Tactic.make_elim th (* FIXME classical make_elim!? *) in if mem_thm safeIs th orelse mem_thm safeEs th orelse mem_thm hazIs th orelse mem_thm hazEs th orelse mem_thm safeEs th' orelse mem_thm hazEs th' @@ -561,6 +550,19 @@ fun cs delrules ths = fold delrule ths cs; +fun make_elim th = + if has_fewer_prems 1 th then + error ("Ill-formed destruction rule\n" ^ Display.string_of_thm_without_context th) + else Tactic.make_elim th; + +fun cs addSIs ths = fold_rev (addSI NONE) ths cs; +fun cs addSEs ths = fold_rev (addSE NONE) ths cs; +fun cs addSDs ths = cs addSEs (map make_elim ths); +fun cs addIs ths = fold_rev (addI NONE) ths cs; +fun cs addEs ths = fold_rev (addE NONE) ths cs; +fun cs addDs ths = cs addEs (map make_elim ths); + + (*** Modifying the wrapper tacticals ***) fun map_swrappers f (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, @@ -579,12 +581,11 @@ haz_netpair = haz_netpair, dup_netpair = dup_netpair, xtra_netpair = xtra_netpair}; fun update_warn msg (p as (key : string, _)) xs = - (if AList.defined (op =) xs key then warning msg else (); - AList.update (op =) p xs); + (if AList.defined (op =) xs key then warning msg else (); AList.update (op =) p xs); fun delete_warn msg (key : string) xs = if AList.defined (op =) xs key then AList.delete (op =) key xs - else (warning msg; xs); + else (warning msg; xs); (*Add/replace a safe wrapper*) fun cs addSWrapper new_swrapper = map_swrappers @@ -603,25 +604,17 @@ (delete_warn ("No such unsafe wrapper in claset: " ^ name) name) cs; (* compose a safe tactic alternatively before/after safe_step_tac *) -fun cs addSbefore (name, tac1) = - cs addSWrapper (name, fn tac2 => tac1 ORELSE' tac2); -fun cs addSafter (name, tac2) = - cs addSWrapper (name, fn tac1 => tac1 ORELSE' tac2); +fun cs addSbefore (name, tac1) = cs addSWrapper (name, fn tac2 => tac1 ORELSE' tac2); +fun cs addSafter (name, tac2) = cs addSWrapper (name, fn tac1 => tac1 ORELSE' tac2); (*compose a tactic alternatively before/after the step tactic *) -fun cs addbefore (name, tac1) = - cs addWrapper (name, fn tac2 => tac1 APPEND' tac2); -fun cs addafter (name, tac2) = - cs addWrapper (name, fn tac1 => tac1 APPEND' tac2); +fun cs addbefore (name, tac1) = cs addWrapper (name, fn tac2 => tac1 APPEND' tac2); +fun cs addafter (name, tac2) = cs addWrapper (name, fn tac1 => tac1 APPEND' tac2); -fun cs addD2 (name, thm) = - cs addafter (name, datac thm 1); -fun cs addE2 (name, thm) = - cs addafter (name, eatac thm 1); -fun cs addSD2 (name, thm) = - cs addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac); -fun cs addSE2 (name, thm) = - cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac); +fun cs addD2 (name, thm) = cs addafter (name, datac thm 1); +fun cs addE2 (name, thm) = cs addafter (name, eatac thm 1); +fun cs addSD2 (name, thm) = cs addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac); +fun cs addSE2 (name, thm) = cs addSafter (name, ematch_tac [thm] THEN' eq_assume_tac); (*Merge works by adding all new rules of the 2nd claset into the 1st claset. Merging the term nets may look more efficient, but the rather delicate @@ -636,21 +629,16 @@ val safeEs' = fold rem_thm safeEs safeEs2; val hazIs' = fold rem_thm hazIs hazIs2; val hazEs' = fold rem_thm hazEs hazEs2; - val cs1 = cs addSIs safeIs' - addSEs safeEs' - addIs hazIs' - addEs hazEs'; - val cs2 = map_swrappers - (fn ws => AList.merge (op =) (K true) (ws, swrappers)) cs1; - val cs3 = map_uwrappers - (fn ws => AList.merge (op =) (K true) (ws, uwrappers)) cs2; + val cs1 = cs addSIs safeIs' addSEs safeEs' addIs hazIs' addEs hazEs'; + val cs2 = map_swrappers (fn ws => AList.merge (op =) (K true) (ws, swrappers)) cs1; + val cs3 = map_uwrappers (fn ws => AList.merge (op =) (K true) (ws, uwrappers)) cs2; in cs3 end; (**** Simple tactics for theorem proving ****) (*Attack subgoals using safe inferences -- matching, not resolution*) -fun safe_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = +fun safe_step_tac (cs as CS {safe0_netpair, safep_netpair, ...}) = appSWrappers cs (FIRST' [ eq_assume_tac, eq_mp_tac, @@ -659,8 +647,8 @@ 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)); +fun safe_steps_tac cs = + REPEAT_DETERM1 o (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)); @@ -668,20 +656,20 @@ (*** Clarify_tac: do safe steps without causing branching ***) -fun nsubgoalsP n (k,brl) = (subgoals_of_brl brl = n); +fun nsubgoalsP n (k, brl) = (subgoals_of_brl brl = n); (*version of bimatch_from_nets_tac that only applies rules that create precisely n subgoals.*) fun n_bimatch_from_nets_tac n = - biresolution_from_nets_tac (order_list o filter (nsubgoalsP n)) true; + biresolution_from_nets_tac (order_list o filter (nsubgoalsP n)) true; fun eq_contr_tac i = ematch_tac [not_elim] i THEN eq_assume_tac i; val eq_assume_contr_tac = eq_assume_tac ORELSE' eq_contr_tac; (*Two-way branching is allowed only if one of the branches immediately closes*) fun bimatch2_tac netpair i = - n_bimatch_from_nets_tac 2 netpair i THEN - (eq_assume_contr_tac i ORELSE eq_assume_contr_tac (i+1)); + n_bimatch_from_nets_tac 2 netpair i THEN + (eq_assume_contr_tac i ORELSE eq_assume_contr_tac (i + 1)); (*Attack subgoals using safe inferences -- matching, not resolution*) fun clarify_step_tac (cs as CS{safe0_netpair,safep_netpair,...}) = @@ -715,13 +703,13 @@ biresolve_from_nets_tac haz_netpair; (*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; +fun step_tac cs i = + safe_tac cs ORELSE appWrappers cs (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; +fun slow_step_tac cs i = + safe_tac cs ORELSE appWrappers cs (inst_step_tac cs APPEND' haz_step_tac cs) i; (**** The following tactics all fail unless they solve one goal ****) @@ -749,20 +737,21 @@ (***ASTAR with weight weight_ASTAR, by Norbert Voelker*) -val weight_ASTAR = Unsynchronized.ref 5; +val weight_ASTAR = Unsynchronized.ref 5; (* FIXME argument / config option !? *) fun astar_tac cs = Object_Logic.atomize_prems_tac THEN' SELECT_GOAL - (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev) + (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + ! weight_ASTAR * lev) (step_tac cs 1)); fun slow_astar_tac cs = Object_Logic.atomize_prems_tac THEN' SELECT_GOAL - (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev) + (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + ! weight_ASTAR * lev) (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 easy theorems faster, but loses completeness -- and many of the harder @@ -776,29 +765,26 @@ (*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); -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)) - )) i state; + fun slow_step_tac' cs = appWrappers 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)))) i state; end; (*Search, with depth bound m. This is the "entry point", which does safe inferences first.*) -fun safe_depth_tac cs m = - SUBGOAL - (fn (prem,i) => - let val deti = - (*No Vars in the goal? No need to backtrack between goals.*) - if exists_subterm (fn Var _ => true | _ => false) prem then DETERM else I - in SELECT_GOAL (TRY (safe_tac cs) THEN - DEPTH_SOLVE (deti (depth_tac cs m 1))) i - end); +fun safe_depth_tac cs m = SUBGOAL (fn (prem,i) => + let val deti = + (*No Vars in the goal? No need to backtrack between goals.*) + if exists_subterm (fn Var _ => true | _ => false) prem then DETERM else I + in + SELECT_GOAL (TRY (safe_tac cs) THEN DEPTH_SOLVE (deti (depth_tac cs m 1))) i + end); -fun deepen_tac cs = DEEPEN (2,10) (safe_depth_tac cs); +fun deepen_tac cs = DEEPEN (2, 10) (safe_depth_tac cs);