src/HOL/Predicate_Compile_Examples/Examples.thy
author haftmann
Sat Dec 24 15:53:10 2011 +0100 (2011-12-24)
changeset 45970 b6d0cff57d96
parent 42463 f270e3e18be5
child 51144 0ede9e2266a8
permissions -rw-r--r--
adjusted to set/pred distinction by means of type constructor `set`
bulwahn@39655
     1
theory Examples
wenzelm@41413
     2
imports Main "~~/src/HOL/Library/Predicate_Compile_Alternative_Defs"
bulwahn@39655
     3
begin
bulwahn@39655
     4
krauss@42208
     5
declare [[values_timeout = 480.0]]
krauss@42187
     6
bulwahn@39655
     7
section {* Formal Languages *}
bulwahn@39655
     8
bulwahn@39655
     9
subsection {* General Context Free Grammars *}
bulwahn@39655
    10
bulwahn@39655
    11
text {* a contribution by Aditi Barthwal *}
bulwahn@39655
    12
bulwahn@39655
    13
datatype ('nts,'ts) symbol = NTS 'nts
bulwahn@39655
    14
                            | TS 'ts
bulwahn@39655
    15
bulwahn@39655
    16
                            
bulwahn@39655
    17
datatype ('nts,'ts) rule = rule 'nts "('nts,'ts) symbol list"
bulwahn@39655
    18
wenzelm@42463
    19
type_synonym ('nts,'ts) grammar = "('nts,'ts) rule set * 'nts"
bulwahn@39655
    20
bulwahn@39655
    21
fun rules :: "('nts,'ts) grammar => ('nts,'ts) rule set"
bulwahn@39655
    22
where
bulwahn@39655
    23
  "rules (r, s) = r"
bulwahn@39655
    24
bulwahn@39655
    25
definition derives 
bulwahn@39655
    26
where
bulwahn@39655
    27
"derives g = { (lsl,rsl). \<exists>s1 s2 lhs rhs. 
bulwahn@39655
    28
                         (s1 @ [NTS lhs] @ s2 = lsl) \<and>
bulwahn@39655
    29
                         (s1 @ rhs @ s2) = rsl \<and>
bulwahn@39655
    30
                         (rule lhs rhs) \<in> fst g }"
bulwahn@39655
    31
haftmann@45970
    32
definition derivesp :: "(('nts, 'ts) rule => bool) * 'nts => ('nts, 'ts) symbol list => ('nts, 'ts) symbol list => bool"
haftmann@45970
    33
where
haftmann@45970
    34
  "derivesp g = (\<lambda> lhs rhs. (lhs, rhs) \<in> derives (Collect (fst g), snd g))"
haftmann@45970
    35
 
haftmann@45970
    36
lemma [code_pred_def]:
haftmann@45970
    37
  "derivesp g = (\<lambda> lsl rsl. \<exists>s1 s2 lhs rhs. 
haftmann@45970
    38
                         (s1 @ [NTS lhs] @ s2 = lsl) \<and>
haftmann@45970
    39
                         (s1 @ rhs @ s2) = rsl \<and>
haftmann@45970
    40
                         (fst g) (rule lhs rhs))"
haftmann@45970
    41
unfolding derivesp_def derives_def by auto
haftmann@45970
    42
bulwahn@39655
    43
abbreviation "example_grammar == 
bulwahn@39655
    44
({ rule ''S'' [NTS ''A'', NTS ''B''],
bulwahn@39655
    45
   rule ''S'' [TS ''a''],
bulwahn@39655
    46
  rule ''A'' [TS ''b'']}, ''S'')"
bulwahn@39655
    47
haftmann@45970
    48
definition "example_rules == 
haftmann@45970
    49
(%x. x = rule ''S'' [NTS ''A'', NTS ''B''] \<or>
haftmann@45970
    50
   x = rule ''S'' [TS ''a''] \<or>
haftmann@45970
    51
  x = rule ''A'' [TS ''b''])"
bulwahn@39655
    52
bulwahn@39655
    53
haftmann@45970
    54
code_pred [inductify, skip_proof] derivesp .
haftmann@45970
    55
haftmann@45970
    56
thm derivesp.equation
bulwahn@39655
    57
haftmann@45970
    58
definition "testp = (% rhs. derivesp (example_rules, ''S'') [NTS ''S''] rhs)"
bulwahn@39655
    59
haftmann@45970
    60
code_pred (modes: o \<Rightarrow> bool) [inductify] testp .
haftmann@45970
    61
thm testp.equation
bulwahn@39655
    62
haftmann@45970
    63
values "{rhs. testp rhs}"
haftmann@45970
    64
haftmann@45970
    65
declare rtranclp.intros(1)[code_pred_def] converse_rtranclp_into_rtranclp[code_pred_def]
bulwahn@39655
    66
haftmann@45970
    67
code_pred [inductify] rtranclp .
bulwahn@39655
    68
haftmann@45970
    69
definition "test2 = (\<lambda> rhs. rtranclp (derivesp (example_rules, ''S'')) [NTS ''S''] rhs)"
bulwahn@39655
    70
bulwahn@39655
    71
code_pred [inductify, skip_proof] test2 .
bulwahn@39655
    72
bulwahn@39655
    73
values "{rhs. test2 rhs}"
bulwahn@39655
    74
bulwahn@39655
    75
subsection {* Some concrete Context Free Grammars *}
bulwahn@39655
    76
bulwahn@39655
    77
datatype alphabet = a | b
bulwahn@39655
    78
bulwahn@39655
    79
inductive_set S\<^isub>1 and A\<^isub>1 and B\<^isub>1 where
bulwahn@39655
    80
  "[] \<in> S\<^isub>1"
bulwahn@39655
    81
| "w \<in> A\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
bulwahn@39655
    82
| "w \<in> B\<^isub>1 \<Longrightarrow> a # w \<in> S\<^isub>1"
bulwahn@39655
    83
| "w \<in> S\<^isub>1 \<Longrightarrow> a # w \<in> A\<^isub>1"
bulwahn@39655
    84
| "w \<in> S\<^isub>1 \<Longrightarrow> b # w \<in> S\<^isub>1"
bulwahn@39655
    85
| "\<lbrakk>v \<in> B\<^isub>1; v \<in> B\<^isub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>1"
bulwahn@39655
    86
bulwahn@39655
    87
code_pred [inductify] S\<^isub>1p .
bulwahn@39655
    88
code_pred [random_dseq inductify] S\<^isub>1p .
bulwahn@39655
    89
thm S\<^isub>1p.equation
bulwahn@39655
    90
thm S\<^isub>1p.random_dseq_equation
bulwahn@39655
    91
bulwahn@39655
    92
values [random_dseq 5, 5, 5] 5 "{x. S\<^isub>1p x}"
bulwahn@39655
    93
bulwahn@39655
    94
inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where
bulwahn@39655
    95
  "[] \<in> S\<^isub>2"
bulwahn@39655
    96
| "w \<in> A\<^isub>2 \<Longrightarrow> b # w \<in> S\<^isub>2"
bulwahn@39655
    97
| "w \<in> B\<^isub>2 \<Longrightarrow> a # w \<in> S\<^isub>2"
bulwahn@39655
    98
| "w \<in> S\<^isub>2 \<Longrightarrow> a # w \<in> A\<^isub>2"
bulwahn@39655
    99
| "w \<in> S\<^isub>2 \<Longrightarrow> b # w \<in> B\<^isub>2"
bulwahn@39655
   100
| "\<lbrakk>v \<in> B\<^isub>2; v \<in> B\<^isub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>2"
bulwahn@39655
   101
bulwahn@39655
   102
code_pred [random_dseq inductify] S\<^isub>2p .
bulwahn@39655
   103
thm S\<^isub>2p.random_dseq_equation
bulwahn@39655
   104
thm A\<^isub>2p.random_dseq_equation
bulwahn@39655
   105
thm B\<^isub>2p.random_dseq_equation
bulwahn@39655
   106
bulwahn@39655
   107
values [random_dseq 5, 5, 5] 10 "{x. S\<^isub>2p x}"
bulwahn@39655
   108
bulwahn@39655
   109
inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where
bulwahn@39655
   110
  "[] \<in> S\<^isub>3"
bulwahn@39655
   111
| "w \<in> A\<^isub>3 \<Longrightarrow> b # w \<in> S\<^isub>3"
bulwahn@39655
   112
| "w \<in> B\<^isub>3 \<Longrightarrow> a # w \<in> S\<^isub>3"
bulwahn@39655
   113
| "w \<in> S\<^isub>3 \<Longrightarrow> a # w \<in> A\<^isub>3"
bulwahn@39655
   114
| "w \<in> S\<^isub>3 \<Longrightarrow> b # w \<in> B\<^isub>3"
bulwahn@39655
   115
| "\<lbrakk>v \<in> B\<^isub>3; w \<in> B\<^isub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>3"
bulwahn@39655
   116
bulwahn@39655
   117
code_pred [inductify, skip_proof] S\<^isub>3p .
bulwahn@39655
   118
thm S\<^isub>3p.equation
bulwahn@39655
   119
bulwahn@39655
   120
values 10 "{x. S\<^isub>3p x}"
bulwahn@39655
   121
bulwahn@39655
   122
inductive_set S\<^isub>4 and A\<^isub>4 and B\<^isub>4 where
bulwahn@39655
   123
  "[] \<in> S\<^isub>4"
bulwahn@39655
   124
| "w \<in> A\<^isub>4 \<Longrightarrow> b # w \<in> S\<^isub>4"
bulwahn@39655
   125
| "w \<in> B\<^isub>4 \<Longrightarrow> a # w \<in> S\<^isub>4"
bulwahn@39655
   126
| "w \<in> S\<^isub>4 \<Longrightarrow> a # w \<in> A\<^isub>4"
bulwahn@39655
   127
| "\<lbrakk>v \<in> A\<^isub>4; w \<in> A\<^isub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^isub>4"
bulwahn@39655
   128
| "w \<in> S\<^isub>4 \<Longrightarrow> b # w \<in> B\<^isub>4"
bulwahn@39655
   129
| "\<lbrakk>v \<in> B\<^isub>4; w \<in> B\<^isub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^isub>4"
bulwahn@39655
   130
bulwahn@39655
   131
code_pred (expected_modes: o => bool, i => bool) S\<^isub>4p .
bulwahn@39655
   132
bulwahn@39655
   133
hide_const a b
bulwahn@39655
   134
bulwahn@39655
   135
section {* Semantics of programming languages *}
bulwahn@39655
   136
bulwahn@39655
   137
subsection {* IMP *}
bulwahn@39655
   138
wenzelm@42463
   139
type_synonym var = nat
wenzelm@42463
   140
type_synonym state = "int list"
bulwahn@39655
   141
bulwahn@39655
   142
datatype com =
bulwahn@39655
   143
  Skip |
bulwahn@39655
   144
  Ass var "state => int" |
bulwahn@39655
   145
  Seq com com |
bulwahn@39655
   146
  IF "state => bool" com com |
bulwahn@39655
   147
  While "state => bool" com
bulwahn@39655
   148
bulwahn@39655
   149
inductive exec :: "com => state => state => bool" where
bulwahn@39655
   150
"exec Skip s s" |
bulwahn@39655
   151
"exec (Ass x e) s (s[x := e(s)])" |
bulwahn@39655
   152
"exec c1 s1 s2 ==> exec c2 s2 s3 ==> exec (Seq c1 c2) s1 s3" |
bulwahn@39655
   153
"b s ==> exec c1 s t ==> exec (IF b c1 c2) s t" |
bulwahn@39655
   154
"~b s ==> exec c2 s t ==> exec (IF b c1 c2) s t" |
bulwahn@39655
   155
"~b s ==> exec (While b c) s s" |
bulwahn@39655
   156
"b s1 ==> exec c s1 s2 ==> exec (While b c) s2 s3 ==> exec (While b c) s1 s3"
bulwahn@39655
   157
bulwahn@39655
   158
code_pred exec .
bulwahn@39655
   159
bulwahn@39655
   160
values "{t. exec
bulwahn@39655
   161
 (While (%s. s!0 > 0) (Seq (Ass 0 (%s. s!0 - 1)) (Ass 1 (%s. s!1 + 1))))
bulwahn@39655
   162
 [3,5] t}"
bulwahn@39655
   163
bulwahn@39655
   164
subsection {* Lambda *}
bulwahn@39655
   165
bulwahn@39655
   166
datatype type =
bulwahn@39655
   167
    Atom nat
bulwahn@39655
   168
  | Fun type type    (infixr "\<Rightarrow>" 200)
bulwahn@39655
   169
bulwahn@39655
   170
datatype dB =
bulwahn@39655
   171
    Var nat
bulwahn@39655
   172
  | App dB dB (infixl "\<degree>" 200)
bulwahn@39655
   173
  | Abs type dB
bulwahn@39655
   174
bulwahn@39655
   175
primrec
bulwahn@39655
   176
  nth_el :: "'a list \<Rightarrow> nat \<Rightarrow> 'a option" ("_\<langle>_\<rangle>" [90, 0] 91)
bulwahn@39655
   177
where
bulwahn@39655
   178
  "[]\<langle>i\<rangle> = None"
bulwahn@39655
   179
| "(x # xs)\<langle>i\<rangle> = (case i of 0 \<Rightarrow> Some x | Suc j \<Rightarrow> xs \<langle>j\<rangle>)"
bulwahn@39655
   180
bulwahn@39655
   181
inductive nth_el' :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> bool"
bulwahn@39655
   182
where
bulwahn@39655
   183
  "nth_el' (x # xs) 0 x"
bulwahn@39655
   184
| "nth_el' xs i y \<Longrightarrow> nth_el' (x # xs) (Suc i) y"
bulwahn@39655
   185
bulwahn@39655
   186
inductive typing :: "type list \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"  ("_ \<turnstile> _ : _" [50, 50, 50] 50)
bulwahn@39655
   187
  where
bulwahn@39655
   188
    Var [intro!]: "nth_el' env x T \<Longrightarrow> env \<turnstile> Var x : T"
bulwahn@39655
   189
  | Abs [intro!]: "T # env \<turnstile> t : U \<Longrightarrow> env \<turnstile> Abs T t : (T \<Rightarrow> U)"
bulwahn@39655
   190
  | App [intro!]: "env \<turnstile> s : T \<Rightarrow> U \<Longrightarrow> env \<turnstile> t : T \<Longrightarrow> env \<turnstile> (s \<degree> t) : U"
bulwahn@39655
   191
bulwahn@39655
   192
primrec
bulwahn@39655
   193
  lift :: "[dB, nat] => dB"
bulwahn@39655
   194
where
bulwahn@39655
   195
    "lift (Var i) k = (if i < k then Var i else Var (i + 1))"
bulwahn@39655
   196
  | "lift (s \<degree> t) k = lift s k \<degree> lift t k"
bulwahn@39655
   197
  | "lift (Abs T s) k = Abs T (lift s (k + 1))"
bulwahn@39655
   198
bulwahn@39655
   199
primrec
bulwahn@39655
   200
  subst :: "[dB, dB, nat] => dB"  ("_[_'/_]" [300, 0, 0] 300)
bulwahn@39655
   201
where
bulwahn@39655
   202
    subst_Var: "(Var i)[s/k] =
bulwahn@39655
   203
      (if k < i then Var (i - 1) else if i = k then s else Var i)"
bulwahn@39655
   204
  | subst_App: "(t \<degree> u)[s/k] = t[s/k] \<degree> u[s/k]"
bulwahn@39655
   205
  | subst_Abs: "(Abs T t)[s/k] = Abs T (t[lift s 0 / k+1])"
bulwahn@39655
   206
bulwahn@39655
   207
inductive beta :: "[dB, dB] => bool"  (infixl "\<rightarrow>\<^sub>\<beta>" 50)
bulwahn@39655
   208
  where
bulwahn@39655
   209
    beta [simp, intro!]: "Abs T s \<degree> t \<rightarrow>\<^sub>\<beta> s[t/0]"
bulwahn@39655
   210
  | appL [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> s \<degree> u \<rightarrow>\<^sub>\<beta> t \<degree> u"
bulwahn@39655
   211
  | appR [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> u \<degree> s \<rightarrow>\<^sub>\<beta> u \<degree> t"
bulwahn@39655
   212
  | abs [simp, intro!]: "s \<rightarrow>\<^sub>\<beta> t ==> Abs T s \<rightarrow>\<^sub>\<beta> Abs T t"
bulwahn@39655
   213
bulwahn@39655
   214
code_pred (expected_modes: i => i => o => bool, i => i => i => bool) typing .
bulwahn@39655
   215
thm typing.equation
bulwahn@39655
   216
bulwahn@39655
   217
code_pred (modes: i => i => bool,  i => o => bool as reduce') beta .
bulwahn@39655
   218
thm beta.equation
bulwahn@39655
   219
bulwahn@39655
   220
values "{x. App (Abs (Atom 0) (Var 0)) (Var 1) \<rightarrow>\<^sub>\<beta> x}"
bulwahn@39655
   221
bulwahn@39655
   222
definition "reduce t = Predicate.the (reduce' t)"
bulwahn@39655
   223
bulwahn@39655
   224
value "reduce (App (Abs (Atom 0) (Var 0)) (Var 1))"
bulwahn@39655
   225
bulwahn@39655
   226
code_pred [dseq] typing .
bulwahn@39655
   227
code_pred [random_dseq] typing .
bulwahn@39655
   228
bulwahn@39655
   229
values [random_dseq 1,1,5] 10 "{(\<Gamma>, t, T). \<Gamma> \<turnstile> t : T}"
bulwahn@39655
   230
bulwahn@39655
   231
subsection {* A minimal example of yet another semantics *}
bulwahn@39655
   232
bulwahn@39655
   233
text {* thanks to Elke Salecker *}
bulwahn@39655
   234
wenzelm@42463
   235
type_synonym vname = nat
wenzelm@42463
   236
type_synonym vvalue = int
wenzelm@42463
   237
type_synonym var_assign = "vname \<Rightarrow> vvalue"  --"variable assignment"
bulwahn@39655
   238
bulwahn@39655
   239
datatype ir_expr = 
bulwahn@39655
   240
  IrConst vvalue
bulwahn@39655
   241
| ObjAddr vname
bulwahn@39655
   242
| Add ir_expr ir_expr
bulwahn@39655
   243
bulwahn@39655
   244
datatype val =
bulwahn@39655
   245
  IntVal  vvalue
bulwahn@39655
   246
bulwahn@39655
   247
record  configuration =
bulwahn@39655
   248
  Env :: var_assign
bulwahn@39655
   249
bulwahn@39655
   250
inductive eval_var ::
bulwahn@39655
   251
  "ir_expr \<Rightarrow> configuration \<Rightarrow> val \<Rightarrow> bool"
bulwahn@39655
   252
where
bulwahn@39655
   253
  irconst: "eval_var (IrConst i) conf (IntVal i)"
bulwahn@39655
   254
| objaddr: "\<lbrakk> Env conf n = i \<rbrakk> \<Longrightarrow> eval_var (ObjAddr n) conf (IntVal i)"
bulwahn@39655
   255
| plus: "\<lbrakk> eval_var l conf (IntVal vl); eval_var r conf (IntVal vr) \<rbrakk> \<Longrightarrow> eval_var (Add l r) conf (IntVal (vl+vr))"
bulwahn@39655
   256
bulwahn@39655
   257
bulwahn@39655
   258
code_pred eval_var .
bulwahn@39655
   259
thm eval_var.equation
bulwahn@39655
   260
bulwahn@39655
   261
values "{val. eval_var (Add (IrConst 1) (IrConst 2)) (| Env = (\<lambda>x. 0)|) val}"
bulwahn@39655
   262
bulwahn@39655
   263
subsection {* Another semantics *}
bulwahn@39655
   264
wenzelm@42463
   265
type_synonym name = nat --"For simplicity in examples"
wenzelm@42463
   266
type_synonym state' = "name \<Rightarrow> nat"
bulwahn@39655
   267
bulwahn@39655
   268
datatype aexp = N nat | V name | Plus aexp aexp
bulwahn@39655
   269
bulwahn@39655
   270
fun aval :: "aexp \<Rightarrow> state' \<Rightarrow> nat" where
bulwahn@39655
   271
"aval (N n) _ = n" |
bulwahn@39655
   272
"aval (V x) st = st x" |
bulwahn@39655
   273
"aval (Plus e\<^isub>1 e\<^isub>2) st = aval e\<^isub>1 st + aval e\<^isub>2 st"
bulwahn@39655
   274
bulwahn@39655
   275
datatype bexp = B bool | Not bexp | And bexp bexp | Less aexp aexp
bulwahn@39655
   276
bulwahn@39655
   277
primrec bval :: "bexp \<Rightarrow> state' \<Rightarrow> bool" where
bulwahn@39655
   278
"bval (B b) _ = b" |
bulwahn@39655
   279
"bval (Not b) st = (\<not> bval b st)" |
bulwahn@39655
   280
"bval (And b1 b2) st = (bval b1 st \<and> bval b2 st)" |
bulwahn@39655
   281
"bval (Less a\<^isub>1 a\<^isub>2) st = (aval a\<^isub>1 st < aval a\<^isub>2 st)"
bulwahn@39655
   282
bulwahn@39655
   283
datatype
bulwahn@39655
   284
  com' = SKIP 
bulwahn@39655
   285
      | Assign name aexp         ("_ ::= _" [1000, 61] 61)
bulwahn@39655
   286
      | Semi   com'  com'          ("_; _"  [60, 61] 60)
bulwahn@39655
   287
      | If     bexp com' com'     ("IF _ THEN _ ELSE _"  [0, 0, 61] 61)
bulwahn@39655
   288
      | While  bexp com'         ("WHILE _ DO _"  [0, 61] 61)
bulwahn@39655
   289
bulwahn@39655
   290
inductive
bulwahn@39655
   291
  big_step :: "com' * state' \<Rightarrow> state' \<Rightarrow> bool" (infix "\<Rightarrow>" 55)
bulwahn@39655
   292
where
bulwahn@39655
   293
  Skip:    "(SKIP,s) \<Rightarrow> s"
bulwahn@39655
   294
| Assign:  "(x ::= a,s) \<Rightarrow> s(x := aval a s)"
bulwahn@39655
   295
bulwahn@39655
   296
| Semi:    "(c\<^isub>1,s\<^isub>1) \<Rightarrow> s\<^isub>2  \<Longrightarrow>  (c\<^isub>2,s\<^isub>2) \<Rightarrow> s\<^isub>3  \<Longrightarrow> (c\<^isub>1;c\<^isub>2, s\<^isub>1) \<Rightarrow> s\<^isub>3"
bulwahn@39655
   297
bulwahn@39655
   298
| IfTrue:  "bval b s  \<Longrightarrow>  (c\<^isub>1,s) \<Rightarrow> t  \<Longrightarrow>  (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t"
bulwahn@39655
   299
| IfFalse: "\<not>bval b s  \<Longrightarrow>  (c\<^isub>2,s) \<Rightarrow> t  \<Longrightarrow>  (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s) \<Rightarrow> t"
bulwahn@39655
   300
bulwahn@39655
   301
| WhileFalse: "\<not>bval b s \<Longrightarrow> (WHILE b DO c,s) \<Rightarrow> s"
bulwahn@39655
   302
| WhileTrue:  "bval b s\<^isub>1  \<Longrightarrow>  (c,s\<^isub>1) \<Rightarrow> s\<^isub>2  \<Longrightarrow>  (WHILE b DO c, s\<^isub>2) \<Rightarrow> s\<^isub>3
bulwahn@39655
   303
               \<Longrightarrow> (WHILE b DO c, s\<^isub>1) \<Rightarrow> s\<^isub>3"
bulwahn@39655
   304
bulwahn@39655
   305
code_pred big_step .
bulwahn@39655
   306
bulwahn@39655
   307
thm big_step.equation
bulwahn@39655
   308
bulwahn@42094
   309
definition list :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a list" where
bulwahn@42094
   310
  "list s n = map s [0 ..< n]"
bulwahn@42094
   311
bulwahn@42094
   312
values [expected "{[42, (43 :: nat)]}"] "{list s 2|s. (SKIP, nth [42, 43]) \<Rightarrow> s}"
bulwahn@42094
   313
bulwahn@42094
   314
bulwahn@39655
   315
subsection {* CCS *}
bulwahn@39655
   316
bulwahn@39655
   317
text{* This example formalizes finite CCS processes without communication or
bulwahn@39655
   318
recursion. For simplicity, labels are natural numbers. *}
bulwahn@39655
   319
bulwahn@39655
   320
datatype proc = nil | pre nat proc | or proc proc | par proc proc
bulwahn@39655
   321
bulwahn@39655
   322
inductive step :: "proc \<Rightarrow> nat \<Rightarrow> proc \<Rightarrow> bool" where
bulwahn@39655
   323
"step (pre n p) n p" |
bulwahn@39655
   324
"step p1 a q \<Longrightarrow> step (or p1 p2) a q" |
bulwahn@39655
   325
"step p2 a q \<Longrightarrow> step (or p1 p2) a q" |
bulwahn@39655
   326
"step p1 a q \<Longrightarrow> step (par p1 p2) a (par q p2)" |
bulwahn@39655
   327
"step p2 a q \<Longrightarrow> step (par p1 p2) a (par p1 q)"
bulwahn@39655
   328
bulwahn@39655
   329
code_pred step .
bulwahn@39655
   330
bulwahn@39655
   331
inductive steps where
bulwahn@39655
   332
"steps p [] p" |
bulwahn@39655
   333
"step p a q \<Longrightarrow> steps q as r \<Longrightarrow> steps p (a#as) r"
bulwahn@39655
   334
bulwahn@39655
   335
code_pred steps .
bulwahn@39655
   336
bulwahn@39655
   337
values 3 
bulwahn@39655
   338
 "{as . steps (par (or (pre 0 nil) (pre 1 nil)) (pre 2 nil)) as (par nil nil)}"
bulwahn@39655
   339
bulwahn@39655
   340
values 5
bulwahn@39655
   341
 "{as . steps (par (or (pre 0 nil) (pre 1 nil)) (pre 2 nil)) as (par nil nil)}"
bulwahn@39655
   342
bulwahn@39655
   343
values 3 "{(a,q). step (par nil nil) a q}"
bulwahn@39655
   344
bulwahn@39655
   345
bulwahn@39655
   346
end
bulwahn@39655
   347