src/HOL/IMP/C_like.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 45200 1f1897ac7877
child 47818 151d137f1095
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     1
theory C_like imports Main begin
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     2
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     3
subsection "A C-like Language"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     4
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     5
type_synonym state = "nat \<Rightarrow> nat"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     6
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     7
datatype aexp = N nat | Deref aexp ("!") | Plus aexp aexp
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     8
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
     9
fun aval :: "aexp \<Rightarrow> state \<Rightarrow> nat" where
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    10
"aval (N n) s = n" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    11
"aval (!a) s = s(aval a s)" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    12
"aval (Plus a\<^isub>1 a\<^isub>2) s = aval a\<^isub>1 s + aval a\<^isub>2 s"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    13
45200
1f1897ac7877 renamed B to Bc
nipkow
parents: 43738
diff changeset
    14
datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    15
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    16
primrec bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where
45200
1f1897ac7877 renamed B to Bc
nipkow
parents: 43738
diff changeset
    17
"bval (Bc v) _ = v" |
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    18
"bval (Not b) s = (\<not> bval b s)" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    19
"bval (And b\<^isub>1 b\<^isub>2) s = (if bval b\<^isub>1 s then bval b\<^isub>2 s else False)" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    20
"bval (Less a\<^isub>1 a\<^isub>2) s = (aval a\<^isub>1 s < aval a\<^isub>2 s)"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    21
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    22
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    23
datatype
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    24
  com = SKIP 
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    25
      | Assign aexp aexp         ("_ ::= _" [61, 61] 61)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    26
      | New    aexp aexp
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    27
      | Semi   com  com          ("_;/ _"  [60, 61] 60)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    28
      | If     bexp com com     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    29
      | While  bexp com         ("(WHILE _/ DO _)"  [0, 61] 61)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    30
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    31
inductive
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    32
  big_step :: "com \<times> state \<times> nat \<Rightarrow> state \<times> nat \<Rightarrow> bool"  (infix "\<Rightarrow>" 55)
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    33
where
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    34
Skip:    "(SKIP,sn) \<Rightarrow> sn" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    35
Assign:  "(lhs ::= a,s,n) \<Rightarrow> (s(aval lhs s := aval a s),n)" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    36
New:     "(New lhs a,s,n) \<Rightarrow> (s(aval lhs s := n), n+aval a s)"  |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    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>
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    38
          (c\<^isub>1;c\<^isub>2, sn\<^isub>1) \<Rightarrow> sn\<^isub>3" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    39
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    40
IfTrue:  "\<lbrakk> bval b s;  (c\<^isub>1,s,n) \<Rightarrow> tn \<rbrakk> \<Longrightarrow>
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    41
         (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s,n) \<Rightarrow> tn" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    42
IfFalse: "\<lbrakk> \<not>bval b s;  (c\<^isub>2,s,n) \<Rightarrow> tn \<rbrakk> \<Longrightarrow>
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    43
         (IF b THEN c\<^isub>1 ELSE c\<^isub>2, s,n) \<Rightarrow> tn" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    44
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    45
WhileFalse: "\<not>bval b s \<Longrightarrow> (WHILE b DO c,s,n) \<Rightarrow> (s,n)" |
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    46
WhileTrue:
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    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>
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    48
   (WHILE b DO c, s\<^isub>1,n) \<Rightarrow> sn\<^isub>3"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    49
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    50
code_pred big_step .
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    51
43738
e40d2eddf2c0 adding a very liberal timeout for values after a test case failed due to the restricted timeout
bulwahn
parents: 43158
diff changeset
    52
declare [[values_timeout = 3600]]
43158
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    53
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    54
text{* Examples: *}
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    55
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    56
definition
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    57
"array_sum =
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    58
 WHILE Less (!(N 0)) (Plus (!(N 1)) (N 1))
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    59
 DO ( N 2 ::= Plus (!(N 2)) (!(!(N 0)));
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    60
      N 0 ::= Plus (!(N 0)) (N 1) )"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    61
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    62
text {* To show the first n variables in a @{typ "nat \<Rightarrow> nat"} state: *}
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    63
definition 
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    64
  "list t n = map t [0 ..< n]"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    65
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    66
values "{list t n |t n. (array_sum, nth[3,4,0,3,7],5) \<Rightarrow> (t,n)}"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    67
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    68
definition
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    69
"linked_list_sum =
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    70
 WHILE Less (N 0) (!(N 0))
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    71
 DO ( N 1 ::= Plus(!(N 1)) (!(!(N 0)));
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    72
      N 0 ::= !(Plus(!(N 0))(N 1)) )"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    73
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    74
values "{list t n |t n. (linked_list_sum, nth[4,0,3,0,7,2],6) \<Rightarrow> (t,n)}"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    75
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    76
definition
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    77
"array_init =
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    78
 New (N 0) (!(N 1)); N 2 ::= !(N 0);
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    79
 WHILE Less (!(N 2)) (Plus (!(N 0)) (!(N 1)))
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    80
 DO ( !(N 2) ::= !(N 2);
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    81
      N 2 ::= Plus (!(N 2)) (N 1) )"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    82
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    83
values "{list t n |t n. (array_init, nth[5,2,7],3) \<Rightarrow> (t,n)}"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    84
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    85
definition
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    86
"linked_list_init =
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    87
 WHILE Less (!(N 1)) (!(N 0))
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    88
 DO ( New (N 3) (N 2);
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    89
      N 1 ::=  Plus (!(N 1)) (N 1);
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    90
      !(N 3) ::= !(N 1);
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    91
      Plus (!(N 3)) (N 1) ::= !(N 2);
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    92
      N 2 ::= !(N 3) )"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    93
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    94
values "{list t n |t n. (linked_list_init, nth[2,0,0,0],4) \<Rightarrow> (t,n)}"
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    95
686fa0a0696e imported rest of new IMP
kleing
parents:
diff changeset
    96
end