Quelle  C_like.thy

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 🍋‹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
"linked_list_sum =
 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
"linked_list_init =
 WHILE Less (!(N 1)) (!(N 0))
 DO ( New (N 3) (N 2);
      N 1 ::= Plus (!(N 1)) (N 1);
      !(N 3) ::= !(N 1);
      Plus (!(N 3)) (N 1) ::= !(N 2);
      N 2 ::= !(N 3) )"

values "{list t n |t n. (linked_list_init, nth[2,0,0,0],4) ==> (t,n)}"

end