Theory Form

subsection ‹Formedness Properties›

theory Form
imports
  Semantics.TreeToGraph
begin

definition wf_start where
  "wf_start g = (0 ∈ ids g ∧
    is_StartNode (kind g 0))"

definition wf_closed where
  "wf_closed g = 
    (∀ n ∈ ids g .
      inputs g n ⊆ ids g ∧
      succ g n ⊆ ids g ∧
      kind g n ≠ NoNode)"

definition wf_phis where
  "wf_phis g = 
    (∀ n ∈ ids g.
      is_PhiNode (kind g n) ⟶
      length (ir_values (kind g n))
       = length (ir_ends 
           (kind g (ir_merge (kind g n)))))"

definition wf_ends where
  "wf_ends g = 
    (∀ n ∈ ids g .
      is_AbstractEndNode (kind g n) ⟶
      card (usages g n) > 0)"

fun wf_graph :: "IRGraph ⇒ bool" where
  "wf_graph g = (wf_start g ∧ wf_closed g ∧ wf_phis g ∧ wf_ends g)"

lemmas wf_folds =
  wf_graph.simps
  wf_start_def
  wf_closed_def
  wf_phis_def
  wf_ends_def

fun wf_stamps :: "IRGraph ⇒ bool" where
  "wf_stamps g = (∀ n ∈ ids g . 
    (∀ v m p e . (g ⊢ n ≃ e) ∧ ([m, p] ⊢ e ↦ v) ⟶ valid_value v (stamp_expr e)))"

fun wf_stamp :: "IRGraph ⇒ (ID ⇒ Stamp) ⇒ bool" where
  "wf_stamp g s = (∀ n ∈ ids g . 
    (∀ v m p e . (g ⊢ n ≃ e) ∧ ([m, p] ⊢ e ↦ v) ⟶ valid_value v (s n)))"

lemma wf_empty: "wf_graph start_end_graph"
  unfolding wf_folds by (simp add: start_end_graph_def)

lemma wf_eg2_sq: "wf_graph eg2_sq"
  unfolding wf_folds by (simp add: eg2_sq_def)

fun wf_logic_node_inputs :: "IRGraph ⇒ ID ⇒ bool" where 
"wf_logic_node_inputs g n =
  (∀ inp ∈ set (inputs_of (kind g n)) . (∀ v m p . ([g, m, p] ⊢ inp ↦ v) ⟶ wf_bool v))"

fun wf_values :: "IRGraph ⇒ bool" where
  "wf_values g = (∀ n ∈ ids g .
    (∀ v m p . ([g, m, p] ⊢ n ↦ v) ⟶ 
       (is_LogicNode (kind g n) ⟶ 
        wf_bool v ∧ wf_logic_node_inputs g n)))"

end