Transitive and Well-Founded Relations as Properties
Overview
 Most ProofPower relations are properties not sets, so the theory of this kind of well-foundedness is developed here.
 Introduction A new "wf_relp" theory is created as a child of "wf_rel". The purpose of this theory is entirely cosmetic. I want to use the results in developing set theory but I want to avoid use of the membership sign in a context in which it is likely to cause confusion. Transitive Relations Elementary results about transitive relations and transitive closure. Well-Founded Relations Definition of well-founded and transitive-well-founded and proof that the transitive closure of a well-founded relation is transitive-well-founded.
 Proof Context In this section I will create a decent proof context for recursive definitions, eventually. Listing of Theory wf_relp
Introduction
 A new "wf_relp" theory is created as a child of "wf_rel". The purpose of this theory is entirely cosmetic. I want to use the results in developing set theory but I want to avoid use of the membership sign in a context in which it is likely to cause confusion.
Introduction
One of the principle well-founded relations of interest in this application is g, which has type
 xl-gft GS GS BOOL

so I would like a version of "well-founded" which has type:
 xl-gft ('a 'a BOOL) BOOL The new theory is first created, together with a proof context which we will build up as we develop the theory.

 xl-sml open_theory "hol"; force_new_theory "wf_relp"; force_new_pc "wf_relp"; merge_pcs ["xl_cs__conv"] "wf_relp"; set_merge_pcs ["hol", "wf_relp"];

Transitive Relations
 Elementary results about transitive relations and transitive closure.
Definitions

 xl-holconsttrans: ('a 'a BOOL) BOOL r trans r s t u r s t r t u r s u

 xl-holconsttc: ('a 'a BOOL) ('a 'a BOOL) r tc r = s t tr trans tr (v u r v u tr v u) tr s t
Theorems

 xl-sml set_goal([],r trans (tc r)); a (rewrite_tac(map get_spec [tc,trans])); a (REPEAT strip_tac); a (all_asm_fc_tac []); a (all_asm_fc_tac []); val tran_tc_thm = save_pop_thm("tran_tc_thm"); set_goal([], r x y z tc r x y tc r y z tc r x z); a (prove_tac [rewrite_rule [get_spec trans] tran_tc_thm]); val tran_tc_thm2 = save_pop_thm("tran_tc_thm2"); set_goal([],r x y r x y tc r x y); a (rewrite_tac [get_spec tc, sets_ext_clauses] THEN REPEAT strip_tac); a (all_asm_fc_tac[]); val tc_incr_thm = save_pop_thm("tc_incr_thm");

 xl-sml set_goal([], r x y tc r x y r x y z tc r x z r z y); a (REPEAT strip_tac); a (lemma_tac q trans q (v w r v w q v w) q x y); a (asm_ante_tac tc r x y); a (rewrite_tac [get_spec tc, get_spec trans]); a (spec_nth_asm_tac 1 v w r v w u tc r v u r u w);

 xl-gft (* *** Goal "2.1" *** *) (* 4 *) tc r x y (* 3 *) r x y (* 2 *) q trans q ( v w r v w q v w) q x y (* 1 *) trans ( v w r v w ( u tc r v u r u w)) (* ? *) z tc r x z r z y

 xl-sml a (swap_nth_asm_concl_tac 1 THEN rewrite_tac [get_spec trans] THEN REPEAT strip_tac); (* *** Goal "2.1.1" *** *) a (_tac t THEN asm_rewrite_tac[]); a (all_fc_tac [tc_incr_thm]); (* *** Goal "2.1.2" *** *) a (_tac u' THEN asm_rewrite_tac[]); a (REPEAT (all_asm_fc_tac [tran_tc_thm2,tc_incr_thm])); (* *** Goal "2.1.3" *** *) a (_tac t THEN asm_rewrite_tac[]); a (REPEAT(all_asm_fc_tac [tran_tc_thm2,tc_incr_thm])); (* *** Goal "2.1.4" *** *) a (_tac u'' THEN asm_rewrite_tac[]); a (REPEAT(all_asm_fc_tac [tran_tc_thm2,tc_incr_thm])); (* *** Goal "2.2" *** *) a (swap_nth_asm_concl_tac 1 THEN asm_rewrite_tac []); (* *** Goal "2.3" *** *) a (swap_nth_asm_concl_tac 1 THEN asm_rewrite_tac []); val tc_decomp_thm = save_pop_thm "tc_decomp_thm";

 xl-sml set_goal([], r1 r2 ( x y r1 x y r2 x y) ( x y tc r1 x y tc r2 x y)); a (rewrite_tac [get_spec tc]); a (REPEAT strip_tac); a (spec_nth_asm_tac 3 tr); a (all_asm_fc_tac[]); a (all_asm_fc_tac[]); val tc_mono_thm = save_pop_thm "tc_mono_thm";

 xl-sml set_goal([], r p ( x y r x y p x) ( x y tc r x y p x)); a (rewrite_tac [get_spec tc]); a (REPEAT strip_tac); a (SPEC_NTH_ASM_T 1 x y:'a (p x):BOOL (fn x => strip_asm_tac (rewrite_rule[] x)) THEN_TRY all_asm_fc_tac[]); a (swap_nth_asm_concl_tac 1 THEN rewrite_tac [get_spec trans] THEN REPEAT strip_tac); val tc_p_thm = save_pop_thm "tc_p_thm";

Well-Founded Relations
 Definition of well-founded and transitive-well-founded and proof that the transitive closure of a well-founded relation is transitive-well-founded.
Definitions

 xl-holconstwell_founded: ('a 'a BOOL) BOOL r well_founded r s ( x ( y r y x s y) s x) x s x

 xl-holconsttwfp: ('a 'a BOOL) BOOL r twfp r well_founded r trans r
Theorems
The first thing I need to prove here is that the transitive closure of a well-founded relation is also well-founded. This provides a form of induction with a stronger induction hypothesis. Naturally we would expect this to be proven inductively and the question is therefore what property to use in the inductive proof, the observation that the transitive closure of a relation is well-founded is not explicitly the ascription of a property to the field of the relation. The obvious method is to relativise the required result to the transitive closure of a set, giving a property of sets, and then to prove that this property is hereditary if the relation is well-founded.

 xl-sml set_goal([],s r well_founded r x (y tc r y x (z tc r z y s z) s y) (y tc r y x s y)); a (rewrite_tac [get_spec well_founded]); a (REPEAT_N 3 strip_tac); a (SPEC_NTH_ASM_T 1 x (y tc r y x (z tc r z y s z) s y) (y tc r y x s y) ante_tac THEN rewrite_tac[] THEN REPEAT strip_tac); a (fc_tac [list__elim [r,y,x] tc_decomp_thm]); (* *** Goal "1" *** *) a (spec_nth_asm_tac 7 y); (* *** Goal "1.1" *** *) a (all_fc_tac [tran_tc_thm2]); a (spec_nth_asm_tac 10 y''); a (asm_fc_tac[]); (* *** Goal "1.2" *** *) a (spec_nth_asm_tac 7 y); a (spec_nth_asm_tac 3 z); (* *** Goal "2" *** *) a (spec_nth_asm_tac 8 z); (* *** Goal "2.1" *** *) a (lemma_tac tc r z x THEN1 fc_tac [tc_incr_thm]); a (lemma_tac tc r y'' x THEN1 strip_asm_tac (list__elim [r,y'',z,x] tran_tc_thm2)); a (spec_nth_asm_tac 12 y''); a (spec_nth_asm_tac 6 z'); (* *** Goal "2.2" *** *) a (asm_fc_tac[]); val tcwf_lemma1 = save_pop_thm "tcwf_lemma1";

 xl-sml set_goal([],r well_founded r s (t (u tc r u t s u) s t) (e s e)); a (REPEAT strip_tac THEN fc_tac [tcwf_lemma1]); a (spec_nth_asm_tac 2 e); a (list_spec_nth_asm_tac 3 [e,s,u]); a (spec_nth_asm_tac 7 y); a (spec_nth_asm_tac 4 u'); val tcwf_lemma2 = save_pop_thm "tcwf_lemma2";

 xl-sml set_goal([],r well_founded r well_founded (tc r)); a (strip_tac THEN strip_tac THEN fc_tac [tcwf_lemma1]); a (rewrite_tac [get_spec well_founded]); a (REPEAT strip_tac); a (spec_nth_asm_tac 1 x); a (list_spec_nth_asm_tac 4 [x,s,y]); a (spec_nth_asm_tac 6 y'); a (spec_nth_asm_tac 4 y''); val wf_tc_wf_thm = save_pop_thm "wf_tc_wf_thm";

Now we prove that if the transitive closure of a relation is well-founded then so must be the relation.
 xl-sml set_goal([], r well_founded (tc r) well_founded r); a (rewrite_tac [get_spec well_founded] THEN REPEAT strip_tac); a (spec_nth_asm_tac 2 s); (* *** Goal "1" *** *) a (spec_nth_asm_tac 3 x'); a (all_asm_fc_tac [tc_incr_thm]); a (all_asm_fc_tac []); (* *** Goal "2" *** *) a (asm_rewrite_tac[]); val tc_wf_wf_thm = save_pop_thm "tc_wf_wf_thm";

 xl-sml set_goal([],r well_founded r twfp (tc r)); a (REPEAT strip_tac); a (fc_tac [wf_tc_wf_thm]); a (asm_rewrite_tac [get_spec twfp, tran_tc_thm]); val tc_wf_twf_thm = save_pop_thm "tc_wf_twf_thm";

Induction Tactics etc.
We here define a general tactic for performing induction using some well-founded relation. The following function (I think these things are called "THM-TACTICAL"s) must be given a theorem which asserts that some relation is well-founded, and then a THM-TACTIC (which determines what is done with the induction assumption), and then a term which is the variable to induct over, and will then facilitate an inductive proof of the current goal using that theorem.
 xl-sml fun WF_INDUCTION_T (thm : THM) (ttac : THM -> TACTIC) : TERM -> TACTIC = ( letfun bad_thm thm = thm_fail "WF_INDUCTION_T" 29021 [thm]; val (wf, r) = (dest_app (concl thm)) handle Fail _ => bad_thm thm; val sthm = _elim r tcwf_lemma2 handle Fail _ => bad_thm thm; val ithm = _elim sthm thm handle Fail _ => bad_thm thm; in GEN_INDUCTION_T ithm ttac end );

And now we make a tactic out of that (basically by saying "strip the induction hypothesis into the assumptions").
 xl-sml fun wf_induction_tac (thm : THM) : TERM -> TACTIC = ( letval ttac = (WF_INDUCTION_T thm strip_asm_tac) handle ex => reraise ex "wf_induction_tac"; in fn tm => letval tac = (ttac tm) handle ex => reraise ex "wf_induction_tac"; infn gl => ((tac gl) handle ex => reraise ex "wf_induction_tac") end end );

Well-foundedness and Induction
The following proof shows how the above induction tactic can be used. The theorem can be paraphrased loosely along the lines that there are no bottomless descending chains in a well-founded relation. We think of a bottomless descending chain as a non-empty set (represented by a property called "p") every element of which is preceded by an element under the transitive closure of r.
 xl-sml set_goal([], r well_founded r x p v p v y p y tc r y x z p z r z y); a (strip_tac THEN strip_tac THEN strip_tac); a (wf_induction_tac (asm_rule well_founded r) x); a contr_tac; a (all_asm_fc_tac[]); a (spec_nth_asm_tac 6 v); a (SPEC_NTH_ASM_T 1 x p x tc r x v ante_tac THEN rewrite_tac[] THEN REPEAT strip_tac); a (_tac z THEN REPEAT strip_tac); (* *** Goal "1" *** *) a (fc_tac [tc_incr_thm]); (* *** Goal "2" *** *) a (spec_nth_asm_tac 7 y); a (_tac z' THEN asm_rewrite_tac[]); a (lemma_tac tc r z' y THEN1 fc_tac [tc_incr_thm]); a (all_fc_tac [tran_tc_thm2]); val wf_nochain_thm = save_pop_thm "wf_nochain_thm";

Now a shorter formulation of bottomless pits.
 xl-sml set_goal([], r well_founded r p v p v y p y z p z r z y); a (contr_tac); a (lemma_tac x p x THEN1 (strip_tac THEN wf_induction_tac (asm_rule well_founded r) x)); (* *** Goal "1" *** *) a (contr_tac THEN REPEAT (all_asm_fc_tac[tc_incr_thm])); (* *** Goal "2" *** *) a (REPEAT (all_asm_fc_tac[])); val wf_wf_thm = save_pop_thm "wf_wf_thm";

Next we prove the converse, that the lack of bottomless pits entails well-foundedness.
 xl-sml set_goal([], r (x p v p v y p y tc r y x z p z r z y) well_founded r); a (rewrite_tac [get_spec well_founded]); a contr_tac; a (DROP_NTH_ASM_T 3 ante_tac THEN rewrite_tac[] THEN strip_tac); a (_tac x THEN rewrite_tac[]); a (lemma_tac rel rel = v w s v s w r v w THEN1 prove__tac); a (_tac q tc rel q xTHEN rewrite_tac[]); a (spec_nth_asm_tac 3 x); a (_tac y THEN REPEAT strip_tac); (* *** Goal "1" *** *) a (lemma_tac rel y x THEN1 asm_rewrite_tac[]); a (all_asm_fc_tac [tc_incr_thm]); (* *** Goal "2" *** *) a (lemma_tac x y rel x y r x y THEN1 (strip_tac THEN strip_tac THEN asm_rewrite_tac[] THEN REPEAT strip_tac)); a (all_fc_tac [tc_mono_thm]); (* *** Goal "3" *** *) a (lemma_tac s y'); (* *** Goal "3.1" *** *) a (lemma_tac x y rel x y s x THEN1 (REPEAT _tac THEN asm_rewrite_tac [] THEN REPEAT strip_tac)); a (all_asm_fc_tac[rewrite_rule[](list__elim [rel, x s x] tc_p_thm)]); (* *** Goal "3.2" *** *) a (spec_nth_asm_tac 7 y'); a (_tac y'' THEN REPEAT strip_tac); a (lemma_tac tc rel y'' y'); (* *** Goal "3.2.1" *** *) a (lemma_tac rel y'' y' THEN1 asm_rewrite_tac[]); a (all_asm_fc_tac[tc_incr_thm]); (* *** Goal "3.2.2" *** *) a (all_asm_fc_tac[tran_tc_thm2]); val nochain_wf_thm = save_pop_thm "nochain_wf_thm";

Now with second order foundation.
 xl-sml set_goal([], (p v p v y p y z p z r z y) well_founded r); a (rewrite_tac [get_spec well_founded] THEN REPEAT strip_tac); a (SPEC_NTH_ASM_T 2 x s x ante_tac THEN rewrite_tac[] THEN strip_tac); a (spec_nth_asm_tac 1 x); a (spec_nth_asm_tac 4 y); a (spec_nth_asm_tac 3 y'); val wf_induct_thm = save_pop_thm "wf_induct_thm";

Try a weaker hypothesis.
 xl-sml set_goal([], r (x p v p v y p y z p z r z y) well_founded r); a (rewrite_tac [get_spec well_founded]); a contr_tac; a (DROP_NTH_ASM_T 3 ante_tac THEN rewrite_tac[] THEN strip_tac); a (lemma_tac rel rel = v w s v s w r v w THEN1 prove__tac); a (_tac q tc rel q xTHEN rewrite_tac[]); a (spec_nth_asm_tac 3 x); a (_tac y THEN REPEAT strip_tac); (* *** Goal "1" *** *) a (lemma_tac rel y x THEN1 asm_rewrite_tac[]); a (all_asm_fc_tac [tc_incr_thm]); (* *** Goal "2" *** *) a (lemma_tac x y rel x y s x THEN1 (REPEAT _tac THEN asm_rewrite_tac [] THEN REPEAT strip_tac)); a (all_asm_fc_tac[rewrite_rule[](list__elim [rel, x s x] tc_p_thm)]); a (spec_nth_asm_tac 8 y'); a (_tac y'' THEN REPEAT strip_tac); a (lemma_tac rel y'' y' THEN1 asm_rewrite_tac[]); a (lemma_tac tc rel y'' y' THEN1 all_asm_fc_tac[tc_incr_thm]); a (all_asm_fc_tac[tran_tc_thm2]); val nochain_wf_thm2 = save_pop_thm "nochain_wf_thm2";

Bottomless Pits and Minimal Elements
The following theorem states something like that if there are no unending downward chains then every "set" has a minimal element.
 xl-sml set_goal([], r(x p v p v y p y tc r y x z p z r z y) x (y r y x) z r z x v r v z r v x); a contr_tac; a (DROP_NTH_ASM_T 3 ante_tac THEN rewrite_tac[] THEN REPEAT strip_tac THEN rewrite_tac[] ); a (_tac x THEN _tac w r w x THEN _tac y THEN asm_rewrite_tac[]); a (strip_tac THEN asm_rewrite_tac[]); a (REPEAT strip_tac); (* *** Goal "1" *** *) a (all_asm_fc_tac [tc_incr_thm]); (* *** Goal "2" *** *) a (spec_nth_asm_tac 2 y'); a (_tac v THEN asm_rewrite_tac[]); val nochain_min_thm = save_pop_thm "nochain_min_thm";

A second order version with the weaker bottomless pits can be formulated as follows:
 xl-sml set_goal([], r(x p v p v y p y z p z r z y) p (y p y) z p z v r v z p v); a contr_tac; a (DROP_NTH_ASM_T 3 ante_tac THEN rewrite_tac[] THEN REPEAT strip_tac ); a (_tac p THEN _tac y THEN asm_rewrite_tac[]); a (REPEAT strip_tac); a (spec_nth_asm_tac 2 y'); a (_tac v THEN asm_rewrite_tac[]); val nochain_min_thm2 = save_pop_thm "nochain_min_thm2";

It follows that all non-empty collections of predecessors under a well-founded relation have minimal elements.
 xl-sml set_goal([], r well_founded r x (y r y x) z r z x v r v z r v x); a (REPEAT_N 2 strip_tac); a (strip_asm_tac ( _elim r wf_nochain_thm)); a (ante_tac (_elim r nochain_min_thm)); a (GET_NTH_ASM_T 1 ante_tac); a (rewrite_tac [prove_rule [] a b a (a b) b ]); val wf_min_thm = save_pop_thm "wf_min_thm";

But the converse does not hold.
 xl-sml set_goal([], r: BOOLBOOLBOOL(x (y r y x) z r z x v r v z r v x) well_founded r); a (_tac x y:BOOL y THEN rewrite_tac [get_spec well_founded] THEN REPEAT strip_tac); (* *** Goal "1" *** *) a (_tac F THEN asm_rewrite_tac []); (* *** Goal "2" *** *) a (_tac \$ THEN REPEAT strip_tac); (* *** Goal "2.1" *** *) a (spec_nth_asm_tac 1 x); (* *** Goal "2.2" *** *) a (_tac T THEN rewrite_tac[]); val minr_not_wf_thm = save_pop_thm "minr_not_wf_thm";

Restrictions of Well-Founded Relations
 In this section we show that a restriction of a well-founded relation is well-founded.
Restriction of Well-Founded Relation

 xl-sml set_goal([], r well_founded r r2 well_founded (x y r2 x y r x y)); a (REPEAT strip_tac); a (bc_tac [nochain_wf_thm]); a (fc_tac [wf_nochain_thm]); a (REPEAT strip_tac); a (list_spec_nth_asm_tac 2 [p, x, v]); (* *** Goal "1" *** *) a (spec_nth_asm_tac 3 y); a (lemma_tac x y ( x y r2 x y r x y) x y r x y THEN1 (rewrite_tac[] THEN REPEAT strip_tac)); a (FC_T fc_tac [tc_mono_thm]); (* *** Goal "2" *** *) a (SPEC_NTH_ASM_T 3 y ante_tac THEN (rewrite_tac []) THEN REPEAT strip_tac); a (spec_nth_asm_tac 5 z); val wf_restrict_wf_thm = save_pop_thm "wf_restrict_wf_thm";

Proof Context
 In this section I will create a decent proof context for recursive definitions, eventually.
Proof Context

 xl-sml (* commit_pc "wf_relp"; *)