# HG changeset patch
# User nipkow
# Date 778343119 -7200
# Node ID 47be9d22a0d69a2ebaf6b702fe68e672ce8e3301
# Parent  41bf53133ba66b55a6d272df225f228758401836
Renamed a few types and vars

diff -r 41bf53133ba6 -r 47be9d22a0d6 IMP/Denotation.thy
--- a/IMP/Denotation.thy	Wed Aug 31 15:15:54 1994 +0200
+++ b/IMP/Denotation.thy	Wed Aug 31 16:25:19 1994 +0200
@@ -1,4 +1,4 @@
-(*  Title: 	ZF/IMP/Denotation.thy
+(*  Title: 	HOL/IMP/Denotation.thy
     ID:         $Id$
     Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
     Copyright   1994 TUM
@@ -9,26 +9,26 @@
 Denotation = Com + 
 
 consts
-  A     :: "aexp => env => nat"
-  B     :: "bexp => env => bool"
-  C     :: "com => (env*env)set"
-  Gamma :: "[bexp,com,(env*env)set] => (env*env)set"
+  A     :: "aexp => state => nat"
+  B     :: "bexp => state => bool"
+  C     :: "com => (state*state)set"
+  Gamma :: "[bexp,com,(state*state)set] => (state*state)set"
 
 rules
-  A_nat_def	"A(N(n)) == (%sigma. n)"
-  A_loc_def	"A(X(x)) == (%sigma. sigma(x))" 
-  A_op1_def	"A(Op1(f,a)) == (%sigma. f(A(a,sigma)))"
-  A_op2_def	"A(Op2(f,a0,a1)) == (%sigma. f(A(a0,sigma),A(a1,sigma)))"
+  A_nat_def	"A(N(n)) == (%s. n)"
+  A_loc_def	"A(X(x)) == (%s. s(x))" 
+  A_op1_def	"A(Op1(f,a)) == (%s. f(A(a,s)))"
+  A_op2_def	"A(Op2(f,a0,a1)) == (%s. f(A(a0,s),A(a1,s)))"
 
 
-  B_true_def	"B(true) == (%sigma. True)"
-  B_false_def	"B(false) == (%sigma. False)"
-  B_op_def	"B(ROp(f,a0,a1)) == (%sigma. f(A(a0,sigma),A(a1,sigma)))" 
+  B_true_def	"B(true) == (%s. True)"
+  B_false_def	"B(false) == (%s. False)"
+  B_op_def	"B(ROp(f,a0,a1)) == (%s. f(A(a0,s),A(a1,s)))" 
 
 
-  B_not_def	"B(noti(b)) == (%sigma. ~B(b,sigma))"
-  B_and_def	"B(b0 andi b1) == (%sigma. B(b0,sigma) & B(b1,sigma))"
-  B_or_def	"B(b0 ori b1) == (%sigma. B(b0,sigma) | B(b1,sigma))"
+  B_not_def	"B(noti(b)) == (%s. ~B(b,s))"
+  B_and_def	"B(b0 andi b1) == (%s. B(b0,s) & B(b1,s))"
+  B_or_def	"B(b0 ori b1) == (%s. B(b0,s) | B(b1,s))"
 
   C_skip_def	"C(skip) == id"
   C_assign_def	"C(x := a) == {io . snd(io) = fst(io)[A(a,fst(io))/x]}"
diff -r 41bf53133ba6 -r 47be9d22a0d6 IMP/Equiv.ML
--- a/IMP/Equiv.ML	Wed Aug 31 15:15:54 1994 +0200
+++ b/IMP/Equiv.ML	Wed Aug 31 16:25:19 1994 +0200
@@ -1,10 +1,10 @@
-(*  Title: 	ZF/IMP/Equiv.ML
+(*  Title: 	HOL/IMP/Equiv.ML
     ID:         $Id$
     Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
     Copyright   1994 TUM
 *)
 
-goal Equiv.thy "(<a,sigma> -a-> n) = (A(a,sigma) = n)";
+goal Equiv.thy "(<a,s> -a-> n) = (A(a,s) = n)";
 by (res_inst_tac [("x","n")] spec 1);                     (* quantify n *)
 by (aexp.induct_tac "a" 1);                		  (* struct. ind. *)
 by (rewrite_goals_tac A_rewrite_rules);			  (* rewr. Den.   *)
@@ -16,7 +16,7 @@
 val aexp2 = aexp_iff RS iffD2;
 
 
-goal Equiv.thy "(<b,sigma> -b-> w) = (B(b,sigma) = w)";
+goal Equiv.thy "(<b,s> -b-> w) = (B(b,s) = w)";
 by (res_inst_tac [("x","w")] spec 1);			(* quantify w *)
 by (bexp.induct_tac "b" 1);		                (* struct. ind. *)
 by (rewrite_goals_tac B_rewrite_rules);			(* rewr. Den.   *)
@@ -34,7 +34,7 @@
 val BfstD = read_instantiate_sg (sign_of Equiv.thy)
               [("P","%x.B(?b,x)")] (fst_conv RS subst);
 
-goal Equiv.thy "!!c. <c,sigma> -c-> sigma' ==> <sigma,sigma'> : C(c)";
+goal Equiv.thy "!!c. <c,s> -c-> t ==> <s,t> : C(c)";
 
 (* start with rule induction *)
 be (evalc.mutual_induct RS spec RS spec RS spec RSN (2,rev_mp)) 1;
@@ -60,7 +60,7 @@
 
 val com_cs = comp_cs addSIs [aexp2,bexp2] addIs evalc.intrs;
 
-goal Equiv.thy "!x:C(c). <c,fst(x)> -c-> snd(x)";
+goal Equiv.thy "!io:C(c). <c,fst(io)> -c-> snd(io)";
 by (com.induct_tac "c" 1);
 by (rewrite_tac C_rewrite_rules);
 by (safe_tac com_cs);
diff -r 41bf53133ba6 -r 47be9d22a0d6 IMP/Equiv.thy
--- a/IMP/Equiv.thy	Wed Aug 31 15:15:54 1994 +0200
+++ b/IMP/Equiv.thy	Wed Aug 31 16:25:19 1994 +0200
@@ -1,4 +1,4 @@
-(*  Title: 	ZF/IMP/Equiv.thy
+(*  Title: 	HOL/IMP/Equiv.thy
     ID:         $Id$
     Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
     Copyright   1994 TUM
diff -r 41bf53133ba6 -r 47be9d22a0d6 IMP/ROOT.ML
--- a/IMP/ROOT.ML	Wed Aug 31 15:15:54 1994 +0200
+++ b/IMP/ROOT.ML	Wed Aug 31 16:25:19 1994 +0200
@@ -1,4 +1,4 @@
-(*  Title: 	ZF/IMP/ROOT.ML
+(*  Title: 	HOL/IMP/ROOT.ML
     ID:         $Id$
     Author: 	Heiko Loetzbeyer & Robert Sandner, TUM
     Copyright   1994 TUM
@@ -12,9 +12,9 @@
 
 *)
 
-ZF_build_completed;	(*Make examples fail if ZF did*)
+HOL_build_completed;	(*Make examples fail if HOL did*)
 
-writeln"Root file for ZF/IMP";
+writeln"Root file for HOL/IMP";
 proof_timing := true;
 loadpath := [".","IMP"];
 time_use_thy "Equiv";