# HG changeset patch
# User paulson
# Date 914860493 -3600
# Node ID f2e0938ba38decae75ef9f8f0ee1715dad077264
# Parent  2c8a8be36c94d99946b744741a458606a0de7580
converted to use new primrec section and update operator

diff -r 2c8a8be36c94 -r f2e0938ba38d src/ZF/IMP/Com.ML
--- a/src/ZF/IMP/Com.ML	Mon Dec 28 16:54:01 1998 +0100
+++ b/src/ZF/IMP/Com.ML	Mon Dec 28 16:54:53 1998 +0100
@@ -6,10 +6,6 @@
 
 open Com;
 
-val assign_type = prove_goalw Com.thy [assign_def]
-        "!!n. [| sigma:loc -> nat; n:nat |] ==> sigma[n/x] : loc -> nat"
-    (fn _ => [ fast_tac (claset() addIs [apply_type,lam_type,if_type]) 1 ]);
-
 val type_cs = claset() addSDs [evala.dom_subset RS subsetD,
 			      evalb.dom_subset RS subsetD,
 			      evalc.dom_subset RS subsetD];
diff -r 2c8a8be36c94 -r f2e0938ba38d src/ZF/IMP/Com.thy
--- a/src/ZF/IMP/Com.thy	Mon Dec 28 16:54:01 1998 +0100
+++ b/src/ZF/IMP/Com.thy	Mon Dec 28 16:54:53 1998 +0100
@@ -8,7 +8,7 @@
 And their Operational semantics
 *)
 
-Com = Datatype +
+Com = Main +
 
 (** Arithmetic expressions **)
 consts  loc  :: i
@@ -80,7 +80,7 @@
 
 datatype <= "univ(loc Un aexp Un bexp)"
   "com" = skip
-        | ":="  ("x:loc", "a:aexp")             (infixl 60)
+        | asgt  ("x:loc", "a:aexp")             (infixl 60)
         | semic ("c0:com", "c1:com")            ("_; _"  [60, 60] 10)
         | while ("b:bexp", "c:com")             ("while _ do _"  60)
         | ifc   ("b:bexp", "c0:com", "c1:com")  ("ifc _ then _ else _"  60)
@@ -91,13 +91,10 @@
 (** Execution of commands **)
 consts  evalc    :: i
         "-c->"   :: [i,i] => o                   (infixl 50)
-        "assign" :: [i,i,i] => i                 ("_[_'/_]"       [95,0,0] 95)
 
 translations
        "p -c-> s" == "<p,s> : evalc"
 
-defs 
-        assign_def      "sigma[m/x] == lam y:loc. if(y=x,m,sigma`y)"
 
 inductive
   domains "evalc" <= "(com * (loc -> nat)) * (loc -> nat)"
@@ -105,7 +102,7 @@
     skip    "[| sigma: loc -> nat |] ==> <skip,sigma> -c-> sigma"
 
     assign  "[| m: nat; x: loc; <a,sigma> -a-> m |] ==> 
-            <x := a,sigma> -c-> sigma[m/x]"
+            <x asgt a,sigma> -c-> sigma(x:=m)"
 
     semi    "[| <c0,sigma> -c-> sigma2; <c1,sigma2> -c-> sigma1 |] ==> 
             <c0 ; c1, sigma> -c-> sigma1"
@@ -125,9 +122,8 @@
                 <while b do c, sigma2> -c-> sigma1 |] ==> 
              <while b do c, sigma> -c-> sigma1 "
 
-  con_defs   "[assign_def]"
-  type_intrs "bexp.intrs @ com.intrs @ [if_type,lam_type,apply_type]"
+  type_intrs "com.intrs @ [update_type]"
   type_elims "[make_elim(evala.dom_subset RS subsetD),   
-              make_elim(evalb.dom_subset RS subsetD) ]"
+               make_elim(evalb.dom_subset RS subsetD) ]"
 
 end
diff -r 2c8a8be36c94 -r f2e0938ba38d src/ZF/IMP/Denotation.thy
--- a/src/ZF/IMP/Denotation.thy	Mon Dec 28 16:54:01 1998 +0100
+++ b/src/ZF/IMP/Denotation.thy	Mon Dec 28 16:54:53 1998 +0100
@@ -31,8 +31,8 @@
   B_or_def      "B(b0 ori b1) == (%sigma. B(b0,sigma) or B(b1,sigma))"
 
   C_skip_def    "C(skip) == id(loc->nat)"
-  C_assign_def  "C(x := a) == {io:(loc->nat)*(loc->nat). 
-                               snd(io) = fst(io)[A(a,fst(io))/x]}"
+  C_assign_def  "C(x asgt a) == {io:(loc->nat)*(loc->nat). 
+                               snd(io) = fst(io)(x := A(a,fst(io)))}"
 
   C_comp_def    "C(c0 ; c1) == C(c1) O C(c0)"
   C_if_def      "C(ifc b then c0 else c1) == {io:C(c0). B(b,fst(io))=1} Un 
diff -r 2c8a8be36c94 -r f2e0938ba38d src/ZF/IMP/Equiv.ML
--- a/src/ZF/IMP/Equiv.ML	Mon Dec 28 16:54:01 1998 +0100
+++ b/src/ZF/IMP/Equiv.ML	Mon Dec 28 16:54:53 1998 +0100
@@ -49,7 +49,7 @@
 by (Fast_tac 1);
 (* assign *)
 by (asm_full_simp_tac (simpset() addsimps 
-		       [aexp1, assign_type] @ op_type_intrs) 1);
+		       [aexp1, update_type] @ op_type_intrs) 1);
 (* comp *)
 by (Fast_tac 1);
 (* while *)