Transitive and Well-Founded Relations
Overview
This is the theory of transitive and well founded relations as sets (using ProofPower's SET type constructor).
A new "wf_rel" theory is created as a child of "bin_rel". Probably
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_rel" theory is created as a child of "bin_rel". Probably
The Theory wf_rel
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 "bin_rel";
force_new_theory "wf_rel";
force_new_pc "wf_rel";
merge_pcs ["xl_cs_∃_conv"] "wf_rel";
set_merge_pcs ["hol", "'bin_rel", "wf_rel"];

Auxiliary Results
We here demonstrate certain results which properly belong to theories higher up the tree.
xl-sml
set_goal([],
fttab⌜∀f s• Dom (s ⊲ f) = s ∩ (Dom f)⌝
);
a (prove_tac [sets_ext_clauses, ∈_in_clauses]);
val Dom_rest_thm = save_pop_thm "Dom_rest_thm";

And a result about equality of binary relations:
xl-sml
set_goal([],⌜∀r s• r = s ≡ Dom r = Dom s ∧
fttab∀x• x∈ Dom r ∩ Dom s ⇒ ∀y• (x,y)∈r ≡ (x,y)∈s⌝);
a (REPEAT_N 4 strip_tac
fttabTHEN1 (strip_tac THEN asm_rewrite_tac[]));
a (rewrite_tac[sets_ext_clauses, ∈_in_clauses]);
a (REPEAT strip_tac);
(* *** Goal "1" *** *)
a (spec_nth_asm_tac 3 ⌜Fst x⌝
fttabTHEN spec_nth_asm_tac 4 ⌜Fst x⌝
fttabTHEN_TRY (SOLVED_T (asm_fc_tac[])));
a (SPEC_NTH_ASM_T 2 ⌜Snd x⌝ (strip_asm_tac o (rewrite_rule[])));
a (SPEC_NTH_ASM_T 3 ⌜Snd x⌝ (strip_asm_tac o (rewrite_rule[])));
a (SPEC_NTH_ASM_T 1 ⌜Snd x⌝ (strip_asm_tac o (rewrite_rule[])));
(* *** Goal "2" *** *)
a (spec_nth_asm_tac 3 ⌜Fst x⌝
fttabTHEN spec_nth_asm_tac 4 ⌜Fst x⌝
fttabTHEN_TRY (SOLVED_T (asm_fc_tac[])));
a (SPEC_NTH_ASM_T 1 ⌜Snd x⌝ (strip_asm_tac o (rewrite_rule[])));
a (SPEC_NTH_ASM_T 2 ⌜Snd x⌝ (strip_asm_tac o (rewrite_rule[])));
a (SPEC_NTH_ASM_T 1 ⌜Snd x⌝ (strip_asm_tac o (rewrite_rule[])));
val rel_ext_Dom_thm = save_pop_thm "rel_ext_Dom_thm";

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

xl-sml
set_goal([],⌜∀r• r+ ∈ Transitive⌝);
a (rewrite_tac(map get_spec [⌜$+⌝,⌜Transitive⌝]));
a (REPEAT strip_tac THEN REPEAT (all_asm_fc_tac[]));
val tran_tc_thm = save_pop_thm("tran_tc_thm");

set_goal([],⌜∀ r x y z• (x,y) ∈ r+ ∧ (y,z) ∈ r+ ⇒ (x,z) ∈ r+⌝);
a (prove_tac [rewrite_rule [get_spec ⌜Transitive⌝] tran_tc_thm]);
val tran_tc_thm2 = save_pop_thm("tran_tc_thm2");

set_goal([],⌜∀r • r ⊆ r+⌝);
a (prove_tac [get_spec ⌜$+⌝, sets_ext_clauses]);
val ⊆_tc_thm = save_pop_thm("⊆_tc_thm");

set_goal([],⌜∀r x y • (x,y) ∈ r ⇒ (x,y) ∈ r+⌝);
a (prove_tac [get_spec ⌜$+⌝, sets_ext_clauses]);
val ∈_tc_thm = save_pop_thm("∈_tc_thm");

set_goal([],⌜∀ r x y• (x,y) ∈ r+ ∧ ¬ (x,y) ∈ r ⇒ ∃z• (x,z) ∈ r+ ∧ (z,y) ∈ r⌝);
a (REPEAT strip_tac);
a (lemma_tac ⌜∀q• q ∈ Transitive ∧ r ⊆ q ⇒ (x,y) ∈ q⌝);
a (asm_ante_tac ⌜(x, y) ∈ r +⌝);
a (prove_tac [get_spec ⌜$+⌝, ∈_in_clauses]);
a (spec_nth_asm_tac 1 ⌜{(v, w) | (v,w) ∈ r ∨ ∃u• (v,u) ∈ r+ ∧ (u,w) ∈ r}⌝);
(* *** Goal "2.1" *** *)
a (spec_nth_asm_tac 1 ⌜x2⌝);
a (all_asm_fc_tac [∈_tc_thm]);
(* *** Goal "2.2" *** *)
a (spec_nth_asm_tac 1 ⌜u⌝);
a (REPEAT (all_fc_tac [tran_tc_thm2,∈_tc_thm]));
(* *** Goal "2.3" *** *)
a (spec_nth_asm_tac 1 ⌜x2⌝);
a (REPEAT (all_fc_tac [tran_tc_thm2,∈_tc_thm]));
(* *** Goal "2.4" *** *)
a (spec_nth_asm_tac 1 ⌜u'⌝);
a (REPEAT (all_fc_tac [tran_tc_thm2,∈_tc_thm]));
(* *** Goal "2.5" *** *)
a (DROP_NTH_ASM_T 1 (strip_asm_tac o (rewrite_rule[sets_ext_clauses])));
(* *** Goal "2.6" *** *)
a (∃_tac ⌜u⌝ THEN asm_rewrite_tac[]);
val tc_decomp_thm = save_pop_thm "tc_decomp_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
wf: (('a × 'a)SET)SET
∀ r •
ftbr r ∈ wf ≡ ∀ s •
ftbr (∀ x • (∀ y • (y,x) ∈ r ⇒ y ∈ s) ⇒ x ∈ s)
ftbr ⇒ ∀ x • x ∈ s

xl-holconst
twf: (('a × 'a)SET)SET
∀ r •
ftbr r ∈ twf ≡ r ∈ wf ∧ r ∈ Transitive
Theorems

xl-sml
set_goal([],⌜∀s r• r ∈ wf ⇒ ∀x• (∀y• (y,x) ∈ r+ ⇒ (∀z• (z,y) ∈ r+ ⇒ z ∈ s) ⇒ y ∈ s)
fttab⇒ (∀y• (y,x) ∈ r+ ⇒ y ∈ s)⌝);
a (pure_rewrite_tac [get_spec ⌜wf⌝, ∈_in_clauses]);
a (REPEAT_N 3 strip_tac);
a (spec_nth_asm_tac 1 ⌜{x | (∀y• (y,x) ∈ r+ ⇒ (∀z• (z,y) ∈ r+ ⇒ z ∈ s) ⇒ y ∈ s)
fttab⇒ (∀y• (y,x) ∈ r+ ⇒ y ∈ s)}⌝
fttabTHEN REPEAT strip_tac);
(* *** Goal "1" *** *)


xl-gft
(* 7 *) ⌜∀ s• (∀ x• (∀ y• (y, x) ∈ r ⇒ y ∈ s) ⇒ x ∈ s) ⇒ (∀ x• x ∈ s)⌝
(* 6 *) ⌜∀ y
ftbr • (y, x) ∈ r
ftbr ⇒ y
ftbr ∈ {x
ftbr |(∀ y• (y, x) ∈ r + ⇒ (∀ z• (z, y) ∈ r + ⇒ z ∈ s) ⇒ y ∈ s)
ftbr ⇒ (∀ y• (y, x) ∈ r + ⇒ y ∈ s)}⌝
(* 5 *) ⌜∀ y• (y, x) ∈ r + ⇒ (∀ z• (z, y) ∈ r + ⇒ z ∈ s) ⇒ y ∈ s⌝
(* 4 *) ⌜(y, x) ∈ r +
(* 3 *) ⌜¬ y ∈ s⌝
(* 2 *) ⌜∀ y• (y, x') ∈ r + ⇒ (∀ z• (z, y) ∈ r + ⇒ z ∈ s) ⇒ y ∈ s⌝
(* 1 *) ⌜(y', x') ∈ r +

(* ?⊢ *) ⌜y' ∈ s⌝


xl-sml
a (fc_tac [list_∀_elim [⌜r⌝,⌜y⌝,⌜x⌝] tc_decomp_thm]);
(* *** Goal "1.1" *** *)


xl-gft
(* 8 *) ⌜∀ s• (∀ x• (∀ y• (y, x) ∈ r ⇒ y ∈ s) ⇒ x ∈ s) ⇒ (∀ x• x ∈ s)⌝
(* 7 *) ⌜∀ y
ftbr • (y, x) ∈ r
ftbr ⇒ y
ftbr ∈ {x
ftbr |(∀ y• (y, x) ∈ r + ⇒ (∀ z• (z, y) ∈ r + ⇒ z ∈ s) ⇒ y ∈ s)
ftbr ⇒ (∀ y• (y, x) ∈ r + ⇒ y ∈ s)}⌝
(* 6 *) ⌜∀ y• (y, x) ∈ r + ⇒ (∀ z• (z, y) ∈ r + ⇒ z ∈ s) ⇒ y ∈ s⌝
(* 5 *) ⌜(y, x) ∈ r +
(* 4 *) ⌜¬ y ∈ s⌝
(* 3 *) ⌜∀ y• (y, x') ∈ r + ⇒ (∀ z• (z, y) ∈ r + ⇒ z ∈ s) ⇒ y ∈ s⌝
(* 2 *) ⌜(y', x') ∈ r +
(* 1 *) ⌜(y, x) ∈ r⌝

(* ?⊢ *) ⌜y' ∈ s⌝


xl-sml
a (spec_nth_asm_tac 7 ⌜y⌝);
(* *** Goal "1.1.1" *** *)


xl-gft
(* 11 *) ⌜∀ s• (∀ x• (∀ y• (y, x) ∈ r ⇒ y ∈ s) ⇒ x ∈ s) ⇒ (∀ x• x ∈ s)⌝
(* 10 *) ⌜∀ y
ftbr • (y, x) ∈ r
ftbr ⇒ y
ftbr ∈ {x
ftbr |(∀ y• (y, x) ∈ r + ⇒ (∀ z• (z, y) ∈ r + ⇒ z ∈ s) ⇒ y ∈ s)
ftbr ⇒ (∀ y• (y, x) ∈ r + ⇒ y ∈ s)}⌝
(* 9 *) ⌜∀ y• (y, x) ∈ r + ⇒ (∀ z• (z, y) ∈ r + ⇒ z ∈ s) ⇒ y ∈ s⌝
(* 8 *) ⌜(y, x) ∈ r +
(* 7 *) ⌜¬ y ∈ s⌝
(* 6 *) ⌜∀ y• (y, x') ∈ r + ⇒ (∀ z• (z, y) ∈ r + ⇒ z ∈ s) ⇒ y ∈ s⌝
(* 5 *) ⌜(y', x') ∈ r +
(* 4 *) ⌜(y, x) ∈ r⌝
(* 3 *) ⌜(y'', y) ∈ r +
(* 2 *) ⌜∀ z• (z, y'') ∈ r + ⇒ z ∈ s⌝
(* 1 *) ⌜¬ y'' ∈ s⌝

(* ?⊢ *) ⌜y' ∈ s⌝


xl-sml
a (all_fc_tac [tran_tc_thm2]);
a (spec_nth_asm_tac 10 ⌜y''⌝);
a (asm_fc_tac[]);
(* *** Goal "1.1.2" *** *)


xl-gft
(* 9 *) ⌜∀ s• (∀ x• (∀ y• (y, x) ∈ r ⇒ y ∈ s) ⇒ x ∈ s) ⇒ (∀ x• x ∈ s)⌝
(* 8 *) ⌜∀ y
ftbr • (y, x) ∈ r
ftbr ⇒ y
ftbr ∈ {x
ftbr |(∀ y• (y, x) ∈ r + ⇒ (∀ z• (z, y) ∈ r + ⇒ z ∈ s) ⇒ y ∈ s)
ftbr ⇒ (∀ y• (y, x) ∈ r + ⇒ y ∈ s)}⌝
(* 7 *) ⌜∀ y• (y, x) ∈ r + ⇒ (∀ z• (z, y) ∈ r + ⇒ z ∈ s) ⇒ y ∈ s⌝
(* 6 *) ⌜(y, x) ∈ r +
(* 5 *) ⌜¬ y ∈ s⌝
(* 4 *) ⌜∀ y• (y, x') ∈ r + ⇒ (∀ z• (z, y) ∈ r + ⇒ z ∈ s) ⇒ y ∈ s⌝
(* 3 *) ⌜(y', x') ∈ r +
(* 2 *) ⌜(y, x) ∈ r⌝
(* 1 *) ⌜∀ y'• (y', y) ∈ r + ⇒ y' ∈ s⌝

(* ?⊢ *) ⌜y' ∈ s⌝


xl-sml
a (spec_nth_asm_tac 7 ⌜y⌝);
a (spec_nth_asm_tac 3 ⌜z⌝);
(* *** Goal "1.2" *** *)


xl-gft
(* 9 *) ⌜∀ s• (∀ x• (∀ y• (y, x) ∈ r ⇒ y ∈ s) ⇒ x ∈ s) ⇒ (∀ x• x ∈ s)⌝
(* 8 *) ⌜∀ y
ftbr • (y, x) ∈ r
ftbr ⇒ y
ftbr ∈ {x
ftbr |(∀ y• (y, x) ∈ r + ⇒ (∀ z• (z, y) ∈ r + ⇒ z ∈ s) ⇒ y ∈ s)
ftbr ⇒ (∀ y• (y, x) ∈ r + ⇒ y ∈ s)}⌝
(* 7 *) ⌜∀ y• (y, x) ∈ r + ⇒ (∀ z• (z, y) ∈ r + ⇒ z ∈ s) ⇒ y ∈ s⌝
(* 6 *) ⌜(y, x) ∈ r +
(* 5 *) ⌜¬ y ∈ s⌝
(* 4 *) ⌜∀ y• (y, x') ∈ r + ⇒ (∀ z• (z, y) ∈ r + ⇒ z ∈ s) ⇒ y ∈ s⌝
(* 3 *) ⌜(y', x') ∈ r +
(* 2 *) ⌜(y, z) ∈ r +
(* 1 *) ⌜(z, x) ∈ r⌝

(* ?⊢ *) ⌜y' ∈ s⌝


xl-sml
a (spec_nth_asm_tac 8 ⌜z⌝);
(* *** Goal "1.2.1" *** *)


xl-gft
(* 12 *) ⌜∀ s• (∀ x• (∀ y• (y, x) ∈ r ⇒ y ∈ s) ⇒ x ∈ s) ⇒ (∀ x• x ∈ s)⌝
(* 11 *) ⌜∀ y
ftbr • (y, x) ∈ r
ftbr ⇒ y
ftbr ∈ {x
ftbr |(∀ y• (y, x) ∈ r + ⇒ (∀ z• (z, y) ∈ r + ⇒ z ∈ s) ⇒ y ∈ s)
ftbr ⇒ (∀ y• (y, x) ∈ r + ⇒ y ∈ s)}⌝
(* 10 *) ⌜∀ y• (y, x) ∈ r + ⇒ (∀ z• (z, y) ∈ r + ⇒ z ∈ s) ⇒ y ∈ s⌝
(* 9 *) ⌜(y, x) ∈ r +
(* 8 *) ⌜¬ y ∈ s⌝
(* 7 *) ⌜∀ y• (y, x') ∈ r + ⇒ (∀ z• (z, y) ∈ r + ⇒ z ∈ s) ⇒ y ∈ s⌝
(* 6 *) ⌜(y', x') ∈ r +
(* 5 *) ⌜(y, z) ∈ r +
(* 4 *) ⌜(z, x) ∈ r⌝
(* 3 *) ⌜(y'', z) ∈ r +
(* 2 *) ⌜∀ z• (z, y'') ∈ r + ⇒ z ∈ s⌝
(* 1 *) ⌜¬ y'' ∈ s⌝

(* ?⊢ *) ⌜y' ∈ s⌝


xl-sml
a (lemma_tac ⌜(z, x) ∈ r +
fttabTHEN1 fc_tac [∈_tc_thm]);
a (lemma_tac ⌜(y'', x) ∈ r +
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 "1.2.2" *** *)


xl-gft
(* 10 *) ⌜∀ s• (∀ x• (∀ y• (y, x) ∈ r ⇒ y ∈ s) ⇒ x ∈ s) ⇒ (∀ x• x ∈ s)⌝
(* 9 *) ⌜∀ y
ftbr • (y, x) ∈ r
ftbr ⇒ y
ftbr ∈ {x
ftbr |(∀ y• (y, x) ∈ r + ⇒ (∀ z• (z, y) ∈ r + ⇒ z ∈ s) ⇒ y ∈ s)
ftbr ⇒ (∀ y• (y, x) ∈ r + ⇒ y ∈ s)}⌝
(* 8 *) ⌜∀ y• (y, x) ∈ r + ⇒ (∀ z• (z, y) ∈ r + ⇒ z ∈ s) ⇒ y ∈ s⌝
(* 7 *) ⌜(y, x) ∈ r +
(* 6 *) ⌜¬ y ∈ s⌝
(* 5 *) ⌜∀ y• (y, x') ∈ r + ⇒ (∀ z• (z, y) ∈ r + ⇒ z ∈ s) ⇒ y ∈ s⌝
(* 4 *) ⌜(y', x') ∈ r +
(* 3 *) ⌜(y, z) ∈ r +
(* 2 *) ⌜(z, x) ∈ r⌝
(* 1 *) ⌜∀ y• (y, z) ∈ r + ⇒ y ∈ s⌝

(* ?⊢ *) ⌜y' ∈ s⌝


xl-sml
a (asm_fc_tac[]);
(* *** Goal "2" *** *)


xl-gft
(* 4 *) ⌜∀ s• (∀ x• (∀ y• (y, x) ∈ r ⇒ y ∈ s) ⇒ x ∈ s) ⇒ (∀ x• x ∈ s)⌝
(* 3 *) ⌜∀ x
ftbr • x
ftbr ∈ {x
ftbr |(∀ y• (y, x) ∈ r + ⇒ (∀ z• (z, y) ∈ r + ⇒ z ∈ s) ⇒ y ∈ s)
ftbr ⇒ (∀ y• (y, x) ∈ r + ⇒ y ∈ s)}⌝
(* 2 *) ⌜∀ y• (y, x) ∈ r + ⇒ (∀ z• (z, y) ∈ r + ⇒ z ∈ s) ⇒ y ∈ s⌝
(* 1 *) ⌜(y, x) ∈ r +

(* ?⊢ *) ⌜y ∈ s⌝


xl-sml
a (spec_nth_asm_tac 3 ⌜x⌝);
(* *** Goal "2.1" *** *)


xl-gft
(* 7 *) ⌜∀ s• (∀ x• (∀ y• (y, x) ∈ r ⇒ y ∈ s) ⇒ x ∈ s) ⇒ (∀ x• x ∈ s)⌝
(* 6 *) ⌜∀ x
ftbr • x
ftbr ∈ {x
ftbr |(∀ y• (y, x) ∈ r + ⇒ (∀ z• (z, y) ∈ r + ⇒ z ∈ s) ⇒ y ∈ s)
ftbr ⇒ (∀ y• (y, x) ∈ r + ⇒ y ∈ s)}⌝
(* 5 *) ⌜∀ y• (y, x) ∈ r + ⇒ (∀ z• (z, y) ∈ r + ⇒ z ∈ s) ⇒ y ∈ s⌝
(* 4 *) ⌜(y, x) ∈ r +
(* 3 *) ⌜(y', x) ∈ r +
(* 2 *) ⌜∀ z• (z, y') ∈ r + ⇒ z ∈ s⌝
(* 1 *) ⌜¬ y' ∈ s⌝

(* ?⊢ *) ⌜y ∈ s⌝


xl-sml
a (spec_nth_asm_tac 5 ⌜y'⌝);
a (asm_fc_tac[]);
(* *** Goal "2.2" *** *)


xl-gft
(* 5 *) ⌜∀ s• (∀ x• (∀ y• (y, x) ∈ r ⇒ y ∈ s) ⇒ x ∈ s) ⇒ (∀ x• x ∈ s)⌝
(* 4 *) ⌜∀ x
ftbr • x
ftbr ∈ {x
ftbr |(∀ y• (y, x) ∈ r + ⇒ (∀ z• (z, y) ∈ r + ⇒ z ∈ s) ⇒ y ∈ s)
ftbr ⇒ (∀ y• (y, x) ∈ r + ⇒ y ∈ s)}⌝
(* 3 *) ⌜∀ y• (y, x) ∈ r + ⇒ (∀ z• (z, y) ∈ r + ⇒ z ∈ s) ⇒ y ∈ s⌝
(* 2 *) ⌜(y, x) ∈ r +
(* 1 *) ⌜∀ y• (y, x) ∈ r + ⇒ y ∈ s⌝

(* ?⊢ *) ⌜y ∈ s⌝


xl-sml
a (asm_fc_tac[]);
val tcwf_lemma1 = save_pop_thm "tcwf_lemma1";

set_goal([],⌜∀r• r ∈ wf ⇒ ∀s• (∀t• (∀u• (u,t) ∈ r+ ⇒ u ∈ s) ⇒ t ∈ s) ⇒ (∀e• e ∈ s)⌝);
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";

set_goal([],⌜∀r• r ∈ wf ⇒ r+ ∈ twf⌝);
a (REPEAT strip_tac);
a (fc_tac [tcwf_lemma2]);
a (pure_rewrite_tac [get_spec ⌜twf⌝,get_spec ⌜wf⌝, tran_tc_thm]);
a (REPEAT strip_tac);
a (list_spec_nth_asm_tac 2 [⌜s⌝,⌜x⌝]);
a (spec_nth_asm_tac 3 ⌜t⌝);
a (spec_nth_asm_tac 4 ⌜y⌝);
val tc_wf_twf_thm = save_pop_thm "tc_wf_twf_thm";

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

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


up quick index © RBJ

privacy policy

Created:

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

V