Theory AbsAlgo

(*  Title:       Tree Automata
    Author:      Peter Lammich <peter dot lammich at uni-muenster.de>
    Maintainer:  Peter Lammich <peter dot lammich at uni-muenster.de>
*)
section "Abstract Tree Automata Algorithms"
theory AbsAlgo
imports 
  Ta 
  Collections_Examples.Exploration
  Collections.CollectionsV1
begin

no_notation fun_rel_syn (infixr ‹→› 60)

text_raw ‹\label{sec:absalgo}›
text ‹This theory defines tree automata algorithms on an abstract level, 
  that is using non-executable datatypes and constructs like sets, 
  set-collecting operations, etc. 
    
  These algorithms are then refined to executable algorithms in 
  Section~\ref{sec:taimpl}.
›

subsection ‹Word Problem›
  
text ‹
  First, a recursive version of the @{const accs}-predicate is defined.
›

fun r_match :: "'a set list ⇒ 'a list ⇒ bool" where
  "r_match [] [] ⟷ True" |
  "r_match (A#AS) (a#as) ⟷ a∈A ∧ r_match AS as" |
  "r_match _ _ ⟷ False"

― ‹@{const r_match} accepts two lists, if they have the same length and 
  the elements in the second list are contained in the respective 
  elements of the first list:›
lemma r_match_alt: 
  "r_match L l ⟷ length L = length l ∧ (∀i<length l. l!i ∈ L!i)"
  apply (induct L l rule: r_match.induct)
  apply auto
  apply (case_tac i)
  apply auto
  done

― ‹Whether a rule matches the given state, label and list of sets of states›
fun r_matchc where
  "r_matchc q l Qs (qr → lr qsr) ⟷ q=qr ∧ l=lr ∧ r_match Qs qsr"

― ‹recursive version of @{const accs}-predicate›  
fun faccs :: "('Q,'L) ta_rule set ⇒ 'L tree ⇒ 'Q set" where
  "faccs δ (NODE f ts) = (
    let Qs = map (faccs δ) (ts) in
      {q. ∃r∈δ. r_matchc q f Qs r }
  )"

lemma faccs_correct_aux: 
  "q∈faccs δ n = accs δ n q" (is ?T1)
  "(map (faccs δ) ts = map (λt. { q . accs δ t q}) ts)" (is ?T2)
proof -
  have "(∀q. q∈faccs δ n = accs δ n q) 
        ∧ (map (faccs δ) ts = map (λt. { q . accs δ t q}) ts)"
  proof (induct rule: compat_tree_tree_list.induct)
    case (NODE f ts)
    thus ?case
      apply (intro allI iffI)
      apply simp
      apply (erule bexE)
      apply (case_tac x)
      apply simp
      apply (rule accs.intros)
      apply assumption
      apply (unfold r_match_alt)
      apply simp
      apply fastforce
      apply simp
      apply (erule accs.cases)
      apply auto
      apply (rule_tac x="qa → f qs" in bexI)
      apply simp
      apply (unfold r_match_alt)
      apply auto
      done
  qed auto
  thus ?T1 ?T2 by auto
qed

theorem faccs_correct1: "q∈faccs δ n ⟹ accs δ n q" 
  by (simp add: faccs_correct_aux)
theorem faccs_correct2: "accs δ n q ⟹ q∈faccs δ n" 
  by (simp add: faccs_correct_aux)

lemmas faccs_correct = faccs_correct1 faccs_correct2

lemma faccs_alt: "faccs δ t = {q. accs δ t q}" by (auto intro: faccs_correct)

subsection ‹Backward Reduction and Emptiness Check›
subsubsection "Auxiliary Definitions"

― ‹Step function, that maps a set of states to those states 
  that are reachable via one backward step.›
inductive_set bacc_step :: "('Q,'L) ta_rule set ⇒ 'Q set ⇒ 'Q set" 
  for δ Q 
  where
  "⟦ r∈δ; set (rhsq r) ⊆ Q ⟧ ⟹ lhs r ∈ bacc_step δ Q"

― ‹If a set is closed under adding all states that are reachable from the set 
  by one backward step, then this set contains all backward accessible states.›
lemma b_accs_as_closed:
  assumes A: "bacc_step δ Q ⊆ Q"  
  shows "b_accessible δ ⊆ Q"
proof (rule subsetI)
  fix q
  assume "q∈b_accessible δ"
  thus "q∈Q" 
  proof (induct rule: b_accessible.induct)
    fix q f qs
    assume BC: "(q→f qs)∈δ" 
               "!!x. x∈set qs ⟹ x∈b_accessible δ" 
               "!!x. x∈set qs ⟹ x∈Q"
    from bacc_step.intros[OF BC(1)] BC(3) have "q∈bacc_step δ Q" by auto
    with A show "q∈Q" by blast
  qed
qed

subsubsection "Algorithms"

text ‹
  First, the basic workset algorithm is specified. 
  Then, it is refined to contain a counter for each rule, 
  that counts the number of undiscovered states on the RHS. 
  For both levels of abstraction, a version that computes the 
  backwards reduction, and a version that checks for emptiness is specified.

  Additionally, a version of the algorithm that computes a witness
  for non-emptiness is provided.
  
  Levels of abstraction:
  \begin{itemize} 
    \item[‹α›] On this level, the state consists of a set of 
      discovered states and a workset.
    \item[‹α'›] On this level, the state consists of a set of 
      discovered states, a workset and a map from rules to number of 
      undiscovered rhs states. This map can be used to make the discovery of
      rules that have to be considered more efficient.
  \end{itemize}
›

text_raw ‹\paragraph {‹α› - Level:}›

  ― ‹A state contains the set of discovered states and a workset›
type_synonym ('Q,'L) br_state = "'Q set × 'Q set"

  ― ‹Set of states that are non-empty (accept a tree) after adding the 
  state $q$ to the set of discovered states›
definition br_dsq 
  :: "('Q,'L) ta_rule set ⇒ 'Q ⇒ ('Q,'L) br_state ⇒ 'Q set" 
  where  
  "br_dsq δ q == λ(Q,W). { lhs r | r. r∈δ ∧ set (rhsq r) ⊆ (Q-(W-{q})) }"

  ― ‹Description of a step: One state is removed from the workset, and all 
  new states that become non-empty due to this state are added to, both, 
  the workset and the set of discovered states›
inductive_set br_step 
  :: "('Q,'L) ta_rule set ⇒ (('Q,'L) br_state × ('Q,'L) br_state) set" 
  for δ where
  "⟦
     q∈W;
     Q' = Q ∪ br_dsq δ q (Q,W);
     W' = W - {q} ∪ (br_dsq δ q (Q,W) - Q)
   ⟧ ⟹ ((Q,W),(Q',W'))∈br_step δ"

  ― ‹Termination condition for backwards reduction: The workset is empty›
definition br_cond :: "('Q,'L) br_state set" 
  where "br_cond == {(Q,W). W≠{}}"

  ― ‹Termination condition for emptiness check: 
      The workset is empty or a non-empty initial state has been discovered›
definition bre_cond :: "'Q set ⇒ ('Q,'L) br_state set" 
  where "bre_cond Qi == {(Q,W). W≠{} ∧ (Qi∩Q={})}"

  ― ‹Set of all states that occur on the lhs of a constant-rule›
definition br_iq :: "('Q,'L) ta_rule set ⇒ 'Q set" 
  where "br_iq δ == { lhs r | r. r∈δ ∧ rhsq r = [] }"

  ― ‹Initial state for the iteration›
definition br_initial :: "('Q,'L) ta_rule set ⇒ ('Q,'L) br_state" 
  where "br_initial δ == (br_iq δ, br_iq δ)"

  ― ‹Invariant for the iteration: 
    \begin{itemize}
      \item States on the workset have been discovered
      \item Only accessible states have been discovered
      \item If a state is non-empty due to a rule whose 
            rhs-states have been discovered and processed 
            (i.e. are in $Q-W$), then the lhs state of the 
            rule has also been discovered.
      \item The set of discovered states is finite
    \end{itemize}›
definition br_invar :: "('Q,'L) ta_rule set ⇒ ('Q,'L) br_state set" 
  where "br_invar δ == {(Q,W). 
    W⊆Q ∧ 
    Q ⊆ b_accessible δ ∧ 
    bacc_step δ (Q - W) ⊆ Q ∧ 
    finite Q}"

definition "br_algo δ == ⦇
  wa_cond = br_cond,
  wa_step = br_step δ,
  wa_initial = {br_initial δ},
  wa_invar = br_invar δ
⦈"

definition "bre_algo Qi δ == ⦇
  wa_cond = bre_cond Qi,
  wa_step = br_step δ,
  wa_initial = {br_initial δ},
  wa_invar = br_invar δ
⦈"


  ― ‹Termination: Either a new state is added, or the workset decreases.›
definition "br_termrel δ == 
  ({(Q',Q). Q ⊂ Q' ∧ Q' ⊆ b_accessible δ}) <*lex*> finite_psubset"

lemma bre_cond_imp_br_cond[intro, simp]: "bre_cond Qi ⊆ br_cond" 
  by (auto simp add: br_cond_def bre_cond_def)

lemma br_termrel_wf[simp, intro!]: "finite δ ⟹ wf (br_termrel δ)"
  apply (unfold br_termrel_def)
  apply (auto simp add: wf_bounded_supset)
  done

  ― ‹Only accessible states are discovered›
lemma br_dsq_ss:
  assumes A: "(Q,W)∈br_invar δ" "W ≠ {}" "q∈W"
  shows "br_dsq δ q (Q,W) ⊆ b_accessible δ"
proof (rule subsetI)
  fix q'
  assume B: "q'∈br_dsq δ q (Q,W)"
  then obtain r where 
    R: "q' = lhs r" "r∈δ" and 
    S: "set (rhsq r) ⊆ (Q-(W-{q}))" 
    by (unfold br_dsq_def) auto
  note S
  also have "(Q-(W-{q})) ⊆ b_accessible δ" using A(1,3)
    by (auto simp add: br_invar_def)
  finally show "q'∈b_accessible δ" using R
    by (cases r)
  (auto intro: b_accessible.intros)
qed

lemma br_step_in_termrel: 
  assumes A: "Σ∈br_cond" "Σ∈br_invar δ" "(Σ,Σ')∈br_step δ"
  shows "(Σ', Σ)∈br_termrel δ"
proof -
  obtain Q W Q' W' where 
    [simp]: "Σ=(Q,W)" "Σ'=(Q',W')" 
    by (cases Σ, cases Σ', auto)
  obtain q where 
    QIW: "q∈W" and 
    ASSFMT[simp]: "Q' = Q ∪ br_dsq δ q (Q, W)"
                  "W' = W - {q} ∪ (br_dsq δ q (Q, W) - Q)"
    by (auto intro: br_step.cases[OF A(3)[simplified]])

  from A(2) have [simp]: "finite Q" 
    by (auto simp add: br_invar_def)
  from A(2)[unfolded br_invar_def] have [simp]: "finite W" 
    by (auto simp add: finite_subset)
  from A(1) have WNE: "W≠{}" by (unfold br_cond_def) auto

  note DSQSS = br_dsq_ss[OF A(2)[simplified] WNE QIW]
  {
    assume "br_dsq δ q (Q,W) - Q = {}"
    hence ?thesis using QIW
      by (simp add: br_termrel_def set_simps)
  } moreover {
    assume "br_dsq δ q (Q,W) - Q ≠ {}"
    hence "Q ⊂ Q'" by auto
    moreover from DSQSS A(2)[unfolded br_invar_def] have 
      "Q' ⊆ b_accessible δ" 
      by auto
    ultimately have ?thesis 
      by (auto simp add: br_termrel_def)
  } ultimately show ?thesis by blast
qed

lemma br_invar_initial[simp]: "finite δ ⟹ (br_initial δ)∈br_invar δ"
  apply (auto simp add: br_initial_def br_invar_def br_iq_def)
    
  apply (case_tac r)
  apply (fastforce intro: b_accessible.intros)
  apply (fastforce elim!: bacc_step.cases)
  done

lemma br_invar_step: 
  assumes [simp]: "finite δ"
  assumes A: "Σ∈br_cond" "Σ∈br_invar δ" "(Σ,Σ')∈br_step δ"
  shows "Σ'∈br_invar δ"
proof -
  obtain Q W Q' W' where SF[simp]: "Σ=(Q,W)" "Σ'=(Q',W')" 
    by (cases Σ, cases Σ', auto)
  obtain q where 
    QIW: "q∈W" and 
    ASSFMT[simp]: "Q' = Q ∪ br_dsq δ q (Q, W)"
                  "W' = W - {q} ∪ (br_dsq δ q (Q, W) - Q)"
    by (auto intro: br_step.cases[OF A(3)[simplified]])

  from A(1) have WNE: "W≠{}" by (unfold br_cond_def) auto

  have DSQSS: "br_dsq δ q (Q,W) ⊆ b_accessible δ"
    using br_dsq_ss[OF A(2)[simplified] WNE QIW] .

  show ?thesis
    apply (simp add: br_invar_def del: ASSFMT)
  proof (intro conjI)
    from A(2) have "W ⊆ Q" by (simp add: br_invar_def)
    thus "W' ⊆ Q'" by auto
  next
    from A(2) have "Q ⊆ b_accessible δ" by (simp add: br_invar_def)
    with DSQSS show "Q' ⊆ b_accessible δ" by auto
  next
    show "bacc_step δ (Q' - W') ⊆ Q'"
      apply (rule subsetI)
      apply (erule bacc_step.cases)
      apply (auto simp add: br_dsq_def)
      done
  next
    show "finite Q'" using A(2) by (simp add: br_invar_def br_dsq_def)
  qed
qed


lemma br_invar_final:
  "∀Σ. Σ∈wa_invar (br_algo δ) ∧ Σ∉wa_cond (br_algo δ) 
   ⟶ fst Σ = b_accessible δ"
  apply (simp add: br_invar_def br_cond_def br_algo_def)
  apply (auto intro: rev_subsetD[OF _ b_accs_as_closed])
  done
(*  shows "⟦(Q,W)∈br_invar δ; (Q,W)∉br_cond⟧ ⟹ Q = b_accessible δ"
  apply (simp add: br_invar_def br_cond_def)
  apply (auto intro: rev_subsetD[OF _ b_accs_as_closed])
  done*)

theorem br_while_algo: 
  assumes FIN[simp]: "finite δ"
  shows "while_algo (br_algo δ)"
  apply (unfold_locales)
  apply (simp_all add: br_algo_def br_invar_step br_invar_initial 
                       br_step_in_termrel)
  apply (rule_tac r="br_termrel δ" in wf_subset)
  apply (auto intro: br_step_in_termrel)
  done

lemma bre_invar_final:
  "∀Σ. Σ∈wa_invar (bre_algo Qi δ) ∧ Σ∉wa_cond (bre_algo Qi δ) 
     ⟶ ((Qi∩fst Σ={}) ⟷ (Qi ∩ b_accessible δ = {}))"
  apply (simp add: br_invar_def bre_cond_def bre_algo_def)
  apply safe
  apply (auto dest!: b_accs_as_closed)
  done

theorem bre_while_algo:
  assumes FIN[simp]: "finite δ"
  shows "while_algo (bre_algo Qi δ)"
  apply (unfold_locales)
  apply (unfold bre_algo_def)
  apply (auto simp add: br_invar_initial br_step_in_termrel
    intro: br_invar_step 
    dest: rev_subsetD[OF _ bre_cond_imp_br_cond])
  apply (rule_tac r="br_termrel δ" in wf_subset)
  apply (auto intro: br_step_in_termrel
              dest: rev_subsetD[OF _ bre_cond_imp_br_cond])
  done

text_raw ‹\paragraph{‹α'› - Level}›
text ‹
  Here, an optimization is added:
    For each rule, the algorithm now maintains a counter that counts the number
    of undiscovered states on the rules RHS. Whenever a new state is discovered,
    this counter is decremented for all rules where the state occurs on the RHS.
    The LHS states of rules where the counter falls to 0 are added to the 
    worklist. The idea is that decrementing the counter is more efficient than 
    checking whether all states on the rule's RHS have been discovered.

  A similar algorithm is sketched in \<^cite>‹"tata2007"›(Exercise~1.18).
›
type_synonym ('Q,'L) br'_state = "'Q set × 'Q set × (('Q,'L) ta_rule ⇀ nat)"

  ― ‹Abstraction to @{text α}-level›
definition br'_α :: "('Q,'L) br'_state ⇒ ('Q,'L) br_state" 
  where "br'_α = (λ(Q,W,rcm). (Q,W))"

definition br'_invar_add :: "('Q,'L) ta_rule set ⇒ ('Q,'L) br'_state set"
  where "br'_invar_add δ == {(Q,W,rcm). 
    (∀r∈δ. rcm r = Some (card (set (rhsq r) - (Q - W)))) ∧ 
    {lhs r | r. r∈δ ∧ the (rcm r) = 0} ⊆ Q
  }"

definition br'_invar :: "('Q,'L) ta_rule set ⇒ ('Q,'L) br'_state set"
  where "br'_invar δ == br'_invar_add δ ∩ {Σ. br'_α Σ ∈ br_invar δ}"

inductive_set br'_step 
  :: "('Q,'L) ta_rule set ⇒ (('Q,'L) br'_state × ('Q,'L) br'_state) set" 
  for δ where
  "⟦ q∈W;
     Q' = Q ∪ { lhs r | r. r∈δ ∧ q ∈ set (rhsq r) ∧ the (rcm r) ≤ 1 };
     W' = (W-{q}) 
          ∪ ({ lhs r | r. r∈δ ∧ q ∈ set (rhsq r) ∧ the (rcm r) ≤ 1 } 
              - Q);
     !!r. r∈δ ⟹ rcm' r = ( if q ∈ set (rhsq r) then 
                               Some (the (rcm r) - 1) 
                             else rcm r
                           )
   ⟧ ⟹ ((Q,W,rcm),(Q',W',rcm')) ∈ br'_step δ"

definition br'_cond :: "('Q,'L) br'_state set" 
  where "br'_cond == {(Q,W,rcm). W≠{}}"
definition bre'_cond :: "'Q set ⇒ ('Q,'L) br'_state set" 
  where "bre'_cond Qi == {(Q,W,rcm). W≠{} ∧ (Qi∩Q={})}"

inductive_set br'_initial :: "('Q,'L) ta_rule set ⇒ ('Q,'L) br'_state set" 
  for δ where
  "⟦ !!r. r∈δ ⟹ rcm r = Some (card (set (rhsq r))) ⟧ 
     ⟹ (br_iq δ, br_iq δ, rcm)∈br'_initial δ"

definition "br'_algo δ == ⦇
  wa_cond=br'_cond,
  wa_step = br'_step δ,
  wa_initial = br'_initial δ,
  wa_invar = br'_invar δ
⦈"

definition "bre'_algo Qi δ == ⦇
  wa_cond=bre'_cond Qi,
  wa_step = br'_step δ,
  wa_initial = br'_initial δ,
  wa_invar = br'_invar δ
⦈"

lemma br'_step_invar: 
  assumes finite[simp]: "finite δ"
  assumes INV: "Σ∈br'_invar_add δ" "br'_α Σ ∈ br_invar δ"
  assumes STEP: "(Σ,Σ') ∈ br'_step δ"
  shows "Σ'∈br'_invar_add δ"
proof -
  obtain Q W rcm where [simp]: "Σ=(Q,W,rcm)"
    by (cases Σ) auto
  obtain Q' W' rcm' where [simp]: "Σ'=(Q',W',rcm')"
    by (cases Σ') auto

  from STEP obtain q where
    STEPF:
    "q∈W"
    "Q' = Q ∪ { lhs r | r. r∈δ ∧ q ∈ set (rhsq r) ∧ the (rcm r) ≤ 1 }"
    "W' = (W-{q}) 
          ∪ ({ lhs r | r. r∈δ ∧ q ∈ set (rhsq r) ∧ the (rcm r) ≤ 1 } 
              - Q)"
    "!!r. r∈δ ⟹ rcm' r = ( if q ∈ set (rhsq r) then 
                               Some (the (rcm r) - 1) 
                             else rcm r
                           )"
    by (auto elim: br'_step.cases)

  from INV[unfolded br'_invar_def br_invar_def br'_invar_add_def br'_α_def, 
           simplified] 
  have INV:
    "(∀r∈δ. rcm r = Some (card (set (rhsq r) - (Q - W))))" 
    "{lhs r |r. r ∈ δ ∧ the (rcm r) = 0} ⊆ Q" 
    "W ⊆ Q" 
    "Q ⊆ b_accessible δ" 
    "bacc_step δ (Q - W) ⊆ Q" 
    "finite Q"
    by auto

  {
    fix r
    assume A: "r∈δ"
    with INV(1) have RCMR: "rcm r = Some (card (set (rhsq r) - (Q - W)))" 
      by auto

    have "rcm' r = Some (card (set (rhsq r) - (Q' - W')))"
    proof (cases "q∈set (rhsq r)")
      case False
      with A STEPF(4) have "rcm' r = rcm r" by auto
      moreover from STEPF INV(3) False have 
        "set (rhsq r) - (Q-W) = set (rhsq r) - (Q'-W')" 
        by auto
      ultimately show ?thesis
        by (simp add: RCMR)
    next
      case True
      with A STEPF(4) RCMR have 
        "rcm' r = Some ((card (set (rhsq r) - (Q - W))) - 1)"
        by simp
      moreover from STEPF INV(3) True have 
        "set (rhsq r) - (Q-W) = insert q (set (rhsq r) - (Q'-W'))"
        "q∉(set (rhsq r) - (Q'-W'))"
        by auto
      ultimately show ?thesis
        by (simp add: RCMR card_insert_disjoint')
    qed
  } moreover {
    fix r
    assume A: "r∈δ" "the (rcm' r) = 0"
    have "lhs r ∈ Q'" proof (cases "q∈set (rhsq r)")
      case True
      with A(1) STEPF(4) have "rcm' r = Some (the (rcm r) - 1)" by auto
      with A(2) have "the (rcm r) - 1 = 0" by auto
      hence "the (rcm r) ≤ 1" by auto
      with STEPF(2) A(1) True show ?thesis by auto
    next
      case False
      with A(1) STEPF(4) have "rcm' r = rcm r" by auto
      with A(2) have "the (rcm r) = 0" by auto
      with A(1) INV(2) have "lhs r ∈ Q" by auto
      with STEPF(2) show ?thesis by auto
    qed
  } ultimately show ?thesis
    by (auto simp add: br'_invar_add_def)
qed

lemma br'_invar_initial: 
  "br'_initial δ ⊆ br'_invar_add δ"
  apply safe
  apply (erule br'_initial.cases)
  apply (unfold br'_invar_add_def)
  apply (auto simp add: br_iq_def)
  done

lemma br'_rcm_aux': 
  "⟦ (Q,W,rcm)∈br'_invar δ; q∈W ⟧ 
    ⟹ {r ∈ δ. q ∈ set (rhsq r) ∧ the (rcm r) ≤ Suc 0} 
         = {r∈δ. q∈set (rhsq r) ∧ set (rhsq r) ⊆ (Q - (W-{q}))}"
proof (intro subsetI equalityI, goal_cases)
  case prems: (1 r)
  hence  B: "r∈δ" "q∈set (rhsq r)" "the (rcm r) ≤ Suc 0" by auto
  from B(1,3) prems(1)[unfolded br'_invar_def br'_invar_add_def] have 
    CARD: "card (set (rhsq r) - (Q - W)) ≤ Suc 0" 
    by auto
  from prems(1)[unfolded br'_invar_def br_invar_def br'_α_def] have WSQ: "W⊆Q" 
    by auto
  have "set (rhsq r) - (Q - W) = {q}" 
  proof -
    from B(2) prems(2) have R1: "q∈set (rhsq r) - (Q - W)" by auto
    moreover
    {
      fix x
      assume A: "x≠q" "x∈set (rhsq r) - (Q - W)"
      with R1 have "{x,q} ⊆ set (rhsq r) - (Q - W)" by auto
      hence "card {x,q} ≤ card (set (rhsq r) - (Q - W))" 
        by (auto simp add: card_mono)
      with CARD A(1) have False by auto
    }
    ultimately show ?thesis by auto
  qed
  with prems(2) WSQ have "set (rhsq r) ⊆ Q - (W - {q})" by auto
  thus ?case using B(1,2) by auto 
next
  case prems: (2 r)
  hence B: "r∈δ" "q∈set (rhsq r)" "set (rhsq r) ⊆ Q - (W - {q})" by auto
  with prems(1)[unfolded br'_invar_def br'_invar_add_def 
                         br'_α_def br_invar_def] 
  have 
    IC: "W⊆Q" "the (rcm r) = card (set (rhsq r) - (Q - W))" 
    by auto
  have "set (rhsq r) - (Q - W) ⊆ {q}" using B(2,3) IC(1) by auto
  from card_mono[OF _ this] have "the (rcm r) ≤ Suc 0" by (simp add: IC(2))
  with B(1,2) show ?case by auto
qed

lemma br'_rcm_aux: 
  assumes A: "(Q,W,rcm)∈br'_invar δ" "q∈W"  
  shows "{lhs r |r. r ∈ δ ∧ q ∈ set (rhsq r) ∧ the (rcm r) ≤ Suc 0} 
         = {lhs r | r. r∈δ ∧ q∈set (rhsq r) ∧ set (rhsq r) ⊆ (Q - (W-{q}))}"
proof -
  have "{lhs r |r. r ∈ δ ∧ q ∈ set (rhsq r) ∧ the (rcm r) ≤ Suc 0} 
        = lhs ` {r ∈ δ. q ∈ set (rhsq r) ∧ the (rcm r) ≤ Suc 0}" 
    by auto
  also from br'_rcm_aux'[OF A] have 
    "… = lhs ` {r ∈ δ. q ∈ set (rhsq r) ∧ set (rhsq r) ⊆ Q - (W - {q})}" 
    by simp
  also have 
    "… = {lhs r | r. r∈δ ∧ q∈set (rhsq r) ∧ set (rhsq r) ⊆ (Q - (W-{q}))}" 
    by auto
  finally show ?thesis .
qed
  
lemma br'_invar_QcD: 
  "(Q,W,rcm) ∈ br'_invar δ ⟹ {lhs r | r. r∈δ ∧ set (rhsq r) ⊆ (Q-W)} ⊆ Q"
proof (safe)
  fix r
  assume A: "(Q,W,rcm)∈br'_invar δ" "r∈δ" "set (rhsq r) ⊆ Q - W"
  from A(1)[unfolded br'_invar_def br'_invar_add_def br'_α_def br_invar_def, 
            simplified] 
  have 
    IC: "W ⊆ Q" 
        "finite Q" 
        "(∀r∈δ. rcm r = Some (card (set (rhsq r) - (Q - W))))" 
        "{lhs r |r. r ∈ δ ∧ the (rcm r) = 0} ⊆ Q" by auto
  from IC(3) A(2,3) have "the (rcm r) = 0" by auto
  with IC(4) A(2) show "lhs r ∈ Q" by auto
qed

lemma br'_rcm_aux2: 
  "⟦ (Q,W,rcm)∈br'_invar δ; q∈W ⟧ 
    ⟹ Q ∪ br_dsq δ q (Q,W) 
        = Q ∪ {lhs r |r. r ∈ δ ∧ q ∈ set (rhsq r) ∧ the (rcm r) ≤ Suc 0}"
  apply (simp only: br'_rcm_aux)
  apply (unfold br_dsq_def)
  apply simp
  apply (frule br'_invar_QcD)
  apply auto
  done

lemma br'_rcm_aux3: 
  "⟦ (Q,W,rcm)∈br'_invar δ; q∈W ⟧ 
    ⟹ br_dsq δ q (Q,W) - Q 
        = {lhs r |r. r ∈ δ ∧ q ∈ set (rhsq r) ∧ the (rcm r) ≤ Suc 0} - Q"
  apply (simp only: br'_rcm_aux)
  apply (unfold br_dsq_def)
  apply simp
  apply (frule br'_invar_QcD)
  apply auto
  done

lemma br'_step_abs: 
  "⟦ 
     Σ∈br'_invar δ; 
     (Σ,Σ') ∈ br'_step δ 
   ⟧ ⟹ (br'_α Σ, br'_α Σ')∈br_step δ"
  apply (cases Σ, cases Σ', simp)
  apply (erule br'_step.cases)
  apply (simp add: br'_α_def)
  apply (rule_tac q=q in br_step.intros)
  apply simp
  apply (simp only: br'_rcm_aux2)
  apply (simp only: br'_rcm_aux3)
  done
  

lemma br'_initial_abs: "br'_α`(br'_initial δ) = {br_initial δ}"
  apply (force simp add: br_initial_def br'_α_def
               elim: br'_initial.cases 
               intro: br'_initial.intros)
  done

lemma br'_cond_abs: "Σ∈br'_cond ⟷ (br'_α Σ) ∈ br_cond"
  by (cases Σ) 
     (simp add: br'_cond_def br_cond_def br'_α_def image_Collect 
                br'_algo_def br_algo_def)

lemma bre'_cond_abs: "Σ∈bre'_cond Qi ⟷ (br'_α Σ)∈bre_cond Qi"
  by (cases Σ) (simp add: bre'_cond_def bre_cond_def br'_α_def image_Collect 
                          bre'_algo_def bre_algo_def)

lemma br'_invar_abs: "br'_α`br'_invar δ ⊆ br_invar δ"
  by (auto simp add: br'_invar_def)

theorem br'_pref_br: "wa_precise_refine (br'_algo δ) (br_algo δ) br'_α"
  apply unfold_locales
  apply (simp_all add: br'_algo_def br_algo_def)
  apply (simp_all add: br'_cond_abs br'_step_abs br'_invar_abs br'_initial_abs)
  done

interpretation br'_pref: wa_precise_refine "br'_algo δ" "br_algo δ" "br'_α" 
  using br'_pref_br .

theorem br'_while_algo: 
  "finite δ ⟹ while_algo (br'_algo δ)"
  apply (rule br'_pref.wa_intro)
  apply (simp add: br_while_algo)
  apply (simp_all add: br'_algo_def br_algo_def)
  apply (simp add: br'_invar_def)
  apply (erule (3) br'_step_invar)
  apply (simp add: br'_invar_initial)
  done

lemma fst_br'_α: "fst (br'_α s) = fst s" by (cases s) (simp add: br'_α_def)

lemmas br'_invar_final = 
  br'_pref.transfer_correctness[OF br_invar_final, unfolded fst_br'_α]

theorem bre'_pref_br: "wa_precise_refine (bre'_algo Qi δ) (bre_algo Qi δ) br'_α"
  apply unfold_locales
  apply (simp_all add: bre'_algo_def bre_algo_def)
  apply (simp_all add: bre'_cond_abs br'_step_abs br'_invar_abs br'_initial_abs)
  done

interpretation bre'_pref: 
  wa_precise_refine "bre'_algo Qi δ" "bre_algo Qi δ" "br'_α" 
  using bre'_pref_br .

theorem bre'_while_algo: 
  "finite δ ⟹ while_algo (bre'_algo Qi δ)"
  apply (rule bre'_pref.wa_intro)
  apply (simp add: bre_while_algo)
  apply (simp_all add: bre'_algo_def bre_algo_def)
  apply (simp add: br'_invar_def)
  apply (erule (3) br'_step_invar)
  apply (simp add: br'_invar_initial)
  done

lemmas bre'_invar_final = 
  bre'_pref.transfer_correctness[OF bre_invar_final, unfolded fst_br'_α]

text_raw ‹\paragraph{Implementing a Step}›
text ‹
  In this paragraph, it is shown how to implement a step of the br'-algorithm 
  by iteration over the rules that have the discovered state on their RHS.
›

definition br'_inner_step 
  :: "('Q,'L) ta_rule ⇒ ('Q,'L) br'_state ⇒ ('Q,'L) br'_state" 
  where
  "br'_inner_step == λr (Q,W,rcm). let c=the (rcm r) in (
    if c≤1 then insert (lhs r) Q else Q,
    if c≤1 ∧ (lhs r) ∉ Q then insert (lhs r) W else W,
    rcm ( r ↦ (c-(1::nat)))
  )
"

definition br'_inner_invar 
  :: "('Q,'L) ta_rule set ⇒ 'Q ⇒ ('Q,'L) br'_state 
      ⇒ ('Q,'L) ta_rule set ⇒ ('Q,'L) br'_state ⇒ bool" 
  where
  "br'_inner_invar rules q == λ(Q,W,rcm) it (Q',W',rcm'). 
    Q' = Q ∪ { lhs r | r. r∈rules-it ∧ the (rcm r) ≤ 1 } ∧ 
    W' = (W-{q}) ∪ ({ lhs r | r. r∈rules-it ∧ the (rcm r) ≤ 1 } - Q) ∧ 
    (∀r. rcm' r = (if r∈rules-it then Some (the (rcm r) - 1) else rcm r))
  "

lemma br'_inner_invar_imp_final: 
  "⟦ q∈W; br'_inner_invar {r∈δ. q∈set (rhsq r)} q (Q,W-{q},rcm) {} Σ' ⟧ 
     ⟹ ((Q,W,rcm),Σ') ∈ br'_step δ"
  apply (unfold br'_inner_invar_def)
  apply auto
  apply (rule br'_step.intros)
  apply assumption
  apply auto
  done

lemma br'_inner_invar_step: 
  "⟦ q∈W; br'_inner_invar {r∈δ. q∈set (rhsq r)} q (Q,W-{q},rcm) it Σ'; 
     r∈it; it⊆{r∈δ. q∈set (rhsq r)} 
   ⟧ ⟹ br'_inner_invar {r∈δ. q∈set (rhsq r)} q (Q,W-{q},rcm) 
                         (it-{r}) (br'_inner_step r Σ')
  "
  apply (cases Σ', simp)
  apply (unfold br'_inner_invar_def br'_inner_step_def Let_def)
  apply auto
  done

lemma br'_inner_invar_initial: 
  "⟦ q∈W ⟧ ⟹ br'_inner_invar {r∈δ. q∈set (rhsq r)} q (Q,W-{q},rcm) 
                               {r∈δ. q∈set (rhsq r)} (Q,W-{q},rcm)"
  apply (simp add: br'_inner_invar_def)
  apply auto
  done

lemma br'_inner_step_proof:
  fixes αs :: "'Σ ⇒ ('Q,'L) br'_state"
  fixes cstep :: "('Q,'L) ta_rule ⇒ 'Σ ⇒ 'Σ"
  fixes Σh :: "'Σ"
  fixes cinvar :: "('Q,'L) ta_rule set ⇒ 'Σ ⇒ bool"

  assumes iterable_set: "set_iteratei α invar iteratei"
  assumes invar_initial: "cinvar {r∈δ. q∈set (rhsq r)} Σh"
  assumes invar_step: 
    "!!it r Σ. ⟦ r∈it; it ⊆ {r∈δ. q∈set (rhsq r)}; cinvar it Σ ⟧ 
                 ⟹ cinvar (it-{r}) (cstep r Σ)"
  assumes step_desc: 
    "!!it r Σ. ⟦ r∈it; it⊆{r∈δ. q∈set (rhsq r)}; cinvar it Σ ⟧ 
                 ⟹ αs (cstep r Σ) = br'_inner_step r (αs Σ)"
  assumes it_set_desc: "invar it_set" "α it_set = {r∈δ. q∈set (rhsq r)}"

  assumes QIW[simp]: "q∈W"

  assumes Σ_desc[simp]: "αs Σ = (Q,W,rcm)"
  assumes Σh_desc[simp]: "αs Σh = (Q,W-{q},rcm)"

  shows "(αs Σ, αs (iteratei it_set (λ_. True) cstep Σh))∈br'_step δ"
proof -
  interpret set_iteratei α invar iteratei by fact

  show ?thesis
    apply (rule_tac 
      I="λit Σ. cinvar it Σ 
                ∧ br'_inner_invar {r∈δ. q∈set (rhsq r)} q (Q,W-{q},rcm) 
                                  it (αs Σ)" 
      in iterate_rule_P)
    apply (simp_all 
      add: it_set_desc invar_initial br'_inner_invar_initial invar_step 
           step_desc br'_inner_invar_step)
    apply (rule br'_inner_invar_imp_final)
    apply (rule QIW)
    apply simp
    done
qed


text_raw ‹\paragraph{Computing Witnesses}›
text ‹
  The algorithm is now refined further, such that it stores, for each discovered
  state, a witness for non-emptiness, i.e. a tree that is accepted with the
  discovered state.
›

― ‹A map from states to trees has the witness-property, if it maps states to 
    trees that are accepted with that state:›
definition "witness_prop δ m == ∀q t. m q = Some t ⟶ accs δ t q"

― ‹Construct a witness for the LHS of a rule, provided that the map contains 
    witnesses for all states on the RHS:›
definition construct_witness 
  :: "('Q ⇀ 'L tree) ⇒ ('Q,'L) ta_rule ⇒ 'L tree"
  where 
  "construct_witness Q r == NODE (rhsl r) (List.map (λq. the (Q q)) (rhsq r))"

lemma witness_propD: "⟦witness_prop δ m; m q = Some t⟧ ⟹ accs δ t q" 
  by (auto simp add: witness_prop_def)

lemma construct_witness_correct: 
  "⟦ witness_prop δ Q; r∈δ; set (rhsq r) ⊆ dom Q ⟧ 
    ⟹ accs δ (construct_witness Q r) (lhs r)"
  apply (unfold construct_witness_def witness_prop_def)
  apply (cases r)
  apply simp
  apply (erule accs.intros)
  apply (auto dest: nth_mem)
  done

lemma construct_witness_eq: 
  "⟦ Q |` set (rhsq r) = Q' |` set (rhsq r) ⟧ ⟹ 
    construct_witness Q r = construct_witness Q' r"
  apply (unfold construct_witness_def)
  apply auto
  apply (subgoal_tac "Q x = Q' x")
  apply (simp)
  apply (drule_tac x=x in fun_cong)
  apply auto
  done

text ‹
  The set of discovered states is refined by a map from discovered states to 
  their witnesses:
›
type_synonym ('Q,'L) brw_state = "('Q⇀'L tree) × 'Q set × (('Q,'L) ta_rule ⇀ nat)"

definition brw_α :: "('Q,'L) brw_state ⇒ ('Q,'L) br'_state" 
  where "brw_α = (λ(Q,W,rcm). (dom Q,W,rcm))"

definition brw_invar_add :: "('Q,'L) ta_rule set ⇒ ('Q,'L) brw_state set"
  where "brw_invar_add δ == {(Q,W,rcm). witness_prop δ Q}"

definition "brw_invar δ == brw_invar_add δ ∩ {s. brw_α s ∈ br'_invar δ}"

(* TODO:
    This step description does not allow full flexibility, because
    we may want to construct new witnesses from other witnesses constructed 
    in the same step!
    
    However, if we say t = construct_witness Q' r, may we run into cyclicity 
    problems, where a cycle of witnesses
    may witness itself?. Hmm? As these cyclic witnesses would have to
    be infinite, they cannot exist?

    But, if we use a BFS search strategy, the current step description will 
    compute minimal depth witnesses.
    The argumentation is, that:
      Initially, all witnesses of depth 1 (definitely minimal) are discovered
      A witness of depth n has children of length < n
      The states that are initially on the workset are all those with 
      witnesses of depth 1. Thus,
      after they have been processed, all states with witnesses of depth 2 have
      been discovered. This argument can be iterated inductively.
*)
inductive_set brw_step 
  :: "('Q,'L) ta_rule set ⇒ (('Q,'L) brw_state × ('Q,'L) brw_state) set" 
  for δ where
  "⟦ 
     q∈W;
     dsqr = { r∈δ. q ∈ set (rhsq r) ∧ the (rcm r) ≤ 1 };
     dom Q' = dom Q ∪ lhs`dsqr;
     !!q t. Q' q = Some t ⟹ Q q = Some t 
                              ∨ (∃r∈dsqr. q=lhs r ∧ t=construct_witness Q r);
     W' = (W-{q}) ∪ (lhs`dsqr - dom Q);
     !!r. r∈δ ⟹ rcm' r = ( if q ∈ set (rhsq r) then 
                               Some (the (rcm r) - 1) 
                             else rcm r
                           )
   ⟧ ⟹ ((Q,W,rcm),(Q',W',rcm')) ∈ brw_step δ"


definition brw_cond :: "'Q set ⇒ ('Q,'L) brw_state set" 
  where "brw_cond Qi == {(Q,W,rcm). W≠{} ∧ (Qi∩dom Q={})}"

inductive_set brw_iq :: "('Q,'L) ta_rule set ⇒ ('Q ⇀ 'L tree) set" 
  for δ where 
  "⟦ 
    ∀q t. Q q = Some t ⟶ (∃r∈δ. rhsq r = [] ∧ q = lhs r 
                                  ∧ t = NODE (rhsl r) []);
    ∀r∈δ. rhsq r = [] ⟶ Q (lhs r) ≠ None
   ⟧ ⟹ Q ∈ brw_iq δ"

inductive_set brw_initial :: "('Q,'L) ta_rule set ⇒ ('Q,'L) brw_state set" 
  for δ where
  "⟦ !!r. r∈δ ⟹ rcm r = Some (card (set (rhsq r))); Q∈brw_iq δ ⟧ 
     ⟹ (Q, br_iq δ, rcm)∈brw_initial δ"

definition "brw_algo Qi δ == ⦇
  wa_cond=brw_cond Qi,
  wa_step = brw_step δ,
  wa_initial = brw_initial δ,
  wa_invar = brw_invar δ
⦈"

lemma brw_cond_abs: "Σ∈brw_cond Qi ⟷ (brw_α Σ)∈bre'_cond Qi"
  apply (cases Σ)
  apply (simp add: brw_cond_def bre'_cond_def brw_α_def)
  done

lemma brw_initial_abs: "Σ∈brw_initial δ ⟹ brw_α Σ ∈ br'_initial δ"
  apply (cases Σ, simp)
  apply (erule brw_initial.cases)
  apply (erule brw_iq.cases)
  apply (auto simp add: brw_α_def)
  apply (subgoal_tac "dom Qa = br_iq δ")
  apply simp
  apply (rule br'_initial.intros)
  apply auto [1]
  apply (force simp add: br_iq_def)
  done


lemma brw_invar_initial: "brw_initial δ ⊆ brw_invar_add δ"
  apply safe
  apply (unfold brw_invar_add_def)
  apply (auto simp add: witness_prop_def)
  apply (erule brw_initial.cases)
  apply (erule brw_iq.cases)
  apply auto
proof goal_cases
  case prems: (1 q t rcm Q)
  from prems(3)[rule_format, OF prems(1)] obtain r where 
    [simp]: "r∈δ" "rhsq r = []" "q=lhs r" "t=NODE (rhsl r) []" 
    by blast
  have RF[simplified]: "r=((lhs r) → (rhsl r) (rhsq r))" by (cases r) simp
  show ?case 
    apply (simp)
    apply (rule accs.intros)
    apply (subst RF[symmetric])
    apply auto
    done
qed
    
lemma brw_step_abs:
  "⟦ (Σ,Σ')∈brw_step δ ⟧ ⟹ (brw_α Σ, brw_α Σ')∈br'_step δ"
  apply (cases Σ, cases Σ', simp)
  apply (erule brw_step.cases)
  apply (simp add: brw_α_def)
  apply hypsubst
  apply (rule br'_step.intros)
  apply assumption
  apply auto
  done

lemma brw_step_invar:
  assumes FIN[simp]: "finite δ"
  assumes INV: "Σ∈brw_invar_add δ" and BR'INV: "brw_α Σ ∈ br'_invar δ"
  assumes STEP: "(Σ,Σ') ∈ brw_step δ"
  shows "Σ'∈brw_invar_add δ"
proof -
  obtain Q W rcm Q' W' rcm' where 
    [simp]: "Σ=(Q,W,rcm)" "Σ'=(Q',W',rcm')" 
    by (cases Σ, cases Σ') force

  from INV have WP: "witness_prop δ Q" 
    by (simp_all add: brw_invar_add_def)

  obtain qw dsqr where SPROPS:
    "dsqr = {r ∈ δ. qw ∈ set (rhsq r) ∧ the (rcm r) ≤ 1}"
    "qw∈W"
    "dom Q' = dom Q ∪ lhs ` dsqr"
    "!!q t. Q' q = Some t ⟹ Q q = Some t 
                              ∨ (∃r∈dsqr. q=lhs r ∧ t=construct_witness Q r)"
    by (auto intro: brw_step.cases[OF STEP[simplified]])
  from br'_rcm_aux'[OF BR'INV[unfolded brw_α_def, simplified] SPROPS(2)] have 
    DSQR_ALT: "dsqr = {r ∈ δ. qw ∈ set (rhsq r) 
                              ∧ set (rhsq r) ⊆ dom Q - (W - {qw})}" 
    by (simp add: SPROPS(1))
  have "witness_prop δ Q'" 
  proof (unfold witness_prop_def, safe)
    fix q t
    assume A: "Q' q = Some t"

    from SPROPS(4)[OF A] have 
      "Q q = Some t ∨ (∃r∈dsqr. q = lhs r ∧ t = construct_witness Q r)" .
    moreover {
      assume C: "Q q = Some t"
      from witness_propD[OF WP, OF C] have "accs δ t q" .
    } moreover {
      fix r
      assume "r∈dsqr" and [simp]: "q=lhs r" "t=construct_witness Q r"
      from ‹r∈dsqr› have 1: "r∈δ" "set (rhsq r) ⊆ dom Q" 
        by (auto simp add: DSQR_ALT)
      from construct_witness_correct[OF WP 1] have "accs δ t q" by simp
    } ultimately show "accs δ t q" by blast
  qed
  thus ?thesis by (simp add: brw_invar_add_def)
qed
      
theorem brw_pref_bre': "wa_precise_refine (brw_algo Qi δ) (bre'_algo Qi δ) brw_α"
  apply (unfold_locales)
  apply (simp_all add: brw_algo_def bre'_algo_def)
  apply (auto simp add: brw_cond_abs brw_step_abs brw_initial_abs brw_invar_def)
  done

interpretation brw_pref: 
  wa_precise_refine "brw_algo Qi δ" "bre'_algo Qi δ" "brw_α" 
  using brw_pref_bre' .

theorem brw_while_algo: "finite δ ⟹ while_algo (brw_algo Qi δ)"
  apply (rule brw_pref.wa_intro)
  apply (simp add: bre'_while_algo)
  apply (simp_all add: brw_algo_def bre'_algo_def)
  apply (simp add: brw_invar_def)
  apply (auto intro: brw_step_invar simp add: brw_invar_initial)
  done

lemma fst_brw_α: "fst (brw_α s) = dom (fst s)" 
  by (cases s) (simp add: brw_α_def)

theorem brw_invar_final: 
  "∀sc. sc ∈ wa_invar (brw_algo Qi δ) ∧ sc ∉ wa_cond (brw_algo Qi δ) 
    ⟶ (Qi ∩ dom (fst sc) = {}) = (Qi ∩ b_accessible δ = {}) 
        ∧ (witness_prop δ (fst sc))"
  apply (intro conjI allI impI)
  using brw_pref.transfer_correctness[OF bre'_invar_final, unfolded fst_brw_α] 
    apply blast
  apply (auto simp add: brw_algo_def brw_invar_def brw_invar_add_def)
  done
     

text_raw ‹\paragraph{Implementing a Step}›
inductive_set brw_inner_step 
  :: "('Q,'L) ta_rule ⇒ (('Q,'L) brw_state × ('Q,'L) brw_state) set" 
  for r where
  "⟦  c = the (rcm r); Σ = (Q,W,rcm); Σ'=(Q',W',rcm');
     if c≤1 ∧ (lhs r) ∉ dom Q then 
       Q' = Q(lhs r ↦ construct_witness Q r) 
     else Q' = Q;
     if c≤1 ∧ (lhs r) ∉ dom Q then 
       W' = insert (lhs r) W 
     else W' = W;
     rcm' = rcm ( r ↦ (c-(1::nat)))
   ⟧ ⟹ (Σ,Σ')∈brw_inner_step r"

definition brw_inner_invar 
  :: "('Q,'L) ta_rule set ⇒ 'Q ⇒ ('Q,'L) brw_state ⇒ ('Q,'L) ta_rule set 
      ⇒ ('Q,'L) brw_state ⇒ bool" 
  where
  "brw_inner_invar rules q == λ(Q,W,rcm) it (Q',W',rcm').
    (br'_inner_invar rules q (brw_α (Q,W,rcm)) it (brw_α (Q',W',rcm')) ∧  
    (Q'|`dom Q = Q) ∧ 
    (let dsqr = { r∈rules - it. the (rcm r) ≤ 1 } in
      (∀q t. Q' q = Some t ⟶ (Q q = Some t 
           ∨ (Q q = None ∧ (∃r∈dsqr. q=lhs r ∧ t=construct_witness Q r))
                                )
      )))
  "

lemma brw_inner_step_abs: 
  "(Σ,Σ')∈brw_inner_step r ⟹ br'_inner_step r (brw_α Σ) = brw_α Σ'"
  apply (erule brw_inner_step.cases)
  apply (unfold br'_inner_step_def brw_α_def Let_def)
  apply auto
  done


lemma brw_inner_invar_imp_final: 
  "⟦ q∈W; brw_inner_invar {r∈δ. q∈set (rhsq r)} q (Q,W-{q},rcm) {} Σ' ⟧ 
    ⟹ ((Q,W,rcm),Σ') ∈ brw_step δ"
  apply (unfold brw_inner_invar_def br'_inner_invar_def brw_α_def)
  apply (auto simp add: Let_def)
  apply (rule brw_step.intros)
  apply assumption
  apply (rule refl)
  apply auto
  done


lemma brw_inner_invar_step: 
  assumes INVI: "(Q,W,rcm)∈brw_invar δ"
  assumes A: "q∈W" "r∈it" "it⊆{r∈δ. q∈set (rhsq r)}" 
  assumes INVH: "brw_inner_invar {r∈δ. q∈set (rhsq r)} q (Q,W-{q},rcm) it Σh"
  assumes STEP: "(Σh,Σ')∈brw_inner_step r" 
  shows "brw_inner_invar {r∈δ. q∈set (rhsq r)} q (Q,W-{q},rcm) (it-{r}) Σ'"
proof -
  from INVI have BR'_INV: "(dom Q,W,rcm)∈br'_invar δ"
    by (simp add: brw_invar_def brw_α_def)

  obtain c Qh Wh rcmh Q' W' rcm' where
    SIGMAF[simp]: "Σh=(Qh,Wh,rcmh)" "Σ'=(Q',W',rcm')" and
    CF[simp]: "c = the (rcmh r)" and
    SF: "if c≤1 ∧ (lhs r) ∉ dom Qh then 
           Q' = Qh(lhs r ↦ (construct_witness Qh r)) 
         else Q' = Qh"

        "if c≤1 ∧ (lhs r) ∉ dom Qh then 
           W' = insert (lhs r) Wh 
         else W' = Wh"

        "rcm' = rcmh ( r ↦ (c-(1::nat)))"
    by (blast intro: brw_inner_step.cases[OF STEP])
  let ?rules = "{r∈δ. q∈set (rhsq r)}"
  let ?dsqr = "λit. { r∈?rules - it. the (rcm r) ≤ 1 }"
  from INVH have INVHF:
    "br'_inner_invar ?rules q (dom Q, W-{q}, rcm) (it) (dom Qh,Wh,rcmh)"
    "Qh|`dom Q = Q"
    "(∀q t. Qh q = Some t ⟶ (Q q = Some t 
         ∨ (Q q = None ∧ (∃r∈?dsqr it. q=lhs r ∧ t=construct_witness Q r))
                               )
     )"
    by (auto simp add: brw_inner_invar_def Let_def brw_α_def)
  from INVHF(1)[unfolded br'_inner_invar_def] have INV'HF:
    "dom Qh = dom Q ∪ lhs`?dsqr it"
    "(∀r. rcmh r = (if r ∈ ?rules - it then 
                      Some (the (rcm r) - 1) 
                    else rcm r))"
    by auto
  from brw_inner_step_abs[OF STEP] 
       br'_inner_invar_step[OF A(1) INVHF(1) A(2,3)] have 
    G1: "br'_inner_invar ?rules q (dom Q, W-{q}, rcm) (it-{r}) (dom Q',W',rcm')"
    by (simp add: brw_α_def)
  moreover have
    "(∀q t. Q' q = Some t ⟶ (Q q = Some t 
        ∨ ( Q q = None 
            ∧ (∃r∈?dsqr (it-{r}). q=lhs r ∧ t=construct_witness Q r)
           ) 
                              ) 
     )" (is ?G1)

    "Q'|`dom Q = Q" (is ?G2)
  proof -
    {
      assume C: "¬ c≤1 ∨ lhs r ∈ dom Qh"
      with SF have "Q'=Qh" by auto
      with INVHF(2,3) have ?G1 ?G2 by auto
    } moreover {
      assume C: "c≤1" "lhs r∉ dom Qh"
      with SF have Q'F: "Q'=Qh(lhs r ↦ (construct_witness Qh r))" by auto
      from C(2) INVHF(2) INV'HF(1) have G2: ?G2 by (auto simp add: Q'F)
      from C(1) INV'HF A have 
        RI: "r∈?dsqr (it-{r})" and 
        DSS: "dom Q ⊆ dom Qh" 
        by (auto)
      from br'_rcm_aux'[OF BR'_INV A(1)] RI have 
        RDQ: "set (rhsq r) ⊆ dom Q" 
        by auto
      with INVHF(2) have "Qh |` set (rhsq r) = Q |` set (rhsq r)"
        by (blast intro: restrict_map_subset_eq)
      hence [simp]: "construct_witness Qh r = construct_witness Q r" 
        by (blast dest: construct_witness_eq)

      from DSS C(2) have [simp]: "Q (lhs r) = None" "Qh (lhs r) = None" by auto
      have G1: ?G1
      proof (intro allI impI, goal_cases)
        case prems: (1 q t)
        {
          assume [simp]: "q=lhs r"
          from prems Q'F have [simp]: "t = (construct_witness Qh r)" by simp
          from RI have ?case by auto
        } moreover {
          assume "q≠lhs r"
          with Q'F prems have "Qh q = Some t" by auto
          with INVHF(3) have ?case by auto
        } ultimately show ?case by blast
      qed
      note G1 G2
    } ultimately show ?G1 ?G2 by blast+
  qed
  ultimately show ?thesis
    by (unfold brw_inner_invar_def Let_def brw_α_def) auto
qed


lemma brw_inner_invar_initial: 
  "⟦q∈W⟧ ⟹ brw_inner_invar {r∈δ. q∈set (rhsq r)} q (Q,W-{q},rcm) 
                             {r∈δ. q∈set (rhsq r)} (Q,W-{q},rcm)"
  by (simp add: brw_inner_invar_def br'_inner_invar_initial brw_α_def)

theorem brw_inner_step_proof:
  fixes αs :: "'Σ ⇒ ('Q,'L) brw_state"
  fixes cstep :: "('Q,'L) ta_rule ⇒ 'Σ ⇒ 'Σ"
  fixes Σh :: "'Σ"
  fixes cinvar :: "('Q,'L) ta_rule set ⇒ 'Σ ⇒ bool"

  assumes set_iterate: "set_iteratei α invar iteratei"
  assumes invar_start: "(αs Σ)∈brw_invar δ"
  assumes invar_initial: "cinvar {r∈δ. q∈set (rhsq r)} Σh"
  assumes invar_step: 
    "!!it r Σ. ⟦ r∈it; it ⊆ {r∈δ. q∈set (rhsq r)}; cinvar it Σ ⟧ 
                ⟹ cinvar (it-{r}) (cstep r Σ)"
  assumes step_desc: 
    "!!it r Σ. ⟦ r∈it; it⊆{r∈δ. q∈set (rhsq r)}; cinvar it Σ ⟧ 
                ⟹ (αs Σ, αs (cstep r Σ)) ∈ brw_inner_step r"
  assumes it_set_desc: "invar it_set" "α it_set = {r∈δ. q∈set (rhsq r)}"

  assumes QIW[simp]: "q∈W"

  assumes Σ_desc[simp]: "αs Σ = (Q,W,rcm)"
  assumes Σh_desc[simp]: "αs Σh = (Q,W-{q},rcm)"

  shows "(αs Σ, αs (iteratei it_set (λ_. True) cstep Σh))∈brw_step δ"
proof -
  interpret set_iteratei α invar iteratei by fact

  show ?thesis
    apply (rule_tac 
      I="λit Σ. cinvar it Σ ∧ brw_inner_invar {r∈δ. q∈set (rhsq r)} q 
                                                (Q,W-{q},rcm) it (αs Σ)" 
      in iterate_rule_P)
    apply (auto 
      simp add: it_set_desc invar_initial brw_inner_invar_initial invar_step 
                step_desc brw_inner_invar_step[OF invar_start[simplified]] 
                brw_inner_invar_imp_final[OF QIW])
    done
qed

subsection ‹Product Automaton›

text ‹
  The forward-reduced product automaton can be described as a state-space
  exploration problem. 

  In this section, the DFS-algorithm for state-space exploration 
  (cf. Theory~@{theory Collections_Examples.Exploration} in the Isabelle Collections Framework) is refined to compute the product automaton.
›

type_synonym ('Q1,'Q2,'L) frp_state = 
  "('Q1×'Q2) set × ('Q1×'Q2) list × (('Q1×'Q2),'L) ta_rule set"

definition frp_α :: "('Q1,'Q2,'L) frp_state ⇒ ('Q1×'Q2) dfs_state"
  where "frp_α S == let (Q,W,δ)=S in (Q, W)"

definition "frp_invar_add δ1 δ2 == 
  { (Q,W,δd). δd = { r. r∈δ_prod δ1 δ2 ∧ lhs r ∈ Q - set W} }"

definition frp_invar 
  :: "('Q1, 'L) tree_automaton_rec ⇒ ('Q2, 'L) tree_automaton_rec 
      ⇒ ('Q1,'Q2,'L) frp_state set"
  where "frp_invar T1 T2 == 
  frp_invar_add (ta_rules T1) (ta_rules T2) 
  ∩ { s. frp_α s ∈ dfs_invar (ta_initial T1 × ta_initial T2) 
                              (f_succ (δ_prod (ta_rules T1) (ta_rules T2))) }"

inductive_set frp_step 
  :: "('Q1,'L) ta_rule set ⇒ ('Q2,'L) ta_rule set 
      ⇒ (('Q1,'Q2,'L) frp_state × ('Q1,'Q2,'L) frp_state) set" 
  for δ1 δ2 where
  "⟦ W=(q1,q2)#Wtl;
     distinct Wn;
     set Wn = f_succ (δ_prod δ1 δ2) `` {(q1,q2)} - Q;
     W'=Wn@Wtl;
     Q'=Q ∪ f_succ (δ_prod δ1 δ2) `` {(q1,q2)};
     δd'=δd ∪ {r∈δ_prod δ1 δ2. lhs r = (q1,q2) }
  ⟧ ⟹ ((Q,W,δd),(Q',W',δd'))∈frp_step δ1 δ2"

inductive_set frp_initial :: "'Q1 set ⇒ 'Q2 set ⇒ ('Q1,'Q2,'L) frp_state set"
  for Q10 Q20 where 
  "⟦ distinct W; set W = Q10×Q20 ⟧ ⟹ (Q10×Q20,W,{}) ∈ frp_initial Q10 Q20"

definition frp_cond :: "('Q1,'Q2,'L) frp_state set" where
  "frp_cond == {(Q,W,δd). W≠[]}"

definition "frp_algo T1 T2 == ⦇
  wa_cond = frp_cond,
  wa_step = frp_step (ta_rules T1) (ta_rules T2),
  wa_initial = frp_initial (ta_initial T1) (ta_initial T2),
  wa_invar = frp_invar T1 T2
⦈"

  ― ‹The algorithm refines the DFS-algorithm›
theorem frp_pref_dfs: 
  "wa_precise_refine (frp_algo T1 T2) 
     (dfs_algo (ta_initial T1 × ta_initial T2) 
               (f_succ (δ_prod (ta_rules T1) (ta_rules T2))))
     frp_α"
  apply unfold_locales
  apply (auto simp add: frp_algo_def frp_α_def frp_cond_def dfs_algo_def 
                        dfs_cond_def frp_invar_def
    elim!: frp_step.cases frp_initial.cases
    intro: dfs_step.intros dfs_initial.intros
  )
  done 

interpretation frp_ref: wa_precise_refine "(frp_algo T1 T2)"
                  "(dfs_algo (ta_initial T1 × ta_initial T2) 
                             (f_succ (δ_prod (ta_rules T1) (ta_rules T2))))"
                  "frp_α" using frp_pref_dfs .

― ‹The algorithm is a well-defined while-algorithm›
theorem frp_while_algo:
  assumes TA: "tree_automaton T1" 
              "tree_automaton T2"
  shows "while_algo (frp_algo T1 T2)"
proof -
  interpret t1: tree_automaton T1 by fact
  interpret t2: tree_automaton T2 by fact

  have finite: "finite ((f_succ (δ_prod (ta_rules T1) (ta_rules T2)))⇧* 
               `` (ta_initial T1 × ta_initial T2))"
  proof -
    have "((f_succ (δ_prod (ta_rules T1) (ta_rules T2)))⇧* 
               `` (ta_initial T1 × ta_initial T2)) 
          ⊆ ((ta_initial T1 × ta_initial T2) 
             ∪ δ_states (δ_prod (ta_rules T1) (ta_rules T2)))"
      apply rule
      apply (drule f_accessible_subset[unfolded f_accessible_def])
      apply auto
      done
    moreover have "finite …"
      by auto
    ultimately show ?thesis by (simp add: finite_subset)
  qed

  show ?thesis
    apply (rule frp_ref.wa_intro)
    apply (rule dfs_while_algo[OF finite])
    apply (simp add: frp_algo_def dfs_algo_def frp_invar_def)
    apply (auto simp add: dfs_algo_def frp_algo_def frp_α_def 
                          dfs_α_def frp_invar_add_def dfs_invar_def 
                          dfs_invar_add_def sse_invar_def 
                elim!: frp_step.cases) [1]
    apply (force simp add: frp_algo_def frp_invar_add_def 
                 elim!: frp_initial.cases)
    done
qed

(* unused
lemma f_succ_adv: 
  "⟦lhs r ∈ (f_succ δ)⇧* `` Q0; r∈δ⟧ ⟹ set (rhsq r) ⊆ (f_succ δ)⇧* `` Q0"
  by (case_tac r) (auto dest: rtrancl_into_rtrancl intro: f_succ.intros)
*)

― ‹If the algorithm terminates, the forward reduced product automaton 
    can be constructed from the result›
theorem frp_inv_final:
  "∀s. s∈wa_invar (frp_algo T1 T2) ∧ s∉wa_cond (frp_algo T1 T2)
       ⟶ (case s of (Q,W,δd) ⇒ 
             ⦇ ta_initial = ta_initial T1 × ta_initial T2, 
               ta_rules = δd 
             ⦈ = ta_fwd_reduce (ta_prod T1 T2))"
  apply (intro allI impI)
  apply (case_tac s)
  apply simp
  apply (simp add: ta_reduce_def ta_prod_def frp_algo_def)
proof -
  fix Q W δd
  assume A: "(Q,W,δd)∈frp_invar T1 T2 ∧ (Q,W,δd)∉frp_cond"

  from frp_ref.transfer_correctness[OF dfs_invar_final, 
                                    unfolded frp_algo_def, simplified, 
                                    rule_format, OF A]
  have [simp]: "Q = f_accessible (δ_prod (ta_rules T1) (ta_rules T2)) 
                                 (ta_initial T1 × ta_initial T2)"
    by (simp add: f_accessible_def dfs_α_def frp_α_def)

  from A show "δd = reduce_rules 
    (δ_prod (ta_rules T1) (ta_rules T2)) 
    (f_accessible (δ_prod (ta_rules T1) (ta_rules T2)) 
                  (ta_initial T1 × ta_initial T2))"
    apply (auto simp add: reduce_rules_def f_accessible_def frp_invar_def 
                          frp_invar_add_def frp_α_def frp_cond_def)
    apply (case_tac x) 
    apply (auto dest: rtrancl_into_rtrancl intro: f_succ.intros)
    done
qed


end