(** rep.tac - Replacement predicate - procedures **)
exception NotMono of term ;
(* oprepthm : term -> thm, where term is a single operator, finds
the rule analogous to rep_or *)
fun oprepthm (Const ("LPF.Not", _)) = rep_not
| oprepthm (Const ("LPF.op |", _)) = rep_or
| oprepthm (Const ("LPF.op &", _)) = rep_and
| oprepthm (Const ("LPF.op -->", _)) = rep_imp
| oprepthm (Const ("LPF.op <->", _)) = rep_iff
| oprepthm (Const ("LPF.op =", _)) = rep_eq
| oprepthm (Const ("LPF.defl", _)) = rep_defl
| oprepthm (Const ("LPF.deq", _)) = rep_deq
| oprepthm (Const ("LPF.All", _)) = rep_all
| oprepthm (Const ("LPF.Ex", _)) = rep_ex
| oprepthm hdtm = raise NotMono hdtm ;
val rep_thms = [ rep_refl, rep_not, rep_or, rep_and, rep_imp, rep_iff, rep_eq,
rep_defl, rep_deq, rep_all, rep_ex] ;
val rep_tac = resolve_tac rep_thms ;
(* demo
goalw thy [imp_or_def]
"rep((P --> R) & (R --> P), (P --> S) & (S --> P))";
by (REPEAT (SOMEGOAL rep_tac));
goalw thy [and_or_def]
"T --> rep((P --> R) & (R --> P), (P --> S) & (S --> P))";
br impI 1;
by (REPEAT (SOMEGOAL rep_tac));
goalw thy [all_def, imp_or_def]
"rep(ALL x. P(x) --> R(x::'a), ALL x. Q(x) --> R(x))";
by (REPEAT (SOMEGOAL rep_tac));
*)
(* using HOL-type conversionals *)
datatype crep = Unc | Rep of thm ;
(* a rep-conversion is given a certified term ct which is a
proposition (without "Trueprop") and produces a theorem which is
rep (ct, r) or rep (r, ct) for forwards or backwards proof respectively ;
a rep-transformation is given a theorem rep (a,b) and transforms it to
the theorem rep (a,c) or rep (c,b), for forwards or backwards proof ;
in either case the resulting theorem is prefixed by Rep ; if no
change is made then Unc is returned *)
(* Tr2 : thm -> cterm, from rep (a,b), gives b *)
fun Tr2 th =
let val (_, r) = dest_comb (cprop_of th) (* gets rid of Trueprop *)
val (_, v) = dest_comb r
in v end ;
(* mkrep : cterm -> thm, makes theorem rep (ct, ct) *)
local val (_, r) = dest_comb (cprop_of rep_refl)
val (_, v) = dest_comb r
in fun mkrep ct = instantiate ([], [(v, ct)]) rep_refl end ;
(* rep_tt : thm -> thm -> crep
from a theorem rep (A, B), gives the rep-transformation
rep (X, A') --> rep (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 rep_tt repth th = Rep ([th, repth] MRS rep_trans)
handle THM _ => Unc ;
infix THENcr ;
infix THENtt ;
(* conv2tt : (cterm -> crep) -> thm -> crep
takes rep-conversion to rep-transformation *)
fun conv2tt c th =
case c (Tr2 th) of Unc => Unc
| Rep rth => Rep ([th, rth] MRS rep_trans) ;
(* tt2conv : (thm -> 'a) -> cterm -> 'a
takes rep-transformation to rep-conversion *)
fun tt2conv tt = tt o mkrep ;
(* THENtt : (thm -> crep) * (thm -> crep) -> thm -> crep
sequencing two rep-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 -> crep) * (cterm -> crep) -> cterm -> crep
sequencing two rep-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 rep_trans) ;
(* rep2th : rep -> thm, from rep gives corresponding theorem *)
fun rep2th Unc = rep_refl | rep2th (Rep rth) = rth ;
(* val SUBcr = fn : (cterm -> crep) -> cterm -> crep
applies rep-conversion to immediate subterms *)
fun SUBcr c ct =
case term_of ct of
b $ l $ r =>
(let val orth = oprepthm b
val (cbl, cr) = dest_comb ct
val (_, cl) = dest_comb cbl
in case (c cl, c cr) of (Unc, Unc) => Unc
| (lrep, rrep) => Rep ([rep2th lrep, rep2th rrep] MRS orth) end
handle NotMono _ => Unc)
| b $ u =>
(let val orth = oprepthm b
val (_, cu) = dest_comb ct
in case c cu of Unc => Unc
| rep => Rep (rep2th rep RS orth) end
handle NotMono _ => Unc)
| _ => Unc ;
(* SUBtt : (thm -> crep) -> thm -> crep
applies rep-transformation to immediate subterms *)
fun SUBtt tt th = SUBcr (tt o mkrep) (Tr2 th) ;
(* TRYREPtt : (thm -> crep) -> thm -> thm
repeats rep-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 -> crep) -> thm -> crep
repeats rep-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 -> crep) -> thm -> crep
applies rep-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 ;
(* strip_imp_concl : cterm -> cterm, as in drule.ML *)
fun strip_imp_concl ct =
case term_of ct of (Const("==>", _) $ _ $ _) =>
strip_imp_concl (#2 (dest_comb ct))
| _ => ct;
(* reprule : (thm -> crep) -> thm -> thm
applies rep-transformation tt to th, performing forward proof *)
fun reprule tt th =
[(rep2th o tt o mkrep o snd o dest_comb o strip_imp_concl o cprop_of) th,
th] MRS repD ;
(* test and example
val ttt = TDtt (rep_tt idemp_or) ;
val btt = BUtt (rep_tt idemp_or) ;
val rtt = REPtt (rep_tt idemp_or) ;
val stt = SUBtt (rep_tt idemp_or) ;
val tt = (rep_tt idemp_or) ;
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";
reprule ttt p ;
reprule btt p ;
reprule stt p ;
*)
(* applying forward proof to premises of goals *)
(* rep_prem_tac : (thm -> crep) -> int -> int -> tactic
with tt a rep-transformation,
does forward proof on premise number pn in subgoal number sg ;
note that pn is used to calculate the forward proof theorem th to use,
but dtac applies it to the first matching premise *)
fun rep_prem_tac tt pn sg state =
let
(* identify desired subgoal and premise, get as ct *)
val goals = cprems_of state
val prems = strip_imp_prems (List.nth (goals, sg-1))
val (_, ct) = dest_comb (List.nth (prems, pn-1))
val th = rep2th (tt (mkrep ct)) RS repD
in dtac th sg state end ;
(* test and example
goal thy "X";
by (subgoal_tac "P | P <-> (Q | Q) | (R | R) & (S | S)" 1);
by (rep_prem_tac tt 1 1) ;
chop() ; by (rep_prem_tac ttt 1 1) ;
chop() ; by (rep_prem_tac btt 1 1) ;
chop() ; by (rep_prem_tac stt 1 1) ;
*)
(* now for backward proof *)
(* Tr1 : thm -> cterm, from rep (a,b), gives a *)
fun Tr1 th =
let val (_, r) = dest_comb (cprop_of th) (* gets rid of Trueprop *)
val (rv, _) = dest_comb r
val (_, v) = dest_comb rv
in v end ;
(* rep_tt_rev : thm -> thm -> crep
from a theorem rep (A, B), gives the rep-transformation
rep (B', X) --> rep (A', X), where A' and B' are instantiations of A and B *)
fun rep_tt_rev repth th = Rep ([repth, th] MRS rep_trans)
handle THM _ => Unc ;
(* conv2tt_rev : (cterm -> crep) -> thm -> crep
takes rep-conversion to rep-transformation *)
fun conv2tt_rev c th =
case c (Tr1 th) of Unc => Unc
| Rep rth => Rep ([rth, th] MRS rep_trans) ;
(* SUBtt_rev : (thm -> crep) -> thm -> crep
applies rep-transformation to immediate subterms *)
fun SUBtt_rev tt th = SUBcr (tt o mkrep) (Tr1 th) ;
fun TDtt_rev tt th = (REPtt tt THENtt SUBtt_rev (TDtt_rev tt)) th ;
fun BUtt_rev tt th = (SUBtt_rev (BUtt_rev tt) THENtt REPtt tt) th ;
(* rep_rew_tac : (thm -> crep) -> int -> tactic
applies rep-transformation as a tactic in backwards proof *)
fun rep_rew_tac tt sg state =
let val (_, ct) = dest_comb (List.nth (cprems_of state, sg-1))
val th = (rep2th o tt o mkrep) ct RS repD
in rtac th sg state end ;
(* test and example
val tttr = TDtt_rev (rep_tt_rev idemp_or_rev) ;
val bttr = BUtt_rev (rep_tt_rev idemp_or_rev) ;
val rttr = REPtt (rep_tt_rev idemp_or_rev) ;
val sttr = SUBtt_rev (rep_tt_rev idemp_or_rev) ;
val ttr = (rep_tt_rev idemp_or_rev) ;
goal thy "P | P";
goal thy "P | P <-> (Q | Q) | (R | R) & (S | S)";
goal thy "P | P <-> (Q | Q)";
by (rep_rew_tac tttr 1) ;
chop() ; by (rep_rew_tac bttr 1) ;
chop() ; by (rep_rew_tac sttr 1) ;
*)