diff -r 0ccba1b6d00b -r a09ec6daaa19 src/HOL/Datatype_Examples/Process.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Datatype_Examples/Process.thy Thu Sep 11 19:26:59 2014 +0200 @@ -0,0 +1,278 @@ +(* Title: HOL/Datatype_Examples/Process.thy + Author: Andrei Popescu, TU Muenchen + Copyright 2012 + +Processes. +*) + +header {* Processes *} + +theory Process +imports 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 *) + +section {* Customization *} + +subsection {* Basic properties *} + +declare + rel_pre_process_def[simp] + rel_sum_def[simp] + rel_prod_def[simp] + +(* 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_new 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_new ('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