# Theory Process

theory Process
imports Stream
```(*  Title:      HOL/Datatype_Examples/Process.thy
Author:     Andrei Popescu, TU Muenchen

Processes.
*)

section ‹Processes›

theory Process
imports "HOL-Library.Stream"
begin

codatatype 'a process =
isAction: Action (prefOf: 'a) (contOf: "'a process") |
isChoice: Choice (ch1Of: "'a process") (ch2Of: "'a process")

(* Read: prefix of, continuation of, choice 1 of, choice 2 of *)

subsection ‹Basic properties›

(* Constructors versus discriminators *)
theorem isAction_isChoice:
"isAction p ∨ isChoice p"
by (rule process.exhaust_disc) auto

theorem not_isAction_isChoice: "¬ (isAction p ∧ isChoice p)"
by (cases rule: process.exhaust[of p]) auto

subsection‹Coinduction›

theorem process_coind[elim, consumes 1, case_names iss Action Choice, induct pred: "HOL.eq"]:
assumes phi: "φ p p'" and
iss: "⋀p p'. φ p p' ⟹ (isAction p ⟷ isAction p') ∧ (isChoice p ⟷ isChoice p')" and
Act: "⋀ a a' p p'. φ (Action a p) (Action a' p') ⟹ a = a' ∧ φ p p'" and
Ch: "⋀ p q p' q'. φ (Choice p q) (Choice p' q') ⟹ φ p p' ∧ φ q q'"
shows "p = p'"
using assms
by (coinduct rule: process.coinduct) (metis process.collapse(1,2) process.disc(3))

(* Stronger coinduction, up to equality: *)
theorem process_strong_coind[elim, consumes 1, case_names iss Action Choice]:
assumes phi: "φ p p'" and
iss: "⋀p p'. φ p p' ⟹ (isAction p ⟷ isAction p') ∧ (isChoice p ⟷ isChoice p')" and
Act: "⋀ a a' p p'. φ (Action a p) (Action a' p') ⟹ a = a' ∧ (φ p p' ∨ p = p')" and
Ch: "⋀ p q p' q'. φ (Choice p q) (Choice p' q') ⟹ (φ p p' ∨ p = p') ∧ (φ q q' ∨ q = q')"
shows "p = p'"
using assms
by (coinduct rule: process.coinduct_strong) (metis process.collapse(1,2) process.disc(3))

subsection ‹Coiteration (unfold)›

section‹Coinductive definition of the notion of trace›
coinductive trace where
"trace p as ⟹ trace (Action a p) (a ## as)"
|
"trace p as ∨ trace q as ⟹ trace (Choice p q) as"

section‹Examples of corecursive definitions:›

subsection‹Single-guard fixpoint definition›

primcorec BX where
"isAction BX"
| "prefOf BX = ''a''"
| "contOf BX = BX"

subsection‹Multi-guard fixpoint definitions, simulated with auxiliary arguments›

datatype x_y_ax = x | y | ax

primcorec F :: "x_y_ax ⇒ char list process" where
"xyax = x ⟹ isChoice (F xyax)"
| "ch1Of (F xyax) = F ax"
| "ch2Of (F xyax) = F y"
| "prefOf (F xyax) = (if xyax = y then ''b'' else ''a'')"
| "contOf (F xyax) = F x"

definition "X = F x"  definition "Y = F y"  definition "AX = F ax"

lemma X_Y_AX: "X = Choice AX Y"  "Y = Action ''b'' X"  "AX = Action ''a'' X"
unfolding X_def Y_def AX_def by (subst F.code, simp)+

(* end product: *)
lemma X_AX:
"X = Choice AX (Action ''b'' X)"
"AX = Action ''a'' X"
using X_Y_AX by simp_all

section‹Case study: Multi-guard fixpoint definitions, without auxiliary arguments›

hide_const x y ax X Y AX

(* Process terms *)
datatype ('a,'pvar) process_term =
VAR 'pvar |
PROC "'a process" |
ACT 'a "('a,'pvar) process_term" | CH "('a,'pvar) process_term" "('a,'pvar) process_term"

(* below, sys represents a system of equations *)
fun isACT where
"isACT sys (VAR X) =
(case sys X of ACT a T ⇒ True |PROC p ⇒ isAction p |_ ⇒ False)"
|
"isACT sys (PROC p) = isAction p"
|
"isACT sys (ACT a T) = True"
|
"isACT sys (CH T1 T2) = False"

fun PREF where
"PREF sys (VAR X) =
(case sys X of ACT a T ⇒ a | PROC p ⇒ prefOf p)"
|
"PREF sys (PROC p) = prefOf p"
|
"PREF sys (ACT a T) = a"

fun CONT where
"CONT sys (VAR X) =
(case sys X of ACT a T ⇒ T | PROC p ⇒ PROC (contOf p))"
|
"CONT sys (PROC p) = PROC (contOf p)"
|
"CONT sys (ACT a T) = T"

fun CH1 where
"CH1 sys (VAR X) =
(case sys X of CH T1 T2 ⇒ T1 |PROC p ⇒ PROC (ch1Of p))"
|
"CH1 sys (PROC p) = PROC (ch1Of p)"
|
"CH1 sys (CH T1 T2) = T1"

fun CH2 where
"CH2 sys (VAR X) =
(case sys X of CH T1 T2 ⇒ T2 |PROC p ⇒ PROC (ch2Of p))"
|
"CH2 sys (PROC p) = PROC (ch2Of p)"
|
"CH2 sys (CH T1 T2) = T2"

definition "guarded sys ≡ ∀ X Y. sys X ≠ VAR Y"

primcorec solution where
"isACT sys T ⟹ solution sys T = Action (PREF sys T) (solution sys (CONT sys T))"
| "_ ⟹ solution sys T = Choice (solution sys (CH1 sys T)) (solution sys (CH2 sys T))"

lemma isACT_VAR:
assumes g: "guarded sys"
shows "isACT sys (VAR X) ⟷ isACT sys (sys X)"
using g unfolding guarded_def by (cases "sys X") auto

lemma solution_VAR:
assumes g: "guarded sys"
shows "solution sys (VAR X) = solution sys (sys X)"
proof(cases "isACT sys (VAR X)")
case True
hence T: "isACT sys (sys X)" unfolding isACT_VAR[OF g] .
show ?thesis
unfolding solution.ctr(1)[OF T] using solution.ctr(1)[of sys "VAR X"] True g
unfolding guarded_def by (cases "sys X", auto)
next
case False note FFalse = False
hence TT: "¬ isACT sys (sys X)" unfolding isACT_VAR[OF g] .
show ?thesis
unfolding solution.ctr(2)[OF TT] using solution.ctr(2)[of sys "VAR X"] FFalse g
unfolding guarded_def by (cases "sys X", auto)
qed

lemma solution_PROC[simp]:
"solution sys (PROC p) = p"
proof-
{fix q assume "q = solution sys (PROC p)"
hence "p = q"
proof (coinduct rule: process_coind)
case (iss p p')
from isAction_isChoice[of p] show ?case
proof
assume p: "isAction p"
hence 0: "isACT sys (PROC p)" by simp
thus ?thesis using iss not_isAction_isChoice by auto
next
assume "isChoice p"
hence 0: "¬ isACT sys (PROC p)"
using not_isAction_isChoice by auto
thus ?thesis using iss isAction_isChoice by auto
qed
next
case (Action a a' p p')
hence 0: "isACT sys (PROC (Action a p))" by simp
show ?case using Action unfolding solution.ctr(1)[OF 0] by simp
next
case (Choice p q p' q')
hence 0: "¬ isACT sys (PROC (Choice p q))" using not_isAction_isChoice by auto
show ?case using Choice unfolding solution.ctr(2)[OF 0] by simp
qed
}
thus ?thesis by metis
qed

lemma solution_ACT[simp]:
"solution sys (ACT a T) = Action a (solution sys T)"
by (metis CONT.simps(3) PREF.simps(3) isACT.simps(3) solution.ctr(1))

lemma solution_CH[simp]:
"solution sys (CH T1 T2) = Choice (solution sys T1) (solution sys T2)"
by (metis CH1.simps(3) CH2.simps(3) isACT.simps(4) solution.ctr(2))

(* Example: *)

fun sys where
"sys 0 = CH (VAR (Suc 0)) (ACT ''b'' (VAR 0))"
|
"sys (Suc 0) = ACT ''a'' (VAR 0)"
| (* dummy guarded term for variables outside the system: *)
"sys X = ACT ''a'' (VAR 0)"

lemma guarded_sys:
"guarded sys"
unfolding guarded_def proof (intro allI)
fix X Y show "sys X ≠ VAR Y" by (cases X, simp, case_tac nat, auto)
qed

(* the actual processes: *)
definition "x ≡ solution sys (VAR 0)"
definition "ax ≡ solution sys (VAR (Suc 0))"

(* end product: *)
lemma x_ax:
"x = Choice ax (Action ''b'' x)"
"ax = Action ''a'' x"
unfolding x_def ax_def by (subst solution_VAR[OF guarded_sys], simp)+

(* Thanks to the inclusion of processes as process terms, one can
also consider parametrized systems of equations---here, x is a (semantic)
process parameter: *)

fun sys' where
"sys' 0 = CH (PROC x) (ACT ''b'' (VAR 0))"
|
"sys' (Suc 0) = CH (ACT ''a'' (VAR 0)) (PROC x)"
| (* dummy guarded term : *)
"sys' X = ACT ''a'' (VAR 0)"

lemma guarded_sys':
"guarded sys'"
unfolding guarded_def proof (intro allI)
fix X Y show "sys' X ≠ VAR Y" by (cases X, simp, case_tac nat, auto)
qed

(* the actual processes: *)
definition "y ≡ solution sys' (VAR 0)"
definition "ay ≡ solution sys' (VAR (Suc 0))"

(* end product: *)
lemma y_ay:
"y = Choice x (Action ''b'' y)"
"ay = Choice (Action ''a'' y) x"
unfolding y_def ay_def by (subst solution_VAR[OF guarded_sys'], simp)+

end
```