Isabelle中归纳谓词S与balanced函数双向等价性证明求助

第一个方向：balanced n w ⟹ S (replicate n a @ w) 证明 #

你猜测的引理 S (x @ y) ⟹ S (x @ [a,b] @ y) 完全可证，该引理对应合法括号串的基础性质：任意合法括号串的任意位置插入一对匹配的a,b括号，得到的仍然是合法括号串。
你可以先证明该辅助引理：

lemma insert_matched: "S (u @ v) ⟹ S (u @ [a,b] @ v)"
proof (induct rule: S.induct)
  case empty
  then show ?case by (simp add: S.step1 S.empty)
next
  case (step1 w)
  then show ?case
    by (metis S.step1 S.step2 append.assoc append_Cons append_Nil append_eq_Cons_conv)
next
  case (step2 w1 w2)
  then show ?case
    by (smt S.step2 append.assoc append_eq_append_conv)
qed

回到第三个case，首先化简目标：
replicate (Suc n) a @ (b # w) = replicate n a @ [a] @ [b] @ w = replicate n a @ [a,b] @ w
根据case3的前提，balanced (Suc n) (b # w) 由balanced的定义等价于balanced n w，结合归纳假设可以得到S (replicate n a @ w)，直接代入上面的辅助引理，令u = replicate n a，v = w，即可得S (replicate n a @ [a,b] @ w)，正好匹配目标，这个case就证完了。

第二个方向：S (replicate n a @ w) ⟹ balanced n w 证明 #

你这里的核心问题是选错了归纳规则：要证明S成立的前提下的性质，应该使用S的归纳规则，而不是balanced的归纳规则，自然就不会出现你遇到的前提恒假的问题。
正确的归纳方式是对S的推导过程做归纳，泛化n和w：

proof (induct "replicate n a @ w" arbitrary: n w rule: S.induct)
  case empty
  then have "replicate n a @ w = []" by simp
  hence "n=0" "w=[]" by auto
  then show ?case by simp
next
  case (step1 x)
  then have "replicate n a @ w = a # x @ [b]" by simp
  (* 分情况拆分append，结合balanced的定义即可推导 *)
next
  case (step2 x y)
  then have "replicate n a @ w = x @ y" by simp
  (* 拆分n和w，结合两次IH即可推导 *)
qed

如果你不想换归纳规则，要证明你遇到的假前提子目标，只需要先证明S的两个基础性质，就可以直接推出前提恒假：

1. 计数相等性质：S w ⟹ count_list w a = count_list w b，直接对S归纳即可证明
2. 前缀性质：S w ⟹ ∀k ≤ length w. count_list (take k w) a ≥ count_list (take k w) b，同样对S归纳可证
   对于你提到的case4_2子目标，前提是S (b # va)，取前缀长度1，count_list (take 1 (b#va)) a = 0，count_list (take 1 (b#va)) b =1，违反前缀性质，因此前提恒假，蕴含式自然成立。其他假前提case都可以用这两个性质证明前提不成立。

内容的提问来源于stack exchange，提问作者一十一