# [isabelle] Theorem proving

```Hi,

I am a beginner in theorem prover, can someone help me in proving the
following:

theory simple

imports Base

begin

types Input = "int list \<times> nat"

types State = "Input \<times> nat"

consts property_p :: "State \<Rightarrow> bool"

defs property_p_def [simp]:

"property_p s \<equiv> (if snd (fst s) > 1 then snd s > 0 else True)"

consts transition :: "State \<Rightarrow> State"

defs transition_def [simp]:

"transition s \<equiv> ((fst (fst s),Suc (snd (fst s))),Suc (snd s))"

consts evaluate :: "nat \<Rightarrow> State \<times> bool"

theorem evaluate_Obligation_subsort:

"\<lbrakk>\<not> (n = 0)\<rbrakk> \<Longrightarrow> 0 \<le> int n - 1"

apply(auto)

done

primrec

"evaluate 0 = ((([1,2,3],1),0),True)"

"evaluate (Suc n)

= (let s = evaluate n

in

(if snd s then

(transition (fst s),property_p (fst s))

else

(transition (fst s),snd s)))"

theorem simple [simp]:

"snd (evaluate n)"

apply(induct_tac n)

done

end

Thank you.

Marcus.

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.