converted to Isar
authorkleing
Sun Dec 09 14:35:36 2001 +0100 (2001-12-09)
changeset 1243107ec657249e5
parent 12430 bfbd4d8faad7
child 12432 90b0fc84f8d9
converted to Isar
src/HOL/IMP/Com.thy
src/HOL/IMP/Denotation.ML
src/HOL/IMP/Denotation.thy
src/HOL/IMP/Examples.ML
src/HOL/IMP/Examples.thy
src/HOL/IMP/Expr.ML
src/HOL/IMP/Expr.thy
src/HOL/IMP/Hoare.ML
src/HOL/IMP/Hoare.thy
src/HOL/IMP/Natural.ML
src/HOL/IMP/Natural.thy
src/HOL/IMP/Transition.ML
src/HOL/IMP/Transition.thy
src/HOL/IMP/VC.ML
src/HOL/IMP/VC.thy
src/HOLCF/IMP/Denotational.ML
src/HOLCF/IMP/Denotational.thy
src/HOLCF/IMP/HoareEx.ML
src/HOLCF/IMP/HoareEx.thy
     1.1 --- a/src/HOL/IMP/Com.thy	Sun Dec 09 14:35:11 2001 +0100
     1.2 +++ b/src/HOL/IMP/Com.thy	Sun Dec 09 14:35:36 2001 +0100
     1.3 @@ -1,28 +1,36 @@
     1.4 -(*  Title:      HOL/IMP/Com.thy
     1.5 -    ID:         $Id$
     1.6 -    Author:     Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
     1.7 -    Copyright   1994 TUM
     1.8 -
     1.9 -Semantics of arithmetic and boolean expressions
    1.10 -Syntax of commands
    1.11 +(*  Title:        HOL/IMP/Com.thy
    1.12 +    ID:           $Id$
    1.13 +    Author:       Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
    1.14 +    Isar Version: Gerwin Klein, 2001
    1.15 +    Copyright     1994 TUM
    1.16  *)
    1.17  
    1.18 -Com = Main +
    1.19 +header "Syntax of Commands"
    1.20 +
    1.21 +theory Com = Main:
    1.22  
    1.23 -types
    1.24 -      loc
    1.25 -      val   = nat (* or anything else, nat used in examples *)
    1.26 -      state = loc => val
    1.27 -      aexp  = state => val
    1.28 -      bexp  = state => bool
    1.29 -
    1.30 -arities loc :: type
    1.31 +typedecl loc 
    1.32 +  -- "an unspecified (arbitrary) type of locations 
    1.33 +      (adresses/names) for variables"
    1.34 +      
    1.35 +types 
    1.36 +  val   = nat -- "or anything else, @{text nat} used in examples"
    1.37 +  state = "loc \<Rightarrow> val"
    1.38 +  aexp  = "state \<Rightarrow> val"  
    1.39 +  bexp  = "state \<Rightarrow> bool"
    1.40 +  -- "arithmetic and boolean expressions are not modelled explicitly here,"
    1.41 +  -- "they are just functions on states"
    1.42  
    1.43  datatype
    1.44 -  com = SKIP
    1.45 -      | ":=="  loc aexp         (infixl  60)
    1.46 -      | Semi  com com          ("_; _"  [60, 60] 10)
    1.47 -      | Cond  bexp com com     ("IF _ THEN _ ELSE _"  60)
    1.48 -      | While bexp com         ("WHILE _ DO _"  60)
    1.49 +  com = SKIP                    
    1.50 +      | Assign loc aexp         ("_ :== _ " 60)
    1.51 +      | Semi   com com          ("_; _"  [60, 60] 10)
    1.52 +      | Cond   bexp com com     ("IF _ THEN _ ELSE _"  60)
    1.53 +      | While  bexp com         ("WHILE _ DO _"  60)
    1.54 +
    1.55 +syntax (latex)
    1.56 +  SKIP :: com   ("\<SKIP>")
    1.57 +  Cond :: "bexp \<Rightarrow> com \<Rightarrow> com \<Rightarrow> com"  ("\<IF> _ \<THEN> _ \<ELSE> _"  60)
    1.58 +  While :: "bexp \<Rightarrow> com \<Rightarrow> com" ("\<WHILE> _ \<DO> _"  60)
    1.59  
    1.60  end
     2.1 --- a/src/HOL/IMP/Denotation.ML	Sun Dec 09 14:35:11 2001 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,60 +0,0 @@
     2.4 -(*  Title:      HOL/IMP/Denotation.ML
     2.5 -    ID:         $Id$
     2.6 -    Author:     Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
     2.7 -    Copyright   1994 TUM
     2.8 -*)
     2.9 -
    2.10 -(**** mono (Gamma(b,c)) ****)
    2.11 -
    2.12 -qed_goalw "Gamma_mono" Denotation.thy [mono_def,Gamma_def]
    2.13 -        "mono (Gamma b c)"
    2.14 -     (fn _ => [Fast_tac 1]);
    2.15 -
    2.16 -
    2.17 -Goal "C(WHILE b DO c) = C(IF b THEN c;WHILE b DO c ELSE SKIP)";
    2.18 -by (Simp_tac 1);
    2.19 -by (EVERY[stac (Gamma_mono RS lfp_unfold) 1,
    2.20 -          stac (Gamma_def RS meta_eq_to_obj_eq RS fun_cong) 1,
    2.21 -          Simp_tac 1,
    2.22 -          IF_UNSOLVED no_tac]);
    2.23 -qed "C_While_If";
    2.24 -
    2.25 -
    2.26 -(* Operational Semantics implies Denotational Semantics *)
    2.27 -
    2.28 -Goal "<c,s> -c-> t ==> (s,t) : C(c)";
    2.29 -
    2.30 -(* start with rule induction *)
    2.31 -by (etac evalc.induct 1);
    2.32 -by Auto_tac;
    2.33 -(* while *)
    2.34 -by (rewtac Gamma_def);
    2.35 -by (stac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_unfold)) 1);
    2.36 -by (Fast_tac 1);
    2.37 -by (stac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_unfold)) 1);
    2.38 -by (Fast_tac 1);
    2.39 -
    2.40 -qed "com1";
    2.41 -
    2.42 -(* Denotational Semantics implies Operational Semantics *)
    2.43 -
    2.44 -Goal "!s t. (s,t):C(c) --> <c,s> -c-> t";
    2.45 -by (induct_tac "c" 1);
    2.46 -
    2.47 -by (ALLGOALS Full_simp_tac);
    2.48 -by (ALLGOALS (TRY o Fast_tac));
    2.49 -
    2.50 -(* while *)
    2.51 -by (strip_tac 1);
    2.52 -by (etac (Gamma_mono RSN (2,lfp_induct)) 1);
    2.53 -by (rewtac Gamma_def);  
    2.54 -by (Fast_tac 1);
    2.55 -
    2.56 -qed_spec_mp "com2";
    2.57 -
    2.58 -
    2.59 -(**** Proof of Equivalence ****)
    2.60 -
    2.61 -Goal "(s,t) : C(c)  =  (<c,s> -c-> t)";
    2.62 -by (fast_tac (claset() addEs [com2] addDs [com1]) 1);
    2.63 -qed "denotational_is_natural";
     3.1 --- a/src/HOL/IMP/Denotation.thy	Sun Dec 09 14:35:11 2001 +0100
     3.2 +++ b/src/HOL/IMP/Denotation.thy	Sun Dec 09 14:35:36 2001 +0100
     3.3 @@ -2,28 +2,79 @@
     3.4      ID:         $Id$
     3.5      Author:     Heiko Loetzbeyer & Robert Sandner, TUM
     3.6      Copyright   1994 TUM
     3.7 -
     3.8 -Denotational semantics of commands
     3.9  *)
    3.10  
    3.11 -Denotation = Natural + 
    3.12 +header "Denotational Semantics of Commands"
    3.13  
    3.14 -types com_den = "(state*state)set"
    3.15 +theory Denotation = Natural:
    3.16 +
    3.17 +types com_den = "(state\<times>state)set"
    3.18  
    3.19  constdefs
    3.20 -  Gamma :: [bexp,com_den] => (com_den => com_den)
    3.21 -           "Gamma b cd == (%phi.{(s,t). (s,t) : (phi O cd) & b(s)} Un 
    3.22 -                                 {(s,t). s=t & ~b(s)})"
    3.23 +  Gamma :: "[bexp,com_den] => (com_den => com_den)"
    3.24 +  "Gamma b cd == (\<lambda>phi. {(s,t). (s,t) \<in> (phi O cd) \<and> b s} \<union> 
    3.25 +                        {(s,t). s=t \<and> \<not>b s})"
    3.26      
    3.27  consts
    3.28 -  C     :: com => com_den
    3.29 +  C :: "com => com_den"
    3.30  
    3.31  primrec
    3.32 -  C_skip    "C(SKIP) = Id"
    3.33 -  C_assign  "C(x :== a) = {(s,t). t = s[x::=a(s)]}"
    3.34 -  C_comp    "C(c0 ; c1) = C(c1) O C(c0)"
    3.35 -  C_if      "C(IF b THEN c1 ELSE c2) = {(s,t). (s,t) : C(c1) & b(s)} Un
    3.36 -                                       {(s,t). (s,t) : C(c2) & ~ b(s)}"
    3.37 -  C_while   "C(WHILE b DO c) = lfp (Gamma b (C c))"
    3.38 +  C_skip:   "C \<SKIP>   = Id"
    3.39 +  C_assign: "C (x :== a) = {(s,t). t = s[x\<mapsto>a(s)]}"
    3.40 +  C_comp:   "C (c0;c1)   = C(c1) O C(c0)"
    3.41 +  C_if:     "C (\<IF> b \<THEN> c1 \<ELSE> c2) = {(s,t). (s,t) \<in> C c1 \<and> b s} \<union>
    3.42 +                                                 {(s,t). (s,t) \<in> C c2 \<and> \<not>b s}"
    3.43 +  C_while:  "C(\<WHILE> b \<DO> c) = lfp (Gamma b (C c))"
    3.44 +
    3.45 +
    3.46 +(**** mono (Gamma(b,c)) ****)
    3.47 +
    3.48 +lemma Gamma_mono: "mono (Gamma b c)"
    3.49 +  by (unfold Gamma_def mono_def) fast
    3.50 +
    3.51 +lemma C_While_If: "C(\<WHILE> b \<DO> c) = C(\<IF> b \<THEN> c;\<WHILE> b \<DO> c \<ELSE> \<SKIP>)"
    3.52 +apply (simp (no_asm))
    3.53 +apply (subst lfp_unfold [OF Gamma_mono],
    3.54 +       subst Gamma_def [THEN meta_eq_to_obj_eq, THEN fun_cong],
    3.55 +       simp)
    3.56 +done
    3.57 +
    3.58 +(* Operational Semantics implies Denotational Semantics *)
    3.59 +
    3.60 +lemma com1: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> (s,t) \<in> C(c)"
    3.61 +
    3.62 +(* start with rule induction *)
    3.63 +apply (erule evalc.induct)
    3.64 +apply auto
    3.65 +(* while *)
    3.66 +apply (unfold Gamma_def)
    3.67 +apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def])
    3.68 +apply fast
    3.69 +apply (subst lfp_unfold[OF Gamma_mono, simplified Gamma_def])
    3.70 +apply fast
    3.71 +done
    3.72 +
    3.73 +(* Denotational Semantics implies Operational Semantics *)
    3.74 +
    3.75 +lemma com2 [rule_format]: "\<forall>s t. (s,t)\<in>C(c) \<longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
    3.76 +apply (induct_tac "c")
    3.77 +
    3.78 +apply (simp_all (no_asm_use))
    3.79 +apply fast
    3.80 +apply fast
    3.81 +
    3.82 +(* while *)
    3.83 +apply (intro strip)
    3.84 +apply (erule lfp_induct [OF _ Gamma_mono])
    3.85 +apply (unfold Gamma_def)
    3.86 +apply fast
    3.87 +done
    3.88 +
    3.89 +
    3.90 +(**** Proof of Equivalence ****)
    3.91 +
    3.92 +lemma denotational_is_natural: "(s,t) \<in> C(c)  =  (\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t)"
    3.93 +apply (fast elim: com2 dest: com1)
    3.94 +done
    3.95  
    3.96  end
     4.1 --- a/src/HOL/IMP/Examples.ML	Sun Dec 09 14:35:11 2001 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,65 +0,0 @@
     4.4 -(*  Title:      HOL/IMP/Examples.ML
     4.5 -    ID:         $Id$
     4.6 -    Author:     David von Oheimb, TUM
     4.7 -    Copyright   2000 TUM
     4.8 -*)
     4.9 -
    4.10 -Addsimps[update_def];
    4.11 -
    4.12 -section "An example due to Tony Hoare";
    4.13 -
    4.14 -Goal "[| !x. P x --> Q x; <w,s> -c-> t |] ==> \
    4.15 -\ !c. w = While P c --> <While Q c,t> -c-> u --> <While Q c,s> -c-> u";
    4.16 -by (etac evalc.induct 1);
    4.17 -by (Auto_tac);
    4.18 -val lemma1 = result() RS spec RS mp RS mp;
    4.19 -
    4.20 -Goal "[| !x. P x --> Q x; <w,s> -c-> u |] ==> \
    4.21 -\ !c. w = While Q c --> <While P c; While Q c,s> -c-> u";
    4.22 -by (etac evalc.induct 1);
    4.23 -by (ALLGOALS Asm_simp_tac);
    4.24 -by (Blast_tac 1);
    4.25 -by (case_tac "P s" 1);
    4.26 -by (Auto_tac);
    4.27 -val lemma2 = result() RS spec RS mp;
    4.28 -
    4.29 -Goal "!x. P x --> Q x ==> \
    4.30 -\ (<While P c; While Q c, s> -c-> t) = (<While Q c, s> -c-> t)";
    4.31 -by (blast_tac (claset() addIs [lemma1,lemma2]) 1);
    4.32 -qed "Hoare_example";
    4.33 -
    4.34 -
    4.35 -section "Factorial";
    4.36 -
    4.37 -val step = resolve_tac evalc.intrs 1;
    4.38 -val simp = Asm_simp_tac 1;
    4.39 -Goalw [factorial_def] "a~=b ==> \
    4.40 -\ <factorial a b, Mem(a:=3)>  -c-> Mem(b:=6, a:=0)";
    4.41 -by (ftac not_sym 1);
    4.42 -by step;
    4.43 -by  step;
    4.44 -by simp;
    4.45 -by step;
    4.46 -by   simp;
    4.47 -by  step;
    4.48 -by   step;
    4.49 -by  simp;
    4.50 -by  step;
    4.51 -by simp;
    4.52 -by step;
    4.53 -by   simp;
    4.54 -by  step;
    4.55 -by   step;
    4.56 -by  simp;
    4.57 -by  step;
    4.58 -by simp;
    4.59 -by step;
    4.60 -by   simp;
    4.61 -by  step;
    4.62 -by   step;
    4.63 -by  simp;
    4.64 -by  step;
    4.65 -by simp;
    4.66 -by step;
    4.67 -by simp;
    4.68 -qed "factorial_3";
     5.1 --- a/src/HOL/IMP/Examples.thy	Sun Dec 09 14:35:11 2001 +0100
     5.2 +++ b/src/HOL/IMP/Examples.thy	Sun Dec 09 14:35:36 2001 +0100
     5.3 @@ -4,17 +4,83 @@
     5.4      Copyright   2000 TUM
     5.5  *)
     5.6  
     5.7 -Examples = Natural +
     5.8 +header "Examples"
     5.9 +
    5.10 +theory Examples = Natural:
    5.11 +
    5.12 +constdefs  
    5.13 +  factorial :: "loc => loc => com"
    5.14 +  "factorial a b == b :== (%s. 1);
    5.15 +                    \<WHILE> (%s. s a ~= 0) \<DO>
    5.16 +                    (b :== (%s. s b * s a); a :== (%s. s a - 1))"
    5.17 +
    5.18 +declare update_def [simp]
    5.19 +
    5.20 +subsection "An example due to Tony Hoare"
    5.21  
    5.22 -defs (* bring up the deferred definition for update *)
    5.23 +lemma lemma1 [rule_format (no_asm)]: 
    5.24 +  "[| !x. P x \<longrightarrow> Q x; \<langle>w,s\<rangle> \<longrightarrow>\<^sub>c t |] ==>
    5.25 +  !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"
    5.26 +apply (erule evalc.induct)
    5.27 +apply auto
    5.28 +done
    5.29 +
    5.30  
    5.31 - update_def "update == fun_upd"
    5.32 +lemma lemma2 [rule_format (no_asm)]: 
    5.33 +  "[| !x. P x \<longrightarrow> Q x; \<langle>w,s\<rangle> \<longrightarrow>\<^sub>c u |] ==>  
    5.34 +  !c. w = While Q c \<longrightarrow> \<langle>While P c; While Q c,s\<rangle> \<longrightarrow>\<^sub>c u"
    5.35 +apply (erule evalc.induct)
    5.36 +apply (simp_all (no_asm_simp))
    5.37 +apply blast
    5.38 +apply (case_tac "P s")
    5.39 +apply auto
    5.40 +done
    5.41 +
    5.42 +
    5.43 +lemma Hoare_example: "!x. P x \<longrightarrow> Q x ==>  
    5.44 +  (\<langle>While P c; While Q c, s\<rangle> \<longrightarrow>\<^sub>c t) = (\<langle>While Q c, s\<rangle> \<longrightarrow>\<^sub>c t)"
    5.45 +  by (blast intro: lemma1 lemma2 dest: semi [THEN iffD1])
    5.46 +
    5.47  
    5.48 -constdefs
    5.49 -  
    5.50 -  factorial :: loc => loc => com
    5.51 - "factorial a b == b :== (%s. 1);
    5.52 -               WHILE (%s. s a ~= 0) DO
    5.53 -                 (b :== (%s. s b * s a); a :== (%s. s a - 1))"
    5.54 +subsection "Factorial"
    5.55 +
    5.56 +lemma factorial_3: "a~=b ==>  
    5.57 +  \<langle>factorial a b, Mem(a:=3)\<rangle> \<longrightarrow>\<^sub>c Mem(b:=6, a:=0)"
    5.58 +apply (unfold factorial_def)
    5.59 +apply simp
    5.60 +done
    5.61 +
    5.62 +text {* the same in single step mode: *}
    5.63 +lemmas [simp del] = evalc_cases
    5.64 +lemma  "a~=b \<Longrightarrow> \<langle>factorial a b, Mem(a:=3)\<rangle> \<longrightarrow>\<^sub>c Mem(b:=6, a:=0)"
    5.65 +apply (unfold factorial_def)
    5.66 +apply (frule not_sym)
    5.67 +apply (rule evalc.intros)
    5.68 +apply  (rule evalc.intros)
    5.69 +apply simp
    5.70 +apply (rule evalc.intros)
    5.71 +apply   simp
    5.72 +apply  (rule evalc.intros)
    5.73 +apply   (rule evalc.intros)
    5.74 +apply  simp
    5.75 +apply  (rule evalc.intros)
    5.76 +apply simp
    5.77 +apply (rule evalc.intros)
    5.78 +apply   simp
    5.79 +apply  (rule evalc.intros)
    5.80 +apply   (rule evalc.intros)
    5.81 +apply  simp
    5.82 +apply  (rule evalc.intros)
    5.83 +apply simp
    5.84 +apply (rule evalc.intros)
    5.85 +apply   simp
    5.86 +apply  (rule evalc.intros)
    5.87 +apply   (rule evalc.intros)
    5.88 +apply  simp
    5.89 +apply  (rule evalc.intros)
    5.90 +apply simp
    5.91 +apply (rule evalc.intros)
    5.92 +apply simp
    5.93 +done
    5.94    
    5.95  end
     6.1 --- a/src/HOL/IMP/Expr.ML	Sun Dec 09 14:35:11 2001 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,48 +0,0 @@
     6.4 -(*  Title:      HOL/IMP/Expr.ML
     6.5 -    ID:         $Id$
     6.6 -    Author:     Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
     6.7 -    Copyright   1994 TUM
     6.8 -
     6.9 -Arithmetic expressions and Boolean expressions.
    6.10 -Not used in the rest of the language, but included for completeness.
    6.11 -*)
    6.12 -
    6.13 -val evala_elim_cases = 
    6.14 -    map evala.mk_cases
    6.15 -       ["(N(n),sigma) -a-> i", 
    6.16 -	"(X(x),sigma) -a-> i",
    6.17 -	"(Op1 f e,sigma) -a-> i", 
    6.18 -	"(Op2 f a1 a2,sigma)  -a-> i"];
    6.19 -
    6.20 -val evalb_elim_cases = 
    6.21 -    map evalb.mk_cases
    6.22 -       ["(true,sigma) -b-> x", 
    6.23 -	"(false,sigma) -b-> x",
    6.24 -	"(ROp f a0 a1,sigma) -b-> x", 
    6.25 -	"(noti(b),sigma) -b-> x",
    6.26 -	"(b0 andi b1,sigma) -b-> x", 
    6.27 -	"(b0 ori b1,sigma) -b-> x"];
    6.28 -
    6.29 -val evalb_simps = map (fn s => prove_goal Expr.thy s
    6.30 -    (fn _ => [fast_tac (HOL_cs addSIs evalb.intrs addSEs evalb_elim_cases) 1]))
    6.31 -  ["((true,sigma) -b-> w) = (w=True)",
    6.32 -   "((false,sigma) -b-> w) = (w=False)",
    6.33 -   "((ROp f a0 a1,sigma) -b-> w) = \
    6.34 -\   (? m. (a0,sigma) -a-> m & (? n. (a1,sigma) -a-> n & w = f m n))",
    6.35 -   "((noti(b),sigma) -b-> w) = (? x. (b,sigma) -b-> x & w = (~x))",
    6.36 -   "((b0 andi b1,sigma) -b-> w) = \
    6.37 -\   (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x&y)))",
    6.38 -   "((b0 ori b1,sigma) -b-> w) = \
    6.39 -\   (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x|y)))"];
    6.40 -
    6.41 -Goal "!n. ((a,s) -a-> n) = (A a s = n)";
    6.42 -by (induct_tac "a" 1);
    6.43 -by (auto_tac (claset() addSIs evala.intrs addSEs evala_elim_cases,
    6.44 -	      simpset()));
    6.45 -qed_spec_mp "aexp_iff";
    6.46 -
    6.47 -Goal "!w. ((b,s) -b-> w) = (B b s = w)";
    6.48 -by (induct_tac "b" 1);
    6.49 -by (auto_tac (claset(), 
    6.50 -	      simpset() addsimps aexp_iff::evalb_simps));
    6.51 -qed_spec_mp "bexp_iff";
     7.1 --- a/src/HOL/IMP/Expr.thy	Sun Dec 09 14:35:11 2001 +0100
     7.2 +++ b/src/HOL/IMP/Expr.thy	Sun Dec 09 14:35:36 2001 +0100
     7.3 @@ -2,20 +2,24 @@
     7.4      ID:         $Id$
     7.5      Author:     Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
     7.6      Copyright   1994 TUM
     7.7 -
     7.8 -Arithmetic expressions and Boolean expressions.
     7.9 -Not used in the rest of the language, but included for completeness.
    7.10  *)
    7.11  
    7.12 -Expr = Datatype +
    7.13 +header "Expressions"
    7.14 +
    7.15 +theory Expr = Datatype:
    7.16  
    7.17 -(** Arithmetic expressions **)
    7.18 -types loc
    7.19 -      state = "loc => nat"
    7.20 -      n2n = "nat => nat"
    7.21 -      n2n2n = "nat => nat => nat"
    7.22 +text {*
    7.23 +  Arithmetic expressions and Boolean expressions.
    7.24 +  Not used in the rest of the language, but included for completeness.
    7.25 +*}
    7.26  
    7.27 -arities loc :: type
    7.28 +subsection "Arithmetic expressions"
    7.29 +typedecl loc 
    7.30 +
    7.31 +types
    7.32 +  state = "loc => nat"
    7.33 +  n2n = "nat => nat"
    7.34 +  n2n2n = "nat => nat => nat"
    7.35  
    7.36  datatype
    7.37    aexp = N nat
    7.38 @@ -23,22 +27,24 @@
    7.39         | Op1 n2n aexp
    7.40         | Op2 n2n2n aexp aexp
    7.41  
    7.42 -(** Evaluation of arithmetic expressions **)
    7.43 +subsection "Evaluation of arithmetic expressions"
    7.44  consts  evala    :: "((aexp*state) * nat) set"
    7.45         "-a->"    :: "[aexp*state,nat] => bool"         (infixl 50)
    7.46  translations
    7.47      "aesig -a-> n" == "(aesig,n) : evala"
    7.48  inductive evala
    7.49 -  intrs 
    7.50 -    N   "(N(n),s) -a-> n"
    7.51 -    X   "(X(x),s) -a-> s(x)"
    7.52 -    Op1 "(e,s) -a-> n ==> (Op1 f e,s) -a-> f(n)"
    7.53 -    Op2 "[| (e0,s) -a-> n0;  (e1,s)  -a-> n1 |] 
    7.54 -           ==> (Op2 f e0 e1,s) -a-> f n0 n1"
    7.55 +  intros 
    7.56 +  N:   "(N(n),s) -a-> n"
    7.57 +  X:   "(X(x),s) -a-> s(x)"
    7.58 +  Op1: "(e,s) -a-> n ==> (Op1 f e,s) -a-> f(n)"
    7.59 +  Op2: "[| (e0,s) -a-> n0;  (e1,s)  -a-> n1 |] 
    7.60 +        ==> (Op2 f e0 e1,s) -a-> f n0 n1"
    7.61 +
    7.62 +lemmas [intro] = N X Op1 Op2
    7.63  
    7.64  types n2n2b = "[nat,nat] => bool"
    7.65  
    7.66 -(** Boolean expressions **)
    7.67 +subsection "Boolean expressions"
    7.68  
    7.69  datatype
    7.70    bexp = true
    7.71 @@ -48,7 +54,7 @@
    7.72         | andi bexp bexp         (infixl 60)
    7.73         | ori  bexp bexp         (infixl 60)
    7.74  
    7.75 -(** Evaluation of boolean expressions **)
    7.76 +subsection "Evaluation of boolean expressions"
    7.77  consts evalb    :: "((bexp*state) * bool)set"       
    7.78         "-b->"   :: "[bexp*state,bool] => bool"         (infixl 50)
    7.79  
    7.80 @@ -56,21 +62,24 @@
    7.81      "besig -b-> b" == "(besig,b) : evalb"
    7.82  
    7.83  inductive evalb
    7.84 - intrs (*avoid clash with ML constructors true, false*)
    7.85 -    tru   "(true,s) -b-> True"
    7.86 -    fls   "(false,s) -b-> False"
    7.87 -    ROp   "[| (a0,s) -a-> n0; (a1,s) -a-> n1 |] 
    7.88 -           ==> (ROp f a0 a1,s) -b-> f n0 n1"
    7.89 -    noti  "(b,s) -b-> w ==> (noti(b),s) -b-> (~w)"
    7.90 -    andi  "[| (b0,s) -b-> w0; (b1,s) -b-> w1 |] 
    7.91 +  -- "avoid clash with ML constructors true, false"
    7.92 +  intros
    7.93 +  tru:   "(true,s) -b-> True"
    7.94 +  fls:   "(false,s) -b-> False"
    7.95 +  ROp:   "[| (a0,s) -a-> n0; (a1,s) -a-> n1 |] 
    7.96 +          ==> (ROp f a0 a1,s) -b-> f n0 n1"
    7.97 +  noti:  "(b,s) -b-> w ==> (noti(b),s) -b-> (~w)"
    7.98 +  andi:  "[| (b0,s) -b-> w0; (b1,s) -b-> w1 |] 
    7.99            ==> (b0 andi b1,s) -b-> (w0 & w1)"
   7.100 -    ori   "[| (b0,s) -b-> w0; (b1,s) -b-> w1 |] 
   7.101 -            ==> (b0 ori b1,s) -b-> (w0 | w1)"
   7.102 +  ori:   "[| (b0,s) -b-> w0; (b1,s) -b-> w1 |] 
   7.103 +          ==> (b0 ori b1,s) -b-> (w0 | w1)"
   7.104 +
   7.105 +lemmas [intro] = tru fls ROp noti andi ori
   7.106  
   7.107 -(** Denotational semantics of arithemtic and boolean expressions **)
   7.108 +subsection "Denotational semantics of arithmetic and boolean expressions"
   7.109  consts
   7.110 -  A     :: aexp => state => nat
   7.111 -  B     :: bexp => state => bool
   7.112 +  A     :: "aexp => state => nat"
   7.113 +  B     :: "bexp => state => bool"
   7.114  
   7.115  primrec
   7.116    "A(N(n)) = (%s. n)"
   7.117 @@ -86,5 +95,59 @@
   7.118    "B(b0 andi b1) = (%s. (B b0 s) & (B b1 s))"
   7.119    "B(b0 ori b1) = (%s. (B b0 s) | (B b1 s))"
   7.120  
   7.121 +lemma [simp]: "(N(n),s) -a-> n' = (n = n')"
   7.122 +  by (rule,cases set: evala) auto
   7.123 +
   7.124 +lemma [simp]: "(X(x),sigma) -a-> i = (i = sigma x)" 
   7.125 +  by (rule,cases set: evala) auto
   7.126 +
   7.127 +lemma	[simp]: 
   7.128 +  "(Op1 f e,sigma) -a-> i = (\<exists>n. i = f n \<and> (e,sigma) -a-> n)" 
   7.129 +  by (rule,cases set: evala) auto
   7.130 +
   7.131 +lemma [simp]:
   7.132 +  "(Op2 f a1 a2,sigma) -a-> i = 
   7.133 +  (\<exists>n0 n1. i = f n0 n1 \<and> (a1, sigma) -a-> n0 \<and> (a2, sigma) -a-> n1)"
   7.134 +  by (rule,cases set: evala) auto
   7.135 +
   7.136 +lemma [simp]: "((true,sigma) -b-> w) = (w=True)" 
   7.137 +  by (rule,cases set: evalb) auto
   7.138 +
   7.139 +lemma [simp]:
   7.140 +  "((false,sigma) -b-> w) = (w=False)" 
   7.141 +  by (rule,cases set: evalb) auto
   7.142 +
   7.143 +lemma [simp]:
   7.144 +  "((ROp f a0 a1,sigma) -b-> w) =   
   7.145 +  (? m. (a0,sigma) -a-> m & (? n. (a1,sigma) -a-> n & w = f m n))" 
   7.146 +  by (rule,cases set: evalb) auto
   7.147 +
   7.148 +lemma [simp]:  
   7.149 +  "((noti(b),sigma) -b-> w) = (? x. (b,sigma) -b-> x & w = (~x))" 
   7.150 +  by (rule,cases set: evalb) auto
   7.151 +
   7.152 +lemma [simp]:
   7.153 +  "((b0 andi b1,sigma) -b-> w) =   
   7.154 +  (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x&y)))" 
   7.155 +  by (rule,cases set: evalb) auto
   7.156 +
   7.157 +lemma [simp]:  
   7.158 +  "((b0 ori b1,sigma) -b-> w) =   
   7.159 +  (? x. (b0,sigma) -b-> x & (? y. (b1,sigma) -b-> y & w = (x|y)))" 
   7.160 +  by (rule,cases set: evalb) auto
   7.161 +
   7.162 +
   7.163 +lemma aexp_iff [rule_format (no_asm)]: 
   7.164 +  "!n. ((a,s) -a-> n) = (A a s = n)"
   7.165 +  apply (induct_tac "a")
   7.166 +  apply auto
   7.167 +  done
   7.168 +
   7.169 +lemma bexp_iff [rule_format (no_asm)]: 
   7.170 +  "!w. ((b,s) -b-> w) = (B b s = w)"
   7.171 +  apply (induct_tac "b")
   7.172 +  apply (auto simp add: aexp_iff)
   7.173 +  done
   7.174 +
   7.175  end
   7.176  
     8.1 --- a/src/HOL/IMP/Hoare.ML	Sun Dec 09 14:35:11 2001 +0100
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,117 +0,0 @@
     8.4 -(*  Title:      HOL/IMP/Hoare.ML
     8.5 -    ID:         $Id$
     8.6 -    Author:     Tobias Nipkow
     8.7 -    Copyright   1995 TUM
     8.8 -
     8.9 -Soundness (and part of) relative completeness of Hoare rules
    8.10 -wrt denotational semantics
    8.11 -*)
    8.12 -
    8.13 -Goal "[| !s. P' s --> P s; |- {P}c{Q} |] ==> |- {P'}c{Q}";
    8.14 -by (etac hoare.conseq 1);
    8.15 -by  (atac 1);
    8.16 -by (Fast_tac 1);
    8.17 -qed "hoare_conseq1";
    8.18 -
    8.19 -Goal "[| |- {P}c{Q}; !s. Q s --> Q' s |] ==> |- {P}c{Q'}";
    8.20 -by (rtac hoare.conseq 1);
    8.21 -by    (atac 2);
    8.22 -by   (ALLGOALS Fast_tac);
    8.23 -qed "hoare_conseq2";
    8.24 -
    8.25 -Goalw [hoare_valid_def] "|- {P}c{Q} ==> |= {P}c{Q}";
    8.26 -by (etac hoare.induct 1);
    8.27 -     by (ALLGOALS Asm_simp_tac);
    8.28 -  by (Fast_tac 1);
    8.29 - by (Fast_tac 1);
    8.30 -by (EVERY' [rtac allI, rtac allI, rtac impI] 1);
    8.31 -by (etac lfp_induct2 1);
    8.32 - by (rtac Gamma_mono 1);
    8.33 -by (rewtac Gamma_def);  
    8.34 -by (Fast_tac 1);
    8.35 -qed "hoare_sound";
    8.36 -
    8.37 -Goalw [wp_def] "wp SKIP Q = Q";
    8.38 -by (Simp_tac 1);
    8.39 -qed "wp_SKIP";
    8.40 -
    8.41 -Goalw [wp_def] "wp (x:==a) Q = (%s. Q(s[x::=a s]))";
    8.42 -by (Simp_tac 1);
    8.43 -qed "wp_Ass";
    8.44 -
    8.45 -Goalw [wp_def] "wp (c;d) Q = wp c (wp d Q)";
    8.46 -by (Simp_tac 1);
    8.47 -by (rtac ext 1);
    8.48 -by (Fast_tac 1);
    8.49 -qed "wp_Semi";
    8.50 -
    8.51 -Goalw [wp_def]
    8.52 - "wp (IF b THEN c ELSE d) Q = (%s. (b s --> wp c Q s) &  (~b s --> wp d Q s))";
    8.53 -by (Simp_tac 1);
    8.54 -by (rtac ext 1);
    8.55 -by (Fast_tac 1);
    8.56 -qed "wp_If";
    8.57 -
    8.58 -Goalw [wp_def]
    8.59 -  "b s ==> wp (WHILE b DO c) Q s = wp (c;WHILE b DO c) Q s";
    8.60 -by (stac C_While_If 1);
    8.61 -by (Asm_simp_tac 1);
    8.62 -qed "wp_While_True";
    8.63 -
    8.64 -Goalw [wp_def] "~b s ==> wp (WHILE b DO c) Q s = Q s";
    8.65 -by (stac C_While_If 1);
    8.66 -by (Asm_simp_tac 1);
    8.67 -qed "wp_While_False";
    8.68 -
    8.69 -Addsimps [wp_SKIP,wp_Ass,wp_Semi,wp_If,wp_While_True,wp_While_False];
    8.70 -
    8.71 -(*Not suitable for rewriting: LOOPS!*)
    8.72 -Goal "wp (WHILE b DO c) Q s = (if b s then wp (c;WHILE b DO c) Q s else Q s)";
    8.73 -by (Simp_tac 1);
    8.74 -qed "wp_While_if";
    8.75 -
    8.76 -Goal "wp (WHILE b DO c) Q s = \
    8.77 -\  (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))";
    8.78 -by (Simp_tac 1);
    8.79 -by (rtac iffI 1);
    8.80 - by (rtac weak_coinduct 1);
    8.81 -  by (etac CollectI 1);
    8.82 - by Safe_tac;
    8.83 -  by (rotate_tac ~1 1);
    8.84 -  by (Asm_full_simp_tac 1);
    8.85 - by (rotate_tac ~1 1);
    8.86 - by (Asm_full_simp_tac 1);
    8.87 -by (asm_full_simp_tac (simpset() addsimps [wp_def,Gamma_def]) 1);
    8.88 -by (strip_tac 1);
    8.89 -by (rtac mp 1);
    8.90 - by (assume_tac 2);
    8.91 -by (etac lfp_induct2 1);
    8.92 -by (fast_tac (claset() addSIs [monoI]) 1);
    8.93 -by (stac gfp_unfold 1);
    8.94 - by (fast_tac (claset() addSIs [monoI]) 1);
    8.95 -by (Fast_tac 1);
    8.96 -qed "wp_While";
    8.97 -
    8.98 -Delsimps [C_while];
    8.99 -
   8.100 -AddSIs [hoare.skip, hoare.ass, hoare.semi, hoare.If];
   8.101 -
   8.102 -Goal "!Q. |- {wp c Q} c {Q}";
   8.103 -by (induct_tac "c" 1);
   8.104 -    by (ALLGOALS Simp_tac);
   8.105 -    by (REPEAT_FIRST Fast_tac);
   8.106 - by (blast_tac (claset() addIs [hoare_conseq1]) 1);
   8.107 -by Safe_tac;
   8.108 -by (rtac hoare_conseq2 1);
   8.109 - by (rtac hoare.While 1);
   8.110 - by (rtac hoare_conseq1 1);
   8.111 -  by (Fast_tac 2);
   8.112 - by (safe_tac HOL_cs);
   8.113 - by (ALLGOALS (EVERY'[rotate_tac ~1, Asm_full_simp_tac]));
   8.114 -qed_spec_mp "wp_is_pre";
   8.115 -
   8.116 -Goal "|= {P}c{Q} ==> |- {P}c{Q}";
   8.117 -by (rtac (wp_is_pre RSN (2,hoare_conseq1)) 1);
   8.118 -by (rewrite_goals_tac [hoare_valid_def,wp_def]);
   8.119 -by (Fast_tac 1);
   8.120 -qed "hoare_relative_complete";
     9.1 --- a/src/HOL/IMP/Hoare.thy	Sun Dec 09 14:35:11 2001 +0100
     9.2 +++ b/src/HOL/IMP/Hoare.thy	Sun Dec 09 14:35:36 2001 +0100
     9.3 @@ -2,34 +2,157 @@
     9.4      ID:         $Id$
     9.5      Author:     Tobias Nipkow
     9.6      Copyright   1995 TUM
     9.7 -
     9.8 -Inductive definition of Hoare logic
     9.9  *)
    9.10  
    9.11 -Hoare = Denotation + Inductive +
    9.12 +header "Inductive Definition of Hoare Logic"
    9.13 +
    9.14 +theory Hoare = Denotation:
    9.15  
    9.16 -types assn = state => bool
    9.17 +types assn = "state => bool"
    9.18  
    9.19 -constdefs hoare_valid :: [assn,com,assn] => bool ("|= {(1_)}/ (_)/ {(1_)}" 50)
    9.20 +constdefs hoare_valid :: "[assn,com,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50)
    9.21            "|= {P}c{Q} == !s t. (s,t) : C(c) --> P s --> Q t"
    9.22  
    9.23  consts hoare :: "(assn * com * assn) set"
    9.24 -syntax "@hoare" :: [bool,com,bool] => bool ("|- ({(1_)}/ (_)/ {(1_)})" 50)
    9.25 +syntax "@hoare" :: "[bool,com,bool] => bool" ("|- ({(1_)}/ (_)/ {(1_)})" 50)
    9.26  translations "|- {P}c{Q}" == "(P,c,Q) : hoare"
    9.27  
    9.28  inductive hoare
    9.29 -intrs
    9.30 -  skip "|- {P}SKIP{P}"
    9.31 -  ass  "|- {%s. P(s[x::=a s])} x:==a {P}"
    9.32 -  semi "[| |- {P}c{Q}; |- {Q}d{R} |] ==> |- {P} c;d {R}"
    9.33 -  If "[| |- {%s. P s & b s}c{Q}; |- {%s. P s & ~b s}d{Q} |] ==>
    9.34 -      |- {P} IF b THEN c ELSE d {Q}"
    9.35 -  While "|- {%s. P s & b s} c {P} ==>
    9.36 -         |- {P} WHILE b DO c {%s. P s & ~b s}"
    9.37 -  conseq "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==>
    9.38 +intros
    9.39 +  skip: "|- {P}\<SKIP>{P}"
    9.40 +  ass:  "|- {%s. P(s[x\<mapsto>a s])} x:==a {P}"
    9.41 +  semi: "[| |- {P}c{Q}; |- {Q}d{R} |] ==> |- {P} c;d {R}"
    9.42 +  If: "[| |- {%s. P s & b s}c{Q}; |- {%s. P s & ~b s}d{Q} |] ==>
    9.43 +      |- {P} \<IF> b \<THEN> c \<ELSE> d {Q}"
    9.44 +  While: "|- {%s. P s & b s} c {P} ==>
    9.45 +         |- {P} \<WHILE> b \<DO> c {%s. P s & ~b s}"
    9.46 +  conseq: "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==>
    9.47            |- {P'}c{Q'}"
    9.48  
    9.49 -constdefs wp :: com => assn => assn
    9.50 +constdefs wp :: "com => assn => assn"
    9.51            "wp c Q == (%s. !t. (s,t) : C(c) --> Q t)"
    9.52  
    9.53 +(*  
    9.54 +Soundness (and part of) relative completeness of Hoare rules
    9.55 +wrt denotational semantics
    9.56 +*)
    9.57 +
    9.58 +lemma hoare_conseq1: "[| !s. P' s --> P s; |- {P}c{Q} |] ==> |- {P'}c{Q}"
    9.59 +apply (erule hoare.conseq)
    9.60 +apply  assumption
    9.61 +apply fast
    9.62 +done
    9.63 +
    9.64 +lemma hoare_conseq2: "[| |- {P}c{Q}; !s. Q s --> Q' s |] ==> |- {P}c{Q'}"
    9.65 +apply (rule hoare.conseq)
    9.66 +prefer 2 apply    (assumption)
    9.67 +apply fast
    9.68 +apply fast
    9.69 +done
    9.70 +
    9.71 +lemma hoare_sound: "|- {P}c{Q} ==> |= {P}c{Q}"
    9.72 +apply (unfold hoare_valid_def)
    9.73 +apply (erule hoare.induct)
    9.74 +     apply (simp_all (no_asm_simp))
    9.75 +  apply fast
    9.76 + apply fast
    9.77 +apply (rule allI, rule allI, rule impI)
    9.78 +apply (erule lfp_induct2)
    9.79 + apply (rule Gamma_mono)
    9.80 +apply (unfold Gamma_def)
    9.81 +apply fast
    9.82 +done
    9.83 +
    9.84 +lemma wp_SKIP: "wp \<SKIP> Q = Q"
    9.85 +apply (unfold wp_def)
    9.86 +apply (simp (no_asm))
    9.87 +done
    9.88 +
    9.89 +lemma wp_Ass: "wp (x:==a) Q = (%s. Q(s[x\<mapsto>a s]))"
    9.90 +apply (unfold wp_def)
    9.91 +apply (simp (no_asm))
    9.92 +done
    9.93 +
    9.94 +lemma wp_Semi: "wp (c;d) Q = wp c (wp d Q)"
    9.95 +apply (unfold wp_def)
    9.96 +apply (simp (no_asm))
    9.97 +apply (rule ext)
    9.98 +apply fast
    9.99 +done
   9.100 +
   9.101 +lemma wp_If: 
   9.102 + "wp (\<IF> b \<THEN> c \<ELSE> d) Q = (%s. (b s --> wp c Q s) &  (~b s --> wp d Q s))"
   9.103 +apply (unfold wp_def)
   9.104 +apply (simp (no_asm))
   9.105 +apply (rule ext)
   9.106 +apply fast
   9.107 +done
   9.108 +
   9.109 +lemma wp_While_True: 
   9.110 +  "b s ==> wp (\<WHILE> b \<DO> c) Q s = wp (c;\<WHILE> b \<DO> c) Q s"
   9.111 +apply (unfold wp_def)
   9.112 +apply (subst C_While_If)
   9.113 +apply (simp (no_asm_simp))
   9.114 +done
   9.115 +
   9.116 +lemma wp_While_False: "~b s ==> wp (\<WHILE> b \<DO> c) Q s = Q s"
   9.117 +apply (unfold wp_def)
   9.118 +apply (subst C_While_If)
   9.119 +apply (simp (no_asm_simp))
   9.120 +done
   9.121 +
   9.122 +declare wp_SKIP [simp] wp_Ass [simp] wp_Semi [simp] wp_If [simp] wp_While_True [simp] wp_While_False [simp]
   9.123 +
   9.124 +(*Not suitable for rewriting: LOOPS!*)
   9.125 +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)"
   9.126 +apply (simp (no_asm))
   9.127 +done
   9.128 +
   9.129 +lemma wp_While: "wp (\<WHILE> b \<DO> c) Q s =  
   9.130 +   (s : gfp(%S.{s. if b s then wp c (%s. s:S) s else Q s}))"
   9.131 +apply (simp (no_asm))
   9.132 +apply (rule iffI)
   9.133 + apply (rule weak_coinduct)
   9.134 +  apply (erule CollectI)
   9.135 + apply safe
   9.136 +  apply (rotate_tac -1)
   9.137 +  apply simp
   9.138 + apply (rotate_tac -1)
   9.139 + apply simp
   9.140 +apply (simp add: wp_def Gamma_def)
   9.141 +apply (intro strip)
   9.142 +apply (rule mp)
   9.143 + prefer 2 apply (assumption)
   9.144 +apply (erule lfp_induct2)
   9.145 +apply (fast intro!: monoI)
   9.146 +apply (subst gfp_unfold)
   9.147 + apply (fast intro!: monoI)
   9.148 +apply fast
   9.149 +done
   9.150 +
   9.151 +declare C_while [simp del]
   9.152 +
   9.153 +declare hoare.skip [intro!] hoare.ass [intro!] hoare.semi [intro!] hoare.If [intro!]
   9.154 +
   9.155 +lemma wp_is_pre [rule_format (no_asm)]: "!Q. |- {wp c Q} c {Q}"
   9.156 +apply (induct_tac "c")
   9.157 +    apply (simp_all (no_asm))
   9.158 +    apply fast+
   9.159 + apply (blast intro: hoare_conseq1)
   9.160 +apply safe
   9.161 +apply (rule hoare_conseq2)
   9.162 + apply (rule hoare.While)
   9.163 + apply (rule hoare_conseq1)
   9.164 +  prefer 2 apply (fast)
   9.165 +  apply safe
   9.166 + apply (rotate_tac -1, simp)
   9.167 +apply (rotate_tac -1, simp)
   9.168 +done
   9.169 +
   9.170 +lemma hoare_relative_complete: "|= {P}c{Q} ==> |- {P}c{Q}"
   9.171 +apply (rule hoare_conseq1 [OF _ wp_is_pre])
   9.172 +apply (unfold hoare_valid_def wp_def)
   9.173 +apply fast
   9.174 +done
   9.175 +
   9.176  end
    10.1 --- a/src/HOL/IMP/Natural.ML	Sun Dec 09 14:35:11 2001 +0100
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,28 +0,0 @@
    10.4 -(*  Title:      HOL/IMP/Natural.ML
    10.5 -    ID:         $Id$
    10.6 -    Author:     Tobias Nipkow & Larry Paulson, TUM
    10.7 -    Copyright   1996 TUM
    10.8 -*)
    10.9 -
   10.10 -open Natural;
   10.11 -
   10.12 -AddIs evalc.intrs;
   10.13 -
   10.14 -val evalc_elim_cases = 
   10.15 -    map evalc.mk_cases
   10.16 -       ["<SKIP,s> -c-> t", 
   10.17 -	"<x:==a,s> -c-> t", 
   10.18 -	"<c1;c2, s> -c-> t",
   10.19 -	"<IF b THEN c1 ELSE c2, s> -c-> t"];
   10.20 -
   10.21 -val evalc_WHILE_case = evalc.mk_cases "<WHILE b DO c,s> -c-> t";
   10.22 -
   10.23 -AddSEs evalc_elim_cases;
   10.24 -
   10.25 -(* evaluation of com is deterministic *)
   10.26 -Goal "<c,s> -c-> t ==> (!u. <c,s> -c-> u --> u=t)";
   10.27 -by (etac evalc.induct 1);
   10.28 -by (thin_tac "<?c,s2> -c-> s1" 7);
   10.29 -(*blast_tac needs Unify.search_bound, trace_bound ::= 40*)
   10.30 -by (ALLGOALS (best_tac (claset() addEs [evalc_WHILE_case])));
   10.31 -qed_spec_mp "com_det";
    11.1 --- a/src/HOL/IMP/Natural.thy	Sun Dec 09 14:35:11 2001 +0100
    11.2 +++ b/src/HOL/IMP/Natural.thy	Sun Dec 09 14:35:36 2001 +0100
    11.3 @@ -1,45 +1,283 @@
    11.4 -(*  Title:      HOL/IMP/Natural.thy
    11.5 -    ID:         $Id$
    11.6 -    Author:     Tobias Nipkow & Robert Sandner, TUM
    11.7 -    Copyright   1996 TUM
    11.8 -
    11.9 -Natural semantics of commands
   11.10 +(*  Title:        HOL/IMP/Natural.thy
   11.11 +    ID:           $Id$
   11.12 +    Author:       Tobias Nipkow & Robert Sandner, TUM
   11.13 +    Isar Version: Gerwin Klein, 2001
   11.14 +    Copyright     1996 TUM
   11.15  *)
   11.16  
   11.17 -Natural = Com + Inductive +
   11.18 +header "Natural Semantics of Commands"
   11.19 +
   11.20 +theory Natural = Com:
   11.21 +
   11.22 +subsection "Execution of commands"
   11.23  
   11.24 -(** Execution of commands **)
   11.25 -consts  evalc    :: "(com*state*state)set"
   11.26 -        "@evalc" :: [com,state,state] => bool ("<_,_>/ -c-> _" [0,0,50] 50)
   11.27 +consts  evalc  :: "(com \<times> state \<times> state) set" 
   11.28 +        "@evalc" :: "[com,state,state] \<Rightarrow> bool" ("<_,_>/ -c-> _" [0,0,60] 60)
   11.29  
   11.30 -translations  "<ce,sig> -c-> s" == "(ce,sig,s) : evalc"
   11.31 +syntax (xsymbols)
   11.32 +  "@evalc" :: "[com,state,state] \<Rightarrow> bool" ("\<langle>_,_\<rangle>/ \<longrightarrow>\<^sub>c _" [0,0,60] 60)
   11.33  
   11.34 -consts
   11.35 -  update  :: "('a => 'b) => 'a => 'b => ('a => 'b)"
   11.36 -           ("_/[_/::=/_]" [900,0,0] 900)
   11.37 -(* update is NOT defined, only declared!
   11.38 -   Thus the whole theory is independent of its meaning!
   11.39 -   If the definition (update == fun_upd) is included, proofs break.
   11.40 -*)
   11.41 +text {*
   11.42 +  We write @{text "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"} for \emph{Statement @{text c}, started 
   11.43 +  in state @{text s}, terminates in state @{text s'}}. Formally,
   11.44 +  @{text "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"} is just another form of saying \emph{the tuple
   11.45 +  @{text "(c,s,s')"} is part of the relation @{text evalc}}:
   11.46 +*}
   11.47 +translations  "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" == "(c,s,s') \<in> evalc"
   11.48  
   11.49 +constdefs
   11.50 +  update :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("_/[_ ::= /_]" [900,0,0] 900)
   11.51 +  "update == fun_upd"
   11.52 +
   11.53 +syntax (xsymbols)
   11.54 +  update :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)" ("_/[_ \<mapsto> /_]" [900,0,0] 900)
   11.55 +
   11.56 +text {*
   11.57 +  The big-step execution relation @{text evalc} is defined inductively:
   11.58 +*}
   11.59  inductive evalc
   11.60 -  intrs
   11.61 -    Skip    "<SKIP,s> -c-> s"
   11.62 +  intros 
   11.63 +  Skip:    "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s"
   11.64 +  Assign:  "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c s[x\<mapsto>a s]"
   11.65 +
   11.66 +  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'"
   11.67 +
   11.68 +  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'"
   11.69 +  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'"
   11.70 +
   11.71 +  WhileFalse: "\<not>b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c s"
   11.72 +  WhileTrue:  "b s \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'' \<Longrightarrow> \<langle>\<WHILE> b \<DO> c, s''\<rangle> \<longrightarrow>\<^sub>c s'  
   11.73 +               \<Longrightarrow> \<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>c s'"
   11.74 +
   11.75 +lemmas evalc.intros [intro] -- "use those rules in automatic proofs"
   11.76 +
   11.77 +text {*
   11.78 +The induction principle induced by this definition looks like this:
   11.79 +
   11.80 +@{thm [display] evalc.induct [no_vars]}
   11.81 +
   11.82 +
   11.83 +(@{text "\<And>"} and @{text "\<Longrightarrow>"} are Isabelle's 
   11.84 +  meta symbols for @{text "\<forall>"} and @{text "\<longrightarrow>"})
   11.85 +*}
   11.86 +
   11.87 +
   11.88 +text {*
   11.89 +  The rules of @{text evalc} are syntax directed, i.e.~for each
   11.90 +  syntactic category there is always only one rule applicable. That
   11.91 +  means we can use the rules in both directions. The proofs for this
   11.92 +  are all the same: one direction is trivial, the other one is shown
   11.93 +  by using the @{text evalc} rules backwards: 
   11.94 +*}
   11.95 +lemma skip: 
   11.96 +  "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s' = (s' = s)"
   11.97 +  by (rule, erule evalc.elims) auto
   11.98 +
   11.99 +lemma assign: 
  11.100 +  "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c s' = (s' = s[x\<mapsto>a s])" 
  11.101 +  by (rule, erule evalc.elims) auto
  11.102 +
  11.103 +lemma semi: 
  11.104 +  "\<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')"
  11.105 +  by (rule, erule evalc.elims) auto
  11.106  
  11.107 -    Assign  "<x :== a,s> -c-> s[x::=a s]"
  11.108 +lemma ifTrue: 
  11.109 +  "b s \<Longrightarrow> \<langle>\<IF> b \<THEN> c0 \<ELSE> c1, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'" 
  11.110 +  by (rule, erule evalc.elims) auto
  11.111 +
  11.112 +lemma ifFalse: 
  11.113 +  "\<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'"
  11.114 +  by (rule, erule evalc.elims) auto
  11.115 +
  11.116 +lemma whileFalse: 
  11.117 +  "\<not> b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c s' = (s' = s)"
  11.118 +  by (rule, erule evalc.elims) auto  
  11.119 +
  11.120 +lemma whileTrue: 
  11.121 +  "b s \<Longrightarrow> 
  11.122 +  \<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>c s' = 
  11.123 +  (\<exists>s''. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'' \<and> \<langle>\<WHILE> b \<DO> c, s''\<rangle> \<longrightarrow>\<^sub>c s')"
  11.124 +  by (rule, erule evalc.elims) auto
  11.125 +
  11.126 +text "Again, Isabelle may use these rules in automatic proofs:"
  11.127 +lemmas evalc_cases [simp] = skip assign ifTrue ifFalse whileFalse semi whileTrue
  11.128 +
  11.129 +subsection "Equivalence of statements"
  11.130  
  11.131 -    Semi    "[| <c0,s> -c-> s2; <c1,s2> -c-> s1 |] 
  11.132 -            ==> <c0 ; c1, s> -c-> s1"
  11.133 +text {*
  11.134 +  We call two statements @{text c} and @{text c'} equivalent wrt.~the
  11.135 +  big-step semantics when \emph{@{text c} started in @{text s} terminates
  11.136 +  in @{text s'} iff @{text c'} started in the same @{text s} also terminates
  11.137 +  in the same @{text s'}}. Formally:
  11.138 +*} 
  11.139 +constdefs
  11.140 +  equiv_c :: "com \<Rightarrow> com \<Rightarrow> bool" ("_ \<sim> _")
  11.141 +  "c \<sim> c' \<equiv> \<forall>s s'. \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s'"
  11.142 +
  11.143 +text {*
  11.144 +  Proof rules telling Isabelle to unfold the definition
  11.145 +  if there is something to be proved about equivalent
  11.146 +  statements: *} 
  11.147 +lemma equivI [intro!]:
  11.148 +  "(\<And>s s'. \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s') \<Longrightarrow> c \<sim> c'"
  11.149 +  by (unfold equiv_c_def) blast
  11.150 +
  11.151 +lemma equivD1:
  11.152 +  "c \<sim> c' \<Longrightarrow> \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s'"
  11.153 +  by (unfold equiv_c_def) blast
  11.154 +
  11.155 +lemma equivD2:
  11.156 +  "c \<sim> c' \<Longrightarrow> \<langle>c', s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s'"
  11.157 +  by (unfold equiv_c_def) blast
  11.158  
  11.159 -    IfTrue "[| b s; <c0,s> -c-> s1 |] 
  11.160 -            ==> <IF b THEN c0 ELSE c1, s> -c-> s1"
  11.161 +text {*
  11.162 +  As an example, we show that loop unfolding is an equivalence
  11.163 +  transformation on programs:
  11.164 +*}
  11.165 +lemma unfold_while:
  11.166 +  "(\<WHILE> b \<DO> c) \<sim> (\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>)" (is "?w \<sim> ?if")
  11.167 +proof -
  11.168 +  -- "to show the equivalence, we look at the derivation tree for"
  11.169 +  -- "each side and from that construct a derivation tree for the other side"  
  11.170 +  { fix s s' assume w: "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'"
  11.171 +    -- "as a first thing we note that, if @{text b} is @{text False} in state @{text s},"
  11.172 +    -- "then both statements do nothing:"
  11.173 +    hence "\<not>b s \<Longrightarrow> s = s'" by simp
  11.174 +    hence "\<not>b s \<Longrightarrow> \<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'" by simp
  11.175 +    moreover
  11.176 +    -- "on the other hand, if @{text b} is @{text True} in state @{text s},"
  11.177 +    -- {* then only the @{text WhileTrue} rule can have been used to derive @{text "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'"} *}
  11.178 +    { assume b: "b s"
  11.179 +      with w obtain s'' where
  11.180 +        "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s''" and "\<langle>?w, s''\<rangle> \<longrightarrow>\<^sub>c s'" by (cases set: evalc) auto
  11.181 +      -- "now we can build a derivation tree for the @{text \<IF>}"
  11.182 +      -- "first, the body of the True-branch:"
  11.183 +      hence "\<langle>c; ?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by (rule Semi)
  11.184 +      -- "then the whole @{text \<IF>}"
  11.185 +      with b have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'" by (rule IfTrue)
  11.186 +    }
  11.187 +    ultimately 
  11.188 +    -- "both cases together give us what we want:"      
  11.189 +    have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
  11.190 +  }
  11.191 +  moreover
  11.192 +  -- "now the other direction:"
  11.193 +  { fix s s' assume if: "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'"
  11.194 +    -- "again, if @{text b} is @{text False} in state @{text s}, then the False-branch"
  11.195 +    -- "of the @{text \<IF>} is executed, and both statements do nothing:"
  11.196 +    hence "\<not>b s \<Longrightarrow> s = s'" by simp
  11.197 +    hence "\<not>b s \<Longrightarrow> \<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by simp
  11.198 +    moreover
  11.199 +    -- "on the other hand, if @{text b} is @{text True} in state @{text s},"
  11.200 +    -- {* then this time only the @{text IfTrue} rule can have be used *}
  11.201 +    { assume b: "b s"
  11.202 +      with if have "\<langle>c; ?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by (cases set: evalc) auto
  11.203 +      -- "and for this, only the Semi-rule is applicable:"
  11.204 +      then obtain s'' where
  11.205 +        "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s''" and "\<langle>?w, s''\<rangle> \<longrightarrow>\<^sub>c s'" by (cases set: evalc) auto
  11.206 +      -- "with this information, we can build a derivation tree for the @{text \<WHILE>}"
  11.207 +      with b
  11.208 +      have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by (rule WhileTrue) 
  11.209 +    }
  11.210 +    ultimately 
  11.211 +    -- "both cases together again give us what we want:"
  11.212 +    have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
  11.213 +  }
  11.214 +  ultimately
  11.215 +  show ?thesis by blast
  11.216 +qed
  11.217 +
  11.218 +
  11.219 +subsection "Execution is deterministic"
  11.220  
  11.221 -    IfFalse "[| ~b s; <c1,s> -c-> s1 |] 
  11.222 -             ==> <IF b THEN c0 ELSE c1, s> -c-> s1"
  11.223 +text {*
  11.224 +The following proof presents all the details:
  11.225 +*}
  11.226 +theorem com_det: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<and> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<longrightarrow> u=t"
  11.227 +proof clarify -- "transform the goal into canonical form"
  11.228 +  assume "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
  11.229 +  thus "\<And>u. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u=t" 
  11.230 +  proof (induct set: evalc)
  11.231 +    fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u"
  11.232 +    thus "u = s" by simp
  11.233 +  next
  11.234 +    fix a s x u assume "\<langle>x :== a,s\<rangle> \<longrightarrow>\<^sub>c u"
  11.235 +    thus "u = s[x \<mapsto> a s]" by simp      
  11.236 +  next
  11.237 +    fix c0 c1 s s1 s2 u
  11.238 +    assume IH0: "\<And>u. \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2"
  11.239 +    assume IH1: "\<And>u. \<langle>c1,s2\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
  11.240 +
  11.241 +    assume "\<langle>c0;c1, s\<rangle> \<longrightarrow>\<^sub>c u"
  11.242 +    then obtain s' where
  11.243 +      c0: "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c s'" and
  11.244 +      c1: "\<langle>c1,s'\<rangle> \<longrightarrow>\<^sub>c u" 
  11.245 +      by auto
  11.246 +
  11.247 +    from c0 IH0 have "s'=s2" by blast
  11.248 +    with c1 IH1 show "u=s1" by blast
  11.249 +  next
  11.250 +    fix b c0 c1 s s1 u
  11.251 +    assume IH: "\<And>u. \<langle>c0,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1" 
  11.252 +
  11.253 +    assume "b s" and "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>c u"
  11.254 +    hence "\<langle>c0, s\<rangle> \<longrightarrow>\<^sub>c u" by simp
  11.255 +    with IH show "u = s1" by blast
  11.256 +  next
  11.257 +    fix b c0 c1 s s1 u
  11.258 +    assume IH: "\<And>u. \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1" 
  11.259  
  11.260 -    WhileFalse "~b s ==> <WHILE b DO c,s> -c-> s"
  11.261 +    assume "\<not>b s" and "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>c u"
  11.262 +    hence "\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>c u" by simp
  11.263 +    with IH show "u = s1" by blast
  11.264 +  next
  11.265 +    fix b c s u
  11.266 +    assume "\<not>b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u"
  11.267 +    thus "u = s" by simp
  11.268 +  next
  11.269 +    fix b c s s1 s2 u
  11.270 +    assume "IH\<^sub>c": "\<And>u. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2"
  11.271 +    assume "IH\<^sub>w": "\<And>u. \<langle>\<WHILE> b \<DO> c,s2\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
  11.272 +    
  11.273 +    assume "b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u"
  11.274 +    then obtain s' where
  11.275 +      c: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" and
  11.276 +      w: "\<langle>\<WHILE> b \<DO> c,s'\<rangle> \<longrightarrow>\<^sub>c u" 
  11.277 +      by auto
  11.278 +    
  11.279 +    from c "IH\<^sub>c" have "s' = s2" by blast
  11.280 +    with w "IH\<^sub>w" show "u = s1" by blast
  11.281 +  qed
  11.282 +qed
  11.283 +
  11.284  
  11.285 -    WhileTrue  "[| b s;  <c,s> -c-> s2;  <WHILE b DO c, s2> -c-> s1 |] 
  11.286 -               ==> <WHILE b DO c, s> -c-> s1"
  11.287 +text {*
  11.288 +  This is the proof as you might present it in a lecture. The remaining
  11.289 +  cases are simple enough to be proved automatically: 
  11.290 +*} 
  11.291 +theorem "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<and> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<longrightarrow> u=t" 
  11.292 +proof clarify
  11.293 +  assume "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
  11.294 +  thus "\<And>u. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u=t" 
  11.295 +  proof (induct set: evalc)
  11.296 +    -- "the simple @{text \<SKIP>} case for demonstration:"
  11.297 +    fix s u assume "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c u"
  11.298 +    thus "u = s" by simp
  11.299 +  next
  11.300 +    -- "and the only really interesting case, @{text \<WHILE>}:"
  11.301 +    fix b c s s1 s2 u
  11.302 +    assume "IH\<^sub>c": "\<And>u. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s2"
  11.303 +    assume "IH\<^sub>w": "\<And>u. \<langle>\<WHILE> b \<DO> c,s2\<rangle> \<longrightarrow>\<^sub>c u \<Longrightarrow> u = s1"
  11.304 +    
  11.305 +    assume "b s" and "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>c u"
  11.306 +    then obtain s' where
  11.307 +      c: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" and
  11.308 +      w: "\<langle>\<WHILE> b \<DO> c,s'\<rangle> \<longrightarrow>\<^sub>c u"
  11.309 +      by auto
  11.310 +    
  11.311 +    from c "IH\<^sub>c" have "s' = s2" by blast
  11.312 +    with w "IH\<^sub>w" show "u = s1" by blast
  11.313 +  qed (best dest: evalc_cases [THEN iffD1])+ -- "prove the rest automatically"
  11.314 +qed
  11.315  
  11.316  end
    12.1 --- a/src/HOL/IMP/Transition.ML	Sun Dec 09 14:35:11 2001 +0100
    12.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.3 @@ -1,227 +0,0 @@
    12.4 -(*  Title:      HOL/IMP/Transition.ML
    12.5 -    ID:         $Id$
    12.6 -    Author:     Tobias Nipkow & Robert Sandner, TUM
    12.7 -    Copyright   1996 TUM
    12.8 -
    12.9 -Equivalence of Natural and Transition semantics
   12.10 -*)
   12.11 -
   12.12 -section "Winskel's Proof";
   12.13 -
   12.14 -AddSEs [rel_pow_0_E];
   12.15 -
   12.16 -val evalc1_SEs = 
   12.17 -    map evalc1.mk_cases
   12.18 -       ["(SKIP,s) -1-> t", 
   12.19 -	"(x:==a,s) -1-> t",
   12.20 -	"(c1;c2, s) -1-> t", 
   12.21 -	"(IF b THEN c1 ELSE c2, s) -1-> t",
   12.22 -        "(WHILE b DO c, s) -1-> t"];
   12.23 -
   12.24 -val evalc1_E = evalc1.mk_cases "(WHILE b DO c,s) -1-> t";
   12.25 -
   12.26 -AddSEs evalc1_SEs;
   12.27 -
   12.28 -AddIs evalc1.intrs;
   12.29 -
   12.30 -Goal "!s t u c d. (c,s) -n-> (SKIP,t) --> (d,t) -*-> (SKIP,u) --> \
   12.31 -\              (c;d, s) -*-> (SKIP, u)";
   12.32 -by (induct_tac "n" 1);
   12.33 - by (fast_tac (claset() addIs [rtrancl_into_rtrancl2])1);
   12.34 -by (fast_tac  (claset() addIs [rtrancl_into_rtrancl2]addSDs [rel_pow_Suc_D2])1);
   12.35 -qed_spec_mp "lemma1";
   12.36 -
   12.37 -Goal "<c,s> -c-> s1 ==> (c,s) -*-> (SKIP,s1)";
   12.38 -by (etac evalc.induct 1);
   12.39 -
   12.40 -(* SKIP *)
   12.41 -by (rtac rtrancl_refl 1);
   12.42 -
   12.43 -(* ASSIGN *)
   12.44 -by (fast_tac (claset() addSIs [r_into_rtrancl]) 1);
   12.45 -
   12.46 -(* SEMI *)
   12.47 -by (fast_tac (claset() addDs [rtrancl_imp_UN_rel_pow] addIs [lemma1]) 1);
   12.48 -
   12.49 -(* IF *)
   12.50 -by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
   12.51 -by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
   12.52 -
   12.53 -(* WHILE *)
   12.54 -by (fast_tac (claset() addSIs [r_into_rtrancl]) 1);
   12.55 -by (fast_tac (claset() addDs [rtrancl_imp_UN_rel_pow]
   12.56 -                        addIs [rtrancl_into_rtrancl2,lemma1]) 1);
   12.57 -
   12.58 -qed "evalc_impl_evalc1";
   12.59 -
   12.60 -
   12.61 -Goal "(SKIP,s) -m-> (SKIP,t) ==> s = t & m = 0";
   12.62 -by (etac rel_pow_E2 1);
   12.63 -by (Asm_full_simp_tac 1);
   12.64 -by (Fast_tac 1);
   12.65 -val hlemma = result();
   12.66 -
   12.67 -Goal "!c d s u. (c;d,s) -n-> (SKIP,u) --> \
   12.68 -\            (? t m. (c,s) -*-> (SKIP,t) & (d,t) -m-> (SKIP,u) & m <= n)";
   12.69 -by (induct_tac "n" 1);
   12.70 - (* case n = 0 *)
   12.71 - by (fast_tac (claset() addss simpset()) 1);
   12.72 -(* induction step *)
   12.73 -by (fast_tac (claset() addSIs [le_SucI,le_refl]
   12.74 -                     addSDs [rel_pow_Suc_D2]
   12.75 -                     addSEs [rel_pow_imp_rtrancl,rtrancl_into_rtrancl2]) 1);
   12.76 -qed_spec_mp "lemma2";
   12.77 -
   12.78 -Goal "!s t. (c,s) -*-> (SKIP,t) --> <c,s> -c-> t";
   12.79 -by (induct_tac "c" 1);
   12.80 -by (safe_tac (claset() addSDs [rtrancl_imp_UN_rel_pow]));
   12.81 -
   12.82 -(* SKIP *)
   12.83 -by (fast_tac (claset() addSEs [rel_pow_E2]) 1);
   12.84 -
   12.85 -(* ASSIGN *)
   12.86 -by (fast_tac (claset() addSDs [hlemma]  addSEs [rel_pow_E2]) 1);
   12.87 -
   12.88 -(* SEMI *)
   12.89 -by (fast_tac (claset() addSDs [lemma2,rel_pow_imp_rtrancl]) 1);
   12.90 -
   12.91 -(* IF *)
   12.92 -by (etac rel_pow_E2 1);
   12.93 -by (Asm_full_simp_tac 1);
   12.94 -by (fast_tac (claset() addSDs [rel_pow_imp_rtrancl]) 1);
   12.95 -
   12.96 -(* WHILE, induction on the length of the computation *)
   12.97 -by (eres_inst_tac [("P","?X -n-> ?Y")] rev_mp 1);
   12.98 -by (res_inst_tac [("x","s")] spec 1);
   12.99 -by (induct_thm_tac nat_less_induct "n" 1);
  12.100 -by (strip_tac 1);
  12.101 -by (etac rel_pow_E2 1);
  12.102 - by (Asm_full_simp_tac 1);
  12.103 -by (etac evalc1_E 1);
  12.104 -
  12.105 -(* WhileFalse *)
  12.106 - by (fast_tac (claset() addSDs [hlemma]) 1);
  12.107 -
  12.108 -(* WhileTrue *)
  12.109 -by (fast_tac(claset() addSDs[lemma2,le_imp_less_or_eq,less_Suc_eq RS iffD2])1);
  12.110 -
  12.111 -qed_spec_mp "evalc1_impl_evalc";
  12.112 -
  12.113 -
  12.114 -(**** proof of the equivalence of evalc and evalc1 ****)
  12.115 -
  12.116 -Goal "((c, s) -*-> (SKIP, t)) = (<c,s> -c-> t)";
  12.117 -by (fast_tac (HOL_cs addSEs [evalc1_impl_evalc,evalc_impl_evalc1]) 1);
  12.118 -qed "evalc1_eq_evalc";
  12.119 -
  12.120 -
  12.121 -section "A Proof Without -n->";
  12.122 -
  12.123 -Goal "(c1,s1) -*-> (SKIP,s2) ==> \
  12.124 -\ (c2,s2) -*-> cs3 --> (c1;c2,s1) -*-> cs3";
  12.125 -by (etac converse_rtrancl_induct2 1);
  12.126 -by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
  12.127 -by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
  12.128 -qed_spec_mp "my_lemma1";
  12.129 -
  12.130 -
  12.131 -Goal "<c,s> -c-> s1 ==> (c,s) -*-> (SKIP,s1)";
  12.132 -by (etac evalc.induct 1);
  12.133 -
  12.134 -(* SKIP *)
  12.135 -by (rtac rtrancl_refl 1);
  12.136 -
  12.137 -(* ASSIGN *)
  12.138 -by (fast_tac (claset() addSIs [r_into_rtrancl]) 1);
  12.139 -
  12.140 -(* SEMI *)
  12.141 -by (fast_tac (claset() addIs [my_lemma1]) 1);
  12.142 -
  12.143 -(* IF *)
  12.144 -by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
  12.145 -by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
  12.146 -
  12.147 -(* WHILE *)
  12.148 -by (fast_tac (claset() addSIs [r_into_rtrancl]) 1);
  12.149 -by (fast_tac (claset() addIs [rtrancl_into_rtrancl2,my_lemma1]) 1);
  12.150 -
  12.151 -qed "evalc_impl_evalc1";
  12.152 -
  12.153 -(* The opposite direction is based on a Coq proof done by Ranan Fraer and
  12.154 -   Yves Bertot. The following sketch is from an email by Ranan Fraer.
  12.155 -*)
  12.156 -(*
  12.157 -First we've broke it into 2 lemmas:
  12.158 -
  12.159 -Lemma 1
  12.160 -((c,s) --> (SKIP,t)) => (<c,s> -c-> t)
  12.161 -
  12.162 -This is a quick one, dealing with the cases skip, assignment
  12.163 -and while_false.
  12.164 -
  12.165 -Lemma 2
  12.166 -((c,s) -*-> (c',s')) /\ <c',s'> -c'-> t
  12.167 -  => 
  12.168 -<c,s> -c-> t
  12.169 -
  12.170 -This is proved by rule induction on the  -*-> relation
  12.171 -and the induction step makes use of a third lemma: 
  12.172 -
  12.173 -Lemma 3
  12.174 -((c,s) --> (c',s')) /\ <c',s'> -c'-> t
  12.175 -  => 
  12.176 -<c,s> -c-> t
  12.177 -
  12.178 -This captures the essence of the proof, as it shows that <c',s'> 
  12.179 -behaves as the continuation of <c,s> with respect to the natural
  12.180 -semantics.
  12.181 -The proof of Lemma 3 goes by rule induction on the --> relation,
  12.182 -dealing with the cases sequence1, sequence2, if_true, if_false and
  12.183 -while_true. In particular in the case (sequence1) we make use again
  12.184 -of Lemma 1.
  12.185 -*)
  12.186 -
  12.187 -(*Delsimps [update_apply];*)
  12.188 -Goal "((c,s) -1-> (c',s')) ==> (!t. <c',s'> -c-> t --> <c,s> -c-> t)";
  12.189 -by (etac evalc1.induct 1);
  12.190 -by Auto_tac;
  12.191 -qed_spec_mp "FB_lemma3";
  12.192 -(*Addsimps [update_apply];*)
  12.193 -
  12.194 -val [major] = goal Transition.thy
  12.195 -  "(c,s) -*-> (c',s') ==> <c',s'> -c-> t --> <c,s> -c-> t";
  12.196 -by (rtac (major RS rtrancl_induct2) 1);
  12.197 - by (Fast_tac 1);
  12.198 -by (fast_tac (claset() addIs [FB_lemma3]) 1);
  12.199 -qed_spec_mp "FB_lemma2";
  12.200 -
  12.201 -Goal "(c,s) -*-> (SKIP,t) ==> <c,s> -c-> t";
  12.202 -by (fast_tac (claset() addEs [FB_lemma2]) 1);
  12.203 -qed "evalc1_impl_evalc";
  12.204 -
  12.205 -
  12.206 -section "The proof in Nielson and Nielson";
  12.207 -
  12.208 -(* The more precise n=i1+i2+1 is proved by the same script but complicates
  12.209 -   life further down, where i1,i2 < n is needed.
  12.210 -*)
  12.211 -Goal "!c1 s. (c1;c2,s) -n-> (SKIP,t) --> \
  12.212 -\     (? i1 i2 u. (c1,s) -i1-> (SKIP,u) & (c2,u) -i2-> (SKIP,t) & i1<n & i2<n)";
  12.213 -by (induct_tac "n" 1);
  12.214 - by (Fast_tac 1);
  12.215 -by (fast_tac (claset() addSIs [rel_pow_0_I,rel_pow_Suc_I2]
  12.216 -                      addSDs [rel_pow_Suc_D2] addss simpset()) 1);
  12.217 -qed_spec_mp "comp_decomp_lemma";
  12.218 -
  12.219 -Goal "!c s t. (c,s) -n-> (SKIP,t) --> <c,s> -c-> t";
  12.220 -by (induct_thm_tac nat_less_induct "n" 1);
  12.221 -by (Clarify_tac 1);
  12.222 -by (etac rel_pow_E2 1);
  12.223 - by (asm_full_simp_tac (simpset() addsimps evalc.intrs) 1);
  12.224 -by (case_tac "c" 1);
  12.225 -    by (Fast_tac 1);
  12.226 -   by (Blast_tac 1);
  12.227 -  by (blast_tac (claset() addSDs [rel_pow_Suc_I2 RS comp_decomp_lemma]) 1);
  12.228 - by (Blast_tac 1);
  12.229 -by (Blast_tac 1);
  12.230 -qed_spec_mp "evalc1_impl_evalc";
    13.1 --- a/src/HOL/IMP/Transition.thy	Sun Dec 09 14:35:11 2001 +0100
    13.2 +++ b/src/HOL/IMP/Transition.thy	Sun Dec 09 14:35:36 2001 +0100
    13.3 @@ -1,45 +1,686 @@
    13.4 -(*  Title:      HOL/IMP/Transition.thy
    13.5 -    ID:         $Id$
    13.6 -    Author:     Tobias Nipkow & Robert Sandner, TUM
    13.7 -    Copyright   1996 TUM
    13.8 -
    13.9 -Transition semantics of commands
   13.10 +(*  Title:        HOL/IMP/Transition.thy
   13.11 +    ID:           $Id$
   13.12 +    Author:       Tobias Nipkow & Robert Sandner, TUM
   13.13 +    Isar Version: Gerwin Klein, 2001
   13.14 +    Copyright     1996 TUM
   13.15  *)
   13.16  
   13.17 -Transition = Natural +
   13.18 +header "Transition Semantics of Commands"
   13.19 +
   13.20 +theory Transition = Natural:
   13.21 +
   13.22 +subsection "The transition relation"
   13.23  
   13.24 -consts  evalc1    :: "((com*state)*(com*state))set"
   13.25 +text {*
   13.26 +  We formalize the transition semantics as in \cite{Nielson}. This
   13.27 +  makes some of the rules a bit more intuitive, but also requires
   13.28 +  some more (internal) formal overhead.
   13.29 +  
   13.30 +  Since configurations that have terminated are written without 
   13.31 +  a statement, the transition relation is not 
   13.32 +  @{typ "((com \<times> state) \<times> (com \<times> state)) set"}
   13.33 +  but instead:
   13.34 +*}
   13.35 +consts evalc1 :: "((com option \<times> state) \<times> (com option \<times> state)) set"
   13.36  
   13.37 +text {*
   13.38 +  Some syntactic sugar that we will use to hide the 
   13.39 +  @{text option} part in configurations:
   13.40 +*}
   13.41  syntax
   13.42 -        "@evalc1" :: "[(com*state),(com*state)] => bool"
   13.43 -                                ("_ -1-> _" [81,81] 100)
   13.44 -        "@evalcn" :: "[(com*state),nat,(com*state)] => bool"
   13.45 -                                ("_ -_-> _" [81,81] 100)
   13.46 -        "@evalc*" :: "[(com*state),(com*state)] => bool"
   13.47 -                                ("_ -*-> _" [81,81] 100)
   13.48 +  "@angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("<_,_>")
   13.49 +  "@angle2" :: "state \<Rightarrow> com option \<times> state" ("<_>")
   13.50 +
   13.51 +syntax (xsymbols)
   13.52 +  "@angle" :: "[com, state] \<Rightarrow> com option \<times> state" ("\<langle>_,_\<rangle>")
   13.53 +  "@angle2" :: "state \<Rightarrow> com option \<times> state" ("\<langle>_\<rangle>")
   13.54 +
   13.55 +translations
   13.56 +  "\<langle>c,s\<rangle>" == "(Some c, s)"
   13.57 +  "\<langle>s\<rangle>" == "(None, s)"
   13.58 +
   13.59 +text {*
   13.60 +  More syntactic sugar for the transition relation, and its
   13.61 +  iteration.
   13.62 +*}
   13.63 +syntax
   13.64 +  "@evalc1" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
   13.65 +    ("_ -1-> _" [81,81] 100)
   13.66 +  "@evalcn" :: "[(com option\<times>state),nat,(com option\<times>state)] \<Rightarrow> bool"
   13.67 +    ("_ -_-> _" [81,81] 100)
   13.68 +  "@evalc*" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
   13.69 +    ("_ -*-> _" [81,81] 100)
   13.70 +
   13.71 +syntax (xsymbols)
   13.72 +  "@evalc1" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
   13.73 +    ("_ \<longrightarrow>\<^sub>1 _" [81,81] 100)
   13.74 +  "@evalcn" :: "[(com option\<times>state),nat,(com option\<times>state)] \<Rightarrow> bool"
   13.75 +    ("_ -_\<rightarrow>\<^sub>1 _" [81,81] 100)
   13.76 +  "@evalc*" :: "[(com option\<times>state),(com option\<times>state)] \<Rightarrow> bool"
   13.77 +    ("_ \<longrightarrow>\<^sub>1\<^sup>* _" [81,81] 100)
   13.78  
   13.79  translations
   13.80 -  "cs0 -1-> cs1"	== "(cs0,cs1) : evalc1"
   13.81 -  "cs0 -1-> (c1,s1)"	== "(cs0,c1,s1) : evalc1"
   13.82 +  "cs \<longrightarrow>\<^sub>1 cs'" == "(cs,cs') \<in> evalc1"
   13.83 +  "cs -n\<rightarrow>\<^sub>1 cs'" == "(cs,cs') \<in> evalc1^n" 
   13.84 +  "cs \<longrightarrow>\<^sub>1\<^sup>* cs'" == "(cs,cs') \<in> evalc1^*" 
   13.85 +
   13.86 +  -- {* Isabelle converts @{text "(cs0,(c1,s1))"} to @{term "(cs0,c1,s1)"}, 
   13.87 +        so we also include: *}
   13.88 +  "cs0 \<longrightarrow>\<^sub>1 (c1,s1)" == "(cs0,c1,s1) \<in> evalc1"   
   13.89 +  "cs0 -n\<rightarrow>\<^sub>1 (c1,s1)" == "(cs0,c1,s1) \<in> evalc1^n"
   13.90 +  "cs0 \<longrightarrow>\<^sub>1\<^sup>* (c1,s1)" == "(cs0,c1,s1) \<in> evalc1^*" 
   13.91 +
   13.92 +text {*
   13.93 +  Now, finally, we are set to write down the rules for our small step semantics:
   13.94 +*}
   13.95 +inductive evalc1
   13.96 +  intros
   13.97 +  Skip:    "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s\<rangle>"  
   13.98 +  Assign:  "\<langle>x :== a, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s[x \<mapsto> a s]\<rangle>"
   13.99 +
  13.100 +  Semi1:   "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> \<langle>c0;c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1,s'\<rangle>"
  13.101 +  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>"
  13.102 +
  13.103 +  IfTrue:  "b s \<Longrightarrow> \<langle>\<IF> b \<THEN> c1 \<ELSE> c2,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1,s\<rangle>"
  13.104 +  IfFalse: "\<not>b s \<Longrightarrow> \<langle>\<IF> b \<THEN> c1 \<ELSE> c2,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c2,s\<rangle>"
  13.105 +
  13.106 +  While:   "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>,s\<rangle>"
  13.107 +
  13.108 +lemmas [intro] = evalc1.intros -- "again, use these rules in automatic proofs"
  13.109 +
  13.110 +(*<*)
  13.111 +(* fixme: move to Relation_Power.thy *)
  13.112 +lemma rel_pow_Suc_E2 [elim!]:
  13.113 +  "[| (x, z) \<in> R ^ Suc n; !!y. [| (x, y) \<in> R; (y, z) \<in> R ^ n |] ==> P |] ==> P"
  13.114 +  by (drule rel_pow_Suc_D2) blast
  13.115 +
  13.116 +lemma rtrancl_imp_rel_pow: "p \<in> R^* \<Longrightarrow> \<exists>n. p \<in> R^n"
  13.117 +proof -
  13.118 +  assume "p \<in> R\<^sup>*"
  13.119 +  moreover obtain x y where p: "p = (x,y)" by (cases p)
  13.120 +  ultimately have "(x,y) \<in> R\<^sup>*" by hypsubst
  13.121 +  hence "\<exists>n. (x,y) \<in> R^n"
  13.122 +  proof induct
  13.123 +    fix a have "(a,a) \<in> R^0" by simp
  13.124 +    thus "\<exists>n. (a,a) \<in> R ^ n" ..
  13.125 +  next
  13.126 +    fix a b c assume "\<exists>n. (a,b) \<in> R ^ n"
  13.127 +    then obtain n where "(a,b) \<in> R^n" ..
  13.128 +    moreover assume "(b,c) \<in> R"
  13.129 +    ultimately have "(a,c) \<in> R^(Suc n)" by auto
  13.130 +    thus "\<exists>n. (a,c) \<in> R^n" ..
  13.131 +  qed
  13.132 +  with p show ?thesis by hypsubst
  13.133 +qed  
  13.134 +(*>*)    
  13.135 +text {*
  13.136 +  As for the big step semantics you can read these rules in a 
  13.137 +  syntax directed way:
  13.138 +*}
  13.139 +lemma SKIP_1: "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 y = (y = \<langle>s\<rangle>)" 
  13.140 +  by (rule, cases set: evalc1, auto)      
  13.141 +
  13.142 +lemma Assign_1: "\<langle>x :== a, s\<rangle> \<longrightarrow>\<^sub>1 y = (y = \<langle>s[x \<mapsto> a s]\<rangle>)"
  13.143 +  by (rule, cases set: evalc1, auto)
  13.144 +
  13.145 +lemma Cond_1: 
  13.146 +  "\<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>))"
  13.147 +  by (rule, cases set: evalc1, auto)
  13.148 +
  13.149 +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>)"
  13.150 +  by (rule, cases set: evalc1, auto)
  13.151 +
  13.152 +lemmas [simp] = SKIP_1 Assign_1 Cond_1 While_1
  13.153 +
  13.154 +
  13.155 +subsection "Examples"
  13.156 +
  13.157 +lemma 
  13.158 +  "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>"
  13.159 +  (is "_ \<Longrightarrow> \<langle>?w, _\<rangle> \<longrightarrow>\<^sub>1\<^sup>* _")
  13.160 +proof -
  13.161 +  let ?x  = "x:== \<lambda>s. s x+1"
  13.162 +  let ?if = "\<IF> \<lambda>s. s x \<noteq> 1 \<THEN> ?x; ?w \<ELSE> \<SKIP>"
  13.163 +  assume [simp]: "s x = 0"
  13.164 +  have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1  \<langle>?if, s\<rangle>" ..
  13.165 +  also have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?x; ?w, s\<rangle>" by simp 
  13.166 +  also have "\<langle>?x; ?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 1]\<rangle>" by (rule Semi1, simp)
  13.167 +  also have "\<langle>?w, s[x \<mapsto> 1]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s[x \<mapsto> 1]\<rangle>" ..
  13.168 +  also have "\<langle>?if, s[x \<mapsto> 1]\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<SKIP>, s[x \<mapsto> 1]\<rangle>" by (simp add: update_def)
  13.169 +  also have "\<langle>\<SKIP>, s[x \<mapsto> 1]\<rangle> \<longrightarrow>\<^sub>1 \<langle>s[x \<mapsto> 1]\<rangle>" ..
  13.170 +  finally show ?thesis ..
  13.171 +qed
  13.172  
  13.173 -  "cs0 -n-> cs1" 	== "(cs0,cs1) : evalc1^n"
  13.174 -  "cs0 -n-> (c1,s1)" 	== "(cs0,c1,s1) : evalc1^n"
  13.175 +lemma 
  13.176 +  "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'"
  13.177 +  (is "_ \<Longrightarrow> \<langle>?w, _\<rangle> \<longrightarrow>\<^sub>1\<^sup>* s'")
  13.178 +proof -
  13.179 +  let ?c = "x:== \<lambda>s. s x+1"
  13.180 +  let ?if = "\<IF> \<lambda>s. s x \<noteq> 1 \<THEN> ?c; ?w \<ELSE> \<SKIP>"  
  13.181 +  assume [simp]: "s x = 2"
  13.182 +  note update_def [simp]
  13.183 +  have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1  \<langle>?if, s\<rangle>" ..
  13.184 +  also have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?c; ?w, s\<rangle>" by simp
  13.185 +  also have "\<langle>?c; ?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 3]\<rangle>" by (rule Semi1, simp)
  13.186 +  also have "\<langle>?w, s[x \<mapsto> 3]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s[x \<mapsto> 3]\<rangle>" ..
  13.187 +  also have "\<langle>?if, s[x \<mapsto> 3]\<rangle> \<longrightarrow>\<^sub>1  \<langle>?c; ?w, s[x \<mapsto> 3]\<rangle>" by simp
  13.188 +  also have "\<langle>?c; ?w, s[x \<mapsto> 3]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 4]\<rangle>" by (rule Semi1, simp)
  13.189 +  also have "\<langle>?w, s[x \<mapsto> 4]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s[x \<mapsto> 4]\<rangle>" ..
  13.190 +  also have "\<langle>?if, s[x \<mapsto> 4]\<rangle> \<longrightarrow>\<^sub>1  \<langle>?c; ?w, s[x \<mapsto> 4]\<rangle>" by simp
  13.191 +  also have "\<langle>?c; ?w, s[x \<mapsto> 4]\<rangle> \<longrightarrow>\<^sub>1 \<langle>?w, s[x \<mapsto> 5]\<rangle>" by (rule Semi1, simp) 
  13.192 +  oops
  13.193 +
  13.194 +subsection "Basic properties"
  13.195 +
  13.196 +text {* 
  13.197 +  There are no \emph{stuck} programs:
  13.198 +*}
  13.199 +lemma no_stuck: "\<exists>y. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1 y"
  13.200 +proof (induct c)
  13.201 +  -- "case Semi:"
  13.202 +  fix c1 c2 assume "\<exists>y. \<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1 y" 
  13.203 +  then obtain y where "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1 y" ..
  13.204 +  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>"
  13.205 +    by (cases y, cases "fst y", auto)
  13.206 +  thus "\<exists>s'. \<langle>c1;c2,s\<rangle> \<longrightarrow>\<^sub>1 s'" by auto
  13.207 +next
  13.208 +  -- "case If:"
  13.209 +  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"
  13.210 +  thus "\<exists>y. \<langle>\<IF> b \<THEN> c1 \<ELSE> c2, s\<rangle> \<longrightarrow>\<^sub>1 y" by (cases "b s") auto
  13.211 +qed auto -- "the rest is trivial"
  13.212 +
  13.213 +text {*
  13.214 +  If a configuration does not contain a statement, the program
  13.215 +  has terminated and there is no next configuration:
  13.216 +*}
  13.217 +lemma stuck [dest]: "(None, s) \<longrightarrow>\<^sub>1 y \<Longrightarrow> False" by (auto elim: evalc1.elims)
  13.218 +
  13.219 +(*<*)
  13.220 +(* fixme: relpow.simps don't work *)
  13.221 +lemma rel_pow_0 [simp]: "!!R::('a*'a) set. R^0 = Id" by simp
  13.222 +lemma rel_pow_Suc_0 [simp]: "!!R::('a*'a) set. R^(Suc 0) = R" by simp 
  13.223 +lemmas [simp del] = relpow.simps
  13.224 +(*>*)
  13.225 +
  13.226 +lemma evalc_None_0 [simp]: "\<langle>s\<rangle> -n\<rightarrow>\<^sub>1 y = (n = 0 \<and> y = \<langle>s\<rangle>)"
  13.227 +  by (cases n) auto
  13.228  
  13.229 -  "cs0 -*-> cs1" 	== "(cs0,cs1) : evalc1^*"
  13.230 -  "cs0 -*-> (c1,s1)" 	== "(cs0,c1,s1) : evalc1^*"
  13.231 +lemma SKIP_n: "\<langle>\<SKIP>, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle> \<Longrightarrow> s' = s \<and> n=1" 
  13.232 +  by (cases n) auto
  13.233 +
  13.234 +subsection "Equivalence to natural semantics (after Nielson and Nielson)"
  13.235 +
  13.236 +text {*
  13.237 +  We first need two lemmas about semicolon statements:
  13.238 +  decomposition and composition.
  13.239 +*}
  13.240 +lemma semiD:
  13.241 +  "\<And>c1 c2 s s''. \<langle>c1; c2, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle> \<Longrightarrow> 
  13.242 +  \<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"
  13.243 +  (is "PROP ?P n")
  13.244 +proof (induct n)
  13.245 +  show "PROP ?P 0" by simp
  13.246 +next
  13.247 +  fix n assume IH: "PROP ?P n"
  13.248 +  show "PROP ?P (Suc n)"
  13.249 +  proof -
  13.250 +    fix c1 c2 s s''
  13.251 +    assume "\<langle>c1; c2, s\<rangle> -Suc n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>"
  13.252 +    then obtain y where
  13.253 +      1: "\<langle>c1; c2, s\<rangle> \<longrightarrow>\<^sub>1 y" and
  13.254 +      n: "y -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>"
  13.255 +      by blast
  13.256 +
  13.257 +    from 1
  13.258 +    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"
  13.259 +      (is "\<exists>i j s'. ?Q i j s'")
  13.260 +    proof (cases set: evalc1)
  13.261 +      case Semi1
  13.262 +      then obtain s' where
  13.263 +        "y = \<langle>c2, s'\<rangle>" and "\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'\<rangle>"
  13.264 +        by auto
  13.265 +      with 1 n have "?Q 1 n s'" by simp
  13.266 +      thus ?thesis by blast
  13.267 +    next
  13.268 +      case Semi2
  13.269 +      then obtain c1' s' where
  13.270 +        y:  "y = \<langle>c1'; c2, s'\<rangle>" and
  13.271 +        c1: "\<langle>c1, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1', s'\<rangle>"
  13.272 +        by auto
  13.273 +      with n have "\<langle>c1'; c2, s'\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by simp 
  13.274 +      with IH obtain i j s0 where 
  13.275 +        c1': "\<langle>c1',s'\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s0\<rangle>" and
  13.276 +        c2:  "\<langle>c2,s0\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" and
  13.277 +        i:   "n = i+j"
  13.278 +        by blast
  13.279 +          
  13.280 +      from c1 c1'
  13.281 +      have "\<langle>c1,s\<rangle> -(i+1)\<rightarrow>\<^sub>1 \<langle>s0\<rangle>" by (auto simp del: relpow.simps intro: rel_pow_Suc_I2)
  13.282 +      with c2 i
  13.283 +      have "?Q (i+1) j s0" by simp
  13.284 +      thus ?thesis by blast
  13.285 +    qed auto -- "the remaining cases cannot occur"
  13.286 +  qed
  13.287 +qed
  13.288  
  13.289  
  13.290 -inductive evalc1
  13.291 -  intrs
  13.292 -    Assign "(x :== a,s) -1-> (SKIP,s[x ::= a s])"
  13.293 +lemma semiI: 
  13.294 +  "\<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>"
  13.295 +proof (induct n)
  13.296 +  fix c0 s s'' assume "\<langle>c0,s\<rangle> -(0::nat)\<rightarrow>\<^sub>1 \<langle>s''\<rangle>"
  13.297 +  hence False by simp
  13.298 +  thus "?thesis c0 s s''" ..
  13.299 +next
  13.300 +  fix c0 s s'' n 
  13.301 +  assume c0: "\<langle>c0,s\<rangle> -Suc n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>"
  13.302 +  assume c1: "\<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
  13.303 +  assume IH: "\<And>c0 s s''.
  13.304 +    \<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>"
  13.305 +  from c0 obtain y where 
  13.306 +    1: "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1 y" and n: "y -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by blast
  13.307 +  from 1 obtain c0' s0' where
  13.308 +    "y = \<langle>s0'\<rangle> \<or> y = \<langle>c0', s0'\<rangle>" 
  13.309 +    by (cases y, cases "fst y", auto)
  13.310 +  moreover
  13.311 +  { assume y: "y = \<langle>s0'\<rangle>"
  13.312 +    with n have "s'' = s0'" by simp
  13.313 +    with y 1 have "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1, s''\<rangle>" by blast
  13.314 +    with c1 have "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (blast intro: rtrancl_trans)
  13.315 +  }
  13.316 +  moreover
  13.317 +  { assume y: "y = \<langle>c0', s0'\<rangle>"
  13.318 +    with n have "\<langle>c0', s0'\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by blast
  13.319 +    with IH c1 have "\<langle>c0'; c1,s0'\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by blast
  13.320 +    moreover
  13.321 +    from y 1 have "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c0'; c1,s0'\<rangle>" by blast
  13.322 +    hence "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c0'; c1,s0'\<rangle>" by blast
  13.323 +    ultimately
  13.324 +    have "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (blast intro: rtrancl_trans)
  13.325 +  }
  13.326 +  ultimately
  13.327 +  show "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by blast
  13.328 +qed
  13.329 +
  13.330 +text {*
  13.331 +  The easy direction of the equivalence proof:
  13.332 +*}
  13.333 +lemma evalc_imp_evalc1: 
  13.334 +  "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s' \<Longrightarrow> \<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
  13.335 +proof -
  13.336 +  assume "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
  13.337 +  thus "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
  13.338 +  proof induct
  13.339 +    fix s show "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" by auto
  13.340 +  next
  13.341 +    fix x a s show "\<langle>x :== a ,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s[x\<mapsto>a s]\<rangle>" by auto
  13.342 +  next
  13.343 +    fix c0 c1 s s'' s'
  13.344 +    assume "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s''\<rangle>"
  13.345 +    then obtain n where "\<langle>c0,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by (blast dest: rtrancl_imp_rel_pow)
  13.346 +    moreover
  13.347 +    assume "\<langle>c1,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
  13.348 +    ultimately
  13.349 +    show "\<langle>c0; c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (rule semiI)
  13.350 +  next
  13.351 +    fix s::state and b c0 c1 s'
  13.352 +    assume "b s"
  13.353 +    hence "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c0,s\<rangle>" by simp
  13.354 +    also assume "\<langle>c0,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" 
  13.355 +    finally show "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" .
  13.356 +  next
  13.357 +    fix s::state and b c0 c1 s'
  13.358 +    assume "\<not>b s"
  13.359 +    hence "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c1,s\<rangle>" by simp
  13.360 +    also assume "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
  13.361 +    finally show "\<langle>\<IF> b \<THEN> c0 \<ELSE> c1,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" .
  13.362 +  next
  13.363 +    fix b c and s::state
  13.364 +    assume b: "\<not>b s"
  13.365 +    let ?if = "\<IF> b \<THEN> c; \<WHILE> b \<DO> c \<ELSE> \<SKIP>"
  13.366 +    have "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s\<rangle>" by blast
  13.367 +    also have "\<langle>?if,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<SKIP>, s\<rangle>" by (simp add: b)
  13.368 +    also have "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s\<rangle>" by blast
  13.369 +    finally show "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" ..
  13.370 +  next
  13.371 +    fix b c s s'' s'
  13.372 +    let ?w  = "\<WHILE> b \<DO> c"
  13.373 +    let ?if = "\<IF> b \<THEN> c; ?w \<ELSE> \<SKIP>"
  13.374 +    assume w: "\<langle>?w,s''\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
  13.375 +    assume c: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s''\<rangle>"
  13.376 +    assume b: "b s"
  13.377 +    have "\<langle>?w,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>?if, s\<rangle>" by blast
  13.378 +    also have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c; ?w, s\<rangle>" by (simp add: b)
  13.379 +    also 
  13.380 +    from c obtain n where "\<langle>c,s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" by (blast dest: rtrancl_imp_rel_pow)
  13.381 +    with w have "\<langle>c; ?w,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by - (rule semiI)
  13.382 +    finally show "\<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" ..
  13.383 +  qed
  13.384 +qed
  13.385 +
  13.386 +text {*
  13.387 +  Finally, the equivalence theorem:
  13.388 +*}
  13.389 +theorem evalc_equiv_evalc1:
  13.390 +  "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s' = \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
  13.391 +proof
  13.392 +  assume "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'"
  13.393 +  show "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>" by (rule evalc_imp_evalc1)
  13.394 +next  
  13.395 +  assume "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s'\<rangle>"
  13.396 +  then obtain n where "\<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by (blast dest: rtrancl_imp_rel_pow)
  13.397 +  moreover
  13.398 +  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'" 
  13.399 +  proof (induct rule: nat_less_induct)
  13.400 +    fix n
  13.401 +    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')"
  13.402 +    fix c s s'
  13.403 +    assume c:  "\<langle>c, s\<rangle> -n\<rightarrow>\<^sub>1 \<langle>s'\<rangle>"
  13.404 +    then obtain m where n: "n = Suc m" by (cases n) auto
  13.405 +    with c obtain y where 
  13.406 +      c': "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1 y" and m: "y -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by blast
  13.407 +    show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" 
  13.408 +    proof (cases c)
  13.409 +      case SKIP
  13.410 +      with c n show ?thesis by auto
  13.411 +    next 
  13.412 +      case Assign
  13.413 +      with c n show ?thesis by auto
  13.414 +    next
  13.415 +      fix c1 c2 assume semi: "c = (c1; c2)"
  13.416 +      with c obtain i j s'' where
  13.417 +        c1: "\<langle>c1, s\<rangle> -i\<rightarrow>\<^sub>1 \<langle>s''\<rangle>" and
  13.418 +        c2: "\<langle>c2, s''\<rangle> -j\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" and
  13.419 +        ij: "n = i+j"
  13.420 +        by (blast dest: semiD)
  13.421 +      from c1 c2 obtain 
  13.422 +        "0 < i" and "0 < j" by (cases i, auto, cases j, auto)
  13.423 +      with ij obtain
  13.424 +        i: "i < n" and j: "j < n" by simp
  13.425 +      from c1 i IH
  13.426 +      have "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s''" by blast
  13.427 +      moreover
  13.428 +      from c2 j IH
  13.429 +      have "\<langle>c2,s''\<rangle> \<longrightarrow>\<^sub>c s'" by blast
  13.430 +      moreover
  13.431 +      note semi
  13.432 +      ultimately
  13.433 +      show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
  13.434 +    next
  13.435 +      fix b c1 c2 assume If: "c = \<IF> b \<THEN> c1 \<ELSE> c2"
  13.436 +      { assume True: "b s = True"
  13.437 +        with If c n
  13.438 +        have "\<langle>c1,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by auto      
  13.439 +        with n IH
  13.440 +        have "\<langle>c1,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
  13.441 +        with If True
  13.442 +        have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by simp        
  13.443 +      }
  13.444 +      moreover
  13.445 +      { assume False: "b s = False"
  13.446 +        with If c n
  13.447 +        have "\<langle>c2,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>" by auto      
  13.448 +        with n IH
  13.449 +        have "\<langle>c2,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
  13.450 +        with If False
  13.451 +        have "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by simp        
  13.452 +      }
  13.453 +      ultimately
  13.454 +      show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by (cases "b s") auto
  13.455 +    next
  13.456 +      fix b c' assume w: "c = \<WHILE> b \<DO> c'"
  13.457 +      with c n 
  13.458 +      have "\<langle>\<IF> b \<THEN> c'; \<WHILE> b \<DO> c' \<ELSE> \<SKIP>,s\<rangle> -m\<rightarrow>\<^sub>1 \<langle>s'\<rangle>"
  13.459 +        (is "\<langle>?if,_\<rangle> -m\<rightarrow>\<^sub>1 _") by auto
  13.460 +      with n IH
  13.461 +      have "\<langle>\<IF> b \<THEN> c'; \<WHILE> b \<DO> c' \<ELSE> \<SKIP>,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
  13.462 +      moreover note unfold_while [of b c']
  13.463 +      -- {* @{thm unfold_while [of b c']} *}
  13.464 +      ultimately      
  13.465 +      have "\<langle>\<WHILE> b \<DO> c',s\<rangle> \<longrightarrow>\<^sub>c s'" by (blast dest: equivD2)
  13.466 +      with w show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by simp
  13.467 +    qed
  13.468 +  qed
  13.469 +  ultimately
  13.470 +  show "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
  13.471 +qed
  13.472 +
  13.473 +
  13.474 +subsection "Winskel's Proof"
  13.475 +
  13.476 +declare rel_pow_0_E [elim!]
  13.477 +
  13.478 +text {*
  13.479 +  Winskel's small step rules are a bit different \cite{Winskel}; 
  13.480 +  we introduce their equivalents as derived rules:
  13.481 +*}
  13.482 +lemma whileFalse1 [intro]:
  13.483 +  "\<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>")  
  13.484 +proof -
  13.485 +  assume "\<not>b s"
  13.486 +  have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle>" ..
  13.487 +  also have "\<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<SKIP>, s\<rangle>" ..
  13.488 +  also have "\<langle>\<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s\<rangle>" ..
  13.489 +  finally show "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s\<rangle>" ..
  13.490 +qed
  13.491 +
  13.492 +lemma whileTrue1 [intro]:
  13.493 +  "b s \<Longrightarrow> \<langle>\<WHILE> b \<DO> c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;\<WHILE> b \<DO> c, s\<rangle>" 
  13.494 +  (is "_ \<Longrightarrow> \<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;?w,s\<rangle>")
  13.495 +proof -
  13.496 +  assume "b s"
  13.497 +  have "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle>" ..
  13.498 +  also have "\<langle>\<IF> b \<THEN> c;?w \<ELSE> \<SKIP>, s\<rangle> \<longrightarrow>\<^sub>1 \<langle>c;?w, s\<rangle>" ..
  13.499 +  finally show "\<langle>?w, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>c;?w,s\<rangle>" ..
  13.500 +qed
  13.501  
  13.502 -    Semi1   "(SKIP;c,s) -1-> (c,s)"     
  13.503 -    Semi2   "(c0,s) -1-> (c2,s1) ==> (c0;c1,s) -1-> (c2;c1,s1)"
  13.504 +inductive_cases evalc1_SEs: 
  13.505 +  "\<langle>\<SKIP>,s\<rangle> \<longrightarrow>\<^sub>1 t" 
  13.506 +  "\<langle>x:==a,s\<rangle> \<longrightarrow>\<^sub>1 t"
  13.507 +  "\<langle>c1;c2, s\<rangle> \<longrightarrow>\<^sub>1 t"
  13.508 +  "\<langle>\<IF> b \<THEN> c1 \<ELSE> c2, s\<rangle> \<longrightarrow>\<^sub>1 t"
  13.509 +  "\<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>1 t"
  13.510 +
  13.511 +inductive_cases evalc1_E: "\<langle>\<WHILE> b \<DO> c, s\<rangle> \<longrightarrow>\<^sub>1 t"
  13.512 +
  13.513 +declare evalc1_SEs [elim!]
  13.514 +
  13.515 +lemma evalc_impl_evalc1: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s1 \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s1\<rangle>"
  13.516 +apply (erule evalc.induct)
  13.517 +
  13.518 +-- SKIP 
  13.519 +apply blast
  13.520 +
  13.521 +-- ASSIGN 
  13.522 +apply fast
  13.523 +
  13.524 +-- SEMI 
  13.525 +apply (fast dest: rtrancl_imp_UN_rel_pow intro: semiI)
  13.526 +
  13.527 +-- IF 
  13.528 +apply (fast intro: rtrancl_into_rtrancl2)
  13.529 +apply (fast intro: rtrancl_into_rtrancl2)
  13.530 +
  13.531 +-- WHILE 
  13.532 +apply fast
  13.533 +apply (fast dest: rtrancl_imp_UN_rel_pow intro: rtrancl_into_rtrancl2 semiI)
  13.534 +
  13.535 +done
  13.536 +
  13.537 +
  13.538 +lemma lemma2 [rule_format (no_asm)]: 
  13.539 +  "\<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)"
  13.540 +apply (induct_tac "n")
  13.541 + -- "case n = 0"
  13.542 + apply fastsimp
  13.543 +-- "induction step"
  13.544 +apply (fast intro!: le_SucI le_refl dest!: rel_pow_Suc_D2 
  13.545 +            elim!: rel_pow_imp_rtrancl rtrancl_into_rtrancl2)
  13.546 +done
  13.547 +
  13.548 +lemma evalc1_impl_evalc [rule_format (no_asm)]: 
  13.549 +  "\<forall>s t. \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
  13.550 +apply (induct_tac "c")
  13.551 +apply (safe dest!: rtrancl_imp_UN_rel_pow)
  13.552 +
  13.553 +-- SKIP
  13.554 +apply (simp add: SKIP_n)
  13.555 +
  13.556 +-- ASSIGN 
  13.557 +apply (fastsimp elim: rel_pow_E2)
  13.558 +
  13.559 +-- SEMI
  13.560 +apply (fast dest!: rel_pow_imp_rtrancl lemma2)
  13.561 +
  13.562 +-- IF 
  13.563 +apply (erule rel_pow_E2)
  13.564 +apply simp
  13.565 +apply (fast dest!: rel_pow_imp_rtrancl)
  13.566 +
  13.567 +-- "WHILE, induction on the length of the computation"
  13.568 +apply (rename_tac b c s t n)
  13.569 +apply (erule_tac P = "?X -n\<rightarrow>\<^sub>1 ?Y" in rev_mp)
  13.570 +apply (rule_tac x = "s" in spec)
  13.571 +apply (induct_tac "n" rule: nat_less_induct)
  13.572 +apply (intro strip)
  13.573 +apply (erule rel_pow_E2)
  13.574 + apply simp
  13.575 +apply (erule evalc1_E)
  13.576 +
  13.577 +apply simp
  13.578 +apply (case_tac "b x")
  13.579 + -- WhileTrue
  13.580 + apply (erule rel_pow_E2)
  13.581 +  apply simp
  13.582 + apply (clarify dest!: lemma2)
  13.583 + apply (erule allE, erule allE, erule impE, assumption)
  13.584 + apply (erule_tac x=mb in allE, erule impE, fastsimp)
  13.585 + apply blast
  13.586 +-- WhileFalse 
  13.587 +apply (erule rel_pow_E2)
  13.588 + apply simp
  13.589 +apply (simp add: SKIP_n)
  13.590 +done
  13.591 +
  13.592 +
  13.593 +text {* proof of the equivalence of evalc and evalc1 *}
  13.594 +lemma evalc1_eq_evalc: "(\<langle>c, s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle>) = (\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t)"
  13.595 +apply (fast elim!: evalc1_impl_evalc evalc_impl_evalc1)
  13.596 +done
  13.597 +
  13.598 +
  13.599 +subsection "A proof without n"
  13.600 +
  13.601 +text {*
  13.602 +  The inductions are a bit awkward to write in this section,
  13.603 +  because @{text None} as result statement in the small step
  13.604 +  semantics doesn't have a direct counterpart in the big step
  13.605 +  semantics. 
  13.606  
  13.607 -    IfTrue "b s ==> (IF b THEN c1 ELSE c2,s) -1-> (c1,s)"
  13.608 -    IfFalse "~b s ==> (IF b THEN c1 ELSE c2,s) -1-> (c2,s)"
  13.609 +  Winskel's small step rule set (using the @{text "\<SKIP>"} statement
  13.610 +  to indicate termination) is better suited for this proof.
  13.611 +*}
  13.612 +
  13.613 +lemma my_lemma1 [rule_format (no_asm)]: 
  13.614 +  "\<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"
  13.615 +proof -
  13.616 +  -- {* The induction rule needs @{text P} to be a function of @{term "Some c1"} *}
  13.617 +  have "\<langle>c1,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s2\<rangle> \<Longrightarrow> \<langle>c2,s2\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3 \<longrightarrow> 
  13.618 +       \<langle>(\<lambda>c. if c = None then c2 else the c; c2) (Some c1),s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
  13.619 +    apply (erule converse_rtrancl_induct2)
  13.620 +     apply simp
  13.621 +    apply (rename_tac c s')
  13.622 +    apply simp
  13.623 +    apply (rule conjI)
  13.624 +     apply (fast dest: stuck)
  13.625 +    apply clarify
  13.626 +    apply (case_tac c)
  13.627 +    apply (auto intro: rtrancl_into_rtrancl2)
  13.628 +    done
  13.629 +  moreover assume "\<langle>c1,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s2\<rangle>" "\<langle>c2,s2\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
  13.630 +  ultimately show "\<langle>c1;c2,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3" by simp
  13.631 +qed
  13.632 +
  13.633 +lemma evalc_impl_evalc1: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s1 \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s1\<rangle>"
  13.634 +apply (erule evalc.induct)
  13.635 +
  13.636 +-- SKIP 
  13.637 +apply fast
  13.638 +
  13.639 +-- ASSIGN
  13.640 +apply fast
  13.641 +
  13.642 +-- SEMI 
  13.643 +apply (fast intro: my_lemma1)
  13.644 +
  13.645 +-- IF
  13.646 +apply (fast intro: rtrancl_into_rtrancl2)
  13.647 +apply (fast intro: rtrancl_into_rtrancl2) 
  13.648 +
  13.649 +-- WHILE 
  13.650 +apply fast
  13.651 +apply (fast intro: rtrancl_into_rtrancl2 my_lemma1)
  13.652 +
  13.653 +done
  13.654 +
  13.655 +text {*
  13.656 +  The opposite direction is based on a Coq proof done by Ranan Fraer and
  13.657 +  Yves Bertot. The following sketch is from an email by Ranan Fraer.
  13.658 +
  13.659 +\begin{verbatim}
  13.660 +First we've broke it into 2 lemmas:
  13.661  
  13.662 -    WhileFalse "~b s ==> (WHILE b DO c,s) -1-> (SKIP,s)"
  13.663 -    WhileTrue "b s ==> (WHILE b DO c,s) -1-> (c;WHILE b DO c,s)"
  13.664 +Lemma 1
  13.665 +((c,s) --> (SKIP,t)) => (<c,s> -c-> t)
  13.666 +
  13.667 +This is a quick one, dealing with the cases skip, assignment
  13.668 +and while_false.
  13.669 +
  13.670 +Lemma 2
  13.671 +((c,s) -*-> (c',s')) /\ <c',s'> -c'-> t
  13.672 +  => 
  13.673 +<c,s> -c-> t
  13.674 +
  13.675 +This is proved by rule induction on the  -*-> relation
  13.676 +and the induction step makes use of a third lemma: 
  13.677 +
  13.678 +Lemma 3
  13.679 +((c,s) --> (c',s')) /\ <c',s'> -c'-> t
  13.680 +  => 
  13.681 +<c,s> -c-> t
  13.682 +
  13.683 +This captures the essence of the proof, as it shows that <c',s'> 
  13.684 +behaves as the continuation of <c,s> with respect to the natural
  13.685 +semantics.
  13.686 +The proof of Lemma 3 goes by rule induction on the --> relation,
  13.687 +dealing with the cases sequence1, sequence2, if_true, if_false and
  13.688 +while_true. In particular in the case (sequence1) we make use again
  13.689 +of Lemma 1.
  13.690 +\end{verbatim}
  13.691 +*}
  13.692 +
  13.693 +inductive_cases evalc1_term_cases: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1 \<langle>s'\<rangle>"
  13.694 +
  13.695 +lemma FB_lemma3 [rule_format]:
  13.696 +  "(c,s) \<longrightarrow>\<^sub>1 (c',s') \<Longrightarrow> c \<noteq> None \<longrightarrow>
  13.697 +  (\<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)"
  13.698 +  apply (erule evalc1.induct)
  13.699 +  apply (auto elim!: evalc1_term_cases equivD2 [OF unfold_while])
  13.700 +  done
  13.701 +
  13.702 +lemma rtrancl_stuck: "\<langle>s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* s' \<Longrightarrow> s' = (None, s)"
  13.703 +  by (erule rtrancl_induct) (auto dest: stuck)
  13.704 +
  13.705 +lemma FB_lemma2 [rule_format]:
  13.706 +  "(c,s) \<longrightarrow>\<^sub>1\<^sup>* (c',s') \<Longrightarrow> c \<noteq> None \<longrightarrow> 
  13.707 +   \<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" 
  13.708 +  apply (erule converse_rtrancl_induct2)
  13.709 +   apply simp
  13.710 +  apply clarsimp
  13.711 +  apply (fastsimp elim!: evalc1_term_cases dest: rtrancl_stuck intro: FB_lemma3)
  13.712 +  done
  13.713 +
  13.714 +lemma evalc1_impl_evalc: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
  13.715 +  apply (fastsimp dest: FB_lemma2)
  13.716 +  done
  13.717  
  13.718  end
    14.1 --- a/src/HOL/IMP/VC.ML	Sun Dec 09 14:35:11 2001 +0100
    14.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.3 @@ -1,72 +0,0 @@
    14.4 -(*  Title:      HOL/IMP/VC.ML
    14.5 -    ID:         $Id$
    14.6 -    Author:     Tobias Nipkow
    14.7 -    Copyright   1996 TUM
    14.8 -
    14.9 -Soundness and completeness of vc
   14.10 -*)
   14.11 -
   14.12 -AddIs hoare.intrs;
   14.13 -
   14.14 -val lemma = prove_goal HOL.thy "!s. P s --> P s" (K[Fast_tac 1]);
   14.15 -
   14.16 -Goal "!Q. (!s. vc c Q s) --> |- {awp c Q} astrip c {Q}";
   14.17 -by (induct_tac "c" 1);
   14.18 -    by (ALLGOALS Simp_tac);
   14.19 -    by (Fast_tac 1);
   14.20 -   by (Fast_tac 1);
   14.21 -  by (Fast_tac 1);
   14.22 - (* if *)
   14.23 - by (Deepen_tac 4 1);
   14.24 -(* while *)
   14.25 -by (safe_tac HOL_cs);
   14.26 -by (resolve_tac hoare.intrs 1);
   14.27 -  by (rtac lemma 1);
   14.28 - by (resolve_tac hoare.intrs 1);
   14.29 - by (resolve_tac hoare.intrs 1);
   14.30 -   by (ALLGOALS(fast_tac HOL_cs));
   14.31 -qed "vc_sound";
   14.32 -
   14.33 -Goal "!P Q. (!s. P s --> Q s) --> (!s. awp c P s --> awp c Q s)";
   14.34 -by (induct_tac "c" 1);
   14.35 -    by (ALLGOALS Asm_simp_tac);
   14.36 -by (EVERY1[rtac allI, rtac allI, rtac impI]);
   14.37 -by (EVERY1[etac allE, etac allE, etac mp]);
   14.38 -by (EVERY1[etac allE, etac allE, etac mp, atac]);
   14.39 -qed_spec_mp "awp_mono";
   14.40 -
   14.41 -Goal "!P Q. (!s. P s --> Q s) --> (!s. vc c P s --> vc c Q s)";
   14.42 -by (induct_tac "c" 1);
   14.43 -    by (ALLGOALS Asm_simp_tac);
   14.44 -by (safe_tac HOL_cs);
   14.45 -by (EVERY[etac allE 1,etac allE 1,etac impE 1,etac allE 2,etac mp 2,atac 2]);
   14.46 -by (fast_tac (HOL_cs addEs [awp_mono]) 1);
   14.47 -qed_spec_mp "vc_mono";
   14.48 -
   14.49 -Goal "|- {P}c{Q} ==> \
   14.50 -\  (? ac. astrip ac = c & (!s. vc ac Q s) & (!s. P s --> awp ac Q s))";
   14.51 -by (etac hoare.induct 1);
   14.52 -     by (res_inst_tac [("x","Askip")] exI 1);
   14.53 -     by (Simp_tac 1);
   14.54 -    by (res_inst_tac [("x","Aass x a")] exI 1);
   14.55 -    by (Simp_tac 1);
   14.56 -   by (SELECT_GOAL(safe_tac HOL_cs)1);
   14.57 -   by (res_inst_tac [("x","Asemi ac aca")] exI 1);
   14.58 -   by (Asm_simp_tac 1);
   14.59 -   by (fast_tac (HOL_cs addSEs [awp_mono,vc_mono]) 1);
   14.60 -  by (SELECT_GOAL(safe_tac HOL_cs)1);
   14.61 -  by (res_inst_tac [("x","Aif b ac aca")] exI 1);
   14.62 -  by (Asm_simp_tac 1);
   14.63 - by (SELECT_GOAL(safe_tac HOL_cs)1);
   14.64 - by (res_inst_tac [("x","Awhile b P ac")] exI 1);
   14.65 - by (Asm_simp_tac 1);
   14.66 -by (safe_tac HOL_cs);
   14.67 -by (res_inst_tac [("x","ac")] exI 1);
   14.68 -by (Asm_simp_tac 1);
   14.69 -by (fast_tac (HOL_cs addSEs [awp_mono,vc_mono]) 1);
   14.70 -qed "vc_complete";
   14.71 -
   14.72 -Goal "!Q. vcawp c Q = (vc c Q, awp c Q)";
   14.73 -by (induct_tac "c" 1);
   14.74 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [Let_def])));
   14.75 -qed "vcawp_vc_awp";
    15.1 --- a/src/HOL/IMP/VC.thy	Sun Dec 09 14:35:11 2001 +0100
    15.2 +++ b/src/HOL/IMP/VC.thy	Sun Dec 09 14:35:36 2001 +0100
    15.3 @@ -8,7 +8,9 @@
    15.4  awp:   weakest (liberal) precondition
    15.5  *)
    15.6  
    15.7 -VC  =  Hoare +
    15.8 +header "Verification Conditions"
    15.9 +
   15.10 +theory VC = Hoare:
   15.11  
   15.12  datatype  acom = Askip
   15.13                 | Aass   loc aexp
   15.14 @@ -17,45 +19,121 @@
   15.15                 | Awhile bexp assn acom
   15.16  
   15.17  consts
   15.18 -  vc,awp :: acom => assn => assn
   15.19 -  vcawp :: "acom => assn => assn * assn"
   15.20 -  astrip :: acom => com
   15.21 +  vc :: "acom => assn => assn"
   15.22 +  awp :: "acom => assn => assn"
   15.23 +  vcawp :: "acom => assn => assn \<times> assn"
   15.24 +  astrip :: "acom => com"
   15.25  
   15.26  primrec
   15.27    "awp Askip Q = Q"
   15.28 -  "awp (Aass x a) Q = (%s. Q(s[x::=a s]))"
   15.29 +  "awp (Aass x a) Q = (\<lambda>s. Q(s[x\<mapsto>a s]))"
   15.30    "awp (Asemi c d) Q = awp c (awp d Q)"
   15.31 -  "awp (Aif b c d) Q = (%s. (b s-->awp c Q s) & (~b s-->awp d Q s))" 
   15.32 +  "awp (Aif b c d) Q = (\<lambda>s. (b s-->awp c Q s) & (~b s-->awp d Q s))" 
   15.33    "awp (Awhile b I c) Q = I"
   15.34  
   15.35  primrec
   15.36 -  "vc Askip Q = (%s. True)"
   15.37 -  "vc (Aass x a) Q = (%s. True)"
   15.38 -  "vc (Asemi c d) Q = (%s. vc c (awp d Q) s & vc d Q s)"
   15.39 -  "vc (Aif b c d) Q = (%s. vc c Q s & vc d Q s)" 
   15.40 -  "vc (Awhile b I c) Q = (%s. (I s & ~b s --> Q s) &
   15.41 +  "vc Askip Q = (\<lambda>s. True)"
   15.42 +  "vc (Aass x a) Q = (\<lambda>s. True)"
   15.43 +  "vc (Asemi c d) Q = (\<lambda>s. vc c (awp d Q) s & vc d Q s)"
   15.44 +  "vc (Aif b c d) Q = (\<lambda>s. vc c Q s & vc d Q s)" 
   15.45 +  "vc (Awhile b I c) Q = (\<lambda>s. (I s & ~b s --> Q s) &
   15.46                                (I s & b s --> awp c I s) & vc c I s)"
   15.47  
   15.48  primrec
   15.49    "astrip Askip = SKIP"
   15.50    "astrip (Aass x a) = (x:==a)"
   15.51    "astrip (Asemi c d) = (astrip c;astrip d)"
   15.52 -  "astrip (Aif b c d) = (IF b THEN astrip c ELSE astrip d)"
   15.53 -  "astrip (Awhile b I c) = (WHILE b DO astrip c)"
   15.54 +  "astrip (Aif b c d) = (\<IF> b \<THEN> astrip c \<ELSE> astrip d)"
   15.55 +  "astrip (Awhile b I c) = (\<WHILE> b \<DO> astrip c)"
   15.56  
   15.57  (* simultaneous computation of vc and awp: *)
   15.58  primrec
   15.59 -  "vcawp Askip Q = (%s. True, Q)"
   15.60 -  "vcawp (Aass x a) Q = (%s. True, %s. Q(s[x::=a s]))"
   15.61 +  "vcawp Askip Q = (\<lambda>s. True, Q)"
   15.62 +  "vcawp (Aass x a) Q = (\<lambda>s. True, \<lambda>s. Q(s[x\<mapsto>a s]))"
   15.63    "vcawp (Asemi c d) Q = (let (vcd,wpd) = vcawp d Q;
   15.64                                (vcc,wpc) = vcawp c wpd
   15.65 -                          in (%s. vcc s & vcd s, wpc))"
   15.66 +                          in (\<lambda>s. vcc s & vcd s, wpc))"
   15.67    "vcawp (Aif b c d) Q = (let (vcd,wpd) = vcawp d Q;
   15.68                                (vcc,wpc) = vcawp c Q
   15.69 -                          in (%s. vcc s & vcd s,
   15.70 -                              %s.(b s --> wpc s) & (~b s --> wpd s)))"
   15.71 +                          in (\<lambda>s. vcc s & vcd s,
   15.72 +                              \<lambda>s.(b s --> wpc s) & (~b s --> wpd s)))"
   15.73    "vcawp (Awhile b I c) Q = (let (vcc,wpc) = vcawp c I
   15.74 -                             in (%s. (I s & ~b s --> Q s) &
   15.75 +                             in (\<lambda>s. (I s & ~b s --> Q s) &
   15.76                                       (I s & b s --> wpc s) & vcc s, I))"
   15.77  
   15.78 +(*
   15.79 +Soundness and completeness of vc
   15.80 +*)
   15.81 +
   15.82 +declare hoare.intros [intro]
   15.83 +
   15.84 +lemma l: "!s. P s --> P s" by fast
   15.85 +
   15.86 +lemma vc_sound: "!Q. (!s. vc c Q s) --> |- {awp c Q} astrip c {Q}"
   15.87 +apply (induct_tac "c")
   15.88 +    apply (simp_all (no_asm))
   15.89 +    apply fast
   15.90 +   apply fast
   15.91 +  apply fast
   15.92 + (* if *)
   15.93 + apply (tactic "Deepen_tac 4 1")
   15.94 +(* while *)
   15.95 +apply (intro allI impI) 
   15.96 +apply (rule conseq)
   15.97 +  apply (rule l)
   15.98 + apply (rule While)
   15.99 + defer
  15.100 + apply fast
  15.101 +apply (rule_tac P="awp acom fun2" in conseq)
  15.102 +  apply fast
  15.103 + apply fast
  15.104 +apply fast
  15.105 +done
  15.106 +
  15.107 +lemma awp_mono [rule_format (no_asm)]: "!P Q. (!s. P s --> Q s) --> (!s. awp c P s --> awp c Q s)"
  15.108 +apply (induct_tac "c")
  15.109 +    apply (simp_all (no_asm_simp))
  15.110 +apply (rule allI, rule allI, rule impI)
  15.111 +apply (erule allE, erule allE, erule mp)
  15.112 +apply (erule allE, erule allE, erule mp, assumption)
  15.113 +done
  15.114 +
  15.115 +
  15.116 +lemma vc_mono [rule_format (no_asm)]: "!P Q. (!s. P s --> Q s) --> (!s. vc c P s --> vc c Q s)"
  15.117 +apply (induct_tac "c")
  15.118 +    apply (simp_all (no_asm_simp))
  15.119 +apply safe
  15.120 +apply (erule allE,erule allE,erule impE,erule_tac [2] allE,erule_tac [2] mp) 
  15.121 +prefer 2 apply assumption
  15.122 +apply (fast elim: awp_mono)
  15.123 +done
  15.124 +
  15.125 +lemma vc_complete: "|- {P}c{Q} ==>  
  15.126 +   (? ac. astrip ac = c & (!s. vc ac Q s) & (!s. P s --> awp ac Q s))"
  15.127 +apply (erule hoare.induct)
  15.128 +     apply (rule_tac x = "Askip" in exI)
  15.129 +     apply (simp (no_asm))
  15.130 +    apply (rule_tac x = "Aass x a" in exI)
  15.131 +    apply (simp (no_asm))
  15.132 +   apply clarify
  15.133 +   apply (rule_tac x = "Asemi ac aca" in exI)
  15.134 +   apply (simp (no_asm_simp))
  15.135 +   apply (fast elim!: awp_mono vc_mono)
  15.136 +  apply clarify
  15.137 +  apply (rule_tac x = "Aif b ac aca" in exI)
  15.138 +  apply (simp (no_asm_simp))
  15.139 + apply clarify
  15.140 + apply (rule_tac x = "Awhile b P ac" in exI)
  15.141 + apply (simp (no_asm_simp))
  15.142 +apply safe
  15.143 +apply (rule_tac x = "ac" in exI)
  15.144 +apply (simp (no_asm_simp))
  15.145 +apply (fast elim!: awp_mono vc_mono)
  15.146 +done
  15.147 +
  15.148 +lemma vcawp_vc_awp: "!Q. vcawp c Q = (vc c Q, awp c Q)"
  15.149 +apply (induct_tac "c")
  15.150 +apply (simp_all (no_asm_simp) add: Let_def)
  15.151 +done
  15.152 +
  15.153  end
    16.1 --- a/src/HOLCF/IMP/Denotational.ML	Sun Dec 09 14:35:11 2001 +0100
    16.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.3 @@ -1,51 +0,0 @@
    16.4 -(*  Title:      HOLCF/IMP/Denotational.ML
    16.5 -    ID:         $Id$
    16.6 -    Author:     Tobias Nipkow & Robert Sandner
    16.7 -    Copyright   1996 TUM
    16.8 -
    16.9 -Equivalence of Denotational Semantics in HOLCF and Evaluation Semantics in HOL
   16.10 -*)
   16.11 -
   16.12 -Goalw [dlift_def] "dlift f$(Def x) = f$(Discr x)";
   16.13 -by (Simp_tac 1);
   16.14 -qed "dlift_Def";
   16.15 -Addsimps [dlift_Def];
   16.16 -
   16.17 -Goalw [dlift_def] "cont(%f. dlift f)";
   16.18 -by (Simp_tac 1);
   16.19 -qed "cont_dlift";
   16.20 -AddIffs [cont_dlift];
   16.21 -
   16.22 -Goalw [dlift_def]
   16.23 - "(dlift f$l = Def y) = (? x. l = Def x & f$(Discr x) = Def y)";
   16.24 -by (simp_tac (simpset() addsplits [lift.split]) 1);
   16.25 -qed "dlift_is_Def";
   16.26 -Addsimps [dlift_is_Def];
   16.27 -
   16.28 -Goal "<c,s> -c-> t ==> D c$(Discr s) = (Def t)";
   16.29 -by (etac evalc.induct 1);
   16.30 -      by (ALLGOALS Asm_simp_tac);
   16.31 - by (ALLGOALS (stac fix_eq THEN' Asm_full_simp_tac));
   16.32 -qed_spec_mp "eval_implies_D";
   16.33 -
   16.34 -Goal "!s t. D c$(Discr s) = (Def t) --> <c,s> -c-> t";
   16.35 -by (induct_tac "c" 1);
   16.36 -    by (Force_tac 1);
   16.37 -   by (Force_tac 1);
   16.38 -  by (Force_tac 1);
   16.39 - by (Simp_tac 1);
   16.40 - by (Force_tac 1);
   16.41 -by (Simp_tac 1);
   16.42 -by (rtac fix_ind 1);
   16.43 -  by (fast_tac (claset() addSIs adm_lemmas @ [adm_chfindom, ax_flat]) 1);
   16.44 - by (Simp_tac 1);
   16.45 -by (Simp_tac 1);
   16.46 -by Safe_tac;
   16.47 -  by (Fast_tac 1);
   16.48 - by (Force_tac 1);
   16.49 -qed_spec_mp "D_implies_eval";
   16.50 -
   16.51 -
   16.52 -Goal "(D c$(Discr s) = (Def t)) = (<c,s> -c-> t)";
   16.53 -by (fast_tac (claset() addSEs [D_implies_eval,eval_implies_D]) 1);
   16.54 -qed "D_is_eval";
    17.1 --- a/src/HOLCF/IMP/Denotational.thy	Sun Dec 09 14:35:11 2001 +0100
    17.2 +++ b/src/HOLCF/IMP/Denotational.thy	Sun Dec 09 14:35:36 2001 +0100
    17.3 @@ -2,11 +2,13 @@
    17.4      ID:         $Id$
    17.5      Author:     Tobias Nipkow & Robert Sandner, TUM
    17.6      Copyright   1996 TUM
    17.7 -
    17.8 -Denotational semantics of commands in HOLCF
    17.9  *)
   17.10  
   17.11 -Denotational = HOLCF + Natural +
   17.12 +header "Denotational Semantics of Commands in HOLCF"
   17.13 +
   17.14 +theory Denotational = HOLCF + Natural:
   17.15 +
   17.16 +subsection "Definition"
   17.17  
   17.18  constdefs
   17.19     dlift :: "(('a::type) discr -> 'b::pcpo) => ('a lift -> 'b)"
   17.20 @@ -15,13 +17,65 @@
   17.21  consts D :: "com => state discr -> state lift"
   17.22  
   17.23  primrec
   17.24 -  "D(SKIP) = (LAM s. Def(undiscr s))"
   17.25 -  "D(X :== a) = (LAM s. Def((undiscr s)[X ::= a(undiscr s)]))"
   17.26 +  "D(\<SKIP>) = (LAM s. Def(undiscr s))"
   17.27 +  "D(X :== a) = (LAM s. Def((undiscr s)[X \<mapsto> a(undiscr s)]))"
   17.28    "D(c0 ; c1) = (dlift(D c1) oo (D c0))"
   17.29 -  "D(IF b THEN c1 ELSE c2) =
   17.30 +  "D(\<IF> b \<THEN> c1 \<ELSE> c2) =
   17.31  	(LAM s. if b(undiscr s) then (D c1)$s else (D c2)$s)"
   17.32 -  "D(WHILE b DO c) =
   17.33 +  "D(\<WHILE> b \<DO> c) =
   17.34  	fix$(LAM w s. if b(undiscr s) then (dlift w)$((D c)$s)
   17.35                        else Def(undiscr s))"
   17.36  
   17.37 +subsection
   17.38 +  "Equivalence of Denotational Semantics in HOLCF and Evaluation Semantics in HOL"
   17.39 +
   17.40 +lemma dlift_Def: "dlift f$(Def x) = f$(Discr x)"
   17.41 +apply (unfold dlift_def)
   17.42 +apply (simp (no_asm))
   17.43 +done
   17.44 +declare dlift_Def [simp]
   17.45 +
   17.46 +lemma cont_dlift: "cont(%f. dlift f)"
   17.47 +apply (unfold dlift_def)
   17.48 +apply (simp (no_asm))
   17.49 +done
   17.50 +declare cont_dlift [iff]
   17.51 +
   17.52 +lemma dlift_is_Def: 
   17.53 + "(dlift f$l = Def y) = (? x. l = Def x & f$(Discr x) = Def y)"
   17.54 +apply (unfold dlift_def)
   17.55 +apply (simp (no_asm) split add: lift.split)
   17.56 +done
   17.57 +declare dlift_is_Def [simp]
   17.58 +
   17.59 +lemma eval_implies_D [rule_format (no_asm)]: 
   17.60 +  "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t ==> D c$(Discr s) = (Def t)"
   17.61 +apply (erule evalc.induct)
   17.62 +      apply (simp_all (no_asm_simp))
   17.63 + apply (subst fix_eq)
   17.64 + apply simp
   17.65 +apply (subst fix_eq)
   17.66 +apply simp
   17.67 +done
   17.68 +
   17.69 +lemma D_implies_eval [rule_format (no_asm)]: 
   17.70 +  "!s t. D c$(Discr s) = (Def t) --> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
   17.71 +apply (induct_tac "c")
   17.72 +    apply force
   17.73 +   apply force
   17.74 +  apply force
   17.75 + apply (simp (no_asm))
   17.76 + apply force
   17.77 +apply (simp (no_asm))
   17.78 +apply (rule fix_ind)
   17.79 +  apply (fast intro!: adm_lemmas adm_chfindom ax_flat)
   17.80 + apply (simp (no_asm))
   17.81 +apply (simp (no_asm))
   17.82 +apply safe
   17.83 +apply fast
   17.84 +done
   17.85 +
   17.86 +lemma D_is_eval: "(D c$(Discr s) = (Def t)) = (\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t)"
   17.87 +  by (fast elim!: D_implies_eval eval_implies_D)
   17.88 +
   17.89  end
    18.1 --- a/src/HOLCF/IMP/HoareEx.ML	Sun Dec 09 14:35:11 2001 +0100
    18.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.3 @@ -1,19 +0,0 @@
    18.4 -(*  Title:      HOLCF/IMP/HoareEx.ML
    18.5 -    ID:         $Id$
    18.6 -    Author:     Tobias Nipkow
    18.7 -    Copyright   1997 TUM
    18.8 -
    18.9 -Correctness of while-loop.
   18.10 -*)
   18.11 -
   18.12 -val prems = goalw thy [hoare_valid_def]
   18.13 -"|= {A} c {A} ==> |= {A} WHILE b DO c {%s. A s & ~b s}";
   18.14 -by (cut_facts_tac prems 1);
   18.15 -by (Simp_tac 1);
   18.16 -by (rtac fix_ind 1);
   18.17 -  (* simplifier with enhanced adm-tactic: *)
   18.18 -  by (Simp_tac 1);
   18.19 - by (Simp_tac 1);
   18.20 -by (Simp_tac 1);
   18.21 -by (Blast_tac 1);
   18.22 -qed "WHILE_rule_sound";
    19.1 --- a/src/HOLCF/IMP/HoareEx.thy	Sun Dec 09 14:35:11 2001 +0100
    19.2 +++ b/src/HOLCF/IMP/HoareEx.thy	Sun Dec 09 14:35:36 2001 +0100
    19.3 @@ -2,17 +2,32 @@
    19.4      ID:         $Id$
    19.5      Author:     Tobias Nipkow, TUM
    19.6      Copyright   1997 TUM
    19.7 -
    19.8 -An example from the HOLCF paper by Mueller, Nipkow, Oheimb, Slotosch.
    19.9 -It demonstrates fixpoint reasoning by showing the correctness of the Hoare
   19.10 -rule for while-loops.
   19.11  *)
   19.12  
   19.13 -HoareEx = Denotational +
   19.14 +header "Correctness of Hoare by Fixpoint Reasoning"
   19.15 +
   19.16 +theory HoareEx = Denotational:
   19.17  
   19.18 -types assn = state => bool
   19.19 +text {*
   19.20 +  An example from the HOLCF paper by Mueller, Nipkow, Oheimb, Slotosch \cite{MuellerNvOS99}.
   19.21 +  It demonstrates fixpoint reasoning by showing the correctness of the Hoare
   19.22 +  rule for while-loops.
   19.23 +*}
   19.24  
   19.25 -constdefs hoare_valid :: [assn,com,assn] => bool ("|= {(1_)}/ (_)/ {(1_)}" 50)
   19.26 +types assn = "state => bool"
   19.27 +
   19.28 +constdefs hoare_valid :: "[assn,com,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50)
   19.29   "|= {A} c {B} == !s t. A s & D c $(Discr s) = Def t --> B t"
   19.30  
   19.31 +lemma WHILE_rule_sound:
   19.32 +  "|= {A} c {A} ==> |= {A} \<WHILE> b \<DO> c {%s. A s & ~b s}"
   19.33 +  apply (unfold hoare_valid_def)
   19.34 +  apply (simp (no_asm))
   19.35 +  apply (rule fix_ind)
   19.36 +    apply (simp (no_asm)) -- "simplifier with enhanced adm-tactic"
   19.37 +   apply (simp (no_asm))
   19.38 +  apply (simp (no_asm))
   19.39 +  apply blast
   19.40 +  done
   19.41 +
   19.42  end