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