Session CAVA_Automata

Theory Digraph_Basic

section ‹Relations interpreted as Directed Graphs›
theory Digraph_Basic
imports   
  "Automatic_Refinement.Misc"
  "Automatic_Refinement.Refine_Util"
  "HOL-Library.Omega_Words_Fun"
begin

text ‹
  This theory contains some basic graph theory on directed graphs which are 
  modeled as a relation between nodes. 

  The theory here is very fundamental, and 
  also used by non-directly graph-related applications like the theory of 
  tail-recursion in the Refinement Framework. Thus, we decided to put it 
  in the basic theories of the refinement framework.
›


text ‹Directed graphs are modeled as a relation on nodes›
type_synonym 'v digraph = "('v×'v) set"

locale digraph = fixes E :: "'v digraph"

subsection ‹Paths›
text ‹Path are modeled as list of nodes, the last node of a path is not included
  into the list. This formalization allows for nice concatenation and splitting
  of paths.›
inductive path :: "'v digraph  'v  'v list  'v  bool" for E where
  path0: "path E u [] u"
| path_prepend: " (u,v)E; path E v l w   path E u (u#l) w"

lemma path1: "(u,v)E  path E u [u] v"
  by (auto intro: path.intros)

lemma path_empty_conv[simp]:
  "path E u [] v  u=v"
  by (auto intro: path0 elim: path.cases)

inductive_cases path_uncons: "path E u (u'#l) w"
inductive_simps path_cons_conv: "path E u (u'#l) w"

lemma path_no_edges[simp]: "path {} u p v  (u=v  p=[])"
  by (cases p) (auto simp: path_cons_conv)

lemma path_conc: 
  assumes P1: "path E u la v" 
  assumes P2: "path E v lb w"
  shows "path E u (la@lb) w"
  using P1 P2 apply induct 
  by (auto intro: path.intros)
  
lemma path_append:
  " path E u l v; (v,w)E   path E u (l@[v]) w"
  using path_conc[OF _ path1] .

lemma path_unconc:
  assumes "path E u (la@lb) w"
  obtains v where "path E u la v" and "path E v lb w"
  using assms 
  thm path.induct
  apply (induct u "la@lb" w arbitrary: la lb rule: path.induct)
  apply (auto intro: path.intros elim!: list_Cons_eq_append_cases)
  done

lemma path_conc_conv: 
  "path E u (la@lb) w  (v. path E u la v  path E v lb w)"
  by (auto intro: path_conc elim: path_unconc)

lemma (in -) path_append_conv: "path E u (p@[v]) w  (path E u p v  (v,w)E)"
  by (simp add: path_cons_conv path_conc_conv)

lemmas path_simps = path_empty_conv path_cons_conv path_conc_conv


lemmas path_trans[trans] = path_prepend path_conc path_append
lemma path_from_edges: "(u,v)E; (v,w)E  path E u [u] v" 
  by (auto simp: path_simps)


lemma path_edge_cases[case_names no_use split]: 
  assumes "path (insert (u,v) E) w p x"
  obtains 
    "path E w p x" 
  | p1 p2 where "path E w p1 u" "path (insert (u,v) E) v p2 x"
  using assms
  apply induction
  apply simp
  apply (clarsimp)
  apply (metis path_simps path_cons_conv)
  done

lemma path_edge_rev_cases[case_names no_use split]: 
  assumes "path (insert (u,v) E) w p x"
  obtains 
    "path E w p x" 
  | p1 p2 where "path (insert (u,v) E) w p1 u" "path E v p2 x"
  using assms
  apply (induction p arbitrary: x rule: rev_induct)
  apply simp
  apply (clarsimp simp: path_cons_conv path_conc_conv)
  apply (metis path_simps path_append_conv)
  done


lemma path_mono: 
  assumes S: "EE'" 
  assumes P: "path E u p v" 
  shows "path E' u p v"
  using P
  apply induction
  apply simp
  using S
  apply (auto simp: path_cons_conv)
  done

lemma path_is_rtrancl: 
  assumes "path E u l v"
  shows "(u,v)E*"
  using assms 
  by induct auto

lemma rtrancl_is_path:
  assumes "(u,v)E*"
  obtains l where "path E u l v"
  using assms 
  by induct (auto intro: path0 path_append)

lemma path_is_trancl: 
  assumes "path E u l v"
  and "l[]"
  shows "(u,v)E+"
  using assms 
  apply induct
  apply auto []
  apply (case_tac l)
  apply auto
  done

lemma trancl_is_path:
  assumes "(u,v)E+"
  obtains l where "l[]" and "path E u l v"
  using assms 
  by induct (auto intro: path0 path_append)

lemma path_nth_conv: "path E u p v  (let p'=p@[v] in
  u=p'!0 
  (i<length p' - 1. (p'!i,p'!Suc i)E))"
  apply (induct p arbitrary: v rule: rev_induct)
  apply (auto simp: path_conc_conv path_cons_conv nth_append)
  done

lemma path_mapI:
  assumes "path E u p v"
  shows "path (pairself f ` E) (f u) (map f p) (f v)"
  using assms
  apply induction
  apply (simp)
  apply (force simp: path_cons_conv)
  done

lemma path_restrict: 
  assumes "path E u p v" 
  shows "path (E  set p × insert v (set (tl p))) u p v"
  using assms
proof induction
  print_cases
  case (path_prepend u v p w)
  from path_prepend.IH have "path (E  set (u#p) × insert w (set p)) v p w"
    apply (rule path_mono[rotated])
    by (cases p) auto
  thus ?case using (u,v)E
    by (cases p) (auto simp add: path_cons_conv)
qed auto

lemma path_restrict_closed:
  assumes CLOSED: "E``D  D"
  assumes I: "vD" and P: "path E v p v'"
  shows "path (ED×D) v p v'"
  using P CLOSED I
  by induction (auto simp: path_cons_conv)


lemma path_set_induct:
  assumes "path E u p v" and "uI" and "E``I  I"
  shows "set p  I"
  using assms
  by (induction rule: path.induct) auto

lemma path_nodes_reachable: "path E u p v  insert v (set p)  E*``{u}"
  apply (auto simp: in_set_conv_decomp path_cons_conv path_conc_conv)
  apply (auto dest!: path_is_rtrancl)
  done

lemma path_nodes_edges: "path E u p v  set p  fst`E"
  by (induction rule: path.induct) auto

lemma path_tl_nodes_edges: 
  assumes "path E u p v"
  shows "set (tl p)  fst`E  snd`E"
proof -
  from path_nodes_edges[OF assms] have "set (tl p)  fst`E"
    by (cases p) auto

  moreover have "set (tl p)  snd`E"
    using assms
    apply (cases)
    apply simp
    apply simp
    apply (erule path_set_induct[where I = "snd`E"])
    apply auto
    done
  ultimately show ?thesis
    by auto
qed

lemma path_loop_shift: 
  assumes P: "path E u p u"
  assumes S: "vset p"
  obtains p' where "set p' = set p" "path E v p' v"
proof -
  from S obtain p1 p2 where [simp]: "p = p1@v#p2" by (auto simp: in_set_conv_decomp)
  from P obtain v' where A: "path E u p1 v" "(v, v')  E" "path E v' p2 u" 
    by (auto simp: path_simps)
  hence "path E v (v#p2@p1) v" by (auto simp: path_simps)
  thus ?thesis using that[of "v#p2@p1"] by auto
qed

lemma path_hd:
  assumes "p  []" "path E v p w"
  shows "hd p = v"
  using assms
  by (auto simp: path_cons_conv neq_Nil_conv)


lemma path_last_is_edge:
  assumes "path E x p y"
  and "p  []"
  shows "(last p, y)  E"
  using assms
  by (auto simp: neq_Nil_rev_conv path_simps)

lemma path_member_reach_end:
  assumes P: "path E x p y"
  and v: "v  set p"
  shows "(v,y)  E+"
  using assms 
  by (auto intro!: path_is_trancl simp: in_set_conv_decomp path_simps)

lemma path_tl_induct[consumes 2, case_names single step]:
  assumes P: "path E x p y"
  and NE: "x  y"
  and S: "u. (x,u)  E  P x u"
  and ST: "u v. (x,u)  E+; (u,v)  E; P x u  P x v"
  shows "P x y  ( v  set (tl p). P x v)"
proof -
  from P NE have "p  []" by auto
  thus ?thesis using P
  proof (induction p arbitrary: y rule: rev_nonempty_induct)
    case (single u) hence "(x,y)  E" by (simp add: path_cons_conv)
    with S show ?case by simp
  next
    case (snoc u us) hence "path E x us u" by (simp add: path_append_conv)
    with snoc path_is_trancl have 
      "P x u" "(x,u)  E+" "v  set (tl us). P x v" 
      by simp_all
    moreover with snoc have "v  set (tl (us@[u])). P x v" by simp
    moreover from snoc have "(u,y)  E" by (simp add: path_append_conv)
    ultimately show ?case by (auto intro: ST)
  qed
qed


lemma path_restrict_tl: 
  " uR; path (E  UNIV × -R) u p v   path (rel_restrict E R) u p v"
  apply (induction p arbitrary: u)
  apply (auto simp: path_simps rel_restrict_def)
  done

lemma path1_restr_conv: "path (EUNIV × -R) u (x#xs) v 
   (w. wR  x=u  (u,w)E  path (rel_restrict E R) w xs v)"
proof -
  have 1: "rel_restrict E R  E  UNIV × - R" by (auto simp: rel_restrict_def)

  show ?thesis
    by (auto simp: path_simps intro: path_restrict_tl path_mono[OF 1])
qed



lemma dropWhileNot_path:
  assumes "p  []"
  and "path E w p x"
  and "v  set p"
  and "dropWhile ((≠) v) p = c"
  shows "path E v c x"
  using assms
proof (induction arbitrary: w c rule: list_nonempty_induct)
  case (single p) thus ?case by (auto simp add: path_simps)
next
  case (cons p ps) hence [simp]: "w = p" by (simp add: path_cons_conv)
  show ?case
  proof (cases "p=v")
    case True with cons show ?thesis by simp
  next
    case False with cons have "c = dropWhile ((≠) v) ps" by simp
    moreover from cons.prems obtain y where "path E y ps x" 
      using path_uncons by metis
    moreover from cons.prems False have "v  set ps" by simp
    ultimately show ?thesis using cons.IH by metis
  qed
qed

lemma takeWhileNot_path:
  assumes "p  []"
  and "path E w p x"
  and "v  set p"
  and "takeWhile ((≠) v) p = c"
  shows "path E w c v"
  using assms
proof (induction arbitrary: w c rule: list_nonempty_induct)
  case (single p) thus ?case by (auto simp add: path_simps)
next
  case (cons p ps) hence [simp]: "w = p" by (simp add: path_cons_conv)
  show ?case
  proof (cases "p=v")
    case True with cons show ?thesis by simp
  next
    case False with cons obtain c' where 
      "c' = takeWhile ((≠) v) ps" and 
      [simp]: "c = p#c'"
      by simp_all
    moreover from cons.prems obtain y where 
      "path E y ps x" and "(w,y)  E" 
      using path_uncons by metis+
    moreover from cons.prems False have "v  set ps" by simp
    ultimately have "path E y c' v" using cons.IH by metis
    with (w,y)  E show ?thesis by (auto simp add: path_cons_conv)
  qed
qed


subsection ‹Infinite Paths›
definition ipath :: "'q digraph  'q word  bool"
  ― ‹Predicate for an infinite path in a digraph›
  where "ipath E r  i. (r i, r (Suc i))E"


lemma ipath_conc_conv: 
  "ipath E (u  v)  (a. path E a u (v 0)  ipath E v)"
  apply (auto simp: conc_def ipath_def path_nth_conv nth_append)
  apply (metis add_Suc_right diff_add_inverse not_add_less1)
  by (metis Suc_diff_Suc diff_Suc_Suc not_less_eq)

lemma ipath_iter_conv:
  assumes "p[]"
  shows "ipath E (pω)  (path E (hd p) p (hd p))"
proof (cases p)
  case Nil thus ?thesis using assms by simp
next
  case (Cons u p') hence PLEN: "length p > 0" by simp
  show ?thesis proof 
    assume "ipath E (iter (p))"
    hence "i. (iter (p) i, iter (p) (Suc i))  E"
      unfolding ipath_def by simp
    hence "(i<length p. (p!i,(p@[hd p])!Suc i)E)" 
      apply (simp add: assms)
      apply safe
      apply (drule_tac x=i in spec)
      apply simp
      apply (case_tac "Suc i = length p")
      apply (simp add: Cons)
      apply (simp add: nth_append)
      done
    thus "path E (hd p) p (hd p)"
      by (auto simp: path_nth_conv Cons nth_append nth_Cons')
  next
    assume "path E (hd p) p (hd p)"
    thus "ipath E (iter p)"
      apply (auto simp: path_nth_conv ipath_def assms Let_def)
      apply (drule_tac x="i mod length p" in spec)
      apply (auto simp: nth_append assms split: if_split_asm)
      apply (metis less_not_refl mod_Suc)
      by (metis PLEN diff_self_eq_0 mod_Suc nth_Cons_0 mod_less_divisor)
  qed
qed

lemma ipath_to_rtrancl:
  assumes R: "ipath E r"
  assumes I: "i1i2"
  shows "(r i1,r i2)E*"
  using I
proof (induction i2)
  case (Suc i2)
  show ?case proof (cases "i1=Suc i2")
    assume "i1Suc i2"
    with Suc have "(r i1,r i2)E*" by auto
    also from R have "(r i2,r (Suc i2))E" unfolding ipath_def by auto
    finally show ?thesis .
  qed simp
qed simp
    
lemma ipath_to_trancl:
  assumes R: "ipath E r"
  assumes I: "i1<i2"
  shows "(r i1,r i2)E+"
proof -
  from R have "(r i1,r (Suc i1))E"
    by (auto simp: ipath_def)
  also have "(r (Suc i1),r i2)E*"
    using ipath_to_rtrancl[OF R,of "Suc i1" i2] I by auto
  finally (rtrancl_into_trancl2) show ?thesis .
qed

lemma run_limit_two_connectedI:
  assumes A: "ipath E r" 
  assumes B: "a  limit r" "blimit r"
  shows "(a,b)E+"
proof -
  from B have "{a,b}  limit r" by simp
  with A show ?thesis
    by (metis ipath_to_trancl two_in_limit_iff)
qed


lemma ipath_subpath:
  assumes P: "ipath E r"
  assumes LE: "lu"
  shows "path E (r l) (map r [l..<u]) (r u)"
  using LE
proof (induction "u-l" arbitrary: u l)
  case (Suc n)
  note IH=Suc.hyps(1)
  from ‹Suc n = u-l lu obtain u' where [simp]: "u=Suc u'" 
    and A: "n=u'-l" "l  u'" 
    by (cases u) auto
    
  note IH[OF A]
  also from P have "(r u',r u)E"
    by (auto simp: ipath_def)
  finally show ?case using l  u' by (simp add: upt_Suc_append)
qed auto  

lemma ipath_restrict_eq: "ipath (E  (E*``{r 0} × E*``{r 0})) r  ipath E r"
  unfolding ipath_def
  by (auto simp: relpow_fun_conv rtrancl_power)
lemma ipath_restrict: "ipath E r  ipath (E  (E*``{r 0} × E*``{r 0})) r"
  by (simp add: ipath_restrict_eq)


lemma ipathI[intro?]: "i. (r i, r (Suc i))  E  ipath E r"
  unfolding ipath_def by auto

lemma ipathD: "ipath E r  (r i, r (Suc i))  E"
  unfolding ipath_def by auto

lemma ipath_in_Domain: "ipath E r  r i  Domain E"
  unfolding ipath_def by auto

lemma ipath_in_Range: "ipath E r; i0  r i  Range E"
  unfolding ipath_def by (cases i) auto

lemma ipath_suffix: "ipath E r  ipath E (suffix i r)"
  unfolding suffix_def ipath_def by auto

subsection ‹Strongly Connected Components›

text ‹A strongly connected component is a maximal mutually connected set 
  of nodes›
definition is_scc :: "'q digraph  'q set  bool"
  where "is_scc E U  U×UE*  (V. VU  ¬ (V×VE*))"

lemma scc_non_empty[simp]: "¬is_scc E {}" unfolding is_scc_def by auto

lemma scc_non_empty'[simp]: "is_scc E U  U{}" unfolding is_scc_def by auto

lemma is_scc_closed: 
  assumes SCC: "is_scc E U"
  assumes MEM: "xU"
  assumes P: "(x,y)E*" "(y,x)E*"
  shows "yU"
proof -
  from SCC MEM P have "insert y U × insert y U  E*"
    unfolding is_scc_def
    apply clarsimp
    apply rule
    apply clarsimp_all
    apply (erule disjE1)
    apply clarsimp
    apply (metis in_mono mem_Sigma_iff rtrancl_trans)
    apply auto []
    apply (erule disjE1)
    apply clarsimp
    apply (metis in_mono mem_Sigma_iff rtrancl_trans)
    apply auto []
    done
  with SCC show ?thesis unfolding is_scc_def by blast
qed

lemma is_scc_connected:
  assumes SCC: "is_scc E U"
  assumes MEM: "xU" "yU"
  shows "(x,y)E*"
  using assms unfolding is_scc_def by auto

text ‹In the following, we play around with alternative characterizations, and
  prove them all equivalent .›

text ‹A common characterization is to define an equivalence relation 
  ,,mutually connected'' on nodes, and characterize the SCCs as its 
  equivalence classes:›

definition mconn :: "('a×'a) set  ('a × 'a) set"
  ― ‹Mutually connected relation on nodes›
  where "mconn E = E*  (E¯)*"

lemma mconn_pointwise:
   "mconn E = {(u,v). (u,v)E*  (v,u)E*}"
  by (auto simp add: mconn_def rtrancl_converse)

text mconn› is an equivalence relation:›
lemma mconn_refl[simp]: "Idmconn E"
  by (auto simp add: mconn_def)

lemma mconn_sym: "mconn E = (mconn E)¯"
  by (auto simp add: mconn_pointwise)

lemma mconn_trans: "mconn E O mconn E = mconn E"
  by (auto simp add: mconn_def)

lemma mconn_refl': "refl (mconn E)"
  by (auto intro: refl_onI simp: mconn_pointwise)

lemma mconn_sym': "sym (mconn E)"
  by (auto intro: symI simp: mconn_pointwise)

lemma mconn_trans': "trans (mconn E)"
  by (metis mconn_def trans_Int trans_rtrancl)

lemma mconn_equiv: "equiv UNIV (mconn E)"
  using mconn_refl' mconn_sym' mconn_trans'
  by (rule equivI)


lemma is_scc_mconn_eqclasses: "is_scc E U  U  UNIV // mconn E"
  ― ‹The strongly connected components are the equivalence classes of the 
    mutually-connected relation on nodes›
proof
  assume A: "is_scc E U"
  then obtain x where "xU" unfolding is_scc_def by auto
  hence "U = mconn E `` {x}" using A
    unfolding mconn_pointwise is_scc_def
    apply clarsimp
    apply rule
    apply auto []
    apply clarsimp
    by (metis A is_scc_closed)
  thus "U  UNIV // mconn E"
    by (auto simp: quotient_def)
next
  assume "U  UNIV // mconn E"
  thus "is_scc E U"
    by (auto simp: is_scc_def mconn_pointwise quotient_def)
qed

(* For presentation in the paper *)
lemma "is_scc E U  U  UNIV // (E*  (E¯)*)"
  unfolding is_scc_mconn_eqclasses mconn_def by simp

text ‹We can also restrict the notion of "reachability" to nodes
  inside the SCC
›

lemma find_outside_node:
  assumes "(u,v)E*"
  assumes "(u,v)(EU×U)*"
  assumes "uU" "vU"
  shows "u'. u'U  (u,u')E*  (u',v)E*"
  using assms
  apply (induction)
  apply auto []
  apply clarsimp
  by (metis IntI mem_Sigma_iff rtrancl.simps)

lemma is_scc_restrict1:
  assumes SCC: "is_scc E U"
  shows "U×U(EU×U)*"
  using assms
  unfolding is_scc_def
  apply clarsimp
  apply (rule ccontr)
  apply (drule (2) find_outside_node[rotated])
  apply auto []
  by (metis is_scc_closed[OF SCC] mem_Sigma_iff rtrancl_trans subsetD)

lemma is_scc_restrict2:
  assumes SCC: "is_scc E U"
  assumes "VU"
  shows "¬ (V×V(EV×V)*)"
  using assms
  unfolding is_scc_def
  apply clarsimp
  using rtrancl_mono[of "E  V × V" "E"]
  apply clarsimp
  apply blast
  done

lemma is_scc_restrict3: 
  assumes SCC: "is_scc E U"
  shows "((E*``((E*``U) - U))  U = {})"
  apply auto
  by (metis assms is_scc_closed is_scc_connected rtrancl_trans)
  
lemma is_scc_alt_restrict_path:
  "is_scc E U  U{} 
    (U×U  (EU×U)*)  ((E*``((E*``U) - U))  U = {})"
  apply rule
  apply (intro conjI)
  apply simp
  apply (blast dest: is_scc_restrict1)
  apply (blast dest: is_scc_restrict3)
  
  unfolding is_scc_def
  apply rule
  apply clarsimp
  apply (metis (full_types) Int_lower1 in_mono mem_Sigma_iff rtrancl_mono_mp)
  apply blast
  done

lemma is_scc_pointwise:
  "is_scc E U  
    U{}
   (uU. vU. (u,v)(EU×U)*) 
   (uU. v. (vU  (u,v)E*)  (u'U. (v,u')E*))"
  ― ‹Alternative, pointwise characterization›
  unfolding is_scc_alt_restrict_path
  by blast  

lemma is_scc_unique:
  assumes SCC: "is_scc E scc" "is_scc E scc'"
  and v: "v  scc" "v  scc'"
  shows "scc = scc'"
proof -
  from SCC have "scc = scc'  scc  scc' = {}"
    using quotient_disj[OF mconn_equiv]
    by (simp add: is_scc_mconn_eqclasses)
  with v show ?thesis by auto
qed

lemma is_scc_ex1:
  "∃!scc. is_scc E scc  v  scc"
proof (rule ex1I, rule conjI)
  let ?scc = "mconn E `` {v}"
  have "?scc  UNIV // mconn E" by (auto intro: quotientI)
  thus "is_scc E ?scc" by (simp add: is_scc_mconn_eqclasses)
  moreover show "v  ?scc" by (blast intro: refl_onD[OF mconn_refl'])
  ultimately show "scc. is_scc E scc  v  scc  scc = ?scc"
    by (metis is_scc_unique)
qed

lemma is_scc_ex:
  "scc. is_scc E scc  v  scc"
  by (metis is_scc_ex1)

lemma is_scc_connected':
  "is_scc E scc; x  scc; y  scc  (x,y)(Restr E scc)*"
  unfolding is_scc_pointwise
  by blast

definition scc_of :: "('v×'v) set  'v  'v set"
  where
  "scc_of E v = (THE scc. is_scc E scc  v  scc)"

lemma scc_of_is_scc[simp]:
  "is_scc E (scc_of E v)"
  using is_scc_ex1[of E v]
  by (auto dest!: theI' simp: scc_of_def)

lemma node_in_scc_of_node[simp]:
  "v  scc_of E v"
  using is_scc_ex1[of E v]
  by (auto dest!: theI' simp: scc_of_def)

lemma scc_of_unique:
  assumes "w  scc_of E v"
  shows "scc_of E v = scc_of E w"
proof -
  have "is_scc E (scc_of E v)" by simp
  moreover note assms
  moreover have "is_scc E (scc_of E w)" by simp
  moreover have "w  scc_of E w" by simp
  ultimately show ?thesis using is_scc_unique by metis
qed

end

Theory Digraph

section ‹Directed Graphs›
(* Author: Peter Lammich *)
theory Digraph
  imports 
  CAVA_Base.CAVA_Base
  Digraph_Basic
begin

subsection "Directed Graphs with Explicit Node Set and Set of Initial Nodes"

record 'v graph_rec = 
  g_V :: "'v set"
  g_E :: "'v digraph"  
  g_V0 :: "'v set"

definition graph_restrict :: "('v, 'more) graph_rec_scheme  'v set  ('v, 'more) graph_rec_scheme"
  where "graph_restrict G R 
  
    g_V = g_V G,
    g_E = rel_restrict (g_E G) R,
    g_V0 = g_V0 G - R,
     = graph_rec.more G
  "

lemma graph_restrict_simps[simp]:
  "g_V (graph_restrict G R) = g_V G"
  "g_E (graph_restrict G R) = rel_restrict (g_E G) R"
  "g_V0 (graph_restrict G R) = g_V0 G - R"
  "graph_rec.more (graph_restrict G R) = graph_rec.more G"
  unfolding graph_restrict_def by auto

lemma graph_restrict_trivial[simp]: "graph_restrict G {} = G" by simp

locale graph_defs =
  fixes G :: "('v, 'more) graph_rec_scheme"
begin

  abbreviation "V  g_V G"
  abbreviation "E  g_E G"
  abbreviation "V0  g_V0 G"

  abbreviation "reachable  E* `` V0"
  abbreviation "succ v  E `` {v}"

  lemma finite_V0: "finite reachable  finite V0" by (auto intro: finite_subset)

  definition is_run
    ― ‹Infinite run, i.e., a rooted infinite path›
    where "is_run r  r 0  V0  ipath E r"

  lemma run_ipath: "is_run r  ipath E r" unfolding is_run_def by auto
  lemma run_V0: "is_run r  r 0  V0" unfolding is_run_def by auto

  lemma run_reachable: "is_run r  range r  reachable"
    unfolding is_run_def using ipath_to_rtrancl by blast

end

locale graph =
  graph_defs G
  for G :: "('v, 'more) graph_rec_scheme"
  +
  assumes V0_ss: "V0  V"
  assumes E_ss: "E  V × V"
begin

  lemma reachable_V: "reachable  V" using V0_ss E_ss by (auto elim: rtrancl_induct)

  lemma finite_E: "finite V  finite E" using finite_subset E_ss by auto

end

(* TODO: finite reachability is handled using loose assumptions, while finitely branching
  graphs are captured using a locale. it may be advantageous to unify this. *)
locale fb_graph =
  graph G
  for G :: "('v, 'more) graph_rec_scheme"
  +
  assumes finite_V0[simp, intro!]: "finite V0"
  assumes finitely_branching[simp, intro]: "v  reachable  finite (succ v)"
begin

  lemma fb_graph_subset:
    assumes "g_V G' = V"
    assumes "g_E G'  E"
    assumes "finite (g_V0 G')"
    assumes "g_V0 G'  reachable"
    shows "fb_graph G'"
  proof
    show "g_V0 G'  g_V G'" using reachable_V assms(1, 4) by simp
    show "g_E G'  g_V G' × g_V G'" using E_ss assms(1, 2) by simp
    show "finite (g_V0 G')" using assms(3) by this
  next
    fix v
    assume 1: "v  (g_E G')* `` g_V0 G'"
    obtain u where 2: "u  g_V0 G'" "(u, v)  (g_E G')*" using 1 by rule
    have 3: "u  reachable" "(u, v)  E*" using rtrancl_mono assms(2, 4) 2 by auto
    have 4: "v  reachable" using rtrancl_image_advance_rtrancl 3 by metis
    have 5: "finite (E `` {v})" using 4 by rule
    have 6: "g_E G' `` {v}  E `` {v}" using assms(2) by auto
    show "finite (g_E G' `` {v})" using finite_subset 5 6 by auto
  qed

  lemma fb_graph_restrict: "fb_graph (graph_restrict G R)"
    by (rule fb_graph_subset, auto simp: rel_restrict_sub)

end

lemma (in graph) fb_graphI_fr:
  assumes "finite reachable"
  shows "fb_graph G"
proof
  from assms show "finite V0" by (rule finite_subset[rotated]) auto
  fix v
  assume "v  reachable"
  hence "succ v  reachable" by (metis Image_singleton_iff rtrancl_image_advance subsetI)
  thus "finite (succ v)" using assms by (rule finite_subset)
qed

abbreviation "rename_E f E  (λ(u,v). (f u, f v))`E"

definition "fr_rename_ext ecnv f G   
    g_V = f`(g_V G),
    g_E = rename_E f (g_E G),   
    g_V0 = (f`g_V0 G),
     = ecnv G
  "

locale g_rename_precond =
  graph G
  for G :: "('u,'more) graph_rec_scheme"
  +
  fixes f :: "'u  'v"
  fixes ecnv :: "('u, 'more) graph_rec_scheme  'more'"
  assumes INJ: "inj_on f V"
begin

  abbreviation "G'  fr_rename_ext ecnv f G"

  lemma G'_fields:
    "g_V G' = f`V"
    "g_V0 G' = f`V0"
    "g_E G' = rename_E f E"
    unfolding fr_rename_ext_def by simp_all

  definition "fi  the_inv_into V f"

  lemma 
    fi_f: "xV  fi (f x) = x" and
    f_fi: "yf`V  f (fi y) = y" and
    fi_f_eq: "f x = y; xV  fi y = x"
    unfolding fi_def
    by (auto 
      simp: the_inv_into_f_f f_the_inv_into_f the_inv_into_f_eq INJ)

  lemma E'_to_E: "(u,v)  g_E G'  (fi u, fi v)E"
    using E_ss
    by (auto simp: fi_f G'_fields)

  lemma V0'_to_V0: "vg_V0 G'  fi v  V0"
    using V0_ss
    by (auto simp: fi_f G'_fields)


  lemma rtrancl_E'_sim:
    assumes "(f u,v')(g_E G')*"
    assumes "uV"
    shows "v. v' = f v  vV  (u,v)E*"
    using assms
  proof (induction "f u" v' arbitrary: u)
    case (rtrancl_into_rtrancl v' w' u)
    then obtain v w where "v' = f v" "w' = f w" "(v,w)E"
      by (auto simp: G'_fields)
    hence "vV" "wV" using E_ss by auto
    from rtrancl_into_rtrancl obtain vv where "v' = f vv" "vvV" "(u,vv)E*"
      by blast
    from v' = f v vV› v' = f vv vvV› have [simp]: "vv = v"
      using INJ by (metis inj_on_contraD)

    note (u,vv)E*[simplified]
    also note (v,w)E›
    finally show ?case using w' = f w wV› by blast
  qed auto
    
  lemma rtrancl_E'_to_E: assumes "(u,v)(g_E G')*" shows "(fi u, fi v)E*"
    using assms apply induction
    by (fastforce intro: E'_to_E rtrancl_into_rtrancl)+

  lemma G'_invar: "graph G'"
    apply unfold_locales
  proof -
    show "g_V0 G'  g_V G'"
      using V0_ss by (auto simp: G'_fields) []

    show "g_E G'  g_V G' × g_V G'"
      using E_ss by (auto simp: G'_fields) []
  qed

  sublocale G': graph G' using G'_invar .

  lemma G'_finite_reachable:
    assumes "finite ((g_E G)* `` g_V0 G)"
    shows "finite ((g_E G')* `` g_V0 G')"
  proof -
    have "(g_E G')* `` g_V0 G'  f ` (E*``V0)"
      apply (clarsimp_all simp: G'_fields(2))
      apply (drule rtrancl_E'_sim)
      using V0_ss apply auto []
      apply auto
      done
    thus ?thesis using finite_subset assms by blast
  qed

  lemma V'_to_V: "v  G'.V  fi v  V"
    by (auto simp: fi_f G'_fields)

  lemma ipath_sim1: "ipath E r  ipath G'.E (f o r)"
    unfolding ipath_def by (auto simp: G'_fields)

  lemma ipath_sim2: "ipath G'.E r  ipath E (fi o r)"
    unfolding ipath_def 
    apply (clarsimp simp: G'_fields)
    apply (drule_tac x=i in spec)
    using E_ss
    by (auto simp: fi_f)

  lemma run_sim1: "is_run r  G'.is_run (f o r)"
    unfolding is_run_def G'.is_run_def
    apply (intro conjI)
    apply (auto simp: G'_fields) []
    apply (auto simp: ipath_sim1)
    done

  lemma run_sim2: "G'.is_run r  is_run (fi o r)"
    unfolding is_run_def G'.is_run_def
    by (auto simp: ipath_sim2 V0'_to_V0)

end


end

Theory Automata

section ‹Automata›
(* Author: Peter Lammich *)
theory Automata
imports Digraph
begin
  text ‹
    In this theory, we define Generalized Buchi Automata and Buchi Automata 
    based on directed graphs
›

hide_const (open) prod
  
subsection "Generalized Buchi Graphs"
text ‹
  A generalized Buchi graph is a graph where each node belongs to a set of
  acceptance classes. An infinite run on this graph is accepted, iff
  it visits nodes from each acceptance class infinitely often.

  The standard encoding of acceptance classes is as a set of sets of nodes,
  each inner set representing one acceptance class.
›

record 'Q gb_graph_rec = "'Q graph_rec" +
  gbg_F :: "'Q set set"


locale gb_graph =
  graph G 
  for G :: "('Q,'more) gb_graph_rec_scheme" +
  assumes finite_F[simp, intro!]: "finite (gbg_F G)"
  assumes F_ss: "gbg_F G  Pow V"
begin
  abbreviation "F  gbg_F G"

  lemma is_gb_graph: "gb_graph G" by unfold_locales


  definition 
    is_acc :: "'Q word  bool" where "is_acc r  (AF. i. r i  A)"

  definition "is_acc_run r  is_run r  is_acc r"

  (* For presentation in paper *)
  lemma "is_acc_run r  is_run r  (AF. i. r i  A)"
    unfolding is_acc_run_def is_acc_def .

  lemma acc_run_run: "is_acc_run r  is_run r"
    unfolding is_acc_run_def by simp

  lemmas acc_run_reachable = run_reachable[OF acc_run_run]


  lemma acc_eq_limit: 
    assumes FIN: "finite (range r)"  
    shows "is_acc r  (AF. limit r  A  {})"
  proof 
    assume "AF. limit r  A  {}"
    thus "is_acc r"
      unfolding is_acc_def
      by (metis limit_inter_INF)
  next
    from FIN have FIN': "A. finite (A  range r)"
      by simp

    assume "is_acc r"
    hence AUX: "AF. i. r i  (A  range r)"
      unfolding is_acc_def by auto
    have "AF. limit r  (A  range r)  {}"
      apply (rule ballI)
      apply (drule bspec[OF AUX])
      apply (subst (asm) fin_ex_inf_eq_limit[OF FIN'])
      .
    thus "AF. limit r  A  {}" 
      by auto
  qed

  lemma is_acc_run_limit_alt:
    assumes "finite (E* `` V0)"
    shows "is_acc_run r  is_run r  (AF. limit r  A  {})"
    using assms acc_eq_limit[symmetric] unfolding is_acc_run_def
    by (auto dest: run_reachable finite_subset)

  lemma is_acc_suffix[simp]: "is_acc (suffix i r)  is_acc r"
    unfolding is_acc_def suffix_def
    apply (clarsimp simp: INFM_nat)
    apply (rule iffI)
    apply (metis trans_less_add2)
    by (metis add_lessD1 less_imp_add_positive nat_add_left_cancel_less)

  lemma finite_V_Fe:
    assumes "finite V" "A  F"
    shows "finite A"
    using assms by (metis Pow_iff infinite_super rev_subsetD F_ss)

end


definition "gb_rename_ecnv ecnv f G  
  gbg_F = { f`A | A. Agbg_F G },  = ecnv G
"


abbreviation "gb_rename_ext ecnv f  fr_rename_ext (gb_rename_ecnv ecnv f) f"


locale gb_rename_precond =
  gb_graph G +
  g_rename_precond G f "gb_rename_ecnv ecnv f"
  for G :: "('u,'more) gb_graph_rec_scheme"
  and f :: "'u  'v" and ecnv
begin
  lemma G'_gb_fields: "gbg_F G' = { f`A | A. AF }"
    unfolding gb_rename_ecnv_def fr_rename_ext_def
    by simp

  sublocale G': gb_graph G' 
    apply unfold_locales
    apply (simp_all add: G'_fields G'_gb_fields)
    using F_ss 
    by auto

  lemma acc_sim1: "is_acc r  G'.is_acc (f o r)"
    unfolding is_acc_def G'.is_acc_def G'_gb_fields
    by (fastforce intro: imageI simp: INFM_nat)

  lemma acc_sim2: 
    assumes "G'.is_acc r" shows "is_acc (fi o r)"
  proof -
    from assms have 1: "A m. A  gbg_F G  i>m. r i  f`A"
      unfolding G'.is_acc_def G'_gb_fields
      by (auto simp: INFM_nat)

    { fix A m 
      assume 2: "A  gbg_F G"  
      from 1[OF this, of m] have "i>m. fi (r i)  A"
        using F_ss
        apply clarsimp
        by (metis Pow_iff 2 fi_f in_mono)
    } thus ?thesis
      unfolding is_acc_def
      by (auto simp: INFM_nat)
  qed

  lemma acc_run_sim1: "is_acc_run r  G'.is_acc_run (f o r)"
    using acc_sim1 run_sim1 unfolding G'.is_acc_run_def is_acc_run_def
    by auto

  lemma acc_run_sim2: "G'.is_acc_run r  is_acc_run (fi o r)"
    using acc_sim2 run_sim2 unfolding G'.is_acc_run_def is_acc_run_def
    by auto

end

subsection "Generalized Buchi Automata"
text ‹
  A GBA is obtained from a GBG by adding a labeling function, that associates
  each state with a set of labels. A word is accepted if there is an
  accepting run that can be labeld with this word.
›

record ('Q,'L) gba_rec = "'Q gb_graph_rec" +
  gba_L :: "'Q  'L  bool"

locale gba =
  gb_graph G
  for G :: "('Q,'L,'more) gba_rec_scheme" +
  assumes L_ss: "gba_L G q l  q  V"
begin
  abbreviation "L  gba_L G"

  lemma is_gba: "gba G" by unfold_locales

  definition "accept w  r. is_acc_run r  (i. L (r i) (w i))"
  lemma acceptI[intro?]: "is_acc_run r; i. L (r i) (w i)  accept w"
    by (auto simp: accept_def)

  definition "lang  Collect (accept)"
  lemma langI[intro?]: "accept w  wlang" by (auto simp: lang_def)
end

definition "gba_rename_ecnv ecnv f G  
  gba_L = λq l. 
    if qf`g_V G then 
      gba_L G (the_inv_into (g_V G) f q) l
    else
      False, 
   = ecnv G
"

abbreviation "gba_rename_ext ecnv f  gb_rename_ext (gba_rename_ecnv ecnv f) f"

locale gba_rename_precond =  
  gb_rename_precond G f "gba_rename_ecnv ecnv f" + gba G
  for G :: "('u,'L,'more) gba_rec_scheme"
  and f :: "'u  'v" and ecnv
begin
  lemma G'_gba_fields: "gba_L G' = (λq l. 
    if qf`V then L (fi q) l else False)"
    unfolding gb_rename_ecnv_def gba_rename_ecnv_def fr_rename_ext_def fi_def
    by simp

  sublocale G': gba G'
    apply unfold_locales
    apply (auto simp add: G'_gba_fields G'_fields split: if_split_asm)
    done

  lemma L_sim1: "range r  V; L (r i) l  G'.L (f (r i)) l"
    by (auto simp: G'_gba_fields fi_def[symmetric] fi_f 
      dest: inj_onD[OF INJ]
      dest!: rev_subsetD[OF rangeI[of _ i]])

  lemma L_sim2: " range r  f`V; G'.L (r i) l   L (fi (r i)) l"
    by (auto
      simp: G'_gba_fields fi_def[symmetric] f_fi
      dest!: rev_subsetD[OF rangeI[of _ i]])
    
  lemma accept_eq[simp]: "G'.accept = accept"
    apply (rule ext)
    unfolding accept_def G'.accept_def
  proof safe
    fix w r
    assume R: "G'.is_acc_run r"
    assume L: "i. G'.L (r i) (w i)"
    from R have RAN: "range r  f`V"
      using G'.run_reachable[OF G'.acc_run_run[OF R]] G'.reachable_V
      unfolding G'_fields
      by simp
    from L show "r. is_acc_run r  (i. L (r i) (w i))"
      using acc_run_sim2[OF R] L_sim2[OF RAN]
      by auto
  next
    fix w r
    assume R: "is_acc_run r" 
    assume L: "i. L (r i) (w i)"
    
    from R have RAN: "range r  V"
      using run_reachable[OF acc_run_run[OF R]] reachable_V by simp
      
    from L show "r. 
        G'.is_acc_run r 
       (i. G'.L (r i) (w i))"
      using acc_run_sim1[OF R] L_sim1[OF RAN]
      by auto
  qed

  lemma lang_eq[simp]: "G'.lang = lang"
    unfolding G'.lang_def lang_def by simp

  lemma finite_G'_V:
    assumes "finite V"
    shows "finite G'.V"
    using assms by (auto simp add: G'_gba_fields G'_fields split: if_split_asm)

end


abbreviation "gba_rename  gba_rename_ext (λ_. ())"

lemma gba_rename_correct:
  fixes G :: "('v,'l,'m) gba_rec_scheme"
  assumes "gba G" 
  assumes INJ: "inj_on f (g_V G)" 
  defines "G'  gba_rename f G"
  shows "gba G'"
  and "finite (g_V G)  finite (g_V G')"
  and "gba.accept G' = gba.accept G"
  and "gba.lang G' = gba.lang G"
  unfolding G'_def
proof -
  let ?G' = "gba_rename f G"
  interpret gba G by fact
  
  from INJ interpret gba_rename_precond G f "λ_. ()"
    by unfold_locales simp_all

  show "gba ?G'" by (rule G'.is_gba)
  show "finite (g_V G)  finite (g_V ?G')" by (fact finite_G'_V)
  show "G'.accept = accept" by simp
  show "G'.lang = lang" by simp
qed

subsection "Buchi Graphs"

text ‹A Buchi graph has exactly one acceptance class›

record 'Q b_graph_rec = "'Q graph_rec" +
  bg_F :: "'Q set"

locale b_graph =
  graph G 
  for G :: "('Q,'more) b_graph_rec_scheme"
  +
  assumes F_ss: "bg_F G  V"
begin
  abbreviation F where "F  bg_F G"

  lemma is_b_graph: "b_graph G" by unfold_locales

  definition "to_gbg_ext m 
      g_V = V, 
        g_E=E, 
        g_V0=V0, 
        gbg_F = if F=UNIV then {} else {F}, 
         = m "
  abbreviation "to_gbg  to_gbg_ext ()"

  sublocale gbg: gb_graph "to_gbg_ext m"
    apply unfold_locales 
    using V0_ss E_ss F_ss
    apply (auto simp: to_gbg_ext_def split: if_split_asm)
    done

  definition is_acc :: "'Q word  bool" where "is_acc r  (i. r i  F)"
  definition is_acc_run where "is_acc_run r  is_run r  is_acc r"

  lemma to_gbg_alt:
    "gbg.V T m = V"
    "gbg.E T m = E"
    "gbg.V0 T m = V0"
    "gbg.F T m = (if F=UNIV then {} else {F})"
    "gbg.is_run T m = is_run"
    "gbg.is_acc T m = is_acc"
    "gbg.is_acc_run T m = is_acc_run"
    unfolding is_run_def[abs_def] gbg.is_run_def[abs_def]
      is_acc_def[abs_def] gbg.is_acc_def[abs_def]
      is_acc_run_def[abs_def] gbg.is_acc_run_def[abs_def]
    by (auto simp: to_gbg_ext_def)

end

subsection "Buchi Automata"
text ‹Buchi automata are labeled Buchi graphs›

record ('Q,'L) ba_rec = "'Q b_graph_rec" +
  ba_L :: "'Q  'L  bool"

locale ba =
  bg?: b_graph G 
  for G :: "('Q,'L,'more) ba_rec_scheme"
  +
  assumes L_ss: "ba_L G q l  q  V"
begin
  abbreviation L where "L == ba_L G"

  lemma is_ba: "ba G" by unfold_locales


  abbreviation "to_gba_ext m  to_gbg_ext  gba_L = L, =m "
  abbreviation "to_gba  to_gba_ext ()"

  sublocale gba: gba "to_gba_ext m" 
    apply unfold_locales
    unfolding to_gbg_ext_def
    using L_ss apply auto []
    done

  lemma ba_acc_simps[simp]: "gba.L T m = L"
    by (simp add: to_gbg_ext_def)

  definition "accept w  (r. is_acc_run r  (i. L (r i) (w i)))"
  definition "lang  Collect accept"

  lemma to_gba_alt_accept: 
    "gba.accept T m = accept"
    apply (intro ext)
    unfolding accept_def gba.accept_def
    apply (simp_all add: to_gbg_alt)
    done

  lemma to_gba_alt_lang: 
    "gba.lang T m = lang"
    unfolding lang_def gba.lang_def
    apply (simp_all add: to_gba_alt_accept)
    done

  lemmas to_gba_alt = to_gbg_alt to_gba_alt_accept to_gba_alt_lang
end

subsection "Indexed acceptance classes"
record 'Q igb_graph_rec = "'Q graph_rec" +
  igbg_num_acc :: nat
  igbg_acc :: "'Q  nat set"

locale igb_graph = 
  graph G
  for G :: "('Q,'more) igb_graph_rec_scheme"
  +
  assumes acc_bound: "(range (igbg_acc G))  {0..<(igbg_num_acc G)}"
  assumes acc_ss: "igbg_acc G q  {}  qV"
begin
  abbreviation num_acc where "num_acc  igbg_num_acc G"
  abbreviation acc where "acc  igbg_acc G"

  lemma is_igb_graph: "igb_graph G" by unfold_locales


  lemma acc_boundI[simp, intro]: "xacc q  x<num_acc"
    using acc_bound by fastforce

  definition "accn i  {q . iacc q}"
  definition "F  { accn i | i. i<num_acc }"

  definition "to_gbg_ext m 
      g_V = V, g_E = E, g_V0 = V0, gbg_F = F, =m "

  sublocale gbg: gb_graph "to_gbg_ext m" 
    apply unfold_locales
    using V0_ss E_ss acc_ss
    apply (auto simp: to_gbg_ext_def F_def accn_def)
    done

  lemma to_gbg_alt1: 
    "gbg.E T m = E"
    "gbg.V0 T m = V0"
    "gbg.F T m = F" 
    by (simp_all add: to_gbg_ext_def)

  lemma F_fin[simp,intro!]: "finite F"
    unfolding F_def
    by auto

  definition is_acc :: "'Q word  bool" 
    where "is_acc r  (n<num_acc. i. n  acc (r i))"
  definition "is_acc_run r  is_run r  is_acc r"

  lemma is_run_gbg: 
    "gbg.is_run T m = is_run"
    unfolding is_run_def[abs_def] is_acc_run_def[abs_def] 
      gbg.is_run_def[abs_def] gbg.is_acc_run_def[abs_def] 
    by (simp_all add: to_gbg_ext_def)

  lemma is_acc_gbg: 
    "gbg.is_acc T m = is_acc"
    apply (intro ext)
    unfolding gbg.is_acc_def is_acc_def
    apply (simp add: to_gbg_alt1 is_run_gbg)
    unfolding F_def accn_def
    apply (blast intro: INFM_mono)
    done

  lemma is_acc_run_gbg: 
    "gbg.is_acc_run T m = is_acc_run"
    apply (intro ext)
    unfolding gbg.is_acc_run_def is_acc_run_def
    by (simp_all add: to_gbg_alt1 is_run_gbg is_acc_gbg)

  lemmas to_gbg_alt = to_gbg_alt1 is_run_gbg is_acc_gbg is_acc_run_gbg

  lemma acc_limit_alt: 
    assumes FIN: "finite (range r)"
    shows "is_acc r  (n<num_acc. limit r  accn n  {})"
  proof
    assume "n<num_acc. limit r  accn n  {}"
    thus "is_acc r"
      unfolding is_acc_def accn_def
      by (auto dest!: limit_inter_INF)
  next
    from FIN have FIN': "A. finite (A  range r)" by simp
    assume "is_acc r"
    hence "n<num_acc. limit r  (accn n  range r)  {}"
      unfolding is_acc_def accn_def
      by (auto simp: fin_ex_inf_eq_limit[OF FIN', symmetric])
    thus "n<num_acc. limit r  accn n  {}" by auto
  qed

  lemma acc_limit_alt': 
    "finite (range r)  is_acc r  ((acc ` limit r) = {0..<num_acc})"
    unfolding acc_limit_alt
    by (auto simp: accn_def)

end

record ('Q,'L) igba_rec = "'Q igb_graph_rec" +
  igba_L :: "'Q  'L  bool"

locale igba =
  igbg?: igb_graph G
  for G :: "('Q,'L,'more) igba_rec_scheme"
  +
  assumes L_ss: "igba_L G q l  q  V"
begin
  abbreviation L where "L  igba_L G"

  lemma is_igba: "igba G" by unfold_locales


  abbreviation "to_gba_ext m  to_gbg_ext  gba_L = igba_L G, =m "

  sublocale gba: gba "to_gba_ext m" 
    apply unfold_locales
    unfolding to_gbg_ext_def
    using L_ss
    apply auto
    done
  
  lemma to_gba_alt_L:
    "gba.L T m = L"
    by (auto simp: to_gbg_ext_def)

  definition "accept w  r. is_acc_run r  (i. L (r i) (w i))"
  definition "lang  Collect accept"

  lemma accept_gba_alt: "gba.accept T m = accept"
    apply (intro ext)
    unfolding accept_def gba.accept_def
    apply (simp add: to_gbg_alt to_gba_alt_L)
    done

  lemma lang_gba_alt: "gba.lang T m = lang"
    unfolding lang_def gba.lang_def
    apply (simp add: accept_gba_alt)
    done

  lemmas to_gba_alt = to_gbg_alt to_gba_alt_L accept_gba_alt lang_gba_alt

end

subsubsection ‹Indexing Conversion›
definition F_to_idx :: "'Q set set  (nat × ('Q  nat set)) nres" where
  "F_to_idx F  do {
    Flist  SPEC (λFlist. distinct Flist  set Flist = F);
    let num_acc = length Flist;
    let acc = (λv. {i . i<num_acc  vFlist!i});
    RETURN (num_acc,acc)
  }"

lemma F_to_idx_correct:
  shows "F_to_idx F  SPEC (λ(num_acc,acc). F = { {q. iacc q} | i. i<num_acc } 
     (range acc)  {0..<num_acc})"
  unfolding F_to_idx_def
  apply (refine_rcg refine_vcg)
  apply (clarsimp dest!: sym[where t=F])
  apply (intro equalityI subsetI)
  apply (auto simp: in_set_conv_nth) [2]

  apply auto []
  done

definition "mk_acc_impl Flist  do {
  let acc = Map.empty;

  (_,acc)  nfoldli Flist (λ_. True) (λA (i,acc). do {
    acc  FOREACHi (λit acc'. 
      acc' = (λv. 
        if vA-it then 
          Some (insert i (the_default {} (acc v))) 
        else 
          acc v
      )
    ) 
      A (λv acc. RETURN (acc(vinsert i (the_default {} (acc v))))) acc;
    RETURN (Suc i,acc)
  }) (0,acc);
  RETURN (λx. the_default {} (acc x))
}"

lemma mk_acc_impl_correct: 
  assumes F: "(Flist',Flist)Id"
  assumes FIN: "Aset Flist. finite A"
  shows "mk_acc_impl Flist'  Id (RETURN (λv. {i . i<length Flist  vFlist!i}))"
  using F apply simp
  unfolding mk_acc_impl_def

  apply (refine_rcg 
    nfoldli_rule[where 
      I="λl1 l2 (i,res). i=length l1 
         the_default {} o res = (λv. {j . j<i  vFlist!j})"
    ]
    refine_vcg 
  )
  using FIN apply (simp_all)
  apply (rule ext) apply auto []

  apply (rule ext) apply (auto split: if_split_asm simp: nth_append nth_Cons') []
  apply (rule ext) apply (auto split: if_split_asm simp: nth_append nth_Cons' 
    fun_comp_eq_conv) []

  apply (rule ext) apply (auto simp: fun_comp_eq_conv) []
  done

definition F_to_idx_impl :: "'Q set set  (nat × ('Q  nat set)) nres" where
  "F_to_idx_impl F  do {
    Flist  SPEC (λFlist. distinct Flist  set Flist = F);
    let num_acc = length Flist;
    acc  mk_acc_impl Flist;
    RETURN (num_acc,acc)
  }"

lemma F_to_idx_refine: 
  assumes FIN: "AF. finite A"
  shows "F_to_idx_impl F  Id (F_to_idx F)"
  using assms
  unfolding F_to_idx_impl_def F_to_idx_def

  apply (refine_rcg bind_Let_refine2[OF mk_acc_impl_correct])

  apply auto
  done

definition gbg_to_idx_ext 
  :: "_  ('a, 'more) gb_graph_rec_scheme  ('a, 'more') igb_graph_rec_scheme nres"
  where "gbg_to_idx_ext ecnv A = do {
  (num_acc,acc)  F_to_idx_impl (gbg_F A); 
  RETURN  
    g_V = g_V A,
    g_E = g_E A, 
    g_V0=g_V0 A, 
    igbg_num_acc = num_acc, 
    igbg_acc = acc,
     = ecnv A
  
}"

lemma (in gb_graph) gbg_to_idx_ext_correct:
  assumes [simp, intro]: " A. A  F  finite A"
  shows "gbg_to_idx_ext ecnv G  SPEC (λG'. 
    igb_graph.is_acc_run G' = is_acc_run 
   g_V G' = V
   g_E G' = E
   g_V0 G' = V0
   igb_graph_rec.more G' = ecnv G
   igb_graph G'
)"
proof -
  note F_to_idx_refine[of F]
  also note F_to_idx_correct
  finally have R: "F_to_idx_impl F
     SPEC (λ(num_acc, acc). F = {{q. i  acc q} |i. i < num_acc}
       (range acc)  {0..<num_acc})" by simp

  have eq_conjI: "a b c. (bc)  (a&b  a&c)" by simp

  {
    fix acc :: "'Q  nat set" and num_acc r
    have "(A. (i. A = {q. i  acc q}  i < num_acc)  (limit r  A  {})) 
       (i<num_acc. qlimit r. iacc q)"
      by blast
  } note aux1=this

  {
    fix acc :: "'Q  nat set" and num_acc i
    assume FE: "F = {{q. i  acc q} |i. i < num_acc}"
    assume INR: "(x. acc x)  {0..<num_acc}"
    have "finite {q. i  acc q}" 
    proof (cases "i<num_acc")
      case True thus ?thesis using FE by auto
    next
      case False hence "{q. i  acc q} = {}" using INR by force
      thus ?thesis by simp
    qed
  } note aux2=this

  {
    fix acc :: "'Q  nat set" and num_acc q
    assume FE: "F = {{q. i  acc q} |i. i < num_acc}"
      and INR: "(x. acc x)  {0..<num_acc}"
      and "acc q  {}"
    then obtain i where "iacc q" by auto
    moreover with INR have "i<num_acc" by force
    ultimately have "qF" by (auto simp: FE)
    with F_ss have "qV" by auto
  } note aux3=this

  show ?thesis
    unfolding gbg_to_idx_ext_def
    apply (refine_rcg order_trans[OF R] refine_vcg)
  proof clarsimp_all
    fix acc and num_acc :: nat
    assume FE[simp]: "F = {{q. i  acc q} |i. i < num_acc}"
      and BOUND: "(x. acc x)  {0..<num_acc}"
    let ?G' = "
      g_V = V, 
      g_E = E, 
      g_V0 = V0, 
      igbg_num_acc = num_acc, 
      igbg_acc = acc,
       = ecnv G"

    interpret G': igb_graph ?G'
      apply unfold_locales
      using V0_ss E_ss 
      apply (auto simp add: aux2 aux3 BOUND)
      done

    show "igb_graph ?G'" by unfold_locales

    show "G'.is_acc_run = is_acc_run"
      unfolding G'.is_acc_run_def[abs_def] is_acc_run_def[abs_def] 
        G'.is_run_def[abs_def] is_run_def[abs_def]
        G'.is_acc_def[abs_def] is_acc_def[abs_def]
      
      apply (clarsimp intro!: ext eq_conjI)
      apply auto []
      apply (metis (lifting, no_types) INFM_mono mem_Collect_eq)
      done
  qed
qed

abbreviation gbg_to_idx :: "('q,_) gb_graph_rec_scheme  'q igb_graph_rec nres"
  where "gbg_to_idx  gbg_to_idx_ext (λ_. ())"

definition ti_Lcnv where "ti_Lcnv ecnv A   igba_L = gba_L A, =ecnv A "

abbreviation "gba_to_idx_ext ecnv  gbg_to_idx_ext (ti_Lcnv ecnv)"
abbreviation "gba_to_idx  gba_to_idx_ext (λ_. ())"

lemma (in gba) gba_to_idx_ext_correct:
  assumes [simp, intro]: " A. A  F  finite A"
  shows "gba_to_idx_ext ecnv G  
    SPEC (λG'.
    igba.accept G' = accept 
   g_V G' = V
   g_E G' = E
   g_V0 G' = V0
   igba_rec.more G' = ecnv G
   igba G')"
  apply (rule order_trans[OF gbg_to_idx_ext_correct])
  apply (rule, assumption)
  apply (rule SPEC_rule)
  apply (elim conjE, intro conjI)
proof -
  fix G'
  assume 
    ARUN: "igb_graph.is_acc_run G' = is_acc_run"
    and MORE: "igb_graph_rec.more G' = ti_Lcnv ecnv G" 
    and LOC: "igb_graph G'"
    and FIELDS: "g_V G' = V" "g_E G' = E" "g_V0 G' = V0"
  
  from LOC interpret igb: igb_graph G' .

  interpret igb: igba G'
    apply unfold_locales
    using MORE FIELDS L_ss
    unfolding ti_Lcnv_def
    apply (cases G')
    apply simp
    done

  show "igba.accept G' = accept" and "igba_rec.more G' = ecnv G"
    using ARUN MORE 
    unfolding accept_def[abs_def] igb.accept_def[abs_def] ti_Lcnv_def
    apply (cases G', (auto) []) +
    done

  show "igba G'" by unfold_locales
qed

corollary (in gba) gba_to_idx_ext_lang_correct:
  assumes [simp, intro]: " A. A  F  finite A"
  shows "gba_to_idx_ext ecnv G  
    SPEC (λG'. igba.lang G' = lang  igba_rec.more G' = ecnv G  igba G')"
  apply (rule order_trans[OF gba_to_idx_ext_correct])
  apply (rule, assumption)
  apply (rule SPEC_rule)
  unfolding lang_def[abs_def]
  apply (subst igba.lang_def)
  apply auto
  done

subsubsection ‹Degeneralization›

context igb_graph
begin

  definition degeneralize_ext :: "_  ('Q × nat, _) b_graph_rec_scheme" where
    "degeneralize_ext ecnv  
      if num_acc = 0 then 
        g_V = V × {0},
        g_E = {((q,0),(q',0)) | q q'. (q,q')E}, 
        g_V0 = V0×{0}, 
        bg_F = V × {0},
         = ecnv G
      
      else 
        g_V = V × {0..<num_acc},
        g_E = { ((q,i),(q',i')) | i i' q q'. 
            i<num_acc 
           (q,q')E 
           i' = (if iacc q then (i+1) mod num_acc else i) },
        g_V0 = V0 × {0},
        bg_F = {(q,0)| q. 0acc q},
         = ecnv G
      "

  abbreviation degeneralize where "degeneralize  degeneralize_ext (λ_. ())"

  lemma degen_more[simp]: "b_graph_rec.more (degeneralize_ext ecnv) = ecnv G"
    unfolding degeneralize_ext_def
    by auto

  lemma degen_invar: "b_graph (degeneralize_ext ecnv)"
  proof
    let ?G' = "degeneralize_ext ecnv"

    show "g_V0 ?G'  g_V ?G'"
      unfolding degeneralize_ext_def
      using V0_ss
      by auto

    show "g_E ?G'  g_V ?G' × g_V ?G'"
      unfolding degeneralize_ext_def
      using E_ss
      by auto

    show "bg_F ?G'  g_V ?G'"
      unfolding degeneralize_ext_def
      using acc_ss
      by auto

  qed

  sublocale degen: b_graph "degeneralize_ext m" using degen_invar .

  lemma degen_finite_reachable:
    assumes [simp, intro]: "finite (E* `` V0)"
    shows "finite ((g_E (degeneralize_ext ecnv))* `` g_V0 (degeneralize_ext ecnv))"
  proof -
    let ?G' = "degeneralize_ext ecnv"
    have "((g_E ?G')* `` g_V0 ?G')
       E*``V0 × {0..num_acc}"
    proof -
      {
        fix q n q' n'
        assume "((q,n),(q',n'))(g_E ?G')*" 
          and 0: "(q,n)g_V0 ?G'"
        hence G1: "(q,q')E*  n'num_acc"
          apply (induction rule: rtrancl_induct2)
          by (auto simp: degeneralize_ext_def split: if_split_asm)
        
        from 0 have G2: "qV0  nnum_acc"
          by (auto simp: degeneralize_ext_def split: if_split_asm)
        note G1 G2
      } thus ?thesis by fastforce
    qed
    also have "finite " by auto
    finally (finite_subset) show "finite ((g_E ?G')* `` g_V0 ?G')" .
  qed

  lemma degen_is_run_sound: 
    "degen.is_run T m r  is_run (fst o r)"
    unfolding degen.is_run_def is_run_def
    unfolding degeneralize_ext_def
    apply (clarsimp split: if_split_asm simp: ipath_def)
    apply (metis fst_conv)+
    done

  lemma degen_path_sound: 
    assumes "path (degen.E T m) u p v" 
    shows "path E (fst u) (map fst p) (fst v)"
    using assms
    by induction (auto simp: degeneralize_ext_def path_simps split: if_split_asm)

  lemma degen_V0_sound: 
    assumes "u  degen.V0 T m" 
    shows "fst u  V0"
    using assms
    by (auto simp: degeneralize_ext_def path_simps split: if_split_asm)


  lemma degen_visit_acc:
    assumes "path (degen.E T m) (q,n) p (q',n')"
    assumes "nn'"
    shows "qa. (qa,n)set p  nacc qa"
    using assms
  proof (induction _ "(q,n)" p "(q',n')" arbitrary: q rule: path.induct)
    case (path_prepend qnh p)
    then obtain qh nh where [simp]: "qnh=(qh,nh)" by (cases qnh)
    from ((q,n),qnh)  degen.E T m 
    have "nh=n  (nh=(n+1) mod num_acc  nacc q)"
      by (auto simp: degeneralize_ext_def split: if_split_asm)
    thus ?case proof
      assume [simp]: "nh=n"
      from path_prepend obtain qa where "(qa, n)  set p" and "n  acc qa" 
        by auto
      thus ?case by auto
    next
      assume "(nh=(n+1) mod num_acc  nacc q)" thus ?case by auto
    qed
  qed simp

  lemma degen_run_complete0:
    assumes [simp]: "num_acc = 0"
    assumes R: "is_run r"
    shows "degen.is_run T m (λi. (r i,0))"
    using R
    unfolding degen.is_run_def is_run_def
    unfolding ipath_def degeneralize_ext_def
    by auto

  lemma degen_acc_run_complete0:
    assumes [simp]: "num_acc = 0"
    assumes R: "is_acc_run r"
    shows "degen.is_acc_run T m (λi. (r i,0))"
    using R
    unfolding degen.is_acc_run_def is_acc_run_def is_acc_def degen.is_acc_def
    apply (simp add: degen_run_complete0)
    unfolding degeneralize_ext_def
    using run_reachable[of r] reachable_V
    by (auto simp: INFM_nat)

  lemma degen_run_complete:
    assumes [simp]: "num_acc  0"
    assumes R: "is_run r"
    shows "r'. degen.is_run T m r'  r = fst o r'"
    using R
    unfolding degen.is_run_def is_run_def ipath_def
    apply (elim conjE)
  proof -
    assume R0: "r 0  V0" and RS: "i. (r i, r (Suc i))  E"

    define r' where "r' = rec_nat
      (r 0,0) 
      (λi (q,n). (r (Suc i), if n  acc q then (n+1) mod num_acc else n))"

    have [simp]:
      "r' 0 = (r 0,0)"
      "i. r' (Suc i) = (
        let 
          (q,n)=r' i 
        in 
          (r (Suc i), if n  acc q then (n+1) mod num_acc else n)
      )"
      unfolding r'_def
      by auto

    have R0': "r' 0  degen.V0 T m" using R0
      unfolding degeneralize_ext_def by auto

    have MAP: "r = fst o r'"
    proof (rule ext)
      fix i
      show "r i = (fst o r') i"
        by (cases i) (auto simp: split: prod.split)
    qed

    have [simp]: "0<num_acc" by (cases num_acc) auto

    have SND_LESS: "i. snd (r' i) < num_acc"
    proof -
      fix i show "snd (r' i) < num_acc" by (induction i) (auto split: prod.split) 
    qed

    have RS': "i. (r' i, r' (Suc i))  degen.E T m"
    proof
      fix i
      obtain n where [simp]: "r' i = (r i,n)"
        apply (cases i)
        apply (force)
        apply (force split: prod.split)
        done
      from SND_LESS[of i] have [simp]: "n<num_acc" by simp

      show "(r' i, r' (Suc i))  degen.E T m" using RS
        by (auto simp: degeneralize_ext_def)
    qed

    from R0' RS' MAP show 
      "r'. (r' 0  degen.V0 T m
       (i. (r' i, r' (Suc i))  degen.E T m)) 
       r = fst  r'" by blast
  qed

  lemma degen_run_bound:
    assumes [simp]: "num_acc  0"
    assumes R: "degen.is_run T m r"
    shows "snd (r i) < num_acc"
    apply (induction i)
    using R 
    unfolding degen.is_run_def is_run_def
    unfolding degeneralize_ext_def ipath_def
    apply -
    apply auto []
    apply clarsimp
    by (metis snd_conv)
  
  lemma degen_acc_run_complete_aux1: 
    assumes NN0[simp]: "num_acc  0"
    assumes R: "degen.is_run T m r"
    assumes EXJ: "ji. n  acc (fst (r j))"
    assumes RI: "r i = (q,n)"
    shows "ji. q'. r j = (q',n)  n  acc q'"
  proof -
    define j where "j = (LEAST j. ji  n  acc (fst (r j)))"

    from RI have "n<num_acc" using degen_run_bound[OF NN0 R, of i] by auto
    from EXJ have 
      "ji" 
      "n  acc (fst (r j))" 
      "ki. n  acc (fst (r k))  jk"
      using LeastI_ex[OF EXJ]
      unfolding j_def
      apply (auto) [2]
      apply (metis (lifting) Least_le)
      done
    hence "ki. k<j  n  acc (fst (r k))" by auto

    have "k. ki  kj  (snd (r k) = n)"
    proof (clarify)
      fix k
      assume "ik" "kj"
      thus "snd (r k) = n"
      proof (induction k rule: less_induct)
        case (less k)
        show ?case proof (cases "k=i")
          case True thus ?thesis using RI by simp
        next
          case False with less.prems have "k - 1 < k" "i  k - 1" "k - 1j"
            by auto
          from less.IH[OF this] have "snd (r (k - 1)) = n" .
          moreover from R have 
            "(r (k - 1), r k)  degen.E T m"
            unfolding degen.is_run_def is_run_def ipath_def
            by clarsimp (metis One_nat_def Suc_diff_1 k - 1 < k 
              less_nat_zero_code neq0_conv)
          moreover have "n  acc (fst (r (k - 1)))"
            using ki. k < j  n  acc (fst (r k)) i  k - 1 k - 1 < k 
              dual_order.strict_trans1 less.prems(2) 
              by blast
          ultimately show ?thesis
            by (auto simp: degeneralize_ext_def)
        qed
      qed
    qed

    thus ?thesis 
      by (metis i  j n  local.acc (fst (r j)) 
        order_refl surjective_pairing)
  qed
      
  lemma degen_acc_run_complete_aux1': 
    assumes NN0[simp]: "num_acc  0"
    assumes R: "degen.is_run T m r"
    assumes ACC: "n<num_acc. i. n  acc (fst (r i))"
    assumes RI: "r i = (q,n)"
    shows "ji. q'. r j = (q',n)  n  acc q'"
  proof -
    from RI have "n<num_acc" using degen_run_bound[OF NN0 R, of i] by auto
    with ACC have EXJ: "ji. n  acc (fst (r j))" 
      unfolding INFM_nat_le by blast

    from degen_acc_run_complete_aux1[OF NN0 R EXJ RI] show ?thesis .
  qed

  lemma degen_acc_run_complete_aux2:
    assumes NN0[simp]: "num_acc  0"
    assumes R: "degen.is_run T m r"
    assumes ACC: "n<num_acc. i. n  acc (fst (r i))"
    assumes RI: "r i = (q,n)" and OFS: "ofs<num_acc"
    shows "ji. q'. 
      r j = (q',(n + ofs) mod num_acc)  (n + ofs) mod num_acc  acc q'"
    using RI OFS
  proof (induction ofs arbitrary: q n i)
    case 0 
    from degen_run_bound[OF NN0 R, of i] r i = (q, n) 
    have NLE: "n<num_acc" 
      by simp

    with degen_acc_run_complete_aux1'[OF NN0 R ACC r i = (q, n)] show ?case
      by auto
  next
    case (Suc ofs)
    from Suc.IH[OF Suc.prems(1)] Suc.prems(2)
    obtain j q' where "ji" and RJ: "r j = (q',(n+ofs) mod num_acc)" 
      and A: "(n+ofs) mod num_acc  acc q'"
      by auto
    from R have "(r j, r (Suc j))  degen.E T m" 
      by (auto simp: degen.is_run_def is_run_def ipath_def)
    with RJ A obtain q2 where RSJ: "r (Suc j) = (q2,(n+Suc ofs) mod num_acc)" 
      by (auto simp: degeneralize_ext_def mod_simps)

    have aux: "j'. ij  Suc j  j'  ij'" by auto
    from degen_acc_run_complete_aux1'[OF NN0 R ACC RSJ] ji 
    show ?case 
      by (auto dest: aux)
  qed

  lemma degen_acc_run_complete:
    assumes AR: "is_acc_run r"
    obtains r' 
    where "degen.is_acc_run T m r'" and "r = fst o r'"
  proof (cases "num_acc = 0")
    case True 
    with AR degen_acc_run_complete0 
    show ?thesis by (auto intro!: that[of "(λi. (r i, 0))"])
  next
    case False
    assume NN0[simp]: "num_acc  0"

    from AR have R: "is_run r" and ACC: "n<num_acc. i. n  acc (r i)"
      unfolding is_acc_run_def is_acc_def by auto

    from degen_run_complete[OF NN0 R] obtain r' where 
      R': "degen.is_run T m r'" 
      and [simp]: "r = fst  r'" 
      by auto

    from ACC have ACC': "n<num_acc. i. n  acc (fst (r' i))" by simp

    have "i. j>i. r' j  degen.F T m"
    proof
      fix i
      obtain q n where RI: "r' (Suc i) = (q,n)" by (cases "r' (Suc i)")
      have "(n + (num_acc - n mod num_acc)) mod num_acc = 0"
        apply (rule dvd_imp_mod_0)
        apply (metis (mono_tags, lifting) NN0 add_diff_inverse mod_0_imp_dvd
          mod_add_left_eq mod_less_divisor mod_self nat_diff_split not_gr_zero zero_less_diff)
        done
      then obtain ofs where 
        OFS_LESS: "ofs<num_acc" 
        and [simp]: "(n + ofs) mod num_acc = 0"
        by (metis NN0 Nat.add_0_right diff_less neq0_conv)
      with degen_acc_run_complete_aux2[OF NN0 R' ACC' RI OFS_LESS]
      obtain j q' where 
        "j>i" "r' j = (q',0)" and "0acc q'" 
        by (auto simp: less_eq_Suc_le)
      thus "j>i. r' j  degen.F T m" 
        by (auto simp: degeneralize_ext_def)
    qed
    hence "i. r' i  degen.F T m" by (auto simp: INFM_nat)

    have "degen.is_acc_run T m r'"
      unfolding degen.is_acc_run_def degen.is_acc_def
      by rule fact+
    thus ?thesis by (auto intro: that)
  qed

  lemma degen_run_find_change:
    assumes NN0[simp]: "num_acc  0"
    assumes R: "degen.is_run T m r"
    assumes A: "ij" "r i = (q,n)" "r j = (q',n')" "nn'"
    obtains k qk where "ik" "k<j" "r k = (qk,n)" "n  acc qk"
  proof -
    from degen_run_bound[OF NN0 R] A have "n<num_acc" "n'<num_acc"
      by (metis snd_conv)+

    define k where "k = (LEAST k. i<k  snd (r k)  n)"

    have "i<k" "snd (r k)  n"
      by (metis (lifting, mono_tags) LeastI_ex A k_def leD less_linear snd_conv)+

    from Least_le[where P="λk. i<k  snd (r k)  n", folded k_def]
    have LEK_EQN: "k'. ik'  k'<k  snd (r k') = n"
      using r i = (q,n)
      by clarsimp (metis le_neq_implies_less not_le snd_conv)
    hence SND_RKMO: "snd (r (k - 1)) = n" using i<k by auto
    moreover from R have "(r (k - 1), r k)  degen.E T m"
      unfolding degen.is_run_def ipath_def using i<k
      by clarsimp (metis Suc_pred gr_implies_not0 neq0_conv) 
    moreover note ‹snd (r k)  n
    ultimately have "n  acc (fst (r (k - 1)))"
      by (auto simp: degeneralize_ext_def split: if_split_asm)
    moreover have "k - 1 < j" using A LEK_EQN 
      apply (rule_tac ccontr)
      apply clarsimp
      by (metis One_nat_def ‹snd (r (k - 1)) = n less_Suc_eq 
        less_imp_diff_less not_less_eq snd_conv)
    ultimately show thesis
      apply -
      apply (rule that[of "k - 1" "fst (r (k - 1))"])
      using i<k SND_RKMO by auto
  qed


  lemma degen_run_find_acc_aux:
    assumes NN0[simp]: "num_acc  0"
    assumes AR: "degen.is_acc_run T m r"
    assumes A: "r i = (q,0)" "0  acc q" "n<num_acc"
    shows "j qj. ij  r j = (qj,n)  n  acc qj"
  proof -
    from AR have R: "degen.is_run T m r" 
      and ACC: "i. r i  degen.F T m"
      (*and ACC: "limit r ∩ bg_F (degeneralize_ext ecnv) ≠ {}"*)
      unfolding degen.is_acc_run_def degen.is_acc_def by auto
    from ACC have ACC': "i. j>i. r j  degen.F T m"
      by (auto simp: INFM_nat)
    
    show ?thesis using n<num_acc›
    proof (induction n)
      case 0 thus ?case using A by auto
    next
      case (Suc n)
      then obtain j qj where "ij" "r j = (qj,n)" "nacc qj" by auto
      moreover from R have "(r j, r (Suc j))  degen.E T m" 
        unfolding degen.is_run_def ipath_def
        by auto
      ultimately obtain qsj where RSJ: "r (Suc j) = (qsj,Suc n)"
        unfolding degeneralize_ext_def using ‹Suc n<num_acc› by auto
      
      from ACC' obtain k q0 where "Suc j  k" "r k = (q0, 0)"
        unfolding degeneralize_ext_def apply auto
        by (metis less_imp_le_nat)
      from degen_run_find_change[OF NN0 R ‹Suc j  k RSJ r k = (q0, 0)] 
      obtain l ql where
        "Suc j  l" "l < k" "r l = (ql, Suc n)" "Suc n  acc ql" 
        by blast
      thus ?case using i  j
        by (intro exI[where x=l] exI[where x=ql]) auto
    qed
  qed
      
  lemma degen_acc_run_sound:
    assumes A: "degen.is_acc_run T m r"
    shows "is_acc_run (fst o r)"
  proof -
    from A have R: "degen.is_run T m r" 
      and ACC: "i. r i  degen.F T m"
      unfolding degen.is_acc_run_def degen.is_acc_def by auto
    from degen_is_run_sound[OF R] have R': "is_run (fst o r)" .

    show ?thesis
    proof (cases "num_acc = 0")
      case NN0[simp]: False

      from ACC have ACC': "i. j>i. r j  degen.F T m"
        by (auto simp: INFM_nat)

      have "n<num_acc. i. j>i. n  acc (fst (r j))" 
      proof (intro allI impI)
        fix n i

        obtain j qj where "j>i" and RJ: "r j = (qj,0)" and ACCJ: "0  acc (qj)"
          using ACC' unfolding degeneralize_ext_def by fastforce

        assume NLESS: "n<num_acc"
        show "j>i. n  acc (fst (r j))"
        proof (cases n)
          case 0 thus ?thesis using j>i RJ ACCJ by auto
        next
          case [simp]: (Suc n')
          from degen_run_find_acc_aux[OF NN0 A RJ ACCJ NLESS] obtain k qk where
            "jk" "r k = (qk,n)" "n  acc qk" by auto
          thus ?thesis
            by (metis i < j dual_order.strict_trans1 fst_conv)
        qed
      qed
      hence "n<num_acc. i. n  acc (fst (r i))"
        by (auto simp: INFM_nat)
      with R' show ?thesis
        unfolding is_acc_run_def is_acc_def by auto
    next
      case [simp]: True
      with R' show ?thesis
        unfolding is_acc_run_def is_acc_def
        by auto
    qed
  qed

  lemma degen_acc_run_iff:
    "is_acc_run r  (r'. fst o r' = r  degen.is_acc_run T m r')"
    using degen_acc_run_complete degen_acc_run_sound
    by blast

end

subsection "System Automata"
text ‹
  System automata are (finite) rooted graphs with a labeling function. They are 
  used to describe the model (system) to be checked.
›

record ('Q,'L) sa_rec = "'Q graph_rec" +
  sa_L :: "'Q  'L"

locale sa =
  g?: graph G
  for G :: "('Q, 'L, 'more) sa_rec_scheme"
begin

  abbreviation L where "L  sa_L G"

  definition "accept w  r. is_run r  w = L o r"

  lemma acceptI[intro?]: "is_run r; w = L o r  accept w" by (auto simp: accept_def)

  definition "lang  Collect accept"

  lemma langI[intro?]: "accept w  wlang" by (auto simp: lang_def)

end

subsubsection "Product Construction"
text ‹
  In this section we formalize the product construction between a GBA and a system
  automaton. The result is a GBG and a projection function, such that projected 
  runs of the GBG correspond to words accepted by the GBA and the system.
›

locale igba_sys_prod_precond = igba: igba G + sa: sa S for
  G :: "('q,'l,'moreG) igba_rec_scheme"
  and S :: "('s,'l,'moreS) sa_rec_scheme"
begin

  definition "prod  
    g_V = igba.V × sa.V,
    g_E = { ((q,s),(q',s')). 
      igba.L q (sa.L s)  (q,q')  igba.E  (s,s')  sa.E },
    g_V0 = igba.V0 × sa.V0,
    igbg_num_acc = igba.num_acc,
    igbg_acc = (λ(q,s). if ssa.V then igba.acc q else {} ) "

  lemma prod_invar: "igb_graph prod" 
    apply unfold_locales

    using igba.V0_ss sa.V0_ss
    apply (auto simp: prod_def) []

    using igba.E_ss sa.E_ss
    apply (auto simp: prod_def) []

    using igba.acc_bound
    apply (auto simp: prod_def split: if_split_asm) []

    using igba.acc_ss
    apply (fastforce simp: prod_def split: if_split_asm) []
    done
  
  sublocale prod: igb_graph prod using prod_invar .

  lemma prod_finite_reachable:
    assumes "finite (igba.E* `` igba.V0)" "finite (sa.E* `` sa.V0)"
    shows "finite ((g_E prod)* `` g_V0 prod)"
  proof -
    {
      fix q s q' s'
      assume "((q,s),(q',s'))  (g_E prod)*"
      hence "(q,q')  (igba.E)*  (s,s')  (sa.E)*"
        apply (induction rule: rtrancl_induct2)
        apply (auto simp: prod_def)
        done
    } note gsp_reach=this

    have [simp]: "q s. (q,s)  g_V0 prod  q  igba.V0  s  sa.V0"
      by (auto simp: prod_def)

    have reachSS: 
      "((g_E prod)* `` g_V0 prod) 
       ((igba.E)* `` igba.V0) × (sa.E* `` sa.V0)"
      by (auto dest: gsp_reach)
    show ?thesis
      apply (rule finite_subset[OF reachSS])
      using assms
      by simp
  qed

  lemma prod_fields:
    "prod.V = igba.V × sa.V"
    "prod.E = { ((q,s),(q',s')). 
      igba.L q (sa.L s)  (q,q')  igba.E  (s,s')  sa.E }"
    "prod.V0 = igba.V0 × sa.V0"
    "prod.num_acc = igba.num_acc"
    "prod.acc = (λ(q,s). if ssa.V then igba.acc q else {} )"
    unfolding prod_def
    apply simp_all
    done

  lemma prod_run: "prod.is_run r  
      igba.is_run (fst o r) 
     sa.is_run (snd o r)
     (i. igba.L (fst (r i)) (sa.L (snd (r i))))" (is "?L=?R")
    apply rule
    unfolding igba.is_run_def sa.is_run_def prod.is_run_def
    unfolding prod_def ipath_def
    apply (auto split: prod.split_asm intro: in_prod_fst_sndI)
    apply (metis surjective_pairing)
    apply (metis surjective_pairing)
    apply (metis fst_conv snd_conv)
    apply (metis fst_conv snd_conv)
    apply (metis fst_conv snd_conv)
    done

  lemma prod_acc:
    assumes A: "range (snd o r)  sa.V"
    shows "prod.is_acc r  igba.is_acc (fst o r)"
  proof -
    {
      fix i
      from A have "prod.acc (r i) = igba.acc (fst (r i))"
        unfolding prod_fields
        apply safe
        apply (clarsimp_all split: if_split_asm)
        by (metis UNIV_I comp_apply imageI snd_conv subsetD)
    } note [simp] = this
    show ?thesis
      unfolding prod.is_acc_def igba.is_acc_def
      by (simp add: prod_fields(4))
  qed
  
  lemma gsp_correct1: 
    assumes A: "prod.is_acc_run r"
    shows "sa.is_run (snd o r)  (sa.L o snd o r  igba.lang)"
  proof -
    from A have PR: "prod.is_run r" and PA: "prod.is_acc r" 
      unfolding prod.is_acc_run_def by auto

    have PRR: "range r  prod.V" using prod.run_reachable prod.reachable_V PR by auto

    have RSR: "range (snd o r)  sa.V" using PRR unfolding prod_fields by auto
  
    show ?thesis
      using PR PA
      unfolding igba.is_acc_run_def
        igba.lang_def igba.accept_def[abs_def]
      apply (auto simp: prod_run prod_acc[OF RSR])
      done
  qed
  
  lemma gsp_correct2: 
    assumes A: "sa.is_run r" "sa.L o r  igba.lang"
    shows "r'. r = snd o r'  prod.is_acc_run r'"
  proof -
    have [simp]: "r r'. fst o (λi. (r i, r' i)) = r" 
      "r r'. snd o (λi. (r i, r' i)) = r'"
      by auto

    from A show ?thesis
      unfolding prod.is_acc_run_def 
        igba.lang_def igba.accept_def[abs_def] igba.is_acc_run_def
      apply (clarsimp simp: prod_run)
      apply (rename_tac ra)
      apply (rule_tac x="λi. (ra i, r i)" in exI)
      apply clarsimp
      
      apply (subst prod_acc)
      using order_trans[OF sa.run_reachable sa.reachable_V]
      apply auto []

      apply auto []
      done
  qed

end

end

Theory Lasso

section ‹Lassos›
(* Author: Peter Lammich *)
theory Lasso
imports Automata
begin

  record 'v lasso = 
    lasso_reach :: "'v list"
    lasso_va :: "'v"
    lasso_cysfx :: "'v list"
  
  definition "lasso_v0 L  case lasso_reach L of []  lasso_va L | (v0#_)  v0"
  definition lasso_cycle where "lasso_cycle L = lasso_va L # lasso_cysfx L"


  definition "lasso_of_prpl prpl  case prpl of (pr,pl)  
    lasso_reach = pr,
    lasso_va = hd pl,
    lasso_cysfx = tl pl "

  definition "prpl_of_lasso L  (lasso_reach L, lasso_va L # lasso_cysfx L)"

  lemma prpl_of_lasso_simps[simp]: 
    "fst (prpl_of_lasso L) = lasso_reach L"
    "snd (prpl_of_lasso L) = lasso_va L # lasso_cysfx L"
    unfolding prpl_of_lasso_def by auto

  lemma lasso_of_prpl_simps[simp]:
    "lasso_reach (lasso_of_prpl prpl) = fst prpl"
    "snd prpl  []  lasso_cycle (lasso_of_prpl prpl) = snd prpl"
    unfolding lasso_of_prpl_def lasso_cycle_def by (auto split: prod.split)


  definition run_of_lasso :: "'q lasso  'q word"
    ― ‹Run described by a lasso›
    where "run_of_lasso L  lasso_reach L  (lasso_cycle L)ω"

  lemma run_of_lasso_of_prpl: 
    "pl  []  run_of_lasso (lasso_of_prpl (pr, pl)) = pr  plω"
    unfolding run_of_lasso_def lasso_of_prpl_def lasso_cycle_def
    by auto


  definition "map_lasso f L  
    lasso_reach = map f (lasso_reach L),
    lasso_va = f (lasso_va L),
    lasso_cysfx = map f (lasso_cysfx L)
  "

  lemma map_lasso_simps[simp]:
    "lasso_reach (map_lasso f L) = map f (lasso_reach L)"
    "lasso_va (map_lasso f L) = f (lasso_va L)"
    "lasso_cysfx (map_lasso f L) = map f (lasso_cysfx L)"
    "lasso_v0 (map_lasso f L) = f (lasso_v0 L)"
    "lasso_cycle (map_lasso f L) = map f (lasso_cycle L)"
    unfolding map_lasso_def lasso_v0_def lasso_cycle_def
    by (auto split: list.split)
  
  lemma map_lasso_run[simp]:
    shows "run_of_lasso (map_lasso f L) = f o (run_of_lasso L)"
    by (auto simp add: map_lasso_def run_of_lasso_def conc_def iter_def
      lasso_cycle_def lasso_v0_def fun_eq_iff not_less nth_Cons'
      nz_le_conv_less)


  context graph begin
    definition is_lasso_pre :: "'v lasso  bool" 
      where "is_lasso_pre L  
        lasso_v0 L  V0
       path E (lasso_v0 L) (lasso_reach L) (lasso_va L) 
       path E (lasso_va L) (lasso_cycle L) (lasso_va L)"
    
    definition "is_lasso_prpl_pre prpl  case prpl of (pr, pl)  v0 va.
      v0V0 
       pl  []
       path E v0 pr va
       path E va pl va"

    lemma is_lasso_pre_prpl_of_lasso[simp]: 
      "is_lasso_prpl_pre (prpl_of_lasso L)  is_lasso_pre L"
      unfolding is_lasso_pre_def prpl_of_lasso_def is_lasso_prpl_pre_def
      unfolding lasso_v0_def lasso_cycle_def
      by (auto simp: path_simps split: list.split)
  
    lemma is_lasso_prpl_pre_conv: 
      "is_lasso_prpl_pre prpl 
       (snd prpl[]  is_lasso_pre (lasso_of_prpl prpl))"
      unfolding is_lasso_pre_def lasso_of_prpl_def is_lasso_prpl_pre_def
      unfolding lasso_v0_def lasso_cycle_def
      apply (cases prpl)
      apply (rename_tac a b)
      apply (case_tac b)
      apply (auto simp: path_simps split: list.splits)
      done

    lemma is_lasso_pre_empty[simp]: "V0 = {}  ¬is_lasso_pre L"
      unfolding is_lasso_pre_def by auto


    lemma run_of_lasso_pre: 
      assumes "is_lasso_pre L"  
      shows "is_run (run_of_lasso L)"
      and "run_of_lasso L 0  V0"
      using assms
      unfolding is_lasso_pre_def is_run_def run_of_lasso_def 
        lasso_cycle_def lasso_v0_def
      by (auto simp: ipath_conc_conv ipath_iter_conv path_cons_conv conc_fst 
        split: list.splits)

  end

  context gb_graph begin
    definition is_lasso
      :: "'Q lasso  bool" 
      ― ‹Predicate that defines a lasso›
      where "is_lasso L  
        is_lasso_pre L
       (AF. (set (lasso_cycle L))  A  {})"

    definition "is_lasso_prpl prpl  
      is_lasso_prpl_pre prpl
       (AF. set (snd prpl)  A  {})"
  

    lemma is_lasso_prpl_of_lasso[simp]: 
      "is_lasso_prpl (prpl_of_lasso L)  is_lasso L"
      unfolding is_lasso_def is_lasso_prpl_def
      unfolding lasso_v0_def lasso_cycle_def
      by auto
  
    lemma is_lasso_prpl_conv: 
      "is_lasso_prpl prpl  (snd prpl[]  is_lasso (lasso_of_prpl prpl))"
      unfolding is_lasso_def is_lasso_prpl_def is_lasso_prpl_pre_conv
      apply safe
      apply simp_all
      done
    
    lemma is_lasso_empty[simp]: "V0 = {}  ¬is_lasso L"
      unfolding is_lasso_def by auto

    lemma lasso_accepted:
      assumes L: "is_lasso L"
      shows "is_acc_run (run_of_lasso L)"
    proof -
      obtain "pr" va pls where 
        [simp]: "L = lasso_reach = pr,lasso_va = va,lasso_cysfx = pls" 
        by (cases L)

      from L have "is_run (run_of_lasso L)" 
        unfolding is_lasso_def by (auto simp: run_of_lasso_pre)
      moreover from L have "(AF. set (va#pls)  A  {})"
        by (auto simp: is_lasso_def lasso_cycle_def)
      moreover from L have "(run_of_lasso L) 0  V0" 
        unfolding is_lasso_def by (auto simp: run_of_lasso_pre)
      ultimately show "is_acc_run (run_of_lasso L)"
        unfolding is_acc_run_def is_acc_def run_of_lasso_def 
          lasso_cycle_def lasso_v0_def
        by (fastforce intro: limit_inter_INF)
    qed

    lemma lasso_prpl_acc_run:
      "is_lasso_prpl (pr, pl)  is_acc_run (pr  iter pl)"
      apply (clarsimp simp: is_lasso_prpl_conv)
      apply (drule lasso_accepted)
      apply (simp add: run_of_lasso_of_prpl)
      done

  end
  
  context gb_graph
  begin
    lemma accepted_lasso:
      assumes [simp, intro]: "finite (E* `` V0)"
      assumes A: "is_acc_run r"
      shows "L. is_lasso L"
    proof -
      from A have 
        RUN: "is_run r" 
        and ACC: "AF. limit r  A  {}" 
        by (auto simp: is_acc_run_limit_alt)
      from RUN have [simp]: "r 0  V0" and RUN': "ipath E r" 
        by (simp_all add: is_run_def)

      txt ‹Choose a node that is visited infinitely often›
      from RUN have RAN_REACH: "range r  E*``V0"
        by (auto simp: is_run_def dest: ipath_to_rtrancl)
      hence "finite (range r)" by (auto intro: finite_subset)
      then obtain u where "ulimit r" using limit_nonempty by blast
      hence U_REACH: "uE*``V0" using RAN_REACH limit_in_range by force
      then obtain v0 "pr" where PR: "v0V0" "path E v0 pr u" 
        by (auto intro: rtrancl_is_path)
      moreover
      txt ‹Build a path from u› to u›, that contains nodes from
        each acceptance set›
      have "pl. pl[]  path E u pl u  (AF. set pl  A  {})"
        using finite_F ACC
      proof (induction rule: finite_induct)
        case empty
        from run_limit_two_connectedI[OF RUN' ulimit r ulimit r] 
        obtain p where [simp]: "p[]" and P: "path E u p u" 
          by (rule trancl_is_path) 
        thus ?case by blast
      next
        case (insert A F)
        from insert.IH insert.prems obtain pl where 
          [simp]: "pl[]" 
            and P: "path E u pl u" 
            and ACC: "(A'F. set pl  A'  {})"
          by auto
        from insert.prems obtain v where VACC: "vA" "vlimit r" by auto
        from run_limit_two_connectedI[OF RUN' ulimit r vlimit r] 
        obtain p1 where [simp]: "p1[]" 
          and P1: "path E u p1 v" 
          by (rule trancl_is_path) 

        from run_limit_two_connectedI[OF RUN' vlimit r ulimit r] 
        obtain p2 where [simp]: "p2[]" 
          and P2: "path E v p2 u" 
          by (rule trancl_is_path) 

        note P also note P1 also (path_conc) note P2 finally (path_conc)
        have "path E u (pl@p1@p2) u" by simp
        moreover from P2 have "vset (p1@p2)" 
          by (cases p2) (auto simp: path_cons_conv)
        with ACC VACC have "(A'insert A F. set (pl@p1@p2)  A'  {})" by auto
        moreover have "pl@p1@p2  []" by auto
        ultimately show ?case by (intro exI conjI)
      qed
      then obtain pl where "pl  []" "path E u pl u" "(AF. set pl  A  {})" 
        by blast
      then obtain pls where "path E u (u#pls) u" "AF. set (u#pls)  A  {}"
        by (cases pl) (auto simp add: path_simps)
      ultimately show ?thesis
        apply -
        apply (rule 
          exI[where x="lasso_reach = pr,lasso_va = u,lasso_cysfx = pls"])
        unfolding is_lasso_def lasso_v0_def lasso_cycle_def is_lasso_pre_def
        apply (cases "pr")
        apply (simp_all add: path_simps)
        done
    qed
  end
  

  context b_graph
  begin
    definition is_lasso where "is_lasso L  
      is_lasso_pre L
       (set (lasso_cycle L))  F  {}"

    definition is_lasso_prpl where "is_lasso_prpl L  
      is_lasso_prpl_pre L
       (set (snd L))  F  {}"
    
    lemma is_lasso_pre_ext[simp]: 
      "gbg.is_lasso_pre T m = is_lasso_pre"
      unfolding gbg.is_lasso_pre_def[abs_def] is_lasso_pre_def[abs_def]
      unfolding to_gbg_ext_def
      by auto

    lemma is_lasso_gbg: 
      "gbg.is_lasso T m = is_lasso"
      unfolding is_lasso_def[abs_def] gbg.is_lasso_def[abs_def]
      apply simp
      apply (auto simp: to_gbg_ext_def lasso_cycle_def)
      done

    lemmas lasso_accepted = gbg.lasso_accepted[unfolded to_gbg_alt is_lasso_gbg]
    lemmas accepted_lasso = gbg.accepted_lasso[unfolded to_gbg_alt is_lasso_gbg]

    lemma is_lasso_prpl_of_lasso[simp]: 
      "is_lasso_prpl (prpl_of_lasso L)  is_lasso L"
      unfolding is_lasso_def is_lasso_prpl_def
      unfolding lasso_v0_def lasso_cycle_def
      by auto
  
    lemma is_lasso_prpl_conv: 
      "is_lasso_prpl prpl  (snd prpl[]  is_lasso (lasso_of_prpl prpl))"
      unfolding is_lasso_def is_lasso_prpl_def is_lasso_prpl_pre_conv
      apply safe
      apply auto
      done

    lemma lasso_prpl_acc_run:
      "is_lasso_prpl (pr, pl)  is_acc_run (pr  iter pl)"
      apply (clarsimp simp: is_lasso_prpl_conv)
      apply (drule lasso_accepted)
      apply (simp add: run_of_lasso_of_prpl)
      done

  end

  context igb_graph begin
    definition "is_lasso L   
      is_lasso_pre L
       (i<num_acc. qset (lasso_cycle L). iacc q)"

    definition "is_lasso_prpl L   
      is_lasso_prpl_pre L
       (i<num_acc. qset (snd L). iacc q)"

    lemma is_lasso_prpl_of_lasso[simp]: 
      "is_lasso_prpl (prpl_of_lasso L)  is_lasso L"
      unfolding is_lasso_def is_lasso_prpl_def
      unfolding lasso_v0_def lasso_cycle_def
      by auto
  
    lemma is_lasso_prpl_conv: 
      "is_lasso_prpl prpl  (snd prpl[]  is_lasso (lasso_of_prpl prpl))"
      unfolding is_lasso_def is_lasso_prpl_def is_lasso_prpl_pre_conv
      apply safe
      apply auto
      done

    lemma is_lasso_pre_ext[simp]: 
      "gbg.is_lasso_pre T m = is_lasso_pre"
      unfolding gbg.is_lasso_pre_def[abs_def] is_lasso_pre_def[abs_def]
      unfolding to_gbg_ext_def
      by auto

    lemma is_lasso_gbg: "gbg.is_lasso T m = is_lasso"
      unfolding is_lasso_def[abs_def] gbg.is_lasso_def[abs_def]
      apply simp
      apply (simp_all add: to_gbg_ext_def)
      apply (intro ext)
      apply (fo_rule arg_cong | intro ext)+
      apply (auto simp: F_def accn_def intro!: ext)
      done

    lemmas lasso_accepted = gbg.lasso_accepted[unfolded to_gbg_alt is_lasso_gbg]
    lemmas accepted_lasso = gbg.accepted_lasso[unfolded to_gbg_alt is_lasso_gbg]

    lemma lasso_prpl_acc_run:
      "is_lasso_prpl (pr, pl)  is_acc_run (pr  iter pl)"
      apply (clarsimp simp: is_lasso_prpl_conv)
      apply (drule lasso_accepted)
      apply (simp add: run_of_lasso_of_prpl)
      done

    lemma degen_lasso_sound:
      assumes A: "degen.is_lasso T m L"
      shows "is_lasso (map_lasso fst L)"
    proof -
        
      from A have 
        V0: "lasso_v0 L  degen.V0 T m" and
        REACH: "path (degen.E T m) 
                 (lasso_v0 L) (lasso_reach L) (lasso_va L)" and
        LOOP: "path (degen.E T m) 
                  (lasso_va L) (lasso_cycle L) (lasso_va L)" and
        ACC: "(set (lasso_cycle L))  degen.F T m  {}"
        unfolding degen.is_lasso_def degen.is_lasso_pre_def by auto

      {
        fix i
        assume "i<num_acc"
        hence "qset (lasso_cycle L). i  local.acc (fst q)  snd q = i"
        proof (induction i)
          case 0
          thus ?case using ACC unfolding degeneralize_ext_def by fastforce
        next
          case (Suc i)
          then obtain q where "(q,i)set (lasso_cycle L)" and "iacc q" by auto
          with LOOP obtain pl' where SPL: "set (lasso_cycle L) = set pl'" 
            and PS: "path (degen.E T m) (q,i) pl' (q,i)"
            by (blast elim: path_loop_shift)
          from SPL have "pl'[]" by (auto simp: lasso_cycle_def)
          then obtain pl'' where [simp]: "pl'=(q,i)#pl''" 
            using PS by (cases pl') (auto simp: path_simps)
          then obtain q2 pl''' where 
            [simp]: "pl'' = (q2,(i + 1) mod num_acc)#pl'''"
            using PS iacc q ‹Suc i < num_acc›
            apply (cases pl'') 
            apply (auto 
              simp: path_simps degeneralize_ext_def 
              split: if_split_asm)
            done
          from PS have 
            "path (degen.E T m) (q2,Suc i) pl'' (q,i)"
            using ‹Suc i < num_acc›
            by (auto simp: path_simps)
          from degen_visit_acc[OF this] obtain qa 
            where "(qa,Suc i)set pl''" "Suc i  acc qa" 
            by auto
          thus ?case
            by (rule_tac bexI[where x="(qa,Suc i)"]) (auto simp: SPL)
        qed
      } note aux=this

      from degen_V0_sound[OF V0] 
        degen_path_sound[OF REACH] 
        degen_path_sound[OF LOOP] aux
      show ?thesis
        unfolding is_lasso_def is_lasso_pre_def
        by auto
    qed

  end


  definition lasso_rel_ext_internal_def: "Re R. lasso_rel_ext Re R  {
    ( lasso_reach = r', lasso_va = va', lasso_cysfx = cysfx', =m' , 
      lasso_reach = r, lasso_va = va, lasso_cysfx = cysfx, =m ) |
      r' r va' va cysfx' cysfx m' m. 
      (r',r)  Rlist_rel 
     (va',va)R
     (cysfx', cysfx)  Rlist_rel
     (m',m)  Re
    }"


  lemma lasso_rel_ext_def: " Re R. Re,Rlasso_rel_ext = {
    ( lasso_reach = r', lasso_va = va', lasso_cysfx = cysfx', =m' , 
      lasso_reach = r, lasso_va = va, lasso_cysfx = cysfx, =m ) |
      r' r va' va cysfx' cysfx m' m. 
      (r',r)  Rlist_rel 
     (va',va)R
     (cysfx', cysfx)  Rlist_rel
     (m',m)  Re
    }"
    unfolding lasso_rel_ext_internal_def relAPP_def by auto

  lemma lasso_rel_ext_sv[relator_props]: 
    " Re R.  single_valued Re; single_valued R   single_valued (Re,Rlasso_rel_ext)"
    unfolding lasso_rel_ext_def
    apply (rule single_valuedI)
    apply safe
    apply (blast dest: single_valuedD list_rel_sv[THEN single_valuedD])+
    done

  lemma lasso_rel_ext_id[relator_props]: 
    "Re R.  Re=Id; R=Id   Re,Rlasso_rel_ext = Id"
    unfolding lasso_rel_ext_def
    apply simp
    apply safe
    by (metis lasso.surjective)

  consts i_lasso_ext :: "interface  interface  interface"

  lemmas [autoref_rel_intf] = REL_INTFI[of lasso_rel_ext i_lasso_ext]

  find_consts "(_,_) lasso_scheme"
  term lasso_reach_update

  lemma lasso_param[param, autoref_rules]:
    "Re R. (lasso_reach, lasso_reach)  Re,Rlasso_rel_ext  Rlist_rel"
    "Re R. (lasso_va, lasso_va)  Re,Rlasso_rel_ext  R"
    "Re R. (lasso_cysfx, lasso_cysfx)  Re,Rlasso_rel_ext  Rlist_rel"
    "Re R. (lasso_ext, lasso_ext) 
       Rlist_rel  R  Rlist_rel  Re  Re,Rlasso_rel_ext"
    "Re R. (lasso_reach_update, lasso_reach_update) 
       (Rlist_rel  Rlist_rel)  Re,Rlasso_rel_ext  Re,Rlasso_rel_ext"
    "Re R. (lasso_va_update, lasso_va_update) 
       (RR)  Re,Rlasso_rel_ext  Re,Rlasso_rel_ext"
    "Re R. (lasso_cysfx_update, lasso_cysfx_update) 
       (Rlist_rel  Rlist_rel)  Re,Rlasso_rel_ext  Re,Rlasso_rel_ext"
    "Re R. (lasso.more_update, lasso.more_update) 
       (ReRe)  Re,Rlasso_rel_ext  Re,Rlasso_rel_ext"
    unfolding lasso_rel_ext_def
    by (auto dest: fun_relD)


  lemma lasso_param2[param, autoref_rules]:
    "Re R. (lasso_v0, lasso_v0)  Re,Rlasso_rel_ext  R"
    "Re R. (lasso_cycle, lasso_cycle)  Re,Rlasso_rel_ext  Rlist_rel"
    "Re R. (map_lasso, map_lasso) 
       (RR')  Re,Rlasso_rel_ext  unit_rel,R'lasso_rel_ext"
    unfolding lasso_v0_def[abs_def] lasso_cycle_def[abs_def] map_lasso_def[abs_def]
    by parametricity+


  lemma lasso_of_prpl_param: "(l',l)Rlist_rel ×r Rlist_rel; snd l  [] 
     (lasso_of_prpl l', lasso_of_prpl l)  unit_rel,Rlasso_rel_ext"
    unfolding lasso_of_prpl_def
    apply (cases l, cases l', clarsimp)
    apply (case_tac b, simp, case_tac ba, clarsimp_all)
    apply parametricity
    done

  context begin interpretation autoref_syn .

  lemma lasso_of_prpl_autoref[autoref_rules]:
    assumes "SIDE_PRECOND (snd l  [])"
    assumes "(l',l)Rlist_rel ×r Rlist_rel"
    shows "(lasso_of_prpl l', 
      (OP lasso_of_prpl 
        ::: Rlist_rel ×r Rlist_rel  unit_rel,Rlasso_rel_ext)$l) 
       unit_rel,Rlasso_rel_ext"
    using assms
    apply (simp add: lasso_of_prpl_param)
    done

  end




  subsection ‹Implementing runs by lassos›
  
  definition lasso_run_rel_def_internal: 
    "lasso_run_rel R  br run_of_lasso (λ_. True) O (nat_rel  R)"
  lemma lasso_run_rel_def: 
    "Rlasso_run_rel = br run_of_lasso (λ_. True) O (nat_rel  R)"
    unfolding lasso_run_rel_def_internal relAPP_def by simp

  lemma lasso_run_rel_sv[relator_props]: 
    "single_valued R  single_valued (Rlasso_run_rel)"
    unfolding lasso_run_rel_def
    by tagged_solver

  consts i_run :: "interface  interface"

  lemmas [autoref_rel_intf] = REL_INTFI[of lasso_run_rel i_run]

  definition [simp]: "op_map_run  (o)"

  lemma [autoref_op_pat]: "(o)  op_map_run" by simp

  lemma map_lasso_run_refine[autoref_rules]:
    shows "(map_lasso,op_map_run)  (RR')  Rlasso_run_rel  R'lasso_run_rel"
    unfolding lasso_run_rel_def op_map_run_def
  proof (intro fun_relI)
    fix f f' l r
    assume [param]: "(f,f')RR'" and 
      "(l, r)  br run_of_lasso (λ_. True) O (nat_rel  R)"
    then obtain r' where [param]: "(r',r)nat_rel  R" 
      and [simp]: "r' = run_of_lasso l" 
      by (auto simp: br_def)
    
    have "(map_lasso f l, f o r')  br run_of_lasso (λ_. True)" 
      by (simp add: br_def)
    also have "(f o r', f' o r)  nat_rel  R'" by parametricity
    finally (relcompI) show 
      "(map_lasso f l, f' o r)  br run_of_lasso (λ_. True) O (nat_rel  R')" 
      .
  qed

end

Theory Simulation

section ‹Simulation›
theory Simulation
imports Automata
begin

  lemma finite_ImageI:
    assumes "finite A"  
    assumes "a. aA  finite (R``{a})"
    shows "finite (R``A)"
  proof -
    note [[simproc add: finite_Collect]]
    have "R``A = {R``{a} | a. a:A}"
      by auto
    also have "finite ({R``{a} | a. a:A})"
      apply (rule finite_Union)
      apply (simp add: assms)
      apply (clarsimp simp: assms)
      done
    finally show ?thesis .
  qed


  section ‹Simulation›


  subsection ‹Functional Relations›

  definition "the_br_α R  λ x. SOME y. (x, y)  R"
  abbreviation (input) "the_br_invar R  λ x. x  Domain R"

  lemma the_br[simp]: 
    assumes "single_valued R"  
    shows "br (the_br_α R) (the_br_invar R) = R"
    unfolding build_rel_def the_br_α_def
    apply auto
    apply (metis someI_ex)
    apply (metis assms someI_ex single_valuedD)
    done

  lemma the_br_br[simp]: 
    "I x  the_br_α (br α I) x = α x"
    "the_br_invar (br α I) = I"
    unfolding the_br_α_def build_rel_def[abs_def]
    by auto

  subsection ‹Relation between Runs›

  definition run_rel :: "('a × 'b) set  ('a word × 'b word) set" where
    "run_rel R  {(ra, rb).  i. (ra i, rb i)  R}"

  lemma run_rel_converse[simp]: "(ra, rb)  run_rel (R¯)  (rb, ra)  run_rel R"  
    unfolding run_rel_def by auto

  lemma run_rel_single_valued: "single_valued R 
     (ra, rb)  run_rel R  ((i. the_br_invar R (ra i))  rb = the_br_α R o ra)"
    unfolding run_rel_def the_br_α_def
    apply (auto intro!: ext)
    apply (metis single_valuedD someI_ex)
    apply (metis DomainE someI_ex)
    done

  subsection ‹Simulation›
  locale simulation =
    a: graph A +
    b: graph B
    for R :: "('a × 'b) set"
    and A :: "('a, _) graph_rec_scheme"
    and B :: "('b, _) graph_rec_scheme"
    +
    assumes nodes_sim: "a  a.V  (a, b)  R  b  b.V"
    assumes init_sim: "a0  a.V0   b0. b0  b.V0  (a0, b0)  R"
    assumes step_sim: "(a, a')  a.E  (a, b)  R   b'. (b, b')  b.E  (a', b')  R"
  begin

    lemma simulation_this: "simulation R A B" by unfold_locales

    lemma run_sim: 
      assumes arun: "a.is_run ra"
      obtains rb where "b.is_run rb" "(ra, rb)  run_rel R"
    proof -
      from arun have ainit: "ra 0  a.V0" 
        and astep: "i. (ra i, ra (Suc i))  a.E"
        using a.run_V0 a.run_ipath ipathD by blast+
      from init_sim obtain rb0 where rel0: "(ra 0, rb0)  R" and binit: "rb0  b.V0"
        by (auto intro: ainit)
  
      define rb
        where "rb = rec_nat rb0 (λi rbi. SOME rbsi. (rbi, rbsi)  b.E  (ra (Suc i), rbsi)  R)"
      
      have [simp]: 
        "rb 0 = rb0" 
        "i. rb (Suc i) = (SOME rbsi. (rb i, rbsi)  b.E  (ra (Suc i), rbsi)  R)"
        unfolding rb_def by auto
  
      {
        fix i
        have "(rb i, rb (Suc i))  b.E  (ra (Suc i), rb (Suc i))  R"
        proof (induction i)
          case 0
          from step_sim astep rel0 obtain rb1 where "(rb 0, rb1)  b.E" and "(ra 1, rb1)  R"
            by fastforce
          thus ?case by (auto intro!: someI)
        next
          case (Suc i)
          with step_sim astep obtain rbss where "(rb (Suc i), rbss)  b.E" and
            "(ra (Suc (Suc i)), rbss)  R"
            by fastforce
          thus ?case by (auto intro!: someI)
        qed
      } note aux=this
      
      from aux binit have "b.is_run rb"
        unfolding b.is_run_def ipath_def by simp
      moreover from aux rel0 have "(ra, rb)  run_rel R"
        unfolding run_rel_def
        apply safe
        apply (case_tac i)
        by auto
      ultimately show ?thesis by rule
    qed

    lemma stuck_sim: 
      assumes "(a, b)  R"
      assumes "b  Domain b.E"
      shows "a  Domain a.E"
      using assms
      by (auto dest: step_sim)

    lemma run_Domain: "a.is_run r  r i  Domain R"
      by (erule run_sim) (auto simp: run_rel_def)

    lemma br_run_sim:
      assumes "R = br α I"
      assumes "a.is_run r"
      shows "b.is_run (α o r)"
      using assms
      apply -
      apply (erule run_sim)
      apply (auto simp: run_rel_def build_rel_def a.is_run_def b.is_run_def ipath_def)
      done

    lemma is_reachable_sim: "a  a.E* `` a.V0   b. (a, b)  R  b  b.E* `` b.V0"
      apply safe
      apply (erule rtrancl_induct)
      apply (metis ImageI init_sim rtrancl.rtrancl_refl)
      apply (metis rtrancl_image_advance step_sim)
      done

    lemma reachable_sim: "a.E* `` a.V0  R¯ `` b.E* `` b.V0"
      using is_reachable_sim by blast

    lemma reachable_finite_sim:
      assumes "finite (b.E* `` b.V0)"
      assumes "b. b  b.E* `` b.V0  finite (R¯ `` {b})"
      shows "finite (a.E* `` a.V0)"
      apply (rule finite_subset[OF reachable_sim])
      apply (rule finite_ImageI)
      apply fact+
      done

  end  

  lemma simulation_trans[trans]:
    assumes "simulation R1 A B"
    assumes "simulation R2 B C"
    shows "simulation (R1 O R2) A C"
  proof -
    interpret s1: simulation R1 A B by fact
    interpret s2: simulation R2 B C by fact
    show ?thesis
      apply unfold_locales
      using s1.nodes_sim s2.nodes_sim apply blast
      using s1.init_sim s2.init_sim apply blast
      using s1.step_sim s2.step_sim apply blast
      done
  qed

  lemma (in graph) simulation_refl[simp]: "simulation Id G G" by unfold_locales auto

  locale lsimulation = 
    a: sa A +
    b: sa B +
    simulation R A B
    for R :: "('a × 'b) set"
    and A :: "('a, 'l, _) sa_rec_scheme"
    and B :: "('b, 'l, _) sa_rec_scheme"
    +
    assumes labeling_consistent: "(a, b)  R  a.L a = b.L b"
  begin

    lemma lsimulation_this: "lsimulation R A B" by unfold_locales

    lemma run_rel_consistent: "(ra, rb)  run_rel R  a.L o ra = b.L o rb"
      using labeling_consistent unfolding run_rel_def
      by auto

    lemma accept_sim: "a.accept w  b.accept w"
      unfolding a.accept_def b.accept_def
      apply clarsimp
      apply (erule run_sim)
      apply (auto simp: run_rel_consistent)
      done

  end

  lemma lsimulation_trans[trans]: 
    assumes "lsimulation R1 A B"
    assumes "lsimulation R2 B C"
    shows "lsimulation (R1 O R2) A C"
  proof -
    interpret s1: lsimulation R1 A B by fact
    interpret s2: lsimulation R2 B C by fact
    interpret simulation "R1 O R2" A C
      using simulation_trans s1.simulation_this s2.simulation_this by this
    show ?thesis
      apply unfold_locales
      using s1.labeling_consistent s2.labeling_consistent 
      by auto
  qed

  lemma (in sa) lsimulation_refl[simp]: "lsimulation Id G G" by unfold_locales auto


  subsection ‹Bisimulation›

  locale bisimulation = 
    a: graph A +
    b: graph B +
    s1: simulation "R" A B +
    s2: simulation "R¯" B A
    for R :: "('a × 'b) set"
    and A :: "('a, _) graph_rec_scheme"
    and B :: "('b, _) graph_rec_scheme"
  begin

    lemma bisimulation_this: "bisimulation R A B" by unfold_locales

    lemma converse: "bisimulation (R¯) B A"
    proof -
      interpret simulation "(R¯)¯" A B by simp unfold_locales
      show ?thesis by unfold_locales
    qed

    lemma br_run_conv:
      assumes "R = br α I"
      shows "b.is_run rb  (ra. rb=α o ra  a.is_run ra)"
      using assms
      apply safe
      apply (erule s2.run_sim, auto 
        intro!: ext
        simp: run_rel_def build_rel_def) []
      apply (erule s1.br_run_sim, assumption)
      done

    lemma bri_run_conv:
      assumes "R = (br γ I)¯"
      shows "a.is_run ra  (rb. ra=γ o rb  b.is_run rb)"
      using assms
      apply safe
      apply (erule s1.run_sim, auto simp: run_rel_def build_rel_def intro!: ext) []

      apply (erule s2.run_sim, auto simp: run_rel_def build_rel_def)
      by (metis (no_types, hide_lams) fun_comp_eq_conv)
  
    lemma inj_map_run_eq:
      assumes "inj α"
      assumes E: "α o r1 = α o r2"
      shows "r1 = r2"
    proof (rule ext)
      fix i
      from E have "α (r1 i) = α (r2 i)"
        by (simp add: comp_def) metis
      with ‹inj α show "r1 i = r2 i" 
        by (auto dest: injD)
    qed

    lemma br_inj_run_conv:
      assumes INJ: "inj α"
      assumes [simp]: "R = br α I"
      shows "b.is_run (α o ra)  a.is_run ra"
      apply (subst br_run_conv[OF assms(2)])
      apply (auto dest: inj_map_run_eq[OF INJ])
      done

    lemma single_valued_run_conv:
      assumes "single_valued R"
      shows "b.is_run rb 
         (ra. rb=the_br_α R o ra  a.is_run ra)"
      using assms
      apply safe
      apply (erule s2.run_sim)
      apply (auto simp add: run_rel_single_valued)
      apply (erule s1.run_sim)
      apply (auto simp add: run_rel_single_valued)
      done

    lemma stuck_bisim: 
      assumes A: "(a, b)  R"
      shows "a  Domain a.E  b  Domain b.E"
      using s1.stuck_sim[OF A]
      using s2.stuck_sim[OF A[THEN converseI[of _ _ R]]]
      by blast

  end

  lemma bisimulation_trans[trans]:
    assumes "bisimulation R1 A B" 
    assumes "bisimulation R2 B C"
    shows "bisimulation (R1 O R2) A C"
  proof -
    interpret s1: bisimulation R1 A B by fact
    interpret s2: bisimulation R2 B C by fact
    interpret t1: simulation "(R1 O R2)" A C
      using simulation_trans s1.s1.simulation_this s2.s1.simulation_this by this
    interpret t2: simulation "(R1 O R2)¯" C A
      using simulation_trans s2.s2.simulation_this s1.s2.simulation_this
      unfolding converse_relcomp
      by this
    show ?thesis by unfold_locales
  qed

  lemma (in graph) bisimulation_refl[simp]: "bisimulation Id G G" by unfold_locales auto

  locale lbisimulation = 
    a: sa A +
    b: sa B +
    s1: lsimulation "R" A B +
    s2: lsimulation "R¯" B A +
    bisimulation R A B
    for R :: "('a × 'b) set"
    and A :: "('a, 'l, _) sa_rec_scheme"
    and B :: "('b, 'l, _) sa_rec_scheme"
  begin

    lemma lbisimulation_this: "lbisimulation R A B" by unfold_locales

    lemma accept_bisim: "a.accept = b.accept"
      apply (rule ext)
      using s1.accept_sim s2.accept_sim by blast

  end

  lemma lbisimulation_trans[trans]:
    assumes "lbisimulation R1 A B" 
    assumes "lbisimulation R2 B C"
    shows "lbisimulation (R1 O R2) A C"
  proof -
    interpret s1: lbisimulation R1 A B by fact
    interpret s2: lbisimulation R2 B C by fact

    from lsimulation_trans[OF s1.s1.lsimulation_this s2.s1.lsimulation_this]
    interpret t1: lsimulation "(R1 O R2)" A C .

    from lsimulation_trans[OF s2.s2.lsimulation_this s1.s2.lsimulation_this, folded converse_relcomp]
    interpret t2: lsimulation "(R1 O R2)¯" C A .

    show ?thesis by unfold_locales
  qed

  lemma (in sa) lbisimulation_refl[simp]: "lbisimulation Id G G" by unfold_locales auto

end

Theory Step_Conv

theory Step_Conv
imports Main
begin
  (* Different ways of representing transitions, 
    and functions to convert between them:

    rel :: ('a × 'b) set
    pred :: 'a ⇒ 'b ⇒ bool
    succ :: 'a ⇒ 'b set
  *)

  definition "rel_of_pred s  {(a,b). s a b}"
  definition "rel_of_succ s  {(a,b). bs a}"

  definition "pred_of_rel s  λa b. (a,b)s"
  definition "pred_of_succ s  λa b. bs a"

  definition "succ_of_rel s  λa. {b. (a,b)s}"
  definition "succ_of_pred s  λa. {b. s a b}"

  lemma rps_expand[simp]:
    "(a,b)rel_of_pred p  p a b"
    "(a,b)rel_of_succ s  b  s a"

    "pred_of_rel r a b  (a,b)r"
    "pred_of_succ s a b  b  s a"

    "bsucc_of_rel r a  (a,b)r"
    "bsucc_of_pred p a  p a b"
    unfolding rel_of_pred_def pred_of_rel_def
    unfolding rel_of_succ_def succ_of_rel_def
    unfolding pred_of_succ_def succ_of_pred_def
    by auto

  lemma rps_conv[simp]:
    "rel_of_pred (pred_of_rel r) = r"
    "rel_of_pred (pred_of_succ s) = rel_of_succ s"

    "rel_of_succ (succ_of_rel r) = r"
    "rel_of_succ (succ_of_pred p) = rel_of_pred p"

    "pred_of_rel (rel_of_pred p) = p"
    "pred_of_rel (rel_of_succ s) = pred_of_succ s"

    "pred_of_succ (succ_of_pred p) = p"
    "pred_of_succ (succ_of_rel r) = pred_of_rel r"

    "succ_of_rel (rel_of_succ s) = s"
    "succ_of_rel (rel_of_pred p) = succ_of_pred p"

    "succ_of_pred (pred_of_succ s) = s"
    "succ_of_pred (pred_of_rel r) = succ_of_rel r"
    unfolding rel_of_pred_def pred_of_rel_def
    unfolding rel_of_succ_def succ_of_rel_def
    unfolding pred_of_succ_def succ_of_pred_def
    by auto

  (* Lifting transitions from option monad to option×option *)
  definition m2r_rel :: "('a × 'a option) set  'a option rel"
    where "m2r_rel r  {(Some a,b)|a b. (a,b)r}"

  definition m2r_pred :: "('a  'a option  bool)  'a option  'a option  bool"
    where "m2r_pred p  λNone  λ_. False | Some a  p a"

  definition m2r_succ :: "('a  'a option set)  'a option  'a option set"
    where "m2r_succ s  λNone  {} | Some a  s a"

  lemma m2r_expand[simp]:
    "(a,b)m2r_rel r  (a'. a=Some a'  (a',b)r)"
    "m2r_pred p a b  (a'. a=Some a'  p a' b)"
    "bm2r_succ s a  (a'. a=Some a'  b  s a')"
    unfolding m2r_rel_def m2r_succ_def m2r_pred_def
    by (auto split: option.splits)

  lemma m2r_conv[simp]:
    "m2r_rel (rel_of_succ s) = rel_of_succ (m2r_succ s)"
    "m2r_rel (rel_of_pred p) = rel_of_pred (m2r_pred p)"

    "m2r_pred (pred_of_succ s) = pred_of_succ (m2r_succ s)"
    "m2r_pred (pred_of_rel r) = pred_of_rel (m2r_rel r)"

    "m2r_succ (succ_of_pred p) = succ_of_pred (m2r_pred p)"
    "m2r_succ (succ_of_rel r) = succ_of_rel (m2r_rel r)"
    unfolding rel_of_pred_def pred_of_rel_def
    unfolding rel_of_succ_def succ_of_rel_def
    unfolding pred_of_succ_def succ_of_pred_def
    unfolding m2r_rel_def m2r_succ_def m2r_pred_def
    by (auto split: option.splits)


  definition "rel_of_enex enex  let (en, ex) = enex in {(s, ex a s) |s a. a  en s}"
  definition "pred_of_enex enex  λs s'. let (en,ex) = enex in aen s. s'=ex a s"
  definition "succ_of_enex enex  λs. let (en,ex) = enex in {s'. aen s. s'=ex a s}"
  
  lemma x_of_enex_expand[simp]: 
    "(s, s')  rel_of_enex (en, ex)  ( a  en s. s' = ex a s)"
    "pred_of_enex (en,ex) s s'  (aen s. s'=ex a s)"
    "s'succ_of_enex (en,ex) s  (aen s. s'=ex a s)"
    unfolding rel_of_enex_def pred_of_enex_def succ_of_enex_def by auto
  
  lemma x_of_enex_conv[simp]:
    "rel_of_pred (pred_of_enex enex) = rel_of_enex enex"
    "rel_of_succ (succ_of_enex enex) = rel_of_enex enex"
    "pred_of_rel (rel_of_enex enex) = pred_of_enex enex"
    "pred_of_succ (succ_of_enex enex) = pred_of_enex enex"
    "succ_of_rel (rel_of_enex enex) = succ_of_enex enex"
    "succ_of_pred (pred_of_enex enex) = succ_of_enex enex"
    unfolding rel_of_enex_def pred_of_enex_def succ_of_enex_def 
    unfolding rel_of_pred_def rel_of_succ_def
    unfolding pred_of_rel_def pred_of_succ_def
    unfolding succ_of_rel_def succ_of_pred_def
    by auto

end

Theory Stuttering_Extension

theory Stuttering_Extension
imports Simulation Step_Conv
begin

  definition stutter_extend_edges :: "'v set  'v digraph  'v digraph"
    where "stutter_extend_edges V E  E  {(v, v) |v. v  V  v  Domain E}"

  lemma stutter_extend_edgesI_edge:
    assumes "(u, v)  E"
    shows "(u, v)  stutter_extend_edges V E"
    using assms unfolding stutter_extend_edges_def by auto
  lemma stutter_extend_edgesI_stutter:
    assumes "v  V" "v  Domain E"
    shows "(v, v)  stutter_extend_edges V E"
    using assms unfolding stutter_extend_edges_def by auto
  lemma stutter_extend_edgesE:
    assumes "(u, v)  stutter_extend_edges V E"
    obtains (edge) "(u, v)  E" | (stutter) "u  V" "u  Domain E" "u = v"
    using assms unfolding stutter_extend_edges_def by auto

  lemma stutter_extend_wf: "E  V × V  stutter_extend_edges V E  V × V"
    unfolding stutter_extend_edges_def by auto

  lemma stutter_extend_edges_rtrancl[simp]: "(stutter_extend_edges V E)* = E*"
    unfolding stutter_extend_edges_def by (auto intro: in_rtrancl_UnI elim: rtrancl_induct)

  lemma stutter_extend_domain: "V  Domain (stutter_extend_edges V E)"
    unfolding stutter_extend_edges_def by auto

  definition stutter_extend :: "('v, _) graph_rec_scheme  ('v, _) graph_rec_scheme"
    where "stutter_extend G 
    
      g_V = g_V G,
      g_E = stutter_extend_edges (g_V G) (g_E G),
      g_V0 = g_V0 G,
       = graph_rec.more G
    "

  lemma stutter_extend_simps[simp]:
    "g_V (stutter_extend G) = g_V G"
    "g_E (stutter_extend G) = stutter_extend_edges (g_V G) (g_E G)"
    "g_V0 (stutter_extend G) = g_V0 G"
    unfolding stutter_extend_def by auto

  lemma stutter_extend_simps_sa[simp]:
    "sa_L (stutter_extend G) = sa_L G"
    unfolding stutter_extend_def
    by (metis graph_rec.select_convs(4) sa_rec.select_convs(1) sa_rec.surjective)

  lemma (in graph) stutter_extend_graph: "graph (stutter_extend G)"
    using V0_ss E_ss by (unfold_locales, auto intro!: stutter_extend_wf)
  lemma (in sa) stutter_extend_sa: "sa (stutter_extend G)"
  proof -
    interpret graph "stutter_extend G" using stutter_extend_graph by this
    show ?thesis by unfold_locales
  qed

  lemma (in bisimulation) stutter_extend: "bisimulation R (stutter_extend A) (stutter_extend B)"
  proof -
    interpret ea: graph "stutter_extend A" by (rule a.stutter_extend_graph)
    interpret eb: graph "stutter_extend B" by (rule b.stutter_extend_graph)
    show ?thesis
    proof
      fix a b
      assume "a  g_V (stutter_extend A)" "(a, b)  R"
      thus "b  g_V (stutter_extend B)" using s1.nodes_sim by simp
    next
      fix a
      assume "a  g_V0 (stutter_extend A)"
      thus " b. b  g_V0 (stutter_extend B)  (a, b)  R" using s1.init_sim by simp
    next
      fix a a' b
      assume "(a, a')  g_E (stutter_extend A)" "(a, b)  R"
      thus " b'. (b, b')  g_E (stutter_extend B)  (a', b')  R"
        apply simp
        using s1.nodes_sim s1.step_sim s2.stuck_sim 
        by (blast
          intro: stutter_extend_edgesI_edge stutter_extend_edgesI_stutter
          elim: stutter_extend_edgesE)
    next
      fix b a
      assume "b  g_V (stutter_extend B)" "(b, a)  R¯"
      thus "a  g_V (stutter_extend A)" using s2.nodes_sim by simp
    next
      fix b
      assume "b  g_V0 (stutter_extend B)"
      thus " a. a  g_V0 (stutter_extend A)  (b, a)  R¯" using s2.init_sim by simp
    next
      fix b b' a
      assume "(b, b')  g_E (stutter_extend B)" "(b, a)  R¯"
      thus " a'. (a, a')  g_E (stutter_extend A)  (b', a')  R¯"
        apply simp
        using s2.nodes_sim s2.step_sim s1.stuck_sim
        by (blast
          intro: stutter_extend_edgesI_edge stutter_extend_edgesI_stutter
          elim: stutter_extend_edgesE)
    qed
  qed

  lemma (in lbisimulation) lstutter_extend: "lbisimulation R (stutter_extend A) (stutter_extend B)"
  proof -
    interpret se: bisimulation R "stutter_extend A" "stutter_extend B" by (rule stutter_extend)
    show ?thesis by (unfold_locales, auto simp: s1.labeling_consistent)
  qed

  definition stutter_extend_en :: "('s'a set)  ('s  'a option set)" where
    "stutter_extend_en en  λs. let as = en s in if as={} then {None} else Some`as"
  
  definition stutter_extend_ex :: "('a  's  's)  ('a option  's  's)" where
    "stutter_extend_ex ex  λNone  id | Some a  ex a"

  abbreviation stutter_extend_enex 
    :: "('s'a set) × ('a  's  's)  ('s  'a option set) × ('a option  's  's)"
  where
   "stutter_extend_enex  map_prod stutter_extend_en stutter_extend_ex"
  
  lemma stutter_extend_pred_of_enex_conv:
    "stutter_extend_edges UNIV (rel_of_enex enex) = rel_of_enex (stutter_extend_enex enex)"
    unfolding rel_of_enex_def stutter_extend_edges_def
    apply (auto simp: stutter_extend_en_def stutter_extend_ex_def split: prod.splits)
    apply force
    apply blast
    done
  
  lemma stutter_extend_en_Some_eq[simp]:
    "Some a  stutter_extend_en en gc  a  en gc"
    "stutter_extend_ex ex (Some a) gc = ex a gc"
    unfolding stutter_extend_en_def stutter_extend_ex_def by auto
  
  lemma stutter_extend_ex_None_eq[simp]:
    "stutter_extend_ex ex None = id"
    unfolding stutter_extend_ex_def by auto

end

Theory Digraph_Impl

section ‹Implementing Graphs›
(* Author: Peter Lammich *)
theory Digraph_Impl
imports Digraph
begin

subsection ‹Directed Graphs by Successor Function›
type_synonym 'a slg = "'a  'a list"


definition slg_rel :: "('a×'b) set  ('a slg × 'b digraph) set" where 
  slg_rel_def_internal: "slg_rel R  
  (R  Rlist_set_rel) O br (λsuccs. {(u,v). vsuccs u}) (λ_. True)"

lemma slg_rel_def: "Rslg_rel = 
  (R  Rlist_set_rel) O br (λsuccs. {(u,v). vsuccs u}) (λ_. True)"
  unfolding slg_rel_def_internal relAPP_def by simp

lemma slg_rel_sv[relator_props]: 
  "single_valued R; Range R = UNIV  single_valued (Rslg_rel)"
  unfolding slg_rel_def
  by (tagged_solver)

consts i_slg :: "interface  interface"
lemmas [autoref_rel_intf] = REL_INTFI[of slg_rel i_slg]

definition [simp]: "op_slg_succs E v  E``{v}"

lemma [autoref_itype]: "op_slg_succs ::i Iii_slg i I i Iii_set" by simp

context begin interpretation autoref_syn .
lemma [autoref_op_pat]: "E``{v}  op_slg_succs$E$v" by simp
end

lemma refine_slg_succs[autoref_rules_raw]: 
  "(λsuccs v. succs v,op_slg_succs)Rslg_relRRlist_set_rel"
  apply (intro fun_relI)
  apply (auto simp add: slg_rel_def br_def dest: fun_relD)
  done

definition "E_of_succ succ  { (u,v). vsucc u }"
definition "succ_of_E E  (λu. {v . (u,v)E})"

lemma E_of_succ_of_E[simp]: "E_of_succ (succ_of_E E) = E"
  unfolding E_of_succ_def succ_of_E_def
  by auto

lemma succ_of_E_of_succ[simp]: "succ_of_E (E_of_succ E) = E"
  unfolding E_of_succ_def succ_of_E_def
  by auto


context begin interpretation autoref_syn .
  lemma [autoref_itype]: "E_of_succ ::i (I i Iii_set) i Iii_slg" by simp
  lemma [autoref_itype]: "succ_of_E ::i Iii_slg i I i Iii_set" by simp
end

lemma E_of_succ_refine[autoref_rules]:
  "(λx. x, E_of_succ)  (R  Rlist_set_rel)  Rslg_rel"
  "(λx. x, succ_of_E)  Rslg_rel  (R  Rlist_set_rel)"
  unfolding E_of_succ_def[abs_def] succ_of_E_def[abs_def] slg_rel_def br_def
  apply auto []
  apply clarsimp
  apply (blast dest: fun_relD)
  done


subsubsection ‹Restricting Edges›
definition op_graph_restrict :: "'v set  'v set  ('v × 'v) set  ('v × 'v) set"
  where [simp]: "op_graph_restrict Vl Vr E  E  Vl × Vr"

definition op_graph_restrict_left :: "'v set  ('v × 'v) set  ('v × 'v) set"
  where [simp]: "op_graph_restrict_left Vl E  E  Vl × UNIV"

definition op_graph_restrict_right :: "'v set  ('v × 'v) set  ('v × 'v) set"
  where [simp]: "op_graph_restrict_right Vr E  E  UNIV × Vr"

lemma [autoref_op_pat]: 
  "E  (Vl × Vr)  op_graph_restrict Vl Vr E"
  "E  (Vl × UNIV)  op_graph_restrict_left Vl E"
  "E  (UNIV × Vr)  op_graph_restrict_right Vr E"
  by simp_all

lemma graph_restrict_aimpl: "op_graph_restrict Vl Vr E = 
  E_of_succ (λv. if vVl then {x  E``{v}. xVr} else {})"
  by (auto simp: E_of_succ_def succ_of_E_def split: if_split_asm)
lemma graph_restrict_left_aimpl: "op_graph_restrict_left Vl E = 
  E_of_succ (λv. if vVl then E``{v} else {})"
  by (auto simp: E_of_succ_def succ_of_E_def split: if_split_asm)
lemma graph_restrict_right_aimpl: "op_graph_restrict_right Vr E = 
  E_of_succ (λv. {x  E``{v}. xVr})"
  by (auto simp: E_of_succ_def succ_of_E_def split: if_split_asm)

schematic_goal graph_restrict_impl_aux:
  fixes Rsl Rsr
  notes [autoref_rel_intf] = REL_INTFI[of Rsl i_set] REL_INTFI[of Rsr i_set]
  assumes [autoref_rules]: "(meml, (∈))  R  RRsl  bool_rel"
  assumes [autoref_rules]: "(memr, (∈))  R  RRsr  bool_rel"
  shows "(?c, op_graph_restrict)  RRsl  RRsr  Rslg_rel  Rslg_rel"
  unfolding graph_restrict_aimpl[abs_def]
  apply (autoref (keep_goal))
  done

schematic_goal graph_restrict_left_impl_aux:
  fixes Rsl Rsr
  notes [autoref_rel_intf] = REL_INTFI[of Rsl i_set] REL_INTFI[of Rsr i_set]
  assumes [autoref_rules]: "(meml, (∈))  R  RRsl  bool_rel"
  shows "(?c, op_graph_restrict_left)  RRsl  Rslg_rel  Rslg_rel"
  unfolding graph_restrict_left_aimpl[abs_def]
  apply (autoref (keep_goal, trace))
  done

schematic_goal graph_restrict_right_impl_aux:
  fixes Rsl Rsr
  notes [autoref_rel_intf] = REL_INTFI[of Rsl i_set] REL_INTFI[of Rsr i_set]
  assumes [autoref_rules]: "(memr, (∈))  R  RRsr  bool_rel"
  shows "(?c, op_graph_restrict_right)  RRsr  Rslg_rel  Rslg_rel"
  unfolding graph_restrict_right_aimpl[abs_def]
  apply (autoref (keep_goal, trace))
  done

concrete_definition graph_restrict_impl uses graph_restrict_impl_aux
concrete_definition graph_restrict_left_impl uses graph_restrict_left_impl_aux
concrete_definition graph_restrict_right_impl uses graph_restrict_right_impl_aux

context begin interpretation autoref_syn .
  lemma [autoref_itype]:
    "op_graph_restrict ::i Iii_set i Iii_set i Iii_slg i Iii_slg"
    "op_graph_restrict_right ::i Iii_set i Iii_slg i Iii_slg"
    "op_graph_restrict_left ::i Iii_set i Iii_slg i Iii_slg"
    by auto
end

lemmas [autoref_rules_raw] = 
  graph_restrict_impl.refine[OF GEN_OP_D GEN_OP_D]
  graph_restrict_left_impl.refine[OF GEN_OP_D]
  graph_restrict_right_impl.refine[OF GEN_OP_D]

schematic_goal "(?c::?'c, λ(E::nat digraph) x. E``{x})  ?R"
  apply (autoref (keep_goal))
  done

lemma graph_minus_aimpl: 
  fixes E1 E2 :: "'a rel"
  shows "E1-E2 = E_of_succ (λx. E1``{x} - E2``{x})"
  by (auto simp: E_of_succ_def)

schematic_goal graph_minus_impl_aux:
  fixes R :: "('vi×'v) set"
  assumes [autoref_rules]: "(eq,(=))RRbool_rel"
  shows "(?c, (-))  Rslg_rel  Rslg_rel  Rslg_rel"
  apply (subst graph_minus_aimpl[abs_def])
  apply (autoref (keep_goal,trace))
  done

lemmas [autoref_rules] = graph_minus_impl_aux[OF GEN_OP_D]


lemma graph_minus_set_aimpl: 
  fixes E1 E2 :: "'a rel"
  shows "E1-E2 = E_of_succ (λu. {vE1``{u}. (u,v)E2})"
  by (auto simp: E_of_succ_def)

schematic_goal graph_minus_set_impl_aux:
  fixes R :: "('vi×'v) set"
  assumes [autoref_rules]: "(eq,(=))RRbool_rel"
  assumes [autoref_rules]: "(mem,(∈))  R ×r R  R ×r RRs  bool_rel"
  shows "(?c, (-))  Rslg_rel  R×rRRs  Rslg_rel"
  apply (subst graph_minus_set_aimpl[abs_def])
  apply (autoref (keep_goal,trace))
  done

lemmas [autoref_rules (overloaded)] = graph_minus_set_impl_aux[OF GEN_OP_D GEN_OP_D]



subsection ‹Rooted Graphs›

subsubsection ‹Operation Identification Setup›

consts
  i_g_ext :: "interface  interface  interface"

abbreviation "i_frg  i_unitii_g_ext"

context begin interpretation autoref_syn .

lemma g_type[autoref_itype]:
  "g_V ::i Ie,Iii_g_ext i Iii_set"
  "g_E ::i Ie,Iii_g_ext i Iii_slg"
  "g_V0 ::i Ie,Iii_g_ext i Iii_set"
  "graph_rec_ext
    ::i Iii_set i Iii_slg i Iii_set i iE i Ie,Iii_g_ext" 
  by simp_all

end


subsubsection ‹Generic Implementation›
record ('vi,'ei,'v0i) gen_g_impl =
  gi_V :: 'vi
  gi_E :: 'ei
  gi_V0 :: 'v0i

definition gen_g_impl_rel_ext_internal_def: " Rm Rv Re Rv0. gen_g_impl_rel_ext Rm Rv Re Rv0
   { (gen_g_impl_ext Vi Ei V0i mi, graph_rec_ext V E V0 m) 
      | Vi Ei V0i mi V E V0 m. 
        (Vi,V)Rv  (Ei,E)Re  (V0i,V0)Rv0  (mi,m)Rm
    }"

lemma gen_g_impl_rel_ext_def: "Rm Rv Re Rv0. Rm,Rv,Re,Rv0gen_g_impl_rel_ext
   { (gen_g_impl_ext Vi Ei V0i mi, graph_rec_ext V E V0 m) 
      | Vi Ei V0i mi V E V0 m. 
        (Vi,V)Rv  (Ei,E)Re  (V0i,V0)Rv0  (mi,m)Rm
    }"
  unfolding gen_g_impl_rel_ext_internal_def relAPP_def by simp

lemma gen_g_impl_rel_sv[relator_props]: 
  "Rm Rv Re Rv0. single_valued Rv; single_valued Re; single_valued Rv0; single_valued Rm   
  single_valued (Rm,Rv,Re,Rv0gen_g_impl_rel_ext)"
  unfolding gen_g_impl_rel_ext_def
  apply (auto 
    intro!: single_valuedI 
    dest: single_valuedD slg_rel_sv list_set_rel_sv)
  done

lemma gen_g_refine:
  "Rm Rv Re Rv0. (gi_V,g_V)  Rm,Rv,Re,Rv0gen_g_impl_rel_ext  Rv"
  "Rm Rv Re Rv0. (gi_E,g_E)  Rm,Rv,Re,Rv0gen_g_impl_rel_ext  Re"
  "Rm Rv Re Rv0. (gi_V0,g_V0)  Rm,Rv,Re,Rv0gen_g_impl_rel_ext  Rv0"
  "Rm Rv Re Rv0. (gen_g_impl_ext, graph_rec_ext) 
     Rv  Re  Rv0  Rm  Rm,Rv,Re,Rv0gen_g_impl_rel_ext"
  unfolding gen_g_impl_rel_ext_def
  by auto

subsubsection ‹Implementation with list-set for Nodes›
type_synonym ('v,'m) frgv_impl_scheme = 
  "('v list, 'v  'v list, 'v list, 'm) gen_g_impl_scheme"

definition frgv_impl_rel_ext_internal_def: 
  "frgv_impl_rel_ext Rm Rv 
   Rm,Rvlist_set_rel,Rvslg_rel,Rvlist_set_relgen_g_impl_rel_ext"

lemma frgv_impl_rel_ext_def: "Rm,Rvfrgv_impl_rel_ext
   Rm,Rvlist_set_rel,Rvslg_rel,Rvlist_set_relgen_g_impl_rel_ext"
  unfolding frgv_impl_rel_ext_internal_def relAPP_def by simp

lemma [autoref_rel_intf]: "REL_INTF frgv_impl_rel_ext i_g_ext"
  by (rule REL_INTFI)

lemma [relator_props, simp]: 
  "single_valued Rv; Range Rv = UNIV; single_valued Rm 
   single_valued (Rm,Rvfrgv_impl_rel_ext)"
  unfolding frgv_impl_rel_ext_def by tagged_solver

lemmas [param, autoref_rules] = gen_g_refine[where 
  Rv = "Rvlist_set_rel" and Re = "Rvslg_rel" and ?Rv0.0 = "Rvlist_set_rel"
  for Rv, folded frgv_impl_rel_ext_def]

subsubsection ‹Implementation with Cfun for Nodes›
text ‹This implementation allows for the universal node set.›
type_synonym ('v,'m) g_impl_scheme = 
  "('v  bool, 'v  'v list, 'v list, 'm) gen_g_impl_scheme"

definition g_impl_rel_ext_internal_def: 
  "g_impl_rel_ext Rm Rv 
   Rm,Rvfun_set_rel,Rvslg_rel,Rvlist_set_relgen_g_impl_rel_ext"

lemma g_impl_rel_ext_def: "Rm,Rvg_impl_rel_ext
   Rm,Rvfun_set_rel,Rvslg_rel,Rvlist_set_relgen_g_impl_rel_ext"
  unfolding g_impl_rel_ext_internal_def relAPP_def by simp

lemma [autoref_rel_intf]: "REL_INTF g_impl_rel_ext i_g_ext"
  by (rule REL_INTFI)

lemma [relator_props, simp]: 
  "single_valued Rv; Range Rv = UNIV; single_valued Rm 
   single_valued (Rm,Rvg_impl_rel_ext)"
  unfolding g_impl_rel_ext_def by tagged_solver

lemmas [param, autoref_rules] = gen_g_refine[where 
  Rv = "Rvfun_set_rel" 
  and Re = "Rvslg_rel" 
  and ?Rv0.0 = "Rvlist_set_rel" 
  for Rv, folded g_impl_rel_ext_def]

lemma [autoref_rules]: "(gi_V_update, g_V_update)  (Rvfun_set_rel  Rvfun_set_rel) 
  Rm, Rvg_impl_rel_ext  Rm, Rvg_impl_rel_ext"
  unfolding g_impl_rel_ext_def gen_g_impl_rel_ext_def
  by (auto, metis (full_types) tagged_fun_relD_both)
lemma [autoref_rules]: "(gi_E_update, g_E_update)  (Rvslg_rel  Rvslg_rel) 
  Rm, Rvg_impl_rel_ext  Rm, Rvg_impl_rel_ext"
  unfolding g_impl_rel_ext_def gen_g_impl_rel_ext_def
  by (auto, metis (full_types) tagged_fun_relD_both)
lemma [autoref_rules]: "(gi_V0_update, g_V0_update)  (Rvlist_set_rel  Rvlist_set_rel) 
  Rm, Rvg_impl_rel_ext  Rm, Rvg_impl_rel_ext"
  unfolding g_impl_rel_ext_def gen_g_impl_rel_ext_def
  by (auto, metis (full_types) tagged_fun_relD_both)

(* HACK: The homgeneity rule heuristics erronously creates a homogeneity rule that
    equalizes Rv and Rv0, out of the frv-implementation, which happens to be the
    first. This declaration counters the undesired effects caused by this. *)
lemma [autoref_hom]: 
  "CONSTRAINT graph_rec_ext (RvRvs  RvRes  RvRv0s  Rm  Rm,RvRg)"
  by simp


schematic_goal "(?c::?'c, λG x. g_E G `` {x})?R"
  apply (autoref (keep_goal))
  done

schematic_goal "(?c,λV0 E.
    g_V = UNIV, g_E = E, g_V0 = V0   )
  Rlist_set_rel  Rslg_rel  unit_rel,Rg_impl_rel_ext"
  apply (autoref (keep_goal))
  done

schematic_goal "(?c,λV V0 E.
    g_V = V, g_E = E, g_V0 = V0   )
  Rlist_set_rel  Rlist_set_rel  Rslg_rel  unit_rel,Rfrgv_impl_rel_ext"
  apply (autoref (keep_goal))
  done

subsubsection ‹Renaming›

definition "the_inv_into_map V f x 
  = (if x  f`V then Some (the_inv_into V f x) else None)"

lemma the_inv_into_map_None[simp]:
  "the_inv_into_map V f x = None  x  f`V"
  unfolding the_inv_into_map_def by auto

lemma the_inv_into_map_Some':
  "the_inv_into_map V f x = Some y  x  f`V  y=the_inv_into V f x"
  unfolding the_inv_into_map_def by auto

lemma the_inv_into_map_Some[simp]:
  "inj_on f V  the_inv_into_map V f x = Some y  yV  x=f y"
  by (auto simp: the_inv_into_map_Some' the_inv_into_f_f)

definition "the_inv_into_map_impl V f = 
  FOREACH V (λx m. RETURN (m(f x  x))) Map.empty"

lemma the_inv_into_map_impl_correct:
  assumes [simp]: "finite V"
  assumes INJ: "inj_on f V"
  shows "the_inv_into_map_impl V f  SPEC (λr. r = the_inv_into_map V f)"
  unfolding the_inv_into_map_impl_def
  apply (refine_rcg 
    FOREACH_rule[where I="λit m. m=the_inv_into_map (V - it) f"]
    refine_vcg
  )

  apply (vc_solve 
    simp: the_inv_into_map_def[abs_def] it_step_insert_iff 
    intro!: ext)

  apply (intro allI impI conjI)

  apply (subst the_inv_into_f_f[OF subset_inj_on[OF INJ]], auto) []

  apply (subst the_inv_into_f_f[OF subset_inj_on[OF INJ]], auto) []

  apply safe []
  apply (subst the_inv_into_f_f[OF subset_inj_on[OF INJ]], (auto) [2])+
  apply simp
  done

schematic_goal the_inv_into_map_code_aux:
  fixes Rv' :: "('vti × 'vt) set"
  assumes [autoref_ga_rules]: "is_bounded_hashcode Rv' eq bhc"
  assumes [autoref_ga_rules]: "is_valid_def_hm_size TYPE('vti) (def_size)"
  assumes [autoref_rules]: "(Vi,V)Rvlist_set_rel"
  assumes [autoref_rules]: "(fi,f)RvRv'"
  shows "(RETURN ?c, the_inv_into_map_impl V f)  Rv',Rvahm_rel bhcnres_rel"
  unfolding the_inv_into_map_impl_def[abs_def]
  apply (autoref_monadic (plain))
  done

concrete_definition the_inv_into_map_code uses the_inv_into_map_code_aux
export_code the_inv_into_map_code checking SML

thm the_inv_into_map_code.refine

context begin interpretation autoref_syn .
lemma autoref_the_inv_into_map[autoref_rules]:
  fixes Rv' :: "('vti × 'vt) set"
  assumes "SIDE_GEN_ALGO (is_bounded_hashcode Rv' eq bhc)"
  assumes "SIDE_GEN_ALGO (is_valid_def_hm_size TYPE('vti) def_size)"
  assumes INJ: "SIDE_PRECOND (inj_on f V)"
  assumes V: "(Vi,V)Rvlist_set_rel"
  assumes F: "(fi,f)RvRv'"
  shows "(the_inv_into_map_code eq bhc def_size Vi fi, 
    (OP the_inv_into_map 
      ::: Rvlist_set_rel  (RvRv')  Rv', RvImpl_Array_Hash_Map.ahm_rel bhc)
    $V$f)  Rv', RvImpl_Array_Hash_Map.ahm_rel bhc"
proof simp

  from V have FIN: "finite V" using list_set_rel_range by auto

  note the_inv_into_map_code.refine[
    OF assms(1-2,4-5)[unfolded autoref_tag_defs], THEN nres_relD 
  ]
  also note the_inv_into_map_impl_correct[OF FIN INJ[unfolded autoref_tag_defs]]
  finally show "(the_inv_into_map_code eq bhc def_size Vi fi, the_inv_into_map V f)
     Rv', RvImpl_Array_Hash_Map.ahm_rel bhc"
    by (simp add: refine_pw_simps pw_le_iff)
qed

end

schematic_goal "(?c::?'c, do { 
  let s = {1,2,3::nat}; 
  ⌦‹ASSERT (inj_on Suc s);›
  RETURN (the_inv_into_map s Suc) })  ?R"
  apply (autoref (keep_goal))
  done


definition "fr_rename_ext_aimpl ecnv f G  do {
    ASSERT (inj_on f (g_V G));
    ASSERT (inj_on f (g_V0 G));
    let fi_map = the_inv_into_map (g_V G) f;
    e  ecnv fi_map G;
    RETURN 
      g_V = f`(g_V G),
      g_E = (E_of_succ (λv. case fi_map v of
          Some u  f ` (succ_of_E (g_E G) u) | None  {})),
      g_V0 = (f`g_V0 G),
       = e
    
  }"

context g_rename_precond begin

  definition "fi_map x = (if x  f`V then Some (fi x) else None)"
  lemma fi_map_alt: "fi_map = the_inv_into_map V f"
    apply (rule ext)
    unfolding fi_map_def the_inv_into_map_def fi_def
    by simp
    
  lemma fi_map_Some: "(fi_map u = Some v)  uf`V  fi u = v"
    unfolding fi_map_def by (auto split: if_split_asm)

  lemma fi_map_None: "(fi_map u = None)  uf`V"
    unfolding fi_map_def by (auto split: if_split_asm)

  lemma rename_E_aimpl_alt: "rename_E f E = E_of_succ (λv. case fi_map v of
    Some u  f ` (succ_of_E E u) | None  {})"
    unfolding E_of_succ_def succ_of_E_def
    using E_ss
    by (force 
      simp: fi_f f_fi fi_map_Some fi_map_None 
      split: if_split_asm option.splits)


  lemma frv_rename_ext_aimpl_alt: 
    assumes ECNV: "ecnv' fi_map G  SPEC (λr. r = ecnv G)"
    shows "fr_rename_ext_aimpl ecnv' f G 
       SPEC (λr. r = fr_rename_ext ecnv f G)"
  proof -
    (*have [simp]: "⦇ g_E =
             E_of_succ
              (λv. case the_inv_into_map V f v of None ⇒ {}
                 | Some u ⇒ f ` succ_of_E (g_E G) u),
            g_V0 = f ` g_V0 G, … = ecnv Gv⦈
      = frv_G (frv_rename_ext ecnv f Gv)"
      unfolding frv_rename_ext_def 
      by (auto simp: rename_E_aimpl_alt fi_map_alt)

    have [simp]: "⦇frv_V = f ` V, frv_G = frv_G Gv'⦈ = Gv'"
      unfolding frv_rename_ext_def
      by simp*)

    show ?thesis
      unfolding fr_rename_ext_def fr_rename_ext_aimpl_def
      apply (refine_rcg 
        order_trans[OF ECNV[unfolded fi_map_alt]] 
        refine_vcg)
      using subset_inj_on[OF _ V0_ss]
      apply (auto intro: INJ simp: rename_E_aimpl_alt fi_map_alt)
      done
  qed
end

term frv_rename_ext_aimpl
schematic_goal fr_rename_ext_impl_aux:
  fixes Re and Rv' :: "('vti × 'vt) set"
  assumes [autoref_rules]: "(eq, (=))  Rv'  Rv'  bool_rel"
  assumes [autoref_ga_rules]: "is_bounded_hashcode Rv' eq bhc"
  assumes [autoref_ga_rules]: "is_valid_def_hm_size TYPE('vti) def_size"
  shows "(?c,fr_rename_ext_aimpl)  
    ((Rv',Rvahm_rel bhc)  Re,Rvfrgv_impl_rel_ext  Re'nres_rel)    
    (RvRv') 
    Re,Rvfrgv_impl_rel_ext  
    Re',Rv'frgv_impl_rel_extnres_rel"
  unfolding fr_rename_ext_aimpl_def[abs_def]
  apply (autoref (keep_goal))
  done

concrete_definition fr_rename_ext_impl uses fr_rename_ext_impl_aux

thm fr_rename_ext_impl.refine[OF GEN_OP_D SIDE_GEN_ALGO_D SIDE_GEN_ALGO_D]

subsection ‹Graphs from Lists›

definition succ_of_list :: "(nat×nat) list  nat  nat set"
  where
  "succ_of_list l  let
    m = fold (λ(u,v) g. 
          case g u of 
            None  g(u{v})
          | Some s  g(uinsert v s)
        ) l Map.empty
  in
    (λu. case m u of None  {} | Some s  s)"
    
lemma succ_of_list_correct_aux: 
  "(succ_of_list l, set l)  br (λsuccs. {(u,v). vsuccs u}) (λ_. True)"
proof -

  term the_default

  { fix m
    have "fold (λ(u,v) g. 
            case g u of 
              None  g(u{v})
            | Some s  g(uinsert v s)
          ) l m 
      = (λu. let s=set l `` {u} in 
          if s={} then m u else Some (the_default {} (m u)  s))"
      apply (induction l arbitrary: m)
      apply (auto 
        split: option.split if_split 
        simp: Let_def Image_def
        intro!: ext)
      done
  } note aux=this
  
  show ?thesis
    unfolding succ_of_list_def aux
    by (auto simp: br_def Let_def split: option.splits if_split_asm)
qed


schematic_goal succ_of_list_impl:
  notes [autoref_tyrel] = 
    ty_REL[where 'a="natnat set" and R="nat_rel,Riam_map_rel" for R]
    ty_REL[where 'a="nat set" and R="nat_rellist_set_rel"]

  shows "(?f::?'c,succ_of_list)  ?R"
  unfolding succ_of_list_def[abs_def]
  apply (autoref (keep_goal))
  done

concrete_definition succ_of_list_impl uses succ_of_list_impl
export_code succ_of_list_impl in SML

lemma succ_of_list_impl_correct: "(succ_of_list_impl,set)  Id  Idslg_rel"
  apply rule
  unfolding slg_rel_def
  apply rule
  apply (rule succ_of_list_impl.refine[THEN fun_relD])
  apply simp
  apply (rule succ_of_list_correct_aux)
  done

end


Theory Automata_Impl

section ‹Implementing Automata›
(* Author: Peter Lammich *)
theory Automata_Impl
imports Digraph_Impl Automata
begin

subsection ‹Indexed Generalized Buchi Graphs›


consts
  i_igbg_eext :: "interface  interface  interface"

abbreviation "i_igbg Ie Iv  Ie,Ivii_igbg_eext,Ivii_g_ext"

context begin interpretation autoref_syn .

lemma igbg_type[autoref_itype]:
  "igbg_num_acc ::i i_igbg Ie Iv i i_nat"
  "igbg_acc ::i i_igbg Ie Iv i Iv i i_natii_set"
  "igb_graph_rec_ext
    ::i i_nat i (Iv i i_natii_set) i Ie i Ie,Ivii_igbg_eext"
  by simp_all
end


record ('vi,'ei,'v0i,'acci) gen_igbg_impl = "('vi,'ei,'v0i) gen_g_impl" +
  igbgi_num_acc :: nat
  igbgi_acc :: 'acci

definition gen_igbg_impl_rel_eext_def_internal: 
  "gen_igbg_impl_rel_eext Rm Racc  { (
   igbgi_num_acc = num_acci, igbgi_acc = acci, =mi , 
   igbg_num_acc = num_acc, igbg_acc = acc, =m ) 
  | num_acci acci mi num_acc acc m. 
    (num_acci,num_acc)nat_rel 
   (acci,acc)Racc
   (mi,m)Rm
  }"

lemma gen_igbg_impl_rel_eext_def: 
  "Rm,Raccgen_igbg_impl_rel_eext = { (
   igbgi_num_acc = num_acci, igbgi_acc = acci, =mi , 
   igbg_num_acc = num_acc, igbg_acc = acc, =m ) 
  | num_acci acci mi num_acc acc m. 
    (num_acci,num_acc)nat_rel 
   (acci,acc)Racc
   (mi,m)Rm
  }"
  unfolding gen_igbg_impl_rel_eext_def_internal relAPP_def by simp

lemma gen_igbg_impl_rel_sv[relator_props]: 
  "single_valued Racc; single_valued Rm 
   single_valued (Rm,Raccgen_igbg_impl_rel_eext)"
  unfolding gen_igbg_impl_rel_eext_def
  apply (rule single_valuedI)
  apply (clarsimp)
  apply (intro conjI)
  apply (rule single_valuedD[rotated], assumption+)
  apply (rule single_valuedD[rotated], assumption+)
  done

abbreviation gen_igbg_impl_rel_ext 
  :: "_  _  _  _  _  (_×(_,_)igb_graph_rec_scheme) set"
  where "gen_igbg_impl_rel_ext Rm Racc 
   Rm,Raccgen_igbg_impl_rel_eextgen_g_impl_rel_ext "

lemma gen_igbg_refine:
  fixes Rv Re Rv0 Racc
  assumes "TERM (Rv,Re,Rv0)"
  assumes "TERM (Racc)"
  shows
  "(igbgi_num_acc,igbg_num_acc) 
     Rv,Re,Rv0gen_igbg_impl_rel_ext Rm Racc  nat_rel"
  "(igbgi_acc,igbg_acc) 
     Rv,Re,Rv0gen_igbg_impl_rel_ext Rm Racc  Racc"
  "(gen_igbg_impl_ext, igb_graph_rec_ext) 
     nat_rel  Racc  Rm  Rm,Raccgen_igbg_impl_rel_eext"
  unfolding gen_igbg_impl_rel_eext_def gen_g_impl_rel_ext_def
  by auto

subsubsection ‹Implementation with bit-set›

definition igbg_impl_rel_eext_internal_def: 
  "igbg_impl_rel_eext Rm Rv  Rm, Rv  nat_relbs_set_relgen_igbg_impl_rel_eext"

lemma igbg_impl_rel_eext_def: 
  "Rm,Rvigbg_impl_rel_eext  Rm, Rv  nat_relbs_set_relgen_igbg_impl_rel_eext"
  unfolding igbg_impl_rel_eext_internal_def relAPP_def by simp

lemmas [autoref_rel_intf] = REL_INTFI[of igbg_impl_rel_eext i_igbg_eext]

lemma [relator_props, simp]: 
  "Range Rv = UNIV; single_valued Rm 
   single_valued (Rm,Rvigbg_impl_rel_eext)"
  unfolding igbg_impl_rel_eext_def by tagged_solver

lemma g_tag: "TERM (Rvfun_set_rel,Rvslg_rel,Rvlist_set_rel)" .
lemma frgv_tag: "TERM (Rvlist_set_rel,Rvslg_rel,Rvlist_set_rel)" .
lemma igbg_bs_tag: "TERM (Rv  nat_relbs_set_rel)" .

abbreviation "igbgv_impl_rel_ext Rm Rv 
   Rm, Rvigbg_impl_rel_eext, Rvfrgv_impl_rel_ext"

abbreviation "igbg_impl_rel_ext Rm Rv 
   Rm, Rvigbg_impl_rel_eext, Rvg_impl_rel_ext"

type_synonym ('v,'m) igbgv_impl_scheme = 
  "('v,  igbgi_num_acc::nat, igbgi_acc::'vinteger, ::'m  ) 
    frgv_impl_scheme"
type_synonym ('v,'m) igbg_impl_scheme = 
  "('v,  igbgi_num_acc::nat, igbgi_acc::'vinteger, ::'m  ) 
    g_impl_scheme"

context fixes Rv :: "('vi×'v) set" begin
lemmas [autoref_rules] = gen_igbg_refine[
  OF frgv_tag[of Rv] igbg_bs_tag[of Rv], 
  folded frgv_impl_rel_ext_def igbg_impl_rel_eext_def]

lemmas [autoref_rules] = gen_igbg_refine[
  OF g_tag[of Rv] igbg_bs_tag[of Rv], 
  folded g_impl_rel_ext_def igbg_impl_rel_eext_def]
end



schematic_goal "(?c::?'c, 
    λG x. if igbg_num_acc G = 0  1igbg_acc G x then (g_E G `` {x}) else {} 
  )?R"
  apply (autoref (keep_goal))
  done


schematic_goal "(?c, 
  λV0 E num_acc acc. 
     g_V = UNIV, g_E = E, g_V0 = V0, igbg_num_acc = num_acc, igbg_acc = acc 
  )Rlist_set_rel  Rslg_rel  nat_rel  (R  nat_relbs_set_rel) 
     igbg_impl_rel_ext unit_rel R"
  apply (autoref (keep_goal))
  done

schematic_goal "(?c, 
  λV0 E num_acc acc. 
     g_V = {}, g_E = E, g_V0 = V0, igbg_num_acc = num_acc, igbg_acc = acc 
  )Rlist_set_rel  Rslg_rel  nat_rel  (R  nat_relbs_set_rel) 
     igbgv_impl_rel_ext unit_rel R"
  apply (autoref (keep_goal))
  done

subsection ‹Indexed Generalized Buchi Automata›

consts
  i_igba_eext :: "interface  interface  interface  interface"

abbreviation "i_igba Ie Iv Il 
   Ie,Iv,Ilii_igba_eext,Ivii_igbg_eext,Ivii_g_ext"
context begin interpretation autoref_syn .

lemma igba_type[autoref_itype]:
  "igba_L ::i i_igba Ie Iv Il i (Iv i Il i i_bool)"
  "igba_rec_ext ::i (Iv i Il i i_bool) i Ie i Ie,Iv,Ilii_igba_eext"
  by simp_all
end


record ('vi,'ei,'v0i,'acci,'Li) gen_igba_impl = 
  "('vi,'ei,'v0i,'acci)gen_igbg_impl" +
  igbai_L :: "'Li"

definition gen_igba_impl_rel_eext_def_internal: 
  "gen_igba_impl_rel_eext Rm Rl   { (
   igbai_L = Li, =mi , 
   igba_L = L, =m ) 
  | Li mi L m. 
    (Li,L)Rl
   (mi,m)Rm
  }"

lemma gen_igba_impl_rel_eext_def: 
  "Rm,Rlgen_igba_impl_rel_eext = { (
   igbai_L = Li, =mi , 
   igba_L = L, =m ) 
  | Li mi L m. 
    (Li,L)Rl
   (mi,m)Rm
  }"
  unfolding gen_igba_impl_rel_eext_def_internal relAPP_def by simp

lemma gen_igba_impl_rel_sv[relator_props]: 
  "single_valued Rl; single_valued Rm 
   single_valued (Rm,Rlgen_igba_impl_rel_eext)"
  unfolding gen_igba_impl_rel_eext_def
  apply (rule single_valuedI)
  apply (clarsimp)
  apply (intro conjI)
  apply (rule single_valuedD[rotated], assumption+)
  apply (rule single_valuedD[rotated], assumption+)
  done

abbreviation gen_igba_impl_rel_ext 
  :: "_  _  _  _  _  _  (_ × ('a,'b,'c) igba_rec_scheme) set"
  where "gen_igba_impl_rel_ext Rm Rl 
     gen_igbg_impl_rel_ext (Rm,Rlgen_igba_impl_rel_eext)"

lemma gen_igba_refine:
  fixes Rv Re Rv0 Racc Rl
  assumes "TERM (Rv,Re,Rv0)"
  assumes "TERM (Racc)"
  assumes "TERM (Rl)"
  shows
  "(igbai_L,igba_L) 
     Rv,Re,Rv0gen_igba_impl_rel_ext Rm Rl Racc  Rl"
  "(gen_igba_impl_ext, igba_rec_ext) 
     Rl  Rm  Rm,Rlgen_igba_impl_rel_eext"
  unfolding gen_igba_impl_rel_eext_def gen_igbg_impl_rel_eext_def
    gen_g_impl_rel_ext_def
  by auto

subsubsection ‹Implementation as function›
definition igba_impl_rel_eext_internal_def: 
  "igba_impl_rel_eext Rm Rv Rl  Rm, Rv  Rl  bool_relgen_igba_impl_rel_eext"

lemma igba_impl_rel_eext_def: 
  "Rm,Rv,Rligba_impl_rel_eext  Rm, Rv  Rl  bool_relgen_igba_impl_rel_eext"
  unfolding igba_impl_rel_eext_internal_def relAPP_def by simp

lemmas [autoref_rel_intf] = REL_INTFI[of igba_impl_rel_eext i_igba_eext]

lemma [relator_props, simp]: 
  "Range Rv = UNIV; single_valued Rm; Range Rl = UNIV 
   single_valued (Rm,Rv,Rligba_impl_rel_eext)"
  unfolding igba_impl_rel_eext_def by tagged_solver

lemma igba_f_tag: "TERM (Rv  Rl  bool_rel)" .

abbreviation "igbav_impl_rel_ext Rm Rv Rl
   igbgv_impl_rel_ext (Rm, Rv, Rligba_impl_rel_eext) Rv"

abbreviation "igba_impl_rel_ext Rm Rv Rl 
   igbg_impl_rel_ext (Rm, Rv, Rligba_impl_rel_eext) Rv"

type_synonym ('v,'l,'m) igbav_impl_scheme = 
  "('v,  igbai_L :: 'v  'l  bool , ::'m  ) 
    igbgv_impl_scheme"

type_synonym ('v,'l,'m) igba_impl_scheme = 
  "('v,  igbai_L :: 'v  'l  bool , ::'m  ) 
    igbg_impl_scheme"

context 
  fixes Rv :: "('vi×'v) set" 
  fixes Rl :: "('Li×'l) set"
begin
lemmas [autoref_rules] = gen_igba_refine[
  OF frgv_tag[of Rv] igbg_bs_tag[of Rv] igba_f_tag[of Rv Rl], 
  folded frgv_impl_rel_ext_def igbg_impl_rel_eext_def igba_impl_rel_eext_def]

lemmas [autoref_rules] = gen_igba_refine[
  OF g_tag[of Rv] igbg_bs_tag[of Rv] igba_f_tag[of Rv Rl], 
  folded g_impl_rel_ext_def igbg_impl_rel_eext_def igba_impl_rel_eext_def]
end

thm autoref_itype

schematic_goal 
  "(?c::?'c, λG x l. if igba_L G x l then (g_E G `` {x}) else {} )?R"
  apply (autoref (keep_goal))
  done

schematic_goal 
  notes [autoref_tyrel] = TYRELI[of "Id :: ('a×'a) set"]
  shows "(?c::?'c, λE (V0::'a set) num_acc acc L. 
   g_V = UNIV, g_E = E, g_V0 = V0, 
    igbg_num_acc = num_acc, igbg_acc = acc, igba_L = L 
  )?R"
  apply (autoref (keep_goal))
  done

schematic_goal 
  notes [autoref_tyrel] = TYRELI[of "Id :: ('a×'a) set"]
  shows "(?c::?'c, λE (V0::'a set) num_acc acc L. 
   g_V = V0, g_E = E, g_V0 = V0, 
    igbg_num_acc = num_acc, igbg_acc = acc, igba_L = L 
  )?R"
  apply (autoref (keep_goal))
  done

subsection ‹Generalized Buchi Graphs›

consts
  i_gbg_eext :: "interface  interface  interface"

abbreviation "i_gbg Ie Iv  Ie,Ivii_gbg_eext,Ivii_g_ext"

context begin interpretation autoref_syn .

lemma gbg_type[autoref_itype]:
  "gbg_F ::i i_gbg Ie Iv i Ivii_setii_set"
  "gb_graph_rec_ext ::i Ivii_setii_set i Ie i Ie,Ivii_gbg_eext"
  by simp_all
end

record ('vi,'ei,'v0i,'fi) gen_gbg_impl = "('vi,'ei,'v0i) gen_g_impl" +
  gbgi_F :: 'fi

definition gen_gbg_impl_rel_eext_def_internal: 
  "gen_gbg_impl_rel_eext Rm Rf  { (
   gbgi_F = Fi, =mi , 
   gbg_F = F, =m ) 
  | Fi mi F m. 
    (Fi,F)Rf
   (mi,m)Rm
  }"

lemma gen_gbg_impl_rel_eext_def: 
  "Rm,Rfgen_gbg_impl_rel_eext = { (
   gbgi_F = Fi, =mi , 
   gbg_F = F, =m ) 
  | Fi mi F m. 
    (Fi,F)Rf
   (mi,m)Rm
  }"
  unfolding gen_gbg_impl_rel_eext_def_internal relAPP_def by simp

lemma gen_gbg_impl_rel_sv[relator_props]: 
  "single_valued Rm; single_valued Rf 
   single_valued (Rm,Rfgen_gbg_impl_rel_eext)"
  unfolding gen_gbg_impl_rel_eext_def
  apply (rule single_valuedI)
  apply (clarsimp)
  apply (intro conjI)
  apply (rule single_valuedD[rotated], assumption+)
  apply (rule single_valuedD[rotated], assumption+)
  done

abbreviation gen_gbg_impl_rel_ext 
  :: "_  _  _  _  _  (_ × ('q,_) gb_graph_rec_scheme) set"
  where "gen_gbg_impl_rel_ext Rm Rf 
   Rm,Rfgen_gbg_impl_rel_eextgen_g_impl_rel_ext"

lemma gen_gbg_refine:
  fixes Rv Re Rv0 Rf
  assumes "TERM (Rv,Re,Rv0)"
  assumes "TERM (Rf)"
  shows
  "(gbgi_F,gbg_F) 
     Rv,Re,Rv0gen_gbg_impl_rel_ext Rm Rf  Rf"
  "(gen_gbg_impl_ext, gb_graph_rec_ext) 
     Rf  Rm  Rm,Rfgen_gbg_impl_rel_eext"
  unfolding gen_gbg_impl_rel_eext_def gen_g_impl_rel_ext_def
  by auto

subsubsection ‹Implementation with list of lists›

definition gbg_impl_rel_eext_internal_def: 
  "gbg_impl_rel_eext Rm Rv 
   Rm, Rvlist_set_rellist_set_relgen_gbg_impl_rel_eext"

lemma gbg_impl_rel_eext_def: 
  "Rm,Rvgbg_impl_rel_eext 
     Rm, Rvlist_set_rellist_set_relgen_gbg_impl_rel_eext"
  unfolding gbg_impl_rel_eext_internal_def relAPP_def by simp

lemmas [autoref_rel_intf] = REL_INTFI[of gbg_impl_rel_eext i_gbg_eext]

lemma [relator_props, simp]: 
  "single_valued Rm; single_valued Rv 
   single_valued (Rm,Rvgbg_impl_rel_eext)"
  unfolding gbg_impl_rel_eext_def by tagged_solver

lemma gbg_ls_tag: "TERM (Rvlist_set_rellist_set_rel)" .

abbreviation "gbgv_impl_rel_ext Rm Rv 
   Rm, Rvgbg_impl_rel_eext, Rvfrgv_impl_rel_ext"

abbreviation "gbg_impl_rel_ext Rm Rv 
   Rm, Rvgbg_impl_rel_eext, Rvg_impl_rel_ext"

context fixes Rv :: "('vi×'v) set" begin
lemmas [autoref_rules] = gen_gbg_refine[
  OF frgv_tag[of Rv] gbg_ls_tag[of Rv], 
  folded frgv_impl_rel_ext_def gbg_impl_rel_eext_def]

lemmas [autoref_rules] = gen_gbg_refine[
  OF g_tag[of Rv] gbg_ls_tag[of Rv], 
  folded g_impl_rel_ext_def gbg_impl_rel_eext_def]
end

schematic_goal "(?c::?'c, 
    λG x. if gbg_F G = {} then (g_E G `` {x}) else {} 
  )?R"
  apply (autoref (keep_goal))
  done

schematic_goal 
  notes [autoref_tyrel] = TYRELI[of "Id :: ('a×'a) set"]
  shows "(?c::?'c, λE (V0::'a set) F. 
     g_V = {}, g_E = E, g_V0 = V0, gbg_F = F )?R"
  apply (autoref (keep_goal))
  done

schematic_goal 
  notes [autoref_tyrel] = TYRELI[of "Id :: ('a×'a) set"]
  shows "(?c::?'c, λE (V0::'a set) F. 
     g_V = UNIV, g_E = E, g_V0 = V0, gbg_F = insert {} F )?R"
  apply (autoref (keep_goal))
  done

schematic_goal "(?c::?'c, it_to_sorted_list (λ_ _. True) {1,2::nat} )?R"
  apply (autoref (keep_goal))
  done

subsection ‹GBAs›

consts
  i_gba_eext :: "interface  interface  interface  interface"

abbreviation "i_gba Ie Iv Il 
   Ie,Iv,Ilii_gba_eext,Ivii_gbg_eext,Ivii_g_ext"
context begin interpretation autoref_syn .

lemma gba_type[autoref_itype]:
  "gba_L ::i i_gba Ie Iv Il i (Iv i Il i i_bool)"
  "gba_rec_ext ::i (Iv i Il i i_bool) i Ie i Ie,Iv,Ilii_gba_eext"
  by simp_all
end

record ('vi,'ei,'v0i,'acci,'Li) gen_gba_impl = 
  "('vi,'ei,'v0i,'acci)gen_gbg_impl" +
  gbai_L :: "'Li"

definition gen_gba_impl_rel_eext_def_internal: 
  "gen_gba_impl_rel_eext Rm Rl   { (
   gbai_L = Li, =mi , 
   gba_L = L, =m ) 
  | Li mi L m. 
    (Li,L)Rl
   (mi,m)Rm
  }"

lemma gen_gba_impl_rel_eext_def: 
  "Rm,Rlgen_gba_impl_rel_eext = { (
   gbai_L = Li, =mi , 
   gba_L = L, =m ) 
  | Li mi L m. 
    (Li,L)Rl
   (mi,m)Rm
  }"
  unfolding gen_gba_impl_rel_eext_def_internal relAPP_def by simp

lemma gen_gba_impl_rel_sv[relator_props]: 
  "single_valued Rl; single_valued Rm 
   single_valued (Rm,Rlgen_gba_impl_rel_eext)"
  unfolding gen_gba_impl_rel_eext_def
  apply (rule single_valuedI)
  apply (clarsimp)
  apply (intro conjI)
  apply (rule single_valuedD[rotated], assumption+)
  apply (rule single_valuedD[rotated], assumption+)
  done

abbreviation gen_gba_impl_rel_ext 
  :: "_  _  _  _  _  _  (_ × ('a,'b,'c) gba_rec_scheme) set"
  where "gen_gba_impl_rel_ext Rm Rl 
     gen_gbg_impl_rel_ext (Rm,Rlgen_gba_impl_rel_eext)"

lemma gen_gba_refine:
  fixes Rv Re Rv0 Racc Rl
  assumes "TERM (Rv,Re,Rv0)"
  assumes "TERM (Racc)"
  assumes "TERM (Rl)"
  shows
  "(gbai_L,gba_L) 
     Rv,Re,Rv0gen_gba_impl_rel_ext Rm Rl Racc  Rl"
  "(gen_gba_impl_ext, gba_rec_ext) 
     Rl  Rm  Rm,Rlgen_gba_impl_rel_eext"
  unfolding gen_gba_impl_rel_eext_def gen_gbg_impl_rel_eext_def
    gen_g_impl_rel_ext_def
  by auto

subsubsection ‹Implementation as function›
definition gba_impl_rel_eext_internal_def: 
  "gba_impl_rel_eext Rm Rv Rl  Rm, Rv  Rl  bool_relgen_gba_impl_rel_eext"

lemma gba_impl_rel_eext_def: 
  "Rm,Rv,Rlgba_impl_rel_eext  Rm, Rv  Rl  bool_relgen_gba_impl_rel_eext"
  unfolding gba_impl_rel_eext_internal_def relAPP_def by simp

lemmas [autoref_rel_intf] = REL_INTFI[of gba_impl_rel_eext i_gba_eext]

lemma [relator_props, simp]: 
  "Range Rv = UNIV; single_valued Rm; Range Rl = UNIV 
   single_valued (Rm,Rv,Rlgba_impl_rel_eext)"
  unfolding gba_impl_rel_eext_def by tagged_solver

lemma gba_f_tag: "TERM (Rv  Rl  bool_rel)" .

abbreviation "gbav_impl_rel_ext Rm Rv Rl
   gbgv_impl_rel_ext (Rm, Rv, Rlgba_impl_rel_eext) Rv"

abbreviation "gba_impl_rel_ext Rm Rv Rl 
   gbg_impl_rel_ext (Rm, Rv, Rlgba_impl_rel_eext) Rv"

context 
  fixes Rv :: "('vi×'v) set" 
  fixes Rl :: "('Li×'l) set"
begin
lemmas [autoref_rules] = gen_gba_refine[
  OF frgv_tag[of Rv] gbg_ls_tag[of Rv] gba_f_tag[of Rv Rl], 
  folded frgv_impl_rel_ext_def gbg_impl_rel_eext_def gba_impl_rel_eext_def]

lemmas [autoref_rules] = gen_gba_refine[
  OF g_tag[of Rv] gbg_ls_tag[of Rv] gba_f_tag[of Rv Rl], 
  folded g_impl_rel_ext_def gbg_impl_rel_eext_def gba_impl_rel_eext_def]
end

thm autoref_itype

schematic_goal 
  "(?c::?'c, λG x l. if gba_L G x l then (g_E G `` {x}) else {} )?R"
  apply (autoref (keep_goal))
  done

schematic_goal 
  notes [autoref_tyrel] =