Theory SE_Graph_Pre

theory SE_Graph_Pre
  imports
    "LTS.IA_Instance"
begin

(*
  p = position,
  pv = program variable
  lv = logical variable
   n = node identifier
*)

datatype ('p,'pv,'lv) abstract_state =
  As (pos : 'p)
     (stack : "'pv ⇀ 'lv")
     (kb : "'lv IA.formula")

type_synonym ('n,'v) as_config = "'n × ('v × IA.ty ⇒ IA.val)"

inductive as_as_step where
  "as_as_step as⇩1 as⇩2 σ τ μ"
  if
  "IA.assignment v" "IA.assignment v'" "IA.assignment σ" "IA.assignment τ"
  "IA.satisfies v (kb as⇩1)" "IA.satisfies v' (kb as⇩2)"
  "∀ n lv. stack as⇩1 n = Some lv ⟶ σ (n,IA.IntT) = v (lv,IA.IntT)"
  "∀ n lv. stack as⇩2 n = Some lv ⟶ τ (n,IA.IntT) = v' (lv,IA.IntT)"
  "∀ lv ty. v (μ lv,ty) = v' (lv,ty)"

locale graph' =
  fixes as_of_node :: "'n ⇒ ('pos,'pv,'lv::linorder) abstract_state"
        and renaming_of_edge :: "('n × 'n) ⇒ ('lv ⇒ 'lv)"
        and edges ::  "('n × 'n) set"
begin

definition nodes where "nodes = fst ` edges ∪ snd ` edges"

inductive_set as_step :: "(('n,'pv) as_config × ('n,'pv) as_config) set" where
   "{n⇩1,n⇩2} ⊆ nodes ⟹
   (n⇩1, n⇩2) ∈ edges ⟹
   IA.assignment v ⟹
   IA.assignment v' ⟹
   IA.assignment σ ⟹
   IA.assignment τ ⟹
   IA.satisfies v (kb (as_of_node n⇩1)) ⟹
   IA.satisfies v' (kb (as_of_node n⇩2)) ⟹
   (∀ n lv. stack (as_of_node n⇩1) n = Some lv ⟶ σ (n,IA.IntT) = v (lv,IA.IntT) ) ⟹
   (∀ n lv. stack (as_of_node n⇩2) n = Some lv ⟶ τ (n,IA.IntT) = v' (lv,IA.IntT) ) ⟹
   renaming_of_edge (n⇩1, n⇩2) = μ ⟹
   ∀ lv ty. v (μ lv,ty) = v' (lv,ty) ⟹
   ((n⇩1,σ), (n⇩2,τ)) ∈ as_step"

lemma as_as_as_step:
  assumes "(n⇩1, n⇩2) ∈ edges" "renaming_of_edge (n⇩1, n⇩2) = μ"
    and a: "as_as_step (as_of_node n⇩1) (as_of_node n⇩2) σ τ μ"
  shows "((n⇩1,σ), (n⇩2,τ)) ∈ as_step"
  using a assms
proof (induction "as_of_node n⇩1" "as_of_node n⇩2" σ τ μ rule: as_as_step.induct)
  case (1 v v' σ τ μ)
  have "{n⇩1, n⇩2} ⊆ nodes"
    unfolding nodes_def using assms by auto
  then show ?case
    using 1 assms by (intro as_step.intros[where v=v and v'=v']) (auto)
qed

lemma as_as_as_step':
  assumes "((n⇩1,σ), (n⇩2,τ)) ∈ as_step" "renaming_of_edge (n⇩1, n⇩2) = μ"
  shows "as_as_step (as_of_node n⇩1) (as_of_node n⇩2) σ τ μ"
  using assms
proof (induction n⇩1 σ n⇩2 τ rule: as_step.induct)
  case (1 n⇩1 n⇩2 v v' σ τ μ)
  then show ?case
    by (intro as_as_step.intros[where v=v and v'=v']) (auto)
qed

lemma as_step_nodes: "((n⇩1,σ), (n⇩2,τ)) ∈ as_step ⟹ {n⇩1,n⇩2} ⊆ nodes"
  by (induct rule: as_step.induct, auto)

lemma as_step_edge: "((n⇩1,σ), (n⇩2,τ)) ∈ as_step ⟹ (n⇩1,n⇩2) ∈ edges"
  by (induct rule: as_step.induct, auto)

end


end