src/HOL/Datatype_Examples/Process.thy
author haftmann
Fri Oct 10 19:55:32 2014 +0200 (2014-10-10)
changeset 58646 cd63a4b12a33
parent 58607 1f90ea1b4010
child 58889 5b7a9633cfa8
permissions -rw-r--r--
specialized specification: avoid trivial instances
     1 (*  Title:      HOL/Datatype_Examples/Process.thy
     2     Author:     Andrei Popescu, TU Muenchen
     3     Copyright   2012
     4 
     5 Processes.
     6 *)
     7 
     8 header {* Processes *}
     9 
    10 theory Process
    11 imports "~~/src/HOL/Library/Stream"
    12 begin
    13 
    14 codatatype 'a process =
    15   isAction: Action (prefOf: 'a) (contOf: "'a process") |
    16   isChoice: Choice (ch1Of: "'a process") (ch2Of: "'a process")
    17 
    18 (* Read: prefix of, continuation of, choice 1 of, choice 2 of *)
    19 
    20 section {* Customization *}
    21 
    22 subsection {* Basic properties *}
    23 
    24 declare
    25   rel_pre_process_def[simp]
    26   rel_sum_def[simp]
    27   rel_prod_def[simp]
    28 
    29 (* Constructors versus discriminators *)
    30 theorem isAction_isChoice:
    31 "isAction p \<or> isChoice p"
    32 by (rule process.exhaust_disc) auto
    33 
    34 theorem not_isAction_isChoice: "\<not> (isAction p \<and> isChoice p)"
    35 by (cases rule: process.exhaust[of p]) auto
    36 
    37 
    38 subsection{* Coinduction *}
    39 
    40 theorem process_coind[elim, consumes 1, case_names iss Action Choice, induct pred: "HOL.eq"]:
    41   assumes phi: "\<phi> p p'" and
    42   iss: "\<And>p p'. \<phi> p p' \<Longrightarrow> (isAction p \<longleftrightarrow> isAction p') \<and> (isChoice p \<longleftrightarrow> isChoice p')" and
    43   Act: "\<And> a a' p p'. \<phi> (Action a p) (Action a' p') \<Longrightarrow> a = a' \<and> \<phi> p p'" and
    44   Ch: "\<And> p q p' q'. \<phi> (Choice p q) (Choice p' q') \<Longrightarrow> \<phi> p p' \<and> \<phi> q q'"
    45   shows "p = p'"
    46   using assms
    47   by (coinduct rule: process.coinduct) (metis process.collapse(1,2) process.disc(3))
    48 
    49 (* Stronger coinduction, up to equality: *)
    50 theorem process_strong_coind[elim, consumes 1, case_names iss Action Choice]:
    51   assumes phi: "\<phi> p p'" and
    52   iss: "\<And>p p'. \<phi> p p' \<Longrightarrow> (isAction p \<longleftrightarrow> isAction p') \<and> (isChoice p \<longleftrightarrow> isChoice p')" and
    53   Act: "\<And> a a' p p'. \<phi> (Action a p) (Action a' p') \<Longrightarrow> a = a' \<and> (\<phi> p p' \<or> p = p')" and
    54   Ch: "\<And> p q p' q'. \<phi> (Choice p q) (Choice p' q') \<Longrightarrow> (\<phi> p p' \<or> p = p') \<and> (\<phi> q q' \<or> q = q')"
    55   shows "p = p'"
    56   using assms
    57   by (coinduct rule: process.coinduct_strong) (metis process.collapse(1,2) process.disc(3))
    58 
    59 
    60 subsection {* Coiteration (unfold) *}
    61 
    62 
    63 section{* Coinductive definition of the notion of trace *}
    64 coinductive trace where
    65 "trace p as \<Longrightarrow> trace (Action a p) (a ## as)"
    66 |
    67 "trace p as \<or> trace q as \<Longrightarrow> trace (Choice p q) as"
    68 
    69 
    70 section{* Examples of corecursive definitions: *}
    71 
    72 subsection{* Single-guard fixpoint definition *}
    73 
    74 primcorec BX where
    75   "isAction BX"
    76 | "prefOf BX = ''a''"
    77 | "contOf BX = BX"
    78 
    79 
    80 subsection{* Multi-guard fixpoint definitions, simulated with auxiliary arguments *}
    81 
    82 datatype x_y_ax = x | y | ax
    83 
    84 primcorec F :: "x_y_ax \<Rightarrow> char list process" where
    85   "xyax = x \<Longrightarrow> isChoice (F xyax)"
    86 | "ch1Of (F xyax) = F ax"
    87 | "ch2Of (F xyax) = F y"
    88 | "prefOf (F xyax) = (if xyax = y then ''b'' else ''a'')"
    89 | "contOf (F xyax) = F x"
    90 
    91 definition "X = F x"  definition "Y = F y"  definition "AX = F ax"
    92 
    93 lemma X_Y_AX: "X = Choice AX Y"  "Y = Action ''b'' X"  "AX = Action ''a'' X"
    94 unfolding X_def Y_def AX_def by (subst F.code, simp)+
    95 
    96 (* end product: *)
    97 lemma X_AX:
    98 "X = Choice AX (Action ''b'' X)"
    99 "AX = Action ''a'' X"
   100 using X_Y_AX by simp_all
   101 
   102 
   103 
   104 section{* Case study: Multi-guard fixpoint definitions, without auxiliary arguments *}
   105 
   106 hide_const x y ax X Y AX
   107 
   108 (* Process terms *)
   109 datatype ('a,'pvar) process_term =
   110  VAR 'pvar |
   111  PROC "'a process" |
   112  ACT 'a "('a,'pvar) process_term" | CH "('a,'pvar) process_term" "('a,'pvar) process_term"
   113 
   114 (* below, sys represents a system of equations *)
   115 fun isACT where
   116 "isACT sys (VAR X) =
   117  (case sys X of ACT a T \<Rightarrow> True |PROC p \<Rightarrow> isAction p |_ \<Rightarrow> False)"
   118 |
   119 "isACT sys (PROC p) = isAction p"
   120 |
   121 "isACT sys (ACT a T) = True"
   122 |
   123 "isACT sys (CH T1 T2) = False"
   124 
   125 fun PREF where
   126 "PREF sys (VAR X) =
   127  (case sys X of ACT a T \<Rightarrow> a | PROC p \<Rightarrow> prefOf p)"
   128 |
   129 "PREF sys (PROC p) = prefOf p"
   130 |
   131 "PREF sys (ACT a T) = a"
   132 
   133 fun CONT where
   134 "CONT sys (VAR X) =
   135  (case sys X of ACT a T \<Rightarrow> T | PROC p \<Rightarrow> PROC (contOf p))"
   136 |
   137 "CONT sys (PROC p) = PROC (contOf p)"
   138 |
   139 "CONT sys (ACT a T) = T"
   140 
   141 fun CH1 where
   142 "CH1 sys (VAR X) =
   143  (case sys X of CH T1 T2 \<Rightarrow> T1 |PROC p \<Rightarrow> PROC (ch1Of p))"
   144 |
   145 "CH1 sys (PROC p) = PROC (ch1Of p)"
   146 |
   147 "CH1 sys (CH T1 T2) = T1"
   148 
   149 fun CH2 where
   150 "CH2 sys (VAR X) =
   151  (case sys X of CH T1 T2 \<Rightarrow> T2 |PROC p \<Rightarrow> PROC (ch2Of p))"
   152 |
   153 "CH2 sys (PROC p) = PROC (ch2Of p)"
   154 |
   155 "CH2 sys (CH T1 T2) = T2"
   156 
   157 definition "guarded sys \<equiv> \<forall> X Y. sys X \<noteq> VAR Y"
   158 
   159 primcorec solution where
   160   "isACT sys T \<Longrightarrow> solution sys T = Action (PREF sys T) (solution sys (CONT sys T))"
   161 | "_ \<Longrightarrow> solution sys T = Choice (solution sys (CH1 sys T)) (solution sys (CH2 sys T))"
   162 
   163 lemma isACT_VAR:
   164 assumes g: "guarded sys"
   165 shows "isACT sys (VAR X) \<longleftrightarrow> isACT sys (sys X)"
   166 using g unfolding guarded_def by (cases "sys X") auto
   167 
   168 lemma solution_VAR:
   169 assumes g: "guarded sys"
   170 shows "solution sys (VAR X) = solution sys (sys X)"
   171 proof(cases "isACT sys (VAR X)")
   172   case True
   173   hence T: "isACT sys (sys X)" unfolding isACT_VAR[OF g] .
   174   show ?thesis
   175   unfolding solution.ctr(1)[OF T] using solution.ctr(1)[of sys "VAR X"] True g
   176   unfolding guarded_def by (cases "sys X", auto)
   177 next
   178   case False note FFalse = False
   179   hence TT: "\<not> isACT sys (sys X)" unfolding isACT_VAR[OF g] .
   180   show ?thesis
   181   unfolding solution.ctr(2)[OF TT] using solution.ctr(2)[of sys "VAR X"] FFalse g
   182   unfolding guarded_def by (cases "sys X", auto)
   183 qed
   184 
   185 lemma solution_PROC[simp]:
   186 "solution sys (PROC p) = p"
   187 proof-
   188   {fix q assume "q = solution sys (PROC p)"
   189    hence "p = q"
   190    proof (coinduct rule: process_coind)
   191      case (iss p p')
   192      from isAction_isChoice[of p] show ?case
   193      proof
   194        assume p: "isAction p"
   195        hence 0: "isACT sys (PROC p)" by simp
   196        thus ?thesis using iss not_isAction_isChoice by auto
   197      next
   198        assume "isChoice p"
   199        hence 0: "\<not> isACT sys (PROC p)"
   200        using not_isAction_isChoice by auto
   201        thus ?thesis using iss isAction_isChoice by auto
   202      qed
   203    next
   204      case (Action a a' p p')
   205      hence 0: "isACT sys (PROC (Action a p))" by simp
   206      show ?case using Action unfolding solution.ctr(1)[OF 0] by simp
   207    next
   208      case (Choice p q p' q')
   209      hence 0: "\<not> isACT sys (PROC (Choice p q))" using not_isAction_isChoice by auto
   210      show ?case using Choice unfolding solution.ctr(2)[OF 0] by simp
   211    qed
   212   }
   213   thus ?thesis by metis
   214 qed
   215 
   216 lemma solution_ACT[simp]:
   217 "solution sys (ACT a T) = Action a (solution sys T)"
   218 by (metis CONT.simps(3) PREF.simps(3) isACT.simps(3) solution.ctr(1))
   219 
   220 lemma solution_CH[simp]:
   221 "solution sys (CH T1 T2) = Choice (solution sys T1) (solution sys T2)"
   222 by (metis CH1.simps(3) CH2.simps(3) isACT.simps(4) solution.ctr(2))
   223 
   224 
   225 (* Example: *)
   226 
   227 fun sys where
   228 "sys 0 = CH (VAR (Suc 0)) (ACT ''b'' (VAR 0))"
   229 |
   230 "sys (Suc 0) = ACT ''a'' (VAR 0)"
   231 | (* dummy guarded term for variables outside the system: *)
   232 "sys X = ACT ''a'' (VAR 0)"
   233 
   234 lemma guarded_sys:
   235 "guarded sys"
   236 unfolding guarded_def proof (intro allI)
   237   fix X Y show "sys X \<noteq> VAR Y" by (cases X, simp, case_tac nat, auto)
   238 qed
   239 
   240 (* the actual processes: *)
   241 definition "x \<equiv> solution sys (VAR 0)"
   242 definition "ax \<equiv> solution sys (VAR (Suc 0))"
   243 
   244 (* end product: *)
   245 lemma x_ax:
   246 "x = Choice ax (Action ''b'' x)"
   247 "ax = Action ''a'' x"
   248 unfolding x_def ax_def by (subst solution_VAR[OF guarded_sys], simp)+
   249 
   250 
   251 (* Thanks to the inclusion of processes as process terms, one can
   252 also consider parametrized systems of equations---here, x is a (semantic)
   253 process parameter: *)
   254 
   255 fun sys' where
   256 "sys' 0 = CH (PROC x) (ACT ''b'' (VAR 0))"
   257 |
   258 "sys' (Suc 0) = CH (ACT ''a'' (VAR 0)) (PROC x)"
   259 | (* dummy guarded term : *)
   260 "sys' X = ACT ''a'' (VAR 0)"
   261 
   262 lemma guarded_sys':
   263 "guarded sys'"
   264 unfolding guarded_def proof (intro allI)
   265   fix X Y show "sys' X \<noteq> VAR Y" by (cases X, simp, case_tac nat, auto)
   266 qed
   267 
   268 (* the actual processes: *)
   269 definition "y \<equiv> solution sys' (VAR 0)"
   270 definition "ay \<equiv> solution sys' (VAR (Suc 0))"
   271 
   272 (* end product: *)
   273 lemma y_ay:
   274 "y = Choice x (Action ''b'' y)"
   275 "ay = Choice (Action ''a'' y) x"
   276 unfolding y_def ay_def by (subst solution_VAR[OF guarded_sys'], simp)+
   277 
   278 end