diff -r 315cb57e3dd7 -r ceb42ea2f223 src/HOL/IMPP/Natural.thy --- a/src/HOL/IMPP/Natural.thy Sat Sep 17 19:17:35 2005 +0200 +++ b/src/HOL/IMPP/Natural.thy Sat Sep 17 20:14:30 2005 +0200 @@ -2,88 +2,111 @@ ID: $Id$ Author: David von Oheimb (based on a theory by Tobias Nipkow et al), TUM Copyright 1999 TUM - -Natural semantics of commands *) -Natural = Com + +header {* Natural semantics of commands *} + +theory Natural +imports Com +begin (** 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) +consts + evalc :: "(com * state * state) set" + evaln :: "(com * state * nat * state) set" -translations " -c-> s'" == "(c,s, s') : evalc" - " -n-> s'" == "(c,s,n,s') : evaln" +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, s') : evalc" + " -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) + 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) + loc :: "state => locals" ("_<_>" [75,0] 75) translations "s" == "getlocs s X" inductive evalc - intrs - Skip " -c-> s" + intros + Skip: " -c-> s" - Assign " -c-> s[X::=a s]" + Assign: " -c-> s[X::=a s]" - Local " -c-> s1 ==> - -c-> s1[Loc Y::=s0]" + Local: " -c-> s1 ==> + -c-> s1[Loc Y::=s0]" - Semi "[| -c-> s1; -c-> s2 |] ==> - -c-> s2" + Semi: "[| -c-> s1; -c-> s2 |] ==> + -c-> s2" - IfTrue "[| b s; -c-> s1 |] ==> - -c-> s1" + IfTrue: "[| b s; -c-> s1 |] ==> + -c-> s1" - IfFalse "[| ~b s; -c-> s1 |] ==> - -c-> s1" + IfFalse: "[| ~b s; -c-> s1 |] ==> + -c-> s1" - WhileFalse "~b s ==> -c-> s" + WhileFalse: "~b s ==> -c-> s" - WhileTrue "[| b s0; -c-> s1; -c-> s2 |] ==> - -c-> s2" + WhileTrue: "[| b s0; -c-> s1; -c-> s2 |] ==> + -c-> s2" - Body " -c-> s1 ==> - -c-> s1" + Body: " -c-> s1 ==> + -c-> s1" - Call " -c-> s1 ==> - -c-> (setlocs s1 (getlocs s0)) - [X::=s1]" + Call: " -c-> s1 ==> + -c-> (setlocs s1 (getlocs s0)) + [X::=s1]" inductive evaln - intrs - Skip " -n-> s" + intros + Skip: " -n-> s" + + Assign: " -n-> s[X::=a s]" - Assign " -n-> s[X::=a s]" + Local: " -n-> s1 ==> + -n-> s1[Loc Y::=s0]" + + Semi: "[| -n-> s1; -n-> s2 |] ==> + -n-> s2" - Local " -n-> s1 ==> - -n-> s1[Loc Y::=s0]" + IfTrue: "[| b s; -n-> s1 |] ==> + -n-> s1" - Semi "[| -n-> s1; -n-> s2 |] ==> - -n-> s2" + IfFalse: "[| ~b s; -n-> s1 |] ==> + -n-> s1" - IfTrue "[| b s; -n-> s1 |] ==> - -n-> s1" + WhileFalse: "~b s ==> -n-> s" + + WhileTrue: "[| b s0; -n-> s1; -n-> s2 |] ==> + -n-> s2" - IfFalse "[| ~b s; -n-> s1 |] ==> - -n-> s1" + Body: " - n-> s1 ==> + -Suc n-> s1" - WhileFalse "~b s ==> -n-> s" + Call: " -n-> s1 ==> + -n-> (setlocs s1 (getlocs s0)) + [X::=s1]" - WhileTrue "[| b s0; -n-> s1; -n-> s2 |] ==> - -n-> s2" - Body " - n-> s1 ==> - -Suc n-> s1" +inductive_cases evalc_elim_cases: + " -c-> t" " -c-> t" " -c-> t" + " -c-> t" " -c-> t" + " -c-> s1" " -c-> s1" - Call " -n-> s1 ==> - -n-> (setlocs s1 (getlocs s0)) - [X::=s1]" +inductive_cases evaln_elim_cases: + " -n-> t" " -n-> t" " -n-> t" + " -n-> t" " -n-> t" + " -n-> s1" " -n-> s1" + +inductive_cases evalc_WHILE_case: " -c-> t" +inductive_cases evaln_WHILE_case: " -n-> t" + +ML {* use_legacy_bindings (the_context ()) *} + end