# Theory WF

(*  Title:      ZF/WF.thy
Author:     Tobias Nipkow and Lawrence C Paulson

Derived first for transitive relations, and finally for arbitrary WF relations
via wf_trancl and trans_trancl.

It is difficult to derive this general case directly, using r^+ instead of
r.  In is_recfun, the two occurrences of the relation must have the same
form.  Inserting r^+ in the_recfun or wftrec yields a recursion rule with
r^+ -`` {a} instead of r-``{a}.  This recursion rule is stronger in
principle, but harder to use, especially to prove wfrec_eclose_eq in
epsilon.ML.  Expanding out the definition of wftrec in wfrec would yield
a mess.
*)

section‹Well-Founded Recursion›

theory WF imports Trancl begin

definition
wf           :: "io"  where
(*r is a well-founded relation*)
"wf(r)  Z. Z=0 | (xZ. y. y,x:r  ¬ y  Z)"

definition
wf_on        :: "[i,i]o"                      (wf[_]'(_'))  where
(*r is well-founded on A*)
"wf_on(A,r)  wf(r  A*A)"

definition
is_recfun    :: "[i, i, [i,i]i, i] o"  where
"is_recfun(r,a,H,f)  (f = (λxr-``{a}. H(x, restrict(f, r-``{x}))))"

definition
the_recfun   :: "[i, i, [i,i]i] i"  where
"the_recfun(r,a,H)  (THE f. is_recfun(r,a,H,f))"

definition
wftrec :: "[i, i, [i,i]i] i"  where
"wftrec(r,a,H)  H(a, the_recfun(r,a,H))"

definition
wfrec :: "[i, i, [i,i]i] i"  where
(*public version.  Does not require r to be transitive*)
"wfrec(r,a,H)  wftrec(r^+, a, λx f. H(x, restrict(f,r-``{x})))"

definition
wfrec_on     :: "[i, i, i, [i,i]i] i"       (wfrec[_]'(_,_,_'))  where
"wfrec[A](r,a,H)  wfrec(r  A*A, a, H)"

subsection‹Well-Founded Relations›

subsubsection‹Equivalences between termwf and termwf_on

lemma wf_imp_wf_on: "wf(r)  wf[A](r)"
by (unfold wf_def wf_on_def, force)

lemma wf_on_imp_wf: "wf[A](r); r  A*A  wf(r)"

lemma wf_on_field_imp_wf: "wf[field(r)](r)  wf(r)"
by (unfold wf_def wf_on_def, fast)

lemma wf_iff_wf_on_field: "wf(r)  wf[field(r)](r)"
by (blast intro: wf_imp_wf_on wf_on_field_imp_wf)

lemma wf_on_subset_A: "wf[A](r);  B<=A  wf[B](r)"
by (unfold wf_on_def wf_def, fast)

lemma wf_on_subset_r: "wf[A](r); s<=r  wf[A](s)"
by (unfold wf_on_def wf_def, fast)

lemma wf_subset: "wf(s); r<=s  wf(r)"

subsubsection‹Introduction Rules for termwf_on

text‹If every non-empty subset of termA has an termr-minimal element
then we have termwf[A](r).›
lemma wf_onI:
assumes prem: "Z u. Z<=A;  u  Z;  xZ. yZ. y,x:r  False"
shows         "wf[A](r)"
unfolding wf_on_def wf_def
apply (rule equals0I [THEN disjCI, THEN allI])
apply (rule_tac Z = Z in prem, blast+)
done

text‹If termr allows well-founded induction over termA
then we have termwf[A](r).   Premise is equivalent to
propB. xA. (y. y,x: r  y  B)  x  B  A<=B
lemma wf_onI2:
assumes prem: "y B. xA. (yA. y,x:r  y  B)  x  B;   y  A
y  B"
shows         "wf[A](r)"
apply (rule wf_onI)
apply (rule_tac c=u in prem [THEN DiffE])
prefer 3 apply blast
apply fast+
done

subsubsection‹Well-founded Induction›

text‹Consider the least termz in termdomain(r) such that
termP(z) does not hold...›
lemma wf_induct_raw:
"wf(r);
x.y. y,x: r  P(y)  P(x)
P(a)"
unfolding wf_def
apply (erule_tac x = "{z  domain(r). ¬ P(z)}" in allE)
apply blast
done

lemmas wf_induct = wf_induct_raw [rule_format, consumes 1, case_names step, induct set: wf]

text‹The form of this rule is designed to match wfI›
lemma wf_induct2:
"wf(r);  a  A;  field(r)<=A;
x.x  A;  y. y,x: r  P(y)  P(x)
P(a)"
apply (erule_tac P="a  A" in rev_mp)
apply (erule_tac a=a in wf_induct, blast)
done

lemma field_Int_square: "field(r  A*A)  A"
by blast

lemma wf_on_induct_raw [consumes 2, induct set: wf_on]:
"wf[A](r);  a  A;
x.x  A;  yA. y,x: r  P(y)  P(x)
P(a)"
unfolding wf_on_def
apply (erule wf_induct2, assumption)
apply (rule field_Int_square, blast)
done

lemma wf_on_induct [consumes 2, case_names step, induct set: wf_on]:
"wf[A](r)  a  A  (x. x  A  (y. y  A  y, x  r  P(y))  P(x))  P(a)"
using wf_on_induct_raw [of A r a P] by simp

text‹If termr allows well-founded induction
then we have termwf(r).›
lemma wfI:
"field(r)<=A;
y B. xA. (yA. y,x:r  y  B)  x  B;  y  A
y  B
wf(r)"
apply (rule wf_on_subset_A [THEN wf_on_field_imp_wf])
apply (rule wf_onI2)
prefer 2 apply blast
apply blast
done

subsection‹Basic Properties of Well-Founded Relations›

lemma wf_not_refl: "wf(r)  a,a  r"
by (erule_tac a=a in wf_induct, blast)

lemma wf_not_sym [rule_format]: "wf(r)  x. a,x:r  x,a  r"
by (erule_tac a=a in wf_induct, blast)

(* @{term"⟦wf(r);  ⟨a,x⟩ ∈ r;  ¬P ⟹ ⟨x,a⟩ ∈ r⟧ ⟹ P"} *)
lemmas wf_asym = wf_not_sym [THEN swap]

lemma wf_on_not_refl: "wf[A](r); a  A  a,a  r"
by (erule_tac a=a in wf_on_induct, assumption, blast)

lemma wf_on_not_sym:
"wf[A](r);  a  A  (b. bA  a,b:r  b,ar)"
apply (atomize (full), intro impI)
apply (erule_tac a=a in wf_on_induct, assumption, blast)
done

lemma wf_on_asym:
"wf[A](r);  ¬Z  a,b  r;
b,a  r  Z; ¬Z  a  A; ¬Z  b  A  Z"
by (blast dest: wf_on_not_sym)

(*Needed to prove well_ordI.  Could also reason that wf[A](r) means
wf(r ∩ A*A);  thus wf( (r ∩ A*A)^+ ) and use wf_not_refl *)
lemma wf_on_chain3:
"wf[A](r); a,b:r; b,c:r; c,a:r; a  A; b  A; c  A  P"
apply (subgoal_tac "yA. zA. a,y:r  y,z:r  z,a:r  P",
blast)
apply (erule_tac a=a in wf_on_induct, assumption, blast)
done

text‹transitive closure of a WF relation is WF provided
termA is downward closed›
lemma wf_on_trancl:
"wf[A](r);  r-``A  A  wf[A](r^+)"
apply (rule wf_onI2)
apply (frule bspec [THEN mp], assumption+)
apply (erule_tac a = y in wf_on_induct, assumption)
apply (blast elim: tranclE, blast)
done

lemma wf_trancl: "wf(r)  wf(r^+)"
apply (rule wf_on_subset_A)
apply (erule wf_on_trancl)
apply blast
apply (rule trancl_type [THEN field_rel_subset])
done

texttermr-``{a} is the set of everything under terma in termr

lemmas underI = vimage_singleton_iff [THEN iffD2]
lemmas underD = vimage_singleton_iff [THEN iffD1]

subsection‹The Predicate term

lemma is_recfun_type: "is_recfun(r,a,H,f)  f  r-``{a} -> range(f)"
unfolding is_recfun_def
apply (erule ssubst)
apply (rule lamI [THEN rangeI, THEN lam_type], assumption)
done

lemmas is_recfun_imp_function = is_recfun_type [THEN fun_is_function]

lemma apply_recfun:
"is_recfun(r,a,H,f); x,a:r  f`x = H(x, restrict(f,r-``{x}))"
unfolding is_recfun_def
txt‹replace f only on the left-hand side›
apply (erule_tac P = "λx. t(x) = u" for t u in ssubst)
done

lemma is_recfun_equal [rule_format]:
"wf(r);  trans(r);  is_recfun(r,a,H,f);  is_recfun(r,b,H,g)
x,a:r  x,b:r  f`x=g`x"
apply (frule_tac f = f in is_recfun_type)
apply (frule_tac f = g in is_recfun_type)
apply (erule_tac a=x in wf_induct)
apply (intro impI)
apply (elim ssubst)
apply (simp (no_asm_simp) add: vimage_singleton_iff restrict_def)
apply (rule_tac t = "λz. H (x, z)" for x in subst_context)
apply (subgoal_tac "yr-``{x}. z. y,z:f  y,z:g")
apply (blast dest: transD)
apply (blast dest: transD intro: sym)
done

lemma is_recfun_cut:
"wf(r);  trans(r);
is_recfun(r,a,H,f);  is_recfun(r,b,H,g);  b,a:r
restrict(f, r-``{b}) = g"
apply (frule_tac f = f in is_recfun_type)
apply (rule fun_extension)
apply (blast dest: transD intro: restrict_type2)
apply (erule is_recfun_type, simp)
apply (blast dest: transD intro: is_recfun_equal)
done

subsection‹Recursion: Main Existence Lemma›

lemma is_recfun_functional:
"wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,a,H,g)    f=g"
by (blast intro: fun_extension is_recfun_type is_recfun_equal)

lemma the_recfun_eq:
"is_recfun(r,a,H,f);  wf(r);  trans(r)  the_recfun(r,a,H) = f"
unfolding the_recfun_def
apply (blast intro: is_recfun_functional)
done

(*If some f satisfies is_recfun(r,a,H,-) then so does the_recfun(r,a,H) *)
lemma is_the_recfun:
"is_recfun(r,a,H,f);  wf(r);  trans(r)
is_recfun(r, a, H, the_recfun(r,a,H))"

lemma unfold_the_recfun:
"wf(r);  trans(r)  is_recfun(r, a, H, the_recfun(r,a,H))"
apply (rule_tac a=a in wf_induct, assumption)
apply (rename_tac a1)
apply (rule_tac f = "λyr-``{a1}. wftrec (r,y,H)" in is_the_recfun)
apply typecheck
unfolding is_recfun_def wftrec_def
― ‹Applying the substitution: must keep the quantified assumption!›
apply (rule lam_cong [OF refl])
apply (drule underD)
apply (fold is_recfun_def)
apply (rule_tac t = "λz. H(x, z)" for x in subst_context)
apply (rule fun_extension)
apply (blast intro: is_recfun_type)
apply (rule lam_type [THEN restrict_type2])
apply blast
apply (blast dest: transD)
apply atomize
apply (frule spec [THEN mp], assumption)
apply (subgoal_tac "xa,a1  r")
apply (drule_tac x1 = xa in spec [THEN mp], assumption)
apply_recfun is_recfun_cut)
apply (blast dest: transD)
done

subsection‹Unfolding termwftrec(r,a,H)

lemma the_recfun_cut:
"wf(r);  trans(r);  b,a:r
restrict(the_recfun(r,a,H), r-``{b}) = the_recfun(r,b,H)"
by (blast intro: is_recfun_cut unfold_the_recfun)

(*NOT SUITABLE FOR REWRITING: it is recursive!*)
lemma wftrec:
"wf(r);  trans(r)
wftrec(r,a,H) = H(a, λxr-``{a}. wftrec(r,x,H))"
unfolding wftrec_def
apply (subst unfold_the_recfun [unfolded is_recfun_def])
apply (simp_all add: vimage_singleton_iff [THEN iff_sym] the_recfun_cut)
done

subsubsection‹Removal of the Premise termtrans(r)

(*NOT SUITABLE FOR REWRITING: it is recursive!*)
lemma wfrec:
"wf(r)  wfrec(r,a,H) = H(a, λxr-``{a}. wfrec(r,x,H))"
unfolding wfrec_def
apply (erule wf_trancl [THEN wftrec, THEN ssubst])
apply (rule trans_trancl)
apply (rule vimage_pair_mono [THEN restrict_lam_eq, THEN subst_context])
apply (erule r_into_trancl)
apply (rule subset_refl)
done

(*This form avoids giant explosions in proofs.  NOTE USE OF ≡ *)
lemma def_wfrec:
"x. h(x)wfrec(r,x,H);  wf(r)
h(a) = H(a, λxr-``{a}. h(x))"
apply simp
apply (elim wfrec)
done

lemma wfrec_type:
"wf(r);  a  A;  field(r)<=A;
x u. x  A;  u  Pi(r-``{x}, B)  H(x,u)  B(x)
wfrec(r,a,H)  B(a)"
apply (rule_tac a = a in wf_induct2, assumption+)
apply (subst wfrec, assumption)
done

lemma wfrec_on:
"wf[A](r);  a  A
wfrec[A](r,a,H) = H(a, λx(r-``{a})  A. wfrec[A](r,x,H))"
unfolding wf_on_def wfrec_on_def
apply (erule wfrec [THEN trans])