# HG changeset patch # User wenzelm # Date 1439718368 -7200 # Node ID 7cf1ea00a0201d246b13bd1f87567317eac3d06c # Parent 0af3e522406c4b7a7fe8b3ae3d5dcdd95e6d4a66 tuned signature; diff -r 0af3e522406c -r 7cf1ea00a020 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Sun Aug 16 11:29:06 2015 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Sun Aug 16 11:46:08 2015 +0200 @@ -311,10 +311,11 @@ let fun add stature th = Termtab.update (normalize_vars (Thm.prop_of th), stature) - val {safeIs, (* safeEs, *) hazIs, (* hazEs, *) ...} = ctxt |> claset_of |> Classical.rep_cs - val intros = Item_Net.content safeIs @ Item_Net.content hazIs + val {safeIs, (* safeEs, *) unsafeIs, (* unsafeEs, *) ...} = + ctxt |> claset_of |> Classical.rep_cs + val intros = Item_Net.content safeIs @ Item_Net.content unsafeIs (* Add once it is used: - val elims = Item_Net.content safeEs @ Item_Net.content hazEs + val elims = Item_Net.content safeEs @ Item_Net.content unsafeEs |> map Classical.classical_rule *) val specs = Spec_Rules.get ctxt diff -r 0af3e522406c -r 7cf1ea00a020 src/Provers/blast.ML --- a/src/Provers/blast.ML Sun Aug 16 11:29:06 2015 +0200 +++ b/src/Provers/blast.ML Sun Aug 16 11:46:08 2015 +0200 @@ -29,7 +29,7 @@ the formulae get into the wrong order (see WRONG below). With substition for equalities (hyp_subst_tac): - When substitution affects a haz formula or literal, it is moved + When substitution affects an unsage formula or literal, it is moved back to the list of safe formulae. But there's no way of putting it in the right place. A "moved" or "no DETERM" flag would prevent proofs failing here. @@ -93,7 +93,7 @@ (*Pending formulae carry md (may duplicate) flags*) type branch = {pairs: ((term*bool) list * (*safe formulae on this level*) - (term*bool) list) list, (*haz formulae on this level*) + (term*bool) list) list, (*unsafe formulae on this level*) lits: term list, (*literals: irreducible formulae*) vars: term option Unsynchronized.ref list, (*variables occurring in branch*) lim: int}; (*resource limit*) @@ -531,7 +531,7 @@ (*Tableau rule from introduction rule. Flag "upd" says that the inference updated the branch. Flag "dup" requests duplication of the affected formula. - Since haz rules are now delayed, "dup" is always FALSE for + Since unsafe rules are now delayed, "dup" is always FALSE for introduction rules.*) fun fromIntrRule (state as State {ctxt, ...}) vars rl = let val thy = Proof_Context.theory_of ctxt @@ -623,7 +623,7 @@ (*Converts all Goals to Nots in the safe parts of a branch. They could have been moved there from the literals list after substitution (equalSubst). There can be at most one--this function could be made more efficient.*) -fun negOfGoals pairs = map (fn (Gs,haz) => (map negOfGoal2 Gs, haz)) pairs; +fun negOfGoals pairs = map (fn (Gs, unsafe) => (map negOfGoal2 Gs, unsafe)) pairs; (*Tactic. Convert *Goal* to negated assumption in FIRST position*) fun negOfGoal_tac ctxt i = @@ -922,18 +922,18 @@ let val State {ctxt, ntrail, nclosed, ntried, ...} = state; val trace = Config.get ctxt trace; val stats = Config.get ctxt stats; - val {safe0_netpair, safep_netpair, haz_netpair, ...} = + val {safe0_netpair, safep_netpair, unsafe_netpair, ...} = Classical.rep_cs (Classical.claset_of ctxt); - val safeList = [safe0_netpair, safep_netpair] - and hazList = [haz_netpair] + val safeList = [safe0_netpair, safep_netpair]; + val unsafeList = [unsafe_netpair]; fun prv (tacs, trs, choices, []) = (printStats state (trace orelse stats, start, tacs); cont (tacs, trs, choices)) (*all branches closed!*) | prv (tacs, trs, choices, - brs0 as {pairs = ((G,md)::br, haz)::pairs, + brs0 as {pairs = ((G,md)::br, unsafe)::pairs, lits, vars, lim} :: brs) = (*apply a safe rule only (possibly allowing instantiation); - defer any haz formulae*) + defer any unsafe formulae*) let exception PRV (*backtrack to precisely this recursion!*) val ntrl = !ntrail val nbrs = length brs0 @@ -945,12 +945,12 @@ map (fn prem => if (exists isGoal prem) then {pairs = ((joinMd md prem, []) :: - negOfGoals ((br, haz)::pairs)), + negOfGoals ((br, unsafe)::pairs)), lits = map negOfGoal lits, vars = vars', lim = lim'} else {pairs = ((joinMd md prem, []) :: - (br, haz) :: pairs), + (br, unsafe) :: pairs), lits = lits, vars = vars', lim = lim'}) @@ -1014,11 +1014,11 @@ [this handler is pruned if possible!]*) (clearTo state ntrl; closeF Ls) end - (*Try to unify a queued formula (safe or haz) with head goal*) + (*Try to unify a queued formula (safe or unsafe) with head goal*) fun closeFl [] = raise CLOSEF - | closeFl ((br, haz)::pairs) = + | closeFl ((br, unsafe)::pairs) = closeF (map fst br) - handle CLOSEF => closeF (map fst haz) + handle CLOSEF => closeF (map fst unsafe) handle CLOSEF => closeFl pairs in trace_prover state brs0; @@ -1027,49 +1027,49 @@ prv (Data.hyp_subst_tac ctxt trace :: tacs, brs0::trs, choices, equalSubst ctxt - (G, {pairs = (br,haz)::pairs, + (G, {pairs = (br,unsafe)::pairs, lits = lits, vars = vars, lim = lim}) :: brs) handle DEST_EQ => closeF lits - handle CLOSEF => closeFl ((br,haz)::pairs) + handle CLOSEF => closeFl ((br,unsafe)::pairs) handle CLOSEF => deeper rules handle NEWBRANCHES => - (case netMkRules state G vars hazList of - [] => (*there are no plausible haz rules*) + (case netMkRules state G vars unsafeList of + [] => (*there are no plausible unsafe rules*) (cond_tracing trace (fn () => "moving formula to literals"); prv (tacs, brs0::trs, choices, - {pairs = (br,haz)::pairs, + {pairs = (br,unsafe)::pairs, lits = addLit(G,lits), vars = vars, lim = lim} :: brs)) - | _ => (*G admits some haz rules: try later*) - (cond_tracing trace (fn () => "moving formula to haz list"); + | _ => (*G admits some unsafe rules: try later*) + (cond_tracing trace (fn () => "moving formula to unsafe list"); prv (if isGoal G then negOfGoal_tac ctxt :: tacs else tacs, brs0::trs, choices, - {pairs = (br, haz@[(negOfGoal G, md)])::pairs, + {pairs = (br, unsafe@[(negOfGoal G, md)])::pairs, lits = lits, vars = vars, lim = lim} :: brs))) end | prv (tacs, trs, choices, - {pairs = ([],haz)::(Gs,haz')::pairs, lits, vars, lim} :: brs) = - (*no more "safe" formulae: transfer haz down a level*) + {pairs = ([],unsafe)::(Gs,unsafe')::pairs, lits, vars, lim} :: brs) = + (*no more "safe" formulae: transfer unsafe down a level*) prv (tacs, trs, choices, - {pairs = (Gs,haz@haz')::pairs, + {pairs = (Gs,unsafe@unsafe')::pairs, lits = lits, vars = vars, lim = lim} :: brs) | prv (tacs, trs, choices, brs0 as {pairs = [([], (H,md)::Hs)], lits, vars, lim} :: brs) = - (*no safe steps possible at any level: apply a haz rule*) + (*no safe steps possible at any level: apply a unsafe rule*) let exception PRV (*backtrack to precisely this recursion!*) val H = norm H val ntrl = !ntrail - val rules = netMkRules state H vars hazList - (*new premises of haz rules may NOT be duplicated*) + val rules = netMkRules state H vars unsafeList + (*new premises of unsafe rules may NOT be duplicated*) fun newPrem (vars,P,dup,lim') prem = let val Gs' = map (fn Q => (Q,false)) prem and Hs' = if dup then Hs @ [(negOfGoal H, md)] else Hs @@ -1078,7 +1078,7 @@ else lits in {pairs = if exists (match P) prem then [(Gs',Hs')] (*Recursive in this premise. Don't make new - "stack frame". New haz premises will end up + "stack frame". New unsafe premises will end up at the BACK of the queue, preventing exclusion of others*) else [(Gs',[]), ([],Hs')], diff -r 0af3e522406c -r 7cf1ea00a020 src/Provers/clasimp.ML --- a/src/Provers/clasimp.ML Sun Aug 16 11:29:06 2015 +0200 +++ b/src/Provers/clasimp.ML Sun Aug 16 11:46:08 2015 +0200 @@ -90,7 +90,7 @@ Thm.declaration_attribute (fn th => Thm.attribute_declaration (add_iff (Classical.safe_elim NONE, Classical.safe_intro NONE) - (Classical.haz_elim NONE, Classical.haz_intro NONE)) th + (Classical.unsafe_elim NONE, Classical.unsafe_intro NONE)) th #> Thm.attribute_declaration Simplifier.simp_add th); val iff_add' = @@ -122,7 +122,7 @@ fun slow_step_tac' ctxt = Classical.appWrappers ctxt - (Classical.instp_step_tac ctxt APPEND' Classical.haz_step_tac ctxt); + (Classical.instp_step_tac ctxt APPEND' Classical.unsafe_step_tac ctxt); in diff -r 0af3e522406c -r 7cf1ea00a020 src/Provers/classical.ML --- a/src/Provers/classical.ML Sun Aug 16 11:29:06 2015 +0200 +++ b/src/Provers/classical.ML Sun Aug 16 11:46:08 2015 +0200 @@ -4,7 +4,7 @@ Theorem prover for classical reasoning, including predicate calculus, set theory, etc. -Rules must be classified as intro, elim, safe, hazardous (unsafe). +Rules must be classified as intro, elim, safe, unsafe. A rule is unsafe unless it can be applied blindly without harmful results. For a rule to be safe, its premises and conclusion should be logically @@ -76,7 +76,7 @@ val dup_intr: thm -> thm val dup_step_tac: Proof.context -> int -> tactic val eq_mp_tac: Proof.context -> int -> tactic - val haz_step_tac: Proof.context -> int -> tactic + val unsafe_step_tac: Proof.context -> int -> tactic val joinrules: thm list * thm list -> (bool * thm) list val mp_tac: Proof.context -> int -> tactic val safe_tac: Proof.context -> tactic @@ -101,13 +101,13 @@ val rep_cs: claset -> {safeIs: thm Item_Net.T, safeEs: thm Item_Net.T, - hazIs: thm Item_Net.T, - hazEs: thm Item_Net.T, + unsafeIs: thm Item_Net.T, + unsafeEs: thm Item_Net.T, swrappers: (string * (Proof.context -> wrapper)) list, uwrappers: (string * (Proof.context -> wrapper)) list, safe0_netpair: netpair, safep_netpair: netpair, - haz_netpair: netpair, + unsafe_netpair: netpair, dup_netpair: netpair, extra_netpair: Context_Rules.netpair} val get_cs: Context.generic -> claset @@ -115,9 +115,9 @@ val safe_dest: int option -> attribute val safe_elim: int option -> attribute val safe_intro: int option -> attribute - val haz_dest: int option -> attribute - val haz_elim: int option -> attribute - val haz_intro: int option -> attribute + val unsafe_dest: int option -> attribute + val unsafe_elim: int option -> attribute + val unsafe_intro: int option -> attribute val rule_del: attribute val cla_modifiers: Method.modifier parser list val cla_method: @@ -199,7 +199,7 @@ biresolve_tac ctxt (fold_rev addrl rls []) end; -(*Duplication of hazardous rules, for complete provers*) +(*Duplication of unsafe rules, for complete provers*) fun dup_intr th = zero_var_indexes (th RS Data.classical); fun dup_elim ctxt th = @@ -216,13 +216,13 @@ CS of {safeIs : thm Item_Net.T, (*safe introduction rules*) safeEs : thm Item_Net.T, (*safe elimination rules*) - hazIs : thm Item_Net.T, (*unsafe introduction rules*) - hazEs : thm Item_Net.T, (*unsafe elimination rules*) + unsafeIs : thm Item_Net.T, (*unsafe introduction rules*) + unsafeEs : thm Item_Net.T, (*unsafe elimination rules*) swrappers : (string * (Proof.context -> wrapper)) list, (*for transforming safe_step_tac*) uwrappers : (string * (Proof.context -> 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*) + unsafe_netpair : netpair, (*nets for unsafe rules*) dup_netpair : netpair, (*nets for duplication*) extra_netpair : Context_Rules.netpair}; (*nets for extra rules*) @@ -232,13 +232,13 @@ CS {safeIs = Thm.full_rules, safeEs = Thm.full_rules, - hazIs = Thm.full_rules, - hazEs = Thm.full_rules, + unsafeIs = Thm.full_rules, + unsafeEs = Thm.full_rules, swrappers = [], uwrappers = [], safe0_netpair = empty_netpair, safep_netpair = empty_netpair, - haz_netpair = empty_netpair, + unsafe_netpair = empty_netpair, dup_netpair = empty_netpair, extra_netpair = empty_netpair}; @@ -299,18 +299,18 @@ fun warn_rules opt_context msg rules th = Item_Net.member rules th andalso (warn_thm opt_context msg th; true); -fun warn_claset opt_context th (CS {safeIs, safeEs, hazIs, hazEs, ...}) = +fun warn_claset opt_context th (CS {safeIs, safeEs, unsafeIs, unsafeEs, ...}) = warn_rules opt_context "Rule already declared as safe introduction (intro!)\n" safeIs th orelse warn_rules opt_context "Rule already declared as safe elimination (elim!)\n" safeEs th orelse - warn_rules opt_context "Rule already declared as introduction (intro)\n" hazIs th orelse - warn_rules opt_context "Rule already declared as elimination (elim)\n" hazEs th; + warn_rules opt_context "Rule already declared as introduction (intro)\n" unsafeIs th orelse + warn_rules opt_context "Rule already declared as elimination (elim)\n" unsafeEs th; (*** Safe rules ***) fun addSI w opt_context th - (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair, extra_netpair}) = + (cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, + safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = if warn_rules opt_context "Ignoring duplicate safe introduction (intro!)\n" safeIs th then cs else let @@ -327,18 +327,18 @@ safe0_netpair = insert (nI,nE) (safe0_rls, []) safe0_netpair, safep_netpair = insert (nI,nE) (safep_rls, []) safep_netpair, safeEs = safeEs, - hazIs = hazIs, - hazEs = hazEs, + unsafeIs = unsafeIs, + unsafeEs = unsafeEs, swrappers = swrappers, uwrappers = uwrappers, - haz_netpair = haz_netpair, + unsafe_netpair = unsafe_netpair, dup_netpair = dup_netpair, extra_netpair = insert' (the_default 0 w) (nI,nE) ([th], []) extra_netpair} end; fun addSE w opt_context th - (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair, extra_netpair}) = + (cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, + safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = if warn_rules opt_context "Ignoring duplicate safe elimination (elim!)\n" safeEs th then cs else if has_fewer_prems 1 th then bad_thm opt_context "Ill-formed elimination rule" th else @@ -356,11 +356,11 @@ safe0_netpair = insert (nI,nE) ([], safe0_rls) safe0_netpair, safep_netpair = insert (nI,nE) ([], safep_rls) safep_netpair, safeIs = safeIs, - hazIs = hazIs, - hazEs = hazEs, + unsafeIs = unsafeIs, + unsafeEs = unsafeEs, swrappers = swrappers, uwrappers = uwrappers, - haz_netpair = haz_netpair, + unsafe_netpair = unsafe_netpair, dup_netpair = dup_netpair, extra_netpair = insert' (the_default 0 w) (nI,nE) ([], [th]) extra_netpair} end; @@ -371,24 +371,24 @@ (*** Hazardous (unsafe) rules ***) fun addI w opt_context th - (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair, extra_netpair}) = - if warn_rules opt_context "Ignoring duplicate introduction (intro)\n" hazIs th then cs + (cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, + safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = + if warn_rules opt_context "Ignoring duplicate introduction (intro)\n" unsafeIs th then cs else let val ctxt = default_context opt_context th; val th' = flat_rule ctxt th; - val nI = Item_Net.length hazIs + 1; - val nE = Item_Net.length hazEs; + val nI = Item_Net.length unsafeIs + 1; + val nE = Item_Net.length unsafeEs; val _ = warn_claset opt_context th cs; in CS - {hazIs = Item_Net.update th hazIs, - haz_netpair = insert (nI, nE) ([th'], []) haz_netpair, + {unsafeIs = Item_Net.update th unsafeIs, + unsafe_netpair = insert (nI, nE) ([th'], []) unsafe_netpair, dup_netpair = insert (nI, nE) ([dup_intr th'], []) dup_netpair, safeIs = safeIs, safeEs = safeEs, - hazEs = hazEs, + unsafeEs = unsafeEs, swrappers = swrappers, uwrappers = uwrappers, safe0_netpair = safe0_netpair, @@ -399,25 +399,25 @@ bad_thm opt_context "Ill-formed introduction rule" th; fun addE w opt_context th - (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair, extra_netpair}) = - if warn_rules opt_context "Ignoring duplicate elimination (elim)\n" hazEs th then cs + (cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, + safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = + if warn_rules opt_context "Ignoring duplicate elimination (elim)\n" unsafeEs th then cs else if has_fewer_prems 1 th then bad_thm opt_context "Ill-formed elimination rule" th else let val ctxt = default_context opt_context th; val th' = classical_rule ctxt (flat_rule ctxt th); - val nI = Item_Net.length hazIs; - val nE = Item_Net.length hazEs + 1; + val nI = Item_Net.length unsafeIs; + val nE = Item_Net.length unsafeEs + 1; val _ = warn_claset opt_context th cs; in CS - {hazEs = Item_Net.update th hazEs, - haz_netpair = insert (nI, nE) ([], [th']) haz_netpair, + {unsafeEs = Item_Net.update th unsafeEs, + unsafe_netpair = insert (nI, nE) ([], [th']) unsafe_netpair, dup_netpair = insert (nI, nE) ([], [dup_elim ctxt th']) dup_netpair, safeIs = safeIs, safeEs = safeEs, - hazIs = hazIs, + unsafeIs = unsafeIs, swrappers = swrappers, uwrappers = uwrappers, safe0_netpair = safe0_netpair, @@ -435,8 +435,8 @@ ***) fun delSI opt_context th - (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair, extra_netpair}) = + (cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, + safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = if Item_Net.member safeIs th then let val ctxt = default_context opt_context th; @@ -448,19 +448,19 @@ safep_netpair = delete (safep_rls, []) safep_netpair, safeIs = Item_Net.remove th safeIs, safeEs = safeEs, - hazIs = hazIs, - hazEs = hazEs, + unsafeIs = unsafeIs, + unsafeEs = unsafeEs, swrappers = swrappers, uwrappers = uwrappers, - haz_netpair = haz_netpair, + unsafe_netpair = unsafe_netpair, dup_netpair = dup_netpair, extra_netpair = delete' ([th], []) extra_netpair} end else cs; fun delSE opt_context th - (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair, extra_netpair}) = + (cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, + safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = if Item_Net.member safeEs th then let val ctxt = default_context opt_context th; @@ -472,31 +472,31 @@ safep_netpair = delete ([], safep_rls) safep_netpair, safeIs = safeIs, safeEs = Item_Net.remove th safeEs, - hazIs = hazIs, - hazEs = hazEs, + unsafeIs = unsafeIs, + unsafeEs = unsafeEs, swrappers = swrappers, uwrappers = uwrappers, - haz_netpair = haz_netpair, + unsafe_netpair = unsafe_netpair, dup_netpair = dup_netpair, extra_netpair = delete' ([], [th]) extra_netpair} end else cs; fun delI opt_context th - (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair, extra_netpair}) = - if Item_Net.member hazIs th then + (cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, + safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = + if Item_Net.member unsafeIs th then let val ctxt = default_context opt_context th; val th' = flat_rule ctxt th; in CS - {haz_netpair = delete ([th'], []) haz_netpair, + {unsafe_netpair = delete ([th'], []) unsafe_netpair, dup_netpair = delete ([dup_intr th'], []) dup_netpair, safeIs = safeIs, safeEs = safeEs, - hazIs = Item_Net.remove th hazIs, - hazEs = hazEs, + unsafeIs = Item_Net.remove th unsafeIs, + unsafeEs = unsafeEs, swrappers = swrappers, uwrappers = uwrappers, safe0_netpair = safe0_netpair, @@ -508,20 +508,20 @@ bad_thm opt_context "Ill-formed introduction rule" th; fun delE opt_context th - (cs as CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair, extra_netpair}) = - if Item_Net.member hazEs th then + (cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, + safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = + if Item_Net.member unsafeEs th then let val ctxt = default_context opt_context th; val th' = classical_rule ctxt (flat_rule ctxt th); in CS - {haz_netpair = delete ([], [th']) haz_netpair, + {unsafe_netpair = delete ([], [th']) unsafe_netpair, dup_netpair = delete ([], [dup_elim ctxt th']) dup_netpair, safeIs = safeIs, safeEs = safeEs, - hazIs = hazIs, - hazEs = Item_Net.remove th hazEs, + unsafeIs = unsafeIs, + unsafeEs = Item_Net.remove th unsafeEs, swrappers = swrappers, uwrappers = uwrappers, safe0_netpair = safe0_netpair, @@ -531,11 +531,11 @@ else cs; (*Delete ALL occurrences of "th" in the claset (perhaps from several lists)*) -fun delrule opt_context th (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}) = +fun delrule opt_context th (cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, ...}) = let val th' = Tactic.make_elim th in if Item_Net.member safeIs th orelse Item_Net.member safeEs th orelse - Item_Net.member hazIs th orelse Item_Net.member hazEs th orelse - Item_Net.member safeEs th' orelse Item_Net.member hazEs th' + Item_Net.member unsafeIs th orelse Item_Net.member unsafeEs th orelse + Item_Net.member safeEs th' orelse Item_Net.member unsafeEs th' then cs |> delE opt_context th' @@ -554,20 +554,20 @@ (* wrappers *) fun map_swrappers f - (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair, extra_netpair}) = - CS {safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, + (CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, + safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = + CS {safeIs = safeIs, safeEs = safeEs, unsafeIs = unsafeIs, unsafeEs = unsafeEs, swrappers = f swrappers, uwrappers = uwrappers, safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, - haz_netpair = haz_netpair, dup_netpair = dup_netpair, extra_netpair = extra_netpair}; + unsafe_netpair = unsafe_netpair, dup_netpair = dup_netpair, extra_netpair = extra_netpair}; fun map_uwrappers f - (CS {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, - safe0_netpair, safep_netpair, haz_netpair, dup_netpair, extra_netpair}) = - CS {safeIs = safeIs, safeEs = safeEs, hazIs = hazIs, hazEs = hazEs, + (CS {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, + safe0_netpair, safep_netpair, unsafe_netpair, dup_netpair, extra_netpair}) = + CS {safeIs = safeIs, safeEs = safeEs, unsafeIs = unsafeIs, unsafeEs = unsafeEs, swrappers = swrappers, uwrappers = f uwrappers, safe0_netpair = safe0_netpair, safep_netpair = safep_netpair, - haz_netpair = haz_netpair, dup_netpair = dup_netpair, extra_netpair = extra_netpair}; + unsafe_netpair = unsafe_netpair, dup_netpair = dup_netpair, extra_netpair = extra_netpair}; (* merge_cs *) @@ -578,16 +578,16 @@ fun merge_thms add thms1 thms2 = fold_rev (fn thm => if Item_Net.member thms1 thm then I else add thm) (Item_Net.content thms2); -fun merge_cs (cs as CS {safeIs, safeEs, hazIs, hazEs, ...}, - cs' as CS {safeIs = safeIs2, safeEs = safeEs2, hazIs = hazIs2, hazEs = hazEs2, +fun merge_cs (cs as CS {safeIs, safeEs, unsafeIs, unsafeEs, ...}, + cs' as CS {safeIs = safeIs2, safeEs = safeEs2, unsafeIs = unsafeIs2, unsafeEs = unsafeEs2, swrappers, uwrappers, ...}) = if pointer_eq (cs, cs') then cs else cs |> merge_thms (addSI NONE NONE) safeIs safeIs2 |> merge_thms (addSE NONE NONE) safeEs safeEs2 - |> merge_thms (addI NONE NONE) hazIs hazIs2 - |> merge_thms (addE NONE NONE) hazEs hazEs2 + |> merge_thms (addI NONE NONE) unsafeIs unsafeIs2 + |> merge_thms (addE NONE NONE) unsafeEs unsafeEs2 |> map_swrappers (fn ws => AList.merge (op =) (K true) (ws, swrappers)) |> map_uwrappers (fn ws => AList.merge (op =) (K true) (ws, uwrappers)); @@ -619,13 +619,13 @@ fun print_claset ctxt = let - val {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...} = rep_claset_of ctxt; + val {safeIs, safeEs, unsafeIs, unsafeEs, swrappers, uwrappers, ...} = rep_claset_of ctxt; val pretty_thms = map (Display.pretty_thm_item ctxt) o Item_Net.content; in [Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs), - Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs), + Pretty.big_list "introduction rules (intro):" (pretty_thms unsafeIs), Pretty.big_list "safe elimination rules (elim!):" (pretty_thms safeEs), - Pretty.big_list "elimination rules (elim):" (pretty_thms hazEs), + Pretty.big_list "elimination rules (elim):" (pretty_thms unsafeEs), Pretty.strs ("safe wrappers:" :: map #1 swrappers), Pretty.strs ("unsafe wrappers:" :: map #1 uwrappers)] |> Pretty.writeln_chunks @@ -767,17 +767,17 @@ (*These steps could instantiate variables and are therefore unsafe.*) fun inst_step_tac ctxt = inst0_step_tac ctxt APPEND' instp_step_tac ctxt; -fun haz_step_tac ctxt = - biresolve_from_nets_tac ctxt (#haz_netpair (rep_claset_of ctxt)); +fun unsafe_step_tac ctxt = + biresolve_from_nets_tac ctxt (#unsafe_netpair (rep_claset_of ctxt)); (*Single step for the prover. FAILS unless it makes progress. *) fun step_tac ctxt i = - safe_tac ctxt ORELSE appWrappers ctxt (inst_step_tac ctxt ORELSE' haz_step_tac ctxt) i; + safe_tac ctxt ORELSE appWrappers ctxt (inst_step_tac ctxt ORELSE' unsafe_step_tac ctxt) 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 ctxt i = - safe_tac ctxt ORELSE appWrappers ctxt (inst_step_tac ctxt APPEND' haz_step_tac ctxt) i; + safe_tac ctxt ORELSE appWrappers ctxt (inst_step_tac ctxt APPEND' unsafe_step_tac ctxt) i; (**** The following tactics all fail unless they solve one goal ****) @@ -866,9 +866,9 @@ val safe_elim = attrib o addSE; val safe_intro = attrib o addSI; val safe_dest = attrib o addSD; -val haz_elim = attrib o addE; -val haz_intro = attrib o addI; -val haz_dest = attrib o addD; +val unsafe_elim = attrib o addE; +val unsafe_intro = attrib o addI; +val unsafe_dest = attrib o addD; val rule_del = Thm.declaration_attribute (fn th => fn opt_context => @@ -887,11 +887,11 @@ Theory.setup (Attrib.setup @{binding swapped} (Scan.succeed swapped) "classical swap of introduction rule" #> - Attrib.setup @{binding dest} (Context_Rules.add safe_dest haz_dest Context_Rules.dest_query) + Attrib.setup @{binding dest} (Context_Rules.add safe_dest unsafe_dest Context_Rules.dest_query) "declaration of Classical destruction rule" #> - Attrib.setup @{binding elim} (Context_Rules.add safe_elim haz_elim Context_Rules.elim_query) + Attrib.setup @{binding elim} (Context_Rules.add safe_elim unsafe_elim Context_Rules.elim_query) "declaration of Classical elimination rule" #> - Attrib.setup @{binding intro} (Context_Rules.add safe_intro haz_intro Context_Rules.intro_query) + Attrib.setup @{binding intro} (Context_Rules.add safe_intro unsafe_intro Context_Rules.intro_query) "declaration of Classical introduction rule" #> Attrib.setup @{binding rule} (Scan.lift Args.del >> K rule_del) "remove declaration of intro/elim/dest rule"); @@ -938,11 +938,11 @@ val cla_modifiers = [Args.$$$ destN -- Args.bang_colon >> K (Method.modifier (safe_dest NONE) @{here}), - Args.$$$ destN -- Args.colon >> K (Method.modifier (haz_dest NONE) @{here}), + Args.$$$ destN -- Args.colon >> K (Method.modifier (unsafe_dest NONE) @{here}), Args.$$$ elimN -- Args.bang_colon >> K (Method.modifier (safe_elim NONE) @{here}), - Args.$$$ elimN -- Args.colon >> K (Method.modifier (haz_elim NONE) @{here}), + Args.$$$ elimN -- Args.colon >> K (Method.modifier (unsafe_elim NONE) @{here}), Args.$$$ introN -- Args.bang_colon >> K (Method.modifier (safe_intro NONE) @{here}), - Args.$$$ introN -- Args.colon >> K (Method.modifier (haz_intro NONE) @{here}), + Args.$$$ introN -- Args.colon >> K (Method.modifier (unsafe_intro NONE) @{here}), Args.del -- Args.colon >> K (Method.modifier rule_del @{here})]; fun cla_method tac = Method.sections cla_modifiers >> K (SIMPLE_METHOD o tac);