src/HOL/IMP/C_like.thy
author paulson <lp15@cam.ac.uk>
Mon May 23 15:33:24 2016 +0100 (2016-05-23)
changeset 63114 27afe7af7379
parent 58310 91ea607a34d8
child 67406 23307fd33906
permissions -rw-r--r--
Lots of new material for multivariate analysis
kleing@43158
     1
theory C_like imports Main begin
kleing@43158
     2
kleing@43158
     3
subsection "A C-like Language"
kleing@43158
     4
kleing@43158
     5
type_synonym state = "nat \<Rightarrow> nat"
kleing@43158
     6
blanchet@58310
     7
datatype aexp = N nat | Deref aexp ("!") | Plus aexp aexp
kleing@43158
     8
kleing@43158
     9
fun aval :: "aexp \<Rightarrow> state \<Rightarrow> nat" where
kleing@43158
    10
"aval (N n) s = n" |
kleing@43158
    11
"aval (!a) s = s(aval a s)" |
wenzelm@53015
    12
"aval (Plus a\<^sub>1 a\<^sub>2) s = aval a\<^sub>1 s + aval a\<^sub>2 s"
kleing@43158
    13
blanchet@58310
    14
datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
kleing@43158
    15
kleing@43158
    16
primrec bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where
nipkow@45200
    17
"bval (Bc v) _ = v" |
kleing@43158
    18
"bval (Not b) s = (\<not> bval b s)" |
wenzelm@53015
    19
"bval (And b\<^sub>1 b\<^sub>2) s = (if bval b\<^sub>1 s then bval b\<^sub>2 s else False)" |
wenzelm@53015
    20
"bval (Less a\<^sub>1 a\<^sub>2) s = (aval a\<^sub>1 s < aval a\<^sub>2 s)"
kleing@43158
    21
kleing@43158
    22
blanchet@58310
    23
datatype
kleing@43158
    24
  com = SKIP 
kleing@43158
    25
      | Assign aexp aexp         ("_ ::= _" [61, 61] 61)
kleing@43158
    26
      | New    aexp aexp
nipkow@47818
    27
      | Seq    com  com          ("_;/ _"  [60, 61] 60)
kleing@43158
    28
      | If     bexp com com     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61)
kleing@43158
    29
      | While  bexp com         ("(WHILE _/ DO _)"  [0, 61] 61)
kleing@43158
    30
kleing@43158
    31
inductive
kleing@43158
    32
  big_step :: "com \<times> state \<times> nat \<Rightarrow> state \<times> nat \<Rightarrow> bool"  (infix "\<Rightarrow>" 55)
kleing@43158
    33
where
kleing@43158
    34
Skip:    "(SKIP,sn) \<Rightarrow> sn" |
kleing@43158
    35
Assign:  "(lhs ::= a,s,n) \<Rightarrow> (s(aval lhs s := aval a s),n)" |
kleing@43158
    36
New:     "(New lhs a,s,n) \<Rightarrow> (s(aval lhs s := n), n+aval a s)"  |
wenzelm@53015
    37
Seq:    "\<lbrakk> (c\<^sub>1,sn\<^sub>1) \<Rightarrow> sn\<^sub>2;  (c\<^sub>2,sn\<^sub>2) \<Rightarrow> sn\<^sub>3 \<rbrakk> \<Longrightarrow>
wenzelm@53015
    38
          (c\<^sub>1;c\<^sub>2, sn\<^sub>1) \<Rightarrow> sn\<^sub>3" |
kleing@43158
    39
wenzelm@53015
    40
IfTrue:  "\<lbrakk> bval b s;  (c\<^sub>1,s,n) \<Rightarrow> tn \<rbrakk> \<Longrightarrow>
wenzelm@53015
    41
         (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s,n) \<Rightarrow> tn" |
wenzelm@53015
    42
IfFalse: "\<lbrakk> \<not>bval b s;  (c\<^sub>2,s,n) \<Rightarrow> tn \<rbrakk> \<Longrightarrow>
wenzelm@53015
    43
         (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s,n) \<Rightarrow> tn" |
kleing@43158
    44
kleing@43158
    45
WhileFalse: "\<not>bval b s \<Longrightarrow> (WHILE b DO c,s,n) \<Rightarrow> (s,n)" |
kleing@43158
    46
WhileTrue:
wenzelm@53015
    47
  "\<lbrakk> bval b s\<^sub>1;  (c,s\<^sub>1,n) \<Rightarrow> sn\<^sub>2;  (WHILE b DO c, sn\<^sub>2) \<Rightarrow> sn\<^sub>3 \<rbrakk> \<Longrightarrow>
wenzelm@53015
    48
   (WHILE b DO c, s\<^sub>1,n) \<Rightarrow> sn\<^sub>3"
kleing@43158
    49
kleing@43158
    50
code_pred big_step .
kleing@43158
    51
bulwahn@43738
    52
declare [[values_timeout = 3600]]
kleing@43158
    53
kleing@43158
    54
text{* Examples: *}
kleing@43158
    55
kleing@43158
    56
definition
kleing@43158
    57
"array_sum =
kleing@43158
    58
 WHILE Less (!(N 0)) (Plus (!(N 1)) (N 1))
kleing@43158
    59
 DO ( N 2 ::= Plus (!(N 2)) (!(!(N 0)));
kleing@43158
    60
      N 0 ::= Plus (!(N 0)) (N 1) )"
kleing@43158
    61
kleing@43158
    62
text {* To show the first n variables in a @{typ "nat \<Rightarrow> nat"} state: *}
kleing@43158
    63
definition 
kleing@43158
    64
  "list t n = map t [0 ..< n]"
kleing@43158
    65
kleing@43158
    66
values "{list t n |t n. (array_sum, nth[3,4,0,3,7],5) \<Rightarrow> (t,n)}"
kleing@43158
    67
kleing@43158
    68
definition
kleing@43158
    69
"linked_list_sum =
kleing@43158
    70
 WHILE Less (N 0) (!(N 0))
kleing@43158
    71
 DO ( N 1 ::= Plus(!(N 1)) (!(!(N 0)));
kleing@43158
    72
      N 0 ::= !(Plus(!(N 0))(N 1)) )"
kleing@43158
    73
kleing@43158
    74
values "{list t n |t n. (linked_list_sum, nth[4,0,3,0,7,2],6) \<Rightarrow> (t,n)}"
kleing@43158
    75
kleing@43158
    76
definition
kleing@43158
    77
"array_init =
kleing@43158
    78
 New (N 0) (!(N 1)); N 2 ::= !(N 0);
kleing@43158
    79
 WHILE Less (!(N 2)) (Plus (!(N 0)) (!(N 1)))
kleing@43158
    80
 DO ( !(N 2) ::= !(N 2);
kleing@43158
    81
      N 2 ::= Plus (!(N 2)) (N 1) )"
kleing@43158
    82
kleing@43158
    83
values "{list t n |t n. (array_init, nth[5,2,7],3) \<Rightarrow> (t,n)}"
kleing@43158
    84
kleing@43158
    85
definition
kleing@43158
    86
"linked_list_init =
kleing@43158
    87
 WHILE Less (!(N 1)) (!(N 0))
kleing@43158
    88
 DO ( New (N 3) (N 2);
kleing@43158
    89
      N 1 ::=  Plus (!(N 1)) (N 1);
kleing@43158
    90
      !(N 3) ::= !(N 1);
kleing@43158
    91
      Plus (!(N 3)) (N 1) ::= !(N 2);
kleing@43158
    92
      N 2 ::= !(N 3) )"
kleing@43158
    93
kleing@43158
    94
values "{list t n |t n. (linked_list_init, nth[2,0,0,0],4) \<Rightarrow> (t,n)}"
kleing@43158
    95
kleing@43158
    96
end