[Hol-checkins] CVS: hol98/examples/dev FactScript.sml,1.6,1.7 README,1.4,1.5 compile.sml,1.3,1.4

SourceForge Headquarters 225 Broadway Suite 1600 San Diego, CA 92101 +1 (858) 454-5900

Update of /cvsroot/hol/hol98/examples/dev
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv4096

Modified Files:
	FactScript.sml README compile.sml 
Log Message:
Revision of yesterday's version to make refinements more analogous
to conversions. I've also changed some names around (Sorry).

See README for latest stuff.

Main changes are:

 1. Refine renamed to REFINE and now doesn't "depth" scan the circuit.
    The scanning is done explicitly by an operator DEPTHR (which
    is analogous to DEPTH_CONV).

 2. Have added refinement combining operators THENR, ORELSER.

 3. Lib renamed to LIB_REFINE.

 4. ATMfn renamed to ATM_REFINE.

An example (see FactScript.sml) is:

 REFINE
  (DEPTHR(LIB_REFINE[FactIter_dev])
    THENR DEPTHR(LIB_REFINE[SUBS [MultThm] Mult_dev])
    THENR DEPTHR(LIB_REFINE[MultIter_dev])
    THENR DEPTHR ATM_REFINE)
  Fact_dev;

I hope this is converging! I should take a rest and do some more PSL
proofs now.

Index: FactScript.sml
===================================================================
RCS file: /cvsroot/hol/hol98/examples/dev/FactScript.sml,v
retrieving revision 1.6
retrieving revision 1.7
diff -b -C2 -d -r1.6 -r1.7
*** FactScript.sml	19 Jan 2005 10:27:40 -0000	1.6
--- FactScript.sml	19 Jan 2005 21:10:05 -0000	1.7
***************
*** 15,18 ****
--- 15,20 ----
  open arithmeticTheory pairLib pairTheory PairRules combinTheory
       composeTheory compileTheory compile;
+ infixr 3 THENR;
+ infixr 3 ORELSER;
  quietdec := false;
  *)
***************
*** 28,31 ****
--- 30,35 ----
  open arithmeticTheory pairLib pairTheory PairRules combinTheory 
       composeTheory compile;
+ infixr 3 THENR;
+ infixr 3 ORELSER;

  (*****************************************************************************)
***************
*** 90,94 ****
  (*****************************************************************************)
  val FactIter1_dev =
!  Refine (Lib[SUBS [MultThm] Mult_dev]) FactIter_dev;

  (*****************************************************************************)
--- 94,98 ----
  (*****************************************************************************)
  val FactIter1_dev =
!  REFINE (DEPTHR(LIB_REFINE[SUBS [MultThm] Mult_dev])) FactIter_dev;

  (*****************************************************************************)
***************
*** 96,100 ****
  (*****************************************************************************)
  val FactIter2_dev =
!  Refine (Lib[MultIter_dev]) FactIter1_dev;

  (*****************************************************************************)
--- 100,104 ----
  (*****************************************************************************)
  val FactIter2_dev =
!  REFINE (DEPTHR(LIB_REFINE[MultIter_dev])) FactIter1_dev;

  (*****************************************************************************)
***************
*** 131,149 ****
  (*****************************************************************************)
  val Fact1_dev =
!  Refine (Lib[FactIter2_dev]) Fact_dev;

  (*****************************************************************************)
! (* Refine all remaining DEVs to ATM                                          *)
  (*****************************************************************************)
  val Fact2_dev =
!  Refine ATMfn Fact1_dev;

  (*****************************************************************************)
! (* Create implementation of FACT (HOL's built-in factorial function)         *)
  (*****************************************************************************)
  val FACT_dev =
   save_thm
    ("FACT_dev",
!    REWRITE_RULE [FactThm] Fact2_dev);

--- 135,164 ----
  (*****************************************************************************)
  val Fact1_dev =
!  REFINE (DEPTHR(LIB_REFINE[FactIter2_dev])) Fact_dev;

  (*****************************************************************************)
! (* REFINE all remaining DEVs to ATM                                          *)
  (*****************************************************************************)
  val Fact2_dev =
!  REFINE (DEPTHR ATM_REFINE) Fact1_dev;

  (*****************************************************************************)
! (* Alternative derivation using refinement combining combinators             *)
! (*****************************************************************************)
! val Fact3_dev =
!  REFINE
!   (DEPTHR(LIB_REFINE[FactIter_dev])
!     THENR DEPTHR(LIB_REFINE[SUBS [MultThm] Mult_dev])
!     THENR DEPTHR(LIB_REFINE[MultIter_dev])
!     THENR DEPTHR ATM_REFINE)
!   Fact_dev;
! 
! (*****************************************************************************)
! (* Finally, create implementation of FACT (HOL's native factorial function)  *)
  (*****************************************************************************)
  val FACT_dev =
   save_thm
    ("FACT_dev",
!    REWRITE_RULE [FactThm] Fact3_dev);

Index: README
===================================================================
RCS file: /cvsroot/hol/hol98/examples/dev/README,v
retrieving revision 1.4
retrieving revision 1.5
diff -b -C2 -d -r1.4 -r1.5
*** README	18 Jan 2005 17:44:53 -0000	1.4
--- README	19 Jan 2005 21:10:05 -0000	1.5
***************
*** 9,12 ****
--- 9,13 ----
  == [17.01.05: MJCG installed hwDefine and improved examples from KXS]        ==
  == [18.01.05: MJCG added Refine and revised FactScript.sml]                  ==
+ == [19.01.05: MJCG changed to use refinement combinators]                    ==
  ===============================================================================

***************
*** 23,28 ****
          set_fixity "||" (Infixl 650); overload_on ("||", ``PAR``)

! The main user-level functions are hwDefine and Refine,
! for creating hardware and refinement.

  hwDefine : term frag list -> thm * thm * thm
--- 24,29 ----
          set_fixity "||" (Infixl 650); overload_on ("||", ``PAR``)

! The main user-level functions are hwDefine and REFINE,
! for creating hardware and then refining it.

  hwDefine : term frag list -> thm * thm * thm
***************
*** 52,83 ****
  See FactScript.sml for examples.

! Refine: (term -> thm) -> thm -> thm
  -----------------------------------

! The first argument of Refine is a "refine function", refinefn say,
! which maps a term ``DEV g`` to a theorem |- DEV h ===> DEV g,
! where |= P ===> Q = !x. P x ==> Q x. 

! "Refine refinefn (|- <circuit> ===> Dev f)" recursively scans
! <circuit> replacing ``DEV g`` by ``DEV h`` (where refinefn applied to
! ``DEV g`` yields |- DEV h ===> DEV h) and returns a theorem

!    |- <circuit'> ===> Dev f

! where <circuit'> is the result of the scan.

  See FactScript.sml for examples.

- Two useful refine functions are ATMfn and Lib

! ATMfn : term -> thm
! ------------------

  This maps ``DEV f`` to |- ATM f ===> DEV f

- Lib : thm list -> term -> thm
- -----------------------------

! Lib                                                                       *)
   [|- <circuit> ===> DEV f1,
    |- <circuit> ===> DEV f2
--- 53,102 ----
  See FactScript.sml for examples.

! 
! REFINE: (term -> thm) -> thm -> thm
  -----------------------------------

! The first argument of REFINE is a "refine function", refine say,
! which maps a term representing a circuit, <circuit> say, to a theorem

!    |- <circuit'> ===> <circuit>

! where ``===>`` is defined by:

!    |- P ===> Q  =  !x. P x ==> Q x.
! 
! and <circuit'> is a term representing the result of refining <circuit>
! with the function refine.
! 
! Evaluating
! 
!    REFINE refine (|- <circuit> ===> Dev f)
! 
! applies refine to <circuit> to get
! 
!    |- <circuit'> ===> <circuit>
! 
! and then uses transitivity of ===> (DEV_IMP_TRANS) to deduce:
! 
!    |- <circuit'> ===> Dev f

  See FactScript.sml for examples.

! Two useful refine functions are ATM_REFINE and LIB_REFINE.
! 
! 
! ATM_REFINE : term -> thm
! ------------------------

  This maps ``DEV f`` to |- ATM f ===> DEV f

! LIB_REFINE : thm list -> term -> thm
! ------------------------------------
! 
! Evaluating
! 
!    LIB_REFINE
      [|- <circuit> ===> DEV f1,
       |- <circuit> ===> DEV f2
***************
*** 86,91 ****
   ``DEV fi``

! returns the first theorem <circuit> ===> DEV fi that it finds in the
! supplied list (i.e. library)

  *******************************************************************************
--- 105,169 ----
      ``DEV fi``

! returns the first theorem |- <circuit> ===> DEV fi that it finds in the
! supplied list (i.e. the supplied library).
! 
! Refinement functions (analogously to conversions and tactics) can be combined using
! combinators THENR, ORELSER, DEPTHR. See FactScript.sml for examples.
! 
! 
! THENR : (term -> thm) * (term -> thm) -> (term -> thm)
! ------------------------------------------------------
! 
! Combines refinements sequentially.
! 
! 
! ORELSER : (term -> thm) * (term -> thm) -> (term -> thm)
! --------------------------------------------------------
! 
! Tries first refinement and if that fails tries the second one.
! 
! 
! DEPTHR : (term -> thm) -> (term -> thm)
! ---------------------------------------------
! 
! Scans through a term representing a circuit applying the supplied
! refinement function to each subterm of the form ``DEV f`` and 
! either generating
! 
!  |- DEV g ===> DEVf
! 
! if the refinement function returns this, or, if the refinement
! function fails:
! 
!  |- DEV f ===> DEV f
! 
! A refined circuit is then build up using the "monotonicity" theorems:
! 
!   SEQ_DEV_IMP =
!    |- !P1 P2 Q1 Q2.
!        P1 ===> Q1 /\ P2 ===> Q2
!        ==>
!        (SEQ P1 P2 ===> SEQ Q1 Q2)
! 
!   PAR_DEV_IMP =
!    |- !P1 P2 Q1 Q2.
!        P1 ===> Q1 /\ P2 ===> Q2
!        ==>
!        (PAR P1 P2 ===> PAR Q1 Q2)
! 
!   ITE_DEV_IMP =
!    |- !P1 P2 P3 Q1 Q2 Q3.
!        P1 ===> Q1 /\ P2 ===> Q2 /\ P3 ===> Q3
!        ==>
!        (ITE P1 P2 P3 ===> ITE Q1 Q2 Q3)
! 
!   REC_DEV_IMP =
!    |- !P1 P2 P3 Q1 Q2 Q3.
!        P1 ===> Q1 /\ P2 ===> Q2 /\ P3 ===> Q3
!        ==>
!        (REC P1 P2 P3 ===> REC Q1 Q2 Q3)
! 
! Note that "DEPTHR refine" should never fail.
! 

  *******************************************************************************

Index: compile.sml
===================================================================
RCS file: /cvsroot/hol/hol98/examples/dev/compile.sml,v
retrieving revision 1.3
retrieving revision 1.4
diff -b -C2 -d -r1.3 -r1.4
*** compile.sml	18 Jan 2005 17:44:53 -0000	1.3
--- compile.sml	19 Jan 2005 21:10:05 -0000	1.4
***************
*** 45,48 ****
--- 45,59 ----

  (*****************************************************************************)
+ (* Destruct ``d1 ===> d2`` into (``d1``,``d2``)                              *)
+ (*****************************************************************************)
+ fun dest_dev_imp tm = 
+  if is_comb tm
+      andalso is_comb(rator tm) 
+      andalso is_const(rator(rator tm))
+      andalso (fst(dest_const(rator(rator tm))) = "===>")
+   then (rand(rator tm), rand tm)
+   else raise ERR "dest_dev_imp" "attempt to dest a non-DEV";
+ 
+ (*****************************************************************************)
  (* An expression is just a HOL term built using expressions defined earlier  *)
  (* in a program (see description of programs below) and Seq, Par,            *)
***************
*** 621,636 ****
  (* Refine a device to a combinational circuit (i.e. an ATM):                 *)
  (*                                                                           *)
! (* ATMfn ``DEV f``  =  |- ATM f ===> DEV f : thm                             *)
  (*                                                                           *)
  (*****************************************************************************)
! fun ATMfn tm =
   if not(is_comb tm 
           andalso is_const(rator tm)
           andalso (fst(dest_const(rator tm)) = "DEV"))
!   then raise ERR "ATMfn" "argument not a DEV"
    else ISPEC (rand tm) ATM_INTRO;

  (*****************************************************************************)
! (* Lib                                                                       *)
  (*  [|- <circuit> ===> DEV f1,                                               *)
  (*   |- <circuit> ===> DEV f2                                                *)
--- 632,647 ----
  (* Refine a device to a combinational circuit (i.e. an ATM):                 *)
  (*                                                                           *)
! (* ATM_REFINE ``DEV f``  =  |- ATM f ===> DEV f : thm                      *)
  (*                                                                           *)
  (*****************************************************************************)
! fun ATM_REFINE tm =
   if not(is_comb tm 
           andalso is_const(rator tm)
           andalso (fst(dest_const(rator tm)) = "DEV"))
!   then raise ERR "ATM_REFINE" "argument not a DEV"
    else ISPEC (rand tm) ATM_INTRO;

  (*****************************************************************************)
! (* LIB_REFINE                                                                *)
  (*  [|- <circuit> ===> DEV f1,                                               *)
  (*   |- <circuit> ===> DEV f2                                                *)
***************
*** 642,659 ****
  (* that it finds in the supplied list (i.e. library)                         *)
  (*****************************************************************************)
! fun Lib lib tm =
   if is_DEV tm
    then
     case
       List.find 
!       (aconv tm o rand o concl o SPEC_ALL)
        lib
     of SOME th => th
      | NONE    => ISPEC tm DEV_IMP_REFL
!   else raise ERR "Lib" "attempt to lookup a non-DEV";

  (*****************************************************************************)
! (* RefineExp refinefn tm scans through a combinatory expression tm built     *)
! (* from ATM, SEQ, PAR, ITE, REC and DEV and applies the refinefn to all      *)
  (* arguments of DEV using                                                    *)
  (*                                                                           *)
--- 653,670 ----
  (* that it finds in the supplied list (i.e. library)                         *)
  (*****************************************************************************)
! fun LIB_REFINE lib tm =
   if is_DEV tm
    then
     case
       List.find 
!       (aconv tm o snd o dest_dev_imp o concl o SPEC_ALL)
        lib
     of SOME th => th
      | NONE    => ISPEC tm DEV_IMP_REFL
!   else raise ERR "LIB_REFINE" "attempt to lookup a non-DEV";

  (*****************************************************************************)
! (* DEPTHR refine tm scans through a combinatory expression tm built          *)
! (* from ATM, SEQ, PAR, ITE, REC and DEV and applies the refine to all        *)
  (* arguments of DEV using                                                    *)
  (*                                                                           *)
***************
*** 674,682 ****
  (*  |- tm' ===> tm                                                           *)
  (*                                                                           *)
! (* (if refinefn fails, then no action is taken, i.e. |- tm ===> tm used)     *)
  (*****************************************************************************)
! fun RefineExp refinefn tm =
   if is_DEV tm
!   then (refinefn tm
          handle _ => ISPEC tm DEV_IMP_REFL)
   else if is_ATM tm
--- 685,693 ----
  (*  |- tm' ===> tm                                                           *)
  (*                                                                           *)
! (* (if refine fails, then no action is taken, i.e. |- tm ===> tm used)       *)
  (*****************************************************************************)
! fun DEPTHR refine tm =
   if is_DEV tm
!   then (refine tm
          handle _ => ISPEC tm DEV_IMP_REFL)
   else if is_ATM tm
***************
*** 685,690 ****
    then
     let val (tm1,tm2) = dest_SEQ tm
!        val th1 = RefineExp refinefn tm1
!        val th2 = RefineExp refinefn tm2 
     in
      MATCH_MP SEQ_DEV_IMP (CONJ th1 th2)
--- 696,701 ----
    then
     let val (tm1,tm2) = dest_SEQ tm
!        val th1 = DEPTHR refine tm1
!        val th2 = DEPTHR refine tm2 
     in
      MATCH_MP SEQ_DEV_IMP (CONJ th1 th2)
***************
*** 693,698 ****
    then
     let val (tm1,tm2) = dest_PAR tm
!        val th1 = RefineExp refinefn tm1
!        val th2 = RefineExp refinefn tm2 
     in
      MATCH_MP PAR_DEV_IMP (CONJ th1 th2)
--- 704,709 ----
    then
     let val (tm1,tm2) = dest_PAR tm
!        val th1 = DEPTHR refine tm1
!        val th2 = DEPTHR refine tm2 
     in
      MATCH_MP PAR_DEV_IMP (CONJ th1 th2)
***************
*** 701,707 ****
    then
     let val (tm1,tm2,tm3) = dest_ITE tm
!        val th1 = RefineExp refinefn tm1
!        val th2 = RefineExp refinefn tm2 
!        val th3 = RefineExp refinefn tm3 
     in
      MATCH_MP ITE_DEV_IMP (LIST_CONJ[th1,th2,th3])
--- 712,718 ----
    then
     let val (tm1,tm2,tm3) = dest_ITE tm
!        val th1 = DEPTHR refine tm1
!        val th2 = DEPTHR refine tm2 
!        val th3 = DEPTHR refine tm3 
     in
      MATCH_MP ITE_DEV_IMP (LIST_CONJ[th1,th2,th3])
***************
*** 710,724 ****
    then
     let val (tm1,tm2,tm3) = dest_REC tm
!        val th1 = RefineExp refinefn tm1
!        val th2 = RefineExp refinefn tm2 
!        val th3 = RefineExp refinefn tm3 
     in
      MATCH_MP REC_DEV_IMP (LIST_CONJ[th1,th2,th3])
     end
   else (print_term tm; print"\n";
!        raise ERR "RefineExp" "bad argument");

  (*****************************************************************************)
! (* Refine refinefn (|- <circuit> ===> Dev f) uses RefineExp to generate      *)
  (*                                                                           *)
  (*  |- <circuit'> ===> <circuit>                                             *)
--- 721,736 ----
    then
     let val (tm1,tm2,tm3) = dest_REC tm
!        val th1 = DEPTHR refine tm1
!        val th2 = DEPTHR refine tm2 
!        val th3 = DEPTHR refine tm3 
     in
      MATCH_MP REC_DEV_IMP (LIST_CONJ[th1,th2,th3])
     end
   else (print_term tm; print"\n";
!        raise ERR "DEPTHR" "bad argument");

  (*****************************************************************************)
! (* REFINE refine (|- <circuit> ===> Dev f) applies refine to <circuit>       *)
! (* to generate                                                               *)
  (*                                                                           *)
  (*  |- <circuit'> ===> <circuit>                                             *)
***************
*** 728,736 ****
  (*  |- <circuit'> ===> Dev f                                                 *)
  (*****************************************************************************)
! fun Refine refinefn th =
   MATCH_MP 
    DEV_IMP_TRANS 
!   (CONJ (RefineExp refinefn (rand(rator(concl th)))) th)
!  handle _ => raise ERR "Refine" "bad argument";

--- 740,809 ----
  (*  |- <circuit'> ===> Dev f                                                 *)
  (*****************************************************************************)
! fun REFINE refine th =
   MATCH_MP 
    DEV_IMP_TRANS 
!   (CONJ (refine (fst(dest_dev_imp(concl th)))) th)
!  handle _ => raise ERR "REFINE" "bad argument";
! 
! (*****************************************************************************)
! (* Some refinement combinators made by tweaking code from Conv.sml           *)
! (* N.B. Not yet working -- needs rethinking a bit                            *)
! (*****************************************************************************)
! 
! (* ----------------------------------------------------------------------
!     Refinement that always succeeds, but does nothing.
!     Indicates this by raising the UNCHANGEDR exception.
!    ---------------------------------------------------------------------- *)
! 
! exception UNCHANGED_REFINE;
! 
! fun ALL_REFINE t = raise UNCHANGED_REFINE;
! 
! (* ----------------------------------------------------------------------
!     Apply two conversions in succession;  fail if either does.  Handle
!     UNCHANGED_REFINE appropriately.
!    ---------------------------------------------------------------------- *)
! infixr 3 THENR;
! 
! fun (refine1 THENR refine2) tm = 
!  let val th1 = refine1 tm
!  in
!   MATCH_MP DEV_IMP_TRANS (CONJ (refine2 (fst(dest_dev_imp(concl th1)))) th1)
!   handle UNCHANGED_REFINE => th1
!  end 
!  handle UNCHANGED_REFINE => refine2 tm;
! 
! (* ----------------------------------------------------------------------
!     Apply refine1;  if it raises a HOL_ERR then apply refine2. Note that
!     interrupts and other exceptions (including UNCHANGED_REFINE) will sail 
!     on through.
!    ---------------------------------------------------------------------- *)
! infixr 3 ORELSER;
! 
! fun (refine1 ORELSER refine2) tm = 
!  refine1 tm handle HOL_ERR _ => refine2 tm;
! 
! (* Not sure if stuff below is needed, and it's not tested, 
!    so is commented out for now
! 
! (*---------------------------------------------------------------------------
!  * Cause the refinement to fail if it does not change its input.
!  *---------------------------------------------------------------------------*)
! fun CHANGED_REFINE refine tm =
!    let val th = refine tm
!            handle UNCHANGED_REFINE 
!            => raise ERR "CHANGED_REFINE" "Input term unchanged"
!        val (ante,conc) = dest_dev_imp(concl th)
!    in if aconv ante conc then raise ERR "CHANGED_REFINE" "Input term unchanged"
!       else th
!    end;
! 
! (*---------------------------------------------------------------------------
!  * Apply a conversion zero or more times.
!  *---------------------------------------------------------------------------*)
! fun REPEATR refine tm =
!     ((CHANGED_REFINE refine THENC (REPEATR refine)) ORELSER ALL_REFINE) tm;
!  
! *)