Last on my list for today is a more interactive variant of print_cases.
When I currently write
lemma "n + 1 = 1 + (n::nat)"
proof(induct n)
I have
proof (state): step 1
goal (2 subgoals):
1. 0 + 1 = 1 + 0
2. ⋀n. n + 1 = 1 + n ⟹ Suc n + 1 = 1 + Suc n
and with
print_cases
it prints
cases:
0:
let "?case" = "0 + 1 = 1 + 0"
Suc:
fix n_
let "?case" = "Suc n_ + 1 = 1 + Suc n_"
assume Suc.hyps: "n_ + 1 = 1 + n_" and Suc.prems:
What I am missing is a combination of both that is ready to be used as
the structure of an Isar proof, e.g. either completely explicit:
show "0 + 1 = 1 + 0"
sorry
next
fix n
assume "n + 1 = 1 + (n::nat)"
show "Suc n + 1 = 1 + Suc n"
sorry
qed
or, depending on personal preference and number and complexity of the
hypotheses, using the provided case names (and using "case goal1..." if
there are no case names):
case 0
show ?case
sorry
next
case (Suc n)
show ?case
sorry
qed
From there I guess it would be a small step to allow the user to insert
the output of this command (say print_isar_structure) into the proof
document with one click, similar to how sledgehammer works.