Theory Natural

Up to index of Isabelle/HOL/IMPP

theory Natural = Com
files [Natural.ML]:

(*  Title:      HOL/IMPP/Natural.thy
    ID:         $Id: Natural.thy,v 1.18 1999/11/24 13:48:19 oheimb Exp $
    Author:     Tobias Nipkow & Robert Sandner, David von Oheimb, TUM
    Copyright   1996, 1999 TUM

Natural semantics of commands
*)

Natural = Com + 

(** Execution of commands **)
consts   evalc :: "(com * state *       state) set"
       "@evalc":: [com,state,    state] => bool ("<_,_>/ -c-> _" [0,0,  51] 51)
         evaln :: "(com * state * nat * state) set"
       "@evaln":: [com,state,nat,state] => bool ("<_,_>/ -_-> _" [0,0,0,51] 51)

translations  "<c,s> -c-> s'" == "(c,s,  s') : evalc"
              "<c,s> -n-> s'" == "(c,s,n,s') : evaln"

consts
  newlocs :: locals
  setlocs :: state => locals => state
  getlocs :: state => locals
  update  :: state => vname => val => state     ("_/[_/::=/_]" [900,0,0] 900)
defs (* not acutally used in meta theory *)
  newlocs_def "newlocs       == %x. arbitrary"
  setlocs_def "setlocs s l'  == case s of st g l => st g l'"
  getlocs_def "getlocs s     == case s of st g l => l"
   update_def "update s vn v == case vn of
                              Glb gn => (case s of st g l => st (g(gn:=v)) l)
                            | Loc ln => (case s of st g l => st g (l(ln:=v)))"

syntax (* IN Natural.thy *)
  loc :: state => locals    ("_<_>" [75,0] 75)
translations
  "s<X>" == "getlocs s X"

inductive evalc
  intrs
    Skip    "<SKIP,s> -c-> s"

    Assign  "<X :== a,s> -c-> s[X::=a s]"

    Local   "<c, s0[Loc X::= a s0]> -c-> s1 ==>
             <LOCAL X := a IN c, s0> -c-> s1[Loc X::=s0<X>]"

    Semi    "[| <c0,s0> -c-> s1; <c1,s1> -c-> s2 |] ==>
             <c0;; c1, s0> -c-> s2"

    IfTrue  "[| b s; <c0,s> -c-> s1 |] ==>
             <IF b THEN c0 ELSE c1, s> -c-> s1"

    IfFalse "[| ~b s; <c1,s> -c-> s1 |] ==>
             <IF b THEN c0 ELSE c1, s> -c-> s1"

    WhileFalse "~b s ==> <WHILE b DO c,s> -c-> s"

    WhileTrue  "[| b s0;  <c,s0> -c-> s1;  <WHILE b DO c, s1> -c-> s2 |] ==>
                <WHILE b DO c, s0> -c-> s2"

    Body       "<body pn, s0> -c-> s1 ==>
                <BODY pn, s0> -c-> s1"

    Call       "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -c-> s1 ==>
                <X:=CALL pn(a), s0> -c-> (setlocs s1 (getlocs s0))
                                         [X::=s1<Res>]"

inductive evaln
  intrs
    Skip    "<SKIP,s> -n-> s"

    Assign  "<X :== a,s> -n-> s[X::=a s]"

    Local   "<c, s0[Loc X::= a s0]> -n-> s1 ==>
             <LOCAL X := a IN c, s0> -n-> s1[Loc X::=s0<X>]"

    Semi    "[| <c0,s0> -n-> s1; <c1,s1> -n-> s2 |] ==>
             <c0;; c1, s0> -n-> s2"

    IfTrue  "[| b s; <c0,s> -n-> s1 |] ==>
             <IF b THEN c0 ELSE c1, s> -n-> s1"

    IfFalse "[| ~b s; <c1,s> -n-> s1 |] ==>
             <IF b THEN c0 ELSE c1, s> -n-> s1"

    WhileFalse "~b s ==> <WHILE b DO c,s> -n-> s"

    WhileTrue  "[| b s0;  <c,s0> -n-> s1;  <WHILE b DO c, s1> -n-> s2 |] ==>
                <WHILE b DO c, s0> -n-> s2"

    Body       "<body pn, s0> -n    -> s1 ==>
                <BODY pn, s0> -Suc n-> s1"

    Call       "<BODY pn, (setlocs s0 newlocs)[Loc Arg::=a s0]> -n-> s1 ==>
                <X:=CALL pn(a), s0> -n-> (setlocs s1 (getlocs s0))
                                         [X::=s1<Res>]"
end

theorem com_det:

  [| <c,s> -c-> t; <c,s> -c-> u |] ==> u = t  [term, !]

theorem evaln_evalc:

  <c,s> -n-> t ==> <c,s> -c-> t

theorem Suc_le_D:

  Suc n <= m' ==> EX m. m' = Suc m

theorem Suc_le_D_lemma:

  [| Suc n <= m'; !!m. n <= m ==> P (Suc m) |] ==> P m'

theorem evaln_nonstrict:

  [| <c,s> -n-> t; n <= m |] ==> <c,s> -m-> t  [term]

theorem evaln_Suc:

  <c,s> -n-> s' ==> <c,s> -Suc n-> s'

theorem evaln_max2:

  [| <c1,s1> -n1-> t1; <c2,s2> -n2-> t2 |]
  ==> EX n. <c1,s1> -n-> t1 & <c2,s2> -n-> t2

theorem evalc_evaln:

  <c,s> -c-> t ==> EX n. <c,s> -n-> t

theorem eval_eq:

  <c,s> -c-> t = (EX n. <c,s> -n-> t)