Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] hammering away multiple easy subgoals

view this post on Zulip Email Gateway (Aug 22 2022 at 16:47):

From: "Nagashima, Yutaka" <Yutaka.Nagashima@uibk.ac.at>
Hi Peter,

With PSL in the AFP [1], one can keep hammering away easy sub-goals while deferring difficult sub-goals by defining a strategy, "JackHammer", as following:

===
theory Test
imports "PSL/PSL"
begin

definition "my_true ≡ True"
definition "my_true2 ≡ True"

strategy JackHammer = RepeatN (Ors [Hammer, Defer])

lemma "my_true" "my_true2" "False" "my_true"
apply -
find_proof JackHammer
(* This should suggest
apply ( simp add : my_true_def )
apply ( simp add : my_true2_def )
defer
apply ( simp add : my_true_def )
*)
oops

end
===

The drawback is this strategy is a bit slow and sequential.

Regards,
Yutaka

[1] https://www.isa-afp.org/entries/Proof_Strategy_Language.html

Last updated: Apr 26 2024 at 20:16 UTC