0 
datatype alpha = a | b

inductive S :: "alpha list ⇒ bool" where
 empty [simp]: "S []" | 
 step1 [simp]: "S w ⟹ S (a # w @ [b])" |
 step2 [simp]: "⟦S w1; S w2⟧ ⟹ S (w1 @ w2)"

fun balanced :: "nat ⇒ alpha list ⇒ bool" where
 "balanced 0 [] = True "|
 "balanced n (a # w) = balanced (Suc n) w"  |
 "balanced (Suc n) (b # w) = balanced n w " |
 "balanced n w = False"

该函数balanced被定义为balanced n w = S (replicate n a @ w) wherereplicate n a返回[a,a,...,a]长度为 n 的列表。我必须证明balanced n w ⟹ S (replicate n a @ w)，S (replicate n a @ w) ⟹ balanced n w并且在这两方面都遇到了麻烦。

因为balanced n w ⟹ S (replicate n a @ w)我试图证明如下。

  proof (induct n w rule : balanced.induct)
    case 1
    then show ?case by auto
  next
    case (2 n w)
    then show ?case by (metis Cons_eq_appendI ex5_7.b2 replicate_Suc replicate_app_Cons_same)
  next
    case (3 n w)
    then show ?case sorry
  next
    case ("4_1" v)
    then show ?case by auto
  next
    case ("4_2" va)
    then show ?case by auto
  qed

对于第三种情况，我得到了子目标 (balanced n w ⟹ S (replicate n a @ w)) ⟹ balanced (Suc n) (b # w) ⟹ S (replicate (Suc n) a @ b # w)，即使使用 . 也未能证明它try。假设 S (x @ y) ⟹ S (x @ [a,b] @ y)会解决问题，但我也找不到证明它的方法。有没有其他方法可以证明或可以证明 S (x @ y) ⟹ S (x @ [a,b] @ y)？

因为S (replicate n a @ w) ⟹ balanced n w 我试图证明如下。

 proof (induct n w rule : balanced.induct)
   case 1
   then show ?case by simp
 next
   case (2 n w)
   then show ?case try
     by (metis Cons_eq_appendI ex5_7.b2 replicate_Suc replicate_app_Cons_same)
 next
   case (3 n w)
   then show ?case sorry 
 next
   case ("4_1" v)
   then show ?case sorry
 next
   case ("4_2" va)
   then show ?case sorry
 qed

我无法证明案例 3、4_1 和 4_2 的原因显然是因为所有 3 个子目标的假设总是错误的。例如，我为案例 4_2 得到的子目标是 S (replicate 0 a @ b # va) ⟹ balanced 0 (b # va). 因为balanced 0 (b # va)总是假的。我需要证明这S (replicate 0 a @ b # va)也总是错误的。有没有办法在不改变定义的情况下做到这一点S ？

4

0 回答 0