Индукция по рекурсивной функции с завихрением

Question

Я пытаюсь доказать теорему, что если n > 0, то g n b = True (см. Ниже). Это так, потому что g (Suc n) b только звонит g 0 True. К сожалению, у меня нет такого факта в моей индукции, когда я пытаюсь доказать g 0 b. Как я могу закончить доказательство (что мне нужно заменить sorry)?

fun g :: "nat ⇒ bool ⇒ bool" where 
    "g (Suc n) b = g n True" | 
    "g 0 b = b" 

theorem 
    fixes n::nat and b::bool 
    assumes "n > 0" 
    shows "g n b" 
proof (induct n b rule: g.induct) 
    fix n 
    fix b 
    assume "g n True" 
    thus "g (Suc n) b" by (metis g.simps(1)) 
next 
    fix b 
    show "g 0 b" sorry 
qed 

Answer 1

Вы забыли использовать это предположение n > 0 в своей индукции.

Е.Г., вы можете написать

theorem 
    fixes n::nat and b::bool 
    assumes "n > 0" 
    shows "g n b" 
using assms (* this is important *) 
proof (induct n b rule: g.induct) 
    case (1 n b) 
    thus ?case by (cases n) auto 
next 
    case (2 b) 
    thus ?case by auto 
qed 

В качестве альтернативы вы можете сразу же начать теорему как этот и сократить его дальше:

theorem "n > 0 ==> g n b" 
proof (induct n b rule: g.induct) 
    case (1 n b) 
    thus ?case by (cases n) auto 
qed auto