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