Theory Lts_of_Graph

theory Lts_of_Graph
  imports
    SE_Graph_Pre
    LTS.LTS
begin

context IA_locale
begin

sublocale lts  where I = I
    and type_of_fun = type_of_fun
    and Values_of_type = Values_of_type
    and Bool_types = "{BoolT}"
    and to_bool = to_bool
    and type_fixer= "TYPE(_)".
end


context graph'
begin

fun pre_post_mapping :: "_ ⇒ _ ⇒ _ ⇒ _ ⇒ _ IA.formula" where
  "pre_post_mapping pre pri astack [] = True⇩f"
| "pre_post_mapping pre pri astack (n # ns) =
      (let encode_eq  = (λn lv. Atom (Fun IA.EqF [Var ((pre n,IA.IntT)), Var ((pri lv,IA.IntT))])) in
      case astack n of None ⇒ pre_post_mapping pre pri astack ns
                     | Some lv ⇒ encode_eq n lv ∧⇩f pre_post_mapping pre pri astack ns)"

context
  fixes reverse_stack :: "'n ⇒ 'lv ⇒ 'pv"
    and loc_of_node :: "'n ⇒ 'l"
begin

definition lts_rule_of_edge :: "'n ⇒ 'n ⇒ (IA.sig, 'lv, IA.ty, 'l) transition_rule" where
  "lts_rule_of_edge n m = (let
     as⇩1 = as_of_node n;
     as⇩2 = as_of_node m;
     μ = renaming_of_edge (n, m);
     kb⇩1 = kb as⇩1;
     kb⇩2 = kb as⇩2;
     stack⇩1 = stack as⇩1;
     stack⇩2 = stack as⇩2;
     pre_f = pre_post_mapping Pre Intermediate (stack⇩1 ∘ reverse_stack n) (sorted_list_of_set (ran stack⇩1));
     kb1_f = rename_vars Intermediate kb⇩1;
     post_f = pre_post_mapping Post (Intermediate o μ) (stack⇩2 ∘ reverse_stack m) (sorted_list_of_set (ran stack⇩2));
     kb2_f = rename_vars (Intermediate o μ) kb⇩2
     in Transition (loc_of_node n) (loc_of_node m) (pre_f ∧⇩f post_f ∧⇩f kb1_f ∧⇩f kb2_f))"

abbreviation lts_state where "lts_state σ n ≡ State σ (loc_of_node n)"

definition lts_of_graph where "lts_of_graph ns = ⦇
   lts.initial = ns,
   transition_rules = (λ (n,m). lts_rule_of_edge n m) ` edges,
   assertion = (λ _. True⇩f)
  ⦈"

lemma lts_rule_of_edge:
  assumes "((n,σ), (m,τ)) ∈ as_step"
  shows "(lts_state (σ ∘ (λ(v,t). (reverse_stack n v, t))) n, lts_state (τ ∘ (λ(v,t). (reverse_stack m v, t))) m)
         ∈ IA.transition_step (λ σ. IA.assignment (valuation σ)) (lts_rule_of_edge n m)"
  using assms
proof (induction rule: as_step.induct)
  case (1 n m v v' σ τ μ)
  define σ' where "σ' = σ ∘ (λ(v,t). (reverse_stack n v, t))"
  define τ' where "τ' = τ ∘ (λ(v,t). (reverse_stack m v, t))"
  have v: "IA.assignment v" "IA.assignment σ'" "IA.assignment τ'"
    using 1 unfolding σ'_def τ'_def by (auto simp add: comp_def IA.assignment_def)
  have Pre: "IA.satisfies (IA.δ σ' τ' v)
            (pre_post_mapping Pre Intermediate
            ((abstract_state.stack (as_of_node n)) ∘ reverse_stack n) xs)" for xs
    using 1 by (induct xs, auto simp add: σ'_def split: option.split)
  show ?case
  proof -
    have v'v: "v' (lv', ty) = v (μ lv', ty)" for lv' ty
      using 1 by auto
    from 1 have kb: "IA.satisfies v (kb (as_of_node n))" "IA.satisfies v' (kb (as_of_node m))"
      by auto
    have Post: "IA.satisfies (IA.δ σ' τ' v) (pre_post_mapping Post (Intermediate ∘ μ)
                ((abstract_state.stack (as_of_node m)) ∘ reverse_stack m) xs)" for xs
      using 1[unfolded v'v] by (induct xs, auto split: option.split simp add: σ'_def τ'_def)
    have id: "map_formula (rename_vars (Intermediate ∘ μ)) (kb as)
      = map_formula (rename_vars Intermediate) (map_formula (rename_vars μ) (kb as))" for as by simp
    have kbm: "IA.satisfies (IA.δ σ' τ' v) (map_formula (rename_vars (Intermediate ∘ μ)) (kb (as_of_node m)))"
      unfolding id IA.pre_post_inter_satisfies_rename_vars
      by (subst IA.satisfies_rename_vars, insert kb v'v, auto)
    show ?thesis unfolding lts_rule_of_edge_def Let_def option.simps
      using Pre v kbm Post kb 1
      by (intro IA.mem_transition_step_TransitionI[where γ = v]) (auto simp add: σ'_def τ'_def comp_def)
  qed
qed

lemma as_step_to_lts_step:
  assumes "((n,σ), (m,τ)) ∈ as_step"
  shows "(lts_state (σ ∘ (λ(v,t). (reverse_stack n v, t))) n
         , lts_state (τ ∘ (λ(v,t). (reverse_stack m v, t))) m)
       ∈ IA.transition (lts_of_graph ns)"
proof -
  from as_step_edge[OF assms] lts_rule_of_edge[OF assms]
  show ?thesis unfolding IA.transition_def lts_of_graph_def lts.simps IA.state_def
    by (simp, intro bexI[of _ "(n,m)"], auto)
qed

lemma lts_termination_SN_as_step:
  assumes "IA.lts_termination (lts_of_graph {loc_of_node n⇩i})"
  shows "SN_on as_step {(n⇩i, v)}"
proof
  fix states
  assume steps: "∀i. (states i, states (Suc i)) ∈ as_step"
  assume init: "states 0 ∈ {(n⇩i, v)}"
  define σ where "σ = snd o states"
  define n where "n = fst o states"
  define ls where "ls i = lts_state (σ i ∘ (λ(v,t). (reverse_stack (n i) v, t))) (n i)" for i
  have steps: "⋀ i. ((n i, σ i), (n (Suc i), σ (Suc i))) ∈ as_step"
    using steps unfolding σ_def n_def by auto
  from steps[of 0] have n0: "n 0 ∈ nodes ∧ IA.assignment (σ 0)"
    by (induct rule: as_step.induct, auto)
  have steps: "⋀ i. (ls i, ls (Suc i)) ∈ IA.transition (lts_of_graph {loc_of_node n⇩i})"
    using as_step_to_lts_step[OF steps] unfolding ls_def by simp
  have init: "ls 0 ∈ IA.initial_states (lts_of_graph {loc_of_node n⇩i})"
    unfolding IA.initial_states_def ls_def lts_of_graph_def lts.simps using n0 init
    by (auto simp add: IA.assignment_def n_def)
  from assms steps init show False by auto
qed

end
end

declare graph'.pre_post_mapping.simps [code]

end