Theory NBA_Algorithms

section ‹Algorithms on Nondeterministic Büchi Automata›

theory NBA_Algorithms
imports
  NBA_Graphs
  NBA_Implement
  DFS_Framework.Reachable_Nodes
  Gabow_SCC.Gabow_GBG_Code
begin

  subsection ‹Miscellaneous Amendments›

  lemma (in igb_fr_graph) acc_run_lasso_prpl: "Ex is_acc_run  Ex is_lasso_prpl"
    using accepted_lasso is_lasso_prpl_of_lasso by blast
  lemma (in igb_fr_graph)  lasso_prpl_acc_run_iff: "Ex is_lasso_prpl  Ex is_acc_run"
    using acc_run_lasso_prpl lasso_prpl_acc_run by auto

  lemma [autoref_rel_intf]: "REL_INTF igbg_impl_rel_ext i_igbg" by (rule REL_INTFI)

  subsection ‹Operations›

  definition op_language_empty where [simp]: "op_language_empty A  language A = {}"

  lemmas [autoref_op_pat] = op_language_empty_def[symmetric]

  subsection ‹Implementations›

  context
  begin

    interpretation autoref_syn by this

    lemma nba_g_ahs: "nba_g A =  g_V = UNIV, g_E = E_of_succ (λ p. CAST
      (( a  alphabet A. transition A a p ::: S list_set_rel) ::: S ahs_rel bhc)),
      g_V0 = initial A "
      unfolding nba_g_def nba.successors_alt_def CAST_def id_apply autoref_tag_defs by rule

    schematic_goal nbai_gi:
      notes [autoref_ga_rules] = map2set_to_list
      fixes S :: "('statei × 'state) set"
      assumes [autoref_ga_rules]: "is_bounded_hashcode S seq bhc"
      assumes [autoref_ga_rules]: "is_valid_def_hm_size TYPE('statei) hms"
      assumes [autoref_rules]: "(seq, HOL.eq)  S  S  bool_rel"
      assumes [autoref_rules]: "(Ai, A)  L, S nbai_nba_rel"
      shows "(?f :: ?'a, RETURN (nba_g A))  ?A"
      unfolding nba_g_ahs[where S = S and bhc = bhc] by (autoref_monadic (plain))
    concrete_definition nbai_gi uses nbai_gi
    lemma nbai_gi_refine[autoref_rules]:
      fixes S :: "('statei × 'state) set"
      assumes "SIDE_GEN_ALGO (is_bounded_hashcode S seq bhc)"
      assumes "SIDE_GEN_ALGO (is_valid_def_hm_size TYPE('statei) hms)"
      assumes "GEN_OP seq HOL.eq (S  S  bool_rel)"
      shows "(NBA_Algorithms.nbai_gi seq bhc hms, nba_g) 
        L, S nbai_nba_rel  unit_rel, S g_impl_rel_ext"
      using nbai_gi.refine[THEN RETURN_nres_relD] assms unfolding autoref_tag_defs by blast

    schematic_goal nba_nodes:
      fixes S :: "('statei × 'state) set"
      assumes [simp]: "finite ((g_E (nba_g A))* `` g_V0 (nba_g A))"
      assumes [autoref_ga_rules]: "is_bounded_hashcode S seq bhc"
      assumes [autoref_ga_rules]: "is_valid_def_hm_size TYPE('statei) hms"
      assumes [autoref_rules]: "(seq, HOL.eq)  S  S  bool_rel"
      assumes [autoref_rules]: "(Ai, A)  L, S nbai_nba_rel"
      shows "(?f :: ?'a, op_reachable (nba_g A))  ?R" by autoref
    concrete_definition nba_nodes uses nba_nodes
    lemma nba_nodes_refine[autoref_rules]:
      fixes S :: "('statei × 'state) set"
      assumes "SIDE_PRECOND (finite (nodes A))"
      assumes "SIDE_GEN_ALGO (is_bounded_hashcode S seq bhc)"
      assumes "SIDE_GEN_ALGO (is_valid_def_hm_size TYPE('statei) hms)"
      assumes "GEN_OP seq HOL.eq (S  S  bool_rel)"
      assumes "(Ai, A)  L, S nbai_nba_rel"
      shows "(NBA_Algorithms.nba_nodes seq bhc hms Ai,
        (OP nodes ::: L, S nbai_nba_rel  S ahs_rel bhc) $ A)  S ahs_rel bhc"
    proof -
      have 1: "nodes A = op_reachable (nba_g A)" by (auto simp: nba_g_V0 nba_g_E_rtrancl)
      have 2: "finite ((g_E (nba_g A))* `` g_V0 (nba_g A))" using assms(1) unfolding 1 by simp
      show ?thesis using nba_nodes.refine assms 2 unfolding autoref_tag_defs 1 by blast
    qed

    lemma nba_igbg_ahs: "nba_igbg A =  g_V = UNIV, g_E = E_of_succ (λ p. CAST
      (( a  alphabet A. transition A a p ::: S list_set_rel) ::: S ahs_rel bhc)), g_V0 = initial A,
      igbg_num_acc = 1, igbg_acc = λ p. if accepting A p then {0} else {} "
      unfolding nba_g_def nba_igbg_def nba.successors_alt_def CAST_def id_apply autoref_tag_defs
      unfolding graph_rec.defs
      by simp

    schematic_goal nbai_igbgi:
      notes [autoref_ga_rules] = map2set_to_list
      fixes S :: "('statei × 'state) set"
      assumes [autoref_ga_rules]: "is_bounded_hashcode S seq bhc"
      assumes [autoref_ga_rules]: "is_valid_def_hm_size TYPE('statei) hms"
      assumes [autoref_rules]: "(seq, HOL.eq)  S  S  bool_rel"
      assumes [autoref_rules]: "(Ai, A)  L, S nbai_nba_rel"
      shows "(?f :: ?'a, RETURN (nba_igbg A))  ?A"
      unfolding nba_igbg_ahs[where S = S and bhc = bhc] by (autoref_monadic (plain))
    concrete_definition nbai_igbgi uses nbai_igbgi
    lemma nbai_igbgi_refine[autoref_rules]:
      fixes S :: "('statei × 'state) set"
      assumes "SIDE_GEN_ALGO (is_bounded_hashcode S seq bhc)"
      assumes "SIDE_GEN_ALGO (is_valid_def_hm_size TYPE('statei) hms)"
      assumes "GEN_OP seq HOL.eq (S  S  bool_rel)"
      shows "(NBA_Algorithms.nbai_igbgi seq bhc hms, nba_igbg) 
        L, S nbai_nba_rel  igbg_impl_rel_ext unit_rel S"
      using nbai_igbgi.refine[THEN RETURN_nres_relD] assms unfolding autoref_tag_defs by blast

    schematic_goal nba_language_empty:
      fixes S :: "('statei × 'state) set"
      assumes [simp]: "igb_fr_graph (nba_igbg A)"
      assumes [autoref_ga_rules]: "is_bounded_hashcode S seq bhs"
      assumes [autoref_ga_rules]: "is_valid_def_hm_size TYPE('statei) hms"
      assumes [autoref_rules]: "(seq, HOL.eq)  S  S  bool_rel"
      assumes [autoref_rules]: "(Ai, A)  L, S nbai_nba_rel"
      shows "(?f :: ?'a, do { r  op_find_lasso_spec (nba_igbg A); RETURN (r = None)})  ?A"
      by (autoref_monadic (plain))
    concrete_definition nba_language_empty uses nba_language_empty
    lemma nba_language_empty_refine[autoref_rules]:
      fixes S :: "('statei × 'state) set"
      assumes "SIDE_PRECOND (finite (nodes A))"
      assumes "SIDE_GEN_ALGO (is_bounded_hashcode S seq bhc)"
      assumes "SIDE_GEN_ALGO (is_valid_def_hm_size TYPE('statei) hms)"
      assumes "GEN_OP seq HOL.eq (S  S  bool_rel)"
      assumes "(Ai, A)  L, S nbai_nba_rel"
      shows "(NBA_Algorithms.nba_language_empty seq bhc hms Ai,
        (OP op_language_empty ::: L, S nbai_nba_rel  bool_rel) $ A)  bool_rel"
    proof -
      have 1: "nodes A = op_reachable (nba_g A)" by (auto simp: nba_g_V0 nba_g_E_rtrancl)
      have 2: "finite ((g_E (nba_g A))* `` g_V0 (nba_g A))" using assms(1) unfolding 1 by simp
      interpret igb_fr_graph "nba_igbg A"
        using 2 unfolding nba_igbg_def nba_g_def graph_rec.defs by unfold_locales auto
      have "(RETURN (NBA_Algorithms.nba_language_empty seq bhc hms Ai),
        do { r  find_lasso_spec; RETURN (r = None) })  bool_rel nres_rel"
        using nba_language_empty.refine assms igb_fr_graph_axioms by simp
      also have "(do { r  find_lasso_spec; RETURN (r = None) },
        RETURN (¬ Ex is_lasso_prpl))  bool_rel nres_rel"
        unfolding find_lasso_spec_def by (refine_vcg) (auto split: option.splits)
      finally have "NBA_Algorithms.nba_language_empty seq bhc hms Ai  ¬ Ex is_lasso_prpl"
        unfolding nres_rel_comp using RETURN_nres_relD by force
      also have "  ¬ Ex is_acc_run" using lasso_prpl_acc_run_iff by auto
      also have "  language A = {}" using acc_run_language is_igb_graph by auto
      finally show ?thesis by simp
    qed

  end

end