# Theory C_like

theory C_like
imports Main
```theory C_like imports Main begin

subsection "A C-like Language"

type_synonym state = "nat ⇒ nat"

datatype aexp = N nat | Deref aexp ("!") | Plus aexp aexp

fun aval :: "aexp ⇒ state ⇒ nat" where
"aval (N n) s = n" |
"aval (!a) s = s(aval a s)" |
"aval (Plus a⇩1 a⇩2) s = aval a⇩1 s + aval a⇩2 s"

datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp

primrec bval :: "bexp ⇒ state ⇒ bool" where
"bval (Bc v) _ = v" |
"bval (Not b) s = (¬ bval b s)" |
"bval (And b⇩1 b⇩2) s = (if bval b⇩1 s then bval b⇩2 s else False)" |
"bval (Less a⇩1 a⇩2) s = (aval a⇩1 s < aval a⇩2 s)"

datatype
com = SKIP
| Assign aexp aexp         ("_ ::= _" [61, 61] 61)
| New    aexp aexp
| Seq    com  com          ("_;/ _"  [60, 61] 60)
| If     bexp com com     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61)
| While  bexp com         ("(WHILE _/ DO _)"  [0, 61] 61)

inductive
big_step :: "com × state × nat ⇒ state × nat ⇒ bool"  (infix "⇒" 55)
where
Skip:    "(SKIP,sn) ⇒ sn" |
Assign:  "(lhs ::= a,s,n) ⇒ (s(aval lhs s := aval a s),n)" |
New:     "(New lhs a,s,n) ⇒ (s(aval lhs s := n), n+aval a s)"  |
Seq:    "⟦ (c⇩1,sn⇩1) ⇒ sn⇩2;  (c⇩2,sn⇩2) ⇒ sn⇩3 ⟧ ⟹
(c⇩1;c⇩2, sn⇩1) ⇒ sn⇩3" |

IfTrue:  "⟦ bval b s;  (c⇩1,s,n) ⇒ tn ⟧ ⟹
(IF b THEN c⇩1 ELSE c⇩2, s,n) ⇒ tn" |
IfFalse: "⟦ ¬bval b s;  (c⇩2,s,n) ⇒ tn ⟧ ⟹
(IF b THEN c⇩1 ELSE c⇩2, s,n) ⇒ tn" |

WhileFalse: "¬bval b s ⟹ (WHILE b DO c,s,n) ⇒ (s,n)" |
WhileTrue:
"⟦ bval b s⇩1;  (c,s⇩1,n) ⇒ sn⇩2;  (WHILE b DO c, sn⇩2) ⇒ sn⇩3 ⟧ ⟹
(WHILE b DO c, s⇩1,n) ⇒ sn⇩3"

code_pred big_step .

declare [[values_timeout = 3600]]

text‹Examples:›

definition
"array_sum =
WHILE Less (!(N 0)) (Plus (!(N 1)) (N 1))
DO ( N 2 ::= Plus (!(N 2)) (!(!(N 0)));
N 0 ::= Plus (!(N 0)) (N 1) )"

text ‹To show the first n variables in a @{typ "nat ⇒ nat"} state:›
definition
"list t n = map t [0 ..< n]"

values "{list t n |t n. (array_sum, nth[3,4,0,3,7],5) ⇒ (t,n)}"

definition
WHILE Less (N 0) (!(N 0))
DO ( N 1 ::= Plus(!(N 1)) (!(!(N 0)));
N 0 ::= !(Plus(!(N 0))(N 1)) )"

values "{list t n |t n. (linked_list_sum, nth[4,0,3,0,7,2],6) ⇒ (t,n)}"

definition
"array_init =
New (N 0) (!(N 1)); N 2 ::= !(N 0);
WHILE Less (!(N 2)) (Plus (!(N 0)) (!(N 1)))
DO ( !(N 2) ::= !(N 2);
N 2 ::= Plus (!(N 2)) (N 1) )"

values "{list t n |t n. (array_init, nth[5,2,7],3) ⇒ (t,n)}"

definition