HOL theorem-proving system

Update of /cvsroot/hol/hol98/examples/pgcl/src
In directory sc8-pr-cvs1:/tmp/cvs-serv23484/src

Modified Files:
	expectationScript.sml qtl wpScript.sml wpTools.sml 
Log Message:
Factorized out some common subexpressions as new definitions.


Index: expectationScript.sml
===================================================================
RCS file: /cvsroot/hol/hol98/examples/pgcl/src/expectationScript.sml,v
retrieving revision 1.3
retrieving revision 1.4
diff -b -C2 -d -r1.3 -r1.4
*** expectationScript.sml	30 Sep 2003 01:44:56 -0000	1.3
--- expectationScript.sml	30 Sep 2003 15:39:15 -0000	1.4
***************
*** 231,240 ****
  (* ------------------------------------------------------------------------- *)
  
! val prob_def = Define
!   `prob p (a : 'a expect) b s =
     let x = bound1 (p s) in x * a s + (1 - x) * b s`;
  
! val cond_def = Define
!   `cond c (a : 'a expect) b s = if c s then a s else b s`;
  
  (* ------------------------------------------------------------------------- *)
--- 231,251 ----
  (* ------------------------------------------------------------------------- *)
  
! val Lin_def = Define
!   `Lin p (a : 'a expect) b s =
     let x = bound1 (p s) in x * a s + (1 - x) * b s`;
  
! val Cond_def = Define
!   `Cond c (a : 'a expect) b s = if c s then a s else b s`;
! 
! val lin_eta = store_thm
!   ("lin_eta",
!    ``!p a b.
!        Lin p a b = \s. let x = bound1 (p s) in x * a s + (1 - x) * b s``,
!    METIS_TAC [Lin_def]);
! 
! val cond_eta = store_thm
!   ("cond_eta",
!    ``!c a b. Cond c a b = \s. if c s then a s else b s``,
!    METIS_TAC [Cond_def]);
  
  (* ------------------------------------------------------------------------- *)

Index: qtl
===================================================================
RCS file: /cvsroot/hol/hol98/examples/pgcl/src/qtl,v
retrieving revision 1.1
retrieving revision 1.2
diff -b -C2 -d -r1.1 -r1.2
*** qtl	8 Apr 2003 13:48:49 -0000	1.1
--- qtl	30 Sep 2003 15:39:15 -0000	1.2
***************
*** 45,54 ****
  val Suff = Q_TAC SUFF_TAC;
  val REVERSE = Tactical.REVERSE;
! 
! val real_ss = simpLib.++
!   (realLib.real_ss,
!    simpLib.SIMPSET
!    {ac = [], congs = [], convs = [], dprocs = [], filter = NONE,
!     rewrs = []});
  
  (* ------------------------------------------------------------------------- *)
--- 45,49 ----
  val Suff = Q_TAC SUFF_TAC;
  val REVERSE = Tactical.REVERSE;
! val lemma = I prove;
  
  (* ------------------------------------------------------------------------- *)
***************
*** 421,425 ****
  (* ------------------------------------------------------------------------- *)
  
! val eventually_lfp_lemma =prove
    (``!step a.
          wf_trans step /\ wf_prob (sem step a) ==>
--- 416,420 ----
  (* ------------------------------------------------------------------------- *)
  
! val eventually_lfp_lemma = lemma
    (``!step a.
          wf_trans step /\ wf_prob (sem step a) ==>
***************
*** 436,440 ****
         ++ PROVE_TAC [wf_trans_mono, wf_prob_expect, leq_refl]]);
  
! val unless_gfp_lemma =prove
    (``!step a b.
          wf_trans step /\ wf_prob (sem step a) /\ wf_prob (sem step b) ==>
--- 431,435 ----
         ++ PROVE_TAC [wf_trans_mono, wf_prob_expect, leq_refl]]);
  
! val unless_gfp_lemma = lemma
    (``!step a b.
          wf_trans step /\ wf_prob (sem step a) /\ wf_prob (sem step b) ==>

Index: wpScript.sml
===================================================================
RCS file: /cvsroot/hol/hol98/examples/pgcl/src/wpScript.sml,v
retrieving revision 1.4
retrieving revision 1.5
diff -b -C2 -d -r1.4 -r1.5
*** wpScript.sml	30 Sep 2003 01:44:56 -0000	1.4
--- wpScript.sml	30 Sep 2003 15:39:15 -0000	1.5
***************
*** 48,52 ****
  val Suff = Q_TAC SUFF_TAC;
  val REVERSE = Tactical.REVERSE;
! val lemma = prove;
  
  (* ------------------------------------------------------------------------- *)
--- 48,52 ----
  val Suff = Q_TAC SUFF_TAC;
  val REVERSE = Tactical.REVERSE;
! val lemma = I prove;
  
  (* ------------------------------------------------------------------------- *)
***************
*** 85,90 ****
     (Program (c :: c' :: cs) = Seq c (Program (c' :: cs)))`;
  
! val Cond_def = Define
!   `Cond c a b = Prob (\s. if c s then 1 else 0) a b`;
  
  (* Demons [] should evaluate to the identity for Demon, which is Magic.     *)
--- 85,90 ----
     (Program (c :: c' :: cs) = Seq c (Program (c' :: cs)))`;
  
! val If_def = Define
!   `If c a b = Prob (\s. if c s then 1 else 0) a b`;
  
  (* Demons [] should evaluate to the identity for Demon, which is Magic.     *)
***************
*** 101,105 ****
    `(guards cs [] = if cs = [] then Abort else Demons cs) /\
     (guards cs ((p, c) :: rest) =
!     Cond p (guards (c :: cs) rest) (guards cs rest))`;
  
  val Guards_def = Define `Guards l = guards [] l`;
--- 101,105 ----
    `(guards cs [] = if cs = [] then Abort else Demons cs) /\
     (guards cs ((p, c) :: rest) =
!     If p (guards (c :: cs) rest) (guards cs rest))`;
  
  val Guards_def = Define `Guards l = guards [] l`;
***************
*** 126,135 ****
    `(wp Abort = \r. Zero) /\
     (wp Skip = \r. r) /\
!    (wp (Assign v e) = \r s. r (\w. if w = v then e s else s w)) /\
     (wp (Seq a b) = \r. wp a (wp b r)) /\
     (wp (Demon a b) = \r. Min (wp a r) (wp b r)) /\
!    (wp (Prob p a b) =
!     \r s. let x = bound1 (p s) in x * wp a r s + (1 - x) * wp b r s) /\
!    (wp (While c b) = \r. expect_lfp (\e s. if c s then wp b e s else r s))`;
  
  val wp_incognito_def = Define `wp_incognito = wp`;
--- 126,134 ----
    `(wp Abort = \r. Zero) /\
     (wp Skip = \r. r) /\
!    (wp (Assign v e) = \r s. r (assign v e s)) /\
     (wp (Seq a b) = \r. wp a (wp b r)) /\
     (wp (Demon a b) = \r. Min (wp a r) (wp b r)) /\
!    (wp (Prob p a b) = \r. Lin p (wp a r) (wp b r)) /\
!    (wp (While c b) = \r. expect_lfp (\e. Cond c (wp b e) r))`;
  
  val wp_incognito_def = Define `wp_incognito = wp`;
***************
*** 151,155 ****
     ++ Q.EXISTS_TAC `\v. if v "n" = 1 then 1 else 0`
     ++ Q.EXISTS_TAC `\v. 0`
!    ++ REWRITE_TAC [wp_def]
     ++ SIMP_TAC int_ss [Min_def]
     ++ SIMP_TAC posreal_ss [preal_min_def]);
--- 150,154 ----
     ++ Q.EXISTS_TAC `\v. if v "n" = 1 then 1 else 0`
     ++ Q.EXISTS_TAC `\v. 0`
!    ++ REWRITE_TAC [wp_def, assign_eta]
     ++ SIMP_TAC int_ss [Min_def]
     ++ SIMP_TAC posreal_ss [preal_min_def]);
***************
*** 174,178 ****
    (``!v e. healthy (wp (Assign v e))``,
     RW_TAC posreal_ss
!    [wp_def, healthy_def, sublinear_def, feasible_def, Zero_def, sub_mono]
     ++ RW_TAC real_ss [up_continuous_def, lub_def, Leq_def, expect_def]
     >> (BETA_TAC ++ PROVE_TAC [])
--- 173,178 ----
    (``!v e. healthy (wp (Assign v e))``,
     RW_TAC posreal_ss
!    [wp_def, healthy_def, sublinear_def, feasible_def, Zero_def, sub_mono,
!     assign_eta]
     ++ RW_TAC real_ss [up_continuous_def, lub_def, Leq_def, expect_def]
     >> (BETA_TAC ++ PROVE_TAC [])
***************
*** 371,375 ****
          healthy (wp prog) /\ healthy (wp prog') ==>
          healthy (wp (Prob f prog prog'))``,
!    RW_TAC real_ss [wp_def]
     ++ RW_TAC real_ss [healthy_def]
     << [RW_TAC posreal_ss [feasible_def]
--- 371,375 ----
          healthy (wp prog) /\ healthy (wp prog') ==>
          healthy (wp (Prob f prog prog'))``,
!    RW_TAC real_ss [wp_def, lin_eta]
     ++ RW_TAC real_ss [healthy_def]
     << [RW_TAC posreal_ss [feasible_def]
***************
*** 529,535 ****
  
  val wp_while_monotonic = lemma
!   (``!trans cnd l.
         healthy trans /\
!        (!r. expect_lfp (\e s. (if cnd s then trans e s else r s)) = l r) ==>
         monotonic (expect,Leq) l``,
     RW_TAC std_ss []
--- 529,535 ----
  
  val wp_while_monotonic = lemma
!   (``!trans cond l.
         healthy trans /\
!        (!r. expect_lfp (\e s. (if cond s then trans e s else r s)) = l r) ==>
         monotonic (expect,Leq) l``,
     RW_TAC std_ss []
***************
*** 547,556 ****
  
  val wp_while_upcontinuous = lemma
!   (``!trans cnd l.
         healthy trans /\
!        (!r. expect_lfp (\e s. (if cnd s then trans e s else r s)) = l r) ==>
!        (!r. (\s. (if cnd s then trans (l r) s else r s)) = l r) /\
         (!r y.
!           Leq (\s. (if cnd s then trans y s else r s)) y ==> Leq (l r) y) ==>
         up_continuous (expect,Leq) l``,
     RW_TAC std_ss []
--- 547,556 ----
  
  val wp_while_upcontinuous = lemma
!   (``!trans cond l.
         healthy trans /\
!        (!r. expect_lfp (\e s. (if cond s then trans e s else r s)) = l r) ==>
!        (!r. (\s. (if cond s then trans (l r) s else r s)) = l r) /\
         (!r y.
!           Leq (\s. (if cond s then trans y s else r s)) y ==> Leq (l r) y) ==>
         up_continuous (expect,Leq) l``,
     RW_TAC std_ss []
***************
*** 598,602 ****
         ++ Q.PAT_ASSUM `chain X Y` MP_TAC
         ++ RW_TAC posreal_ss [chain_def, expect_def]
!        ++ MP_TAC (Q.SPECL [`trans`, `cnd`, `l`] wp_while_monotonic)
         ++ RW_TAC std_ss [monotonic_def, expect_def]
         ++ METIS_TAC [])
--- 598,602 ----
         ++ Q.PAT_ASSUM `chain X Y` MP_TAC
         ++ RW_TAC posreal_ss [chain_def, expect_def]
!        ++ MP_TAC (Q.SPECL [`trans`, `cond`, `l`] wp_while_monotonic)
         ++ RW_TAC std_ss [monotonic_def, expect_def]
         ++ METIS_TAC [])
***************
*** 611,619 ****
  
  val wp_while_sublinear1 = lemma
!   (``!cnd prog l.
         healthy (wp prog) /\
!        (!r. (\s. (if cnd s then wp prog (l r) s else r s)) = l r) /\
         (!r y.
!           Leq (\s. (if cnd s then wp prog y s else r s)) y ==> Leq (l r) y) ==>
         (!r c s. ~(c = infty) ==> l r s - c <= l (\s'. r s' - c) s)``,
     RW_TAC posreal_ss []
--- 611,619 ----
  
  val wp_while_sublinear1 = lemma
!   (``!cond prog l.
         healthy (wp prog) /\
!        (!r. (\s. (if cond s then wp prog (l r) s else r s)) = l r) /\
         (!r y.
!           Leq (\s. (if cond s then wp prog y s else r s)) y ==> Leq (l r) y) ==>
         (!r c s. ~(c = infty) ==> l r s - c <= l (\s'. r s' - c) s)``,
     RW_TAC posreal_ss []
***************
*** 640,651 ****
  
  val healthy_wp_while = lemma
!   (``!cnd prog. healthy (wp prog) ==> healthy (wp (While cnd prog))``,
!    RW_TAC real_ss [wp_def]
     ++ Know
        `!r.
!          (expect_lfp (\e s. (if cnd s then wp prog e s else r s)) =
!           (\r. expect_lfp (\e s. (if cnd s then wp prog e s else r s))) r) /\
!          lfp (expect,Leq) (\e s. if cnd s then wp prog e s else r s)
!          ((\r. expect_lfp (\e s. (if cnd s then wp prog e s else r s))) r)`
     >> (RW_TAC std_ss []
         ++ MATCH_MP_TAC expect_lfp_def
--- 640,651 ----
  
  val healthy_wp_while = lemma
!   (``!cond prog. healthy (wp prog) ==> healthy (wp (While cond prog))``,
!    RW_TAC real_ss [wp_def, cond_eta]
     ++ Know
        `!r.
!          (expect_lfp (\e s. (if cond s then wp prog e s else r s)) =
!           (\r. expect_lfp (\e s. (if cond s then wp prog e s else r s))) r) /\
!          lfp (expect,Leq) (\e s. if cond s then wp prog e s else r s)
!          ((\r. expect_lfp (\e s. (if cond s then wp prog e s else r s))) r)`
     >> (RW_TAC std_ss []
         ++ MATCH_MP_TAC expect_lfp_def
***************
*** 660,668 ****
         ++ METIS_TAC [healthy_mono])
     ++ Q.SPEC_TAC
!       (`\r. expect_lfp (\e s. (if cnd s then wp prog e s else r s))`, `l`)
     ++ SIMP_TAC std_ss [lfp_def, expect_def, FORALL_AND_THM]
     ++ RW_TAC std_ss []
!    ++ MP_TAC (Q.SPECL [`cnd`, `l`] (Q.ISPEC `wp prog` wp_while_monotonic))
!    ++ MP_TAC (Q.SPECL [`cnd`, `l`] (Q.ISPEC `wp prog` wp_while_upcontinuous))
     ++ RW_TAC std_ss []
     ++ ASM_SIMP_TAC real_ss [healthy_def]
--- 660,668 ----
         ++ METIS_TAC [healthy_mono])
     ++ Q.SPEC_TAC
!       (`\r. expect_lfp (\e s. (if cond s then wp prog e s else r s))`, `l`)
     ++ SIMP_TAC std_ss [lfp_def, expect_def, FORALL_AND_THM]
     ++ RW_TAC std_ss []
!    ++ MP_TAC (Q.SPECL [`cond`, `l`] (Q.ISPEC `wp prog` wp_while_monotonic))
!    ++ MP_TAC (Q.SPECL [`cond`, `l`] (Q.ISPEC `wp prog` wp_while_upcontinuous))
     ++ RW_TAC std_ss []
     ++ ASM_SIMP_TAC real_ss [healthy_def]
***************
*** 682,686 ****
         ++ METIS_TAC [feasible_def, healthy_feasible])
     ++ RW_TAC real_ss [sublinear_alt]
!    << [MP_TAC (Q.SPECL [`cnd`, `prog`, `l`] wp_while_sublinear1)
         ++ RW_TAC std_ss [],
         Suff `Leq (\s. c * l r s) (l (\s'. c * r s'))` >> RW_TAC std_ss [Leq_def]
--- 682,686 ----
         ++ METIS_TAC [feasible_def, healthy_feasible])
     ++ RW_TAC real_ss [sublinear_alt]
!    << [MP_TAC (Q.SPECL [`cond`, `prog`, `l`] wp_while_sublinear1)
         ++ RW_TAC std_ss [],
         Suff `Leq (\s. c * l r s) (l (\s'. c * r s'))` >> RW_TAC std_ss [Leq_def]
***************
*** 874,878 ****
         ++ Know `!s. l r s <= & n`
         >> (GEN_TAC
!            ++ MP_TAC (Q.SPECL [`cnd`, `prog`, `l`] wp_while_sublinear1)
             ++ ASM_SIMP_TAC std_ss []
             ++ DISCH_THEN (MP_TAC o Q.SPECL [`r`, `& n`, `s`])
--- 874,878 ----
         ++ Know `!s. l r s <= & n`
         >> (GEN_TAC
!            ++ MP_TAC (Q.SPECL [`cond`, `prog`, `l`] wp_while_sublinear1)
             ++ ASM_SIMP_TAC std_ss []
             ++ DISCH_THEN (MP_TAC o Q.SPECL [`r`, `& n`, `s`])
***************
*** 910,914 ****
            (fn th => CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV [GSYM th])))       
         ++ RW_TAC posreal_ss [Leq_def]
!        ++ REVERSE (Cases_on `cnd s` ++ ASM_SIMP_TAC posreal_ss [add_sub])
         ++ POP_ASSUM (K ALL_TAC)
         ++ MP_TAC (Q.SPECL [`\s. l (\s' : state. r1 s' + r s' : posreal) s`,
--- 910,914 ----
            (fn th => CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV [GSYM th])))       
         ++ RW_TAC posreal_ss [Leq_def]
!        ++ REVERSE (Cases_on `cond s` ++ ASM_SIMP_TAC posreal_ss [add_sub])
         ++ POP_ASSUM (K ALL_TAC)
         ++ MP_TAC (Q.SPECL [`\s. l (\s' : state. r1 s' + r s' : posreal) s`,
***************
*** 971,979 ****
     RW_TAC std_ss [wp_def]);
  
! val wp_cond = store_thm
!   ("wp_cond",
!    ``!c a b r.
!        wp (Cond c a b) r = \s. if c s then wp a r s else wp b r s``,
!    RW_TAC std_ss [wp_def, Cond_def]
     ++ CONV_TAC FUN_EQ_CONV
     ++ RW_TAC posreal_ss [bound1_basic]);
--- 971,978 ----
     RW_TAC std_ss [wp_def]);
  
! val wp_if = store_thm
!   ("wp_if",
!    ``!c a b r. wp (If c a b) r = Cond c (wp a r) (wp b r)``,
!    RW_TAC std_ss [wp_def, If_def, cond_eta, lin_eta]
     ++ CONV_TAC FUN_EQ_CONV
     ++ RW_TAC posreal_ss [bound1_basic]);
***************
*** 995,999 ****
    ("refines_demon_prob",
     ``!f p q. refines (wp (Demon p q)) (wp (Prob f p q))``,
!    RW_TAC std_ss [refines_def, wp_def, Min_def, Leq_def, min_le_lin]);
  
  (* ------------------------------------------------------------------------- *)
--- 994,998 ----
    ("refines_demon_prob",
     ``!f p q. refines (wp (Demon p q)) (wp (Prob f p q))``,
!    RW_TAC std_ss [refines_def, wp_def, Min_def, Leq_def, min_le_lin, Lin_def]);
  
  (* ------------------------------------------------------------------------- *)
***************
*** 1004,1013 ****
    `(wlp Abort = \r. Magic) /\
     (wlp Skip = \r. r) /\
!    (wlp (Assign v e) = \r s. r (\w. if w = v then e s else s w)) /\
     (wlp (Seq a b) = \r. wlp a (wlp b r)) /\
     (wlp (Demon a b) = \r. Min (wlp a r) (wlp b r)) /\
!    (wlp (Prob p a b) =
!     \r s. let x = bound1 (p s) in x * wlp a r s + (1 - x) * wlp b r s) /\
!    (wlp (While c b) = \r. expect_gfp (\e s. if c s then wlp b e s else r s))`;
  
  (* ------------------------------------------------------------------------- *)
--- 1003,1011 ----
    `(wlp Abort = \r. Magic) /\
     (wlp Skip = \r. r) /\
!    (wlp (Assign v e) = \r s. r (assign v e s)) /\
     (wlp (Seq a b) = \r. wlp a (wlp b r)) /\
     (wlp (Demon a b) = \r. Min (wlp a r) (wlp b r)) /\
!    (wlp (Prob p a b) = \r. Lin p (wlp a r) (wlp b r)) /\
!    (wlp (While c b) = \r. expect_gfp (\e. Cond c (wlp b e) r))`;
  
  (* ------------------------------------------------------------------------- *)
***************
*** 1020,1030 ****
     ``!p r1 r2. Leq r1 r2 ==> Leq (wlp p r1) (wlp p r2)``,
     (Induct ++ RW_TAC std_ss [wlp_def, leq_refl])
!    << [FULL_SIMP_TAC std_ss [Leq_def],
         METIS_TAC [min_leq2_imp],
!        RW_TAC std_ss [Leq_def]
         ++ MATCH_MP_TAC le_add2
         ++ METIS_TAC [Leq_def, le_lmul_imp, le_add2],
         MATCH_MP_TAC refines_gfp
!        ++ RW_TAC std_ss [monotonic_def, refines_def, Leq_def]
         ++ RW_TAC posreal_ss []
         ++ METIS_TAC [Leq_def]]);
--- 1018,1028 ----
     ``!p r1 r2. Leq r1 r2 ==> Leq (wlp p r1) (wlp p r2)``,
     (Induct ++ RW_TAC std_ss [wlp_def, leq_refl])
!    << [FULL_SIMP_TAC std_ss [Leq_def, assign_eta],
         METIS_TAC [min_leq2_imp],
!        RW_TAC std_ss [Leq_def, lin_eta]
         ++ MATCH_MP_TAC le_add2
         ++ METIS_TAC [Leq_def, le_lmul_imp, le_add2],
         MATCH_MP_TAC refines_gfp
!        ++ RW_TAC std_ss [monotonic_def, refines_def, Leq_def, cond_eta]
         ++ RW_TAC posreal_ss []
         ++ METIS_TAC [Leq_def]]);
***************
*** 1038,1051 ****
  val wlp_while = store_thm
    ("wlp_while",
!    ``!cnd body pre post.
!        Leq pre (\s. if cnd s then wlp body pre s else post s) ==>
!        Leq pre (wlp (While cnd body) post)``,
!    RW_TAC std_ss [wlp_def]
     ++ Know
        `!r.
!          (expect_gfp (\e s. (if cnd s then wlp body e s else r s)) =
!           (\r. expect_gfp (\e s. (if cnd s then wlp body e s else r s))) r) /\
!          gfp (expect,Leq) (\e s. if cnd s then wlp body e s else r s)
!          ((\r. expect_gfp (\e s. (if cnd s then wlp body e s else r s))) r)`
     >> (RW_TAC std_ss []
         ++ MATCH_MP_TAC expect_gfp_def
--- 1036,1049 ----
  val wlp_while = store_thm
    ("wlp_while",
!    ``!cond body pre post.
!        Leq pre (Cond cond (wlp body pre) post) ==>
!        Leq pre (wlp (While cond body) post)``,
!    RW_TAC std_ss [wlp_def, cond_eta]
     ++ Know
        `!r.
!          (expect_gfp (\e s. (if cond s then wlp body e s else r s)) =
!           (\r. expect_gfp (\e s. (if cond s then wlp body e s else r s))) r) /\
!          gfp (expect,Leq) (\e s. if cond s then wlp body e s else r s)
!          ((\r. expect_gfp (\e s. (if cond s then wlp body e s else r s))) r)`
     >> (RW_TAC std_ss []
         ++ MATCH_MP_TAC expect_gfp_def
***************
*** 1060,1064 ****
     ++ SIMP_TAC std_ss []
     ++ Q.SPEC_TAC
!       (`expect_gfp (\e s. (if cnd s then wlp body e s else post s))`, `g`)
     ++ RW_TAC std_ss [gfp_def, expect_def]);
  
--- 1058,1062 ----
     ++ SIMP_TAC std_ss []
     ++ Q.SPEC_TAC
!       (`expect_gfp (\e s. (if cond s then wlp body e s else post s))`, `g`)
     ++ RW_TAC std_ss [gfp_def, expect_def]);
  
***************
*** 1120,1129 ****
     ``!pre1 pre2 post p c1 c2.
         Leq pre1 (wlp c1 post) /\ Leq pre2 (wlp c2 post) ==>
!        Leq (prob p pre1 pre2) (wlp (Prob p c1 c2) post)``,
     RW_TAC std_ss [wlp_def, Leq_def]
     ++ MATCH_MP_TAC le_trans
!    ++ Q.EXISTS_TAC `prob p pre1 pre2 s`
     ++ RW_TAC std_ss []
!    ++ RW_TAC std_ss [prob_def, le_refl]
     ++ METIS_TAC [le_add2, le_lmul_imp]);
  
--- 1118,1127 ----
     ``!pre1 pre2 post p c1 c2.
         Leq pre1 (wlp c1 post) /\ Leq pre2 (wlp c2 post) ==>
!        Leq (Lin p pre1 pre2) (wlp (Prob p c1 c2) post)``,
     RW_TAC std_ss [wlp_def, Leq_def]
     ++ MATCH_MP_TAC le_trans
!    ++ Q.EXISTS_TAC `Lin p pre1 pre2 s`
     ++ RW_TAC std_ss []
!    ++ RW_TAC std_ss [Lin_def, le_refl]
     ++ METIS_TAC [le_add2, le_lmul_imp]);
  
***************
*** 1131,1135 ****
    ("wlp_while_vc",
     ``!pre post mid b c.
!        Leq mid (wlp c pre) /\ Leq pre (cond b mid post) ==>
         Leq pre (wlp (Assert pre (While b c)) post)``,
     RW_TAC std_ss []
--- 1129,1133 ----
    ("wlp_while_vc",
     ``!pre post mid b c.
!        Leq mid (wlp c pre) /\ Leq pre (Cond b mid post) ==>
         Leq pre (wlp (Assert pre (While b c)) post)``,
     RW_TAC std_ss []
***************
*** 1138,1154 ****
     ++ RW_TAC std_ss [leq_refl]
     ++ MATCH_MP_TAC wlp_while
!    ++ FULL_SIMP_TAC std_ss [Leq_def, cond_def]
     ++ METIS_TAC [le_trans]);
  
! val wlp_cond_vc = store_thm
!   ("wlp_cond_vc",
     ``!pre1 pre2 post b c1 c2.
         Leq pre1 (wlp c1 post) /\ Leq pre2 (wlp c2 post) ==>
!        Leq (cond b pre1 pre2) (wlp (Cond b c1 c2) post)``,
!    RW_TAC std_ss [Cond_def]
     ++ MATCH_MP_TAC leq_trans
!    ++ Q.EXISTS_TAC `prob (\s. if b s then 1 else 0) pre1 pre2`
     ++ REVERSE CONJ_TAC >> METIS_TAC [wlp_prob_vc]
!    ++ RW_TAC std_ss [Leq_def, bound1_def, prob_def, cond_def]
     ++ RW_TAC posreal_ss []
     ++ FULL_SIMP_TAC posreal_ss []);
--- 1136,1152 ----
     ++ RW_TAC std_ss [leq_refl]
     ++ MATCH_MP_TAC wlp_while
!    ++ FULL_SIMP_TAC std_ss [Leq_def, Cond_def]
     ++ METIS_TAC [le_trans]);
  
! val wlp_if_vc = store_thm
!   ("wlp_if_vc",
     ``!pre1 pre2 post b c1 c2.
         Leq pre1 (wlp c1 post) /\ Leq pre2 (wlp c2 post) ==>
!        Leq (Cond b pre1 pre2) (wlp (If b c1 c2) post)``,
!    RW_TAC std_ss [If_def]
     ++ MATCH_MP_TAC leq_trans
!    ++ Q.EXISTS_TAC `Lin (\s. if b s then 1 else 0) pre1 pre2`
     ++ REVERSE CONJ_TAC >> METIS_TAC [wlp_prob_vc]
!    ++ RW_TAC std_ss [Leq_def, bound1_def, Lin_def, Cond_def]
     ++ RW_TAC posreal_ss []
     ++ FULL_SIMP_TAC posreal_ss []);

Index: wpTools.sml
===================================================================
RCS file: /cvsroot/hol/hol98/examples/pgcl/src/wpTools.sml,v
retrieving revision 1.4
retrieving revision 1.5
diff -b -C2 -d -r1.4 -r1.5
*** wpTools.sml	30 Sep 2003 01:44:56 -0000	1.4
--- wpTools.sml	30 Sep 2003 15:39:15 -0000	1.5
***************
*** 90,94 ****
    val vc_solve = prolog
      [wlp_abort_vc, wlp_skip_vc, wlp_assign_vc, wlp_seq_vc, wlp_demon_vc,
!      wlp_prob_vc, wlp_while_vc, wlp_cond_vc, wlp_assert_vc];
  in
    fun vc_tac (asl,goal) =
--- 90,94 ----
    val vc_solve = prolog
      [wlp_abort_vc, wlp_skip_vc, wlp_assign_vc, wlp_seq_vc, wlp_demon_vc,
!      wlp_prob_vc, wlp_while_vc, wlp_if_vc, wlp_assert_vc];
  in
    fun vc_tac (asl,goal) =
***************
*** 189,193 ****
  local
    fun simps ths = ths @
!     [wlp_min_def, prob_def, cond_def, o_THM, magic_alt, assign_def];
  in
    val leq_tac =
--- 189,193 ----
  local
    fun simps ths = ths @
!     [wlp_min_def, Lin_def, Cond_def, o_THM, magic_alt, assign_def];
  in
    val leq_tac =

Update of /cvsroot/hol/hol98/examples/pgcl/doc
In directory sc8-pr-cvs1:/tmp/cvs-serv23484/doc

Modified Files:
	TODO 
Log Message:
Factorized out some common subexpressions as new definitions.


Index: TODO
===================================================================
RCS file: /cvsroot/hol/hol98/examples/pgcl/doc/TODO,v
retrieving revision 1.5
retrieving revision 1.6
diff -b -C2 -d -r1.5 -r1.6
*** TODO	26 Sep 2003 23:04:10 -0000	1.5
--- TODO	30 Sep 2003 15:39:14 -0000	1.6
***************
*** 24,25 ****
--- 24,26 ----
  - n-location rendezvous problem (strat n "i") a derived command
  - Miller-Rabin
+ - Pugh's skip lists

Update of /cvsroot/hol/hol98/examples/pgcl/examples
In directory sc8-pr-cvs1:/tmp/cvs-serv23484/examples

Modified Files:
	verification.sml 
Log Message:
Factorized out some common subexpressions as new definitions.


Index: verification.sml
===================================================================
RCS file: /cvsroot/hol/hol98/examples/pgcl/examples/verification.sml,v
retrieving revision 1.5
retrieving revision 1.6
diff -b -C2 -d -r1.5 -r1.6
*** verification.sml	30 Sep 2003 01:44:56 -0000	1.5
--- verification.sml	30 Sep 2003 15:39:15 -0000	1.6
***************
*** 38,42 ****
       (\v. if v"i" = v"j" then 1 else 0) = \v. 0``,
     RW_TAC arith_ss
!    [wp_def, Probchoice_def, Probs_def, Demonchoice_def,
      Demons_def, MAP, LENGTH, CHR_11, FUN_EQ_THM, Zero_def, Min_def]
     ++ FULL_SIMP_TAC int_ss []
--- 38,42 ----
       (\v. if v"i" = v"j" then 1 else 0) = \v. 0``,
     RW_TAC arith_ss
!    [wp_def, Probchoice_def, Probs_def, Demonchoice_def, assign_eta, lin_eta,
      Demons_def, MAP, LENGTH, CHR_11, FUN_EQ_THM, Zero_def, Min_def]
     ++ FULL_SIMP_TAC int_ss []
***************
*** 47,51 ****
       (\v. if v"i" = v"j" then 1 else 0) = \v. 1 / 2``,
     RW_TAC arith_ss
!    [wp_def, Probchoice_def, Probs_def, Demonchoice_def,
      Demons_def, MAP, LENGTH, CHR_11, FUN_EQ_THM, Zero_def, Min_def]
     ++ FULL_SIMP_TAC int_ss []
--- 47,51 ----
       (\v. if v"i" = v"j" then 1 else 0) = \v. 1 / 2``,
     RW_TAC arith_ss
!    [wp_def, Probchoice_def, Probs_def, Demonchoice_def, assign_eta, lin_eta,
      Demons_def, MAP, LENGTH, CHR_11, FUN_EQ_THM, Zero_def, Min_def]
     ++ FULL_SIMP_TAC int_ss []
***************
*** 69,73 ****
  val wp_loop = Count.apply prove
    (``!post. wp (While (\s. T) Skip) post = Zero``,
!    RW_TAC std_ss [wp_def]
     ++ Know `monotonic (expect,Leq) (\e s : state. e s)`
     >> (RW_TAC std_ss [monotonic_def]
--- 69,73 ----
  val wp_loop = Count.apply prove
    (``!post. wp (While (\s. T) Skip) post = Zero``,
!    RW_TAC std_ss [wp_def, cond_eta]
     ++ Know `monotonic (expect,Leq) (\e s : state. e s)`
     >> (RW_TAC std_ss [monotonic_def]
***************
*** 86,90 ****
  val wlp_loop = Count.apply prove
    (``!post. wlp (While (\s. T) Skip) post = Magic``,
!    RW_TAC std_ss [wlp_def]
     ++ Know `monotonic (expect,Leq) (\e s : state. e s)`
     >> (RW_TAC std_ss [monotonic_def]
--- 86,90 ----
  val wlp_loop = Count.apply prove
    (``!post. wlp (While (\s. T) Skip) post = Magic``,
!    RW_TAC std_ss [wlp_def, cond_eta]
     ++ Know `monotonic (expect,Leq) (\e s : state. e s)`
     >> (RW_TAC std_ss [monotonic_def]
***************
*** 148,164 ****
     ++ RW_TAC std_ss [montyhall_def, seq_assoc, Program_def]
     ++ RW_TAC std_ss [wp_incognito]
!    ++ RW_TAC std_ss [monty_switch_def, wp_def, CHR_11]
     ++ RW_TAC std_ss [wp_incognito_def] ++ RW_TAC std_ss [wp_incognito]
!    ++ RW_TAC int_ss [wp_def, Guards_def, guards_def, wp_cond, Demons_def,
!                      monty_reveal_def, Min_def]
     ++ RW_TAC posreal_ss [CHR_11]
     ++ RW_TAC std_ss [wp_incognito_def] ++ RW_TAC std_ss [wp_incognito]
     ++ RW_TAC list_ss [monty_choose_def, wp_def, Probchoice_def, Probs_def,
!                       CHR_11]
     ++ RW_TAC int_ss []
     ++ RW_TAC posreal_ss [bound1_basic, Zero_def]
     ++ RW_TAC std_ss [wp_incognito_def]
     ++ RW_TAC int_ss [monty_hide_def, MAP, wp_def, Demonchoice_def,
!                      Demons_def, Min_def]
     ++ RW_TAC posreal_reduce_ss [bound1_def]);
    
--- 148,164 ----
     ++ RW_TAC std_ss [montyhall_def, seq_assoc, Program_def]
     ++ RW_TAC std_ss [wp_incognito]
!    ++ RW_TAC std_ss [monty_switch_def, wp_def, CHR_11, assign_def]
     ++ RW_TAC std_ss [wp_incognito_def] ++ RW_TAC std_ss [wp_incognito]
!    ++ RW_TAC int_ss [wp_def, Guards_def, guards_def, wp_if, Demons_def,
!                      monty_reveal_def, Min_def, cond_eta, assign_def]
     ++ RW_TAC posreal_ss [CHR_11]
     ++ RW_TAC std_ss [wp_incognito_def] ++ RW_TAC std_ss [wp_incognito]
     ++ RW_TAC list_ss [monty_choose_def, wp_def, Probchoice_def, Probs_def,
!                       CHR_11, assign_def, lin_eta]
     ++ RW_TAC int_ss []
     ++ RW_TAC posreal_ss [bound1_basic, Zero_def]
     ++ RW_TAC std_ss [wp_incognito_def]
     ++ RW_TAC int_ss [monty_hide_def, MAP, wp_def, Demonchoice_def,
!                      Demons_def, Min_def, assign_def]
     ++ RW_TAC posreal_reduce_ss [bound1_def]);
    
***************
*** 179,183 ****
            (1 / 2) * r (\w. if w = "n" then v"n" - 1 else v w) +
            (1 / 2) * r (\w. if w = "n" then v"n" + 1 else v w))``,
!    RW_TAC posreal_ss [wp_def, lurch_def, bound1_basic, COND_RAND]
     ++ RW_TAC posreal_reduce_ss []);
  
--- 179,184 ----
            (1 / 2) * r (\w. if w = "n" then v"n" - 1 else v w) +
            (1 / 2) * r (\w. if w = "n" then v"n" + 1 else v w))``,
!    RW_TAC posreal_ss
!    [wp_def, lurch_def, bound1_basic, COND_RAND, assign_eta, lin_eta]
     ++ RW_TAC posreal_reduce_ss []);

Update of /cvsroot/hol/hol98/doc
In directory sc8-pr-cvs1:/tmp/cvs-serv20577

Modified Files:
	kananaskis-2.release 
Log Message:
An incompatibility blurb about my latest change.


Index: kananaskis-2.release
===================================================================
RCS file: /cvsroot/hol/hol98/doc/kananaskis-2.release,v
retrieving revision 1.12
retrieving revision 1.13
diff -b -C2 -d -r1.12 -r1.13
*** kananaskis-2.release	25 Sep 2003 15:36:08 -0000	1.12
--- kananaskis-2.release	30 Sep 2003 03:32:22 -0000	1.13
***************
*** 194,195 ****
--- 194,210 ----
      This can be relatively difficult to track down, but the fix is
      simple enough: change "someconv t" to "QCONV someconv t".
+ 
+   * bool_ss no longer includes the rewrite LET_THM, which turns an
+     expression of the form
+ 
+       let v = e1 in e2
+ 
+     into
+ 
+       e2[e1/v]
+ 
+     std_ss and its descendents in bossLib still include this rewrite.
+     This rewrite is also missing from the stateful rewriter (srw_ss(),
+     and SRW_TAC).  This is so the stateful rewriter can implement a
+     rewriting strategy that only performs the substitution when e1 has
+     simplified to a "real value".

Update of /cvsroot/hol/hol98/src/prob
In directory sc8-pr-cvs1:/tmp/cvs-serv15073/src/prob

Modified Files:
	prob_indepScript.sml prob_uniformScript.sml 
Log Message:
A new approach to handling LETs for the stateful rewriter.  Introduces an 
incompatibility in that bool_ss no longer rewrites LET f x to f x (std_ss
still does though).  The new strategy is: 

   Don't put LET_THM into any of the simpsets, but rather
   put in specialised versions of this that allow "values" to be
   substituted into the body.  Thus ``let v = e1 in e2`` will only reduce
   to  e2[e1/v] when e1 has been reduced to a proper value.  Better,
   allow partial substitution to happen when e1 has become partially
   value-like.  For example, if we get to

      let v = SUC e in v + v

   and e isn't necessarily evaluated, we can still move this to

      let v = e in SUC v + SUC v

   The rewrite for this is  |- LET f (SUC e) = LET (\v. f (SUC v)) e
   Comparable rewrites for constructors of any type are easy to state
   and prove.  Arguably, these theorems should be generated when new
   types are defined, and stored in the TypeBase.  Because I know Konrad
   will be (is already?) messing with the TypeBase to support ML lifting,
   I haven't done this for Hol_datatype (it's not quite so easy to see
   how to capture the notion of "record value").

   I have written the appropriate theorems for the obivous built-in
   types.  This strategy gives the simplifier a notion of "value" that
   is different from "can't reduce any more by the given rewrites"
   (which is what CBV_CONV uses).  The problem with CBV_CONV, or a
   congruence rule that always performs the reduction from LET f e to 
   f e is that you can get big explosions in term size, which is 
   particularly bad if you are doing symbolic evaluation.

Have fixed problems arising in probability (which was using its own 
version of std_ss, and those places where srw_ss() is being used.  The
examples/lambda directory uses SRW_TAC pretty extensively, so there are
fixes required there.  The easiest way is to just put LET_THM back into
the stateful simpset and to forget about it.  The general problem with
the stateful system as it stands is that it is very easy to put things
into it, but impossible to pull them out.  Isabelle has some way of 
doing this that might be worth looking into.



Index: prob_indepScript.sml
===================================================================
RCS file: /cvsroot/hol/hol98/src/prob/prob_indepScript.sml,v
retrieving revision 1.8
retrieving revision 1.9
diff -b -C2 -d -r1.8 -r1.9
*** prob_indepScript.sml	1 Aug 2003 07:46:16 -0000	1.8
--- prob_indepScript.sml	30 Sep 2003 03:13:17 -0000	1.9
***************
*** 23,27 ****
    val std_ss' =
      (boolSimps.bool_ss ++ pairSimps.PAIR_ss ++ optionSimps.OPTION_ss ++
!      numSimps.REDUCE_ss ++ sumSimps.SUM_ss ++ boolSimps.ETA_ss);
  end;
  
--- 23,28 ----
    val std_ss' =
      (boolSimps.bool_ss ++ pairSimps.PAIR_ss ++ optionSimps.OPTION_ss ++
!      numSimps.REDUCE_ss ++ sumSimps.SUM_ss ++ boolSimps.ETA_ss ++
!      rewrites [LET_THM]);
  end;
  

Index: prob_uniformScript.sml
===================================================================
RCS file: /cvsroot/hol/hol98/src/prob/prob_uniformScript.sml,v
retrieving revision 1.7
retrieving revision 1.8
diff -b -C2 -d -r1.7 -r1.8
*** prob_uniformScript.sml	30 Jun 2003 08:17:42 -0000	1.7
--- prob_uniformScript.sml	30 Sep 2003 03:13:17 -0000	1.8
***************
*** 23,27 ****
    val std_ss' =
      (boolSimps.bool_ss ++ pairSimps.PAIR_ss ++ optionSimps.OPTION_ss ++
!      numSimps.REDUCE_ss ++ sumSimps.SUM_ss ++ boolSimps.ETA_ss);
  end;
  
--- 23,28 ----
    val std_ss' =
      (boolSimps.bool_ss ++ pairSimps.PAIR_ss ++ optionSimps.OPTION_ss ++
!      numSimps.REDUCE_ss ++ sumSimps.SUM_ss ++ boolSimps.ETA_ss ++
!      rewrites [LET_THM]);
  end;

Update of /cvsroot/hol/hol98/src/bag
In directory sc8-pr-cvs1:/tmp/cvs-serv15073/src/bag

Modified Files:
	bagScript.sml 
Log Message:
A new approach to handling LETs for the stateful rewriter.  Introduces an 
incompatibility in that bool_ss no longer rewrites LET f x to f x (std_ss
still does though).  The new strategy is: 

   Don't put LET_THM into any of the simpsets, but rather
   put in specialised versions of this that allow "values" to be
   substituted into the body.  Thus ``let v = e1 in e2`` will only reduce
   to  e2[e1/v] when e1 has been reduced to a proper value.  Better,
   allow partial substitution to happen when e1 has become partially
   value-like.  For example, if we get to

      let v = SUC e in v + v

   and e isn't necessarily evaluated, we can still move this to

      let v = e in SUC v + SUC v

   The rewrite for this is  |- LET f (SUC e) = LET (\v. f (SUC v)) e
   Comparable rewrites for constructors of any type are easy to state
   and prove.  Arguably, these theorems should be generated when new
   types are defined, and stored in the TypeBase.  Because I know Konrad
   will be (is already?) messing with the TypeBase to support ML lifting,
   I haven't done this for Hol_datatype (it's not quite so easy to see
   how to capture the notion of "record value").

   I have written the appropriate theorems for the obivous built-in
   types.  This strategy gives the simplifier a notion of "value" that
   is different from "can't reduce any more by the given rewrites"
   (which is what CBV_CONV uses).  The problem with CBV_CONV, or a
   congruence rule that always performs the reduction from LET f e to 
   f e is that you can get big explosions in term size, which is 
   particularly bad if you are doing symbolic evaluation.

Have fixed problems arising in probability (which was using its own 
version of std_ss, and those places where srw_ss() is being used.  The
examples/lambda directory uses SRW_TAC pretty extensively, so there are
fixes required there.  The easiest way is to just put LET_THM back into
the stateful simpset and to forget about it.  The general problem with
the stateful system as it stands is that it is very easy to put things
into it, but impossible to pull them out.  Isabelle has some way of 
doing this that might be worth looking into.



Index: bagScript.sml
===================================================================
RCS file: /cvsroot/hol/hol98/src/bag/bagScript.sml,v
retrieving revision 1.23
retrieving revision 1.24
diff -b -C2 -d -r1.23 -r1.24
*** bagScript.sml	29 Sep 2003 05:02:26 -0000	1.23
--- bagScript.sml	30 Sep 2003 03:13:16 -0000	1.24
***************
*** 1357,1360 ****
--- 1357,1361 ----
     ---------------------------------------------------------------------- *)
  
+ val _ = augment_srw_ss [simpLib.rewrites [LET_THM]]
  val BAG_IMAGE_DEF = new_definition(
    "BAG_IMAGE_DEF",

Update of /cvsroot/hol/hol98/src/boss
In directory sc8-pr-cvs1:/tmp/cvs-serv15073/src/boss

Modified Files:
	bossLib.sml 
Log Message:
A new approach to handling LETs for the stateful rewriter.  Introduces an 
incompatibility in that bool_ss no longer rewrites LET f x to f x (std_ss
still does though).  The new strategy is: 

   Don't put LET_THM into any of the simpsets, but rather
   put in specialised versions of this that allow "values" to be
   substituted into the body.  Thus ``let v = e1 in e2`` will only reduce
   to  e2[e1/v] when e1 has been reduced to a proper value.  Better,
   allow partial substitution to happen when e1 has become partially
   value-like.  For example, if we get to

      let v = SUC e in v + v

   and e isn't necessarily evaluated, we can still move this to

      let v = e in SUC v + SUC v

   The rewrite for this is  |- LET f (SUC e) = LET (\v. f (SUC v)) e
   Comparable rewrites for constructors of any type are easy to state
   and prove.  Arguably, these theorems should be generated when new
   types are defined, and stored in the TypeBase.  Because I know Konrad
   will be (is already?) messing with the TypeBase to support ML lifting,
   I haven't done this for Hol_datatype (it's not quite so easy to see
   how to capture the notion of "record value").

   I have written the appropriate theorems for the obivous built-in
   types.  This strategy gives the simplifier a notion of "value" that
   is different from "can't reduce any more by the given rewrites"
   (which is what CBV_CONV uses).  The problem with CBV_CONV, or a
   congruence rule that always performs the reduction from LET f e to 
   f e is that you can get big explosions in term size, which is 
   particularly bad if you are doing symbolic evaluation.

Have fixed problems arising in probability (which was using its own 
version of std_ss, and those places where srw_ss() is being used.  The
examples/lambda directory uses SRW_TAC pretty extensively, so there are
fixes required there.  The easiest way is to just put LET_THM back into
the stateful simpset and to forget about it.  The general problem with
the stateful system as it stands is that it is very easy to put things
into it, but impossible to pull them out.  Isabelle has some way of 
doing this that might be worth looking into.



Index: bossLib.sml
===================================================================
RCS file: /cvsroot/hol/hol98/src/boss/bossLib.sml,v
retrieving revision 1.54
retrieving revision 1.55
diff -b -C2 -d -r1.54 -r1.55
*** bossLib.sml	4 Aug 2003 19:47:15 -0000	1.54
--- bossLib.sml	30 Sep 2003 03:13:16 -0000	1.55
***************
*** 88,92 ****
  val std_ss =
       (boolSimps.bool_ss ++ pairSimps.PAIR_ss ++ optionSimps.OPTION_ss ++
!       numSimps.REDUCE_ss ++ sumSimps.SUM_ss ++ combinSimps.COMBIN_ss)
  
  val arith_ss = std_ss ++ numSimps.ARITH_ss
--- 88,93 ----
  val std_ss =
       (boolSimps.bool_ss ++ pairSimps.PAIR_ss ++ optionSimps.OPTION_ss ++
!       numSimps.REDUCE_ss ++ sumSimps.SUM_ss ++ combinSimps.COMBIN_ss ++
!       rewrites [LET_THM])
  
  val arith_ss = std_ss ++ numSimps.ARITH_ss

Update of /cvsroot/hol/hol98/examples/lambda
In directory sc8-pr-cvs1:/tmp/cvs-serv15073/examples/lambda

Modified Files:
	chap2Script.sml finite_developmentsScript.sml 
	labelledTermsScript.sml term_posnsScript.sml 
Log Message:
A new approach to handling LETs for the stateful rewriter.  Introduces an 
incompatibility in that bool_ss no longer rewrites LET f x to f x (std_ss
still does though).  The new strategy is: 

   Don't put LET_THM into any of the simpsets, but rather
   put in specialised versions of this that allow "values" to be
   substituted into the body.  Thus ``let v = e1 in e2`` will only reduce
   to  e2[e1/v] when e1 has been reduced to a proper value.  Better,
   allow partial substitution to happen when e1 has become partially
   value-like.  For example, if we get to

      let v = SUC e in v + v

   and e isn't necessarily evaluated, we can still move this to

      let v = e in SUC v + SUC v

   The rewrite for this is  |- LET f (SUC e) = LET (\v. f (SUC v)) e
   Comparable rewrites for constructors of any type are easy to state
   and prove.  Arguably, these theorems should be generated when new
   types are defined, and stored in the TypeBase.  Because I know Konrad
   will be (is already?) messing with the TypeBase to support ML lifting,
   I haven't done this for Hol_datatype (it's not quite so easy to see
   how to capture the notion of "record value").

   I have written the appropriate theorems for the obivous built-in
   types.  This strategy gives the simplifier a notion of "value" that
   is different from "can't reduce any more by the given rewrites"
   (which is what CBV_CONV uses).  The problem with CBV_CONV, or a
   congruence rule that always performs the reduction from LET f e to 
   f e is that you can get big explosions in term size, which is 
   particularly bad if you are doing symbolic evaluation.

Have fixed problems arising in probability (which was using its own 
version of std_ss, and those places where srw_ss() is being used.  The
examples/lambda directory uses SRW_TAC pretty extensively, so there are
fixes required there.  The easiest way is to just put LET_THM back into
the stateful simpset and to forget about it.  The general problem with
the stateful system as it stands is that it is very easy to put things
into it, but impossible to pull them out.  Isabelle has some way of 
doing this that might be worth looking into.



Index: chap2Script.sml
===================================================================
RCS file: /cvsroot/hol/hol98/examples/lambda/chap2Script.sml,v
retrieving revision 1.1
retrieving revision 1.2
diff -b -C2 -d -r1.1 -r1.2
*** chap2Script.sml	6 Aug 2003 05:48:19 -0000	1.1
--- chap2Script.sml	30 Sep 2003 03:13:16 -0000	1.2
***************
*** 1015,1019 ****
         enf ([VAR v/x] t) /\
         (is_comb t ==> (rand t = VAR x) ==> x IN FV (rator t)))``,
!   SRW_TAC [][] THEN NEW_ELIM_TAC THEN Q.X_GEN_TAC `y` THEN
    REPEAT STRIP_TAC THEN
    SRW_TAC [][lemma14a] THEN EQ_TAC THEN SRW_TAC [][] THEN
--- 1015,1019 ----
         enf ([VAR v/x] t) /\
         (is_comb t ==> (rand t = VAR x) ==> x IN FV (rator t)))``,
!   SRW_TAC [][LET_THM] THEN NEW_ELIM_TAC THEN Q.X_GEN_TAC `y` THEN
    REPEAT STRIP_TAC THEN
    SRW_TAC [][lemma14a] THEN EQ_TAC THEN SRW_TAC [][] THEN
***************
*** 1030,1034 ****
    ``!t R. RENAMING R ==> (enf (t ISUB R) = enf t)``,
    HO_MATCH_MP_TAC nc_INDUCTION2 THEN
!   SRW_TAC [][enf_def, ISUB_APP, ISUB_VAR_RENAME, ISUB_CON] THEN
    Q.EXISTS_TAC `{}` THEN SRW_TAC [][] THEN NEW_ELIM_TAC THEN
    Q.X_GEN_TAC `nv` THEN (* bound variable of right hand term *)
--- 1030,1034 ----
    ``!t R. RENAMING R ==> (enf (t ISUB R) = enf t)``,
    HO_MATCH_MP_TAC nc_INDUCTION2 THEN
!   SRW_TAC [][enf_def, ISUB_APP, ISUB_VAR_RENAME, ISUB_CON, LET_THM] THEN
    Q.EXISTS_TAC `{}` THEN SRW_TAC [][] THEN NEW_ELIM_TAC THEN
    Q.X_GEN_TAC `nv` THEN (* bound variable of right hand term *)
***************
*** 1040,1044 ****
    ] THEN
    SRW_TAC [][ISUB_LAM, SUB_ISUB_SINGLETON, ISUB_APPEND, RENAMING_THM,
!              enf_def] THEN SRW_TAC [][] THEN
    EQ_TAC THEN SRW_TAC [][lemma14a] THEN
    Q.PAT_ASSUM `RENAMING R` ASSUME_TAC THEN
--- 1040,1044 ----
    ] THEN
    SRW_TAC [][ISUB_LAM, SUB_ISUB_SINGLETON, ISUB_APPEND, RENAMING_THM,
!              enf_def, LET_THM] THEN SRW_TAC [][] THEN
    EQ_TAC THEN SRW_TAC [][lemma14a] THEN
    Q.PAT_ASSUM `RENAMING R` ASSUME_TAC THEN
***************
*** 1078,1082 ****
    "enf_thm",
    SIMP_RULE (srw_ss()) [RENAMING_THM, SUB_ISUB_SINGLETON, ISUB_APPEND,
!                         enf_renaming_invariant] enf_def);
  
  val benf_def = Define`benf t = bnf t /\ enf t`;
--- 1078,1082 ----
    "enf_thm",
    SIMP_RULE (srw_ss()) [RENAMING_THM, SUB_ISUB_SINGLETON, ISUB_APPEND,
!                         enf_renaming_invariant, LET_THM] enf_def);
  
  val benf_def = Define`benf t = bnf t /\ enf t`;

Index: finite_developmentsScript.sml
===================================================================
RCS file: /cvsroot/hol/hol98/examples/lambda/finite_developmentsScript.sml,v
retrieving revision 1.1
retrieving revision 1.2
diff -b -C2 -d -r1.1 -r1.2
*** finite_developmentsScript.sml	6 Aug 2003 05:48:19 -0000	1.1
--- finite_developmentsScript.sml	30 Sep 2003 03:13:16 -0000	1.2
***************
*** 9,12 ****
--- 9,14 ----
  local open pred_setLib in end
  
+ val _ = augment_srw_ss [simpLib.rewrites [LET_THM]]
+ 
  val _ = new_theory "finite_developments";
  

Index: labelledTermsScript.sml
===================================================================
RCS file: /cvsroot/hol/hol98/examples/lambda/labelledTermsScript.sml,v
retrieving revision 1.1
retrieving revision 1.2
diff -b -C2 -d -r1.1 -r1.2
*** labelledTermsScript.sml	6 Aug 2003 05:48:19 -0000	1.1
--- labelledTermsScript.sml	30 Sep 2003 03:13:16 -0000	1.2
***************
*** 8,11 ****
--- 8,13 ----
  local open pred_setLib in end
  
+ val _ = augment_srw_ss [simpLib.rewrites [LET_THM]]
+ 
  val _ = new_theory "labelledTerms";
  

Index: term_posnsScript.sml
===================================================================
RCS file: /cvsroot/hol/hol98/examples/lambda/term_posnsScript.sml,v
retrieving revision 1.1
retrieving revision 1.2
diff -b -C2 -d -r1.1 -r1.2
*** term_posnsScript.sml	6 Aug 2003 05:48:19 -0000	1.1
--- term_posnsScript.sml	30 Sep 2003 03:13:16 -0000	1.2
***************
*** 5,8 ****
--- 5,9 ----
  val _ = new_theory "term_posns";
  
+ val _ = augment_srw_ss [simpLib.rewrites [LET_THM]]
  val _ = Hol_datatype `redpos = Lt | Rt | In`;

Update of /cvsroot/hol/hol98/src/path
In directory sc8-pr-cvs1:/tmp/cvs-serv15073/src/path

Modified Files:
	pathScript.sml 
Log Message:
A new approach to handling LETs for the stateful rewriter.  Introduces an 
incompatibility in that bool_ss no longer rewrites LET f x to f x (std_ss
still does though).  The new strategy is: 

   Don't put LET_THM into any of the simpsets, but rather
   put in specialised versions of this that allow "values" to be
   substituted into the body.  Thus ``let v = e1 in e2`` will only reduce
   to  e2[e1/v] when e1 has been reduced to a proper value.  Better,
   allow partial substitution to happen when e1 has become partially
   value-like.  For example, if we get to

      let v = SUC e in v + v

   and e isn't necessarily evaluated, we can still move this to

      let v = e in SUC v + SUC v

   The rewrite for this is  |- LET f (SUC e) = LET (\v. f (SUC v)) e
   Comparable rewrites for constructors of any type are easy to state
   and prove.  Arguably, these theorems should be generated when new
   types are defined, and stored in the TypeBase.  Because I know Konrad
   will be (is already?) messing with the TypeBase to support ML lifting,
   I haven't done this for Hol_datatype (it's not quite so easy to see
   how to capture the notion of "record value").

   I have written the appropriate theorems for the obivous built-in
   types.  This strategy gives the simplifier a notion of "value" that
   is different from "can't reduce any more by the given rewrites"
   (which is what CBV_CONV uses).  The problem with CBV_CONV, or a
   congruence rule that always performs the reduction from LET f e to 
   f e is that you can get big explosions in term size, which is 
   particularly bad if you are doing symbolic evaluation.

Have fixed problems arising in probability (which was using its own 
version of std_ss, and those places where srw_ss() is being used.  The
examples/lambda directory uses SRW_TAC pretty extensively, so there are
fixes required there.  The easiest way is to just put LET_THM back into
the stateful simpset and to forget about it.  The general problem with
the stateful system as it stands is that it is very easy to put things
into it, but impossible to pull them out.  Isabelle has some way of 
doing this that might be worth looking into.



Index: pathScript.sml
===================================================================
RCS file: /cvsroot/hol/hol98/src/path/pathScript.sml,v
retrieving revision 1.12
retrieving revision 1.13
diff -b -C2 -d -r1.12 -r1.13
*** pathScript.sml	1 Aug 2003 07:46:16 -0000	1.12
--- pathScript.sml	30 Sep 2003 03:13:17 -0000	1.13
***************
*** 7,10 ****
--- 7,12 ----
  val _ = new_theory "path";
  
+ val _ = augment_srw_ss [simpLib.rewrites [LET_THM]]
+ 
  val path_TY_DEF = new_type_definition (
    "path",
***************
*** 660,664 ****
    (drop (SUC n) p = drop n (tail p))
  `;
! val _ = BasicProvers.export_rewrites ["drop_def"]
  
  
--- 662,669 ----
    (drop (SUC n) p = drop n (tail p))
  `;
! val numeral_drop = save_thm(
!   "numeral_drop",
!   CONV_RULE numLib.SUC_TO_NUMERAL_DEFN_CONV (CONJUNCT2 drop_def));
! val _ = BasicProvers.export_rewrites ["drop_def", "numeral_drop"]
  
  
***************
*** 1293,1296 ****
--- 1298,1309 ----
    ``!R. SN R = !p. okpath R p ==> finite p``,
    PROVE_TAC [finite_paths_SN, SN_finite_paths]);
+ 
+ val LET_PATH = store_thm(
+   "LET_PATH",
+   ``(LET f (stopped_at x) = LET (\v. f (stopped_at v)) x) /\
+     (LET f (pcons x r p) =
+        LET (\v1. LET (\v2. LET (\v3. f (pcons v1 v2 v3)) p) r) x)``,
+   REWRITE_TAC [LET_THM] THEN BETA_TAC THEN REWRITE_TAC []);
+ val _ = export_rewrites ["LET_PATH"]
  
  val _ = export_theory();

Update of /cvsroot/hol/hol98/src/pair/src
In directory sc8-pr-cvs1:/tmp/cvs-serv15073/src/pair/src

Modified Files:
	pairScript.sml 
Log Message:
A new approach to handling LETs for the stateful rewriter.  Introduces an 
incompatibility in that bool_ss no longer rewrites LET f x to f x (std_ss
still does though).  The new strategy is: 

   Don't put LET_THM into any of the simpsets, but rather
   put in specialised versions of this that allow "values" to be
   substituted into the body.  Thus ``let v = e1 in e2`` will only reduce
   to  e2[e1/v] when e1 has been reduced to a proper value.  Better,
   allow partial substitution to happen when e1 has become partially
   value-like.  For example, if we get to

      let v = SUC e in v + v

   and e isn't necessarily evaluated, we can still move this to

      let v = e in SUC v + SUC v

   The rewrite for this is  |- LET f (SUC e) = LET (\v. f (SUC v)) e
   Comparable rewrites for constructors of any type are easy to state
   and prove.  Arguably, these theorems should be generated when new
   types are defined, and stored in the TypeBase.  Because I know Konrad
   will be (is already?) messing with the TypeBase to support ML lifting,
   I haven't done this for Hol_datatype (it's not quite so easy to see
   how to capture the notion of "record value").

   I have written the appropriate theorems for the obivous built-in
   types.  This strategy gives the simplifier a notion of "value" that
   is different from "can't reduce any more by the given rewrites"
   (which is what CBV_CONV uses).  The problem with CBV_CONV, or a
   congruence rule that always performs the reduction from LET f e to 
   f e is that you can get big explosions in term size, which is 
   particularly bad if you are doing symbolic evaluation.

Have fixed problems arising in probability (which was using its own 
version of std_ss, and those places where srw_ss() is being used.  The
examples/lambda directory uses SRW_TAC pretty extensively, so there are
fixes required there.  The easiest way is to just put LET_THM back into
the stateful simpset and to forget about it.  The general problem with
the stateful system as it stands is that it is very easy to put things
into it, but impossible to pull them out.  Isabelle has some way of 
doing this that might be worth looking into.



Index: pairScript.sml
===================================================================
RCS file: /cvsroot/hol/hol98/src/pair/src/pairScript.sml,v
retrieving revision 1.38
retrieving revision 1.39
diff -b -C2 -d -r1.38 -r1.39
*** pairScript.sml	31 Jul 2003 21:17:48 -0000	1.38
--- pairScript.sml	30 Sep 2003 03:13:17 -0000	1.39
***************
*** 402,405 ****
--- 402,414 ----
    THEN REWRITE_TAC[]);
  
+ (* ----------------------------------------------------------------------
+     LET_PAIR
+    ---------------------------------------------------------------------- *)
+ 
+ val LET_PAIR = store_thm(
+   "LET_PAIR",
+   ``LET f (x,y) = LET (\v1. LET (\v2. f(v1,v2)) y) x``,
+   REWRITE_TAC [LET_THM] THEN BETA_TAC THEN REWRITE_TAC []);
+ 
  
  (*---------------------------------------------------------------------------
***************
*** 698,702 ****
           "UNCURRY_CURRY_THM", "CURRY_ONE_ONE_THM", "UNCURRY_ONE_ONE_THM",
           "UNCURRY", "CURRY_DEF", "PAIR_MAP_THM", "FST_PAIR_MAP",
!          "SND_PAIR_MAP"]
  
  val _ = export_theory();
--- 707,711 ----
           "UNCURRY_CURRY_THM", "CURRY_ONE_ONE_THM", "UNCURRY_ONE_ONE_THM",
           "UNCURRY", "CURRY_DEF", "PAIR_MAP_THM", "FST_PAIR_MAP",
!          "SND_PAIR_MAP", "LET_PAIR"]
  
  val _ = export_theory();

Update of /cvsroot/hol/hol98/src/option
In directory sc8-pr-cvs1:/tmp/cvs-serv15073/src/option

Modified Files:
	optionScript.sml 
Log Message:
A new approach to handling LETs for the stateful rewriter.  Introduces an 
incompatibility in that bool_ss no longer rewrites LET f x to f x (std_ss
still does though).  The new strategy is: 

   Don't put LET_THM into any of the simpsets, but rather
   put in specialised versions of this that allow "values" to be
   substituted into the body.  Thus ``let v = e1 in e2`` will only reduce
   to  e2[e1/v] when e1 has been reduced to a proper value.  Better,
   allow partial substitution to happen when e1 has become partially
   value-like.  For example, if we get to

      let v = SUC e in v + v

   and e isn't necessarily evaluated, we can still move this to

      let v = e in SUC v + SUC v

   The rewrite for this is  |- LET f (SUC e) = LET (\v. f (SUC v)) e
   Comparable rewrites for constructors of any type are easy to state
   and prove.  Arguably, these theorems should be generated when new
   types are defined, and stored in the TypeBase.  Because I know Konrad
   will be (is already?) messing with the TypeBase to support ML lifting,
   I haven't done this for Hol_datatype (it's not quite so easy to see
   how to capture the notion of "record value").

   I have written the appropriate theorems for the obivous built-in
   types.  This strategy gives the simplifier a notion of "value" that
   is different from "can't reduce any more by the given rewrites"
   (which is what CBV_CONV uses).  The problem with CBV_CONV, or a
   congruence rule that always performs the reduction from LET f e to 
   f e is that you can get big explosions in term size, which is 
   particularly bad if you are doing symbolic evaluation.

Have fixed problems arising in probability (which was using its own 
version of std_ss, and those places where srw_ss() is being used.  The
examples/lambda directory uses SRW_TAC pretty extensively, so there are
fixes required there.  The easiest way is to just put LET_THM back into
the stateful simpset and to forget about it.  The general problem with
the stateful system as it stands is that it is very easy to put things
into it, but impossible to pull them out.  Isabelle has some way of 
doing this that might be worth looking into.



Index: optionScript.sml
===================================================================
RCS file: /cvsroot/hol/hol98/src/option/optionScript.sml,v
retrieving revision 1.21
retrieving revision 1.22
diff -b -C2 -d -r1.21 -r1.22
*** optionScript.sml	31 Jul 2003 21:17:48 -0000	1.21
--- optionScript.sml	30 Sep 2003 03:13:17 -0000	1.22
***************
*** 14,18 ****
  
  open HolKernel Parse boolLib;
- infix THEN THENL THENC ORELSE ORELSEC THEN_TCL ORELSE_TCL ## |->;
  
  (*---------------------------------------------------------------------------
--- 14,17 ----
***************
*** 288,291 ****
--- 287,297 ----
        Prim_rec.case_cong_thm option_nchotomy option_case_def);
  
+ val OPTION_LET = store_thm(
+   "OPTION_LET",
+   ``(LET f NONE = f NONE) /\
+     (LET f (SOME x) = LET (\v. f (SOME v)) x)``,
+   ASM_REWRITE_TAC [LET_THM] THEN BETA_TAC THEN REWRITE_TAC []);
+ 
+ 
  val _ = adjoin_to_theory
  {sig_ps = SOME (fn ppstrm =>
***************
*** 332,336 ****
             "IS_SOME_DEF", "IS_NONE_EQ_NONE", "NOT_IS_SOME_EQ_NONE",
             "option_case_ID", "option_case_SOME_ID", "option_case_def",
!            "OPTION_MAP_DEF", "OPTION_JOIN_DEF", "SOME_11", "NOT_SOME_NONE"]
  
  val _ = export_theory();
--- 338,343 ----
             "IS_SOME_DEF", "IS_NONE_EQ_NONE", "NOT_IS_SOME_EQ_NONE",
             "option_case_ID", "option_case_SOME_ID", "option_case_def",
!            "OPTION_MAP_DEF", "OPTION_JOIN_DEF", "SOME_11", "NOT_SOME_NONE",
!            "OPTION_LET"]
  
  val _ = export_theory();

Update of /cvsroot/hol/hol98/src/num/arith/src
In directory sc8-pr-cvs1:/tmp/cvs-serv15073/src/num/arith/src

Modified Files:
	numSimps.sml 
Log Message:
A new approach to handling LETs for the stateful rewriter.  Introduces an 
incompatibility in that bool_ss no longer rewrites LET f x to f x (std_ss
still does though).  The new strategy is: 

   Don't put LET_THM into any of the simpsets, but rather
   put in specialised versions of this that allow "values" to be
   substituted into the body.  Thus ``let v = e1 in e2`` will only reduce
   to  e2[e1/v] when e1 has been reduced to a proper value.  Better,
   allow partial substitution to happen when e1 has become partially
   value-like.  For example, if we get to

      let v = SUC e in v + v

   and e isn't necessarily evaluated, we can still move this to

      let v = e in SUC v + SUC v

   The rewrite for this is  |- LET f (SUC e) = LET (\v. f (SUC v)) e
   Comparable rewrites for constructors of any type are easy to state
   and prove.  Arguably, these theorems should be generated when new
   types are defined, and stored in the TypeBase.  Because I know Konrad
   will be (is already?) messing with the TypeBase to support ML lifting,
   I haven't done this for Hol_datatype (it's not quite so easy to see
   how to capture the notion of "record value").

   I have written the appropriate theorems for the obivous built-in
   types.  This strategy gives the simplifier a notion of "value" that
   is different from "can't reduce any more by the given rewrites"
   (which is what CBV_CONV uses).  The problem with CBV_CONV, or a
   congruence rule that always performs the reduction from LET f e to 
   f e is that you can get big explosions in term size, which is 
   particularly bad if you are doing symbolic evaluation.

Have fixed problems arising in probability (which was using its own 
version of std_ss, and those places where srw_ss() is being used.  The
examples/lambda directory uses SRW_TAC pretty extensively, so there are
fixes required there.  The easiest way is to just put LET_THM back into
the stateful simpset and to forget about it.  The general problem with
the stateful system as it stands is that it is very easy to put things
into it, but impossible to pull them out.  Isabelle has some way of 
doing this that might be worth looking into.



Index: numSimps.sml
===================================================================
RCS file: /cvsroot/hol/hol98/src/num/arith/src/numSimps.sml,v
retrieving revision 1.14
retrieving revision 1.15
diff -b -C2 -d -r1.14 -r1.15
*** numSimps.sml	23 Jul 2003 00:15:34 -0000	1.14
--- numSimps.sml	30 Sep 2003 03:13:16 -0000	1.15
***************
*** 328,332 ****
  
     (* mods and divs *)
!    X_MOD_Y_EQ_X, DIVMOD_ID, DIV_1, MOD_1, LESS_MOD, ZERO_MOD, MOD_MOD
     ]
  end;
--- 328,335 ----
  
     (* mods and divs *)
!    X_MOD_Y_EQ_X, DIVMOD_ID, DIV_1, MOD_1, LESS_MOD, ZERO_MOD, MOD_MOD,
! 
!    (* evaluation with lets *)
!    LET_NUM
     ]
  end;

Update of /cvsroot/hol/hol98/src/simp/src
In directory sc8-pr-cvs1:/tmp/cvs-serv15073/src/simp/src

Modified Files:
	boolSimps.sml 
Log Message:
A new approach to handling LETs for the stateful rewriter.  Introduces an 
incompatibility in that bool_ss no longer rewrites LET f x to f x (std_ss
still does though).  The new strategy is: 

   Don't put LET_THM into any of the simpsets, but rather
   put in specialised versions of this that allow "values" to be
   substituted into the body.  Thus ``let v = e1 in e2`` will only reduce
   to  e2[e1/v] when e1 has been reduced to a proper value.  Better,
   allow partial substitution to happen when e1 has become partially
   value-like.  For example, if we get to

      let v = SUC e in v + v

   and e isn't necessarily evaluated, we can still move this to

      let v = e in SUC v + SUC v

   The rewrite for this is  |- LET f (SUC e) = LET (\v. f (SUC v)) e
   Comparable rewrites for constructors of any type are easy to state
   and prove.  Arguably, these theorems should be generated when new
   types are defined, and stored in the TypeBase.  Because I know Konrad
   will be (is already?) messing with the TypeBase to support ML lifting,
   I haven't done this for Hol_datatype (it's not quite so easy to see
   how to capture the notion of "record value").

   I have written the appropriate theorems for the obivous built-in
   types.  This strategy gives the simplifier a notion of "value" that
   is different from "can't reduce any more by the given rewrites"
   (which is what CBV_CONV uses).  The problem with CBV_CONV, or a
   congruence rule that always performs the reduction from LET f e to 
   f e is that you can get big explosions in term size, which is 
   particularly bad if you are doing symbolic evaluation.

Have fixed problems arising in probability (which was using its own 
version of std_ss, and those places where srw_ss() is being used.  The
examples/lambda directory uses SRW_TAC pretty extensively, so there are
fixes required there.  The easiest way is to just put LET_THM back into
the stateful simpset and to forget about it.  The general problem with
the stateful system as it stands is that it is very easy to put things
into it, but impossible to pull them out.  Isabelle has some way of 
doing this that might be worth looking into.



Index: boolSimps.sml
===================================================================
RCS file: /cvsroot/hol/hol98/src/simp/src/boolSimps.sml,v
retrieving revision 1.23
retrieving revision 1.24
diff -b -C2 -d -r1.23 -r1.24
*** boolSimps.sml	9 Jul 2003 04:54:47 -0000	1.23
--- boolSimps.sml	30 Sep 2003 03:13:17 -0000	1.24
***************
*** 134,137 ****
--- 134,138 ----
     ---------------------------------------------------------------------- *)
  
+ (*
   val let_cong = prove(
     ``(v:'a = v') ==> (LET (f:'a -> 'b) v = LET f (I v'))``,
***************
*** 139,147 ****
  val let_I_thm = prove(
    ``LET (f : 'a -> 'b) (I x) = f x``,
!   REWRITE_TAC [combinTheory.I_THM, LET_THM]);
  
! val LET_ss = simpLib.SIMPSET {ac = [], congs = [let_cong],
!                               convs = [], filter = NONE, dprocs = [],
!                               rewrs = [let_I_thm]}
  
  (* ----------------------------------------------------------------------
--- 140,154 ----
  val let_I_thm = prove(
    ``LET (f : 'a -> 'b) (I x) = f x``,
!   REWRITE_TAC [combinTheory.I_THM, LET_THM]);*)
  
! val LET_ss = let
!   val sLET = INST_TYPE[Type.alpha |-> bool] (SPEC_ALL LET_THM)
!   val x = mk_var("x",bool)
!   val T_value = INST [x|->boolSyntax.T] sLET
!   val F_value = INST [x|->boolSyntax.F] sLET
! in
!   simpLib.SIMPSET {ac = [], congs = [], convs = [], filter = NONE,
!                    dprocs = [], rewrs = [T_value, F_value]}
! end
  
  (* ----------------------------------------------------------------------

Update of /cvsroot/hol/hol98/src/sum
In directory sc8-pr-cvs1:/tmp/cvs-serv15073/src/sum

Modified Files:
	sumScript.sml 
Log Message:
A new approach to handling LETs for the stateful rewriter.  Introduces an 
incompatibility in that bool_ss no longer rewrites LET f x to f x (std_ss
still does though).  The new strategy is: 

   Don't put LET_THM into any of the simpsets, but rather
   put in specialised versions of this that allow "values" to be
   substituted into the body.  Thus ``let v = e1 in e2`` will only reduce
   to  e2[e1/v] when e1 has been reduced to a proper value.  Better,
   allow partial substitution to happen when e1 has become partially
   value-like.  For example, if we get to

      let v = SUC e in v + v

   and e isn't necessarily evaluated, we can still move this to

      let v = e in SUC v + SUC v

   The rewrite for this is  |- LET f (SUC e) = LET (\v. f (SUC v)) e
   Comparable rewrites for constructors of any type are easy to state
   and prove.  Arguably, these theorems should be generated when new
   types are defined, and stored in the TypeBase.  Because I know Konrad
   will be (is already?) messing with the TypeBase to support ML lifting,
   I haven't done this for Hol_datatype (it's not quite so easy to see
   how to capture the notion of "record value").

   I have written the appropriate theorems for the obivous built-in
   types.  This strategy gives the simplifier a notion of "value" that
   is different from "can't reduce any more by the given rewrites"
   (which is what CBV_CONV uses).  The problem with CBV_CONV, or a
   congruence rule that always performs the reduction from LET f e to 
   f e is that you can get big explosions in term size, which is 
   particularly bad if you are doing symbolic evaluation.

Have fixed problems arising in probability (which was using its own 
version of std_ss, and those places where srw_ss() is being used.  The
examples/lambda directory uses SRW_TAC pretty extensively, so there are
fixes required there.  The easiest way is to just put LET_THM back into
the stateful simpset and to forget about it.  The general problem with
the stateful system as it stands is that it is very easy to put things
into it, but impossible to pull them out.  Isabelle has some way of 
doing this that might be worth looking into.



Index: sumScript.sml
===================================================================
RCS file: /cvsroot/hol/hol98/src/sum/sumScript.sml,v
retrieving revision 1.21
retrieving revision 1.22
diff -b -C2 -d -r1.21 -r1.22
*** sumScript.sml	4 Aug 2003 19:38:46 -0000	1.21
--- sumScript.sml	30 Sep 2003 03:13:17 -0000	1.22
***************
*** 34,40 ****
  
  open HolKernel Parse boolLib;
- infix THEN THENL ORELSEC THENC |->;
- 
- type thm = Thm.thm;
  
  val _ = new_theory "sum";
--- 34,37 ----
***************
*** 360,363 ****
--- 357,366 ----
                               Prim_rec.case_cong_thm sum_CASES sum_case_def);
  
+ val LET_SUM = store_thm(
+   "LET_SUM",
+   ``(LET f (INL a) = LET (\v. f (INL v)) a) /\
+     (LET f (INR b) = LET (\u. f (INR u)) b)``,
+   REWRITE_TAC [LET_THM] THEN BETA_TAC THEN REWRITE_TAC []);
+ 
  val _ = adjoin_to_theory
  {sig_ps = NONE,
***************
*** 388,392 ****
  val _ = BasicProvers.export_rewrites ["ISL", "ISR", "OUTL", "OUTR",
                                        "sum_distinct", "INR_INL_11",
!                                       "sum_case_def", "INL", "INR"]
  
  
--- 391,395 ----
  val _ = BasicProvers.export_rewrites ["ISL", "ISR", "OUTL", "OUTR",
                                        "sum_distinct", "INR_INL_11",
!                                       "sum_case_def", "INL", "INR", "LET_SUM"]

Update of /cvsroot/hol/hol98/src/num/theories
In directory sc8-pr-cvs1:/tmp/cvs-serv15073/src/num/theories

Modified Files:
	arithmeticScript.sml 
Log Message:
A new approach to handling LETs for the stateful rewriter.  Introduces an 
incompatibility in that bool_ss no longer rewrites LET f x to f x (std_ss
still does though).  The new strategy is: 

   Don't put LET_THM into any of the simpsets, but rather
   put in specialised versions of this that allow "values" to be
   substituted into the body.  Thus ``let v = e1 in e2`` will only reduce
   to  e2[e1/v] when e1 has been reduced to a proper value.  Better,
   allow partial substitution to happen when e1 has become partially
   value-like.  For example, if we get to

      let v = SUC e in v + v

   and e isn't necessarily evaluated, we can still move this to

      let v = e in SUC v + SUC v

   The rewrite for this is  |- LET f (SUC e) = LET (\v. f (SUC v)) e
   Comparable rewrites for constructors of any type are easy to state
   and prove.  Arguably, these theorems should be generated when new
   types are defined, and stored in the TypeBase.  Because I know Konrad
   will be (is already?) messing with the TypeBase to support ML lifting,
   I haven't done this for Hol_datatype (it's not quite so easy to see
   how to capture the notion of "record value").

   I have written the appropriate theorems for the obivous built-in
   types.  This strategy gives the simplifier a notion of "value" that
   is different from "can't reduce any more by the given rewrites"
   (which is what CBV_CONV uses).  The problem with CBV_CONV, or a
   congruence rule that always performs the reduction from LET f e to 
   f e is that you can get big explosions in term size, which is 
   particularly bad if you are doing symbolic evaluation.

Have fixed problems arising in probability (which was using its own 
version of std_ss, and those places where srw_ss() is being used.  The
examples/lambda directory uses SRW_TAC pretty extensively, so there are
fixes required there.  The easiest way is to just put LET_THM back into
the stateful simpset and to forget about it.  The general problem with
the stateful system as it stands is that it is very easy to put things
into it, but impossible to pull them out.  Isabelle has some way of 
doing this that might be worth looking into.



Index: arithmeticScript.sml
===================================================================
RCS file: /cvsroot/hol/hol98/src/num/theories/arithmeticScript.sml,v
retrieving revision 1.37
retrieving revision 1.38
diff -b -C2 -d -r1.37 -r1.38
*** arithmeticScript.sml	31 Jul 2003 21:17:48 -0000	1.37
--- arithmeticScript.sml	30 Sep 2003 03:13:17 -0000	1.38
***************
*** 3027,3030 ****
--- 3027,3037 ----
     ``!p. (?n. p n) ==> (p ($LEAST p) /\ !n. n < $LEAST p ==> ~p n)``,
     REWRITE_TAC [LEAST_EXISTS]);
+ 
+ val LET_NUM = store_thm(
+   "LET_NUM",
+   ``(LET f 0 = f 0) /\
+     (LET f (SUC x) = LET (\v. f (SUC v)) x) /\
+     (LET f (NUMERAL v) = f (NUMERAL v))``,
+   REWRITE_TAC [LET_THM] THEN BETA_TAC THEN REWRITE_TAC []);
  
  val _ = adjoin_to_theory

Update of /cvsroot/hol/hol98/src/llist
In directory sc8-pr-cvs1:/tmp/cvs-serv15073/src/llist

Modified Files:
	llistScript.sml 
Log Message:
A new approach to handling LETs for the stateful rewriter.  Introduces an 
incompatibility in that bool_ss no longer rewrites LET f x to f x (std_ss
still does though).  The new strategy is: 

   Don't put LET_THM into any of the simpsets, but rather
   put in specialised versions of this that allow "values" to be
   substituted into the body.  Thus ``let v = e1 in e2`` will only reduce
   to  e2[e1/v] when e1 has been reduced to a proper value.  Better,
   allow partial substitution to happen when e1 has become partially
   value-like.  For example, if we get to

      let v = SUC e in v + v

   and e isn't necessarily evaluated, we can still move this to

      let v = e in SUC v + SUC v

   The rewrite for this is  |- LET f (SUC e) = LET (\v. f (SUC v)) e
   Comparable rewrites for constructors of any type are easy to state
   and prove.  Arguably, these theorems should be generated when new
   types are defined, and stored in the TypeBase.  Because I know Konrad
   will be (is already?) messing with the TypeBase to support ML lifting,
   I haven't done this for Hol_datatype (it's not quite so easy to see
   how to capture the notion of "record value").

   I have written the appropriate theorems for the obivous built-in
   types.  This strategy gives the simplifier a notion of "value" that
   is different from "can't reduce any more by the given rewrites"
   (which is what CBV_CONV uses).  The problem with CBV_CONV, or a
   congruence rule that always performs the reduction from LET f e to 
   f e is that you can get big explosions in term size, which is 
   particularly bad if you are doing symbolic evaluation.

Have fixed problems arising in probability (which was using its own 
version of std_ss, and those places where srw_ss() is being used.  The
examples/lambda directory uses SRW_TAC pretty extensively, so there are
fixes required there.  The easiest way is to just put LET_THM back into
the stateful simpset and to forget about it.  The general problem with
the stateful system as it stands is that it is very easy to put things
into it, but impossible to pull them out.  Isabelle has some way of 
doing this that might be worth looking into.



Index: llistScript.sml
===================================================================
RCS file: /cvsroot/hol/hol98/src/llist/llistScript.sml,v
retrieving revision 1.19
retrieving revision 1.20
diff -b -C2 -d -r1.19 -r1.20
*** llistScript.sml	1 Aug 2003 07:46:16 -0000	1.19
--- llistScript.sml	30 Sep 2003 03:13:16 -0000	1.20
***************
*** 22,26 ****
  val hol_ss = bool_ss ++ optionSimps.OPTION_ss ++ listSimps.LIST_ss ++
                          numSimps.ARITH_ss ++ numSimps.REDUCE_ss ++
!                         pairSimps.PAIR_ss ++ rewrites [UNCURRY_THM] ++
                          combinSimps.COMBIN_ss
  
--- 22,26 ----
  val hol_ss = bool_ss ++ optionSimps.OPTION_ss ++ listSimps.LIST_ss ++
                          numSimps.ARITH_ss ++ numSimps.REDUCE_ss ++
!                         pairSimps.PAIR_ss ++ rewrites [UNCURRY_THM, LET_THM] ++
                          combinSimps.COMBIN_ss
  
***************
*** 1587,1592 ****
    ]);
  
  val _ = BasicProvers.export_rewrites
!           ["LCONS_NOT_NIL", "LCONS_11", "LMAP", "LAPPEND", "LFILTER_THM"]
  
  
--- 1587,1599 ----
    ]);
  
+ val LET_LLIST = store_thm(
+   "LET_LLIST",
+   ``(LET f LNIL = f LNIL) /\
+     (LET f (LCONS h t) = LET (\v1. LET (\v2. f (LCONS v1 v2)) t) h)``,
+   REWRITE_TAC [LET_THM] THEN BETA_TAC THEN REWRITE_TAC []);
+ 
  val _ = BasicProvers.export_rewrites
!           ["LCONS_NOT_NIL", "LCONS_11", "LMAP", "LAPPEND", "LFILTER_THM",
!            "LET_LLIST"]

Update of /cvsroot/hol/hol98/src/list/src
In directory sc8-pr-cvs1:/tmp/cvs-serv15073/src/list/src

Modified Files:
	listScript.sml 
Log Message:
A new approach to handling LETs for the stateful rewriter.  Introduces an 
incompatibility in that bool_ss no longer rewrites LET f x to f x (std_ss
still does though).  The new strategy is: 

   Don't put LET_THM into any of the simpsets, but rather
   put in specialised versions of this that allow "values" to be
   substituted into the body.  Thus ``let v = e1 in e2`` will only reduce
   to  e2[e1/v] when e1 has been reduced to a proper value.  Better,
   allow partial substitution to happen when e1 has become partially
   value-like.  For example, if we get to

      let v = SUC e in v + v

   and e isn't necessarily evaluated, we can still move this to

      let v = e in SUC v + SUC v

   The rewrite for this is  |- LET f (SUC e) = LET (\v. f (SUC v)) e
   Comparable rewrites for constructors of any type are easy to state
   and prove.  Arguably, these theorems should be generated when new
   types are defined, and stored in the TypeBase.  Because I know Konrad
   will be (is already?) messing with the TypeBase to support ML lifting,
   I haven't done this for Hol_datatype (it's not quite so easy to see
   how to capture the notion of "record value").

   I have written the appropriate theorems for the obivous built-in
   types.  This strategy gives the simplifier a notion of "value" that
   is different from "can't reduce any more by the given rewrites"
   (which is what CBV_CONV uses).  The problem with CBV_CONV, or a
   congruence rule that always performs the reduction from LET f e to 
   f e is that you can get big explosions in term size, which is 
   particularly bad if you are doing symbolic evaluation.

Have fixed problems arising in probability (which was using its own 
version of std_ss, and those places where srw_ss() is being used.  The
examples/lambda directory uses SRW_TAC pretty extensively, so there are
fixes required there.  The easiest way is to just put LET_THM back into
the stateful simpset and to forget about it.  The general problem with
the stateful system as it stands is that it is very easy to put things
into it, but impossible to pull them out.  Isabelle has some way of 
doing this that might be worth looking into.



Index: listScript.sml
===================================================================
RCS file: /cvsroot/hol/hol98/src/list/src/listScript.sml,v
retrieving revision 1.41
retrieving revision 1.42
diff -b -C2 -d -r1.41 -r1.42
*** listScript.sml	3 Sep 2003 13:46:01 -0000	1.41
--- listScript.sml	30 Sep 2003 03:13:16 -0000	1.42
***************
*** 925,928 ****
--- 925,939 ----
    metisLib.METIS_TAC []);
  
+ (* ----------------------------------------------------------------------
+     LET_LIST
+    ---------------------------------------------------------------------- *)
+ 
+ val LET_LIST = store_thm(
+   "LET_LIST",
+   ``(LET f [] = f []) /\
+     (LET f (h::t) = LET (\v1. LET (\v2. f (v1 :: v2)) t) h)``,
+   REWRITE_TAC [LET_THM] THEN BETA_TAC THEN REWRITE_TAC []);
+ 
+ 
  (* --------------------------------------------------------------------- *)
  
***************
*** 967,971 ****
             "EXISTS_SIMP", "NOT_EVERY", "NOT_EXISTS", "MEM_APPEND",
             "LAST_CONS", "FRONT_CONS", "FOLDL", "FOLDR", "FILTER",
!            "ALL_DISTINCT"];
  
  val _ = export_theory();
--- 978,982 ----
             "EXISTS_SIMP", "NOT_EVERY", "NOT_EXISTS", "MEM_APPEND",
             "LAST_CONS", "FRONT_CONS", "FOLDL", "FOLDR", "FILTER",
!            "ALL_DISTINCT", "LET_LIST"];
  
  val _ = export_theory();

Update of /cvsroot/hol/hol98/examples/lambda
In directory sc8-pr-cvs1:/tmp/cvs-serv6362

Added Files:
	ncLib.sig 
Log Message:
This directory wouldn't build without this sig file also available.


--- NEW FILE: ncLib.sig ---
signature ncLib =
sig

  include Abbrev
  val NEW_TAC : string -> term -> tactic
  val NEW_ELIM_TAC : tactic

  val recursive_term_function_existence : term -> thm
  val prove_recursive_term_function_exists : term -> thm
  val define_recursive_term_function :
      term quotation -> thm * (thm * thm) option

end;

Update of /cvsroot/hol/hol98/examples/pgcl/src
In directory sc8-pr-cvs1:/tmp/cvs-serv3458/src

Modified Files:
	expectationScript.sml posrealScript.sml wpScript.sml 
	wpTools.sml 
Log Message:
Some reorganization and name changes while I'm correcting my pGCL paper.


Index: expectationScript.sml
===================================================================
RCS file: /cvsroot/hol/hol98/examples/pgcl/src/expectationScript.sml,v
retrieving revision 1.2
retrieving revision 1.3
diff -b -C2 -d -r1.2 -r1.3
*** expectationScript.sml	25 Sep 2003 09:59:20 -0000	1.2
--- expectationScript.sml	30 Sep 2003 01:44:56 -0000	1.3
***************
*** 228,231 ****
--- 228,242 ----
  
  (* ------------------------------------------------------------------------- *)
+ (* More complicated operations on expectations                               *)
+ (* ------------------------------------------------------------------------- *)
+ 
+ val prob_def = Define
+   `prob p (a : 'a expect) b s =
+    let x = bound1 (p s) in x * a s + (1 - x) * b s`;
+ 
+ val cond_def = Define
+   `cond c (a : 'a expect) b s = if c s then a s else b s`;
+ 
+ (* ------------------------------------------------------------------------- *)
  (* Fundamental properties of expectation transformers                        *)
  (* ------------------------------------------------------------------------- *)

Index: posrealScript.sml
===================================================================
RCS file: /cvsroot/hol/hol98/examples/pgcl/src/posrealScript.sml,v
retrieving revision 1.2
retrieving revision 1.3
diff -b -C2 -d -r1.2 -r1.3
*** posrealScript.sml	25 Sep 2003 09:59:20 -0000	1.2
--- posrealScript.sml	30 Sep 2003 01:44:56 -0000	1.3
***************
*** 1360,1363 ****
--- 1360,1398 ----
  
  (* ------------------------------------------------------------------------- *)
+ (* 1-boundedness                                                             *)
+ (* ------------------------------------------------------------------------- *)
+ 
+ val bound1_def = Define `bound1 (x:posreal) = if x <= 1 then x else 1`;
+ 
+ val bound1 = store_thm
+   ("bound1",
+    ``!x. bound1 x <= 1``,
+    RW_TAC std_ss [bound1_def, le_refl]);
+ 
+ val bound1_basic = store_thm
+   ("bound1_basic",
+    ``(bound1 0 = 0) /\ (bound1 1 = 1) /\ (bound1 (1 / 2) = 1 / 2) /\
+      (bound1 (1 / 3) = 1 / 3) /\ (bound1 (2 / 3) = 2 / 3)``,
+    RW_TAC std_ss [bound1_def, zero_le, half_between, thirds_between]);
+ 
+ val bound1_cancel = store_thm
+   ("bound1_cancel",
+    ``!x. bound1 x + (1 - bound1 x) = 1``,
+    GEN_TAC
+    ++ MATCH_MP_TAC sub_add2
+    ++ RW_TAC std_ss [bound1]
+    ++ METIS_TAC [posreal_of_num_not_infty, infty_le, le_trans, bound1]);
+ 
+ val bound1_cancel2 = store_thm
+   ("bound1_cancel2",
+    ``!x. (1 - bound1 x) + bound1 x = 1``,
+    METIS_TAC [bound1_cancel, add_comm]);
+ 
+ val bound1_min = store_thm
+   ("bound1_min",
+    ``!x. bound1 x = min x 1``,
+    RW_TAC std_ss [bound1_def, preal_min_def]);
+ 
+ (* ------------------------------------------------------------------------- *)
  (* Supremums and infimums (these are always defined on posreals)             *)
  (* ------------------------------------------------------------------------- *)

Index: wpScript.sml
===================================================================
RCS file: /cvsroot/hol/hol98/examples/pgcl/src/wpScript.sml,v
retrieving revision 1.3
retrieving revision 1.4
diff -b -C2 -d -r1.3 -r1.4
*** wpScript.sml	26 Sep 2003 23:04:10 -0000	1.3
--- wpScript.sml	30 Sep 2003 01:44:56 -0000	1.4
***************
*** 51,84 ****
  
  (* ------------------------------------------------------------------------- *)
- (* The probify constant makes sure probabilities lie between 0 and 1         *)
- (* ------------------------------------------------------------------------- *)
- 
- val probify_def = Define `probify (x:posreal) = if x <= 1 then x else 1`;
- 
- val probify = store_thm
-   ("probify",
-    ``!x. probify x <= 1``,
-    RW_TAC posreal_ss [probify_def]);
- 
- val probify_basic = store_thm
-   ("probify_basic",
-    ``(probify 0 = 0) /\ (probify 1 = 1) /\ (probify (1 / 2) = 1 / 2) /\
-      (probify (1 / 3) = 1 / 3) /\ (probify (2 / 3) = 2 / 3)``,
-    RW_TAC posreal_ss [probify_def]);
- 
- val probify_cancel = store_thm
-   ("probify_cancel",
-    ``!x. probify x + (1 - probify x) = 1``,
-    GEN_TAC
-    ++ MATCH_MP_TAC sub_add2
-    ++ RW_TAC posreal_ss [probify]
-    ++ METIS_TAC [posreal_of_num_not_infty, infty_le, le_trans, probify]);
- 
- val probify_cancel2 = store_thm
-   ("probify_cancel2",
-    ``!x. (1 - probify x) + probify x = 1``,
-    METIS_TAC [probify_cancel, add_comm]);
- 
- (* ------------------------------------------------------------------------- *)
  (* The HOL type we use to model states                                       *)
  (* ------------------------------------------------------------------------- *)
--- 51,54 ----
***************
*** 86,89 ****
--- 56,68 ----
  val () = type_abbrev ("state", Type `:string -> int`);
  
+ val assign_def = Define
+   `assign v (e : state -> int) s w = if v = w then e s else s w`;
+ 
+ val assign_eta = store_thm
+   ("assign_eta",
+    ``!v e s. assign v e s = \w. if w = v then e s else s w``,
+    CONV_TAC (DEPTH_CONV FUN_EQ_CONV)
+    ++ RW_TAC std_ss [assign_def]);
+ 
  (* ------------------------------------------------------------------------- *)
  (* Probabilisitic programs: syntax                                           *)
***************
*** 151,155 ****
     (wp (Demon a b) = \r. Min (wp a r) (wp b r)) /\
     (wp (Prob p a b) =
!     \r s. let x = probify (p s) in x * wp a r s + (1 - x) * wp b r s) /\
     (wp (While c b) = \r. expect_lfp (\e s. if c s then wp b e s else r s))`;
  
--- 130,134 ----
     (wp (Demon a b) = \r. Min (wp a r) (wp b r)) /\
     (wp (Prob p a b) =
!     \r s. let x = bound1 (p s) in x * wp a r s + (1 - x) * wp b r s) /\
     (wp (While c b) = \r. expect_lfp (\e s. if c s then wp b e s else r s))`;
  
***************
*** 421,427 ****
         ++ DISCH_THEN (fn th => ONCE_REWRITE_TAC [th])
         ++ Suff
!           `(probify (f s) * (c1 * x1) + probify (f s) * (c2 * x2)) +
!            ((1 - probify (f s)) * (c1 * x1') + (1 - probify (f s)) * (c2 * x2'))
!            - c <= probify (f s) * y + (1 - probify (f s)) * y'`
         >> (MATCH_MP_TAC (PROVE[]``(a : posreal = a') ==> (a <= b ==> a' <= b)``)
             ++ METIS_TAC [mul_comm, mul_assoc])
--- 400,406 ----
         ++ DISCH_THEN (fn th => ONCE_REWRITE_TAC [th])
         ++ Suff
!           `(bound1 (f s) * (c1 * x1) + bound1 (f s) * (c2 * x2)) +
!            ((1 - bound1 (f s)) * (c1 * x1') + (1 - bound1 (f s)) * (c2 * x2'))
!            - c <= bound1 (f s) * y + (1 - bound1 (f s)) * y'`
         >> (MATCH_MP_TAC (PROVE[]``(a : posreal = a') ==> (a <= b ==> a' <= b)``)
             ++ METIS_TAC [mul_comm, mul_assoc])
***************
*** 429,434 ****
         ++ MATCH_MP_TAC sub_le_imp
         ++ ASM_REWRITE_TAC []
!        ++ Know `c = probify (f s) * c + (1 - probify (f s)) * c`
!        >> RW_TAC posreal_ss [GSYM add_rdistrib, probify_cancel]
         ++ DISCH_THEN (fn th => ONCE_REWRITE_TAC [th])
         ++ Know `!a b c d : posreal. (a + b) + (c + d) = (a + c) + (b + d)`
--- 408,413 ----
         ++ MATCH_MP_TAC sub_le_imp
         ++ ASM_REWRITE_TAC []
!        ++ Know `c = bound1 (f s) * c + (1 - bound1 (f s)) * c`
!        >> RW_TAC posreal_ss [GSYM add_rdistrib, bound1_cancel]
         ++ DISCH_THEN (fn th => ONCE_REWRITE_TAC [th])
         ++ Know `!a b c d : posreal. (a + b) + (c + d) = (a + c) + (b + d)`
***************
*** 468,478 ****
                ?z.
                  c z /\
!                 (r = probify (f s) * wp prog z s +
!                      (1 - probify (f s)) * wp prog' z s))`
         ++ REVERSE CONJ_TAC
         >> (RW_TAC posreal_ss [sup_le]
             ++ Suff
!               `Leq (\s. probify (f s) * wp prog z' s +
!                     (1 - probify (f s)) * wp prog' z' s) z`
             >> RW_TAC posreal_ss [Leq_def]
             ++ FIRST_ASSUM MATCH_MP_TAC
--- 447,457 ----
                ?z.
                  c z /\
!                 (r = bound1 (f s) * wp prog z s +
!                      (1 - bound1 (f s)) * wp prog' z s))`
         ++ REVERSE CONJ_TAC
         >> (RW_TAC posreal_ss [sup_le]
             ++ Suff
!               `Leq (\s. bound1 (f s) * wp prog z' s +
!                     (1 - bound1 (f s)) * wp prog' z' s) z`
             >> RW_TAC posreal_ss [Leq_def]
             ++ FIRST_ASSUM MATCH_MP_TAC
***************
*** 484,489 ****
         ++ MATCH_MP_TAC le_trans
         ++ Q.EXISTS_TAC
!           `sup (\r. ?z. c z /\ (r = probify (f s) * wp prog z s)) +
!            sup (\r. ?z. c z /\ (r = (1 - probify (f s)) * wp prog' z s))`
         ++ REVERSE CONJ_TAC
         >> (RW_TAC posreal_ss [add_sup, sup_le]
--- 463,468 ----
         ++ MATCH_MP_TAC le_trans
         ++ Q.EXISTS_TAC
!           `sup (\r. ?z. c z /\ (r = bound1 (f s) * wp prog z s)) +
!            sup (\r. ?z. c z /\ (r = (1 - bound1 (f s)) * wp prog' z s))`
         ++ REVERSE CONJ_TAC
         >> (RW_TAC posreal_ss [add_sup, sup_le]
***************
*** 495,500 ****
                 ++ MATCH_MP_TAC le_trans
                 ++ Q.EXISTS_TAC
!                   `probify (f s) * wp prog w s +
!                    (1 - probify (f s)) * wp prog' w s`
                 ++ REVERSE CONJ_TAC >> METIS_TAC []
                 ++ MATCH_MP_TAC le_add2
--- 474,479 ----
                 ++ MATCH_MP_TAC le_trans
                 ++ Q.EXISTS_TAC
!                   `bound1 (f s) * wp prog w s +
!                    (1 - bound1 (f s)) * wp prog' w s`
                 ++ REVERSE CONJ_TAC >> METIS_TAC []
                 ++ MATCH_MP_TAC le_add2
***************
*** 509,514 ****
                 MATCH_MP_TAC le_trans
                 ++ Q.EXISTS_TAC
!                   `probify (f s) * wp prog z s +
!                    (1 - probify (f s)) * wp prog' z s`
                 ++ REVERSE CONJ_TAC >> METIS_TAC []
                 ++ MATCH_MP_TAC le_add2
--- 488,493 ----
                 MATCH_MP_TAC le_trans
                 ++ Q.EXISTS_TAC
!                   `bound1 (f s) * wp prog z s +
!                    (1 - bound1 (f s)) * wp prog' z s`
                 ++ REVERSE CONJ_TAC >> METIS_TAC []
                 ++ MATCH_MP_TAC le_add2
***************
*** 516,521 ****
                 MATCH_MP_TAC le_trans
                 ++ Q.EXISTS_TAC
!                   `probify (f s) * wp prog z s +
!                    (1 - probify (f s)) * wp prog' z s`
                 ++ REVERSE CONJ_TAC >> METIS_TAC []
                 ++ MATCH_MP_TAC le_add2
--- 495,500 ----
                 MATCH_MP_TAC le_trans
                 ++ Q.EXISTS_TAC
!                   `bound1 (f s) * wp prog z s +
!                    (1 - bound1 (f s)) * wp prog' z s`
                 ++ REVERSE CONJ_TAC >> METIS_TAC []
                 ++ MATCH_MP_TAC le_add2
***************
*** 550,556 ****
  
  val wp_while_monotonic = lemma
!   (``!trans cond l.
         healthy trans /\
!        (!r. expect_lfp (\e s. (if cond s then trans e s else r s)) = l r) ==>
         monotonic (expect,Leq) l``,
     RW_TAC std_ss []
--- 529,535 ----
  
  val wp_while_monotonic = lemma
!   (``!trans cnd l.
         healthy trans /\
!        (!r. expect_lfp (\e s. (if cnd s then trans e s else r s)) = l r) ==>
         monotonic (expect,Leq) l``,
     RW_TAC std_ss []
***************
*** 568,577 ****
  
  val wp_while_upcontinuous = lemma
!   (``!trans cond l.
         healthy trans /\
!        (!r. expect_lfp (\e s. (if cond s then trans e s else r s)) = l r) ==>
!        (!r. (\s. (if cond s then trans (l r) s else r s)) = l r) /\
         (!r y.
!           Leq (\s. (if cond s then trans y s else r s)) y ==> Leq (l r) y) ==>
         up_continuous (expect,Leq) l``,
     RW_TAC std_ss []
--- 547,556 ----
  
  val wp_while_upcontinuous = lemma
!   (``!trans cnd l.
         healthy trans /\
!        (!r. expect_lfp (\e s. (if cnd s then trans e s else r s)) = l r) ==>
!        (!r. (\s. (if cnd s then trans (l r) s else r s)) = l r) /\
         (!r y.
!           Leq (\s. (if cnd s then trans y s else r s)) y ==> Leq (l r) y) ==>
         up_continuous (expect,Leq) l``,
     RW_TAC std_ss []
***************
*** 619,623 ****
         ++ Q.PAT_ASSUM `chain X Y` MP_TAC
         ++ RW_TAC posreal_ss [chain_def, expect_def]
!        ++ MP_TAC (Q.SPECL [`trans`, `cond`, `l`] wp_while_monotonic)
         ++ RW_TAC std_ss [monotonic_def, expect_def]
         ++ METIS_TAC [])
--- 598,602 ----
         ++ Q.PAT_ASSUM `chain X Y` MP_TAC
         ++ RW_TAC posreal_ss [chain_def, expect_def]
!        ++ MP_TAC (Q.SPECL [`trans`, `cnd`, `l`] wp_while_monotonic)
         ++ RW_TAC std_ss [monotonic_def, expect_def]
         ++ METIS_TAC [])
***************
*** 632,640 ****
  
  val wp_while_sublinear1 = lemma
!   (``!cond prog l.
         healthy (wp prog) /\
!        (!r. (\s. (if cond s then wp prog (l r) s else r s)) = l r) /\
         (!r y.
!           Leq (\s. (if cond s then wp prog y s else r s)) y ==> Leq (l r) y) ==>
         (!r c s. ~(c = infty) ==> l r s - c <= l (\s'. r s' - c) s)``,
     RW_TAC posreal_ss []
--- 611,619 ----
  
  val wp_while_sublinear1 = lemma
!   (``!cnd prog l.
         healthy (wp prog) /\
!        (!r. (\s. (if cnd s then wp prog (l r) s else r s)) = l r) /\
         (!r y.
!           Leq (\s. (if cnd s then wp prog y s else r s)) y ==> Leq (l r) y) ==>
         (!r c s. ~(c = infty) ==> l r s - c <= l (\s'. r s' - c) s)``,
     RW_TAC posreal_ss []
***************
*** 661,672 ****
  
  val healthy_wp_while = lemma
!   (``!cond prog. healthy (wp prog) ==> healthy (wp (While cond prog))``,
     RW_TAC real_ss [wp_def]
     ++ Know
        `!r.
!          (expect_lfp (\e s. (if cond s then wp prog e s else r s)) =
!           (\r. expect_lfp (\e s. (if cond s then wp prog e s else r s))) r) /\
!          lfp (expect,Leq) (\e s. if cond s then wp prog e s else r s)
!          ((\r. expect_lfp (\e s. (if cond s then wp prog e s else r s))) r)`
     >> (RW_TAC std_ss []
         ++ MATCH_MP_TAC expect_lfp_def
--- 640,651 ----
  
  val healthy_wp_while = lemma
!   (``!cnd prog. healthy (wp prog) ==> healthy (wp (While cnd prog))``,
     RW_TAC real_ss [wp_def]
     ++ Know
        `!r.
!          (expect_lfp (\e s. (if cnd s then wp prog e s else r s)) =
!           (\r. expect_lfp (\e s. (if cnd s then wp prog e s else r s))) r) /\
!          lfp (expect,Leq) (\e s. if cnd s then wp prog e s else r s)
!          ((\r. expect_lfp (\e s. (if cnd s then wp prog e s else r s))) r)`
     >> (RW_TAC std_ss []
         ++ MATCH_MP_TAC expect_lfp_def
***************
*** 681,689 ****
         ++ METIS_TAC [healthy_mono])
     ++ Q.SPEC_TAC
!       (`\r. expect_lfp (\e s. (if cond s then wp prog e s else r s))`, `l`)
     ++ SIMP_TAC std_ss [lfp_def, expect_def, FORALL_AND_THM]
     ++ RW_TAC std_ss []
!    ++ MP_TAC (Q.SPECL [`cond`, `l`] (Q.ISPEC `wp prog` wp_while_monotonic))
!    ++ MP_TAC (Q.SPECL [`cond`, `l`] (Q.ISPEC `wp prog` wp_while_upcontinuous))
     ++ RW_TAC std_ss []
     ++ ASM_SIMP_TAC real_ss [healthy_def]
--- 660,668 ----
         ++ METIS_TAC [healthy_mono])
     ++ Q.SPEC_TAC
!       (`\r. expect_lfp (\e s. (if cnd s then wp prog e s else r s))`, `l`)
     ++ SIMP_TAC std_ss [lfp_def, expect_def, FORALL_AND_THM]
     ++ RW_TAC std_ss []
!    ++ MP_TAC (Q.SPECL [`cnd`, `l`] (Q.ISPEC `wp prog` wp_while_monotonic))
!    ++ MP_TAC (Q.SPECL [`cnd`, `l`] (Q.ISPEC `wp prog` wp_while_upcontinuous))
     ++ RW_TAC std_ss []
     ++ ASM_SIMP_TAC real_ss [healthy_def]
***************
*** 703,707 ****
         ++ METIS_TAC [feasible_def, healthy_feasible])
     ++ RW_TAC real_ss [sublinear_alt]
!    << [MP_TAC (Q.SPECL [`cond`, `prog`, `l`] wp_while_sublinear1)
         ++ RW_TAC std_ss [],
         Suff `Leq (\s. c * l r s) (l (\s'. c * r s'))` >> RW_TAC std_ss [Leq_def]
--- 682,686 ----
         ++ METIS_TAC [feasible_def, healthy_feasible])
     ++ RW_TAC real_ss [sublinear_alt]
!    << [MP_TAC (Q.SPECL [`cnd`, `prog`, `l`] wp_while_sublinear1)
         ++ RW_TAC std_ss [],
         Suff `Leq (\s. c * l r s) (l (\s'. c * r s'))` >> RW_TAC std_ss [Leq_def]
***************
*** 895,899 ****
         ++ Know `!s. l r s <= & n`
         >> (GEN_TAC
!            ++ MP_TAC (Q.SPECL [`cond`, `prog`, `l`] wp_while_sublinear1)
             ++ ASM_SIMP_TAC std_ss []
             ++ DISCH_THEN (MP_TAC o Q.SPECL [`r`, `& n`, `s`])
--- 874,878 ----
         ++ Know `!s. l r s <= & n`
         >> (GEN_TAC
!            ++ MP_TAC (Q.SPECL [`cnd`, `prog`, `l`] wp_while_sublinear1)
             ++ ASM_SIMP_TAC std_ss []
             ++ DISCH_THEN (MP_TAC o Q.SPECL [`r`, `& n`, `s`])
***************
*** 931,935 ****
            (fn th => CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV [GSYM th])))       
         ++ RW_TAC posreal_ss [Leq_def]
!        ++ REVERSE (Cases_on `cond s` ++ ASM_SIMP_TAC posreal_ss [add_sub])
         ++ POP_ASSUM (K ALL_TAC)
         ++ MP_TAC (Q.SPECL [`\s. l (\s' : state. r1 s' + r s' : posreal) s`,
--- 910,914 ----
            (fn th => CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV [GSYM th])))       
         ++ RW_TAC posreal_ss [Leq_def]
!        ++ REVERSE (Cases_on `cnd s` ++ ASM_SIMP_TAC posreal_ss [add_sub])
         ++ POP_ASSUM (K ALL_TAC)
         ++ MP_TAC (Q.SPECL [`\s. l (\s' : state. r1 s' + r s' : posreal) s`,
***************
*** 998,1002 ****
     RW_TAC std_ss [wp_def, Cond_def]
     ++ CONV_TAC FUN_EQ_CONV
!    ++ RW_TAC posreal_ss [probify_basic]);
  
  (* ------------------------------------------------------------------------- *)
--- 977,981 ----
     RW_TAC std_ss [wp_def, Cond_def]
     ++ CONV_TAC FUN_EQ_CONV
!    ++ RW_TAC posreal_ss [bound1_basic]);
  
  (* ------------------------------------------------------------------------- *)
***************
*** 1029,1033 ****
     (wlp (Demon a b) = \r. Min (wlp a r) (wlp b r)) /\
     (wlp (Prob p a b) =
!     \r s. let x = probify (p s) in x * wlp a r s + (1 - x) * wlp b r s) /\
     (wlp (While c b) = \r. expect_gfp (\e s. if c s then wlp b e s else r s))`;
  
--- 1008,1012 ----
     (wlp (Demon a b) = \r. Min (wlp a r) (wlp b r)) /\
     (wlp (Prob p a b) =
!     \r s. let x = bound1 (p s) in x * wlp a r s + (1 - x) * wlp b r s) /\
     (wlp (While c b) = \r. expect_gfp (\e s. if c s then wlp b e s else r s))`;
  
***************
*** 1059,1072 ****
  val wlp_while = store_thm
    ("wlp_while",
!    ``!cond body pre post.
!        Leq pre (\s. if cond s then wlp body pre s else post s) ==>
!        Leq pre (wlp (While cond body) post)``,
     RW_TAC std_ss [wlp_def]
     ++ Know
        `!r.
!          (expect_gfp (\e s. (if cond s then wlp body e s else r s)) =
!           (\r. expect_gfp (\e s. (if cond s then wlp body e s else r s))) r) /\
!          gfp (expect,Leq) (\e s. if cond s then wlp body e s else r s)
!          ((\r. expect_gfp (\e s. (if cond s then wlp body e s else r s))) r)`
     >> (RW_TAC std_ss []
         ++ MATCH_MP_TAC expect_gfp_def
--- 1038,1051 ----
  val wlp_while = store_thm
    ("wlp_while",
!    ``!cnd body pre post.
!        Leq pre (\s. if cnd s then wlp body pre s else post s) ==>
!        Leq pre (wlp (While cnd body) post)``,
     RW_TAC std_ss [wlp_def]
     ++ Know
        `!r.
!          (expect_gfp (\e s. (if cnd s then wlp body e s else r s)) =
!           (\r. expect_gfp (\e s. (if cnd s then wlp body e s else r s))) r) /\
!          gfp (expect,Leq) (\e s. if cnd s then wlp body e s else r s)
!          ((\r. expect_gfp (\e s. (if cnd s then wlp body e s else r s))) r)`
     >> (RW_TAC std_ss []
         ++ MATCH_MP_TAC expect_gfp_def
***************
*** 1081,1085 ****
     ++ SIMP_TAC std_ss []
     ++ Q.SPEC_TAC
!       (`expect_gfp (\e s. (if cond s then wlp body e s else post s))`, `g`)
     ++ RW_TAC std_ss [gfp_def, expect_def]);
  
--- 1060,1064 ----
     ++ SIMP_TAC std_ss []
     ++ Q.SPEC_TAC
!       (`expect_gfp (\e s. (if cnd s then wlp body e s else post s))`, `g`)
     ++ RW_TAC std_ss [gfp_def, expect_def]);
  
***************
*** 1088,1105 ****
  (* ------------------------------------------------------------------------- *)
  
! val wlp_assign_def = Define
!   `wlp_assign v e s = \w. if w = v then e s else s w`;
! 
! val wlp_demon_def = Define `wlp_demon a b s = min (a s) (b s)`;
! 
! val wlp_prob_def = Define
!   `wlp_prob p a b s = let x = probify (p s) in x * a s + (1 - x) * b s`;
! 
! val wlp_cond_def = Define `wlp_cond c a b s = if c s then a s else b s`;
! 
! val wlp_assign = store_thm
!   ("wlp_assign",
!    ``!v e s w. wlp_assign v e s w = if v = w then e s else s w``,
!    RW_TAC std_ss [wlp_assign_def]);
  
  val wlp_assert_vc = store_thm
--- 1067,1071 ----
  (* ------------------------------------------------------------------------- *)
  
! val wlp_min_def = Define `wlp_min a b s = min (a s) (b s)`;
  
  val wlp_assert_vc = store_thm
***************
*** 1124,1129 ****
  val wlp_assign_vc = store_thm
    ("wlp_assign_vc",
!    ``!post v e. Leq (post o wlp_assign v e) (wlp (Assign v e) post)``,
!    RW_TAC std_ss [wlp_def, Leq_def, wlp_assign_def, o_THM, le_refl]);
  
  val wlp_seq_vc = store_thm
--- 1090,1095 ----
  val wlp_assign_vc = store_thm
    ("wlp_assign_vc",
!    ``!post v e. Leq (post o assign v e) (wlp (Assign v e) post)``,
!    RW_TAC std_ss [wlp_def, Leq_def, assign_eta, o_THM, le_refl]);
  
  val wlp_seq_vc = store_thm
***************
*** 1142,1151 ****
     ``!pre1 pre2 post c1 c2.
         Leq pre1 (wlp c1 post) /\ Leq pre2 (wlp c2 post) ==>
!        Leq (wlp_demon pre1 pre2) (wlp (Demon c1 c2) post)``,
     RW_TAC std_ss [wlp_def, Leq_def]
     ++ MATCH_MP_TAC le_trans
!    ++ Q.EXISTS_TAC `wlp_demon pre1 pre2 s`
     ++ RW_TAC std_ss []
!    ++ RW_TAC std_ss [wlp_demon_def, Min_def, le_refl]
     ++ METIS_TAC [min_le2_imp]);
  
--- 1108,1117 ----
     ``!pre1 pre2 post c1 c2.
         Leq pre1 (wlp c1 post) /\ Leq pre2 (wlp c2 post) ==>
!        Leq (wlp_min pre1 pre2) (wlp (Demon c1 c2) post)``,
     RW_TAC std_ss [wlp_def, Leq_def]
     ++ MATCH_MP_TAC le_trans
!    ++ Q.EXISTS_TAC `wlp_min pre1 pre2 s`
     ++ RW_TAC std_ss []
!    ++ RW_TAC std_ss [wlp_min_def, Min_def, le_refl]
     ++ METIS_TAC [min_le2_imp]);
  
***************
*** 1154,1163 ****
     ``!pre1 pre2 post p c1 c2.
         Leq pre1 (wlp c1 post) /\ Leq pre2 (wlp c2 post) ==>
!        Leq (wlp_prob p pre1 pre2) (wlp (Prob p c1 c2) post)``,
     RW_TAC std_ss [wlp_def, Leq_def]
     ++ MATCH_MP_TAC le_trans
!    ++ Q.EXISTS_TAC `wlp_prob p pre1 pre2 s`
     ++ RW_TAC std_ss []
!    ++ RW_TAC std_ss [wlp_prob_def, le_refl]
     ++ METIS_TAC [le_add2, le_lmul_imp]);
  
--- 1120,1129 ----
     ``!pre1 pre2 post p c1 c2.
         Leq pre1 (wlp c1 post) /\ Leq pre2 (wlp c2 post) ==>
!        Leq (prob p pre1 pre2) (wlp (Prob p c1 c2) post)``,
     RW_TAC std_ss [wlp_def, Leq_def]
     ++ MATCH_MP_TAC le_trans
!    ++ Q.EXISTS_TAC `prob p pre1 pre2 s`
     ++ RW_TAC std_ss []
!    ++ RW_TAC std_ss [prob_def, le_refl]
     ++ METIS_TAC [le_add2, le_lmul_imp]);
  
***************
*** 1165,1169 ****
    ("wlp_while_vc",
     ``!pre post mid b c.
!        Leq mid (wlp c pre) /\ Leq pre (wlp_cond b mid post) ==>
         Leq pre (wlp (Assert pre (While b c)) post)``,
     RW_TAC std_ss []
--- 1131,1135 ----
    ("wlp_while_vc",
     ``!pre post mid b c.
!        Leq mid (wlp c pre) /\ Leq pre (cond b mid post) ==>
         Leq pre (wlp (Assert pre (While b c)) post)``,
     RW_TAC std_ss []
***************
*** 1172,1176 ****
     ++ RW_TAC std_ss [leq_refl]
     ++ MATCH_MP_TAC wlp_while
!    ++ FULL_SIMP_TAC std_ss [Leq_def, wlp_cond_def]
     ++ METIS_TAC [le_trans]);
  
--- 1138,1142 ----
     ++ RW_TAC std_ss [leq_refl]
     ++ MATCH_MP_TAC wlp_while
!    ++ FULL_SIMP_TAC std_ss [Leq_def, cond_def]
     ++ METIS_TAC [le_trans]);
  
***************
*** 1179,1188 ****
     ``!pre1 pre2 post b c1 c2.
         Leq pre1 (wlp c1 post) /\ Leq pre2 (wlp c2 post) ==>
!        Leq (wlp_cond b pre1 pre2) (wlp (Cond b c1 c2) post)``,
     RW_TAC std_ss [Cond_def]
     ++ MATCH_MP_TAC leq_trans
!    ++ Q.EXISTS_TAC `wlp_prob (\s. if b s then 1 else 0) pre1 pre2`
     ++ REVERSE CONJ_TAC >> METIS_TAC [wlp_prob_vc]
!    ++ RW_TAC std_ss [Leq_def, probify_def, wlp_prob_def, wlp_cond_def]
     ++ RW_TAC posreal_ss []
     ++ FULL_SIMP_TAC posreal_ss []);
--- 1145,1154 ----
     ``!pre1 pre2 post b c1 c2.
         Leq pre1 (wlp c1 post) /\ Leq pre2 (wlp c2 post) ==>
!        Leq (cond b pre1 pre2) (wlp (Cond b c1 c2) post)``,
     RW_TAC std_ss [Cond_def]
     ++ MATCH_MP_TAC leq_trans
!    ++ Q.EXISTS_TAC `prob (\s. if b s then 1 else 0) pre1 pre2`
     ++ REVERSE CONJ_TAC >> METIS_TAC [wlp_prob_vc]
!    ++ RW_TAC std_ss [Leq_def, bound1_def, prob_def, cond_def]
     ++ RW_TAC posreal_ss []
     ++ FULL_SIMP_TAC posreal_ss []);

Index: wpTools.sml
===================================================================
RCS file: /cvsroot/hol/hol98/examples/pgcl/src/wpTools.sml,v
retrieving revision 1.3
retrieving revision 1.4
diff -b -C2 -d -r1.3 -r1.4
*** wpTools.sml	24 Sep 2003 14:27:18 -0000	1.3
--- wpTools.sml	30 Sep 2003 01:44:56 -0000	1.4
***************
*** 8,12 ****
  open HolKernel Parse boolLib bossLib simpLib metisLib intLib
       integerTheory stringTheory combinTheory listTheory
!      posrealLib expectationTheory wpTheory;
  
  (* ------------------------------------------------------------------------- *)
--- 8,12 ----
  open HolKernel Parse boolLib bossLib simpLib metisLib intLib
       integerTheory stringTheory combinTheory listTheory
!      posrealTheory posrealLib expectationTheory wpTheory;
  
  (* ------------------------------------------------------------------------- *)
***************
*** 176,180 ****
      let
        (*val () = print ("\nthm = " ^ thm_to_string th ^ "\n");*)
!       val th1 = SIMP_RULE arith_ss ([STRING_11, CHR_11, wlp_assign] @ ths) th
        val th2 = SIMP_RULE int_ss int_simps th1
        val th3 = SIMP_RULE posreal_reduce_ss [] th2
--- 176,180 ----
      let
        (*val () = print ("\nthm = " ^ thm_to_string th ^ "\n");*)
!       val th1 = SIMP_RULE arith_ss ([STRING_11, CHR_11, assign_def] @ ths) th
        val th2 = SIMP_RULE int_ss int_simps th1
        val th3 = SIMP_RULE posreal_reduce_ss [] th2
***************
*** 189,193 ****
  local
    fun simps ths = ths @
!     [wlp_demon_def, wlp_prob_def, wlp_cond_def, o_THM, magic_alt, wlp_assign];
  in
    val leq_tac =
--- 189,193 ----
  local
    fun simps ths = ths @
!     [wlp_min_def, prob_def, cond_def, o_THM, magic_alt, assign_def];
  in
    val leq_tac =
***************
*** 201,205 ****
      THEN elim_redundant_lam_tac
      THEN RW_TAC posreal_ss []
!     THEN RW_TAC posreal_reduce_ss [probify_def];
  end;
  
--- 201,205 ----
      THEN elim_redundant_lam_tac
      THEN RW_TAC posreal_ss []
!     THEN RW_TAC posreal_reduce_ss [bound1_def];
  end;

Update of /cvsroot/hol/hol98/examples/pgcl/examples
In directory sc8-pr-cvs1:/tmp/cvs-serv3458/examples

Modified Files:
	verification.sml 
Log Message:
Some reorganization and name changes while I'm correcting my pGCL paper.


Index: verification.sml
===================================================================
RCS file: /cvsroot/hol/hol98/examples/pgcl/examples/verification.sml,v
retrieving revision 1.4
retrieving revision 1.5
diff -b -C2 -d -r1.4 -r1.5
*** verification.sml	26 Sep 2003 23:04:10 -0000	1.4
--- verification.sml	30 Sep 2003 01:44:56 -0000	1.5
***************
*** 41,45 ****
      Demons_def, MAP, LENGTH, CHR_11, FUN_EQ_THM, Zero_def, Min_def]
     ++ FULL_SIMP_TAC int_ss []
!    ++ FULL_SIMP_TAC posreal_reduce_ss [probify_def]);
  
  val demon_then_prob = Count.apply prove
--- 41,45 ----
      Demons_def, MAP, LENGTH, CHR_11, FUN_EQ_THM, Zero_def, Min_def]
     ++ FULL_SIMP_TAC int_ss []
!    ++ FULL_SIMP_TAC posreal_reduce_ss [bound1_def]);
  
  val demon_then_prob = Count.apply prove
***************
*** 50,54 ****
      Demons_def, MAP, LENGTH, CHR_11, FUN_EQ_THM, Zero_def, Min_def]
     ++ FULL_SIMP_TAC int_ss []
!    ++ FULL_SIMP_TAC posreal_reduce_ss [probify_def]);
  
  val partial_demon_then_prob = Count.apply prove
--- 50,54 ----
      Demons_def, MAP, LENGTH, CHR_11, FUN_EQ_THM, Zero_def, Min_def]
     ++ FULL_SIMP_TAC int_ss []
!    ++ FULL_SIMP_TAC posreal_reduce_ss [bound1_def]);
  
  val partial_demon_then_prob = Count.apply prove
***************
*** 157,165 ****
                        CHR_11]
     ++ RW_TAC int_ss []
!    ++ RW_TAC posreal_ss [probify_basic, Zero_def]
     ++ RW_TAC std_ss [wp_incognito_def]
     ++ RW_TAC int_ss [monty_hide_def, MAP, wp_def, Demonchoice_def,
                       Demons_def, Min_def]
!    ++ RW_TAC posreal_reduce_ss [probify_def]);
    
  (* ------------------------------------------------------------------------- *)
--- 157,165 ----
                        CHR_11]
     ++ RW_TAC int_ss []
!    ++ RW_TAC posreal_ss [bound1_basic, Zero_def]
     ++ RW_TAC std_ss [wp_incognito_def]
     ++ RW_TAC int_ss [monty_hide_def, MAP, wp_def, Demonchoice_def,
                       Demons_def, Min_def]
!    ++ RW_TAC posreal_reduce_ss [bound1_def]);
    
  (* ------------------------------------------------------------------------- *)
***************
*** 179,183 ****
            (1 / 2) * r (\w. if w = "n" then v"n" - 1 else v w) +
            (1 / 2) * r (\w. if w = "n" then v"n" + 1 else v w))``,
!    RW_TAC posreal_ss [wp_def, lurch_def, probify_basic, COND_RAND]
     ++ RW_TAC posreal_reduce_ss []);
  
--- 179,183 ----
            (1 / 2) * r (\w. if w = "n" then v"n" - 1 else v w) +
            (1 / 2) * r (\w. if w = "n" then v"n" + 1 else v w))``,
!    RW_TAC posreal_ss [wp_def, lurch_def, bound1_basic, COND_RAND]
     ++ RW_TAC posreal_reduce_ss []);

Update of /cvsroot/hol/hol98/src/string
In directory sc8-pr-cvs1:/tmp/cvs-serv29037

Modified Files:
	stringScript.sml 
Log Message:
A couple of new, and obvious, theorems, prompted by netsem work.


Index: stringScript.sml
===================================================================
RCS file: /cvsroot/hol/hol98/src/string/stringScript.sml,v
retrieving revision 1.13
retrieving revision 1.14
diff -b -C2 -d -r1.13 -r1.14
*** stringScript.sml	31 Jul 2003 21:17:48 -0000	1.13
--- stringScript.sml	29 Sep 2003 07:04:58 -0000	1.14
***************
*** 276,279 ****
--- 276,301 ----
     ---------------------------------------------------------------------- *)
  
+ val IMPLODE_EQ_EMPTYSTRING = store_thm(
+   "IMPLODE_EQ_EMPTYSTRING",
+   ``((IMPLODE l = "") = (l = [])) /\
+     (("" = IMPLODE l) = (l = []))``,
+   CONV_TAC (RAND_CONV (LAND_CONV (ONCE_REWRITE_CONV [EQ_SYM_EQ]))) THEN
+   REWRITE_TAC [] THEN
+   RW_TAC bool_ss [EQ_IMP_THM, IMPLODE_EQNS, IMPLODE_EXPLODE] THEN
+   POP_ASSUM (MP_TAC o Q.AP_TERM `EXPLODE`) THEN
+   RW_TAC bool_ss [EXPLODE_EQNS, EXPLODE_IMPLODE]);
+ 
+ val EXPLODE_EQ_NIL = store_thm(
+   "EXPLODE_EQ_NIL",
+   ``((EXPLODE s = []) = (s = "")) /\
+     (([] = EXPLODE s) = (s = ""))``,
+   CONV_TAC (RAND_CONV (LAND_CONV (ONCE_REWRITE_CONV [EQ_SYM_EQ]))) THEN
+   REWRITE_TAC [] THEN
+   RW_TAC bool_ss [EQ_IMP_THM, EXPLODE_EQNS, EXPLODE_IMPLODE] THEN
+   POP_ASSUM (MP_TAC o Q.AP_TERM `IMPLODE`) THEN
+   RW_TAC bool_ss [IMPLODE_EQNS, IMPLODE_EXPLODE]);
+ 
+ 
+ 
  val EXPLODE_EQ_THM = Q.store_thm
  ("EXPLODE_EQ_THM",
***************
*** 386,390 ****
     ["ORD_CHR_RWT","IMPLODE_EXPLODE", "EXPLODE_IMPLODE",
      "IMPLODE_11", "EXPLODE_11","EXPLODE_EQNS", "IMPLODE_EQNS",
!     "EXPLODE_EQ_THM", "IMPLODE_EQ_THM", "STRLEN_DEF"];
  
  
--- 408,413 ----
     ["ORD_CHR_RWT","IMPLODE_EXPLODE", "EXPLODE_IMPLODE",
      "IMPLODE_11", "EXPLODE_11","EXPLODE_EQNS", "IMPLODE_EQNS",
!     "EXPLODE_EQ_THM", "IMPLODE_EQ_THM", "STRLEN_DEF",
!     "IMPLODE_EQ_EMPTYSTRING", "EXPLODE_EQ_NIL"];

Update of /cvsroot/hol/hol98/src/bag
In directory sc8-pr-cvs1:/tmp/cvs-serv11913

Modified Files:
	bagScript.sml 
Log Message:
A couple of new functions for bags: BAG_FILTER which does what you might
expect, and BAG_IMAGE, which I thought would be equally obvious, but
turns out to be slightly complicated.  I think there's quite possibly
an argument that instead of mapping an infinite number of elements to 
zero, I should map it to one (see comments in the script file to see
what I'm on about here).  


Index: bagScript.sml
===================================================================
RCS file: /cvsroot/hol/hol98/src/bag/bagScript.sml,v
retrieving revision 1.22
retrieving revision 1.23
diff -b -C2 -d -r1.22 -r1.23
*** bagScript.sml	3 Sep 2003 13:46:01 -0000	1.22
--- bagScript.sml	29 Sep 2003 05:02:26 -0000	1.23
***************
*** 1046,1049 ****
--- 1046,1051 ----
    "FINITE_BAG_THM",
    CONJ FINITE_EMPTY_BAG FINITE_BAG_INSERT);
+ val _ = export_rewrites ["FINITE_BAG_THM"]
+ 
  
  val FINITE_BAG_DIFF = Q.store_thm(
***************
*** 1234,1237 ****
--- 1236,1241 ----
     ONCE_REWRITE_RULE [BCARD_rwts] >-
     SIMP_RULE hol_ss [BAG_INSERT_NOT_EMPTY]) BAG_CARD;
+ val _ = save_thm("BAG_CARD_EMPTY", BAG_CARD_EMPTY)
+ val _ = export_rewrites ["BAG_CARD_EMPTY"]
  
  val BCARD_0 = Q.store_thm(
***************
*** 1296,1299 ****
--- 1300,1414 ----
    ]);
  
+ (* ----------------------------------------------------------------------
+     FILTER for bags (alternatively, intersection with a set)
+    ---------------------------------------------------------------------- *)
+ 
+ val BAG_FILTER_DEF = new_definition(
+   "BAG_FILTER_DEF",
+   ``BAG_FILTER P (b :'a bag) : 'a bag = \e. if P e then b e else 0``);
+ 
+ val BAG_FILTER_EMPTY = store_thm(
+   "BAG_FILTER_EMPTY",
+   ``BAG_FILTER P {||} = {||}``,
+   SRW_TAC [][BAG_FILTER_DEF, FUN_EQ_THM] THEN
+   SRW_TAC [][EMPTY_BAG]);
+ val _ = BasicProvers.export_rewrites ["BAG_FILTER_EMPTY"]
+ 
+ val BAG_FILTER_BAG_INSERT = store_thm(
+   "BAG_FILTER_BAG_INSERT",
+   ``BAG_FILTER P (BAG_INSERT e b) = if P e then BAG_INSERT e (BAG_FILTER P b)
+                                     else BAG_FILTER P b``,
+   SRW_TAC [][BAG_FILTER_DEF, FUN_EQ_THM] THEN
+   SRW_TAC [][BAG_INSERT] THEN RES_TAC);
+ val _ = BasicProvers.export_rewrites ["BAG_FILTER_BAG_INSERT"]
+ 
+ val FINITE_BAG_FILTER = store_thm(
+   "FINITE_BAG_FILTER",
+   ``!b. FINITE_BAG b ==> FINITE_BAG (BAG_FILTER P b)``,
+   HO_MATCH_MP_TAC FINITE_BAG_INDUCT THEN SRW_TAC [][] THEN
+   SRW_TAC [][]);
+ val _ = export_rewrites ["FINITE_BAG_FILTER"]
+ 
+ val BAG_INN_BAG_FILTER = store_thm(
+   "BAG_INN_BAG_FILTER",
+   ``BAG_INN e n (BAG_FILTER P b) = (n = 0) \/ P e /\ BAG_INN e n b``,
+   SRW_TAC [numSimps.ARITH_ss][BAG_FILTER_DEF, BAG_INN]);
+ val _ = export_rewrites ["BAG_INN_BAG_FILTER"]
+ 
+ val BAG_IN_BAG_FILTER = store_thm(
+   "BAG_IN_BAG_FILTER",
+   ``BAG_IN e (BAG_FILTER P b) = P e /\ BAG_IN e b``,
+   SRW_TAC [][BAG_IN]);
+ val _ = export_rewrites ["BAG_IN_BAG_FILTER"]
+ 
+ (* ----------------------------------------------------------------------
+     IMAGE for bags.
+ 
+     This is complicated by the fact that a taking the image of a
+     non-injective function over an infinite bag might produce a bag that
+     wanted to have an infinite number of some element.  For example,
+        BAG_IMAGE (\e. 1) (BAG_OF_SET (UNIV : num set))
+     would want to populate a bag with an infinite number of ones.
+ 
+     BAG_IMAGE is "safe" if the input bag is finite, or if the function is
+     only finitely non-injective.  I don't want to have these side conditions
+     hanging around on my theorems, so I've decided to simply make BAG_IMAGE
+     take elements that want to be infinite to zero instead.
+    ---------------------------------------------------------------------- *)
+ 
+ val BAG_IMAGE_DEF = new_definition(
+   "BAG_IMAGE_DEF",
+   ``BAG_IMAGE f b = \e. let sb = BAG_FILTER (\e0. f e0 = e) b
+                         in
+                             if FINITE_BAG sb then BAG_CARD sb
+                             else 0``);
+ 
+ val BAG_IMAGE_EMPTY = store_thm(
+   "BAG_IMAGE_EMPTY",
+   ``BAG_IMAGE f {||} = {||}``,
+   SRW_TAC [][BAG_IMAGE_DEF] THEN SRW_TAC [][EMPTY_BAG_alt]);
+ val _ = export_rewrites ["BAG_IMAGE_EMPTY"]
+ 
+ val BAG_IMAGE_FINITE_INSERT = store_thm(
+   "BAG_IMAGE_FINITE_INSERT",
+   ``!b. FINITE_BAG b ==>
+         (BAG_IMAGE f (BAG_INSERT e b) = BAG_INSERT (f e) (BAG_IMAGE f b))``,
+   SRW_TAC [][BAG_IMAGE_DEF] THEN
+   SRW_TAC [][FUN_EQ_THM] THEN
+   Cases_on `f e = e'` THENL [
+     SRW_TAC [][BAG_CARD_THM] THEN SRW_TAC [][BAG_INSERT],
+     SRW_TAC [][] THEN SRW_TAC [][BAG_INSERT]
+   ]);
+ val _ = export_rewrites ["BAG_IMAGE_FINITE_INSERT"]
+ 
+ val BAG_IMAGE_FINITE = store_thm(
+   "BAG_IMAGE_FINITE",
+   ``!b. FINITE_BAG b ==> FINITE_BAG (BAG_IMAGE f b)``,
+   HO_MATCH_MP_TAC STRONG_FINITE_BAG_INDUCT THEN SRW_TAC [][]);
+ val _ = export_rewrites ["BAG_IMAGE_FINITE"]
+ 
+ val BAG_IN_FINITE_BAG_IMAGE = store_thm(
+   "BAG_IN_FINITE_BAG_IMAGE",
+   ``FINITE_BAG b ==>
+     (BAG_IN x (BAG_IMAGE f b) = ?y. (f y = x) /\ BAG_IN y b)``,
+   SRW_TAC [][BAG_IMAGE_DEF] THEN EQ_TAC THEN STRIP_TAC THENL [
+     FULL_SIMP_TAC (srw_ss()) [BAG_IN, BAG_INN] THEN
+     Q.ABBREV_TAC `bf = BAG_FILTER (\e0. f e0 = x) b` THEN
+     `FINITE_BAG bf` by SRW_TAC [][] THEN
+     `0 < BAG_CARD bf` by SRW_TAC [numSimps.ARITH_ss][] THEN
+     `?m. BAG_CARD bf = SUC m`
+         by PROVE_TAC [arithmeticTheory.num_CASES,
+                       arithmeticTheory.NOT_ZERO_LT_ZERO] THEN
+     `?e bf0. (bf = BAG_INSERT e bf0)` by PROVE_TAC [BCARD_SUC] THEN
+     `BAG_IN e bf` by SRW_TAC [][BAG_IN_BAG_INSERT] THEN
+     `BAG_IN e (BAG_FILTER (\e0. f e0 = x) b)` by PROVE_TAC [] THEN
+     POP_ASSUM (STRIP_ASSUME_TAC o SIMP_RULE bool_ss [BAG_IN_BAG_FILTER]) THEN
+     PROVE_TAC [BAG_IN, BAG_INN],
+     `?b0. BAG_DELETE b y b0` by PROVE_TAC [BAG_IN_BAG_DELETE] THEN
+     `b = BAG_INSERT y b0` by PROVE_TAC [BAG_DELETE] THEN
+     SIMP_TAC (srw_ss()) [BAG_IN, BAG_INN] THEN SRW_TAC [][] THEN
+     FULL_SIMP_TAC (srw_ss() ++ numSimps.ARITH_ss) [BAG_CARD_THM]
+   ]);
+ val _ = export_rewrites ["BAG_IN_FINITE_BAG_IMAGE"]
  
  (*---------------------------------------------------------------------------

Update of /cvsroot/hol/hol98/examples/pgcl/examples
In directory sc8-pr-cvs1:/tmp/cvs-serv28769/examples

Modified Files:
	verification.sml 
Log Message:
The example now works with the current version of HOL4.


Index: verification.sml
===================================================================
RCS file: /cvsroot/hol/hol98/examples/pgcl/examples/verification.sml,v
retrieving revision 1.3
retrieving revision 1.4
diff -b -C2 -d -r1.3 -r1.4
*** verification.sml	24 Sep 2003 14:27:17 -0000	1.3
--- verification.sml	26 Sep 2003 23:04:10 -0000	1.4
***************
*** 240,252 ****
                           Assign "n" (\v. v"n" - 1)]))]))`;
  
! val wlp_annotated_rabin = Count.apply prove
!   (``wlp annotated_rabin = wlp rabin``,
!    RW_TAC std_ss [annotated_rabin_def, rabin_def, FUN_EQ_THM]
!    ++ RW_TAC std_ss [wlp_def, Program_def]);
  
  val partial_rabin = Count.apply prove
    (``Leq (\v. if v"i" = 1 then 1 else if 1 < v"i" then 2 / 3 else 0)
       (wlp rabin (\v. if v"i" = 1 then 1 else 0))``,
!    (RW_TAC std_ss [annotated_rabin_def, GSYM wlp_annotated_rabin]
      ++ wlp_tac
      ++ TRY (Suff `F` >> METIS_TAC [] ++ COOPER_TAC)
--- 240,251 ----
                           Assign "n" (\v. v"n" - 1)]))]))`;
  
! val annotated_rabin = Count.apply prove
!   (``annotated_rabin = rabin``,
!    RW_TAC std_ss [annotated_rabin_def, Assert_def, rabin_def]);
  
  val partial_rabin = Count.apply prove
    (``Leq (\v. if v"i" = 1 then 1 else if 1 < v"i" then 2 / 3 else 0)
       (wlp rabin (\v. if v"i" = 1 then 1 else 0))``,
!    (RW_TAC std_ss [annotated_rabin_def, GSYM annotated_rabin]
      ++ wlp_tac
      ++ TRY (Suff `F` >> METIS_TAC [] ++ COOPER_TAC)

Update of /cvsroot/hol/hol98/examples/pgcl/src
In directory sc8-pr-cvs1:/tmp/cvs-serv28769/src

Modified Files:
	wpScript.sml 
Log Message:
The example now works with the current version of HOL4.


Index: wpScript.sml
===================================================================
RCS file: /cvsroot/hol/hol98/examples/pgcl/src/wpScript.sml,v
retrieving revision 1.2
retrieving revision 1.3
diff -b -C2 -d -r1.2 -r1.3
*** wpScript.sml	25 Sep 2003 09:59:20 -0000	1.2
--- wpScript.sml	26 Sep 2003 23:04:10 -0000	1.3
***************
*** 9,13 ****
  (* ------------------------------------------------------------------------- *)
  (*
- *)
  loadPath :=
    ["/home/jeh1004/dev/hol/metis/src/mlib",
--- 9,12 ----
***************
*** 18,21 ****
--- 17,21 ----
     "metisLib","posrealLib","expectationTheory","intLib"(*,"MetisLib"*)];
  quietdec := true;
+ *)
  
  open HolKernel Parse boolLib bossLib intLib realLib metisLib;
***************
*** 25,30 ****
  
  (*
- *)
  quietdec := false;
  
  (* ------------------------------------------------------------------------- *)
--- 25,30 ----
  
  (*
  quietdec := false;
+ *)
  
  (* ------------------------------------------------------------------------- *)
***************
*** 91,96 ****
  
  val () = Hol_datatype `command =
!   Assert of (state -> posreal) => command
! | Abort
  | Skip
  | Assign of string => (state -> int)
--- 91,95 ----
  
  val () = Hol_datatype `command =
!   Abort
  | Skip
  | Assign of string => (state -> int)
***************
*** 100,103 ****
--- 99,104 ----
  | While  of (state -> bool) => command`;
  
+ val Assert_def = Define `Assert (x : state -> posreal) (c : command) = c`;
+ 
  val Program_def = Define
    `(Program [] = Skip) /\
***************
*** 144,149 ****
  
  val wp_def = Define
!   `(wp (Assert p a) = wp a) /\
!    (wp Abort = \r. Zero) /\
     (wp Skip = \r. r) /\
     (wp (Assign v e) = \r s. r (\w. if w = v then e s else s w)) /\
--- 145,149 ----
  
  val wp_def = Define
!   `(wp Abort = \r. Zero) /\
     (wp Skip = \r. r) /\
     (wp (Assign v e) = \r s. r (\w. if w = v then e s else s w)) /\
***************
*** 180,187 ****
  (* ------------------------------------------------------------------------- *)
  
- val healthy_wp_assert = lemma
-   (``!exp prog. healthy (wp prog) ==> healthy (wp (Assert exp prog))``,
-    RW_TAC posreal_ss [wp_def]);
- 
  val healthy_wp_abort = lemma
    (``healthy (wp Abort)``,
--- 180,183 ----
***************
*** 408,422 ****
         ++ Know `sublinear (wp prog)` >> PROVE_TAC [healthy_sublinear]
         ++ SIMP_TAC std_ss [sublinear_def]
!        ++ DISCH_THEN (MP_TAC o Q.SPECL [`r1`, `r2`, `c1`, `c2`, `c`, `s`])
         ++ Know `sublinear (wp prog')` >> PROVE_TAC [healthy_sublinear]
         ++ SIMP_TAC std_ss [sublinear_def]
!        ++ DISCH_THEN (MP_TAC o Q.SPECL [`r1`, `r2`, `c1`, `c2`, `c`, `s`])
         ++ ASM_SIMP_TAC std_ss []
!        ++ Q.SPEC_TAC (`wp prog' r1 s`, `x1'`)
!        ++ Q.SPEC_TAC (`wp prog' r2 s`, `x2'`)
!        ++ Q.SPEC_TAC (`wp prog r1 s`, `x1`)
!        ++ Q.SPEC_TAC (`wp prog r2 s`, `x2`)
!        ++ Q.SPEC_TAC (`wp prog' (\s'. c1 * r1 s' + c2 * r2 s' - c) s`, `y'`)
!        ++ Q.SPEC_TAC (`wp prog (\s'. c1 * r1 s' + c2 * r2 s' - c) s`, `y`)
         ++ REPEAT (Q.PAT_ASSUM `healthy X` (K ALL_TAC))
         ++ RW_TAC posreal_ss [add_ldistrib]
--- 404,418 ----
         ++ Know `sublinear (wp prog)` >> PROVE_TAC [healthy_sublinear]
         ++ SIMP_TAC std_ss [sublinear_def]
!        ++ DISCH_THEN (MP_TAC o Q.SPECL [`r`, `r'`, `c1`, `c2`, `c`, `s`])
         ++ Know `sublinear (wp prog')` >> PROVE_TAC [healthy_sublinear]
         ++ SIMP_TAC std_ss [sublinear_def]
!        ++ DISCH_THEN (MP_TAC o Q.SPECL [`r`, `r'`, `c1`, `c2`, `c`, `s`])
         ++ ASM_SIMP_TAC std_ss []
!        ++ Q.SPEC_TAC (`wp prog' r s`, `x1'`)
!        ++ Q.SPEC_TAC (`wp prog' r' s`, `x2'`)
!        ++ Q.SPEC_TAC (`wp prog r s`, `x1`)
!        ++ Q.SPEC_TAC (`wp prog r' s`, `x2`)
!        ++ Q.SPEC_TAC (`wp prog' (\s'. c1 * r s' + c2 * r' s' - c) s`, `y'`)
!        ++ Q.SPEC_TAC (`wp prog (\s'. c1 * r s' + c2 * r' s' - c) s`, `y`)
         ++ REPEAT (Q.PAT_ASSUM `healthy X` (K ALL_TAC))
         ++ RW_TAC posreal_ss [add_ldistrib]
***************
*** 448,457 ****
         >> PROVE_TAC [healthy_up_continuous]
         ++ RW_TAC std_ss [up_continuous_def, expect_def]
!        ++ POP_ASSUM (MP_TAC o Q.SPECL [`c`, `x`])
         ++ RW_TAC posreal_ss []
         ++ Know `up_continuous (expect,Leq) (wp prog')`
         >> PROVE_TAC [healthy_up_continuous]
         ++ RW_TAC std_ss [up_continuous_def, expect_def]
!        ++ POP_ASSUM (MP_TAC o Q.SPECL [`c`, `x`])
         ++ RW_TAC posreal_ss []
         ++ RW_TAC std_ss [lub_def, expect_def]
--- 444,453 ----
         >> PROVE_TAC [healthy_up_continuous]
         ++ RW_TAC std_ss [up_continuous_def, expect_def]
!        ++ POP_ASSUM (MP_TAC o Q.SPECL [`c`, `r'`])
         ++ RW_TAC posreal_ss []
         ++ Know `up_continuous (expect,Leq) (wp prog')`
         >> PROVE_TAC [healthy_up_continuous]
         ++ RW_TAC std_ss [up_continuous_def, expect_def]
!        ++ POP_ASSUM (MP_TAC o Q.SPECL [`c`, `r'`])
         ++ RW_TAC posreal_ss []
         ++ RW_TAC std_ss [lub_def, expect_def]
***************
*** 459,466 ****
             ++ MATCH_MP_TAC le_add2
             ++ (CONJ_TAC ++ MATCH_MP_TAC le_lmul_imp)
!            << [Suff `Leq (wp prog z) (wp prog x)` >> RW_TAC std_ss [Leq_def]
                 ++ MATCH_MP_TAC healthy_mono
                 ++ METIS_TAC [lub_def, expect_def],
!                Suff `Leq (wp prog' z) (wp prog' x)` >> RW_TAC std_ss [Leq_def]
                 ++ MATCH_MP_TAC healthy_mono
                 ++ PROVE_TAC [lub_def, expect_def]])
--- 455,462 ----
             ++ MATCH_MP_TAC le_add2
             ++ (CONJ_TAC ++ MATCH_MP_TAC le_lmul_imp)
!            << [Suff `Leq (wp prog r) (wp prog r')` >> RW_TAC std_ss [Leq_def]
                 ++ MATCH_MP_TAC healthy_mono
                 ++ METIS_TAC [lub_def, expect_def],
!                Suff `Leq (wp prog' r) (wp prog' r')` >> RW_TAC std_ss [Leq_def]
                 ++ MATCH_MP_TAC healthy_mono
                 ++ PROVE_TAC [lub_def, expect_def]])
***************
*** 565,571 ****
         ++ RW_TAC std_ss [Leq_def]
         ++ RW_TAC posreal_ss [])
!    << [Suff `Leq (trans x') (trans y')` >> RW_TAC std_ss [Leq_def]
         ++ METIS_TAC [healthy_mono],
!        Suff `Leq (trans x') (trans y')` >> RW_TAC std_ss [Leq_def]
         ++ METIS_TAC [healthy_mono],
         FULL_SIMP_TAC std_ss [Leq_def]]);
--- 561,567 ----
         ++ RW_TAC std_ss [Leq_def]
         ++ RW_TAC posreal_ss [])
!    << [Suff `Leq (trans e) (trans e')` >> RW_TAC std_ss [Leq_def]
         ++ METIS_TAC [healthy_mono],
!        Suff `Leq (trans e) (trans e')` >> RW_TAC std_ss [Leq_def]
         ++ METIS_TAC [healthy_mono],
         FULL_SIMP_TAC std_ss [Leq_def]]);
***************
*** 592,596 ****
     ++ REVERSE CONJ_TAC
     >> (RW_TAC posreal_ss [sup_le, Leq_def]
!        ++ Suff `Leq (l y') z`
         >> RW_TAC posreal_ss [Leq_def]
         ++ FIRST_ASSUM MATCH_MP_TAC
--- 588,592 ----
     ++ REVERSE CONJ_TAC
     >> (RW_TAC posreal_ss [sup_le, Leq_def]
!        ++ Suff `Leq (l y) z`
         >> RW_TAC posreal_ss [Leq_def]
         ++ FIRST_ASSUM MATCH_MP_TAC
***************
*** 955,960 ****
     ``!prog. healthy (wp prog)``,
     Induct
!    << [PROVE_TAC [healthy_wp_assert],
!        PROVE_TAC [healthy_wp_abort],
         PROVE_TAC [healthy_wp_skip],
         PROVE_TAC [healthy_wp_assign],
--- 951,955 ----
     ``!prog. healthy (wp prog)``,
     Induct
!    << [PROVE_TAC [healthy_wp_abort],
         PROVE_TAC [healthy_wp_skip],
         PROVE_TAC [healthy_wp_assign],
***************
*** 1028,1033 ****
  
  val wlp_def = Define
!   `(wlp (Assert p a) = wlp a) /\
!    (wlp Abort = \r. Magic) /\
     (wlp Skip = \r. r) /\
     (wlp (Assign v e) = \r s. r (\w. if w = v then e s else s w)) /\
--- 1023,1027 ----
  
  val wlp_def = Define
!   `(wlp Abort = \r. Magic) /\
     (wlp Skip = \r. r) /\
     (wlp (Assign v e) = \r s. r (\w. if w = v then e s else s w)) /\
***************
*** 1115,1119 ****
          Leq pre mid ==>
          Leq pre (wlp (Assert pre a) post)``,
!    RW_TAC std_ss [wlp_def]
     ++ METIS_TAC [leq_trans]);
  
--- 1109,1113 ----
          Leq pre mid ==>
          Leq pre (wlp (Assert pre a) post)``,
!    RW_TAC std_ss [Assert_def]
     ++ METIS_TAC [leq_trans]);

Update of /cvsroot/hol/hol98/examples/pgcl/doc
In directory sc8-pr-cvs1:/tmp/cvs-serv28769/doc

Modified Files:
	TODO 
Log Message:
The example now works with the current version of HOL4.


Index: TODO
===================================================================
RCS file: /cvsroot/hol/hol98/examples/pgcl/doc/TODO,v
retrieving revision 1.4
retrieving revision 1.5
diff -b -C2 -d -r1.4 -r1.5
*** TODO	24 Sep 2003 14:27:17 -0000	1.4
--- TODO	26 Sep 2003 23:04:10 -0000	1.5
***************
*** 10,14 ****
  
  WP:
- - Remove the Assert command, instead Define `Assert p c = c`
  - Theorems connecting wlp and wp
    - Lemma: wlp prog p = 1 - awp prog (1 - p)      [for 1-bounded p]
--- 10,13 ----
***************
*** 18,22 ****
  
  Temporal Logic:
! - Get it working with positive reals and 1-bounded expectations
  - Verify random walker
  
--- 17,21 ----
  
  Temporal Logic:
! - Get qtlTheory working with positive reals and 1-bounded expectations
  - Verify random walker