--- 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')],
--- 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);