(** rewr.tac - controlled rewriting - procedures **)
(* using HOL-type conversionals *)
datatype rep = Unc | Rep of thm ;
(* a eq-conversion is given a certified term ct and produces a theorem
which is ct == ct' ;
a eq-transformation is given a theorem (a == b) and transforms it to
the theorem (a == c) ;
in either case the resulting theorem is prefixed by Rep ; if no
change is made then Unc is returned *)
(* Tr2 : thm -> cterm, from (a == b), gives b *)
fun Tr2 th =
let val (_, r) = dest_comb (cprop_of th)
in r end ;
(* rewr_tt : thm -> thm -> rep
from a theorem (A == B), gives the eq-transformation
(X == A') --> (X == B'), where A' and B' are instantiations of A and B *)
(* do we need to fix this so as to ensure that Vars in the thing to be
rewritten do not get instantiated? *)
fun rewr_tt rewrth th = Rep ([th, rewrth] MRS transitive_thm)
handle THM _ => Unc ;
infix THENcr ;
infix THENtt ;
(* conv2tt : (cterm -> rep) -> thm -> rep
takes eq-conversion to eq-transformation *)
fun conv2tt c th =
case c (Tr2 th) of Unc => Unc
| Rep rth => Rep ([th, rth] MRS transitive_thm) ;
(* tt2conv : (thm -> 'a) -> cterm -> 'a
takes eq-transformation to eq-conversion *)
fun tt2conv tt = tt o reflexive ;
(* THENtt : (thm -> rep) * (thm -> rep) -> thm -> rep
sequencing two eq-transformations *)
fun (tt1 THENtt tt2) th =
case tt1 th of Unc => tt2 th
| Rep rth1 =>
case tt2 rth1 of Unc => Rep rth1
| Rep rth2 => Rep rth2 ;
(* THENcr : (cterm -> rep) * (cterm -> rep) -> cterm -> rep
sequencing two eq-conversions - forward proof only *)
fun (c1 THENcr c2) ct =
case c1 ct of Unc => c2 ct
| Rep rth1 =>
case c2 (Tr2 rth1) of Unc => Rep rth1
| Rep rth2 => Rep ([rth1, rth2] MRS transitive_thm) ;
(* rep2th : rep -> thm, from rep gives corresponding theorem *)
fun rep2th Unc = reflexive_thm | rep2th (Rep rth) = rth ;
(* val SUBcr = fn : (cterm -> rep) -> cterm -> rep
applies eq-conversion to immediate subterms *)
fun SUBcr c ct =
case term_of ct of
_ $ _ =>
let val (cl, cr) = dest_comb ct
in case (c cl, c cr) of (Unc, Unc) => Unc
| (Unc, rrep) => Rep (combination (reflexive cl) (rep2th rrep))
| (lrep, Unc) => Rep (combination (rep2th lrep) (reflexive cr))
| (lrep, rrep) => Rep (combination (rep2th lrep) (rep2th rrep)) end
| _ => Unc ;
(* SUBtt : (thm -> rep) -> thm -> rep
applies eq-transformation to immediate subterms *)
fun SUBtt tt th = SUBcr (tt o reflexive) (Tr2 th) ;
(* TRYREPtt : (thm -> rep) -> thm -> thm
repeats eq-transformation zero or more times until it fails,
doesn't fail itself *)
fun TRYREPtt tt th =
case tt th of Unc => th
| Rep rth => TRYREPtt tt rth ;
(* REPtt : (thm -> rep) -> thm -> rep
repeats eq-transformation one or more times until it fails *)
fun REPtt tt th =
case tt th of Unc => Unc
| Rep rth => Rep (TRYREPtt tt rth) ;
(* TDtt, BUtt : (thm -> rep) -> thm -> rep
applies eq-transformation wherever possible, using top-down or bottom-up
search strategy *)
fun TDtt tt th = (REPtt tt THENtt SUBtt (TDtt tt)) th ;
fun BUtt tt th = (SUBtt (BUtt tt) THENtt REPtt tt) th ;
(* rewr_rule : (thm -> rep) -> thm -> thm
applies eq-transformation tt to th, performing forward proof *)
fun rewr_rule tt th =
case (tt o reflexive o cprop_of) th of
Unc => th
| Rep rth => equal_elim rth th ;
(* test and example, using FOL
val rth = List.nth (disj_simps, 4) RS iff_reflection ;
val tt = (rewr_tt rth) ;
val ttt = TDtt tt ;
val btt = BUtt tt ;
val rtt = REPtt tt ;
val stt = SUBtt tt ;
val [p] = goal thy "P | P ==> X";
val [p] = goal thy "P | P <-> (Q | Q) ==> X";
val [p] = goal thy "P | P <-> (Q | Q) | (R | R) & (S | S) ==> X";
rewr_rule tt p ;
rewr_rule ttt p ;
rewr_rule btt p ;
rewr_rule stt p ;
*)
(* rewr_tac : (thm -> rep) -> tactic
applies eq-transformation tt to st, makes a tactic *)
(* still need to apply to subgoals only *)
fun rewr_tac tt st =
case (tt o reflexive o cprop_of) st of
Unc => Seq.single st (* or Seq.empty, for tactic to fail *)
| Rep rth => Seq.single (equal_elim rth st) ;
(* test and example
goal thy "P | P";
goal thy "P | P <-> (Q | Q) | (R | R) & (S | S)";
goal thy "P | P <-> (Q | Q)";
by (rewr_tac ttt) ;
chop() ; by (rewr_tac btt) ;
chop() ; by (rewr_tac stt) ;
*)