Theory Process

(*<*)
―‹ ********************************************************************
 * Project         : HOL-CSP - A Shallow Embedding of CSP in  Isabelle/HOL
 * Version         : 2.0
 *
 * Author          : Benoit Ballenghien, Safouan Taha, Burkhart Wolff
 *                   (Based on HOL-CSP 1.0 by Haykal Tej and Burkhart Wolff)
 *
 * This file       : A Combined CSP Theory
 *
 * Copyright (c) 2009 Université Paris-Sud, France
 * Copyright (c) 2023 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
begin

text‹Since 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.)›

datatype 'α event = ev 'α | tick

type_synonym 'α trace = "('α event) list"

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

instantiation  list :: (type) order
begin 

definition  le_list_def  : "(s::'a list) ≤ t ⟷ (∃ r. s @ r = t)"

definition  less_list_def: "(s::'a list) < t ⟷ s ≤ t ∧ s ≠ t" 

lemma A : "((x::'a list) < y) = (x ≤ y ∧ ¬ y ≤ x)"
by(auto simp: le_list_def less_list_def)

instance 
proof
   fix x y z ::"'a list"
   show "(x < y) = (x ≤ y ∧ ¬ y ≤ x)" 
     by(auto simp: le_list_def less_list_def)
   show "x ≤ x"  by(simp add: le_list_def)
   assume A:"x ≤ y" and B:"y ≤ z" thus "x ≤ z"
     apply(insert A B, simp add: le_list_def, safe)  
     apply(rename_tac r ra, rule_tac x="r@ra" in exI, simp)
     done
   assume A:"x ≤ y" and B:"y ≤ x" thus "x = y"
     by(insert A B, auto simp: le_list_def)  
qed

end

text‹Some facts on the prefix ordering.›

lemma nil_le[simp]: "[] ≤ s"
by(induct "s", simp_all, auto simp: le_list_def) 

lemma nil_le2[simp]: "s ≤ [] = (s = [])"
by(induct "s", auto simp:le_list_def)

lemma nil_less[simp]: "¬ t < []"
by(simp add: less_list_def)

lemma nil_less2[simp]: "[] < t @ [a]"
by(simp add: less_list_def)

lemma less_self[simp]: "t < t@[a]"
by(simp add:less_list_def le_list_def)
   
lemma le_length_mono: "s ≤ t ⟹ length s ≤ length t"
by(auto simp: le_list_def)

lemma less_length_mono: "s < t ⟹ length s < length t"
by(auto simp: less_list_def le_list_def)

lemma less_cons: "s < t ⟹ a # s < a # t"
by (simp add: le_list_def less_list_def)

lemma less_append: "s < t ⟹ a @ s < a @ t"
by (simp add: le_list_def less_list_def)

lemma less_tail: "s ≠ [] ⟹ s < t ⟹ tl s < tl t"
by (auto simp add: le_list_def less_list_def)

―‹should be in the List library›
lemma list_nonMt_append: "s ≠ [] ⟹ ∃ a t. s = t @ [a]"
by(erule rev_mp,induct "s",simp_all,case_tac "s = []",auto)

lemma append_eq_first_pref_spec[rule_format]: "s @ t = r @ [x] ∧ t ≠ [] ⟶ s ≤ r"
  apply(rule_tac x=s in spec)
  apply(induct r,auto)
    apply(erule rev_mp)
    apply(rename_tac xa, rule_tac list=xa in list.induct, simp_all)
  apply(simp add: le_list_def)
  apply(drule list_nonMt_append, auto)
  done

lemma prefixes_fin: "let prefixes = {t. ∃t2. x = t @ t2} in finite prefixes ∧ card prefixes = length x + 1"  
proof(induct x, simp)
  case (Cons a x)
  hence A:"finite {t. (∃t2. x = t @ t2)}" using not_add_less2 by fastforce
  have B:"inj_on Cons UNIV" by (metis injI list.inject)
  from Cons A B inj_on_iff_eq_card have  C:"card ((λx. a#x)`{t. (∃t2. x = t @ t2)}) = length x + 1"
    by fastforce
  have D:"{t. ∃t2. a # x = t @ t2} = {[]} ∪ (λx. a#x)`{t. (∃t2. x = t @ t2)}" 
    by(intro set_eqI iffI, auto simp add:Cons_eq_append_conv) 
  from C D card_insert_if[of "(λx. a#x)`{t. (∃t2. x = t @ t2)}"] show ?case 
    by (metis (no_types, lifting) One_nat_def Suc_eq_plus1 Un_insert_left finite.insertI 
        finite_imageI image_iff list.distinct(1) list.size(4) local.A sup_bot.left_neutral)
qed

lemma sublists_fin: "finite {t. ∃t1 t2. x = t1 @ t @ t2}"
  proof(induct x, simp)
    case (Cons a x)
    have "{t. ∃t1 t2. a # x = t1 @ t @ t2} ⊆ {t. ∃t1 t2. x = t1 @ t @ t2} ∪ {t. ∃t2. a#x = t @ t2}"
      apply(auto) by (metis Cons_eq_append_conv)
    with Cons prefixes_fin[of "a#x"] show ?case by (meson finite_UnI finite_subset)
  qed

lemma suffixes_fin: "finite {t. ∃t1. x = t1 @ t}"
  apply(subgoal_tac "{t. ∃t1. x = t1 @ t} ⊆ {t. ∃t1 t2. x = t1 @ t @ t2}")
  using infinite_super sublists_fin apply blast
  by 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 :: "'α trace ⇒ bool"
  where "tickFree s = (tick ∉ set s)"

definition front_tickFree :: "'α trace ⇒ bool"
  where "front_tickFree s = (s =[] ∨ tickFree(tl(rev s)))"

lemma tickFree_Nil [simp]: "tickFree []"
by(simp add: tickFree_def)

lemma tickFree_Cons [simp]: "tickFree (a # t) = (a ≠ tick ∧ tickFree t)"
by(auto simp add: tickFree_def)

lemma tickFree_tl : "tickFree s ⟹ tickFree(tl s)"
by(case_tac s, simp_all)
  
lemma tickFree_append[simp]: "tickFree(s@t) = (tickFree s ∧ tickFree t)"
by(simp add: tickFree_def member_def)

lemma non_tickFree_tick [simp]: "¬ tickFree [tick]"
by(simp add: tickFree_def)

lemma non_tickFree_implies_nonMt: "¬ tickFree s ⟹ s ≠ []"
by(simp add:tickFree_def,erule rev_mp, induct s, simp_all)

lemma  tickFree_rev : "tickFree(rev t) = (tickFree t)"
by(simp  add: tickFree_def member_def)

lemma front_tickFree_Nil[simp]: "front_tickFree []"
by(simp add: front_tickFree_def)

lemma front_tickFree_single[simp]: "front_tickFree [a]"
by(simp add: front_tickFree_def)

lemma tickFree_implies_front_tickFree: "tickFree s ⟹ front_tickFree s"
apply(simp add: tickFree_def front_tickFree_def member_def,safe)
apply(erule contrapos_np, simp,(erule rev_mp)+)
apply(rule_tac xs=s in List.rev_induct,simp_all)
done

lemma front_tickFree_charn: "front_tickFree s = (s = [] ∨ (∃a t. s = t @ [a] ∧ tickFree t))"
apply(simp add: front_tickFree_def)
apply(cases "s=[]", simp_all)
apply(drule list_nonMt_append, auto simp: tickFree_rev)
done

lemma front_tickFree_implies_tickFree: "front_tickFree (t @ [a]) ⟹ tickFree t"
by(simp add: tickFree_def front_tickFree_def member_def)

lemma tickFree_implies_front_tickFree_single: "tickFree t ⟹ front_tickFree (t @ [a])"
by(simp add:front_tickFree_charn) 


lemma nonTickFree_n_frontTickFree: "⟦¬ tickFree s; front_tickFree s ⟧ ⟹ ∃t. s = t @ [tick]"
apply(frule non_tickFree_implies_nonMt)
apply(drule front_tickFree_charn[THEN iffD1], auto)
done

lemma front_tickFree_dw_closed : "front_tickFree (s @ t) ⟹  front_tickFree s"
apply(erule rev_mp, rule_tac x= s in spec)
apply(rule_tac xs=t in List.rev_induct, simp, safe)
apply(rename_tac x xs xa)
apply(simp only: append_assoc[symmetric])
apply(rename_tac x xs xa, erule_tac x="xa @ xs" in all_dupE)
apply(drule front_tickFree_implies_tickFree)
apply(erule_tac x="xa" in allE, auto)
apply(auto dest!:tickFree_implies_front_tickFree)
done

lemma front_tickFree_append: "⟦ tickFree s; front_tickFree t⟧ ⟹ front_tickFree (s @ t)"
apply(drule front_tickFree_charn[THEN iffD1], auto)
apply(erule tickFree_implies_front_tickFree)
apply(subst append_assoc[symmetric])
apply(rule tickFree_implies_front_tickFree_single)
apply(auto intro: tickFree_append)
done

lemma front_tickFree_mono: "front_tickFree (t @ r) ∧ r ≠ [] ⟶ tickFree t ∧ front_tickFree r"
by(metis append_assoc append_butlast_last_id front_tickFree_charn 
         front_tickFree_implies_tickFree tickFree_append)


lemma tickFree_butlast: ‹tickFree s ⟷ tickFree (butlast s) ∧ (s ≠ [] ⟶ last s ≠ tick)›
  by (induct s, simp_all)

lemma front_tickFree_butlast: ‹front_tickFree s ⟷ tickFree (butlast s)›
  by (induct s, auto simp add: front_tickFree_def)


section‹ Basic Types, Traces, Failures and Divergences ›

type_synonym 'α refusal = "('α event) set"
type_synonym 'α failure = "'α trace × 'α refusal"
type_synonym 'α divergence = "'α trace set"
type_synonym 'α process⇩0 = "'α failure set × 'α divergence"
 
definition FAILURES :: "'α process⇩0 ⇒ ('α failure set)"
  where "FAILURES P = fst P"

definition TRACES :: "'α process⇩0 ⇒ ('α trace set)"
  where "TRACES P = {tr. ∃ a. a ∈ FAILURES P ∧ tr = fst a}"

definition DIVERGENCES :: "'α process⇩0 ⇒ 'α divergence"
  where "DIVERGENCES P = snd P"

definition REFUSALS :: "'α process⇩0 ⇒ ('α refusal set)"
  where "REFUSALS P = {ref.  ∃ F. F ∈ FAILURES P ∧ F = ([],ref)}"

section‹ The Process Type Invariant ›

definition is_process :: "'α process⇩0 ⇒ bool" where
  "is_process P =
      (([],{}) ∈ FAILURES P ∧
       (∀ s X.  (s,X) ∈ FAILURES P ⟶ front_tickFree 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 X.  (s@[tick],{}) : FAILURES P ⟶ (s,X-{tick}) ∈ FAILURES P) ∧
       (∀ s t.  s ∈ DIVERGENCES P ∧ tickFree s ∧ front_tickFree t 
                                      ⟶ s@t ∈ DIVERGENCES P)  ∧
       (∀ s X. s ∈ DIVERGENCES P ⟶ (s,X) ∈ FAILURES P) ∧
       (∀ s. s @ [tick] : DIVERGENCES P ⟶ s ∈ DIVERGENCES P))"


lemma is_process_spec:
 "is_process P = 
       (([],{}) ∈  FAILURES P ∧
       (∀ s X. (s,X) ∈  FAILURES P ⟶ front_tickFree 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 X. (s@[tick],{}) ∈  FAILURES P ⟶ (s,X - {tick}) ∈  FAILURES P) ∧
       (∀ s t. s ∉ DIVERGENCES P ∨ ¬tickFree s ∨ ¬front_tickFree t 
                                 ∨ s @ t ∈ DIVERGENCES P) ∧
       (∀ s X. s ∉ DIVERGENCES P ∨ (s,X) ∈  FAILURES P) ∧
       (∀ s. s @ [tick] ∉  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 :
assumes A: "FAILURES P = FAILURES Q "
assumes B: "DIVERGENCES P = DIVERGENCES Q"
shows      "(P::'α process⇩0) = Q"
apply(insert A B, unfold FAILURES_def DIVERGENCES_def) 
apply(rule_tac t=P in surjective_pairing[symmetric,THEN subst])
apply(rule_tac t=Q in surjective_pairing[symmetric,THEN subst])
apply(simp)
done

lemma process_eq_spec:
"((P::'a process⇩0) = Q) = (FAILURES P = FAILURES Q ∧ DIVERGENCES P = DIVERGENCES Q)"
apply(auto simp: FAILURES_def DIVERGENCES_def)
apply(rule_tac t=P in surjective_pairing[symmetric,THEN subst])
apply(rule_tac t=Q in surjective_pairing[symmetric,THEN subst])
apply(simp)
done

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:  "is_process P ⟹ ([],{})∈ FAILURES P "
by(auto simp: is_process_def)

lemma is_process2: "is_process P ⟹ ∀ s X. (s,X) ∈ FAILURES P ⟶ front_tickFree s "
by(simp only: is_process_spec, metis)

lemma is_process3: "is_process P ⟹ ∀ s t. (s @ t,{}) ∈ FAILURES P ⟶ (s, {}) ∈ FAILURES P"
by(simp only: is_process_spec, metis)


lemma is_process3_S_pref: "⟦is_process P; (t, {}) ∈ FAILURES P; s ≤ t⟧ ⟹ (s, {}) ∈ FAILURES P"
by(auto simp: le_list_def intro: is_process3 [rule_format])

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 ⟹
    ∀sa X Y. (sa, X) ∈ FAILURES P ∧ (∀c. c ∈ Y ⟶ (sa @ [c], {}) ∉ FAILURES P) ⟶ (sa, 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@[tick],{}) ∈ FAILURES P ⟶ (s,X-{tick}) ∈ FAILURES P"
by(drule is_process_spec[THEN iffD1], metis)

lemma is_process6_S: "⟦is_process P ;(s@[tick],{}) ∈ FAILURES P⟧ ⟹  (s,X-{tick}) ∈ FAILURES P"
by(drule is_process6, metis)

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"
apply(drule is_process5_sing, auto)
by(simp add: TRACES_def, auto)


lemma front_trace_is_tickfree:
assumes A: "is_process P" and B: "(t @ [tick],X) ∈ FAILURES P"
shows     "tickFree t"
proof -
  have C: "front_tickFree(t @ [tick])" by(insert A B, drule is_process2, metis) 
  show ?thesis  by(rule front_tickFree_implies_tickFree[OF C])   
qed


lemma trace_with_Tick_implies_tickFree_front : "⟦is_process P; t @ [tick] ∈ TRACES P⟧ ⟹ tickFree t"
by(auto simp: TRACES_def intro: front_trace_is_tickfree)


section ‹ The Abstraction to the process-Type ›

typedef 
  'α process = "{p :: 'α process⇩0 . is_process p}"
proof - 
  have "({(s, X). s = []},{}) ∈ {p::'α process⇩0. is_process p}"
    by(simp add: is_process_def  front_tickFree_def
                 FAILURES_def TRACES_def DIVERGENCES_def )
  thus ?thesis by auto
qed

setup_lifting type_definition_process

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 :: "'α process ⇒ ('α failure set)" ("ℱ")
  is "λP. FAILURES P" .


lift_definition Traces :: "'α process ⇒  ('α trace set)"   ("𝒯")
  is "λP. TRACES P" .


lift_definition Divergences :: "'α process ⇒ 'α divergence"     ("𝒟")
  is "λP. DIVERGENCES P" .


lift_definition Refusals :: "'α process ⇒ ('α refusal set)"  ("ℛ")
  is "λP. REFUSALS P" .



lemma is_process_Rep : "is_process (Rep_process P)"
  using Rep_process by blast


lemma Process_spec: "Abs_process (ℱ P, 𝒟 P) = P"
  by (simp add: Divergences.rep_eq Failures.rep_eq Rep_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 ⟶ front_tickFree 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@[tick],{}) ∈ ℱ P ⟶ (s, X-{tick}) ∈ ℱ P) ∧
 (∀ s t. s ∈ 𝒟 P ∧ tickFree s ∧ front_tickFree t ⟶ s @ t ∈ 𝒟 P) ∧
 (∀ s X. s ∈ 𝒟 P ⟶ (s,X) ∈ ℱ P) ∧
 (∀ s. s@[tick] ∈ 𝒟 P ⟶ s ∈ 𝒟 P)" 
  apply (simp add: Divergences.rep_eq Failures.rep_eq)
  by (meson is_process_spec[of ‹Rep_process P›, simplified Rep_process[simplified]])
  
 

lemma process_charn:
  "([], {}) ∈ ℱ P ∧
    (∀s X. (s, X) ∈ ℱ P ⟶ front_tickFree 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 @ [tick], {}) ∈ ℱ P ⟶ (s, X - {tick}) ∈ ℱ P) ∧
    (∀s t. s ∉ 𝒟 P ∨ ¬ tickFree s ∨ ¬ front_tickFree t ∨ s @ t ∈ 𝒟 P) ∧
    (∀s X. s ∉ 𝒟 P ∨ (s, X) ∈ ℱ P) ∧ (∀s. s @ [tick] ∉ 𝒟 P ∨ s ∈ 𝒟 P)"
  (* by (meson is_processT) *)
proof -
  {
    have A: "(∀s t. (s @ t, {}) ∉ ℱ P ∨  (s, {}) ∈ ℱ P) = 
      (∀s t. (s @ t, {}) ∈ ℱ P ⟶ (s, {}) ∈ ℱ P)"
      by metis

    have B : "(∀s X Y. (s, Y) ∉ ℱ P ∨ ¬ X ⊆ Y ∨ (s, X) ∈ ℱ P)  =
      (∀s X Y. (s, Y) ∈ ℱ P ∧ X ⊆ Y ⟶ (s, X) ∈ ℱ P) "
      by metis

    have C : "(∀s t. s ∉ 𝒟 P ∨ ¬ tickFree s ∨ 
      ¬ front_tickFree t ∨ s @ t ∈ 𝒟 P)  =
      (∀s t. s ∈ 𝒟 P ∧ tickFree s ∧ front_tickFree t ⟶ s @ t ∈ 𝒟 P) "
      by metis

    have D:"(∀s X. s ∉ 𝒟 P ∨ (s, X) ∈ ℱ P) = (∀s X. s ∈ 𝒟 P ⟶ (s, X) ∈ ℱ P)"
      by metis

    have E:"(∀s. s @ [tick] ∉ 𝒟 P ∨ s ∈ 𝒟 P) = 
      (∀s. s @ [tick] ∈ 𝒟 P ⟶ s ∈ 𝒟 P)"
      by metis

    note A B C D E 
  }
  note a = this
  then
  show ?thesis
    apply(simp only: a)
    apply(rule is_processT)
    done
qed


text‹ split of \verb+is_processT+: ›

lemma is_processT1: "([], {}) ∈ ℱ P"
by(simp add:process_charn)

lemma is_processT2: "∀s X. (s, X) ∈ ℱ P ⟶ front_tickFree s"
by(simp add:process_charn)

lemma  is_processT2_TR : "∀s. s ∈ 𝒯 P ⟶ front_tickFree s"
  apply (simp add: Traces.rep_eq Traces_def TRACES_def Failures.rep_eq[symmetric])
  using is_processT2 by blast
  

lemma is_proT2:
  assumes A : " (s, X) ∈ ℱ P" and B : " s ≠ []"
  shows   "tick ∉ set (tl (rev s))"
proof -
  have C: "front_tickFree s" by(insert A B, simp add: is_processT2)
  show ?thesis
  by(insert C,simp add: B  tickFree_def front_tickFree_def) 
qed

lemma is_processT3 : "∀s t. (s @ t, {}) ∈ ℱ P ⟶ (s, {}) ∈ ℱ P"
by(simp only: process_charn  HOL.nnf_simps(3), simp)

lemma is_processT3_S_pref : 
"⟦(t, {}) ∈ ℱ P; s ≤ t⟧ ⟹ (s, {}) ∈ ℱ P"
apply(simp only: le_list_def, safe)
apply(erule is_processT3[rule_format])
done

lemma  is_processT4 : "∀s X Y. (s, Y) ∈ ℱ P ∧ X ⊆ Y ⟶ (s, X) ∈ ℱ P"
by(insert  process_charn [of P], metis)

lemma is_processT4_S1 : "⟦x ∈ ℱ P; X ⊆ snd x⟧ ⟹ (fst x, X) ∈ ℱ P"
apply(rule_tac Y = "snd x" in is_processT4[rule_format])
apply simp
done

lemma is_processT5: 
"∀s X Y. (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[rule_format])

lemma is_processT5_S2: "(s, X) ∈ ℱ P ⟹ (s @ [c], {}) ∉ ℱ P ⟹ (s, X ∪ {c}) ∈ ℱ P"
by(rule is_processT5[rule_format,OF conjI], metis, safe)


lemma is_processT5_S2a: "(s, X) ∈ ℱ P ⟹ (s, X ∪ {c}) ∉ ℱ P ⟹ (s @ [c], {}) ∈ ℱ P"
apply(erule contrapos_np)
apply(rule is_processT5_S2)
apply(simp_all)
done

lemma  is_processT5_S3:
assumes A: "(s, {}) ∈ ℱ P"
and     B: "(s @ [c], {}) ∉ ℱ P"
shows      "(s, {c}) ∈ ℱ P"
proof -
   have C : " {c} = ({} Un {c})" by simp
   show ?thesis
   by(subst C, rule is_processT5_S2, simp_all add: A B)
qed
   
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(erule_tac Q = "∀c. c ∈ Y ⟶ (s, X ∪ {c}) ∉ ℱ P" in contrapos_pp, metis is_processT5_S2) 

lemma is_processT5_S6: "([], {c}) ∉ ℱ P ⟹ ([c], {}) ∈ ℱ P"
apply(rule_tac t="[c]" and s="[]@[c]" in subst, simp)
apply(rule is_processT5_S4, simp_all add: is_processT1)
done

lemma is_processT6: "∀s X. (s @ [tick], {}) ∈ ℱ P ⟶ (s, X - {tick}) ∈ ℱ P"
by(simp add: process_charn)


lemma is_processT7:  "∀s t. s ∈ 𝒟 P ∧ tickFree s ∧ front_tickFree t ⟶ s @ t ∈ 𝒟 P"
by(insert process_charn[of P], metis)

lemmas is_processT7_S = is_processT7[rule_format,OF conjI[THEN conjI, THEN  conj_commute[THEN iffD1]]]

lemma is_processT8: "∀s X. s ∈ 𝒟 P ⟶ (s, X) ∈ ℱ P"
by(insert process_charn[of P], metis)

lemmas is_processT8_S = is_processT8[rule_format]

lemma is_processT8_Pair: "fst s ∈ 𝒟 P ⟹ s ∈ ℱ P"
apply(subst surjective_pairing)
apply(rule is_processT8_S, simp)
done

lemma is_processT9: "∀s. 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[rule_format])


section‹ Some Consequences of the Process Characterization›

lemma no_Trace_implies_no_Failure: "s ∉ 𝒯 P ⟹ (s, {}) ∉ ℱ P"
by(simp add: Traces_def TRACES_def Failures_def)

lemmas  NT_NF = no_Trace_implies_no_Failure

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

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

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


lemma T_F: "s ∈ 𝒯 P ⟹ (s, {}) ∈ ℱ P"
apply(auto simp: T_def_spec)
apply(drule is_processT4_S1, simp_all)
done

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

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

lemma  is_processT6_S1: "tick ∉ X ⟹ (s @ [tick], {}) ∈ ℱ P ⟹ (s, X) ∈ ℱ P"
by(subst Diff_triv[of X "{tick}", symmetric],
   simp, erule is_processT6[rule_format])

lemmas is_processT3_ST = T_F [THEN is_processT3[rule_format,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[rule_format]]]

lemmas D_T = is_processT8_S [THEN F_T]

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_S)

lemmas NT_ND = D_T_subset[THEN Set.contra_subsetD]

lemma T_F_spec : "((t, {}) ∈ ℱ P) = (t ∈ 𝒯 P)"
by(auto simp:T_F F_T)

lemma is_processT5_S7:  "t ∈ 𝒯 P ⟹ (t, A) ∉ ℱ P ⟹ ∃x. x ∈ A ∧ t @ [x] ∈ 𝒯 P"
apply(erule contrapos_np, simp)
apply(rule is_processT5[rule_format, OF conjI,of _ "{}", simplified])
apply(auto simp: T_F_spec)
  done

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

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

lemma Nil_elem_T: "[] ∈ 𝒯 P"
by(simp add: Nil_subset_T[THEN subsetD])

lemmas D_imp_front_tickFree = is_processT8_S[THEN is_processT2[rule_format]]

lemma D_front_tickFree_subset : "𝒟 P ⊆ Collect front_tickFree"
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 intro:is_processT8_Pair)

lemma D_F : "{(s, x). s ∈ 𝒟 P} ⊆ ℱ P"
by(auto intro:is_processT8_Pair)

lemma append_T_imp_tickFree:  "t @ s ∈ 𝒯 P ⟹ s ≠ [] ⟹ tickFree t"
by(frule is_processT2_TR[rule_format], 
   simp add: front_tickFree_def tickFree_rev)

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: "tick ∉ X ⟹ [tick] ∈ 𝒯 P ⟹ ([], X) ∈ ℱ P"
by(erule is_processT6_S1, simp add: T_F_spec) 

lemma is_processT9_tick: "[tick] ∈ 𝒟 P ⟹ front_tickFree s ⟹ s ∈ 𝒟 P"
apply(rule append.simps(1) [THEN subst, of _ s])
apply(rule is_processT7_S, simp_all)
apply(rule is_processT9 [rule_format], simp)
done


lemma T_nonTickFree_imp_decomp: "t ∈ 𝒯 P ⟹ ¬ tickFree t ⟹ ∃s. t = s @ [tick]"
by(auto elim: is_processT2_TR[rule_format] 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 $Ra$ (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. 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 front_tickFree) = {[]}"
apply(auto simp: min_elems_def le_list_def)
apply(drule front_tickFree_charn[THEN iffD1])
apply(auto dest!: tickFree_implies_front_tickFree)
done

lemma min_elems5 : 
  assumes A: "(x::'a list) ∈ A"
  shows      "∃s≤x. s ∈ min_elems A"
proof -
   have * : "!! (x::'a list) (A::'a list set) (n::nat).
                x ∈ A ∧ length x ≤ n ⟶ (∃s≤x. s ∈ min_elems A)"
            apply(rule_tac x=x in spec)
            apply(rule_tac n=n in nat_induct) (* quirk in induct *)
            apply(auto simp: Nil_min_elems)
            apply(case_tac "∃ y.  y ∈ A ∧ y < x",auto)
            apply(rename_tac A na x y, erule_tac x=y in allE, simp)
            apply(erule impE,drule less_length_mono, arith)
            apply(safe, rename_tac s, rule_tac x=s in exI,simp)
            apply(rule_tac x=x in exI, simp add:min_elems_def)
            done
   show ?thesis by(rule_tac n="length x" in *[rule_format],simp add:A)
qed

lemma min_elems4: "A ≠ {} ⟹ ∃s. (s :: 'a trace) ∈ min_elems A"
by(auto dest: min_elems5)

lemma min_elems_charn: "t ∈ A ⟹ ∃ t' r. t = (t' @ r) ∧ t' ∈ min_elems A"
by(drule min_elems5[simplified le_list_def], auto)

lemmas min_elems_ex = min_elems_charn  (* Legacy *)

lemma min_elems_no: "(x::'a list) ∈ min_elems A ⟹ t ∈ A ⟹ t ≤ x ⟹ x = t" 
  by (metis (no_types, lifting) less_list_def mem_Collect_eq min_elems_def)

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

definition Ra :: "['α process, 'α trace] ⇒ ('α refusal set)" ("ℛ⇩a")
  where   "ℛ⇩a P s = {X. (s, X) ∈ ℱ 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 
   process  ::  ("type") below     
begin
text‹ declares approximation ordering $\_ \sqsubseteq \_$ also written 
        \verb+_ << _+. ›

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: Ra_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"
apply(subst F_D_part[of Q], subst F_D_part[of P])
apply(auto simp:le_approx_def Ra_def min_elems_def)
done

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 Ra_def)


instance
   process :: ("type") po
proof
   fix P::"'α process"
   show "P ⊑ P" by(auto simp: le_approx_def min_elems_def elim: Process.D_T)
 next
   fix P Q ::"'α process" 
   assume A:"P ⊑ Q" and B:"Q ⊑ P" thus "P = Q"
   apply(insert A[THEN le_approx1] B[THEN le_approx1])
   apply(insert A[THEN le_approx_lemma_F] B[THEN le_approx_lemma_F])
   by(auto simp: Process_eq_spec)
 next
   fix P Q R ::"'α process" 
   assume A: "P ⊑ Q" and B: "Q ⊑ R" thus "P ⊑ R" 
   proof -
      have C : "𝒟 R ⊆ 𝒟 P" 
               by(insert A[THEN le_approx1] B[THEN le_approx1], auto)
      have D : "∀s. s ∉ 𝒟 P ⟶ {X. (s, X) ∈ ℱ P} = {X. (s, X) ∈ ℱ R}" 
               apply(rule allI, rule impI, rule set_eqI, simp)
               apply(frule A[THEN le_approx1, THEN Set.contra_subsetD])
               apply(frule B[THEN le_approx1, THEN Set.contra_subsetD])
               apply(drule A[THEN le_approx2], drule B[THEN le_approx2]) 
               apply auto
               done
      have E : "min_elems (𝒟 P) ⊆ 𝒯 R"
               apply(insert B[THEN le_approx3] A[THEN le_approx3] )
               apply(insert B[THEN le_approx_lemma_T] A[THEN le_approx1] ) 
               apply(rule subsetI, simp add: min_elems_def, auto)
               apply(rename_tac x, case_tac "x ∈ 𝒟 Q")
               apply(drule_tac B = "𝒯 R" and t=x 
                     in subset_iff[THEN iffD1,rule_format], auto)
               apply(subst B [THEN le_approx2T],simp)
               apply(rename_tac x, drule_tac B = "𝒯 Q" and t=x 
                     in subset_iff[THEN iffD1,rule_format],auto)
               done
      show ?thesis
      by(insert C D E, simp add: le_approx_def Ra_def)
   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+Porder.chainE+ : @{thm "Porder.chainE"}
\item \verb+Porder.chain_mono+ : @{thm "Porder.chain_mono"}
\item \verb+Porder.is_ubD+ : @{thm "Porder.is_ubD"}
\item \verb+Porder.ub_rangeI+ : \\ @{thm "Porder.ub_rangeI"}
\item \verb+Porder.ub_imageD+ : @{thm "Porder.ub_imageD"}
\item \verb+Porder.is_ub_upward+ : @{thm "Porder.is_ub_upward"}
\item \verb+Porder.is_lubD1+ : @{thm "Porder.is_lubD1"}
\item \verb+Porder.is_lubI+ : @{thm "Porder.is_lubI"}
\item \verb+Porder.is_lub_maximal+ : @{thm "Porder.is_lub_maximal"}
\item \verb+Porder.is_lub_lub+ : @{thm "Porder.is_lub_lub"}
\item \verb+Porder.is_lub_range_shift+: \\ @{thm "Porder.is_lub_range_shift"}
\item \verb+Porder.is_lub_rangeD1+: @{thm "Porder.is_lub_rangeD1"}
\item \verb+Porder.lub_eqI+: @{thm "Porder.lub_eqI"}
\item \verb+Porder.is_lub_unique+:@{thm "Porder.is_lub_unique"}
\end{itemize}
›


definition lim_proc :: "('α process) set ⇒ 'α process"
  where   "lim_proc (X) = Abs_process (⋂ (ℱ ` X), ⋂ (𝒟 ` X))"

lemma min_elems3: " s @ [c] ∈ 𝒟 P ⟹ s @ [c] ∉ min_elems (𝒟 P) ⟹ s ∈ 𝒟 P"
apply(auto simp: min_elems_def le_list_def less_list_def)
apply(rename_tac t r) 
apply(subgoal_tac "t ≤ s")
apply(subgoal_tac "r ≠ []")
apply(simp add: le_list_def)
apply(auto intro!: is_processT7_S append_eq_first_pref_spec)
apply(auto dest!: D_T)
apply(simp_all only: append_assoc[symmetric],
      drule append_T_imp_tickFree,
      simp_all add: tickFree_implies_front_tickFree)+
done

lemma min_elems1: "s ∉ 𝒟 P ⟹ s @ [c] ∈ 𝒟 P ⟹ s @ [c] ∈ min_elems (𝒟 P)"
  by(erule contrapos_np, auto elim!: min_elems3)

lemma min_elems2: "s ∉ 𝒟 P ⟹ s @ [c] ∈ 𝒟 P ⟹ P ⊑ S ⟹ Q ⊑ S ⟹ (s @ [c], {}) ∈ ℱ Q"
  apply(frule_tac P=Q and Q=S in le_approx_lemma_T)
  apply(simp add: T_F_spec)
  apply(rule_tac A="𝒯 S" in subsetD, assumption)
  apply(rule_tac A="min_elems(𝒟 P)" in subsetD) 
  apply(simp_all add: le_approx_def min_elems1)
done

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"
  apply(frule_tac P=Q and Q=S in le_approx_lemma_T)
  apply(simp add: le_approx_def Ra_def T_F_spec, safe)
  apply((erule_tac x=s in allE)+,simp)
  apply(drule_tac x="{}" in eqset_imp_iff, auto simp: T_F_spec)
done ―‹orig version›

lemma ND_F_dir2': "s ∉ 𝒟 P ⟹ s ∈ 𝒯 P ⟹ P ⊑ S ⟹ Q ⊑ S ⟹ s ∈ 𝒯 Q"
  apply(frule_tac P=Q and Q=S in le_approx_lemma_T)
  apply(simp add: le_approx_def Ra_def T_F_spec, safe)
  apply((erule_tac x=s in allE)+,simp)
  apply(drule_tac x="{}" in eqset_imp_iff, auto simp: T_F_spec)
done


lemma chain_lemma: "⟦chain S⟧ ⟹ S i ⊑ S k ∨ S k ⊑ S i"
by(case_tac "i ≤ k", auto intro:chain_mono chain_mono_less)
 

lemma is_process_REP_LUB: 
  assumes chain: "chain S"
  shows "is_process (⋂ (ℱ ` range S), ⋂ (𝒟 ` range S))"

proof (auto simp: is_process_def)
   show   "([], {}) ∈ FAILURES (⋂ a::nat. ℱ (S a), ⋂ a::nat. 𝒟 (S a))"
          by(auto simp: FAILURES_def is_processT)
next
   fix s::"'a trace" fix X::"'a event set"
   assume A : "(s, X) ∈ (FAILURES (⋂ a :: nat. ℱ (S a), ⋂ a :: nat. 𝒟 (S a)))" 
   thus   "front_tickFree s"
          by(auto simp:   DIVERGENCES_def FAILURES_def
                  intro!: is_processT2[rule_format])
next
   fix s  t::"'a trace"
   assume " (s @ t, {}) ∈ FAILURES (⋂ a::nat. ℱ (S a), ⋂ a::nat. 𝒟 (S a)) "
   thus "(s, {}) ∈ FAILURES (⋂ a::nat. ℱ (S a), ⋂ a::nat. 𝒟 (S a))"
          by(auto simp:  DIVERGENCES_def FAILURES_def
                  intro: is_processT3[rule_format])
next
   fix s::"'a trace"   fix X Y ::"'a event set"
   assume "(s, Y) ∈ FAILURES (⋂ a::nat. ℱ (S a), ⋂ a::nat. 𝒟(S a))" and "X ⊆ Y"
   thus   "(s, X) ∈ FAILURES (⋂ a::nat. ℱ (S a), ⋂ a::nat. 𝒟(S a))"
          by(auto simp:  DIVERGENCES_def FAILURES_def
                  intro: is_processT4[rule_format])
next
   fix s::"'a trace"   fix X Y ::" 'a event set"
   assume A:"(s, X) ∈ FAILURES (⋂ a::nat. ℱ (S a), ⋂ a::nat. 𝒟 (S a))"
   assume B:"∀ c. c∈Y ⟶ (s@[c],{})∉FAILURES(⋂ a::nat. ℱ(S a),⋂ a::nat. 𝒟(S a))"
   thus   "(s, X ∪ Y) ∈ FAILURES (⋂ a::nat. ℱ (S a), ⋂ a::nat. 𝒟 (S a))"
   txt‹ What does this mean: All trace prolongations $c$ in all $Y$, 
         which are blocking in the limit, will also occur in the refusal set 
         of the limit. ›
   using A B chain
   proof (auto simp: DIVERGENCES_def FAILURES_def,
          case_tac "∀ x. x ∈ (range S) ⟶ (s, X ∪ Y) ∈ ℱ x",
          simp_all add:DIVERGENCES_def FAILURES_def,rename_tac a,
          case_tac "s ∉ 𝒟 (S a)",simp_all add: is_processT8)
      fix a::nat 
      assume X: "∀a. (s, X) ∈ ℱ (S a)"
                 have X_ref_at_a: "(s, X) ∈ ℱ (S a)"
                 using X by auto
      assume Y: "∀c. c ∈ Y ⟶ (∃a. (s @ [c], {}) ∉ ℱ (S a))"
      assume defined: "s ∉ 𝒟 (S a)"
      show   "(s::'a trace, X ∪ Y) ∈ ℱ (S a)"
      proof(auto simp:X_ref_at_a
                 intro!: is_processT5[rule_format],
            frule Y[THEN spec, THEN mp], erule exE,
            erule_tac Q="(s @ [c], {}) ∈ ℱ (S a)" in contrapos_pp)
         fix c::"'a event" fix a' :: nat
         assume s_c_trace_not_trace_somewhere: "(s @ [c], {}) ∉ ℱ (S a')"
         show "(s @ [c], {}) ∉ ℱ (S a)"
         proof(insert chain_lemma[OF chain, of "a" "a'"],erule disjE)
           assume before: "S a ⊑ S a'"
           show "(s @ [c], {}) ∉ ℱ (S a)"
             using s_c_trace_not_trace_somewhere  before
             apply(case_tac "s @ [c] ∉ 𝒟 (S a)",
                   simp_all add: T_F_spec before[THEN le_approx2T,symmetric])
             apply(erule contrapos_nn)
             apply(simp only: T_F_spec[symmetric])
             apply(auto dest!:min_elems6[OF defined])
             done
         next
           assume after:"S a' ⊑ S a"
           show "(s @ [c], {}) ∉ ℱ (S a)"
             using s_c_trace_not_trace_somewhere
             by(simp add:T_F_spec after[THEN le_approx2T]
                         s_c_trace_not_trace_somewhere[THEN NF_ND])
         qed
      qed
   qed
next
   fix s::"'a trace"   fix X::"'a event set"
   assume "(s @ [tick], {}) ∈ FAILURES (⋂ a::nat. ℱ (S a), ⋂ a::nat. 𝒟 (S a))"
   thus   "(s, X - {tick}) ∈ FAILURES (⋂ a::nat. ℱ (S a), ⋂ a::nat. 𝒟 (S a))"
          by(auto simp: DIVERGENCES_def FAILURES_def
                  intro! : is_processT6[rule_format])
next
   fix s t ::"'a trace"
   assume "s : DIVERGENCES (⋂ a::nat. ℱ (S a), ⋂ a::nat. 𝒟 (S a))"
   and    "tickFree s" and " front_tickFree t"
   thus   "s @ t ∈ DIVERGENCES (⋂ a::nat. ℱ (S a), ⋂ a::nat. 𝒟 (S a))"
          by(auto simp: DIVERGENCES_def FAILURES_def
                  intro: is_processT7[rule_format])
next
   fix s::"'a trace"  fix X::"'a event set"
   assume "s ∈ DIVERGENCES (⋂ a::nat. ℱ (S a), ⋂ a::nat. 𝒟 (S a)) "
   thus   "(s, X) ∈ FAILURES (⋂ a::nat. ℱ (S a), ⋂ a::nat. 𝒟 (S a))"
          by(auto simp: DIVERGENCES_def FAILURES_def
                       intro: is_processT8[rule_format])
next
   fix s::"'a trace"
   assume "s @ [tick] ∈ DIVERGENCES (⋂ a::nat. ℱ (S a), ⋂ a::nat. 𝒟 (S a)) "
   thus   "s ∈ DIVERGENCES (⋂ a::nat. ℱ (S a), ⋂ a::nat. 𝒟 (S a))"
          by(auto simp: DIVERGENCES_def FAILURES_def
                  intro: is_processT9[rule_format])
qed



lemmas Rep_Abs_LUB = Abs_process_inverse[simplified Rep_process, 
                                         simplified, OF is_process_REP_LUB,
                                         simplified]

lemma F_LUB: "chain S ⟹ ℱ(lim_proc(range S)) = ⋂ (ℱ ` range S)"
by(simp add: lim_proc_def , subst Failures_def, auto simp: FAILURES_def Rep_Abs_LUB)

lemma D_LUB: "chain S ⟹ 𝒟(lim_proc(range S)) = ⋂ (𝒟 ` range S)"
by(simp add: lim_proc_def , subst Divergences_def, auto simp: DIVERGENCES_def Rep_Abs_LUB)

lemma T_LUB: "chain S ⟹ 𝒯 (lim_proc(range S)) = ⋂ (𝒯  ` range S)"
apply(simp add: lim_proc_def , subst Traces_def) 
apply(simp add: TRACES_def FAILURES_def Rep_Abs_LUB)
apply(auto intro: F_T, rule_tac x="{}" in exI, auto intro: T_F)
done

schematic_goal D_LUB_2: "chain S ⟹ t ∈ 𝒟(lim_proc(range S)) =  ?X"
apply(subst D_LUB, simp)
apply(rule trans, simp)
apply(simp)
done

schematic_goal T_LUB_2: "chain S ⟹ (t ∈ 𝒯 (lim_proc (range S))) = ?X"
apply(subst T_LUB, simp)
apply(rule trans, simp)
apply(simp)
done


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
   process :: (type) ord          
begin

definition  le_ref_def   : "P ≤ Q ≡ 𝒟 Q ⊆ 𝒟 P ∧ ℱ Q ⊆ ℱ P"

definition  less_ref_def : "(P::'a process) < 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_approx_implies_le_ref:    "(P::'α process) ⊑ Q ⟹ P ≤ Q"
by(simp add: le_ref_def le_approx1 le_approx_lemma_F)

lemma le_ref1:                     "P ≤ Q ⟹ 𝒟 Q ⊆ 𝒟 P"
by(simp add: le_ref_def) 

lemma le_ref2:                     "P≤Q ⟹ ℱ Q ⊆ ℱ P"
by(simp add: le_ref_def) 

lemma le_ref2T :                    "P≤Q ⟹ 𝒯 Q ⊆ 𝒯 P"
  by (rule subsetI) (simp add: T_F_spec[symmetric] le_ref2[THEN subsetD])


instance  process :: (type) order
proof
   fix P Q R :: "'α process"
   {
     show "(P < Q) = (P ≤ Q ∧ ¬ Q ≤  P)"
       by(auto simp: le_ref_def less_ref_def Process_eq_spec)
   next
     show "P ≤ P"  by(simp add: le_ref_def)
   next
     assume "P ≤ Q" and "Q ≤ R" then show "P ≤ R"
       by (simp add: le_ref_def, auto)
   next
     assume "P ≤ Q" and "Q ≤ P" then show "P = Q"
       by(auto simp: le_ref_def Process_eq_spec)  
   }
qed

lemma lim_proc_is_ub:"chain S ⟹ range S <| lim_proc (range S)" 
  apply(auto simp: is_ub_def le_approx_def F_LUB D_LUB T_LUB Ra_def) 
  using chain_lemma is_processT8 le_approx2 apply blast 
  using D_T chain_lemma le_approx2T le_approx_def by blast

lemma lim_proc_is_lub1: "chain S ⟹ ∀ u . (range S <| u ⟶  𝒟 u ⊆ 𝒟 (lim_proc (range S)))"
  by(auto simp: D_LUB, frule_tac i=a in Porder.ub_rangeD, auto dest: le_approx1)

lemma lim_proc_is_lub2: 
  "chain S ⟹ ∀ u . range S <| u ⟶ (∀ s.  s ∉ 𝒟 (lim_proc (range S))
   ⟶ Ra (lim_proc (range S)) s = Ra u s)" 
    apply(auto simp: is_ub_def D_LUB F_LUB Ra_def)
    using proc_ord2a apply blast
    using is_processT8_S proc_ord2a by blast


lemma lim_proc_is_lub3a: "front_tickFree s ⟹ s ∉ 𝒟 P ⟶ (∀t. t ∈ 𝒟 P ⟶ ¬ t < s @ [c])" 
apply(rule impI, erule contrapos_np, auto)
  apply(auto simp: le_list_def  less_list_def)
  by (metis butlast_append butlast_snoc front_tickFree_mono is_processT self_append_conv)



lemma lim_proc_is_lub3b:
assumes 1 : "∀x. x ∈ X ⟶ (∀xa. xa ∈ 𝒟 x ∧ (∀t. t ∈ 𝒟 x ⟶ ¬ t < xa) ⟶ xa ∈ 𝒯  u)"
and     2 : "xa ∈ X"
and     3 : "∀xa. xa ∈ X ⟶ x ∈ 𝒟 xa"
and     4 : "∀t. (∀x. x ∈ X ⟶ t ∈ 𝒟 x) ⟶ ¬ t < x"
shows       "x ∈ 𝒯  u"
proof (cases "∀t. t ∈ 𝒟 xa ⟶ ¬ t < x") 
      case True  from ‹∀t. t ∈ 𝒟 xa ⟶ ¬ t < x›  show ?thesis using 1 2 3  by simp
next
      case False from ‹¬(∀t. t ∈ 𝒟 xa ⟶ ¬ t < x)› and 3 4
                 have A: "∃y r c. y ∈ X ∧ r ∉ 𝒟 y ∧ r ∈ 𝒟 xa ∧ r @ [c] = x" 
                         by (metis D_imp_front_tickFree front_tickFree_charn 
                                   less_self lim_proc_is_lub3a nil_less 
                                   tickFree_implies_front_tickFree)
           show ?thesis
              apply(insert A) apply(erule exE)+
              using "1" "3" D_imp_front_tickFree lim_proc_is_lub3a by blast
qed

lemma lim_proc_is_lub3c: 
assumes *:"chain S"
and     **:"X = range S"  ―‹protection for range - otherwise auto unfolds and gets lost›
shows   "∀ u. X <| u ⟶  min_elems(𝒟 (lim_proc X)) ⊆ 𝒯  u"
proof -
  have B : "𝒟 (lim_proc X) = ⋂ (𝒟 ` X)" by(simp add: * ** D_LUB)
  show ?thesis
     apply(auto simp: is_ub_def * **)
     apply(auto simp: B min_elems_def le_approx_def HOL.imp_conjR HOL.all_conj_distrib Ball_def)
      apply(simp add: subset_iff imp_conjL[symmetric])
    apply(rule lim_proc_is_lub3b[of "range S", simplified])
    using "**" B by auto
qed

lemma limproc_is_lub: "chain S ⟹ range S <<| lim_proc (range S)"
apply (auto simp: is_lub_def lim_proc_is_ub)
apply (simp add: le_approx_def is_lub_def lim_proc_is_ub)
by (simp add: lim_proc_is_lub1 lim_proc_is_lub2 lim_proc_is_lub3c)

lemma limproc_is_thelub: "chain S ⟹ Lub S = lim_proc (range S)"
by (frule limproc_is_lub,frule Porder.po_class.lub_eqI, simp)


instance
   process :: (type) cpo
proof
   fix S ::"nat ⇒ 'α process"
   assume C:"chain S" 
   thus "∃ x. range S <<| x" using limproc_is_lub by blast
qed

instance
   process :: (type) pcpo
proof
  show "∃ x::'a process. ∀ y::'a process. x ⊑ y" 
   proof -
      have is_process_witness : 
           "is_process({(s,X). front_tickFree s},{d. front_tickFree d})"
           apply(auto simp:is_process_def FAILURES_def DIVERGENCES_def)
           apply(auto elim!: tickFree_implies_front_tickFree front_tickFree_dw_closed
                             front_tickFree_append)
           done
      have bot_inverse : 
           "Rep_process(Abs_process({(s, X). front_tickFree s},Collect front_tickFree))=
                          ({(s, X). front_tickFree s}, Collect front_tickFree)"
           by(subst Abs_process_inverse, simp_all add: Rep_process is_process_witness)
      have divergences_frontTickFree:
           "⋀y x. x ∈ snd (Rep_process y) ⟹ front_tickFree x" 
           by(rule D_imp_front_tickFree, simp add: Divergences_def DIVERGENCES_def)
      have failures_frontTickFree:
           "⋀y s x. (s, x) ∈ fst (Rep_process y) ⟹ front_tickFree s"
           by(rule is_processT2[rule_format], 
              simp add: Failures_def FAILURES_def)
      have minelems_contains_mt:
           "⋀y x. x ∈ min_elems (Collect front_tickFree) ⟹ x = []"
           by(simp add: min_elems_def front_tickFree_charn,safe, 
              auto simp: Nil_elem_T)
      show ?thesis 
      apply(rule_tac x="Abs_process ({(s,X). front_tickFree s},{d. front_tickFree d})" 
            in exI)
      apply(auto simp: le_approx_def bot_inverse Ra_def 
                       Failures_def Divergences_def FAILURES_def DIVERGENCES_def
                       divergences_frontTickFree failures_frontTickFree)
      apply (metis minelems_contains_mt Nil_elem_T )
      done
   qed
qed


section‹ Process Refinement is Admissible ›

lemma le_adm[simp]: "cont (u::('a::cpo) ⇒ 'b process) ⟹ monofun v ⟹ adm(λx. u x ≤ v x)"
proof(auto simp add:le_ref_def cont2contlubE adm_def, goal_cases)
  case (1 Y x)
  hence "v (Y i)  ⊑ v (⨆i. Y i)" for i by (simp add: is_ub_thelub monofunE)
  hence "𝒟 (v (⨆i. Y i)) ⊆ 𝒟 (u (Y i))" for i using "1"(4) le_approx1 by blast    
  then show ?case 
    using D_LUB[OF ch2ch_cont[OF 1(1) 1(3)]] limproc_is_thelub[OF ch2ch_cont[OF 1(1) 1(3)]] "1"(5) by force
next
  case (2 Y a b)
  hence "v (Y i)  ⊑ v (⨆i. Y i)" for i by (simp add: is_ub_thelub monofunE)
  hence "ℱ (v (⨆i. Y i)) ⊆ ℱ (u (Y i))" for i using "2"(4) le_approx_lemma_F by blast   
  then show ?case
    using F_LUB[OF ch2ch_cont[OF 2(1) 2(3)]] limproc_is_thelub[OF ch2ch_cont[OF 2(1) 2(3)]] "2"(5) by force
qed

lemmas le_adm_cont[simp] = le_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]: 
  assumes *:"(⋀x. P x ⟹ cont ((f::'c ⇒ ('a::cpo) ⇒ 'b process) x))"
  and     **:"(⋀x. ¬ P x ⟹ cont (g x))"
  shows "⋀x. cont(λy. if P x then f x y else g x y)"
  using * ** by (auto simp:cont_def)


end