made "query" type systes a bit more sound -- local facts, e.g. the negated conjecture, may make invalid the infinity check, e.g. if we are proving that there exists two values of an infinite type, we can use the negated conjecture that there is only one value to derive unsound proofs unless the type is properly encoded
(* Title: HOL/Tools/Function/scnp_reconstruct.ML
Author: Armin Heller, TU Muenchen
Author: Alexander Krauss, TU Muenchen
Proof reconstruction for SCNP termination.
*)
signature SCNP_RECONSTRUCT =
sig
val sizechange_tac : Proof.context -> tactic -> tactic
val decomp_scnp_tac : ScnpSolve.label list -> Proof.context -> tactic
val setup : theory -> theory
datatype multiset_setup =
Multiset of
{
msetT : typ -> typ,
mk_mset : typ -> term list -> term,
mset_regroup_conv : int list -> conv,
mset_member_tac : int -> int -> tactic,
mset_nonempty_tac : int -> tactic,
mset_pwleq_tac : int -> tactic,
set_of_simps : thm list,
smsI' : thm,
wmsI2'' : thm,
wmsI1 : thm,
reduction_pair : thm
}
val multiset_setup : multiset_setup -> theory -> theory
end
structure ScnpReconstruct : SCNP_RECONSTRUCT =
struct
val PROFILE = Function_Common.PROFILE
open ScnpSolve
val natT = HOLogic.natT
val nat_pairT = HOLogic.mk_prodT (natT, natT)
(* Theory dependencies *)
datatype multiset_setup =
Multiset of
{
msetT : typ -> typ,
mk_mset : typ -> term list -> term,
mset_regroup_conv : int list -> conv,
mset_member_tac : int -> int -> tactic,
mset_nonempty_tac : int -> tactic,
mset_pwleq_tac : int -> tactic,
set_of_simps : thm list,
smsI' : thm,
wmsI2'' : thm,
wmsI1 : thm,
reduction_pair : thm
}
structure Multiset_Setup = Theory_Data
(
type T = multiset_setup option
val empty = NONE
val extend = I;
val merge = merge_options
)
val multiset_setup = Multiset_Setup.put o SOME
fun undef _ = error "undef"
fun get_multiset_setup thy = Multiset_Setup.get thy
|> the_default (Multiset
{ msetT = undef, mk_mset=undef,
mset_regroup_conv=undef, mset_member_tac = undef,
mset_nonempty_tac = undef, mset_pwleq_tac = undef,
set_of_simps = [],reduction_pair = refl,
smsI'=refl, wmsI2''=refl, wmsI1=refl })
fun order_rpair _ MAX = @{thm max_rpair_set}
| order_rpair msrp MS = msrp
| order_rpair _ MIN = @{thm min_rpair_set}
fun ord_intros_max true =
(@{thm smax_emptyI}, @{thm smax_insertI})
| ord_intros_max false =
(@{thm wmax_emptyI}, @{thm wmax_insertI})
fun ord_intros_min true =
(@{thm smin_emptyI}, @{thm smin_insertI})
| ord_intros_min false =
(@{thm wmin_emptyI}, @{thm wmin_insertI})
fun gen_probl D cs =
let
val n = Termination.get_num_points D
val arity = length o Termination.get_measures D
fun measure p i = nth (Termination.get_measures D p) i
fun mk_graph c =
let
val (_, p, _, q, _, _) = Termination.dest_call D c
fun add_edge i j =
case Termination.get_descent D c (measure p i) (measure q j)
of SOME (Termination.Less _) => cons (i, GTR, j)
| SOME (Termination.LessEq _) => cons (i, GEQ, j)
| _ => I
val edges =
fold_product add_edge (0 upto arity p - 1) (0 upto arity q - 1) []
in
G (p, q, edges)
end
in
GP (map_range arity n, map mk_graph cs)
end
(* General reduction pair application *)
fun rem_inv_img ctxt =
let
val unfold_tac = Local_Defs.unfold_tac ctxt
in
rtac @{thm subsetI} 1
THEN etac @{thm CollectE} 1
THEN REPEAT (etac @{thm exE} 1)
THEN unfold_tac @{thms inv_image_def}
THEN rtac @{thm CollectI} 1
THEN etac @{thm conjE} 1
THEN etac @{thm ssubst} 1
THEN unfold_tac (@{thms split_conv} @ @{thms triv_forall_equality}
@ @{thms sum.cases})
end
(* Sets *)
val setT = HOLogic.mk_setT
fun set_member_tac m i =
if m = 0 then rtac @{thm insertI1} i
else rtac @{thm insertI2} i THEN set_member_tac (m - 1) i
val set_nonempty_tac = rtac @{thm insert_not_empty}
fun set_finite_tac i =
rtac @{thm finite.emptyI} i
ORELSE (rtac @{thm finite.insertI} i THEN (fn st => set_finite_tac i st))
(* Reconstruction *)
fun reconstruct_tac ctxt D cs (GP (_, gs)) certificate =
let
val thy = Proof_Context.theory_of ctxt
val Multiset
{ msetT, mk_mset,
mset_regroup_conv, mset_pwleq_tac, set_of_simps,
smsI', wmsI2'', wmsI1, reduction_pair=ms_rp, ...}
= get_multiset_setup thy
fun measure_fn p = nth (Termination.get_measures D p)
fun get_desc_thm cidx m1 m2 bStrict =
case Termination.get_descent D (nth cs cidx) m1 m2
of SOME (Termination.Less thm) =>
if bStrict then thm
else (thm COMP (Thm.lift_rule (cprop_of thm) @{thm less_imp_le}))
| SOME (Termination.LessEq (thm, _)) =>
if not bStrict then thm
else raise Fail "get_desc_thm"
| _ => raise Fail "get_desc_thm"
val (label, lev, sl, covering) = certificate
fun prove_lev strict g =
let
val G (p, q, _) = nth gs g
fun less_proof strict (j, b) (i, a) =
let
val tag_flag = b < a orelse (not strict andalso b <= a)
val stored_thm =
get_desc_thm g (measure_fn p i) (measure_fn q j)
(not tag_flag)
|> Conv.fconv_rule (Thm.beta_conversion true)
val rule = if strict
then if b < a then @{thm pair_lessI2} else @{thm pair_lessI1}
else if b <= a then @{thm pair_leqI2} else @{thm pair_leqI1}
in
rtac rule 1 THEN PRIMITIVE (Thm.elim_implies stored_thm)
THEN (if tag_flag then Arith_Data.arith_tac ctxt 1 else all_tac)
end
fun steps_tac MAX strict lq lp =
let
val (empty, step) = ord_intros_max strict
in
if length lq = 0
then rtac empty 1 THEN set_finite_tac 1
THEN (if strict then set_nonempty_tac 1 else all_tac)
else
let
val (j, b) :: rest = lq
val (i, a) = the (covering g strict j)
fun choose xs = set_member_tac (Library.find_index (curry op = (i, a)) xs) 1
val solve_tac = choose lp THEN less_proof strict (j, b) (i, a)
in
rtac step 1 THEN solve_tac THEN steps_tac MAX strict rest lp
end
end
| steps_tac MIN strict lq lp =
let
val (empty, step) = ord_intros_min strict
in
if length lp = 0
then rtac empty 1
THEN (if strict then set_nonempty_tac 1 else all_tac)
else
let
val (i, a) :: rest = lp
val (j, b) = the (covering g strict i)
fun choose xs = set_member_tac (Library.find_index (curry op = (j, b)) xs) 1
val solve_tac = choose lq THEN less_proof strict (j, b) (i, a)
in
rtac step 1 THEN solve_tac THEN steps_tac MIN strict lq rest
end
end
| steps_tac MS strict lq lp =
let
fun get_str_cover (j, b) =
if is_some (covering g true j) then SOME (j, b) else NONE
fun get_wk_cover (j, b) = the (covering g false j)
val qs = subtract (op =) (map_filter get_str_cover lq) lq
val ps = map get_wk_cover qs
fun indices xs ys = map (fn y => Library.find_index (curry op = y) xs) ys
val iqs = indices lq qs
val ips = indices lp ps
local open Conv in
fun t_conv a C =
params_conv ~1 (K ((concl_conv ~1 o arg_conv o arg1_conv o a) C)) ctxt
val goal_rewrite =
t_conv arg1_conv (mset_regroup_conv iqs)
then_conv t_conv arg_conv (mset_regroup_conv ips)
end
in
CONVERSION goal_rewrite 1
THEN (if strict then rtac smsI' 1
else if qs = lq then rtac wmsI2'' 1
else rtac wmsI1 1)
THEN mset_pwleq_tac 1
THEN EVERY (map2 (less_proof false) qs ps)
THEN (if strict orelse qs <> lq
then Local_Defs.unfold_tac ctxt set_of_simps
THEN steps_tac MAX true
(subtract (op =) qs lq) (subtract (op =) ps lp)
else all_tac)
end
in
rem_inv_img ctxt
THEN steps_tac label strict (nth lev q) (nth lev p)
end
val (mk_set, setT) = if label = MS then (mk_mset, msetT) else (HOLogic.mk_set, setT)
fun tag_pair p (i, tag) =
HOLogic.pair_const natT natT $
(measure_fn p i $ Bound 0) $ HOLogic.mk_number natT tag
fun pt_lev (p, lm) = Abs ("x", Termination.get_types D p,
mk_set nat_pairT (map (tag_pair p) lm))
val level_mapping =
map_index pt_lev lev
|> Termination.mk_sumcases D (setT nat_pairT)
|> cterm_of thy
in
PROFILE "Proof Reconstruction"
(CONVERSION (Conv.arg_conv (Conv.arg_conv (Function_Lib.regroup_union_conv sl))) 1
THEN (rtac @{thm reduction_pair_lemma} 1)
THEN (rtac @{thm rp_inv_image_rp} 1)
THEN (rtac (order_rpair ms_rp label) 1)
THEN PRIMITIVE (instantiate' [] [SOME level_mapping])
THEN unfold_tac @{thms rp_inv_image_def} (simpset_of ctxt)
THEN Local_Defs.unfold_tac ctxt
(@{thms split_conv} @ @{thms fst_conv} @ @{thms snd_conv})
THEN REPEAT (SOMEGOAL (resolve_tac [@{thm Un_least}, @{thm empty_subsetI}]))
THEN EVERY (map (prove_lev true) sl)
THEN EVERY (map (prove_lev false) (subtract (op =) sl (0 upto length cs - 1))))
end
fun single_scnp_tac use_tags orders ctxt D = Termination.CALLS (fn (cs, i) =>
let
val ms_configured = is_some (Multiset_Setup.get (Proof_Context.theory_of ctxt))
val orders' = if ms_configured then orders
else filter_out (curry op = MS) orders
val gp = gen_probl D cs
val certificate = generate_certificate use_tags orders' gp
in
case certificate
of NONE => no_tac
| SOME cert =>
SELECT_GOAL (reconstruct_tac ctxt D cs gp cert) i
THEN TRY (rtac @{thm wf_empty} i)
end)
local open Termination in
fun gen_decomp_scnp_tac orders autom_tac ctxt =
TERMINATION ctxt autom_tac (fn D =>
let
val decompose = decompose_tac D
val scnp_full = single_scnp_tac true orders ctxt D
in
REPEAT_ALL_NEW (scnp_full ORELSE' decompose)
end)
end
fun gen_sizechange_tac orders autom_tac ctxt =
TRY (Function_Common.apply_termination_rule ctxt 1)
THEN TRY (Termination.wf_union_tac ctxt)
THEN
(rtac @{thm wf_empty} 1
ORELSE gen_decomp_scnp_tac orders autom_tac ctxt 1)
fun sizechange_tac ctxt autom_tac =
gen_sizechange_tac [MAX, MS, MIN] autom_tac ctxt
fun decomp_scnp_tac orders ctxt =
let
val extra_simps = Function_Common.Termination_Simps.get ctxt
val autom_tac = auto_tac (map_simpset (fn ss => ss addsimps extra_simps) ctxt)
in
gen_sizechange_tac orders autom_tac ctxt
end
(* Method setup *)
val orders =
Scan.repeat1
((Args.$$$ "max" >> K MAX) ||
(Args.$$$ "min" >> K MIN) ||
(Args.$$$ "ms" >> K MS))
|| Scan.succeed [MAX, MS, MIN]
val setup = Method.setup @{binding size_change}
(Scan.lift orders --| Method.sections clasimp_modifiers >>
(fn orders => SIMPLE_METHOD o decomp_scnp_tac orders))
"termination prover with graph decomposition and the NP subset of size change termination"
end