--- a/src/HOL/Tools/Function/scnp_reconstruct.ML Wed Oct 29 14:05:36 2014 +0100
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Wed Oct 29 14:14:36 2014 +0100
@@ -7,13 +7,10 @@
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
{
@@ -30,9 +27,7 @@
reduction_pair : thm
}
-
val multiset_setup : multiset_setup -> theory -> theory
-
end
structure ScnpReconstruct : SCNP_RECONSTRUCT =
@@ -45,6 +40,7 @@
val natT = HOLogic.natT
val nat_pairT = HOLogic.mk_prodT (natT, natT)
+
(* Theory dependencies *)
datatype multiset_setup =
@@ -74,26 +70,24 @@
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 })
+ { 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 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
@@ -131,6 +125,7 @@
THEN etac @{thm ssubst} 1
THEN Local_Defs.unfold_tac ctxt @{thms split_conv triv_forall_equality sum.case}
+
(* Sets *)
val setT = HOLogic.mk_setT
@@ -154,20 +149,20 @@
val Multiset
{ msetT, mk_mset,
mset_regroup_conv, mset_pwleq_tac, set_of_simps,
- smsI', wmsI2'', wmsI1, reduction_pair=ms_rp, ...}
+ 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) =>
+ (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, _)) =>
+ | SOME (Termination.LessEq (thm, _)) =>
if not bStrict then thm
else raise Fail "get_desc_thm"
- | _ => raise Fail "get_desc_thm"
+ | _ => raise Fail "get_desc_thm")
val (label, lev, sl, covering) = certificate
@@ -184,7 +179,8 @@
(not tag_flag)
|> Conv.fconv_rule (Thm.beta_conversion true)
- val rule = if strict
+ 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
@@ -193,72 +189,72 @@
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)
+ val (empty, step) = ord_intros_max strict
in
- rtac step 1 THEN solve_tac THEN steps_tac MAX strict rest lp
+ 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
- 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)
+ val (empty, step) = ord_intros_min strict
in
- rtac step 1 THEN solve_tac THEN steps_tac MIN strict lq rest
+ 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
- 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)
+ 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
+ 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
+ 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
+ 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)
@@ -270,8 +266,8 @@
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))
+ 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
@@ -295,36 +291,32 @@
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 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)
+ (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
+ Termination.TERMINATION ctxt autom_tac (fn D =>
+ let
+ val decompose = Termination.decompose_tac D
+ val scnp_full = single_scnp_tac true orders ctxt D
+ in
+ REPEAT_ALL_NEW (scnp_full ORELSE' decompose)
+ 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)
+ 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
@@ -347,9 +339,11 @@
(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"
+val _ =
+ Theory.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