Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Message-Id: <9407100909.AA26645@maui.cs.ucla.edu>
To: info-hol@leopard.cs.byu.edu
Subject: "Meta" rewriting
Date: Sun, 10 Jul 94 02:09:38 PDT
From: chou@cs.ucla.edu


Consider the conversion FORALL_AND_CONV.  Wouldn't it be great if
one could prove a single theorem:

(*)     |- !P Q. (!x:'a. P x /\ Q x) = (!x. P x) /\ (!x. Q x)

and then use (*) to "rewrite", say, !n. (n + i < 0) /\ (n + j > 0)
into (!n. n + i < 0) /\ (!n. n + j > 0)?  Unfortunately, as we all
know, this doesn't work.  I find this situation very annoying
because I have some binders in my theories and hence must spend
considerable time to write new conversions whenever I need anything
like FORALL_AND_CONV for my binders.  Furthermore, (*) is much
clearer and more self-explanatory than the mnemonic FORALL_AND_CONV.
So I hacked a little conversion meta_REWR_CONV to do the following:

==============================================================================
- th3;
val it = |- !P_ Q_. (!x:'a. P_ x /\ Q_ x) = (!x. P_ x) /\ (!x. Q_ x) : thm

- meta_REWR_CONV (th3) (--`!n. (n + i < 0) /\ (n + j > 0)`--) ;
val it = |- (!n. n + i < 0 /\ n + j > 0) = (!n. n + i < 0) /\ (!n. n + j > 0) : thm
==============================================================================

The notational convention is that variables with names ending in _
are "meta-variables", i.e., they denote terms of HOL.  More examples
should make this clear:

==============================================================================
(* meta_REWR_CONV as BETA_CONV *)

- th0;
val it = |- !(P_:'a->'b) x. (\y. P_ y) x = P_ x : thm

- meta_REWR_CONV (th0) (--`(\n. 5 - n) (i + j)`--) ;
val it = |- (\n. 5 - n) (i + j) = 5 - (i + j) : thm

(* meta_REWR_CONV as SWAP_FORALL_CONV (which doesn't exist!) *)

- th1;
val it = |- !(P_:'a#'b->bool). (!x y. P_ (x,y)) = (!y x. P_ (x,y)) : thm

- meta_REWR_CONV (th1) (--`!m n. m + n < k`--) ;
val it = |- (!m n. m + n < k) = (!n m. m + n < k) : thm

- ONCE_DEPTH_CONV (meta_REWR_CONV (th1)) (--`!k. k>0 \/ (!m n. m + n < k)`--) ;
val it = |- (!k. k > 0 \/ (!m n. m + n < k)) = (!k. k > 0 \/ (!n m. m + n < k)) : thm

(* meta_REWR_CONV as LEFT_AND_FORALL_CONV and its reverse *)

- th2;
val it = |- !P_ Q_. (!x:'a. P_ x) /\ Q_ = (!x. P_ x /\ Q_) : thm

- meta_REWR_CONV (th2) (--`(!a. f(a:'a) < 0) /\ (g(b:'b) > 0)`--) ;
val it = |- (!a. f a < 0) /\ g b > 0 = (!a. f a < 0 /\ g b > 0) : thm

- meta_REWR_CONV (th2) (--`(!a. f(a:'a) < 0) /\ (g(a:'a) > 0)`--) ;
val it = |- (!a. f a < 0) /\ g a > 0 = (!a'. f a' < 0 /\ g a > 0) : thm

- meta_REWR_CONV (GSYM th2) (--`!a. (f(a:'a) < 0) /\ (g(b:'b) > 0)`--) ;
val it = |- (!a. f a < 0 /\ g b > 0) = (!a. f a < 0) /\ g b > 0 : thm

- meta_REWR_CONV (GSYM th2) (--`!a'. (f(a':'a) < 0) /\ (g(a:'a) > 0)`--) ;
val it = |- (!a'. f a' < 0 /\ g a > 0) = (!a'. f a' < 0) /\ g a > 0 : thm

(* meta_REWR_CONV as FORALL_AND_CONV and its reverse *)

- th3;
val it = |- !P_ Q_. (!x:'a. P_ x /\ Q_ x) = (!x. P_ x) /\ (!x. Q_ x) : thm

- meta_REWR_CONV (th3) (--`!n. (n + i < 0) /\ (n + j > 0)`--) ;
val it = |- (!n. n + i < 0 /\ n + j > 0) = (!n. n + i < 0) /\ (!n. n + j > 0) : thm

- TOP_DEPTH_CONV (meta_REWR_CONV (th3))
= (--`!i. (i = 0) \/ (!k n. (n + i < 0) /\ (n + k > 0))`--) ;
val it =
  |- (!i. (i = 0) \/ (!k n. n + i < 0 /\ n + k > 0)) =
     (!i. (i = 0) \/ (!k n. n + i < 0) /\ (!k n. n + k > 0)) : thm

- meta_REWR_CONV (th3) (--`!n:'b. (k + i < 0) /\ (m + j > 0)`--) ;
val it = |- (!n. k + i < 0 /\ m + j > 0) = (!n. k + i < 0) /\ (!n. m + j > 0) : thm

- meta_REWR_CONV (GSYM th3) (--`(!n. (n + i < 0)) /\ (!n. (n + j > 0))`--) ;
val it = |- (!n. n + i < 0) /\ (!n. n + j > 0) = (!n. n + i < 0 /\ n + j > 0) : thm

- meta_REWR_CONV (GSYM th3) (--`(!n. (n + i < 0)) /\ (!m. (m + j > 0))`--) ;
val it = |- (!n. n + i < 0) /\ (!m. m + j > 0) = (!n. n + i < 0 /\ n + j > 0) : thm

- meta_REWR_CONV (GSYM th3) (--`(!n:'b. (k + i < 0)) /\ (!m:'b. (l + j > 0))`--) ;
val it = |- (!n. k + i < 0) /\ (!m. l + j > 0) = (!n. k + i < 0 /\ l + j > 0) : thm
==============================================================================

The codes of meta_REWR_CONV are given below.

==============================================================================
val meta_OBJ_DEF = new_definition ("meta_OBJ_DEF",
(--`
  meta_OBJ (x:'a) = x
`--)) ;

val meta_APP0_DEF = new_definition ("meta_APP0_DEF",
(--`
  meta_APP0 (f:'b) = f
`--)) ;

val meta_APP1_DEF = new_definition ("meta_APP1_DEF",
(--`
  meta_APP1 (f:'a->'b) (x:'a) = f(x)
`--)) ;

fun failwith (f) (m) =
  raise HOL_ERR {origin_structure = "Meta",
                 origin_function = f, message = m} ;

val PBETA_CONV = Pair_basic.PBETA_CONV ;
val mk_pabs = Pair_syn.mk_pabs ;

fun last [x] = x
  | last (_::t) = last (t) ;

val var_name = #Name o dest_var ;

val is_meta = eq "_" o last o explode o var_name ;

fun is_meta_var (tm) = (is_var tm) andalso     (is_meta tm) ;
fun is_obj_var  (tm) = (is_var tm) andalso not (is_meta tm) ;

val meta_OBJ_ELIM_CONV = REWR_CONV (meta_OBJ_DEF) ;
val meta_APP0_ELIM_CONV = REWR_CONV (meta_APP0_DEF) ;
val meta_APP1_ELIM_CONV = REWR_CONV (meta_APP1_DEF) ;
val meta_OBJ_INTR_CONV = REWR_CONV (GSYM meta_OBJ_DEF) ;
val meta_APP0_INTR_CONV = REWR_CONV (GSYM meta_APP0_DEF) ;
val meta_APP1_INTR_CONV = REWR_CONV (GSYM meta_APP1_DEF) ;

val meta_ELIM_CONV =
  (ONCE_DEPTH_CONV o FIRST_CONV)
  [ meta_OBJ_ELIM_CONV
  , meta_APP0_ELIM_CONV
  , meta_APP1_ELIM_CONV THENC TRY_CONV PBETA_CONV
  ] ;

fun meta_INTR_CONV' (tm) =
  ( if (is_const tm) orelse (is_obj_var tm) then
      meta_OBJ_INTR_CONV
    else
    if (is_abs tm) then
      ABS_CONV meta_OBJ_ELIM_CONV THENC meta_OBJ_INTR_CONV
    else
    if (is_comb tm) then
    ( if (is_meta_var (rator tm)) then
        RAND_CONV meta_OBJ_ELIM_CONV THENC meta_APP1_INTR_CONV
      else
      if (is_meta_var (rand tm)) then
        RAND_CONV meta_APP0_INTR_CONV
      else
       RATOR_CONV meta_OBJ_ELIM_CONV THENC
        RAND_CONV meta_OBJ_ELIM_CONV THENC meta_OBJ_INTR_CONV )
    else
      NO_CONV
  ) (tm) ;

fun BOTTOM_UP_CONV (conv : conv) tm =
  ( SUB_CONV (BOTTOM_UP_CONV conv) THENC TRY_CONV conv ) tm ;

val meta_INTR_CONV = BOTTOM_UP_CONV (meta_INTR_CONV') ;

val is_meta_OBJ  = can (match_term (--`meta_OBJ  (x:'a)`--)) ;
val is_meta_APP0 = can (match_term (--`meta_APP0 (f:'b)`--)) ;
val is_meta_APP1 = can (match_term (--`meta_APP1 (f:'a->'b) (x:'a)`--)) ;

fun meta_MATCH (src) (des) =
  if (is_meta_OBJ src) then
    ((--`meta_OBJ (^des)`--), [])
  else
  if (is_meta_APP0 src) then
    ((--`meta_APP0 (^des)`--), [])
  else
  if (is_meta_APP1 src) then
  ( let
      val marg = rand (src) ;
      val mabs = mk_pabs {Bvar=marg, Body=des} ;
    in
      ((--`meta_APP1 (^mabs) (^marg)`--), [])
    end )
  else
  if (is_comb src) then
  ( let
      val {Rator=srcL, Rand=srcR} = dest_comb (src) ;
      val {Rator=desL, Rand=desR} = dest_comb (des) ;
      val (midL, nnlL) = meta_MATCH (srcL) (desL) ;
      val (midR, nnlR) = meta_MATCH (srcR) (desR) ;
    in
      (mk_comb {Rator=midL, Rand=midR}, union (nnlL) (nnlR))
    end )
  else
  if (is_abs src) then
  ( let
      val src' = inst (match_type (type_of src) (type_of des)) (src) ;
      val {Bvar=srcV, Body=srcB} = dest_abs (src') ;
      val {Bvar=desV, Body=desB} = dest_abs (des) ;
      val (srcN, desN) = (var_name srcV, var_name desV) ;
      val (nn, srcB') =
        if (srcN = desN) then ([], srcB)
        else ([(srcN, desN)], subst [{redex=srcV, residue=desV}] (srcB)) ;
      val (mid, nnl) = meta_MATCH (srcB') (desB) ;
    in
      (mk_abs {Bvar=desV, Body=mid}, union (nn) (nnl))
    end )
  else
    failwith "meta_MATCH" "This can't possibly happen!" ;

fun meta_RENAME_CONV (nnl) (tm) =
  ( if (is_meta_OBJ tm)  orelse
       (is_meta_APP0 tm) orelse
       (is_meta_APP1 tm) then
      ALL_CONV
    else
    if (is_comb tm) then
      RATOR_CONV (meta_RENAME_CONV nnl) THENC
       RAND_CONV (meta_RENAME_CONV nnl)
    else
    if (is_abs tm) then
      ( let
          val {Name=nm, Ty=ty} = dest_var (bvar tm)
        in
          case (assoc1 nm nnl)
          of NONE          => ALL_CONV
           | SOME (_, nm') => ALPHA_CONV (mk_var {Name=nm', Ty=ty})
        end
      ) THENC ABS_CONV (meta_RENAME_CONV nnl)
    else
      failwith "meta_MATCH" "This can't possibly happen!"
  ) (tm) ;

fun meta_REWR_CONV (th) =
  let
    val th' = CONV_RULE (RAND2_CONV meta_INTR_CONV) (SPEC_ALL th) ;
    val rew = REWR_CONV (th') ;
    val pat = lhs (concl th') ;
  in
  ( fn (tm) =>
    let
      val (tm', nnl) = meta_MATCH (pat) (tm) ;
      val eq1 = (SYM o meta_ELIM_CONV) (tm') ;
      val eq2 = (rew THENC meta_RENAME_CONV nnl THENC meta_ELIM_CONV) (tm') ;
    in
      TRANS (eq1) (eq2)
    end )
  end ;
==============================================================================

All comments are welcomed!

Cheers,
- Ching Tsun