[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)

    apply(auto simp add: Let_def)

  done

end

 

Thank you.

 

Marcus.





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