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