src/HOL/Induct/Com.thy
 changeset 10759 994877ee68cb parent 5184 9b8547a9496a child 11464 ddea204de5bc
```--- 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```