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.

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

We here demonstrate certain results which properly belong to theories higher up the tree.

xl-sml set_goal([], ⌜∀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 ∧ ∀x• x∈ Dom r ∩ Dom s ⇒ ∀y• (x,y)∈r ≡ (x,y)∈s⌝); a (REPEAT_N 4 strip_tac THEN1 (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⌝ THEN spec_nth_asm_tac 4 ⌜Fst x⌝ THEN_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⌝ THEN spec_nth_asm_tac 4 ⌜Fst x⌝ THEN_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";

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

xl-holconst wf: (('a × 'a)SET)SET

∀ r • r ∈ wf ≡ ∀ s • (∀ x • (∀ y • (y,x) ∈ r ⇒ y ∈ s) ⇒ x ∈ s) ⇒ ∀ x • x ∈ s

xl-holconst twf: (('a × 'a)SET)SET

∀ r • r ∈ twf ≡ r ∈ wf ∧ r ∈ Transitive

xl-sml set_goal([],⌜∀s r• r ∈ wf ⇒ ∀x• (∀y• (y,x) ∈ r+ ⇒ (∀z• (z,y) ∈ r+ ⇒ z ∈ s) ⇒ y ∈ s) ⇒ (∀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) ⇒ (∀y• (y,x) ∈ r+ ⇒ y ∈ s)}⌝ THEN REPEAT strip_tac); (* *** Goal "1" *** *)

xl-gft (* 7 *) ⌜∀ s• (∀ x• (∀ y• (y, x) ∈ r ⇒ y ∈ s) ⇒ x ∈ s) ⇒ (∀ x• x ∈ s)⌝ (* 6 *) ⌜∀ y • (y, x) ∈ r ⇒ y ∈ {x |(∀ y• (y, x) ∈ r + ⇒ (∀ z• (z, y) ∈ r + ⇒ z ∈ s) ⇒ y ∈ s) ⇒ (∀ 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 • (y, x) ∈ r ⇒ y ∈ {x |(∀ y• (y, x) ∈ r + ⇒ (∀ z• (z, y) ∈ r + ⇒ z ∈ s) ⇒ y ∈ s) ⇒ (∀ 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 • (y, x) ∈ r ⇒ y ∈ {x |(∀ y• (y, x) ∈ r + ⇒ (∀ z• (z, y) ∈ r + ⇒ z ∈ s) ⇒ y ∈ s) ⇒ (∀ 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 • (y, x) ∈ r ⇒ y ∈ {x |(∀ y• (y, x) ∈ r + ⇒ (∀ z• (z, y) ∈ r + ⇒ z ∈ s) ⇒ y ∈ s) ⇒ (∀ 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 • (y, x) ∈ r ⇒ y ∈ {x |(∀ y• (y, x) ∈ r + ⇒ (∀ z• (z, y) ∈ r + ⇒ z ∈ s) ⇒ y ∈ s) ⇒ (∀ 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 • (y, x) ∈ r ⇒ y ∈ {x |(∀ y• (y, x) ∈ r + ⇒ (∀ z• (z, y) ∈ r + ⇒ z ∈ s) ⇒ y ∈ s) ⇒ (∀ 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 +⌝ THEN1 fc_tac [∈_tc_thm]); a (lemma_tac ⌜(y'', x) ∈ r +⌝ 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 "1.2.2" *** *)

xl-gft (* 10 *) ⌜∀ s• (∀ x• (∀ y• (y, x) ∈ r ⇒ y ∈ s) ⇒ x ∈ s) ⇒ (∀ x• x ∈ s)⌝ (* 9 *) ⌜∀ y • (y, x) ∈ r ⇒ y ∈ {x |(∀ y• (y, x) ∈ r + ⇒ (∀ z• (z, y) ∈ r + ⇒ z ∈ s) ⇒ y ∈ s) ⇒ (∀ 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 • x ∈ {x |(∀ y• (y, x) ∈ r + ⇒ (∀ z• (z, y) ∈ r + ⇒ z ∈ s) ⇒ y ∈ s) ⇒ (∀ 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 • x ∈ {x |(∀ y• (y, x) ∈ r + ⇒ (∀ z• (z, y) ∈ r + ⇒ z ∈ s) ⇒ y ∈ s) ⇒ (∀ 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 • x ∈ {x |(∀ y• (y, x) ∈ r + ⇒ (∀ z• (z, y) ∈ r + ⇒ z ∈ s) ⇒ y ∈ s) ⇒ (∀ 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";

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