Changed [/] to [:=] and removed actual definition.
authornipkow
Wed May 06 11:46:00 1998 +0200 (1998-05-06)
changeset 4897be11be0b6ea1
parent 4896 4727272f3db6
child 4898 68fd1a2b8b7b
Changed [/] to [:=] and removed actual definition.
src/HOL/IMP/Denotation.thy
src/HOL/IMP/Hoare.ML
src/HOL/IMP/Hoare.thy
src/HOL/IMP/Natural.thy
src/HOL/IMP/Transition.ML
src/HOL/IMP/Transition.thy
src/HOL/IMP/VC.thy
     1.1 --- a/src/HOL/IMP/Denotation.thy	Tue May 05 17:28:22 1998 +0200
     1.2 +++ b/src/HOL/IMP/Denotation.thy	Wed May 06 11:46:00 1998 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4  
     1.5  primrec C com
     1.6    C_skip    "C(SKIP) = id"
     1.7 -  C_assign  "C(x := a) = {(s,t). t = s[a(s)/x]}"
     1.8 +  C_assign  "C(x := a) = {(s,t). t = s[x:=a(s)]}"
     1.9    C_comp    "C(c0 ; c1) = C(c1) O C(c0)"
    1.10    C_if      "C(IF b THEN c1 ELSE c2) = {(s,t). (s,t) : C(c1) & b(s)} Un
    1.11                                         {(s,t). (s,t) : C(c2) & ~ b(s)}"
     2.1 --- a/src/HOL/IMP/Hoare.ML	Tue May 05 17:28:22 1998 +0200
     2.2 +++ b/src/HOL/IMP/Hoare.ML	Wed May 06 11:46:00 1998 +0200
     2.3 @@ -27,7 +27,7 @@
     2.4  by (Simp_tac 1);
     2.5  qed "wp_SKIP";
     2.6  
     2.7 -goalw Hoare.thy [wp_def] "wp (x:=a) Q = (%s. Q(s[a s/x]))";
     2.8 +goalw Hoare.thy [wp_def] "wp (x:=a) Q = (%s. Q(s[x:=a s]))";
     2.9  by (Simp_tac 1);
    2.10  qed "wp_Ass";
    2.11  
     3.1 --- a/src/HOL/IMP/Hoare.thy	Tue May 05 17:28:22 1998 +0200
     3.2 +++ b/src/HOL/IMP/Hoare.thy	Wed May 06 11:46:00 1998 +0200
     3.3 @@ -20,7 +20,7 @@
     3.4  inductive hoare
     3.5  intrs
     3.6    skip "|- {P}SKIP{P}"
     3.7 -  ass  "|- {%s. P(s[a s/x])} x:=a {P}"
     3.8 +  ass  "|- {%s. P(s[x:=a s])} x:=a {P}"
     3.9    semi "[| |- {P}c{Q}; |- {Q}d{R} |] ==> |- {P} c;d {R}"
    3.10    If "[| |- {%s. P s & b s}c{Q}; |- {%s. P s & ~b s}d{Q} |] ==>
    3.11        |- {P} IF b THEN c ELSE d {Q}"
     4.1 --- a/src/HOL/IMP/Natural.thy	Tue May 05 17:28:22 1998 +0200
     4.2 +++ b/src/HOL/IMP/Natural.thy	Wed May 06 11:46:00 1998 +0200
     4.3 @@ -14,15 +14,19 @@
     4.4  
     4.5  translations  "<ce,sig> -c-> s" == "(ce,sig,s) : evalc"
     4.6  
     4.7 -constdefs assign :: [state,val,loc] => state    ("_[_'/_]" [95,0,0] 95)
     4.8 -  "s[m/x] ==  (%y. if y=x then m else s y)"
     4.9 -
    4.10 +consts
    4.11 +  update  :: "('a => 'b) => 'a => 'b => ('a => 'b)"
    4.12 +           ("_/[_/:=/_]" [900,0,0] 900)
    4.13 +(* update is NOT defined, only declared!
    4.14 +   Thus the whole theory is independent of its meaning!
    4.15 +   If theory Update is included, proofs break.
    4.16 +*)
    4.17  
    4.18  inductive evalc
    4.19    intrs
    4.20      Skip    "<SKIP,s> -c-> s"
    4.21  
    4.22 -    Assign  "<x := a,s> -c-> s[a(s)/x]"
    4.23 +    Assign  "<x := a,s> -c-> s[x:=a(s)]"
    4.24  
    4.25      Semi    "[| <c0,s> -c-> s2; <c1,s2> -c-> s1 |] 
    4.26              ==> <c0 ; c1, s> -c-> s1"
     5.1 --- a/src/HOL/IMP/Transition.ML	Tue May 05 17:28:22 1998 +0200
     5.2 +++ b/src/HOL/IMP/Transition.ML	Wed May 06 11:46:00 1998 +0200
     5.3 @@ -65,7 +65,7 @@
     5.4  goal Transition.thy
     5.5    "!c d s u. (c;d,s) -n-> (SKIP,u) --> \
     5.6  \            (? t m. (c,s) -*-> (SKIP,t) & (d,t) -m-> (SKIP,u) & m <= n)";
     5.7 -by (nat_ind_tac "n" 1);
     5.8 +by (induct_tac "n" 1);
     5.9   (* case n = 0 *)
    5.10   by (fast_tac (claset() addss simpset()) 1);
    5.11  (* induction step *)
    5.12 @@ -75,15 +75,14 @@
    5.13  qed_spec_mp "lemma2";
    5.14  
    5.15  goal Transition.thy "!s t. (c,s) -*-> (SKIP,t) --> <c,s> -c-> t";
    5.16 -by (com.induct_tac "c" 1);
    5.17 +by (induct_tac "c" 1);
    5.18  by (safe_tac (claset() addSDs [rtrancl_imp_UN_rel_pow]));
    5.19  
    5.20  (* SKIP *)
    5.21  by (fast_tac (claset() addSEs [rel_pow_E2]) 1);
    5.22  
    5.23  (* ASSIGN *)
    5.24 -by (fast_tac (claset() addSDs [hlemma]  addSEs [rel_pow_E2]
    5.25 -                       addss simpset()) 1);
    5.26 +by (fast_tac (claset() addSDs [hlemma]  addSEs [rel_pow_E2]) 1);
    5.27  
    5.28  (* SEMI *)
    5.29  by (fast_tac (claset() addSDs [lemma2,rel_pow_imp_rtrancl]) 1);
    5.30 @@ -185,17 +184,18 @@
    5.31  of Lemma 1.
    5.32  *)
    5.33  
    5.34 -
    5.35 +(*Delsimps [update_apply];*)
    5.36  goal Transition.thy 
    5.37    "!!c s. ((c,s) -1-> (c',s')) ==> (!t. <c',s'> -c-> t --> <c,s> -c-> t)";
    5.38  by (etac evalc1.induct 1);
    5.39  by Auto_tac;
    5.40  qed_spec_mp "FB_lemma3";
    5.41 +(*Addsimps [update_apply];*)
    5.42  
    5.43  val [major] = goal Transition.thy
    5.44    "(c,s) -*-> (c',s') ==> <c',s'> -c-> t --> <c,s> -c-> t";
    5.45  by (rtac (major RS rtrancl_induct2) 1);
    5.46 -by (Fast_tac 1);
    5.47 + by (Fast_tac 1);
    5.48  by (fast_tac (claset() addIs [FB_lemma3]) 1);
    5.49  qed_spec_mp "FB_lemma2";
    5.50  
     6.1 --- a/src/HOL/IMP/Transition.thy	Tue May 05 17:28:22 1998 +0200
     6.2 +++ b/src/HOL/IMP/Transition.thy	Wed May 06 11:46:00 1998 +0200
     6.3 @@ -24,7 +24,7 @@
     6.4  
     6.5  inductive evalc1
     6.6    intrs
     6.7 -    Assign "(x := a,s) -1-> (SKIP,s[a s / x])"
     6.8 +    Assign "(x := a,s) -1-> (SKIP,s[x := a s])"
     6.9  
    6.10      Semi1   "(SKIP;c,s) -1-> (c,s)"	
    6.11      Semi2   "(c0,s) -1-> (c2,s1) ==> (c0;c1,s) -1-> (c2;c1,s1)"
     7.1 --- a/src/HOL/IMP/VC.thy	Tue May 05 17:28:22 1998 +0200
     7.2 +++ b/src/HOL/IMP/VC.thy	Wed May 06 11:46:00 1998 +0200
     7.3 @@ -23,7 +23,7 @@
     7.4  
     7.5  primrec awp acom
     7.6    "awp Askip Q = Q"
     7.7 -  "awp (Aass x a) Q = (%s. Q(s[a s/x]))"
     7.8 +  "awp (Aass x a) Q = (%s. Q(s[x:=a s]))"
     7.9    "awp (Asemi c d) Q = awp c (awp d Q)"
    7.10    "awp (Aif b c d) Q = (%s. (b s-->awp c Q s) & (~b s-->awp d Q s))" 
    7.11    "awp (Awhile b I c) Q = I"
    7.12 @@ -46,7 +46,7 @@
    7.13  (* simultaneous computation of vc and awp: *)
    7.14  primrec vcawp acom
    7.15    "vcawp Askip Q = (%s. True, Q)"
    7.16 -  "vcawp (Aass x a) Q = (%s. True, %s. Q(s[a s/x]))"
    7.17 +  "vcawp (Aass x a) Q = (%s. True, %s. Q(s[x:=a s]))"
    7.18    "vcawp (Asemi c d) Q = (let (vcd,wpd) = vcawp d Q;
    7.19                                (vcc,wpc) = vcawp c wpd
    7.20                            in (%s. vcc s & vcd s, wpc))"