|
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
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⌝
</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"];
|
|
|
|
Definitions
|
xl-holconst trans: ('a → 'a → BOOL) → BOOL
|
∀ r •
trans r ≡ ∀ s t u• r s t ∧ r t u ⇒ r s u
|
|
xl-holconst tc: ('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
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";
|
|
|
|
Definitions
|
xl-holconst well_founded: ('a → 'a → BOOL) → BOOL
|
∀ r •
well_founded r ≡ ∀ s • (∀ x • (∀ y • r y x ⇒ s y) ⇒ s x) ⇒ ∀ x • s x
|
|
xl-holconst twfp: ('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([],⌜∀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.
And now we make a tactic out of that (basically by saying "strip the induction hypothesis into the assumptions").
|
|
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.
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.
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.
|
|
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.
A second order version with the weaker bottomless pits can be formulated as follows:
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⌝
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";
|
|
|
|
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
|
xl-sml
(* commit_pc "wf_relp"; *)
|
|
|
