--- a/src/HOL/IMP/Com.thy Tue Jul 04 10:54:32 2000 +0200
+++ b/src/HOL/IMP/Com.thy Tue Jul 04 10:54:46 2000 +0200
@@ -9,18 +9,18 @@
Com = Main +
-types
- val
+types
loc
- state = "loc => val"
- aexp = "state => val"
+ val = nat (* or anything else, nat used in examples *)
+ state = loc => val
+ aexp = state => val
bexp = state => bool
-arities loc,val :: term
+arities loc :: term
datatype
com = SKIP
- | ":=" loc aexp (infixl 60)
+ | ":==" loc aexp (infixl 60)
| Semi com com ("_; _" [60, 60] 10)
| Cond bexp com com ("IF _ THEN _ ELSE _" 60)
| While bexp com ("WHILE _ DO _" 60)
--- a/src/HOL/IMP/Denotation.thy Tue Jul 04 10:54:32 2000 +0200
+++ b/src/HOL/IMP/Denotation.thy Tue Jul 04 10:54:46 2000 +0200
@@ -20,7 +20,7 @@
primrec
C_skip "C(SKIP) = Id"
- C_assign "C(x := a) = {(s,t). t = s[x:=a(s)]}"
+ C_assign "C(x :== a) = {(s,t). t = s[x::=a(s)]}"
C_comp "C(c0 ; c1) = C(c1) O C(c0)"
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)}"
--- a/src/HOL/IMP/Hoare.ML Tue Jul 04 10:54:32 2000 +0200
+++ b/src/HOL/IMP/Hoare.ML Tue Jul 04 10:54:46 2000 +0200
@@ -35,7 +35,7 @@
by (Simp_tac 1);
qed "wp_SKIP";
-Goalw [wp_def] "wp (x:=a) Q = (%s. Q(s[x:=a s]))";
+Goalw [wp_def] "wp (x:==a) Q = (%s. Q(s[x::=a s]))";
by (Simp_tac 1);
qed "wp_Ass";
--- a/src/HOL/IMP/Hoare.thy Tue Jul 04 10:54:32 2000 +0200
+++ b/src/HOL/IMP/Hoare.thy Tue Jul 04 10:54:46 2000 +0200
@@ -20,7 +20,7 @@
inductive hoare
intrs
skip "|- {P}SKIP{P}"
- ass "|- {%s. P(s[x:=a s])} x:=a {P}"
+ ass "|- {%s. P(s[x::=a s])} x:==a {P}"
semi "[| |- {P}c{Q}; |- {Q}d{R} |] ==> |- {P} c;d {R}"
If "[| |- {%s. P s & b s}c{Q}; |- {%s. P s & ~b s}d{Q} |] ==>
|- {P} IF b THEN c ELSE d {Q}"
--- a/src/HOL/IMP/Natural.ML Tue Jul 04 10:54:32 2000 +0200
+++ b/src/HOL/IMP/Natural.ML Tue Jul 04 10:54:46 2000 +0200
@@ -11,7 +11,7 @@
val evalc_elim_cases =
map evalc.mk_cases
["<SKIP,s> -c-> t",
- "<x:=a,s> -c-> t",
+ "<x:==a,s> -c-> t",
"<c1;c2, s> -c-> t",
"<IF b THEN c1 ELSE c2, s> -c-> t"];
@@ -23,7 +23,7 @@
Goal "<c,s> -c-> t ==> (!u. <c,s> -c-> u --> u=t)";
by (etac evalc.induct 1);
by (thin_tac "<?c,s2> -c-> s1" 7);
-(*blast_tac needs Unify.search_bound, trace_bound := 40*)
+(*blast_tac needs Unify.search_bound, trace_bound ::= 40*)
by (ALLGOALS (best_tac (claset() addEs [evalc_WHILE_case])));
qed_spec_mp "com_det";
--- a/src/HOL/IMP/Natural.thy Tue Jul 04 10:54:32 2000 +0200
+++ b/src/HOL/IMP/Natural.thy Tue Jul 04 10:54:46 2000 +0200
@@ -16,17 +16,17 @@
consts
update :: "('a => 'b) => 'a => 'b => ('a => 'b)"
- ("_/[_/:=/_]" [900,0,0] 900)
+ ("_/[_/::=/_]" [900,0,0] 900)
(* update is NOT defined, only declared!
Thus the whole theory is independent of its meaning!
- If theory Update is included, proofs break.
+ If the definition (update == fun_upd) is included, proofs break.
*)
inductive evalc
intrs
Skip "<SKIP,s> -c-> s"
- Assign "<x := a,s> -c-> s[x:=a(s)]"
+ Assign "<x :== a,s> -c-> s[x::=a s]"
Semi "[| <c0,s> -c-> s2; <c1,s2> -c-> s1 |]
==> <c0 ; c1, s> -c-> s1"
--- a/src/HOL/IMP/ROOT.ML Tue Jul 04 10:54:32 2000 +0200
+++ b/src/HOL/IMP/ROOT.ML Tue Jul 04 10:54:46 2000 +0200
@@ -7,3 +7,4 @@
time_use_thy "Expr";
time_use_thy "Transition";
time_use_thy "VC";
+time_use_thy "Examples";
--- a/src/HOL/IMP/Transition.ML Tue Jul 04 10:54:32 2000 +0200
+++ b/src/HOL/IMP/Transition.ML Tue Jul 04 10:54:46 2000 +0200
@@ -13,7 +13,7 @@
val evalc1_SEs =
map evalc1.mk_cases
["(SKIP,s) -1-> t",
- "(x:=a,s) -1-> t",
+ "(x:==a,s) -1-> t",
"(c1;c2, s) -1-> t",
"(IF b THEN c1 ELSE c2, s) -1-> t",
"(WHILE b DO c, s) -1-> t"];
--- a/src/HOL/IMP/Transition.thy Tue Jul 04 10:54:32 2000 +0200
+++ b/src/HOL/IMP/Transition.thy Tue Jul 04 10:54:46 2000 +0200
@@ -31,7 +31,7 @@
inductive evalc1
intrs
- Assign "(x := a,s) -1-> (SKIP,s[x := a s])"
+ Assign "(x :== a,s) -1-> (SKIP,s[x ::= a s])"
Semi1 "(SKIP;c,s) -1-> (c,s)"
Semi2 "(c0,s) -1-> (c2,s1) ==> (c0;c1,s) -1-> (c2;c1,s1)"
--- a/src/HOL/IMP/VC.thy Tue Jul 04 10:54:32 2000 +0200
+++ b/src/HOL/IMP/VC.thy Tue Jul 04 10:54:46 2000 +0200
@@ -23,7 +23,7 @@
primrec
"awp Askip Q = Q"
- "awp (Aass x a) Q = (%s. Q(s[x:=a s]))"
+ "awp (Aass x a) Q = (%s. Q(s[x::=a s]))"
"awp (Asemi c d) Q = awp c (awp d Q)"
"awp (Aif b c d) Q = (%s. (b s-->awp c Q s) & (~b s-->awp d Q s))"
"awp (Awhile b I c) Q = I"
@@ -38,7 +38,7 @@
primrec
"astrip Askip = SKIP"
- "astrip (Aass x a) = (x:=a)"
+ "astrip (Aass x a) = (x:==a)"
"astrip (Asemi c d) = (astrip c;astrip d)"
"astrip (Aif b c d) = (IF b THEN astrip c ELSE astrip d)"
"astrip (Awhile b I c) = (WHILE b DO astrip c)"
@@ -46,7 +46,7 @@
(* simultaneous computation of vc and awp: *)
primrec
"vcawp Askip Q = (%s. True, Q)"
- "vcawp (Aass x a) Q = (%s. True, %s. Q(s[x:=a s]))"
+ "vcawp (Aass x a) Q = (%s. True, %s. Q(s[x::=a s]))"
"vcawp (Asemi c d) Q = (let (vcd,wpd) = vcawp d Q;
(vcc,wpc) = vcawp c wpd
in (%s. vcc s & vcd s, wpc))"
--- a/src/HOL/IsaMakefile Tue Jul 04 10:54:32 2000 +0200
+++ b/src/HOL/IsaMakefile Tue Jul 04 10:54:46 2000 +0200
@@ -151,7 +151,7 @@
$(LOG)/HOL-IMP.gz: $(OUT)/HOL IMP/Com.thy IMP/Denotation.ML \
IMP/Denotation.thy IMP/Expr.ML IMP/Expr.thy IMP/Hoare.ML IMP/Hoare.thy \
- IMP/Natural.ML IMP/Natural.thy IMP/ROOT.ML IMP/Transition.ML \
+ IMP/Natural.ML IMP/Natural.thy IMP/Example.thy IMP/ROOT.ML IMP/Transition.ML \
IMP/Transition.thy IMP/VC.ML IMP/VC.thy
@$(ISATOOL) usedir $(OUT)/HOL IMP