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