# Theory Natural

Up to index of Isabelle/HOL/IMPP

theory Natural
imports Com
uses [Natural.ML]
begin

    (*  Title:      HOL/IMPP/Natural.thy
        ID:         $Id: Natural.thy,v 1.2 2005/09/17 18:14:31 wenzelm Exp $
        Author:     David von Oheimb (based on a theory by Tobias Nipkow et al), TUM
        Copyright   1999 TUM
    *)

    header {* Natural semantics of commands *}

    theory Natural
    imports Com
    begin

    (** Execution of commands **)
    consts
      evalc :: "(com * state *       state) set"
      evaln :: "(com * state * nat * state) set"

    syntax
      "@evalc":: "[com,state,    state] => bool"  ("<_,_>/ -c-> _" [0,0,  51] 51)
      "@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)
    syntax (* IN Natural.thy *)
      loc :: "state => locals"    ("_<_>" [75,0] 75)
    translations
      "s<X>" == "getlocs s X"

    inductive evalc
      intros
        Skip:    "<SKIP,s> -c-> s"

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

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

        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:       "<the (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
      intros
        Skip:    "<SKIP,s> -n-> s"

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

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

        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:       "<the (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>]"

    inductive_cases evalc_elim_cases:
      "<SKIP,s> -c-> t"  "<X:==a,s> -c-> t"  "<LOCAL Y:=a IN c,s> -c-> t"
      "<c1;;c2,s> -c-> t"  "<IF b THEN c1 ELSE c2,s> -c-> t"
      "<BODY P,s> -c-> s1"  "<X:=CALL P(a),s> -c-> s1"

    inductive_cases evaln_elim_cases:
      "<SKIP,s> -n-> t"  "<X:==a,s> -n-> t"  "<LOCAL Y:=a IN c,s> -n-> t"
      "<c1;;c2,s> -n-> t"  "<IF b THEN c1 ELSE c2,s> -n-> t"
      "<BODY P,s> -n-> s1"  "<X:=CALL P(a),s> -n-> s1"

    inductive_cases evalc_WHILE_case: "<WHILE b DO c,s> -c-> t"
    inductive_cases evaln_WHILE_case: "<WHILE b DO c,s> -n-> t"

    ML {* use_legacy_bindings (the_context ()) *}

    end

lemmas evalc_elim_cases:

      [| <SKIP,s> -c-> t; t = s ==> P |] ==> P

      [| <X:==a,s> -c-> t; t = s[X::=a s] ==> P |] ==> P

      [| <LOCAL Y:=a IN c,s> -c-> t;
         !!s1. [| <c,s[Loc Y::=a s]> -c-> s1; t = s1[Loc Y::=s<Y>] |] ==> P |]
      ==> P

      [| <c1.0;; c2.0,s> -c-> t;
         !!s1. [| <c1.0,s> -c-> s1; <c2.0,s1> -c-> t |] ==> P |]
      ==> P

      [| <IF b THEN c1.0 ELSE c2.0,s> -c-> t; [| b s; <c1.0,s> -c-> t |] ==> P;
         [| ¬ b s; <c2.0,s> -c-> t |] ==> P |]
      ==> P

      [| <BODY Pa,s> -c-> s1.0; <the (body Pa),s> -c-> s1.0 ==> P |] ==> P

      [| <X:=CALL Pa(a),s> -c-> s1.0;
         !!s1. [| <BODY Pa,setlocs s newlocs[Loc Arg::=a s]> -c-> s1;
                  s1.0 = setlocs s1 (getlocs s)[X::=s1<Res>] |]
               ==> P |]
      ==> P

lemmas evaln_elim_cases:

      [| <SKIP,s> -n-> t; t = s ==> P |] ==> P

      [| <X:==a,s> -n-> t; t = s[X::=a s] ==> P |] ==> P

      [| <LOCAL Y:=a IN c,s> -n-> t;
         !!s1. [| <c,s[Loc Y::=a s]> -n-> s1; t = s1[Loc Y::=s<Y>] |] ==> P |]
      ==> P

      [| <c1.0;; c2.0,s> -n-> t;
         !!s1. [| <c1.0,s> -n-> s1; <c2.0,s1> -n-> t |] ==> P |]
      ==> P

      [| <IF b THEN c1.0 ELSE c2.0,s> -n-> t; [| b s; <c1.0,s> -n-> t |] ==> P;
         [| ¬ b s; <c2.0,s> -n-> t |] ==> P |]
      ==> P

      [| <BODY Pa,s> -n-> s1.0;
         !!n. [| <the (body Pa),s> -n-> s1.0; n = Suc n |] ==> P |]
      ==> P

      [| <X:=CALL Pa(a),s> -n-> s1.0;
         !!s1. [| <BODY Pa,setlocs s newlocs[Loc Arg::=a s]> -n-> s1;
                  s1.0 = setlocs s1 (getlocs s)[X::=s1<Res>] |]
               ==> P |]
      ==> P

lemmas evalc_WHILE_case:

      [| <WHILE b DO c,s> -c-> t; [| ¬ b s; t = s |] ==> P;
         !!s1. [| b s; <c,s> -c-> s1; <WHILE b DO c,s1> -c-> t |] ==> P |]
      ==> P

lemmas evaln_WHILE_case:

      [| <WHILE b DO c,s> -n-> t; [| ¬ b s; t = s |] ==> P;
         !!s1. [| b s; <c,s> -n-> s1; <WHILE b DO c,s1> -n-> t |] ==> P |]
      ==> P

theorem com_det:

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

theorem evaln_evalc:

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

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

theorem evaln_Suc:

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

theorem evaln_max2:

      [| <c1.0,s1.0> -n1.0-> t1.0; <c2.0,s2.0> -n2.0-> t2.0 |]
      ==> ∃n. <c1.0,s1.0> -n-> t1.0 ∧ <c2.0,s2.0> -n-> t2.0

theorem evalc_evaln:

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

theorem eval_eq:

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