Email Gateway (Aug 18 2022 at 12:35): Email Gateway (Aug 18 2022 at 12:35):From: Eng Siong Ng <eng@nps.edu>
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.
Last updated: May 03 2024 at 12:27 UTC