Theory Complementation_Final

section ‹Final Instantiation of Algorithms Related to Complementation›

theory Complementation_Final
imports
  "Complementation_Implement"
  "Formula"
  "Transition_Systems_and_Automata.NBA_Translate"
  "Transition_Systems_and_Automata.NGBA_Algorithms"
  "HOL-Library.Multiset"
begin

  subsection ‹Syntax›

  (* TODO: this syntax has unnecessarily high inner binding strength, requiring extra parentheses
    the regular let syntax correctly uses inner binding strength 0: ("(2_ =/ _)" 10) *)
  no_syntax "_do_let" :: "[pttrn, 'a] ⇒ do_bind" (‹(‹indent=2 notation=‹infix do let››let _ =/ _)› [1000, 13] 13)
  syntax "_do_let" :: "[pttrn, 'a] ⇒ do_bind" (‹(‹indent=2 notation=‹infix do let››let _ =/ _)› 13)

  subsection ‹Hashcodes on Complement States›

  definition "hci k ≡ uint32_of_nat k * 1103515245 + 12345"
  definition "hc ≡ λ (p, q, b). hci p + hci q * 31 + (if b then 1 else 0)"
  definition "list_hash xs ≡ fold (xor ∘ hc) xs 0"

  lemma list_hash_eq:
    assumes "distinct xs" "distinct ys" "set xs = set ys"
    shows "list_hash xs = list_hash ys"
  proof -
    have "mset (remdups xs) = mset (remdups ys)" using assms(3)
      using set_eq_iff_mset_remdups_eq by blast 
    then have "mset xs = mset ys" using assms(1, 2) by (simp add: distinct_remdups_id)
    have "fold (xor ∘ hc) xs = fold (xor ∘ hc) ys"
      apply (rule fold_multiset_equiv)
       apply (simp_all add: fun_eq_iff ac_simps)
      using ‹mset xs = mset ys› .
    then show ?thesis unfolding list_hash_def by simp
  qed

  definition state_hash :: "nat ⇒ Complementation_Implement.state ⇒ nat" where
    "state_hash n p ≡ nat_of_hashcode (list_hash p) mod n"

  lemma state_hash_bounded_hashcode[autoref_ga_rules]: "is_bounded_hashcode state_rel
    (gen_equals (Gen_Map.gen_ball (foldli ∘ list_map_to_list)) (list_map_lookup (=))
    (prod_eq (=) (⟷))) state_hash"
  proof
    show [param]: "(gen_equals (Gen_Map.gen_ball (foldli ∘ list_map_to_list)) (list_map_lookup (=))
      (prod_eq (=) (⟷)), (=)) ∈ state_rel → state_rel → bool_rel" by autoref
    show "state_hash n xs = state_hash n ys" if "xs ∈ Domain state_rel" "ys ∈ Domain state_rel"
      "gen_equals (Gen_Map.gen_ball (foldli ∘ list_map_to_list))
      (list_map_lookup (=)) (prod_eq (=) (=)) xs ys" for xs ys n
    proof -
      have 1: "distinct (map fst xs)" "distinct (map fst ys)"
        using that(1, 2) unfolding list_map_rel_def list_map_invar_def by (auto simp: in_br_conv)
      have 2: "distinct xs" "distinct ys" using 1 by (auto intro: distinct_mapI)
      have 3: "(xs, map_of xs) ∈ state_rel" "(ys, map_of ys) ∈ state_rel"
        using 1 unfolding list_map_rel_def list_map_invar_def by (auto simp: in_br_conv)
      have 4: "(gen_equals (Gen_Map.gen_ball (foldli ∘ list_map_to_list)) (list_map_lookup (=))
        (prod_eq (=) (⟷)) xs ys, map_of xs = map_of ys) ∈ bool_rel" using 3 by parametricity
      have 5: "map_to_set (map_of xs) = map_to_set (map_of ys)" using that(3) 4 by simp
      have 6: "set xs = set ys" using map_to_set_map_of 1 5 by blast
      show "state_hash n xs = state_hash n ys" unfolding state_hash_def using list_hash_eq 2 6 by metis
    qed
    show "state_hash n x < n" if "1 < n" for n x using that unfolding state_hash_def by simp
  qed

  subsection ‹Complementation›

  schematic_goal complement_impl:
    assumes [simp]: "finite (NBA.nodes A)"
    assumes [autoref_rules]: "(Ai, A) ∈ ⟨Id, nat_rel⟩ nbai_nba_rel"
    shows "(?f :: ?'c, op_translate (complement_4 A)) ∈ ?R"
    by (autoref_monadic (plain))
  concrete_definition complement_impl uses complement_impl

  theorem complement_impl_correct:
    assumes "finite (NBA.nodes A)"
    assumes "(Ai, A) ∈ ⟨Id, nat_rel⟩ nbai_nba_rel"
    shows "NBA.language (nbae_nba (nbaei_nbae (complement_impl Ai))) =
      streams (nba.alphabet A) - NBA.language A"
    using op_translate_language[OF complement_impl.refine[OF assms]]
    using complement_4_correct[OF assms(1)]
    by simp

  subsection ‹Language Subset›

  definition [simp]: "op_language_subset A B ≡ NBA.language A ⊆ NBA.language B"

  lemmas [autoref_op_pat] = op_language_subset_def[symmetric]

  schematic_goal language_subset_impl:
    assumes [simp]: "finite (NBA.nodes B)"
    assumes [autoref_rules]: "(Ai, A) ∈ ⟨Id, nat_rel⟩ nbai_nba_rel"
    assumes [autoref_rules]: "(Bi, B) ∈ ⟨Id, nat_rel⟩ nbai_nba_rel"
    shows "(?f :: ?'c, do {
      let AB' = intersect' A (complement_4 B);
      ASSERT (finite (NGBA.nodes AB'));
      RETURN (NGBA.language AB' = {})
    }) ∈ ?R"
		by (autoref_monadic (plain))
  concrete_definition language_subset_impl uses language_subset_impl
  lemma language_subset_impl_refine[autoref_rules]:
    assumes "SIDE_PRECOND (finite (NBA.nodes A))"
    assumes "SIDE_PRECOND (finite (NBA.nodes B))"
    assumes "SIDE_PRECOND (nba.alphabet A ⊆ nba.alphabet B)"
    assumes "(Ai, A) ∈ ⟨Id, nat_rel⟩ nbai_nba_rel"
    assumes "(Bi, B) ∈ ⟨Id, nat_rel⟩ nbai_nba_rel"
    shows "(language_subset_impl Ai Bi, (OP op_language_subset :::
      ⟨Id, nat_rel⟩ nbai_nba_rel → ⟨Id, nat_rel⟩ nbai_nba_rel → bool_rel) $ A $ B) ∈ bool_rel"
  proof -
    have "(RETURN (language_subset_impl Ai Bi), do {
      let AB' = intersect' A (complement_4 B);
      ASSERT (finite (NGBA.nodes AB'));
      RETURN (NGBA.language AB' = {})
    }) ∈ ⟨bool_rel⟩ nres_rel"
      using language_subset_impl.refine assms(2, 4, 5) unfolding autoref_tag_defs by this
    also have "(do {
      let AB' = intersect' A (complement_4 B);
      ASSERT (finite (NGBA.nodes AB'));
      RETURN (NGBA.language AB' = {})
    }, RETURN (NBA.language A ⊆ NBA.language B)) ∈ ⟨bool_rel⟩ nres_rel"
    proof refine_vcg
      show "finite (NGBA.nodes (intersect' A (complement_4 B)))" using assms(1, 2) by auto
      have 1: "NBA.language A ⊆ streams (nba.alphabet B)"
        using nba.language_alphabet streams_mono2 assms(3) unfolding autoref_tag_defs by blast
      have 2: "NBA.language (complement_4 B) = streams (nba.alphabet B) - NBA.language B"
        using complement_4_correct assms(2) by auto
      show "(NGBA.language (intersect' A (complement_4 B)) = {},
        NBA.language A ⊆ NBA.language B) ∈ bool_rel" using 1 2 by auto
    qed
    finally show ?thesis using RETURN_nres_relD unfolding nres_rel_comp by force
  qed

  subsection ‹Language Equality›

  definition [simp]: "op_language_equal A B ≡ NBA.language A = NBA.language B"

  lemmas [autoref_op_pat] = op_language_equal_def[symmetric]

  schematic_goal language_equal_impl:
    assumes [simp]: "finite (NBA.nodes A)"
    assumes [simp]: "finite (NBA.nodes B)"
    assumes [simp]: "nba.alphabet A = nba.alphabet B"
    assumes [autoref_rules]: "(Ai, A) ∈ ⟨Id, nat_rel⟩ nbai_nba_rel"
    assumes [autoref_rules]: "(Bi, B) ∈ ⟨Id, nat_rel⟩ nbai_nba_rel"
    shows "(?f :: ?'c, NBA.language A ⊆ NBA.language B ∧ NBA.language B ⊆ NBA.language A) ∈ ?R"
    by autoref
  concrete_definition language_equal_impl uses language_equal_impl
  lemma language_equal_impl_refine[autoref_rules]:
    assumes "SIDE_PRECOND (finite (NBA.nodes A))"
    assumes "SIDE_PRECOND (finite (NBA.nodes B))"
    assumes "SIDE_PRECOND (nba.alphabet A = nba.alphabet B)"
    assumes "(Ai, A) ∈ ⟨Id, nat_rel⟩ nbai_nba_rel"
    assumes "(Bi, B) ∈ ⟨Id, nat_rel⟩ nbai_nba_rel"
    shows "(language_equal_impl Ai Bi, (OP op_language_equal :::
      ⟨Id, nat_rel⟩ nbai_nba_rel → ⟨Id, nat_rel⟩ nbai_nba_rel → bool_rel) $ A $ B) ∈ bool_rel"
    using language_equal_impl.refine[OF assms[unfolded autoref_tag_defs]] by auto

  schematic_goal product_impl:
    assumes [simp]: "finite (NBA.nodes B)"
    assumes [autoref_rules]: "(Ai, A) ∈ ⟨Id, nat_rel⟩ nbai_nba_rel"
    assumes [autoref_rules]: "(Bi, B) ∈ ⟨Id, nat_rel⟩ nbai_nba_rel"
    shows "(?f :: ?'c, do {
      let AB' = intersect A (complement_4 B);
      ASSERT (finite (NBA.nodes AB'));
      op_translate AB'
    }) ∈ ?R"
		by (autoref_monadic (plain))
  concrete_definition product_impl uses product_impl

  (* TODO: possible optimizations:
    - introduce op_map_map operation for maps instead of manually iterating via FOREACH
    - consolidate various binds and maps in expand_map_get_7 *)
  export_code
    Set.empty Set.insert Set.member
    "Inf :: 'a set set ⇒ 'a set" "Sup :: 'a set set ⇒ 'a set" image Pow set
    nat_of_integer integer_of_nat
    Variable Negation Conjunction Disjunction satisfies map_formula
    nbaei alphabetei initialei transitionei acceptingei
    nbae_nba_impl complement_impl language_equal_impl product_impl
    in SML module_name Complementation file_prefix Complementation

end