DISP	cond_df	cond{ < i:level > }( < f:f:* > ; < s:s:* > )== Cond Cond== Cond
ABS	cond	Cond == Env
ML	cond_soft	add_soft_abs ``cond``;;
DISP	hoare_df	({ < e:env-var > . < P:pre-cond:* > } < st:stmt:* > { < e:env-var > . < Q:post-cond:* > } wrt < f:f:* > ; < s:s:* > ) == { < P > } < st > { < Q > } { < P:pre-cond:* > } < st:stmt:* > { < Q:post-cond:* > }== { < P > } < st > { < Q > }
ABS	hoare	{P[e]} st {Q[e]} == p:Env P[p] st p in! StmtValue(f;s) IsNorm(st p) Q[env(st p)]
THM	hoare_wf	f:Atom . s:Spec. P,Q:Cond. st:Stmt. {P[e]} st {Q[e]}
THM	hoare_skip	f:Atom . s:Spec. P,Q:Cond. (e:Env. P[e] Q[e]) {P[e]} skip {Q[e]}
THM	env_seq	f:Atom . s:Spec. st1,st2:Stmt. p:Env. st1 p in! StmtValue(f;s) IsNorm(st1 p) st1; st2 p = st2 env(st1 p)
THM	induce_seq	f:Atom . s:Spec. p:Env. st1,st2:Stmt. st1; st2 p in! StmtValue(f;s) st1 p in! StmtValue(f;s)
THM	is_norm_seq	f:Atom . s:Spec. st1,st2:Stmt. p:Env. st1; st2 p in! StmtValue(f;s) IsNorm(st1; st2 p) IsNorm(st1 p)
THM	hoare_seq	f:Atom . s:Spec. P,Q:Cond. st1,st2:Stmt. (R:Cond. {P[en]} st1 {R en} {R en} st2 {Q[en]}) {P[en]} st1; st2 {Q[en]}
ML	hoare_seq_tac	let HoareSeq t = BLemma `hoare_seq` THENM (With t (D 0) THENL [Id; Reduce 0 THEN D 0; MemCD THEN BLemma `hoare_wf`]) ;;
THM	hoare_var_assig_int	f:Atom . s:Spec. P,Q:Cond. v:Atom. z:. (en:Env. P[en] Q[en{(v:int) - > JConst(z;int)}]) {P[en]} (v:int) := (z) {Q[en]}
THM	hoare_var_assig_var	f:Atom . s:Spec. P,Q:Cond. t:Type. v,w:Atom. (en:Env. P[en] Q[en{(v:t) - > en w t}]) {P[en]} (v:t) := (w:t) {Q[en]}
ML	hoare_tac	let Hoare = (BLemma `hoare_var_assig_int` THENM Unfold `env_update` 0 THENM Reduce 0 THENM RWH eq_atom_evalC 0 THENM Reduce 0) ORELSE (BLemma `hoare_var _assig_var` THENM Unfold `env_update` 0 THENM Reduce 0 THENM RWH eq_at om_evalC 0 THENM Reduce 0) ORELSE Id ;;
THM	and_hoare	f:Atom . s:Spec. P1,P2,Q1,Q2:Cond. st:Stmt. {P1[en]} st {Q1[en]} {P2[en]} st {Q2[en]} {P1[en] P2[en]} st {Q1[en] Q2[en]}

the other theories