isabelle - Local assumptions in "state" mode

Question

Frequently, when proving a statement in "prove" mode, I find myself in need of some intermediate statements that are not yet stated nor proved. To state them, I usually make use of the subgoal command, followed by proof- to change to "state" mode. In the process, however, all of the local assumptions are removed. A typical example could look like this

lemma "0 < n ? ((2::nat)^n < 3^n)"
  apply(auto)
  subgoal
  proof-
    have "0<n" sorry (* here I would like to refer to the assumption from the subgoal *)
    then show ?thesis sorry
  qed
  subgoal sorry
  done

I am aware that I could state the assumptions using assume explicitly. However, this becomes quickly rather tedious when multiple assumptions are involved. Is there an easier way to simply refer to all of the assumptions? Alternatively, is there a good way to implement statements with short proofs directly in "prove" mode?

question from:https://stackoverflow.com/questions/65598494/local-assumptions-in-state-mode

Answer 1

There is the syntax subgoal premises prems to bind the premises of the subgoal to the name prems (or any other name – but prems is a sensible default):

lemma "0 < n ? ((2::nat)^n < 3^n)"
  apply(auto)
  subgoal premises prems
  proof -
    thm prems

There is also a method called goal_cases that automatically gives names to all the current subgoals – I find it very useful. If subgoal premises did not exist, you could do this instead:

lemma "0 < n ? ((2::nat)^n < 3^n)"
  apply(auto)
  subgoal
  proof goal_cases
    case 1

By the way, looking at your example, it is considered a bad idea to do anything after auto that depends on the exact form of the proof state, such as metis calls or Isar proofs. auto is fairly brutal and might behave differently in the next Isabelle release so that such proofs break. I recommend doing a nice structured Isar proof here.

Also note that your theorem is a direct consequence of power_strict_mono and power_less_imp_less_base and can be proven in a single line:

lemma "0 < n ? ((2::nat)^n < 3^n)"
  by (auto intro: Nat.gr0I power_strict_mono)`