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
 *
 * 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 \verb+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›.›

(* 
typedef ('a, 'r) eventptick = ‹UNIV :: ('a + 'r) set›
  morphisms event_of_sum sum_of_event by simp

setup_lifting type_definition_event

lift_definition ev :: ‹'a ⇒ ('a, 'r) eventptick› is ‹λa. Inl a› .
lift_definition tick :: ‹'r ⇒ ('a, 'r) eventptick› (‹✓'(_')›) is ‹λr. Inr r› .

free_constructors event for is_ev : ev of_ev | is_tick : tick of_tick
proof transfer
  show ‹(⋀x1. y = Inl x1 ⟹ P) ⟹ (⋀x2. y = Inr x2 ⟹ P) ⟹ P› for y :: ‹'a + 'b› and P
    by (metis isl_def sum.collapse(2))
next
  show ‹ev x = ev y ⟷ x = y› for x y :: 'a by (metis ev.rep_eq sum.inject(1))
next
  show ‹✓(x) = ✓(y) ⟷ x = y› for x y :: 'r by (metis sum.inject(2) tick.rep_eq)
next
  show ‹ev x ≠ ✓(y)› for x :: 'a and y :: 'r
    by (metis Inl_Inr_False ev.rep_eq tick.rep_eq)
qed

this looks more natural, but does not work fine with the typedef of process
 *)

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 \verb+front_tickFree+ and its stronger version
\verb+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 is_process3_S_pref: ‹⟦is_process P; (t, {}) ∈ FAILURES P; s ≤ t⟧ ⟹ (s, {}) ∈ FAILURES P›
  by (metis prefixE is_process3)

lemma is_process4: ‹is_process P ⟹ ∀s X Y. (s, Y) ∉ FAILURES P ∨ ¬ X ⊆ Y ∨ (s, X) ∈ FAILURES P›
  by (simp only: is_process_spec) simp

lemma is_process4_S: ‹⟦is_process P; (s, Y) ∈ FAILURES P; X ⊆ Y⟧ ⟹ (s, X) ∈ FAILURES P›
  by (drule is_process4, auto)

lemma is_process4_S1: ‹⟦is_process P; x ∈ FAILURES P; X ⊆ snd x⟧ ⟹ (fst x, X) ∈ FAILURES P›
  by (drule is_process4_S, auto)

lemma is_process5:
  ‹is_process P ⟹ ∀s X Y. (s, X) ∈ FAILURES P ∧ (∀c. c ∈ Y ⟶ (s @ [c], {}) ∉ FAILURES P)
                            ⟶ (s, X ∪ Y) ∈ FAILURES P›
  by (drule is_process_spec[THEN iffD1],metis)

lemma is_process5_S:
  ‹⟦is_process P; (sa, X) ∈ FAILURES P; ∀c. c ∈ Y ⟶ (sa @ [c], {}) ∉ FAILURES P⟧
   ⟹ (sa, X ∪ Y) ∈ FAILURES P›
  by (drule is_process5, metis)

lemma is_process5_S1:
  ‹⟦is_process P; (sa, X) ∈ FAILURES P; (sa, X ∪ Y) ∉ FAILURES P⟧
   ⟹ ∃c. c ∈ Y ∧ (sa @ [c], {}) ∈ FAILURES P›
  by (erule contrapos_np, drule is_process5_S, simp_all)

lemma is_process6: ‹is_process P ⟹ ∀s X. (s @ [✓(r)], {}) ∈ FAILURES P ⟶ (s, X - {✓(r)}) ∈ FAILURES P›
  by (drule is_process_spec[THEN iffD1], metis)

lemma is_process6_S: ‹is_process P ⟹ (s @ [✓(r)], {}) ∈ FAILURES P ⟹ (s, X - {✓(r)}) ∈ FAILURES P›
  by (simp add: is_process6)

lemma is_process7:
  ‹is_process P ⟹ ∀ s t. s ∉ DIVERGENCES P ∨ ¬ tickFree s ∨ ¬ front_tickFree t ∨ s @ t ∈ DIVERGENCES P›
  by (drule is_process_spec[THEN iffD1], metis)

lemma is_process7_S:
  ‹is_process P ⟹ s ∈ DIVERGENCES P ⟹ tickFree s ⟹
   front_tickFree t ⟹ s @ t ∈ DIVERGENCES P›
  by (drule is_process7, metis)

lemma is_process8: ‹is_process P ⟹ ∀s X. s ∉ DIVERGENCES P ∨ (s, X) ∈ FAILURES P›
  by (drule is_process_spec[THEN iffD1], metis)

lemma is_process8_S: ‹is_process P ⟹ s ∈ DIVERGENCES P ⟹ (s, X) ∈ FAILURES P›
  by (drule is_process8, metis)

lemma is_process9: ‹is_process P ⟹ ∀s. s @ [tick] ∉ DIVERGENCES P ∨ s ∈ DIVERGENCES P›
  by (drule is_process_spec[THEN iffD1], metis)

lemma is_process9_S: ‹is_process P ⟹ s @ [tick] ∈ DIVERGENCES P ⟹ s ∈ DIVERGENCES P›
  by (drule is_process9, metis)

lemma Failures_implies_Traces: ‹ ⟦is_process P; (s, X) ∈ FAILURES P⟧ ⟹ s ∈ TRACES P›
  by( simp add: TRACES_def, metis)

lemma is_process5_sing: 
  ‹is_process P ⟹ (s, {x}) ∉ FAILURES P ⟹ (s, {}) ∈ FAILURES P ⟹ (s @ [x], {}) ∈ FAILURES P›
  by (drule_tac X = ‹{}› in is_process5_S1, auto)

lemma is_process5_singT: 
  ‹is_process P ⟹ (s, {x}) ∉ FAILURES P ⟹ (s, {}) ∈ FAILURES P ⟹ s @ [x] ∈ TRACES P›
  by (drule is_process5_sing) (auto simp add: TRACES_def)
 *)

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›

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 \verb+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)


(* lemma is_processT8_Pair: ‹fst s ∈ 𝒟 P ⟹ s ∈ ℱ P›
  by (metis eq_fst_iff is_processT8)

lemma is_processT9: ‹s @ [tick] ∈ 𝒟 P ⟹ s ∈ 𝒟 P›
  by (insert process_charn[of P], metis)

  by (simp add:process_charn)

lemma is_processT2: ‹(s, X) ∈ ℱ P ⟹ front_tickFree s›
by(simp add:process_charn)

lemma is_processT2_TR : ‹s ∈ 𝒯 P ⟹ front_tickFree s›
  by (simp add: Traces.rep_eq Traces_def TRACES_def Failures.rep_eq[symmetric])
     (use is_processT2 in blast)
  
(* 
lemma is_proT2: ‹(s, X) ∈ ℱ P ⟹ s ≠ [] ⟹ tick ∉ set (tl (rev s))›
  using front_tickFree_def is_processT2 tickFree_def by blast
 *)

lemma is_processT3 : ‹(s @ t, {}) ∈ ℱ P ⟹ (s, {}) ∈ ℱ P›
  by (metis process_charn)

lemma is_processT3_S_pref : ‹(t, {}) ∈ ℱ P ⟹ s ≤ t ⟹ (s, {}) ∈ ℱ P›
  by (metis is_processT3 le_list_def)


lemma  is_processT4 : ‹(s, Y) ∈ ℱ P ⟹ X ⊆ Y ⟹ (s, X) ∈ ℱ P›
  by (meson process_charn)

lemma is_processT4_S1 : ‹x ∈ ℱ P ⟹ X ⊆ snd x ⟹ (fst x, X) ∈ ℱ P›
  by (metis is_processT4 prod.collapse)

lemma is_processT5:
  ‹(s, X) ∈ ℱ P ⟹ ∀c. c ∈ Y ⟶ (s @ [c], {}) ∉ ℱ P ⟹ (s, X ∪ Y) ∈ ℱ P›
  by (simp add: process_charn)

lemma is_processT5_S1: 
  ‹(s, X) ∈ ℱ P ⟹ (s, X ∪ Y) ∉ ℱ P ⟹ ∃c. c ∈ Y ∧ (s @ [c], {}) ∈ ℱ P›
  by (erule contrapos_np, simp add: is_processT5)

lemma is_processT5_S2: ‹(s, X) ∈ ℱ P ⟹ (s @ [c], {}) ∉ ℱ P ⟹ (s, X ∪ {c}) ∈ ℱ P›
  using is_processT5_S1 by blast

lemma is_processT5_S2a: ‹(s, X) ∈ ℱ P ⟹ (s, X ∪ {c}) ∉ ℱ P ⟹ (s @ [c], {}) ∈ ℱ P›
  using is_processT5_S2 by blast

lemma  is_processT5_S3: ‹(s, {}) ∈ ℱ P ⟹ (s @ [c], {}) ∉ ℱ P ⟹ (s, {c}) ∈ ℱ P›
  using is_processT5_S2a by auto

   
lemma is_processT5_S4: ‹(s, {}) ∈ ℱ P ⟹ (s, {c}) ∉ ℱ P ⟹ (s @ [c], {}) ∈ ℱ P›
  by (erule contrapos_np, simp add: is_processT5_S3)


lemma is_processT5_S5:
  ‹(s, X) ∈ ℱ P ⟹ ∀c. c ∈ Y ⟶ (s, X ∪ {c}) ∉ ℱ P ⟹
    ∀c. c ∈ Y ⟶ (s @ [c], {}) ∈ ℱ P›
  by (simp add: is_processT5_S2a)

lemma is_processT5_S6: ‹([], {c}) ∉ ℱ P ⟹ ([c], {}) ∈ ℱ P›
  by (metis append_self_conv2 is_processT1 is_processT5_S4)

lemma is_processT6: ‹(s @ [tick], {}) ∈ ℱ P ⟹ (s, X - {tick}) ∈ ℱ P›
  by (simp add: process_charn)

lemma is_processT7: ‹s ∈ 𝒟 P ⟹ tickFree s ⟹ front_tickFree t ⟹ s @ t ∈ 𝒟 P›
  by (insert process_charn[of P], metis)

lemma is_processT8: ‹s ∈ 𝒟 P ⟹ (s, X) ∈ ℱ P›
  by (insert process_charn[of P], metis)

lemma is_processT8_Pair: ‹fst s ∈ 𝒟 P ⟹ s ∈ ℱ P›
  by (metis eq_fst_iff is_processT8)

lemma is_processT9: ‹s @ [tick] ∈ 𝒟 P ⟹ s ∈ 𝒟 P›
  by (insert process_charn[of P], metis)

lemma is_processT9_S_swap: ‹s ∉ 𝒟 P ⟹ s @ [tick] ∉ 𝒟 P›
  by (erule contrapos_nn, simp add: is_processT9)
 *)

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 no_Trace_implies_no_Failure: ‹s ∉ 𝒯 P ⟹ (s, {}) ∉ ℱ P›
  by (simp add: T_F_spec)

lemmas  NT_NF = no_Trace_implies_no_Failure



lemma D_T_subset : ‹𝒟 P ⊆ 𝒯 P› by(auto intro!:D_T)

lemma NF_ND : ‹(s, X) ∉ ℱ P ⟹ s ∉ 𝒟 P›
  by (erule contrapos_nn, simp add: is_processT8)

lemmas NT_ND = D_T_subset[THEN Set.contra_subsetD]

lemma F_T1: ‹a ∈ ℱ P ⟹ fst a ∈ 𝒯 P›
  by (rule_tac X=‹snd a› in F_T, simp)



lemma NF_NT: ‹(s, {}) ∉ ℱ P ⟹ s ∉ 𝒯 P›
  by (erule contrapos_nn, simp only: T_F)

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

lemmas is_processT3_ST = T_F [THEN is_processT3, THEN F_T]

lemmas is_processT3_ST_pref = T_F [THEN is_processT3_S_pref, THEN F_T]

lemmas is_processT3_SR = F_T [THEN T_F, THEN is_processT3]
 *)




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)

(* corollary append_single_T_imp_tickFree : ‹t @ [a] ∈ 𝒯 P ⟹ tickFree t›
  by (simp add: append_T_imp_tickFree) *)

(* lemma F_subset_imp_T_subset: ‹ℱ P ⊆ ℱ Q ⟹ 𝒯 P ⊆ 𝒯 Q›
  by (auto simp: subsetD T_F_spec[symmetric]) *)

(* lemma is_processT6_S2: ‹✓(r) ∉ X ⟹ [✓(r)] ∈ 𝒯 P ⟹ ([], X) ∈ ℱ P›
  by (metis Diff_insert_absorb append_Nil is_processT6_TR) *)

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 \emph{approximation ordering} (also called \emph{process ordering})
will be used for giving semantics to recursion (fixpoints) over processes,
the \emph{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 \emph{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 
        \verb+_ << _+. ›

(* TODO: rename this with ‹below› ? *)

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 \verb+chain+,
\verb+directed+(sets), upper bounds and least upper bounds, etc. ›

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


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 \verb+_  <= _+. 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 lim_proc_is_lub3a: ‹front_tickFree s ⟹ s ∉ 𝒟 P ⟹ t ∈ 𝒟 P ⟹ ¬ t < s @ [c]›
  by (auto simp: le_list_def  less_list_def)
     (metis butlast_append butlast_snoc front_tickFree_append_iff process_charn self_append_conv)
 *)


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


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


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
  (*>*)