Theory LTL_to_GBA.LTL_to_GBA

section ‹LTL to GBA translation›
(*
  Author: Alexander Schimpf
    Modified by Peter Lammich

**)
theory LTL_to_GBA
imports
  CAVA_Base.CAVA_Base
  LTL.LTL
  CAVA_Automata.Automata
begin

subsection ‹Statistics›
code_printing
  code_module Gerth_Statistics  (SML) ‹
    structure Gerth_Statistics = struct
      val active = Unsynchronized.ref false
      val data = Unsynchronized.ref (0,0,0)

      fun is_active () = !active
      fun set_data num_states num_init num_acc = (
        active := true;
        data := (num_states, num_init, num_acc)
      )

      fun to_string () = let
        val (num_states, num_init, num_acc) = !data
      in
          "Num states: " ^ IntInf.toString (num_states) ^ "\n"
        ^ "  Num initial: " ^ IntInf.toString num_init ^ "\n"
        ^ "  Num acc-classes: " ^ IntInf.toString num_acc ^ "\n"
      end

      val _ = Statistics.register_stat ("Gerth LTL_to_GBA",is_active,to_string)
    end
›
code_reserved SML Gerth_Statistics

consts
  stat_set_data_int :: "integer  integer  integer  unit"

code_printing
  constant stat_set_data_int  (SML) "Gerth'_Statistics.set'_data"

definition "stat_set_data ns ni na
   stat_set_data_int (integer_of_nat ns) (integer_of_nat ni) (integer_of_nat na)"

lemma [autoref_rules]:
  "(stat_set_data,stat_set_data)  nat_rel  nat_rel  nat_rel  unit_rel"
  by auto

abbreviation "stat_set_data_nres ns ni na  RETURN (stat_set_data ns ni na)"

lemma discard_stat_refine[refine]:
  "m1m2  stat_set_data_nres ns ni na  m1  m2" by simp_all


subsection ‹Preliminaries›

text ‹Some very special lemmas for reasoning about the nres-monad›

lemma SPEC_rule_nested2:
  "m  SPEC P; r1 r2. P (r1, r2)  g (r1, r2)  SPEC P
   m  SPEC (λr'. g r'  SPEC P)"
  by (simp add: pw_le_iff) blast

lemma SPEC_rule_param2:
  assumes "f x  SPEC (P x)"
      and "r1 r2. (P x) (r1, r2)  (P x') (r1, r2)"
    shows "f x  SPEC (P x')"
  using assms
  by (simp add: pw_le_iff)

lemma SPEC_rule_weak:
  assumes "f x  SPEC (Q x)" and "f x  SPEC (P x)"
      and "r1 r2. (Q x) (r1, r2); (P x) (r1, r2)  (P x') (r1, r2)"
    shows "f x  SPEC (P x')"
  using assms
  by (simp add: pw_le_iff)

lemma SPEC_rule_weak_nested2: "f  SPEC Q; f  SPEC P;
  r1 r2. Q (r1, r2); P (r1, r2)  g (r1, r2)  SPEC P
   f  SPEC (λr'. g r'  SPEC P)"
  by (simp add: pw_le_iff) blast


subsection ‹Creation of States›
text ‹
  In this section, the first part of the algorithm, which creates the states of the
  automaton, is formalized.
›

(* FIXME: Abstraktion über node_name *)

type_synonym node_name = nat

type_synonym 'a frml = "'a ltlr"

type_synonym 'a interprt = "'a set word"

record 'a node =
  name :: node_name
  incoming :: "node_name set"
  new :: "'a frml set"
  old :: "'a frml set"
  "next" :: "'a frml set"

context
begin

fun new1 where
  "new1 (μ andr ψ) = {μ,ψ}"
| "new1 (μ Ur ψ) = {μ}"
| "new1 (μ Rr ψ) = {ψ}"
| "new1 (μ orr ψ) = {μ}"
| "new1 _ = {}"

fun next1 where
  "next1 (Xr ψ) = {ψ}"
| "next1 (μ Ur ψ) = {μ Ur ψ}"
| "next1 (μ Rr ψ) = {μ Rr ψ}"
| "next1 _ = {}"

fun new2 where
  "new2 (μ Ur ψ) = {ψ}"
| "new2 (μ Rr ψ) = {μ, ψ}"
| "new2 (μ orr ψ) = {ψ}"
| "new2 _ = {}"


(* FIXME: Abstraction over concrete definition *)

definition "expand_init  0"
definition "expand_new_name  Suc"

lemma expand_new_name_expand_init: "expand_init < expand_new_name nm"
  by (auto simp add:expand_init_def expand_new_name_def)

lemma expand_new_name_step[intro]:
  fixes n :: "'a node"
  shows "name n < expand_new_name (name n)"
  by (auto simp add:expand_new_name_def)

lemma expand_new_name__less_zero[intro]: "0 < expand_new_name nm"
proof -
  from expand_new_name_expand_init have "expand_init < expand_new_name nm"
    by auto
  then show ?thesis
    by (metis gr0I less_zeroE)
qed

abbreviation
  "upd_incoming_f n  (λn'.
    if (old n' = old n  next n' = next n) then
      n' incoming := incoming n  incoming n' 
    else n'
  )"

definition
 "upd_incoming n ns  ((upd_incoming_f n) ` ns)"

lemma upd_incoming__elem:
  assumes "ndupd_incoming n ns"
  shows "ndns
          (nd'ns. nd = nd' incoming := incoming n  incoming nd'  
                            old nd' = old n 
                            next nd' = next n)"
proof -
  obtain nd' where "nd'ns" and nd_eq: "nd = upd_incoming_f n nd'"
    using assms unfolding upd_incoming_def by blast
  then show ?thesis by auto
qed

lemma upd_incoming__ident_node:
  assumes "ndupd_incoming n ns" and "ndns"
    shows "incoming n  incoming nd  ¬ (old nd = old n  next nd = next n)"
proof (rule ccontr)
  assume "¬ ?thesis"
  then have nsubset: "¬ (incoming n  incoming nd)" and
    old_next_eq: "old nd = old n  next nd = next n"
    by auto
  moreover
  obtain nd' where "nd'ns" and nd_eq: "nd = upd_incoming_f n nd'"
    using assms unfolding upd_incoming_def by blast
  { assume "old nd' = old n  next nd' = next n"
    with nd_eq have "nd = nd'incoming := incoming n  incoming nd'" by auto
    with nsubset have "False" by auto }
  moreover
  { assume "¬ (old nd' = old n  next nd' = next n)"
    with nd_eq old_next_eq have "False" by auto }
  ultimately show "False" by fast
qed

lemma upd_incoming__ident:
  assumes "nns. P n"
      and "n. nns; P n  (v. P (n incoming := v ))"
    shows "nupd_incoming n ns. P n"
proof
  fix nd v
  let ?f = "λn'.
    if (old n' = old n  next n' = next n) then
      n' incoming := incoming n  incoming n' 
    else n'"
  assume "ndupd_incoming n ns"
  then obtain nd' where "nd'ns" and nd_eq: "nd = ?f nd'"
    unfolding upd_incoming_def by blast
  { assume "old nd' = old n  next nd' = next n"
    then obtain v where "nd = nd' incoming := v " using nd_eq by auto
    with assms nd'ns have "P nd" by auto }
  then show "P nd" using nd_eq nd'ns assms by auto
qed


lemma name_upd_incoming_f[simp]: "name (upd_incoming_f n x) = name x"
  by auto


lemma name_upd_incoming[simp]:
  "name ` (upd_incoming n ns) = name ` ns" (is "?lhs = ?rhs")
  unfolding upd_incoming_def
proof safe
  fix x
  assume "xns"
  then have "upd_incoming_f n x  (λn'. local.upd_incoming_f n n') ` ns" by auto
  then have "name (upd_incoming_f n x)  name ` (λn'. local.upd_incoming_f n n') ` ns"
    by blast
  then show "name x  name ` (λn'. local.upd_incoming_f n n') ` ns" by simp
qed auto


abbreviation expand_body
where
  "expand_body  (λexpand (n,ns).
      if new n = {} then (
        if (n'ns. old n' = old n  next n' = next n) then
          RETURN (name n, upd_incoming n ns)
        else
          expand (
            
              name=expand_new_name (name n),
              incoming={name n},
              new=next n,
              old={},
              next={}
            ,
            {n}  ns)
      ) else do {
        φ  SPEC (λx. x(new n));
        let n = n new := new n - {φ} ;
        if (q. φ = propr(q)  φ = npropr(q)) then
          (if (notr φ)  old n then RETURN (name n, ns)
           else expand (n old := {φ}  old n , ns))
        else if φ = truer then expand (n old := {φ}  old n , ns)
        else if φ = falser then RETURN (name n, ns)
        else if (ν μ. (φ = ν andr μ)  (φ = Xr ν)) then
          expand (
            n
              new := new1 φ  new n,
              old := {φ}  old n,
              next := next1 φ  next n
            ,
            ns)
        else do {
          (nm, nds)  expand (
            n
              new := new1 φ  new n,
              old := {φ}  old n,
              next := next1 φ  next n
            ,
            ns);
          expand (n name := nm, new := new2 φ  new n, old := {φ}  old n , nds)
        }
      }
     )"

lemma expand_body_mono: "trimono expand_body" by refine_mono

definition expand :: "('a node × ('a node set))  (node_name × 'a node set) nres"
  where "expand  REC expand_body"

lemma REC_rule_old: (* TODO: Adapt proofs below, have fun with subgoal 27 ...*)
  fixes x::"'x"
  assumes M: "trimono body"
  assumes I0: "Φ x"
  assumes IS: "f x.  x. Φ x  f x  M x; Φ x; f  REC body 
     body f x  M x"
  shows "REC body x  M x"
  by (rule REC_rule_arb[where pre="λ_. Φ" and M="λ_. M", OF assms])

lemma expand_rec_rule:
  assumes I0: "Φ x"
  assumes IS: "f x.  x. f x  expand x; x. Φ x  f x  M x; Φ x 
     expand_body f x  M x"
  shows "expand x  M x"
  unfolding expand_def
  apply (rule REC_rule_old[where Φ="Φ"])
  apply (rule expand_body_mono)
  apply (rule I0)
  apply (rule IS[unfolded expand_def])
  apply (blast dest: le_funD)
  apply blast
  apply blast
  done

abbreviation
  "expand_assm_incoming n_ns
    (nmincoming (fst n_ns). name (fst n_ns) > nm)
     0 < name (fst n_ns)
     (qsnd n_ns.
        name (fst n_ns) > name q
       (nmincoming q. name (fst n_ns) > nm))"

abbreviation
  "expand_rslt_incoming nm_nds
    (qsnd nm_nds. (fst nm_nds > name q  (nm'incoming q. fst nm_nds > nm')))"

abbreviation
  "expand_rslt_name n_ns nm_nds
    (name (fst n_ns)  fst nm_nds  name ` (snd n_ns)  name ` (snd nm_nds))
      name ` (snd nm_nds)
       = name ` (snd n_ns)  name ` {ndsnd nm_nds. name nd  name (fst n_ns)}"

abbreviation
  "expand_name_ident nds
    (qnds. ∃!q'nds. name q = name q')"

abbreviation
  "expand_assm_exist ξ n_ns
    {η. μ. μ Ur η  old (fst n_ns)  ξ r η}  new (fst n_ns)  old (fst n_ns)
          (ψnew (fst n_ns). ξ r ψ)
          (ψold (fst n_ns). ξ r ψ)
          (ψnext (fst n_ns). ξ r Xr ψ)"

abbreviation
  "expand_rslt_exist__node_prop ξ n nd
    incoming n  incoming nd
       (ψold nd. ξ r ψ)  (ψnext nd. ξ r Xr ψ)
       {η. μ. μ Ur η  old nd  ξ r η}  old nd"

abbreviation
  "expand_rslt_exist ξ n_ns nm_nds
   (ndsnd nm_nds. expand_rslt_exist__node_prop ξ (fst n_ns) nd)"

abbreviation
  "expand_rslt_exist_eq__node n nd
    name n = name nd
     old n = old nd
     next n = next nd
     incoming n  incoming nd"

abbreviation
  "expand_rslt_exist_eq n_ns nm_nds 
    (nsnd n_ns. ndsnd nm_nds. expand_rslt_exist_eq__node n nd)"

lemma expand_name_propag:
  assumes "expand_assm_incoming n_ns  expand_name_ident (snd n_ns)" (is "?Q n_ns")
    shows "expand n_ns  SPEC (λr. expand_rslt_incoming r
                                     expand_rslt_name n_ns r
                                     expand_name_ident (snd r))"
      (is "expand _  SPEC (?P n_ns)")
  using assms
proof (rule_tac expand_rec_rule[where Φ="?Q"], simp, intro refine_vcg, goal_cases)
  case prems: (1 _ _ n ns)
  then have Q: "?Q (n, ns)" by fast
  let ?nds = "upd_incoming n ns"

  from prems have "q?nds. name q < name n"
    by (rule_tac upd_incoming__ident) auto
  moreover
  have "q?nds. nm'incoming q. nm' < name n" (is "q_. ?sg q")
  proof
    fix q
    assume q_in:"q?nds"
    show "?sg q"
    proof (cases "qns")
      case True
      with prems show ?thesis by auto
    next
      case False
      with upd_incoming__elem[OF q_in]
      obtain nd' where
        nd'_def:"nd'ns  q = nd'incoming := incoming n  incoming nd'"
      by blast

      { fix nm'
        assume "nm'incoming q"
        moreover
        { assume "nm'incoming n"
          with Q have "nm' < name n" by auto }
        moreover
        { assume "nm'incoming nd'"
          with Q nd'_def have "nm' < name n" by auto }
        ultimately have "nm' < name n" using nd'_def by auto }

      then show ?thesis by fast
    qed
  qed
  moreover
  have "expand_name_ident ?nds"
  proof (rule upd_incoming__ident, goal_cases)
    case 1
    show ?case
    proof
      fix q
      assume "qns"

      with Q have "∃!q'ns. name q = name q'" by auto
      then obtain q' where "q'ns" and "name q = name q'"
                       and q'_all: "q''ns. name q' = name q''  q' = q''"
        by auto
      let ?q' = "upd_incoming_f n q'"
      have P_a: "?q'?nds  name q = name ?q'"
        using q'ns name q = name q' q'_all
        unfolding upd_incoming_def by auto

      have P_all: "q''?nds. name ?q' = name q''  ?q' = q''"
      proof(clarify)
        fix q''
        assume "q''?nds" and q''_name_eq: "name ?q' = name q''"
        { assume "q''ns"
          with upd_incoming__elem[OF q''?nds]
          obtain nd'' where
            "nd''ns"
            and q''_is: "q'' = nd''incoming := incoming n  incoming nd''
                           old nd'' = old n  next nd'' = next n"
            by auto
          then have "name nd'' = name q'"
            using q''_name_eq
            by (cases "old q' = old n  next q' = next n") auto
          with nd''ns q'_all have "nd'' = q'" by auto
          then have "?q' = q''" using q''_is by simp }
        moreover
        { assume "q''ns"
          moreover
          have "name q' = name q''"
            using q''_name_eq
            by (cases "old q' = old n  next q' = next n") auto
          moreover
          then have "incoming n  incoming q''
             incoming q'' = incoming n  incoming q''"
            by auto
          ultimately have "?q' = q''"
            using upd_incoming__ident_node[OF q''?nds] q'_all
            by auto
        }
        ultimately show "?q' = q''" by fast
      qed

      show "∃!q'upd_incoming n ns. name q = name q'"
      proof(rule ex1I[of _ ?q'], goal_cases)
        case 1
        then show ?case using P_a by simp
      next
        case 2
        then show ?case
          using P_all unfolding P_a[THEN conjunct2, THEN sym]
          by blast
      qed
    qed
  qed simp
  ultimately show ?case using prems by auto
next
  case prems: (2 f x n ns)
  then have step: "x. ?Q x  f x  SPEC (?P x)" by simp
  from prems have Q: "?Q (n, ns)" by auto

  show ?case unfolding x = (n, ns)
  proof (rule_tac SPEC_rule_param2[where P = "?P"], rule_tac step, goal_cases)
    case 1
    with expand_new_name_step[of n] show ?case
      using Q
      by (auto elim: order_less_trans[rotated])
  next
    case prems': (2 _ nds)
    then have "name ` ns  name ` nds" by auto
    with expand_new_name_step[of n] show ?case
      using prems' by auto
  qed
next
  case 3
  then show ?case by auto
next
  case prems: (4 f)
  then have step: "x. ?Q x  f x  SPEC (?P x)"
    by simp_all
  with prems show ?case
    by (rule_tac SPEC_rule_param2, rule_tac step) auto
next
  case prems: (5 f)
  then have step: "x. ?Q x  f x  SPEC (?P x)"
    by simp_all
  from prems show ?case
    by (rule_tac SPEC_rule_param2, rule_tac step) auto
next
  case 6
  then show ?case by auto
next
  case prems: (7 f)
  then have step: "x. ?Q x  f x  SPEC (?P x)"
    by simp_all
  from prems show ?case
    by (rule_tac SPEC_rule_param2, rule_tac step) auto
next
  case prems: (8 f x n ns ψ)
  then have goal_assms: "ψ  new n  (ν μ. ψ = ν orr μ  ψ = ν Ur μ  ψ = ν Rr μ)"
    by (cases ψ) auto
  from prems have Q: "?Q (n, ns)" and step: "x. ?Q x  f x  SPEC (?P x)"
    by simp_all
  show ?case
    using goal_assms Q
    unfolding case_prod_unfold x = (n, ns)
  proof (rule_tac SPEC_rule_nested2, goal_cases)
    case 1
    then show ?case
      by (rule_tac SPEC_rule_param2, rule_tac step) auto
  next
    case prems: (2 nm nds)
    then have P_x: "(name n  nm  name ` ns  name ` nds)
       name ` nds = name ` ns  name ` {ndnds. name nd  name n}"
      (is "_  ?nodes_eq nds ns (name n)") by auto
    show ?case
    proof (rule_tac SPEC_rule_param2[where P = "?P"], goal_cases)
      case 1
      with prems show ?case by (rule_tac step) auto
    next
      case prems': (2 nm' nds')
      then have "qnds'. name q < nm'  (nm''incoming q. nm'' < nm')" by auto
      moreover
      have "?nodes_eq nds ns (name n)" and "?nodes_eq nds' nds nm" and "name n  nm"
        using prems' P_x by auto
      then have "?nodes_eq nds' ns (name n)" by auto
      then have "expand_rslt_name (n, ns) (nm', nds')"
        using prems' P_x subset_trans[of "name ` ns" "name ` nds"] by auto
      ultimately show ?case using prems' by auto
    qed
  qed
qed

lemmas expand_name_propag__incoming = SPEC_rule_conjunct1[OF expand_name_propag]
lemmas expand_name_propag__name =
  SPEC_rule_conjunct1[OF SPEC_rule_conjunct2[OF expand_name_propag]]
lemmas expand_name_propag__name_ident =
  SPEC_rule_conjunct2[OF SPEC_rule_conjunct2[OF expand_name_propag]]


lemma expand_rslt_exist_eq:
  shows "expand n_ns  SPEC (expand_rslt_exist_eq n_ns)"
    (is "_  SPEC (?P n_ns)")
proof (rule_tac expand_rec_rule[where Φ="λ_. True"], simp, intro refine_vcg, goal_cases)
  case prems: (1 f x n ns)
  let ?r = "(name n, upd_incoming n ns)"
  have "expand_rslt_exist_eq (n, ns) ?r"
    unfolding snd_conv
  proof
    fix n'
    assume "n'ns"
    { assume "old n' = old n  next n' = next n"
      with n'ns
      have "n' incoming := incoming n  incoming n'   upd_incoming n ns"
        unfolding upd_incoming_def by auto
    }
    moreover
    { assume "¬ (old n' = old n  next n' = next n)"
      with n'ns have "n'  upd_incoming n ns"
        unfolding upd_incoming_def by auto
    }
    ultimately show "ndupd_incoming n ns. expand_rslt_exist_eq__node n' nd"
      by force
  qed
  with prems show ?case by auto
next
  case prems: (2 f)
  then have step: "x. f x  SPEC (?P x)" by simp
  with prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto
next
  case 3 then show ?case by auto
next
  case prems: (4 f)
  then have step: "x. f x  SPEC (?P x)" by simp
  with prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto
next
  case prems: (5 f)
  then have step: "x. f x  SPEC (?P x)" by simp
  with prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto
next
  case 6 then show ?case by auto
next
  case prems: (7 f)
  then have step: "x. f x  SPEC (?P x)" by simp
  with prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto
next
  case prems: (8 f x n ns)
  then have step: "x. f x  SPEC (?P x)" by simp

  show ?case
  proof (rule_tac SPEC_rule_nested2, goal_cases)
    case 1
    with prems show ?case
      by (rule_tac SPEC_rule_param2, rule_tac step) auto
  next
    case (2 nm nds)
    with prems have P_x: "?P (n, ns) (nm, nds)" by fast
    show ?case
      unfolding case_prod_unfold x = (n, ns)
    proof (rule_tac SPEC_rule_param2[where P = "?P"], goal_cases)
      case 1
      then show ?case by (rule_tac step)
    next
      case prems': (2 nm' nds')
      {
        fix n'
        assume "n'ns"
        with P_x obtain nd where "ndnds" and n'_split: "expand_rslt_exist_eq__node n' nd"
          by auto
        with prems' obtain nd' where "nd'nds'" and "expand_rslt_exist_eq__node nd nd'"
          by auto
        then have "nd'nds'. expand_rslt_exist_eq__node n' nd'"
          using n'_split subset_trans[of "incoming n'"] by auto
      }
      then have "expand_rslt_exist_eq (n, ns) (nm', nds')" by auto
      with prems show ?case by auto
    qed
  qed
qed

lemma expand_prop_exist:
  "expand n_ns  SPEC (λr. expand_assm_exist ξ n_ns  expand_rslt_exist ξ n_ns r)"
  (is "_  SPEC (?P n_ns)")
proof (rule_tac expand_rec_rule[where Φ="λ_. True"], simp, intro refine_vcg, goal_cases)
  case prems: (1 f x n ns)
  let ?nds = "upd_incoming n ns"
  let ?r = "(name n, ?nds)"
  { assume Q: "expand_assm_exist ξ (n, ns)"
    note n'ns. old n' = old n  next n' = next n
    then obtain n' where "n'ns" and assm_eq: "old n' = old n  next n' = next n"
      by auto
    let ?nd = "n' incoming := incoming n  incoming n'"
    have "?nd  ?nds" using n'ns assm_eq unfolding upd_incoming_def by auto
    moreover
    have "incoming n  incoming ?nd" by auto
    moreover
    have "expand_rslt_exist__node_prop ξ n ?nd" using Q assm_eq new n = {}
      by simp
    ultimately have "expand_rslt_exist ξ (n, ns) ?r"
      unfolding fst_conv snd_conv by blast
  }
  with prems show ?case
    by auto
next
  case prems: (2 f x n ns)
  then have step: "x. f x  SPEC (?P x)"
    and f_sup: "x. f x  expand x" by auto
  show ?case
    unfolding x = (n, ns)
  proof (rule_tac SPEC_rule_weak[where Q = "expand_rslt_exist_eq"], goal_cases)
    case 1
    then show ?case
      by (rule_tac order_trans, rule_tac f_sup, rule_tac expand_rslt_exist_eq)
  next
    case 2
    then show ?case by (rule_tac step)
  next
    case prems': (3 nm nds)
    then have "name ` ns  name ` nds" by auto
    moreover
    { assume assm_ex: "expand_assm_exist ξ (n, ns)"
      with prems' obtain nd where "ndnds" and "expand_rslt_exist_eq__node n nd"
        by force+
      then have "expand_rslt_exist__node_prop ξ n nd"
       using assm_ex new n = {} by auto
      then have "expand_rslt_exist ξ (n, ns) (nm, nds)" using ndnds by auto }
    ultimately show ?case
      using expand_new_name_step[of n] prems' by auto
  qed
next
  case prems: (3 f x n ns ψ)
  { assume "expand_assm_exist ξ (n, ns)"
    with prems have "ξ r ψ" and "ξ r notr ψ"  
      by (metis (no_types, lifting) fstI node.select_convs(4) node.surjective node.update_convs(3))+
    then have False by simp }
  with prems show ?case by auto
next
  case prems: (4 f x n ns ψ)
  then have goal_assms: "ψ  new n  (q. ψ = propr(q)  ψ = npropr(q))"
    and step: "x. f x  SPEC (?P x)" by simp_all
  show ?case
    using goal_assms unfolding x = (n, ns)
  proof (rule_tac SPEC_rule_param2, rule_tac step, goal_cases)
    case prems': (1 nm nds)
    { assume "expand_assm_exist ξ (n, ns)"
      with prems' have "expand_rslt_exist ξ (n, ns) (nm, nds)" by auto }
    then show ?case by auto
  qed
next
  case prems: (5 f x n ns ψ)
  then have goal_assms: "ψ  new n  ψ = truer"
    and step: "x. f x  SPEC (?P x)" by simp_all
  show ?case
    using goal_assms unfolding x = (n, ns)
  proof (rule_tac SPEC_rule_param2, rule_tac step, goal_cases)
    case prems': (1 nm nds)
    { assume "expand_assm_exist ξ (n, ns)"
      with prems' have "expand_rslt_exist ξ (n, ns) (nm, nds)" by auto }
    then show ?case by auto
  qed
next
  case prems: (6 f x n ns ψ)
  { assume "expand_assm_exist ξ (n, ns)"
    with prems have "ξ r falser" by auto }
  with prems show ?case by auto
next
  case prems: (7 f x n ns ψ)
  then have goal_assms: "ψ  new n  (ν μ. ψ = ν andr μ  ψ = Xr ν)"
    and step: "x. f x  SPEC (?P x)" by simp_all
  show ?case
    using goal_assms unfolding x = (n, ns)
  proof (rule_tac SPEC_rule_param2, rule_tac step, goal_cases)
    case prems': (1 nm nds)
    { assume "expand_assm_exist ξ (n, ns)"
      with prems' have "expand_rslt_exist ξ (n, ns) (nm, nds)" by auto }
    then show ?case by auto
  qed
next
  case prems: (8 f x n ns ψ)
  then have goal_assms: "ψ  new n  (ν μ. ψ = ν orr μ  ψ = ν Ur μ  ψ = ν Rr μ)"
    by (cases ψ) auto
  from prems have step: "x. f x  SPEC (?P x)"
    and f_sup: "x. f x  expand x" by auto
  let ?x1 = "(nnew := new n - {ψ}, new := new1 ψ  new (nnew := new n - {ψ}),
                old := {ψ}  old n, next := next1 ψ  next n, ns)"

  let ?new1_assm_sel = "λψ. (case ψ of μ Ur η => η | μ Rr η  μ | μ orr η  η)"

  { assume new1_assm: "¬ (ξ r (?new1_assm_sel ψ))"
    then have ?case
      using goal_assms unfolding x = (n, ns)
    proof (rule_tac SPEC_rule_nested2, goal_cases)
      case prems': 1
      then show ?case
      proof (rule_tac SPEC_rule_param2, rule_tac step, goal_cases)
        case prems'': (1 nm nds)
        { assume "expand_assm_exist ξ (n, ns)"
          with prems'' have "expand_assm_exist ξ ?x1"
            unfolding fst_conv
          proof (cases ψ, goal_cases)
            case ψ: (8 μ η)
            then have "ξ r μ Ur η" by fast
            then have "ξ r μ" and "ξ r Xr (μ Ur η)"
              using ψ ltlr_expand_Until[of ξ μ η] by auto
            with ψ show ?case by auto
          next
            case ψ: (9 μ η)
            then have *: "ξ r μ Rr η" by fast
            with ψ have "ξ r η" and "ξ r Xr (μ Rr η)"
              using ltlr_expand_Release[of ξ μ η] by auto
            with ψ * show ?case by auto
          qed auto
          with prems'' have "expand_rslt_exist ξ (n, ns) (nm, nds)" by force }
        with prems'' show ?case by auto
      qed
    next
      case prems': (2 nm nds)
      then have P_x: "?P (n, ns) (nm, nds)" by fast

      show ?case
        unfolding case_prod_unfold
      proof (rule_tac SPEC_rule_weak[where P = "?P" and Q = "expand_rslt_exist_eq"], goal_cases)
        case 1
        then show ?case
          by (rule_tac order_trans,
            rule_tac f_sup,
            rule_tac expand_rslt_exist_eq)
      next
        case 2
        then show ?case by (rule_tac step)
      next
        case prems'': (3 nm' nds')
        { assume "expand_assm_exist ξ (n, ns)"
          with P_x have "expand_rslt_exist ξ (n, ns) (nm, nds)" by simp
          then obtain nd where nd: "ndnds" "expand_rslt_exist__node_prop ξ n nd"
            using goal_assms by auto
          with prems'' obtain nd' where
            "nd'nds'" and "expand_rslt_exist_eq__node nd nd'"
            by force
          with nd have "expand_rslt_exist__node_prop ξ n nd'"
            using subset_trans[of "incoming n" "incoming nd"] by auto
          then have "expand_rslt_exist ξ (n,ns) (nm', nds')"
            using nd'nds' goal_assms by auto }
        then show ?case by fast
      qed
    qed
  }
  moreover
  { assume new1_assm: "ξ r (?new1_assm_sel ψ)"
    let ?x2f = "λ(nm::node_name, nds::'a node set). (
        nnew := new n - {ψ},
          name := nm,
          new := new2 ψ  new (nnew := new n - {ψ}),
          old := {ψ}  old n,
        nds)"
    have P_x: "f ?x1  SPEC (?P ?x1)" by (rule step)
    moreover
    { fix r :: "node_name × 'a node set"
      let ?x2 = "?x2f r"

      assume assm: "(?P ?x1) r"
      have "f ?x2  SPEC (?P (n, ns))"
        unfolding case_prod_unfold fst_conv
      proof (rule_tac SPEC_rule_param2, rule_tac step, goal_cases)
        case prems': (1 nm' nds')
        { assume "expand_assm_exist ξ (n, ns)"
          with new1_assm goal_assms have "expand_assm_exist ξ ?x2"
          proof (cases r, cases ψ, goal_cases)
            case prems'': (9 _ _ μ η)
            then have *: "ξ r μ Rr η" unfolding fst_conv by fast
            with ltlr_expand_Release[of ξ μ η] have "ξ r η" by auto
            with prems'' * show ?case by auto
          qed auto
          with prems' have "expand_rslt_exist ξ ?x2 (nm', nds')"
            unfolding case_prod_unfold fst_conv snd_conv by fast
          then have "expand_rslt_exist ξ (n, ns) (nm', nds')" by (cases r, auto) }
        then show ?case by simp
      qed
    }
    then have "SPEC (?P ?x1)
       SPEC (λr. (case r of (nm, nds) =>
          f (?x2f (nm, nds)))  SPEC (?P (n, ns)))"
      using goal_assms by (rule_tac SPEC_rule) force
    finally have ?case unfolding case_prod_unfold x = (n, ns) by simp
  }
  ultimately show ?case by fast
qed


text ‹Termination proof›

definition expandT :: "('a node × ('a node set))  (node_name × 'a node set) nres"
  where "expandT n_ns  RECT expand_body n_ns"

abbreviation "old_next_pair n  (old n, next n)"

abbreviation "old_next_limit φ  Pow (subfrmlsr φ) × Pow (subfrmlsr φ)"

lemma old_next_limit_finite: "finite (old_next_limit φ)"
  using subfrmlsr_finite by auto

definition
  "expand_ord φ 
     inv_image (finite_psupset (old_next_limit φ) <*lex*> less_than)
               (λ(n, ns). (old_next_pair ` ns, size_set (new n)))"

lemma expand_ord_wf[simp]: "wf (expand_ord φ)"
  using finite_psupset_wf[OF old_next_limit_finite]
  unfolding expand_ord_def by auto

abbreviation
  "expand_inv_node φ n
   finite (new n)  finite (old n)  finite (next n)
   (new n)  (old n)  (next n)  subfrmlsr φ"

abbreviation
  "expand_inv_result φ ns  finite ns  (n'ns. (new n')  (old n')  (next n')  subfrmlsr φ)"

definition
  "expand_inv φ n_ns  (case n_ns of (n, ns)  expand_inv_node φ n  expand_inv_result φ ns)"

lemma new1_less_sum: 
  "size_set (new1 φ) < size_set {φ}"
proof (cases φ)
  case (And_ltlr ν μ)
    thus ?thesis
      by (cases "ν = μ"; simp)
qed (simp_all)

lemma new2_less_sum: 
  "size_set (new2 φ) < size_set {φ}"
proof (cases φ)
  case (Release_ltlr ν μ)
    thus ?thesis
      by (cases "ν = μ"; simp)
qed (simp_all)

lemma new1_finite[intro]: "finite (new1 ψ)"
  by (cases ψ) auto
lemma new1_subset_frmls: "φ  new1 ψ  φ  subfrmlsr ψ"
  by (cases ψ) auto

lemma new2_finite[intro]: "finite (new2 ψ)"
  by (cases ψ) auto
lemma new2_subset_frmls: "φ  new2 ψ  φ  subfrmlsr ψ"
  by (cases ψ) auto

lemma next1_finite[intro]: "finite (next1 ψ)"
  by (cases ψ) auto
lemma next1_subset_frmls: "φ  next1 ψ  φ  subfrmlsr ψ"
  by (cases ψ) auto

lemma expand_inv_impl[intro!]:
  assumes "expand_inv φ (n, ns)"
      and newn: "ψ  new n"
      and "old_next_pair ` ns  old_next_pair ` ns'"
      and "expand_inv_result φ ns'"
      and "(n' = n new := new n - {ψ}, 
                    old := {ψ}  old n ) 
           (n' = n new := new1 ψ  (new n - {ψ}),
                    old := {ψ}  old n,
                    next := next1 ψ  next n ) 
           (n' = n name := nm, 
                    new := new2 ψ  (new n - {ψ}), 
                    old := {ψ}  old n )"
          (is "?case1  ?case2  ?case3")
    shows "((n', ns'), (n, ns))expand_ord φ  expand_inv φ (n', ns')"
          (is "?concl1  ?concl2")
proof
  from assms consider ?case1 | ?case2 | ?case3 by blast
  then show ?concl1
  proof cases
    case n'def: 1
    with assms show ?thesis
      unfolding expand_ord_def expand_inv_def finite_psupset_def 
      apply (cases "old_next_pair ` ns  old_next_pair ` ns'") 
      apply simp_all
      apply auto [1]
      apply (metis (no_types, lifting) add_Suc diff_Suc_less psubsetI sum.remove sum_diff1_nat zero_less_Suc)
      done
  next
    case n'def: 2
    have ψinnew: "ψ  new n" and fin_new: "finite (new n)"
      using assms unfolding expand_inv_def by auto
    then have "size_set (new n - {ψ}) = size_set (new n) - size_set {ψ}"
      using size_set_diff by fastforce
    moreover
    from fin_new sum_Un_nat[OF new1_finite _, of "new n - {ψ}" size ψ]
    have "size_set (new n')  size_set (new1 ψ) + size_set (new n - {ψ})"
      unfolding n'def by (simp add: new1_finite sum_Un_nat) 
    moreover 
    have sum_leq: "size_set (new n)  size_set {ψ}"
      using ψinnew sum_mono2[OF fin_new, of "{ψ}"]
      by blast
    ultimately 
    have "size_set (new n') < size_set (new n)"
      using new1_less_sum[of ψ] by auto
    with assms show ?thesis 
      unfolding expand_ord_def finite_psupset_def by auto
  next
    case n'def: 3
    have ψinnew: "ψ  new n" and fin_new: "finite (new n)"
      using assms unfolding expand_inv_def by auto
    from ψinnew sum_diff1_nat[of size "new n" ψ]
    have "size_set (new n - {ψ}) = size_set (new n) - size_set {ψ}"
      using size_set_diff[of "new n" "{ψ}"] by fastforce
    moreover
    from fin_new sum_Un_nat[OF new2_finite _, of "new n - {ψ}" size ψ]
    have "size_set (new n')  size_set (new2 ψ) + size_set (new n - {ψ})"
      unfolding n'def by (simp add: new2_finite sum_Un_nat) 
    moreover 
    have sum_leq:"size_set (new n)   size_set {ψ}"
      using ψinnew sum_mono2[OF fin_new, of "{ψ}"] by blast
    ultimately 
    have "size_set (new n') < size_set (new n)"
      using new2_less_sum[of ψ] sum_leq by auto
    with assms show ?thesis
      unfolding expand_ord_def finite_psupset_def by auto
  qed
next
  have "new1 ψ  subfrmlsr φ"
    and "new2 ψ  subfrmlsr φ"
    and "next1 ψ  subfrmlsr φ"
    using assms subfrmlsr_subset[OF new1_subset_frmls[of _ ψ]]
      subfrmlsr_subset[of ψ φ, OF rev_subsetD[of _ "new n"]]
      subfrmlsr_subset[OF new2_subset_frmls[of _ ψ]]
      subfrmlsr_subset[OF next1_subset_frmls[of _ ψ]]
    unfolding expand_inv_def
    (* This proof is merely a speed optimization. A single force+ does the job,
       but takes very long *)
    apply -
    apply (clarsimp split: prod.splits)
    apply (metis in_mono new1_subset_frmls)
    apply (clarsimp split: prod.splits)
    apply (metis new2_subset_frmls rev_subsetD)
    apply (clarsimp split: prod.splits)
    apply (metis in_mono next1_subset_frmls)
    done
  with assms show ?concl2
    unfolding expand_inv_def
    by auto
qed

lemma expand_term_prop_help:
  assumes "((n', ns'), (n, ns))expand_ord φ  expand_inv φ (n', ns')"
    and assm_rule: "expand_inv φ (n', ns'); ((n', ns'), n, ns)  expand_ord φ
       f (n', ns')  SPEC P"
  shows "f (n', ns')  SPEC P"
  using assms by (rule_tac assm_rule) auto

lemma expand_inv_upd_incoming:
  assumes "expand_inv φ (n, ns)"
  shows "expand_inv_result φ (upd_incoming n ns)"
  using assms unfolding expand_inv_def upd_incoming_def by force


lemma upd_incoming_eq_old_next_pair: "old_next_pair ` ns = old_next_pair ` (upd_incoming n ns)"
  (is "?A = ?B")
proof
  show "?A  ?B"
  proof
    fix x
    let ?f = "λn'. n'incoming := incoming n  incoming n'"
    assume "x  ?A"
    then obtain n' where "n'  ns" and xeq: "x = (old n', next n')"
      by auto
    have "x  (old_next_pair ` (λn'. n'incoming := incoming n  incoming n')
             ` (ns  {n'  ns. old n' = old n  next n' = next n}))
           (old_next_pair ` (ns  {n'  ns. old n'  old n  next n'  next n}))"
    proof (cases "old n' = old n  next n' = next n")
      case True
      with n'  ns
      have "?f n'  ?f ` (ns  {n'ns. old n' = old n  next n' = next n})"  (is "_  ?C")
        by auto
      then have "old_next_pair (?f n')  old_next_pair ` ?C"
        by (rule_tac imageI) auto
      with xeq have "xold_next_pair ` ?C" by auto
      then show ?thesis by blast
    next
      case False
      with n'  ns xeq
      have "x  old_next_pair ` (ns  {n'ns. old n'  old n  next n'  next n})"
        by auto
      then show ?thesis by blast
    qed
    then show "x  ?B"
      using x  ?A unfolding upd_incoming_def by auto
  qed
  show "?B  ?A"
    unfolding upd_incoming_def by (force intro:imageI)
qed

lemma expand_term_prop:
  "expand_inv φ n_ns 
    expandT n_ns  SPEC (λ(_, nds). old_next_pair ` snd n_nsold_next_pair `nds
     expand_inv_result φ nds)"
  (is "_  _  SPEC (?P n_ns)")
  unfolding expandT_def
  apply (rule_tac RECT_rule[where pre="λ(n, ns). expand_inv φ (n, ns)" and V="expand_ord φ"])
  apply (refine_mono)
  apply simp
  apply simp
proof (intro refine_vcg, goal_cases)
  case prems: (1 _ _ n ns)
  have "old_next_pair ` ns  old_next_pair ` (upd_incoming n ns)"
    by (rule equalityD1[OF upd_incoming_eq_old_next_pair])
  with prems show ?case
    using expand_inv_upd_incoming[of φ n ns] by auto
next
  case prems: (2 expand x n ns)
  let ?n' = "
    name = expand_new_name (name n),
    incoming = {name n},
    new = next n,
    old = {},
    next = {}"
  let ?ns' = "{n}  ns"
  from prems have SPEC_sub:"SPEC (?P (?n', ?ns'))  SPEC (?P x)"
    by (rule_tac SPEC_rule) auto
  from prems have "old_next_pair n  old_next_pair ` ns"
    by auto
  then have "old_next_pair ` ns  old_next_pair ` (insert n ns)"
    by auto
  moreover from prems have "expand_inv φ (n, ns)"
    by simp
  ultimately have "((?n', ?ns'), (n, ns))  expand_ord φ"
    by (auto simp add: expand_ord_def finite_psupset_def expand_inv_def)
  moreover from prems have "expand_inv φ (?n', ?ns')"
    unfolding expand_inv_def by auto
  ultimately have "expand (?n', ?ns')  SPEC (?P (?n', ?ns'))"
    using prems by fast
  with SPEC_sub show ?case
    by (rule_tac order_trans) fast+
next
  case 3
  then show ?case by (auto simp add:expand_inv_def)
next
  case 4
  then show ?case
    apply (rule_tac expand_term_prop_help[OF expand_inv_impl])
    apply (simp add: expand_inv_def)+
    apply force
    done
next
  case 5
  then show ?case
    apply (rule_tac expand_term_prop_help[OF expand_inv_impl])
    apply (simp add: expand_inv_def)+
    apply force
    done
next
  case 6
  then show ?case by (simp add: expand_inv_def)
next
  case 7
  then show ?case
    apply (rule_tac expand_term_prop_help[OF expand_inv_impl])
    apply (simp add: expand_inv_def)+
    apply force
    done
next
  case prems: (8 f x a b xa)
  let ?n' = "a
    new := new1 xa  (new a - {xa}),
    old := insert xa (old a),
    next := next1 xa  next a"
  let ?n'' = "λnm. a
    name := nm,
    new := new2 xa  (new a - {xa}),
    old := insert xa (old a)"
  have step:"((?n', b), (a, b))  expand_ord φ  expand_inv φ (?n', b)"
    using prems by (rule_tac expand_inv_impl) (auto simp add: expand_inv_def)
  with prems have assm1: "f (?n', b)  SPEC (?P (a, b))"
    by auto
  moreover
  {
    fix nm::node_name and nds::"'a node set"
    assume assm1: "old_next_pair ` b  old_next_pair ` nds"
      and assm2: "expand_inv_result φ nds"
    with prems step have "((?n'' nm, nds), (a, b))  expand_ord φ  expand_inv φ (?n'' nm, nds)"
      by (rule_tac expand_inv_impl) auto
    with prems have "f (?n'' nm, nds)  SPEC (?P (?n'' nm, nds))"
      by auto
    moreover
    have "SPEC (?P (?n'' nm, nds))  SPEC (?P (a, b))"
      using assm2 subset_trans[OF assm1] by auto
    ultimately have "f (?n'' nm, nds)  SPEC (?P (a, b))"
      by (rule order_trans)
  }
  then have assm2: "SPEC (?P (a, b))
     SPEC (λr. (case r of (nm, nds)  f (?n'' nm, nds))  SPEC (?P (a, b)))"
    by (rule_tac SPEC_rule) auto
  from prems order_trans[OF assm1 assm2] show ?case
    by auto
qed

lemma expand_eq_expandT:
  assumes inv: "expand_inv φ n_ns"
  shows "expandT n_ns = expand n_ns"
  unfolding expandT_def expand_def
  apply (rule RECT_eq_REC)
  unfolding expandT_def[symmetric]
  using expand_term_prop[OF inv] apply auto
  done

lemma expand_nofail:
  assumes inv: "expand_inv φ n_ns"
  shows "nofail (expandT n_ns)"
  using expand_term_prop[OF inv] by (simp add: pw_le_iff)

lemma [intro!]: "expand_inv φ (
  
    name = expand_new_name expand_init,
    incoming = {expand_init},
    new = {φ},
    old = {},
    next = {} ,
  {})"
  by (auto simp add: expand_inv_def)

definition create_graph :: "'a frml  'a node set nres"
where
  "create_graph φ 
    do {
      (_, nds)  expand (
        
          name = expand_new_name expand_init,
          incoming = {expand_init},
          new = {φ},
          old = {},
          next = {}
        ::'a node,
        {}::'a node set);
      RETURN nds
    }"

(* "expand_eq_expandT" *)

definition create_graphT :: "'a frml  'a node set nres"
where
  "create_graphT φ  do {
    (_, nds)  expandT (
      
        name = expand_new_name expand_init,
        incoming = {expand_init},
        new = {φ},
        old = {},
        next = {}
      ::'a node,
    {}::'a node set);
    RETURN nds
  }"

lemma create_graph_eq_create_graphT: "create_graph φ = create_graphT φ"
  unfolding create_graphT_def create_graph_def
  unfolding eq_iff
proof (standard, goal_cases)
  case 1
  then show ?case
    by refine_mono (unfold expand_def expandT_def, rule REC_le_RECT)
next
  case 2
  then show ?case
    by (refine_mono, rule expand_eq_expandT[unfolded eq_iff, THEN conjunct1]) auto
qed

lemma create_graph_finite: "create_graph φ  SPEC finite"
  unfolding create_graph_def expand_def
  apply (intro refine_vcg)
  apply (rule_tac order_trans)
  apply (rule_tac REC_le_RECT)
  apply (fold expandT_def)
  apply (rule_tac order_trans[OF expand_term_prop])
  apply auto[1]
  apply (rule_tac SPEC_rule)
  apply auto
  done

lemma create_graph_nofail: "nofail (create_graph φ)"
  by (rule_tac pwD1[OF create_graph_finite]) auto


abbreviation
  "create_graph_rslt_exist ξ nds
    ndnds.
        expand_initincoming nd
       (ψold nd. ξ r ψ)  (ψnext nd. ξ r Xr ψ)
       {η. μ. μ Ur η  old nd  ξ r η}  old nd"

lemma L4_7:
  assumes "ξ r φ"
  shows "create_graph φ  SPEC (create_graph_rslt_exist ξ)"
  using assms unfolding create_graph_def
  by (intro refine_vcg, rule_tac order_trans, rule_tac expand_prop_exist) (
    auto simp add:expand_new_name_expand_init)


lemma expand_incoming_name_exist:
  assumes "name (fst n_ns) > expand_init
     (nmincoming (fst n_ns). nm  expand_init  nmname ` (snd n_ns))
     expand_assm_incoming n_ns  expand_name_ident (snd n_ns)" (is "?Q n_ns")
  and "ndsnd n_ns.
    name nd > expand_init
     (nmincoming nd. nm  expand_init  nmname ` (snd n_ns))"
    (is "?P (snd n_ns)")
  shows "expand n_ns  SPEC (λnm_nds. ?P (snd nm_nds))"
  using assms
  apply (rule_tac expand_rec_rule[where Φ="λn_ns. ?Q n_ns  ?P (snd n_ns)"])
  apply simp
  apply (intro refine_vcg)
proof goal_cases
  case (1 f x n ns)
  then show ?case
  proof (simp, clarify, goal_cases)
    case prems: (1 _ _ nd)
    { assume "ndns"
      with prems have ?case by auto }
    moreover
    { assume "ndns"
      with upd_incoming__elem[OF ndupd_incoming n ns]
      obtain nd' where "nd'ns" and "nd = nd'incoming :=
        incoming n  incoming nd' 
        old nd' = old n 
        next nd' = next n" by auto
      with prems have ?case by auto }
    ultimately show ?case by fast
  qed
next
  case (2 f x n ns)
  then have step: "x. ?Q x  ?P (snd x)  f x  SPEC (λx. ?P (snd x))"
    and QP: "?Q (n, ns)  ?P ns"
    and f_sup: "x. f x  expand x" by auto
  show ?case
    unfolding x = (n, ns)
    using QP expand_new_name_expand_init
  proof (rule_tac step, goal_cases)
    case prems: 1
    then have name_less: "name n < expand_new_name (name n)"
      by auto
    moreover
    from prems name_less have "nmincoming n. nm < expand_new_name (name n)"
      by auto
    moreover
    from prems name_less have **: "qns. name q < expand_new_name (name n) 
      (nmincoming q. nm < expand_new_name (name n))"
      by force
    moreover
    from QP have "∃!q'. (q' = n  q'  ns)  name n = name q'"
      by force
    moreover
    have "qns. ∃!q'.
      (q' = n  q'  ns) 
      name q = name q' " using QP by auto
    ultimately show ?case using prems by simp
  qed
next
  case 3
  then show ?case by simp
next
  case 4
  then show ?case by simp
next
  case 5
  then show ?case by simp
next
  case 6
  then show ?case by simp
next
  case 7
  then show ?case by simp
next
  case prems: (8 f x n ns ψ)
  then have goal_assms: "ψ  new n  (ν μ. ψ = ν orr μ  ψ = ν Ur μ  ψ = ν Rr μ)"
    by (cases ψ) auto
  with prems have QP: "?Q (n, ns)  ?P ns"
    and step: "x. ?Q x  ?P (snd x)  f x  SPEC (λx'. ?P (snd x'))"
    and f_sup: "x. f x  expand x" by auto
  let ?x = "(nnew := new n - {ψ}, new := new1 ψ  new (nnew := new n - {ψ}),
        old := {ψ}  old (nnew := new n - {ψ}),
        next := next1 ψ  next (nnew := new n - {ψ}), ns)"
  let ?props = "λx r. expand_rslt_incoming r
     expand_rslt_name x r
     expand_name_ident (snd r)"

  show ?case
    using goal_assms QP unfolding case_prod_unfold x = (n, ns)
  proof (rule_tac SPEC_rule_weak_nested2[where Q = "?props ?x"], goal_cases)
    case 1
    then show ?case
      by (rule_tac order_trans, rule_tac f_sup, rule_tac expand_name_propag) simp
  next
    case 2
    then show ?case
      by (rule_tac SPEC_rule_param2[where P = "λx r. ?P (snd r)"], rule_tac step)
        auto
  next
    case (3 nm nds)
    then show ?case
    proof (rule_tac SPEC_rule_weak[where P = "λx r. ?P (snd r)"
        and Q = "λx r. expand_rslt_exist_eq x r  ?props x r"], goal_cases)
      case 1
      then show ?case
        by (rule_tac SPEC_rule_conjI,
               rule_tac order_trans,
               rule_tac f_sup,
               rule_tac expand_rslt_exist_eq,
               rule_tac order_trans,
               rule_tac f_sup,
               rule_tac expand_name_propag) force
    next
      case 2
      then show ?case
        by (rule_tac SPEC_rule_param2[where P = "λx r. ?P (snd r)"],
          rule_tac step) force
    next
      case (3 nm' nds')
      then show ?case
        by simp
    qed
  qed
qed

lemma create_graph__incoming_name_exist:
  "create_graph φ  SPEC (λnds. ndnds. expand_init < name nd  (nmincoming nd. nm  expand_init  nmname ` nds))"
  unfolding create_graph_def
  by (intro refine_vcg,
    rule_tac order_trans,
    rule_tac expand_incoming_name_exist) (
    auto simp add:expand_new_name_expand_init)


abbreviation
  "expand_rslt_all__ex_equiv ξ nd nds 
   (nd'nds.
    name nd  incoming nd'
     (ψold nd'. suffix 1 ξ r ψ)  (ψnext nd'. suffix 1 ξ r Xr ψ)
     {η. μ. μ Ur η  old nd'  suffix 1 ξ r η}  old nd')"

abbreviation
  "expand_rslt_all ξ n_ns nm_nds 
   (ndsnd nm_nds. name nd  name ` (snd n_ns) 
        (ψold nd. ξ r ψ)  (ψnext nd. ξ r Xr ψ)
         expand_rslt_all__ex_equiv ξ nd (snd nm_nds))"

lemma expand_prop_all:
  assumes "expand_assm_incoming n_ns  expand_name_ident (snd n_ns)" (is "?Q n_ns")
  shows "expand n_ns  SPEC (expand_rslt_all ξ n_ns)"
    (is "_  SPEC (?P n_ns)")
  using assms
  apply (rule_tac expand_rec_rule[where Φ="?Q"])
  apply simp
  apply (intro refine_vcg)
proof goal_cases
  case 1
  then show ?case by (simp, rule_tac upd_incoming__ident) simp_all
next
  case (2 f x n ns)
  then have step: "x. ?Q x  f x  SPEC (?P x)"
    and Q: "?Q (n, ns)"
    and f_sup: "x. f x  expand x" by auto
  let ?x = "(name = expand_new_name (name n),
    incoming = {name n}, new = next n, old = {}, next = {}, {n}  ns)"
  from Q have name_le: "name n < expand_new_name (name n)" by auto
  show ?case
    unfolding x = (n, ns)
  proof (rule_tac SPEC_rule_weak[where
      Q = "λp r.
      (expand_assm_exist (suffix 1 ξ) ?x  expand_rslt_exist (suffix 1 ξ) ?x r)
       expand_rslt_exist_eq p r  (expand_name_ident (snd r))"], goal_cases)
    case 1
    then show ?case
    proof (rule_tac SPEC_rule_conjI,
           rule_tac order_trans,
           rule_tac f_sup,
           rule_tac expand_prop_exist,
           rule_tac SPEC_rule_conjI,
           rule_tac order_trans,
           rule_tac f_sup,
           rule_tac expand_rslt_exist_eq,
           rule_tac order_trans,
           rule_tac f_sup,
           rule_tac expand_name_propag__name_ident,
           goal_cases)
      case 1
      then show ?case using Q name_le by force
    qed
  next
    case 2
    then show ?case using Q name_le by (rule_tac step) force
  next
    case prems: (3 nm nds)
    then obtain n' where "n'nds"
      and eq_node: "expand_rslt_exist_eq__node n n'" by auto
    with prems have ex1_name: "∃!qnds. name n = name q" by auto
    then have nds_eq: "nds = {n'}  {x  nds. name n  name x}"
      using eq_node n'nds by blast
    have name_notin: "name n  name ` ns" using Q by auto
    from prems have P_x: "expand_rslt_all ξ ?x (nm, nds)" by fast
    show ?case
      unfolding snd_conv
    proof clarify
      fix nd
      assume "nd  nds" and name_img: "name nd  name ` ns"
        and nd_old_equiv: "ψold nd. ξ r ψ"
        and nd_next_equiv: "ψnext nd. ξ r Xr ψ"
      show "expand_rslt_all__ex_equiv ξ nd nds"
      proof (cases "name nd = name n")
        case True
        with nds_eq eq_node ndnds have "nd = n'" by auto
        with prems(1)[THEN conjunct1, simplified]
          nd_old_equiv nd_next_equiv eq_node
        show ?thesis by simp
      next
        case False
        with name_img nd  nds nd_old_equiv nd_next_equiv P_x
        show ?thesis by simp
      qed
    qed
  qed
next
  case 3
  then show ?case by auto
next
  case prems: (4 f)
  then have step: "x. ?Q x  f x  SPEC (?P x)" by simp
  from prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto
next
  case prems: (5 f)
  then have step: "x. ?Q x  f x  SPEC (?P x)" by simp
  from prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto
next
  case 6
  then show ?case by auto
next
  case prems: (7 f)
  then have step: "x. ?Q x  f x  SPEC (?P x)" by simp
  from prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto
next
  case prems: (8 f x n ns ψ)
  then have goal_assms: "ψ  new n  (ν μ. ψ = ν orr μ  ψ = ν Ur μ  ψ = ν Rr μ)"
    by (cases ψ) auto
  from prems have Q: "?Q (n, ns)"
    and step: "x. ?Q x  f x  SPEC (?P x)"
    and f_sup: "x. f x  expand x" by auto
  let ?x = "(nnew := new n - {ψ}, new := new1 ψ  new (nnew := new n - {ψ}),
          old := {ψ}  old (nnew := new n - {ψ}),
                            next := next1 ψ  next (nnew := new n - {ψ})
        , ns)"
  let ?props = "λx r. expand_rslt_incoming r
     expand_rslt_name x r
     expand_name_ident (snd r)"
  show ?case
    using goal_assms Q
    unfolding case_prod_unfold x = (n, ns)
  proof (rule_tac SPEC_rule_weak_nested2[where Q = "?props ?x"], goal_cases)
    case 1
    then show ?case
      by (rule_tac order_trans, rule_tac f_sup, rule_tac expand_name_propag) simp
  next
    case 2
    then show ?case
      by (rule_tac SPEC_rule_param2[where P = "?P"], rule_tac step) auto
  next
    case prems: (3 nm nds)
    then show ?case
    proof (rule_tac SPEC_rule_weak[where
        P = "?P" and
        Q = "λx r. expand_rslt_exist_eq x r  ?props x r"], goal_cases)
      case 1
      then show ?case
        by (rule_tac SPEC_rule_conjI,
               rule_tac order_trans,
               rule_tac f_sup,
               rule_tac expand_rslt_exist_eq,
               rule_tac order_trans,
               rule_tac f_sup,
               rule_tac expand_name_propag) auto
    next
      case 2
      then show ?case
        by (rule_tac SPEC_rule_param2[where P = "?P"], rule_tac step) auto
    next
      case prems': (3 nm' nds')
      then have P_x: "?P (n, ns) (nm, nds)"
        and P_x': "?P (n, nds) (nm', nds')" by simp_all
      show ?case
        unfolding snd_conv
      proof clarify
        fix nd
        assume "ndnds'"
          and name_nd_notin: "name nd  name ` ns"
          and old_equiv: "ψold nd. ξ r ψ"
          and next_equiv: "ψnext nd. ξ r Xr ψ"
        show "expand_rslt_all__ex_equiv ξ nd nds'"
        proof (cases "name nd  name ` nds")
          case True
          then obtain n' where "n'  nds" and "name nd = name n'" by auto
          with prems' obtain nd' where "nd'nds'"
            and nd'_eq: "expand_rslt_exist_eq__node n' nd'"
            by auto
          moreover from prems' have "qnds'. ∃!q'nds'. name q = name q'"
            by simp
          ultimately have "nd' = nd"
            using name nd = name n' nd  nds' by auto
          with nd'_eq have n'_eq: "expand_rslt_exist_eq__node n' nd"
            by simp
          then have "name n'name ` ns" and "ψold n'. ξ r ψ" and "ψnext n'. ξ r Xr ψ"
            using name_nd_notin old_equiv next_equiv n'  nds
            by auto
          then have "expand_rslt_all__ex_equiv ξ n' nds"  (is "nd'nds. ?sthm n' nd'")
            using P_x n'  nds unfolding snd_conv by blast
          then obtain sucnd where sucnd: "sucndnds" and sthm: "?sthm n' sucnd"
            by blast
          moreover
          from prems' sucnd sthm obtain sucnd' where "sucnd'nds'"
              and sucnd'_eq: "expand_rslt_exist_eq__node sucnd sucnd'"
            by auto
          ultimately have "?sthm n' sucnd'" by auto
          then show ?thesis
            using sucnd'  nds'
            unfolding name nd = name n' by blast
        next
          case False
          with nd  nds' P_x' old_equiv next_equiv
          show ?thesis unfolding snd_conv by blast
        qed
      qed
    qed
  qed
qed

abbreviation
  "create_graph_rslt_all ξ nds
    qnds. (ψold q. ξ r ψ)  (ψnext q. ξ r Xr ψ)
     (q'nds. name q  incoming q'
          (ψold q'. suffix 1 ξ r ψ)
          (ψnext q'. suffix 1 ξ r Xr ψ)
          {η. μ. μ Ur η  old q'  suffix 1 ξ r η}  old q')"

lemma L4_5: "create_graph φ  SPEC (create_graph_rslt_all ξ)"
  unfolding create_graph_def
  apply (refine_vcg expand_prop_all)
  apply (auto simp add:expand_new_name_expand_init)  
  done  

subsection ‹Creation of GBA›

text ‹This section formalizes the second part of the algorithm, that creates
  the actual generalized B\"uchi automata from the set of nodes.›

definition create_gba_from_nodes :: "'a frml  'a node set  ('a node, 'a set) gba_rec"
where "create_gba_from_nodes φ qs  
  g_V = qs,
  g_E = {(q, q'). qqs  q'qs  name qincoming q'},
  g_V0 = {qqs. expand_initincoming q},
  gbg_F = {{qqs. μ Ur ηold q  ηold q}|μ η. μ Ur η  subfrmlsr φ},
  gba_L = λq l. qqs  {p. propr(p)old q}l  {p. npropr(p)old q}  l = {}
"

end

locale create_gba_from_nodes_precond =
  fixes φ :: "'a ltlr"
  fixes qs :: "'a node set"
  assumes res: "inres (create_graph φ) qs"
begin

lemma finite_qs[simp, intro!]: "finite qs"
  using res create_graph_finite by (auto simp add: pw_le_iff)

lemma create_gba_from_nodes__invar: "gba (create_gba_from_nodes φ qs)"
  using [[simproc finite_Collect]]
  apply unfold_locales
  apply (auto
    intro!: finite_vimageI subfrmlsr_finite injI
    simp: create_gba_from_nodes_def)
  done

sublocale gba: gba "create_gba_from_nodes φ qs"
  by (rule create_gba_from_nodes__invar)

lemma create_gba_from_nodes__fin: "finite (g_V (create_gba_from_nodes φ qs))"
  unfolding create_gba_from_nodes_def by auto

lemma create_gba_from_nodes__ipath:
  "ipath gba.E r  (i. r i qs  name (r i)incoming (r (Suc i)))"
  unfolding create_gba_from_nodes_def ipath_def
  by auto

lemma create_gba_from_nodes__is_run:
  "gba.is_run r  expand_init  incoming (r 0)
     (i. r iqs  name (r i)incoming (r (Suc i)))"
  unfolding gba.is_run_def
  apply (simp add: create_gba_from_nodes__ipath)
  apply (auto simp: create_gba_from_nodes_def)
  done


context
begin

abbreviation
  "auto_run_j j ξ q 
        (ψold q. suffix j ξ r ψ)  (ψnext q. suffix j ξ r Xr ψ) 
        {η. μ. μ Ur η  old q  suffix j ξ r η}  old q"

fun auto_run :: "['a interprt, 'a node set]  'a node word"
where
  "auto_run ξ nds 0
   = (SOME q. qnds  expand_init  incoming q  auto_run_j 0 ξ q)"
| "auto_run ξ nds (Suc k)
   = (SOME q'. q'nds  name (auto_run ξ nds k)  incoming q'
         auto_run_j (Suc k) ξ q')"


(* TODO: Remove. Only special instance of more generic principle
lemma create_graph_comb:
  assumes "⋀x. inres (create_graph φ) x ⟹ P x"
    shows "create_graph φ≤SPEC P"
  using create_graph_nofail assms
  by (auto simp add: pw_le_iff refine_pw_simps)
*)

lemma run_propag_on_create_graph:
  assumes "ipath gba.E σ"
  shows "σ kqs  name (σ k)incoming (σ (k+1))"
  using assms
  by (auto simp: create_gba_from_nodes__ipath)

lemma expand_false_propag:
  assumes "falser  old (fst n_ns)  (ndsnd n_ns. falser  old nd)"
    (is "?Q n_ns")
  shows "expand n_ns  SPEC (λnm_nds. ndsnd nm_nds. falser  old nd)"
  using assms
proof (rule_tac expand_rec_rule[where Φ="?Q"], simp, intro refine_vcg, goal_cases)
  case 1
  then show ?case by (simp, rule_tac upd_incoming__ident) auto
next
  case 8
  then show ?case by (rule_tac SPEC_rule_nested2) auto
qed auto

lemma false_propag_on_create_graph: "create_graph φ  SPEC (λnds. ndnds. falser  old nd)"
  unfolding create_graph_def
  by (intro refine_vcg, rule_tac order_trans, rule_tac expand_false_propag) auto


lemma expand_and_propag:
  assumes "μ andr η  old (fst n_ns)
     {μ, η}  old (fst n_ns)  new (fst n_ns)" (is "?Q n_ns")
    and "ndsnd n_ns. μ andr η  old nd  {μ, η}  old nd" (is "?P (snd n_ns)")
  shows "expand n_ns  SPEC (λnm_nds. ?P (snd nm_nds))"
  using assms
proof (rule_tac expand_rec_rule[where Φ="λx. ?Q x  ?P (snd x)"],
    simp, intro refine_vcg, goal_cases)
  case 1
  then show ?case by (simp, rule_tac upd_incoming__ident) auto
next
  case prems: (4 f x n ns)
  then have step: "x. ?Q x  ?P (snd x)  f x  SPEC (λx'. ?P (snd x'))" by simp
  with prems show ?case by (rule_tac step) auto
next
  case prems: (5 f x n ns)
  then have step: "x. ?Q x  ?P (snd x)  f x  SPEC (λx'. ?P (snd x'))" by simp
  with prems show ?case by (rule_tac step) auto
next
  case (6 f x n ns)
  then show ?case by auto
next
  case prems: (7 f x n ns)
  then have step: "x. ?Q x  ?P (snd x)  f x  SPEC (λx'. ?P (snd x'))" by simp
  with prems show ?case by (rule_tac step) auto
next
  case prems: (8 f x n ns ψ)
  then have goal_assms: "ψ  new n
     ¬ (q. ψ = propr(q)  ψ = npropr(q))
     ψ  truer  ψ  falser
     ¬ (ν μ. ψ = ν andr μ  ψ = Xr ν)
     (ν μ. ψ = ν orr μ  ψ = ν Ur μ  ψ = ν Rr μ)"
    by (cases ψ) auto
  from prems have QP: "?Q (n, ns)  ?P ns"
    and step: "x. ?Q x  ?P (snd x)  f x  SPEC (λx'. ?P (snd x'))"
    by simp_all
  show ?case
    using goal_assms QP unfolding case_prod_unfold x = (n, ns)
  proof (rule_tac SPEC_rule_nested2, goal_cases)
    case 1
    then show ?case by (rule_tac step) auto
  next
    case 2
    then show ?case by (rule_tac step) auto
  qed
qed auto

lemma and_propag_on_create_graph:
  "create_graph φ  SPEC (λnds. ndnds. μ andr η  old nd  {μ, η}  old nd)"
  unfolding create_graph_def
  by (intro refine_vcg, rule_tac order_trans, rule_tac expand_and_propag) auto

lemma expand_or_propag:
  assumes "μ orr η  old (fst n_ns)
     {μ, η}  (old (fst n_ns)  new (fst n_ns))  {}" (is "?Q n_ns")
    and "ndsnd n_ns. μ orr η  old nd  {μ, η}  old nd  {}"
    (is "?P (snd n_ns)")
  shows "expand n_ns  SPEC (λnm_nds. ?P (snd nm_nds))"
  using assms
proof (rule_tac expand_rec_rule[where Φ="λx. ?Q x  ?P (snd x)"],
    simp, intro refine_vcg, goal_cases)
  case 1
  then show ?case by (simp, rule_tac upd_incoming__ident) auto
next
  case prems: (4 f x n ns)
  then have step: "x. ?Q x  ?P (snd x)  f x  SPEC (λx'. ?P (snd x'))" by simp
  with prems show ?case by (rule_tac step) auto
next
  case prems: (5 f x n ns)
  then have step: "x. ?Q x  ?P (snd x)  f x  SPEC (λx'. ?P (snd x'))" by simp
  with prems show ?case by (rule_tac step) auto
next
  case (6 f x n ns)
  then show ?case by auto
next
  case prems: (7 f x n ns)
  then have step: "x. ?Q x  ?P (snd x)  f x  SPEC (λx'. ?P (snd x'))" by simp
  with prems show ?case by (rule_tac step) auto
next
  case prems: (8 f x n ns ψ)
  then have goal_assms: "ψ  new n
     ¬ (q. ψ = propr(q)  ψ = npropr(q))
     ψ  truer  ψ  falser
     ¬ (ν μ. ψ = ν andr μ  ψ = Xr ν)
     (ν μ. ψ = ν orr μ  ψ = ν Ur μ  ψ = ν Rr μ)"
    by (cases ψ) auto
  from prems have QP: "?Q (n, ns)  ?P ns"
    and step: "x. ?Q x  ?P (snd x)  f x  SPEC (λx'. ?P (snd x'))"
    by simp_all
  show ?case
    using goal_assms QP
    unfolding case_prod_unfold x = (n, ns)
  proof (rule_tac SPEC_rule_nested2, goal_cases)
    case 1
    then show ?case by (rule_tac step) auto
  next
    case 2
    then show ?case by (rule_tac step) auto
  qed
qed auto

lemma or_propag_on_create_graph:
  "create_graph φ  SPEC (λnds. ndnds. μ orr η  old nd  {μ, η}  old nd  {})"
  unfolding create_graph_def
  by (intro refine_vcg, rule_tac order_trans, rule_tac expand_or_propag) auto


abbreviation
  "next_propag__assm μ n_ns 
     (Xr μ  old (fst n_ns)  μ  next (fst n_ns))
      (ndsnd n_ns. Xr μ  old nd  name nd  incoming (fst n_ns)
         μ  old (fst n_ns)  new (fst n_ns))"

abbreviation
  "next_propag__rslt μ ns 
     ndns. nd'ns. Xr μ  old nd  name nd  incoming nd'  μ  old nd'"

lemma expand_next_propag:
  fixes n_ns :: "_ × 'a node set"
  assumes "next_propag__assm μ n_ns
            next_propag__rslt μ (snd n_ns)
            expand_assm_incoming n_ns
            expand_name_ident (snd n_ns)" (is "?Q n_ns")
  shows "expand n_ns  SPEC (λr. next_propag__rslt μ (snd r))"
    (is "_  SPEC ?P")
  using assms
proof (rule_tac expand_rec_rule[where Φ="?Q"], simp, intro refine_vcg, goal_cases)
  case (1 f x n ns)
  then show ?case
  proof (simp, rule_tac upd_incoming__ident, goal_cases)
    case prems: 1
    {
      fix nd :: "'a node" and nd' :: "'a node"
      assume "ndns" and nd'_elem: "nd'upd_incoming n ns"
      have "μ  old nd'" if *: "Xr μ  old nd" and **: "name nd  incoming nd'"
      proof (cases "nd'ns")
        case True
        with prems * ** show ?thesis using ndns by auto
      next
        case False
        with upd_incoming__elem[of nd' n ns] nd'_elem * **
        obtain nd'' where "nd''ns"
          and nd'_eq: "nd' = nd''incoming := incoming n  incoming nd''"
          and old_eq: "old nd'' = old n" by auto
        have "μ  old nd'"
        proof (cases "name nd  incoming n")
          case True
          with prems * ndns have "μ  old n" by auto
          then show ?thesis using nd'_eq old_eq by simp
        next
          case False
          then have "name nd  incoming nd''"
            using name nd incoming nd' nd'_eq by simp
          then show ?thesis
            unfolding nd'_eq using ndns nd''ns * prems by auto
        qed
        then show ?thesis by auto
      qed
    }
    then show ?case by auto
  next
    case 2
    then show ?case by simp
  qed
next
  case prems: (2 f x n ns)
  then have step: "x. ?Q x  f x  SPEC ?P"
    and f_sup: "x. f x  expand x" by auto
  from prems have Q: "?Q (n, ns)" by auto
  from Q have name_le: "name n < expand_new_name (name n)" by auto
  let ?x' = "(name = expand_new_name (name n),
               incoming = {name n}, new = next n,
               old = {}, next = {}, {n}  ns)"
  have Q'1: "expand_assm_incoming ?x' expand_name_ident (snd ?x')"
    using new n = {} Q[THEN conjunct2, THEN conjunct2] name_le by force
  have Q'2: "next_propag__assm μ ?x'  next_propag__rslt μ (snd ?x')"
    using Q new n = {} by auto
  show ?case
    using new n = {}
    unfolding x = (n, ns)
  proof (rule_tac SPEC_rule_weak[where
      Q = "λ_ r. expand_name_ident (snd r)" and P = "λ_. ?P"], goal_cases)
    case 1
    then show ?case
    using Q'1
      by (rule_tac order_trans,
        rule_tac f_sup,
        rule_tac expand_name_propag__name_ident) auto
  next
    case 2
    then show ?case
      using Q'1 Q'2 by (rule_tac step) simp
  next
    case (3 nm nds)
    then show ?case by simp
  qed
next
  case 3
  then show ?case by auto
next
  case prems: (4 f)
  then have step: "x. ?Q x  f x  SPEC ?P" by simp
  from prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto
next
  case prems: (5 f)
  then have step: "x. ?Q x  f x  SPEC ?P" by simp
  from prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto
next
  case 6
  then show ?case by auto
next
  case prems: (7 f)
  then have step: "x. ?Q x  f x  SPEC ?P" by simp
  from prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto
next
  case prems: (8 f x n ns ψ)
  then have goal_assms: "ψ  new n  (ν μ. ψ = ν orr μ  ψ = ν Ur μ  ψ = ν Rr μ)"
    by (cases ψ) auto
  from prems have Q: "?Q (n, ns)"
      and step: "x. ?Q x  f x  SPEC ?P"
      and f_sup: "x. f x  expand x"
    by auto
  let ?x = "(nnew := new n - {ψ}, new := new1 ψ  new (nnew := new n - {ψ}),
        old := {ψ}  old (nnew := new n - {ψ}),
                            next := next1 ψ  next (nnew := new n - {ψ})
        , ns)"
  let ?props = "λx r. expand_rslt_exist_eq x r
     expand_rslt_incoming r  expand_rslt_name x r  expand_name_ident (snd r)"
  show ?case
    using goal_assms Q unfolding case_prod_unfold x = (n, ns)
  proof (rule_tac SPEC_rule_weak_nested2[where Q = "?props ?x"], goal_cases)
    case 1 then
    show ?case
      by (rule_tac SPEC_rule_conjI,
             rule_tac order_trans,
             rule_tac f_sup,
             rule_tac expand_rslt_exist_eq,
             rule_tac order_trans,
             rule_tac f_sup,
             rule_tac expand_name_propag) simp+
  next
    case 2
    then show ?case
      by (rule_tac SPEC_rule_param2[where P = "λ_. ?P"], rule_tac step) auto
  next
    case prems': (3 nm nds)
    let ?x' = "(nnew := new n - {ψ},
       name := fst (nm, nds),
       new := new2 ψ  new (nnew := new n - {ψ}),
       old := {ψ}  old (nnew := new n - {ψ}), nds)"
    from prems' show ?case
    proof (rule_tac step, goal_cases)
      case prems'': 1
      then have "expand_assm_incoming ?x'" by auto
      moreover
      from prems'' have nds_ident: "expand_name_ident (snd ?x')" by simp
      moreover
      have "Xr μ  old (fst ?x')  μnext (fst ?x')"
      using Q[THEN conjunct1] goal_assms by auto
      moreover
      from prems'' have "next_propag__rslt μ (snd ?x')" by simp
      moreover
      from prems'' have name_nds_eq: "name ` nds = name ` ns  name ` {ndnds. name nd  name n}"
        by auto
      have "ndnds. (Xr μ  old nd  name nd  incoming (fst ?x'))
                        μold (fst ?x')new (fst ?x')"
       (is "ndnds. ?assm (fst ?x') nd  ?concl (fst ?x') nd")
      proof
        fix nd
        assume "ndnds"
        { assume loc_assm: "name ndname ` ns"
          then obtain n' where n': "n'ns" "name n' = name nd" by auto
          moreover
          from prems'' n' obtain nd' where "nd'nds"
              and n'_nd'_eq: "expand_rslt_exist_eq__node n' nd'"
            by auto
          ultimately have "nd = nd'"
            using nds_ident ndnds loc_assm by auto
          moreover from prems'' have "?assm n n'  ?concl n n'"
            using n'ns by auto
          ultimately have "?assm (fst ?x') nd  ?concl (fst ?x') nd"
            using n'_nd'_eq by auto }
        moreover
        { assume "name ndname ` ns"
          with name_nds_eq ndnds have "name nd  name n" by auto
          with prems'' have "¬ (?assm (fst ?x') nd)" by auto }
        ultimately show "?assm (fst ?x') nd  ?concl (fst ?x') nd" by auto
      qed
      ultimately show ?case by simp
    qed
  qed
qed

lemma next_propag_on_create_graph:
  "create_graph φ  SPEC (λnds. nnds. n'nds. Xr μold n  name nincoming n'  μold n')"
  unfolding create_graph_def
  apply (refine_vcg expand_next_propag)  
  apply (auto simp add:expand_new_name_expand_init)
  done
    

abbreviation
  "release_propag__assm μ η n_ns 
     (μ Rr η  old (fst n_ns)
       {μ, η}old (fst n_ns)new (fst n_ns) 
         (ηold (fst n_ns)new (fst n_ns))  μ Rr η  next (fst n_ns))
      (ndsnd n_ns.
         μ Rr η  old nd  name nd  incoming (fst n_ns)
          {μ, η}old nd 
            (ηold nd  μ Rr η  old (fst n_ns)new (fst n_ns)))"

abbreviation
  "release_propag__rslt μ η ns 
     ndns.
       nd'ns.
         μ Rr η  old nd  name nd  incoming nd'
          {μ, η}old nd 
            (ηold nd  μ Rr η  old nd')"

lemma expand_release_propag:
  fixes n_ns :: "_ × 'a node set"
  assumes "release_propag__assm μ η n_ns
            release_propag__rslt μ η (snd n_ns)
            expand_assm_incoming n_ns
            expand_name_ident (snd n_ns)" (is "?Q n_ns")
  shows "expand n_ns  SPEC (λr. release_propag__rslt μ η (snd r))"
    (is "_  SPEC ?P")
  using assms
proof (rule_tac expand_rec_rule[where Φ="?Q"], simp, intro refine_vcg, goal_cases)
  case (1 f x n ns)
  then show ?case
  proof (simp, rule_tac upd_incoming__ident, goal_cases)
    case prems: 1
    { fix nd :: "'a node" and nd' :: "'a node"
      let ?V_prop = "μ Rr η  old nd  name nd  incoming nd'
         {μ, η}  old nd  η  old nd  μ Rr η  old nd'"
      assume "ndns" and nd'_elem: "nd'upd_incoming n ns"
      { assume "nd'ns"
        with prems have ?V_prop using ndns by auto }
      moreover
      { assume "nd'ns"
          and V_in_nd: "μ Rr η  old nd" and "name nd incoming nd'"
        with upd_incoming__elem[of nd' n ns] nd'_elem
        obtain nd'' where "nd''ns"
          and nd'_eq: "nd' = nd''incoming := incoming n  incoming nd''"
          and old_eq: "old nd'' = old n"
          by auto
        { assume "name nd  incoming n"
          with prems V_in_nd ndns
          have "{μ, η}  old nd  η  old nd  μ Rr η  old n"
            by auto
          then have "{μ, η}  old nd  η  old nd  μ Rr η  old nd'"
            using nd'_eq old_eq by simp }
        moreover
        { assume "name nd  incoming n"
          then have "name nd  incoming nd''"
            using name nd incoming nd' nd'_eq by simp
          then have "{μ, η}  old nd  η  old nd  μ Rr η  old nd'"
            unfolding nd'_eq
            using prems ndns nd''ns V_in_nd by auto }
        ultimately have "{μ, η}  old nd  η  old nd  μ Rr η  old nd'"
          by fast
      }
      ultimately have ?V_prop by auto
    }
    then show ?case by auto
  next
    case 2
    then show ?case by simp
  qed
next
  case prems: (2 f x n ns)
  then have step: "x. ?Q x  f x  SPEC ?P"
    and f_sup: "x. f x  expand x" by auto
  from prems have Q: "?Q (n, ns)" by auto
  from Q have name_le: "name n < expand_new_name (name n)" by auto
  let ?x' = "(name = expand_new_name (name n),
               incoming = {name n}, new = next n,
               old = {}, next = {}, {n}  ns)"
  have Q'1: "expand_assm_incoming ?x' expand_name_ident (snd ?x')"
  using new n = {} Q[THEN conjunct2, THEN conjunct2] name_le by force
  have Q'2: "release_propag__assm μ η ?x'  release_propag__rslt μ η (snd ?x')"
    using Q new n = {} by auto

  show ?case using new n = {} unfolding x = (n, ns)

  proof (rule_tac SPEC_rule_weak[where
      Q = "λ_ r. expand_name_ident (snd r)" and P = "λ_. ?P"], goal_cases)
    case 1
    then show ?case using Q'1
      by (rule_tac order_trans,
        rule_tac f_sup,
        rule_tac expand_name_propag__name_ident) auto
  next
    case 2
    then show ?case using Q'1 Q'2 by (rule_tac step) simp
  next
    case (3 nm nds)
    then show ?case by simp
  qed
next
  case 3 then show ?case by auto
next
  case prems: (4 f x n ns ψ)
  then have goal_assms: "ψ  new n  (q. ψ = propr(q)  ψ = npropr(q))" by simp
  from prems have step: "x. ?Q x  f x  SPEC ?P" and Q: "?Q (n, ns)"
    by simp_all
  show ?case
    using Q goal_assms by (rule_tac SPEC_rule_param2, rule_tac step) auto
next
  case prems: (5 f x n ns ψ)
  then have goal_assms: "ψ  new n  ψ = truer" by simp
  from prems have step: "x. ?Q x  f x  SPEC ?P" and Q: "?Q (n, ns)"
    by simp_all
  show ?case using Q goal_assms by (rule_tac SPEC_rule_param2, rule_tac step) auto
next
  case 6
  then show ?case by auto
next
  case prems: (7 f x n ns ψ)
  then have goal_assms: "ψ  new n  (ν μ. ψ = ν andr μ  ψ = Xr ν)" by simp
  from prems have step: "x. ?Q x  f x  SPEC ?P" and Q: "?Q (n, ns)"
    by simp_all
  show ?case using Q goal_assms by (rule_tac SPEC_rule_param2, rule_tac step) auto
next
  case prems: (8 f x n ns ψ)
  then have goal_assms: "ψ  new n  (ν μ. ψ = ν orr μ  ψ = ν Ur μ  ψ = ν Rr μ)"
    by (cases ψ) auto
  from prems have Q: "?Q (n, ns)"
    and step: "x. ?Q x  f x  SPEC ?P"
    and f_sup: "x. f x  expand x" by auto
  let ?x = "(nnew := new n - {ψ}, new := new1 ψ  new (nnew := new n - {ψ}),
        old := {ψ}  old (nnew := new n - {ψ}),
                            next := next1 ψ  next (nnew := new n - {ψ})
      , ns)"
  let ?props = "λx r. expand_rslt_exist_eq x r
     expand_rslt_incoming r  expand_rslt_name x r  expand_name_ident (snd r)"

  show ?case using goal_assms Q unfolding case_prod_unfold x = (n, ns)

  proof (rule_tac SPEC_rule_weak_nested2[where Q = "?props ?x"], goal_cases)
    case 1
    then show ?case
      by (rule_tac SPEC_rule_conjI,
             rule_tac order_trans,
             rule_tac f_sup,
             rule_tac expand_rslt_exist_eq,
             rule_tac order_trans,
             rule_tac f_sup,
             rule_tac expand_name_propag) simp+
  next
    case 2
    then show ?case
      by (rule_tac SPEC_rule_param2[where P = "λ_. ?P"], rule_tac step) auto
  next
    case prems': (3 nm nds)
    let ?x' = "(nnew := new n - {ψ},
       name := fst (nm, nds),
       new := new2 ψ  new (nnew := new n - {ψ}),
       old := {ψ}  old (nnew := new n - {ψ}), nds)"
    from prems' show ?case
    proof (rule_tac step, goal_cases)
      case prems'': 1
      then have "expand_assm_incoming ?x'" by auto
      moreover
      from prems'' have nds_ident: "expand_name_ident (snd ?x')" by simp
      moreover
      have "(μ Rr η  old (fst ?x')
              ({μ, η}old (fst ?x')  new (fst ?x')
                   (ηold (fst ?x')new (fst ?x')
                      μ Rr η  next (fst ?x'))))"
        using Q[THEN conjunct1] goal_assms by auto
      moreover
      from prems'' have "release_propag__rslt μ η (snd ?x')" by simp
      moreover
      from prems'' have name_nds_eq: "name ` nds = name ` ns  name ` {ndnds. name nd  name n}"
        by auto
      have "ndnds. (μ Rr η  old nd  name nd  incoming (fst ?x'))
                  ({μ, η}old nd
                       (ηold nd  μ Rr η old (fst ?x')new (fst ?x')))"
       (is "ndnds. ?assm (fst ?x') nd  ?concl (fst ?x') nd")
      proof
        fix nd
        assume "ndnds"
        { assume loc_assm: "name ndname ` ns"
          then obtain n' where n': "n'ns" "name n' = name nd" by auto
          with prems'' obtain nd' where "nd'nds"
            and n'_nd'_eq: "expand_rslt_exist_eq__node n' nd'"
            by auto
          with n' have "nd = nd'" using nds_ident ndnds loc_assm
            by auto
          moreover from prems'' have "?assm n n'  ?concl n n'"
            using n'ns by auto
          ultimately have "?assm (fst ?x') nd  ?concl (fst ?x') nd"
            using n'_nd'_eq by auto }
        moreover
        { assume "name ndname ` ns"
          with name_nds_eq ndnds have "name nd  name n" by auto
          with prems'' have "¬ (?assm (fst ?x') nd)" by auto }
        ultimately show "?assm (fst ?x') nd  ?concl (fst ?x') nd" by auto
      qed
      ultimately show ?case by simp
    qed
  qed
qed

lemma release_propag_on_create_graph:
  "create_graph φ
      SPEC (λnds. nnds. n'nds. μ Rr ηold n  name nincoming n'
                                       ({μ, η}old n  ηold n  μ Rr ηold n'))"
  unfolding create_graph_def
  apply (refine_vcg expand_release_propag)  
  by (auto simp add:expand_new_name_expand_init)


abbreviation
  "until_propag__assm f g n_ns 
     (f Ur g  old (fst n_ns)
       (gold (fst n_ns)new (fst n_ns)
             (fold (fst n_ns)new (fst n_ns)  f Ur g  next (fst n_ns))))
      (ndsnd n_ns. f Ur g  old nd  name nd  incoming (fst n_ns)
         (gold nd  (fold nd  f Ur g old (fst n_ns)new (fst n_ns))))"

abbreviation
  "until_propag__rslt f g ns 
     nns. ndns. f Ur g  old n  name n  incoming nd
                                   (g  old n  (fold n  f Ur g  old nd))"

lemma expand_until_propag:
  fixes n_ns :: "_ × 'a node set"
  assumes "until_propag__assm μ η n_ns
            until_propag__rslt μ η (snd n_ns)
            expand_assm_incoming n_ns
            expand_name_ident (snd n_ns)" (is "?Q n_ns")
  shows "expand n_ns  SPEC (λr. until_propag__rslt μ η (snd r))"
    (is "_  SPEC ?P")
  using assms
proof (rule_tac expand_rec_rule[where Φ="?Q"], simp, intro refine_vcg, goal_cases)
  case prems: (1 f x n ns)
  then show ?case
  proof (simp, rule_tac upd_incoming__ident, goal_cases)
    case prems': 1
    { fix nd :: "'a node" and nd' :: "'a node"
      let ?U_prop = "μ Ur η  old nd  name nd  incoming nd'
                            η  old nd  μ  old nd  μ Ur η  old nd'"
      assume "ndns" and nd'_elem: "nd'upd_incoming n ns"
      { assume "nd'ns"
        with prems' have ?U_prop using ndns by auto }
      moreover
      { assume "nd'ns" and
        U_in_nd: "μ Ur η  old nd" and "name nd incoming nd'"
        with upd_incoming__elem[of nd' n ns] nd'_elem
        obtain nd'' where "nd''ns"
          and nd'_eq: "nd' = nd''incoming := incoming n  incoming nd''"
          and old_eq: "old nd'' = old n" by auto
        { assume "name nd  incoming n"
          with prems' U_in_nd ndns
          have "η  old nd  μ  old nd  μ Ur η  old n" by auto
          then have "η  old nd  μ  old nd  μ Ur η  old nd'"
            using nd'_eq old_eq by simp }
        moreover
        { assume "name nd  incoming n"
          then have "name nd  incoming nd''"
            using name nd incoming nd' nd'_eq by simp
          then have "η  old nd  μ  old nd  μ Ur η  old nd'"
            unfolding nd'_eq
            using prems' ndns nd''ns U_in_nd by auto }
        ultimately have "η  old nd  μ  old nd  μ Ur η  old nd'" by fast }
      ultimately have ?U_prop by auto }
    then show ?case by auto
  next
    case 2
    then show ?case by simp
  qed
next
  case prems: (2 f x n ns)
  then have step: "x. ?Q x  f x  SPEC ?P" and f_sup: "x. f x  expand x"
    by auto
  from prems have Q: "?Q (n, ns)" by auto
  from Q have name_le: "name n < expand_new_name (name n)" by auto
  let ?x' = "(name = expand_new_name (name n),
               incoming = {name n}, new = next n,
               old = {}, next = {}, {n}  ns)"
  have Q'1: "expand_assm_incoming ?x' expand_name_ident (snd ?x')"
    using new n = {} Q[THEN conjunct2, THEN conjunct2] name_le by force
  have Q'2: "until_propag__assm μ η ?x'  until_propag__rslt μ η (snd ?x')"
    using Q new n = {} by auto

  show ?case
    using new n = {} unfolding x = (n, ns)
  proof (rule_tac SPEC_rule_weak[where
      Q = "λ_ r. expand_name_ident (snd r)" and P = "λ_. ?P"], goal_cases)
    case 1
    then show ?case using Q'1
      by (rule_tac order_trans,
        rule_tac f_sup,
        rule_tac expand_name_propag__name_ident) auto
  next
    case 2
    then show ?case using Q'1 Q'2 by (rule_tac step) simp
  next
    case (3 nm nds)
    then show ?case by simp
  qed
next
  case 3
  then show ?case by auto
next
  case prems: (4 f)
  then have step: "x. ?Q x  f x  SPEC ?P" by simp_all
  from prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto
next
  case prems: (5 f)
  then have step: "x. ?Q x  f x  SPEC ?P" by simp_all
  from prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto
next
  case 6
  then show ?case by auto
next
  case prems: (7 f)
  then have step: "x. ?Q x  f x  SPEC ?P" by simp_all
  from prems show ?case by (rule_tac SPEC_rule_param2, rule_tac step) auto
next
  case prems: (8 f x n ns ψ)
  then have goal_assms: "ψ  new n  (ν μ. ψ = ν orr μ  ψ = ν Ur μ  ψ = ν Rr μ)"
    by (cases ψ) auto
  from prems have Q: "?Q (n, ns)"
    and step: "x. ?Q x  f x  SPEC ?P"
    and f_sup: "x. f x  expand x" by auto
  let ?x = "(nnew := new n - {ψ}, new := new1 ψ  new (nnew := new n - {ψ}),
        old := {ψ}  old (nnew := new n - {ψ}),
                            next := next1 ψ  next (nnew := new n - {ψ})
       , ns)"
  let ?props = "λx r. expand_rslt_exist_eq x r
     expand_rslt_incoming r  expand_rslt_name x r  expand_name_ident (snd r)"

  show ?case
    using goal_assms Q unfolding case_prod_unfold x = (n, ns)
  proof (rule_tac SPEC_rule_weak_nested2[where Q = "?props ?x"], goal_cases)
    case 1
    then show ?case
      by (rule_tac SPEC_rule_conjI,
             rule_tac order_trans,
             rule_tac f_sup,
             rule_tac expand_rslt_exist_eq,
             rule_tac order_trans,
             rule_tac f_sup,
             rule_tac expand_name_propag) simp+
  next
    case 2
    then show ?case
      by (rule_tac SPEC_rule_param2[where P = "λ_. ?P"], rule_tac step) auto
  next
    case prems: (3 nm nds)
    let ?x' = "(nnew := new n - {ψ},
       name := fst (nm, nds),
       new := new2 ψ  new (nnew := new n - {ψ}),
       old := {ψ}  old (nnew := new n - {ψ}), nds)"
    from prems show ?case
    proof (rule_tac step, goal_cases)
      case prems': 1
      then have "expand_assm_incoming ?x'" by auto
      moreover
      from prems' have nds_ident: "expand_name_ident (snd ?x')"
        by simp
      moreover
      have "(μ Ur η  old (fst ?x')
              (ηold (fst ?x')new (fst ?x')
                   (μold (fst ?x')new (fst ?x')
                      μ Ur η  next (fst ?x'))))"
        using Q[THEN conjunct1] goal_assms by auto
      moreover
      from prems' have "until_propag__rslt μ η (snd ?x')"
        by simp
      moreover
      from prems' have name_nds_eq:
        "name ` nds = name ` ns  name ` {ndnds. name nd  name n}"
        by auto
      have "ndnds. (μ Ur η  old nd  name nd  incoming (fst ?x'))
         (ηold nd  (μold nd  μ Ur η old (fst ?x')new (fst ?x')))"
       (is "ndnds. ?assm (fst ?x') nd  ?concl (fst ?x') nd")
      proof
        fix nd
        assume "ndnds"
        { assume loc_assm: "name ndname ` ns"
          then obtain n' where n': "n'ns" "name n' = name nd" by auto
          moreover
          from prems' n' obtain nd' where "nd'nds"
            and n'_nd'_eq: "expand_rslt_exist_eq__node n' nd'"
            by auto
          ultimately have "nd = nd'"
            using nds_ident ndnds loc_assm by auto
          moreover from prems' have "?assm n n'  ?concl n n'"
            using n'ns by auto
          ultimately have "?assm (fst ?x') nd  ?concl (fst ?x') nd"
            using n'_nd'_eq by auto }
        moreover
        { assume "name ndname ` ns"
          with name_nds_eq ndnds have "name nd  name n" by auto
          with prems' have "¬ (?assm (fst ?x') nd)" by auto }
        ultimately show "?assm (fst ?x') nd  ?concl (fst ?x') nd" by auto
      qed
      ultimately show ?case by simp
    qed
  qed
qed

lemma until_propag_on_create_graph:
  "create_graph φ  SPEC (λnds. nnds. n'nds. μ Ur ηold n  name nincoming n'
     (ηold n  μold n  μ Ur ηold n'))"
  unfolding create_graph_def
  apply (refine_vcg expand_until_propag)  
  by (auto simp add:expand_new_name_expand_init)

definition all_subfrmls :: "'a node  'a frml set"
  where "all_subfrmls n  (subfrmlsr ` (new n  old n  next n))"

lemma all_subfrmls__UnionD:
  assumes "(xA. subfrmlsr x)  B"
    and "xA"
    and "ysubfrmlsr x"
  shows "yB"
proof -
  note subfrmlsr_id[of x]
  also have "subfrmlsr x  (xA. subfrmlsr x)"
    using assms by auto
  finally show ?thesis using assms by auto
qed


lemma expand_all_subfrmls_propag:
  assumes "all_subfrmls (fst n_ns)  B  (ndsnd n_ns. all_subfrmls nd  B)" (is "?Q n_ns")
  shows "expand n_ns  SPEC (λr. ndsnd r. all_subfrmls nd  B)"
    (is "_  SPEC ?P")
  using assms
proof (rule_tac expand_rec_rule[where Φ="?Q"], simp, intro refine_vcg, goal_cases)
  case 1
  then show ?case
  proof (simp, rule_tac upd_incoming__ident, goal_cases)
    case 1
    then show ?case by auto
  next
    case 2
    then show ?case by (simp add: all_subfrmls_def)
  qed
next
  case 2
  then show ?case by (auto simp add: all_subfrmls_def)
next
  case 3
  then show ?case by (auto simp add: all_subfrmls_def)
next
  case prems: (4 f)
  then have step: "x. ?Q x  f x  SPEC ?P" by simp_all
  from prems show ?case by (rule_tac step) (auto simp add: all_subfrmls_def)
next
  case prems: (5 f _ n ns ψ)
  then have goal_assms: "ψ  new n  ψ = truer" by simp
  from prems have step: "x. ?Q x  f x  SPEC ?P" and Q: "?Q (n, ns)"
    by simp_all
  show ?case using Q goal_assms
    by (rule_tac step) (auto dest: all_subfrmls__UnionD simp add: all_subfrmls_def)
next
  case 6
  then show ?case by auto
next
  case prems: (7 f x n ns ψ)
  then have goal_assms: "ψ  new n  (ν μ. ψ = ν andr μ  ψ = Xr ν)" by simp
  from prems have step: "x. ?Q x  f x  SPEC ?P" and Q: "?Q (n, ns)"
    by simp_all
  show ?case
    using Q goal_assms
    by (rule_tac step) (auto dest: all_subfrmls__UnionD simp add: all_subfrmls_def)
next
  case prems: (8 f x n ns ψ)
  then have goal_assms: "ψ  new n
     ¬ (q. ψ = propr(q)  ψ = npropr(q))
     ψ  truer  ψ  falser
      ¬ (ν μ. ψ = ν andr μ  ψ = Xr ν)
     (ν μ. ψ = ν orr μ  ψ = ν Ur μ  ψ = ν Rr μ)"
    by (cases ψ) auto
  from prems have Q: "?Q (n, ns)" and step: "x. ?Q x  f x  SPEC ?P"
    by simp_all
  show ?case
    using goal_assms Q unfolding case_prod_unfold x = (n, ns)
  proof (rule_tac SPEC_rule_nested2, goal_cases)
    case 1
    then show ?case
      by (rule_tac step) (auto dest: all_subfrmls__UnionD simp: all_subfrmls_def)
  next
    case 2
    then show ?case
      by (rule_tac step) (auto dest: all_subfrmls__UnionD simp: all_subfrmls_def)
  qed
qed

lemma old_propag_on_create_graph: "create_graph φ  SPEC (λnds. nnds. old n  subfrmlsr φ)"
  unfolding create_graph_def
  by (intro refine_vcg,
    rule_tac order_trans,
    rule_tac expand_all_subfrmls_propag[where B = "subfrmlsr φ"])
   (force simp add:all_subfrmls_def expand_new_name_expand_init)+

lemma L4_2__aux:
  assumes run: "ipath gba.E σ"
    and "μ Ur η  old (σ 0)"
    and "j. (i<j. {μ, μ Ur η}  old (σ i))  η  old (σ j)"
  shows "i. {μ, μ Ur η}  old (σ i)  η  old (σ i)"
proof -
  have "i<j. {μ, μ Ur η}  old (σ i)" (is "?sbthm j") for j
  proof (induct j)
    show "?sbthm 0" by auto
  next
    fix k
    assume step: "?sbthm k"
    then have σ_k_prop: "η  old (σ k)
       σ kqs  σ (Suc k)qs
       name (σ k)  incoming (σ (Suc k))"
    using assms run_propag_on_create_graph[OF run] by auto
    with inres_SPEC[OF res until_propag_on_create_graph[where μ = μ and η = η]]
    have "{μ, μ Ur η}  old (σ k)" (is "?subsetthm")
    proof (cases k)
      assume "k = 0"
      with assms σ_k_prop
        inres_SPEC[OF res until_propag_on_create_graph[where μ = μ and η = η]]
      show ?subsetthm by auto
    next
      fix l
      assume "k = Suc l"
      then have "{μ, μ Ur η}old (σ l)  ηold (σ l)
         σ lqs  σ kqs
         name (σ l)incoming (σ k)"
      using step assms run_propag_on_create_graph[OF run] by auto
      with inres_SPEC[OF res until_propag_on_create_graph[where μ = μ and η = η]]
      have "μ Ur ηold (σ k)" by auto
      with σ_k_prop
        inres_SPEC[OF res until_propag_on_create_graph[where μ = μ and η = η]]
      show ?subsetthm by auto
    qed
    with step show "?sbthm (Suc k)" by (metis less_SucE)
  qed
  with assms show ?thesis by auto
qed

lemma L4_2a:
  assumes "ipath gba.E σ"
    and "μ Ur η  old (σ 0)"
  shows "(i. {μ, μ Ur η}  old (σ i)  η  old (σ i))
          (j. (i<j. {μ, μ Ur η}  old (σ i))  η  old (σ j))"
    (is "?A  ?B")
proof (rule disjCI)
  assume "¬ ?B"
  then show ?A
    using assms by (rule_tac L4_2__aux) blast+
qed

lemma L4_2b:
  assumes run: "ipath gba.E σ"
    and "μ Ur η  old (σ 0)"
    and ACC: "gba.is_acc σ"
  shows "j. (i<j. {μ, μ Ur η}  old (σ i))  η  old (σ j)"
proof (rule ccontr)
  assume "¬ ?thesis"
  then have contr: "i. {μ, μ Ur η}old(σ i)  ηold(σ i)"
    using assms L4_2a[of σ μ η] by blast

  define S where "S = {q  qs. μ Ur η  old q  η  old q}"

  from assms inres_SPEC[OF res old_propag_on_create_graph] create_gba_from_nodes__ipath
  have "μ Ur η  subfrmlsr φ"
    by (metis assms(2) subsetD)
  then have "Sgbg_F(create_gba_from_nodes φ qs)"
    unfolding S_def create_gba_from_nodes_def by auto
  with ACC have 1: "i. σ i  S"
    unfolding gba.is_acc_def by blast

  from INFM_EX[OF 1] obtain k where "σ k  qs" and "μ Ur η  old (σ k)  η  old (σ k)"
    unfolding S_def by auto
  moreover have "{μ, μ Ur η}old(σ k)  ηold(σ k)"
    using contr by auto
  ultimately show False by auto
qed

lemma L4_2c:
  assumes run: "ipath gba.E σ"
    and "μ Rr η  old (σ 0)"
  shows "i. η  old (σ i)  (j<i. μ  old (σ j))"
proof -
  have "{η, μ Rr η}  old (σ i)  (j<i. μ  old (σ j))" (is "?thm i") for i
  proof (induct i)
    case 0
    have "σ 0qs  σ 1qs  name (σ 0)  incoming (σ 1)"
    using create_gba_from_nodes__ipath assms by auto
    then show ?case
      using assms inres_SPEC[OF res release_propag_on_create_graph, of μ η]
      by auto
  next
    case (Suc k)
    note ?thm k
    moreover
    { assume "{η, μ Rr η}  old (σ k)"
      moreover
      have "σ kqs  σ (Suc k)qs  name (σ k)  incoming (σ (Suc k))"
      using create_gba_from_nodes__ipath assms by auto
      ultimately have "μ  old (σ k)  μ Rr η  old (σ (Suc k))"
        using assms inres_SPEC[OF res release_propag_on_create_graph, of μ η]
        by auto
      moreover
      { assume "μ  old (σ k)"
        then have ?case by blast }
      moreover
      { assume "μ Rr η  old (σ (Suc k))"
        moreover
        have "σ (Suc k)qs  σ (Suc (Suc k))qs
           name (σ (Suc k))  incoming (σ (Suc (Suc k)))"
        using create_gba_from_nodes__ipath assms by auto
        ultimately have ?case
          using assms
            inres_SPEC[OF res release_propag_on_create_graph, of μ η]
          by auto }
      ultimately have ?case by fast }
    moreover
    { assume "j<k. μ  old (σ j)"
      then have ?case by auto }
    ultimately show ?case by auto
  qed
  then show ?thesis by auto
qed

lemma L4_8':
  assumes "ipath gba.E σ" (is "?inf_run σ")
    and "gba.is_acc σ" (is "?gbarel_accept σ")
    and "i. gba.L (σ i) (ξ i)" (is "?lgbarel_accept ξ σ")
    and "ψ  old (σ 0)"
  shows "ξ r ψ"
  using assms
proof (induct ψ arbitrary: σ ξ)
  case True_ltlr
  show ?case by auto
next
  case False_ltlr
  then show ?case
    using inres_SPEC[OF res false_propag_on_create_graph]
      create_gba_from_nodes__ipath
    by (metis)
next
  case (Prop_ltlr p)
  then show ?case
    unfolding create_gba_from_nodes_def by auto
next
  case (Nprop_ltlr p)
  then show ?case
    unfolding create_gba_from_nodes_def by auto
next
  case (And_ltlr μ η)
  then show ?case
    using inres_SPEC[OF res and_propag_on_create_graph, of μ η]
      create_gba_from_nodes__ipath
      by (metis insert_subset semantics_ltlr.simps(5))
next
  case (Or_ltlr μ η)
  then have "μ  old (σ 0)  η  old (σ 0)"
    using inres_SPEC[OF res or_propag_on_create_graph, of μ η]
    create_gba_from_nodes__ipath
    by (metis (full_types) Int_empty_left Int_insert_left_if0)
  moreover have "ξ r μ" if "μ  old (σ 0)"
    using Or_ltlr that by auto
  moreover have "ξ r η" if "η  old (σ 0)"
    using Or_ltlr that by auto
  ultimately show ?case by auto
next
  case (Next_ltlr μ)
  with create_gba_from_nodes__ipath[of σ]
  have "σ 0  qs  σ 1  qs  name (σ 0)  incoming (σ 1)"
    by auto
  with inres_SPEC[OF res next_propag_on_create_graph, of μ] have "μold (suffix 1 σ 0)"
    using Next_ltlr by auto
  moreover
  have "?inf_run (suffix 1 σ)"
    and "?gbarel_accept (suffix 1 σ)"
    and "?lgbarel_accept (suffix 1 ξ) (suffix 1 σ )"
    using Next_ltlr create_gba_from_nodes__ipath
    apply -
    apply (metis ipath_suffix)
    apply (auto simp del: suffix_nth) [] (* FIXME:
      "λa. suffix i σ a" is unfolded, but "suffix i σ" is not! *)
    apply auto
    done
  ultimately show ?case using Next_ltlr by simp
next
  case (Until_ltlr μ η)
  then have "j. (i<j. {μ, μ Ur η}  old (σ i))  η  old (σ j)"
    using L4_2b by auto
  then obtain j where σ_pre: "i<j. {μ, μ Ur η}  old (σ i)" and "η  old (suffix j σ 0)"
    by auto
  moreover
  have "?inf_run (suffix j σ)"
    and "?gbarel_accept (suffix j σ)"
    and "?lgbarel_accept (suffix j ξ) (suffix j σ)"
    unfolding limit_suffix
    using Until_ltlr create_gba_from_nodes__ipath
    apply -
    apply (metis ipath_suffix)
    apply (auto simp del: suffix_nth) [] (* FIXME:
      "λa. suffix i σ a" is unfolded, but "suffix i σ" is not! *)
    apply auto
    done
  ultimately have "suffix j ξ r η"
    using Until_ltlr by simp
  moreover {
    fix i
    assume "i < j"
    have "?inf_run (suffix i σ)"
      and "?gbarel_accept (suffix i σ)"
      and "?lgbarel_accept (suffix i ξ) (suffix i σ )"
      unfolding limit_suffix
      using Until_ltlr create_gba_from_nodes__ipath
      apply -
      apply (metis ipath_suffix)
      apply (auto simp del: suffix_nth) [] (* FIXME:
        "λa. suffix i σ a" is unfolded, but "suffix i σ" is not! *)
      apply auto
      done
    moreover have "μold (suffix i σ 0)"
      using σ_pre i<j by auto
    ultimately have "suffix i ξ r μ" using Until_ltlr by simp
  }
  ultimately show ?case by auto
next
  case (Release_ltlr μ η)
  { fix i
    assume "η  old (σ i)  (j<i. μ  old (σ j))"
    moreover
    {
      assume *: "η  old (σ i)"
      have "?inf_run (suffix i σ)"
        and "?gbarel_accept (suffix i σ)"
        and "?lgbarel_accept (suffix i ξ) (suffix i σ )"
        unfolding limit_suffix
        using Release_ltlr create_gba_from_nodes__ipath
        apply -
        apply (metis ipath_suffix)
        apply (auto simp del: suffix_nth) [] (* FIXME:
          "λa. suffix i σ a" is unfolded, but "suffix i σ" is not! *)
        apply auto
        done
      with * have "suffix i ξ r η"
        using Release_ltlr by auto
    }
    moreover
    {
      assume "j<i. μ  old (σ j)"
      then obtain j where "j<i" and "μ  old (σ j)" by auto
      moreover
      have "?inf_run (suffix j σ)"
        and "?gbarel_accept (suffix j σ)"
        and "?lgbarel_accept (suffix j ξ) (suffix j σ )" unfolding limit_suffix
        using Release_ltlr create_gba_from_nodes__ipath
        apply -
        apply (metis ipath_suffix)
        apply (auto simp del: suffix_nth) [] (* FIXME:
          "λa. suffix i σ a" is unfolded, but "suffix i σ" is not! *)
        apply auto
        done
      ultimately have "suffix j ξ r μ"
        using Release_ltlr by auto
      then have "j<i. suffix j ξ r μ"
        using j<i by auto
    }
    ultimately have "suffix i ξ r η  (j<i. suffix j ξ r μ)" by auto
  }
  then show ?case using Release_ltlr L4_2c by auto
qed


lemma L4_8:
  assumes "gba.is_acc_run σ"
    and "i. gba.L (σ i) (ξ i)"
    and "ψ  old (σ 0)"
  shows "ξ r ψ"
  using assms
  unfolding gba.is_acc_run_def gba.is_run_def
  using L4_8' by blast

lemma expand_expand_init_propag:
  assumes "(nmincoming n'. nm < name n')
            name n'  name (fst n_ns)
            (incoming n'  incoming (fst n_ns)  {}
               new n'  old (fst n_ns)  new (fst n_ns))
           " (is "?Q n_ns")
  and "ndsnd n_ns. nmincoming n'. nmincoming nd  new n'  old nd"
    (is "?P (snd n_ns)")
  shows "expand n_ns  SPEC (λr. name n'fst r  ?P (snd r))"
  using assms
proof (rule_tac expand_rec_rule[where Φ="λx. ?Q x  ?P (snd x)"],
    simp,
    intro refine_vcg, goal_cases)
  case prems: (1 f x n ns)
  then have goal_assms: "new n = {}  ?Q (n, ns)  ?P ns" by simp
  { fix nd nm
    assume "ndupd_incoming n ns" and "nmincoming n'" and "nmincoming nd"
    { assume "ndns"
      with goal_assms nmincoming n' nmincoming nd have "new n'  old nd"
        by auto }
    moreover
    { assume "ndns"
      with upd_incoming__elem[OF ndupd_incoming n ns]
      obtain nd' where "nd'ns"
                   and nd_eq: "nd = nd'incoming := incoming n  incoming nd'"
                   and old_next_eq: "old nd' = old n  next nd' = next n" by auto
      { assume "nmincoming nd'"
        with goal_assms nmincoming n' nd'ns have "new n'  old nd"
          unfolding nd_eq by auto }
      moreover
      { assume "nmincoming n"
        with nd_eq old_next_eq goal_assms nmincoming n'
        have "new n'  old nd"
          by auto }
      ultimately have "new n'  old nd" using nmincoming nd nd_eq by auto }
    ultimately have "new n'  old nd" by fast }
  with prems show ?case by auto
next
  case prems: (2 f x n ns)
  then have goal_assms: "new n = {}  ?Q (n, ns)  ?P ns" and step: "x. ?Q x  ?P (snd x)
       f x  SPEC (λr. name n'  fst r  ?P (snd r))"
    by simp_all
  then show ?case
  proof (rule_tac step, goal_cases)
    case prems': 1
    have expand_new_name_less: "name n < expand_new_name (name n)"
      by auto
    moreover have "name n  incoming n'"
      using goal_assms by auto
    ultimately show ?case using prems' by auto
  qed
next
  case 3 then show ?case by auto
next
  case prems: (4 f x n ns)
  then have step: "x. ?Q x  ?P (snd x)  f x  SPEC (λr. name n'  fst r  ?P (snd r))"
    by simp
  from prems show ?case by (rule_tac step) auto
next
  case prems: (5 f x n ns)
  then have step: "x. ?Q x  ?P (snd x)  f x  SPEC (λr. name n'  fst r  ?P (snd r))"
    by simp
  from prems show ?case by (rule_tac step) auto
next
  case 6 then show ?case by auto
next
  case prems: (7 f x n ns)
  then have step: "x. ?Q x  ?P (snd x)  f x  SPEC (λr. name n'  fst r  ?P (snd r))"
    by simp
  from prems show ?case by (rule_tac step) auto
next
  case prems: (8 f x n ns ψ)
  then have goal_assms: "ψ  new n
     ¬ (q. ψ = propr(q)  ψ = npropr(q))
     ψ  truer  ψ  falser
     ¬ (ν μ. ψ = ν andr μ  ψ = Xr ν)
     (ν μ. ψ = ν orr μ  ψ = ν Ur μ  ψ = ν Rr μ)"
    by (cases ψ) auto
  from prems have QP: "?Q (n, ns)  ?P ns" and
    step: "x. ?Q x  ?P (snd x)  f x  SPEC (λr. name n'  fst r  ?P (snd r))"
    by simp_all
  show ?case
    using goal_assms QP unfolding case_prod_unfold x = (n, ns)
  proof (rule_tac SPEC_rule_nested2, goal_cases)
    case 1
    then show ?case by (rule_tac step) auto
  next
    case 2
    then show ?case by (rule_tac step) auto
  qed
qed

lemma expand_init_propag_on_create_graph:
  "create_graph φ  SPEC(λnds. ndnds. expand_initincoming nd  φ  old nd)"
  unfolding create_graph_def
  by (intro refine_vcg, rule_tac order_trans,
      rule_tac expand_expand_init_propag[where
          n' = " name = expand_new_name expand_init,
          incoming = {expand_init},
          new = {φ},
          old = {},
          next = {} "]) (auto simp add:expand_new_name_expand_init)

lemma L4_6:
  assumes "qgba.V0"
  shows "φold q"
  using assms inres_SPEC[OF res expand_init_propag_on_create_graph]
  unfolding create_gba_from_nodes_def by auto

lemma L4_9:
  assumes acc: "gba.accept ξ"
  shows "ξ r φ"
proof -
  from acc obtain σ where accept: "gba.is_acc_run σ  (i. gba.L (σ i) (ξ i))"
    unfolding gba.accept_def by auto
  then have "σ 0gba.V0"
    unfolding gba.is_acc_run_def gba.is_run_def by simp
  with L4_6 have "φold (σ 0)" by auto
  with L4_8 accept show ?thesis by auto
qed

lemma L4_10:
  assumes "ξ r φ"
  shows "gba.accept ξ"
proof -
  define σ where "σ = auto_run ξ qs"
  let ?G = "create_graph φ"

  have σ_prop_0: "(σ 0)qs  expand_initincoming(σ 0)  auto_run_j 0 ξ (σ 0)"
    (is "?sbthm")
  using inres_SPEC[OF res L4_7[OF ξ r φ]]
  unfolding σ_def auto_run.simps by (rule_tac someI_ex, simp) blast

  have σ_valid: "j. σ j  qs  auto_run_j j ξ (σ j)" (is "j. ?σ_valid j")
  proof
    fix j
    show "?σ_valid j"
    proof(induct j)
      from σ_prop_0 show "?σ_valid 0" by fast
    next
      fix k
      assume goal_assms: "σ k  qs  auto_run_j k ξ (σ k)"
      with inres_SPEC[OF res L4_5, of "suffix k ξ"]
      have sbthm: "q'. q'qs  name (σ k)incoming q'  auto_run_j (Suc k) ξ q'"
        (is "q'. ?sbthm q'")
        by auto
      have "?sbthm (σ (Suc k))" using someI_ex[OF sbthm]
      unfolding σ_def auto_run.simps by blast
      then show "?σ_valid (Suc k)" by fast
    qed
  qed

  have σ_prop_Suc: "k. σ k qs  σ (Suc k)qs
     name (σ k)incoming (σ (Suc k))
     auto_run_j (Suc k) ξ (σ (Suc k))"
  proof -
    fix k
    from σ_valid have "σ k  qs" and "auto_run_j k ξ (σ k)" by blast+
    with inres_SPEC[OF res L4_5, of "suffix k ξ"]
    have sbthm: "q'. q'qs  name (σ k)incoming q'
       auto_run_j (Suc k) ξ q'" (is "q'. ?sbthm q'")
      by auto
    show "σ k qs  ?sbthm (σ (Suc k))" using σ kqs someI_ex[OF sbthm]
      unfolding σ_def auto_run.simps by blast
  qed

  have σ_vnaccpt:
    "k μ η. μ Ur η  old (σ k)  ¬ (i. {μ, μ Ur η}  old (σ (k+i))  η  old (σ (k+i)))"
  proof clarify
    fix k μ η
    assume U_in: "μ Ur η  old (σ k)"
      and cntr_prm: "i. {μ, μ Ur η}  old (σ (k+i))  η  old (σ (k+i))"
    have "suffix k ξ r μ Ur η"
      using U_in σ_valid by force
    then obtain i where "suffix (k+i) ξ r η" and "j<i. suffix (k+j) ξ r μ"
      by auto
    moreover have "μ Ur η  old (σ (k+i))  η  old (σ (k+i))"
      using cntr_prm by auto
    ultimately show False
      using σ_valid by force
  qed

  have σ_exec: "gba.is_run σ"
    using σ_prop_0 σ_prop_Suc σ_valid
    unfolding gba.is_run_def ipath_def
    unfolding create_gba_from_nodes_def
    by auto
  moreover
  have σ_vaccpt:
    "k μ η. μ Ur η  old (σ k) 
      (j. (i<j. {μ, μ Ur η}  old (σ (k+i)))  η  old (σ (k+j)))"
  proof(clarify)
    fix k μ η
    assume U_in: "μ Ur η  old (σ k)"
    then have "¬ (i. {μ, μ Ur η}  old (suffix k σ i)  η  old (suffix k σ i))"
      using σ_vnaccpt[THEN allE, of k] by auto
    moreover have "suffix k σ 0  qs" using σ_valid by auto
    ultimately show "j. (i<j. {μ, μ Ur η}  old (σ (k+i)))  η  old (σ (k+j))"
      apply -
      apply (rule make_pos_rule'[OF L4_2a])
      apply (fold suffix_def)
      apply (rule ipath_suffix)
      using σ_exec[unfolded gba.is_run_def]
      apply simp
      using U_in apply simp
      apply simp
      done
  qed

  have "gba.is_acc σ"
    unfolding gba.is_acc_def
  proof
    fix S
    assume "Sgba.F"
    then obtain μ η where S_eq: "S = {q  qs. μ Ur η  old q  η  old q}"
      and "μ Ur η  subfrmlsr φ"
      by (auto simp add: create_gba_from_nodes_def)
    have range_subset: "range σ  qs"
    proof
      fix q
      assume "qrange σ"
      with full_SetCompr_eq[of σ] obtain k where "q = σ k" by auto
      then show "q  qs" using σ_valid by auto
    qed
    with limit_nonempty[of σ]
         limit_in_range[of σ]
         finite_subset[OF range_subset]
         inres_SPEC[OF res create_graph_finite]
    obtain q where q_in_limit: "q  limit σ" and q_is_node: "qqs"
      by auto
    show "i. σ i  S"
    proof (cases "μ Ur η  old q")
      case False
      with S_eq q_in_limit q_is_node
      show ?thesis
        by (auto simp: limit_iff_frequent intro: INFM_mono)
    next
      case True
      obtain k where q_eq: "q = σ k" using q_in_limit
        unfolding limit_iff_frequent by (metis (lifting, full_types) INFM_nat_le)
      have " k. η  old (σ k)"
        unfolding INFM_nat
      proof (rule ccontr)
        assume "¬ (m. n>m. η  old (σ n))"
        then obtain m where "n>m. η  old (σ n)" by auto
        moreover
        from q_eq q_in_limit limit_iff_frequent[of q σ] INFM_nat[of "λn. σ n = q"]
        obtain n where "m<n" and σn_eq: "σ n = σ k" by auto
        moreover
        obtain j where "η  old (σ (n+j))"
          using σ_vaccpt μ Ur η  old q unfolding q_eq by (fold σn_eq) force
        ultimately show False by auto
      qed
      then have " k. σ k  qs  η  old (σ k)"
        using σ_valid by (auto intro: INF_mono)
      then show " k. σ k  S"
        unfolding S_eq by (rule INFM_mono) simp
    qed
  qed
  moreover have "gba.L (σ i) (ξ i)" for i
  proof -
    from σ_valid have [simp]: "σ i  qs" by auto
    have "ψold (σ i). suffix i ξ r ψ"
      using σ_valid by auto
    then show ?thesis
      unfolding create_gba_from_nodes_def by auto
  qed
  ultimately show ?thesis
    unfolding gba.accept_def gba.is_acc_run_def by blast
qed

end
end

lemma create_graph__name_ident: "create_graph φ  SPEC (λnds. qnds. ∃!q'nds. name q = name q')"
  unfolding create_graph_def
  apply (refine_vcg expand_name_propag__name_ident)  
  by (auto simp add:expand_new_name_expand_init)

corollary create_graph__name_inj: "create_graph φ  SPEC (λnds. inj_on name nds)"
  by (rule order_trans[OF create_graph__name_ident]) (auto intro: inj_onI)


definition
  "create_gba φ
    do { nds  create_graphT φ;
          RETURN (create_gba_from_nodes φ nds) }"

lemma create_graph_precond: "create_graph φ
   SPEC (create_gba_from_nodes_precond φ)"
  apply (clarsimp simp: pw_le_iff create_graph_nofail)
  apply unfold_locales
  apply simp
  done

lemma create_gba__invar: "create_gba φ  SPEC gba"
  unfolding create_gba_def create_graph_eq_create_graphT[symmetric]
  apply (refine_rcg refine_vcg order_trans[OF create_graph_precond])
  by (rule create_gba_from_nodes_precond.create_gba_from_nodes__invar)

lemma create_gba_acc:
  shows "create_gba φ  SPEC(λ𝒜. ξ. gba.accept 𝒜 ξ  ξ r φ)"
  unfolding create_gba_def create_graph_eq_create_graphT[symmetric]
  apply (refine_rcg refine_vcg order_trans[OF create_graph_precond])
  using create_gba_from_nodes_precond.L4_9
  using create_gba_from_nodes_precond.L4_10
  by blast

lemma create_gba__name_inj:
  shows "create_gba φ  SPEC(λ𝒜. (inj_on name (g_V 𝒜)))"
  unfolding create_gba_def create_graph_eq_create_graphT[symmetric]
  apply (refine_rcg refine_vcg order_trans[OF create_graph__name_inj])
  apply (auto simp: create_gba_from_nodes_def)
  done

lemma create_gba__fin:
  shows "create_gba φ  SPEC(λ𝒜. (finite (g_V 𝒜)))"
  unfolding create_gba_def create_graph_eq_create_graphT[symmetric]
  apply (refine_rcg refine_vcg order_trans[OF create_graph_finite])
  apply (auto simp: create_gba_from_nodes_def)
  done

lemma create_graph_old_finite:
  "create_graph φ  SPEC (λnds. ndnds. finite (old nd))"
proof -
  show ?thesis
    unfolding create_graph_def create_graph_eq_create_graphT[symmetric]
    unfolding expand_def
    apply (intro refine_vcg)
    apply (rule_tac order_trans)
    apply (rule_tac REC_le_RECT)
    apply (fold expandT_def)
    apply (rule_tac order_trans[OF expand_term_prop])
    apply auto[1]
    apply (rule_tac SPEC_rule)
    apply auto
    by (metis infinite_super subfrmlsr_finite)
qed

lemma create_gba__old_fin:
  shows "create_gba φ  SPEC(λ𝒜. ndg_V 𝒜. finite (old nd))"
  unfolding create_gba_def create_graph_eq_create_graphT[symmetric]
  apply (refine_rcg refine_vcg order_trans[OF create_graph_old_finite])
  apply (simp add: create_gba_from_nodes_def)
  done

lemma create_gba__incoming_exists:
  shows "create_gba φ
   SPEC(λ𝒜. ndg_V 𝒜. incoming nd  insert expand_init (name ` (g_V 𝒜)))"
  unfolding create_gba_def create_graph_eq_create_graphT[symmetric]
  apply (refine_rcg refine_vcg order_trans[OF create_graph__incoming_name_exist])
  apply (auto simp add: create_gba_from_nodes_def)
  done

lemma create_gba__no_init:
  shows "create_gba φ  SPEC(λ𝒜. expand_init  name ` (g_V 𝒜))"
  unfolding create_gba_def create_graph_eq_create_graphT[symmetric]
  apply (refine_rcg refine_vcg order_trans[OF create_graph__incoming_name_exist])
  apply (auto simp add: create_gba_from_nodes_def)
  done

definition "nds_invars nds 
  inj_on name nds
   finite nds
   expand_init  name`nds
   (ndnds.
    finite (old nd)
     incoming nd  insert expand_init (name ` nds))"

lemma create_gba_nds_invars: "create_gba φ  SPEC (λ𝒜. nds_invars (g_V 𝒜))"
  using create_gba__name_inj[of φ] create_gba__fin[of φ]
    create_gba__old_fin[of φ] create_gba__incoming_exists[of φ]
    create_gba__no_init[of φ]
  unfolding nds_invars_def
  by (simp add: pw_le_iff)

theorem T4_1:
  "create_gba φ  SPEC(
    λ𝒜. gba 𝒜
     finite (g_V 𝒜)
     (ξ. gba.accept 𝒜 ξ  ξ r φ)
     (nds_invars (g_V 𝒜)))"
  using create_gba__invar create_gba__fin create_gba_acc create_gba_nds_invars
  apply (simp add: pw_le_iff)
  apply blast
  done

definition "create_name_gba φ  do {
  G  create_gba φ;
  ASSERT (nds_invars (g_V G));
  RETURN (gba_rename name G)
}"


theorem create_name_gba_correct:
  "create_name_gba φ  SPEC(λ𝒜. gba 𝒜  finite (g_V 𝒜)  (ξ. gba.accept 𝒜 ξ  ξ r φ))"
  unfolding create_name_gba_def
  apply (refine_rcg refine_vcg order_trans[OF T4_1])
  apply (simp_all add: nds_invars_def gba_rename_correct)
  done

definition create_name_igba :: "'a::linorder ltlr  _" where
"create_name_igba φ  do {
  A  create_name_gba φ;
  A'  gba_to_idx A;
  stat_set_data_nres (card (g_V A)) (card (g_V0 A')) (igbg_num_acc A');
  RETURN A'
}"

lemma create_name_igba_correct: "create_name_igba φ  SPEC (λG.
  igba G  finite (g_V G)  (ξ. igba.accept G ξ  ξ r φ))"
  unfolding create_name_igba_def
  apply (refine_rcg
    order_trans[OF create_name_gba_correct]
    order_trans[OF gba.gba_to_idx_ext_correct]
    refine_vcg)
  apply clarsimp_all
proof -
  fix G :: "(nat, 'a set) gba_rec"
  fix A :: "nat set"
  assume 1: "gba G"
  assume 2: "finite (g_V G)" "A  gbg_F G"
  interpret gba G using 1 .
  show "finite A" using finite_V_Fe 2 .
qed

(* For presentation in paper*)
context
  notes [refine_vcg] = order_trans[OF create_name_gba_correct]
begin

lemma "create_name_igba φ  SPEC (λG. igba G  (ξ. igba.accept G ξ  ξ r φ))"
  unfolding create_name_igba_def
proof (refine_rcg refine_vcg, clarsimp_all)
  fix G :: "(nat, 'a set) gba_rec"
  assume "gba G"
  then interpret gba G .
  note [refine_vcg] = order_trans[OF gba_to_idx_ext_correct]

  assume "ξ. gba.accept G ξ = ξ r φ" "finite (g_V G)"
  then show "gba_to_idx G  SPEC (λG'. igba G'  (ξ. igba.accept G' ξ = ξ r φ))"
    by (refine_rcg refine_vcg) (auto intro: finite_V_Fe)
qed

end

end