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