(* stuff to do with closure under context *)
theory clcon imports base begin
consts
(* these now parameterized by "primitive" reduction *)
ctxt :: "'a rule set => 'a rule set"
ctxt1 :: "'a rule => 'a rule set"
nctxt :: "'a rule set => nat => 'a rule set"
ltnctxt :: "'a rule set => nat => 'a rule set"
nured :: "'a rule set => 'a rule set"
nured1 :: "'a rule => 'a rule set"
sn1order :: "'a rule set => 'a rule set"
sn2order :: "'a rule set => 'a rule set"
constrict :: "'a rule set => 'a rule set"
onered :: "'a rule set => ('a rtree list * 'a rtree list) set"
sn1red :: "'a rule set => ('a rtree list * 'a rtree list) set"
sn2red :: "'a rule set => ('a rtree list * 'a rtree list) set"
wfpc :: "('a * 'a) set => ('a * 'a) set"
inductive "ctxt r"
intros
red_nuI : "(dtr, dt) : oneup (onerel (ctxt r)) ==>
(dtr, dt) : ctxt r"
red_cutI : "(dtr, dt) : r ==> (dtr, dt) : ctxt r"
monos oo_mono
defs
ctxt1_def : "ctxt1 p == ctxt {p}"
nured1_def : "nured1 p == nured {p}"
(*
wfpc_def : "wfpc r == {(t, s). s : wfp (ctxt r)}"
*)
inductive "wfpc r"
intros
I : "s : wfp (ctxt r) ==> (t, s) : wfpc r"
(* context, but at a specific or limited depth in the tree *)
primrec
nctxt_0 : "nctxt r 0 = r"
nctxt_Suc : "nctxt r (Suc n) = oneup (onerel (nctxt r n))"
primrec
ltnctxt_0 : "ltnctxt r 0 = {}"
ltnctxt_Suc : "ltnctxt r (Suc n) = (ltnctxt r n Un nctxt r n)"
defs
nured_def : "nured r == oneup (onerel (ctxt r))"
onered_def : "onered r == onerel (ctxt r)"
sn1red_def : "sn1red r == onerel (fwf (ctxt r))"
sn2red_def : "sn2red r == onerel (ctxt (fwf (ctxt r)))"
defs
sn1order_def : "sn1order r == oneup (sn1red r)"
sn2order_def : "sn2order r == oneup (sn2red r)"
defs
(* constricting derivations, in the sense of
Nachum Dershowitz. Termination Dependencies. Extended Abstract.
www.cs.tau.ac.il/~nachumd/papers/depend.pdf
see also (which differ)
Femke van Raamsdonk, Paula Severi, Morten Heine Sørensen and Hongwei Xi
Perpetual Reductions in Lambda Calculus
Information and Computation 149(2):173--225, March 1999,
http://www.cs.vu.nl/~femke/ps/jic98.ps, page 25,
David Plaisted, RTA-93, LNCS 690, 405-420 *)
constrict_def : "constrict r ==
{(dtn, dt). (dtn, dt) : r & set (isubts dt) <= wfp (ctxt r)}"
end