Theory LTL_to_GBA.LTL_to_GBA_impl

section ‹Refinement to Efficient Code›
(*
  Author: Peter Lammich
  Inspired by previous version of Alexander Schimpf.
*)
theory LTL_to_GBA_impl
imports 
  LTL_to_GBA
  Deriving.Compare_Instances
  CAVA_Automata.Automata_Impl
  CAVA_Base.CAVA_Code_Target
begin

subsection ‹Parametricity Setup Boilerplate›

subsubsection ‹LTL Formulas›

derive linorder ltlr

inductive_set ltlr_rel for R where
  "(True_ltlr, True_ltlr)  ltlr_rel R"
| "(False_ltlr, False_ltlr)  ltlr_rel R"
| "(a,a')R  (Prop_ltlr a,Prop_ltlr a')  ltlr_rel R"
| "(a,a')R  (Nprop_ltlr a,Nprop_ltlr a')  ltlr_rel R"
| "(a,a')ltlr_rel R; (b,b')ltlr_rel R 
   (And_ltlr a b,And_ltlr a' b')  ltlr_rel R"
| "(a,a')ltlr_rel R; (b,b')ltlr_rel R 
   (Or_ltlr a b,Or_ltlr a' b')  ltlr_rel R"
| "(a,a')ltlr_rel R  (Next_ltlr a,Next_ltlr a')  ltlr_rel R"
| "(a,a')ltlr_rel R; (b,b')ltlr_rel R 
   (Until_ltlr a b,Until_ltlr a' b')  ltlr_rel R"
| "(a,a')ltlr_rel R; (b,b')ltlr_rel R 
   (Release_ltlr a b,Release_ltlr a' b')  ltlr_rel R"

lemmas ltlr_rel_induct[induct set] 
  = ltlr_rel.induct[simplified relAPP_def[of ltlr_rel, symmetric]]
lemmas ltlr_rel_cases[cases set] 
  = ltlr_rel.cases[simplified relAPP_def[of ltlr_rel, symmetric]]
lemmas ltlr_rel_intros 
  = ltlr_rel.intros[simplified relAPP_def[of ltlr_rel, symmetric]]

inductive_simps ltlr_rel_left_simps[simplified relAPP_def[of ltlr_rel, symmetric]]: 
  "(True_ltlr,z)  ltlr_rel R"
  "(False_ltlr,z)  ltlr_rel R"
  "(Prop_ltlr p, z)  ltlr_rel R"
  "(Nprop_ltlr p, z)  ltlr_rel R"
  "(And_ltlr a b, z)  ltlr_rel R"
  "(Or_ltlr a b, z)  ltlr_rel R"
  "(Next_ltlr a, z)  ltlr_rel R"
  "(Until_ltlr a b, z)  ltlr_rel R"
  "(Release_ltlr a b, z)  ltlr_rel R"

lemma ltlr_rel_sv[relator_props]: 
  assumes SV: "single_valued R"  
  shows "single_valued (Rltlr_rel)"
proof (intro single_valuedI allI impI)
  fix x y z
  assume "(x, y)  Rltlr_rel" "(x, z)  Rltlr_rel"
  then show "y=z"
    apply (induction arbitrary: z)
    apply (simp (no_asm_use) only: ltlr_rel_left_simps 
      | blast intro: single_valuedD[OF SV])+
    done
qed

lemma ltlr_rel_id[relator_props]: " R = Id   Rltlr_rel = Id"
proof (intro equalityI subsetI, clarsimp_all)
  fix a b
  assume "(a,b)Idltlr_rel"
  then show "a=b"
    by induction auto
next
  fix a
  show "(a,a)Idltlr_rel"
    by (induction a) (auto intro: ltlr_rel_intros)
qed

lemma ltlr_rel_id_simp[simp]:  "Idltlr_rel = Id" by (rule ltlr_rel_id) simp

consts i_ltlr :: "interface  interface"
lemmas [autoref_rel_intf] = REL_INTFI[of ltlr_rel i_ltlr]

thm ltlr_rel_intros[no_vars]

lemma ltlr_con_param[param, autoref_rules]:
  "(True_ltlr, True_ltlr)  Rltlr_rel"
  "(False_ltlr, False_ltlr)  Rltlr_rel"
  "(Prop_ltlr, Prop_ltlr)  R  Rltlr_rel"
  "(Nprop_ltlr, Nprop_ltlr)  R  Rltlr_rel"
  "(And_ltlr, And_ltlr)  Rltlr_rel  Rltlr_rel  Rltlr_rel"
  "(Or_ltlr, Or_ltlr)  Rltlr_rel  Rltlr_rel  Rltlr_rel"
  "(Next_ltlr, Next_ltlr)  Rltlr_rel  Rltlr_rel"
  "(Until_ltlr, Until_ltlr)  Rltlr_rel  Rltlr_rel  Rltlr_rel"
  "(Release_ltlr, Release_ltlr)  Rltlr_rel  Rltlr_rel  Rltlr_rel"
  by (auto intro: ltlr_rel_intros)

lemma case_ltlr_param[param, autoref_rules]: 
  "(case_ltlr,case_ltlr)  Rv  Rv  (R  Rv)
                 (R  Rv)
                   (Rltlr_rel  Rltlr_rel  Rv)
                     (Rltlr_rel  Rltlr_rel  Rv)
                       (Rltlr_rel  Rv)
                         (Rltlr_rel  Rltlr_rel  Rv)
                           (Rltlr_rel  Rltlr_rel  Rv)  Rltlr_rel  Rv"
  apply (clarsimp)
  apply (case_tac ai, simp_all add: ltlr_rel_left_simps)
  apply (clarsimp_all)
  apply parametricity+
  done

lemma rec_ltlr_param[param, autoref_rules]: 
  "(rec_ltlr,rec_ltlr)  Rv  Rv  (R  Rv)
                 (R  Rv)
                   (Rltlr_rel  Rltlr_rel  Rv  Rv  Rv)
                     (Rltlr_rel  Rltlr_rel  Rv  Rv  Rv)
                       (Rltlr_rel  Rv  Rv)
                         (Rltlr_rel  Rltlr_rel  Rv  Rv  Rv)
                           (Rltlr_rel  Rltlr_rel  Rv  Rv  Rv)
                             Rltlr_rel  Rv"
proof (clarsimp, goal_cases)
  case prems: 1
  from prems(10)
  show ?case 
    apply (induction)
    using prems(1-9)
    apply simp_all
    apply parametricity+
    done
qed

lemma case_ltlr_mono[refine_mono]: 
  assumes "φ = True_ltlr  aa'"
  assumes "φ = False_ltlr  bb'"
  assumes "p. φ = Prop_ltlr p  c pc' p"
  assumes "p. φ = Nprop_ltlr p  d pd' p"
  assumes "μ ν. φ = And_ltlr μ ν  e μ νe' μ ν"
  assumes "μ ν. φ = Or_ltlr μ ν  f μ νf' μ ν"
  assumes "μ. φ = Next_ltlr μ  g μg' μ"
  assumes "μ ν. φ = Until_ltlr μ ν  h μ νh' μ ν"
  assumes "μ ν. φ = Release_ltlr μ ν  i μ νi' μ ν"
  shows "case_ltlr a b c d e f g h i φ  case_ltlr a' b' c' d' e' f' g' h' i' φ"
  using assms
  apply (cases φ)
  apply simp_all
  done


primrec ltlr_eq where
  "ltlr_eq eq True_ltlr f  (case f of True_ltlr  True | _  False)"
| "ltlr_eq eq False_ltlr f  (case f of False_ltlr  True | _  False)"
| "ltlr_eq eq (Prop_ltlr p) f  (case f of Prop_ltlr p'  eq p p' | _  False)"
| "ltlr_eq eq (Nprop_ltlr p) f  (case f of Nprop_ltlr p'  eq p p' | _  False)"
| "ltlr_eq eq (And_ltlr μ ν) f 
   (case f of And_ltlr μ' ν'  ltlr_eq eq μ μ'  ltlr_eq eq ν ν' | _  False)"
| "ltlr_eq eq (Or_ltlr μ ν) f 
   (case f of Or_ltlr μ' ν'  ltlr_eq eq μ μ'  ltlr_eq eq ν ν' | _  False)"
| "ltlr_eq eq (Next_ltlr φ) f 
   (case f of Next_ltlr φ'  ltlr_eq eq φ φ' | _  False)"
| "ltlr_eq eq (Until_ltlr μ ν) f 
   (case f of Until_ltlr μ' ν'  ltlr_eq eq μ μ'  ltlr_eq eq ν ν' | _  False)"
| "ltlr_eq eq (Release_ltlr μ ν) f 
   (case f of 
    Release_ltlr μ' ν'  ltlr_eq eq μ μ'  ltlr_eq eq ν ν' 
  | _  False)"

lemma ltlr_eq_autoref[autoref_rules]:
  assumes EQP: "(eq,(=))  R  R  bool_rel"
  shows "(ltlr_eq eq, (=))  Rltlr_rel  Rltlr_rel  bool_rel"
proof (intro fun_relI)
  fix μ' μ ν' ν
  assume "(μ',μ)Rltlr_rel" and "(ν',ν)Rltlr_rel"
  then show "(ltlr_eq eq μ' ν', μ=ν)bool_rel"
    apply (induction arbitrary: ν' ν)
    apply (erule ltlr_rel_cases, simp_all) []
    apply (erule ltlr_rel_cases, simp_all) []
    apply (erule ltlr_rel_cases, 
      simp_all add: EQP[THEN fun_relD, THEN fun_relD, THEN IdD]) []
    apply (erule ltlr_rel_cases, 
      simp_all add: EQP[THEN fun_relD, THEN fun_relD, THEN IdD]) []
    apply (rotate_tac -1)
    apply (erule ltlr_rel_cases, simp_all) []
    apply (rotate_tac -1)
    apply (erule ltlr_rel_cases, simp_all) []
    apply (rotate_tac -1)
    apply (erule ltlr_rel_cases, simp_all) []
    apply (rotate_tac -1)
    apply (erule ltlr_rel_cases, simp_all) []
    apply (rotate_tac -1)
    apply (erule ltlr_rel_cases, simp_all) []
    done
qed

lemma ltlr_dflt_cmp[autoref_rules_raw]: 
  assumes "PREFER_id R"
  shows
  "(dflt_cmp (≤) (<), dflt_cmp (≤) (<)) 
   Rltlr_rel  Rltlr_rel  comp_res_rel"
  using assms
  by simp

type_synonym
  node_name_impl = node_name 

abbreviation (input) "node_name_rel  Id :: (node_name_impl×node_name) set"

lemma case_ltlr_gtransfer:
  assumes
  "γ ai  a"
  "γ bi  b"
  "a. γ (ci a)  c a"
  "a. γ (di a)  d a"
  "ltlr1 ltlr2. γ (ei ltlr1 ltlr2)  e ltlr1 ltlr2"
  "ltlr1 ltlr2. γ (fi ltlr1 ltlr2)  f ltlr1 ltlr2"
  "ltlr. γ (gi ltlr)  g ltlr"
  "ltlr1 ltlr2. γ (hi ltlr1 ltlr2)  h ltlr1 ltlr2"
  "ltlr1 ltlr2. γ (iiv ltlr1 ltlr2)  i ltlr1 ltlr2"
  shows "γ (case_ltlr ai bi ci di ei fi gi hi iiv φ) 
     (case_ltlr a b c d e f g h i φ)"
  apply (cases φ)
  apply (auto intro: assms)
  done

lemmas [refine_transfer] 
  = case_ltlr_gtransfer[where γ=nres_of] case_ltlr_gtransfer[where γ=RETURN]

lemma [refine_transfer]:
  assumes 
  "ai  dSUCCEED"
  "bi  dSUCCEED"
  "a. ci a  dSUCCEED"
  "a. di a  dSUCCEED"
  "ltlr1 ltlr2. ei ltlr1 ltlr2  dSUCCEED"
  "ltlr1 ltlr2. fi ltlr1 ltlr2  dSUCCEED"
  "ltlr. gi ltlr  dSUCCEED"
  "ltlr1 ltlr2. hi ltlr1 ltlr2  dSUCCEED"
  "ltlr1 ltlr2. iiv ltlr1 ltlr2  dSUCCEED"
  shows "case_ltlr ai bi ci di ei fi gi hi iiv φ  dSUCCEED"
  apply (cases φ)
  apply (simp_all add: assms)
  done

subsubsection ‹Nodes›

record 'a node_impl =
  name_impl   :: node_name_impl
  incoming_impl :: "(node_name_impl,unit) RBT_Impl.rbt"
  new_impl :: "'a frml list"
  old_impl :: "'a frml list"
  next_impl :: "'a frml list"

definition node_rel where node_rel_def_internal: "node_rel Re R  {( 
   name_impl = namei, 
    incoming_impl = inci, 
    new_impl = newi,
    old_impl = oldi,
    next_impl = nexti,
     = morei
  , 
   name = name,
    incoming = inc,
    new=new,
    old=old,
    next = next,
     = more
   ) | namei name inci inc newi new oldi old nexti next morei more. 
    (namei,name)node_name_rel 
   (inci,inc)node_name_reldflt_rs_rel 
   (newi,new)Rltlr_rellss.rel
   (oldi,old)Rltlr_rellss.rel
   (nexti,next)Rltlr_rellss.rel
   (morei,more)Re
  }"

lemma node_rel_def: "Re,Rnode_rel = {( 
   name_impl = namei, 
    incoming_impl = inci, 
    new_impl = newi,
    old_impl = oldi,
    next_impl = nexti,
     = morei
  , 
   name = name,
    incoming = inc,
    new=new,
    old=old,
    next = next,
     = more
   ) | namei name inci inc newi new oldi old nexti next morei more. 
    (namei,name)node_name_rel 
   (inci,inc)node_name_reldflt_rs_rel  
   (newi,new)Rltlr_rellss.rel
   (oldi,old)Rltlr_rellss.rel
   (nexti,next)Rltlr_rellss.rel
   (morei,more)Re
  }" by (simp add: node_rel_def_internal relAPP_def)


lemma node_rel_sv[relator_props]: 
  "single_valued Re  single_valued R  single_valued (Re,Rnode_rel)"
  apply (rule single_valuedI)
  apply (simp add: node_rel_def)
  apply (auto 
    dest: single_valuedD lss.rel_sv[OF ltlr_rel_sv] map2set_rel_sv[OF ahm_rel_sv] 
    dest: single_valuedD[
      OF map2set_rel_sv[OF rbt_map_rel_sv[OF single_valued_Id single_valued_Id]]
    ])
  done

consts i_node :: "interface  interface  interface"

lemmas [autoref_rel_intf] = REL_INTFI[of node_rel i_node]

lemma [autoref_rules]: "(node_impl_ext, node_ext)  
  node_name_rel 
   node_name_reldflt_rs_rel 
   Rltlr_rellss.rel 
   Rltlr_rellss.rel 
   Rltlr_rellss.rel 
   Re 
   Re,Rnode_rel"
  unfolding node_rel_def
  by auto

lemma [autoref_rules]: 
  "(node_impl.name_impl_update,node.name_update) 
   (node_name_rel  node_name_rel)  Re,Rnode_rel  Re,Rnode_rel"
  "(node_impl.incoming_impl_update,node.incoming_update) 
   (node_name_reldflt_rs_rel  node_name_reldflt_rs_rel) 
     Re,Rnode_rel 
     Re,Rnode_rel"
  "(node_impl.new_impl_update,node.new_update) 
   (Rltlr_rellss.rel  Rltlr_rellss.rel)  Re,Rnode_rel  Re,Rnode_rel"
  "(node_impl.old_impl_update,node.old_update) 
   (Rltlr_rellss.rel  Rltlr_rellss.rel)  Re,Rnode_rel  Re,Rnode_rel"
  "(node_impl.next_impl_update,node.next_update) 
   (Rltlr_rellss.rel  Rltlr_rellss.rel)  Re,Rnode_rel  Re,Rnode_rel"
  "(node_impl.more_update,node.more_update) 
   (Re  Re)  Re,Rnode_rel  Re,Rnode_rel"
  unfolding node_rel_def
  by (auto dest: fun_relD)

term name
lemma [autoref_rules]:
  "(node_impl.name_impl,node.name)Re,Rnode_rel  node_name_rel"
  "(node_impl.incoming_impl,node.incoming)
   Re,Rnode_rel  node_name_reldflt_rs_rel"
  "(node_impl.new_impl,node.new)Re,Rnode_rel  Rltlr_rellss.rel"
  "(node_impl.old_impl,node.old)Re,Rnode_rel  Rltlr_rellss.rel"
  "(node_impl.next_impl,node.next)Re,Rnode_rel  Rltlr_rellss.rel"
  "(node_impl.more, node.more)Re,Rnode_rel  Re"
  unfolding node_rel_def by auto


subsection ‹Massaging the Abstract Algorithm›
text ‹
  In a first step, we do some refinement steps on the abstract data structures,
  with the goal to make the algorithm more efficient.
›

subsubsection ‹Creation of the Nodes›
text ‹
  In the expand-algorithm, we replace nested conditionals by case-distinctions,
  and slightly stratify the code.
›



abbreviation (input) "expand2 exp n ns φ n1 nx1 n2  do {
    (nm, nds)  exp (
      n 
        new := insert n1 (new n), 
        old := insert φ (old n), 
        next := nx1  next n , 
      ns);
    exp (n name := nm, new := n2  new n, old := {φ}  old n , nds)
  }"



definition "expand_aimpl  RECT (λ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 do {
          ASSERT (n  ns);
          ASSERT (name n  name`ns);
          expand ( 
            name=expand_new_name (name n), 
            incoming={name n}, 
            new=next n, 
            old={}, 
            next={} , 
            insert n ns)
        }
      ) else do { 
        φ  SPEC (λx. x(new n));
        let n = n new := new n - {φ} ;
        case φ of
          propr(q)  
            if npropr(q)old n then RETURN (name n, ns)
            else expand (n old := {φ}  old n , ns)
        | npropr(q)  
            if propr(q)old n then RETURN (name n, ns)
            else expand (n old := {φ}  old n , ns)
        | truer  expand (n old := {φ}  old n , ns)
        | falser  RETURN (name n, ns)
        | ν andr μ  expand (n 
            new := insert ν (insert μ (new n)), 
            old := {φ}  old n, 
            next := next n , ns)
        | Xr ν  expand 
            (n new := new n, old := {φ}  old n, next := insert ν (next n) , ns)
        | μ orr ν  expand2 expand n ns φ μ {} {ν}
        | μ Ur ν  expand2 expand n ns φ μ {φ} {ν}
        | μ Rr ν  expand2 expand n ns φ ν {φ} {μ,ν}
        ⌦‹| _ ⇒ 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_aimpl_refine:
  fixes n_ns :: "('a node × _)"
  defines "R  Id  {(_,(n,ns)). n'ns. n > name n'}"
  defines "R'  Id  {(_,(n,ns)). n'ns. name n > name n'}"
  assumes [refine]: "(n_ns',n_ns)R'"
  shows "expand_aimpl n_ns'  R (expandT n_ns)"
  using [[goals_limit = 1]]
proof -
  have [relator_props]: "single_valued R" 
    by (auto simp add: R_def intro: single_valuedI)
  have [relator_props]: "single_valued R'" 
    by (auto simp add: R'_def intro: single_valuedI)

  {
    fix n :: "'a node" and ns and n' ns'
    assume "((n', ns'), (n, ns))  R'"
    then have "(RETURN (name n', ns')   R (RETURN (name n, ns)))"
      by (auto simp: R_def R'_def pw_le_iff refine_pw_simps)
  } note aux = this


  show ?thesis
    unfolding expand_aimpl_def expandT_def
    apply refine_rcg
    apply (simp add: R_def R'_def)
    apply (simp add: R_def R'_def)
    apply (auto simp add: R_def R'_def upd_incoming_def) []
    apply (auto simp add: R_def R'_def upd_incoming_def) []
    apply (auto simp add: R_def R'_def upd_incoming_def) []
    apply rprems
    apply (auto simp: R'_def expand_new_name_def) []
    apply (simp add: R'_def)

    apply (auto split: ltlr.split) []
    apply (fastforce simp: R_def R'_def) []
    apply (fastforce simp: R_def R'_def) []

    apply (auto simp: R_def R'_def) []
    apply (auto simp: R_def R'_def) []
    apply (auto simp: R_def R'_def) []
    apply (auto simp: R_def R'_def) []
    apply (auto simp: R_def R'_def) []
    apply (auto simp: R_def R'_def) []
    apply (auto simp: R_def R'_def) []
    apply (auto simp: R_def R'_def) []
    apply (auto simp: R_def R'_def) []
    apply (refine_rcg, rprems, (fastforce simp: R_def R'_def)+) []
    apply (fastforce simp: R'_def) []
    apply (refine_rcg, rprems, (fastforce simp: R_def R'_def)+) []
    apply (refine_rcg, rprems, (fastforce simp: R_def R'_def)+) []
    done
qed


thm create_graph_def
definition "create_graph_aimpl φ = do {
  (_, nds) 
  expand_aimpl
   (name = expand_new_name expand_init, incoming = {expand_init},
       new = {φ}, old = {}, next = {},
    {});
  RETURN nds
}"

lemma create_graph_aimpl_refine: "create_graph_aimpl φ  Id (create_graphT φ)"
  unfolding create_graph_aimpl_def create_graphT_def
  apply (refine_rcg expand_aimpl_refine)
  apply auto
  done

subsubsection ‹Creation of GBA from Nodes›

text ‹
  We summarize creation of the GBA and renaming of the nodes into one step
›
lemma create_name_gba_alt: "create_name_gba φ = do {
  nds  create_graphT φ;
  ASSERT (nds_invars nds);
  RETURN (gba_rename_ext (λ_. ()) name (create_gba_from_nodes φ nds))
  }"
proof -
  have [simp]: "nds. g_V (create_gba_from_nodes φ nds) = nds"
    by (auto simp: create_gba_from_nodes_def)

  show ?thesis
    unfolding create_name_gba_def create_gba_def
    by simp
qed

text ‹In the following, we implement the componenents of the
  renamed GBA separately.
›

text ‹\paragraph{Successor Function}›

definition "build_succ nds = 
  FOREACH 
    nds (λq' s.
    FOREACH
      (incoming q') (λqn s. 
        if qn=expand_init then 
          RETURN s 
        else 
          RETURN (s(qn  insert (name q') (the_default {} (s qn))))
    ) s
  ) Map.empty"

lemma build_succ_aux1:
  assumes [simp]: "finite nds"
  assumes [simp]: "q. qnds  finite (incoming q)"
  shows "build_succ nds  SPEC (λr. r = (λqn. 
  dflt_None_set {qn'. q'. 
    q'nds  qn' = name q'  qnincoming q'  qnexpand_init 
  }))"
  unfolding build_succ_def
  apply (refine_rcg refine_vcg 
    FOREACH_rule[where
      I="λit s. s = (λqn. dflt_None_set {qn'. q'. q'nds-it  qn' = name q' 
     qnincoming q'  qnexpand_init })"])

  apply (simp_all add: dflt_None_set_def) [2]
  apply (rename_tac q' it s)
  apply (rule_tac I="λit2 s. s = 
    (λqn. dflt_None_set (
      {qn'. q'. q'nds-it  qn' = name q'  qnincoming q'  qnexpand_init }  
      {qn' . qn'=name q'  qnincoming q' - it2  qnexpand_init} ))" 
    in FOREACH_rule)

  apply auto []

  apply (simp_all add: dflt_None_set_def)

  apply (refine_rcg refine_vcg)
  apply (auto simp: dflt_None_set_def intro!: ext) []
  apply (rule ext, (auto) [])+
  done

lemma build_succ_aux2:
  assumes NINIT: "expand_init  name`nds"
  assumes CL: "nd. ndnds  incoming nd  insert expand_init (name`nds)"
  shows
  "(λqn. dflt_None_set 
    {qn'. q'. q'nds  qn' = name q'  qnincoming q'  qnexpand_init }) 
  = (λqn. dflt_None_set (succ_of_E 
       (rename_E name {(q, q'). q  nds  q'  nds  name q  incoming q'}) qn))" 
  (is "(λqn. dflt_None_set (?L qn)) = (λqn. dflt_None_set (?R qn))")
  apply (intro ext)
  apply (fo_rule arg_cong)
proof (intro ext equalityI subsetI)
  fix qn x
  assume "x?R qn"
  then show "x?L qn" using NINIT
    by (force simp: succ_of_E_def)
next
  fix qn x
  assume XL: "x?L qn"
  show "x?R qn"
  proof (cases "qn = expand_init")
    case False
    from XL obtain q' where 
      A: "q'nds" "qnincoming q'" 
      and [simp]: "x=name q'" 
      by auto
    from False obtain q where B: "qnds" and [simp]: "qn = name q"
      using CL A by auto

    from A B show "x?R qn"
      by (auto simp: succ_of_E_def image_def)
  next
    case [simp]: True
    from XL show "x?R qn" by simp
  qed
qed

lemma build_succ_correct:
  assumes NINIT: "expand_init  name`nds"
  assumes FIN: "finite nds"
  assumes CL: "nd. ndnds  incoming nd  insert expand_init (name`nds)"
  shows "build_succ nds  SPEC (λr. 
    E_of_succ (λqn. the_default {} (r qn)) 
    = rename_E (λu. name u) {(q, q'). q  nds  q'  nds  name q  incoming q'})"
proof -
  from FIN CL have FIN': "q. qnds  finite (incoming q)"
    by (metis finite_imageI finite_insert infinite_super)
  
  note build_succ_aux1[OF FIN FIN']
  also note build_succ_aux2[OF NINIT CL]
  finally show ?thesis
    by (rule order_trans) auto
qed

text ‹\paragraph{ Accepting Sets}›

primrec until_frmlsr :: "'a frml  ('a frml × 'a frml) set" where
  "until_frmlsr (μ andr ψ) = (until_frmlsr μ)  (until_frmlsr ψ)"
| "until_frmlsr (Xr μ) = until_frmlsr μ"
| "until_frmlsr (μ Ur ψ) = insert (μ, ψ) ((until_frmlsr μ)  (until_frmlsr ψ))"
| "until_frmlsr (μ Rr ψ) = (until_frmlsr μ)  (until_frmlsr ψ)"
| "until_frmlsr (μ orr ψ) = (until_frmlsr μ)  (until_frmlsr ψ)"
| "until_frmlsr (truer) = {}"
| "until_frmlsr (falser) = {}"
| "until_frmlsr (propr(_)) = {}"
| "until_frmlsr (npropr(_)) = {}"

lemma until_frmlsr_correct: 
  "until_frmlsr φ = {(μ, η). Until_ltlr μ η  subfrmlsr φ}"
  by (induct φ) auto


definition "build_F nds φ 
   (λ(μ,η). name ` {q  nds. (Until_ltlr μ η  old q  η  old q)}) `
    until_frmlsr φ"

lemma build_F_correct: "build_F nds φ = 
  {name ` A |A. μ η. A = {q  nds. Until_ltlr μ η  old q  η  old q} 
                     Until_ltlr μ η  subfrmlsr φ}"
proof -
  have "{name ` A |A. μ η. A = {q  nds. Until_ltlr μ η  old q  η  old q} 
                     Until_ltlr μ η  subfrmlsr φ}
    = (λ(μ,η). name`{qnds. Until_ltlr μ η  old q  η  old q}) 
      ` {(μ, η). Until_ltlr μ η  subfrmlsr φ}"
    by auto
  also have " = (λ(μ,η). name`{qnds. Until_ltlr μ η  old q  η  old q}) 
      ` until_frmlsr φ"
    unfolding until_frmlsr_correct ..
  finally show ?thesis
    unfolding build_F_def by simp
qed

text ‹\paragraph{ Labeling Function }›
definition "pn_props ps  FOREACHi 
  (λit (P,N). P = {p. Prop_ltlr p  ps - it}  N = {p. Nprop_ltlr p  ps - it}) 
  ps (λp (P,N). 
    case p of Prop_ltlr p  RETURN (insert p P,N)
    | Nprop_ltlr p  RETURN (P, insert p N)
    | _  RETURN (P,N)
  ) ({},{})"

lemma pn_props_correct: 
  assumes [simp]: "finite ps"
  shows "pn_props ps  SPEC(λr. r = 
  ({p. Prop_ltlr p  ps}, {p. Nprop_ltlr p  ps}))"
  unfolding pn_props_def
  apply (refine_rcg refine_vcg)
  apply (auto split: ltlr.split)
  done

definition "pn_map nds  FOREACH nds 
  (λnd m. do {
    PN  pn_props (old nd);
    RETURN (m(name nd  PN))
  }) Map.empty"

lemma pn_map_correct: 
  assumes [simp]: "finite nds"
  assumes FIN': "nd. ndnds  finite (old nd)"
  assumes INJ: "inj_on name nds"
  shows "pn_map nds  SPEC (λr. qn. 
    case r qn of 
      None  qn  name`nds
    | Some (P,N)  qn  name`nds 
       P = {p. Prop_ltlr p  old (the_inv_into nds name qn)}
       N = {p. Nprop_ltlr p  old (the_inv_into nds name qn)}
  )"
  unfolding pn_map_def
  apply (refine_rcg refine_vcg
    FOREACH_rule[where I="λit r. qn. 
      case r qn of 
        None  qn  name`(nds - it)
      | Some (P,N)  qn  name`(nds - it)
         P = {p. Prop_ltlr p  old (the_inv_into nds name qn)}
         N = {p. Nprop_ltlr p  old (the_inv_into nds name qn)}"]
    order_trans[OF pn_props_correct]
  )
  apply simp_all
  apply (blast dest: subsetD[THEN FIN']) []
  apply (force 
    split: option.splits 
    simp: the_inv_into_f_f[OF INJ] it_step_insert_iff) []
  apply (fastforce split: option.splits) []
  done

 
text ‹\paragraph{ Assembling the Implementation }›
  
definition "cr_rename_gba nds φ  do {
  let V = name ` nds;
  let V0 = name ` {q  nds. expand_init  incoming q};
  succmap  build_succ nds;
  let E = E_of_succ (the_default {} o succmap);
  let F = build_F nds φ;
  pnm  pn_map nds;
  let L = (λqn l. case pnm qn of 
      None  False 
    | Some (P,N)  (pP. p(l:::rIdfun_set_rel))  (pN. pl)
  );
  RETURN ( g_V = V, g_E=E, g_V0=V0, gbg_F = F, gba_L = L )
}"

lemma cr_rename_gba_refine:
  assumes INV: "nds_invars nds"
  assumes REL[simplified]: "(nds',nds)Id" "(φ',φ)Id"
  shows "cr_rename_gba nds' φ' 
   Id (RETURN (gba_rename_ext (λ_. ()) name (create_gba_from_nodes φ nds)))"
  unfolding RETURN_SPEC_conv
proof (rule Id_SPEC_refine)
  from INV have
    NINIT: "expand_init  name`nds"
    and FIN: "finite nds"
    and FIN': "nd. ndnds  finite (old nd)"
    and CL: "nd. ndnds  incoming nd  insert expand_init (name`nds)"
    and INJ: "inj_on name nds"
    unfolding nds_invars_def by auto
  show "cr_rename_gba nds' φ'
     SPEC (λx. x = gba_rename_ext (λ_. ()) name (create_gba_from_nodes φ nds))"
    unfolding REL
    unfolding cr_rename_gba_def
    apply (refine_rcg refine_vcg
      order_trans[OF build_succ_correct[OF NINIT FIN CL]]
      order_trans[OF pn_map_correct[OF FIN FIN' INJ]]
    )
    unfolding gba_rename_ecnv_def gb_rename_ecnv_def 
      fr_rename_ext_def create_gba_from_nodes_def
    apply simp
    apply (intro conjI)
    apply (simp add: comp_def)
    apply (simp add: build_F_correct)
    apply (intro ext)
    apply (drule_tac x=qn in spec)
    apply (auto simp: the_inv_into_f_f[OF INJ] split: option.split prod.split)
    done
qed

definition "create_name_gba_aimpl φ  do {
  nds  create_graph_aimpl φ;
  ASSERT (nds_invars nds);
  cr_rename_gba nds φ
}"


lemma create_name_gba_aimpl_refine: 
  "create_name_gba_aimpl φ  Id (create_name_gba φ)"
  unfolding create_name_gba_aimpl_def create_name_gba_alt
  apply (refine_rcg create_graph_aimpl_refine cr_rename_gba_refine)
  by auto

subsection ‹Refinement to Efficient Data Structures›

subsubsection ‹Creation of GBA from Nodes›

schematic_goal until_frmlsr_impl_aux:
  assumes [relator_props, simp]: "R=Id"
  shows "(?c,until_frmlsr) 
   (R::(_×_::linorder) set)ltlr_rel  Rltlr_rel ×r Rltlr_reldflt_rs_rel"
  unfolding until_frmlsr_def
  apply (autoref (keep_goal, trace))
  done
concrete_definition until_frmlsr_impl uses until_frmlsr_impl_aux
lemmas [autoref_rules] = until_frmlsr_impl.refine[OF PREFER_id_D]




schematic_goal build_succ_impl_aux:
  shows "(?c,build_succ)  
    Rm,Rnode_rellist_set_rel 
     nat_rel,nat_rellist_set_reliam_map_relnres_rel"
  unfolding build_succ_def[abs_def] expand_init_def
  using [[autoref_trace_failed_id]]
  apply (autoref (keep_goal, trace))
  done

concrete_definition build_succ_impl uses build_succ_impl_aux
lemmas [autoref_rules] = build_succ_impl.refine

(* TODO: Post-processing should be on by default! *)
schematic_goal build_succ_code_aux: "RETURN ?c  build_succ_impl x"
  unfolding build_succ_impl_def
  apply (refine_transfer (post))
  done

concrete_definition build_succ_code uses build_succ_code_aux
lemmas [refine_transfer] = build_succ_code.refine




schematic_goal build_F_impl_aux:
  assumes [relator_props]:  "R = Id"
  shows "(?c,build_F)  
    Rm,Rnode_rellist_set_rel  Rltlr_rel  nat_rellist_set_rellist_set_rel"
  unfolding build_F_def[abs_def]
  using [[autoref_trace_failed_id]]
  apply (autoref (keep_goal, trace))
  done

concrete_definition build_F_impl uses build_F_impl_aux
lemmas [autoref_rules] = build_F_impl.refine[OF PREFER_id_D]




schematic_goal pn_map_impl_aux:
  shows "(?c,pn_map)  
    Rm,Idnode_rellist_set_rel 
     nat_rel,Idlist_set_rel ×r Idlist_set_reliam_map_relnres_rel"
  unfolding pn_map_def[abs_def] pn_props_def
  using [[autoref_trace_failed_id]]
  apply (autoref (keep_goal, trace))
  done

concrete_definition pn_map_impl uses pn_map_impl_aux
lemma pn_map_impl_autoref[autoref_rules]: 
  assumes "PREFER_id R"
  shows "(pn_map_impl,pn_map)  
    Rm,Rnode_rellist_set_rel 
     nat_rel,Rlist_set_rel ×r Rlist_set_reliam_map_relnres_rel"
  using assms pn_map_impl.refine by simp

schematic_goal pn_map_code_aux: "RETURN ?c  pn_map_impl x"
  unfolding pn_map_impl_def
  apply (refine_transfer (post))
  done
concrete_definition pn_map_code uses pn_map_code_aux
lemmas [refine_transfer] = pn_map_code.refine 

schematic_goal cr_rename_gba_impl_aux:
  assumes ID[relator_props]: "R=Id"
  notes [autoref_tyrel del] = tyrel_dflt_linorder_set
  notes [autoref_tyrel] = ty_REL[of "nat_rellist_set_rel"]
  shows "(?c,cr_rename_gba)  
    Rm,Rnode_rellist_set_rel  Rltlr_rel  (?R::(?'c × _) set)"
  unfolding ID
  unfolding cr_rename_gba_def[abs_def] expand_init_def comp_def
  using [[autoref_trace_failed_id]]
  apply (autoref (keep_goal, trace))
  done
concrete_definition cr_rename_gba_impl uses cr_rename_gba_impl_aux

thm cr_rename_gba_impl.refine

lemma cr_rename_gba_autoref[autoref_rules]:
  assumes "PREFER_id R"
  shows "(cr_rename_gba_impl, cr_rename_gba)  
    Rm, Rnode_rellist_set_rel  Rltlr_rel 
    gbav_impl_rel_ext unit_rel nat_rel (Rfun_set_rel)nres_rel"
  using assms cr_rename_gba_impl.refine[of R Rm] by simp


schematic_goal cr_rename_gba_code_aux: "RETURN ?c  cr_rename_gba_impl x y"
  unfolding cr_rename_gba_impl_def
  apply (refine_transfer (post))
  done
concrete_definition cr_rename_gba_code uses cr_rename_gba_code_aux
lemmas [refine_transfer] = cr_rename_gba_code.refine 


subsubsection ‹Creation of Graph›

text ‹
  The implementation of the node-set. The relation enforces that there are no
  different nodes with the same name. This effectively establishes an additional
  invariant, made explicit by an assertion in the refined program. This invariant
  allows for a more efficient implementation.
›
definition ls_nds_rel_def_internal: 
  "ls_nds_rel R  Rlist_set_rel  {(_,s). inj_on name s}"
lemma ls_nds_rel_def: "Rls_nds_rel = Rlist_set_rel  {(_,s). inj_on name s}"
  by (simp add: relAPP_def ls_nds_rel_def_internal)

lemmas [autoref_rel_intf] = REL_INTFI[of ls_nds_rel i_set]

lemma ls_nds_rel_sv[relator_props]: 
  assumes "single_valued R" 
  shows "single_valued (Rls_nds_rel)"
  using list_set_rel_sv[OF assms]
  unfolding ls_nds_rel_def
  by (metis inf.cobounded1 single_valued_subset)

context begin interpretation autoref_syn .
lemma lsnds_empty_autoref[autoref_rules]:
  assumes "PREFER_id R"
  shows "([],{})Rls_nds_rel"
  using assms
  apply (simp add: ls_nds_rel_def)
  by autoref

lemma lsnds_insert_autoref[autoref_rules]:
  assumes "SIDE_PRECOND (name n  name`ns)"
  assumes "(n',n)R"
  assumes "(ns',ns)Rls_nds_rel"
  shows "(n'#ns',(OP insert ::: R  Rls_nds_rel  Rls_nds_rel)$n$ns)
    Rls_nds_rel"
  using assms
  unfolding ls_nds_rel_def
  apply simp
proof (elim conjE, rule conjI)
  assume [autoref_rules]: "(n', n)  R" "(ns', ns)  Rlist_set_rel"
  assume "name n  name ` ns"
    and "inj_on name ns"
  then have "n  ns" by (auto)
  then show "(n' # ns', insert n ns)  Rlist_set_rel"
    by autoref
qed auto

lemma ls_nds_image_autoref_aux:
  assumes [autoref_rules]: "(fi,f)  Ra  Rb"
  assumes "(l,s)  Rals_nds_rel"
  assumes [simp]: "x. name (f x) = name x"
  shows "(map fi l, f`s)  Rbls_nds_rel"
proof -
  from assms have 
    [autoref_rules]: "(l,s)Ralist_set_rel" 
      and INJ: "(inj_on name s)"
    by (auto simp add: ls_nds_rel_def)
  
  have [simp]: "inj_on f s"
    by (rule inj_onI) (metis INJ assms(3) inj_on_eq_iff)

  have "(map fi l, f`s)  Rblist_set_rel"
    by (autoref (keep_goal))
  moreover have "inj_on name (f`s)"
    apply (rule inj_onI)
    apply (auto simp: image_iff dest: inj_onD[OF INJ])
    done
  ultimately show ?thesis
    by (auto simp: ls_nds_rel_def)
qed  

lemma ls_nds_image_autoref[autoref_rules]:
  assumes "(fi,f)  Ra  Rb"
  assumes "SIDE_PRECOND (x. name (f x) = name x)"
  shows "(map fi, (OP (`) ::: (RaRb)  Rals_nds_rel  Rbls_nds_rel)$f) 
     Rals_nds_rel  Rbls_nds_rel"
  using assms
  unfolding autoref_tag_defs
  using ls_nds_image_autoref_aux
  by blast

lemma list_set_autoref_to_list[autoref_ga_rules]: 
  shows "is_set_to_sorted_list (λ_ _. True) R ls_nds_rel id"
  unfolding is_set_to_list_def is_set_to_sorted_list_def ls_nds_rel_def
    it_to_sorted_list_def list_set_rel_def br_def
  by auto


end

context begin interpretation autoref_syn .
lemma [autoref_itype]:
  "upd_incoming 
    ::i Im, Iii_node i Im', Iii_nodeii_set i Im', Iii_nodeii_set"
  by simp
end

term upd_incoming
schematic_goal upd_incoming_impl_aux:
  assumes "REL_IS_ID R"
  shows "(?c, upd_incoming)Rm1,Rnode_rel 
   Rm2,Rnode_rells_nds_rel 
   Rm2,Rnode_rells_nds_rel"
  using assms apply simp
  unfolding upd_incoming_def[abs_def]
  using [[autoref_trace_failed_id]]
  apply (autoref (keep_goal))
  done

concrete_definition upd_incoming_impl uses upd_incoming_impl_aux
lemmas [autoref_rules] = upd_incoming_impl.refine[OF PREFER_D[of REL_IS_ID]]


schematic_goal expand_impl_aux: "(?c, expand_aimpl)  
  unit_rel,Idnode_rel ×r unit_rel,Idnode_rells_nds_rel 
   nat_rel ×r unit_rel,Idnode_rells_nds_relnres_rel"
  unfolding expand_aimpl_def[abs_def] expand_new_name_def
  using [[autoref_trace_failed_id, autoref_trace_intf_unif]]
  apply (autoref (trace,keep_goal))
  done

concrete_definition expand_impl uses expand_impl_aux

context begin interpretation autoref_syn .
lemma [autoref_itype]: "expandT 
  ::i i_unit, Iii_node, i_unit, Iii_nodeii_setii_prod 
  i i_nat,i_unit, Iii_nodeii_setii_prodii_nres" by simp

lemma expand_autoref[autoref_rules]:
  assumes ID: "PREFER_id R"
  assumes A: "(n_ns', n_ns) 
     unit_rel,Rnode_rel ×r unit_rel,Rnode_rellist_set_rel"
  assumes B: "SIDE_PRECOND (
    let (n,ns)=n_ns in inj_on name ns  (n'ns. name n > name n')
  )"
  shows "(expand_impl n_ns', 
    (OP expand_aimpl
    ::: unit_rel,Rnode_rel ×r unit_rel,Rnode_rellist_set_rel 
     nat_rel ×r unit_rel,Rnode_rellist_set_relnres_rel)$n_ns) 
   nat_rel ×r unit_rel,Rnode_rellist_set_relnres_rel"
proof simp
  from ID A B have 
    1: "(n_ns, n_ns)  Id  {(_,(n,ns)). n'ns. name n > name n'}"
    and 2: "(n_ns', n_ns) 
       unit_rel,Idnode_rel ×r unit_rel,Idnode_rells_nds_rel"
    unfolding ls_nds_rel_def
    apply -
    apply auto []
    apply (cases n_ns')
    apply auto []
    done

  have [simp]: "single_valued (nat_rel ×r unit_rel, Idnode_rellist_set_rel)"
    by tagged_solver


  have [relator_props]: "R. single_valued (Id  R)"
    by (metis IntE single_valuedD single_valuedI single_valued_Id)
    
  have [simp]: "single_valued ((nat_rel ×r unit_rel, Idnode_rells_nds_rel) O
                          (Id  {(_, n, ns). n'ns. name n' < n}))"
    by (tagged_solver)
    
  from expand_impl.refine[THEN fun_relD, OF 2, THEN nres_relD]
  show "(expand_impl n_ns', expand_aimpl n_ns)
     nat_rel ×r unit_rel, Rnode_rellist_set_relnres_rel"
    apply -
    apply (rule nres_relI)
    using ID
    apply (simp add: pw_le_iff refine_pw_simps)
    apply (fastforce simp: ls_nds_rel_def)
    done
qed

end


schematic_goal expand_code_aux: "RETURN ?c  expand_impl n_ns"
  unfolding expand_impl_def
  by (refine_transfer the_resI)
concrete_definition expand_code uses expand_code_aux
prepare_code_thms expand_code_def
lemmas [refine_transfer] = expand_code.refine 


schematic_goal create_graph_impl_aux: 
  assumes ID: "R=Id"
  shows "(?c, create_graph_aimpl) 
     Rltlr_rel  unit_rel,Rnode_rellist_set_relnres_rel"
  unfolding ID
  unfolding create_graph_aimpl_def[abs_def] expand_init_def expand_new_name_def
  using [[autoref_trace_failed_id]]
  apply (autoref (keep_goal))
  done
concrete_definition create_graph_impl uses create_graph_impl_aux

lemmas [autoref_rules] = create_graph_impl.refine[OF PREFER_id_D]

schematic_goal create_graph_code_aux: "RETURN ?c  create_graph_impl φ" 
  unfolding create_graph_impl_def
  by refine_transfer
concrete_definition create_graph_code uses create_graph_code_aux
lemmas [refine_transfer] = create_graph_code.refine


schematic_goal create_name_gba_impl_aux: 
  "(?c, (create_name_gba_aimpl:: 'a::linorder ltlr  _)) 
   Idltlr_rel  (?R::(?'c×_) set)"
  unfolding create_name_gba_aimpl_def[abs_def]
  using [[autoref_trace_failed_id]]
  apply (autoref (keep_goal, trace))
  done
concrete_definition create_name_gba_impl uses create_name_gba_impl_aux

lemma create_name_gba_autoref[autoref_rules]:
  assumes "PREFER_id R"
  shows
  "(create_name_gba_impl, create_name_gba)
   Rltlr_rel  gbav_impl_rel_ext unit_rel nat_rel (Rfun_set_rel)nres_rel" 
  (is "_:_?Rnres_rel")
proof (intro fun_relI nres_relI)
  fix φ φ'
  assume A: "(φ,φ')Rltlr_rel"
  from assms have RID[simp]: "R=Id" by simp
    
  note create_name_gba_impl.refine[THEN fun_relD,THEN nres_relD, OF A[unfolded RID]]
  also note create_name_gba_aimpl_refine
  finally show "create_name_gba_impl φ   ?R (create_name_gba φ')" by simp
qed
 
schematic_goal create_name_gba_code_aux: "RETURN ?c  create_name_gba_impl φ" 
  unfolding create_name_gba_impl_def
  by (refine_transfer (post))
concrete_definition create_name_gba_code uses create_name_gba_code_aux
lemmas [refine_transfer] = create_name_gba_code.refine

schematic_goal create_name_igba_impl_aux: 
  assumes RID: "R=Id"
  shows "(?c,create_name_igba)
  Rltlr_rel  igbav_impl_rel_ext unit_rel nat_rel (Rfun_set_rel)nres_rel"
  unfolding RID
  unfolding create_name_igba_def[abs_def]
  using [[autoref_trace_failed_id]]
  apply (autoref (trace, keep_goal))
  done
concrete_definition create_name_igba_impl uses create_name_igba_impl_aux
lemmas [autoref_rules] = create_name_igba_impl.refine[OF PREFER_id_D]

schematic_goal create_name_igba_code_aux: "RETURN ?c  create_name_igba_impl φ" 
  unfolding create_name_igba_impl_def
  by (refine_transfer (post))
concrete_definition create_name_igba_code uses create_name_igba_code_aux
lemmas [refine_transfer] = create_name_igba_code.refine

export_code create_name_igba_code checking SML

end