如何为Concrete Semantics第7章第1题定义Isar证明的假设与归纳假设？

需证明以下性质：

⟦ (c, s) ⇒ t; x ∉ assigned c ⟧ ⟹ s x = t x

其中assigned函数定义如下：

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"

使用apply脚本可快速完成证明：

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

但尝试编写结构化Isar证明时两次失败：

• 第一次采用普通归纳，无法处理While分支的条件为真的情况；
• 第二次采用规则归纳，无法正确定义前提与归纳假设，出现Failed to refine any pending goal错误。

现寻求该证明中假设与归纳假设的正确定义方式，两次尝试的代码如下：

第一次普通归纳尝试 #

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

第二次规则归纳尝试 #

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

内容的提问来源于stack exchange，提问作者david-wang-0