src/HOL/IMPP/Natural.thy
author wenzelm
Sat, 17 Sep 2005 20:14:30 +0200
changeset 17477 ceb42ea2f223
parent 8177 e59e93ad85eb
child 19803 aa2581752afb
permissions -rw-r--r--
converted to Isar theory format;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     1
(*  Title:      HOL/IMPP/Natural.thy
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     2
    ID:         $Id$
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     3
    Author:     David von Oheimb (based on a theory by Tobias Nipkow et al), TUM
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     4
    Copyright   1999 TUM
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     5
*)
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
     6
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
     7
header {* Natural semantics of commands *}
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
     8
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
     9
theory Natural
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    10
imports Com
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    11
begin
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    12
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    13
(** Execution of commands **)
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    14
consts
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    15
  evalc :: "(com * state *       state) set"
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    16
  evaln :: "(com * state * nat * state) set"
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    17
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    18
syntax
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    19
  "@evalc":: "[com,state,    state] => bool"  ("<_,_>/ -c-> _" [0,0,  51] 51)
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    20
  "@evaln":: "[com,state,nat,state] => bool"  ("<_,_>/ -_-> _" [0,0,0,51] 51)
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    21
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    22
translations
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    23
  "<c,s> -c-> s'" == "(c,s,  s') : evalc"
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    24
  "<c,s> -n-> s'" == "(c,s,n,s') : evaln"
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    25
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    26
consts
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    27
  newlocs :: locals
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    28
  setlocs :: "state => locals => state"
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    29
  getlocs :: "state => locals"
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    30
  update  :: "state => vname => val => state"     ("_/[_/::=/_]" [900,0,0] 900)
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    31
syntax (* IN Natural.thy *)
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    32
  loc :: "state => locals"    ("_<_>" [75,0] 75)
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    33
translations
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    34
  "s<X>" == "getlocs s X"
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    35
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    36
inductive evalc
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    37
  intros
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    38
    Skip:    "<SKIP,s> -c-> s"
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    39
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    40
    Assign:  "<X :== a,s> -c-> s[X::=a s]"
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    41
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    42
    Local:   "<c, s0[Loc Y::= a s0]> -c-> s1 ==>
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    43
              <LOCAL Y := a IN c, s0> -c-> s1[Loc Y::=s0<Y>]"
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    44
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    45
    Semi:    "[| <c0,s0> -c-> s1; <c1,s1> -c-> s2 |] ==>
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    46
              <c0;; c1, s0> -c-> s2"
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    47
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    48
    IfTrue:  "[| b s; <c0,s> -c-> s1 |] ==>
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    49
              <IF b THEN c0 ELSE c1, s> -c-> s1"
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    50
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    51
    IfFalse: "[| ~b s; <c1,s> -c-> s1 |] ==>
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    52
              <IF b THEN c0 ELSE c1, s> -c-> s1"
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    53
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    54
    WhileFalse: "~b s ==> <WHILE b DO c,s> -c-> s"
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    55
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    56
    WhileTrue:  "[| b s0;  <c,s0> -c-> s1;  <WHILE b DO c, s1> -c-> s2 |] ==>
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    57
                 <WHILE b DO c, s0> -c-> s2"
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    58
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    59
    Body:       "<the (body pn), s0> -c-> s1 ==>
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    60
                 <BODY pn, s0> -c-> s1"
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    61
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    62
    Call:       "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -c-> s1 ==>
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    63
                 <X:=CALL pn(a), s0> -c-> (setlocs s1 (getlocs s0))
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    64
                                          [X::=s1<Res>]"
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    65
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    66
inductive evaln
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    67
  intros
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    68
    Skip:    "<SKIP,s> -n-> s"
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    69
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    70
    Assign:  "<X :== a,s> -n-> s[X::=a s]"
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    71
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    72
    Local:   "<c, s0[Loc Y::= a s0]> -n-> s1 ==>
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    73
              <LOCAL Y := a IN c, s0> -n-> s1[Loc Y::=s0<Y>]"
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    74
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    75
    Semi:    "[| <c0,s0> -n-> s1; <c1,s1> -n-> s2 |] ==>
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    76
              <c0;; c1, s0> -n-> s2"
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    77
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    78
    IfTrue:  "[| b s; <c0,s> -n-> s1 |] ==>
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    79
              <IF b THEN c0 ELSE c1, s> -n-> s1"
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    80
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    81
    IfFalse: "[| ~b s; <c1,s> -n-> s1 |] ==>
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    82
              <IF b THEN c0 ELSE c1, s> -n-> s1"
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    83
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    84
    WhileFalse: "~b s ==> <WHILE b DO c,s> -n-> s"
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    85
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    86
    WhileTrue:  "[| b s0;  <c,s0> -n-> s1;  <WHILE b DO c, s1> -n-> s2 |] ==>
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    87
                 <WHILE b DO c, s0> -n-> s2"
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    88
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    89
    Body:       "<the (body pn), s0> -    n-> s1 ==>
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    90
                 <BODY pn, s0> -Suc n-> s1"
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    91
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    92
    Call:       "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -n-> s1 ==>
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    93
                 <X:=CALL pn(a), s0> -n-> (setlocs s1 (getlocs s0))
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    94
                                          [X::=s1<Res>]"
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    95
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
    96
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    97
inductive_cases evalc_elim_cases:
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    98
  "<SKIP,s> -c-> t"  "<X:==a,s> -c-> t"  "<LOCAL Y:=a IN c,s> -c-> t"
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
    99
  "<c1;;c2,s> -c-> t"  "<IF b THEN c1 ELSE c2,s> -c-> t"
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
   100
  "<BODY P,s> -c-> s1"  "<X:=CALL P(a),s> -c-> s1"
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   101
17477
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
   102
inductive_cases evaln_elim_cases:
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
   103
  "<SKIP,s> -n-> t"  "<X:==a,s> -n-> t"  "<LOCAL Y:=a IN c,s> -n-> t"
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
   104
  "<c1;;c2,s> -n-> t"  "<IF b THEN c1 ELSE c2,s> -n-> t"
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
   105
  "<BODY P,s> -n-> s1"  "<X:=CALL P(a),s> -n-> s1"
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
   106
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
   107
inductive_cases evalc_WHILE_case: "<WHILE b DO c,s> -c-> t"
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
   108
inductive_cases evaln_WHILE_case: "<WHILE b DO c,s> -n-> t"
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
   109
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
   110
ML {* use_legacy_bindings (the_context ()) *}
ceb42ea2f223 converted to Isar theory format;
wenzelm
parents: 8177
diff changeset
   111
8177
e59e93ad85eb added IMPP to HOL
oheimb
parents:
diff changeset
   112
end