Theory Process_Normalization

(***********************************************************************************
 * Copyright (c) 2025 Université Paris-Saclay
 *
 * Author: Benoît Ballenghien, Université Paris-Saclay,
 *         CNRS, ENS Paris-Saclay, LMF
 * Author: Burkhart Wolff, Université Paris-Saclay,
 *         CNRS, ENS Paris-Saclay, LMF
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 * * Redistributions of source code must retain the above copyright notice, this
 *
 * * Redistributions in binary form must reproduce the above copyright notice,
 *   this list of conditions and the following disclaimer in the documentation
 *   and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
 * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
 * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 ***********************************************************************************)


chapter ‹ProcOmata: Functional Automata embedded into CSP Processes›

(*<*)
theory Process_Normalization
  imports "HOL-CSP_PTick"
begin
  (*>*)


text ‹
We will often have to perform induction on both the list of automata
and the list of states, provided that they have the same length.›

lemma induct_2_lists012 [consumes 1, case_names Nil single Cons] : 
  ‹⟦length xs = length ys; P [] []; ⋀x1 y1. P [x1] [y1];
    ⋀x1 x2 xs y1 y2 ys. length xs = length ys ⟹ P xs ys ⟹
                         P (x2 # xs) (y2 # ys) ⟹ P (x1 # x2 # xs) (y1 # y2 # ys)⟧
   ⟹ P xs ys›
  by (induct xs arbitrary: ys rule: induct_list012)
    (auto simp add: Suc_length_conv length_Suc_conv)

lemma nat_induct_012 [case_names 0 1 2 Suc]:
  ‹⟦P 0; P (Suc 0); P (Suc (Suc 0)); ⋀k. Suc (Suc 0) ≤ k ⟹ P k ⟹ P (Suc k)⟧ ⟹ P n›
  by (metis One_nat_def Suc_1 less_2_cases_iff linorder_not_le nat_induct)



text ‹
The following results will be moved to session‹Restriction_Spaces› in the future.
›

lemma restriction_shift_iterated :
  ‹restriction_shift (f ^^ k) (int k * m)›
  if ‹restriction_shift f m› for f :: ‹'a ⇒ 'a :: restriction_space›
proof (induct k)
  show ‹restriction_shift (f ^^ 0) (int 0 * m)›
    by (simp add: restriction_shiftI)
next
  fix k assume * : ‹restriction_shift (f ^^ k) (int k * m)›
  have ‹restriction_shift (f ^^ Suc k) (int (Suc k) * m) ⟷
        restriction_shift (λx. f ((f ^^ k) x)) (int k * m + m)›
    by (simp add: comp_def distrib_left mult.commute add.commute)
  also have … by (fact restriction_shift_comp_restriction_shift[OF that "*"])
  finally show ‹restriction_shift (f ^^ Suc k) (int (Suc k) * m)› .
qed

lemma non_destructive_iterated :
  ‹non_destructive f ⟹ non_destructive (f ^^ k)›
  for f :: ‹'a ⇒ 'a :: restriction_space›
  by (metis mult.commute mult_zero_left non_destructive_def non_destructive_on_def
      restriction_shift_def restriction_shift_iterated)

lemma constructive_iterated :
  ‹constructive (f ^^ k)› if ‹0 < k› ‹constructive f›
for f :: ‹'a ⇒ 'a :: restriction_space›
proof -
  from ‹constructive f› have ‹restriction_shift f 1›
    unfolding constructive_def constructive_on_def restriction_shift_def by blast
  with restriction_shift_iterated
  have ‹restriction_shift (f ^^ k) (int k * 1)› .
  hence ‹restriction_shift (f ^^ k) (int k)› by simp
  with ‹0 < k› show ‹constructive (f ^^ k)›
    by (metis One_nat_def constructive_def constructive_on_def
        less_eq_Suc_le nat_int_comparison(3) of_nat_1_eq_iff
        restriction_shift_def restriction_shift_imp_restriction_shift_le )
qed


lemma restriction_fix_unique_iterated :
  ‹⟦0 < k; constructive f; (f ^^ k) x = x⟧ ⟹ (υ x. f x) = x›
  by (metis constructive_iterated funpow_swap1 restriction_fix_unique)


lemma restriction_fix_iterated :
  ‹0 < k ⟹ constructive f ⟹ (υ x. (f ^^ k) x) = (υ x. f x)›
  by (metis constructive_iterated restriction_fix_eq restriction_fix_unique_iterated)



corollary restriction_fix_ind_iterated
  [consumes 1, case_names constructive adm base step]:
  ‹P (υ x. f x)› if ‹0 < k› ‹constructive f› ‹adm↓ P› ‹P x› ‹⋀x. P x ⟹ P ((f ^^ k) x)›
proof -
  from constructive_iterated that(1, 2) have ‹constructive (f ^^ k)› .
  from restriction_fix_ind[OF this that(3-5)] have ‹P (υ x. (f ^^ k) x)› .
  also from restriction_fix_iterated that(1, 2) have ‹(υ x. (f ^^ k) x) = (υ x. f x)› .
  finally show ‹P (υ x. f x)› .
qed




section ‹Definitions›


subsection ‹Non-deterministic and deterministic Automata›

unbundle option_type_syntax

type_synonym ('σ, 'a) enabl  = ‹'σ ⇒ 'a set›
type_synonym ('σ, 'a, 'σ') trans = ‹'σ ⇒ 'a ⇒ 'σ'›
type_synonym ('σ, 'a) transd  = ‹('σ, 'a, 'σ option) trans›
type_synonym ('σ, 'a) transnd = ‹('σ, 'a, 'σ set) trans›

record ('σ, 'a, 'σ', 'r) A =
  τ :: ‹('σ, 'a, 'σ') trans›
  ω :: ‹'σ ⇒ 'r›

type_synonym ('σ, 'a, 'r) Ad = ‹('σ, 'a, 'σ option, 'r option) A›
type_synonym ('σ, 'a, 'r, 'α) Ad_scheme = ‹('σ, 'a, 'σ option, 'r option, 'α) A_scheme›
type_synonym ('σ, 'a, 'r) And = ‹('σ, 'a, 'σ set, 'r set) A›
type_synonym ('σ, 'a, 'r, 'α) And_scheme = ‹('σ, 'a, 'σ set, 'r set, 'α) A_scheme›



subsection ‹Enableness›

consts ε :: ‹('σ, 'a, 'σ', 'r', 'α) A_scheme ⇒ ('σ, 'a) enabl›
overloading
  εd ≡ ‹ε :: ('σ, 'a, 'σ option, 'r', 'α) A_scheme ⇒ ('σ, 'a) enabl›
  εnd ≡ ‹ε :: ('σ, 'a, 'σ set, 'r', 'α) A_scheme ⇒ ('σ, 'a) enabl›
begin
fun εd :: ‹('σ, 'a, 'σ option, 'r', 'α) A_scheme ⇒ ('σ, 'a) enabl›
  where ‹εd A σ = {a. τ A σ a ≠ ◇}›
fun εnd :: ‹('σ, 'a, 'σ set, 'r', 'α) A_scheme ⇒ ('σ, 'a) enabl›
  where ‹εnd A σ = {a. τ A σ a ≠ {}}›
end

lemmas ε_simps[simp del] = εd.simps εnd.simps


subsection ‹States allowing Termination›

consts ρ :: ‹('σ, 'a, 'σ', 'r', 'α) A_scheme ⇒ 'σ set›
overloading
  ρd ≡ ‹ρ :: ('σ, 'a, 'σ', 'r option, 'α) A_scheme ⇒ 'σ set›
  ρnd ≡ ‹ρ :: ('σ, 'a, 'σ', 'r set, 'α) A_scheme ⇒ 'σ set›
begin
fun ρd :: ‹('σ, 'a, 'σ', 'r option, 'α) A_scheme ⇒ 'σ set›
  where ‹ρd A = {σ. ω A σ ≠ ◇}›
fun ρnd :: ‹('σ, 'a, 'σ', 'r set, 'α) A_scheme ⇒ 'σ set›
  where ‹ρnd A = {σ. ω A σ ≠ {}}›
end

lemmas ρ_simps[simp del] = ρd.simps ρnd.simps


subsection ‹Reachability›

inductive_set ℛd :: ‹('σ, 'a, 'r, 'α) Ad_scheme ⇒ 'σ ⇒ 'σ set›
  for A :: ‹('σ, 'a, 'r, 'α) Ad_scheme› and σ :: 'σ
  where init : ‹σ  ∈ ℛd A σ›
  |     step : ‹σ' ∈ ℛd A σ ⟹ ⌊σ''⌋ = τ A σ' a ⟹ σ'' ∈ ℛd A σ›

inductive_set ℛnd :: ‹('σ, 'a, 'r, 'α) And_scheme ⇒ 'σ ⇒ 'σ set›
  for A :: ‹('σ, 'a, 'r, 'α) And_scheme› and σ :: 'σ
  where init : ‹σ  ∈ ℛnd A σ›
  |     step : ‹σ' ∈ ℛnd A σ ⟹ σ'' ∈ τ A σ' a ⟹ σ'' ∈ ℛnd A σ›


lemma ℛd_trans: ‹σ'' ∈ ℛd A σ' ⟹ σ' ∈ ℛd A σ ⟹ σ'' ∈ ℛd A σ›
  by (induct rule: ℛd.induct, simp add: ℛd.init) (meson ℛd.step)

lemma ℛnd_trans: ‹σ'' ∈ ℛnd A σ' ⟹ σ' ∈ ℛnd A σ ⟹ σ'' ∈ ℛnd A σ›
  by (induct rule: ℛnd.induct, simp add: ℛnd.init) (meson ℛnd.step)



subsection ‹Morphisms›

text ‹
Our morphisms are defined considering that,
except from const‹τ›, the fields remain unchanged.›

definition from_det_to_ndet ::
  ‹('σ, 'a, 'r, 'α) Ad_scheme ⇒ ('σ, 'a, 'r, 'α) And_scheme›
  where ‹from_det_to_ndet A ≡
         ⦇τ = λσ a. case τ A σ a of ⌊σ'⌋ ⇒ {σ'} | ◇ ⇒ {},
          ω = λσ. case ω A σ of ⌊r⌋ ⇒ {r} | ◇ ⇒ {}, … = more A⦈›
definition from_ndet_to_det ::
  ‹('σ, 'a, 'r, 'α) And_scheme ⇒ ('σ, 'a, 'r, 'α) Ad_scheme›
  where ‹from_ndet_to_det A ≡
         ⦇τ = λσ a. if τ A σ a = {} then ◇ else ⌊THE σ'. σ' ∈ τ A σ a⌋,
          ω = λσ. if ω A σ = {} then ◇ else ⌊THE r. r ∈ ω A σ⌋, … = more A⦈›

definition from_σ_to_σsd ::
  ‹('σ, 'a, 'r, 'α) Ad_scheme ⇒ ('σ list, 'a, 'r, 'α) Ad_scheme›
  where ‹from_σ_to_σsd A ≡
         ⦇τ = λσs a. case τ A (hd σs) a of ⌊σ'⌋ ⇒ ⌊[σ']⌋ | ◇ ⇒ ◇,
          ω = λσs. ω A (hd σs), … = more A⦈›
definition from_σ_to_σsnd ::
  ‹('σ, 'a, 'r, 'α) And_scheme ⇒ ('σ list, 'a, 'r, 'α) And_scheme›
  where ‹from_σ_to_σsnd A ≡
         ⦇τ = λσs a. {[σ'] |σ'. σ' ∈ τ A (hd σs) a},
          ω = λσs. ω A (hd σs), … = more A⦈›

definition from_σs_to_σd ::
  ‹('σ list, 'a, 'r, 'α) Ad_scheme ⇒ ('σ, 'a, 'r, 'α) Ad_scheme›
  where ‹from_σs_to_σd A ≡
         ⦇τ = λσ a. case τ A [σ] a of ⌊σs'⌋ ⇒ ⌊hd σs'⌋ | ◇ ⇒ ◇,
          ω = λσ. ω A [σ], … = more A⦈›
definition from_σs_to_σnd ::
  ‹('σ list, 'a, 'r, 'α) And_scheme ⇒ ('σ, 'a, 'r, 'α) And_scheme›
  where ‹from_σs_to_σnd A ≡
         ⦇τ = λσ a. {hd σs' |σs'. σs' ∈ τ A [σ] a},
          ω = λσ. ω A [σ], … = more A⦈›

definition from_singl_to_listd ::
  ‹('σ, 'a, 'r, 'α) Ad_scheme ⇒ ('σ list, 'a, 'r list, 'α) Ad_scheme›
  where ‹from_singl_to_listd A ≡
         ⦇τ = λσs a. case τ A (hd σs) a of ⌊σ'⌋ ⇒ ⌊[σ']⌋ | ◇ ⇒ ◇,
          ω = λσs. case ω A (hd σs) of ⌊r⌋ ⇒ ⌊[r]⌋ | ◇ ⇒ ◇, … = more A⦈›
definition from_singl_to_listnd ::
  ‹('σ, 'a, 'r, 'α) And_scheme ⇒ ('σ list, 'a, 'r list, 'α) And_scheme›
  where ‹from_singl_to_listnd A ≡
         ⦇τ = λσs a. {[σ'] |σ'. σ' ∈ τ A (hd σs) a},
          ω = λσs. {[r] |r. r ∈ ω A (hd σs)}, … = more A⦈›

definition from_list_to_singld ::
  ‹('σ list, 'a, 'r list, 'α) Ad_scheme ⇒ ('σ, 'a, 'r, 'α) Ad_scheme›
  where ‹from_list_to_singld A ≡
         ⦇τ = λσ a. case τ A [σ] a of ⌊σs'⌋ ⇒ ⌊hd σs'⌋ | ◇ ⇒ ◇,
          ω = λσ. case ω A [σ] of ⌊rs⌋ ⇒ ⌊hd rs⌋ | ◇ ⇒ ◇, … = more A⦈›
definition from_list_to_singlnd ::
  ‹('σ list, 'a, 'r list, 'α) And_scheme ⇒ ('σ, 'a, 'r, 'α) And_scheme›
  where ‹from_list_to_singlnd A ≡
         ⦇τ = λσ a. {hd σs' |σs'. σs' ∈ τ A [σ] a},
          ω = λσ. {hd rs |rs. rs ∈ ω A [σ]}, … = more A⦈›

lemmas det_ndet_conv_defs  = from_det_to_ndet_def from_ndet_to_det_def
  and      σ_σs_conv_defs  = from_σ_to_σsd_def from_σ_to_σsnd_def
  from_σs_to_σd_def from_σs_to_σnd_def
  and singl_list_conv_defs = from_singl_to_listd_def from_singl_to_listnd_def
  from_list_to_singld_def from_list_to_singlnd_def


bundle functional_automata_morphisms_syntax begin

notation from_det_to_ndet (‹⟪_⟫d↪nd› [0])
notation from_ndet_to_det (‹⟪_⟫nd↝d› [0])
notation from_σ_to_σsd (‹d⟪_⟫σ↪σs› [0])
notation from_σ_to_σsnd (‹nd⟪_⟫σ↪σs› [0])
notation from_σs_to_σd (‹d⟪_⟫σs↝σ› [0])
notation from_σs_to_σnd (‹nd⟪_⟫σs↝σ› [0])
notation from_singl_to_listd (‹d⟪_⟫singl↪list› [0])
notation from_singl_to_listnd (‹nd⟪_⟫singl↪list› [0])
notation from_list_to_singld (‹d⟪_⟫list↝singl› [0])
notation from_list_to_singlnd (‹nd⟪_⟫list↝singl› [0])

end


unbundle functional_automata_morphisms_syntax


lemma morphisms_A_scheme_more_simps [simp] :
  ‹more ⟪A⟫d↪nd = more A› ‹more ⟪B⟫nd↝d = more B›
  ‹more d⟪C⟫σ↪σs = more C› ‹more nd⟪D⟫σ↪σs = more D›
  ‹more d⟪E⟫σs↝σ = more E› ‹more nd⟪F⟫σs↝σ = more F›
  ‹more d⟪G⟫singl↪list = more G› ‹more nd⟪H⟫singl↪list = more H›
  ‹more d⟪I⟫list↝singl = more I› ‹more nd⟪J⟫list↝singl = more J›
  by (simp_all add: det_ndet_conv_defs σ_σs_conv_defs singl_list_conv_defs)


subsection ‹Generic update Functions›

definition update_both  where ‹update_both  A0 A1 σ0 σ1 e f ≡ f (τ A0 σ0 e) (τ A1 σ1 e)›

definition update_left  where ‹update_left  A0 σ0 σ1 e f g  ≡ f (τ A0 σ0 e) (g σ1)›

definition update_right where ‹update_right A1 σ0 σ1 e f g  ≡ f (g σ0) (τ A1 σ1 e)›

lemmas update_defs[simp] = update_both_def update_left_def update_right_def

abbreviation f_up_set where ‹f_up_set f B C ≡ {f s t| s t. (s, t) ∈ B × C}›

abbreviation f_up_opt where ‹f_up_opt f s t ≡ case s of ◇ ⇒ ◇ | ⌊s'⌋ ⇒ map_option (f s') t›





subsection ‹Assumptions on Automata›

(*required hypothesis when we will need continuity*)
definition finite_trans :: ‹('σ, 'a, 'r, 'α) And_scheme ⇒ bool›
  where ‹finite_trans A ≡ ∀σ a. finite (τ A σ a)›

lemma finite_trans_morphisms_simps[simp]: 
  ‹finite_trans ⟪A⟫d↪nd›
  ‹finite_trans B ⟹ finite_trans nd⟪B⟫σ↪σs›
  ‹finite_trans C ⟹ finite_trans nd⟪C⟫σs↝σ›
  ‹finite_trans D ⟹ finite_trans nd⟪D⟫singl↪list›
  ‹finite_trans E ⟹ finite_trans nd⟪E⟫list↝singl›                       
  unfolding det_ndet_conv_defs σ_σs_conv_defs singl_list_conv_defs finite_trans_def
  by (simp_all add: option.case_eq_if)


definition at_most_1_elem :: ‹('σ, 'a, 'r, 'α) And_scheme ⇒ bool›
  where ‹at_most_1_elem A ≡
         (∀σ a. τ A σ a = {} ∨ (∃σ'. τ A σ a = {σ'})) ∧
         (∀σ. ω A σ = {} ∨ (∃r. ω A σ = {r}))›

lemma at_most_1_elem_def_bis :
  ‹at_most_1_elem A ⟷ (∀σ a. ∃σ'. τ A σ a ⊆ {σ'}) ∧ (∀σ. ∃r. ω A σ ⊆ {r})›
  by (auto simp add: at_most_1_elem_def subset_iff)
    (((metis empty_iff singleton_iff)+)[2],
      ((metis equals0D is_singletonI' is_singleton_some_elem)+)[2])

lemma at_most_1_elemI :
  ‹⟦⋀σ a. τ A σ a = {} ∨ (∃σ'. τ A σ a = {σ'});
    ⋀σ. ω A σ = {} ∨ (∃r. ω A σ = {r})⟧ ⟹ at_most_1_elem A›
  by (simp add: at_most_1_elem_def)

lemma at_most_1_elemE :
  ‹⟦τ A σ a = {} ⟹ thesis; ⋀σ'. τ A σ a = {σ'} ⟹ thesis⟧ ⟹ thesis›
  ‹⟦ω A σ = {} ⟹ thesis; ⋀r. ω A σ = {r} ⟹ thesis⟧ ⟹ thesis›
  if ‹at_most_1_elem A›
  by (meson at_most_1_elem_def ‹at_most_1_elem A›)+



definition at_most_1_elem_trans :: ‹('σ, 'a, 'r, 'α) And_scheme ⇒ bool›
  where ‹at_most_1_elem_trans A ≡ ∀σ a. τ A σ a = {} ∨ (∃σ'. τ A σ a = {σ'})›

lemma at_most_1_elem_trans_def_bis :
  ‹at_most_1_elem_trans A ⟷ (∀σ a. ∃σ'. τ A σ a ⊆ {σ'})›
  by (auto simp add: at_most_1_elem_trans_def subset_iff)
    (metis empty_iff singleton_iff,
      metis equals0D is_singletonI' is_singleton_some_elem)

lemma at_most_1_elem_transI :
  ‹⟦⋀σ a. τ A σ a = {} ∨ (∃σ'. τ A σ a = {σ'})⟧ ⟹ at_most_1_elem_trans A›
  by (simp add: at_most_1_elem_trans_def)

lemma at_most_1_elem_transE :
  ‹⟦τ A σ a = {} ⟹ thesis; ⋀σ'. τ A σ a = {σ'} ⟹ thesis⟧ ⟹ thesis›
  if ‹at_most_1_elem_trans A›
  by (meson at_most_1_elem_trans_def ‹at_most_1_elem_trans A›)+

lemma at_most_1_elem_imp_at_most_1_elem_trans :
  ‹at_most_1_elem A ⟹ at_most_1_elem_trans A›
  by (simp add: at_most_1_elem_def at_most_1_elem_trans_def)



definition length_1_transd :: ‹('σ list, 'a, 'r, 'α) Ad_scheme ⇒ bool›
  where ‹length_1_transd A ≡
         ∀σs a. case τ A σs a of ◇ ⇒ True | ⌊σs'⌋ ⇒ length σs' = Suc 0›

lemma length_1_transdI :
  ‹⟦⋀σs a σs'. τ A σs a = ⌊σs'⌋ ⟹ length σs' = Suc 0⟧ ⟹ length_1_transd A›
  by (simp add: length_1_transd_def split: option.split)

lemma length_1_transdE :
  ‹⟦length_1_transd A; τ A σs a = ⌊σs'⌋; ⋀σ. σs' = [σ] ⟹ thesis⟧ ⟹ thesis›
  by (simp add: length_1_transd_def split: option.split_asm)
    (metis (no_types) length_0_conv length_Suc_conv)


definition length_1_transnd :: ‹('σ list, 'a, 'r, 'α) And_scheme ⇒ bool›
  where ‹length_1_transnd A ≡ ∀σs a. ∀σs' ∈ τ A σs a. length σs' = Suc 0›

lemma length_1_transndI :
  ‹⟦⋀σs a σs'. σs' ∈ τ A σs a ⟹ length σs' = Suc 0⟧ ⟹ length_1_transnd A›
  by (simp add: length_1_transnd_def split: option.split)

lemma length_1_transndE :
  ‹⟦length_1_transnd A; σs' ∈ τ A σs a; ⋀σ. σs' = [σ] ⟹ thesis⟧ ⟹ thesis›
  by (simp add: length_1_transnd_def split: option.split_asm)
    (metis (no_types) length_0_conv length_Suc_conv)


definition length_1d :: ‹('σ list, 'a, 'r list, 'α) Ad_scheme ⇒ bool›
  where ‹length_1d A ≡
         (∀σs a. case τ A σs a of ◇ ⇒ True | ⌊σs'⌋ ⇒ length σs' = Suc 0) ∧
         (∀σs. case ω A σs of ◇ ⇒ True | ⌊rs⌋ ⇒ length rs = Suc 0)›

lemma length_1dI :
  ‹⟦⋀σs a σs'. τ A σs a = ⌊σs'⌋ ⟹ length σs' = Suc 0;
    ⋀σs rs. ω A σs = ⌊rs⌋ ⟹ length rs = Suc 0⟧ ⟹ length_1d A›
  by (simp add: length_1d_def split: option.split)

lemma length_1dE :
  ‹⟦length_1d A; τ A σs a = ⌊σs'⌋; ⋀σ. σs' = [σ] ⟹ thesis⟧ ⟹ thesis›
  ‹⟦length_1d A; ω A σs = ⌊rs⌋; ⋀r. rs = [r] ⟹ thesis⟧ ⟹ thesis›
  by (simp add: length_1d_def split: option.split_asm,
      metis (no_types) length_0_conv length_Suc_conv)+


definition length_1nd :: ‹('σ list, 'a, 'r list, 'α) And_scheme ⇒ bool›
  where ‹length_1nd A ≡ (∀σs a. ∀σs' ∈ τ A σs a. length σs' = Suc 0) ∧
                        (∀σs. ∀rs ∈ ω A σs. length rs = Suc 0)›

lemma length_1ndI :
  ‹⟦⋀σs a σs'. σs' ∈ τ A σs a ⟹ length σs' = Suc 0;
    ⋀σs rs. rs ∈ ω A σs ⟹ length rs = Suc 0⟧ ⟹ length_1nd A›
  by (simp add: length_1nd_def split: option.split)

lemma length_1ndE :
  ‹⟦length_1nd A; σs' ∈ τ A σs a; ⋀σ. σs' = [σ] ⟹ thesis⟧ ⟹ thesis›
  ‹⟦length_1nd A; rs ∈ ω A σs; ⋀r. rs = [r] ⟹ thesis⟧ ⟹ thesis›
  by (simp add: length_1nd_def split: option.split_asm,
      metis (no_types) length_0_conv length_Suc_conv)+

(* abbreviation card_trans_le1 :: ‹('σ, 'a, 'r, 'α) And_scheme ⇒ bool›
  where ‹card_trans_le1 A ≡ ∀s e. card (τ A s e) ≤ Suc 0›

lemma finite_trans_conj_card_trans_le1_is:
  ‹finite_trans A ∧ card_trans_le1 A ⟷ (∀s e.  τ A s e = {} ∨ (∃!t. τ A s e = {t}))›
  by (auto, metis card_1_singleton_iff card_mono empty_subsetI insert_subset le_antisym,
      metis finite.simps, metis card_1_singleton_iff card_eq_0_iff le_eq_less_or_eq less_Suc_eq_le)

lemma finite_trans_imp_card_trans_le1_is:
  ‹finite_trans A ⟹ card_trans_le1 A ⟷ (∀s e.  τ A s e = {} ∨ (∃!t. τ A s e = {t}))›
  by (simp add: finite_trans_conj_card_trans_le1_is[symmetric]) *)


(*when this hypothesis is not verified, the product of two deterministic automata can become non deterministic*)
definition indep_enabl :: ‹('σ0, 'a, 'r0, 'α) Ad_scheme ⇒ 'σ0 ⇒ 'a set ⇒ ('σ1, 'a, 'r1, 'β) Ad_scheme ⇒ 'σ1 ⇒ bool›
  where ‹indep_enabl A0 σ0 E A1 σ1 ≡ ∀t0 ∈ ℛd A0 σ0. ∀t1 ∈ ℛd A1 σ1. ε A0 t0 ∩ ε A1 t1 ⊆ E›

lemma indep_enablI :
  ‹(⋀t0 t1. t0 ∈ ℛd A0 σ0 ⟹ t1 ∈ ℛd A1 σ1 ⟹ ε A0 t0 ∩ ε A1 t1 ⊆ E)
   ⟹ indep_enabl A0 σ0 E A1 σ1›
  and indep_enablD :
  ‹⟦indep_enabl A0 σ0 E A1 σ1; t0 ∈ ℛd A0 σ0; t1 ∈ ℛd A1 σ1⟧ ⟹ ε A0 t0 ∩ ε A1 t1 ⊆ E›
  by (simp_all add: indep_enabl_def)


definition ρ_disjoint_ε :: ‹('σ, 'a, 'σ', 'r', 'α) A_scheme ⇒ bool›
  where ‹ρ_disjoint_ε A ≡ ∀σ ∈ ρ A. ε A σ = {}›

lemma ρ_disjoint_εI : ‹(⋀σ. σ ∈ ρ A ⟹ ε A σ = {}) ⟹ ρ_disjoint_ε A›
  and ρ_disjoint_εD : ‹ρ_disjoint_ε A ⟹ σ ∈ ρ A ⟹ ε A σ = {}›
  by (simp_all add: ρ_disjoint_ε_def)



definition at_most_1_elem_term :: ‹('σ, 'a, 'r, 'α) And_scheme ⇒ bool›
  where ‹at_most_1_elem_term A ≡ ∀σ. ω A σ = {} ∨ (∃r. ω A σ = {r})›

lemma at_most_1_elem_term_def_bis :
  ‹at_most_1_elem_term A ⟷ (∀σ. ∃r. ω A σ ⊆ {r})›
  by (auto simp add: at_most_1_elem_term_def subset_iff)
    (metis empty_iff singleton_iff,
      metis equals0D is_singletonI' is_singleton_some_elem)

lemma at_most_1_elem_termI :
  ‹⟦⋀σ. ω A σ = {} ∨ (∃r. ω A σ = {r})⟧ ⟹ at_most_1_elem_term A›
  by (simp add: at_most_1_elem_term_def)

lemma at_most_1_elem_termE :
  ‹⟦ω A σ = {} ⟹ thesis; ⋀r. ω A σ = {r} ⟹ thesis⟧ ⟹ thesis›
  if ‹at_most_1_elem_term A›
  by (meson at_most_1_elem_term_def ‹at_most_1_elem_term A›)+

lemma at_most_1_elem_imp_at_most_1_elem_term :
  ‹at_most_1_elem A ⟹ at_most_1_elem_term A›
  by (simp add: at_most_1_elem_def at_most_1_elem_term_def)




section ‹First Properties›

subsection ‹const‹ε›, const‹ρ› and const‹ω› first equalities›

lemma base_trans_ε[simp]:
  ‹ε (⦇τ = λσ a. ◇, ω = λσ. ◇, … = some⦈ :: ('σ, 'a, 'r, 'α) Ad_scheme) σ = {}›
  ‹ε (⦇τ = λσ a. {}, ω = λσ. {}, … = some⦈ :: ('σ, 'a, 'r, 'α) And_scheme) σ = {}›
  by (simp_all add: ε_simps)

lemma base_trans_ρ[simp]:
  ‹ρ (⦇τ = λσ a. ◇, ω = λσ. ◇, … = some⦈ :: ('σ, 'a, 'r, 'α) Ad_scheme) = {}›
  ‹ρ (⦇τ = λσ a. {}, ω = λσ. {}, … = some⦈ :: ('σ, 'a, 'r, 'α) And_scheme) = {}›
  by (simp_all add: ρ_simps)


lemma σ_σs_conv_ε[simp]:
  ‹ε d⟪A⟫σ↪σs σs = ε A (hd σs)› ‹ε nd⟪B⟫σ↪σs σs = ε B (hd σs)›
  ‹ε d⟪C⟫σs↝σ σ = ε C [σ]› ‹ε nd⟪D⟫σs↝σ σ = ε D [σ]›
  by (simp_all add: σ_σs_conv_defs ε_simps option.case_eq_if)

lemma σ_σs_conv_ρ[simp]:
  ‹ρ d⟪A⟫σ↪σs = {σs. hd σs ∈ ρ A}› ‹ρ nd⟪B⟫σ↪σs = {σs. hd σs ∈ ρ B}›
  ‹ρ d⟪C⟫σs↝σ = {σ. [σ] ∈ ρ C}› ‹ρ nd⟪D⟫σs↝σ = {σ. [σ] ∈ ρ D}›
  by (simp_all add: σ_σs_conv_defs ρ_simps option.case_eq_if)


lemma singl_list_conv_ε[simp]:
  ‹ε d⟪A⟫singl↪list σs = ε A (hd σs)› ‹ε nd⟪B⟫singl↪list σs = ε B (hd σs)›
  ‹ε d⟪C⟫list↝singl σ = ε C [σ]› ‹ε nd⟪D⟫list↝singl σ = ε D [σ]›
  by (simp_all add: singl_list_conv_defs ε_simps option.case_eq_if)

lemma singl_list_conv_ρ[simp]:
  ‹ρ d⟪A⟫singl↪list = {σs. hd σs ∈ ρ A}› ‹ρ nd⟪B⟫singl↪list = {σs. hd σs ∈ ρ B}›
  ‹ρ d⟪C⟫list↝singl = {σ. [σ] ∈ ρ C}› ‹ρ nd⟪D⟫list↝singl = {σ. [σ] ∈ ρ D}›
  by (simp_all add: singl_list_conv_defs ρ_simps option.case_eq_if)


lemma det_ndet_conv_ε[simp]: ‹ε ⟪A⟫d↪nd = ε A› ‹ε ⟪B⟫nd↝d = ε B›
  by (rule ext, simp add: det_ndet_conv_defs ε_simps option.case_eq_if)+

lemma det_ndet_conv_ρ[simp]: ‹ρ ⟪A⟫d↪nd = ρ A› ‹ρ ⟪B⟫nd↝d = ρ B›
  by (simp_all add: det_ndet_conv_defs ρ_simps option.case_eq_if)

lemma ω_from_det_to_ndet :
  ‹ω ⟪A⟫d↪nd = (λσ. case ω A σ of ⌊r⌋ ⇒ {r} | ◇ ⇒ {})›
  by (auto simp add: det_ndet_conv_defs)


lemma ε_ω_useless [simp] :
  ‹ε (A⦇ω := some_ω⦈) = ε A› ‹ε (B⦇ω := some_ω'⦈) = ε B›
  for A :: ‹('σ, 'a, 'σ option, 'r option, 'α) A_scheme›
    and B :: ‹('σ, 'a, 'σ set, 'r set, 'α) A_scheme›
  by (rule ext, simp add: ε_simps)+

lemma ρ_disjoint_ε_updated_ω [simp] :
  ‹ρ_disjoint_ε (A⦇ω := λσ. ◇⦈)›
  ‹ρ_disjoint_ε (B⦇ω := λσ. {}⦈)›
  by (simp_all add: ρ_disjoint_ε_def ρ_simps)

lemma ρ_disjoint_ε_det_ndet_conv_iff [simp] :
  ‹ρ_disjoint_ε ⟪A⟫d↪nd ⟷ ρ_disjoint_ε A›
  ‹ρ_disjoint_ε ⟪B⟫nd↝d ⟷ ρ_disjoint_ε B›
  by (simp_all add: ρ_disjoint_ε_def)

lemma at_most_1_elem_term_updated_ω [simp] :
  ‹at_most_1_elem_term (A⦇ω := λσ. {}⦈)›
  by (simp add: at_most_1_elem_term_def)

lemma at_most_1_elem_term_from_det_to_ndet [simp] :
  ‹at_most_1_elem_term ⟪A⟫d↪nd›
  by (simp add: det_ndet_conv_defs at_most_1_elem_term_def split: option.split)

lemma at_most_1_elem_term_unit [simp] :
  ‹at_most_1_elem_term (A :: ('σ, 'a, unit, 'α) And_scheme)›
  by (auto simp add: at_most_1_elem_term_def)



subsection ‹Properties of our morphisms›

method expand_A_scheme =
  match conclusion in ‹A = B› for A B :: ‹('σ, 'a, 'σ', 'r', 'α) A_scheme› ⇒
  ‹cases A, cases B›


lemma base_trans_det_ndet_conv:
  ‹⟪⦇τ = λσ a. ◇, ω = λσ. ◇, … = some⦈⟫d↪nd =
    ⦇τ = λσ a. {}, ω = λσ. {}, … = some⦈›
  ‹⟪⦇τ = λσ a. {}, ω = λσ. {}, … = some⦈⟫nd↝d =
   ⦇τ = λσ a. ◇, ω = λσ. ◇, … = some⦈›
  unfolding det_ndet_conv_defs by simp_all


lemma from_det_to_ndet_σ_σs_conv_commute:
  ‹nd⟪⟪A⟫d↪nd⟫σ↪σs = ⟪d⟪A⟫σ↪σs⟫d↪nd› ‹nd⟪⟪B⟫d↪nd⟫σs↝σ = ⟪d⟪B⟫σs↝σ⟫d↪nd›
  by (simp add: det_ndet_conv_defs σ_σs_conv_defs, rule ext,
      auto simp add: option.case_eq_if split: if_splits)+

lemma from_det_to_ndet_singl_list_conv_commute:
  ‹nd⟪⟪A⟫d↪nd⟫singl↪list = ⟪d⟪A⟫singl↪list⟫d↪nd› ‹nd⟪⟪B⟫d↪nd⟫list↝singl = ⟪d⟪B⟫list↝singl⟫d↪nd›
  by (simp add: det_ndet_conv_defs singl_list_conv_defs,
      solves ‹intro conjI ext, auto split: option.split›)+


lemma from_ndet_to_det_σ_σs_conv_commute:
  ‹at_most_1_elem_trans A ⟹ d⟪⟪A⟫nd↝d⟫σ↪σs = ⟪nd⟪A⟫σ↪σs⟫nd↝d›
  ‹at_most_1_elem_trans B ⟹ d⟪⟪B⟫nd↝d⟫σs↝σ = ⟪nd⟪B⟫σs↝σ⟫nd↝d›
proof -
  assume * : ‹at_most_1_elem_trans A›
  from "*" have ‹τ d⟪⟪A⟫nd↝d⟫σ↪σs σs a = τ ⟪nd⟪A⟫σ↪σs⟫nd↝d σs a› for σs a
    by (auto simp add: det_ndet_conv_defs σ_σs_conv_defs
        elim: at_most_1_elem_transE)
  moreover have ‹ω d⟪⟪A⟫nd↝d⟫σ↪σs σs = ω ⟪nd⟪A⟫σ↪σs⟫nd↝d σs› for σs
    by (auto simp add: det_ndet_conv_defs σ_σs_conv_defs)
  moreover have ‹more d⟪⟪A⟫nd↝d⟫σ↪σs = more ⟪nd⟪A⟫σ↪σs⟫nd↝d› by simp
  ultimately show ‹d⟪⟪A⟫nd↝d⟫σ↪σs = ⟪nd⟪A⟫σ↪σs⟫nd↝d› by expand_A_scheme auto
next
  assume * : ‹at_most_1_elem_trans B›
  from "*" have ‹τ d⟪⟪B⟫nd↝d⟫σs↝σ σ a = τ ⟪nd⟪B⟫σs↝σ⟫nd↝d σ a› for σ a
    by (auto simp add: det_ndet_conv_defs σ_σs_conv_defs
        elim: at_most_1_elem_transE)
  moreover have ‹ω d⟪⟪B⟫nd↝d⟫σs↝σ σ = ω ⟪nd⟪B⟫σs↝σ⟫nd↝d σ› for σ
    by (auto simp add: det_ndet_conv_defs σ_σs_conv_defs)
  moreover have ‹more d⟪⟪B⟫nd↝d⟫σs↝σ = more ⟪nd⟪B⟫σs↝σ⟫nd↝d› by simp
  ultimately show ‹d⟪⟪B⟫nd↝d⟫σs↝σ = ⟪nd⟪B⟫σs↝σ⟫nd↝d› by expand_A_scheme auto
qed

lemma from_ndet_to_det_singl_list_conv_commute:
  ‹at_most_1_elem A ⟹ d⟪⟪A⟫nd↝d⟫singl↪list = ⟪nd⟪A⟫singl↪list⟫nd↝d›
  ‹at_most_1_elem B ⟹ d⟪⟪B⟫nd↝d⟫list↝singl = ⟪nd⟪B⟫list↝singl⟫nd↝d›
proof -
  assume * : ‹at_most_1_elem A›
  from "*" have ‹τ d⟪⟪A⟫nd↝d⟫singl↪list σs a = τ ⟪nd⟪A⟫singl↪list⟫nd↝d σs a› for σs a
    by (auto simp add: det_ndet_conv_defs singl_list_conv_defs
        elim: at_most_1_elemE(1))
  moreover from "*" have ‹ω d⟪⟪A⟫nd↝d⟫singl↪list σs = ω ⟪nd⟪A⟫singl↪list⟫nd↝d σs› for σs
    by (auto simp add: det_ndet_conv_defs singl_list_conv_defs
        elim: at_most_1_elemE(2))
  moreover have ‹more d⟪⟪A⟫nd↝d⟫singl↪list = more ⟪nd⟪A⟫singl↪list⟫nd↝d› by simp
  ultimately show ‹d⟪⟪A⟫nd↝d⟫singl↪list = ⟪nd⟪A⟫singl↪list⟫nd↝d› by expand_A_scheme auto
next
  assume * : ‹at_most_1_elem B›
  from "*" have ‹τ d⟪⟪B⟫nd↝d⟫list↝singl σ a = τ ⟪nd⟪B⟫list↝singl⟫nd↝d σ a› for σ a
    by (auto simp add: det_ndet_conv_defs singl_list_conv_defs
        elim: at_most_1_elemE(1))
  moreover from "*" have ‹ω d⟪⟪B⟫nd↝d⟫list↝singl σ = ω ⟪nd⟪B⟫list↝singl⟫nd↝d σ› for σ
    by (auto simp add: det_ndet_conv_defs singl_list_conv_defs
        elim: at_most_1_elemE(2))
  moreover have ‹more d⟪⟪B⟫nd↝d⟫list↝singl = more ⟪nd⟪B⟫list↝singl⟫nd↝d› by simp
  ultimately show ‹d⟪⟪B⟫nd↝d⟫list↝singl = ⟪nd⟪B⟫list↝singl⟫nd↝d› by expand_A_scheme auto
qed



lemma behaviour_σ_σs_conv:
  ‹ε d⟪A⟫σ↪σs [σ] = ε A σ›
  ‹τ d⟪A⟫σ↪σs [σ] a = (case τ A σ a of ◇ ⇒ ◇ | ⌊t⌋ ⇒ ⌊[t]⌋)›
  ‹ρ d⟪A⟫σ↪σs = {σs. hd σs ∈ ρ A}›
  ‹ω d⟪A⟫σ↪σs [σ] = ω A σ›
  ‹ε nd⟪B⟫σ↪σs [σ] = ε B σ›
  ‹τ nd⟪B⟫σ↪σs [σ] a = {[σ'] |σ'. σ' ∈ τ B σ a}›
  ‹ρ nd⟪B⟫σ↪σs = {σs. hd σs ∈ ρ B}›
  ‹ω nd⟪B⟫σ↪σs [σ] = ω B σ›
  ‹ε d⟪C⟫σs↝σ σ = ε C [σ]›
  ‹τ d⟪C⟫σs↝σ σ a = (case τ C [σ] a of ◇ ⇒ ◇ | ⌊σs'⌋ ⇒ ⌊hd σs'⌋)›
  ‹ρ d⟪C⟫σs↝σ = {σ. [σ] ∈ ρ C}›
  ‹ω d⟪C⟫σs↝σ σ = ω C [σ]›
  ‹ε nd⟪D⟫σs↝σ σ = ε D [σ]›
  ‹τ nd⟪D⟫σs↝σ σ a = {hd σs'| σs'. σs' ∈ τ D [σ] a}›
  ‹ρ nd⟪D⟫σs↝σ = {σ. [σ] ∈ ρ D}› ‹ω nd⟪D⟫σs↝σ σ = ω D [σ]›
  by simp_all (simp_all add: σ_σs_conv_defs)


lemma behaviour_singl_list_conv:
  ‹ε d⟪A⟫singl↪list [σ] = ε A σ›
  ‹τ d⟪A⟫singl↪list [σ] a = (case τ A σ a of ◇ ⇒ ◇ | ⌊t⌋ ⇒ ⌊[t]⌋)›
  ‹ρ d⟪A⟫singl↪list = {σs. hd σs ∈ ρ A}›
  ‹ω d⟪A⟫singl↪list [σ] = (case ω A σ of ◇ ⇒ ◇ | ⌊r⌋ ⇒ ⌊[r]⌋)›
  ‹ε nd⟪B⟫singl↪list [σ] = ε B σ›
  ‹τ nd⟪B⟫singl↪list [σ] a = {[σ'] |σ'. σ' ∈ τ B σ a}›
  ‹ρ nd⟪B⟫singl↪list = {σs. hd σs ∈ ρ B}›
  ‹ω nd⟪B⟫singl↪list [σ] = {[r] |r. r ∈ ω B σ}›
  ‹ε d⟪C⟫list↝singl σ = ε C [σ]›
  ‹τ d⟪C⟫list↝singl σ a = (case τ C [σ] a of ◇ ⇒ ◇ | ⌊σs'⌋ ⇒ ⌊hd σs'⌋)›
  ‹ρ d⟪C⟫list↝singl = {σ. [σ] ∈ ρ C}›
  ‹ω d⟪C⟫list↝singl σ = (case ω C [σ] of ◇ ⇒ ◇ | ⌊rs⌋ ⇒ ⌊hd rs⌋)›
  ‹ε nd⟪D⟫list↝singl σ = ε D [σ]›
  ‹τ nd⟪D⟫list↝singl σ a = {hd σs'| σs'. σs' ∈ τ D [σ] a}›
  ‹ρ nd⟪D⟫list↝singl = {σ. [σ] ∈ ρ D}›
  ‹ω nd⟪D⟫list↝singl σ = {hd rs |rs. rs ∈ ω D [σ]}›
  by simp_all (simp_all add: singl_list_conv_defs)


lemma empty_from_det_to_ndet_is_None_trans [simp] : ‹τ ⟪A⟫d↪nd σ a = {} ⟷ τ A σ a = ◇›
  by (simp add: ε_simps det_ndet_conv_defs option.case_eq_if)


lemma at_most_1_elem_from_det_to_ndet [simp] : ‹at_most_1_elem ⟪A⟫d↪nd›
  by (rule at_most_1_elemI)
    (simp_all add: det_ndet_conv_defs split: option.split)


lemma from_ndet_to_det_from_det_to_ndet [simp] : ‹⟪⟪A⟫d↪nd⟫nd↝d = A›
  by (cases A, simp add: det_ndet_conv_defs)
    (intro conjI ext, simp_all split: option.split)

lemma from_det_to_ndet_from_ndet_to_det [simp] :
  ‹⟪⟪A⟫nd↝d⟫d↪nd = A› if ‹at_most_1_elem A›
proof -
  from that have ‹τ ⟪⟪A⟫nd↝d⟫d↪nd σ a = τ A σ a› for σ a
    by (auto simp add: det_ndet_conv_defs elim: at_most_1_elemE(1))
  moreover from that have ‹ω ⟪⟪A⟫nd↝d⟫d↪nd σ = ω A σ› for σ
    by (auto simp add: det_ndet_conv_defs elim: at_most_1_elemE(2))
  moreover have ‹more ⟪⟪A⟫nd↝d⟫d↪nd = more A› by simp
  ultimately show ‹⟪⟪A⟫nd↝d⟫d↪nd = A› by expand_A_scheme fastforce
qed


theorem bij_betw_from_det_to_ndet :
  ‹bij_betw (λA. ⟪A⟫d↪nd) UNIV {A. at_most_1_elem A}›
  unfolding bij_betw_iff_bijections
  by (rule exI[where x = ‹λA. ⟪A⟫nd↝d›]) simp

lemma bij_betw_from_ndet_to_det :
  ‹bij_betw (λA. ⟪A⟫nd↝d) {A. at_most_1_elem A} UNIV›
  unfolding bij_betw_iff_bijections
  by (rule exI[where x = ‹λA. ⟪A⟫d↪nd›]) simp


lemma length_1_trans_from_σ_to_σs [simp] :
  ‹length_1_transd d⟪A⟫σ↪σs› ‹length_1_transnd nd⟪B⟫σ↪σs›
  by (rule length_1_transdI, solves ‹auto simp add: σ_σs_conv_defs split: option.split_asm›)
    (rule length_1_transndI, solves ‹auto simp add: σ_σs_conv_defs split: option.split_asm›)

lemma τ_hd_from_σ_to_σs_eq [simp] :
  ‹τ d⟪A⟫σ↪σs [hd σs] a = τ d⟪A⟫σ↪σs σs a›
  ‹τ nd⟪B⟫σ↪σs [hd σs] a = τ nd⟪B⟫σ↪σs σs a›
  by (simp_all add: σ_σs_conv_defs)

lemma ω_hd_from_σ_to_σs_eq [simp] :
  ‹ω d⟪A⟫σ↪σs [hd σs] = ω d⟪A⟫σ↪σs σs›
  ‹ω nd⟪B⟫σ↪σs [hd σs] = ω nd⟪B⟫σ↪σs σs›
  by (simp_all add: σ_σs_conv_defs)


lemma from_σs_to_σ_from_σ_to_σs [simp] :
  ‹d⟪d⟪A⟫σ↪σs⟫σs↝σ = A› ‹nd⟪nd⟪B⟫σ↪σs⟫σs↝σ = B›
  by (cases A, simp add: σ_σs_conv_defs, intro conjI ext;
      simp add: option.case_eq_if set_eq_iff; metis list.sel(1))
    (cases B, simp add: σ_σs_conv_defs, intro conjI ext;
      simp add: option.case_eq_if set_eq_iff; metis list.sel(1))

lemma from_σ_to_σs_from_σs_to_σ [simp] :
  ‹⟦length_1_transd A; ⋀σs a. τ A [hd σs] a = τ A σs a;
    ⋀σs. ω A [hd σs] = ω A σs⟧ ⟹ d⟪d⟪A⟫σs↝σ⟫σ↪σs = A›
  ‹⟦length_1_transnd B; ⋀σs a. τ B [hd σs] a = τ B σs a;
    ⋀σs. ω B [hd σs] = ω B σs⟧ ⟹ nd⟪nd⟪B⟫σs↝σ⟫σ↪σs = B›
proof -
  assume * : ‹length_1_transd A› ‹⋀σs a. τ A [hd σs] a = τ A σs a›
    ‹⋀σs. ω A [hd σs] = ω A σs›
  from "*"(1) have ‹τ d⟪d⟪A⟫σs↝σ⟫σ↪σs σs a = τ A σs a› for σs a
    by (auto simp add: σ_σs_conv_defs "*"(2) split: option.split
        elim: length_1_transdE)
  moreover have ‹ω d⟪d⟪A⟫σs↝σ⟫σ↪σs σs = ω A σs› for σs
    by (simp add: σ_σs_conv_defs "*"(3))
  moreover have ‹more d⟪d⟪A⟫σs↝σ⟫σ↪σs = more A› by simp
  ultimately show ‹d⟪d⟪A⟫σs↝σ⟫σ↪σs = A› by expand_A_scheme auto
next
  assume * : ‹length_1_transnd B› ‹⋀σs a. τ B [hd σs] a = τ B σs a›
    ‹⋀σs. ω B [hd σs] = ω B σs›
  from "*"(1) have ‹τ nd⟪nd⟪B⟫σs↝σ⟫σ↪σs σs a = τ B σs a› for σs a
    by (auto simp add: σ_σs_conv_defs "*"(2) elim: length_1_transndE)
      (metis length_1_transndE list.sel(1))
  moreover have ‹ω nd⟪nd⟪B⟫σs↝σ⟫σ↪σs σs = ω B σs› for σs
    by (simp add: σ_σs_conv_defs "*"(3))
  moreover have ‹more nd⟪nd⟪B⟫σs↝σ⟫σ↪σs = more B› by simp
  ultimately show ‹nd⟪nd⟪B⟫σs↝σ⟫σ↪σs = B› by expand_A_scheme fastforce
qed

theorem bij_betw_from_σ_to_σs : 
  ‹bij_betw (λA. d⟪A⟫σ↪σs) UNIV
   {A. length_1_transd A ∧ (∀σs a. τ A [hd σs] a = τ A σs a) ∧ (∀σs. ω A [hd σs] = ω A σs)}›
  (is ‹bij_betw (λA. d⟪A⟫σ↪σs) UNIV ?Sd›)
  ‹bij_betw (λB. nd⟪B⟫σ↪σs) UNIV
   {B. length_1_transnd B ∧ (∀σs a. τ B σs a = τ B [hd σs] a) ∧ (∀σs. ω B [hd σs] = ω B σs)}›
  unfolding bij_betw_iff_bijections
  by (rule exI[where x = ‹λA. d⟪A⟫σs↝σ›], simp)
    (rule exI[where x = ‹λA. nd⟪A⟫σs↝σ›], simp)


lemma bij_betw_from_σs_to_σ : 
  ‹bij_betw (λA. d⟪A⟫σs↝σ)
   {A. length_1_transd A ∧ (∀σs a. τ A [hd σs] a = τ A σs a) ∧ (∀σs. ω A [hd σs] = ω A σs)} UNIV›
  ‹bij_betw (λB. nd⟪B⟫σs↝σ)
   {B. length_1_transnd B ∧ (∀σs a. τ B σs a = τ B [hd σs] a) ∧ (∀σs. ω B [hd σs] = ω B σs)} UNIV›
  unfolding bij_betw_iff_bijections
  by (rule exI[where x = ‹λA. d⟪A⟫σ↪σs›], simp)
    (rule exI[where x = ‹λA. nd⟪A⟫σ↪σs›], simp)



lemma length_1_from_singl_to_list [simp] :
  ‹length_1d d⟪A⟫singl↪list› ‹length_1nd nd⟪B⟫singl↪list›
  by (rule length_1dI; solves ‹auto simp add: singl_list_conv_defs split: option.split_asm›)
    (rule length_1ndI; solves ‹auto simp add: singl_list_conv_defs split: option.split_asm›)

lemma τ_hd_from_singl_to_list_eq [simp] :
  ‹τ d⟪A⟫singl↪list [hd σs] a = τ d⟪A⟫singl↪list σs a›
  ‹τ nd⟪B⟫singl↪list [hd σs] a = τ nd⟪B⟫singl↪list σs a›
  by (simp_all add: singl_list_conv_defs)

lemma ω_hd_from_singl_to_list_eq [simp] :
  ‹ω d⟪A⟫singl↪list [hd σs] = ω d⟪A⟫singl↪list σs›
  ‹ω nd⟪B⟫singl↪list [hd σs] = ω nd⟪B⟫singl↪list σs›
  by (simp_all add: singl_list_conv_defs)


lemma from_list_to_singl_from_singl_to_list [simp] :
  ‹d⟪d⟪A⟫singl↪list⟫list↝singl = A› ‹nd⟪nd⟪B⟫singl↪list⟫list↝singl = B›
  by (cases A, simp add: singl_list_conv_defs, intro conjI ext;
      simp add: option.case_eq_if set_eq_iff; metis list.sel(1))
    (cases B, simp add: singl_list_conv_defs, intro conjI ext;
      simp add: option.case_eq_if set_eq_iff; metis list.sel(1))

lemma from_singl_to_list_from_list_to_singl [simp] :
  ‹⟦length_1d A; ⋀σs a. τ A [hd σs] a = τ A σs a;
    ⋀σs. ω A [hd σs] = ω A σs⟧ ⟹ d⟪d⟪A⟫list↝singl⟫singl↪list = A›
  ‹⟦length_1nd B; ⋀σs a. τ B [hd σs] a = τ B σs a;
    ⋀σs. ω B [hd σs] = ω B σs⟧ ⟹ nd⟪nd⟪B⟫list↝singl⟫singl↪list = B›
proof -
  assume * : ‹length_1d A› ‹⋀σs a. τ A [hd σs] a = τ A σs a›
    ‹⋀σs. ω A [hd σs] = ω A σs›
  from "*"(1) have ‹τ d⟪d⟪A⟫list↝singl⟫singl↪list σs a = τ A σs a› for σs a
    by (auto simp add: singl_list_conv_defs "*"(2)
        split: option.split elim: length_1dE(1))
  moreover from "*"(1) have ‹ω d⟪d⟪A⟫list↝singl⟫singl↪list σs = ω A σs› for σs
    by (auto simp add: singl_list_conv_defs "*"(3)
        split: option.split elim: length_1dE(2))
  moreover have ‹more d⟪d⟪A⟫list↝singl⟫singl↪list = more A› by simp
  ultimately show ‹d⟪d⟪A⟫list↝singl⟫singl↪list = A› by expand_A_scheme auto
next
  assume * : ‹length_1nd B› ‹⋀σs a. τ B [hd σs] a = τ B σs a›
    ‹⋀σs. ω B [hd σs] = ω B σs›
  from "*"(1) have ‹τ nd⟪nd⟪B⟫list↝singl⟫singl↪list σs a = τ B σs a› for σs a
    by (auto simp add: singl_list_conv_defs "*"(2) elim: length_1ndE(1))
      (metis length_1ndE(1) list.sel(1))
  moreover from "*"(1) have ‹ω nd⟪nd⟪B⟫list↝singl⟫singl↪list σs = ω B σs› for σs
    by (auto simp add: singl_list_conv_defs "*"(3) elim: length_1ndE(2))
      (metis length_1ndE(2) list.sel(1))
  moreover have ‹more nd⟪nd⟪B⟫list↝singl⟫singl↪list = more B› by simp
  ultimately show ‹nd⟪nd⟪B⟫list↝singl⟫singl↪list = B› by expand_A_scheme fastforce
qed


theorem bij_betw_from_singl_to_list : 
  ‹bij_betw (λA. d⟪A⟫singl↪list) UNIV
   {A. length_1d A ∧ (∀σs a. τ A [hd σs] a = τ A σs a) ∧ (∀σs. ω A [hd σs] = ω A σs)}›
  (is ‹bij_betw (λA. d⟪A⟫singl↪list) UNIV ?Sd›)
  ‹bij_betw (λB. nd⟪B⟫singl↪list) UNIV
   {B. length_1nd B ∧ (∀σs a. τ B σs a = τ B [hd σs] a) ∧ (∀σs. ω B [hd σs] = ω B σs)}›
  unfolding bij_betw_iff_bijections
  by (rule exI[where x = ‹λA. d⟪A⟫list↝singl›], simp)
    (rule exI[where x = ‹λA. nd⟪A⟫list↝singl›], simp)

lemma bij_betw_from_list_to_singl : 
  ‹bij_betw (λA. d⟪A⟫list↝singl)
   {A. length_1d A ∧ (∀σs a. τ A [hd σs] a = τ A σs a) ∧ (∀σs. ω A [hd σs] = ω A σs)} UNIV›
  ‹bij_betw (λB. nd⟪B⟫list↝singl)
   {B. length_1nd B ∧ (∀σs a. τ B σs a = τ B [hd σs] a) ∧ (∀σs. ω B [hd σs] = ω B σs)} UNIV›
  unfolding bij_betw_iff_bijections
  by (rule exI[where x = ‹λA. d⟪A⟫singl↪list›], simp)
    (rule exI[where x = ‹λA. nd⟪A⟫singl↪list›], simp)



subsection ‹Reachability results (for const‹ℛd› and const‹ℛnd›)›

lemma ℛ_base_trans[simp]: ‹ℛd  ⦇τ = λσ a. ◇, ω = λσ. ◇, … = some⦈ = (λσ. {σ})›
  ‹ℛnd ⦇τ = λσ a. {}, ω = λσ. {}, … = some⦈ = (λσ. {σ})›
  by (rule ext, safe, subst (asm) ℛd.simps ℛnd.simps, simp_all add: ℛd.init ℛnd.init)+


theorem ℛnd_from_det_to_ndet : ‹ℛnd ⟪A⟫d↪nd σ = ℛd A σ›
proof safe
  show ‹σ' ∈ ℛnd ⟪A⟫d↪nd σ ⟹ σ' ∈ ℛd A σ› for σ'
    by (induct rule: ℛnd.induct, fact ℛd.init, erule ℛd.step)
      (simp add: from_det_to_ndet_def option.case_eq_if split: if_split_asm)
next
  show ‹σ' ∈ ℛd A σ ⟹ σ' ∈ ℛnd ⟪A⟫d↪nd σ› for σ'
    by (induct rule: ℛd.induct, fact ℛnd.init)
      (metis ℛnd.step det_ndet_conv_defs(1) option.case(2) 
        option.set_intros option.simps(15) select_convs(1))
qed


(*TODO: see where this can be useful*)
lemma bij_betw_ℛnd_if_same_τ : ‹bij_betw f (ℛnd B0 σ0) (ℛnd B1 (f σ0))›
  if ‹inj_on f (ℛnd B0 σ0)› and ‹⋀σ0' a. σ0' ∈ ℛnd B0 σ0 ⟹ τ B1 (f σ0') a = f ` τ B0 σ0' a›
proof (rule bij_betw_imageI, fact that(1), auto simp add: image_def, goal_cases)
  show ‹s ∈ ℛnd B0 σ0 ⟹ f s ∈ ℛnd B1 (f σ0)› for s
    by (induct rule: ℛnd.induct, simp add: ℛnd.init, metis ℛnd.step that(2) image_eqI)
next
  show ‹s ∈ ℛnd B1 (f σ0) ⟹ ∃t ∈ ℛnd B0 σ0. s = f t› for s
    by (induct rule: ℛnd.induct, metis ℛnd.simps, metis (mono_tags, lifting) ℛnd.step that(2) image_iff)
qed

lemma bij_betw_ℛd_if_same_τ: ‹bij_betw f (ℛd A0 σ0) (ℛd A1 (f σ0))›
  if ‹inj_on f (ℛd A0 σ0)› and ‹⋀σ0' a. σ0' ∈ ℛd A0 σ0 ⟹ τ A1 (f σ0') a = map_option f (τ A0 σ0' a)›
  by (subst (1 2) ℛnd_from_det_to_ndet[symmetric], rule bij_betw_ℛnd_if_same_τ)
    (simp_all add: ℛnd_from_det_to_ndet that(1),
      simp add: det_ndet_conv_defs that(2) option.case_eq_if map_option_case)

lemmas same_τ_implies_same_ℛnd = bij_betw_ℛnd_if_same_τ[where f = id, simplified bij_betw_def, simplified]
  and same_τ_implies_same_ℛd = bij_betw_ℛd_if_same_τ[where f = id, simplified bij_betw_def option.map_id, simplified]

corollary ℛd_ω_useless [simp] : ‹ℛd (A⦇ω := some_ω⦈) σ = ℛd A σ›
  by (auto intro!: same_τ_implies_same_ℛd)

corollary ℛnd_ω_useless [simp] : ‹ℛnd (A⦇ω := some_ω⦈) σ = ℛnd A σ›
  by (auto intro!: same_τ_implies_same_ℛnd)

corollary indep_enabl_ω_useless [simp] :
  ‹indep_enabl (A0⦇ω := some_ω⦈) σ0 E A1 σ1 ⟷ indep_enabl A0 σ0 E A1 σ1›
  ‹indep_enabl A0 σ0 E (A1⦇ω := some_ω⦈) σ1 ⟷ indep_enabl A0 σ0 E A1 σ1›
  by (simp_all add: indep_enabl_def)


method ℛ_subset_method uses defs opt induct init simps = 
  induct rule: induct, auto simp add: init defs ε_simps split: if_splits,
  (metis (no_types, opaque_lifting) simps)+

method ℛd_subset_method uses defs opt =
  ℛ_subset_method defs: defs opt: opt induct: ℛd.induct init: ℛd.init simps: ℛd.simps

method ℛnd_subset_method uses defs opt =
  ℛ_subset_method defs: defs opt: opt induct: ℛnd.induct init: ℛnd.init simps: ℛnd.simps


lemma ℛnd_from_σ_to_σs_description: ‹ℛnd nd⟪B⟫σ↪σs [σ] = {[σ']| σ'. σ' ∈ ℛnd B σ}›
proof safe
  show ‹σs ∈ ℛnd nd⟪B⟫σ↪σs [σ] ⟹ ∃σ'. σs = [σ'] ∧ σ' ∈ ℛnd B σ› for σs
    by (induct rule: ℛnd.induct, auto simp add: ℛnd.init behaviour_σ_σs_conv(6), metis ℛnd.step)
next
  show ‹σ' ∈ ℛnd B σ ⟹ [σ'] ∈ ℛnd nd⟪B⟫σ↪σs [σ]› for σ'
    by (induct rule: ℛnd.induct) (simp_all add: ℛnd.init ℛnd.step behaviour_σ_σs_conv(6))
qed


lemma ℛd_from_σ_to_σs_description: ‹ℛd d⟪A⟫σ↪σs [σ] = {[σ']| σ'. σ' ∈ ℛd A σ}›
  by (simp add: ℛnd_from_σ_to_σs_description
      flip: ℛnd_from_det_to_ndet from_det_to_ndet_σ_σs_conv_commute(1))


lemma ℛnd_from_singl_to_list_description: ‹ℛnd nd⟪B⟫singl↪list [σ] = {[σ']| σ'. σ' ∈ ℛnd B σ}›
proof safe
  show ‹σs ∈ ℛnd nd⟪B⟫singl↪list [σ] ⟹ ∃σ'. σs = [σ'] ∧ σ' ∈ ℛnd B σ› for σs
    by (induct rule: ℛnd.induct, auto simp add: ℛnd.init behaviour_singl_list_conv(6), metis ℛnd.step)
next
  show ‹σ' ∈ ℛnd B σ ⟹ [σ'] ∈ ℛnd nd⟪B⟫singl↪list [σ]› for σ'
    by (induct rule: ℛnd.induct) (simp_all add: ℛnd.init ℛnd.step behaviour_singl_list_conv(6))
qed


lemma ℛd_from_singl_to_list_description: ‹ℛd d⟪A⟫singl↪list [σ] = {[σ']| σ'. σ' ∈ ℛd A σ}›
  by (simp add: ℛnd_from_singl_to_list_description
      flip: ℛnd_from_det_to_ndet from_det_to_ndet_singl_list_conv_commute(1))



lemma length_ℛd_from_σ_to_σs:
  ‹σs' ∈ ℛd d⟪A⟫σ↪σs σs ⟹ σs' = σs ∨ length σs' = 1›  
  by (simp add: σ_σs_conv_defs)
    (induct rule: ℛd.induct, simp_all split: option.split_asm)

lemma length_ℛnd_from_σ_to_σs:
  ‹σs' ∈ ℛnd nd⟪B⟫σ↪σs σs ⟹ σs' = σs ∨ length σs' = 1›
  by (simp add: σ_σs_conv_defs)
    (induct rule: ℛnd.induct, auto)

lemma length_ℛd_from_singl_to_list:
  ‹σs' ∈ ℛd d⟪A⟫singl↪list σs ⟹ σs' = σs ∨ length σs' = 1›
  by (simp add: singl_list_conv_defs)
    (induct rule: ℛd.induct, simp_all split: option.split_asm)

lemma length_ℛnd_from_singl_to_list:
  ‹σs' ∈ ℛnd nd⟪B⟫singl↪list σs ⟹ σs' = σs ∨ length σs' = 1›
  by (simp add: singl_list_conv_defs)
    (induct rule: ℛnd.induct, auto)



section ‹Normalization› 

subsection ‹Non-deterministic Case›

text ‹First version, without final state notion›

abbreviation P_nd_step :: ‹[('σ, 'a) enabl, ('σ, 'a) transnd, 'σ ⇒ ('a, 'r) processptick, 'σ] ⇒ ('a, 'r) processptick›
  where ‹P_nd_step εA τA X σ ≡ □ e ∈ εA σ → ⊓ σ' ∈ τA σ e. X σ'›

definition P_nd :: ‹('σ, 'a, 'r, 'α) And_scheme ⇒ 'σ ⇒ ('a, 'r) processptick› (‹P⟪_⟫nd› 1000)
  where ‹P⟪A⟫nd ≡ υ X. P_nd_step (ε A) (τ A) X›


lemma P_nd_step_constructive [simp] : ‹constructive (P_nd_step εA τA)› by simp

lemma P_nd_step_cont [simp] : ‹∀σ a. finite (τA σ a) ⟹ cont (P_nd_step εA τA)›
  by (simp add: cont_fun)

lemma P_nd_step_constructive_bis : ‹constructive (P_nd_step (ε A) (τ A))› by simp

lemma P_nd_step_cont_bis [simp] : ‹finite_trans A ⟹ cont (P_nd_step (ε A) (τ A))›
  by (simp add: finite_trans_def)

lemma P_nd_rec: ‹P⟪A⟫nd = (λσ. P_nd_step (ε A) (τ A) P⟪A⟫nd σ)›
  by (unfold P_nd_def, rule ext, subst restriction_fix_eq, simp_all)

lemma P_nd_is_fix : ‹finite_trans A ⟹ P⟪A⟫nd = (μ X. P_nd_step (ε A) (τ A) X)›
  by (simp add: P_nd_def restriction_fix_is_fix)

lemma non_destructive_imp_restriction_cont [simp] :
  ‹non_destructive f ⟹ restriction_cont f›
  by (simp add: non_destructive_on_def)



lemma P_nd_ω_useless: ‹P⟪A⟫nd = P⟪A⦇ω := some_ω⦈⟫nd›
  by (simp add: P_nd_def ε_simps)

lemma P_nd_ω_useless_bis : ‹P⟪A⟫nd = P⟪A⦇ω := λσ. {}⦈⟫nd›
  by (fact P_nd_ω_useless)

lemma P_nd_induct [case_names adm base step] :
  ‹adm↓ P ⟹ P σ ⟹ (⋀X. P X ⟹ P (P_nd_step (ε A) (τ A) X)) ⟹ P P⟪A⟫nd›
  unfolding P_nd_def
  by (rule restriction_fix_ind[OF P_nd_step_constructive_bis]) simp_all

lemma P_nd_induct_iterated [consumes 1, case_names adm base step] :
  ‹⟦0 < k; adm↓ P; P σ; ⋀X. P X ⟹ P ((P_nd_step (ε A) (τ A) ^^ k) X)⟧ ⟹ P P⟪A⟫nd›
  unfolding P_nd_def
  by (rule restriction_fix_ind_iterated[where f = ‹P_nd_step (ε A) (τ A)›]) auto



text ‹New version with final state notion where we just have const‹SKIPS›.›

abbreviation PSKIPS_nd_step ::
  ‹[('σ, 'a) enabl, ('σ, 'a) transnd, 'σ ⇒ 'r set, 'σ ⇒ ('a, 'r) processptick, 'σ] ⇒ ('a, 'r) processptick›
  where ‹PSKIPS_nd_step εA τA ωA X σ ≡ if ωA σ = {} then P_nd_step εA τA X σ else SKIPS (ωA σ)›

definition PSKIPS_nd :: ‹('σ, 'a, 'r, 'α) And_scheme ⇒ 'σ ⇒ ('a, 'r) processptick› (‹PSKIPS⟪_⟫nd› 1000)
  where ‹PSKIPS⟪A⟫nd ≡ υ X. PSKIPS_nd_step (ε A) (τ A) (ω A) X›



lemma PSKIPS_nd_step_constructive [simp] : ‹constructive (PSKIPS_nd_step εA τA ωA)› by auto


lemma PSKIPS_nd_step_cont [simp] : ‹∀σ a. finite (τA σ a) ⟹ cont (PSKIPS_nd_step εA τA ωA)›
  by (simp add: cont_fun)

lemma PSKIPS_nd_step_constructive_bis : ‹constructive (PSKIPS_nd_step (ε A) (τ A) (ω A))› by simp

lemma PSKIPS_nd_step_cont_bis [simp] : ‹finite_trans A ⟹ cont (PSKIPS_nd_step (ε A) (τ A) (ω A))›
  by (simp add: finite_trans_def)

lemma PSKIPS_nd_rec: ‹PSKIPS⟪A⟫nd = (λσ. PSKIPS_nd_step (ε A) (τ A) (ω A) PSKIPS⟪A⟫nd σ)›
  by (unfold PSKIPS_nd_def, rule ext, subst restriction_fix_eq, simp_all)

lemma PSKIPS_nd_is_fix : ‹finite_trans A ⟹ PSKIPS⟪A⟫nd = (μ X. PSKIPS_nd_step (ε A) (τ A) (ω A) X)›
  by (simp add: PSKIPS_nd_def restriction_fix_is_fix)

lemma PSKIPS_nd_induct [case_names adm base step] :
  ‹adm↓ P ⟹ P σ ⟹ (⋀X. P X ⟹ P (PSKIPS_nd_step (ε A) (τ A) (ω A) X)) ⟹ P PSKIPS⟪A⟫nd›
  unfolding PSKIPS_nd_def
  by (rule restriction_fix_ind[OF PSKIPS_nd_step_constructive_bis]) simp_all

lemma PSKIPS_nd_induct_iterated [consumes 1, case_names adm base step] :
  ‹⟦0 < k; adm↓ P; P σ; ⋀X. P X ⟹ P ((PSKIPS_nd_step (ε A) (τ A) (ω A) ^^ k) X)⟧ ⟹ P PSKIPS⟪A⟫nd›
  unfolding PSKIPS_nd_def
  by (rule restriction_fix_ind_iterated[where f = ‹PSKIPS_nd_step (ε A) (τ A) (ω A)›]) auto



text ‹Correspondence when we always have term‹ω A σ = {}›.›

lemma PSKIPS_nd_empty_ρ : ‹ρ A = {} ⟹ PSKIPS⟪A⟫nd = P⟪A⟫nd›
  by (simp add: PSKIPS_nd_def P_nd_def ρ_simps)

lemma PSKIPS_nd_updated_ω: ‹P⟪A⟫nd = PSKIPS⟪A⦇ω := λσ. {}⦈⟫nd›
  by (metis (mono_tags, lifting) PSKIPS_nd_empty_ρ P_nd_ω_useless_bis ρnd.simps
      empty_Collect_eq select_convs(2) surjective update_convs(2))

lemma PSKIPS_nd_empty_ρ_inter_ℛnd:
  ‹PSKIPS⟪A⟫nd σ = P⟪A⟫nd σ› if ‹ρ A ∩ ℛnd A σ = {}›
proof -
  have ‹σ' ∈ ℛnd A σ ⟹ PSKIPS⟪A⟫nd σ' = P⟪A⟫nd σ'› for σ'
  proof (induct A arbitrary: σ' rule: PSKIPS_nd_induct)
    case adm show ?case by simp
  next
    case base show ‹P⟪A⟫nd σ' = P⟪A⟫nd σ'› ..
  next
    case (step X)
    from step.prems(1) that have ‹σ' ∉ ρ A› by blast
    hence ‹ω A σ' = {}› by (simp add: ρ_simps)
    thus ?case
      by (subst P_nd_rec, auto intro!: mono_Mprefix_eq mono_GlobalNdet_eq)
        (metis (lifting) ℛnd.simps step.hyps step.prems)
  qed
  thus ‹PSKIPS⟪A⟫nd σ = P⟪A⟫nd σ› by (simp add: ℛnd.init)
qed



lemma PSKIPS_nd_rec_notin_ρ:
  ‹σ ∉ ρ A ⟹ PSKIPS⟪A⟫nd σ = P_nd_step (ε A) (τ A) PSKIPS⟪A⟫nd σ›
  by (subst PSKIPS_nd_rec) (simp add: ρ_simps)

lemma PSKIPS_nd_rec_in_ρ: ‹σ ∈ ρ A ⟹ PSKIPS⟪A⟫nd σ = SKIPS (ω A σ)›
  by (subst PSKIPS_nd_rec, simp add: ρ_simps)



subsection ‹Deterministic Case›

text ‹First version, without final state notion.›

abbreviation P_d_step :: ‹[('σ, 'a) enabl, ('σ, 'a) transd, 'σ ⇒ ('a, 'r) processptick, 'σ] ⇒ ('a, 'r) processptick›
  where ‹P_d_step εA τA X s ≡ □ e ∈ εA s → X ⌈τA s e⌉›

definition P_d :: ‹('σ, 'a, 'r, 'α) Ad_scheme ⇒ 'σ ⇒ ('a, 'r) processptick› (‹P⟪_⟫d› 1000)
  where ‹P⟪A⟫d ≡ υ X. P_d_step (ε A) (τ A) X›


lemma P_d_step_constructive[simp] : ‹constructive (P_d_step εA τA)› by simp

lemmas P_d_step_constructive_bis = P_d_step_constructive[of ‹ε A› ‹τ A›] for A

lemma P_d_step_cont[simp]: ‹cont (P_d_step εA τA)›
  by (simp add: cont_fun)

lemmas P_d_step_cont_bis = P_d_step_cont[of ‹ε A› ‹τ A›] for A

lemma P_d_rec: ‹P⟪A⟫d = (λs. P_d_step (ε A) (τ A) P⟪A⟫d s)›
  by (unfold P_d_def, subst restriction_fix_eq) simp_all

lemma P_d_is_fix : ‹P⟪A⟫d = (μ X. P_d_step (ε A) (τ A) X)›
  by (simp add: P_d_def restriction_fix_is_fix)


lemma P_d_ω_useless: ‹P⟪A⟫d = P⟪A⦇ω := some_ω⦈⟫d›
  by (simp add: P_d_def ε_simps)

lemma P_d_ω_useless_bis: ‹P⟪A⟫d = P⟪A⦇ω := λσ. ◇⦈⟫d›
  by (fact P_d_ω_useless)

lemma P_d_induct [case_names adm base step] :
  ‹⟦adm↓ P; P σ; ⋀X. P X ⟹ P (P_d_step (ε A) (τ A) X)⟧ ⟹ P P⟪A⟫d›
  unfolding P_d_def
  by (rule restriction_fix_ind[OF P_d_step_constructive_bis]) simp_all

lemma P_d_induct_iterated [consumes 1, case_names adm base step] :
  ‹⟦0 < k; adm↓ P; P σ; ⋀X. P X ⟹ P ((P_d_step (ε A) (τ A) ^^ k) X)⟧ ⟹ P P⟪A⟫d›
  unfolding P_d_def
  by (rule restriction_fix_ind_iterated[where f = ‹P_d_step (ε A) (τ A)›]) auto



text ‹New version with final state notion where we just const‹SKIP›.›

abbreviation PSKIPS_d_step ::
  ‹[('σ, 'a) enabl, ('σ, 'a) transd, 'σ ⇒ 'r option, 'σ ⇒ ('a, 'r) processptick, 'σ] ⇒ ('a, 'r) processptick›
  where ‹PSKIPS_d_step εA τA ωA X σ ≡ case ωA σ of ⌊r⌋ ⇒ SKIP r | ◇ ⇒ P_d_step εA τA X σ›

definition PSKIPS_d :: ‹('σ, 'a, 'r, 'α) Ad_scheme ⇒ 'σ ⇒ ('a, 'r) processptick› (‹PSKIPS⟪_⟫d› 1000)
  where ‹PSKIPS⟪A⟫d ≡ υ X. PSKIPS_d_step (ε A) (τ A) (ω A) X›

lemma PSKIPS_d_step_constructive[simp]: ‹constructive (PSKIPS_d_step εA τA 𝒮FA)›
  by (auto simp add: option.case_eq_if)

lemmas PSKIPS_d_step_constructive_bis = PSKIPS_d_step_constructive[of ‹ε A› ‹τ A› ‹ω A›] for A


lemma PSKIPS_d_step_cont[simp]: ‹cont (PSKIPS_d_step εA τA 𝒮FA)›
  by (simp add: cont_fun option.case_eq_if)

lemmas PSKIPS_d_step_cont_bis = PSKIPS_d_step_cont[of ‹ε A› ‹τ A› ‹ω A›] for A

lemma PSKIPS_d_rec: ‹PSKIPS⟪A⟫d = (λσ. PSKIPS_d_step (ε A) (τ A) (ω A) PSKIPS⟪A⟫d σ)›
  by (unfold PSKIPS_d_def, subst restriction_fix_eq) auto

lemma PSKIPS_d_is_fix : ‹PSKIPS⟪A⟫d = (μ X. PSKIPS_d_step (ε A) (τ A) (ω A) X)›
  by (simp add: PSKIPS_d_def restriction_fix_is_fix)


lemma PSKIPS_d_induct [case_names adm base step] :
  ‹adm↓ P ⟹ P σ ⟹ (⋀X. P X ⟹ P (PSKIPS_d_step (ε A) (τ A) (ω A) X)) ⟹ P PSKIPS⟪A⟫d›
  unfolding PSKIPS_d_def
  by (rule restriction_fix_ind[OF PSKIPS_d_step_constructive_bis]) simp_all

lemma PSKIPS_d_induct_iterated [consumes 1, case_names adm base step] :
  ‹⟦0 < k; adm↓ P; P σ; ⋀X. P X ⟹ P ((PSKIPS_d_step (ε A) (τ A) (ω A) ^^ k) X)⟧ ⟹ P PSKIPS⟪A⟫d›
  unfolding PSKIPS_d_def
  by (rule restriction_fix_ind_iterated[where f = ‹PSKIPS_d_step (ε A) (τ A) (ω A)›]) auto



text ‹Correspondence when we always have term‹ω A σ = {}›.›

lemma PSKIPS_d_empty_ρ : ‹ρ A = {} ⟹ PSKIPS⟪A⟫d = P⟪A⟫d›
  by (simp add: ρ_simps P_d_def PSKIPS_d_def)

lemma PSKIPS_d_updated_ω: ‹P⟪A⟫d = PSKIPS⟪A⦇ω := λσ. ◇⦈⟫d›
  by (simp add: PSKIPS_d_empty_ρ P_d_ω_useless ρ_simps)


lemma PSKIPS_d_empty_ρ_inter_ℛd:
  ‹PSKIPS⟪A⟫d σ = P⟪A⟫d σ› if ‹ρ A ∩ ℛd A σ = {}›
proof -
  have ‹σ' ∈ ℛd A σ ⟹ PSKIPS⟪A⟫d σ' = P⟪A⟫d σ'› for σ'
  proof (induct A arbitrary: σ' rule: PSKIPS_d_induct)
    case adm show ?case by simp
  next
    case base show ‹P⟪A⟫d σ' = P⟪A⟫d σ'› ..
  next
    case (step X)
    from step.prems(1) that have ‹σ' ∉ ρ A› by blast
    hence ‹ω A σ' = ◇› by (simp add: ρ_simps)
    thus ?case
      by (subst P_d_rec, auto intro!: mono_Mprefix_eq mono_GlobalNdet_eq)
        (subst (asm) ε_simps, auto, metis (lifting) ℛd.step step.hyps step.prems)
  qed
  thus ‹PSKIPS⟪A⟫d σ = P⟪A⟫d σ› by (simp add: ℛd.init)
qed



lemma PSKIPS_d_rec_notin_ρ:
  ‹σ ∉ ρ A ⟹ PSKIPS⟪A⟫d σ = P_d_step (ε A) (τ A) PSKIPS⟪A⟫d σ›
  by (subst PSKIPS_d_rec) (simp add: ρ_simps)

lemma PSKIPS_d_rec_in_ρ: ‹σ ∈ ρ A ⟹ PSKIPS⟪A⟫d σ = SKIP ⌈ω A σ⌉›
  by (subst PSKIPS_d_rec, simp add: ρ_simps split: option.split)



subsection ‹Link between deterministic and non-deterministic ProcOmata›

lemma PSKIPS_nd_from_det_to_ndet_is_PSKIPS_d : ‹PSKIPS⟪⟪A⟫d↪nd⟫nd = PSKIPS⟪A⟫d›
proof (subst PSKIPS_nd_def, rule restriction_fix_unique)
  show ‹constructive (PSKIPS_nd_step (ε ⟪A⟫d↪nd) (τ ⟪A⟫d↪nd) (ω ⟪A⟫d↪nd))› by simp
next
  show ‹PSKIPS_nd_step (ε ⟪A⟫d↪nd) (τ ⟪A⟫d↪nd) (ω ⟪A⟫d↪nd) PSKIPS⟪A⟫d = PSKIPS⟪A⟫d›
    by (subst (3) PSKIPS_d_rec)
      (rule ext, auto simp add: from_det_to_ndet_def ε_simps
        split: option.split intro: mono_Mprefix_eq)
qed


corollary P_nd_from_det_to_ndet_is_P_d : ‹P⟪⟪A⟫d↪nd⟫nd = P⟪A⟫d›
proof -
  have ‹P⟪⟪A⟫d↪nd⟫nd = PSKIPS⟪⟪A⟫d↪nd⦇ω := λσ. {}⦈⟫nd›
    by (fact PSKIPS_nd_updated_ω)
  also have ‹⟪A⟫d↪nd⦇ω := λσ. {}⦈ = ⟪A⦇ω := λσ. ◇⦈⟫d↪nd›
    by (simp add: from_det_to_ndet_def)
  finally show ‹P⟪⟪A⟫d↪nd⟫nd = P⟪A⟫d›
    by (simp add: PSKIPS_d_updated_ω PSKIPS_nd_from_det_to_ndet_is_PSKIPS_d)
qed



subsection ‹Prove Equality between ProcOmata›

subsubsection ‹This is the easiest method we can think about.›

lemma P_d_eqI : ‹(⋀σ a. τ A σ a = τ B σ a) ⟹ P⟪A⟫d = P⟪B⟫d›
  by (simp add: P_d_def ε_simps)

lemma P_nd_eqI : ‹(⋀σ a. τ A σ a = τ B σ a) ⟹ P⟪A⟫nd = P⟪B⟫nd›
  by (simp add: P_nd_def ε_simps)

lemma PSKIPS_d_eqI :
  ‹(⋀σ a. σ ∉ ρ A ⟹ τ A σ a = τ B σ a) ⟹ (⋀σ. ω A σ = ω B σ) ⟹ PSKIPS⟪A⟫d = PSKIPS⟪B⟫d›
  by (subst PSKIPS_d_def, rule restriction_fix_unique, simp)
    (subst (2) PSKIPS_d_rec, auto simp add: ε_simps ρ_simps split: option.split)

lemma PSKIPS_nd_eqI :
  ‹(⋀σ a. σ ∉ ρ A ⟹ τ A σ a = τ B σ a) ⟹ (⋀σ. ω A σ = ω B σ) ⟹ PSKIPS⟪A⟫nd = PSKIPS⟪B⟫nd›
  by (subst PSKIPS_nd_def, rule restriction_fix_unique[OF PSKIPS_nd_step_constructive])
    (subst (2) PSKIPS_nd_rec, auto simp add: ε_simps ρ_simps split: option.split)



subsubsection ‹We establish now a much more powerful theorem.›

theorem PSKIPS_nd_eqI_strong:
  (* TODO: see if we can obtain better by looking at ρ *)
  assumes inj_on_f : ‹inj_on f (ℛnd A0 σ0)›
    and eq_trans : ‹⋀σ0' a. σ0' ∈ ℛnd A0 σ0 ⟹ τ A1 (f σ0') a = f ` (τ A0 σ0' a)›
    and eq_fin : ‹⋀σ0'. σ0' ∈ ℛnd A0 σ0 ⟹ ω A1 (f σ0') = ω A0 σ0'›
  shows ‹PSKIPS⟪A0⟫nd σ0 = PSKIPS⟪A1⟫nd (f σ0)›
proof -
  have ‹σ0' ∈ ℛnd A0 σ0 ⟹ PSKIPS⟪A1⟫nd (f σ0') = PSKIPS⟪A0⟫nd σ0'› for σ0'
  proof (induct A1 arbitrary: σ0' rule: PSKIPS_nd_induct)
    case adm show ?case by simp
  next
    show ‹σ0' ∈ ℛnd A0 σ0 ⟹ PSKIPS⟪A0⟫nd (inv_into (ℛnd A0 σ0) f (f σ0')) = PSKIPS⟪A0⟫nd σ0'› for σ0'
      by (simp add: inj_on_f)
  next
    case (step X)
    from step.prems eq_trans have ‹ε A0 σ0' = ε A1 (f σ0')›
      by (auto simp add: ε_simps)
    moreover have ‹ω A1 (f σ0') = ω A0 σ0'› by (simp add: eq_fin step.prems)
    ultimately show ?case
      by (subst PSKIPS_nd_rec, auto)
        (metis (mono_tags, lifting) ℛnd.step eq_trans mono_GlobalNdet_eq2
          step.hyps step.prems)
  qed
  thus ‹PSKIPS⟪A0⟫nd σ0 = PSKIPS⟪A1⟫nd (f σ0)› by (simp add: ℛnd.init)
qed


theorem P_nd_eqI_strong:
  ‹⟦inj_on f (ℛnd A0 σ0);
    ⋀σ0' a. σ0' ∈ ℛnd A0 σ0 ⟹ τ A1 (f σ0') a = f ` (τ A0 σ0' a)⟧
  ⟹ P⟪A0⟫nd σ0 = P⟪A1⟫nd (f σ0)›
  by (unfold PSKIPS_nd_updated_ω, rule PSKIPS_nd_eqI_strong) simp_all


theorem PSKIPS_d_eqI_strong:
  assumes ‹inj_on f (ℛd A0 σ0)›
    and ‹⋀σ0' a. σ0' ∈ ℛd A0 σ0 ⟹ τ A1 (f σ0') a = map_option f (τ A0 σ0' a)›
    and ‹⋀σ0'. σ0' ∈ ℛd A0 σ0 ⟹ ω A1 (f σ0') = ω A0 σ0'›
  shows ‹PSKIPS⟪A0⟫d σ0 = PSKIPS⟪A1⟫d (f σ0)›
  by (fold PSKIPS_nd_from_det_to_ndet_is_PSKIPS_d, rule PSKIPS_nd_eqI_strong)
    (unfold ℛnd_from_det_to_ndet,
      simp_all add: assms from_det_to_ndet_def map_option_case split: option.split)


theorem P_d_eqI_strong:
  ‹⟦inj_on f (ℛd A0 σ0);
    ⋀σ0' a. σ0' ∈ ℛd A0 σ0 ⟹ τ A1 (f σ0') a = map_option f (τ A0 σ0' a)⟧
   ⟹ P⟪A0⟫d σ0 = P⟪A1⟫d (f σ0)›
  by (unfold PSKIPS_d_updated_ω, rule PSKIPS_d_eqI_strong) simp_all


lemmas PSKIPS_nd_eqI_strong_id = PSKIPS_nd_eqI_strong[of id, simplified]
  and  PSKIPS_d_eqI_strong_id = PSKIPS_d_eqI_strong
  [of id, simplified id_def option.map_ident, simplified]
  and  P_nd_eqI_strong_id = P_nd_eqI_strong[of id, simplified]
  and  P_d_eqI_strong_id = P_d_eqI_strong
  [of id, simplified id_def option.map_ident, simplified]


corollary PSKIPS_nd_from_σ_to_σs_is_PSKIPS_nd : ‹PSKIPS⟪nd⟪A⟫σ↪σs⟫nd [σ] = PSKIPS⟪A⟫nd σ›
  by (auto simp add: image_iff behaviour_σ_σs_conv(6, 8)
      intro!: inj_onI PSKIPS_nd_eqI_strong[symmetric])

corollary PSKIPS_d_from_σ_to_σs_is_PSKIPS_d : ‹PSKIPS⟪d⟪A⟫σ↪σs⟫d [σ] = PSKIPS⟪A⟫d σ›
  by (auto simp add: image_iff behaviour_σ_σs_conv(2, 4)
      intro!: inj_onI PSKIPS_d_eqI_strong[symmetric] split: option.split)

corollary P_nd_from_σ_to_σs_is_P_nd : ‹P⟪nd⟪A⟫σ↪σs⟫nd [σ] = P⟪A⟫nd σ›
  by (auto simp add: image_iff behaviour_σ_σs_conv(6, 8)
      intro!: inj_onI P_nd_eqI_strong[symmetric])

corollary P_d_from_σ_to_σs_is_P_d : ‹P⟪d⟪A⟫σ↪σs⟫d [σ] = P⟪A⟫d σ›
  by (auto simp add: image_iff behaviour_σ_σs_conv(2, 4)
      intro!: inj_onI P_d_eqI_strong[symmetric] split: option.split)



text ‹Behaviour of normalizations. We will use the following methods in combining theories.›
  (* 
method PSKIPS_when_indep_method uses indep R_d_subset R_nd_subset trans_result defs = 
  subst PSKIPS_d_is_some_PSKIPS_nd, rule PSKIPS_ndI_strong_id[rule_format], simp_all,
  subst (asm) ℛnd_is_ℛd, drule set_mp[OF R_d_subset, rotated],
  (simp add: indep)?, (insert trans_result indep)[1], fastforce,
  rule arg_cong2[where f = ‹(∩)›], solves simp, simp add: det_ndet_conv_defs defs

method P_when_indep_method uses indep R_d_subset trans_result = 
  subst P_d_is_some_P_nd, rule P_ndI_strong_id[rule_format], simp_all, 
  subst (asm) ℛnd_is_ℛd, drule set_mp[OF R_d_subset, rotated], (simp add: indep)?, (*for arbitrary*)
  (insert trans_result indep)[1], fastforce
 *)



(* TODO: find a better place for the things below ? *)
fun recursive_modifier_fund :: ‹[('σ × 'a) ⇒ 'σ option, (('σ × 'a) × 'σ option) list] ⇒ ('σ × 'a) ⇒ 'σ option›
  where ‹recursive_modifier_fund f [] = f›
  |     ‹recursive_modifier_fund f (((s, e), t) # 𝒢A) = recursive_modifier_fund (f((s, e) := t)) 𝒢A›


abbreviation recursive_constructor_Ad :: ‹[(('σ × 'a) × 'σ option) list, 'σ ⇒ 'r option] ⇒ ('σ, 'a, 'r) Ad›
  where ‹recursive_constructor_Ad 𝒢A ωA ≡ ⦇τ = curry (recursive_modifier_fund (λ(s, e). ◇) 𝒢A), ω = ωA⦈›


lemma ε_det_breaker:
  ‹ε (⦇τ = curry (g((σ'::'σ, a) ↦ σ''::'σ)), ω = some_ω, … = some_more⦈ ) σ = 
   (if σ = σ' then {a} ∪ ε ⦇τ = curry g, ω = some_ω⦈ σ' else ε ⦇τ = curry g, ω = some_ω⦈ σ)›
  by (auto simp add: ε_simps split: if_splits)

method ε_det_calc = (unfold recursive_modifier_fund.simps ε_det_breaker, simp cong: if_cong)[1]

method τ_det_calc = (unfold recursive_modifier_fund.simps, simp cong: if_cong)[1]







lemma bij_Renaming_PSKIPS_nd :
  fixes A :: ‹('σ, 'a, 'r, 'α) And_scheme› and f :: ‹'a ⇒ 'b› and g :: ‹'r ⇒ 's›
  assumes ‹bij f›
  defines B_def : ‹B ≡ ⦇τ = λσ b. τ A σ (inv f b), ω = λσ. g ` (ω A σ)⦈›
  shows ‹Renaming (PSKIPS⟪A⟫nd σ) f g = PSKIPS⟪B⟫nd σ› (is ‹?lhs σ = _›)
proof (rule fun_cong[of ?lhs ‹PSKIPS⟪B⟫nd› σ])
  show ‹?lhs = PSKIPS⟪B⟫nd›
  proof (rule restriction_fix_unique[OF PSKIPS_nd_step_constructive_bis[of B],
        symmetric, folded PSKIPS_nd_def])
    show ‹PSKIPS_nd_step (ε B) (τ B) (ω B) ?lhs = ?lhs›
    proof (rule ext)
      have * : ‹ε B σ = f ` ε A σ› for σ
        by (simp add: B_def ε_simps image_def) (metis ‹bij f› bij_inv_eq_iff)
      have ** : ‹inv f (f a) = a› for a
        by (metis ‹bij f› bij_inv_eq_iff)
      have *** : ‹(THE a'. f a' = f a) = a› for a
        by (rule the1_equality', metis (mono_tags, lifting) Uniq_I assms(1) bij_betw_def injD, simp)
      show ‹PSKIPS_nd_step (ε B) (τ B) (ω B) ?lhs σ = ?lhs σ› for σ
        by (subst (2) PSKIPS_nd_rec, simp add: "*")
          (auto simp add: "**" "***" B_def Renaming_distrib_GlobalNdet
            Renaming_Mprefix_image_inj[OF ‹bij f›[THEN bij_is_inj]]
            intro: mono_Mprefix_eq)
    qed
  qed
qed

lemma bij_Renaming_PSKIPS_d :
  ‹bij f ⟹ Renaming (PSKIPS⟪A⟫d σ) f g =
             PSKIPS⟪⦇τ = λσ b. τ A σ (inv f b), ω = λσ. map_option g (ω A σ)⦈⟫d σ›
  by (subst (1 2) PSKIPS_nd_from_det_to_ndet_is_PSKIPS_d[symmetric],
      subst bij_Renaming_PSKIPS_nd, assumption)
    (rule fun_cong[of _ _ σ], rule PSKIPS_nd_eqI,
      simp_all add: from_det_to_ndet_def split: option.split)


lemma RenamingTick_PSKIPS_nd :
  ‹RenamingTick (PSKIPS⟪A⟫nd σ) g = PSKIPS⟪⦇τ = τ A, ω = λσ. g ` ω A σ⦈⟫nd σ›
  by (simp add: bij_Renaming_PSKIPS_nd)

lemma RenamingTick_PSKIPS_d :
  ‹RenamingTick (PSKIPS⟪A⟫d σ) g = PSKIPS⟪⦇τ = τ A, ω = λσ. map_option g (ω A σ)⦈⟫d σ›
  by (simp add: bij_Renaming_PSKIPS_d)



(*<*)
end
  (*>*)