A completely new version of IMP.
--- 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)))"];
--- 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
--- 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";
--- 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
+
+
--- 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";
--- 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
--- 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";
--- 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
--- 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";
--- 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"
--- 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>
--- 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";
--- 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