File ‹sturm.ML›
signature STURM =
sig
val sturm_conv : Proof.context -> conv
val sturm_tac : Proof.context -> bool -> int -> tactic
end;
structure Sturm : STURM =
struct
fun sturm_conv ctxt = Code_Runtime.dynamic_holds_conv ctxt
val sturm_id_thmss = [@{thms sturm_id_PR_prio2}, @{thms sturm_id_PR_prio1},
@{thms sturm_id_PR_prio0}]
val sturm_PR_tag_intro_thmss = [@{thms PR_TAG_intro_prio2}, @{thms PR_TAG_intro_prio1}, @{thms PR_TAG_intro_prio0}]
fun extract_PR_tags (t as (Const (@{const_name PR_TAG}, _) $ _)) acc = t :: acc
| extract_PR_tags (s $ t) acc = extract_PR_tags s (extract_PR_tags t acc)
| extract_PR_tags (Abs (_,_,t)) acc = extract_PR_tags t acc
| extract_PR_tags _ acc = acc
fun sturm_preprocess_tac ctxt i =
let fun subst_tac thms = EqSubst.eqsubst_tac ctxt [1] thms i
fun process_PR_tag_tac thm =
let val trms = extract_PR_tags (Thm.prop_of thm) []
fun tac trm =
let val subst = Thm.reflexive (Thm.cterm_of ctxt trm) RS @{thm HOL.meta_eq_to_obj_eq}
val subst = subst RS @{thm HOL.trans}
val subst = subst RS @{thm HOL.ssubst}
in TRY (resolve_tac ctxt [subst] i
THEN REPEAT_ALL_NEW (FIRST' (map (fn thms =>
DETERM o resolve_tac ctxt thms) sturm_PR_tag_intro_thmss)) i)
end;
in EVERY (map tac trms) thm
end;
in FIRST (map subst_tac sturm_id_thmss)
THEN REPEAT (subst_tac @{thms HOL.nnf_simps(1,2,5) not_less not_le})
THEN process_PR_tag_tac
end;
fun find_sturm_card_eq_thm ctxt s =
let val thy = Proof_Context.theory_of ctxt
fun matches thm =
case Thm.concl_of thm of
Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $
(Const (@{const_name Finite_Set.card}, _) $ s') $ _)
=> Pattern.matches thy (s',s)
| _ =>
let val _ = warning ("Invalid theorem in " ^
"sturm_card_eq_substs: \n" ^ Pretty.string_of (
Syntax.pretty_term ctxt (Thm.concl_of thm)));
in false
end
val thm = find_first matches @{thms sturm_card_substs};
in
thm
end;
fun sturm_card_eq_instantiate_tac ctxt _ thm =
let val prop = case Thm.prems_of thm of p :: _ => p | _ => Thm.concl_of thm
val prop = case prop of Const (@{const_name Pure.prop}, _) $ prop => prop
| _ => prop
val prop = case prop of Const (@{const_name Pure.conjunction}, _) $
(Const (@{const_name Pure.term}, _) $ _) $ prop => prop
| _ => prop
val (lhs,rhs) = prop |> HOLogic.dest_Trueprop |> HOLogic.dest_eq
val vars = Term.add_vars rhs []
in case vars of
[v] => let val (idxname,ty) = v
val n = Code_Evaluation.dynamic_value ctxt lhs
in case n of
NONE => Seq.empty
| SOME n =>
let val n' = (if ty = @{typ nat} then "" else "%_. ") ^ Int.toString (snd (HOLogic.dest_number n))
in Seq.single (Rule_Insts.read_instantiate ctxt [((idxname, Position.none), n')] [] thm)
end
end
| _ => Seq.single thm
end;
fun sturm_card_eq_tac ctxt i thm =
let val prop = case Thm.prems_of thm of p :: _ => p | _ => Thm.concl_of thm
val prop = case prop of Const (@{const_name Pure.prop}, _) $ prop => prop
| _ => prop
val prop = case prop of Const (@{const_name Pure.conjunction}, _) $
(Const (@{const_name Pure.term}, _) $ _) $ prop => prop
| _ => prop
val s = case prop of
Const (@{const_name Trueprop}, _) $
(Const (@{const_name HOL.eq}, _) $
(Const (@{const_name Finite_Set.card}, _) $ s) $ _)
=> s;
val thm' = find_sturm_card_eq_thm ctxt s
in case thm' of
NONE => Seq.empty
| SOME thm'' => (EqSubst.eqsubst_tac ctxt [1] [thm''] i
THEN sturm_card_eq_instantiate_tac ctxt i) thm
end;
fun find_sturm_prop_thm ctxt prop =
let val thy = Proof_Context.theory_of ctxt
fun matches thm =
case Thm.concl_of thm of
Const (@{const_name Trueprop}, _) $ (Const (@{const_name HOL.eq}, _) $ prop' $ _)
=> Pattern.matches thy (prop',prop)
| _ =>
let val _ = warning ("Invalid theorem in " ^
"sturm_prop_substs: \n" ^ Pretty.string_of (
Syntax.pretty_term ctxt (Thm.concl_of thm)));
in false
end
val thm = find_first matches @{thms sturm_prop_substs};
in
thm
end;
fun sturm_prop_tac ctxt i thm =
let val prop = case Thm.prems_of thm of p :: _ => p | _ => Thm.concl_of thm
val prop = case prop of Const (@{const_name Pure.prop}, _) $ prop => prop
| _ => prop
val prop = case prop of Const (@{const_name Pure.conjunction}, _) $
(Const (@{const_name Pure.term}, _) $ _) $ prop => prop
| _ => prop
val prop = case prop of Const (@{const_name Trueprop}, _) $ prop => prop
| _ => prop
val thm' = find_sturm_prop_thm ctxt prop
in case thm' of
NONE => Seq.empty
| SOME thm' => EqSubst.eqsubst_tac ctxt [1] [thm'] i thm
end;
fun sturm_main_tac ctxt keep_goal i thm =
let val prop = case Thm.prems_of thm of p :: _ => p | _ => Thm.concl_of thm
val prop = case prop of Const (@{const_name Pure.prop}, _) $ prop => prop
| _ => prop
val prop = case prop of Const (@{const_name Pure.conjunction}, _) $
(Const (@{const_name Pure.term}, _) $ _) $ prop => prop
| _ => prop
val tac = case prop of
Const (@{const_name Trueprop}, _) $
(Const (@{const_name HOL.eq}, _) $
(Const (@{const_name Finite_Set.card}, _) $ _) $ _)
=> sturm_card_eq_tac
| _ => sturm_prop_tac;
in ((tac ctxt i
THEN CONVERSION (sturm_conv ctxt) i
THEN resolve_tac ctxt @{thms TrueI} i
) ORELSE (if keep_goal then all_tac else no_tac)) thm
end;
fun convert_meta_spec_tac ctxt = SUBGOAL (fn (goal, i) =>
let val frees = Term.add_frees goal []
in case frees of
[_] =>
let
val goal' = Logic.close_form goal
val rule = Goal.prove ctxt [] [] (Logic.mk_implies (goal', goal)) (fn _ =>
dresolve_tac ctxt @{thms sturm_meta_spec} i THEN assume_tac ctxt i)
in resolve_tac ctxt [rule] i end
| _ => no_tac
end)
fun sturm_tac ctxt keep_goal = SELECT_GOAL
(prune_params_tac ctxt
THEN TRY (Object_Logic.full_atomize_tac ctxt 1)
THEN TRY (EqSubst.eqsubst_tac ctxt [1] @{thms sturm_imp_conv} 1)
THEN TRY (convert_meta_spec_tac ctxt 1)
THEN TRY (Object_Logic.full_atomize_tac ctxt 1)
THEN sturm_preprocess_tac ctxt 1
THEN sturm_main_tac ctxt keep_goal 1)
end;