Unable to apply rule · Beginner Questions

Hi I was doing Exercise 12.8 from Concrete Semantics. And I get stuck because I think i should be able to apply a rule but isablle fails to apply proof method

theory Ch12
  imports "HOL-IMP.Hoare_Examples"

begin


lemma NoPost: "⊢ {P} c {λs. True}"
proof (induction c arbitrary: P)
  case SKIP
  then show ?case
   apply (rule strengthen_pre[of P  "λs. True"])
       apply simp
    apply (rule Skip)
    done
next
  case (Assign x1 x2)
  then show ?case
     apply(rule Assign')
    apply simp
    done
next
  case (Seq c1 c2)
  then show ?case
    apply(rule Hoare.Seq)
    done
next
  case (If x1 c1 c2)
  then show ?case
    apply(rule Hoare.If)
    done
next
  case (While b c )
  thm  strengthen_pre[of P "λs. True" "(WHILE b DO c)" "λs. True"]
  thus ?case
    apply (rule strengthen_pre[of P "λs. True" "(WHILE b DO c)" "λs. True"])
    (*using conseq by metis*)
qed

it occurs in the while case. I successfully apply the same rule earlier in the Skip Case and when I use thm to view the rule with arguments I supply I get
∀s. P s ⟶ True ⟹ ⊢ {λs. True} WHILE b DO c {λs. True} ⟹ ⊢ {P} WHILE b DO c {λs. True}
To me this looks like I should be able to get two new subgoals which are the premises of the rule

Maximilian Schäffeler (May 04 2026 at 08:38):

If you change thus to show, rule application works. The rule method expects chained facts to match the premises of the rule to be applied. This is also discussed here: https://stackoverflow.com/questions/67704281/fragile-rule-application-in-isabelle.

Stream: Beginner Questions

Topic: Unable to apply rule

sadra (May 04 2026 at 06:45):

Maximilian Schäffeler (May 04 2026 at 08:38):