Concrete Semantics Chapter 7 Question 1 structured Isar Proof

Question

I am trying to produce a structured Isar proof for Chapter 7 Question 1 in Concrete Semantics, but I am having trouble defining the proper assumptions and induction hypotheses for the inductive cases.

fun assigned :: "com ⇒ vname set" where
"assigned SKIP = {}" |
"assigned (Assign n e) = {n}" |
"assigned (Seq c1 c2) = (assigned c1) ∪ (assigned c2)" |
"assigned (If b c1 c2) = (assigned c1) ∪ (assigned c2)" |
"assigned (While b c) = assigned c"

The question asks for a proof of the following property, which is easily achieved with an apply script:

lemma "⟦ (c, s) ⇒ t; x ∉ assigned c ⟧ ⟹ s x = t x"
  apply (induction rule: big_step_induct)
        apply auto
  done

However, I would like to retrace the reasoning behind it and produce a structured Isar proof.

My first attempt was a simple induction. I am having trouble with the While (true) case and suspect that this is not the right approach:

lemma "⟦ (c, s) ⇒ t; x ∉ assigned c ⟧ ⟹ s x = t x"
proof (induction arbitrary: s t)
  case SKIP
  then show ?case by auto
next
  case (Assign c1 c2)
  then show ?case by auto
next
  case (Seq c1 c2)
  from Seq.prems obtain s1 where
    c1: "(c1, s) ⇒ s1 ∧ x ∉ assigned c1" and
    c2: "(c2, s1) ⇒ t ∧ x ∉ assigned c2"
    by auto
  from this moreover have "s x = s1 x" using Seq.IH(1) by auto
  ultimately have "s x = t x" using Seq.IH(2) by auto
  thus ?case by simp
next
  case (If b c1 c2)
  then show ?case 
  proof cases
    assume "bval b s"
    hence "(If b c1 c2, s) ⇒ t ⟷ (c1, s) ⇒ t" by auto
    thus ?case using If.IH If.prems by auto
  next
    assume "¬bval b s"
    hence "(If b c1 c2, s) ⇒ t ⟷ (c2, s) ⇒ t" by auto
    thus ?case using If.IH If.prems by auto 
  qed
next
  case (While b c)
  then show ?case 
  proof cases
    assume asm: "bval b s"
    from this While.prems obtain s1 where
      c: "(c, s) ⇒ s1 ∧ x ∉ assigned c" and
      c1: "(WHILE b DO c, s1) ⇒ t ∧ x ∉ assigned c"
      by auto
    from this moreover have "s x = s1 x" using While.IH by auto
    (*moreover have "s1 x = t x" using c c1 While.IH While.prems by sledgehammer*)
    show ?thesis sorry
  next
    assume asm: "¬bval b s"
    hence "(WHILE b DO c, s) ⇒ s" by auto
    thus ?case using asm While.prems by auto
  qed
qed

The next attempt was a proof by rule induction. In the inductive cases, I am having trouble identifying/defining the correct premises and induction hypotheses. I am getting the error Failed to refine any pending goal.

lemma "⟦ (c, s) ⇒ t; x ∉ assigned c ⟧ ⟹ s x = t x"
proof (induction rule: big_step_induct)
  fix s
  assume "x ∉ assigned SKIP"
  have "(SKIP, s) ⇒ s" by (simp add: Skip)
  thus "s x = s x" by simp
next
  fix s x1 a
  assume "x ∉ assigned (x1 ::= a)"
  hence "x1 ≠ x" by simp
  thus "s x = (s(x1 := aval a s)) x" by simp
next
  fix b s c1 c2 t 
  assume prems: "bval b s" "x ∉ assigned (IF b THEN c1 ELSE c2)"
  assume IH: "(c1, s) ⇒ t ⟹ x ∉ assigned c1 ⟹ s x = t x" "(c2, s) ⇒ t ⟹ x ∉ assigned c2 ⟹ s x = t x"
  have "(IF b THEN c1 ELSE c2, s) ⇒ t ⟷ (c1, s) ⇒ t" using prems by auto
  moreover have "x ∉ assigned c1" using prems by auto
  ultimately show "s x = t x"
next
  fix c1 c2 s s' t
  assume prems:"(c1;;c2, s) ⇒ t" 
           and "x ∉ assigned (c1;;c2)"
           and "(c1, s) ⇒ s'" 
           and "(c2, s') ⇒ t"
  assume IH: "x ∉ assigned c1 ⟹ s x = s' x"
         and "x ∉ assigned c2 ⟹ s' x = t x"
  have "x ∉ assigned c1" using prems by auto
  hence s': "s x = s' x" using IH by auto 
  have "x ∉ assigned c2" using prems by auto
  hence "s' x = t x" using IH by auto 
  show "s x = t x"
next
qed

What is the proper way define the assumption and induction hypotheses?

Answer 1

You should be able to use simply

proof (induction rule: big_step_induct)
qed auto

If you really want to write all the cases out explicitly, let Isabelle do it for you. Type

proof (induction rule: big_step_induct)

Then click on "proof" (which should be underlined) and Isabelle will generate the proof skeleton. Then put "auto" for each case.