Theory Process

(*<*)
―‹ ********************************************************************
 * Project         : HOL-CSP - A Shallow Embedding of CSP in Isabelle/HOL
 * Version         : 2.0
 *
 * Author          : Benoît Ballenghien, Safouan Taha, Burkhart Wolff, Lina Ye.
 *                   (Based on HOL-CSP 1.0 by Haykal Tej and Burkhart Wolff)
 *
 * This file       : The notion of processes
 *
 * Copyright (c) 2009 Université Paris-Sud, France
 * Copyright (c) 2025 Université Paris-Saclay, France
 * Copyright (c) 2026 Université Paris-Saclay, France
 *
 * 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 list of conditions and the following disclaimer.
 *
 *     * 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.
 *
 *     * Neither the name of the copyright holders nor the names of its
 *       contributors may be used to endorse or promote products derived
 *       from this software without specific prior written permission.
 *
 * 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
 * OWNER 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.
 ******************************************************************************›
(*>*)

chapter‹The Notion of Processes›

text‹As mentioned earlier, we base the theory of CSP on HOLCF, a Isabelle/HOL library
providing a theory of continuous functions, fixpoint induction and recursion.›

(*<*)
theory Process
  imports HOLCF "HOL-Library.Prefix_Order" "HOL-Eisbach.Eisbach"
begin
  (*>*)

text‹HOLCF sets the default type class to @{class cpo}, while our 
Process theory establishes links between standard types and @{class pcpo} 
types. Consequently, we reset the default type class to the default in HOL.›

default_sort type

section‹Pre-Requisite: Basic Traces and tick-Freeness›

text‹The denotational semantics of CSP assumes a distinguishable
special event, called ▩‹tick› and written $\checkmark$, that is required
to occur only in the end of traces in order to signalize successful termination of
a process. (In the original text of Hoare, this treatment was more
liberal and lead to foundational problems: the process invariant
could not be established for the sequential composition operator
of CSP; see cite‹"tej.ea:corrected:1997"› for details.)›

text ‹From the Isabelle-2025 version on, the classical constant tick (‹✓›) of the CSP theory
      has been replaced by a parameterized version carrying a kind of return value.›

datatype ('a, 'r) eventptick =
    is_ev   : ev   (of_ev   : 'a)
  | is_tick : tick (of_tick : 'r) (‹✓'(_')›)


text ‹This type typ‹('a, 'r) eventptick› is of course isomorphic to the sum type typ‹'a + 'r›.›
text ‹``ptick'' stands for parameterized tick, and we introduce the type synonym for
      the classical process event type.›

type_synonym 'a event = ‹('a, unit) eventptick›

abbreviation tick_unit :: ‹'a event› (‹✓›) where ‹✓ ≡ ✓(())›

definition sum_of_eventptick :: ‹('a, 'r) eventptick ⇒ 'a + 'r›
  where ‹sum_of_eventptick e ≡ case e of ev a ⇒ Inl a | ✓(r) ⇒ Inr r›

definition eventptick_of_sum :: ‹'a + 'r ⇒ ('a, 'r) eventptick›
  where ‹eventptick_of_sum s ≡ case s of Inl a ⇒ ev a | Inr r ⇒ ✓(r)›

lemma type_definition_eventptick : ‹type_definition sum_of_eventptick eventptick_of_sum UNIV›
proof unfold_locales
  show ‹sum_of_eventptick s ∈ UNIV› for s :: ‹('a, 'r) eventptick› by simp
next
  show ‹eventptick_of_sum (sum_of_eventptick e) = e› for e :: ‹('a, 'r) eventptick›
    by (cases e) (simp_all add: eventptick_of_sum_def sum_of_eventptick_def)
next
  show ‹sum_of_eventptick (eventptick_of_sum s) = s› for s :: ‹'a + 'r›
    by (cases s) (simp_all add: eventptick_of_sum_def sum_of_eventptick_def)
qed

setup_lifting type_definition_eventptick

lemma range_tick_Un_range_ev_is_UNIV [simp] : ‹range tick ∪ range ev = UNIV›
  by (metis UNIV_eq_I UnCI eventptick.exhaust rangeI)

text ‹The generalization is done in a very straightforward way:
      the old version is recovered by considering typ‹('a, unit) eventptick›.›


lemma not_is_ev   [simp] : ‹¬ is_ev   e ⟷ is_tick e›
  and not_is_tick [simp] : ‹¬ is_tick e ⟷ is_ev   e›
  by (use eventptick.exhaust_disc in blast)+


type_synonym ('a, 'r) traceptick = ‹('a, 'r) eventptick list›

text ‹We recover the classical version with typ‹unit›.›

type_synonym 'a trace = ‹('a, unit) traceptick›


text‹We chose as standard ordering on traces the prefix ordering.›


text‹Some facts on the prefix ordering.›

lemma nil_le     [simp]: ‹[] ≤ s›
  and nil_le2    [simp]: ‹s ≤ [] ⟷ s = []›
  and nil_less   [simp]: ‹¬ t < []›
  and nil_less2  [simp]: ‹[] < t @ [a]›
  and less_self  [simp]: ‹t < t @ [a]›
  and le_cons    [simp]: ‹a # s ≤ a # t ⟷ s ≤ t›
  and le_append  [simp]: ‹b @ s ≤ b @ t ⟷ s ≤ t›
  and less_cons  [simp]: ‹a # s < a # t ⟷ s < t›
  and less_append[simp]: ‹b @ s < b @ t ⟷ s < t›

and   le_length_mono: ‹s ≤ t ⟹ length s ≤ length t›
and less_length_mono: ‹s < t ⟹ length s < length t›
and   le_tail: ‹s ≠ [] ⟹ s ≤ t ⟹ tl s ≤ tl t›
and less_tail: ‹s ≠ [] ⟹ s < t ⟹ tl s < tl t›
              apply (simp_all add: less_eq_list_def less_list_def prefix_length_le)
    apply (metis prefix_length_less prefix_order.dual_order.not_eq_order_implies_strict)
   apply (metis prefix_def tl_append2)
  by (metis prefix_def prefix_order.eq_iff self_append_conv tl_append2)


lemma le_same_imp_eq_or_less: ‹(s :: 'a list) ≤ u ⟹ t ≤ u ⟹ t = s ∨ s < t ∨ t < s›
  by (metis less_eq_list_def linorder_le_cases nless_le prefix_length_prefix)


lemma append_eq_first_pref_spec: ‹s @ t = r @ [x] ⟹ t ≠ [] ⟹ s ≤ r›
  by (metis butlast_append butlast_snoc less_eq_list_def prefix_def)


lemma prefixes_fin: ‹finite {t. t ≤ s} ∧ card {t. t ≤ s} = Suc (length s)›
proof (induct s)
  show ‹finite {t. t ≤ []} ∧ card {t. t ≤ []} = Suc (length [])› by simp
next
  case (Cons x s)
  have * : ‹{t. t ≤ x # s} = {[]} ∪ (λt. x # t) ` {t. t ≤ s}›
    by (simp add: image_def less_eq_list_def set_eq_iff)
      (meson Sublist.prefix_Cons)
  show ‹finite {t. t ≤ x # s} ∧ card {t. t ≤ x # s} = Suc (length (x # s))›
  proof (intro conjI)
    show ‹finite {t. t ≤ x # s}› by (simp add: "*" Cons.hyps)
  next
    have ‹finite ((λt. x # t) ` {t. t ≤ s})› by (simp add: Cons.hyps)
    show ‹card {t. t ≤ x # s} = Suc (length (x # s))›
      by (subst card_Un_disjoint[of ‹{[]}› ‹(λt. x # t) ` {t. t ≤ s}›, folded "*"])
        (auto simp add: card_image Cons.hyps)   
  qed
qed


lemma sublists_fin: ‹finite {t. ∃t1 t2. s = t1 @ t @ t2}›
proof (induct s)
  show ‹finite {t. ∃t1 t2. [] = t1 @ t @ t2}› by simp
next
  case (Cons x s)
  have ‹{t. t ≤ x # s} = {t. ∃t2. x # s = t @ t2}›
    by (simp add: less_eq_list_def prefix_def)
  with prefixes_fin[of ‹x # s›] have ‹finite {t. ∃t2. x # s = t @ t2}› by simp
  have ‹{t. ∃t1 t2. x # s = t1 @ t @ t2} ⊆
        {t. ∃t1 t2. s = t1 @ t @ t2} ∪ {t. ∃t2. x # s = t @ t2}›
    by (simp add: subset_iff) (meson Cons_eq_append_conv)
  show ‹finite {t. ∃t1 t2. x # s = t1 @ t @ t2}›
    by (rule finite_subset[OF ‹?this›], rule finite_UnI)
      (simp_all add: Cons.hyps ‹finite {t. ∃t2. x # s = t @ t2}›)
qed


lemma suffixes_fin: ‹finite {t. ∃t1. s = t1 @ t}›
  by (rule finite_subset[of _ ‹{t. ∃t1 t2. s = t1 @ t @ t2}›];
      simp add: subset_iff sublists_fin) blast 


text‹For the process invariant, it is a key element to
reduce the notion of traces to traces that may only contain
one tick event at the very end. This is captured by the definition
of the predicate ▩‹front_tickFree› and its stronger version
▩‹tickFree›. Here is the theory of this concept.›

definition tickFree :: ‹('a, 'r) traceptick ⇒ bool› (‹tF›)
  where ‹tF s ≡ range tick ∩ set s = {}›

definition front_tickFree :: ‹('a, 'r) traceptick ⇒ bool› (‹ftF›)
  where ‹ftF s ≡ s = [] ∨ tickFree (tl (rev s))›

lemma tickFree_Nil        [simp] : ‹tF []›
  and tickFree_Cons_iff   [simp] : ‹tF (a # t) ⟷ is_ev a ∧ tF t›
  and tickFree_append_iff [simp] : ‹tF (s @ t) ⟷ tF s    ∧ tF t›
  and tickFree_rev_iff    [simp] : ‹tF (rev t) ⟷ tF t›
  and non_tickFree_tick   [simp] : ‹¬ tF [✓(r)]›
  by (cases a; auto simp add: tickFree_def)+

lemma tickFree_iff_is_map_ev : ‹tF t ⟷ (∃u. t = map ev u)›
  by (induct t) (simp_all add: Cons_eq_map_conv is_ev_def)

lemma front_tickFree_Nil   [simp] : ‹ftF []›
  and front_tickFree_single[simp] : ‹ftF [a]›
  by (simp_all add: front_tickFree_def)


lemma tickFree_tl : ‹tF s ⟹ tF (tl s)›
  by (cases s) simp_all

lemma non_tickFree_imp_not_Nil: ‹¬ tF s ⟹ s ≠ []›
  using tickFree_Nil by blast

lemma tickFree_butlast: ‹tF s ⟷ tF (butlast s) ∧ (s ≠ [] ⟶ is_ev (last s))›
  by (induct s) simp_all

lemma front_tickFree_iff_tickFree_butlast: ‹ftF s ⟷ tF (butlast s)›
  by (induct s) (auto simp add: front_tickFree_def)

lemma front_tickFree_Cons_iff: ‹ftF (a # s) ⟷ s = [] ∨ is_ev a ∧ ftF s›
  by (simp add: front_tickFree_iff_tickFree_butlast)

lemma front_tickFree_append_iff:
  ‹ftF (s @ t) ⟷ (if t = [] then ftF s else tF s ∧ ftF t)›
  by (simp add: butlast_append front_tickFree_iff_tickFree_butlast)

lemma tickFree_imp_front_tickFree [simp] : ‹tF s ⟹ ftF s›
  by (simp add: front_tickFree_def tickFree_tl)

lemma front_tickFree_charn: ‹ftF s ⟷ s = [] ∨ (∃a t. s = t @ [a] ∧ tF t)›
  by (cases s rule: rev_cases) (simp_all add: front_tickFree_def)


lemma nonTickFree_n_frontTickFree: ‹¬ tF s ⟹ ftF s ⟹ ∃t r. s = t @ [✓(r)]›
  by (metis eventptick.disc(1) eventptick.exhaust front_tickFree_append_iff list.distinct(1)
      rev_exhaust tickFree_Cons_iff tickFree_Nil tickFree_append_iff)

lemma front_tickFree_dw_closed : ‹ftF (s @ t) ⟹ ftF s›
  by (metis front_tickFree_append_iff tickFree_imp_front_tickFree)

lemma front_tickFree_append: ‹tF s ⟹ ftF t ⟹ ftF (s @ t)›
  by (simp add: front_tickFree_append_iff)

lemma tickFree_imp_front_tickFree_snoc: ‹tF s ⟹ ftF (s @ [a])›
  by (simp add: front_tickFree_append)

lemma front_tickFree_nonempty_append_imp: ‹ftF (t @ r) ⟹ r ≠ [] ⟹ tF t ∧ ftF r›
  by (simp add: front_tickFree_append_iff)

lemma tickFree_map_ev [simp] : ‹tF (map ev t)›
  by (induct t) simp_all

lemma tickFree_map_tick_iff [simp] : ‹tF (map tick t) ⟷ t = []›
  by (induct t) simp_all

lemma front_tickFree_map_tick_iff [simp] : ‹ftF (map tick t) ⟷ t = [] ∨ (∃r. t = [r])›
  by (simp add: front_tickFree_iff_tickFree_butlast map_butlast[symmetric])
    (metis append_Nil append_butlast_last_id butlast.simps(1, 2))

― ‹term‹map ev (map f t)› if automatically simplified into term‹map (ev ∘ f) t› by the
    simplified, so we need to add the following versions.›

lemma tickFree_map_ev_comp [simp] : ‹tF (map (ev ∘ f) t)›
  by (metis list.map_comp tickFree_map_ev)

lemma tickFree_map_tick_comp_iff [simp] : ‹tF (map (tick ∘ f) t) ⟷ t = []›
  by (fold map_map, unfold tickFree_map_tick_iff) simp

lemma front_tickFree_map_tick_comp_iff [simp] : ‹ftF (map (tick ∘ f) t) ⟷ t = [] ∨ (∃r. t = [r])›
  by (fold map_map, unfold front_tickFree_map_tick_iff)
    (simp add: map_eq_Cons_conv)



section‹ Basic Types, Traces, Failures and Divergences ›

type_synonym ('a, 'r) refusalptick = ‹('a, 'r) eventptick set›
type_synonym 'a refusal = ‹('a, unit) refusalptick›
type_synonym ('a, 'r) failureptick = ‹('a, 'r) traceptick × ('a, 'r) refusalptick›
type_synonym 'a failure = ‹('a, unit) failureptick›
type_synonym ('a, 'r) divergenceptick = ‹('a, 'r) traceptick›
type_synonym 'a divergence = ‹('a, unit) divergenceptick›
type_synonym ('a, 'r) process0 = ‹('a, 'r) failureptick set × ('a, 'r) divergenceptick set›

definition FAILURES :: ‹('a, 'r) process0 ⇒ ('a, 'r) failureptick set›
  where ‹FAILURES P ≡ fst P›

definition TRACES :: ‹('a, 'r) process0 ⇒ ('a, 'r) traceptick set›
  where ‹TRACES P ≡ {tr. ∃ref. (tr, ref) ∈ FAILURES P}›

definition DIVERGENCES :: ‹('a, 'r) process0 ⇒ ('a, 'r) divergenceptick set›
  where ‹DIVERGENCES P ≡ snd P›

definition REFUSALS :: ‹('a, 'r) process0 ⇒ ('a, 'r) refusalptick set›
  where ‹REFUSALS P ≡ {ref. ([], ref) ∈ FAILURES P}›

section‹ The Process Type Invariant ›

definition is_process :: ‹('a, 'r) process0 ⇒ bool› where
  ‹is_process P ≡
   ([], {}) ∈ FAILURES P ∧
   (∀s X. (s, X) ∈ FAILURES P ⟶ ftF s) ∧
   (∀s t. (s @ t, {}) ∈ FAILURES P ⟶ (s, {}) ∈ FAILURES P) ∧
   (∀s X Y. (s, Y) ∈ FAILURES P ∧ X ⊆ Y ⟶ (s, X) ∈ FAILURES P) ∧
   (∀s X Y. (s, X) ∈ FAILURES P ∧ (∀c. c ∈ Y ⟶ (s @ [c], {}) ∉ FAILURES P)
            ⟶ (s, X ∪ Y) ∈ FAILURES P) ∧
   (∀s r X. (s @ [✓(r)], {}) ∈ FAILURES P ⟶ (s, X - {✓(r)}) ∈ FAILURES P) ∧
   (∀s t. s ∈ DIVERGENCES P ∧ tF s ∧ ftF t ⟶ s @ t ∈ DIVERGENCES P) ∧
   (∀s X. s ∈ DIVERGENCES P ⟶ (s, X) ∈ FAILURES P) ∧
   (∀s r. s @ [✓(r)] ∈ DIVERGENCES P ⟶ s ∈ DIVERGENCES P)›


lemma is_process_spec:
  ‹is_process P ⟷
  ([], {}) ∈ FAILURES P ∧
  (∀s X. (s, X) ∈ FAILURES P ⟶ ftF s) ∧
  (∀s t. (s @ t, {}) ∉ FAILURES P ∨ (s, {}) ∈ FAILURES P) ∧
  (∀s X Y. (s, Y) ∉ FAILURES P ∨ ¬ X ⊆ Y ∨ (s, X) ∈ FAILURES P) ∧
  (∀s X Y. (s, X) ∈ FAILURES P ∧ (∀c. c ∈ Y ⟶ (s @ [c], {}) ∉ FAILURES P)
           ⟶ (s, X ∪ Y) ∈ FAILURES P) ∧
  (∀s r X. (s @ [✓(r)], {}) ∈ FAILURES P ⟶ (s, X - {✓(r)}) ∈ FAILURES P) ∧
  (∀s t. s ∉ DIVERGENCES P ∨ ¬ tF s ∨ ¬ ftF t ∨ s @ t ∈ DIVERGENCES P) ∧
  (∀s X. s ∉ DIVERGENCES P ∨ (s, X) ∈ FAILURES P) ∧
  (∀s r. s @ [✓(r)] ∉ DIVERGENCES P ∨ s ∈ DIVERGENCES P)›
  by (simp only: is_process_def HOL.nnf_simps(1)
      HOL.nnf_simps(3) [symmetric] HOL.imp_conjL[symmetric])

lemma Process_eqI :
  ‹FAILURES P = FAILURES Q ⟹ DIVERGENCES P = DIVERGENCES Q ⟹ P = Q›
  by (metis DIVERGENCES_def FAILURES_def prod_eq_iff)

lemma process_eq_spec:
  ‹P = Q ⟷ FAILURES P = FAILURES Q ∧ DIVERGENCES P = DIVERGENCES Q›
  by (meson Process_eqI)


lemma process_surj_pair: ‹(FAILURES P, DIVERGENCES P) = P›
  by(auto simp: FAILURES_def DIVERGENCES_def)

lemma Fa_eq_imp_Tr_eq: ‹FAILURES P = FAILURES Q ⟹ TRACES P = TRACES Q›
  by (auto simp: FAILURES_def DIVERGENCES_def TRACES_def) 



lemma is_process1 : ‹([], {}) ∈ FAILURES P›
  and is_process2 : ‹(s, X) ∈ FAILURES P ⟹ ftF s›
  and is_process3 : ‹(s @ t, {}) ∈ FAILURES P ⟹ (s, {}) ∈ FAILURES P›
  and is_process4 : ‹⟦is_process P; (s, Y) ∈ FAILURES P; X ⊆ Y⟧ ⟹ (s, X) ∈ FAILURES P›
  and is_process5 : ‹⟦is_process P; (s, X) ∈ FAILURES P; ∀c. c ∈ Y ⟶ (s @ [c], {}) ∉ FAILURES P⟧
                     ⟹ (s, X ∪ Y) ∈ FAILURES P›
  and is_process6 : ‹(s @ [✓(r)], {}) ∈ FAILURES P ⟹ (s, X - {✓(r)}) ∈ FAILURES P›
  and is_process7 : ‹⟦s ∈ DIVERGENCES P; tF s; ftF t⟧ ⟹ s @ t ∈ DIVERGENCES P›
  and is_process8 : ‹s ∈ DIVERGENCES P ⟹ (s, X) ∈ FAILURES P›
  and is_process9 : ‹s @ [✓(r)] ∈ DIVERGENCES P ⟹ s ∈ DIVERGENCES P›
  if ‹is_process P›
  using ‹is_process P› unfolding is_process_def by metis+



lemma trace_with_Tick_imp_tickFree_front :
  ‹is_process P ⟹ t @ [✓(r)] ∈ TRACES P ⟹ tF t›
  by (simp add: TRACES_def) (meson front_tickFree_append_iff is_process2 neq_Nil_conv)


section ‹ The Abstraction to the process-Type ›

typedef ('a, 'r) processptick = ‹{p :: ('a, 'r) process0 . is_process p}›
  morphisms process0_of_process process_of_process0
proof - 
  have ‹({(s, X). s = []}, {}) ∈ {p. is_process p}›
    by (simp add: DIVERGENCES_def FAILURES_def is_process_def)
  thus ?thesis by auto
qed

text ‹Again, the old version without parameterized termination can be recovered
      by considering typ‹('a, unit) processptick›.›

type_synonym 'a process = ‹('a, unit) processptick›

translations
  (type) "'a process"  ⇌ (type)  "('a, unit) processptick"

setup_lifting type_definition_processptick

text ‹This is where we differ from previous versions: we lift definitions 
      using Isabelle's machinery instead of doing it by hand.›

lift_definition Failures :: ‹('a, 'r) processptick ⇒ ('a, 'r) failureptick set› (‹ℱ›) is FAILURES .

lift_definition Traces :: ‹('a, 'r) processptick ⇒ ('a, 'r) traceptick set› (‹𝒯›) is TRACES .

lift_definition Divergences :: ‹('a, 'r) processptick ⇒ ('a, 'r) divergenceptick set› (‹𝒟›) is DIVERGENCES .

lift_definition Refusals :: ‹('a, 'r) processptick ⇒ ('a, 'r) refusalptick set› (‹ℛ›) is REFUSALS .

lemma Refusals_def_bis : ‹ℛ P = {X. ([], X) ∈ ℱ P}›
  by (simp add: Failures.rep_eq REFUSALS_def Refusals.rep_eq)

lemma Refusals_iff : ‹X ∈ ℛ P ⟷ ([], X) ∈ ℱ P›
  by (simp add: Failures_def Refusals_def_bis)

lemma T_def_spec: ‹𝒯 P = {tr. ∃f. f ∈ ℱ P ∧ tr = fst f}›
  by (simp add: Traces_def TRACES_def Failures_def)

lemma T_F_spec : ‹(t, {}) ∈ ℱ P ⟷ t ∈ 𝒯 P›
  by transfer (auto simp add: TRACES_def intro: is_process4)


lemma Process_spec: ‹process_of_process0 (ℱ P, 𝒟 P) = P›
  by (simp add: Divergences.rep_eq Failures.rep_eq
      process0_of_process_inverse process_surj_pair)


lemma Process_eq_spec: ‹P = Q ⟷ ℱ P = ℱ Q ∧ 𝒟 P = 𝒟 Q›
  by (metis Process_spec)


lemma Process_eq_spec_optimized: ‹P = Q ⟷ 𝒟 P = 𝒟 Q ∧ (𝒟 P = 𝒟 Q ⟶ ℱ P = ℱ Q)›
  using Process_eq_spec by auto

lemma is_processT:
  ‹([], {}) ∈ ℱ P ∧
   (∀s X. (s, X) ∈ ℱ P ⟶ ftF s) ∧
   (∀s t. (s @ t, {}) ∈ ℱ P ⟶ (s, {}) ∈ ℱ P) ∧
   (∀s X Y. (s, Y) ∈ ℱ P ∧ X ⊆ Y ⟶ (s, X) ∈ ℱ P) ∧
   (∀s X Y. (s, X) ∈ ℱ P ∧ (∀c. c ∈ Y ⟶ (s @ [c], {}) ∉ ℱ P) ⟶ (s, X ∪ Y) ∈ ℱ P) ∧
   (∀s r X. (s @ [✓(r)], {}) ∈ ℱ P ⟶ (s, X - {✓(r)}) ∈ ℱ P) ∧
   (∀s t. s ∈ 𝒟 P ∧ tF s ∧ ftF t ⟶ s @ t ∈ 𝒟 P) ∧
   (∀s r X. s ∈ 𝒟 P ⟶ (s, X) ∈ ℱ P) ∧ (∀s. s @ [✓(r)] ∈ 𝒟 P ⟶ s ∈ 𝒟 P)›
  by transfer (unfold is_process_def, fast)

text ‹When the second type is set to typ‹unit›, we recover the classical definition
      as defined in the book by Roscoe.›

lemma is_processT_unit:
  ‹([], {}) ∈ ℱ P ∧
   (∀s X. (s, X) ∈ ℱ P ⟶ ftF s) ∧
   (∀s t. (s @ t, {}) ∈ ℱ P ⟶ (s, {}) ∈ ℱ P) ∧
   (∀s X Y. (s, Y) ∈ ℱ P ∧ X ⊆ Y ⟶ (s, X) ∈ ℱ P) ∧
   (∀s X Y. (s, X) ∈ ℱ P ∧ (∀c. c ∈ Y ⟶ (s @ [c], {}) ∉ ℱ P) ⟶ (s, X ∪ Y) ∈ ℱ P) ∧
   (∀s X. (s @ [✓], {}) ∈ ℱ P ⟶ (s, X - {✓}) ∈ ℱ P) ∧
   (∀s t. s ∈ 𝒟 P ∧ tF s ∧ ftF t ⟶ s @ t ∈ 𝒟 P) ∧
   (∀s X. s ∈ 𝒟 P ⟶ (s, X) ∈ ℱ P) ∧ (∀s. s @ [✓] ∈ 𝒟 P ⟶ s ∈ 𝒟 P)›
  by transfer (unfold is_process_def, fast)


lemma process_charn:
  ‹([], {}) ∈ ℱ P ∧
   (∀s X. (s, X) ∈ ℱ P ⟶ ftF s) ∧
   (∀s t. (s @ t, {}) ∉ ℱ P ∨ (s, {}) ∈ ℱ P) ∧
   (∀s X Y. (s, Y) ∉ ℱ P ∨ ¬ X ⊆ Y ∨ (s, X) ∈ ℱ P) ∧
   (∀s X Y. (s, X) ∈ ℱ P ∧ (∀c. c ∈ Y ⟶ (s @ [c], {}) ∉ ℱ P) ⟶ (s, X ∪ Y) ∈ ℱ P) ∧
   (∀s r X. (s @ [✓(r)], {}) ∈ ℱ P ⟶ (s, X - {✓(r)}) ∈ ℱ P) ∧
   (∀s t. s ∉ 𝒟 P ∨ ¬ tF s ∨ ¬ ftF t ∨ s @ t ∈ 𝒟 P) ∧
   (∀s r X. s ∉ 𝒟 P ∨ (s, X) ∈ ℱ P) ∧ (∀s. s @ [✓(r)] ∉ 𝒟 P ∨ s ∈ 𝒟 P)›
  by (meson is_processT)



text‹ split of ▩‹is_processT›: ›

lemma is_processT1          : ‹([], {}) ∈ ℱ P›
  and is_processT1_TR       : ‹[] ∈ 𝒯 P›
  and is_processT2          : ‹(s, X) ∈ ℱ P ⟹ ftF s›
  and is_processT2_TR       : ‹s ∈ 𝒯 P ⟹ ftF s›
  and is_processT3          : ‹(s @ t, {}) ∈ ℱ P ⟹ (s, {}) ∈ ℱ P›
  and is_processT3_pref     : ‹(t, {}) ∈ ℱ P ⟹ s ≤ t ⟹ (s, {}) ∈ ℱ P›
  and is_processT3_TR       : ‹t ∈ 𝒯 P ⟹ s ≤ t ⟹ s ∈ 𝒯 P›
  and is_processT3_TR_pref  : ‹(t, {}) ∈ ℱ P ⟹ s ≤ t ⟹ (s, {}) ∈ ℱ P›
  and is_processT4          : ‹(s, Y) ∈ ℱ P ⟹ X ⊆ Y ⟹ (s, X) ∈ ℱ P› 
  and is_processT5          : ‹(s, X) ∈ ℱ P ⟹ ∀c. c ∈ Y ⟶ (s @ [c], {}) ∉ ℱ P
                               ⟹ (s, X ∪ Y) ∈ ℱ P›
  and is_processT6          : ‹(s @ [✓(r)], {}) ∈ ℱ P ⟹ (s, X - {✓(r)}) ∈ ℱ P›
  and is_processT6_TR       : ‹s @ [✓(r)] ∈ 𝒯 P ⟹ (s, X - {✓(r)}) ∈ ℱ P›
  and is_processT7          : ‹s ∈ 𝒟 P ⟹ tF s ⟹ ftF t ⟹ s @ t ∈ 𝒟 P›
  and is_processT8          : ‹s ∈ 𝒟 P ⟹ (s, X) ∈ ℱ P›
  and is_processT9          : ‹s @ [✓(r)] ∈ 𝒟 P ⟹ s ∈ 𝒟 P›
  by (fold T_F_spec)
    (use is_processT in ‹metis [[metis_verbose=false]] prefixE›)+

lemma is_processT6_notin    : ‹(s @ [✓(r)], {}) ∈ ℱ P ⟹ ✓(r) ∉ X ⟹ (s, X) ∈ ℱ P›
  and is_processT6_TR_notin : ‹s @ [✓(r)] ∈ 𝒯 P ⟹ ✓(r) ∉ X ⟹ (s, X) ∈ ℱ P›
  by (metis Diff_insert_absorb is_processT6)
    (metis Diff_insert_absorb is_processT6_TR)

lemma is_processT3_TR_append : ‹t @ u ∈ 𝒯 P ⟹ t ∈ 𝒯 P›
  using is_processT3_TR by fastforce

lemma nonempty_divE : 
  ‹𝒟 P ≠ {} ⟹ (⋀t. tF t ⟹ t ∈ 𝒟 P ⟹ thesis) ⟹ thesis›
  by (metis ex_in_conv front_tickFree_nonempty_append_imp is_processT2 is_processT8
      is_processT9 neq_Nil_conv nonTickFree_n_frontTickFree)


lemma div_butlast_when_non_tickFree_iff :
  ‹ftF s ⟹ (if tF s then s else butlast s) ∈ 𝒟 P ⟷ s ∈ 𝒟 P›
  by (cases s rule: rev_cases; simp add: front_tickFree_iff_tickFree_butlast)
    (metis front_tickFree_Cons_iff is_processT7 is_processT9 is_tick_def)



section‹ Some Consequences of the Process Characterization›

lemma F_T: ‹(s, X) ∈ ℱ P ⟹ s ∈ 𝒯 P›
  by (simp add: T_def_spec split_def, metis)

lemma T_F: ‹s ∈ 𝒯 P ⟹ (s, {}) ∈ ℱ P›
  using is_processT4 by (auto simp add: T_def_spec)

lemmas D_T = is_processT8 [THEN F_T]

lemmas is_processT4_empty [elim!] = F_T [THEN T_F]


lemma is_processT5_S7: ‹t ∈ 𝒯 P ⟹ (t, A) ∉ ℱ P ⟹ ∃x. x ∈ A ∧ t @ [x] ∈ 𝒯 P›
  by (metis T_F_spec is_processT5 sup_bot_left)

lemma is_processT5_S7': 
  ‹(t, X) ∈ ℱ P ⟹ (t, X ∪ A) ∉ ℱ P ⟹ ∃x. x ∈ A ∧ x ∉ X ∧ t @ [x] ∈ 𝒯 P›
  by (erule contrapos_np, subst Un_Diff_cancel[symmetric])
    (rule is_processT5, auto simp: T_F_spec)

lemma trace_tick_continuation_or_all_tick_failuresE:
  ‹⟦(s, {}) ∈ ℱ P; ⋀r. s @ [✓(r)] ∈ 𝒯 P ⟹ thesis; (s, range tick) ∈ ℱ P ⟹ thesis⟧ ⟹ thesis›
  by (metis F_T f_inv_into_f is_processT5_S7)

(* lemma Nil_subset_T: ‹{[]} ⊆ 𝒯 P›
  by (auto simp: T_F_spec[symmetric] is_processT1) *)

lemmas Nil_elem_T [simp] = is_processT1_TR

lemmas F_imp_front_tickFree = is_processT2
  and D_imp_front_tickFree = is_processT8[THEN is_processT2]
  and T_imp_front_tickFree = T_F[THEN is_processT2]


lemma D_front_tickFree_subset : ‹𝒟 P ⊆ Collect ftF›
  by (auto simp: D_imp_front_tickFree)

lemma F_D_part : ‹ℱ P = {(s, x). s ∈ 𝒟 P} ∪ {(s, x). s ∉ 𝒟 P ∧ (s, x) ∈ ℱ P}›
  by (auto simp add: is_processT8)

lemma D_F : ‹{(s, x). s ∈ 𝒟 P} ⊆ ℱ P›
  using F_D_part by blast

lemma append_T_imp_tickFree:  ‹t @ s ∈ 𝒯 P ⟹ s ≠ [] ⟹ tF t›
  by (meson front_tickFree_append_iff is_processT2_TR)

lemma tick_T_F: ‹t @ [✓(r)] ∈ 𝒯 P ⟹ (t @ [✓(r)], X) ∈ ℱ P›
  by (meson append_T_imp_tickFree is_processT5_S7 list.discI non_tickFree_tick tickFree_append_iff)

lemma is_processT9_tick: ‹[✓(r)] ∈ 𝒟 P ⟹ ftF s ⟹ s ∈ 𝒟 P›
  by (metis append_Nil is_processT7 is_processT9 tickFree_Nil)

lemma T_nonTickFree_imp_decomp: ‹t ∈ 𝒯 P ⟹ ¬ tF t ⟹ ∃s r. t = s @ [✓(r)]›
  by (simp add: is_processT2_TR nonTickFree_n_frontTickFree)



section‹ Process Approximation is a Partial Ordering, a Cpo, and a Pcpo ›
text‹The Failure/Divergence Model of CSP Semantics provides two orderings:
The ∗‹approximation ordering› (also called ∗‹process ordering›)
will be used for giving semantics to recursion (fixpoints) over processes,
the ∗‹refinement ordering› captures our intuition that a more concrete
process is more deterministic and more defined than an abstract one.

We start with the key-concepts of the approximation ordering, namely
the predicates $min\_elems$ and ‹ℛa› (abbreviating ∗‹refusals after›).
The former provides just a set of minimal elements from a given set
of elements of type-class $ord$ \ldots ›

definition min_elems :: ‹('s::ord) set ⇒ 's set›
  where   ‹min_elems X ≡ {s ∈ X. ∀t ∈ X. ¬ (t < s)}›

lemma Nil_min_elems : ‹[] ∈ A ⟹ [] ∈ min_elems A›
  by (simp add: min_elems_def)

lemma min_elems_le_self[simp] : ‹(min_elems A) ⊆ A›
  by (auto simp: min_elems_def)

lemmas elem_min_elems = Set.set_mp[OF min_elems_le_self]

lemma min_elems_Collect_ftF_is_Nil : ‹min_elems (Collect ftF) = {[]}›
  by (simp add: min_elems_def less_eq_list_def set_eq_iff)
    (metis front_tickFree_charn nil_less nil_less2)

lemma min_elems5 : ‹(s :: 'a list) ∈ A ⟹ ∃t≤s. t ∈ min_elems A›
proof -
  have * : ‹x ∈ A ⟹ length x ≤ n ⟹ ∃s≤x. s ∈ min_elems A› for x :: ‹'a list› and A n
  proof (induct n arbitrary: x rule: nat_induct)
    show ‹x ∈ A ⟹ length x ≤ 0 ⟹ ∃s≤x. s ∈ min_elems A› for x by (simp add: Nil_min_elems)
  next
    fix n x
    assume ‹x ∈ A› ‹length x ≤ Suc n›
    assume hyp : ‹x ∈ A ⟹ length x ≤ n ⟹ ∃s≤x. s ∈ min_elems A› for x
    show ‹∃s≤x. s ∈ min_elems A›
    proof (cases ‹∃y ∈ A. y < x›)
      show ‹∃y∈A. y < x ⟹ ∃s≤x. s ∈ min_elems A›
        by (elim bexE, frule hyp, drule less_length_mono, use ‹length x ≤ Suc n› in simp)
          (meson dual_order.strict_trans2 less_list_def)
    next
      show ‹¬ (∃y∈A. y < x) ⟹ ∃s≤x. s ∈ min_elems A›
        using ‹x ∈ A› unfolding min_elems_def by auto
    qed
  qed
  thus ‹s ∈ A ⟹ ∃t≤s. t ∈ min_elems A› by auto
qed

lemma min_elems4: ‹A ≠ {} ⟹ ∃s. (s :: ('a, 'r) traceptick) ∈ min_elems A›
  by (auto dest: min_elems5)

lemma min_elems_charn: ‹t ∈ A ⟹ ∃ t' r. t = (t' @ r) ∧ t' ∈ min_elems A›
  by (meson prefixE min_elems5)

lemma min_elems_no: ‹(s::'a list) ∈ min_elems A ⟹ t ∈ A ⟹ t ≤ s ⟹ s = t›
  by (metis (mono_tags, lifting) mem_Collect_eq min_elems_def order_neq_le_trans)

text‹ \ldots while the second returns the set of possible
refusal sets after a given trace $s$ and a given process
$P$: ›

definition Refusals_after :: ‹[('a, 'r) processptick, ('a, 'r) traceptick] ⇒ ('a, 'r) refusalptick set› (‹ℛa›)
  where   ‹ℛa P tr ≡ {ref. (tr, ref) ∈ ℱ P}›

text‹ In the following, we link the process theory to the underlying 
fixpoint/domain theory of HOLCF by identifying the approximation ordering 
with HOLCF's pcpo's. ›

instantiation 
  processptick  ::  (type, type) below     
begin
text‹ declares approximation ordering $\_ \sqsubseteq \_$ also written 
        ▩‹_ << _›. ›


definition le_approx_def : ‹P ⊑ Q ≡ 𝒟 Q ⊆ 𝒟 P ∧
                                    (∀s. s ∉ 𝒟 P ⟶ ℛa P s = ℛa Q s) ∧ 
                                     min_elems (𝒟 P) ⊆ 𝒯 Q›

text‹ The approximation ordering captures the fact that more concrete
processes should be more defined by ordering the divergence sets
appropriately. For defined positions in a process, the failure
sets must coincide pointwise; moreover, the minimal elements
(wrt.~prefix ordering on traces, i.e.~lists) must be contained in
the trace set of the more concrete process.›

instance ..

end


lemma le_approx1: ‹P ⊑ Q ⟹ 𝒟 Q ⊆ 𝒟 P›
  by (simp add: le_approx_def)


lemma le_approx2: ‹P ⊑ Q ⟹ s ∉ 𝒟 P ⟹ ((s, X) ∈ ℱ Q) = ((s, X) ∈ ℱ P)›
  by (auto simp: Refusals_after_def le_approx_def)


lemma le_approx3: ‹P ⊑ Q ⟹ min_elems(𝒟 P) ⊆ 𝒯 Q›
  by (simp add: le_approx_def)

lemma le_approx2T: ‹P ⊑ Q ⟹ s ∉ 𝒟 P ⟹ s ∈ 𝒯 Q ⟷ s ∈ 𝒯 P›
  by (auto simp: le_approx2 T_F_spec[symmetric])

lemma le_approx_lemma_F : ‹P ⊑ Q ⟹ ℱ Q ⊆ ℱ P›
  by (meson le_approx2 process_charn subrelI)

lemmas order_lemma = le_approx_lemma_F

lemma le_approx_lemma_T: ‹P ⊑ Q ⟹ 𝒯 Q ⊆ 𝒯 P›
  by(auto dest!:le_approx_lemma_F simp: T_F_spec[symmetric])

lemma proc_ord2a : ‹P ⊑ Q ⟹ s ∉ 𝒟 P ⟹ (s, X) ∈ ℱ P ⟷ (s, X) ∈ ℱ Q›
  by (auto simp: le_approx_def Refusals_after_def)


instance processptick :: (type, type) po
proof intro_classes
  show ‹P ⊑ P› for P :: ‹('a, 'r) processptick›
    by (metis D_T elem_min_elems le_approx_def subsetI)
next
  show ‹P ⊑ Q ⟹ Q ⊑ P ⟹ P = Q› for P Q :: ‹('a, 'r) processptick›
    by (simp add: Process_eq_spec le_approx1 le_approx_lemma_F subset_antisym)
next
  fix P Q R :: ‹('a, 'r) processptick›
  assume ‹P ⊑ Q› and ‹Q ⊑ R›
  show ‹P ⊑ R› 
  proof (unfold le_approx_def, intro conjI allI impI)
    show ‹𝒟 R ⊆ 𝒟 P› by (meson ‹P ⊑ Q› ‹Q ⊑ R› dual_order.trans le_approx1)
  next
    show ‹s ∉ 𝒟 P ⟹ ℛa P s = ℛa R s› for s
      by (metis ‹P ⊑ Q› ‹Q ⊑ R› le_approx_def subsetD)
  next
    from ‹P ⊑ Q›[THEN le_approx1]  ‹P ⊑ Q›[THEN le_approx3]
      ‹Q ⊑ R›[THEN le_approx2T] ‹Q ⊑ R›[THEN le_approx3]
    show ‹min_elems (𝒟 P) ⊆ 𝒯 R›
      by (simp add: min_elems_def subset_iff) blast
  qed
qed


text‹ At this point, we inherit quite a number of facts from the underlying
HOLCF theory, which comprises a library of facts such as ▩‹chain›,
▩‹directed›(sets), upper bounds and least upper bounds, etc. ›

text‹
Some facts from the theory of complete partial orders:
    ▪ ▩‹po_class.chainE› : @{thm po_class.chainE}
    ▪ ▩‹po_class.chain_mono› : @{thm po_class.chain_mono}
    ▪ ▩‹po_class.is_ubD› : @{thm po_class.is_ubD}
    ▪ ▩‹po_class.ub_rangeI› : \\ @{thm po_class.ub_rangeI}
    ▪ ▩‹po_class.ub_imageD› : @{thm po_class.ub_imageD}
    ▪ ▩‹po_class.is_ub_upward› : @{thm po_class.is_ub_upward}
    ▪ ▩‹po_class.is_lubD1› : @{thm po_class.is_lubD1}
    ▪ ▩‹po_class.is_lubI› : @{thm po_class.is_lubI}
    ▪ ▩‹po_class.is_lub_maximal› : @{thm po_class.is_lub_maximal}
    ▪ ▩‹po_class.is_lub_lub› : @{thm po_class.is_lub_lub}
    ▪ ▩‹po_class.is_lub_range_shift›: \\ @{thm po_class.is_lub_range_shift}
    ▪ ▩‹po_class.is_lub_rangeD1›: @{thm po_class.is_lub_rangeD1}
    ▪ ▩‹po_class.lub_eqI›: @{thm po_class.lub_eqI}
    ▪ ▩‹po_class.is_lub_unique›:@{thm po_class.is_lub_unique}
›


lemma min_elems3: ‹s @ [c] ∈ 𝒟 P ⟹ s @ [c] ∉ min_elems (𝒟 P) ⟹ s ∈ 𝒟 P›
  by (simp add: min_elems_def less_eq_list_def less_list_def)
    (metis D_imp_front_tickFree append.right_neutral front_tickFree_append_iff
      front_tickFree_dw_closed is_processT7 prefix_def)


lemma min_elems1: ‹s ∉ 𝒟 P ⟹ s @ [c] ∈ 𝒟 P ⟹ s @ [c] ∈ min_elems (𝒟 P)›
  using min_elems3 by blast

lemma min_elems2: ‹s ∉ 𝒟 P ⟹ s @ [c] ∈ 𝒟 P ⟹ P ⊑ S ⟹ Q ⊑ S ⟹ (s @ [c], {}) ∈ ℱ Q›
  by (meson T_F in_mono le_approx3 le_approx_lemma_F min_elems3)

lemma min_elems6: ‹s ∉ 𝒟 P ⟹ s @ [c] ∈ 𝒟 P ⟹ P ⊑ S ⟹ (s @ [c], {}) ∈ ℱ S›
  by (auto intro!: min_elems2)

lemma ND_F_dir2: ‹s ∉ 𝒟 P ⟹ (s, {}) ∈ ℱ P ⟹ P ⊑ S ⟹ Q ⊑ S ⟹ (s, {}) ∈ ℱ Q›
  by (meson is_processT8 le_approx2)

lemma ND_F_dir2': ‹s ∉ 𝒟 P ⟹ s ∈ 𝒯 P ⟹ P ⊑ S ⟹ Q ⊑ S ⟹ s ∈ 𝒯 Q›
  by (meson D_T le_approx2T)


lemma chain_lemma: ‹chain S ⟹ S i ⊑ S k ∨ S k ⊑ S i›
  by (metis chain_mono_less not_le_imp_less po_class.chain_mono)


context fixes S :: ‹nat ⇒ ('a, 'r) processptick›
  assumes ‹chain S›
begin

lift_definition lim_proc :: ‹('a, 'r) processptick›
  is ‹(⋂ (ℱ ` range S), ⋂ (𝒟 ` range S))›
proof (unfold is_process_def FAILURES_def DIVERGENCES_def fst_conv snd_conv, intro conjI allI impI)
  show ‹([], {}) ∈ ⋂ (ℱ ` range S)› by (simp add: is_processT)
next
  show ‹(s, X) ∈ ⋂ (ℱ ` range S) ⟹ ftF s› for s X
    by (meson INT_iff UNIV_I image_eqI is_processT2)
next
  show ‹(s @ t, {}) ∈ ⋂ (ℱ ` range S) ⟹
        (s, {}) ∈ ⋂ (ℱ ` range S)› for s t by (auto intro: is_processT3)
next
  show ‹(s, Y) ∈ ⋂ (ℱ ` range S) ∧ X ⊆ Y ⟹ (s, X) ∈ ⋂ (ℱ ` range S)› for s X Y
    by (metis (full_types) INT_iff is_processT4)
next
  show ‹(s, X ∪ Y) ∈ ⋂ (ℱ ` range S)›
    if assm : ‹(s, X) ∈ ⋂ (ℱ ` range S) ∧
               (∀c. c ∈ Y ⟶ (s @ [c], {}) ∉ ⋂ (ℱ ` range S))› for s X Y
  proof (rule ccontr)
    assume ‹(s, X ∪ Y) ∉ ⋂ (ℱ ` range S)›
    then obtain i where ‹(s, X ∪ Y) ∉ ℱ (S i)› by blast
    moreover have ‹(s, X) ∈ ℱ (S j)› for j using assm by blast
    ultimately obtain c where ‹c ∈ Y› and * : ‹(s @ [c], {}) ∈ ℱ (S i)› 
      using is_processT5 by blast
    from ‹(s, X ∪ Y) ∉ ℱ (S i)› is_processT8 have ‹s ∉ 𝒟 (S i)› by blast
    from assm ‹c ∈ Y› obtain j where ** : ‹(s @ [c], {}) ∉ ℱ (S j)› by blast

    from chain_lemma[OF ‹chain S›, of i j] "*" "**" show False
      by (elim disjE; use ‹s ∉ 𝒟 (S i)› is_processT8 min_elems6 proc_ord2a in blast)
  qed
next
  show ‹(s @ [✓(r)], {}) ∈ ⋂ (ℱ ` range S) ⟹
        (s, X - {✓(r)}) ∈ ⋂ (ℱ ` range S)› for s r X by (simp add: is_processT6)
next
  show ‹s ∈ ⋂ (𝒟 ` range S) ∧ tF s ∧ ftF t ⟹
        s @ t ∈ ⋂ (𝒟 ` range S)› for s t by (simp add: is_processT7)
next
  show ‹s ∈ ⋂ (𝒟 ` range S) ⟹ (s, X) ∈ ⋂ (ℱ ` range S)› for s X
    by (simp add: is_processT8)
next
  show ‹s @ [✓(r)] ∈ ⋂ (𝒟 ` range S) ⟹ s ∈ ⋂ (𝒟 ` range S)› for s r
    by (auto intro: is_processT9)
qed


lemma F_LUB: ‹ℱ lim_proc = ⋂ (ℱ ` range S)›
  by (metis Failures.rep_eq lim_proc.rep_eq process_surj_pair prod.sel(1))

lemma D_LUB: ‹𝒟 lim_proc = ⋂ (𝒟 ` range S)›
  by (metis Divergences.rep_eq lim_proc.rep_eq process_surj_pair prod.inject)

lemma T_LUB: ‹𝒯 lim_proc = ⋂ (𝒯 ` range S)›
  by (insert F_LUB, auto simp add: T_def_spec) (meson F_T T_F)

lemmas LUB_projs = F_LUB D_LUB T_LUB

lemma Refusals_LUB: ‹ℛ lim_proc = ⋂ (ℛ ` range S)›
  by (auto simp add: Refusals_def_bis F_LUB)

lemma Refusals_after_LUB: ‹ℛa lim_proc s = (⋂i. (ℛa (S i) s))›
  by (auto simp add: Refusals_after_def F_LUB)

lemma F_LUB_2: ‹(s, X) ∈ ℱ lim_proc ⟷ (∀i. (s, X) ∈ ℱ (S i))› 
  and D_LUB_2: ‹t ∈ 𝒟 lim_proc ⟷ (∀i. t ∈ 𝒟 (S i))›
  and T_LUB_2: ‹t ∈ 𝒯 lim_proc ⟷ (∀i. t ∈ 𝒯 (S i))›
  and Refusals_LUB_2: ‹X ∈ ℛ lim_proc ⟷ (∀i. X ∈ ℛ (S i))›
  and Refusals_after_LUB_2: ‹X ∈ ℛa lim_proc s ⟷ (∀i. X ∈ ℛa (S i) s)›
  by (simp_all add: F_LUB D_LUB T_LUB Refusals_LUB Refusals_after_LUB)

end


text ‹By exiting the context, terms like ‹ℱ lim_proc› will become term‹ℱ (lim_proc S)›
      and the assumption term‹chain S› will be added.›


section‹ Process Refinement is a Partial Ordering›

text‹ The following type instantiation declares the refinement order
$\_ \le \_ $ written ▩‹_  <= _›. It captures the intuition that more
concrete processes should be more deterministic and more defined.›

instantiation processptick :: (type, type) ord
begin

definition less_eq_processptick :: ‹('a, 'r) processptick ⇒ ('a, 'r) processptick ⇒ bool›
  where ‹less_eq_processptick P Q ≡ 𝒟 Q ⊆ 𝒟 P ∧ ℱ Q ⊆ ℱ P›

definition less_processptick :: ‹('a, 'r) processptick ⇒ ('a, 'r) processptick ⇒ bool›
  where ‹less_processptick P Q ≡ P ≤ Q ∧ P ≠ Q›

instance ..

end



text‹Note that this just another syntax to our standard process refinement order 
     defined in the theory Process. › 


lemma le_ref1  : ‹P ≤ Q ⟹ 𝒟 Q ⊆ 𝒟 P›
  and le_ref2  : ‹P ≤ Q ⟹ ℱ Q ⊆ ℱ P›
  and le_ref2T : ‹P ≤ Q ⟹ 𝒯 Q ⊆ 𝒯 P›
  and le_approx_imp_le_ref: ‹(P::('a, 'r) processptick) ⊑ Q ⟹ P ≤ Q›
  by (simp_all add: less_eq_processptick_def le_approx1 le_approx_lemma_F)
    (use T_F_spec in blast)

lemma F_subset_imp_T_subset : ‹ℱ P ⊆ ℱ Q ⟹ 𝒯 P ⊆ 𝒯 Q›
  using T_F_spec by blast

lemma D_extended_is_D :
  ‹{t @ u |t u. t ∈ 𝒟 P ∧ tF t ∧ ftF u} = 𝒟 P›
  by (auto simp add: is_processT7)
    (metis D_imp_front_tickFree append.right_neutral butlast_snoc front_tickFree_append_iff
      front_tickFree_charn is_processT9 nonTickFree_n_frontTickFree tickFree_Nil)


lemma Process_eq_optimizedI :
  ‹⟦⋀t. t ∈ 𝒟 P ⟹ t ∈ 𝒟 Q; ⋀t. t ∈ 𝒟 Q ⟹ t ∈ 𝒟 P;
    ⋀t X. (t, X) ∈ ℱ P ⟹ t ∉ 𝒟 P ⟹ t ∉ 𝒟 Q ⟹ (t, X) ∈ ℱ Q;
    ⋀t X. (t, X) ∈ ℱ Q ⟹ t ∉ 𝒟 Q ⟹ t ∉ 𝒟 P ⟹ (t, X) ∈ ℱ P⟧ ⟹ P = Q›
  by (simp add: Process_eq_spec_optimized, safe, auto intro: is_processT8)



instance  processptick :: (type, type) order
  by intro_classes (auto simp: less_eq_processptick_def less_processptick_def Process_eq_spec)


lemma lim_proc_is_ub: ‹chain S ⟹ range S <| lim_proc S›
  by (simp add: is_ub_def le_approx_def F_LUB D_LUB T_LUB Refusals_after_def)
    (intro allI conjI, blast, use chain_lemma is_processT8 le_approx2 in blast,
      use D_T chain_lemma le_approx2T le_approx_def in blast)


lemma chain_min_elem_div_is_min_for_sequel:
  ‹chain S ⟹ s ∈ min_elems (𝒟 (S i)) ⟹ i ≤ j ⟹ s ∈ 𝒟 (S j) ⟹ s ∈ min_elems (𝒟 (S j))›
  by (metis elem_min_elems insert_absorb insert_subset le_approx1 
      min_elems5 min_elems_no po_class.chain_mono)


lemma limproc_is_lub: ‹range S <<| lim_proc S› if ‹chain S›
proof (unfold is_lub_def, intro conjI allI impI)
  show ‹range S <| lim_proc S› by (simp add: lim_proc_is_ub ‹chain S›)
next
  show ‹lim_proc S ⊑ P› if ‹range S <| P› for P
  proof (unfold le_approx_def, intro conjI allI impI subsetI)
    show ‹s ∈ 𝒟 P ⟹ s ∈ 𝒟 (lim_proc S)› for s
      by (meson D_LUB_2 ‹chain S› ‹range S <| P› is_ub_def le_approx1 rangeI subsetD)
  next
    show ‹s ∉ 𝒟 (lim_proc S) ⟹ ℛa (lim_proc S) s = ℛa P s› for s
      by (metis ‹chain S› ‹range S <| P› D_LUB_2 le_approx_def lim_proc_is_ub ub_rangeD)
  next
    fix s
    assume ‹s ∈ min_elems (𝒟 (lim_proc S))›
    from elem_min_elems[OF this] have ‹∀i. s ∈ 𝒟 (S i)›
      by (simp add: ‹chain S› D_LUB)
    have ‹∃i. ∀j≥i. s ∈ min_elems (𝒟 (S j))›
    proof (rule ccontr)
      assume ‹∄i. ∀j≥i. s ∈ min_elems (𝒟 (S j))›
      hence ‹∀i. ∃j≥i. s ∉ min_elems (𝒟 (S j))› by simp
      with ‹∀i. s ∈ 𝒟 (S i)› chain_min_elem_div_is_min_for_sequel ‹chain S›
      have ‹∀j. s ∉ min_elems (𝒟 (S j))› by blast
      from ‹s ∈ min_elems (𝒟 (lim_proc S))› ‹∀i. s ∈ 𝒟 (S i)› show False
        by (cases s rule: rev_cases; simp add: min_elems_def D_LUB ‹chain S›)
          (use Nil_min_elems ‹∀j. s ∉ min_elems (𝒟 (S j))› in blast,
            metis (no_types, lifting) INT_iff ‹∀j. s ∉ min_elems (𝒟 (S j))› less_self min_elems3)
    qed
    thus ‹s ∈ 𝒯 P› by (meson le_approx3 order.refl subset_eq ‹range S <| P› ub_rangeD)
  qed
qed

subsubsection‹Some basic facts over chain, limproc, and lub's›
text‹Facts that are missing in HOLCF, unfortunately.›

lemma limproc_is_thelub: ‹chain S ⟹ (⨆i. S i) = lim_proc S›
  by (frule limproc_is_lub, frule po_class.lub_eqI, simp)


lemma interate_vs_compower : "cont F ⟹  iterate i⋅(Abs_cfun F)⋅⊥ = (F ^^ i) ⊥"
  by(induct "i")(auto)

lemma fix_def_alt : "cont F ⟹ (⨆i. (F ^^ i) ⊥) =  (fix ⋅ (Abs_cfun F))" 
  unfolding fix_def cfun_def 
  by(subst beta_cfun,simp)(simp add: interate_vs_compower)

lemma fix_def_alt': "cont F ⟹ (⨆i. (F ^^ i) ⊥) = (μ x . F x)"
  using fix_def_alt by blast

lemma cont_compow [simp] :
  fixes f :: ‹'a::cpo ⇒ 'a›
  assumes ‹cont f›
  shows ‹cont (f ^^ n)›
proof (induct n)
  case 0
  show ?case by (simp add: id_def)
next
  case (Suc n)
  then show ?case by (simp add: comp_def cont_compose assms)
qed

lemma chain_compow_bot :
  fixes f :: ‹'a::pcpo ⇒ 'a›
  assumes ‹cont f› shows ‹chain (λi. (f ^^ i) ⊥)›
  using chain_iterate[of ‹Abs_cfun f›] by (simp add: interate_vs_compower[OF assms])

text‹We now formalize a general domain-theoretic fact:
for a continuous term‹f› on a pointed cpo, the least fixed point of term‹f› coincides
with the least fixed point of any finite iterate term‹f ^^ Suc n› of term‹f›. This is
Kleene's theorem applied to the fact that the Kleene chain of term‹f› and the (cofinal)
subchain obtained by keeping only every term‹Suc n›-th element have the ∗‹same› least 
upper bound.›

lemma lub_cofinal_compow :
  fixes f :: ‹'a::pcpo ⇒ 'a›
  assumes ‹cont f›
  shows ‹(⨆i. (f ^^ (Suc n * i)) ⊥) = (⨆k. (f ^^ k) ⊥)›
proof (rule below_antisym)
  have chain : ‹chain (λk. (f ^^ k) ⊥)› by (rule chain_compow_bot[OF assms])
  have chain2 : ‹chain (λi. (f ^^ (Suc n * i)) ⊥)›
    by (rule chainI, rule chain_mono[OF chain]) simp
  show ‹(⨆i. (f ^^ (Suc n * i)) ⊥) ⊑ (⨆k. (f ^^ k) ⊥)›
    by (rule lub_below[OF chain2], rule is_ub_thelub[OF chain])
next
  have chain : ‹chain (λk. (f ^^ k) ⊥)› by (rule chain_compow_bot[OF assms])
  have chain2 : ‹chain (λi. (f ^^ (Suc n * i)) ⊥)›
    by (rule chainI, rule chain_mono[OF chain]) simp
  show ‹(⨆k. (f ^^ k) ⊥) ⊑ (⨆i. (f ^^ (Suc n * i)) ⊥)›
  proof (rule lub_below[OF chain])
    fix k
    have ‹(f ^^ k) ⊥ ⊑ (f ^^ (Suc n * k)) ⊥›
      by (rule chain_mono[OF chain]) (metis le_add1 mult_Suc)
    also have ‹… ⊑ (⨆i. (f ^^ (Suc n * i)) ⊥)›
      by (rule is_ub_thelub[OF chain2])
    finally show ‹(f ^^ k) ⊥ ⊑ (⨆i. (f ^^ (Suc n * i)) ⊥)› .
  qed
qed

lemma fix_funpow_eq :
  fixes f :: ‹'a::pcpo ⇒ 'a›
  assumes cont_f : ‹cont f›
  shows ‹(μ x. (f ^^ Suc n) x) = (μ x. f x)›
proof -
  define g where g_def : ‹g ≡ f ^^ Suc n›
  have cont_g : ‹cont g› unfolding g_def by (rule cont_compow[OF cont_f])
  have ‹(μ x. g x) = (⨆i. (g ^^ i) ⊥)›
    by (simp add: fix_def_alt'[OF cont_g])
  also have ‹… = (⨆i. (f ^^ (Suc n * i)) ⊥)›
    unfolding g_def by (simp only: funpow_mult)
  also have ‹… = (⨆k. (f ^^ k) ⊥)›
    by (rule lub_cofinal_compow[OF cont_f])
  also have ‹… = (μ x. f x)›
    by (simp add: fix_def_alt'[OF cont_f])
  finally show ?thesis unfolding g_def .
qed


instance processptick :: (type, type) cpo
  by intro_classes (use limproc_is_lub in blast)



instance processptick :: (type, type) pcpo
proof
  define bot0 :: ‹('a, 'r) process0› where ‹bot0 ≡ ({(s, X). ftF s}, {d. ftF d})›
  define bot :: ‹('a, 'r) processptick› where ‹bot ≡ process_of_process0 bot0›

  have ‹is_process bot0›
    unfolding is_process_def bot0_def
    by (simp add: FAILURES_def DIVERGENCES_def)
      (meson front_tickFree_append_iff front_tickFree_dw_closed)
  have F_bot : ‹ℱ bot = {(s, X). ftF s}›
    by (metis CollectI FAILURES_def Failures.rep_eq ‹is_process bot0› 
        bot0_def bot_def fst_eqD process_of_process0_inverse)
  have D_bot : ‹𝒟 bot = {d. ftF d}›
    by (metis CollectI DIVERGENCES_def Divergences.rep_eq ‹is_process bot0›
        bot0_def bot_def process_of_process0_inverse prod.sel(2))

  show ‹∃x :: ('a, 'r) processptick. ∀ y. x ⊑ y› 
  proof (intro exI allI)
    show ‹bot ⊑ y› for y
    proof (unfold le_approx_def, intro conjI allI impI subsetI)
      show ‹s ∈ 𝒟 y ⟹ s ∈ 𝒟 bot› for s
        by (simp add: D_bot D_imp_front_tickFree)
    next
      from F_imp_front_tickFree show ‹s ∉ 𝒟 bot ⟹ ℛa bot s = ℛa y s› for s
        by (auto simp add: D_bot Refusals_after_def F_bot)
    next
      show ‹s ∈ min_elems (𝒟 bot) ⟹ s ∈ 𝒯 y› for s
        by (simp add: D_bot min_elems_Collect_ftF_is_Nil)
    qed
  qed
qed



section‹ Process Refinement is Admissible ›

lemma le_FD_adm : ‹cont (u :: ('b::cpo) ⇒ ('a, 'r) processptick) ⟹ monofun v ⟹ adm (λx. u x ≤ v x)›
  apply (unfold less_eq_processptick_def adm_def)
  apply (simp add: cont2contlubE D_LUB F_LUB ch2ch_cont limproc_is_thelub monofun_def)
  by (meson INF_greatest dual_order.trans is_ub_thelub le_approx1 le_approx_lemma_F)

lemmas le_FD_adm_cont[simp] = le_FD_adm[OF _ cont2mono]

section‹ The Conditional Statement is Continuous ›
text‹The conditional operator of CSP is obtained by a direct shallow embedding. Here we prove it continuous›

lemma if_then_else_cont[simp]:
  ‹⟦⋀x. P x ⟹ cont (f x); ⋀x. ¬ P x ⟹ cont (g x)⟧ ⟹
   cont (λy. if P x then f x y else g x y)›
  for f :: ‹'c ⇒ 'b :: cpo ⇒ ('a, 'r) processptick›
  by (auto simp: cont_def)


section ‹Tools for proving continuity›

― ‹The following result is very useful (especially for ProcOmata).›

lemma cont_process_rec: ‹P = (μ X. f X) ⟹ cont f ⟹ P = f P›
  by (simp add: def_cont_fix_eq)


lemma Inter_nonempty_finite_chained_sets: ‹(⋂i. S i) ≠ {}›
  if ‹⋀i. j ≤ i ⟹ S i ≠ {}› ‹finite (S j)› ‹⋀i. S (Suc i) ⊆ S i› for S :: ‹nat ⇒ 'a set›
proof -
  have * : ‹∀i. S i ≠ {} ⟹ finite (S 0) ⟹ ∀i. S (Suc i) ⊆ S i ⟹ (⋂i. S i) ≠ {}›
    for S :: ‹nat ⇒ 'a set›
  proof (induct ‹card (S 0)› arbitrary: S rule: nat_less_induct)
    case 1
    show ?case
    proof (cases ‹∀i. S i = S 0›)
      case True
      thus ?thesis by (metis "1.prems"(1) INT_iff ex_in_conv)
    next 
      case False
      have f1: ‹i ≤ j ⟹ S j ⊆ S i› for i j by (simp add: "1.prems"(3) lift_Suc_antimono_le)
      with False obtain j m where f2: ‹m < card (S 0)› and f3: ‹m = card (S j)›
        by (metis "1.prems"(2) psubsetI psubset_card_mono zero_le)
      define T where ‹T i ≡ S (i + j)› for i
      have f4: ‹m = card (T 0)› unfolding T_def by (simp add: f3)
      from f1 have f5: ‹(⋂i. S i) = (⋂i. T i)› unfolding T_def by (auto intro: le_add1)
      show ?thesis
        apply (subst f5)
        apply (rule "1.hyps"[rule_format, OF f2, of T, OF f4], unfold T_def)
        by (simp_all add: "1.prems"(1, 3) lift_Suc_antimono_le)
          (metis "1.prems"(2) add_0 f1 finite_subset le_add1)
    qed
  qed
  define S' where ‹S' i ≡ S (j + i)› for i
  have ‹∀i. S' i ≠ {}› by (simp add: S'_def ‹⋀i. j ≤ i ⟹ S i ≠ {}›)
  moreover have ‹finite (S' 0)› by (simp add: ‹S' ≡ λi. S (j + i)› ‹finite (S j)›)
  moreover have ‹∀i. S' (Suc i) ⊆ S' i› by (simp add: S'_def ‹⋀i. S (Suc i) ⊆ S i›)
  ultimately have ‹(⋂i. S' i) ≠ {}› by (fact "*")
  also from lift_Suc_antimono_le[where f = S, OF ‹⋀i. S (Suc i) ⊆ S i›]
  have ‹(⋂i. S' i) = (⋂i. S i)›
    by (simp add: INF_greatest INF_lower INF_mono' S'_def equalityI)
  finally show ‹(⋂i. S i) ≠ {}› .
qed


method prove_finite_subset_of_prefixes for t :: ‹('a, 'r) traceptick› =
  ―‹Useful for establishing the second hypothesis›
  solves ‹(rule finite_UnI; prove_finite_subset_of_prefixes t) |
          (rule finite_subset[of _ ‹{u. u ≤ t}›],
           use prefixI in blast, simp add: prefixes_fin)›


(*<*)
end
(*>*)