(* generalised approach to situation where some rewrite rules depend
on something being sn, even more generalised than trgen.thy *)
theory trgg imports Gen Wfss begin
(* rewrite (rule), dependent on things in set being sn *)
types 'tc snrel = "'tc set * ('tc * 'tc)"
axclass wflt < order
wf_lt : "wf {(t, s). t < s}"
axclass grade < type
consts
grade :: "'tc => 'm :: order"
snrules :: "'tc snrel set"
consts
snrel_props :: "('tc => 'm :: order) => 'tc snrel => bool"
(* required property of rules: where a rule depends on some term being in SN,
that term is of smaller measure (mlt),
and the rule takes a term to a term of smaller or equal measure (mle) *)
(*
defs
snrel_props_def : "snrel_props gr == %(sns, rule).
(let (t, s) = rule in (ALL x:sns. gr x < gr s) & gr t <= gr s)"
*)
primrec
defn : "snrel_props gr (sns, rule) =
(let (t, s) = rule in (ALL x:sns. gr x < gr s) & gr t <= gr s)"
consts
ggredstd :: "'tc snrel set =>'tc set => 'tc relation"
(* NOTE - in the following definitions, snrules has not yet been defined
care to avoid circular inconsistent definitions when it is defined *)
defs
ggredstd_def : "ggredstd rules sn ==
{(t, s). EX sns. sns <= sn & (sns, (t, s)) : rules}"
(*
defs
(* ggreduction relation, but that part of it which depends on the
definition of sn is based on SN for smaller terms *)
ggredstud_def : "ggredstud sn t == Union {ggredstd sn t' | t'. t' <= t}"
*)
lemma fc_cong: "[| S = S' ; !!x. x : S' ==> f x = g x |] ==>
{f t | t. t : S} = {g t | t. t : S'}" ;
apply auto ;
apply (rule_tac exI) ;
apply (rule_tac conjI) ;
apply (erule_tac [2] asm_rl) ;
by auto ;
(* doesn't work *)
(*
recdef (permissive) "snu" "mlt"
snu_def : "snu t = wfp (ggredstud (Union {snu t' | t'. (t', t) : mlt}) t)"
(hints recdef_cong: fc_cong)
*)
(*
recdef "snu snl" "mlt"
snu_def : "snu t = wfp (ggredstud (snl t) t)"
snl_def : "snl t = Union {snu t' | t'. (t', t) : mlt}"
*)
(* how to define a function f on a well-founded set, f depends on the
values of f for smaller members *)
consts recfs :: "('tf set => 'tc => 'tf) => 'tc relation => ('tc * 'tf) set"
(* the function from recfs *)
frecfs :: "('tf set => 'tc => 'tf) => 'tc relation => 'tc => 'tf"
inductive "recfs F r"
intros
I : "ALL dtn. (dtn, dt) : r --> (dtn, f dtn) : recfs F r ==>
(dt, F (f ` {dtn. (dtn, dt) : r}) dt) : recfs F r"
defs
frecfs_def : "frecfs F r t == SOME y. (t, y) : recfs F r"
consts
issnp :: "('tc => 'm :: order) => 'tc snrel set => 'tc => 'tc * bool"
issn :: "('tc => 'm :: order) => 'tc snrel set => 'tc => bool"
defs
issnp_def : "issnp gr rules ==
let F = %xs t. (t, t : wfp (ggredstd rules {x. (x, True) : xs})) in
frecfs F {(x, y). gr x < gr y}"
issn_def : "issn gr rules t == snd (issnp gr rules t)"
end