File ‹classical.ML›
signature CLASSICAL_DATA =
sig
val mp: thm
val not_elim: thm
val swap: thm
val sizef : thm -> int
val hyp_subst_tacs: Proof.context -> (int -> tactic) list
end;
infix 4 addSIs addSEs addSDs addIs addEs addDs;
signature CLASSICAL =
sig
type claset
val empty_cs: 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 print_cs: Proof.context -> claset -> unit
val rep_cs: claset ->
{safeIs: thm list, safeEs: thm list, hazIs: thm list, hazEs: thm list,
safe0_brls:(bool*thm)list, safep_brls: (bool*thm)list,
haz_brls: (bool*thm)list}
val best_tac : Proof.context -> claset -> int -> tactic
val contr_tac : Proof.context -> int -> tactic
val fast_tac : Proof.context -> claset -> int -> tactic
val inst_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 -> claset -> tactic
val safe_step_tac : Proof.context -> claset -> int -> tactic
val slow_step_tac : Proof.context -> claset -> int -> tactic
val step_tac : Proof.context -> claset -> int -> tactic
val swapify : thm list -> thm list
val swap_res_tac : Proof.context -> thm list -> int -> tactic
val uniq_mp_tac: Proof.context -> int -> tactic
end;
functor Classical(Data: CLASSICAL_DATA): CLASSICAL =
struct
local open Data in
val imp_elim = make_elim mp;
fun contr_tac ctxt = eresolve_tac ctxt [not_elim] THEN' assume_tac ctxt;
fun mp_tac ctxt i = eresolve_tac ctxt ([not_elim,imp_elim]) i THEN assume_tac ctxt i;
fun uniq_mp_tac ctxt i = ematch_tac ctxt ([not_elim,imp_elim]) i THEN uniq_assume_tac ctxt i;
fun swapify intrs = intrs RLN (2, [swap]);
fun swap_res_tac ctxt rls =
let fun tacf rl = resolve_tac ctxt [rl] ORELSE' eresolve_tac ctxt [rl RSN (2, swap)]
in assume_tac ctxt ORELSE' contr_tac ctxt ORELSE' FIRST' (map tacf rls)
end;
datatype claset =
CS of {safeIs: thm list,
safeEs: thm list,
hazIs: thm list,
hazEs: thm list,
safe0_brls: (bool*thm)list,
safep_brls: (bool*thm)list,
haz_brls: (bool*thm)list};
fun rep_cs (CS x) = x;
fun joinrules (intrs,elims) =
map (pair true) (elims @ swapify intrs) @ map (pair false) intrs;
fun make_cs {safeIs,safeEs,hazIs,hazEs} =
let val (safe0_brls, safep_brls) =
List.partition (curry (op =) 0 o subgoals_of_brl)
(sort (make_ord lessb) (joinrules(safeIs, safeEs)))
in CS{safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs,
safe0_brls=safe0_brls, safep_brls=safep_brls,
haz_brls = sort (make_ord lessb) (joinrules(hazIs, hazEs))}
end;
val empty_cs = make_cs{safeIs=[], safeEs=[], hazIs=[], hazEs=[]};
fun print_cs ctxt (CS{safeIs,safeEs,hazIs,hazEs,...}) =
writeln (cat_lines
(["Introduction rules"] @ map (Thm.string_of_thm ctxt) hazIs @
["Safe introduction rules"] @ map (Thm.string_of_thm ctxt) safeIs @
["Elimination rules"] @ map (Thm.string_of_thm ctxt) hazEs @
["Safe elimination rules"] @ map (Thm.string_of_thm ctxt) safeEs));
fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSIs ths =
make_cs {safeIs=ths@safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=hazEs};
fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addSEs ths =
make_cs {safeIs=safeIs, safeEs=ths@safeEs, hazIs=hazIs, hazEs=hazEs};
fun cs addSDs ths = cs addSEs (map make_elim ths);
fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addIs ths =
make_cs {safeIs=safeIs, safeEs=safeEs, hazIs=ths@hazIs, hazEs=hazEs};
fun (CS{safeIs,safeEs,hazIs,hazEs,...}) addEs ths =
make_cs {safeIs=safeIs, safeEs=safeEs, hazIs=hazIs, hazEs=ths@hazEs};
fun cs addDs ths = cs addEs (map make_elim ths);
fun safe_step_tac ctxt (CS{safe0_brls,safep_brls,...}) =
FIRST' [uniq_assume_tac ctxt,
uniq_mp_tac ctxt,
biresolve_tac ctxt safe0_brls,
FIRST' (hyp_subst_tacs ctxt),
biresolve_tac ctxt safep_brls] ;
fun safe_tac ctxt cs = DETERM (REPEAT_FIRST (safe_step_tac ctxt cs));
fun inst_step_tac ctxt = assume_tac ctxt APPEND' contr_tac ctxt;
fun step_tac ctxt (cs as (CS{haz_brls,...})) i =
FIRST [safe_tac ctxt cs,
inst_step_tac ctxt i,
biresolve_tac ctxt haz_brls i];
fun fast_tac ctxt cs = SELECT_GOAL (DEPTH_SOLVE (step_tac ctxt cs 1));
fun best_tac ctxt cs =
SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac ctxt cs 1));
fun slow_step_tac ctxt (cs as (CS{haz_brls,...})) i =
safe_tac ctxt cs ORELSE (assume_tac ctxt i APPEND biresolve_tac ctxt haz_brls i);
end;
end;