--- a/src/HOL/Induct/Com.thy Mon Jan 01 11:52:04 2001 +0100
+++ b/src/HOL/Induct/Com.thy Tue Jan 02 10:27:10 2001 +0100
@@ -6,7 +6,7 @@
Example of Mutual Induction via Iteratived Inductive Definitions: Commands
*)
-Com = Datatype +
+Com = Main +
types loc
state = "loc => nat"
@@ -14,23 +14,22 @@
arities loc :: term
-(*To avoid a mutually recursive datatype declaration, expressions and commands
- are combined to form a single datatype.*)
datatype
exp = N nat
| X loc
| Op n2n2n exp exp
- | valOf exp exp ("VALOF _ RESULTIS _" 60)
- | SKIP
+ | valOf com exp ("VALOF _ RESULTIS _" 60)
+and
+ com = SKIP
| ":=" loc exp (infixl 60)
- | Semi exp exp ("_;;_" [60, 60] 60)
- | Cond exp exp exp ("IF _ THEN _ ELSE _" 60)
- | While exp exp ("WHILE _ DO _" 60)
+ | Semi com com ("_;;_" [60, 60] 60)
+ | Cond exp com com ("IF _ THEN _ ELSE _" 60)
+ | While exp com ("WHILE _ DO _" 60)
(** Execution of commands **)
-consts exec :: "((exp*state) * (nat*state)) set => ((exp*state)*state)set"
+consts exec :: "((exp*state) * (nat*state)) set => ((com*state)*state)set"
"@exec" :: "((exp*state) * (nat*state)) set =>
- [exp*state,state] => bool" ("_/ -[_]-> _" [50,0,50] 50)
+ [com*state,state] => bool" ("_/ -[_]-> _" [50,0,50] 50)
translations "csig -[eval]-> s" == "(csig,s) : exec eval"
@@ -40,16 +39,12 @@
translations
"esig -|[eval]-> ns" => "(esig,ns) : eval"
-constdefs assign :: [state,nat,loc] => state ("_[_'/_]" [95,0,0] 95)
- "s[m/x] == (%y. if y=x then m else s y)"
-
-
(*Command execution. Natural numbers represent Booleans: 0=True, 1=False*)
inductive "exec eval"
intrs
Skip "(SKIP,s) -[eval]-> s"
- Assign "(e,s) -|[eval]-> (v,s') ==> (x := e, s) -[eval]-> s'[v/x]"
+ Assign "(e,s) -|[eval]-> (v,s') ==> (x := e, s) -[eval]-> s'(x:=v)"
Semi "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |]
==> (c0 ;; c1, s) -[eval]-> s1"
@@ -65,11 +60,4 @@
WhileTrue "[| (e,s) -|[eval]-> (0,s1);
(c,s1) -[eval]-> s2; (WHILE e DO c, s2) -[eval]-> s3 |]
==> (WHILE e DO c, s) -[eval]-> s3"
-
-constdefs
- Unique :: "['a, 'b, ('a*'b) set] => bool"
- "Unique x y r == ALL y'. (x,y'): r --> y = y'"
-
- Function :: "('a*'b) set => bool"
- "Function r == ALL x y. (x,y): r --> Unique x y r"
end