Theory Eisbach_Methods
chapter "Proof Methods"
theory Eisbach_Methods
imports
Subgoal_Methods
"HOL-Eisbach.Eisbach_Tools"
Rule_By_Method
begin
section ‹Debugging methods›
method print_concl = (match conclusion in P for P ⇒ ‹print_term P›)
method_setup print_raw_goal = ‹Scan.succeed (fn ctxt => fn facts =>
(fn (ctxt, st) => (Output.writeln (Thm.string_of_thm ctxt st);
Seq.make_results (Seq.single (ctxt, st)))))›
ML ‹fun method_evaluate text ctxt facts =
NO_CONTEXT_TACTIC ctxt
(Method.evaluate_runtime text ctxt facts)›
method_setup print_headgoal =
‹Scan.succeed (fn ctxt =>
fn _ => fn (ctxt', thm) =>
((SUBGOAL (fn (t,_) =>
(Output.writeln
(Pretty.string_of (Syntax.pretty_term ctxt t)); all_tac)) 1 thm);
(Seq.make_results (Seq.single (ctxt', thm)))))›
section ‹Simple Combinators›
method_setup defer_tac = ‹Scan.succeed (fn _ => SIMPLE_METHOD (defer_tac 1))›
method_setup prefer_last = ‹Scan.succeed (fn _ => SIMPLE_METHOD (PRIMITIVE (Thm.permute_prems 0 ~1)))›
method_setup all =
‹Method.text_closure >> (fn m => fn ctxt => fn facts =>
let
fun tac i st' =
Goal.restrict i 1 st'
|> method_evaluate m ctxt facts
|> Seq.map (Goal.unrestrict i)
in SIMPLE_METHOD (ALLGOALS tac) facts end)
›
method_setup determ =
‹Method.text_closure >> (fn m => fn ctxt => fn facts =>
let
fun tac st' = method_evaluate m ctxt facts st'
in SIMPLE_METHOD (DETERM tac) facts end)
› ‹Run the given method, but only yield the first result›
ML ‹
fun require_determ (method : Method.method) facts st =
case method facts st |> Seq.filter_results |> Seq.pull of
NONE => Seq.empty
| SOME (r1, rs) =>
(case Seq.pull rs of
NONE => Seq.single r1 |> Seq.make_results
| _ => Method.fail facts st);
fun require_determ_method text ctxt =
require_determ (Method.evaluate_runtime text ctxt);
›
method_setup require_determ =
‹Method.text_closure >> require_determ_method›
‹Run the given method, but fail if it returns more than one result›
method_setup changed =
‹Method.text_closure >> (fn m => fn ctxt => fn facts =>
let
fun tac st' = method_evaluate m ctxt facts st'
in SIMPLE_METHOD (CHANGED tac) facts end)
›
method_setup timeit =
‹Method.text_closure >> (fn m => fn ctxt => fn facts =>
let
fun timed_tac st seq = Seq.make (fn () => Option.map (apsnd (timed_tac st))
(timeit (fn () => (Seq.pull seq))));
fun tac st' =
timed_tac st' (method_evaluate m ctxt facts st');
in SIMPLE_METHOD tac [] end)
›
method_setup timeout =
‹Scan.lift Parse.int -- Method.text_closure >> (fn (i,m) => fn ctxt => fn facts =>
let
fun str_of_goal th = Pretty.string_of (Goal_Display.pretty_goal ctxt th);
fun limit st f x = Timeout.apply (Time.fromSeconds i) f x
handle Timeout.TIMEOUT _ => error ("Method timed out:\n" ^ (str_of_goal st));
fun timed_tac st seq = Seq.make (limit st (fn () => Option.map (apsnd (timed_tac st))
(Seq.pull seq)));
fun tac st' =
timed_tac st' (method_evaluate m ctxt facts st');
in SIMPLE_METHOD tac [] end)
›
method repeat_new methods m = (m ; (repeat_new ‹m›)?)
text ‹The following @{text fails} and @{text succeeds} methods protect the goal from the effect
of a method, instead simply determining whether or not it can be applied to the current goal.
The @{text fails} method inverts success, only succeeding if the given method would fail.›
method_setup fails =
‹Method.text_closure >> (fn m => fn ctxt => fn facts =>
let
fun fail_tac st' =
(case Seq.pull (method_evaluate m ctxt facts st') of
SOME _ => Seq.empty
| NONE => Seq.single st')
in SIMPLE_METHOD fail_tac facts end)
›
method_setup succeeds =
‹Method.text_closure >> (fn m => fn ctxt => fn facts =>
let
fun can_tac st' =
(case Seq.pull (method_evaluate m ctxt facts st') of
SOME (st'',_) => Seq.single st'
| NONE => Seq.empty)
in SIMPLE_METHOD can_tac facts end)
›
text ‹This method wraps up the "focus" mechanic of match without actually doing any matching.
We need to consider whether or not there are any assumptions in the goal,
as premise matching fails if there are none.
If the @{text fails} method is removed here, then backtracking will produce
a set of invalid results, where only the conclusion is focused despite
the presence of subgoal premises.
›
method focus_concl methods m =
((fails ‹erule thin_rl›, match conclusion in _ ⇒ ‹m›)
| match premises (local) in H:_ (multi) ⇒ ‹m›)
text ‹
@{text repeat} applies a method a specific number of times,
like a bounded version of the '+' combinator.
usage:
apply (repeat n ‹text›)
- Applies the method ‹text› to the current proof state n times.
- Fails if ‹text› can't be applied n times.
›
ML ‹
fun repeat_tac count tactic =
if count = 0
then all_tac
else tactic THEN (repeat_tac (count - 1) tactic)
›
method_setup repeat = ‹
Scan.lift Parse.nat -- Method.text_closure >> (fn (count, text) => fn ctxt => fn facts =>
let val tactic = method_evaluate text ctxt facts
in SIMPLE_METHOD (repeat_tac count tactic) facts end)
›
notepad begin
fix A B C
assume assms: A B C
text ‹repeat: simple repeated application.›
have "A ∧ B ∧ C ∧ True"
text ‹repeat: fails if method can't be applied the specified number of times.›
apply (fails ‹repeat 4 ‹rule conjI, rule assms››)
apply (repeat 3 ‹rule conjI, rule assms›)
by (rule TrueI)
text ‹repeat: application with subgoals.›
have "A ∧ A" "B ∧ B" "C ∧ C"
apply -
text ‹We have three subgoals. This @{text repeat} call consumes two of them.›
apply (repeat 2 ‹rule conjI, (rule assms)+›)
text ‹One subgoal remaining...›
apply (rule conjI, (rule assms)+)
done
end
text ‹
Literally a copy of the parser for @{method subgoal_tac} composed with an analogue of
@{command prefer}.
Useful if you find yourself introducing many new facts via @{method subgoal_tac}, but prefer to prove
them immediately rather than after they're used.
›
setup ‹
Method.setup \<^binding>‹prop_tac›
(Args.goal_spec -- Scan.lift (Scan.repeat1 Parse.embedded_inner_syntax -- Parse.for_fixes) >>
(fn (quant, (props, fixes)) => fn ctxt =>
(SIMPLE_METHOD'' quant
(EVERY' (map (fn prop => Rule_Insts.subgoal_tac ctxt prop fixes) props)
THEN'
(K (prefer_tac 2))))))
"insert prop (dynamic instantiation), introducing prop subgoal first"
›
notepad begin {
fix xs
assume assms: "list_all even (xs :: nat list)"
from assms have "even (sum_list xs)"
apply (induct xs)
apply simp
text ‹Inserts the desired proposition as the current subgoal.›
apply (prop_tac "list_all even xs")
subgoal by simp
text ‹
The prop @{term "list_all even xs"} is now available as an assumption.
Let's add another one.›
apply (prop_tac "even (sum_list xs)")
subgoal by simp
text ‹Now that we've proven our introduced props, use them!›
apply clarsimp
done
}
end
section ‹Advanced combinators›
subsection ‹Protecting goal elements (assumptions or conclusion) from methods›
context
begin
private definition "protect_concl x ≡ ¬ x"
private definition "protect_false ≡ False"
private lemma protect_start: "(protect_concl P ⟹ protect_false) ⟹ P"
by (simp add: protect_concl_def protect_false_def) (rule ccontr)
private lemma protect_end: "protect_concl P ⟹ P ⟹ protect_false"
by (simp add: protect_concl_def protect_false_def)
method only_asm methods m =
(match premises in H[thin]:_ (multi,cut) ⇒
‹rule protect_start,
match premises in H'[thin]:"protect_concl _" ⇒
‹insert H,m;rule protect_end[OF H']››)
method only_concl methods m = (focus_concl ‹m›)
end
notepad begin
fix D C
assume DC:"D ⟹ C"
have "D ∧ D ⟹ C ∧ C"
apply (only_asm ‹simp›)
apply (only_concl ‹simp add: DC›)
by (rule DC)
end
subsection ‹Safe subgoal folding (avoids expanding meta-conjuncts)›
text ‹Isabelle's goal mechanism wants to aggressively expand meta-conjunctions if they
are the top-level connective. This means that @{text fold_subgoals} will immediately
be unfolded if there are no common assumptions to lift over.
To avoid this we simply wrap conjunction inside of conjunction' to hide it
from the usual facilities.›
context begin
definition
conjunction' :: "prop ⇒ prop ⇒ prop" (infixr "&^&" 2) where
"conjunction' A B ≡ (PROP A &&& PROP B)"
text ‹In general the context antiquotation does not work in method definitions.
Here it is fine because @{ML Conv.top_sweep_conv} is just over-specified to need a Proof.context
when anything would do.›
method safe_meta_conjuncts =
raw_tactic
‹REPEAT_DETERM
(CHANGED_PROP
(PRIMITIVE
(Conv.gconv_rule ((Conv.top_sweep_conv (K (Conv.rewr_conv @{thm conjunction'_def[symmetric]})) @{context})) 1)))›
method safe_fold_subgoals = (fold_subgoals (prefix), safe_meta_conjuncts)
lemma atomize_conj' [atomize]: "(A &^& B) == Trueprop (A & B)"
by (simp add: conjunction'_def, rule atomize_conj)
lemma context_conjunction'I:
"PROP P ⟹ (PROP P ⟹ PROP Q) ⟹ PROP P &^& PROP Q"
apply (simp add: conjunction'_def)
apply (rule conjunctionI)
apply assumption
apply (erule meta_mp)
apply assumption
done
lemma conjunction'I:
"PROP P ⟹ PROP Q ⟹ PROP P &^& PROP Q"
by (rule context_conjunction'I; simp)
lemma conjunction'E:
assumes PQ: "PROP P &^& PROP Q"
assumes PQR: "PROP P ⟹ PROP Q ⟹ PROP R"
shows
"PROP R"
apply (rule PQR)
apply (rule PQ[simplified conjunction'_def, THEN conjunctionD1])
by (rule PQ[simplified conjunction'_def, THEN conjunctionD2])
end
notepad begin
fix D C E
assume DC: "D ∧ C"
have "D" "C ∧ C"
apply -
apply (safe_fold_subgoals, simp, atomize (full))
apply (rule DC)
done
end
section ‹Utility methods›
subsection ‹Finding a goal based on successful application of a method›
method_setup find_goal =
‹Method.text_closure >> (fn m => fn ctxt => fn facts =>
let
fun prefer_first i = SELECT_GOAL
(fn st' =>
(case Seq.pull (method_evaluate m ctxt facts st') of
SOME (st'',_) => Seq.single st''
| NONE => Seq.empty)) i THEN prefer_tac i
in SIMPLE_METHOD (FIRSTGOAL prefer_first) facts end)›
text ‹Ensure that the proof state is in a certain case of a case distinction:›
method in_case for x = match premises in "t = x" for t ⇒ succeed
text ‹Focus on a case in a case distinction:›
method find_case for x = find_goal ‹in_case x›
notepad begin
fix A B
assume A: "A" and B: "B"
have "A" "A" "B"
apply (find_goal ‹match conclusion in B ⇒ ‹-››)
apply (rule B)
by (rule A)+
have "A ∧ A" "A ∧ A" "B"
apply (find_goal ‹fails ‹simp››)
apply (rule B)
by (simp add: A)+
have "B" "A" "A ∧ A"
apply (find_goal ‹succeeds ‹simp››)
apply (rule conjI)
by (rule A B)+
fix x::'a and S :: "nat ⇒ 'a" and T R
have
"x = T ⟹ A"
"x = S 10 ⟹ B"
"x = R ⟹ B"
apply -
apply (find_case "S ?n")
apply (fails ‹in_case R›)
apply (in_case "S ?n")
by (rule A B)+
end
subsection ‹Remove redundant subgoals›
text ‹Tries to solve subgoals by assuming the others and then using the given method.
Backtracks over all possible re-orderings of the subgoals.›
context begin
definition "protect (PROP P) ≡ P"
lemma protectE: "PROP protect P ⟹ (PROP P ⟹ PROP R) ⟹ PROP R" by (simp add: protect_def)
private lemmas protect_thin = thin_rl[where V="PROP protect P" for P]
private lemma context_conjunction'I_protected:
assumes P: "PROP P"
assumes PQ: "PROP protect (PROP P) ⟹ PROP Q"
shows
"PROP P &^& PROP Q"
apply (simp add: conjunction'_def)
apply (rule P)
apply (rule PQ)
apply (simp add: protect_def)
by (rule P)
private lemma conjunction'_sym: "PROP P &^& PROP Q ⟹ PROP Q &^& PROP P"
apply (simp add: conjunction'_def)
apply (frule conjunctionD1)
apply (drule conjunctionD2)
apply (rule conjunctionI)
by assumption+
private lemmas context_conjuncts'I =
context_conjunction'I_protected
context_conjunction'I_protected[THEN conjunction'_sym]
method distinct_subgoals_strong methods m =
(safe_fold_subgoals,
(intro context_conjuncts'I;
(((elim protectE conjunction'E)?, solves ‹m›)
| (elim protect_thin)?)))?
end
method forward_solve methods fwd m =
(fwd, prefer_last, fold_subgoals, safe_meta_conjuncts, rule conjunction'I,
defer_tac, ((intro conjunction'I)?; solves ‹m›))[1]
method frule_solve methods m uses rule = (forward_solve ‹frule rule› ‹m›)
method drule_solve methods m uses rule = (forward_solve ‹drule rule› ‹m›)
notepad begin
{
fix A B C D E
assume ABCD: "A ⟹ B ⟹ C ⟹ D"
assume ACD: "A ⟹ C ⟹ D"
assume DE: "D ⟹ E"
assume B C
have "A ⟹ D"
apply (frule_solve ‹simp add: ‹B› ‹C›› rule: ABCD)
apply (drule_solve ‹simp add: ‹B› ‹C›› rule: ACD)
apply (match premises in A ⇒ ‹fail› ¦ _ ⇒ ‹-›)
apply assumption
done
}
end
notepad begin
{
fix A B C
assume A: "A"
have "A" "B ⟹ A"
apply -
apply (distinct_subgoals_strong ‹assumption›)
by (rule A)
have "B ⟹ A" "A"
by (distinct_subgoals_strong ‹assumption›, rule A)
}
{
fix A B C
assume B: "B"
assume BC: "B ⟹ C" "B ⟹ A"
have "A" "B ⟶ (A ∧ C)" "B"
apply (distinct_subgoals_strong ‹simp›, rule B)
by (simp add: BC)
}
end
section ‹Attribute methods (for use with ‹rule_by_method› attributes)›
method prove_prop_raw for P :: "prop" methods m =
(erule thin_rl, rule revcut_rl[of "PROP P"],
solves ‹match conclusion in _ ⇒ ‹m››)
method prove_prop for P :: "prop" = (prove_prop_raw "PROP P" ‹auto›)
experiment begin
lemma assumes A[simp]:A shows A by (rule [[@‹prove_prop A›]])
end
section ‹Shortcuts for @{method prove_prop}. ›
text ‹Note these are less efficient than using the raw syntax because
the facts are re-proven every time.›
method ruleP for P :: "prop" = (catch ‹rule [[@‹prove_prop "PROP P"›]]› ‹fail›)
method insertP for P :: "prop" = (catch ‹insert [[@‹prove_prop "PROP P"›]]› ‹fail›)[1]
experiment begin
lemma assumes A[simp]:A shows A by (ruleP False | ruleP A)
lemma assumes A:A shows A by (ruleP "⋀P. P ⟹ P ⟹ P", rule A, rule A)
end
context begin
private definition "bool_protect (b::bool) ≡ b"
lemma bool_protectD:
"bool_protect P ⟹ P"
unfolding bool_protect_def by simp
lemma bool_protectI:
"P ⟹ bool_protect P"
unfolding bool_protect_def by simp
text ‹
When you want to apply a rule/tactic to transform a potentially complex goal into another
one manually, but want to indicate that any fresh emerging goals are solved by a more
brutal method.
E.g. ‹apply (solves_emerging frule x=... in my_rule›‹fastforce simp: ... intro!: ... ›
›
method solves_emerging methods m1 m2 = (rule bool_protectD, (m1 ; (rule bool_protectI | (m2; fail))))
end
end