--- 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]}"
--- 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);
--- 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
--- 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";