src/HOL/IMP/C_like.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 45200 1f1897ac7877
child 47818 151d137f1095
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
     1 theory C_like imports Main begin
     2 
     3 subsection "A C-like Language"
     4 
     5 type_synonym state = "nat \<Rightarrow> nat"
     6 
     7 datatype aexp = N nat | Deref aexp ("!") | Plus aexp aexp
     8 
     9 fun aval :: "aexp \<Rightarrow> state \<Rightarrow> nat" where
    10 "aval (N n) s = n" |
    11 "aval (!a) s = s(aval a s)" |
    12 "aval (Plus a\<^isub>1 a\<^isub>2) s = aval a\<^isub>1 s + aval a\<^isub>2 s"
    13 
    14 datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
    15 
    16 primrec bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where
    17 "bval (Bc v) _ = v" |
    18 "bval (Not b) s = (\<not> bval b s)" |
    19 "bval (And b\<^isub>1 b\<^isub>2) s = (if bval b\<^isub>1 s then bval b\<^isub>2 s else False)" |
    20 "bval (Less a\<^isub>1 a\<^isub>2) s = (aval a\<^isub>1 s < aval a\<^isub>2 s)"
    21 
    22 
    23 datatype
    24   com = SKIP 
    25       | Assign aexp aexp         ("_ ::= _" [61, 61] 61)
    26       | New    aexp aexp
    27       | Semi   com  com          ("_;/ _"  [60, 61] 60)
    28       | If     bexp com com     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61)
    29       | While  bexp com         ("(WHILE _/ DO _)"  [0, 61] 61)
    30 
    31 inductive
    32   big_step :: "com \<times> state \<times> nat \<Rightarrow> state \<times> nat \<Rightarrow> bool"  (infix "\<Rightarrow>" 55)
    33 where
    34 Skip:    "(SKIP,sn) \<Rightarrow> sn" |
    35 Assign:  "(lhs ::= a,s,n) \<Rightarrow> (s(aval lhs s := aval a s),n)" |
    36 New:     "(New lhs a,s,n) \<Rightarrow> (s(aval lhs s := n), n+aval a s)"  |
    37 Semi:    "\<lbrakk> (c\<^isub>1,sn\<^isub>1) \<Rightarrow> sn\<^isub>2;  (c\<^isub>2,sn\<^isub>2) \<Rightarrow> sn\<^isub>3 \<rbrakk> \<Longrightarrow>
    38           (c\<^isub>1;c\<^isub>2, sn\<^isub>1) \<Rightarrow> sn\<^isub>3" |
    39 
    40 IfTrue:  "\<lbrakk> bval b s;  (c\<^isub>1,s,n) \<Rightarrow> tn \<rbrakk> \<Longrightarrow>
    41          (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s,n) \<Rightarrow> tn" |
    42 IfFalse: "\<lbrakk> \<not>bval b s;  (c\<^isub>2,s,n) \<Rightarrow> tn \<rbrakk> \<Longrightarrow>
    43          (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s,n) \<Rightarrow> tn" |
    44 
    45 WhileFalse: "\<not>bval b s \<Longrightarrow> (WHILE b DO c,s,n) \<Rightarrow> (s,n)" |
    46 WhileTrue:
    47   "\<lbrakk> bval b s\<^isub>1;  (c,s\<^isub>1,n) \<Rightarrow> sn\<^isub>2;  (WHILE b DO c, sn\<^isub>2) \<Rightarrow> sn\<^isub>3 \<rbrakk> \<Longrightarrow>
    48    (WHILE b DO c, s\<^isub>1,n) \<Rightarrow> sn\<^isub>3"
    49 
    50 code_pred big_step .
    51 
    52 declare [[values_timeout = 3600]]
    53 
    54 text{* Examples: *}
    55 
    56 definition
    57 "array_sum =
    58  WHILE Less (!(N 0)) (Plus (!(N 1)) (N 1))
    59  DO ( N 2 ::= Plus (!(N 2)) (!(!(N 0)));
    60       N 0 ::= Plus (!(N 0)) (N 1) )"
    61 
    62 text {* To show the first n variables in a @{typ "nat \<Rightarrow> nat"} state: *}
    63 definition 
    64   "list t n = map t [0 ..< n]"
    65 
    66 values "{list t n |t n. (array_sum, nth[3,4,0,3,7],5) \<Rightarrow> (t,n)}"
    67 
    68 definition
    69 "linked_list_sum =
    70  WHILE Less (N 0) (!(N 0))
    71  DO ( N 1 ::= Plus(!(N 1)) (!(!(N 0)));
    72       N 0 ::= !(Plus(!(N 0))(N 1)) )"
    73 
    74 values "{list t n |t n. (linked_list_sum, nth[4,0,3,0,7,2],6) \<Rightarrow> (t,n)}"
    75 
    76 definition
    77 "array_init =
    78  New (N 0) (!(N 1)); N 2 ::= !(N 0);
    79  WHILE Less (!(N 2)) (Plus (!(N 0)) (!(N 1)))
    80  DO ( !(N 2) ::= !(N 2);
    81       N 2 ::= Plus (!(N 2)) (N 1) )"
    82 
    83 values "{list t n |t n. (array_init, nth[5,2,7],3) \<Rightarrow> (t,n)}"
    84 
    85 definition
    86 "linked_list_init =
    87  WHILE Less (!(N 1)) (!(N 0))
    88  DO ( New (N 3) (N 2);
    89       N 1 ::=  Plus (!(N 1)) (N 1);
    90       !(N 3) ::= !(N 1);
    91       Plus (!(N 3)) (N 1) ::= !(N 2);
    92       N 2 ::= !(N 3) )"
    93 
    94 values "{list t n |t n. (linked_list_init, nth[2,0,0,0],4) \<Rightarrow> (t,n)}"
    95 
    96 end