src/HOL/Induct/Com.thy
changeset 3120 c58423c20740
child 3146 922a60451382
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/Com.thy	Wed May 07 12:50:26 1997 +0200
@@ -0,0 +1,69 @@
+(*  Title:      HOL/Induct/Com
+    ID:         $Id$
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1997  University of Cambridge
+
+Example of Mutual Induction via Iteratived Inductive Definitions: Commands
+*)
+
+Com = Arith +
+
+types loc
+      state = "loc => nat"
+      n2n2n = "nat => nat => nat"
+
+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
+      | ":="  loc exp          (infixl  60)
+      | Semi  exp exp          ("_;;_"  [60, 60] 10)
+      | Cond  exp exp exp      ("IF _ THEN _ ELSE _"  60)
+      | While exp exp          ("WHILE _ DO _"  60)
+
+(** Execution of commands **)
+consts  exec    :: "((exp*state) * (nat*state)) set => ((exp*state)*state)set"
+       "@exec"  :: "((exp*state) * (nat*state)) set => 
+                    [exp*state,state] => bool"     ("_/ -[_]-> _" [50,0,50] 50)
+
+translations  "csig -[eval]-> s" == "(csig,s) : exec 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), (v,s')) : eval ==> (x := e, s) -[eval]-> s'[v/x]"
+
+    Semi    "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |] 
+            ==> (c0 ;; c1, s) -[eval]-> s1"
+
+    IfTrue "[| ((e,s), (0,s')) : eval;  (c0,s') -[eval]-> s1 |] 
+            ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
+
+    IfFalse "[| ((e,s), (1,s')) : eval;  (c1,s') -[eval]-> s1 |] 
+             ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
+
+    WhileFalse "((e,s), (1,s1)) : eval ==> (WHILE e DO c, s) -[eval]-> s1"
+
+    WhileTrue  "[| ((e,s), (0,s1)) : eval;
+                (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