Quelle  AWN_Cterms.thy

(*  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 ↝_<Gamma> p2"  ⇌ "CONST microstep Γ p1 p2"
  "p1 ↝_<Gamma>^* p2" ⇌ "CONST microstep_rtcl Γ p1 p2"
  "p1 ↝_<Gamma>⁺ p2" ⇌ "CONST microstep_tcl Γ p1 p2"

lemma microstep_choiceD [dest]:
  "(p1 ⊕ p2) ↝_<Gamma> p ==> p = p1 ∨ p = p2"
  by (ind_cases "(p1 ⊕ p2) ↝_<Gamma> p") auto

lemma microstep_choiceE [elim]:
  "[ (p1 ⊕ p2) ↝_<Gamma> p;
     (p1 ⊕ p2) ↝_<Gamma> p1 ==> P;
     (p1 ⊕ p2) ↝_<Gamma> p2 ==> P ] ==> P"
  by (blast)

lemma microstep_callD [dest]:
  "(call(pn)) ↝_<Gamma> p ==> p = Γ pn"
  by (ind_cases "(call(pn)) ↝_<Gamma> p")

lemma microstep_callE [elim]:
  "[ (call(pn)) ↝_<Gamma> p; p = Γ(pn) ==> P ] ==> P"
  by auto

lemma no_microstep_guard: "¬ (({l}⟨g⟩ p) ↝_<Gamma> q)"
  by (rule notI) (ind_cases "({l}⟨g⟩ p) ↝_<Gamma> q")

lemma no_microstep_assign: "¬ ({l}[f] p) ↝_<Gamma> q"
  by (rule notI) (ind_cases "({l}[f] p) ↝_<Gamma> q")

lemma no_microstep_unicast: "¬ (({l}unicast(s_ip, s_msg).p ▹ q) ↝_<Gamma> r)"
  by (rule notI) (ind_cases "({l}unicast(s_ip, s_msg).p ▹ q) ↝_<Gamma> r")

lemma no_microstep_broadcast: "¬ (({l}broadcast(s_msg).p) ↝_<Gamma> q)"
  by (rule notI) (ind_cases "({l}broadcast(s_msg).p) ↝_<Gamma> q")

lemma no_microstep_groupcast: "¬ (({l}groupcast(s_ips, s_msg).p) ↝_<Gamma> q)"
  by (rule notI) (ind_cases "({l}groupcast(s_ips, s_msg).p) ↝_<Gamma> q")

lemma no_microstep_send: "¬ (({l}send(s_msg).p) ↝_<Gamma> q)"
  by (rule notI) (ind_cases "({l}send(s_msg).p) ↝_<Gamma> q")

lemma no_microstep_deliver: "¬ (({l}deliver(s_data).p) ↝_<Gamma> q)"
  by (rule notI) (ind_cases "({l}deliver(s_data).p) ↝_<Gamma> q")

lemma no_microstep_receive: "¬ (({l}receive(u_msg).p) ↝_<Gamma> q)"
  by (rule notI) (ind_cases "({l}receive(u_msg).p) ↝_<Gamma> q")

lemma microstep_call_or_choice [dest]:
  assumes "p ↝_<Gamma> 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 "Γ₁(p1) = call(p1)"}

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

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

definition
  wellformed :: "('s, 'm, 'p, 'l) seqp_env ==> bool"
where
  "wellformed Γ = wf {(q, p). p ↝_<Gamma> q}"

lemma wellformed_defP: "wellformed Γ = wfP (λq p. p ↝_<Gamma> 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) ↝_<Gamma> 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)) ↝_<Gamma> 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 ↝_<Gamma> 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 ↝<sub><Gamma></sub> 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 ↝_<Gamma> 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 ↝_<Gamma> q} `` A"
    hence hasnext: "∧p. p ∈ A ==> ∃q. p ↝_<Gamma> 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') ↝_<Gamma> 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) ↝_<Gamma> 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)) ↝_<Gamma> 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 ↝_<Gamma> q'" by auto
        moreover from  ‹q ∈ stermsl (Γ pn)› ‹not_call q› have "¬ (q ↝_<Gamma> 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 ↝_<Gamma> q})"
      by (rule ext)+ (auto simp: sterms_rel.simps elim: microstep.cases)

    from assms have "∀x. x ∈ Wellfounded.acc {(q, p). p ↝_<Gamma> q}"
      unfolding wellformed_def by (simp add: wf_iff_acc)
    hence "p ∈ Wellfounded.acc {(q, p). p ↝_<Gamma> q}" ..

    hence "(Γ, p) ∈ Wellfounded.acc {((Γ, q), (Γ', p)). Γ = Γ' ∧ p ↝_<Gamma> 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 ↝_<Gamma> 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) ↝_<Gamma> 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)) ↝_<Gamma> 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 ↝_<Gamma>^* q"
    shows "q = p"
  using assms(3) proof (rule converse_rtranclpE)
    fix p'
    assume "p ↝_<Gamma> 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 ↝_<Gamma>^* q ∧ sterms Γ q = {q}} = {p}"
  proof (rule set_eqI)
    fix p'
    show "(p' ∈ {q. p ↝_<Gamma>^* q ∧ sterms Γ q = {q}}) = (p' ∈ {p})"
    proof
      assume "p' ∈ {q. p ↝_<Gamma>^* 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 ↝_<Gamma> 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 ↝_<Gamma>^* q ∧ sterms Γ q = {q}}"
        by (cases p) simp_all
    qed
  qed

theorem sterms_maximal_microstep:
  assumes "wellformed Γ"
    shows "sterms Γ p = {q. p ↝_<Gamma>^* q ∧ ¬(∃q'. q ↝_<Gamma> q')}"
  proof
    from ‹wellformed Γ› have "sterms Γ p ⊆ {q. p ↝_<Gamma>^* q ∧ sterms Γ q = {q}}"
    proof induction
     fix p1 p2
     assume IH1: "sterms Γ p1 ⊆ {q. p1 ↝_<Gamma>^* q ∧ sterms Γ q = {q}}"
        and IH2: "sterms Γ p2 ⊆ {q. p2 ↝_<Gamma>^* q ∧ sterms Γ q = {q}}"
     have "sterms Γ p1 ⊆ {q. (p1 ⊕ p2) ↝_<Gamma>^* q ∧ sterms Γ q = {q}}"
     proof
       fix p'
       assume "p' ∈ sterms Γ p1"
       with IH1 have "p1 ↝_<Gamma>^* p'" by auto
       moreover have "(p1 ⊕ p2) ↝_<Gamma> p1" ..
       ultimately have "(p1 ⊕ p2) ↝_<Gamma>^* p'"
         by - (rule converse_rtranclp_into_rtranclp)
       moreover from ‹wellformed Γ› and ‹p' ∈ sterms Γ p1› have "sterms Γ p' = {p'}" ..
       ultimately show "p' ∈ {q. (p1 ⊕ p2) ↝_<Gamma>^* q ∧ sterms Γ q = {q}}"
         by simp
     qed
     moreover have "sterms Γ p2 ⊆ {q. (p1 ⊕ p2) ↝_<Gamma>^* q ∧ sterms Γ q = {q}}"
     proof
       fix p'
       assume "p' ∈ sterms Γ p2"
       with IH2 have "p2 ↝_<Gamma>^* p'" and "sterms Γ p' = {p'}" by auto
       moreover have "(p1 ⊕ p2) ↝_<Gamma> p2" ..
       ultimately have "(p1 ⊕ p2) ↝_<Gamma>^* p'"
         by - (rule converse_rtranclp_into_rtranclp)
       with ‹sterms Γ p' = {p'}› show "p' ∈ {q. (p1 ⊕ p2) ↝_<Gamma>^* q ∧ sterms Γ q = {q}}"
         by simp
     qed
     ultimately show "sterms Γ (p1 ⊕ p2) ⊆ {q. (p1 ⊕ p2) ↝_<Gamma>^* q ∧ sterms Γ q = {q}}"
       using ‹wellformed Γ› by simp
    next
      fix pn
      assume IH: "sterms Γ (Γ pn) ⊆ {q. Γ pn ↝_<Gamma>^* q ∧ sterms Γ q = {q}}"
      show "sterms Γ (call(pn)) ⊆ {q. (call(pn)) ↝_<Gamma>^* q ∧ sterms Γ q = {q}}"
      proof
        fix p'
        assume "p' ∈ sterms Γ (call(pn))"
        with ‹wellformed Γ› have "p' ∈ sterms Γ (Γ pn)" by simp
        with IH have "Γ pn ↝_<Gamma>^* p'" and "sterms Γ p' = {p'}" by auto
        note this(1)
        moreover have "(call(pn)) ↝_<Gamma> Γ pn" by simp
        ultimately have "(call(pn)) ↝_<Gamma>^* p'"
          by - (rule converse_rtranclp_into_rtranclp)
        with ‹sterms Γ p' = {p'}› show "p' ∈ {q. (call(pn)) ↝_<Gamma>^* q ∧ sterms Γ q = {q}}"
          by simp
      qed
    qed simp_all
    with ‹wellformed Γ› show "sterms Γ p ⊆ {q. p ↝_<Gamma>^* q ∧ ¬(∃q'. q ↝_<Gamma> q')}"
      by (simp only: no_microsteps_sterms_refl)
  next
    from ‹wellformed Γ› have "{q. p ↝_<Gamma>^* q ∧ sterms Γ q = {q}} ⊆ sterms Γ p"
    proof (induction)
      fix p1 p2
      assume IH1: "{q. p1 ↝_<Gamma>^* q ∧ sterms Γ q = {q}} ⊆ sterms Γ p1"
         and IH2: "{q. p2 ↝_<Gamma>^* q ∧ sterms Γ q = {q}} ⊆ sterms Γ p2"
      show "{q. (p1 ⊕ p2) ↝_<Gamma>^* q ∧ sterms Γ q = {q}} ⊆ sterms Γ (p1 ⊕ p2)"
      proof (rule, drule CollectD, erule conjE)
        fix q'
        assume "(p1 ⊕ p2) ↝_<Gamma>^* q'"
           and "sterms Γ q' = {q'}"
        with ‹wellformed Γ› have "(p1 ⊕ p2) ↝_<Gamma>⁺ q'"          
          by (auto dest!: rtranclpD sterms_no_choice)
        hence "p1 ↝_<Gamma>^* q' ∨ p2 ↝_<Gamma>^* q'"
          by (auto dest: tranclpD)
        thus "q' ∈ sterms Γ (p1 ⊕ p2)"
        proof
          assume "p1 ↝_<Gamma>^* q'"
          with IH1 and ‹sterms Γ q' = {q'}› have "q' ∈ sterms Γ p1" by auto
          with ‹wellformed Γ› show ?thesis by auto
        next
          assume "p2 ↝_<Gamma>^* 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 ↝_<Gamma>^* q ∧ sterms Γ q = {q}} ⊆ sterms Γ (Γ pn)"
      show   "{q. (call(pn)) ↝_<Gamma>^* q ∧ sterms Γ q = {q}} ⊆ sterms Γ (call(pn))"
      proof (rule, drule CollectD, erule conjE)
        fix q'
        assume "(call(pn)) ↝_<Gamma>^* q'"
           and "sterms Γ q' = {q'}"
        with ‹wellformed Γ› have "(call(pn)) ↝_<Gamma>⁺ q'"
          by (auto dest!: rtranclpD sterms_no_call)
        moreover have "(call(pn)) ↝_<Gamma> Γ pn" ..
        ultimately have "Γ pn ↝_<Gamma>^* 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 ↝_<Gamma>^* q ∧ ¬(∃q'. q ↝_<Gamma> 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_ip, s_msg).p ▹ q) = sterms Γ p ∪ sterms Γ q"
  | "dterms Γ ({l}broadcast(s_msg). p) = sterms Γ p"
  | "dterms Γ ({l}groupcast(s_ips, s_msg). p) = sterms Γ p"
  | "dterms Γ ({l}send(s_msg).p) = sterms Γ p"
  | "dterms Γ ({l}deliver(s_data).p) = sterms Γ p"
  | "dterms Γ ({l}receive(u_msg).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 ↝_<Gamma> q})"
      by (rule ext)+ (auto simp: dterms_rel.simps elim: microstep.cases)
    from ‹wellformed(Γ)› have "∀x. x ∈ Wellfounded.acc {(q, p). p ↝_<Gamma> q}"
      unfolding wellformed_def by (simp add: wf_iff_acc)
    hence "p ∈ Wellfounded.acc {(q, p). p ↝_<Gamma> q}" ..
    hence "(Γ, p) ∈ Wellfounded.acc {((Γ, q), Γ', p). Γ = Γ' ∧ p ↝_<Gamma> 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_ip, s_msg). p ▹ q) = insert ({l}unicast(s_ip, s_msg). p ▹ q)
                                                                      (ctermsl p ∪ ctermsl q)"
  | "ctermsl ({l}broadcast(s_msg). p) = insert ({l}broadcast(s_msg). p) (ctermsl p)"
  | "ctermsl ({l}groupcast(s_ips, s_msg). p) = insert ({l}groupcast(s_ips, s_msg). p) (ctermsl p)"
  | "ctermsl ({l}send(s_msg). p) = insert ({l}send(s_msg). p) (ctermsl p)"
  | "ctermsl ({l}deliver(s_data). p) = insert ({l}deliver(s_data). p) (ctermsl p)"
  | "ctermsl ({l}receive(u_msg). p) = insert ({l}receive(u_msg). 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