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.

Elementary results about transitive relations and transitive closure.

Definition of well-founded and transitive-well-founded and proof that the transitive closure of a well-founded relation is transitive-well-founded.

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

One of the principle well-founded relations of interest in this application is

_g, which has type

xl-gft

BOOL

so I would like a version of "well-founded" which has type:

xl-gft

('a

BOOL)

BOOL

</subsec>
<subsec title="The Theory wf_relp">
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"];

xl-holconst

trans: ('a

BOOL)

BOOL

trans r

s t u

r s t

r t u

r s u

xl-holconst

tc: ('a

BOOL)

('a

BOOL)

tc r =

s t

trans tr

(

v u

r v u

tr v u)

tr s t

xl-sml

set_goal([],

trans (tc r)

);
a (rewrite_tac(map get_spec [

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

tc r x y

);
a (rewrite_tac [get_spec

, 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

tc r x z

r z y

);
a (REPEAT strip_tac);
a (lemma_tac

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

get_spec

trans

]);
a (spec_nth_asm_tac 1

v w

r v w

tc r v u

r u w

);

xl-gft

(* *** Goal "2.1" *** *)

(* 4 *)

tc r x y

(* 3 *)

r x y

(* 2 *)

trans q

(

v w

r v w

q v w)

q x y

(* 1 *)

trans (

v w

r v w

(

tc r v u

r u w))

(* ?

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

THEN asm_rewrite_tac[]);
a (all_fc_tac [tc_incr_thm]);
(* *** Goal "2.1.2" *** *)
a (

_tac

THEN asm_rewrite_tac[]);
a (REPEAT (all_asm_fc_tac [tran_tc_thm2,tc_incr_thm]));
(* *** Goal "2.1.3" *** *)
a (

_tac

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

]);
a (REPEAT strip_tac);
a (spec_nth_asm_tac 3

);
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

]);
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";

xl-holconst

well_founded: ('a

BOOL)

BOOL

well_founded r

(

r y x

s y)

s x)

s x

xl-holconst

twfp: ('a

BOOL)

BOOL

twfp r

well_founded r

trans r

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

(

tc r y x

(

tc r z y

s z)

s 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

(

tc r y x

(

tc r z y

s z)

s y)

(

tc r y x

s y)

ante_tac

THEN rewrite_tac[]

THEN REPEAT strip_tac);
a (fc_tac [list_

_elim [

] tc_decomp_thm]);
(* *** Goal "1" *** *)
a (spec_nth_asm_tac 7

);
(* *** 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

);
a (spec_nth_asm_tac 3

);
(* *** Goal "2" *** *)
a (spec_nth_asm_tac 8

);
(* *** 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 [

y''

] tran_tc_thm2));
a (spec_nth_asm_tac 12

y''

);
a (spec_nth_asm_tac 6

);
(* *** Goal "2.2" *** *)
a (asm_fc_tac[]);
val tcwf_lemma1 = save_pop_thm "tcwf_lemma1";

xl-sml

set_goal([],

well_founded r

(

tc r u t

s u)

s t)

(

s e)

);
a (REPEAT strip_tac THEN fc_tac [tcwf_lemma1]);
a (spec_nth_asm_tac 2

);
a (list_spec_nth_asm_tac 3 [

]);
a (spec_nth_asm_tac 7

);
a (spec_nth_asm_tac 4

);
val tcwf_lemma2 = save_pop_thm "tcwf_lemma2";

xl-sml

set_goal([],

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

);
a (list_spec_nth_asm_tac 4 [

]);
a (spec_nth_asm_tac 6

);
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([],

well_founded (tc r)

well_founded r

);
a (rewrite_tac [get_spec

well_founded

]

THEN REPEAT strip_tac);
a (spec_nth_asm_tac 2

);
(* *** Goal "1" *** *)
a (spec_nth_asm_tac 3

);
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([],

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";

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 = (

let

fun 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 = (

let

val ttac = (WF_INDUCTION_T thm strip_asm_tac)

handle ex => reraise ex "wf_induction_tac";

fn tm =>

let

val tac = (ttac tm) handle ex => reraise ex "wf_induction_tac";

fn gl => ((tac gl) handle ex => reraise ex "wf_induction_tac")

end

end
);

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([],

well_founded r

p v

p y

tc r y x

p z

r z y

);
a (strip_tac THEN strip_tac THEN strip_tac);
a (wf_induction_tac (asm_rule

well_founded r

)

);
a contr_tac;
a (all_asm_fc_tac[]);
a (spec_nth_asm_tac 6

);
a (SPEC_NTH_ASM_T 1

p x

tc r x v

ante_tac

THEN rewrite_tac[]

THEN REPEAT strip_tac);
a (

_tac

THEN REPEAT strip_tac);
(* *** Goal "1" *** *)
a (fc_tac [tc_incr_thm]);
(* *** Goal "2" *** *)
a (spec_nth_asm_tac 7

);
a (

_tac

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([],

well_founded r

p v

p y

p z

r z y

);
a (contr_tac);
a (lemma_tac

p x

THEN1 (strip_tac

THEN wf_induction_tac (asm_rule

well_founded r

)

));
(* *** 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([],

(

p v

p y

tc r y x

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

THEN rewrite_tac[]);
a (lemma_tac

rel

rel =

v w

s v

s w

r v w

THEN1 prove_

_tac);
a (

_tac

tc rel q x

THEN rewrite_tac[]);
a (spec_nth_asm_tac 3

);
a (

_tac

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

s x

] tc_p_thm)]);
(* *** Goal "3.2" *** *)
a (spec_nth_asm_tac 7

);
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 y

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

s x

ante_tac

THEN rewrite_tac[] THEN strip_tac);
a (spec_nth_asm_tac 1

);
a (spec_nth_asm_tac 4

);
a (spec_nth_asm_tac 3

);
val wf_induct_thm = save_pop_thm "wf_induct_thm";

Try a weaker hypothesis.

xl-sml

set_goal([],

(

p v

p y

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

tc rel q x

THEN rewrite_tac[]);
a (spec_nth_asm_tac 3

);
a (

_tac

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

s x

] tc_p_thm)]);
a (spec_nth_asm_tac 8

);
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";

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([],

(

p v

p y

tc r y x

p z

r z y)

(

r y x)

r z x

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

THEN

_tac

r w x

THEN

_tac

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

);
a (

_tac

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([],

(

p v

p y

p z

r z y)

(

p y)

p z

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

THEN

_tac

THEN asm_rewrite_tac[]);
a (REPEAT strip_tac);
a (spec_nth_asm_tac 2

);
a (

_tac

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([],

well_founded r

(

r y x)

r z x

r v z

r v x

);
a (REPEAT_N 2 strip_tac);
a (strip_asm_tac (

_elim

wf_nochain_thm));
a (ante_tac (

_elim

nochain_min_thm));
a (GET_NTH_ASM_T 1 ante_tac);
a (rewrite_tac [prove_rule []

a b

]);
val wf_min_thm = save_pop_thm "wf_min_thm";

But the converse does not hold.

xl-sml

set_goal([],

r: BOOL

BOOL

(

r y x)

r z x

r v z

r v x)

well_founded r

);
a (

_tac

x y:BOOL

THEN rewrite_tac [get_spec

well_founded

]

THEN REPEAT strip_tac);
(* *** Goal "1" *** *)
a (

_tac

THEN asm_rewrite_tac []);
(* *** Goal "2" *** *)
a (

_tac

THEN REPEAT strip_tac);
(* *** Goal "2.1" *** *)
a (spec_nth_asm_tac 1

);
(* *** Goal "2.2" *** *)
a (

_tac

THEN rewrite_tac[]);
val minr_not_wf_thm = save_pop_thm "minr_not_wf_thm";

xl-sml

set_goal([],

well_founded r

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 [

]);
(* *** Goal "1" *** *)
a (spec_nth_asm_tac 3

);
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

ante_tac

THEN (rewrite_tac []) THEN REPEAT strip_tac);
a (spec_nth_asm_tac 5

);
val wf_restrict_wf_thm = save_pop_thm "wf_restrict_wf_thm";

xl-sml

(* commit_pc "wf_relp"; *)