Theory AWN_Cterms

(*  Title:       AWN_Cterms.thy
    License:     BSD 2-Clause. See LICENSE.
    Author:      Timothy Bourke
*)

section "Control terms and well-definedness of sequential processes"

theory AWN_Cterms
imports AWN
begin

subsection "Microsteps "

text ‹
  We distinguish microsteps from `external' transitions (observable or not). Here, they are
  a kind of `hypothetical computation', since, unlike ‹τ›-transitions, they do not make
  choices but rather `compute' which choices are possible.
›

inductive
  microstep :: "('s, 'm, 'p, 'l) seqp_env
                ⇒ ('s, 'm, 'p, 'l) seqp
                ⇒ ('s, 'm, 'p, 'l) seqp
                ⇒ bool"
for Γ :: "('s, 'm, 'p, 'l) seqp_env"
where
    microstep_choiceI1 [intro, simp]: "microstep Γ (p1 ⊕ p2) p1"
  | microstep_choiceI2 [intro, simp]: "microstep Γ (p1 ⊕ p2) p2"
  | microstep_callI [intro, simp]: "microstep Γ (call(pn)) (Γ pn)"

abbreviation microstep_rtcl
where "microstep_rtcl Γ p q ≡ (microstep Γ)⇧*⇧* p q"

abbreviation microstep_tcl
where "microstep_tcl Γ p q ≡ (microstep Γ)⇧+⇧+ p q"

syntax
  "_microstep"
     :: "[('s, 'm, 'p, 'l) seqp, ('s, 'm, 'p, 'l) seqp_env, ('s, 'm, 'p, 'l) seqp] ⇒ bool"
     (‹(_) ↝⇘_⇙ (_)› [61, 0, 61] 50)
  "_microstep_rtcl"
     :: "[('s, 'm, 'p, 'l) seqp, ('s, 'm, 'p, 'l) seqp_env, ('s, 'm, 'p, 'l) seqp] ⇒ bool"
     (‹(_) ↝⇘_⇙⇧* (_)› [61, 0, 61] 50)
  "_microstep_tcl"
     :: "[('s, 'm, 'p, 'l) seqp, ('s, 'm, 'p, 'l) seqp_env, ('s, 'm, 'p, 'l) seqp] ⇒ bool"
     (‹(_) ↝⇘_⇙⇧+ (_)› [61, 0, 61] 50)

syntax_consts
  "_microstep" ⇌ microstep and
  "_microstep_rtcl" ⇌ microstep_rtcl and
  "_microstep_tcl" ⇌ microstep_tcl

translations
  "p1 ↝⇘Γ⇙ p2"  ⇌ "CONST microstep Γ p1 p2"
  "p1 ↝⇘Γ⇙⇧* p2" ⇌ "CONST microstep_rtcl Γ p1 p2"
  "p1 ↝⇘Γ⇙⇧+ p2" ⇌ "CONST microstep_tcl Γ p1 p2"

lemma microstep_choiceD [dest]:
  "(p1 ⊕ p2) ↝⇘Γ⇙ p ⟹ p = p1 ∨ p = p2"
  by (ind_cases "(p1 ⊕ p2) ↝⇘Γ⇙ p") auto

lemma microstep_choiceE [elim]:
  "⟦ (p1 ⊕ p2) ↝⇘Γ⇙ p;
     (p1 ⊕ p2) ↝⇘Γ⇙ p1 ⟹ P;
     (p1 ⊕ p2) ↝⇘Γ⇙ p2 ⟹ P ⟧ ⟹ P"
  by (blast)

lemma microstep_callD [dest]:
  "(call(pn)) ↝⇘Γ⇙ p ⟹ p = Γ pn"
  by (ind_cases "(call(pn)) ↝⇘Γ⇙ p")

lemma microstep_callE [elim]:
  "⟦ (call(pn)) ↝⇘Γ⇙ p;  p = Γ(pn) ⟹ P ⟧ ⟹ P"
  by auto

lemma no_microstep_guard: "¬ (({l}⟨g⟩ p) ↝⇘Γ⇙ q)"
  by (rule notI) (ind_cases "({l}⟨g⟩ p) ↝⇘Γ⇙ q")

lemma no_microstep_assign: "¬ ({l}⟦f⟧ p) ↝⇘Γ⇙ q"
  by (rule notI) (ind_cases "({l}⟦f⟧ p) ↝⇘Γ⇙ q")

lemma no_microstep_unicast: "¬ (({l}unicast(s⇩i⇩p, s⇩m⇩s⇩g).p ▹ q) ↝⇘Γ⇙ r)"
  by (rule notI) (ind_cases "({l}unicast(s⇩i⇩p, s⇩m⇩s⇩g).p ▹ q) ↝⇘Γ⇙ r")

lemma no_microstep_broadcast: "¬ (({l}broadcast(s⇩m⇩s⇩g).p) ↝⇘Γ⇙ q)"
  by (rule notI) (ind_cases "({l}broadcast(s⇩m⇩s⇩g).p) ↝⇘Γ⇙ q")

lemma no_microstep_groupcast: "¬ (({l}groupcast(s⇩i⇩p⇩s, s⇩m⇩s⇩g).p) ↝⇘Γ⇙ q)"
  by (rule notI) (ind_cases "({l}groupcast(s⇩i⇩p⇩s, s⇩m⇩s⇩g).p) ↝⇘Γ⇙ q")

lemma no_microstep_send: "¬ (({l}send(s⇩m⇩s⇩g).p) ↝⇘Γ⇙ q)"
  by (rule notI) (ind_cases "({l}send(s⇩m⇩s⇩g).p) ↝⇘Γ⇙ q")

lemma no_microstep_deliver: "¬ (({l}deliver(s⇩d⇩a⇩t⇩a).p) ↝⇘Γ⇙ q)"
  by (rule notI) (ind_cases "({l}deliver(s⇩d⇩a⇩t⇩a).p) ↝⇘Γ⇙ q")

lemma no_microstep_receive: "¬ (({l}receive(u⇩m⇩s⇩g).p) ↝⇘Γ⇙ q)"
  by (rule notI) (ind_cases "({l}receive(u⇩m⇩s⇩g).p) ↝⇘Γ⇙ q")

lemma microstep_call_or_choice [dest]:
  assumes "p ↝⇘Γ⇙ q"
    shows "(∃pn. p = call(pn)) ∨ (∃p1 p2. p = p1 ⊕ p2)"
  using assms by clarsimp (metis microstep.simps)

lemmas no_microstep [intro,simp] =
  no_microstep_guard
  no_microstep_assign
  no_microstep_unicast
  no_microstep_broadcast
  no_microstep_groupcast
  no_microstep_send
  no_microstep_deliver
  no_microstep_receive

subsection "Wellformed process specifications "

text ‹
  A process specification ‹Γ› is wellformed if its @{term "microstep Γ"} relation is
  free of loops and infinite chains.

  For example, these specifications are not wellformed:
    @{term "Γ⇩1(p1) = call(p1)"}

    @{term "Γ⇩2(p1) = send(msg).call(p1) ⊕ call(p1)"}

    @{term "Γ⇩3(p1) = send(msg).call(p2)"}
    @{term "Γ⇩3(p2) = call(p3)"}
    @{term "Γ⇩3(p3) = call(p4)"}
    @{term "Γ⇩3(p4) = call(p5)"}
    \ldots
›

definition
  wellformed :: "('s, 'm, 'p, 'l) seqp_env ⇒ bool"
where
  "wellformed Γ = wf {(q, p). p ↝⇘Γ⇙ q}"

lemma wellformed_defP: "wellformed Γ = wfP (λq p. p ↝⇘Γ⇙ q)"
  unfolding wellformed_def wfp_def by simp

text ‹
  The induction rule for @{term "wellformed Γ"} is stronger than @{thm seqp.induct} because
  the case for @{term "call(pn)"} can be shown with the assumption on @{term "Γ pn"}.
›

lemma wellformed_induct
  [consumes 1, case_names ASSIGN CHOICE CALL GUARD UCAST BCAST GCAST SEND DELIVER RECEIVE,
   induct set: wellformed]:
  assumes "wellformed Γ"
      and ASSIGN:  "⋀l f p.          wellformed Γ ⟹ P ({l}⟦f⟧ p)"
      and GUARD:   "⋀l f p.          wellformed Γ ⟹ P ({l}⟨f⟩ p)"
      and UCAST:   "⋀l fip fmsg p q. wellformed Γ ⟹ P ({l}unicast(fip, fmsg). p ▹ q)"
      and BCAST:   "⋀l fmsg p.       wellformed Γ ⟹ P ({l}broadcast(fmsg). p)"
      and GCAST:   "⋀l fips fmsg p.  wellformed Γ ⟹ P ({l}groupcast(fips, fmsg). p)"
      and SEND:    "⋀l fmsg p.       wellformed Γ ⟹ P ({l}send(fmsg). p)"
      and DELIVER: "⋀l fdata p.      wellformed Γ ⟹ P ({l}deliver(fdata). p)"
      and RECEIVE: "⋀l fmsg p.       wellformed Γ ⟹ P ({l}receive(fmsg). p)"
      and CHOICE:  "⋀p1 p2.        ⟦ wellformed Γ; P p1; P p2 ⟧ ⟹ P (p1 ⊕ p2)"
      and CALL:    "⋀pn.           ⟦ wellformed Γ; P (Γ pn) ⟧ ⟹ P (call(pn))"
    shows "P a"
  using assms(1) unfolding wellformed_defP
  proof (rule wfp_induct_rule, case_tac x, simp_all)
    fix p1 p2
    assume "⋀q. (p1 ⊕ p2) ↝⇘Γ⇙ q ⟹ P q"
    then obtain "P p1" and "P p2" by (auto intro!: microstep.intros)
    thus "P (p1 ⊕ p2)" by (rule CHOICE [OF ‹wellformed Γ›])
  next
    fix pn
    assume "⋀q. (call(pn)) ↝⇘Γ⇙ q ⟹ P q"
    hence "P (Γ pn)" by (auto intro!: microstep.intros)
    thus "P (call(pn))" by (rule CALL [OF ‹wellformed Γ›])
  qed (auto intro: assms)

subsection "Start terms (sterms) "

text ‹
  Formulate sets of local subterms from which an action is directly possible. Since the
  process specification @{term "Γ"} is not considered, only choice terms @{term "p1 ⊕ p2"}
  are traversed, and not @{term "call(p)"} terms.
›

fun stermsl :: "('s, 'm, 'p, 'l) seqp ⇒ ('s, 'm, 'p , 'l) seqp set"
where
    "stermsl (p1 ⊕ p2) = stermsl p1 ∪ stermsl p2"
  | "stermsl p          = {p}"

lemma stermsl_nobigger: "q ∈ stermsl p ⟹ size q ≤ size p"
  by (induct p) auto

lemma stermsl_no_choice[simp]: "p1 ⊕ p2 ∉ stermsl p"
  by (induct p) simp_all

lemma stermsl_choice_disj[simp]:
  "p ∈ stermsl (p1 ⊕ p2) = (p ∈ stermsl p1 ∨ p ∈ stermsl p2)"
  by simp

lemma stermsl_in_branch[elim]:
  "⟦p ∈ stermsl (p1 ⊕ p2); p ∈ stermsl p1 ⟹ P; p ∈ stermsl p2 ⟹ P⟧ ⟹ P"
  by auto

lemma stermsl_commute:
  "stermsl (p1 ⊕ p2) = stermsl (p2 ⊕ p1)"
  by simp (rule Un_commute)

lemma stermsl_not_empty:
  "stermsl p ≠ {}"
  by (induct p) auto

lemma stermsl_idem [simp]:
  "(⋃q∈stermsl p. stermsl q) = stermsl p"
  by (induct p) simp_all

lemma stermsl_in_wfpf:
  assumes AA: "A ⊆ {(q, p). p ↝⇘Γ⇙ q} `` A"
      and *: "p ∈ A"
    shows "∃r∈stermsl p. r ∈ A"
  using *
  proof (induction p)
    fix p1 p2
    assume IH1: "p1 ∈ A ⟹ ∃r∈stermsl p1. r ∈ A"
       and IH2: "p2 ∈ A ⟹ ∃r∈stermsl p2. r ∈ A"
       and *: "p1 ⊕ p2 ∈ A"
    from * and AA have "p1 ⊕ p2 ∈ {(q, p). p ↝⇘Γ⇙ q} `` A" by auto
    hence "p1 ∈ A ∨ p2 ∈ A" by auto
    hence "(∃r∈stermsl p1. r ∈ A) ∨ (∃r∈stermsl p2. r ∈ A)"
      proof
        assume "p1 ∈ A" hence "∃r∈stermsl p1. r ∈ A" by (rule IH1) thus ?thesis ..
      next
        assume "p2 ∈ A" hence "∃r∈stermsl p2. r ∈ A" by (rule IH2) thus ?thesis ..
      qed
      hence "∃r∈stermsl p1 ∪ stermsl p2. r ∈ A" by blast
      thus "∃r∈stermsl (p1 ⊕ p2). r ∈ A" by simp
    next case UCAST from UCAST.prems show ?case by auto
  qed auto

lemma nocall_stermsl_max:
  assumes "r ∈ stermsl p"
      and "not_call r"
    shows "¬ (r ↝⇘Γ⇙ q)"
  using assms
  by (induction p) auto

theorem wf_no_direct_calls[intro]:
    fixes Γ :: "('s, 'm, 'p, 'l) seqp_env"
  assumes no_calls: "⋀pn. ∀pn'. call(pn') ∉ stermsl(Γ(pn))"
    shows "wellformed Γ"
  unfolding wellformed_def wfp_def
  proof (rule wfI_pf)
    fix A
    assume ARA: "A ⊆ {(q, p). p ↝⇘Γ⇙ q} `` A"
    hence hasnext: "⋀p. p ∈ A ⟹ ∃q. p ↝⇘Γ⇙ q ∧ q ∈ A" by auto
    show "A = {}"
    proof (rule Set.equals0I)
      fix p assume "p ∈ A" thus "False"
      proof (induction p)
        fix l f p'
        assume *: "{l}⟨f⟩ p' ∈ A"
        from hasnext [OF *] have "∃q. ({l}⟨f⟩ p') ↝⇘Γ⇙ q" by simp
        thus "False" by simp
      next
        fix p1 p2
        assume *: "p1 ⊕ p2 ∈ A"
         and IH1: "p1 ∈ A ⟹ False"
         and IH2: "p2 ∈ A ⟹ False"
        have "∃q. (p1 ⊕ p2) ↝⇘Γ⇙ q ∧ q ∈ A" by (rule hasnext [OF *])
        hence "p1 ∈ A ∨ p2 ∈ A" by auto
        thus "False" by (auto dest: IH1 IH2)
      next
        fix pn
        assume "call(pn) ∈ A"
        hence "∃q. (call(pn)) ↝⇘Γ⇙ q ∧ q ∈ A" by (rule hasnext)
        hence "Γ(pn) ∈ A" by auto

        with ARA [THEN stermsl_in_wfpf] obtain q where "q∈stermsl (Γ pn)" and "q ∈ A" by metis
        hence "not_call q" using no_calls [of pn]
          unfolding not_call_def by auto

        from hasnext [OF ‹q ∈ A›] obtain q' where "q ↝⇘Γ⇙ q'" by auto
        moreover from  ‹q ∈ stermsl (Γ pn)› ‹not_call q› have "¬ (q ↝⇘Γ⇙ q')"
          by (rule nocall_stermsl_max)
        ultimately show "False" by simp
      qed (auto dest: hasnext)
    qed
  qed

subsection "Start terms"

text ‹
  The start terms are those terms, relative to a wellformed process specification ‹Γ›,
  from which transitions can occur directly.
›

function (domintros, sequential) sterms
  :: "('s, 'm, 'p, 'l) seqp_env ⇒ ('s, 'm, 'p, 'l) seqp ⇒ ('s, 'm, 'p, 'l) seqp set"
  where
    sterms_choice: "sterms Γ (p1 ⊕ p2)  = sterms Γ p1 ∪ sterms Γ p2"
  | sterms_call:   "sterms Γ (call(pn))  = sterms Γ (Γ pn)"
  | sterms_other:  "sterms Γ p           = {p}"
  by pat_completeness auto

lemma sterms_dom_basic[simp]:
  assumes "not_call p"
      and "not_choice p"
    shows "sterms_dom (Γ, p)"
  proof (rule accpI)
    fix y
    assume "sterms_rel y (Γ, p)"
    with assms show "sterms_dom y"
      by (cases p) (auto simp: sterms_rel.simps)
  qed

lemma sterms_termination:
  assumes "wellformed Γ"
    shows "sterms_dom (Γ, p)"
  proof -
    have sterms_rel':
      "sterms_rel = (λgq gp. (gq, gp) ∈ {((Γ, q), (Γ', p)). Γ = Γ' ∧ p ↝⇘Γ⇙ q})"
      by (rule ext)+ (auto simp: sterms_rel.simps elim: microstep.cases)

    from assms have "∀x. x ∈ Wellfounded.acc {(q, p). p ↝⇘Γ⇙ q}"
      unfolding wellformed_def by (simp add: wf_iff_acc)
    hence "p ∈ Wellfounded.acc {(q, p). p ↝⇘Γ⇙ q}" ..

    hence "(Γ, p) ∈ Wellfounded.acc {((Γ, q), (Γ', p)). Γ = Γ' ∧ p ↝⇘Γ⇙ q}"
      by (rule acc_induct) (auto intro: accI)

    thus "sterms_dom (Γ, p)" unfolding sterms_rel' accp_acc_eq .
  qed

declare sterms.psimps [simp]

lemmas sterms_psimps[simp] = sterms.psimps [OF sterms_termination]
   and sterms_pinduct = sterms.pinduct [OF sterms_termination]

lemma sterms_reflD [dest]:
  assumes "q ∈ sterms Γ p"
      and "not_choice p" "not_call p"
    shows "q = p"
  using assms by (cases p) auto

lemma sterms_choice_disj [simp]:
  assumes "wellformed Γ"
    shows "p ∈ sterms Γ (p1 ⊕ p2) = (p ∈ sterms Γ p1 ∨ p ∈ sterms Γ p2)"
  using assms by (simp)

lemma sterms_no_choice [simp]:
  assumes "wellformed Γ"
    shows "p1 ⊕ p2 ∉ sterms Γ p"
  using assms by induction auto

lemma sterms_not_choice [simp]:
  assumes "wellformed Γ"
      and "q ∈ sterms Γ p"
    shows "not_choice q"
  using assms unfolding not_choice_def
  by (auto dest: sterms_no_choice)

lemma sterms_no_call [simp]:
  assumes "wellformed Γ"
    shows "call(pn) ∉ sterms Γ p"
  using assms by induction auto

lemma sterms_not_call [simp]:
  assumes "wellformed Γ"
      and "q ∈ sterms Γ p"
    shows "not_call q"
  using assms unfolding not_call_def
  by (auto dest: sterms_no_call)

lemma sterms_in_branch:
  assumes "wellformed Γ"
      and "p ∈ sterms Γ (p1 ⊕ p2)"
      and "p ∈ sterms Γ p1 ⟹ P"
      and "p ∈ sterms Γ p2 ⟹ P"
  shows "P"
  using assms by auto

lemma sterms_commute:
  assumes "wellformed Γ"
    shows "sterms Γ (p1 ⊕ p2) = sterms Γ (p2 ⊕ p1)"
  using assms by simp (rule Un_commute)

lemma sterms_not_empty:
  assumes "wellformed Γ"
    shows "sterms Γ p ≠ {}"
  using assms
  by (induct p rule: sterms_pinduct [OF ‹wellformed Γ›]) simp_all

lemma sterms_sterms [simp]:
  assumes "wellformed Γ"
    shows "(⋃x∈sterms Γ p. sterms Γ x) = sterms Γ p"
  using assms by induction simp_all

lemma sterms_stermsl:
  assumes "ps ∈ sterms Γ p"
      and "wellformed Γ"
    shows "ps ∈ stermsl p ∨ (∃pn. ps ∈ stermsl (Γ pn))"
  using assms by (induction p rule: sterms_pinduct [OF ‹wellformed Γ›]) auto

lemma stermsl_sterms [elim]:
  assumes "q ∈ stermsl p"
      and "not_call q"
      and "wellformed Γ"
    shows "q ∈ sterms Γ p"
  using assms by (induct p) auto

lemma sterms_stermsl_heads:
  assumes "ps ∈ sterms Γ (Γ pn)"
      and "wellformed Γ"
    shows "∃pn. ps ∈ stermsl (Γ pn)"
  proof -
    from assms have "ps ∈ stermsl (Γ pn) ∨ (∃pn'. ps ∈ stermsl (Γ pn'))"
      by (rule sterms_stermsl)
    thus ?thesis by auto
  qed

lemma sterms_subterms [dest]:
  assumes "wellformed Γ"
      and "∃pn. p ∈ subterms (Γ pn)"
      and "q ∈ sterms Γ p"
    shows "∃pn. q ∈ subterms (Γ pn)"
  using assms by (induct p) auto

lemma no_microsteps_sterms_refl:
  assumes "wellformed Γ"
  shows "(¬(∃q. p ↝⇘Γ⇙ q)) = (sterms Γ p = {p})"
  proof (cases p)
    fix p1 p2
    assume "p = p1 ⊕ p2"
    from ‹wellformed Γ› have "p1 ⊕ p2 ∉ sterms Γ (p1 ⊕ p2)" by simp
    hence "sterms Γ (p1 ⊕ p2) ≠ {p1 ⊕ p2}" by auto
    moreover have "∃q. (p1 ⊕ p2) ↝⇘Γ⇙ q" by auto
    ultimately show ?thesis
      using ‹p = p1 ⊕ p2› by simp
  next
    fix pn
    assume "p = call(pn)"
    from ‹wellformed Γ› have "call(pn) ∉ sterms Γ (call(pn))" by simp
    hence "sterms Γ (call(pn)) ≠ {call(pn)}" by auto
    moreover have "∃q. (call(pn)) ↝⇘Γ⇙ q" by auto
    ultimately show ?thesis
      using ‹p = call(pn)› by simp
  qed simp_all

lemma sterms_maximal [elim]:
  assumes "wellformed Γ"
      and "q ∈ sterms Γ p"
    shows "sterms Γ q = {q}"
  using assms by (cases q) auto

lemma microstep_rtranscl_equal:
  assumes "not_call p"
      and "not_choice p"
      and "p ↝⇘Γ⇙⇧* q"
    shows "q = p"
  using assms(3) proof (rule converse_rtranclpE)
    fix p'
    assume "p ↝⇘Γ⇙ p'"
    with assms(1-2) show "q = p"
      by (cases p) simp_all
  qed simp

lemma microstep_rtranscl_singleton [simp]:
  assumes "not_call p"
      and "not_choice p"
    shows "{q. p ↝⇘Γ⇙⇧* q ∧ sterms Γ q = {q}} = {p}"
  proof (rule set_eqI)
    fix p'
    show "(p' ∈ {q. p ↝⇘Γ⇙⇧* q ∧ sterms Γ q = {q}}) = (p' ∈ {p})"
    proof
      assume "p' ∈ {q. p ↝⇘Γ⇙⇧* q ∧ sterms Γ q = {q}}"
      hence "(microstep Γ)⇧*⇧* p p'" and "sterms Γ p' = {p'}" by auto
      from this(1) have "p' = p"
      proof (rule converse_rtranclpE)
        fix q assume "p ↝⇘Γ⇙ q"
        with ‹not_call p› and ‹not_choice p› have False
          by (cases p) auto
        thus "p' = p" ..
      qed simp
      thus "p' ∈ {p}" by simp
    next
      assume "p' ∈ {p}"
      hence "p' = p" ..
      with ‹not_call p› and ‹not_choice p› show "p' ∈ {q. p ↝⇘Γ⇙⇧* q ∧ sterms Γ q = {q}}"
        by (cases p) simp_all
    qed
  qed

theorem sterms_maximal_microstep:
  assumes "wellformed Γ"
    shows "sterms Γ p = {q. p ↝⇘Γ⇙⇧* q ∧ ¬(∃q'. q ↝⇘Γ⇙ q')}"
  proof
    from ‹wellformed Γ› have "sterms Γ p ⊆ {q. p ↝⇘Γ⇙⇧* q ∧ sterms Γ q = {q}}"
    proof induction
     fix p1 p2
     assume IH1: "sterms Γ p1 ⊆ {q. p1 ↝⇘Γ⇙⇧* q ∧ sterms Γ q = {q}}"
        and IH2: "sterms Γ p2 ⊆ {q. p2 ↝⇘Γ⇙⇧* q ∧ sterms Γ q = {q}}"
     have "sterms Γ p1 ⊆ {q. (p1 ⊕ p2) ↝⇘Γ⇙⇧* q ∧ sterms Γ q = {q}}"
     proof
       fix p'
       assume "p' ∈ sterms Γ p1"
       with IH1 have "p1 ↝⇘Γ⇙⇧* p'" by auto
       moreover have "(p1 ⊕ p2) ↝⇘Γ⇙ p1" ..
       ultimately have "(p1 ⊕ p2) ↝⇘Γ⇙⇧* p'"
         by - (rule converse_rtranclp_into_rtranclp)
       moreover from ‹wellformed Γ› and ‹p' ∈ sterms Γ p1› have "sterms Γ p' = {p'}" ..
       ultimately show "p' ∈ {q. (p1 ⊕ p2) ↝⇘Γ⇙⇧* q ∧ sterms Γ q = {q}}"
         by simp
     qed
     moreover have "sterms Γ p2 ⊆ {q. (p1 ⊕ p2) ↝⇘Γ⇙⇧* q ∧ sterms Γ q = {q}}"
     proof
       fix p'
       assume "p' ∈ sterms Γ p2"
       with IH2 have "p2 ↝⇘Γ⇙⇧* p'" and "sterms Γ p' = {p'}" by auto
       moreover have "(p1 ⊕ p2) ↝⇘Γ⇙ p2" ..
       ultimately have "(p1 ⊕ p2) ↝⇘Γ⇙⇧* p'"
         by - (rule converse_rtranclp_into_rtranclp)
       with ‹sterms Γ p' = {p'}› show "p' ∈ {q. (p1 ⊕ p2) ↝⇘Γ⇙⇧* q ∧ sterms Γ q = {q}}"
         by simp
     qed
     ultimately show "sterms Γ (p1 ⊕ p2) ⊆ {q. (p1 ⊕ p2) ↝⇘Γ⇙⇧* q ∧ sterms Γ q = {q}}"
       using ‹wellformed Γ› by simp
    next
      fix pn
      assume IH: "sterms Γ (Γ pn) ⊆ {q. Γ pn ↝⇘Γ⇙⇧* q ∧ sterms Γ q = {q}}"
      show "sterms Γ (call(pn)) ⊆ {q. (call(pn)) ↝⇘Γ⇙⇧* q ∧ sterms Γ q = {q}}"
      proof
        fix p'
        assume "p' ∈ sterms Γ (call(pn))"
        with ‹wellformed Γ› have "p' ∈ sterms Γ (Γ pn)" by simp
        with IH have "Γ pn ↝⇘Γ⇙⇧* p'" and "sterms Γ p' = {p'}" by auto
        note this(1)
        moreover have "(call(pn)) ↝⇘Γ⇙ Γ pn" by simp
        ultimately have "(call(pn)) ↝⇘Γ⇙⇧* p'"
          by - (rule converse_rtranclp_into_rtranclp)
        with ‹sterms Γ p' = {p'}› show "p' ∈ {q. (call(pn)) ↝⇘Γ⇙⇧* q ∧ sterms Γ q = {q}}"
          by simp
      qed
    qed simp_all
    with ‹wellformed Γ› show "sterms Γ p ⊆ {q. p ↝⇘Γ⇙⇧* q ∧ ¬(∃q'. q ↝⇘Γ⇙ q')}"
      by (simp only: no_microsteps_sterms_refl)
  next
    from ‹wellformed Γ› have "{q. p ↝⇘Γ⇙⇧* q ∧ sterms Γ q = {q}} ⊆ sterms Γ p"
    proof (induction)
      fix p1 p2
      assume IH1: "{q. p1 ↝⇘Γ⇙⇧* q ∧ sterms Γ q = {q}} ⊆ sterms Γ p1"
         and IH2: "{q. p2 ↝⇘Γ⇙⇧* q ∧ sterms Γ q = {q}} ⊆ sterms Γ p2"
      show "{q. (p1 ⊕ p2) ↝⇘Γ⇙⇧* q ∧ sterms Γ q = {q}} ⊆ sterms Γ (p1 ⊕ p2)"
      proof (rule, drule CollectD, erule conjE)
        fix q'
        assume "(p1 ⊕ p2) ↝⇘Γ⇙⇧* q'"
           and "sterms Γ q' = {q'}"
        with ‹wellformed Γ› have "(p1 ⊕ p2) ↝⇘Γ⇙⇧+ q'"          
          by (auto dest!: rtranclpD sterms_no_choice)
        hence "p1 ↝⇘Γ⇙⇧* q' ∨ p2 ↝⇘Γ⇙⇧* q'"
          by (auto dest: tranclpD)
        thus "q' ∈ sterms Γ (p1 ⊕ p2)"
        proof
          assume "p1 ↝⇘Γ⇙⇧* q'"
          with IH1 and ‹sterms Γ q' = {q'}› have "q' ∈ sterms Γ p1" by auto
          with ‹wellformed Γ› show ?thesis by auto
        next
          assume "p2 ↝⇘Γ⇙⇧* q'"
          with IH2 and ‹sterms Γ q' = {q'}› have "q' ∈ sterms Γ p2" by auto
          with ‹wellformed Γ› show ?thesis by auto
        qed
      qed
    next
      fix pn
      assume IH: "{q. Γ pn ↝⇘Γ⇙⇧* q ∧ sterms Γ q = {q}} ⊆ sterms Γ (Γ pn)"
      show   "{q. (call(pn)) ↝⇘Γ⇙⇧* q ∧ sterms Γ q = {q}} ⊆ sterms Γ (call(pn))"
      proof (rule, drule CollectD, erule conjE)
        fix q'
        assume "(call(pn)) ↝⇘Γ⇙⇧* q'"
           and "sterms Γ q' = {q'}"
        with ‹wellformed Γ› have "(call(pn)) ↝⇘Γ⇙⇧+ q'"
          by (auto dest!: rtranclpD sterms_no_call)
        moreover have "(call(pn)) ↝⇘Γ⇙ Γ pn" ..
        ultimately have "Γ pn ↝⇘Γ⇙⇧* q'"
          by (auto dest!: tranclpD)
        with ‹sterms Γ q' = {q'}› and IH have "q' ∈ sterms Γ (Γ pn)" by auto
        with ‹wellformed Γ› show "q' ∈ sterms Γ (call(pn))" by simp
      qed
    qed simp_all
    with ‹wellformed Γ› show "{q. p ↝⇘Γ⇙⇧* q ∧ ¬(∃q'. q ↝⇘Γ⇙ q')} ⊆ sterms Γ p"
    by (simp only: no_microsteps_sterms_refl)
  qed

subsection "Derivative terms "

text ‹
  The derivatives of a term are those @{term sterm}s potentially reachable by taking a
  transition, relative to a wellformed process specification ‹Γ›. These terms
  overapproximate the reachable sterms, since the truth of guards is not considered.
›

function (domintros) dterms
  :: "('s, 'm, 'p, 'l) seqp_env ⇒ ('s, 'm, 'p, 'l) seqp ⇒ ('s, 'm, 'p, 'l) seqp set"
  where
    "dterms Γ ({l}⟨g⟩ p)                     = sterms Γ p"
  | "dterms Γ ({l}⟦u⟧ p)                     = sterms Γ p"
  | "dterms Γ (p1 ⊕ p2)                     = dterms Γ p1 ∪ dterms Γ p2"
  | "dterms Γ ({l}unicast(s⇩i⇩p, s⇩m⇩s⇩g).p ▹ q)  = sterms Γ p ∪ sterms Γ q"
  | "dterms Γ ({l}broadcast(s⇩m⇩s⇩g). p)        = sterms Γ p"
  | "dterms Γ ({l}groupcast(s⇩i⇩p⇩s, s⇩m⇩s⇩g). p)  = sterms Γ p"
  | "dterms Γ ({l}send(s⇩m⇩s⇩g).p)              = sterms Γ p"
  | "dterms Γ ({l}deliver(s⇩d⇩a⇩t⇩a).p)          = sterms Γ p"
  | "dterms Γ ({l}receive(u⇩m⇩s⇩g).p)           = sterms Γ p"
  | "dterms Γ (call(pn))                     = dterms Γ (Γ pn)"
  by pat_completeness auto

lemma dterms_dom_basic [simp]:
  assumes "not_call p"
      and "not_choice p"
    shows "dterms_dom (Γ, p)"
  proof (rule accpI)
    fix y
    assume "dterms_rel y (Γ, p)"
    with assms show "dterms_dom y"
      by (cases p) (auto simp: dterms_rel.simps)
  qed

lemma dterms_termination:
  assumes "wellformed Γ"
    shows "dterms_dom (Γ, p)"
  proof -
    have dterms_rel': "dterms_rel = (λgq gp. (gq, gp) ∈ {((Γ, q), (Γ', p)). Γ = Γ' ∧ p ↝⇘Γ⇙ q})"
      by (rule ext)+ (auto simp: dterms_rel.simps elim: microstep.cases)
    from ‹wellformed(Γ)› have "∀x. x ∈ Wellfounded.acc {(q, p). p ↝⇘Γ⇙ q}"
      unfolding wellformed_def by (simp add: wf_iff_acc)
    hence "p ∈ Wellfounded.acc {(q, p). p ↝⇘Γ⇙ q}" ..
    hence "(Γ, p) ∈ Wellfounded.acc {((Γ, q), Γ', p). Γ = Γ' ∧ p ↝⇘Γ⇙ q}"
      by (rule acc_induct) (auto intro: accI)
    thus "dterms_dom (Γ, p)"
      unfolding dterms_rel' by (subst accp_acc_eq)
  qed

lemmas dterms_psimps [simp] = dterms.psimps [OF dterms_termination]
   and dterms_pinduct = dterms.pinduct [OF dterms_termination]

lemma sterms_after_dterms [simp]:
  assumes "wellformed Γ"
  shows "(⋃x∈dterms Γ p. sterms Γ x) = dterms Γ p"
  using assms by (induction p) simp_all

lemma sterms_before_dterms [simp]:
  assumes "wellformed Γ"
  shows "(⋃x∈sterms Γ p. dterms Γ x) = dterms Γ p"
  using assms by (induction p) simp_all

lemma dterms_choice_disj [simp]:
  assumes "wellformed Γ"
    shows "p ∈ dterms Γ (p1 ⊕ p2) = (p ∈ dterms Γ p1 ∨ p ∈ dterms Γ p2)"
  using assms by (simp)

lemma dterms_in_branch:
  assumes "wellformed Γ"
      and "p ∈ dterms Γ (p1 ⊕ p2)"
      and "p ∈ dterms Γ p1 ⟹ P"
      and "p ∈ dterms Γ p2 ⟹ P"
  shows "P"
  using assms by auto

lemma dterms_no_choice:
  assumes "wellformed Γ"
    shows "p1 ⊕ p2 ∉ dterms Γ p"
  using assms by induction simp_all

lemma dterms_not_choice [simp]:
  assumes "wellformed Γ"
      and "q ∈ dterms Γ p"
    shows "not_choice q"
  using assms unfolding not_choice_def
  by (auto dest: dterms_no_choice)

lemma dterms_no_call:
  assumes "wellformed Γ"
    shows "call(pn) ∉ dterms Γ p"
  using assms by induction simp_all

lemma dterms_not_call [simp]:
  assumes "wellformed Γ"
      and "q ∈ dterms Γ p"
    shows "not_call q"
  using assms unfolding not_call_def
  by (auto dest: dterms_no_call)

lemma dterms_subterms:
  assumes wf: "wellformed Γ"
      and "∃pn. p ∈ subterms (Γ pn)"
      and "q ∈ dterms Γ p"
    shows "∃pn. q ∈ subterms (Γ pn)"
  using assms
  proof (induct p)
       fix p1 p2
    assume IH1: "∃pn. p1 ∈ subterms (Γ pn) ⟹ q ∈ dterms Γ p1 ⟹ ∃pn. q ∈ subterms (Γ pn)"
       and IH2: "∃pn. p2 ∈ subterms (Γ pn) ⟹ q ∈ dterms Γ p2 ⟹ ∃pn. q ∈ subterms (Γ pn)"
       and *: "∃pn. p1 ⊕ p2 ∈ subterms (Γ pn)"
       and "q ∈ dterms Γ (p1 ⊕ p2)"
    from * obtain pn where "p1 ⊕ p2 ∈ subterms (Γ pn)"
      by auto
    hence "p1 ∈ subterms (Γ pn)" and "p2 ∈ subterms (Γ pn)"
      by auto
    from ‹q ∈ dterms Γ (p1 ⊕ p2)› wf have "q ∈ dterms Γ p1 ∨ q ∈ dterms Γ p2"
      by auto
    thus "∃pn. q ∈ subterms (Γ pn)"
      proof
        assume "q ∈ dterms Γ p1"
        with ‹p1 ∈ subterms (Γ pn)› show ?thesis
          by (auto intro: IH1)
      next
        assume "q ∈ dterms Γ p2"
        with ‹p2 ∈ subterms (Γ pn)› show ?thesis
          by (auto intro: IH2)
      qed
  qed auto

text ‹
  Note that the converse of @{thm dterms_subterms} is not true because @{term dterm}s are an
  over-approximation; i.e., we cannot show, in general, that guards return a non-empty set
  of post-states.
›

subsection "Control terms "

text ‹
  The control terms of a process specification @{term Γ} are those subterms from which
  transitions are directly possible. We can omit @{term "call(pn)"} terms, since
  the root terms of all processes are considered, and also @{term "p1 ⊕ p2"} terms
  since they effectively combine the transitions of the subterms @{term p1} and
  @{term p2}.

  It will be shown that only the control terms, rather than all subterms, need be
  considered in invariant proofs.
›

inductive_set
  cterms :: "('s, 'm, 'p, 'l) seqp_env ⇒ ('s, 'm, 'p, 'l) seqp set"
  for Γ :: "('s, 'm, 'p, 'l) seqp_env"
where
    ctermsSI[intro]: "p ∈ sterms Γ (Γ pn) ⟹ p ∈ cterms Γ"
  | ctermsDI[intro]: "⟦ pp ∈ cterms Γ; p ∈ dterms Γ pp ⟧ ⟹ p ∈ cterms Γ"

lemma cterms_not_choice [simp]:
  assumes "wellformed Γ"
      and "p ∈ cterms Γ"
    shows "not_choice p"
  using assms
  proof (cases p)
    case CHOICE from ‹p ∈ cterms Γ› show ?thesis
      using ‹wellformed Γ› by cases simp_all
  qed simp_all

lemma cterms_no_choice [simp]:
  assumes "wellformed Γ"
    shows "p1 ⊕ p2 ∉ cterms Γ"
  using assms by (auto dest: cterms_not_choice)

lemma cterms_not_call [simp]:
  assumes "wellformed Γ"
      and "p ∈ cterms Γ"
    shows "not_call p"
  using assms
  proof (cases p)
    case CALL from ‹p ∈ cterms Γ› show ?thesis
      using ‹wellformed Γ› by cases simp_all
  qed simp_all

lemma cterms_no_call [simp]:
  assumes "wellformed Γ"
    shows "call(pn) ∉ cterms Γ"
  using assms by (auto dest: cterms_not_call)

lemma sterms_cterms [elim]:
  assumes "p ∈ cterms Γ"
      and "q ∈ sterms Γ p"
      and "wellformed Γ"
    shows "q ∈ cterms Γ"
  using assms by - (cases p, auto)

lemma dterms_cterms [elim]:
  assumes "p ∈ cterms Γ"
      and "q ∈ dterms Γ p"
      and "wellformed Γ"
    shows "q ∈ cterms Γ"
  using assms by (cases p) auto

lemma derivs_in_cterms [simp]:
  "⋀l f p. {l}⟨f⟩ p ∈ cterms Γ                            ⟹ sterms Γ p ⊆ cterms Γ"
  "⋀l f p. {l}⟦f⟧ p ∈ cterms Γ                           ⟹ sterms Γ p ⊆ cterms Γ"
  "⋀l fip fmsg q p. {l}unicast(fip, fmsg). p ▹ q ∈ cterms Γ
                            ⟹ sterms Γ p ⊆ cterms Γ ∧ sterms Γ q ⊆ cterms Γ"
  "⋀l fmsg p.      {l}broadcast(fmsg).p ∈ cterms Γ       ⟹ sterms Γ p ⊆ cterms Γ"
  "⋀l fips fmsg p. {l}groupcast(fips, fmsg).p ∈ cterms Γ ⟹ sterms Γ p ⊆ cterms Γ"
  "⋀l fmsg p.      {l}send(fmsg).p ∈ cterms Γ            ⟹ sterms Γ p ⊆ cterms Γ"
  "⋀l fdata p.     {l}deliver(fdata).p ∈ cterms Γ        ⟹ sterms Γ p ⊆ cterms Γ"
  "⋀l fmsg p.      {l}receive(fmsg).p ∈ cterms Γ         ⟹ sterms Γ p ⊆ cterms Γ"
  by (auto simp: dterms.psimps)

subsection "Local control terms"

text ‹
  We introduce a `local' version of @{term cterms} that does not step through calls and,
  thus, that is defined independently of a process specification @{term Γ}.
  This allows an alternative, terminating characterisation of cterms as a set of
  subterms. Including @{term "call(pn)"}s in the set makes for a simpler relation with
  @{term "stermsl"}, even if they must be filtered out for the desired characterisation.
›

function
  ctermsl :: "('s, 'm, 'p, 'l) seqp ⇒ ('s, 'm, 'p , 'l) seqp set"
where
    "ctermsl ({l}⟨g⟩ p)                     = insert ({l}⟨g⟩ p)  (ctermsl p)"
  | "ctermsl ({l}⟦u⟧ p)                     = insert ({l}⟦u⟧ p)  (ctermsl p)"
  | "ctermsl ({l}unicast(s⇩i⇩p, s⇩m⇩s⇩g). p ▹ q) = insert ({l}unicast(s⇩i⇩p, s⇩m⇩s⇩g). p ▹ q)
                                                                      (ctermsl p ∪ ctermsl q)"
  | "ctermsl ({l}broadcast(s⇩m⇩s⇩g). p)       = insert ({l}broadcast(s⇩m⇩s⇩g). p)       (ctermsl p)"
  | "ctermsl ({l}groupcast(s⇩i⇩p⇩s, s⇩m⇩s⇩g). p)  = insert ({l}groupcast(s⇩i⇩p⇩s, s⇩m⇩s⇩g). p) (ctermsl p)"
  | "ctermsl ({l}send(s⇩m⇩s⇩g). p)            = insert ({l}send(s⇩m⇩s⇩g). p)            (ctermsl p)"
  | "ctermsl ({l}deliver(s⇩d⇩a⇩t⇩a). p)        = insert ({l}deliver(s⇩d⇩a⇩t⇩a). p)        (ctermsl p)"
  | "ctermsl ({l}receive(u⇩m⇩s⇩g). p)         = insert ({l}receive(u⇩m⇩s⇩g). p)         (ctermsl p)"
  | "ctermsl (p1 ⊕ p2)                    = ctermsl p1 ∪ ctermsl p2"
  | "ctermsl (call(pn))                   = {call(pn)}"
  by pat_completeness auto
  termination by (relation "measure(size)") (auto dest: stermsl_nobigger)

lemmas ctermsl_induct =
  ctermsl.induct [case_names GUARD ASSIGN UCAST BCAST GCAST
                             SEND DELIVER RECEIVE CHOICE CALL]

lemma ctermsl_refl [intro]: "not_choice p ⟹ p ∈ ctermsl p"
  by (cases p) auto

lemma ctermsl_subterms:
  "ctermsl p = {q. q ∈ subterms p ∧ not_choice q }" (is "?lhs = ?rhs")
  proof
    show "?lhs ⊆ ?rhs" by (induct p, auto) next
    show "?rhs ⊆ ?lhs" by (induct p, auto)
  qed

lemma ctermsl_trans [elim]:
  assumes "q ∈ ctermsl p"
      and "r ∈ ctermsl q"
    shows "r ∈ ctermsl p"
  using assms
  proof (induction p rule: ctermsl_induct)
    case (CHOICE p1 p2)
      have "(q ∈ ctermsl p1) ∨ (q ∈ ctermsl p2)"
        using CHOICE.prems(1) by simp
      hence "r ∈ ctermsl p1 ∨ r ∈ ctermsl p2"
      proof (rule disj_forward)
        assume "q ∈ ctermsl p1"
        thus "r ∈ ctermsl p1" using ‹r ∈ ctermsl q› by (rule CHOICE.IH)
      next
        assume "q ∈ ctermsl p2"
        thus "r ∈ ctermsl p2" using ‹r ∈ ctermsl q› by (rule CHOICE.IH)
      qed
      thus "r ∈ ctermsl (p1 ⊕ p2)" by simp
    qed auto

lemma ctermsl_ex_trans [elim]:
  assumes "∃q ∈ ctermsl p. r ∈ ctermsl q"
    shows "r ∈ ctermsl p"
  using assms by auto

lemma call_ctermsl_empty [elim]:
  "⟦ p ∈ ctermsl p'; not_call p ⟧ ⟹ not_call p'"
  unfolding not_call_def by (cases p) auto

lemma stermsl_ctermsl_choice1 [simp]:
  assumes "q ∈ stermsl p1"
    shows "q ∈ ctermsl (p1 ⊕ p2)"
  using assms by (induction p1) auto

lemma stermsl_ctermsl_choice2 [simp]:
  assumes "q ∈ stermsl p2"
    shows "q ∈ ctermsl (p1 ⊕ p2)"
  using assms by (induction p2) auto

lemma stermsl_ctermsl [elim]:
  assumes "q ∈ stermsl p"
    shows "q ∈ ctermsl p"
  using assms
  proof (cases p)
    case (CHOICE p1 p2)
    hence "q ∈ stermsl (p1 ⊕ p2)" using assms by simp
    hence "q ∈ stermsl p1 ∨ q ∈ stermsl p2" by simp
    hence "q ∈ ctermsl (p1 ⊕ p2)" by (rule) (simp_all del: ctermsl.simps)
    thus  "q ∈ ctermsl p" using CHOICE by simp
  qed simp_all

lemma stermsl_after_ctermsl [simp]:
  "(⋃x∈ctermsl p. stermsl x) = ctermsl p"
  by (induct p) auto

lemma stermsl_before_ctermsl [simp]:
  "(⋃x∈stermsl p. ctermsl x) = ctermsl p"
  by (induct p) simp_all

lemma ctermsl_no_choice: "p1 ⊕ p2 ∉ ctermsl p"
  by (induct p) simp_all

lemma ctermsl_ex_stermsl: "q ∈ ctermsl p ⟹ ∃ps∈stermsl p. q ∈ ctermsl ps"
  by (induct p) auto

lemma dterms_ctermsl [intro]:
  assumes "q ∈ dterms Γ p"
      and "wellformed Γ"
    shows "q ∈ ctermsl p ∨ (∃pn. q ∈ ctermsl (Γ pn))"
  using assms(1-2)
  proof (induction p rule: dterms_pinduct [OF ‹wellformed Γ›])
    fix Γ l fg p
    assume "q ∈ dterms Γ ({l}⟨fg⟩ p)"
       and "wellformed Γ"
    hence "q ∈ sterms Γ p" by simp
    hence "q ∈ stermsl p ∨ (∃pn. q ∈ stermsl (Γ pn))"
      using ‹wellformed Γ›  by (rule sterms_stermsl)
    thus "q ∈ ctermsl ({l}⟨fg⟩ p) ∨ (∃pn. q ∈ ctermsl (Γ pn))"
    proof
      assume "q ∈ stermsl p"
      hence "q ∈ ctermsl p" by (rule stermsl_ctermsl)
      hence "q ∈ ctermsl ({l}⟨fg⟩ p)" by simp
      thus ?thesis ..
    next
      assume "∃pn. q ∈ stermsl (Γ pn)"
      then obtain pn where "q ∈ stermsl (Γ pn)" by auto
      hence "q ∈ ctermsl (Γ pn)" by (rule stermsl_ctermsl)
      hence "∃pn. q ∈ ctermsl (Γ pn)" ..
      thus ?thesis ..
    qed
  next
    fix Γ p1 p2
    assume "q ∈ dterms Γ (p1 ⊕ p2)"
       and IH1: "⟦ q ∈ dterms Γ p1; wellformed Γ ⟧ ⟹ q ∈ ctermsl p1 ∨ (∃pn. q ∈ ctermsl (Γ pn))"
       and IH2: "⟦ q ∈ dterms Γ p2; wellformed Γ ⟧ ⟹ q ∈ ctermsl p2 ∨ (∃pn. q ∈ ctermsl (Γ pn))"
       and "wellformed Γ"
    thus "q ∈ ctermsl (p1 ⊕ p2) ∨ (∃pn. q ∈ ctermsl (Γ pn))"
      by auto
  next
    fix Γ pn
    assume "q ∈ dterms Γ (call(pn))"
       and "wellformed Γ"
       and "⟦ q ∈ dterms Γ (Γ pn); wellformed Γ ⟧ ⟹ q ∈ ctermsl (Γ pn) ∨ (∃pn. q ∈ ctermsl (Γ pn))"
    thus "q ∈ ctermsl (call(pn)) ∨ (∃pn. q ∈ ctermsl (Γ pn))"
      by auto
  qed (simp_all, (metis sterms_stermsl stermsl_ctermsl)+)

lemma ctermsl_cterms [elim]:
  assumes "q ∈ ctermsl p"
      and "not_call q"
      and "sterms Γ p ⊆ cterms Γ"
      and "wellformed Γ"
    shows "q ∈ cterms Γ"
  using assms by (induct p rule: ctermsl.induct) auto

subsection "Local deriviative terms"

text ‹
  We define local @{term "dterm"}s for use in the theorem that relates @{term "cterms"}
  and sets of @{term "ctermsl"}.
›

function dtermsl
  :: "('s, 'm, 'p, 'l) seqp ⇒ ('s, 'm, 'p, 'l) seqp set"
  where
    "dtermsl ({l}⟨fg⟩ p)                     = stermsl p"
  | "dtermsl ({l}⟦fa⟧ p)                     = stermsl p"
  | "dtermsl (p1 ⊕ p2)                      = dtermsl p1 ∪ dtermsl p2"
  | "dtermsl ({l}unicast(fip, fmsg).p ▹ q)  = stermsl p ∪ stermsl q"
  | "dtermsl ({l}broadcast(fmsg). p)         = stermsl p"
  | "dtermsl ({l}groupcast(fips, fmsg). p)   = stermsl p"
  | "dtermsl ({l}send(fmsg).p)               = stermsl p"
  | "dtermsl ({l}deliver(fdata).p)           = stermsl p"
  | "dtermsl ({l}receive(fmsg).p)            = stermsl p"
  | "dtermsl (call(pn))                      = {}"
  by pat_completeness auto
  termination by (relation "measure(size)") (auto dest: stermsl_nobigger)

lemma stermsl_after_dtermsl [simp]:
  shows "(⋃x∈dtermsl p. stermsl x) = dtermsl p"
  by (induct p) simp_all

lemma stermsl_before_dtermsl [simp]:
  "(⋃x∈stermsl p. dtermsl x) = dtermsl p"
  by (induct p) simp_all

lemma dtermsl_no_choice [simp]: "p1 ⊕ p2 ∉ dtermsl p"
  by (induct p) simp_all

lemma dtermsl_choice_disj [simp]:
  "p ∈ dtermsl (p1 ⊕ p2) = (p ∈ dtermsl p1 ∨ p ∈ dtermsl p2)"
  by simp

lemma dtermsl_in_branch [elim]:
  "⟦p ∈ dtermsl (p1 ⊕ p2); p ∈ dtermsl p1 ⟹ P; p ∈ dtermsl p2 ⟹ P⟧ ⟹ P"
  by auto

lemma ctermsl_dtermsl [elim]:
  assumes "q ∈ dtermsl p"
    shows "q ∈ ctermsl p"
  using assms by (induct p) (simp_all, (metis stermsl_ctermsl)+)

lemma dtermsl_dterms [elim]:
  assumes "q ∈ dtermsl p"
      and "not_call q"
      and "wellformed Γ"
    shows "q ∈ dterms Γ p"
  using assms
  using assms by (induct p) (simp_all, (metis stermsl_sterms)+)

lemma ctermsl_stermsl_or_dtermsl:
  assumes "q ∈ ctermsl p"
    shows "q ∈ stermsl p ∨ (∃p'∈dtermsl p. q ∈ ctermsl p')"
  using assms by (induct p) (auto dest: ctermsl_ex_stermsl)

lemma dtermsl_add_stermsl_beforeD:
  assumes "q ∈ dtermsl p"
    shows "∃ps∈stermsl p. q ∈ dtermsl ps"
  proof -
    from assms have "q ∈ (⋃x∈stermsl p. dtermsl x)" by auto
    thus ?thesis
      by (rule UN_E) auto
  qed

lemma call_dtermsl_empty [elim]:
 "q ∈ dtermsl p ⟹ not_call p"
  by (cases p) simp_all

subsection "More properties of control terms"

text ‹
  We now show an alternative definition of @{term "cterms"} based on sets of local control
  terms. While the original definition has convenient induction and simplification rules,
  useful for proving properties like cterms\_includes\_sterms\_of\_seq\_reachable, this
  definition makes it easier to systematically generate the set of control terms of a
  process specification.
›

theorem cterms_def':
  assumes wfg: "wellformed Γ"
    shows "cterms Γ = { p |p pn. p ∈ ctermsl (Γ pn) ∧ not_call p }"
          (is "_ = ?ctermsl_set")
  proof (rule iffI [THEN set_eqI])
    fix p
    assume "p ∈ cterms Γ"
    thus "p ∈ ?ctermsl_set"
    proof (induction p)
      fix p pn
      assume "p ∈ sterms Γ (Γ pn)"
      then obtain pn' where "p ∈ stermsl (Γ pn')" using wfg
        by (blast dest: sterms_stermsl_heads)
      hence "p ∈ ctermsl (Γ pn')" ..
      moreover from ‹p ∈ sterms Γ (Γ pn)› wfg have "not_call p" by simp
      ultimately show "p ∈ ?ctermsl_set" by auto
    next
      fix pp p
      assume "pp ∈ cterms Γ"
         and IH: "pp ∈ ?ctermsl_set"
         and *: "p ∈ dterms Γ pp"
      from * have "p ∈ ctermsl pp ∨ (∃pn. p ∈ ctermsl (Γ pn))"
        using wfg by (rule dterms_ctermsl)
      hence "∃pn. p ∈ ctermsl (Γ pn)"
        proof
          assume "p ∈ ctermsl pp"
          from ‹pp ∈ cterms Γ› and IH obtain pn' where "pp ∈ ctermsl (Γ pn')"
            by auto
          with ‹p ∈ ctermsl pp› have "p ∈ ctermsl (Γ pn')" by auto
          thus "∃pn. p ∈ ctermsl (Γ pn)" ..
        qed -
      moreover from ‹p ∈ dterms Γ pp› wfg have "not_call p" by simp
      ultimately show "p ∈ ?ctermsl_set" by auto
    qed
  next
    fix p
    assume "p ∈ ?ctermsl_set"
    then obtain pn where *: "p ∈ ctermsl (Γ pn)" and "not_call p" by auto
    from * have "p ∈ stermsl (Γ pn) ∨ (∃p'∈dtermsl (Γ pn). p ∈ ctermsl p')"
      by (rule ctermsl_stermsl_or_dtermsl)
    thus "p ∈ cterms Γ"
    proof
      assume "p ∈ stermsl (Γ pn)"
      hence "p ∈ sterms Γ (Γ pn)" using ‹not_call p› wfg ..
      thus "p ∈ cterms Γ" ..
    next
      assume "∃p'∈dtermsl (Γ pn). p ∈ ctermsl p'"
      then obtain p' where p'1: "p' ∈ dtermsl (Γ pn)"
                       and p'2: "p ∈ ctermsl p'" ..
      from p'2 and ‹not_call p› have "not_call p'" ..
      from p'1 obtain ps where ps1: "ps ∈ stermsl (Γ pn)"
                           and ps2: "p' ∈ dtermsl ps"
        by (blast dest: dtermsl_add_stermsl_beforeD)
      from ps2 have "not_call ps" ..
      with ps1 have "ps ∈ cterms Γ" using wfg by auto
      with ‹p' ∈ dtermsl ps› and ‹not_call p'› have "p' ∈ cterms Γ" using wfg by auto
      hence "sterms Γ p' ⊆ cterms Γ" using wfg by auto
      with ‹p ∈ ctermsl p'› ‹not_call p› show "p ∈ cterms Γ" using wfg ..
    qed
  qed

lemma ctermsE [elim]:
  assumes "wellformed Γ"
      and "p ∈ cterms Γ"
  obtains pn where "p ∈ ctermsl (Γ pn)"
               and "not_call p"
  using assms(2) unfolding cterms_def' [OF assms(1)] by auto

corollary cterms_subterms:
  assumes "wellformed Γ"
    shows "cterms Γ = {p|p pn. p∈subterms (Γ pn) ∧ not_call p ∧ not_choice p}"
  by (subst cterms_def' [OF assms(1)], subst ctermsl_subterms) auto

lemma subterms_in_cterms [elim]:
  assumes "wellformed Γ"
      and "p∈subterms (Γ pn)"
      and "not_call p"
      and "not_choice p"
    shows "p ∈ cterms Γ"
  using assms unfolding cterms_subterms [OF ‹wellformed Γ›] by auto

lemma subterms_stermsl_ctermsl:
  assumes "q ∈ subterms p"
      and "r ∈ stermsl q"
    shows "r ∈ ctermsl p"
  using assms
  proof (induct p)
    fix p1 p2
    assume IH1: "q ∈ subterms p1 ⟹ r ∈ stermsl q ⟹ r ∈ ctermsl p1"
       and IH2: "q ∈ subterms p2 ⟹ r ∈ stermsl q ⟹ r ∈ ctermsl p2"
       and *: "q ∈ subterms (p1 ⊕ p2)"
       and "r ∈ stermsl q"
    from * have "q ∈ {p1 ⊕ p2} ∪ subterms p1 ∪ subterms p2" by simp
    thus "r ∈ ctermsl (p1 ⊕ p2)"
    proof (elim UnE)
      assume "q ∈ {p1 ⊕ p2}" with ‹r ∈ stermsl q› show ?thesis
      by simp (metis stermsl_ctermsl)
    next
      assume "q ∈ subterms p1" hence "r ∈ ctermsl p1" using ‹r ∈ stermsl q› by (rule IH1)
      thus ?thesis by simp
    next
      assume "q ∈ subterms p2" hence "r ∈ ctermsl p2" using ‹r ∈ stermsl q› by (rule IH2)
      thus ?thesis by simp
    qed
  qed auto

lemma subterms_sterms_cterms:
  assumes wf: "wellformed Γ"
      and "p ∈ subterms (Γ pn)"
    shows "sterms Γ p ⊆ cterms Γ"
  using assms(2)
  proof (induct p)
    fix p
    assume "call(p) ∈ subterms (Γ pn)"
    from wf have "sterms Γ (call(p)) = sterms Γ (Γ p)" by simp
      thus "sterms Γ (call(p)) ⊆ cterms Γ" by auto
  next
    fix p1 p2
    assume IH1: "p1 ∈ subterms (Γ pn) ⟹ sterms Γ p1 ⊆ cterms Γ"
       and IH2: "p2 ∈ subterms (Γ pn) ⟹ sterms Γ p2 ⊆ cterms Γ"
       and *: "p1 ⊕ p2 ∈ subterms (Γ pn)"
    from * have "p1 ∈ subterms (Γ pn)" by auto
    hence "sterms Γ p1 ⊆ cterms Γ" by (rule IH1)
    moreover from * have "p2 ∈ subterms (Γ pn)" by auto
      hence "sterms Γ p2 ⊆ cterms Γ" by (rule IH2)
    ultimately show "sterms Γ (p1 ⊕ p2 ) ⊆ cterms Γ" using wf by simp
  qed (auto elim!: subterms_in_cterms [OF ‹wellformed Γ›])

lemma subterms_sterms_in_cterms:
  assumes "wellformed Γ"
      and "p ∈ subterms (Γ pn)"
      and "q ∈ sterms Γ p"
    shows "q ∈ cterms Γ"
  using assms
  by (auto dest!: subterms_sterms_cterms [OF ‹wellformed Γ›])

end