--- a/src/HOL/IMP/Com.thy Sun Dec 09 14:35:11 2001 +0100
+++ b/src/HOL/IMP/Com.thy Sun Dec 09 14:35:36 2001 +0100
@@ -1,28 +1,36 @@
-(* Title: HOL/IMP/Com.thy
- ID: $Id$
- Author: Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
- Copyright 1994 TUM
-
-Semantics of arithmetic and boolean expressions
-Syntax of commands
+(* Title: HOL/IMP/Com.thy
+ ID: $Id$
+ Author: Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
+ Isar Version: Gerwin Klein, 2001
+ Copyright 1994 TUM
*)
-Com = Main +
+header "Syntax of Commands"
+
+theory Com = Main:
-types
- loc
- val = nat (* or anything else, nat used in examples *)
- state = loc => val
- aexp = state => val
- bexp = state => bool
-
-arities loc :: type
+typedecl loc
+ -- "an unspecified (arbitrary) type of locations
+ (adresses/names) for variables"
+
+types
+ val = nat -- "or anything else, @{text nat} used in examples"
+ state = "loc \<Rightarrow> val"
+ aexp = "state \<Rightarrow> val"
+ bexp = "state \<Rightarrow> bool"
+ -- "arithmetic and boolean expressions are not modelled explicitly here,"
+ -- "they are just functions on states"
datatype
- 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)
+ com = SKIP
+ | Assign loc aexp ("_ :== _ " 60)
+ | Semi com com ("_; _" [60, 60] 10)
+ | Cond bexp com com ("IF _ THEN _ ELSE _" 60)
+ | While bexp com ("WHILE _ DO _" 60)
+
+syntax (latex)
+ SKIP :: com ("\<SKIP>")
+ Cond :: "bexp \<Rightarrow> com \<Rightarrow> com \<Rightarrow> com" ("\<IF> _ \<THEN> _ \<ELSE> _" 60)
+ While :: "bexp \<Rightarrow> com \<Rightarrow> com" ("\<WHILE> _ \<DO> _" 60)
end
--- a/src/HOL/IMP/Denotation.ML Sun Dec 09 14:35:11 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,60 +0,0 @@
-(* Title: HOL/IMP/Denotation.ML
- ID: $Id$
- Author: Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
- Copyright 1994 TUM
-*)
-
-(**** mono (Gamma(b,c)) ****)
-
-qed_goalw "Gamma_mono" Denotation.thy [mono_def,Gamma_def]
- "mono (Gamma b c)"
- (fn _ => [Fast_tac 1]);
-
-
-Goal "C(WHILE b DO c) = C(IF b THEN c;WHILE b DO c ELSE SKIP)";
-by (Simp_tac 1);
-by (EVERY[stac (Gamma_mono RS lfp_unfold) 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 "<c,s> -c-> t ==> (s,t) : C(c)";
-
-(* start with rule induction *)
-by (etac evalc.induct 1);
-by Auto_tac;
-(* while *)
-by (rewtac Gamma_def);
-by (stac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_unfold)) 1);
-by (Fast_tac 1);
-by (stac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_unfold)) 1);
-by (Fast_tac 1);
-
-qed "com1";
-
-(* Denotational Semantics implies Operational Semantics *)
-
-Goal "!s t. (s,t):C(c) --> <c,s> -c-> t";
-by (induct_tac "c" 1);
-
-by (ALLGOALS Full_simp_tac);
-by (ALLGOALS (TRY o Fast_tac));
-
-(* while *)
-by (strip_tac 1);
-by (etac (Gamma_mono RSN (2,lfp_induct)) 1);
-by (rewtac Gamma_def);
-by (Fast_tac 1);
-
-qed_spec_mp "com2";
-
-
-(**** Proof of Equivalence ****)
-
-Goal "(s,t) : C(c) = (<c,s> -c-> t)";
-by (fast_tac (claset() addEs [com2] addDs [com1]) 1);
-qed "denotational_is_natural";
--- a/src/HOL/IMP/Denotation.thy Sun Dec 09 14:35:11 2001 +0100
+++ b/src/HOL/IMP/Denotation.thy Sun Dec 09 14:35:36 2001 +0100
@@ -2,28 +2,79 @@
ID: $Id$
Author: Heiko Loetzbeyer & Robert Sandner, TUM
Copyright 1994 TUM
-
-Denotational semantics of commands
*)
-Denotation = Natural +
+header "Denotational Semantics of Commands"
-types com_den = "(state*state)set"
+theory Denotation = Natural:
+
+types com_den = "(state\<times>state)set"
constdefs
- Gamma :: [bexp,com_den] => (com_den => com_den)
- "Gamma b cd == (%phi.{(s,t). (s,t) : (phi O cd) & b(s)} Un
- {(s,t). s=t & ~b(s)})"
+ Gamma :: "[bexp,com_den] => (com_den => com_den)"
+ "Gamma b cd == (\<lambda>phi. {(s,t). (s,t) \<in> (phi O cd) \<and> b s} \<union>
+ {(s,t). s=t \<and> \<not>b s})"
consts
- C :: com => com_den
+ C :: "com => com_den"
primrec
- C_skip "C(SKIP) = Id"
- 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)}"
- C_while "C(WHILE b DO c) = lfp (Gamma b (C c))"
+ C_skip: "C \<SKIP> = Id"
+ C_assign: "C (x :== a) = {(s,t). t = s[x\<mapsto>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) \<in> C c1 \<and> b s} \<union>
+ {(s,t). (s,t) \<in> C c2 \<and> \<not>b s}"
+ C_while: "C(\<WHILE> b \<DO> c) = lfp (Gamma b (C c))"
+
+
+(**** mono (Gamma(b,c)) ****)
+
+lemma Gamma_mono: "mono (Gamma b c)"
+ by (unfold Gamma_def mono_def) fast
+
+lemma C_While_If: "C(\<WHILE> b \<DO> c) = C(\<IF> b \<THEN> c;\<WHILE> b \<DO> c \<ELSE> \<SKIP>)"
+apply (simp (no_asm))
+apply (subst lfp_unfold [OF Gamma_mono],
+ subst Gamma_def [THEN meta_eq_to_obj_eq, THEN fun_cong],
+ simp)
+done
+
+(* Operational Semantics implies Denotational Semantics *)
+
+lemma com1: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> (s,t) \<in> C(c)"
+
+(* start with rule induction *)
+apply (erule evalc.induct)
+apply auto
+(* while *)
+apply (unfold Gamma_def)
+apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def])
+apply fast
+apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def])
+apply fast
+done
+
+(* Denotational Semantics implies Operational Semantics *)
+
+lemma com2 [rule_format]: "\<forall>s t. (s,t)\<in>C(c) \<longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
+apply (induct_tac "c")
+
+apply (simp_all (no_asm_use))
+apply fast
+apply fast
+
+(* while *)
+apply (intro strip)
+apply (erule lfp_induct [OF _ Gamma_mono])
+apply (unfold Gamma_def)
+apply fast
+done
+
+
+(**** Proof of Equivalence ****)
+
+lemma denotational_is_natural: "(s,t) \<in> C(c) = (\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t)"
+apply (fast elim: com2 dest: com1)
+done
end
--- a/src/HOL/IMP/Examples.ML Sun Dec 09 14:35:11 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,65 +0,0 @@
-(* Title: HOL/IMP/Examples.ML
- ID: $Id$
- Author: David von Oheimb, TUM
- Copyright 2000 TUM
-*)
-
-Addsimps[update_def];
-
-section "An example due to Tony Hoare";
-
-Goal "[| !x. P x --> Q x; <w,s> -c-> t |] ==> \
-\ !c. w = While P c --> <While Q c,t> -c-> u --> <While Q c,s> -c-> u";
-by (etac evalc.induct 1);
-by (Auto_tac);
-val lemma1 = result() RS spec RS mp RS mp;
-
-Goal "[| !x. P x --> Q x; <w,s> -c-> u |] ==> \
-\ !c. w = While Q c --> <While P c; While Q c,s> -c-> u";
-by (etac evalc.induct 1);
-by (ALLGOALS Asm_simp_tac);
-by (Blast_tac 1);
-by (case_tac "P s" 1);
-by (Auto_tac);
-val lemma2 = result() RS spec RS mp;
-
-Goal "!x. P x --> Q x ==> \
-\ (<While P c; While Q c, s> -c-> t) = (<While Q c, s> -c-> t)";
-by (blast_tac (claset() addIs [lemma1,lemma2]) 1);
-qed "Hoare_example";
-
-
-section "Factorial";
-
-val step = resolve_tac evalc.intrs 1;
-val simp = Asm_simp_tac 1;
-Goalw [factorial_def] "a~=b ==> \
-\ <factorial a b, Mem(a:=3)> -c-> Mem(b:=6, a:=0)";
-by (ftac not_sym 1);
-by step;
-by step;
-by simp;
-by step;
-by simp;
-by step;
-by step;
-by simp;
-by step;
-by simp;
-by step;
-by simp;
-by step;
-by step;
-by simp;
-by step;
-by simp;
-by step;
-by simp;
-by step;
-by step;
-by simp;
-by step;
-by simp;
-by step;
-by simp;
-qed "factorial_3";
--- a/src/HOL/IMP/Examples.thy Sun Dec 09 14:35:11 2001 +0100
+++ b/src/HOL/IMP/Examples.thy Sun Dec 09 14:35:36 2001 +0100
@@ -4,17 +4,83 @@
Copyright 2000 TUM
*)
-Examples = Natural +
+header "Examples"
+
+theory Examples = Natural:
+
+constdefs
+ factorial :: "loc => loc => com"
+ "factorial a b == b :== (%s. 1);
+ \<WHILE> (%s. s a ~= 0) \<DO>
+ (b :== (%s. s b * s a); a :== (%s. s a - 1))"
+
+declare update_def [simp]
+
+subsection "An example due to Tony Hoare"
-defs (* bring up the deferred definition for update *)
+lemma lemma1 [rule_format (no_asm)]:
+ "[| !x. P x \<longrightarrow> Q x; \<langle>w,s\<rangle> \<longrightarrow>\<^sub>c t |] ==>
+ !c. w = While P c \<longrightarrow> \<langle>While Q c,t\<rangle> \<longrightarrow>\<^sub>c u \<longrightarrow> \<langle>While Q c,s\<rangle> \<longrightarrow>\<^sub>c u"
+apply (erule evalc.induct)
+apply auto
+done
+
- update_def "update == fun_upd"
+lemma lemma2 [rule_format (no_asm)]:
+ "[| !x. P x \<longrightarrow> Q x; \<langle>w,s\<rangle> \<longrightarrow>\<^sub>c u |] ==>
+ !c. w = While Q c \<longrightarrow> \<langle>While P c; While Q c,s\<rangle> \<longrightarrow>\<^sub>c u"
+apply (erule evalc.induct)
+apply (simp_all (no_asm_simp))
+apply blast
+apply (case_tac "P s")
+apply auto
+done
+
+
+lemma Hoare_example: "!x. P x \<longrightarrow> Q x ==>
+ (\<langle>While P c; While Q c, s\<rangle> \<longrightarrow>\<^sub>c t) = (\<langle>While Q c, s\<rangle> \<longrightarrow>\<^sub>c t)"
+ by (blast intro: lemma1 lemma2 dest: semi [THEN iffD1])
+
-constdefs
-
- factorial :: loc => loc => com
- "factorial a b == b :== (%s. 1);
- WHILE (%s. s a ~= 0) DO
- (b :== (%s. s b * s a); a :== (%s. s a - 1))"
+subsection "Factorial"
+
+lemma factorial_3: "a~=b ==>
+ \<langle>factorial a b, Mem(a:=3)\<rangle> \<longrightarrow>\<^sub>c Mem(b:=6, a:=0)"
+apply (unfold factorial_def)
+apply simp
+done
+
+text {* the same in single step mode: *}
+lemmas [simp del] = evalc_cases
+lemma "a~=b \<Longrightarrow> \<langle>factorial a b, Mem(a:=3)\<rangle> \<longrightarrow>\<^sub>c Mem(b:=6, a:=0)"
+apply (unfold factorial_def)
+apply (frule not_sym)
+apply (rule evalc.intros)
+apply (rule evalc.intros)
+apply simp
+apply (rule evalc.intros)
+apply simp
+apply (rule evalc.intros)
+apply (rule evalc.intros)
+apply simp
+apply (rule evalc.intros)
+apply simp
+apply (rule evalc.intros)
+apply simp
+apply (rule evalc.intros)
+apply (rule evalc.intros)
+apply simp
+apply (rule evalc.intros)
+apply simp
+apply (rule evalc.intros)
+apply simp
+apply (rule evalc.intros)
+apply (rule evalc.intros)
+apply simp
+apply (rule evalc.intros)
+apply simp
+apply (rule evalc.intros)
+apply simp
+done
end
--- a/src/HOL/IMP/Expr.ML Sun Dec 09 14:35:11 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,48 +0,0 @@
-(* Title: HOL/IMP/Expr.ML
- ID: $Id$
- Author: Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
- Copyright 1994 TUM
-
-Arithmetic expressions and Boolean expressions.
-Not used in the rest of the language, but included for completeness.
-*)
-
-val evala_elim_cases =
- map evala.mk_cases
- ["(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
- ["(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 Expr.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)))"];
-
-Goal "!n. ((a,s) -a-> n) = (A a s = n)";
-by (induct_tac "a" 1);
-by (auto_tac (claset() addSIs evala.intrs addSEs evala_elim_cases,
- simpset()));
-qed_spec_mp "aexp_iff";
-
-Goal "!w. ((b,s) -b-> w) = (B b s = w)";
-by (induct_tac "b" 1);
-by (auto_tac (claset(),
- simpset() addsimps aexp_iff::evalb_simps));
-qed_spec_mp "bexp_iff";
--- a/src/HOL/IMP/Expr.thy Sun Dec 09 14:35:11 2001 +0100
+++ b/src/HOL/IMP/Expr.thy Sun Dec 09 14:35:36 2001 +0100
@@ -2,20 +2,24 @@
ID: $Id$
Author: Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
Copyright 1994 TUM
-
-Arithmetic expressions and Boolean expressions.
-Not used in the rest of the language, but included for completeness.
*)
-Expr = Datatype +
+header "Expressions"
+
+theory Expr = Datatype:
-(** Arithmetic expressions **)
-types loc
- state = "loc => nat"
- n2n = "nat => nat"
- n2n2n = "nat => nat => nat"
+text {*
+ Arithmetic expressions and Boolean expressions.
+ Not used in the rest of the language, but included for completeness.
+*}
-arities loc :: type
+subsection "Arithmetic expressions"
+typedecl loc
+
+types
+ state = "loc => nat"
+ n2n = "nat => nat"
+ n2n2n = "nat => nat => nat"
datatype
aexp = N nat
@@ -23,22 +27,24 @@
| Op1 n2n aexp
| Op2 n2n2n aexp aexp
-(** Evaluation of arithmetic expressions **)
+subsection "Evaluation of arithmetic expressions"
consts evala :: "((aexp*state) * nat) set"
"-a->" :: "[aexp*state,nat] => bool" (infixl 50)
translations
"aesig -a-> n" == "(aesig,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"
+ intros
+ 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"
+
+lemmas [intro] = N X Op1 Op2
types n2n2b = "[nat,nat] => bool"
-(** Boolean expressions **)
+subsection "Boolean expressions"
datatype
bexp = true
@@ -48,7 +54,7 @@
| andi bexp bexp (infixl 60)
| ori bexp bexp (infixl 60)
-(** Evaluation of boolean expressions **)
+subsection "Evaluation of boolean expressions"
consts evalb :: "((bexp*state) * bool)set"
"-b->" :: "[bexp*state,bool] => bool" (infixl 50)
@@ -56,21 +62,24 @@
"besig -b-> b" == "(besig,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 |]
+ -- "avoid clash with ML constructors true, false"
+ intros
+ 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)"
+ ori: "[| (b0,s) -b-> w0; (b1,s) -b-> w1 |]
+ ==> (b0 ori b1,s) -b-> (w0 | w1)"
+
+lemmas [intro] = tru fls ROp noti andi ori
-(** Denotational semantics of arithemtic and boolean expressions **)
+subsection "Denotational semantics of arithmetic and boolean expressions"
consts
- A :: aexp => state => nat
- B :: bexp => state => bool
+ A :: "aexp => state => nat"
+ B :: "bexp => state => bool"
primrec
"A(N(n)) = (%s. n)"
@@ -86,5 +95,59 @@
"B(b0 andi b1) = (%s. (B b0 s) & (B b1 s))"
"B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))"
+lemma [simp]: "(N(n),s) -a-> n' = (n = n')"
+ by (rule,cases set: evala) auto
+
+lemma [simp]: "(X(x),sigma) -a-> i = (i = sigma x)"
+ by (rule,cases set: evala) auto
+
+lemma [simp]:
+ "(Op1 f e,sigma) -a-> i = (\<exists>n. i = f n \<and> (e,sigma) -a-> n)"
+ by (rule,cases set: evala) auto
+
+lemma [simp]:
+ "(Op2 f a1 a2,sigma) -a-> i =
+ (\<exists>n0 n1. i = f n0 n1 \<and> (a1, sigma) -a-> n0 \<and> (a2, sigma) -a-> n1)"
+ by (rule,cases set: evala) auto
+
+lemma [simp]: "((true,sigma) -b-> w) = (w=True)"
+ by (rule,cases set: evalb) auto
+
+lemma [simp]:
+ "((false,sigma) -b-> w) = (w=False)"
+ by (rule,cases set: evalb) auto
+
+lemma [simp]:
+ "((ROp f a0 a1,sigma) -b-> w) =
+ (? m. (a0,sigma) -a-> m & (? n. (a1,sigma) -a-> n & w = f m n))"
+ by (rule,cases set: evalb) auto
+
+lemma [simp]:
+ "((noti(b),sigma) -b-> w) = (? x. (b,sigma) -b-> x & w = (~x))"
+ by (rule,cases set: evalb) auto
+
+lemma [simp]:
+ "((b0 andi b1,sigma) -b-> w) =
+ (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x&y)))"
+ by (rule,cases set: evalb) auto
+
+lemma [simp]:
+ "((b0 ori b1,sigma) -b-> w) =
+ (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x|y)))"
+ by (rule,cases set: evalb) auto
+
+
+lemma aexp_iff [rule_format (no_asm)]:
+ "!n. ((a,s) -a-> n) = (A a s = n)"
+ apply (induct_tac "a")
+ apply auto
+ done
+
+lemma bexp_iff [rule_format (no_asm)]:
+ "!w. ((b,s) -b-> w) = (B b s = w)"
+ apply (induct_tac "b")
+ apply (auto simp add: aexp_iff)
+ done
+
end
--- a/src/HOL/IMP/Hoare.ML Sun Dec 09 14:35:11 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,117 +0,0 @@
-(* Title: HOL/IMP/Hoare.ML
- ID: $Id$
- Author: Tobias Nipkow
- Copyright 1995 TUM
-
-Soundness (and part of) relative completeness of Hoare rules
-wrt denotational semantics
-*)
-
-Goal "[| !s. P' s --> P s; |- {P}c{Q} |] ==> |- {P'}c{Q}";
-by (etac hoare.conseq 1);
-by (atac 1);
-by (Fast_tac 1);
-qed "hoare_conseq1";
-
-Goal "[| |- {P}c{Q}; !s. Q s --> Q' s |] ==> |- {P}c{Q'}";
-by (rtac hoare.conseq 1);
-by (atac 2);
-by (ALLGOALS Fast_tac);
-qed "hoare_conseq2";
-
-Goalw [hoare_valid_def] "|- {P}c{Q} ==> |= {P}c{Q}";
-by (etac hoare.induct 1);
- by (ALLGOALS Asm_simp_tac);
- by (Fast_tac 1);
- by (Fast_tac 1);
-by (EVERY' [rtac allI, rtac allI, rtac impI] 1);
-by (etac lfp_induct2 1);
- by (rtac Gamma_mono 1);
-by (rewtac Gamma_def);
-by (Fast_tac 1);
-qed "hoare_sound";
-
-Goalw [wp_def] "wp SKIP Q = Q";
-by (Simp_tac 1);
-qed "wp_SKIP";
-
-Goalw [wp_def] "wp (x:==a) Q = (%s. Q(s[x::=a s]))";
-by (Simp_tac 1);
-qed "wp_Ass";
-
-Goalw [wp_def] "wp (c;d) Q = wp c (wp d Q)";
-by (Simp_tac 1);
-by (rtac ext 1);
-by (Fast_tac 1);
-qed "wp_Semi";
-
-Goalw [wp_def]
- "wp (IF b THEN c ELSE d) Q = (%s. (b s --> wp c Q s) & (~b s --> wp d Q s))";
-by (Simp_tac 1);
-by (rtac ext 1);
-by (Fast_tac 1);
-qed "wp_If";
-
-Goalw [wp_def]
- "b s ==> wp (WHILE b DO c) Q s = wp (c;WHILE b DO c) Q s";
-by (stac C_While_If 1);
-by (Asm_simp_tac 1);
-qed "wp_While_True";
-
-Goalw [wp_def] "~b s ==> wp (WHILE b DO c) Q s = Q s";
-by (stac C_While_If 1);
-by (Asm_simp_tac 1);
-qed "wp_While_False";
-
-Addsimps [wp_SKIP,wp_Ass,wp_Semi,wp_If,wp_While_True,wp_While_False];
-
-(*Not suitable for rewriting: LOOPS!*)
-Goal "wp (WHILE b DO c) Q s = (if b s then wp (c;WHILE b DO c) Q s else Q s)";
-by (Simp_tac 1);
-qed "wp_While_if";
-
-Goal "wp (WHILE b DO c) Q s = \
-\ (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))";
-by (Simp_tac 1);
-by (rtac iffI 1);
- by (rtac weak_coinduct 1);
- by (etac CollectI 1);
- by Safe_tac;
- by (rotate_tac ~1 1);
- by (Asm_full_simp_tac 1);
- by (rotate_tac ~1 1);
- by (Asm_full_simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [wp_def,Gamma_def]) 1);
-by (strip_tac 1);
-by (rtac mp 1);
- by (assume_tac 2);
-by (etac lfp_induct2 1);
-by (fast_tac (claset() addSIs [monoI]) 1);
-by (stac gfp_unfold 1);
- by (fast_tac (claset() addSIs [monoI]) 1);
-by (Fast_tac 1);
-qed "wp_While";
-
-Delsimps [C_while];
-
-AddSIs [hoare.skip, hoare.ass, hoare.semi, hoare.If];
-
-Goal "!Q. |- {wp c Q} c {Q}";
-by (induct_tac "c" 1);
- by (ALLGOALS Simp_tac);
- by (REPEAT_FIRST Fast_tac);
- by (blast_tac (claset() addIs [hoare_conseq1]) 1);
-by Safe_tac;
-by (rtac hoare_conseq2 1);
- by (rtac hoare.While 1);
- by (rtac hoare_conseq1 1);
- by (Fast_tac 2);
- by (safe_tac HOL_cs);
- by (ALLGOALS (EVERY'[rotate_tac ~1, Asm_full_simp_tac]));
-qed_spec_mp "wp_is_pre";
-
-Goal "|= {P}c{Q} ==> |- {P}c{Q}";
-by (rtac (wp_is_pre RSN (2,hoare_conseq1)) 1);
-by (rewrite_goals_tac [hoare_valid_def,wp_def]);
-by (Fast_tac 1);
-qed "hoare_relative_complete";
--- a/src/HOL/IMP/Hoare.thy Sun Dec 09 14:35:11 2001 +0100
+++ b/src/HOL/IMP/Hoare.thy Sun Dec 09 14:35:36 2001 +0100
@@ -2,34 +2,157 @@
ID: $Id$
Author: Tobias Nipkow
Copyright 1995 TUM
-
-Inductive definition of Hoare logic
*)
-Hoare = Denotation + Inductive +
+header "Inductive Definition of Hoare Logic"
+
+theory Hoare = Denotation:
-types assn = state => bool
+types assn = "state => bool"
-constdefs hoare_valid :: [assn,com,assn] => bool ("|= {(1_)}/ (_)/ {(1_)}" 50)
+constdefs hoare_valid :: "[assn,com,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50)
"|= {P}c{Q} == !s t. (s,t) : C(c) --> P s --> Q t"
consts hoare :: "(assn * com * assn) set"
-syntax "@hoare" :: [bool,com,bool] => bool ("|- ({(1_)}/ (_)/ {(1_)})" 50)
+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[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}"
- 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 |] ==>
+intros
+ skip: "|- {P}\<SKIP>{P}"
+ ass: "|- {%s. P(s[x\<mapsto>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}"
+ 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'}"
-constdefs wp :: com => assn => assn
+constdefs wp :: "com => assn => assn"
"wp c Q == (%s. !t. (s,t) : C(c) --> Q t)"
+(*
+Soundness (and part of) relative completeness of Hoare rules
+wrt denotational semantics
+*)
+
+lemma hoare_conseq1: "[| !s. P' s --> P s; |- {P}c{Q} |] ==> |- {P'}c{Q}"
+apply (erule hoare.conseq)
+apply assumption
+apply fast
+done
+
+lemma hoare_conseq2: "[| |- {P}c{Q}; !s. Q s --> Q' s |] ==> |- {P}c{Q'}"
+apply (rule hoare.conseq)
+prefer 2 apply (assumption)
+apply fast
+apply fast
+done
+
+lemma hoare_sound: "|- {P}c{Q} ==> |= {P}c{Q}"
+apply (unfold hoare_valid_def)
+apply (erule hoare.induct)
+ apply (simp_all (no_asm_simp))
+ apply fast
+ apply fast
+apply (rule allI, rule allI, rule impI)
+apply (erule lfp_induct2)
+ apply (rule Gamma_mono)
+apply (unfold Gamma_def)
+apply fast
+done
+
+lemma wp_SKIP: "wp \<SKIP> Q = Q"
+apply (unfold wp_def)
+apply (simp (no_asm))
+done
+
+lemma wp_Ass: "wp (x:==a) Q = (%s. Q(s[x\<mapsto>a s]))"
+apply (unfold wp_def)
+apply (simp (no_asm))
+done
+
+lemma wp_Semi: "wp (c;d) Q = wp c (wp d Q)"
+apply (unfold wp_def)
+apply (simp (no_asm))
+apply (rule ext)
+apply fast
+done
+
+lemma wp_If:
+ "wp (\<IF> b \<THEN> c \<ELSE> d) Q = (%s. (b s --> wp c Q s) & (~b s --> wp d Q s))"
+apply (unfold wp_def)
+apply (simp (no_asm))
+apply (rule ext)
+apply fast
+done
+
+lemma wp_While_True:
+ "b s ==> wp (\<WHILE> b \<DO> c) Q s = wp (c;\<WHILE> b \<DO> c) Q s"
+apply (unfold wp_def)
+apply (subst C_While_If)
+apply (simp (no_asm_simp))
+done
+
+lemma wp_While_False: "~b s ==> wp (\<WHILE> b \<DO> c) Q s = Q s"
+apply (unfold wp_def)
+apply (subst C_While_If)
+apply (simp (no_asm_simp))
+done
+
+declare wp_SKIP [simp] wp_Ass [simp] wp_Semi [simp] wp_If [simp] wp_While_True [simp] wp_While_False [simp]
+
+(*Not suitable for rewriting: LOOPS!*)
+lemma wp_While_if: "wp (\<WHILE> b \<DO> c) Q s = (if b s then wp (c;\<WHILE> b \<DO> c) Q s else Q s)"
+apply (simp (no_asm))
+done
+
+lemma wp_While: "wp (\<WHILE> b \<DO> c) Q s =
+ (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))"
+apply (simp (no_asm))
+apply (rule iffI)
+ apply (rule weak_coinduct)
+ apply (erule CollectI)
+ apply safe
+ apply (rotate_tac -1)
+ apply simp
+ apply (rotate_tac -1)
+ apply simp
+apply (simp add: wp_def Gamma_def)
+apply (intro strip)
+apply (rule mp)
+ prefer 2 apply (assumption)
+apply (erule lfp_induct2)
+apply (fast intro!: monoI)
+apply (subst gfp_unfold)
+ apply (fast intro!: monoI)
+apply fast
+done
+
+declare C_while [simp del]
+
+declare hoare.skip [intro!] hoare.ass [intro!] hoare.semi [intro!] hoare.If [intro!]
+
+lemma wp_is_pre [rule_format (no_asm)]: "!Q. |- {wp c Q} c {Q}"
+apply (induct_tac "c")
+ apply (simp_all (no_asm))
+ apply fast+
+ apply (blast intro: hoare_conseq1)
+apply safe
+apply (rule hoare_conseq2)
+ apply (rule hoare.While)
+ apply (rule hoare_conseq1)
+ prefer 2 apply (fast)
+ apply safe
+ apply (rotate_tac -1, simp)
+apply (rotate_tac -1, simp)
+done
+
+lemma hoare_relative_complete: "|= {P}c{Q} ==> |- {P}c{Q}"
+apply (rule hoare_conseq1 [OF _ wp_is_pre])
+apply (unfold hoare_valid_def wp_def)
+apply fast
+done
+
end
--- a/src/HOL/IMP/Natural.ML Sun Dec 09 14:35:11 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-(* Title: HOL/IMP/Natural.ML
- ID: $Id$
- Author: Tobias Nipkow & Larry Paulson, TUM
- Copyright 1996 TUM
-*)
-
-open Natural;
-
-AddIs evalc.intrs;
-
-val evalc_elim_cases =
- map evalc.mk_cases
- ["<SKIP,s> -c-> t",
- "<x:==a,s> -c-> t",
- "<c1;c2, s> -c-> t",
- "<IF b THEN c1 ELSE c2, s> -c-> t"];
-
-val evalc_WHILE_case = evalc.mk_cases "<WHILE b DO c,s> -c-> t";
-
-AddSEs evalc_elim_cases;
-
-(* evaluation of com is deterministic *)
-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*)
-by (ALLGOALS (best_tac (claset() addEs [evalc_WHILE_case])));
-qed_spec_mp "com_det";
--- a/src/HOL/IMP/Natural.thy Sun Dec 09 14:35:11 2001 +0100
+++ b/src/HOL/IMP/Natural.thy Sun Dec 09 14:35:36 2001 +0100
@@ -1,45 +1,283 @@
-(* Title: HOL/IMP/Natural.thy
- ID: $Id$
- Author: Tobias Nipkow & Robert Sandner, TUM
- Copyright 1996 TUM
-
-Natural semantics of commands
+(* Title: HOL/IMP/Natural.thy
+ ID: $Id$
+ Author: Tobias Nipkow & Robert Sandner, TUM
+ Isar Version: Gerwin Klein, 2001
+ Copyright 1996 TUM
*)
-Natural = Com + Inductive +
+header "Natural Semantics of Commands"
+
+theory Natural = Com:
+
+subsection "Execution of commands"
-(** Execution of commands **)
-consts evalc :: "(com*state*state)set"
- "@evalc" :: [com,state,state] => bool ("<_,_>/ -c-> _" [0,0,50] 50)
+consts evalc :: "(com \<times> state \<times> state) set"
+ "@evalc" :: "[com,state,state] \<Rightarrow> bool" ("<_,_>/ -c-> _" [0,0,60] 60)
-translations "<ce,sig> -c-> s" == "(ce,sig,s) : evalc"
+syntax (xsymbols)
+ "@evalc" :: "[com,state,state] \<Rightarrow> bool" ("\<langle>_,_\<rangle>/ \<longrightarrow>\<^sub>c _" [0,0,60] 60)
-consts
- update :: "('a => 'b) => 'a => 'b => ('a => 'b)"
- ("_/[_/::=/_]" [900,0,0] 900)
-(* update is NOT defined, only declared!
- Thus the whole theory is independent of its meaning!
- If the definition (update == fun_upd) is included, proofs break.
-*)
+text {*
+ We write @{text "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"} for \emph{Statement @{text c}, started
+ in state @{text s}, terminates in state @{text s'}}. Formally,
+ @{text "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"} is just another form of saying \emph{the tuple
+ @{text "(c,s,s')"} is part of the relation @{text evalc}}:
+*}
+translations "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" == "(c,s,s') \<in> evalc"
+constdefs
+ update :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("_/[_ ::= /_]" [900,0,0] 900)
+ "update == fun_upd"
+
+syntax (xsymbols)
+ update :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("_/[_ \<mapsto> /_]" [900,0,0] 900)
+
+text {*
+ The big-step execution relation @{text evalc} is defined inductively:
+*}
inductive evalc
- intrs
- Skip "<SKIP,s> -c-> s"
+ intros
+ Skip: "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s"
+ Assign: "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c s[x\<mapsto>a s]"
+
+ Semi: "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'' \<Longrightarrow> \<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>c0; c1, s\<rangle> \<longrightarrow>\<^sub>c s'"
+
+ IfTrue: "b s \<Longrightarrow> \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s'"
+ IfFalse: "\<not>b s \<Longrightarrow> \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s'"
+
+ WhileFalse: "\<not>b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c s"
+ WhileTrue: "b s \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'' \<Longrightarrow> \<langle>\<WHILE> b \<DO> c, s''\<rangle> \<longrightarrow>\<^sub>c s'
+ \<Longrightarrow> \<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>c s'"
+
+lemmas evalc.intros [intro] -- "use those rules in automatic proofs"
+
+text {*
+The induction principle induced by this definition looks like this:
+
+@{thm [display] evalc.induct [no_vars]}
+
+
+(@{text "\<And>"} and @{text "\<Longrightarrow>"} are Isabelle's
+ meta symbols for @{text "\<forall>"} and @{text "\<longrightarrow>"})
+*}
+
+
+text {*
+ The rules of @{text evalc} are syntax directed, i.e.~for each
+ syntactic category there is always only one rule applicable. That
+ means we can use the rules in both directions. The proofs for this
+ are all the same: one direction is trivial, the other one is shown
+ by using the @{text evalc} rules backwards:
+*}
+lemma skip:
+ "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s' = (s' = s)"
+ by (rule, erule evalc.elims) auto
+
+lemma assign:
+ "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c s' = (s' = s[x\<mapsto>a s])"
+ by (rule, erule evalc.elims) auto
+
+lemma semi:
+ "\<langle>c0; c1, s\<rangle> \<longrightarrow>\<^sub>c s' = (\<exists>s''. \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'' \<and> \<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>c s')"
+ by (rule, erule evalc.elims) auto
- Assign "<x :== a,s> -c-> s[x::=a s]"
+lemma ifTrue:
+ "b s \<Longrightarrow> \<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'"
+ by (rule, erule evalc.elims) auto
+
+lemma ifFalse:
+ "\<not>b s \<Longrightarrow> \<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s'"
+ by (rule, erule evalc.elims) auto
+
+lemma whileFalse:
+ "\<not> b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c s' = (s' = s)"
+ by (rule, erule evalc.elims) auto
+
+lemma whileTrue:
+ "b s \<Longrightarrow>
+ \<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>c s' =
+ (\<exists>s''. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'' \<and> \<langle>\<WHILE> b \<DO> c, s''\<rangle> \<longrightarrow>\<^sub>c s')"
+ by (rule, erule evalc.elims) auto
+
+text "Again, Isabelle may use these rules in automatic proofs:"
+lemmas evalc_cases [simp] = skip assign ifTrue ifFalse whileFalse semi whileTrue
+
+subsection "Equivalence of statements"
- Semi "[| <c0,s> -c-> s2; <c1,s2> -c-> s1 |]
- ==> <c0 ; c1, s> -c-> s1"
+text {*
+ We call two statements @{text c} and @{text c'} equivalent wrt.~the
+ big-step semantics when \emph{@{text c} started in @{text s} terminates
+ in @{text s'} iff @{text c'} started in the same @{text s} also terminates
+ in the same @{text s'}}. Formally:
+*}
+constdefs
+ equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" ("_ \<sim> _")
+ "c \<sim> c' \<equiv> \<forall>s s'. \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s'"
+
+text {*
+ Proof rules telling Isabelle to unfold the definition
+ if there is something to be proved about equivalent
+ statements: *}
+lemma equivI [intro!]:
+ "(\<And>s s'. \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s') \<Longrightarrow> c \<sim> c'"
+ by (unfold equiv_c_def) blast
+
+lemma equivD1:
+ "c \<sim> c' \<Longrightarrow> \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s'"
+ by (unfold equiv_c_def) blast
+
+lemma equivD2:
+ "c \<sim> c' \<Longrightarrow> \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s'"
+ by (unfold equiv_c_def) blast
- IfTrue "[| b s; <c0,s> -c-> s1 |]
- ==> <IF b THEN c0 ELSE c1, s> -c-> s1"
+text {*
+ As an example, we show that loop unfolding is an equivalence
+ transformation on programs:
+*}
+lemma unfold_while:
+ "(\<WHILE> b \<DO> c) \<sim> (\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>)" (is "?w \<sim> ?if")
+proof -
+ -- "to show the equivalence, we look at the derivation tree for"
+ -- "each side and from that construct a derivation tree for the other side"
+ { fix s s' assume w: "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'"
+ -- "as a first thing we note that, if @{text b} is @{text False} in state @{text s},"
+ -- "then both statements do nothing:"
+ hence "\<not>b s \<Longrightarrow> s = s'" by simp
+ hence "\<not>b s \<Longrightarrow> \<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'" by simp
+ moreover
+ -- "on the other hand, if @{text b} is @{text True} in state @{text s},"
+ -- {* then only the @{text WhileTrue} rule can have been used to derive @{text "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'"} *}
+ { assume b: "b s"
+ with w obtain s'' where
+ "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s''" and "\<langle>?w, s''\<rangle> \<longrightarrow>\<^sub>c s'" by (cases set: evalc) auto
+ -- "now we can build a derivation tree for the @{text \<IF>}"
+ -- "first, the body of the True-branch:"
+ hence "\<langle>c; ?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by (rule Semi)
+ -- "then the whole @{text \<IF>}"
+ with b have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'" by (rule IfTrue)
+ }
+ ultimately
+ -- "both cases together give us what we want:"
+ have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
+ }
+ moreover
+ -- "now the other direction:"
+ { fix s s' assume if: "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'"
+ -- "again, if @{text b} is @{text False} in state @{text s}, then the False-branch"
+ -- "of the @{text \<IF>} is executed, and both statements do nothing:"
+ hence "\<not>b s \<Longrightarrow> s = s'" by simp
+ hence "\<not>b s \<Longrightarrow> \<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by simp
+ moreover
+ -- "on the other hand, if @{text b} is @{text True} in state @{text s},"
+ -- {* then this time only the @{text IfTrue} rule can have be used *}
+ { assume b: "b s"
+ with if have "\<langle>c; ?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by (cases set: evalc) auto
+ -- "and for this, only the Semi-rule is applicable:"
+ then obtain s'' where
+ "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s''" and "\<langle>?w, s''\<rangle> \<longrightarrow>\<^sub>c s'" by (cases set: evalc) auto
+ -- "with this information, we can build a derivation tree for the @{text \<WHILE>}"
+ with b
+ have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by (rule WhileTrue)
+ }
+ ultimately
+ -- "both cases together again give us what we want:"
+ have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
+ }
+ ultimately
+ show ?thesis by blast
+qed
+
+
+subsection "Execution is deterministic"
- IfFalse "[| ~b s; <c1,s> -c-> s1 |]
- ==> <IF b THEN c0 ELSE c1, s> -c-> s1"
+text {*
+The following proof presents all the details:
+*}
+theorem com_det: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<and> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<longrightarrow> u=t"
+proof clarify -- "transform the goal into canonical form"
+ assume "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
+ thus "\<And>u. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u=t"
+ proof (induct set: evalc)
+ fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u"
+ thus "u = s" by simp
+ next
+ fix a s x u assume "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c u"
+ thus "u = s[x \<mapsto> a s]" by simp
+ next
+ fix c0 c1 s s1 s2 u
+ assume IH0: "\<And>u. \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2"
+ assume IH1: "\<And>u. \<langle>c1,s2\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
+
+ assume "\<langle>c0;c1, s\<rangle> \<longrightarrow>\<^sub>c u"
+ then obtain s' where
+ c0: "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'" and
+ c1: "\<langle>c1,s'\<rangle> \<longrightarrow>\<^sub>c u"
+ by auto
+
+ from c0 IH0 have "s'=s2" by blast
+ with c1 IH1 show "u=s1" by blast
+ next
+ fix b c0 c1 s s1 u
+ assume IH: "\<And>u. \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
+
+ assume "b s" and "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>c u"
+ hence "\<langle>c0, s\<rangle> \<longrightarrow>\<^sub>c u" by simp
+ with IH show "u = s1" by blast
+ next
+ fix b c0 c1 s s1 u
+ assume IH: "\<And>u. \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
- WhileFalse "~b s ==> <WHILE b DO c,s> -c-> s"
+ assume "\<not>b s" and "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>c u"
+ hence "\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>c u" by simp
+ with IH show "u = s1" by blast
+ next
+ fix b c s u
+ assume "\<not>b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u"
+ thus "u = s" by simp
+ next
+ fix b c s s1 s2 u
+ assume "IH\<^sub>c": "\<And>u. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2"
+ assume "IH\<^sub>w": "\<And>u. \<langle>\<WHILE> b \<DO> c,s2\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
+
+ assume "b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u"
+ then obtain s' where
+ c: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" and
+ w: "\<langle>\<WHILE> b \<DO> c,s'\<rangle> \<longrightarrow>\<^sub>c u"
+ by auto
+
+ from c "IH\<^sub>c" have "s' = s2" by blast
+ with w "IH\<^sub>w" show "u = s1" by blast
+ qed
+qed
+
- WhileTrue "[| b s; <c,s> -c-> s2; <WHILE b DO c, s2> -c-> s1 |]
- ==> <WHILE b DO c, s> -c-> s1"
+text {*
+ This is the proof as you might present it in a lecture. The remaining
+ cases are simple enough to be proved automatically:
+*}
+theorem "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<and> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<longrightarrow> u=t"
+proof clarify
+ assume "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
+ thus "\<And>u. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u=t"
+ proof (induct set: evalc)
+ -- "the simple @{text \<SKIP>} case for demonstration:"
+ fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u"
+ thus "u = s" by simp
+ next
+ -- "and the only really interesting case, @{text \<WHILE>}:"
+ fix b c s s1 s2 u
+ assume "IH\<^sub>c": "\<And>u. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2"
+ assume "IH\<^sub>w": "\<And>u. \<langle>\<WHILE> b \<DO> c,s2\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
+
+ assume "b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u"
+ then obtain s' where
+ c: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" and
+ w: "\<langle>\<WHILE> b \<DO> c,s'\<rangle> \<longrightarrow>\<^sub>c u"
+ by auto
+
+ from c "IH\<^sub>c" have "s' = s2" by blast
+ with w "IH\<^sub>w" show "u = s1" by blast
+ qed (best dest: evalc_cases [THEN iffD1])+ -- "prove the rest automatically"
+qed
end
--- a/src/HOL/IMP/Transition.ML Sun Dec 09 14:35:11 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,227 +0,0 @@
-(* Title: HOL/IMP/Transition.ML
- ID: $Id$
- Author: Tobias Nipkow & Robert Sandner, TUM
- Copyright 1996 TUM
-
-Equivalence of Natural and Transition semantics
-*)
-
-section "Winskel's Proof";
-
-AddSEs [rel_pow_0_E];
-
-val evalc1_SEs =
- map evalc1.mk_cases
- ["(SKIP,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"];
-
-val evalc1_E = evalc1.mk_cases "(WHILE b DO c,s) -1-> t";
-
-AddSEs evalc1_SEs;
-
-AddIs evalc1.intrs;
-
-Goal "!s t u c d. (c,s) -n-> (SKIP,t) --> (d,t) -*-> (SKIP,u) --> \
-\ (c;d, s) -*-> (SKIP, u)";
-by (induct_tac "n" 1);
- by (fast_tac (claset() addIs [rtrancl_into_rtrancl2])1);
-by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]addSDs [rel_pow_Suc_D2])1);
-qed_spec_mp "lemma1";
-
-Goal "<c,s> -c-> s1 ==> (c,s) -*-> (SKIP,s1)";
-by (etac evalc.induct 1);
-
-(* SKIP *)
-by (rtac rtrancl_refl 1);
-
-(* ASSIGN *)
-by (fast_tac (claset() addSIs [r_into_rtrancl]) 1);
-
-(* SEMI *)
-by (fast_tac (claset() addDs [rtrancl_imp_UN_rel_pow] addIs [lemma1]) 1);
-
-(* IF *)
-by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
-by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
-
-(* WHILE *)
-by (fast_tac (claset() addSIs [r_into_rtrancl]) 1);
-by (fast_tac (claset() addDs [rtrancl_imp_UN_rel_pow]
- addIs [rtrancl_into_rtrancl2,lemma1]) 1);
-
-qed "evalc_impl_evalc1";
-
-
-Goal "(SKIP,s) -m-> (SKIP,t) ==> s = t & m = 0";
-by (etac rel_pow_E2 1);
-by (Asm_full_simp_tac 1);
-by (Fast_tac 1);
-val hlemma = result();
-
-Goal "!c d s u. (c;d,s) -n-> (SKIP,u) --> \
-\ (? t m. (c,s) -*-> (SKIP,t) & (d,t) -m-> (SKIP,u) & m <= n)";
-by (induct_tac "n" 1);
- (* case n = 0 *)
- by (fast_tac (claset() addss simpset()) 1);
-(* induction step *)
-by (fast_tac (claset() addSIs [le_SucI,le_refl]
- addSDs [rel_pow_Suc_D2]
- addSEs [rel_pow_imp_rtrancl,rtrancl_into_rtrancl2]) 1);
-qed_spec_mp "lemma2";
-
-Goal "!s t. (c,s) -*-> (SKIP,t) --> <c,s> -c-> t";
-by (induct_tac "c" 1);
-by (safe_tac (claset() addSDs [rtrancl_imp_UN_rel_pow]));
-
-(* SKIP *)
-by (fast_tac (claset() addSEs [rel_pow_E2]) 1);
-
-(* ASSIGN *)
-by (fast_tac (claset() addSDs [hlemma] addSEs [rel_pow_E2]) 1);
-
-(* SEMI *)
-by (fast_tac (claset() addSDs [lemma2,rel_pow_imp_rtrancl]) 1);
-
-(* IF *)
-by (etac rel_pow_E2 1);
-by (Asm_full_simp_tac 1);
-by (fast_tac (claset() addSDs [rel_pow_imp_rtrancl]) 1);
-
-(* WHILE, induction on the length of the computation *)
-by (eres_inst_tac [("P","?X -n-> ?Y")] rev_mp 1);
-by (res_inst_tac [("x","s")] spec 1);
-by (induct_thm_tac nat_less_induct "n" 1);
-by (strip_tac 1);
-by (etac rel_pow_E2 1);
- by (Asm_full_simp_tac 1);
-by (etac evalc1_E 1);
-
-(* WhileFalse *)
- by (fast_tac (claset() addSDs [hlemma]) 1);
-
-(* WhileTrue *)
-by (fast_tac(claset() addSDs[lemma2,le_imp_less_or_eq,less_Suc_eq RS iffD2])1);
-
-qed_spec_mp "evalc1_impl_evalc";
-
-
-(**** proof of the equivalence of evalc and evalc1 ****)
-
-Goal "((c, s) -*-> (SKIP, t)) = (<c,s> -c-> t)";
-by (fast_tac (HOL_cs addSEs [evalc1_impl_evalc,evalc_impl_evalc1]) 1);
-qed "evalc1_eq_evalc";
-
-
-section "A Proof Without -n->";
-
-Goal "(c1,s1) -*-> (SKIP,s2) ==> \
-\ (c2,s2) -*-> cs3 --> (c1;c2,s1) -*-> cs3";
-by (etac converse_rtrancl_induct2 1);
-by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
-by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
-qed_spec_mp "my_lemma1";
-
-
-Goal "<c,s> -c-> s1 ==> (c,s) -*-> (SKIP,s1)";
-by (etac evalc.induct 1);
-
-(* SKIP *)
-by (rtac rtrancl_refl 1);
-
-(* ASSIGN *)
-by (fast_tac (claset() addSIs [r_into_rtrancl]) 1);
-
-(* SEMI *)
-by (fast_tac (claset() addIs [my_lemma1]) 1);
-
-(* IF *)
-by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
-by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
-
-(* WHILE *)
-by (fast_tac (claset() addSIs [r_into_rtrancl]) 1);
-by (fast_tac (claset() addIs [rtrancl_into_rtrancl2,my_lemma1]) 1);
-
-qed "evalc_impl_evalc1";
-
-(* The opposite direction is based on a Coq proof done by Ranan Fraer and
- Yves Bertot. The following sketch is from an email by Ranan Fraer.
-*)
-(*
-First we've broke it into 2 lemmas:
-
-Lemma 1
-((c,s) --> (SKIP,t)) => (<c,s> -c-> t)
-
-This is a quick one, dealing with the cases skip, assignment
-and while_false.
-
-Lemma 2
-((c,s) -*-> (c',s')) /\ <c',s'> -c'-> t
- =>
-<c,s> -c-> t
-
-This is proved by rule induction on the -*-> relation
-and the induction step makes use of a third lemma:
-
-Lemma 3
-((c,s) --> (c',s')) /\ <c',s'> -c'-> t
- =>
-<c,s> -c-> t
-
-This captures the essence of the proof, as it shows that <c',s'>
-behaves as the continuation of <c,s> with respect to the natural
-semantics.
-The proof of Lemma 3 goes by rule induction on the --> relation,
-dealing with the cases sequence1, sequence2, if_true, if_false and
-while_true. In particular in the case (sequence1) we make use again
-of Lemma 1.
-*)
-
-(*Delsimps [update_apply];*)
-Goal "((c,s) -1-> (c',s')) ==> (!t. <c',s'> -c-> t --> <c,s> -c-> t)";
-by (etac evalc1.induct 1);
-by Auto_tac;
-qed_spec_mp "FB_lemma3";
-(*Addsimps [update_apply];*)
-
-val [major] = goal Transition.thy
- "(c,s) -*-> (c',s') ==> <c',s'> -c-> t --> <c,s> -c-> t";
-by (rtac (major RS rtrancl_induct2) 1);
- by (Fast_tac 1);
-by (fast_tac (claset() addIs [FB_lemma3]) 1);
-qed_spec_mp "FB_lemma2";
-
-Goal "(c,s) -*-> (SKIP,t) ==> <c,s> -c-> t";
-by (fast_tac (claset() addEs [FB_lemma2]) 1);
-qed "evalc1_impl_evalc";
-
-
-section "The proof in Nielson and Nielson";
-
-(* The more precise n=i1+i2+1 is proved by the same script but complicates
- life further down, where i1,i2 < n is needed.
-*)
-Goal "!c1 s. (c1;c2,s) -n-> (SKIP,t) --> \
-\ (? i1 i2 u. (c1,s) -i1-> (SKIP,u) & (c2,u) -i2-> (SKIP,t) & i1<n & i2<n)";
-by (induct_tac "n" 1);
- by (Fast_tac 1);
-by (fast_tac (claset() addSIs [rel_pow_0_I,rel_pow_Suc_I2]
- addSDs [rel_pow_Suc_D2] addss simpset()) 1);
-qed_spec_mp "comp_decomp_lemma";
-
-Goal "!c s t. (c,s) -n-> (SKIP,t) --> <c,s> -c-> t";
-by (induct_thm_tac nat_less_induct "n" 1);
-by (Clarify_tac 1);
-by (etac rel_pow_E2 1);
- by (asm_full_simp_tac (simpset() addsimps evalc.intrs) 1);
-by (case_tac "c" 1);
- by (Fast_tac 1);
- by (Blast_tac 1);
- by (blast_tac (claset() addSDs [rel_pow_Suc_I2 RS comp_decomp_lemma]) 1);
- by (Blast_tac 1);
-by (Blast_tac 1);
-qed_spec_mp "evalc1_impl_evalc";
--- a/src/HOL/IMP/Transition.thy Sun Dec 09 14:35:11 2001 +0100
+++ b/src/HOL/IMP/Transition.thy Sun Dec 09 14:35:36 2001 +0100
@@ -1,45 +1,686 @@
-(* Title: HOL/IMP/Transition.thy
- ID: $Id$
- Author: Tobias Nipkow & Robert Sandner, TUM
- Copyright 1996 TUM
-
-Transition semantics of commands
+(* Title: HOL/IMP/Transition.thy
+ ID: $Id$
+ Author: Tobias Nipkow & Robert Sandner, TUM
+ Isar Version: Gerwin Klein, 2001
+ Copyright 1996 TUM
*)
-Transition = Natural +
+header "Transition Semantics of Commands"
+
+theory Transition = Natural:
+
+subsection "The transition relation"
-consts evalc1 :: "((com*state)*(com*state))set"
+text {*
+ We formalize the transition semantics as in \cite{Nielson}. This
+ makes some of the rules a bit more intuitive, but also requires
+ some more (internal) formal overhead.
+
+ Since configurations that have terminated are written without
+ a statement, the transition relation is not
+ @{typ "((com \<times> state) \<times> (com \<times> state)) set"}
+ but instead:
+*}
+consts evalc1 :: "((com option \<times> state) \<times> (com option \<times> state)) set"
+text {*
+ Some syntactic sugar that we will use to hide the
+ @{text option} part in configurations:
+*}
syntax
- "@evalc1" :: "[(com*state),(com*state)] => bool"
- ("_ -1-> _" [81,81] 100)
- "@evalcn" :: "[(com*state),nat,(com*state)] => bool"
- ("_ -_-> _" [81,81] 100)
- "@evalc*" :: "[(com*state),(com*state)] => bool"
- ("_ -*-> _" [81,81] 100)
+ "@angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("<_,_>")
+ "@angle2" :: "state \<Rightarrow> com option \<times> state" ("<_>")
+
+syntax (xsymbols)
+ "@angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("\<langle>_,_\<rangle>")
+ "@angle2" :: "state \<Rightarrow> com option \<times> state" ("\<langle>_\<rangle>")
+
+translations
+ "\<langle>c,s\<rangle>" == "(Some c, s)"
+ "\<langle>s\<rangle>" == "(None, s)"
+
+text {*
+ More syntactic sugar for the transition relation, and its
+ iteration.
+*}
+syntax
+ "@evalc1" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
+ ("_ -1-> _" [81,81] 100)
+ "@evalcn" :: "[(com option\<times>state),nat,(com option\<times>state)] \<Rightarrow> bool"
+ ("_ -_-> _" [81,81] 100)
+ "@evalc*" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
+ ("_ -*-> _" [81,81] 100)
+
+syntax (xsymbols)
+ "@evalc1" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
+ ("_ \<longrightarrow>\<^sub>1 _" [81,81] 100)
+ "@evalcn" :: "[(com option\<times>state),nat,(com option\<times>state)] \<Rightarrow> bool"
+ ("_ -_\<rightarrow>\<^sub>1 _" [81,81] 100)
+ "@evalc*" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
+ ("_ \<longrightarrow>\<^sub>1\<^sup>* _" [81,81] 100)
translations
- "cs0 -1-> cs1" == "(cs0,cs1) : evalc1"
- "cs0 -1-> (c1,s1)" == "(cs0,c1,s1) : evalc1"
+ "cs \<longrightarrow>\<^sub>1 cs'" == "(cs,cs') \<in> evalc1"
+ "cs -n\<rightarrow>\<^sub>1 cs'" == "(cs,cs') \<in> evalc1^n"
+ "cs \<longrightarrow>\<^sub>1\<^sup>* cs'" == "(cs,cs') \<in> evalc1^*"
+
+ -- {* Isabelle converts @{text "(cs0,(c1,s1))"} to @{term "(cs0,c1,s1)"},
+ so we also include: *}
+ "cs0 \<longrightarrow>\<^sub>1 (c1,s1)" == "(cs0,c1,s1) \<in> evalc1"
+ "cs0 -n\<rightarrow>\<^sub>1 (c1,s1)" == "(cs0,c1,s1) \<in> evalc1^n"
+ "cs0 \<longrightarrow>\<^sub>1\<^sup>* (c1,s1)" == "(cs0,c1,s1) \<in> evalc1^*"
+
+text {*
+ Now, finally, we are set to write down the rules for our small step semantics:
+*}
+inductive evalc1
+ intros
+ Skip: "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s\<rangle>"
+ Assign: "\<langle>x :== a, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s[x \<mapsto> a s]\<rangle>"
+
+ Semi1: "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> \<langle>c0;c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1,s'\<rangle>"
+ Semi2: "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c0',s'\<rangle> \<Longrightarrow> \<langle>c0;c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c0';c1,s'\<rangle>"
+
+ IfTrue: "b s \<Longrightarrow> \<langle>\<IF> b \<THEN> c1 \<ELSE> c2,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1,s\<rangle>"
+ IfFalse: "\<not>b s \<Longrightarrow> \<langle>\<IF> b \<THEN> c1 \<ELSE> c2,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c2,s\<rangle>"
+
+ While: "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>,s\<rangle>"
+
+lemmas [intro] = evalc1.intros -- "again, use these rules in automatic proofs"
+
+(*<*)
+(* fixme: move to Relation_Power.thy *)
+lemma rel_pow_Suc_E2 [elim!]:
+ "[| (x, z) \<in> R ^ Suc n; !!y. [| (x, y) \<in> R; (y, z) \<in> R ^ n |] ==> P |] ==> P"
+ by (drule rel_pow_Suc_D2) blast
+
+lemma rtrancl_imp_rel_pow: "p \<in> R^* \<Longrightarrow> \<exists>n. p \<in> R^n"
+proof -
+ assume "p \<in> R\<^sup>*"
+ moreover obtain x y where p: "p = (x,y)" by (cases p)
+ ultimately have "(x,y) \<in> R\<^sup>*" by hypsubst
+ hence "\<exists>n. (x,y) \<in> R^n"
+ proof induct
+ fix a have "(a,a) \<in> R^0" by simp
+ thus "\<exists>n. (a,a) \<in> R ^ n" ..
+ next
+ fix a b c assume "\<exists>n. (a,b) \<in> R ^ n"
+ then obtain n where "(a,b) \<in> R^n" ..
+ moreover assume "(b,c) \<in> R"
+ ultimately have "(a,c) \<in> R^(Suc n)" by auto
+ thus "\<exists>n. (a,c) \<in> R^n" ..
+ qed
+ with p show ?thesis by hypsubst
+qed
+(*>*)
+text {*
+ As for the big step semantics you can read these rules in a
+ syntax directed way:
+*}
+lemma SKIP_1: "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 y = (y = \<langle>s\<rangle>)"
+ by (rule, cases set: evalc1, auto)
+
+lemma Assign_1: "\<langle>x :== a, s\<rangle> \<longrightarrow>\<^sub>1 y = (y = \<langle>s[x \<mapsto> a s]\<rangle>)"
+ by (rule, cases set: evalc1, auto)
+
+lemma Cond_1:
+ "\<langle>\<IF> b \<THEN> c1 \<ELSE> c2, s\<rangle> \<longrightarrow>\<^sub>1 y = ((b s \<longrightarrow> y = \<langle>c1, s\<rangle>) \<and> (\<not>b s \<longrightarrow> y = \<langle>c2, s\<rangle>))"
+ by (rule, cases set: evalc1, auto)
+
+lemma While_1: "\<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>1 y = (y = \<langle>\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>, s\<rangle>)"
+ by (rule, cases set: evalc1, auto)
+
+lemmas [simp] = SKIP_1 Assign_1 Cond_1 While_1
+
+
+subsection "Examples"
+
+lemma
+ "s x = 0 \<Longrightarrow> \<langle>\<WHILE> \<lambda>s. s x \<noteq> 1 \<DO> x:== \<lambda>s. s x+1, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s[x \<mapsto> 1]\<rangle>"
+ (is "_ \<Longrightarrow> \<langle>?w, _\<rangle> \<longrightarrow>\<^sub>1\<^sup>* _")
+proof -
+ let ?x = "x:== \<lambda>s. s x+1"
+ let ?if = "\<IF> \<lambda>s. s x \<noteq> 1 \<THEN> ?x; ?w \<ELSE> \<SKIP>"
+ assume [simp]: "s x = 0"
+ have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s\<rangle>" ..
+ also have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?x; ?w, s\<rangle>" by simp
+ also have "\<langle>?x; ?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 1]\<rangle>" by (rule Semi1, simp)
+ also have "\<langle>?w, s[x \<mapsto> 1]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s[x \<mapsto> 1]\<rangle>" ..
+ also have "\<langle>?if, s[x \<mapsto> 1]\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<SKIP>, s[x \<mapsto> 1]\<rangle>" by (simp add: update_def)
+ also have "\<langle>\<SKIP>, s[x \<mapsto> 1]\<rangle> \<longrightarrow>\<^sub>1 \<langle>s[x \<mapsto> 1]\<rangle>" ..
+ finally show ?thesis ..
+qed
- "cs0 -n-> cs1" == "(cs0,cs1) : evalc1^n"
- "cs0 -n-> (c1,s1)" == "(cs0,c1,s1) : evalc1^n"
+lemma
+ "s x = 2 \<Longrightarrow> \<langle>\<WHILE> \<lambda>s. s x \<noteq> 1 \<DO> x:== \<lambda>s. s x+1, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* s'"
+ (is "_ \<Longrightarrow> \<langle>?w, _\<rangle> \<longrightarrow>\<^sub>1\<^sup>* s'")
+proof -
+ let ?c = "x:== \<lambda>s. s x+1"
+ let ?if = "\<IF> \<lambda>s. s x \<noteq> 1 \<THEN> ?c; ?w \<ELSE> \<SKIP>"
+ assume [simp]: "s x = 2"
+ note update_def [simp]
+ have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s\<rangle>" ..
+ also have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?c; ?w, s\<rangle>" by simp
+ also have "\<langle>?c; ?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 3]\<rangle>" by (rule Semi1, simp)
+ also have "\<langle>?w, s[x \<mapsto> 3]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s[x \<mapsto> 3]\<rangle>" ..
+ also have "\<langle>?if, s[x \<mapsto> 3]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?c; ?w, s[x \<mapsto> 3]\<rangle>" by simp
+ also have "\<langle>?c; ?w, s[x \<mapsto> 3]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 4]\<rangle>" by (rule Semi1, simp)
+ also have "\<langle>?w, s[x \<mapsto> 4]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s[x \<mapsto> 4]\<rangle>" ..
+ also have "\<langle>?if, s[x \<mapsto> 4]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?c; ?w, s[x \<mapsto> 4]\<rangle>" by simp
+ also have "\<langle>?c; ?w, s[x \<mapsto> 4]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 5]\<rangle>" by (rule Semi1, simp)
+ oops
+
+subsection "Basic properties"
+
+text {*
+ There are no \emph{stuck} programs:
+*}
+lemma no_stuck: "\<exists>y. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1 y"
+proof (induct c)
+ -- "case Semi:"
+ fix c1 c2 assume "\<exists>y. \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1 y"
+ then obtain y where "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1 y" ..
+ then obtain c1' s' where "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'\<rangle> \<or> \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1',s'\<rangle>"
+ by (cases y, cases "fst y", auto)
+ thus "\<exists>s'. \<langle>c1;c2,s\<rangle> \<longrightarrow>\<^sub>1 s'" by auto
+next
+ -- "case If:"
+ fix b c1 c2 assume "\<exists>y. \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1 y" and "\<exists>y. \<langle>c2,s\<rangle> \<longrightarrow>\<^sub>1 y"
+ thus "\<exists>y. \<langle>\<IF> b \<THEN> c1 \<ELSE> c2, s\<rangle> \<longrightarrow>\<^sub>1 y" by (cases "b s") auto
+qed auto -- "the rest is trivial"
+
+text {*
+ If a configuration does not contain a statement, the program
+ has terminated and there is no next configuration:
+*}
+lemma stuck [dest]: "(None, s) \<longrightarrow>\<^sub>1 y \<Longrightarrow> False" by (auto elim: evalc1.elims)
+
+(*<*)
+(* fixme: relpow.simps don't work *)
+lemma rel_pow_0 [simp]: "!!R::('a*'a) set. R^0 = Id" by simp
+lemma rel_pow_Suc_0 [simp]: "!!R::('a*'a) set. R^(Suc 0) = R" by simp
+lemmas [simp del] = relpow.simps
+(*>*)
+
+lemma evalc_None_0 [simp]: "\<langle>s\<rangle> -n\<rightarrow>\<^sub>1 y = (n = 0 \<and> y = \<langle>s\<rangle>)"
+ by (cases n) auto
- "cs0 -*-> cs1" == "(cs0,cs1) : evalc1^*"
- "cs0 -*-> (c1,s1)" == "(cs0,c1,s1) : evalc1^*"
+lemma SKIP_n: "\<langle>\<SKIP>, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> s' = s \<and> n=1"
+ by (cases n) auto
+
+subsection "Equivalence to natural semantics (after Nielson and Nielson)"
+
+text {*
+ We first need two lemmas about semicolon statements:
+ decomposition and composition.
+*}
+lemma semiD:
+ "\<And>c1 c2 s s''. \<langle>c1; c2, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<Longrightarrow>
+ \<exists>i j s'. \<langle>c1, s\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<and> \<langle>c2, s'\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<and> n = i+j"
+ (is "PROP ?P n")
+proof (induct n)
+ show "PROP ?P 0" by simp
+next
+ fix n assume IH: "PROP ?P n"
+ show "PROP ?P (Suc n)"
+ proof -
+ fix c1 c2 s s''
+ assume "\<langle>c1; c2, s\<rangle> -Suc n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>"
+ then obtain y where
+ 1: "\<langle>c1; c2, s\<rangle> \<longrightarrow>\<^sub>1 y" and
+ n: "y -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>"
+ by blast
+
+ from 1
+ show "\<exists>i j s'. \<langle>c1, s\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<and> \<langle>c2, s'\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<and> Suc n = i+j"
+ (is "\<exists>i j s'. ?Q i j s'")
+ proof (cases set: evalc1)
+ case Semi1
+ then obtain s' where
+ "y = \<langle>c2, s'\<rangle>" and "\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'\<rangle>"
+ by auto
+ with 1 n have "?Q 1 n s'" by simp
+ thus ?thesis by blast
+ next
+ case Semi2
+ then obtain c1' s' where
+ y: "y = \<langle>c1'; c2, s'\<rangle>" and
+ c1: "\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1', s'\<rangle>"
+ by auto
+ with n have "\<langle>c1'; c2, s'\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by simp
+ with IH obtain i j s0 where
+ c1': "\<langle>c1',s'\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s0\<rangle>" and
+ c2: "\<langle>c2,s0\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" and
+ i: "n = i+j"
+ by blast
+
+ from c1 c1'
+ have "\<langle>c1,s\<rangle> -(i+1)\<rightarrow>\<^sub>1 \<langle>s0\<rangle>" by (auto simp del: relpow.simps intro: rel_pow_Suc_I2)
+ with c2 i
+ have "?Q (i+1) j s0" by simp
+ thus ?thesis by blast
+ qed auto -- "the remaining cases cannot occur"
+ qed
+qed
-inductive evalc1
- intrs
- Assign "(x :== a,s) -1-> (SKIP,s[x ::= a s])"
+lemma semiI:
+ "\<And>c0 s s''. \<langle>c0,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<Longrightarrow> \<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle> \<Longrightarrow> \<langle>c0; c1, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
+proof (induct n)
+ fix c0 s s'' assume "\<langle>c0,s\<rangle> -(0::nat)\<rightarrow>\<^sub>1 \<langle>s''\<rangle>"
+ hence False by simp
+ thus "?thesis c0 s s''" ..
+next
+ fix c0 s s'' n
+ assume c0: "\<langle>c0,s\<rangle> -Suc n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>"
+ assume c1: "\<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
+ assume IH: "\<And>c0 s s''.
+ \<langle>c0,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<Longrightarrow> \<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle> \<Longrightarrow> \<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
+ from c0 obtain y where
+ 1: "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1 y" and n: "y -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by blast
+ from 1 obtain c0' s0' where
+ "y = \<langle>s0'\<rangle> \<or> y = \<langle>c0', s0'\<rangle>"
+ by (cases y, cases "fst y", auto)
+ moreover
+ { assume y: "y = \<langle>s0'\<rangle>"
+ with n have "s'' = s0'" by simp
+ with y 1 have "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1, s''\<rangle>" by blast
+ with c1 have "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (blast intro: rtrancl_trans)
+ }
+ moreover
+ { assume y: "y = \<langle>c0', s0'\<rangle>"
+ with n have "\<langle>c0', s0'\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by blast
+ with IH c1 have "\<langle>c0'; c1,s0'\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by blast
+ moreover
+ from y 1 have "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c0'; c1,s0'\<rangle>" by blast
+ hence "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c0'; c1,s0'\<rangle>" by blast
+ ultimately
+ have "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (blast intro: rtrancl_trans)
+ }
+ ultimately
+ show "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by blast
+qed
+
+text {*
+ The easy direction of the equivalence proof:
+*}
+lemma evalc_imp_evalc1:
+ "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
+proof -
+ assume "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
+ thus "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
+ proof induct
+ fix s show "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" by auto
+ next
+ fix x a s show "\<langle>x :== a ,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s[x\<mapsto>a s]\<rangle>" by auto
+ next
+ fix c0 c1 s s'' s'
+ assume "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s''\<rangle>"
+ then obtain n where "\<langle>c0,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by (blast dest: rtrancl_imp_rel_pow)
+ moreover
+ assume "\<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
+ ultimately
+ show "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (rule semiI)
+ next
+ fix s::state and b c0 c1 s'
+ assume "b s"
+ hence "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c0,s\<rangle>" by simp
+ also assume "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
+ finally show "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" .
+ next
+ fix s::state and b c0 c1 s'
+ assume "\<not>b s"
+ hence "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1,s\<rangle>" by simp
+ also assume "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
+ finally show "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" .
+ next
+ fix b c and s::state
+ assume b: "\<not>b s"
+ let ?if = "\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>"
+ have "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s\<rangle>" by blast
+ also have "\<langle>?if,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<SKIP>, s\<rangle>" by (simp add: b)
+ also have "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s\<rangle>" by blast
+ finally show "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" ..
+ next
+ fix b c s s'' s'
+ let ?w = "\<WHILE> b \<DO> c"
+ let ?if = "\<IF> b \<THEN> c; ?w \<ELSE> \<SKIP>"
+ assume w: "\<langle>?w,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
+ assume c: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s''\<rangle>"
+ assume b: "b s"
+ have "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s\<rangle>" by blast
+ also have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c; ?w, s\<rangle>" by (simp add: b)
+ also
+ from c obtain n where "\<langle>c,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by (blast dest: rtrancl_imp_rel_pow)
+ with w have "\<langle>c; ?w,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by - (rule semiI)
+ finally show "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" ..
+ qed
+qed
+
+text {*
+ Finally, the equivalence theorem:
+*}
+theorem evalc_equiv_evalc1:
+ "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
+proof
+ assume "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
+ show "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (rule evalc_imp_evalc1)
+next
+ assume "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
+ then obtain n where "\<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by (blast dest: rtrancl_imp_rel_pow)
+ moreover
+ have "\<And>c s s'. \<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
+ proof (induct rule: nat_less_induct)
+ fix n
+ assume IH: "\<forall>m. m < n \<longrightarrow> (\<forall>c s s'. \<langle>c, s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s')"
+ fix c s s'
+ assume c: "\<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle>"
+ then obtain m where n: "n = Suc m" by (cases n) auto
+ with c obtain y where
+ c': "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1 y" and m: "y -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by blast
+ show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
+ proof (cases c)
+ case SKIP
+ with c n show ?thesis by auto
+ next
+ case Assign
+ with c n show ?thesis by auto
+ next
+ fix c1 c2 assume semi: "c = (c1; c2)"
+ with c obtain i j s'' where
+ c1: "\<langle>c1, s\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" and
+ c2: "\<langle>c2, s''\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" and
+ ij: "n = i+j"
+ by (blast dest: semiD)
+ from c1 c2 obtain
+ "0 < i" and "0 < j" by (cases i, auto, cases j, auto)
+ with ij obtain
+ i: "i < n" and j: "j < n" by simp
+ from c1 i IH
+ have "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s''" by blast
+ moreover
+ from c2 j IH
+ have "\<langle>c2,s''\<rangle> \<longrightarrow>\<^sub>c s'" by blast
+ moreover
+ note semi
+ ultimately
+ show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
+ next
+ fix b c1 c2 assume If: "c = \<IF> b \<THEN> c1 \<ELSE> c2"
+ { assume True: "b s = True"
+ with If c n
+ have "\<langle>c1,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by auto
+ with n IH
+ have "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
+ with If True
+ have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by simp
+ }
+ moreover
+ { assume False: "b s = False"
+ with If c n
+ have "\<langle>c2,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by auto
+ with n IH
+ have "\<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
+ with If False
+ have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by simp
+ }
+ ultimately
+ show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by (cases "b s") auto
+ next
+ fix b c' assume w: "c = \<WHILE> b \<DO> c'"
+ with c n
+ have "\<langle>\<IF> b \<THEN> c'; \<WHILE> b \<DO> c' \<ELSE> \<SKIP>,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>"
+ (is "\<langle>?if,_\<rangle> -m\<rightarrow>\<^sub>1 _") by auto
+ with n IH
+ have "\<langle>\<IF> b \<THEN> c'; \<WHILE> b \<DO> c' \<ELSE> \<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
+ moreover note unfold_while [of b c']
+ -- {* @{thm unfold_while [of b c']} *}
+ ultimately
+ have "\<langle>\<WHILE> b \<DO> c',s\<rangle> \<longrightarrow>\<^sub>c s'" by (blast dest: equivD2)
+ with w show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by simp
+ qed
+ qed
+ ultimately
+ show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
+qed
+
+
+subsection "Winskel's Proof"
+
+declare rel_pow_0_E [elim!]
+
+text {*
+ Winskel's small step rules are a bit different \cite{Winskel};
+ we introduce their equivalents as derived rules:
+*}
+lemma whileFalse1 [intro]:
+ "\<not> b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" (is "_ \<Longrightarrow> \<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>")
+proof -
+ assume "\<not>b s"
+ have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle>" ..
+ also have "\<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<SKIP>, s\<rangle>" ..
+ also have "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s\<rangle>" ..
+ finally show "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" ..
+qed
+
+lemma whileTrue1 [intro]:
+ "b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;\<WHILE> b \<DO> c, s\<rangle>"
+ (is "_ \<Longrightarrow> \<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;?w,s\<rangle>")
+proof -
+ assume "b s"
+ have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle>" ..
+ also have "\<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c;?w, s\<rangle>" ..
+ finally show "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;?w,s\<rangle>" ..
+qed
- Semi1 "(SKIP;c,s) -1-> (c,s)"
- Semi2 "(c0,s) -1-> (c2,s1) ==> (c0;c1,s) -1-> (c2;c1,s1)"
+inductive_cases evalc1_SEs:
+ "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>1 t"
+ "\<langle>x:==a,s\<rangle> \<longrightarrow>\<^sub>1 t"
+ "\<langle>c1;c2, s\<rangle> \<longrightarrow>\<^sub>1 t"
+ "\<langle>\<IF> b \<THEN> c1 \<ELSE> c2, s\<rangle> \<longrightarrow>\<^sub>1 t"
+ "\<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>1 t"
+
+inductive_cases evalc1_E: "\<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>1 t"
+
+declare evalc1_SEs [elim!]
+
+lemma evalc_impl_evalc1: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s1 \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s1\<rangle>"
+apply (erule evalc.induct)
+
+-- SKIP
+apply blast
+
+-- ASSIGN
+apply fast
+
+-- SEMI
+apply (fast dest: rtrancl_imp_UN_rel_pow intro: semiI)
+
+-- IF
+apply (fast intro: rtrancl_into_rtrancl2)
+apply (fast intro: rtrancl_into_rtrancl2)
+
+-- WHILE
+apply fast
+apply (fast dest: rtrancl_imp_UN_rel_pow intro: rtrancl_into_rtrancl2 semiI)
+
+done
+
+
+lemma lemma2 [rule_format (no_asm)]:
+ "\<forall>c d s u. \<langle>c;d,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>u\<rangle> \<longrightarrow> (\<exists>t m. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<and> \<langle>d,t\<rangle> -m\<rightarrow>\<^sub>1 \<langle>u\<rangle> \<and> m \<le> n)"
+apply (induct_tac "n")
+ -- "case n = 0"
+ apply fastsimp
+-- "induction step"
+apply (fast intro!: le_SucI le_refl dest!: rel_pow_Suc_D2
+ elim!: rel_pow_imp_rtrancl rtrancl_into_rtrancl2)
+done
+
+lemma evalc1_impl_evalc [rule_format (no_asm)]:
+ "\<forall>s t. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
+apply (induct_tac "c")
+apply (safe dest!: rtrancl_imp_UN_rel_pow)
+
+-- SKIP
+apply (simp add: SKIP_n)
+
+-- ASSIGN
+apply (fastsimp elim: rel_pow_E2)
+
+-- SEMI
+apply (fast dest!: rel_pow_imp_rtrancl lemma2)
+
+-- IF
+apply (erule rel_pow_E2)
+apply simp
+apply (fast dest!: rel_pow_imp_rtrancl)
+
+-- "WHILE, induction on the length of the computation"
+apply (rename_tac b c s t n)
+apply (erule_tac P = "?X -n\<rightarrow>\<^sub>1 ?Y" in rev_mp)
+apply (rule_tac x = "s" in spec)
+apply (induct_tac "n" rule: nat_less_induct)
+apply (intro strip)
+apply (erule rel_pow_E2)
+ apply simp
+apply (erule evalc1_E)
+
+apply simp
+apply (case_tac "b x")
+ -- WhileTrue
+ apply (erule rel_pow_E2)
+ apply simp
+ apply (clarify dest!: lemma2)
+ apply (erule allE, erule allE, erule impE, assumption)
+ apply (erule_tac x=mb in allE, erule impE, fastsimp)
+ apply blast
+-- WhileFalse
+apply (erule rel_pow_E2)
+ apply simp
+apply (simp add: SKIP_n)
+done
+
+
+text {* proof of the equivalence of evalc and evalc1 *}
+lemma evalc1_eq_evalc: "(\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle>) = (\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t)"
+apply (fast elim!: evalc1_impl_evalc evalc_impl_evalc1)
+done
+
+
+subsection "A proof without n"
+
+text {*
+ The inductions are a bit awkward to write in this section,
+ because @{text None} as result statement in the small step
+ semantics doesn't have a direct counterpart in the big step
+ semantics.
- IfTrue "b s ==> (IF b THEN c1 ELSE c2,s) -1-> (c1,s)"
- IfFalse "~b s ==> (IF b THEN c1 ELSE c2,s) -1-> (c2,s)"
+ Winskel's small step rule set (using the @{text "\<SKIP>"} statement
+ to indicate termination) is better suited for this proof.
+*}
+
+lemma my_lemma1 [rule_format (no_asm)]:
+ "\<langle>c1,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s2\<rangle> \<Longrightarrow> \<langle>c2,s2\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3 \<Longrightarrow> \<langle>c1;c2,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
+proof -
+ -- {* The induction rule needs @{text P} to be a function of @{term "Some c1"} *}
+ have "\<langle>c1,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s2\<rangle> \<Longrightarrow> \<langle>c2,s2\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3 \<longrightarrow>
+ \<langle>(\<lambda>c. if c = None then c2 else the c; c2) (Some c1),s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
+ apply (erule converse_rtrancl_induct2)
+ apply simp
+ apply (rename_tac c s')
+ apply simp
+ apply (rule conjI)
+ apply (fast dest: stuck)
+ apply clarify
+ apply (case_tac c)
+ apply (auto intro: rtrancl_into_rtrancl2)
+ done
+ moreover assume "\<langle>c1,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s2\<rangle>" "\<langle>c2,s2\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
+ ultimately show "\<langle>c1;c2,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3" by simp
+qed
+
+lemma evalc_impl_evalc1: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s1 \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s1\<rangle>"
+apply (erule evalc.induct)
+
+-- SKIP
+apply fast
+
+-- ASSIGN
+apply fast
+
+-- SEMI
+apply (fast intro: my_lemma1)
+
+-- IF
+apply (fast intro: rtrancl_into_rtrancl2)
+apply (fast intro: rtrancl_into_rtrancl2)
+
+-- WHILE
+apply fast
+apply (fast intro: rtrancl_into_rtrancl2 my_lemma1)
+
+done
+
+text {*
+ The opposite direction is based on a Coq proof done by Ranan Fraer and
+ Yves Bertot. The following sketch is from an email by Ranan Fraer.
+
+\begin{verbatim}
+First we've broke it into 2 lemmas:
- WhileFalse "~b s ==> (WHILE b DO c,s) -1-> (SKIP,s)"
- WhileTrue "b s ==> (WHILE b DO c,s) -1-> (c;WHILE b DO c,s)"
+Lemma 1
+((c,s) --> (SKIP,t)) => (<c,s> -c-> t)
+
+This is a quick one, dealing with the cases skip, assignment
+and while_false.
+
+Lemma 2
+((c,s) -*-> (c',s')) /\ <c',s'> -c'-> t
+ =>
+<c,s> -c-> t
+
+This is proved by rule induction on the -*-> relation
+and the induction step makes use of a third lemma:
+
+Lemma 3
+((c,s) --> (c',s')) /\ <c',s'> -c'-> t
+ =>
+<c,s> -c-> t
+
+This captures the essence of the proof, as it shows that <c',s'>
+behaves as the continuation of <c,s> with respect to the natural
+semantics.
+The proof of Lemma 3 goes by rule induction on the --> relation,
+dealing with the cases sequence1, sequence2, if_true, if_false and
+while_true. In particular in the case (sequence1) we make use again
+of Lemma 1.
+\end{verbatim}
+*}
+
+inductive_cases evalc1_term_cases: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'\<rangle>"
+
+lemma FB_lemma3 [rule_format]:
+ "(c,s) \<longrightarrow>\<^sub>1 (c',s') \<Longrightarrow> c \<noteq> None \<longrightarrow>
+ (\<forall>t. \<langle>if c'=None then \<SKIP> else the c',s'\<rangle> \<longrightarrow>\<^sub>c t \<longrightarrow> \<langle>the c,s\<rangle> \<longrightarrow>\<^sub>c t)"
+ apply (erule evalc1.induct)
+ apply (auto elim!: evalc1_term_cases equivD2 [OF unfold_while])
+ done
+
+lemma rtrancl_stuck: "\<langle>s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* s' \<Longrightarrow> s' = (None, s)"
+ by (erule rtrancl_induct) (auto dest: stuck)
+
+lemma FB_lemma2 [rule_format]:
+ "(c,s) \<longrightarrow>\<^sub>1\<^sup>* (c',s') \<Longrightarrow> c \<noteq> None \<longrightarrow>
+ \<langle>if c' = None then \<SKIP> else the c',s'\<rangle> \<longrightarrow>\<^sub>c t \<longrightarrow> \<langle>the c,s\<rangle> \<longrightarrow>\<^sub>c t"
+ apply (erule converse_rtrancl_induct2)
+ apply simp
+ apply clarsimp
+ apply (fastsimp elim!: evalc1_term_cases dest: rtrancl_stuck intro: FB_lemma3)
+ done
+
+lemma evalc1_impl_evalc: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
+ apply (fastsimp dest: FB_lemma2)
+ done
end
--- a/src/HOL/IMP/VC.ML Sun Dec 09 14:35:11 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,72 +0,0 @@
-(* Title: HOL/IMP/VC.ML
- ID: $Id$
- Author: Tobias Nipkow
- Copyright 1996 TUM
-
-Soundness and completeness of vc
-*)
-
-AddIs hoare.intrs;
-
-val lemma = prove_goal HOL.thy "!s. P s --> P s" (K[Fast_tac 1]);
-
-Goal "!Q. (!s. vc c Q s) --> |- {awp c Q} astrip c {Q}";
-by (induct_tac "c" 1);
- by (ALLGOALS Simp_tac);
- by (Fast_tac 1);
- by (Fast_tac 1);
- by (Fast_tac 1);
- (* if *)
- by (Deepen_tac 4 1);
-(* while *)
-by (safe_tac HOL_cs);
-by (resolve_tac hoare.intrs 1);
- by (rtac lemma 1);
- by (resolve_tac hoare.intrs 1);
- by (resolve_tac hoare.intrs 1);
- by (ALLGOALS(fast_tac HOL_cs));
-qed "vc_sound";
-
-Goal "!P Q. (!s. P s --> Q s) --> (!s. awp c P s --> awp c Q s)";
-by (induct_tac "c" 1);
- by (ALLGOALS Asm_simp_tac);
-by (EVERY1[rtac allI, rtac allI, rtac impI]);
-by (EVERY1[etac allE, etac allE, etac mp]);
-by (EVERY1[etac allE, etac allE, etac mp, atac]);
-qed_spec_mp "awp_mono";
-
-Goal "!P Q. (!s. P s --> Q s) --> (!s. vc c P s --> vc c Q s)";
-by (induct_tac "c" 1);
- by (ALLGOALS Asm_simp_tac);
-by (safe_tac HOL_cs);
-by (EVERY[etac allE 1,etac allE 1,etac impE 1,etac allE 2,etac mp 2,atac 2]);
-by (fast_tac (HOL_cs addEs [awp_mono]) 1);
-qed_spec_mp "vc_mono";
-
-Goal "|- {P}c{Q} ==> \
-\ (? ac. astrip ac = c & (!s. vc ac Q s) & (!s. P s --> awp ac Q s))";
-by (etac hoare.induct 1);
- by (res_inst_tac [("x","Askip")] exI 1);
- by (Simp_tac 1);
- by (res_inst_tac [("x","Aass x a")] exI 1);
- by (Simp_tac 1);
- by (SELECT_GOAL(safe_tac HOL_cs)1);
- by (res_inst_tac [("x","Asemi ac aca")] exI 1);
- by (Asm_simp_tac 1);
- by (fast_tac (HOL_cs addSEs [awp_mono,vc_mono]) 1);
- by (SELECT_GOAL(safe_tac HOL_cs)1);
- by (res_inst_tac [("x","Aif b ac aca")] exI 1);
- by (Asm_simp_tac 1);
- by (SELECT_GOAL(safe_tac HOL_cs)1);
- by (res_inst_tac [("x","Awhile b P ac")] exI 1);
- by (Asm_simp_tac 1);
-by (safe_tac HOL_cs);
-by (res_inst_tac [("x","ac")] exI 1);
-by (Asm_simp_tac 1);
-by (fast_tac (HOL_cs addSEs [awp_mono,vc_mono]) 1);
-qed "vc_complete";
-
-Goal "!Q. vcawp c Q = (vc c Q, awp c Q)";
-by (induct_tac "c" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [Let_def])));
-qed "vcawp_vc_awp";
--- a/src/HOL/IMP/VC.thy Sun Dec 09 14:35:11 2001 +0100
+++ b/src/HOL/IMP/VC.thy Sun Dec 09 14:35:36 2001 +0100
@@ -8,7 +8,9 @@
awp: weakest (liberal) precondition
*)
-VC = Hoare +
+header "Verification Conditions"
+
+theory VC = Hoare:
datatype acom = Askip
| Aass loc aexp
@@ -17,45 +19,121 @@
| Awhile bexp assn acom
consts
- vc,awp :: acom => assn => assn
- vcawp :: "acom => assn => assn * assn"
- astrip :: acom => com
+ vc :: "acom => assn => assn"
+ awp :: "acom => assn => assn"
+ vcawp :: "acom => assn => assn \<times> assn"
+ astrip :: "acom => com"
primrec
"awp Askip Q = Q"
- "awp (Aass x a) Q = (%s. Q(s[x::=a s]))"
+ "awp (Aass x a) Q = (\<lambda>s. Q(s[x\<mapsto>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 (Aif b c d) Q = (\<lambda>s. (b s-->awp c Q s) & (~b s-->awp d Q s))"
"awp (Awhile b I c) Q = I"
primrec
- "vc Askip Q = (%s. True)"
- "vc (Aass x a) Q = (%s. True)"
- "vc (Asemi c d) Q = (%s. vc c (awp d Q) s & vc d Q s)"
- "vc (Aif b c d) Q = (%s. vc c Q s & vc d Q s)"
- "vc (Awhile b I c) Q = (%s. (I s & ~b s --> Q s) &
+ "vc Askip Q = (\<lambda>s. True)"
+ "vc (Aass x a) Q = (\<lambda>s. True)"
+ "vc (Asemi c d) Q = (\<lambda>s. vc c (awp d Q) s & vc d Q s)"
+ "vc (Aif b c d) Q = (\<lambda>s. vc c Q s & vc d Q s)"
+ "vc (Awhile b I c) Q = (\<lambda>s. (I s & ~b s --> Q s) &
(I s & b s --> awp c I s) & vc c I s)"
primrec
"astrip Askip = SKIP"
"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)"
+ "astrip (Aif b c d) = (\<IF> b \<THEN> astrip c \<ELSE> astrip d)"
+ "astrip (Awhile b I c) = (\<WHILE> b \<DO> astrip c)"
(* 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 Askip Q = (\<lambda>s. True, Q)"
+ "vcawp (Aass x a) Q = (\<lambda>s. True, \<lambda>s. Q(s[x\<mapsto>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))"
+ in (\<lambda>s. vcc s & vcd s, wpc))"
"vcawp (Aif b c d) Q = (let (vcd,wpd) = vcawp d Q;
(vcc,wpc) = vcawp c Q
- in (%s. vcc s & vcd s,
- %s.(b s --> wpc s) & (~b s --> wpd s)))"
+ in (\<lambda>s. vcc s & vcd s,
+ \<lambda>s.(b s --> wpc s) & (~b s --> wpd s)))"
"vcawp (Awhile b I c) Q = (let (vcc,wpc) = vcawp c I
- in (%s. (I s & ~b s --> Q s) &
+ in (\<lambda>s. (I s & ~b s --> Q s) &
(I s & b s --> wpc s) & vcc s, I))"
+(*
+Soundness and completeness of vc
+*)
+
+declare hoare.intros [intro]
+
+lemma l: "!s. P s --> P s" by fast
+
+lemma vc_sound: "!Q. (!s. vc c Q s) --> |- {awp c Q} astrip c {Q}"
+apply (induct_tac "c")
+ apply (simp_all (no_asm))
+ apply fast
+ apply fast
+ apply fast
+ (* if *)
+ apply (tactic "Deepen_tac 4 1")
+(* while *)
+apply (intro allI impI)
+apply (rule conseq)
+ apply (rule l)
+ apply (rule While)
+ defer
+ apply fast
+apply (rule_tac P="awp acom fun2" in conseq)
+ apply fast
+ apply fast
+apply fast
+done
+
+lemma awp_mono [rule_format (no_asm)]: "!P Q. (!s. P s --> Q s) --> (!s. awp c P s --> awp c Q s)"
+apply (induct_tac "c")
+ apply (simp_all (no_asm_simp))
+apply (rule allI, rule allI, rule impI)
+apply (erule allE, erule allE, erule mp)
+apply (erule allE, erule allE, erule mp, assumption)
+done
+
+
+lemma vc_mono [rule_format (no_asm)]: "!P Q. (!s. P s --> Q s) --> (!s. vc c P s --> vc c Q s)"
+apply (induct_tac "c")
+ apply (simp_all (no_asm_simp))
+apply safe
+apply (erule allE,erule allE,erule impE,erule_tac [2] allE,erule_tac [2] mp)
+prefer 2 apply assumption
+apply (fast elim: awp_mono)
+done
+
+lemma vc_complete: "|- {P}c{Q} ==>
+ (? ac. astrip ac = c & (!s. vc ac Q s) & (!s. P s --> awp ac Q s))"
+apply (erule hoare.induct)
+ apply (rule_tac x = "Askip" in exI)
+ apply (simp (no_asm))
+ apply (rule_tac x = "Aass x a" in exI)
+ apply (simp (no_asm))
+ apply clarify
+ apply (rule_tac x = "Asemi ac aca" in exI)
+ apply (simp (no_asm_simp))
+ apply (fast elim!: awp_mono vc_mono)
+ apply clarify
+ apply (rule_tac x = "Aif b ac aca" in exI)
+ apply (simp (no_asm_simp))
+ apply clarify
+ apply (rule_tac x = "Awhile b P ac" in exI)
+ apply (simp (no_asm_simp))
+apply safe
+apply (rule_tac x = "ac" in exI)
+apply (simp (no_asm_simp))
+apply (fast elim!: awp_mono vc_mono)
+done
+
+lemma vcawp_vc_awp: "!Q. vcawp c Q = (vc c Q, awp c Q)"
+apply (induct_tac "c")
+apply (simp_all (no_asm_simp) add: Let_def)
+done
+
end
--- a/src/HOLCF/IMP/Denotational.ML Sun Dec 09 14:35:11 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,51 +0,0 @@
-(* Title: HOLCF/IMP/Denotational.ML
- ID: $Id$
- Author: Tobias Nipkow & Robert Sandner
- Copyright 1996 TUM
-
-Equivalence of Denotational Semantics in HOLCF and Evaluation Semantics in HOL
-*)
-
-Goalw [dlift_def] "dlift f$(Def x) = f$(Discr x)";
-by (Simp_tac 1);
-qed "dlift_Def";
-Addsimps [dlift_Def];
-
-Goalw [dlift_def] "cont(%f. dlift f)";
-by (Simp_tac 1);
-qed "cont_dlift";
-AddIffs [cont_dlift];
-
-Goalw [dlift_def]
- "(dlift f$l = Def y) = (? x. l = Def x & f$(Discr x) = Def y)";
-by (simp_tac (simpset() addsplits [lift.split]) 1);
-qed "dlift_is_Def";
-Addsimps [dlift_is_Def];
-
-Goal "<c,s> -c-> t ==> D c$(Discr s) = (Def t)";
-by (etac evalc.induct 1);
- by (ALLGOALS Asm_simp_tac);
- by (ALLGOALS (stac fix_eq THEN' Asm_full_simp_tac));
-qed_spec_mp "eval_implies_D";
-
-Goal "!s t. D c$(Discr s) = (Def t) --> <c,s> -c-> t";
-by (induct_tac "c" 1);
- by (Force_tac 1);
- by (Force_tac 1);
- by (Force_tac 1);
- by (Simp_tac 1);
- by (Force_tac 1);
-by (Simp_tac 1);
-by (rtac fix_ind 1);
- by (fast_tac (claset() addSIs adm_lemmas @ [adm_chfindom, ax_flat]) 1);
- by (Simp_tac 1);
-by (Simp_tac 1);
-by Safe_tac;
- by (Fast_tac 1);
- by (Force_tac 1);
-qed_spec_mp "D_implies_eval";
-
-
-Goal "(D c$(Discr s) = (Def t)) = (<c,s> -c-> t)";
-by (fast_tac (claset() addSEs [D_implies_eval,eval_implies_D]) 1);
-qed "D_is_eval";
--- a/src/HOLCF/IMP/Denotational.thy Sun Dec 09 14:35:11 2001 +0100
+++ b/src/HOLCF/IMP/Denotational.thy Sun Dec 09 14:35:36 2001 +0100
@@ -2,11 +2,13 @@
ID: $Id$
Author: Tobias Nipkow & Robert Sandner, TUM
Copyright 1996 TUM
-
-Denotational semantics of commands in HOLCF
*)
-Denotational = HOLCF + Natural +
+header "Denotational Semantics of Commands in HOLCF"
+
+theory Denotational = HOLCF + Natural:
+
+subsection "Definition"
constdefs
dlift :: "(('a::type) discr -> 'b::pcpo) => ('a lift -> 'b)"
@@ -15,13 +17,65 @@
consts D :: "com => state discr -> state lift"
primrec
- "D(SKIP) = (LAM s. Def(undiscr s))"
- "D(X :== a) = (LAM s. Def((undiscr s)[X ::= a(undiscr s)]))"
+ "D(\<SKIP>) = (LAM s. Def(undiscr s))"
+ "D(X :== a) = (LAM s. Def((undiscr s)[X \<mapsto> a(undiscr s)]))"
"D(c0 ; c1) = (dlift(D c1) oo (D c0))"
- "D(IF b THEN c1 ELSE c2) =
+ "D(\<IF> b \<THEN> c1 \<ELSE> c2) =
(LAM s. if b(undiscr s) then (D c1)$s else (D c2)$s)"
- "D(WHILE b DO c) =
+ "D(\<WHILE> b \<DO> c) =
fix$(LAM w s. if b(undiscr s) then (dlift w)$((D c)$s)
else Def(undiscr s))"
+subsection
+ "Equivalence of Denotational Semantics in HOLCF and Evaluation Semantics in HOL"
+
+lemma dlift_Def: "dlift f$(Def x) = f$(Discr x)"
+apply (unfold dlift_def)
+apply (simp (no_asm))
+done
+declare dlift_Def [simp]
+
+lemma cont_dlift: "cont(%f. dlift f)"
+apply (unfold dlift_def)
+apply (simp (no_asm))
+done
+declare cont_dlift [iff]
+
+lemma dlift_is_Def:
+ "(dlift f$l = Def y) = (? x. l = Def x & f$(Discr x) = Def y)"
+apply (unfold dlift_def)
+apply (simp (no_asm) split add: lift.split)
+done
+declare dlift_is_Def [simp]
+
+lemma eval_implies_D [rule_format (no_asm)]:
+ "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t ==> D c$(Discr s) = (Def t)"
+apply (erule evalc.induct)
+ apply (simp_all (no_asm_simp))
+ apply (subst fix_eq)
+ apply simp
+apply (subst fix_eq)
+apply simp
+done
+
+lemma D_implies_eval [rule_format (no_asm)]:
+ "!s t. D c$(Discr s) = (Def t) --> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
+apply (induct_tac "c")
+ apply force
+ apply force
+ apply force
+ apply (simp (no_asm))
+ apply force
+apply (simp (no_asm))
+apply (rule fix_ind)
+ apply (fast intro!: adm_lemmas adm_chfindom ax_flat)
+ apply (simp (no_asm))
+apply (simp (no_asm))
+apply safe
+apply fast
+done
+
+lemma D_is_eval: "(D c$(Discr s) = (Def t)) = (\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t)"
+ by (fast elim!: D_implies_eval eval_implies_D)
+
end
--- a/src/HOLCF/IMP/HoareEx.ML Sun Dec 09 14:35:11 2001 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-(* Title: HOLCF/IMP/HoareEx.ML
- ID: $Id$
- Author: Tobias Nipkow
- Copyright 1997 TUM
-
-Correctness of while-loop.
-*)
-
-val prems = goalw thy [hoare_valid_def]
-"|= {A} c {A} ==> |= {A} WHILE b DO c {%s. A s & ~b s}";
-by (cut_facts_tac prems 1);
-by (Simp_tac 1);
-by (rtac fix_ind 1);
- (* simplifier with enhanced adm-tactic: *)
- by (Simp_tac 1);
- by (Simp_tac 1);
-by (Simp_tac 1);
-by (Blast_tac 1);
-qed "WHILE_rule_sound";
--- a/src/HOLCF/IMP/HoareEx.thy Sun Dec 09 14:35:11 2001 +0100
+++ b/src/HOLCF/IMP/HoareEx.thy Sun Dec 09 14:35:36 2001 +0100
@@ -2,17 +2,32 @@
ID: $Id$
Author: Tobias Nipkow, TUM
Copyright 1997 TUM
-
-An example from the HOLCF paper by Mueller, Nipkow, Oheimb, Slotosch.
-It demonstrates fixpoint reasoning by showing the correctness of the Hoare
-rule for while-loops.
*)
-HoareEx = Denotational +
+header "Correctness of Hoare by Fixpoint Reasoning"
+
+theory HoareEx = Denotational:
-types assn = state => bool
+text {*
+ An example from the HOLCF paper by Mueller, Nipkow, Oheimb, Slotosch \cite{MuellerNvOS99}.
+ It demonstrates fixpoint reasoning by showing the correctness of the Hoare
+ rule for while-loops.
+*}
-constdefs hoare_valid :: [assn,com,assn] => bool ("|= {(1_)}/ (_)/ {(1_)}" 50)
+types assn = "state => bool"
+
+constdefs hoare_valid :: "[assn,com,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50)
"|= {A} c {B} == !s t. A s & D c $(Discr s) = Def t --> B t"
+lemma WHILE_rule_sound:
+ "|= {A} c {A} ==> |= {A} \<WHILE> b \<DO> c {%s. A s & ~b s}"
+ apply (unfold hoare_valid_def)
+ apply (simp (no_asm))
+ apply (rule fix_ind)
+ apply (simp (no_asm)) -- "simplifier with enhanced adm-tactic"
+ apply (simp (no_asm))
+ apply (simp (no_asm))
+ apply blast
+ done
+
end