Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Message-Id: <9203200232.AA13272@maui.cs.ucla.edu>
To: info-hol@edu.uidaho.cs.ted
Cc: chou@edu.ucla.cs
Subject: On using theorem continuation functions
Date: Thu, 19 Mar 92 18:32:31 PST
From: chou@edu.ucla.cs

Some time ago I asked this question:

> I like to use theorem continuation functions to "capture" assumptions.
> For instance, suppose I want to prove "A ==> B" for some terms A and B.
> Instead of using DISCH_TAC to add A to the set of assumptions and then
> worrying about how to get to A again, I would write something like:
>
> (*)     DISCH_THEN (\asm. rest_of_the_proof)
>
> Thus, A is bound to ML identifier asm and can be referred to easily
> within rest_of_the_proof as a theorem.  The trouble is that such
> tactics are hard to test.  What I usually ended up doing was to
> re-run (*) every time I make a refinement to rest_of_the_proof.
> Is there a better way?

Well, I think I now have a solution, which is described below.  I would
like to hear suggestions and criticisms from more experienced HOL hackers.

First define the following:

==============================================================================
lettype aug_tactic = goal -> (thm list # subgoals) ;;

let aug_thm_tactic_tactic
      (ttacl : thm_tactic -> tactic)
      (ttac : thm_tactic) (g : goal) =
  letref thm = TRUTH
  in
  let sg = ttacl ( \ thm' . thm := thm' ; ttac thm' ) g
  in
  ([thm], sg)
;;

let aug_thm_tactic_thm_tactic
      (ttacl : thm_tactic -> thm_tactic)
      (ttac : thm_tactic) (t : thm) (g : goal) =
  letref thm = TRUTH
  in
  let sg = ttacl ( \ thm' . thm := thm' ; ttac thm' ) t g
  in
  ([thm], sg)
;;

let aug_DISCH_THEN  = aug_thm_tactic_tactic DISCH_THEN
and aug_CHOOSE_THEN = aug_thm_tactic_thm_tactic CHOOSE_THEN
;;

let aug_apply (f : tactic -> *) (aug_tac : aug_tactic) =
  letref thmL = [TRUTH]
  in
  let v = f ( \ g . let (thmL', sg) = aug_tac g
                    in
                    thmL := thmL' ; sg )
  in
  (thmL, v)
;;

let e' = fst o (aug_apply expand)
and f' = fst o (aug_apply expandf)
and f  = expandf
;;
==============================================================================

The following is a sample HOL session:

==============================================================================
#g "(?x. x < 0) ==> (?y. y < 0)" ;;
"(?x. x < 0) ==> (?y. y < 0)"

() : void

#let [t1] = e' (aug_DISCH_THEN (K ALL_TAC)) ;;
OK..
"?y. y < 0"

t1 = . |- ?x. x < 0

#let [t2] = e' (aug_CHOOSE_THEN (K ALL_TAC) t1) ;;
OK..
evaluation failed     Invalid tactic

#let [t2] = f' (aug_CHOOSE_THEN (K ALL_TAC) t1) ;;
OK..
"?y. y < 0"

t2 = . |- x < 0

#e (EXISTS_TAC "x:num") ;;
OK..
"x < 0"

() : void

#e (ACCEPT_TAC t2) ;;
OK..
evaluation failed     Invalid tactic

#f (ACCEPT_TAC t2) ;;
OK..
goal proved
. |- x < 0
. |- ?y. y < 0
. |- ?y. y < 0
|- (?x. x < 0) ==> (?y. y < 0)

Previous subproof:
goal proved
() : void
==============================================================================

The above session can be condensed into one single tactic:

==============================================================================
#b() ; b() ; b() ; b() ;;
"(?x. x < 0) ==> (?y. y < 0)"

() : void

#e ( DISCH_THEN
     ( \ t1 . CHOOSE_THEN
             ( \ t2 . EXISTS_TAC "x:num" THEN ACCEPT_TAC t2 )
             t1 ) ) ;;
####OK..
goal proved
|- (?x. x < 0) ==> (?y. y < 0)

Previous subproof:
goal proved
() : void
==============================================================================

The validity check performed by expand doesn't seem to be very compatible
with this style of doing proofs, so perhaps one should use expandf everywhere.
Or is this a bad idea?

My thanks to Tom Melham for reminding me of the existence of assignable
variables in ML.

- Ching Tsun