[isabelle] hammering away multiple easy subgoals



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



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.