Theory Ta_impl

(*  Title:       Tree Automata
    Author:      Peter Lammich <peter dot lammich at uni-muenster.de>
    Maintainer:  Peter Lammich <peter dot lammich at uni-muenster.de>
*)
section "Executable Implementation of Tree Automata"
theory Ta_impl
imports 
  Main
  Collections.CollectionsV1 
  Ta AbsAlgo
  "HOL-Library.Code_Target_Numeral" 
begin




text_raw ‹\label{sec:taimpl}›

text ‹
  In this theory, an effcient executable implementation of non-deterministic 
  tree automata and basic algorithms is defined.

  The algorithms use red-black trees to represent sets of states or rules 
  where appropriate.
›

subsection "Prelude"

  ― ‹Make rules hashable›
instantiation ta_rule :: (hashable,hashable) hashable
begin
fun hashcode_of_ta_rule 
  :: "('Q1::hashable,'Q2::hashable) ta_rule ⇒ hashcode" 
  where
  "hashcode_of_ta_rule (q → f qs) = hashcode q + hashcode f + hashcode qs"

definition [simp]: "hashcode = hashcode_of_ta_rule"

definition "def_hashmap_size::(('a,'b) ta_rule itself ⇒ nat) == (λ_. 32)"

instance 
  by (intro_classes)(auto simp add: def_hashmap_size_ta_rule_def)
end


  ― ‹Make wrapped states hashable›
instantiation ustate_wrapper :: (hashable,hashable) hashable
begin
  definition "hashcode x == (case x of USW1 a ⇒ 2 * hashcode a | USW2 b ⇒ 2 * hashcode b + 1)"
  definition "def_hashmap_size = (λ_ :: (('a,'b) ustate_wrapper) itself. def_hashmap_size TYPE('a) + def_hashmap_size TYPE('b))"

  instance using def_hashmap_size[where ?'a="'a"] def_hashmap_size[where ?'a="'b"]
    by(intro_classes)(simp_all add: bounded_hashcode_bounds def_hashmap_size_ustate_wrapper_def split: ustate_wrapper.split)

end

subsubsection ‹Ad-Hoc instantiations of generic Algorithms›
setup Locale_Code.open_block
interpretation hll_idx: build_index_loc hm_ops ls_ops ls_ops by unfold_locales
interpretation ll_set_xy: g_set_xy_loc ls_ops ls_ops 
  by unfold_locales

interpretation lh_set_xx: g_set_xx_loc ls_ops hs_ops
  by unfold_locales
interpretation lll_iflt_cp: inj_image_filter_cp_loc ls_ops ls_ops ls_ops
  by unfold_locales
interpretation hhh_cart: cart_loc hs_ops hs_ops hs_ops by unfold_locales
interpretation hh_set_xy: g_set_xy_loc hs_ops hs_ops 
  by unfold_locales

interpretation llh_set_xyy: g_set_xyy_loc ls_ops ls_ops hs_ops
  by unfold_locales

interpretation hh_map_to_nat: map_to_nat_loc hs_ops hm_ops by unfold_locales
interpretation hh_set_xy: g_set_xy_loc hs_ops hs_ops by unfold_locales
interpretation lh_set_xy: g_set_xy_loc ls_ops hs_ops by unfold_locales
interpretation hh_set_xx: g_set_xx_loc hs_ops hs_ops by unfold_locales
interpretation hs_to_fifo: set_to_list_loc hs_ops fifo_ops by unfold_locales

setup Locale_Code.close_block

subsection "Generating Indices of Rules"
text ‹
  Rule indices are pieces of extra information that may be attached to a 
  tree automaton.
  There are three possible rule indices
    \begin{description}
      \item[f]   index of rules by function symbol
      \item[s]   index of rules by lhs
      \item[sf]  index of rules
    \end{description}
›

definition build_rule_index 
  :: "(('q,'l) ta_rule ⇒ 'i::hashable) ⇒ ('q,'l) ta_rule ls 
      ⇒ ('i,('q,'l) ta_rule ls) hm"
  where "build_rule_index == hll_idx.idx_build"

definition "build_rule_index_f δ == build_rule_index (λr. rhsl r) δ"
definition "build_rule_index_s δ == build_rule_index (λr. lhs r) δ"
definition "build_rule_index_sf δ == build_rule_index (λr. (lhs r, rhsl r)) δ"

lemma build_rule_index_f_correct[simp]: 
  assumes I[simp, intro!]: "ls_invar δ"
  shows "hll_idx.is_index rhsl (ls_α δ) (build_rule_index_f δ)"
  apply (unfold build_rule_index_f_def build_rule_index_def)
  apply (simp add: hll_idx.idx_build_is_index)
  done

lemma build_rule_index_s_correct[simp]: 
  assumes I[simp, intro!]: "ls_invar δ"
  shows
  "hll_idx.is_index lhs (ls_α δ) (build_rule_index_s δ)"
  by (unfold build_rule_index_s_def build_rule_index_def)
     (simp add: hll_idx.idx_build_is_index)

lemma build_rule_index_sf_correct[simp]: 
  assumes I[simp, intro!]: "ls_invar δ"
  shows
  "hll_idx.is_index (λr. (lhs r, rhsl r)) (ls_α δ) (build_rule_index_sf δ)"
  by (unfold build_rule_index_sf_def build_rule_index_def)
     (simp add: hll_idx.idx_build_is_index)

subsection "Tree Automaton with Optional Indices"

text ‹
  A tree automaton contains a hashset of initial states, a list-set of rules and
  several (optional) rule indices.
›

record (overloaded) ('q,'l) hashedTa =
    ― ‹Initial states›
  hta_Qi :: "'q hs"           
    ― ‹Rules›
  hta_δ :: "('q,'l) ta_rule ls"    
    ― ‹Rules by function symbol›
  hta_idx_f :: "('l,('q,'l) ta_rule ls) hm option" 
    ― ‹Rules by lhs state›
  hta_idx_s :: "('q,('q,'l) ta_rule ls) hm option" 
    ― ‹Rules by lhs state and function symbol›
  hta_idx_sf :: "('q×'l,('q,'l) ta_rule ls) hm option" 

  ― ‹Abstraction of a concrete tree automaton to an abstract one›
definition hta_α 
  where "hta_α H = ⦇ ta_initial = hs_α (hta_Qi H), ta_rules = ls_α (hta_δ H) ⦈"

  ― ‹Builds the f-index if not present›
definition "hta_ensure_idx_f H ==
  case hta_idx_f H of 
    None ⇒ H⦇ hta_idx_f := Some (build_rule_index_f (hta_δ H)) ⦈ |
    Some _ ⇒ H
  "

  ― ‹Builds the s-index if not present›
definition "hta_ensure_idx_s H ==
  case hta_idx_s H of 
    None ⇒ H⦇ hta_idx_s := Some (build_rule_index_s (hta_δ H)) ⦈ |
    Some _ ⇒ H
  "

  ― ‹Builds the sf-index if not present›
definition "hta_ensure_idx_sf H ==
  case hta_idx_sf H of 
    None ⇒ H⦇ hta_idx_sf := Some (build_rule_index_sf (hta_δ H)) ⦈ |
    Some _ ⇒ H
  "

lemma hta_ensure_idx_f_correct_α[simp]: 
  "hta_α (hta_ensure_idx_f H) = hta_α H" 
  by (simp add: hta_ensure_idx_f_def hta_α_def split: option.split)
lemma hta_ensure_idx_s_correct_α[simp]: 
  "hta_α (hta_ensure_idx_s H) = hta_α H" 
  by (simp add: hta_ensure_idx_s_def hta_α_def split: option.split)
lemma hta_ensure_idx_sf_correct_α[simp]: 
  "hta_α (hta_ensure_idx_sf H) = hta_α H" 
  by (simp add: hta_ensure_idx_sf_def hta_α_def split: option.split)

lemma hta_ensure_idx_other[simp]:
  "hta_Qi (hta_ensure_idx_f H) = hta_Qi H"  
  "hta_δ (hta_ensure_idx_f H) = hta_δ H"
  
  "hta_Qi (hta_ensure_idx_s H) = hta_Qi H"  
  "hta_δ (hta_ensure_idx_s H) = hta_δ H"
  
  "hta_Qi (hta_ensure_idx_sf H) = hta_Qi H" 
  "hta_δ (hta_ensure_idx_sf H) = hta_δ H"
  by (auto 
    simp add: hta_ensure_idx_f_def hta_ensure_idx_s_def hta_ensure_idx_sf_def 
    split: option.split)

  ― ‹Check whether the f-index is present›
definition "hta_has_idx_f H == hta_idx_f H ≠ None"
  ― ‹Check whether the s-index is present›
definition "hta_has_idx_s H == hta_idx_s H ≠ None"
  ― ‹Check whether the sf-index is present›
definition "hta_has_idx_sf H == hta_idx_sf H ≠ None"

lemma hta_idx_f_pres
  [simp, intro!]: "hta_has_idx_f (hta_ensure_idx_f H)" and
  [simp, intro]: "hta_has_idx_s H ⟹ hta_has_idx_s (hta_ensure_idx_f H)" and
  [simp, intro]: "hta_has_idx_sf H ⟹ hta_has_idx_sf (hta_ensure_idx_f H)"
  by (simp_all 
    add: hta_has_idx_f_def hta_has_idx_s_def hta_has_idx_sf_def 
         hta_ensure_idx_f_def 
    split: option.split)

lemma hta_idx_s_pres
  [simp, intro!]: "hta_has_idx_s (hta_ensure_idx_s H)" and
  [simp, intro]: "hta_has_idx_f H ⟹ hta_has_idx_f (hta_ensure_idx_s H)" and
  [simp, intro]: "hta_has_idx_sf H ⟹ hta_has_idx_sf (hta_ensure_idx_s H)"
  by (simp_all 
    add: hta_has_idx_f_def hta_has_idx_s_def hta_has_idx_sf_def 
         hta_ensure_idx_s_def 
    split: option.split)

lemma hta_idx_sf_pres
  [simp, intro!]: "hta_has_idx_sf (hta_ensure_idx_sf H)" and
  [simp, intro]: "hta_has_idx_f H ⟹ hta_has_idx_f (hta_ensure_idx_sf H)" and
  [simp, intro]: "hta_has_idx_s H ⟹ hta_has_idx_s (hta_ensure_idx_sf H)"
  by (simp_all 
    add: hta_has_idx_f_def hta_has_idx_s_def hta_has_idx_sf_def 
         hta_ensure_idx_sf_def 
    split: option.split)

text ‹
  The lookup functions are only defined if the required index is present. 
  This enforces generation of the index before applying lookup functions.
›
  ― ‹Lookup rules by function symbol›
definition "hta_lookup_f f H == hll_idx.lookup f (the (hta_idx_f H))"
  ― ‹Lookup rules by lhs-state›
definition "hta_lookup_s q H == hll_idx.lookup q (the (hta_idx_s H))"
  ― ‹Lookup rules by function symbol and lhs-state›
definition "hta_lookup_sf q f H == hll_idx.lookup (q,f) (the (hta_idx_sf H))"


  ― ‹This locale defines the invariants of a tree automaton›
locale hashedTa =
  fixes H :: "('Q::hashable,'L::hashable) hashedTa"

  ― ‹The involved sets satisfy their invariants›
  assumes invar[simp, intro!]: 
    "hs_invar (hta_Qi H)"
    "ls_invar (hta_δ H)"

  ― ‹The indices are correct, if present›
  assumes index_correct:
    "hta_idx_f H = Some idx_f 
      ⟹ hll_idx.is_index rhsl (ls_α (hta_δ H)) idx_f"
    "hta_idx_s H = Some idx_s 
      ⟹ hll_idx.is_index lhs (ls_α (hta_δ H)) idx_s"
    "hta_idx_sf H = Some idx_sf 
      ⟹ hll_idx.is_index (λr. (lhs r, rhsl r)) (ls_α (hta_δ H)) idx_sf"

begin
  ― ‹Inside this locale, some shorthand notations for the sets of 
      rules and initial states are used›
  abbreviation "δ == hta_δ H"
  abbreviation "Qi == hta_Qi H"

  ― ‹The lookup-xxx operations are correct›
  lemma hta_lookup_f_correct: 
    "hta_has_idx_f H ⟹ ls_α (hta_lookup_f f H) = {r∈ls_α δ . rhsl r = f}"
    "hta_has_idx_f H ⟹ ls_invar (hta_lookup_f f H)"
    apply (cases "hta_has_idx_f H")
    apply (unfold hta_has_idx_f_def hta_lookup_f_def)
    apply (auto 
      simp add: hll_idx.lookup_correct[OF index_correct(1)] 
                index_def)
    done

  lemma hta_lookup_s_correct: 
    "hta_has_idx_s H ⟹ ls_α (hta_lookup_s q H) = {r∈ls_α δ . lhs r = q}"
    "hta_has_idx_s H ⟹ ls_invar (hta_lookup_s q H)"
    apply (cases "hta_has_idx_s H")
    apply (unfold hta_has_idx_s_def hta_lookup_s_def)
    apply (auto 
      simp add: hll_idx.lookup_correct[OF index_correct(2)] 
                index_def)
    done

  lemma hta_lookup_sf_correct: 
    "hta_has_idx_sf H 
      ⟹ ls_α (hta_lookup_sf q f H) = {r∈ls_α δ . lhs r = q ∧ rhsl r = f}"
    "hta_has_idx_sf H ⟹ ls_invar (hta_lookup_sf q f H)"
    apply (cases "hta_has_idx_sf H")
    apply (unfold hta_has_idx_sf_def hta_lookup_sf_def)
    apply (auto 
      simp add: hll_idx.lookup_correct[OF index_correct(3)] 
                index_def)
    done

  ― ‹The ensure-index operations preserve the invariants›
  lemma hta_ensure_idx_f_correct[simp, intro!]: "hashedTa (hta_ensure_idx_f H)"
    apply (unfold_locales)
    apply (auto)
    apply (auto 
      simp add: hta_ensure_idx_f_def hta_ensure_idx_s_def hta_ensure_idx_sf_def 
               index_correct 
      split: option.split_asm)
    done

  lemma hta_ensure_idx_s_correct[simp, intro!]: "hashedTa (hta_ensure_idx_s H)"
    apply (unfold_locales)
    apply (auto)
    apply (auto 
      simp add: hta_ensure_idx_f_def hta_ensure_idx_s_def hta_ensure_idx_sf_def 
                index_correct 
      split: option.split_asm)
    done

  lemma hta_ensure_idx_sf_correct[simp, intro!]: "hashedTa (hta_ensure_idx_sf H)"
    apply (unfold_locales)
    apply (auto)
    apply (auto 
      simp add: hta_ensure_idx_f_def hta_ensure_idx_s_def hta_ensure_idx_sf_def 
                index_correct 
      split: option.split_asm)
    done

  text ‹The abstract tree automaton satisfies the invariants for an abstract
          tree automaton›
  lemma hta_α_is_ta[simp, intro!]: "tree_automaton (hta_α H)"
    apply unfold_locales
    apply (unfold hta_α_def)
    apply auto
    done

end

― ‹Add some lemmas to simpset -- also outside the locale›
lemmas [simp, intro] = 
  hashedTa.hta_ensure_idx_f_correct
  hashedTa.hta_ensure_idx_s_correct
  hashedTa.hta_ensure_idx_sf_correct

  ― ‹Build a tree automaton from a set of initial states and a set of rules›
definition "init_hta Qi δ == 
  ⦇ hta_Qi= Qi, 
    hta_δ = δ, 
    hta_idx_f = None, 
    hta_idx_s = None, 
    hta_idx_sf = None 
  ⦈"

  ― ‹Building a tree automaton from a valid tree automaton yields again a 
      valid tree automaton. This operation has the only effect of removing 
      the indices.›
lemma (in hashedTa) init_hta_is_hta: 
  "hashedTa (init_hta (hta_Qi H) (hta_δ H))"
  apply (unfold_locales)
  apply (unfold init_hta_def)
  apply (auto)
  done

subsection "Algorithm for the Word Problem"

lemma r_match_by_laz: "r_match L l = list_all_zip (λQ q. q∈Q) L l"
  by (unfold r_match_alt list_all_zip_alt)
      auto


text "Executable function that computes the set of accepting states for 
    a given tree"
fun faccs' where
  "faccs' H (NODE f ts) = (
    let Qs = List.map (faccs' H) ts in
      ll_set_xy.g_image_filter (λr. case r of (q → f' qs) ⇒ 
           if list_all_zip (λQ q. ls_memb q Q) Qs qs then Some (lhs r) else None
                          ) 
                      (hta_lookup_f f H)
  )"

  ― ‹Executable algorithm to decide the word-problem. The first version 
      depends on the f-index to be present, the second version computes the 
      index if not present.›
definition "hta_mem' t H == ¬lh_set_xx.g_disjoint (faccs' H t) (hta_Qi H)"
definition "hta_mem t H == hta_mem' t (hta_ensure_idx_f H)"

context hashedTa
begin

  lemma faccs'_invar:
    assumes HI[simp, intro!]: "hta_has_idx_f H"
    shows "ls_invar (faccs' H t)" (is ?T1) 
          "list_all ls_invar (List.map (faccs' H) ts)" (is ?T2)
  proof -
    have "?T1 ∧ ?T2"
      apply (induct rule: compat_tree_tree_list.induct)
      apply (auto simp add: ll_set_xy.image_filter_correct hta_lookup_f_correct)
      done
    thus ?T1 ?T2 by auto
  qed

  declare faccs'_invar(1)[simp, intro]

  lemma faccs'_correct:
    assumes HI[simp, intro!]: "hta_has_idx_f H"
    shows 
      "ls_α (faccs' H t) = faccs (ls_α (hta_δ H)) t" (is ?T1)
      "List.map ls_α (List.map (faccs' H) ts) 
       = List.map (faccs (ls_α (hta_δ H))) ts" (is ?T2)
  proof -
    have "?T1 ∧ ?T2"
    proof (induct rule: compat_tree_tree_list.induct)
      case (NODE f ts)
      let ?δ = "(ls_α (hta_δ H))"
      have "faccs ?δ (NODE f ts) = (
        let Qs = List.map (faccs ?δ) ts in
          {q. ∃r∈?δ. r_matchc q f Qs r })"
        by (rule faccs.simps)
      also note NODE.hyps[symmetric]
      finally have 
        1: "faccs ?δ (NODE f ts) 
            = ( let Qs = List.map ls_α (List.map (faccs' H) ts) in
                 {q. ∃r∈?δ. r_matchc q f Qs r })" .
      {
        fix Qsc:: "'Q ls list"
        assume QI: "list_all ls_invar Qsc"
        let ?Qs = "List.map ls_α Qsc"
        have "{ q. ∃r∈?δ. r_matchc q f ?Qs r } 
              = { q. ∃qs. (q → f qs)∈?δ ∧ r_match ?Qs qs }"
          apply (safe)
          apply (case_tac r)
          apply auto [1]
          apply force
          done
        also have "… = lhs ` { r∈{r∈?δ. rhsl r = f}. 
                                 case r of (q → f' qs) ⇒ r_match ?Qs qs}"
          apply auto
          apply force
          apply (case_tac xa)
          apply auto
          done
        finally have 
          1: "{ q. ∃r∈?δ. r_matchc q f ?Qs r } 
              = lhs ` { r∈{r∈?δ. rhsl r = f}. 
                         case r of (q → f' qs) ⇒ r_match ?Qs qs}" 
          by auto
        from QI have 
          [simp]: "!!qs. list_all_zip (λQ q. q∈ls_α Q) Qsc qs 
                         ⟷ list_all_zip (λQ q. ls_memb q Q) Qsc qs"
          apply (induct Qsc)
          apply (case_tac qs)
          apply auto [2]
          apply (case_tac qs)
          apply (auto simp add: ls.correct) [2]
          done
        have 2: "!!qs. r_match ?Qs qs = list_all_zip (λa b. ls_memb b a) Qsc qs"
          apply (unfold r_match_by_laz)
          apply (simp add: list_all_zip_map1)
          done
        from 1 have 
          "{ q. ∃r∈?δ. r_matchc q f ?Qs r } 
           = lhs ` { r∈{r∈?δ. rhsl r = f}. 
                     case r of (q → f' qs) ⇒ 
                       list_all_zip (λa b. ls_memb b a) Qsc qs}" 
          by (simp only: 2)
        also have 
          "… = lhs ` { r∈ls_α (hta_lookup_f f H). 
                         case r of (q → f' qs) ⇒ 
                           list_all_zip (λa b. ls_memb b a) Qsc qs}" 
          by (simp add: hta_lookup_f_correct)
        also have 
          "… = ls_α ( ll_set_xy.g_image_filter 
                         ( λr. case r of (q → f' qs) ⇒ 
                             (if (list_all_zip (λQ q. ls_memb q Q) Qsc qs) then Some (lhs r) else None))
                         (hta_lookup_f f H)
                     )"
          apply (simp add: ll_set_xy.image_filter_correct hta_lookup_f_correct)
          apply (auto split: ta_rule.split)
          apply (rule_tac x=xa in exI)
          apply auto
          apply (case_tac a)
          apply (simp add: image_iff)
          apply (rule_tac x=a in exI)
          apply auto
          done
        finally have 
          "{ q. ∃r∈?δ. r_matchc q f ?Qs r } 
           = ls_α ( ll_set_xy.g_image_filter 
                      (λr. case r of (q → f' qs) ⇒ 
                        (if (list_all_zip (λQ q. ls_memb q Q) Qsc qs) then Some (lhs r) else None))
                      (hta_lookup_f f H))" .
      } note 2=this
      
      from 
        1 
        2[ where Qsc2 = "(List.map (faccs' H) ts)", 
           simplified faccs'_invar[OF HI]] 
      show ?case by simp
    qed simp_all
    thus ?T1 ?T2 by auto
  qed

    ― ‹Correctness of the algorithms for the word problem›
  lemma hta_mem'_correct: 
    "hta_has_idx_f H ⟹ hta_mem' t H ⟷ t∈ta_lang (hta_α H)"
    apply (unfold ta_lang_def hta_α_def hta_mem'_def)
    apply (auto simp add: lh_set_xx.disjoint_correct faccs'_correct faccs_alt)
    done

  theorem hta_mem_correct: "hta_mem t H ⟷ t∈ta_lang (hta_α H)"
    using hashedTa.hta_mem'_correct[OF hta_ensure_idx_f_correct, simplified]
    apply (unfold hta_mem_def)
    apply simp
    done

end


subsection "Product Automaton and Intersection"

subsubsection "Brute Force Product Automaton"
text ‹
  In this section, an algorithm that computes the product 
  automaton without reduction is implemented. While the runtime is always
  quadratic, this algorithm is very simple and the constant factors are 
  smaller than that of the version with integrated reduction.
  Moreover, lazy languages like Haskell seem to profit from this algorithm.
›

definition δ_prod_h 
  :: "('q1::hashable,'l::hashable) ta_rule ls 
      ⇒ ('q2::hashable,'l) ta_rule ls ⇒ ('q1×'q2,'l) ta_rule ls" 
  where "δ_prod_h δ1 δ2 == 
    lll_iflt_cp.inj_image_filter_cp (λ(r1,r2). r_prod r1 r2) 
                (λ(r1,r2). rhsl r1 = rhsl r2 
                         ∧ length (rhsq r1) = length (rhsq r2)) 
                δ1 δ2"

lemma r_prod_inj: 
  "⟦ rhsl r1 = rhsl r2; length (rhsq r1) = length (rhsq r2); 
     rhsl r1' = rhsl r2'; length (rhsq r1') = length (rhsq r2'); 
     r_prod r1 r2 = r_prod r1' r2' ⟧ ⟹ r1=r1' ∧ r2=r2'"
  apply (cases r1, cases r2, cases r1', cases r2')
  apply (auto dest: zip_inj)
  done

lemma δ_prod_h_correct:
  assumes INV[simp]: "ls_invar δ1" "ls_invar δ2"
  shows 
    "ls_α (δ_prod_h δ1 δ2) = δ_prod (ls_α δ1) (ls_α δ2)"
    "ls_invar (δ_prod_h δ1 δ2)"
  apply (unfold δ_prod_def δ_prod_h_def)
  apply (subst lll_iflt_cp.inj_image_filter_cp_correct)
  apply simp_all [2]
  using r_prod_inj
  apply (auto intro!: inj_onI) []
  apply auto []
  apply (case_tac xa, case_tac y, simp, blast)
  apply force
  apply simp
  done

definition "hta_prodWR H1 H2 == 
  init_hta (hhh_cart.cart (hta_Qi H1) (hta_Qi H2)) (δ_prod_h (hta_δ H1) (hta_δ H2))"

lemma hta_prodWR_correct_aux: 
  assumes A: "hashedTa H1" "hashedTa H2"
  shows 
    "hta_α (hta_prodWR H1 H2) = ta_prod (hta_α H1) (hta_α H2)" (is ?T1)
    "hashedTa (hta_prodWR H1 H2)" (is ?T2)
proof -
  interpret a1: hashedTa H1 + a2: hashedTa H2 using A .
  show ?T1 ?T2
    apply (unfold hta_prodWR_def init_hta_def hta_α_def ta_prod_def)
    apply (simp add: hhh_cart.cart_correct δ_prod_h_correct)
    apply (unfold_locales)
    apply (simp_all add: hhh_cart.cart_correct δ_prod_h_correct)
    done
qed
  
lemma hta_prodWR_correct:
  assumes TA: "hashedTa H1" "hashedTa H2"
  shows 
    "ta_lang (hta_α (hta_prodWR H1 H2)) 
     = ta_lang (hta_α H1) ∩ ta_lang (hta_α H2)"
    "hashedTa (hta_prodWR H1 H2)"
  by (simp_all add: hta_prodWR_correct_aux[OF TA] ta_prod_correct_aux1)

subsubsection "Product Automaton with Forward-Reduction"
text ‹
  A more elaborated algorithm combines forward-reduction and the product 
  construction, i.e. product rules are only created ,,by need''.
›

  ― ‹State of the product-automaton DFS-algorithm›
type_synonym ('q1,'q2,'l) pa_state 
  = "('q1×'q2) hs × ('q1×'q2) list × ('q1×'q2,'l) ta_rule ls"

  ― ‹Abstraction mapping to algorithm specified in 
  Section~\ref{sec:absalgo}.›
definition pa_α 
  :: "('q1::hashable,'q2::hashable,'l::hashable) pa_state 
      ⇒ ('q1,'q2,'l) frp_state"
  where "pa_α S == let (Q,W,δd)=S in (hs_α Q,W,ls_α δd)"

definition pa_cond 
  :: "('q1::hashable,'q2::hashable,'l::hashable) pa_state ⇒ bool" 
  where "pa_cond S == let (Q,W,δd) = S in W≠[]"

  ― ‹Adds all successor states to the set of discovered states and to the 
  worklist›
fun pa_upd_rule 
  :: "('q1×'q2) hs ⇒ ('q1×'q2) list 
      ⇒ (('q1::hashable)×('q2::hashable)) list 
      ⇒ (('q1×'q2) hs × ('q1×'q2) list)" 
  where
  "pa_upd_rule Q W [] = (Q,W)" |
  "pa_upd_rule Q W (qp#qs) = (
    if ¬ hs_memb qp Q then
      pa_upd_rule (hs_ins qp Q) (qp#W) qs
    else pa_upd_rule Q W qs
  )"


definition pa_step 
  :: "('q1::hashable,'l::hashable) hashedTa 
      ⇒ ('q2::hashable,'l) hashedTa 
      ⇒ ('q1,'q2,'l) pa_state ⇒ ('q1,'q2,'l) pa_state"
  where "pa_step H1 H2 S == let 
    (Q,W,δd)=S;
    (q1,q2)=hd W
  in  
    ls_iteratei (hta_lookup_s q1 H1) (λ_. True) (λr1 res. 
      ls_iteratei (hta_lookup_sf q2 (rhsl r1) H2) (λ_. True) (λr2 res.
        if (length (rhsq r1) = length (rhsq r2)) then
          let 
            rp=r_prod r1 r2;
            (Q,W,δd) = res;
            (Q',W') = pa_upd_rule Q W (rhsq rp)
          in
            (Q',W',ls_ins_dj rp δd)
        else
          res
      ) res
    ) (Q,tl W,δd)
  "

definition pa_initial 
  :: "('q1::hashable,'l::hashable) hashedTa 
      ⇒ ('q2::hashable,'l) hashedTa 
      ⇒ ('q1,'q2,'l) pa_state"
where "pa_initial H1 H2 == 
  let Qip = hhh_cart.cart (hta_Qi H1) (hta_Qi H2) in (
    Qip,
    hs_to_list Qip,
    ls_empty ()
  )"

definition pa_invar_add:: 
  "('q1::hashable,'q2::hashable,'l::hashable) pa_state set" 
  where "pa_invar_add == { (Q,W,δd). hs_invar Q ∧ ls_invar δd }"

definition "pa_invar H1 H2 == 
  pa_invar_add ∩ {s. (pa_α s) ∈ frp_invar (hta_α H1) (hta_α H2)}"

definition "pa_det_algo H1 H2 
  == ⦇ dwa_cond=pa_cond, 
       dwa_step = pa_step H1 H2, 
       dwa_initial = pa_initial H1 H2, 
       dwa_invar = pa_invar H1 H2 ⦈"

lemma pa_upd_rule_correct:
  assumes INV[simp, intro!]: "hs_invar Q"
  assumes FMT: "pa_upd_rule Q W qs = (Q',W')"
  shows
    "hs_invar Q'" (is ?T1)
    "hs_α Q' = hs_α Q ∪ set qs" (is ?T2)
    "∃Wn. distinct Wn ∧ set Wn = set qs - hs_α Q ∧ W'=Wn@W" (is ?T3)
proof -
  from INV FMT have "?T1 ∧ ?T2 ∧ ?T3"
  proof (induct qs arbitrary: Q W Q' W')
    case Nil thus ?case by simp
  next
    case (Cons q qs Q W Q' W')
    show ?case 
    proof (cases "q∈hs_α Q")
      case True 
      obtain Qh Wh where RF: "pa_upd_rule Q W qs = (Qh,Wh)" by force
      with True Cons.prems have [simp]: "Q'=Qh" "W'=Wh"
        by (auto simp add: hs.correct)
      from Cons.hyps[OF Cons.prems(1) RF] have
        "hs_invar Qh" 
        "hs_α Qh = hs_α Q ∪ set qs" 
        "(∃Wn. distinct Wn ∧ set Wn = set qs - hs_α Q ∧ Wh = Wn @ W)"
        by auto
      thus ?thesis using True by auto
    next
      case False
      with Cons.prems have RF: "pa_upd_rule (hs_ins q Q) (q#W) qs = (Q',W')"
        by (auto simp add: hs.correct)

      from Cons.hyps[OF _ RF] Cons.prems(1) have
        "hs_invar Q'" 
        "hs_α Q' = insert q (hs_α Q) ∪ set (qs)"
        "∃Wn. distinct Wn 
              ∧ set Wn = set qs - insert q (hs_α Q) 
              ∧ W' = Wn @ q # W"
        by (auto simp add: hs.correct)
      thus ?thesis using False by auto
    qed
  qed
  thus ?T1 ?T2 ?T3 by auto
qed


lemma pa_step_correct:
  assumes TA: "hashedTa H1" "hashedTa H2"
  assumes idx[simp]: "hta_has_idx_s H1" "hta_has_idx_sf H2"
  assumes INV: "(Q,W,δd)∈pa_invar H1 H2"
  assumes COND: "pa_cond (Q,W,δd)"
  shows 
    "(pa_step H1 H2 (Q,W,δd))∈pa_invar_add" (is ?T1)
    "(pa_α (Q,W,δd), pa_α (pa_step H1 H2 (Q,W,δd))) 
     ∈ frp_step (ls_α (hta_δ H1)) (ls_α (hta_δ H2))" (is ?T2)
proof -
  interpret h1: hashedTa H1 by fact
  interpret h2: hashedTa H2 by fact

  from COND obtain q1 q2 Wtl where 
    [simp]: "W=(q1,q2)#Wtl" 
    by (cases W) (auto simp add: pa_cond_def)

  from INV have [simp]: "hs_invar Q" "ls_invar δd" 
    by (auto simp add: pa_invar_add_def pa_invar_def)

  define inv where "inv = (λδp (Q', W', δd'). 
    hs_invar Q' 
    ∧ ls_invar δd' 
    ∧ (∃Wn. distinct Wn 
            ∧ set Wn = (f_succ δp `` {(q1,q2)}) - hs_α Q 
            ∧ W'=Wn@Wtl 
            ∧ hs_α Q'=hs_α Q ∪ (f_succ δp `` {(q1,q2)}))
    ∧ (ls_α δd' = ls_α δd ∪ {r∈δp. lhs r = (q1,q2) }))"

  have G: "inv (δ_prod (ls_α (hta_δ H1)) (ls_α (hta_δ H2))) 
               (pa_step H1 H2 (Q,W,δd))"
    apply (unfold pa_step_def)
    apply simp
    apply (rule_tac 
      I="λit1 res. inv (δ_prod (ls_α (hta_δ H1) - it1) (ls_α (hta_δ H2))) res"
      in ls.iterate_rule_P)
    ― ‹Invar›
    apply (simp add: h1.hta_lookup_s_correct)
    ― ‹Initial›
    apply (fastforce simp add: inv_def δ_prod_def h1.hta_lookup_s_correct 
                              f_succ_alt)
    ― ‹Step›
    apply (rule_tac 
      I="λit2 res. inv ( δ_prod (ls_α (hta_δ H1) - it) (ls_α (hta_δ H2)) 
                         ∪ δ_prod {x} (ls_α (hta_δ H2) - it2)) 
                        res" 
      in ls.iterate_rule_P)
      ― ‹Invar›
      apply (simp add: h2.hta_lookup_sf_correct)
      ― ‹Init›
      apply (case_tac σ)
      apply (simp add: inv_def h1.hta_lookup_s_correct h2.hta_lookup_sf_correct)
      apply (force simp add: f_succ_alt elim: δ_prodE intro: δ_prodI) [1]
      ― ‹Step›
      defer ― ‹Requires considerably more work: Deferred to Isar proof below›
      ― ‹Final›
      apply (simp add: h1.hta_lookup_s_correct h2.hta_lookup_sf_correct)
      apply (auto) [1]
      apply (subgoal_tac 
        "ls_α (hta_δ H1) - (it - {x}) = (ls_α (hta_δ H1) - it) ∪ {x}")
      apply (simp add: δ_prod_insert)
      apply (subst Un_commute)
      apply simp
      apply blast
    ― ‹Final›
    apply force
  proof goal_cases
    case prems: (1 r1 it1 resxh r2 it2 resh)
    ― ‹Resolve lookup-operations›
    hence G': 
      "it1 ⊆ {r ∈ ls_α (hta_δ H1). lhs r = q1}" 
      "it2 ⊆ {r ∈ ls_α (hta_δ H2). lhs r = q2 ∧ rhsl r = rhsl r1}"
      by (simp_all add: h1.hta_lookup_s_correct h2.hta_lookup_sf_correct)

    ― ‹Basic reasoning setup›
    from prems(1,4) G' have 
      [simp]: "ls_α (hta_δ H2) - (it2 - {r2}) = (ls_α (hta_δ H2) - it2) ∪ {r2}"
      by auto
    obtain Qh Wh δdh Q' W' δd' where [simp]: "resh=(Qh,Wh,δdh)" 
      by (cases resh) fastforce
    from prems(6) have INVAH[simp]: "hs_invar Qh" "ls_invar δdh" 
      by (auto simp add: inv_def)

    ― ‹The involved rules have the same label, and their lhs is determined›
    from prems(1,4) G' obtain l qs1 qs2 where 
      RULE_FMT: "r1 = (q1 → l qs1)" "r2=(q2 → l qs2)"
      apply (cases r1, cases r2)
      apply force
      done

    {
      ― ‹If the rhs have different lengths, the algorithm ignores the rule:›
      assume LEN: "length (rhsq r1) ≠ length (rhsq r2)"
      
      hence [simp]: "δ_prod_sng2 {r1} r2 = {}"
        by (auto simp add: δ_prod_sng2_def split: ta_rule.split)

      have ?case using prems 
        by (simp add: LEN δ_prod_insert)
    } moreover {
      ― ‹If the rhs have the same length, the rule is inserted›
      assume LEN: "length (rhsq r1) = length (rhsq r2)"
      hence [simp]: "length qs1 = length qs2" by (simp add: RULE_FMT)

      hence [simp]: "δ_prod_sng2 {r1} r2 = {(q1,q2) → l (zip qs1 qs2)}"
        using prems(1,4) G'
        by (auto simp add: δ_prod_sng2_def RULE_FMT)

      ― ‹Obtain invariant of previous state›
      from prems(6)[unfolded inv_def, simplified] obtain Wn where INVH:
        "distinct Wn"
        "set Wn = f_succ (δ_prod (ls_α (hta_δ H1) - it1) (ls_α (hta_δ H2)) 
                          ∪ δ_prod {r1} (ls_α (hta_δ H2) - it2)) 
                  `` {(q1, q2)} - hs_α Q"
        "Wh = Wn @ Wtl" 
        "hs_α Qh = hs_α Q 
                   ∪ f_succ (δ_prod (ls_α (hta_δ H1) - it1) (ls_α (hta_δ H2))
                              ∪ δ_prod {r1} (ls_α (hta_δ H2) - it2)) 
                      `` {(q1, q2)}" 
        "ls_α δdh = ls_α δd 
          ∪ {r. ( r ∈ δ_prod (ls_α (hta_δ H1) - it1) (ls_α (hta_δ H2)) 
                  ∨ r ∈ δ_prod {r1} (ls_α (hta_δ H2) - it2)
                 ) ∧ lhs r = (q1, q2)
             }"
        by blast

      ― ‹Required to justify disjoint insert›
      have RPD: "r_prod r1 r2 ∉ ls_α δdh" 
      proof -
        from INV[unfolded pa_invar_def frp_invar_def frp_invar_add_def]
        have LSDD: 
          "ls_α δd = {r ∈ δ_prod (ls_α (hta_δ H1)) (ls_α (hta_δ H2)). 
                        lhs r ∈ hs_α Q - set W}"
          by (auto simp add: pa_α_def hta_α_def)
        have "r_prod r1 r2 ∉ ls_α δd"
        proof
          assume "r_prod r1 r2 ∈ ls_α δd"
          with LSDD have "lhs (r_prod r1 r2) ∉ set W" by auto
          moreover from prems(1,4) G' have "lhs (r_prod r1 r2) = (q1,q2)" 
            by (cases r1, cases r2) auto
          ultimately show False by simp
        qed
        moreover from prems(6) have "ls_α δdh = 
          ls_α δd ∪ 
          {r. ( r ∈ δ_prod (ls_α (hta_δ H1) - it1) (ls_α (hta_δ H2)) 
                ∨ r ∈ δ_prod {r1} (ls_α (hta_δ H2) - it2)
              ) ∧ lhs r = (q1, q2)}" (is "_= _ ∪ ?s")
          by (simp add: inv_def)
        moreover have "r_prod r1 r2 ∉ ?s" using prems(1,4) G'(2) LEN
          apply (cases r1, cases r2)
          apply (auto simp add: δ_prod_def)
          done
        ultimately show ?thesis by blast
      qed

      ― ‹Correctness of result of @{text pa_upd_rule}›
      obtain Q' W' where 
        PAUF: "(pa_upd_rule Qh Wh (rhsq (r_prod r1 r2))) = (Q',W')" 
        by force
      from pa_upd_rule_correct[OF INVAH(1) PAUF] obtain Wnn where UC:
        "hs_invar Q'"
        "hs_α Q' = hs_α Qh ∪ set (rhsq (r_prod r1 r2))"
        "distinct Wnn" 
        "set Wnn = set (rhsq (r_prod r1 r2)) - hs_α Qh" 
        "W' = Wnn @ Wh"
        by blast

      ― ‹Put it all together›
      have ?case
        apply (simp add: LEN Let_def ls.ins_dj_correct[OF INVAH(2) RPD] 
                         PAUF inv_def UC(1))
        apply (intro conjI)
        apply (rule_tac x="Wnn@Wn" in exI)
        apply (auto simp add: f_succ_alt δ_prod_insert RULE_FMT UC INVH 
                              δ_prod_sng2_def δ_prod_sng1_def)
        done
    } ultimately show ?case by blast
  qed
  from G show ?T1
    by (cases "pa_step H1 H2 (Q,W,δd)")
       (simp add: pa_invar_add_def inv_def)
  from G show ?T2
    by (cases "pa_step H1 H2 (Q,W,δd)")
       (auto simp add: inv_def pa_α_def Let_def intro: frp_step.intros)

qed
    
  

  ― ‹The product-automaton algorithm is a precise implementation of its
      specification›
lemma pa_pref_frp: 
  assumes TA: "hashedTa H1" "hashedTa H2"
  assumes idx[simp]: "hta_has_idx_s H1" "hta_has_idx_sf H2"

  shows "wa_precise_refine (det_wa_wa (pa_det_algo H1 H2)) 
                           (frp_algo (hta_α H1) (hta_α H2)) 
                           pa_α"
proof -
  interpret h1: hashedTa H1 by fact
  interpret h2: hashedTa H2 by fact
  
  show ?thesis
    apply (unfold_locales)
    apply (auto simp add: det_wa_wa_def pa_det_algo_def pa_α_def 
                          pa_cond_def frp_algo_def frp_cond_def) [1]
    apply (auto simp add: det_wa_wa_def pa_det_algo_def pa_cond_def
                          hta_α_def frp_algo_def frp_cond_def 
                intro!: pa_step_correct(2)[OF TA]) [1]
    apply (auto simp add: det_wa_wa_def pa_det_algo_def pa_α_def 
                          hta_α_def pa_cond_def frp_algo_def frp_cond_def
                          pa_invar_def pa_step_def pa_initial_def 
                          hs.correct ls.correct Let_def hhh_cart.cart_correct 
                intro: frp_initial.intros
    ) [3]
    done
qed


  ― ‹The product automaton algorithm is a correct while-algorithm›
lemma pa_while_algo: 
  assumes TA: "hashedTa H1" "hashedTa H2"
  assumes idx[simp]: "hta_has_idx_s H1" "hta_has_idx_sf H2"

  shows "while_algo (det_wa_wa (pa_det_algo H1 H2))"
proof -
  interpret h1: hashedTa H1 by fact
  interpret h2: hashedTa H2 by fact

  interpret ref: wa_precise_refine "(det_wa_wa (pa_det_algo H1 H2))" 
                                   "(frp_algo (hta_α H1) (hta_α H2))" 
                                   "pa_α" 
    using pa_pref_frp[OF TA idx] .
  show ?thesis
    apply (rule ref.wa_intro)
    apply (simp add: frp_while_algo)
    apply (simp add: det_wa_wa_def pa_det_algo_def pa_invar_def frp_algo_def)

    apply (auto simp add: det_wa_wa_def pa_det_algo_def) [1]
    apply (rule pa_step_correct(1)[OF TA idx])
    apply (auto simp add: pa_invar_def frp_algo_def) [2]
    
    apply (simp add: det_wa_wa_def pa_det_algo_def pa_initial_def 
                     pa_invar_add_def Let_def hhh_cart.cart_correct ls.correct)
    done
qed
    
― ‹By definition, the product automaton algorithm is deterministic›
lemmas pa_det_while_algo = det_while_algo_intro[OF pa_while_algo]

― ‹Transferred correctness lemma›
lemmas pa_inv_final = 
  wa_precise_refine.transfer_correctness[OF pa_pref_frp frp_inv_final]


― ‹The next two definitions specify the product-automata algorithm. The first
    version requires the s-index of the first and the sf-index of the second
    automaton to be present, while the second version computes the required 
    indices, if necessary›
definition "hta_prod' H1 H2 ==
  let (Q,W,δd) = while pa_cond (pa_step H1 H2) (pa_initial H1 H2) in
    init_hta (hhh_cart.cart (hta_Qi H1) (hta_Qi H2)) δd
  "

definition "hta_prod H1 H2 == 
  hta_prod' (hta_ensure_idx_s H1) (hta_ensure_idx_sf H2)"


lemma hta_prod'_correct_aux:
  assumes TA: "hashedTa H1" "hashedTa H2"
  assumes idx: "hta_has_idx_s H1" "hta_has_idx_sf H2"
  shows "hta_α (hta_prod' H1 H2) 
         = ta_fwd_reduce (ta_prod (hta_α H1) (hta_α H2))" (is ?T1)
        "hashedTa (hta_prod' H1 H2)" (is ?T2)
proof -
  interpret h1: hashedTa H1 by fact
  interpret h2: hashedTa H2 by fact

  interpret dwa: det_while_algo "pa_det_algo H1 H2" 
    using pa_det_while_algo[OF TA idx] .

  have LC: "while pa_cond (pa_step H1 H2) (pa_initial H1 H2) = dwa.loop"
    by (unfold dwa.loop_def)
       (simp add: pa_det_algo_def)

  from dwa.while_proof'[OF pa_inv_final[OF TA idx]]
  show ?T1
    apply (unfold dwa.loop_def)
    apply (simp add: hta_prod'_def init_hta_def hta_α_def pa_det_algo_def)
    apply (cases "(while pa_cond (pa_step H1 H2) (pa_initial H1 H2))")
    apply (simp add: pa_α_def hhh_cart.cart_correct hta_α_def)
    done

  show ?T2
    apply (simp add: hta_prod'_def LC)
    apply (rule dwa.while_proof)
    apply (case_tac s)
    apply (simp add: pa_det_algo_def pa_invar_add_def pa_invar_def init_hta_def)
    apply unfold_locales
    apply (simp_all add: hhh_cart.cart_correct)
    done
qed

theorem hta_prod'_correct:
  assumes TA: "hashedTa H1" "hashedTa H2"
  assumes HI: "hta_has_idx_s H1" "hta_has_idx_sf H2"
  shows 
    "ta_lang (hta_α (hta_prod' H1 H2)) 
     = ta_lang (hta_α H1) ∩ ta_lang (hta_α H2)"

    "hashedTa (hta_prod' H1 H2)"
  by (simp_all add: hta_prod'_correct_aux[OF TA HI] ta_prod_correct_aux1)

lemma hta_prod_correct_aux:
  assumes TA[simp]: "hashedTa H1" "hashedTa H2"
  shows 
    "hta_α (hta_prod H1 H2) = ta_fwd_reduce (ta_prod (hta_α H1) (hta_α H2))"
    "hashedTa (hta_prod H1 H2)"
  by (unfold hta_prod_def)
     (simp_all add: hta_prod'_correct_aux)
  
theorem hta_prod_correct:
  assumes TA: "hashedTa H1" "hashedTa H2"
  shows 
    "ta_lang (hta_α (hta_prod H1 H2)) 
     = ta_lang (hta_α H1) ∩ ta_lang (hta_α H2)"
    "hashedTa (hta_prod H1 H2)"
  by (simp_all add: hta_prod_correct_aux[OF TA] ta_prod_correct_aux1)


subsection "Remap States"

― ‹Mapping the states of an automaton›
definition hta_remap 
  :: "('q::hashable ⇒ 'qn::hashable) ⇒ ('q,'l::hashable) hashedTa 
      ⇒ ('qn,'l) hashedTa" 
  where "hta_remap f H == 
    init_hta (hh_set_xy.g_image f (hta_Qi H)) 
      (ll_set_xy.g_image (remap_rule f) (hta_δ H))"
  
lemma (in hashedTa) hta_remap_correct:
  shows "hta_α (hta_remap f H) = ta_remap f (hta_α H)"
        "hashedTa (hta_remap f H)"
  apply (auto 
    simp add: hta_remap_def init_hta_def hta_α_def 
              hh_set_xy.image_correct ll_set_xy.image_correct ta_remap_def)
  apply (unfold_locales)
  apply (auto simp add: hh_set_xy.image_correct ll_set_xy.image_correct)
  done


subsubsection "Reindex Automaton"
text ‹
  In this section, an algorithm for re-indexing the states of the automaton to
  an initial segment of the naturals is implemented. The language of the 
  automaton is not changed by the reindexing operation.
›

  ― ‹Set of states of a rule›
fun rule_states_l where
  "rule_states_l (q → f qs) = ls_ins q (ls.from_list qs)"

lemma rule_states_l_correct[simp]: 
  "ls_α (rule_states_l r) = rule_states r"
  "ls_invar (rule_states_l r)"
  by (cases r, simp add: ls.correct)+

definition "hta_δ_states H 
  == (llh_set_xyy.g_Union_image id (ll_set_xy.g_image_filter 
       (λr. Some (rule_states_l r)) (hta_δ H)))"

definition "hta_states H ==
  hs_union (hta_Qi H) (hta_δ_states H)"

lemma (in hashedTa) hta_δ_states_correct:
  "hs_α (hta_δ_states H) = δ_states (ta_rules (hta_α H))"
  "hs_invar (hta_δ_states H)"
proof (simp_all add: hta_α_def hta_δ_states_def, goal_cases)
  case 1
  have 
    [simp]: "ls_α (ll_set_xy.g_image_filter (λx. Some (rule_states_l x)) δ) 
             = rule_states_l ` ls_α δ"
    by (auto simp add: ll_set_xy.image_filter_correct)
  show ?case
    apply (simp add: δ_states_def)
    apply (subst
      llh_set_xyy.Union_image_correct[
        of "(ll_set_xy.g_image_filter (λx. Some (rule_states_l x)) δ)", 
        simplified])
    apply (auto simp add: ll_set_xy.image_filter_correct)
    done
(*next
  case goal2 thus ?case
    apply (rule llh.Union_image_correct)
    apply (auto simp add: ls.image_filter_correct)
    done*)
qed

lemma (in hashedTa) hta_states_correct:
  "hs_α (hta_states H) = ta_rstates (hta_α H)"
  "hs_invar (hta_states H)"
  by (simp_all 
    add: hta_states_def ta_rstates_def hs.correct hta_δ_states_correct 
         hta_α_def)

definition "reindex_map H == 
  λq. the (hm_lookup q (hh_map_to_nat.map_to_nat (hta_states H)))"

definition hta_reindex 
  :: "('Q::hashable,'L::hashable) hashedTa ⇒ (nat,'L) hashedTa" where
  "hta_reindex H == hta_remap (reindex_map H) H"

declare hta_reindex_def [code del]

  ― ‹This version is more efficient, as the map is only computed once›
lemma [code]: "hta_reindex H = (
  let mp = (hh_map_to_nat.map_to_nat (hta_states H)) in
    hta_remap (λq. the (hm_lookup q mp)) H)
  "
  by (simp add: Let_def hta_reindex_def reindex_map_def)


lemma (in hashedTa) reindex_map_correct:
  "inj_on (reindex_map H) (ta_rstates (hta_α H))"
proof -
  have [simp]: 
    "reindex_map H = the ∘ hm_α (hh_map_to_nat.map_to_nat (hta_states H))"
    by (rule ext)
       (simp add: reindex_map_def hm.correct 
         hh_map_to_nat.map_to_nat_correct(4) 
         hta_states_correct)

  show ?thesis
    apply (simp add: hta_states_correct(1)[symmetric])
    apply (rule inj_on_map_the)
    apply (simp_all add: hh_map_to_nat.map_to_nat_correct hta_states_correct(2))
    done
qed

theorem (in hashedTa) hta_reindex_correct:
  "ta_lang (hta_α (hta_reindex H)) = ta_lang (hta_α H)"
  "hashedTa (hta_reindex H)"
  apply (unfold hta_reindex_def)
  apply (simp_all 
    add: hta_remap_correct tree_automaton.remap_lang[OF hta_α_is_ta] 
         reindex_map_correct)
  done

subsection "Union"

text "Computes the union of two automata"
definition hta_union 
  :: "('q1::hashable,'l::hashable) hashedTa 
      ⇒ ('q2::hashable,'l) hashedTa 
      ⇒ (('q1,'q2) ustate_wrapper,'l) hashedTa" 
  where "hta_union H1 H2 == 
    init_hta (hs_union (hh_set_xy.g_image USW1 (hta_Qi H1)) 
                       (hh_set_xy.g_image USW2 (hta_Qi H2))) 
             (ls_union_dj (ll_set_xy.g_image (remap_rule USW1) (hta_δ H1)) 
                          (ll_set_xy.g_image (remap_rule USW2) (hta_δ H2)))"

lemma hta_union_correct': 
  assumes TA: "hashedTa H1" "hashedTa H2"
  shows "hta_α (hta_union H1 H2) 
         = ta_union_wrap (hta_α H1) (hta_α H2)" (is ?T1)
        "hashedTa (hta_union H1 H2)" (is ?T2)
proof -
  interpret a1: hashedTa H1 + a2: hashedTa H2 using TA .
  show ?T1 ?T2 
    apply (auto 
      simp add: hta_union_def init_hta_def hta_α_def 
                hs.correct ls.correct 
                ll_set_xy.image_correct hh_set_xy.image_correct
                ta_remap_def ta_union_def ta_union_wrap_def)
    apply (unfold_locales)
    apply (auto 
      simp add: hs.correct ls.correct)
    done
qed

theorem hta_union_correct: 
  assumes TA: "hashedTa H1" "hashedTa H2"
  shows 
    "ta_lang (hta_α (hta_union H1 H2)) 
     = ta_lang (hta_α H1) ∪ ta_lang (hta_α H2)" (is ?T1)
    "hashedTa (hta_union H1 H2)" (is ?T2)
proof -
  interpret a1: hashedTa H1 + a2: hashedTa H2 using TA .
  show ?T1 ?T2
    by (simp_all add: hta_union_correct'[OF TA] ta_union_wrap_correct)
qed

subsection "Operators to Construct Tree Automata"
text ‹
  This section defines operators that add initial states and rules to a tree 
  automaton, and thus incrementally construct a tree automaton from the empty
  automaton.
›

― ‹The empty automaton›
definition hta_empty :: "unit ⇒ ('q::hashable,'l::hashable) hashedTa" 
  where "hta_empty u == init_hta (hs_empty ()) (ls_empty ())"
lemma hta_empty_correct [simp, intro!]: 
  shows "(hta_α (hta_empty ())) = ta_empty"
        "hashedTa (hta_empty ())"
  apply (auto
    simp add: init_hta_def hta_empty_def hta_α_def δ_states_def ta_empty_def
              hs.correct ls.correct)
  apply (unfold_locales)
  apply (auto simp add: hs.correct ls.correct)
  done

― ‹Add an initial state to the automaton›
definition hta_add_qi 
  :: "'q ⇒ ('q::hashable,'l::hashable) hashedTa ⇒ ('q,'l) hashedTa" 
  where "hta_add_qi qi H == init_hta (hs_ins qi (hta_Qi H)) (hta_δ H)"

lemma (in hashedTa) hta_add_qi_correct[simp, intro!]:
  shows "hta_α (hta_add_qi qi H) 
         = ⦇ ta_initial = insert qi (ta_initial (hta_α H)), 
             ta_rules = ta_rules (hta_α H) 
           ⦈"
        "hashedTa (hta_add_qi qi H)"
  apply (auto 
    simp add: init_hta_def hta_add_qi_def hta_α_def δ_states_def 
              hs.correct)
  apply (unfold_locales)
  apply (auto simp add: hs.correct)
  done

lemmas [simp, intro] = hashedTa.hta_add_qi_correct

― ‹Add a rule to the automaton›
definition hta_add_rule 
  :: "('q,'l) ta_rule ⇒ ('q::hashable,'l::hashable) hashedTa 
      ⇒ ('q,'l) hashedTa" 
  where "hta_add_rule r H == init_hta (hta_Qi H) (ls_ins r (hta_δ H))"

lemma (in hashedTa) hta_add_rule_correct[simp, intro!]:
  shows "hta_α (hta_add_rule r H) 
         = ⦇ ta_initial = ta_initial (hta_α H), 
             ta_rules = insert r (ta_rules (hta_α H)) 
           ⦈"
        "hashedTa (hta_add_rule r H)"
  apply (auto 
    simp add: init_hta_def hta_add_rule_def hta_α_def 
              δ_states_def ls.correct)
  apply (unfold_locales)
  apply (auto simp add: ls.correct)
  done

lemmas [simp, intro] = hashedTa.hta_add_rule_correct


  ― ‹Reduces an automaton to the given set of states›
definition "hta_reduce H Q ==
  init_hta (hs_inter Q (hta_Qi H)) 
           (ll_set_xy.g_image_filter 
              (λr. if hs_memb (lhs r) Q ∧ list_all (λq. hs_memb q Q) (rhsq r) then Some r else None) 
              (hta_δ H))
"

theorem (in hashedTa) hta_reduce_correct:
  assumes INV[simp]: "hs_invar Q"
  shows
  "hta_α (hta_reduce H Q) = ta_reduce (hta_α H) (hs_α Q)" (is ?T1)
  "hashedTa (hta_reduce H Q)" (is ?T2)
  apply (auto 
    simp add: 
      hta_reduce_def ta_reduce_def hta_α_def init_hta_def 
      hs.correct ls.correct
    (*hs_correct ls_correct *)
      list_all_iff 
      reduce_rules_def rule_states_simp 
      ll_set_xy.image_filter_correct
    split: 
      ta_rule.split_asm
  ) [1]
  apply (unfold_locales)
  apply (unfold hta_reduce_def init_hta_def)
  apply (auto simp add: hs.correct ls.correct)
  done



subsection "Backwards Reduction and Emptiness Check"

text ‹
  The algorithm uses a map from states to the set of rules that contain 
  the state on their rhs.
›

  ― ‹Add an entry to the index›
definition "rqrm_add q r res ==
  case hm_lookup q res of
    None ⇒ hm_update q (ls_ins r (ls_empty ())) res |
    Some s ⇒ hm_update q (ls_ins r s) res
  "

  ― ‹Lookup the set of rules with given state on rhs›
definition "rqrm_lookup rqrm q == case hm_lookup q rqrm of
  None ⇒ ls_empty () |
  Some s ⇒ s
  "

  ― ‹Build the index from a set of rules›
definition build_rqrm 
  :: "('q::hashable,'l::hashable) ta_rule ls 
      ⇒ ('q,('q,'l) ta_rule ls) hm" 
  where
  "build_rqrm δ ==
    ls_iteratei δ (λ_. True)
      (λr res. 
        foldl (λres q. rqrm_add q r res) res (rhsq r)
      )
      (hm_empty ())
  "

― ‹Whether the index satisfies the map and set invariants›
definition "rqrm_invar rqrm == 
  hm_invar rqrm ∧ (∀q. ls_invar (rqrm_lookup rqrm q))"
― ‹Whether the index really maps a state to the set of rules with this 
    state on their rhs›
definition "rqrm_prop δ rqrm == 
  ∀q. ls_α (rqrm_lookup rqrm q) = {r∈δ. q∈set (rhsq r)}"

lemma rqrm_α_lookup_update[simp]: 
  "rqrm_invar rqrm ⟹ 
    ls_α (rqrm_lookup (rqrm_add q r rqrm) q') 
    = ( if q=q' then 
          insert r (ls_α (rqrm_lookup rqrm q')) 
        else 
          ls_α (rqrm_lookup rqrm q')
      )"
  by (simp 
    add: rqrm_lookup_def rqrm_add_def rqrm_invar_def hm.correct 
         ls.correct 
    split: option.split_asm option.split)

lemma rqrm_propD: 
  "rqrm_prop δ rqrm ⟹ ls_α (rqrm_lookup rqrm q) = {r∈δ. q∈set (rhsq r)}"
  by (simp add: rqrm_prop_def)

lemma build_rqrm_correct:
  fixes δ
  assumes [simp]: "ls_invar δ"
  shows "rqrm_invar (build_rqrm δ)" (is ?T1) and
        "rqrm_prop (ls_α δ) (build_rqrm δ)" (is ?T2)
proof -
  have "rqrm_invar (build_rqrm δ) ∧ 
    (∀q. ls_α (rqrm_lookup (build_rqrm δ) q) = {r∈ls_α δ. q∈set (rhsq r)})"
    apply (unfold build_rqrm_def)
    apply (rule_tac 
      I="λit res. (rqrm_invar res) 
                  ∧ (∀q. ls_α (rqrm_lookup res q) 
                     = {r∈ls_α δ - it. q∈set (rhsq r)})" 
      in ls.iterate_rule_P)
      ― ‹Invar›
    apply simp
      ― ‹Initial›
    apply (simp add: hm_correct ls_correct rqrm_lookup_def rqrm_invar_def)
      ― ‹Step›
    apply (rule_tac 
      I="λres itl itr. 
        (rqrm_invar res) 
        ∧ (∀q. ls_α (rqrm_lookup res q) 
           = {r∈ls_α δ - it. q∈set (rhsq r)} 
             ∪ {r. r=x ∧ q∈set itl})" 
      in Misc.foldl_rule_P)
        ― ‹Initial›
      apply simp
        ― ‹Step›
      apply (intro conjI)
      apply (simp 
        add: rqrm_invar_def rqrm_add_def rqrm_lookup_def hm_correct 
             ls_correct 
        split: option.split option.split_asm)
      apply simp
      apply (simp 
        add: rqrm_add_def rqrm_lookup_def hm_correct ls_correct 
        split: option.split option.split_asm)
      apply (auto) [1]
        ― ‹Final›
      apply auto [1]
      ― ‹Final›
    apply simp
    done
  thus ?T1 ?T2 by (simp_all add: rqrm_prop_def)
qed

― ‹A state of the basic algorithm contains a set of discovered states, 
    a worklist and a map from rules to the number of distinct states on 
    its RHS that have not yet been discovered or are still on the worklist›
type_synonym ('Q,'L) brc_state 
  = "'Q hs × 'Q list × (('Q,'L) ta_rule, nat) hm"

― ‹Abstraction to @{text α'}-level:›
definition brc_α 
  :: "('Q::hashable,'L::hashable) brc_state ⇒ ('Q,'L) br'_state"
  where "brc_α == λ(Q,W,rcm). (hs_α Q, set W, hm_α rcm)"

definition brc_invar_add :: "('Q::hashable,'L::hashable) brc_state set" 
  where
  "brc_invar_add == {(Q,W,rcm). 
    hs_invar Q ∧ 
    distinct W ∧ 
    hm_invar rcm
    ⌦‹∧ set W ⊆ hs_α Q›}
  "

definition "brc_invar δ == brc_invar_add ∩ {s. brc_α s ∈ br'_invar δ}"

definition brc_cond :: "('q::hashable,'l::hashable) brc_state ⇒ bool" 
  where "brc_cond == λ(Q,W,rcm). W≠[]"

definition brc_inner_step 
  :: "('q,'l) ta_rule ⇒ ('q::hashable,'l::hashable) brc_state 
      ⇒ ('q,'l) brc_state"
  where 
  "brc_inner_step r == λ(Q,W,rcm). 
    let c=the (hm_lookup r rcm);
        rcm' = hm_update r (c-(1::nat)) rcm;
        Q' = (if c ≤ 1 then hs_ins (lhs r) Q else Q);
        W' = (if c ≤ 1 ∧ ¬ hs_memb (lhs r) Q then lhs r # W else W) in
      (Q',W',rcm')"

definition brc_step 
  :: "('q,('q,'l) ta_rule ls) hm 
      ⇒ ('q::hashable,'l::hashable) brc_state 
      ⇒ ('q,'l) brc_state" 
where 
  "brc_step rqrm == λ(Q,W,rcm).
    ls_iteratei (rqrm_lookup rqrm (hd W)) (λ_. True) brc_inner_step 
      (Q,tl W, rcm)"

  ― ‹Initial concrete state›
definition brc_iq :: "('q,'l) ta_rule ls ⇒ 'q::hashable hs" 
  where "brc_iq δ == lh_set_xy.g_image_filter (λr. 
    if rhsq r = [] then Some (lhs r) else None) δ"

definition brc_rcm_init 
  :: "('q::hashable,'l::hashable) ta_rule ls 
      ⇒ (('q,'l) ta_rule,nat) hm" 
  where "brc_rcm_init δ == 
    ls_iteratei δ (λ_. True) 
      (λr res. hm_update r ((length (remdups (rhsq r)))) res) 
      (hm_empty ())"

definition brc_initial 
  :: "('q::hashable,'l::hashable) ta_rule ls ⇒ ('q,'l) brc_state" 
  where "brc_initial δ == 
    let iq=brc_iq δ in 
      (iq, hs_to_list (iq), brc_rcm_init δ)"

definition "brc_det_algo rqrm δ == ⦇
  dwa_cond = brc_cond,
  dwa_step = brc_step rqrm,
  dwa_initial = brc_initial δ,
  dwa_invar = brc_invar (ls_α δ)
⦈"

  ― ‹Additional facts needed from the abstract level›
lemma brc_inv_imp_WssQ: "brc_α (Q,W,rcm)∈br'_invar δ ⟹ set W ⊆ hs_α Q"
  by (auto simp add: brc_α_def br'_invar_def br'_α_def br_invar_def)

lemma brc_iq_correct: 
  assumes [simp]: "ls_invar δ"
  shows "hs_invar (brc_iq δ)"
        "hs_α (brc_iq δ) = br_iq (ls_α δ)"
  by (auto simp add: brc_iq_def br_iq_def lh_set_xy.image_filter_correct)

lemma brc_rcm_init_correct:
  assumes INV[simp]: "ls_invar δ"
  shows "r∈ls_α δ 
    ⟹ hm_α (brc_rcm_init δ) r = Some ((card (set (rhsq r))))" 
  (is "_ ⟹ ?T1 r") and
    "hm_invar (brc_rcm_init δ)" (is ?T2)
proof -
  have G: "(∀r∈ls_α δ. ?T1 r) ∧ ?T2"
    apply (unfold brc_rcm_init_def)
    apply (rule_tac 
      I="λit res. hm_invar res 
           ∧ (∀r∈ls_α δ - it. hm_α res r = Some ((card (set (rhsq r)))))" 
      in ls.iterate_rule_P)
      ― ‹Invar›
    apply simp
      ― ‹Init›
    apply (auto simp add: hm_correct) [1]
      ― ‹Step›
    apply (rule conjI)
      apply (simp add: hm.update_correct)

      apply (simp only: hm_correct hs_correct INV)
      apply (rule ballI)
      apply (case_tac "r=x")
      apply (auto 
        simp add: length_remdups_card 
        intro!: arg_cong[where f=card]) [1]
      apply simp
      ― ‹Final›
    apply simp
    done
  from G show ?T2 by auto
  fix r
  assume "r∈ls_α δ"
  thus "?T1 r" using G by auto
qed

lemma brc_inner_step_br'_desc: 
  "⟦ (Q,W,rcm)∈brc_invar δ ⟧ ⟹ brc_α (brc_inner_step r (Q,W,rcm)) = (
    if the (hm_α rcm r) ≤ 1 then 
      insert (lhs r) (hs_α Q) 
    else hs_α Q, 
    if the (hm_α rcm r) ≤ 1 ∧ (lhs r) ∉ hs_α Q then 
      insert (lhs r) (set W) 
    else (set W), 
    ((hm_α rcm)(r ↦ the (hm_α rcm r) - 1))
  )"
  by (simp 
    add: brc_invar_def brc_invar_add_def brc_α_def brc_inner_step_def Let_def 
         hs_correct hm_correct)

lemma brc_step_invar:
  assumes RQRM: "rqrm_invar rqrm"
  shows "⟦ Σ∈brc_invar_add; brc_α Σ∈br'_invar δ; brc_cond Σ ⟧ 
         ⟹ (brc_step rqrm Σ)∈brc_invar_add"
  apply (cases Σ)
  apply (simp add: brc_step_def)
  apply (rule_tac I="λit (Q,W,rcm). (Q,W,rcm)∈brc_invar_add ∧ set W ⊆ hs_α Q" 
                  in ls.iterate_rule_P)
  apply (simp add: RQRM[unfolded rqrm_invar_def])
  apply (case_tac b)
  apply (simp add: brc_invar_add_def distinct_tl brc_cond_def)
  apply (auto simp add: brc_invar_add_def distinct_tl brc_cond_def 
              dest!: brc_inv_imp_WssQ) [1]
  apply (case_tac σ)
  apply (auto simp add: brc_invar_add_def br_invar_def brc_inner_step_def 
                        Let_def hs_correct hm_correct) [1]
  apply (case_tac σ)
  apply simp
  done


lemma brc_step_abs:
  assumes RQRM: "rqrm_invar rqrm" "rqrm_prop δ rqrm"
  assumes A: "Σ∈brc_invar δ" "brc_cond Σ"  
  shows "(brc_α Σ, brc_α (brc_step rqrm Σ)) ∈ br'_step δ"
proof -
  obtain Q W rcm where [simp]: "Σ=(Q,W,rcm)" by (cases Σ) auto
  from A show ?thesis
    apply (simp add: brc_step_def)
    apply (rule 
      br'_inner_step_proof[OF ls.v1_iteratei_impl, 
         where cinvar="λit (Q,W,rcm). (Q,W,rcm)∈brc_invar_add 
                                      ∧ set W ⊆ hs_α Q" and 
               q="hd W"])
    apply (case_tac W) 
    apply (auto simp add: brc_cond_def brc_invar_add_def brc_invar_def 
                dest!: brc_inv_imp_WssQ) [2]
    prefer 6
    apply (simp add: brc_α_def)
    apply (case_tac Σ)
    apply (auto 
      simp add: brc_invar_def brc_invar_add_def brc_inner_step_def 
                Let_def hm_correct hs_correct) [1]
    apply (auto 
      simp add: brc_invar_add_def brc_inner_step_def brc_α_def 
                br'_inner_step_def Let_def hm_correct hs_correct) [1]
    apply (simp add: RQRM[unfolded rqrm_invar_def])
    apply (simp add: rqrm_propD[OF RQRM(2)])
    apply (case_tac W)
    apply (simp_all add: brc_α_def brc_cond_def brc_invar_def) [2]
    apply (case_tac W)
    apply (simp_all add: brc_α_def brc_cond_def brc_invar_def 
                         brc_invar_add_def) [2]
    done
qed
    
lemma brc_initial_invar: "ls_invar δ ⟹ (brc_initial δ)∈brc_invar_add"
  by (simp 
    add: brc_invar_add_def brc_initial_def brc_iq_correct Let_def 
         brc_rcm_init_correct hs_correct)

lemma brc_cond_abs: "brc_cond Σ ⟷ (brc_α Σ)∈br'_cond"
  apply (cases Σ)
  apply (simp add: brc_cond_def br'_cond_def brc_α_def)
  done

lemma brc_initial_abs: 
  "ls_invar δ ⟹ brc_α (brc_initial δ) ∈ br'_initial (ls_α δ)"
  by (auto 
    simp add: brc_initial_def Let_def brc_α_def brc_iq_correct 
              brc_rcm_init_correct hs_correct 
    intro: br'_initial.intros)

lemma brc_pref_br':
  assumes RQRM[simp]: "rqrm_invar rqrm" "rqrm_prop (ls_α δ) rqrm"
  assumes INV[simp]: "ls_invar δ"
  shows "wa_precise_refine (det_wa_wa (brc_det_algo rqrm δ)) 
                           (br'_algo (ls_α δ)) 
                           brc_α"
  apply (unfold_locales)
  apply (simp_all add: brc_det_algo_def br'_algo_def det_wa_wa_def)
  apply (simp add: brc_cond_abs)
  apply (auto simp add: brc_step_abs[OF RQRM]) [1]
  apply (simp add: brc_initial_abs)
  apply (auto simp add: brc_invar_def) [1]
  apply (simp add: brc_cond_abs)
  done

lemma brc_while_algo:
  assumes RQRM[simp]: "rqrm_invar rqrm" "rqrm_prop (ls_α δ) rqrm"
  assumes INV[simp]: "ls_invar δ"
  shows "while_algo (det_wa_wa (brc_det_algo rqrm δ))"
proof -
  from brc_pref_br'[OF RQRM INV] interpret 
    ref: wa_precise_refine "(det_wa_wa (brc_det_algo rqrm δ))" 
                           "(br'_algo (ls_α δ))" 
                           brc_α .
  show ?thesis
    apply (rule ref.wa_intro)
    apply (simp add: br'_while_algo)
    apply (simp_all add: det_wa_wa_def brc_det_algo_def br'_algo_def)
    apply (simp add: brc_invar_def)
    apply (auto simp add: brc_step_invar) [1]
    apply (simp add: brc_initial_invar)
    done
qed

lemmas brc_det_while_algo =
  det_while_algo_intro[OF brc_while_algo]


lemma fst_brc_α: "fst (brc_α s) = hs_α (fst s)" 
  by (cases s) (simp add: brc_α_def)

lemmas brc_invar_final =
  wa_precise_refine.transfer_correctness[OF 
    brc_pref_br' br'_invar_final, unfolded fst_brc_α]

definition "hta_bwd_reduce H == 
  let rqrm = build_rqrm (hta_δ H) in 
    hta_reduce 
      H 
      (fst (while brc_cond (brc_step rqrm) (brc_initial (hta_δ H))))
"

theorem (in hashedTa) hta_bwd_reduce_correct:
  shows "hta_α (hta_bwd_reduce H) 
         = ta_reduce (hta_α H) (b_accessible (ls_α (hta_δ H)))" (is ?T1)
        "hashedTa (hta_bwd_reduce H)" (is ?T2)
proof -
  interpret det_while_algo "(brc_det_algo (build_rqrm δ) δ)"
    by (rule brc_det_while_algo)
       (simp_all add: build_rqrm_correct)

  have LC: "(while brc_cond (brc_step (build_rqrm δ)) (brc_initial δ)) = loop"
    by (unfold loop_def)
       (simp add: brc_det_algo_def)

  from while_proof'[OF brc_invar_final] have 
    G1: "hs_α (fst loop) = b_accessible (ls_α δ)" 
    by (simp add: build_rqrm_correct)
  have G2: "loop ∈ brc_invar (ls_α δ)"
    by (rule while_proof)
       (simp add: brc_det_algo_def)
  hence [simp]: "hs_invar (fst loop)"
    by (cases loop)
       (simp add: brc_invar_def brc_invar_add_def)

  show ?T1 ?T2
    by (simp_all add: hta_bwd_reduce_def LC hta_reduce_correct G1)
    
qed

subsubsection ‹Emptiness Check with Witness Computation›

definition brec_construct_witness 
  :: "('q::hashable,'l::hashable tree) hm ⇒ ('q,'l) ta_rule ⇒ 'l tree"
  where "brec_construct_witness Qm r == 
  NODE (rhsl r) (List.map (λq. the (hm_lookup q Qm)) (rhsq r))"

lemma brec_construct_witness_correct: 
  "⟦hm_invar Qm⟧ ⟹ 
    brec_construct_witness Qm r = construct_witness (hm_α Qm) r"
  by (auto 
    simp add: construct_witness_def brec_construct_witness_def hm_correct)

type_synonym ('Q,'L) brec_state 
  = "(('Q,'L tree) hm 
      × 'Q fifo 
      × (('Q,'L) ta_rule, nat) hm 
      × 'Q option)"


  ― ‹Abstractions›
definition brec_α 
  :: "('Q::hashable,'L::hashable) brec_state ⇒ ('Q,'L) brw_state"
  where "brec_α == λ(Q,W,rcm,f). (hm_α Q, set (fifo_α W), (hm_α rcm))"

definition brec_inner_step 
  :: "'q hs ⇒ ('q,'l) ta_rule 
      ⇒ ('q::hashable,'l::hashable) brec_state 
      ⇒ ('q,'l) brec_state"
  where "brec_inner_step Qi r == λ(Q,W,rcm,qwit). 
    let c=the (hm_lookup r rcm); 
        cond = c ≤ 1 ∧ hm_lookup (lhs r) Q = None;
        rcm' = hm_update r (c-(1::nat)) rcm;
        Q' = ( if cond then 
                 hm_update (lhs r) (brec_construct_witness Q r) Q 
               else Q);
        W' = (if cond then fifo_enqueue (lhs r) W else W);
        qwit' = (if c ≤ 1 ∧ hs_memb (lhs r) Qi then Some (lhs r) else qwit)
    in
      (Q',W',rcm',qwit')"

definition brec_step 
  :: "('q,('q,'l) ta_rule ls) hm ⇒ 'q hs 
      ⇒ ('q::hashable,'l::hashable) brec_state 
      ⇒ ('q,'l) brec_state" 
  where "brec_step rqrm Qi == λ(Q,W,rcm,qwit).
    let (q,W')=fifo_dequeue W in 
      ls_iteratei (rqrm_lookup rqrm q) (λ_. True) 
        (brec_inner_step Qi) (Q,W',rcm,qwit)
  "

definition brec_iqm 
  :: "('q::hashable,'l::hashable) ta_rule ls ⇒ ('q,'l tree) hm" 
  where "brec_iqm δ == 
    ls_iteratei δ (λ_. True) (λr m. if rhsq r = [] then 
                         hm_update (lhs r) (NODE (rhsl r) []) m 
                      else m) 
                (hm_empty ())"

definition brec_initial 
  :: "'q hs ⇒ ('q::hashable,'l::hashable) ta_rule ls 
      ⇒ ('q,'l) brec_state" 
  where "brec_initial Qi δ == 
  let iq=brc_iq δ in 
    ( brec_iqm δ, 
      hs_to_fifo.g_set_to_listr iq, 
      brc_rcm_init δ,
      hh_set_xx.g_disjoint_witness iq Qi)"

definition brec_cond 
  :: "('q,'l) brec_state ⇒ bool" 
  where "brec_cond == λ(Q,W,rcm,qwit). ¬ fifo_isEmpty W ∧ qwit = None"

definition brec_invar_add
  :: "'Q set ⇒ ('Q::hashable,'L::hashable) brec_state set" 
  where
  "brec_invar_add Qi == {(Q,W,rcm,qwit). 
    hm_invar Q ∧ 
    distinct (fifo_α W) ∧ 
    hm_invar rcm ∧
    ( case qwit of 
        None ⇒ Qi ∩ dom (hm_α Q) = {} | 
        Some q ⇒ q∈Qi ∩ dom (hm_α Q))}
  "

definition "brec_invar Qi δ == brec_invar_add Qi ∩ {s. brec_α s ∈ brw_invar δ}"

definition "brec_invar_inner Qi == 
  brec_invar_add Qi ∩ {(Q,W,_,_). set (fifo_α W) ⊆ dom (hm_α Q)}"

lemma brec_invar_cons: 
  "Σ∈brec_invar Qi δ ⟹ Σ∈brec_invar_inner Qi"
  apply (cases Σ)
  apply (simp add: brec_invar_def brw_invar_def br'_invar_def br_invar_def
                   brec_α_def brw_α_def br'_α_def brec_invar_inner_def)
  done

lemma brec_brw_invar_cons: 
  "brec_α Σ ∈ brw_invar Qi ⟹ set (fifo_α (fst (snd Σ))) ⊆ dom (hm_α (fst Σ))"
  apply (cases Σ)
  apply (simp add: brec_invar_def brw_invar_def br'_invar_def br_invar_def
                   brec_α_def brw_α_def br'_α_def)
  done

definition "brec_det_algo rqrm Qi δ == ⦇
  dwa_cond=brec_cond,
  dwa_step=brec_step rqrm Qi,
  dwa_initial=brec_initial Qi δ,
  dwa_invar=brec_invar (hs_α Qi) (ls_α δ)
⦈"

lemma brec_iqm_correct':
  assumes INV[simp]: "ls_invar δ"
  shows 
    "dom (hm_α (brec_iqm δ)) = {lhs r | r. r∈ls_α δ ∧ rhsq r = []}" (is ?T1)
    "witness_prop (ls_α δ) (hm_α (brec_iqm δ))" (is ?T2)
    "hm_invar (brec_iqm δ)" (is ?T3)
proof -
  have "?T1 ∧ ?T2 ∧ ?T3"
    apply (unfold brec_iqm_def)
    apply (rule_tac 
      I="λit m. hm_invar m 
                ∧ dom (hm_α m) = {lhs r | r. r∈ls_α δ - it ∧ rhsq r = []} 
                ∧ witness_prop (ls_α δ) (hm_α m)" 
      in ls.iterate_rule_P)
    apply simp
    apply (auto simp add: hm_correct witness_prop_def) [1]
    apply (auto simp add: hm_correct witness_prop_def) [1]
    apply (case_tac x)
    apply (auto intro: accs.intros) [1]
    apply simp
    done
  thus ?T1 ?T2 ?T3 by auto
qed

lemma brec_iqm_correct:
  assumes INV[simp]: "ls_invar δ"
  shows "hm_α (brec_iqm δ) ∈ brw_iq (ls_α δ)"
proof -
  have "(∀q t. hm_α (brec_iqm δ) q = Some t 
          ⟶ (∃r∈ls_α δ. rhsq r = [] ∧ q = lhs r ∧ t = NODE (rhsl r) [])) 
        ∧ (∀r∈ls_α δ. rhsq r = [] ⟶ hm_α (brec_iqm δ) (lhs r) ≠ None)" 
    apply (unfold brec_iqm_def)
    apply (rule_tac I="λit m. (
      (hm_invar m) ∧ 
      (∀q t. hm_α m q = Some t 
        ⟶ (∃r∈ls_α δ. rhsq r = [] ∧ q = lhs r ∧ t = NODE (rhsl r) [])) ∧ 
      (∀r∈ls_α δ-it. rhsq r = [] ⟶ hm_α m (lhs r) ≠ None)
      )" 
      in ls.iterate_rule_P)
    apply simp
    apply (simp add: hm_correct)
    apply (auto simp add: hm_correct) [1]
    apply (auto simp add: hm_correct) [1]
    done
  thus ?thesis by (blast intro: brw_iq.intros)
qed

lemma brec_inner_step_brw_desc: 
  "⟦ Σ∈brec_invar_inner (hs_α Qi) ⟧ 
    ⟹ (brec_α Σ, brec_α (brec_inner_step Qi r Σ)) ∈ brw_inner_step r"
  apply (cases Σ)
  apply (rule brw_inner_step.intros)
  apply (simp only: )
  apply (simp only: brec_α_def split_conv)
  apply (simp only: brec_inner_step_def brec_α_def Let_def split_conv)
  apply (auto 
    simp add: brec_invar_inner_def brec_invar_add_def brec_α_def 
              brec_inner_step_def 
              Let_def hs_correct hm_correct fifo_correct
              brec_construct_witness_correct)
  done


lemma brec_step_invar:
  assumes RQRM: "rqrm_invar rqrm" "rqrm_prop δ rqrm"
  assumes [simp]: "hs_invar Qi"
  shows "⟦ Σ∈brec_invar_add (hs_α Qi); brec_α Σ ∈ brw_invar δ;  brec_cond Σ ⟧ 
          ⟹ (brec_step rqrm Qi Σ)∈brec_invar_add (hs_α Qi)"
  apply (frule brec_brw_invar_cons)
  apply (cases Σ)
  apply (simp add: brec_step_def fifo_correct)
  apply (case_tac "fifo_α b")
  apply (simp 
    add: brec_invar_def distinct_tl brec_cond_def fifo_correct
         )
  apply (rule_tac s=b in fifo.removelE)
  apply simp
  apply simp
  apply simp

  apply (rule_tac 
    I="λit (Q,W,rcm,qwit). (Q,W,rcm,qwit)∈brec_invar_add (hs_α Qi) 
                           ∧ set (fifo_α W) ⊆ dom (hm_α Q)" 
    in ls.iterate_rule_P)
  apply simp
  apply (simp 
    add: brec_invar_def distinct_tl brec_cond_def fifo_correct
         )
  apply (simp 
    add: brec_invar_def brec_invar_add_def distinct_tl brec_cond_def 
         fifo_correct)
  apply (case_tac σ)
  apply (auto 
    simp add: brec_invar_add_def brec_inner_step_def Let_def hs_correct 
              hm_correct fifo_correct split: option.split_asm) [1]
  apply (case_tac σ)
  apply simp
  done

lemma brec_step_abs:
  assumes RQRM: "rqrm_invar rqrm" "rqrm_prop δ rqrm"
  assumes INV[simp]: "hs_invar Qi"
  assumes A': "Σ∈brec_invar (hs_α Qi) δ"
  assumes COND: "brec_cond Σ"
  shows "(brec_α Σ, brec_α (brec_step rqrm Qi Σ)) ∈ brw_step δ"
proof -
  from A' have A: "(brec_α Σ)∈brw_invar δ" "Σ∈brec_invar_add (hs_α Qi)"
    by (simp_all add: brec_invar_def)

  obtain Q W rcm qwit where [simp]: "Σ=(Q,W,rcm,qwit)" by (cases Σ) blast
  from A COND show ?thesis
    apply (simp add: brec_step_def fifo_correct)
    apply (case_tac "fifo_α W")
    apply (simp 
      add: brec_invar_def distinct_tl brec_cond_def fifo_correct
    )
    apply (rule_tac s=W in fifo.removelE)
    apply simp
    apply simp
    apply simp

    apply (rule brw_inner_step_proof[
      OF ls.v1_iteratei_impl, 
      where cinvar="λit Σ. Σ∈brec_invar_inner (hs_α Qi)" and 
            q="hd (fifo_α W)"])
    apply assumption
    apply (frule brec_brw_invar_cons)
    apply (simp_all 
      add: brec_cond_def brec_invar_add_def fifo_correct
            brec_invar_inner_def) [1]
    prefer 6
    apply (simp add: brec_α_def)
    apply (case_tac Σ)
    apply (auto 
      simp add: brec_invar_add_def brec_inner_step_def Let_def hm_correct 
                hs_correct fifo_correct brec_invar_inner_def 
      split: option.split_asm) [1]
    apply (blast intro: brec_inner_step_brw_desc)
    apply (simp add: RQRM[unfolded rqrm_invar_def])
    apply (simp 
      add: rqrm_propD[OF RQRM(2)] fifo_correct)
    apply (simp_all 
      add: brec_α_def brec_cond_def brec_invar_def fifo_correct) [1]
    apply (simp_all 
      add: brec_α_def brec_cond_def brec_invar_add_def fifo_correct) [1]
    done
qed
    
lemma brec_invar_initial: 
  "⟦ls_invar δ; hs_invar Qi⟧ ⟹ (brec_initial Qi δ) ∈ brec_invar_add (hs_α Qi)"
  apply (auto 
    simp add: brec_invar_add_def brec_initial_def brc_iq_correct 
              brec_iqm_correct' hs_correct hs.isEmpty_correct Let_def 
              brc_rcm_init_correct br_iq_def 
              hh_set_xx.disjoint_witness_correct 
              hs_to_fifo.g_set_to_listr_correct 
    split: option.split)
  apply (auto simp add: brc_iq_correct 
    hh_set_xx.disjoint_witness_None br_iq_def) [1]

  apply (drule hh_set_xx.disjoint_witness_correct[simplified])
  apply simp

  apply (drule hh_set_xx.disjoint_witness_correct[simplified])
  apply (simp add: brc_iq_correct br_iq_def)
  done

lemma brec_cond_abs: 
  "⟦Σ∈brec_invar Qi δ⟧ ⟹ brec_cond Σ ⟷ (brec_α Σ)∈brw_cond Qi"
  apply (cases Σ)
  apply (auto 
    simp add: brec_cond_def brw_cond_def brec_α_def brec_invar_def 
              brec_invar_add_def fifo_correct
    split: option.split_asm)
  done

lemma brec_initial_abs: 
  "⟦ ls_invar δ; hs_invar Qi ⟧ 
     ⟹ brec_α (brec_initial Qi δ) ∈ brw_initial (ls_α δ)"
  by (auto simp add: brec_initial_def Let_def brec_α_def 
                     brc_iq_correct brc_rcm_init_correct brec_iqm_correct 
                     br_iq_def fifo_correct hs_to_fifo.g_set_to_listr_correct 
              intro: brw_initial.intros[unfolded br_iq_def])

lemma brec_pref_brw:
  assumes RQRM[simp]: "rqrm_invar rqrm" "rqrm_prop (ls_α δ) rqrm"
  assumes INV[simp]: "ls_invar δ" "hs_invar Qi"
  shows "wa_precise_refine (det_wa_wa (brec_det_algo rqrm Qi δ)) 
                           (brw_algo (hs_α Qi) (ls_α δ))  
                           brec_α"
  apply (unfold_locales)
  apply (simp_all add: det_wa_wa_def brec_det_algo_def brw_algo_def)
  apply (auto simp add: brec_cond_abs brec_step_abs brec_initial_abs)
  apply (simp add: brec_invar_def)
  done

lemma brec_while_algo:
  assumes RQRM[simp]: "rqrm_invar rqrm" "rqrm_prop (ls_α δ) rqrm"
  assumes INV[simp]: "ls_invar δ" "hs_invar Qi"
  shows "while_algo (det_wa_wa (brec_det_algo rqrm Qi δ))"
proof -
  interpret ref: 
    wa_precise_refine "(det_wa_wa (brec_det_algo rqrm Qi δ))" 
                      "(brw_algo (hs_α Qi) (ls_α δ))" 
                      "brec_α" 
    using brec_pref_brw[OF RQRM INV] . 

  show ?thesis
    apply (rule ref.wa_intro)
    apply (simp add: brw_while_algo)
    apply (simp_all add: det_wa_wa_def brec_det_algo_def brw_algo_def)
    apply (simp add: brec_invar_def)
    apply (auto simp add: brec_step_invar[OF RQRM INV(2)]) [1]
    apply (simp add: brec_invar_initial) [1]
    done
qed

lemma fst_brec_α: "fst (brec_α Σ) = hm_α (fst Σ)"
  by (cases Σ) (simp add: brec_α_def)

lemmas brec_invar_final = 
  wa_precise_refine.transfer_correctness[
    OF brec_pref_brw brw_invar_final, 
    unfolded fst_brec_α]

lemmas brec_det_algo = det_while_algo_intro[OF brec_while_algo]

definition "hta_is_empty_witness H == 
  let rqrm = build_rqrm (hta_δ H);
      (Q,_,_,qwit) = (while brec_cond (brec_step rqrm (hta_Qi H)) 
                            (brec_initial (hta_Qi H) (hta_δ H))) 
  in
    case qwit of 
      None ⇒ None |
      Some q ⇒ (hm_lookup q Q)
"

theorem (in hashedTa) hta_is_empty_witness_correct:
  shows [rule_format]: "hta_is_empty_witness H = Some t 
                        ⟶ t∈ta_lang (hta_α H)" (is ?T1)
        "hta_is_empty_witness H = None ⟶ ta_lang (hta_α H) = {}" (is ?T2)
proof -

  interpret det_while_algo "(brec_det_algo (build_rqrm δ) Qi δ)"
    by (rule brec_det_algo)
       (simp_all add: build_rqrm_correct)

  have LC: 
    "(while brec_cond (brec_step (build_rqrm δ) Qi) (brec_initial Qi δ)) = loop"
    by (unfold loop_def)
       (simp add: brec_det_algo_def)

  from while_proof'[OF brec_invar_final] have X:
    "hs_α Qi ∩ dom (hm_α (fst loop)) = {} 
     ⟷ (hs_α Qi ∩ b_accessible (ls_α δ) = {})"
    "witness_prop (ls_α δ) (hm_α (fst loop))"
    by (simp_all add: build_rqrm_correct)

  obtain Q W rcm qwit where 
    [simp]: "loop = (Q,W,rcm,qwit)" 
    by (case_tac "loop") blast

  from loop_invar have I: "loop ∈ brec_invar (hs_α Qi) (ls_α δ)" 
    by (simp add: brec_det_algo_def)
  hence INVARS[simp]: "hm_invar Q" "hm_invar rcm" 
    by (simp_all add: brec_invar_def brec_invar_add_def) 
  
  {
    assume C: "hta_is_empty_witness H = Some t"
    then obtain q where 
      [simp]: "qwit=Some q" and 
        LUQ: "hm_lookup q Q = Some t"
      by (unfold hta_is_empty_witness_def)
         (simp add: LC split: option.split_asm)
    from LUQ have QqF: "hm_α Q q = Some t" by (simp add: hm_correct)
    from I have QMEM: "q∈hs_α Qi" 
      by (simp_all add: brec_invar_def brec_invar_add_def)
    moreover from witness_propD[OF X(2)] QqF have "accs (ls_α δ) t q" by simp
    ultimately have "t∈ta_lang (hta_α H)"
      by (auto simp add: ta_lang_def hta_α_def)
  } moreover {
    assume C: "hta_is_empty_witness H = None"
    hence DJ: "hs_α Qi ∩ dom (hm_α Q) = {}" using I
      by (auto simp add: hta_is_empty_witness_def LC brec_invar_def 
                         brec_invar_add_def hm_correct 
               split: option.split_asm)
    with X have "hs_α Qi ∩ b_accessible (ls_α δ) = {}" 
      by (simp add: brec_α_def)
    with empty_if_no_b_accessible[of "hta_α H"] have "ta_lang (hta_α H) = {}"
      by (simp add: hta_α_def)
  } ultimately show ?T1 ?T2 by auto
qed

subsection ‹Interface for Natural Number States and Symbols›
  text_raw ‹\label{sec:htai_intf}›
text ‹
  The library-interface is statically instantiated to use natural numbers 
  as both, states and symbols.

  This interface is easier to use from ML and OCaml, because there is no 
  overhead with typeclass emulation.
›

type_synonym htai = "(nat,nat) hashedTa"

definition htai_mem :: "_ ⇒ htai ⇒ bool" 
  where "htai_mem == hta_mem"
definition htai_prod :: "htai ⇒ htai ⇒ htai" 
  where "htai_prod H1 H2 == hta_reindex (hta_prod H1 H2)"
definition htai_prodWR :: "htai ⇒ htai ⇒ htai" 
  where "htai_prodWR H1 H2 == hta_reindex (hta_prodWR H1 H2)"
definition htai_union :: "htai ⇒ htai ⇒ htai" 
  where "htai_union H1 H2 == hta_reindex (hta_union H1 H2)"
definition htai_empty :: "unit ⇒ htai"
  where "htai_empty == hta_empty"
definition htai_add_qi :: "_ ⇒ htai ⇒ htai" 
  where "htai_add_qi == hta_add_qi"
definition htai_add_rule :: "_ ⇒ htai ⇒ htai" 
  where "htai_add_rule == hta_add_rule"
definition htai_bwd_reduce :: "htai ⇒ htai" 
  where "htai_bwd_reduce == hta_bwd_reduce"
definition htai_is_empty_witness :: "htai ⇒ _" 
  where "htai_is_empty_witness == hta_is_empty_witness"
definition htai_ensure_idx_f :: "htai ⇒ htai" 
  where "htai_ensure_idx_f == hta_ensure_idx_f"
definition htai_ensure_idx_s :: "htai ⇒ htai" 
  where "htai_ensure_idx_s == hta_ensure_idx_s"
definition htai_ensure_idx_sf :: "htai ⇒ htai" 
  where "htai_ensure_idx_sf == hta_ensure_idx_sf"

definition htaip_prod :: "htai ⇒ htai ⇒ (nat * nat,nat) hashedTa" 
  where "htaip_prod == hta_prod"
definition htaip_prodWR :: "htai ⇒ htai ⇒ (nat * nat,nat) hashedTa" 
  where "htaip_prodWR == hta_prodWR"
definition htaip_reindex :: "(nat * nat,nat) hashedTa ⇒ htai" 
  where "htaip_reindex == hta_reindex"

locale htai = hashedTa +
  constrains H :: htai
begin
  lemmas htai_mem_correct = hta_mem_correct[folded htai_mem_def]

  lemma htai_empty_correct[simp]:
    "hta_α (htai_empty ()) = ta_empty"
    "hashedTa (htai_empty ())"
  by (auto simp add: htai_empty_def hta_empty_correct)

  lemmas htai_add_qi_correct = hta_add_qi_correct[folded htai_add_qi_def]
  lemmas htai_add_rule_correct = hta_add_rule_correct[folded htai_add_rule_def]

  lemmas htai_bwd_reduce_correct = 
    hta_bwd_reduce_correct[folded htai_bwd_reduce_def]
  lemmas htai_is_empty_witness_correct = 
    hta_is_empty_witness_correct[folded htai_is_empty_witness_def]

  lemmas htai_ensure_idx_f_correct = 
    hta_ensure_idx_f_correct[folded htai_ensure_idx_f_def]
  lemmas htai_ensure_idx_s_correct = 
    hta_ensure_idx_s_correct[folded htai_ensure_idx_s_def]
  lemmas htai_ensure_idx_sf_correct = 
    hta_ensure_idx_sf_correct[folded htai_ensure_idx_sf_def]

end

lemma htai_prod_correct:
  assumes [simp]: "hashedTa H1" "hashedTa H2"
  shows 
  "ta_lang (hta_α (htai_prod H1 H2)) = ta_lang (hta_α H1) ∩ ta_lang (hta_α H2)"
  "hashedTa (htai_prod H1 H2)"
  apply (unfold htai_prod_def)
  apply (auto simp add: hta_prod_correct hashedTa.hta_reindex_correct)
  done

lemma htai_prodWR_correct:
  assumes [simp]: "hashedTa H1" "hashedTa H2"
  shows 
  "ta_lang (hta_α (htai_prodWR H1 H2)) 
   = ta_lang (hta_α H1) ∩ ta_lang (hta_α H2)"
  "hashedTa (htai_prodWR H1 H2)"
  apply (unfold htai_prodWR_def)
  apply (auto simp add: hta_prodWR_correct hashedTa.hta_reindex_correct)
  done

lemma htai_union_correct:
  assumes [simp]: "hashedTa H1" "hashedTa H2"
  shows 
  "ta_lang (hta_α (htai_union H1 H2)) 
   = ta_lang (hta_α H1) ∪ ta_lang (hta_α H2)"
  "hashedTa (htai_union H1 H2)"
  apply (unfold htai_union_def)
  apply (auto simp add: hta_union_correct hashedTa.hta_reindex_correct)
  done

subsection ‹Interface Documentation› text_raw‹\label{sec:intf_doc}›
text ‹
  This section contains a documentation of the executable tree-automata
  interface. The documentation contains a description of each function along
  with the relevant correctness lemmas.
›

text ‹
  ML/OCaml users should note, that there is an interface that has the fixed type
  Int for both states and function symbols. This interface is simpler to use
  from ML/OCaml than the generic one, as it requires no overhead to emulate
  Isabelle/HOL type-classes.

  The functions of this interface start with the prefix {\em htai} instead of
  {\em hta}, but have the same semantics otherwise 
  (cf Section~\ref{sec:htai_intf}).
›

subsubsection ‹Building a Tree Automaton›
text_raw ‹
  \newcommand{\fundesc}[2]{{\bf Function: #1}\\#2}

›

text ‹
  \fundesc{@{const [show_types] hta_empty}}{
    Returns a tree automaton with no states and no rules. 
  }
  
  \paragraph{Relevant Lemmas}
  \begin{description}
    \item[@{thm [source] hta_empty_correct}:] @{thm hta_empty_correct[no_vars]}
    \item[@{thm [source] ta_empty_lang}:] @{thm ta_empty_lang[no_vars]}
  \end{description}
›

text ‹
  \fundesc{@{const [show_types] hta_add_qi}}{
    Adds an initial state to the given automaton.
  }
  \paragraph{Relevant Lemmas}
  \begin{description}
    \item[@{thm [source] hashedTa.hta_add_qi_correct}]
      @{thm hashedTa.hta_add_qi_correct[no_vars]}
  \end{description}
›

text ‹
  \fundesc{@{const [show_types] hta_add_rule}}{
    Adds a rule to the given automaton.
  }
  \paragraph{Relevant Lemmas}
  \begin{description}
    \item[@{thm [source] hashedTa.hta_add_rule_correct}:]
      @{thm hashedTa.hta_add_rule_correct[no_vars]}
  \end{description}
›

subsubsection ‹Basic Operations›

text ‹
  The tree automata of this library may have some optional indices, that 
  accelerate computation. The tree-automata operations will compute the 
  indices if necessary, but due to the pure nature of the Isabelle-language,
  the computed index cannot be stored for the next usage. Hence, before using a
  bulk of tree-automaton operations on the same tree-automata, the relevant 
  indexes should be pre-computed.
›

text ‹
  \fundesc{
    @{const [show_types] hta_ensure_idx_f}\\
    @{const [show_types] hta_ensure_idx_s}\\
    @{const [show_types] hta_ensure_idx_sf}
  }{
    Computes an index for a tree automaton, if it is not yet present.
  }
›

text ‹
  \fundesc{@{const [show_types] hta_mem}, @{const [show_types] hta_mem'}}{
    Check whether a tree is accepted by the tree automaton.
  }
  \paragraph{Relevant Lemmas}
  \begin{description}
    \item[@{thm [source] hashedTa.hta_mem_correct}:]
      @{thm hashedTa.hta_mem_correct[no_vars]}
    \item[@{thm [source] hashedTa.hta_mem'_correct}:]
      @{thm hashedTa.hta_mem'_correct[no_vars]}
  \end{description}
›

text ‹
  \fundesc{@{const [show_types] hta_prod}, @{const [show_types] hta_prod'}}{
    Compute the product automaton. The computed automaton is in 
    forward-reduced form. 
    The language of the product automaton is the intersection of 
    the languages of the two argument automata.
  }
  \paragraph{Relevant Lemmas}
  \begin{description}
    \item[@{thm [source] hta_prod_correct_aux}:] 
      @{thm hta_prod_correct_aux[no_vars]}
    \item[@{thm [source] hta_prod_correct}:] 
      @{thm hta_prod_correct[no_vars]}
    \item[@{thm [source] hta_prod'_correct_aux}:] 
      @{thm hta_prod'_correct_aux[no_vars]}
    \item[@{thm [source] hta_prod'_correct}:] 
      @{thm hta_prod'_correct[no_vars]}
  \end{description}
›

text ‹
  \fundesc{@{const [show_types] hta_prodWR}}{
    Compute the product automaton by brute-force algorithm. 
    The resulting automaton is not reduced.
    The language of the product automaton is the intersection of 
    the languages of the two argument automata.
  }
  \paragraph{Relevant Lemmas}
  \begin{description}
  \item[@{thm [source] hta_prodWR_correct_aux}:]
    @{thm hta_prodWR_correct_aux[no_vars]}
  \item[@{thm [source] hta_prodWR_correct}:] 
    @{thm hta_prodWR_correct[no_vars]}
  \end{description}
›

text ‹
  \fundesc{@{const [show_types] hta_union}}{
    Compute the union of two tree automata.
  }
  \paragraph{Relevant Lemmas}
  \begin{description}
  \item[@{thm [source] hta_union_correct'}:] @{thm hta_union_correct'[no_vars]}
  \item[@{thm [source] hta_union_correct}:] @{thm hta_union_correct[no_vars]}
  \end{description}
›

text ‹
  \fundesc{@{const [show_types] hta_reduce}}{
    Reduce the automaton to the given set of states. All initial states outside
    this set will be removed. Moreover, all rules that contain states outside 
    this set are removed, too.
  }
  \paragraph{Relevant Lemmas}
  \begin{description}
    \item[@{thm [source] hashedTa.hta_reduce_correct}:]
      @{thm hashedTa.hta_reduce_correct[no_vars]}
  \end{description}
›

text ‹
  \fundesc{@{const [show_types] hta_bwd_reduce}}{
    Compute the backwards-reduced version of a tree automata.
    States from that no tree can be produced are removed. 
    Backwards reduction does not change the language of the automaton.
  }
  \paragraph{Relevant Lemmas}
  \begin{description}
    \item[@{thm [source] hashedTa.hta_bwd_reduce_correct}:]
      @{thm hashedTa.hta_bwd_reduce_correct[no_vars]}
    \item[@{thm [source] ta_reduce_b_acc}:] @{thm ta_reduce_b_acc[no_vars]}
  \end{description}
›

text ‹
  \fundesc{@{const [show_types] hta_is_empty_witness}}{
    Check whether the language of the automaton is empty.
    If the language is not empty, a tree of the language is returned.

    The following property is not (yet) formally proven, but should hold: 
    If a tree is returned, the language contains no tree with a smaller depth
    than the returned one.
  }
  \paragraph{Relevant Lemmas}
  \begin{description}
    \item[@{thm [source] hashedTa.hta_is_empty_witness_correct}:]
       @{thm hashedTa.hta_is_empty_witness_correct[no_vars]}
  \end{description}
›

subsection ‹Code Generation›

(* TODO/FIXME: There seems to be no way to reference the project-directory,
  in order to control the placement of the generated code files.
  The code-generation in this file only dumps the generated code to standard output.
  Hence it is safe to include this file from other projects.

  Actual code generation is done in Ta_impl_codegen.thy
  *)

export_code 
  hta_mem hta_mem' hta_prod hta_prod' hta_prodWR hta_union 
  hta_empty hta_add_qi hta_add_rule
  hta_reduce hta_bwd_reduce hta_is_empty_witness
  hta_ensure_idx_f hta_ensure_idx_s hta_ensure_idx_sf

  htai_mem htai_prod htai_prodWR htai_union 
  htai_empty htai_add_qi htai_add_rule
  htai_bwd_reduce htai_is_empty_witness
  htai_ensure_idx_f htai_ensure_idx_s htai_ensure_idx_sf

  (*ls_size hs_size rs_size*)
  in SML 
  module_name Ta


export_code 
  hta_mem hta_mem' hta_prod hta_prod' hta_prodWR hta_union 
  hta_empty hta_add_qi hta_add_rule
  hta_reduce hta_bwd_reduce hta_is_empty_witness
  hta_ensure_idx_f hta_ensure_idx_s hta_ensure_idx_sf

  htai_mem htai_prod htai_prodWR htai_union 
  htai_empty htai_add_qi htai_add_rule
  htai_bwd_reduce htai_is_empty_witness
  htai_ensure_idx_f htai_ensure_idx_s htai_ensure_idx_sf

  (*ls_size hs_size rs_size*)
  in Haskell 
  module_name Ta
  (string_classes)

export_code 
  hta_mem hta_mem' hta_prod hta_prod' hta_prodWR hta_union 
  hta_empty hta_add_qi hta_add_rule
  hta_reduce hta_bwd_reduce hta_is_empty_witness
  hta_ensure_idx_f hta_ensure_idx_s hta_ensure_idx_sf

  htai_mem htai_prod htai_prodWR htai_union 
  htai_empty htai_add_qi htai_add_rule
  htai_bwd_reduce htai_is_empty_witness
  htai_ensure_idx_f htai_ensure_idx_s htai_ensure_idx_sf

  (*ls_size hs_size rs_size*)
  in OCaml 
  module_name Ta

(* If this statement fails with an error from ML, this indicates a problem 
  with the code-generator. The most frequent problem in this context is, that
  the code generator generates code that violates the ML value-restriction.
*)

ML ‹
  @{code hta_mem};
  @{code hta_mem'};
  @{code hta_prod};
  @{code hta_prod'};
  @{code hta_prodWR};
  @{code hta_union};
  @{code hta_empty};
  @{code hta_add_qi};
  @{code hta_add_rule};
  @{code hta_reduce};
  @{code hta_bwd_reduce};
  @{code hta_is_empty_witness};
  @{code hta_ensure_idx_f};
  @{code hta_ensure_idx_s};
  @{code hta_ensure_idx_sf};
  @{code htai_mem};
  @{code htai_prod};
  @{code htai_prodWR};
  @{code htai_union};
  @{code htai_empty};
  @{code htai_add_qi};
  @{code htai_add_rule};
  @{code htai_bwd_reduce};
  @{code htai_is_empty_witness};
  @{code htai_ensure_idx_f};
  @{code htai_ensure_idx_s};
  @{code htai_ensure_idx_sf};
  (*@{code ls_size};
  @{code hs_size};
  @{code rs_size}*)
›

end