src/HOL/Predicate_Compile_Examples/Examples.thy
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 66453 cc19f7ca2ed6
child 67443 3abf6a722518
permissions -rw-r--r--
more robust sorted_entries;
     1 theory Examples
     2 imports Main "HOL-Library.Predicate_Compile_Alternative_Defs"
     3 begin
     4 
     5 declare [[values_timeout = 480.0]]
     6 
     7 section \<open>Formal Languages\<close>
     8 
     9 subsection \<open>General Context Free Grammars\<close>
    10 
    11 text \<open>a contribution by Aditi Barthwal\<close>
    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 \<open>Some concrete Context Free Grammars\<close>
    77 
    78 datatype alphabet = a | b
    79 
    80 inductive_set S\<^sub>1 and A\<^sub>1 and B\<^sub>1 where
    81   "[] \<in> S\<^sub>1"
    82 | "w \<in> A\<^sub>1 \<Longrightarrow> b # w \<in> S\<^sub>1"
    83 | "w \<in> B\<^sub>1 \<Longrightarrow> a # w \<in> S\<^sub>1"
    84 | "w \<in> S\<^sub>1 \<Longrightarrow> a # w \<in> A\<^sub>1"
    85 | "w \<in> S\<^sub>1 \<Longrightarrow> b # w \<in> S\<^sub>1"
    86 | "\<lbrakk>v \<in> B\<^sub>1; v \<in> B\<^sub>1\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>1"
    87 
    88 code_pred [inductify] S\<^sub>1p .
    89 code_pred [random_dseq inductify] S\<^sub>1p .
    90 thm S\<^sub>1p.equation
    91 thm S\<^sub>1p.random_dseq_equation
    92 
    93 values [random_dseq 5, 5, 5] 5 "{x. S\<^sub>1p x}"
    94 
    95 inductive_set S\<^sub>2 and A\<^sub>2 and B\<^sub>2 where
    96   "[] \<in> S\<^sub>2"
    97 | "w \<in> A\<^sub>2 \<Longrightarrow> b # w \<in> S\<^sub>2"
    98 | "w \<in> B\<^sub>2 \<Longrightarrow> a # w \<in> S\<^sub>2"
    99 | "w \<in> S\<^sub>2 \<Longrightarrow> a # w \<in> A\<^sub>2"
   100 | "w \<in> S\<^sub>2 \<Longrightarrow> b # w \<in> B\<^sub>2"
   101 | "\<lbrakk>v \<in> B\<^sub>2; v \<in> B\<^sub>2\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>2"
   102 
   103 code_pred [random_dseq inductify] S\<^sub>2p .
   104 thm S\<^sub>2p.random_dseq_equation
   105 thm A\<^sub>2p.random_dseq_equation
   106 thm B\<^sub>2p.random_dseq_equation
   107 
   108 values [random_dseq 5, 5, 5] 10 "{x. S\<^sub>2p x}"
   109 
   110 inductive_set S\<^sub>3 and A\<^sub>3 and B\<^sub>3 where
   111   "[] \<in> S\<^sub>3"
   112 | "w \<in> A\<^sub>3 \<Longrightarrow> b # w \<in> S\<^sub>3"
   113 | "w \<in> B\<^sub>3 \<Longrightarrow> a # w \<in> S\<^sub>3"
   114 | "w \<in> S\<^sub>3 \<Longrightarrow> a # w \<in> A\<^sub>3"
   115 | "w \<in> S\<^sub>3 \<Longrightarrow> b # w \<in> B\<^sub>3"
   116 | "\<lbrakk>v \<in> B\<^sub>3; w \<in> B\<^sub>3\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>3"
   117 
   118 code_pred [inductify, skip_proof] S\<^sub>3p .
   119 thm S\<^sub>3p.equation
   120 
   121 values 10 "{x. S\<^sub>3p x}"
   122 
   123 inductive_set S\<^sub>4 and A\<^sub>4 and B\<^sub>4 where
   124   "[] \<in> S\<^sub>4"
   125 | "w \<in> A\<^sub>4 \<Longrightarrow> b # w \<in> S\<^sub>4"
   126 | "w \<in> B\<^sub>4 \<Longrightarrow> a # w \<in> S\<^sub>4"
   127 | "w \<in> S\<^sub>4 \<Longrightarrow> a # w \<in> A\<^sub>4"
   128 | "\<lbrakk>v \<in> A\<^sub>4; w \<in> A\<^sub>4\<rbrakk> \<Longrightarrow> b # v @ w \<in> A\<^sub>4"
   129 | "w \<in> S\<^sub>4 \<Longrightarrow> b # w \<in> B\<^sub>4"
   130 | "\<lbrakk>v \<in> B\<^sub>4; w \<in> B\<^sub>4\<rbrakk> \<Longrightarrow> a # v @ w \<in> B\<^sub>4"
   131 
   132 code_pred (expected_modes: o => bool, i => bool) S\<^sub>4p .
   133 
   134 hide_const a b
   135 
   136 section \<open>Semantics of programming languages\<close>
   137 
   138 subsection \<open>IMP\<close>
   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 \<open>Lambda\<close>
   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 \<open>A minimal example of yet another semantics\<close>
   233 
   234 text \<open>thanks to Elke Salecker\<close>
   235 
   236 type_synonym vname = nat
   237 type_synonym vvalue = int
   238 type_synonym var_assign = "vname \<Rightarrow> vvalue"  \<comment>"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 \<open>Another semantics\<close>
   266 
   267 type_synonym name = nat \<comment>"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\<^sub>1 e\<^sub>2) st = aval e\<^sub>1 st + aval e\<^sub>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\<^sub>1 a\<^sub>2) st = (aval a\<^sub>1 st < aval a\<^sub>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\<^sub>1,s\<^sub>1) \<Rightarrow> s\<^sub>2  \<Longrightarrow>  (c\<^sub>2,s\<^sub>2) \<Rightarrow> s\<^sub>3  \<Longrightarrow> (c\<^sub>1;c\<^sub>2, s\<^sub>1) \<Rightarrow> s\<^sub>3"
   299 
   300 | IfTrue:  "bval b s  \<Longrightarrow>  (c\<^sub>1,s) \<Rightarrow> t  \<Longrightarrow>  (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \<Rightarrow> t"
   301 | IfFalse: "\<not>bval b s  \<Longrightarrow>  (c\<^sub>2,s) \<Rightarrow> t  \<Longrightarrow>  (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s) \<Rightarrow> t"
   302 
   303 | WhileFalse: "\<not>bval b s \<Longrightarrow> (WHILE b DO c,s) \<Rightarrow> s"
   304 | WhileTrue:  "bval b s\<^sub>1  \<Longrightarrow>  (c,s\<^sub>1) \<Rightarrow> s\<^sub>2  \<Longrightarrow>  (WHILE b DO c, s\<^sub>2) \<Rightarrow> s\<^sub>3
   305                \<Longrightarrow> (WHILE b DO c, s\<^sub>1) \<Rightarrow> s\<^sub>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 "{[42::nat, 43]}"] "{list s 2|s. (SKIP, nth [42, 43]) \<Rightarrow> s}"
   315 
   316 
   317 subsection \<open>CCS\<close>
   318 
   319 text\<open>This example formalizes finite CCS processes without communication or
   320 recursion. For simplicity, labels are natural numbers.\<close>
   321 
   322 datatype proc = nil | pre nat proc | or proc proc | par proc proc
   323 
   324 inductive step :: "proc \<Rightarrow> nat \<Rightarrow> proc \<Rightarrow> bool" where
   325 "step (pre n p) n p" |
   326 "step p1 a q \<Longrightarrow> step (or p1 p2) a q" |
   327 "step p2 a q \<Longrightarrow> step (or p1 p2) a q" |
   328 "step p1 a q \<Longrightarrow> step (par p1 p2) a (par q p2)" |
   329 "step p2 a q \<Longrightarrow> step (par p1 p2) a (par p1 q)"
   330 
   331 code_pred step .
   332 
   333 inductive steps where
   334 "steps p [] p" |
   335 "step p a q \<Longrightarrow> steps q as r \<Longrightarrow> steps p (a#as) r"
   336 
   337 code_pred steps .
   338 
   339 values 3 
   340  "{as . steps (par (or (pre 0 nil) (pre 1 nil)) (pre 2 nil)) as (par nil nil)}"
   341 
   342 values 5
   343  "{as . steps (par (or (pre 0 nil) (pre 1 nil)) (pre 2 nil)) as (par nil nil)}"
   344 
   345 values 3 "{(a,q). step (par nil nil) a q}"
   346 
   347 
   348 end
   349