Theory VCG_Total_EX2

theory VCG_Total_EX2
imports Hoare_Total_EX2

theory VCG_Total_EX2
imports Hoare_Total_EX2
begin

subsection

text

text

datatype acom =
Aassign vname aexp     ( [1000, 61] 61) |
Aseq   acom acom       (  [60, 61] 60) |
Aif bexp acom acom     (  [0, 0, 61] 61) |
Awhile assn2 lvname bexp acom
(  [0, 0, 0, 61] 61)

notation com.SKIP ()

text

fun strip ::  where
|
|
|
|

text

fun pre ::  where
|
|
|
|

text

fun vc ::  where
|
|
|
|

lemma vc_sound:
proof(induction C arbitrary: Q)
case (Awhile I x b C)
show ?case
proof(simp, rule weaken_post[OF While[of I x]], goal_cases)
case 1 show ?case
using Awhile.IH[of ] Awhile.prems by (auto intro: strengthen_pre)
next
case 3 show ?case
using Awhile.prems by (simp) (metis fun_upd_triv)
qed (insert Awhile.prems, auto)
qed (auto intro: conseq Seq If simp: Skip Assign)

text

lemma pre_mono:

proof (induction C arbitrary: P P' l s)
case Aseq thus ?case by simp metis
qed simp_all

lemma vc_mono:

proof(induction C arbitrary: P P')
case Aseq thus ?case by simp (metis pre_mono)
qed simp_all

lemma vc_complete:

(is )
proof (induction rule: hoaret.induct)
case Skip
show ?case (is )
proof show  by simp qed
next
case (Assign P a x)
show ?case (is )
proof show  by simp qed
next
case (Seq P c1 Q c2 R)
from Seq.IH obtain C1 where ih1:  by blast
from Seq.IH obtain C2 where ih2:  by blast
show ?case (is )
proof
show
using ih1 ih2 by (fastforce elim!: pre_mono vc_mono)
qed
next
case (If P b c1 Q c2)
from If.IH obtain C1 where ih1:
by blast
from If.IH obtain C2 where ih2:
by blast
show ?case (is )
proof
show  using ih1 ih2 by simp
qed
next
case (While P x c b)
from While.IH obtain C where
ih:
by blast
show ?case (is )
proof
have
using ih While.hyps(2,3)
by simp (metis fun_upd_same zero_less_Suc)
thus  using ih by simp
qed
next
case conseq thus ?case by(fast elim!: pre_mono vc_mono)
qed

end