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.
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.
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
qqco.gifGS → GS → BOOL⌝

so I would like a version of "well-founded" which has type:
xl-gft
qqco.gif('a → '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"];

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

xl-holconst
trans: ('a → 'a → BOOL) → BOOL
∀ r •
ftbr trans r ≡ ∀ s t u• r s t ∧ r t u ⇒ r s u

xl-holconst
tc: ('a → 'a → BOOL) → ('a → 'a → BOOL)
∀ r •
ftbr 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]
fttabTHEN 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⌝,
fttabget_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
fttabTHEN rewrite_tac [get_spec ⌜trans⌝]
fttabTHEN REPEAT strip_tac);
(* *** Goal "2.1.1" *** *)
a (∃_tac ⌜t⌝
fttabTHEN asm_rewrite_tac[]);
a (all_fc_tac [tc_incr_thm]);
(* *** Goal "2.1.2" *** *)
a (∃_tac ⌜u'⌝
fttabTHEN asm_rewrite_tac[]);
a (REPEAT (all_asm_fc_tac [tran_tc_thm2,tc_incr_thm]));
(* *** Goal "2.1.3" *** *)
a (∃_tac ⌜t⌝
fttabTHEN asm_rewrite_tac[]);
a (REPEAT(all_asm_fc_tac [tran_tc_thm2,tc_incr_thm]));
(* *** Goal "2.1.4" *** *)
a (∃_tac ⌜u''⌝
fttabTHEN 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
fttabTHEN asm_rewrite_tac []);
(* *** Goal "2.3" *** *)
a (swap_nth_asm_concl_tac 1
fttabTHEN 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)
fttab⇒ (∀ 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)
fttab⇒ (∀ 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⌝
fttab(fn x => strip_asm_tac (rewrite_rule[] x))
fttabTHEN_TRY all_asm_fc_tac[]);
a (swap_nth_asm_concl_tac 1
fttabTHEN rewrite_tac [get_spec ⌜trans⌝]
fttabTHEN 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-holconst
well_founded: ('a → 'a → BOOL) → BOOL
∀ r •
ftbr well_founded r ≡ ∀ s • (∀ x • (∀ y • r y x ⇒ s y) ⇒ s x) ⇒ ∀ x • s x

xl-holconst
twfp: ('a → 'a → BOOL) → BOOL
∀ r •
ftbr 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)
fttab⇒ (∀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)
fttab⇒ (∀y• tc r y x ⇒ s y)⌝ ante_tac
fttabTHEN rewrite_tac[]
fttabTHEN 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⌝
fttabTHEN1 fc_tac [tc_incr_thm]);
a (lemma_tac ⌜tc r y'' x⌝
fttabTHEN1 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
fttabTHEN 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⌝]
fttabTHEN 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 = (
fttabletfttabfun bad_thm thm = thm_fail "WF_INDUCTION_T" 29021 [thm];
fttabfttabval (wf, r) = (dest_app (concl thm))
fttabfttabfttabhandle Fail _ => bad_thm thm;
fttabfttabval sthm = ∀_elim r tcwf_lemma2
fttabfttabfttabhandle Fail _ => bad_thm thm;
fttabfttabval ithm = ⇒_elim sthm thm
fttabfttabfttabhandle Fail _ => bad_thm thm;
fttabin GEN_INDUCTION_T ithm ttac
fttabend
);

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 = (
fttabletfttabval ttac = (WF_INDUCTION_T thm strip_asm_tac)
fttabfttabfttabhandle ex => reraise ex "wf_induction_tac";
fttabin
fttabfn tm =>
fttabletfttabval tac = (ttac tm) handle ex => reraise ex "wf_induction_tac";
fttabinfttabfn gl => ((tac gl) handle ex => reraise ex "wf_induction_tac")
fttabend
fttabend
);

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
fttabTHEN rewrite_tac[]
fttabTHEN REPEAT strip_tac);
a (∃_tac ⌜z⌝
fttabTHEN 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
fttabTHEN wf_induction_tac (asm_rule ⌜well_founded r⌝) ⌜x⌝));
(* *** Goal "1" *** *)
a (contr_tac
fttabTHEN 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
fttabTHEN rewrite_tac[]
fttabTHEN strip_tac);
a (∃_tac ⌜x⌝
fttabTHEN rewrite_tac[]);
a (lemma_tac ⌜∃rel• rel = λ v w• ¬ s v ∧ ¬ s w ∧ r v w⌝
fttabTHEN1 prove_∃_tac);
a (∃_tac ⌜λq• tc rel q x⌝fttabTHEN 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⌝
fttabTHEN1 (strip_tac THEN strip_tac
fttabTHEN 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⌝
fttabTHEN1
fttab(REPEAT ∀_tac
fttabTHEN asm_rewrite_tac []
fttabTHEN 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'⌝
fttabTHEN1 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⌝]
fttabTHEN REPEAT strip_tac);
a (SPEC_NTH_ASM_T 2 ⌜λx• ¬ s x⌝ ante_tac
fttabTHEN 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
fttabTHEN rewrite_tac[]
fttabTHEN strip_tac);
a (lemma_tac ⌜∃rel• rel = λ v w• ¬ s v ∧ ¬ s w ∧ r v w⌝
fttabTHEN1 prove_∃_tac);
a (∃_tac ⌜λq• tc rel q x⌝fttabTHEN 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⌝
fttabTHEN1
fttab(REPEAT ∀_tac
fttabTHEN asm_rewrite_tac []
fttabTHEN 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)
fttab⇒ ∀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
fttabTHEN rewrite_tac[]
fttabTHEN REPEAT strip_tac
fttabTHEN rewrite_tac[]
);
a (∃_tac ⌜x⌝
fttabTHEN ∃_tac ⌜λw• r w x⌝
fttabTHEN ∃_tac ⌜y⌝
fttabTHEN 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)
fttab⇒ ∀p• (∃y• p y) ⇒ ∃z• p z ∧ ¬∃v• r v z ∧ p v⌝);
a contr_tac;
a (DROP_NTH_ASM_T 3 ante_tac
fttabTHEN rewrite_tac[]
fttabTHEN REPEAT strip_tac
);
a (∃_tac ⌜p⌝
fttabTHEN ∃_tac ⌜y⌝
fttabTHEN 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: BOOL→BOOL→BOOL•(∀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⌝
fttabTHEN rewrite_tac [get_spec ⌜well_founded⌝]
fttabTHEN 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⌝
fttabTHEN1 (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
fttabTHEN (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"; *)


up quick index © RBJ

privacy policy

Created:

$Id: x002.xml,v 1.6 2008/04/15 18:21:36 rbj01 Exp $

V