# Theory SemanticsWellFormed

```section ‹Semantic well-formedness of While CFG›

theory SemanticsWellFormed
imports WellFormed WEquivalence "../Basic/SemanticsCFG"
begin

subsection ‹Instatiation of the ‹CFG_semantics_wf› locale›

fun labels_nodes :: "cmd ⇒ w_node ⇒ cmd ⇒ bool" where
"labels_nodes prog (_ l _) c     = labels prog l c"
| "labels_nodes prog (_Entry_) c = False"
| "labels_nodes prog (_Exit_) c  = False"

interpretation While_semantics_CFG_wf: CFG_semantics_wf
sourcenode targetnode kind "valid_edge prog" Entry reds "labels_nodes prog"
for prog
proof(unfold_locales)
fix n c s c' s' n'
assume "labels_nodes prog n c" and "⟨c,s⟩ →* ⟨c',s'⟩"
then obtain l l' where [simp]:"n = (_ l _)" and "prog ⊢ ⟨c,s,l⟩ ↝* ⟨c',s',l'⟩"
and "labels prog l' c'" by(cases n,auto dest:reds_steps)
from ‹labels prog l' c'› have "l' < #:prog" by(rule label_less_num_inner_nodes)
from ‹prog ⊢ ⟨c,s,l⟩ ↝* ⟨c',s',l'⟩›
have "∃as. CFG.path sourcenode targetnode (valid_edge prog)
(_ l _) as (_ l' _) ∧
transfers (CFG.kinds kind as) s = s' ∧ preds (CFG.kinds kind as) s"
proof(induct rule:converse_rtranclp_induct3)
case refl
from ‹l' < #:prog› have "valid_node prog (_ l' _)"
by(fastforce dest:less_num_nodes_edge simp:valid_node_def valid_edge_def)
hence "CFG.valid_node sourcenode targetnode (valid_edge prog) (_ l' _)"
hence "CFG.path sourcenode targetnode (valid_edge prog) (_ l' _) [] (_ l' _)"
by(rule While_CFG.empty_path)
thus ?case by(auto simp:While_CFG.kinds_def)
next
case (step c s l c'' s'' l'')
from ‹(λ(c, s, l) (c', s', l').
prog ⊢ ⟨c,s,l⟩ ↝ ⟨c',s',l'⟩) (c,s,l) (c'',s'',l'')›
have "prog ⊢ ⟨c,s,l⟩ ↝ ⟨c'',s'',l''⟩" by simp
from ‹∃as. CFG.path sourcenode targetnode (valid_edge prog)
(_ l'' _) as (_ l' _) ∧
transfers (CFG.kinds kind as) s'' = s' ∧
preds (CFG.kinds kind as) s''›
obtain as where "CFG.path sourcenode targetnode (valid_edge prog)
(_ l'' _) as (_ l' _)"
and "transfers (CFG.kinds kind as) s'' = s'"
and "preds (CFG.kinds kind as) s''" by auto
from ‹prog ⊢ ⟨c,s,l⟩ ↝ ⟨c'',s'',l''⟩› obtain et
where "prog ⊢ (_ l _) -et→ (_ l'' _)"
and "transfer et s = s''" and "pred et s"
by(erule step_WCFG_edge)
from ‹prog ⊢ (_ l _) -et→ (_ l'' _)›
‹CFG.path sourcenode targetnode (valid_edge prog) (_ l'' _) as (_ l' _)›
have "CFG.path sourcenode targetnode (valid_edge prog)
(_ l _) (((_ l _),et,(_ l'' _))#as) (_ l' _)"
by(fastforce intro:While_CFG.Cons_path simp:valid_edge_def)
moreover
from ‹transfers (CFG.kinds kind as) s'' = s'› ‹transfer et s = s''›
have "transfers (CFG.kinds kind (((_ l _),et,(_ l'' _))#as)) s = s'"
moreover from ‹preds (CFG.kinds kind as) s''› ‹pred et s› ‹transfer et s = s''›
have "preds (CFG.kinds kind (((_ l _),et,(_ l'' _))#as)) s"