# HG changeset patch
# User nipkow
# Date 830623651 -7200
# Node ID e84bff5c519b348887c6b2db05aa8f8999122622
# Parent  0f9b9eda2a2c1ba98dfc28dd6154dbea2f03003c
A completely new version of IMP.

diff -r 0f9b9eda2a2c -r e84bff5c519b src/HOL/IMP/Com.ML
--- a/src/HOL/IMP/Com.ML	Sat Apr 27 12:09:21 1996 +0200
+++ b/src/HOL/IMP/Com.ML	Sat Apr 27 18:47:31 1996 +0200
@@ -5,26 +5,3 @@
 *)
 
 open Com;
-
-val evala_elim_cases = map (evala.mk_cases aexp.simps)
-   ["<N(n),sigma> -a-> i", "<X(x),sigma> -a-> i",
-    "<Op1 f e,sigma> -a-> i", "<Op2 f a1 a2,sigma>  -a-> i"
-   ];
-
-val evalb_elim_cases = map (evalb.mk_cases bexp.simps)
-   ["<true,sigma> -b-> x", "<false,sigma> -b-> x",
-    "<ROp f a0 a1,sigma> -b-> x", "<noti(b),sigma> -b-> x",
-    "<b0 andi b1,sigma> -b-> x", "<b0 ori b1,sigma> -b-> x"
-   ];
-
-val evalb_simps = map (fn s => prove_goal Com.thy s
-    (fn _ => [fast_tac (HOL_cs addSIs evalb.intrs addSEs evalb_elim_cases) 1]))
-  ["(<true,sigma> -b-> w) = (w=True)",
-   "(<false,sigma> -b-> w) = (w=False)",
-   "(<ROp f a0 a1,sigma> -b-> w) = \
-\   (? m. <a0,sigma> -a-> m & (? n. <a1,sigma> -a-> n & w = f m n))",
-   "(<noti(b),sigma> -b-> w) = (? x. <b,sigma> -b-> x & w = (~x))",
-   "(<b0 andi b1,sigma> -b-> w) = \
-\   (? x. <b0,sigma> -b-> x & (? y. <b1,sigma> -b-> y & w = (x&y)))",
-   "(<b0 ori b1,sigma> -b-> w) = \
-\   (? x. <b0,sigma> -b-> x & (? y. <b1,sigma> -b-> y & w = (x|y)))"];
diff -r 0f9b9eda2a2c -r e84bff5c519b src/HOL/IMP/Com.thy
--- a/src/HOL/IMP/Com.thy	Sat Apr 27 12:09:21 1996 +0200
+++ b/src/HOL/IMP/Com.thy	Sat Apr 27 18:47:31 1996 +0200
@@ -1,112 +1,28 @@
 (*  Title:      HOL/IMP/Com.thy
     ID:         $Id$
-    Author:     Heiko Loetzbeyer & Robert Sandner, TUM
+    Author:     Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
     Copyright   1994 TUM
 
-Arithmetic expressions, Boolean expressions, Commands
-
-And their Operational semantics
+Semantics of arithmetic and boolean expressions
+Syntax of commands
 *)
 
 Com = Arith +
 
-(** Arithmetic expressions **)
-types loc
-      state = "loc => nat"
-      n2n = "nat => nat"
-      n2n2n = "nat => nat => nat"
+types 
+      val
+      loc
+      state = "loc => val"
+      aexp  = "state => val"
+      bexp  = state => bool
 
-arities loc :: term
+arities loc,val :: term
 
 datatype
-  aexp = N nat
-       | X loc
-       | Op1 n2n aexp
-       | Op2 n2n2n aexp aexp
-
-(** Evaluation of arithmetic expressions **)
-consts  evala    :: "(aexp*state*nat)set"
-       "@evala"  :: [aexp,state,nat] => bool ("<_,_>/ -a-> _"  [0,0,50] 50)
-translations
-    "<ae,sig> -a-> n" == "(ae,sig,n) : evala"
-inductive "evala"
-  intrs 
-    N   "<N(n),s> -a-> n"
-    X   "<X(x),s> -a-> s(x)"
-    Op1 "<e,s> -a-> n ==> <Op1 f e,s> -a-> f(n)"
-    Op2 "[| <e0,s> -a-> n0;  <e1,s>  -a-> n1 |] 
-           ==> <Op2 f e0 e1,s> -a-> f n0 n1"
-
-types n2n2b = "[nat,nat] => bool"
-
-(** Boolean expressions **)
-
-datatype
-  bexp = true
-       | false
-       | ROp  n2n2b aexp aexp
-       | noti bexp
-       | andi bexp bexp         (infixl 60)
-       | ori  bexp bexp         (infixl 60)
-
-(** Evaluation of boolean expressions **)
-consts evalb    :: "(bexp*state*bool)set"       
-       "@evalb" :: [bexp,state,bool] => bool ("<_,_>/ -b-> _"  [0,0,50] 50)
-
-translations
-    "<be,sig> -b-> b" == "(be,sig,b) : evalb"
-
-inductive "evalb"
- intrs (*avoid clash with ML constructors true, false*)
-    tru   "<true,s> -b-> True"
-    fls   "<false,s> -b-> False"
-    ROp   "[| <a0,s> -a-> n0; <a1,s> -a-> n1 |] 
-           ==> <ROp f a0 a1,s> -b-> f n0 n1"
-    noti  "<b,s> -b-> w ==> <noti(b),s> -b-> (~w)"
-    andi  "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |] 
-          ==> <b0 andi b1,s> -b-> (w0 & w1)"
-    ori   "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |] 
-            ==> <b0 ori b1,s> -b-> (w0 | w1)"
-
-(** Commands **)
-
-datatype
-  com = Skip
+  com = SKIP
       | ":="  loc aexp         (infixl  60)
       | Semi  com com          ("_; _"  [60, 60] 10)
       | Cond  bexp com com     ("IF _ THEN _ ELSE _"  60)
       | While bexp com         ("WHILE _ DO _"  60)
 
-(** Execution of commands **)
-consts  evalc    :: "(com*state*state)set"
-        "@evalc" :: [com,state,state] => bool ("<_,_>/ -c-> _" [0,0,50] 50)
-        "assign" :: [state,nat,loc] => state  ("_[_'/_]"       [95,0,0] 95)
-
-translations
-       "<ce,sig> -c-> s" == "(ce,sig,s) : evalc"
-
-defs 
-  assign_def   "s[m/x] == (%y. if y=x then m else s y)"
-
-inductive "evalc"
-  intrs
-    skip    "<Skip,s> -c-> s"
-
-    assign  "<a,s> -a-> m ==> <x := a,s> -c-> s[m/x]"
-
-    semi    "[| <c0,s> -c-> s2; <c1,s2> -c-> s1 |] 
-            ==> <c0 ; c1, s> -c-> s1"
-
-    IfTrue "[| <b,s> -b-> True; <c0,s> -c-> s1 |] 
-            ==> <IF b THEN c0 ELSE c1, s> -c-> s1"
-
-    IfFalse "[| <b,s> -b-> False; <c1,s> -c-> s1 |] 
-             ==> <IF b THEN c0 ELSE c1, s> -c-> s1"
-
-    WhileFalse "<b, s> -b-> False ==> <WHILE b DO c,s> -c-> s"
-
-    WhileTrue  "[| <b,s> -b-> True; <c,s> -c-> s2; 
-                  <WHILE b DO c, s2> -c-> s1 |] 
-               ==> <WHILE b DO c, s> -c-> s1"
- 
 end
diff -r 0f9b9eda2a2c -r e84bff5c519b src/HOL/IMP/Denotation.ML
--- a/src/HOL/IMP/Denotation.ML	Sat Apr 27 12:09:21 1996 +0200
+++ b/src/HOL/IMP/Denotation.ML	Sat Apr 27 18:47:31 1996 +0200
@@ -1,28 +1,80 @@
 (*  Title:      HOL/IMP/Denotation.ML
     ID:         $Id$
-    Author:     Heiko Loetzbeyer & Robert Sandner, TUM
+    Author:     Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
     Copyright   1994 TUM
 *)
 
 open Denotation;
 
-(**** Rewrite Rules for A,B,C ****)
+val denotation_cs =  comp_cs addss (!simpset addsimps evalc.intrs);
 
-val B_simps = map (fn t => t RS eq_reflection)
-     [B_true,B_false,B_op,B_not,B_and,B_or]
+
+(**** Rewrite Rules for C ****)
 
 val C_simps = map (fn t => t RS eq_reflection)
   [C_skip,C_assign,C_comp,C_if,C_while]; 
 
+
 (**** mono (Gamma(b,c)) ****)
 
 qed_goalw "Gamma_mono" Denotation.thy [mono_def,Gamma_def]
         "mono (Gamma b c)"
      (fn _ => [(best_tac comp_cs 1)]);
 
-goal Denotation.thy "C(WHILE b DO c) = C(IF b THEN c;WHILE b DO c ELSE Skip)";
+
+goal Denotation.thy "C(WHILE b DO c) = C(IF b THEN c;WHILE b DO c ELSE SKIP)";
 by(Simp_tac 1);
-by(EVERY1[stac (Gamma_mono RS lfp_Tarski),
-          stac (Gamma_def RS meta_eq_to_obj_eq RS fun_cong), rtac refl]);
+by(EVERY[stac (Gamma_mono RS lfp_Tarski) 1,
+          stac (Gamma_def RS meta_eq_to_obj_eq RS fun_cong) 1,
+	  Simp_tac 1,
+	  IF_UNSOLVED no_tac]);
 qed "C_While_If";
 
+
+(* Operational Semantics implies Denotational Semantics *)
+
+goal Denotation.thy "!c s t. <c,s> -c-> t --> (s,t) : C(c)";
+
+(* start with rule induction *)
+by (rtac evalc.mutual_induct 1);
+by (rewrite_tac (Gamma_def::C_simps));
+  (* simplification with HOL_ss too agressive *)
+(* skip *)
+by (fast_tac denotation_cs 1);
+(* assign *)
+by (fast_tac denotation_cs 1);
+(* comp *)
+by (fast_tac denotation_cs 1);
+(* if *)
+by (fast_tac denotation_cs 1);
+by (fast_tac denotation_cs 1);
+(* while *)
+by (rtac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski RS ssubst)) 1);
+by (fast_tac denotation_cs 1);
+by (rtac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski RS ssubst)) 1);
+by (fast_tac denotation_cs 1);
+
+qed_spec_mp "com1";
+
+
+(* Denotational Semantics implies Operational Semantics *)
+
+goal Denotation.thy "!s t. (s,t):C(c) --> <c,s> -c-> t";
+by (com.induct_tac "c" 1);
+by (rewrite_tac C_simps);
+by (ALLGOALS (TRY o fast_tac denotation_cs));
+
+(* while *)
+by (strip_tac 1);
+by (etac (Gamma_mono RSN (2,induct)) 1);
+by (rewtac Gamma_def);  
+by (fast_tac denotation_cs 1);
+
+qed_spec_mp "com2";
+
+
+(**** Proof of Equivalence ****)
+
+goal Denotation.thy "(s,t) : C(c)  =  (<c,s> -c-> t)";
+by (fast_tac (set_cs addEs [com2] addDs [com1]) 1);
+qed "denotational_is_natural";
diff -r 0f9b9eda2a2c -r e84bff5c519b src/HOL/IMP/Denotation.thy
--- a/src/HOL/IMP/Denotation.thy	Sat Apr 27 12:09:21 1996 +0200
+++ b/src/HOL/IMP/Denotation.thy	Sat Apr 27 18:47:31 1996 +0200
@@ -3,44 +3,29 @@
     Author:     Heiko Loetzbeyer & Robert Sandner, TUM
     Copyright   1994 TUM
 
-Denotational semantics of expressions & commands
+Denotational semantics of commands
 *)
 
-Denotation = Com + 
+Denotation = Natural + 
 
 types com_den = "(state*state)set"
-consts
-  A     :: aexp => state => nat
-  B     :: bexp => state => bool
-  C     :: com => com_den
+
+constdefs
   Gamma :: [bexp,com_den] => (com_den => com_den)
-
-primrec A aexp
-  A_nat "A(N(n)) = (%s. n)"
-  A_loc "A(X(x)) = (%s. s(x))" 
-  A_op1 "A(Op1 f a) = (%s. f(A a s))"
-  A_op2 "A(Op2 f a0 a1) = (%s. f (A a0 s) (A a1 s))"
-
-primrec B bexp
-  B_true  "B(true) = (%s. True)"
-  B_false "B(false) = (%s. False)"
-  B_op    "B(ROp f a0 a1) = (%s. f (A a0 s) (A a1 s))" 
-  B_not   "B(noti(b)) = (%s. ~(B b s))"
-  B_and   "B(b0 andi b1) = (%s. (B b0 s) & (B b1 s))"
-  B_or    "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))"
-
-defs
-  Gamma_def     "Gamma b cd ==   
-                   (%phi.{st. st : (phi O cd) & B b (fst st)} Un 
-                         {st. st : id & ~B b (fst st)})"
+           "Gamma b cd == (%phi.{(s,t). (s,t) : (phi O cd) & b(s)} Un 
+                                 {(s,t). (s,t) : id & ~b(s)})"
+    
+consts
+  C     :: com => com_den
 
 primrec C com
-  C_skip    "C(Skip) = id"
-  C_assign  "C(x := a) = {st . snd(st) = fst(st)[A a (fst st)/x]}"
+  C_skip    "C(SKIP) = id"
+  C_assign  "C(x := a) = {(s,t). t = s[a(s)/x]}"
   C_comp    "C(c0 ; c1) = C(c1) O C(c0)"
-  C_if      "C(IF b THEN c0 ELSE c1) =   
-                   {st. st:C(c0) & (B b (fst st))} Un 
-                   {st. st:C(c1) & ~(B b (fst st))}"
+  C_if      "C(IF b THEN c1 ELSE c2) = {(s,t). (s,t) : C(c1) & b(s)} Un
+                                       {(s,t). (s,t) : C(c2) & ~ b(s)}"
   C_while   "C(WHILE b DO c) = lfp (Gamma b (C c))"
 
 end
+
+
diff -r 0f9b9eda2a2c -r e84bff5c519b src/HOL/IMP/Equiv.ML
--- a/src/HOL/IMP/Equiv.ML	Sat Apr 27 12:09:21 1996 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,65 +0,0 @@
-(*  Title:      HOL/IMP/Equiv.ML
-    ID:         $Id$
-    Author:     Heiko Loetzbeyer & Robert Sandner, TUM
-    Copyright   1994 TUM
-*)
-
-goal Equiv.thy "!n. (<a,s> -a-> n) = (n = A a s)";
-by (aexp.induct_tac "a" 1);                               (* struct. ind. *)
-by (ALLGOALS Simp_tac);                                   (* rewr. Den.   *)
-by (TRYALL (fast_tac (set_cs addSIs (evala.intrs@prems)
-                             addSEs evala_elim_cases)));
-qed_spec_mp "aexp_iff";
-
-goal Equiv.thy "!w. (<b,s> -b-> w) = (w = B b s)";
-by (bexp.induct_tac "b" 1);
-by (ALLGOALS(asm_simp_tac (!simpset addcongs [conj_cong]
-                                    addsimps (aexp_iff::evalb_simps))));
-qed_spec_mp "bexp_iff";
-
-val equiv_cs =
- comp_cs addss (simpset_of "Prod" addsimps (aexp_iff::bexp_iff::evalc.intrs));
-
-goal Equiv.thy "!c s t. <c,s> -c-> t --> (s,t) : C(c)";
-
-(* start with rule induction *)
-by (rtac evalc.mutual_induct 1);
-by (rewrite_tac (Gamma_def::C_simps));
-  (* simplification with HOL_ss again too agressive *)
-(* skip *)
-by (fast_tac equiv_cs 1);
-(* assign *)
-by (fast_tac equiv_cs 1);
-(* comp *)
-by (fast_tac equiv_cs 1);
-(* if *)
-by (fast_tac equiv_cs 1);
-by (fast_tac equiv_cs 1);
-(* while *)
-by (rtac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski RS ssubst)) 1);
-by (fast_tac equiv_cs 1);
-by (rtac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski RS ssubst)) 1);
-by (fast_tac equiv_cs 1);
-
-qed_spec_mp "com1";
-
-
-goal Equiv.thy "!s t. (s,t):C(c) --> <c,s> -c-> t";
-by (com.induct_tac "c" 1);
-by (rewrite_tac C_simps);
-by (ALLGOALS (TRY o fast_tac equiv_cs));
-
-(* while *)
-by (strip_tac 1);
-by (etac (Gamma_mono RSN (2,induct)) 1);
-by (rewtac Gamma_def);  
-by (fast_tac equiv_cs 1);
-
-qed_spec_mp "com2";
-
-
-(**** Proof of Equivalence ****)
-
-goal Equiv.thy "(s,t) : C(c)  =  (<c,s> -c-> t)";
-by (fast_tac (set_cs addEs [com2] addDs [com1]) 1);
-qed "com_equivalence";
diff -r 0f9b9eda2a2c -r e84bff5c519b src/HOL/IMP/Equiv.thy
--- a/src/HOL/IMP/Equiv.thy	Sat Apr 27 12:09:21 1996 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,7 +0,0 @@
-(*  Title:      HOL/IMP/Equiv.thy
-    ID:         $Id$
-    Author:     Heiko Loetzbeyer & Robert Sandner, TUM
-    Copyright   1994 TUM
-*)
-
-Equiv = Denotation
diff -r 0f9b9eda2a2c -r e84bff5c519b src/HOL/IMP/Hoare.ML
--- a/src/HOL/IMP/Hoare.ML	Sat Apr 27 12:09:21 1996 +0200
+++ b/src/HOL/IMP/Hoare.ML	Sat Apr 27 18:47:31 1996 +0200
@@ -25,13 +25,13 @@
   by(ALLGOALS Asm_full_simp_tac);
 qed_spec_mp "hoare_sound";
 
-goalw Hoare.thy [swp_def] "swp Skip Q = Q";
+goalw Hoare.thy [swp_def] "swp SKIP Q = Q";
 by(Simp_tac 1);
 br ext 1;
 by(fast_tac HOL_cs 1);
-qed "swp_Skip";
+qed "swp_SKIP";
 
-goalw Hoare.thy [swp_def] "swp (x:=a) Q = (%s.Q(s[A a s/x]))";
+goalw Hoare.thy [swp_def] "swp (x:=a) Q = (%s.Q(s[a s/x]))";
 by(Simp_tac 1);
 br ext 1;
 by(fast_tac HOL_cs 1);
@@ -44,34 +44,29 @@
 qed "swp_Semi";
 
 goalw Hoare.thy [swp_def]
-  "swp (IF b THEN c ELSE d) Q = (%s. (B b s --> swp c Q s) & \
-\                                    (~B b s --> swp d Q s))";
+  "swp (IF b THEN c ELSE d) Q = (%s. (b s --> swp c Q s) & \
+\                                    (~b s --> swp d Q s))";
 by(Simp_tac 1);
 br ext 1;
 by(fast_tac comp_cs 1);
 qed "swp_If";
 
 goalw Hoare.thy [swp_def]
-  "!!s. B b s ==> swp (WHILE b DO c) Q s = swp (c;WHILE b DO c) Q s";
+  "!!s. b s ==> swp (WHILE b DO c) Q s = swp (c;WHILE b DO c) Q s";
 by(stac C_While_If 1);
 by(Asm_simp_tac 1);
 qed "swp_While_True";
 
-goalw Hoare.thy [swp_def] "!!s. ~B b s ==> swp (WHILE b DO c) Q s = Q s";
+goalw Hoare.thy [swp_def] "!!s. ~b s ==> swp (WHILE b DO c) Q s = Q s";
 by(stac C_While_If 1);
 by(Asm_simp_tac 1);
 by(fast_tac HOL_cs 1);
 qed "swp_While_False";
 
-Addsimps [swp_Skip,swp_Ass,swp_Semi,swp_If,swp_While_True,swp_While_False];
+Addsimps [swp_SKIP,swp_Ass,swp_Semi,swp_If,swp_While_True,swp_While_False];
 
 Delsimps [C_while];
 
-goalw Hoare.thy [hoare_valid_def,swp_def]
-  "!!c. |= {P}c{Q} ==> !s. P s --> swp c Q s";
-by(fast_tac HOL_cs 1);
-qed "swp_is_weakest";
-
 goal Hoare.thy "!Q. |- {swp c Q} c {Q}";
 by(com.induct_tac "c" 1);
 by(ALLGOALS Simp_tac);
@@ -88,9 +83,9 @@
   by(fast_tac HOL_cs 2);
  by(fast_tac HOL_cs 1);
 br hoare.conseq 1;
-  br hoare.While 2;
   be thin_rl 1;
   by(fast_tac HOL_cs 1);
+ br hoare.While 1;
  br hoare.conseq 1;
    be thin_rl 3;
    br allI 3;
@@ -107,5 +102,6 @@
 goal Hoare.thy "!!c. |= {P}c{Q} ==> |- {P}c{Q}";
 br (swp_is_pre RSN (2,hoare.conseq)) 1;
  by(fast_tac HOL_cs 2);
-be swp_is_weakest 1;
+by(rewrite_goals_tac [hoare_valid_def,swp_def]);
+by(fast_tac HOL_cs 1);
 qed "hoare_relative_complete";
diff -r 0f9b9eda2a2c -r e84bff5c519b src/HOL/IMP/Hoare.thy
--- a/src/HOL/IMP/Hoare.thy	Sat Apr 27 12:09:21 1996 +0200
+++ b/src/HOL/IMP/Hoare.thy	Sat Apr 27 18:47:31 1996 +0200
@@ -10,28 +10,26 @@
 
 types assn = state => bool
 
-consts
-  hoare :: "(assn * com * assn) set"
-  hoare_valid :: [assn,com,assn] => bool ("|= {(1_)}/ (_)/ {(1_)}" 50)
-defs
-  hoare_valid_def "|= {P}c{Q} == !s t. (s,t) : C(c) --> P s --> Q t"
+constdefs hoare_valid :: [assn,com,assn] => bool ("|= {(1_)}/ (_)/ {(1_)}" 50)
+          "|= {P}c{Q} == !s t. (s,t) : C(c) --> P s --> Q t"
 
-syntax "@hoare" :: [bool,com,bool] => bool ("|- {(1_)}/ (_)/ {(1_)}" 50)
+consts hoare :: "(assn * com * assn) set"
+syntax "@hoare" :: [bool,com,bool] => bool ("|- ({(1_)}/ (_)/ {(1_)})" 50)
 translations "|- {P}c{Q}" == "(P,c,Q) : hoare"
 
 inductive "hoare"
 intrs
-  skip "|- {P}Skip{P}"
-  ass  "|- {%s.P(s[A a s/x])} x:=a {P}"
+  skip "|- {P}SKIP{P}"
+  ass  "|- {%s.P(s[a s/x])} x:=a {P}"
   semi "[| |- {P}c{Q}; |- {Q}d{R} |] ==> |- {P} c;d {R}"
-  If "[| |- {%s. P s & B b s}c{Q}; |- {%s. P s & ~B b s}d{Q} |] ==>
+  If "[| |- {%s. P s & b s}c{Q}; |- {%s. P s & ~b s}d{Q} |] ==>
       |- {P} IF b THEN c ELSE d {Q}"
-  While "|- {%s. P s & B b s} c {P} ==>
-         |- {P} WHILE b DO c {%s. P s & ~B b s}"
+  While "|- {%s. P s & b s} c {P} ==>
+         |- {P} WHILE b DO c {%s. P s & ~b s}"
   conseq "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==>
           |- {P'}c{Q'}"
 
-consts swp :: com => assn => assn
-defs swp_def "swp c Q == (%s. !t. (s,t) : C(c) --> Q t)"
+constdefs swp :: com => assn => assn
+          "swp c Q == (%s. !t. (s,t) : C(c) --> Q t)"
 
 end
diff -r 0f9b9eda2a2c -r e84bff5c519b src/HOL/IMP/Properties.ML
--- a/src/HOL/IMP/Properties.ML	Sat Apr 27 12:09:21 1996 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,41 +0,0 @@
-(*  Title:      HOL/IMP/Properties.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow, TUM
-    Copyright   1994 TUM
-
-IMP is deterministic.
-*)
-
-(* evaluation of aexp is deterministic *)
-goal Com.thy "!m n. <a,s> -a-> m & <a,s> -a-> n --> m=n";
-by(res_inst_tac[("aexp","a")]Com.aexp.induct 1);
-by(REPEAT(fast_tac (HOL_cs addSIs evala.intrs addSEs evala_elim_cases) 1));
-bind_thm("aexp_detD", conjI RS (result() RS spec RS spec RS mp));
-
-(* evaluation of bexp is deterministic *)
-goal Com.thy "!v w. <b,s> -b-> v & <b,s> -b-> w --> v=w";
-by(res_inst_tac[("bexp","b")]Com.bexp.induct 1);
-by(REPEAT(fast_tac (HOL_cs addSIs evalb.intrs addSEs evalb_elim_cases
-                           addDs [aexp_detD]) 1));
-bind_thm("bexp_detD", conjI RS (result() RS spec RS spec RS mp));
-
-
-val evalc_elim_cases = map (evalc.mk_cases com.simps)
-   ["<Skip,s> -c-> t", "<x:=a,s> -c-> t", "<c1;c2, s> -c-> t",
-    "<IF b THEN c1 ELSE c2, s> -c-> t", "<WHILE b DO c,s> -c-> t"];
-
-(* evaluation of com is deterministic *)
-goal Com.thy "!!c. <c,s> -c-> t ==> !u. <c,s> -c-> u --> u=t";
-(* start with rule induction *)
-by (etac (evalc.mutual_induct RS spec RS spec RS spec RSN (2,rev_mp)) 1);
-by(fast_tac (set_cs addSEs evalc_elim_cases) 1);
-by(fast_tac (set_cs addSEs evalc_elim_cases addDs [aexp_detD]) 1);
-by(fast_tac (set_cs addSEs evalc_elim_cases) 1);
-by(fast_tac (set_cs addSEs evalc_elim_cases addDs [bexp_detD]) 1);
-by(fast_tac (set_cs addSEs evalc_elim_cases addDs [bexp_detD]) 1);
-by(EVERY1[strip_tac, eresolve_tac evalc_elim_cases,
-          atac, dtac bexp_detD, atac, etac False_neq_True]);
-by(EVERY1[strip_tac, eresolve_tac evalc_elim_cases,
-          dtac bexp_detD, atac, etac (sym RS False_neq_True),
-          fast_tac HOL_cs]);
-qed "com_det";
diff -r 0f9b9eda2a2c -r e84bff5c519b src/HOL/IMP/Properties.thy
--- a/src/HOL/IMP/Properties.thy	Sat Apr 27 12:09:21 1996 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-Properties = "Com"
diff -r 0f9b9eda2a2c -r e84bff5c519b src/HOL/IMP/README.html
--- a/src/HOL/IMP/README.html	Sat Apr 27 12:09:21 1996 +0200
+++ b/src/HOL/IMP/README.html	Sat Apr 27 18:47:31 1996 +0200
@@ -1,21 +1,18 @@
 <HTML><HEAD><TITLE>HOL/IMP/ReadMe</TITLE></HEAD><BODY>
 
-<H2>IMP --- A <KBD>while</KBD>-language and its 3 Semantics</H2>
+<H2>IMP --- A <KBD>WHILE</KBD>-language and its Semantics</H2>
 
-The formalization of the denotational, operational and axiomatic semantics of
-a simple while-language, including
-<UL>
-<LI> an equivalence proof between denotational and operational semantics and
-<LI> a soundness proof of the Hoare rules w.r.t. the denotational semantics.
-</UL>
-The whole development essentially formalizes/transcribes chapters 2, 5 and 6 of
-<P>
-<KBD>
+The denotational, operational, and axiomatic semantics, a verification
+condition generator, and all the necessary soundness, completeness and
+equivalence proofs. Essentially a formalization of the first 100 pages
+of
+<PRE>
 @book{Winskel, author = {Glynn Winskel},
 title = {The Formal Semantics of Programming Languages},
 publisher = {MIT Press}, year = 1993}
-</KBD>
+</PRE>
 <P>
-In addition, a verification-condition-generator is proved sound and complete
-w.r.t. the Hoare rules.
+An eminently readable description of this theory is found
+<A HREF="http://www4.informatik.tu-muenchen.de/~nipkow/pubs/imp.html">
+here</A>.
 </BODY></HTML>
diff -r 0f9b9eda2a2c -r e84bff5c519b src/HOL/IMP/ROOT.ML
--- a/src/HOL/IMP/ROOT.ML	Sat Apr 27 12:09:21 1996 +0200
+++ b/src/HOL/IMP/ROOT.ML	Sat Apr 27 18:47:31 1996 +0200
@@ -8,6 +8,6 @@
 
 writeln"Root file for HOL/IMP";
 proof_timing := true;
-time_use_thy "Properties";
-time_use_thy "Equiv";
+time_use_thy "Expr";
+time_use_thy "Transition";
 time_use_thy "VC";
diff -r 0f9b9eda2a2c -r e84bff5c519b src/HOL/IMP/VC.thy
--- a/src/HOL/IMP/VC.thy	Sat Apr 27 12:09:21 1996 +0200
+++ b/src/HOL/IMP/VC.thy	Sat Apr 27 18:47:31 1996 +0200
@@ -23,9 +23,9 @@
 
 primrec wp acom
   wp_Askip  "wp Askip Q = Q"
-  wp_Aass   "wp (Aass x a) Q = (%s.Q(s[A a s/x]))"
+  wp_Aass   "wp (Aass x a) Q = (%s.Q(s[a s/x]))"
   wp_Asemi  "wp (Asemi c d) Q = wp c (wp d Q)"
-  wp_Aif    "wp (Aif b c d) Q = (%s. (B b s-->wp c Q s)&(~B b s-->wp d Q s))" 
+  wp_Aif    "wp (Aif b c d) Q = (%s. (b s-->wp c Q s) & (~b s-->wp d Q s))" 
   wp_Awhile "wp (Awhile b I c) Q = I"
 
 primrec vc acom
@@ -33,11 +33,11 @@
   vc_Aass   "vc (Aass x a) Q = (%s.True)"
   vc_Asemi  "vc (Asemi c d) Q = (%s. vc c (wp d Q) s & vc d Q s)"
   vc_Aif    "vc (Aif b c d) Q = (%s. vc c Q s & vc d Q s)" 
-  vc_Awhile "vc (Awhile b I c) Q = (%s. (I s & ~B b s --> Q s) &
-                              (I s & B b s --> wp c I s) & vc c I s)"
+  vc_Awhile "vc (Awhile b I c) Q = (%s. (I s & ~b s --> Q s) &
+                              (I s & b s --> wp c I s) & vc c I s)"
 
 primrec astrip acom
-  astrip_Askip  "astrip Askip = Skip"
+  astrip_Askip  "astrip Askip = SKIP"
   astrip_Aass   "astrip (Aass x a) = (x:=a)"
   astrip_Asemi  "astrip (Asemi c d) = (astrip c;astrip d)"
   astrip_Aif    "astrip (Aif b c d) = (IF b THEN astrip c ELSE astrip d)"
@@ -48,7 +48,7 @@
   vcwp_Askip
   "vcwp Askip Q = (%s.True, Q)"
   vcwp_Aass
-  "vcwp (Aass x a) Q = (%s.True, %s.Q(s[A a s/x]))"
+  "vcwp (Aass x a) Q = (%s.True, %s.Q(s[a s/x]))"
   vcwp_Asemi
   "vcwp (Asemi c d) Q = (let (vcd,wpd) = vcwp d Q;
                             (vcc,wpc) = vcwp c wpd
@@ -57,10 +57,10 @@
   "vcwp (Aif b c d) Q = (let (vcd,wpd) = vcwp d Q;
                             (vcc,wpc) = vcwp c Q
                          in (%s. vcc s & vcd s,
-                             %s.(B b s-->wpc s) & (~B b s-->wpd s)))"
+                             %s.(b s-->wpc s) & (~b s-->wpd s)))"
   vcwp_Awhile
   "vcwp (Awhile b I c) Q = (let (vcc,wpc) = vcwp c I
-                            in (%s. (I s & ~B b s --> Q s) &
-                                    (I s & B b s --> wpc s) & vcc s, I))"
+                            in (%s. (I s & ~b s --> Q s) &
+                                    (I s & b s --> wpc s) & vcc s, I))"
 
 end