# HG changeset patch # User nipkow # Date 865514362 -7200 # Node ID c1f63cc3a7681af26dfd2a01c880cd79d20e5cfd # Parent 5b658dadf560385fe53314c650fe3c21c3b000fb Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'. Relation.ML Trancl.ML: more thms WF.ML WF.thy: added `acyclic' WF_Rel.ML: moved some thms back into WF and added some new ones. diff -r 5b658dadf560 -r c1f63cc3a768 src/HOL/Finite.ML --- a/src/HOL/Finite.ML Thu Jun 05 14:06:23 1997 +0200 +++ b/src/HOL/Finite.ML Thu Jun 05 14:39:22 1997 +0200 @@ -8,8 +8,9 @@ open Finite; -section "The finite powerset operator -- Fin"; +section "finite"; +(* goalw Finite.thy Fin.defs "!!A B. A<=B ==> Fin(A) <= Fin(B)"; by (rtac lfp_mono 1); by (REPEAT (ares_tac basic_monos 1)); @@ -21,124 +22,99 @@ (* A : Fin(B) ==> A <= B *) val FinD = Fin_subset_Pow RS subsetD RS PowD; +*) (*Discharging ~ x:y entails extra work*) val major::prems = goal Finite.thy - "[| F:Fin(A); P({}); \ -\ !!F x. [| x:A; F:Fin(A); x~:F; P(F) |] ==> P(insert x F) \ + "[| finite F; P({}); \ +\ !!F x. [| finite F; x ~: F; P(F) |] ==> P(insert x F) \ \ |] ==> P(F)"; -by (rtac (major RS Fin.induct) 1); -by (excluded_middle_tac "a:b" 2); +by (rtac (major RS Finites.induct) 1); +by (excluded_middle_tac "a:A" 2); by (etac (insert_absorb RS ssubst) 3 THEN assume_tac 3); (*backtracking!*) by (REPEAT (ares_tac prems 1)); -qed "Fin_induct"; +qed "finite_induct"; + +val major::prems = goal Finite.thy + "[| finite F; \ +\ P({}); \ +\ !!F a. [| finite F; a:A; a ~: F; P(F) |] ==> P(insert a F) \ +\ |] ==> F <= A --> P(F)"; +by (rtac (major RS finite_induct) 1); +by(ALLGOALS (blast_tac (!claset addIs prems))); +val lemma = result(); -Addsimps Fin.intrs; +val prems = goal Finite.thy + "[| finite F; F <= A; \ +\ P({}); \ +\ !!F a. [| finite F; a:A; a ~: F; P(F) |] ==> P(insert a F) \ +\ |] ==> P(F)"; +by(blast_tac (HOL_cs addIs ((lemma RS mp)::prems)) 1); +qed "finite_subset_induct"; + +Addsimps Finites.intrs; +AddSIs Finites.intrs; (*The union of two finite sets is finite*) val major::prems = goal Finite.thy - "[| F: Fin(A); G: Fin(A) |] ==> F Un G : Fin(A)"; -by (rtac (major RS Fin_induct) 1); + "[| finite F; finite G |] ==> finite(F Un G)"; +by (rtac (major RS finite_induct) 1); by (ALLGOALS (asm_simp_tac (!simpset addsimps (prems @ [Un_insert_left])))); -qed "Fin_UnI"; +qed "finite_UnI"; (*Every subset of a finite set is finite*) -val [subs,fin] = goal Finite.thy "[| A<=B; B: Fin(M) |] ==> A: Fin(M)"; -by (EVERY1 [subgoal_tac "ALL C. C<=B --> C: Fin(M)", +val [subs,fin] = goal Finite.thy "[| A<=B; finite B |] ==> finite A"; +by (EVERY1 [subgoal_tac "ALL C. C<=B --> finite C", rtac mp, etac spec, rtac subs]); -by (rtac (fin RS Fin_induct) 1); +by (rtac (fin RS finite_induct) 1); by (simp_tac (!simpset addsimps [subset_Un_eq]) 1); by (safe_tac (!claset addSDs [subset_insert_iff RS iffD1])); by (eres_inst_tac [("t","C")] (insert_Diff RS subst) 2); by (ALLGOALS Asm_simp_tac); -qed "Fin_subset"; +qed "finite_subset"; -goal Finite.thy "(F Un G : Fin(A)) = (F: Fin(A) & G: Fin(A))"; -by (blast_tac (!claset addIs [Fin_UnI] addDs - [Un_upper1 RS Fin_subset, Un_upper2 RS Fin_subset]) 1); -qed "subset_Fin"; -Addsimps[subset_Fin]; +goal Finite.thy "finite(F Un G) = (finite F & finite G)"; +by (blast_tac (!claset addIs [finite_UnI] addDs + [Un_upper1 RS finite_subset, Un_upper2 RS finite_subset]) 1); +qed "finite_Un"; +AddIffs[finite_Un]; -goal Finite.thy "(insert a A : Fin M) = (a:M & A : Fin M)"; +goal Finite.thy "finite(insert a A) = finite A"; by (stac insert_is_Un 1); -by (simp_tac (HOL_ss addsimps [subset_Fin]) 1); -by (blast_tac (!claset addSIs Fin.intrs addDs [FinD]) 1); -qed "insert_Fin"; -Addsimps[insert_Fin]; +by (simp_tac (HOL_ss addsimps [finite_Un]) 1); +by (blast_tac (!claset addSIs Finites.intrs) 1); +qed "finite_insert"; +Addsimps[finite_insert]; -(*The image of a finite set is finite*) -val major::_ = goal Finite.thy - "F: Fin(A) ==> h``F : Fin(h``A)"; -by (rtac (major RS Fin_induct) 1); +(*The image of a finite set is finite *) +goal Finite.thy "!!F. finite F ==> finite(h``F)"; +by (etac finite_induct 1); by (Simp_tac 1); -by (asm_simp_tac - (!simpset addsimps [image_eqI RS Fin.insertI, image_insert] - delsimps [insert_Fin]) 1); -qed "Fin_imageI"; +by (Asm_simp_tac 1); +qed "finite_imageI"; val major::prems = goal Finite.thy - "[| c: Fin(A); b: Fin(A); \ + "[| finite c; finite b; \ \ P(b); \ -\ !!(x::'a) y. [| x:A; y: Fin(A); x:y; P(y) |] ==> P(y-{x}) \ +\ !!x y. [| finite y; x:y; P(y) |] ==> P(y-{x}) \ \ |] ==> c<=b --> P(b-c)"; -by (rtac (major RS Fin_induct) 1); +by (rtac (major RS finite_induct) 1); by (stac Diff_insert 2); by (ALLGOALS (asm_simp_tac - (!simpset addsimps (prems@[Diff_subset RS Fin_subset])))); + (!simpset addsimps (prems@[Diff_subset RS finite_subset])))); val lemma = result(); val prems = goal Finite.thy - "[| b: Fin(A); \ -\ P(b); \ -\ !!x y. [| x:A; y: Fin(A); x:y; P(y) |] ==> P(y-{x}) \ + "[| finite A; \ +\ P(A); \ +\ !!a A. [| finite A; a:A; P(A) |] ==> P(A-{a}) \ \ |] ==> P({})"; by (rtac (Diff_cancel RS subst) 1); by (rtac (lemma RS mp) 1); by (REPEAT (ares_tac (subset_refl::prems) 1)); -qed "Fin_empty_induct"; - - -section "The predicate 'finite'"; - -val major::prems = goalw Finite.thy [finite_def] - "[| finite F; P({}); \ -\ !!F x. [| finite F; x~:F; P(F) |] ==> P(insert x F) \ -\ |] ==> P(F)"; -by (rtac (major RS Fin_induct) 1); -by (REPEAT (ares_tac prems 1)); -qed "finite_induct"; - - -goalw Finite.thy [finite_def] "finite {}"; -by (Simp_tac 1); -qed "finite_emptyI"; -Addsimps [finite_emptyI]; +qed "finite_empty_induct"; -goalw Finite.thy [finite_def] "!!A. finite A ==> finite(insert a A)"; -by (Asm_simp_tac 1); -qed "finite_insertI"; - -(*The union of two finite sets is finite*) -goalw Finite.thy [finite_def] - "!!F. [| finite F; finite G |] ==> finite(F Un G)"; -by (Asm_simp_tac 1); -qed "finite_UnI"; - -goalw Finite.thy [finite_def] "!!A. [| A<=B; finite B |] ==> finite A"; -by (etac Fin_subset 1); -by (assume_tac 1); -qed "finite_subset"; - -goalw Finite.thy [finite_def] "finite(F Un G) = (finite F & finite G)"; -by (Simp_tac 1); -qed "finite_Un_eq"; -Addsimps[finite_Un_eq]; - -goalw Finite.thy [finite_def] "finite(insert a A) = finite(A)"; -by (Simp_tac 1); -qed "finite_insert"; -Addsimps[finite_insert]; (* finite B ==> finite (B - Ba) *) bind_thm ("finite_Diff", Diff_subset RS finite_subset); @@ -152,25 +128,22 @@ qed "finite_Diff_singleton"; AddIffs [finite_Diff_singleton]; -(*The image of a finite set is finite*) -goal Finite.thy "!!F. finite F ==> finite(h``F)"; +(*** FIXME -> equalities.ML ***) +goal Set.thy "(f``A = {}) = (A = {})"; +by (blast_tac (!claset addSEs [equalityE]) 1); +qed "image_is_empty"; +Addsimps [image_is_empty]; + +goal Finite.thy "!!A. finite B ==> !A. f``A = B --> inj_onto f A --> finite A"; by (etac finite_induct 1); -by (ALLGOALS Asm_simp_tac); -qed "finite_imageI"; - -goal Finite.thy "!!A. finite B ==> !A. B = f``A --> inj_onto f A --> finite A"; -by (etac finite_induct 1); -by (ALLGOALS Asm_simp_tac); + by (ALLGOALS Asm_simp_tac); by (Step_tac 1); -by (subgoal_tac "A={}" 1); -by (blast_tac (!claset addSEs [equalityE]) 2); -by (subgoal_tac "EX y:A. f y = x & F = f``(A-{y})" 2); -by (Step_tac 1); -bw inj_onto_def; -by (Blast_tac 2); -by (ALLGOALS Asm_simp_tac); +by (subgoal_tac "EX y:A. f y = x & F = f``(A-{y})" 1); + by (Step_tac 1); + bw inj_onto_def; + by (Blast_tac 1); by (thin_tac "ALL A. ?PP(A)" 1); -by (forward_tac [[equalityD1, insertI1] MRS subsetD] 1); +by (forward_tac [[equalityD2, insertI1] MRS subsetD] 1); by (Step_tac 1); by (res_inst_tac [("x","xa")] bexI 1); by (ALLGOALS Asm_simp_tac); @@ -207,15 +180,6 @@ qed "finite_Pow_iff"; AddIffs [finite_Pow_iff]; -val major::prems = goalw Finite.thy [finite_def] - "[| finite A; \ -\ P(A); \ -\ !!a A. [| finite A; a:A; P(A) |] ==> P(A-{a}) \ -\ |] ==> P({})"; -by (rtac (major RS Fin_empty_induct) 1); -by (REPEAT (ares_tac (subset_refl::prems) 1)); -qed "finite_empty_induct"; - section "Finite cardinality -- 'card'"; @@ -346,7 +310,7 @@ by (Simp_tac 1); by (strip_tac 1); by (case_tac "x:B" 1); - by (dtac mk_disjoint_insert 1); + by (dres_inst_tac [("A","B")] mk_disjoint_insert 1); by (SELECT_GOAL(safe_tac (!claset))1); by (rotate_tac ~1 1); by (asm_full_simp_tac (!simpset addsimps [subset_insert_iff,finite_subset]) 1); @@ -439,7 +403,7 @@ by (etac conjE 1); by (case_tac "x:A" 1); (*1*) -by (dtac mk_disjoint_insert 1); +by (dres_inst_tac [("A","A")]mk_disjoint_insert 1); by (etac exE 1); by (etac conjE 1); by (hyp_subst_tac 1); diff -r 5b658dadf560 -r c1f63cc3a768 src/HOL/Finite.thy --- a/src/HOL/Finite.thy Thu Jun 05 14:06:23 1997 +0200 +++ b/src/HOL/Finite.thy Thu Jun 05 14:39:22 1997 +0200 @@ -8,18 +8,17 @@ Finite = Divides + Power + -consts Fin :: 'a set => 'a set set +consts Finites :: 'a set set -inductive "Fin(A)" +inductive "Finites" intrs - emptyI "{} : Fin(A)" - insertI "[| a: A; b: Fin(A) |] ==> insert a b : Fin(A)" + emptyI "{} : Finites" + insertI "A : Finites ==> insert a A : Finites" + +syntax finite :: 'a set => bool +translations "finite A" == "A : Finites" constdefs - - finite :: 'a set => bool - "finite A == A : Fin(UNIV)" - card :: 'a set => nat "card A == LEAST n. ? f. A = {f i |i. i P; \ +\ !!y. [| (x,y):r; (y,z):r^* |] ==> P \ +\ |] ==> P"; +by (subgoal_tac "x = z | (? y. (x,y) : r & (y,z) : r^*)" 1); +by (rtac (major RS converse_rtrancl_induct) 2); +by (blast_tac (!claset addIs prems) 2); +by (blast_tac (!claset addIs prems) 2); +by (REPEAT (eresolve_tac ([asm_rl,exE,disjE,conjE]@prems) 1)); +qed "rtranclE2"; + +goal Trancl.thy "r O r^* = r^* O r"; +by(Step_tac 1); + by(blast_tac (!claset addEs [rtranclE2] addIs [rtrancl_into_rtrancl]) 1); +by(blast_tac (!claset addEs [rtranclE] addIs [rtrancl_into_rtrancl2]) 1); +qed "r_comp_rtrancl_eq"; + (**** The relation trancl ****) +goalw Trancl.thy [trancl_def] "!!p.[| p:r^+; r <= s |] ==> p:s^+"; +by(blast_tac (!claset addIs [rtrancl_mono RS subsetD]) 1); +qed "trancl_mono"; + (** Conversions between trancl and rtrancl **) val [major] = goalw Trancl.thy [trancl_def] @@ -255,6 +277,11 @@ bind_thm ("trancl_trans", trans_trancl RS transD); +goalw Trancl.thy [trancl_def] + "!!r. [| (x,y):r^*; (y,z):r^+ |] ==> (x,z):r^+"; +by(blast_tac (!claset addIs [rtrancl_trans,r_into_rtrancl]) 1); +qed "rtrancl_trancl_trancl"; + val prems = goal Trancl.thy "[| (a,b) : r; (b,c) : r^+ |] ==> (a,c) : r^+"; by (rtac (r_into_trancl RS (trans_trancl RS transD)) 1); @@ -262,6 +289,26 @@ by (resolve_tac prems 1); qed "trancl_into_trancl2"; +(* primitive recursion for trancl over finite relations: *) +goal Trancl.thy "(insert (y,x) r)^+ = r^+ Un {(a,b). (a,y):r^* & (x,b):r^*}"; +br equalityI 1; + br subsetI 1; + by(split_all_tac 1); + be trancl_induct 1; + by(blast_tac (!claset addIs [r_into_trancl]) 1); + by(blast_tac (!claset addIs + [rtrancl_into_trancl1,trancl_into_rtrancl,r_into_trancl,trancl_trans]) 1); +br subsetI 1; +by(blast_tac (!claset addIs + [rtrancl_into_trancl2, rtrancl_trancl_trancl, + impOfSubs rtrancl_mono, trancl_mono]) 1); +qed "trancl_insert"; + +goalw Trancl.thy [trancl_def] "(converse r)^+ = converse(r^+)"; +by(simp_tac (!simpset addsimps [rtrancl_converse,converse_comp]) 1); +by(simp_tac (!simpset addsimps [rtrancl_converse RS sym,r_comp_rtrancl_eq]) 1); +qed "trancl_converse"; + val major::prems = goal Trancl.thy "[| (a,b) : r^*; r <= A Times A |] ==> a=b | a:A"; diff -r 5b658dadf560 -r c1f63cc3a768 src/HOL/WF.ML --- a/src/HOL/WF.ML Thu Jun 05 14:06:23 1997 +0200 +++ b/src/HOL/WF.ML Thu Jun 05 14:39:22 1997 +0200 @@ -84,6 +84,66 @@ by (blast_tac (!claset addSIs [lemma1, lemma2]) 1); qed "wf_eq_minimal"; +(*--------------------------------------------------------------------------- + * Wellfoundedness of subsets + *---------------------------------------------------------------------------*) + +goal thy "!!r. [| wf(r); p<=r |] ==> wf(p)"; +by (full_simp_tac (!simpset addsimps [wf_eq_minimal]) 1); +by (Fast_tac 1); +qed "wf_subset"; + +(*--------------------------------------------------------------------------- + * Wellfoundedness of the empty relation. + *---------------------------------------------------------------------------*) + +goal thy "wf({})"; +by (simp_tac (!simpset addsimps [wf_def]) 1); +qed "wf_empty"; +AddSIs [wf_empty]; + +(*--------------------------------------------------------------------------- + * Wellfoundedness of `insert' + *---------------------------------------------------------------------------*) + +goal WF.thy "wf(insert (y,x) r) = (wf(r) & (x,y) ~: r^*)"; +br iffI 1; + by(blast_tac (!claset addEs [wf_trancl RS wf_irrefl] addIs + [rtrancl_into_trancl1,wf_subset,impOfSubs rtrancl_mono]) 1); +by(asm_full_simp_tac (!simpset addsimps [wf_eq_minimal]) 1); +by(safe_tac (!claset)); +by(EVERY1[rtac allE, atac, etac impE, Blast_tac]); +be bexE 1; +by(rename_tac "a" 1); +by(case_tac "a = x" 1); + by(res_inst_tac [("x","a")]bexI 2); + ba 3; + by(Blast_tac 2); +by(case_tac "y:Q" 1); + by(Blast_tac 2); +by(res_inst_tac [("x","{z. z:Q & (z,y) : r^*}")]allE 1); + ba 1; +by(fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1); +qed "wf_insert"; +AddIffs [wf_insert]; + +(*** acyclic ***) + +goalw WF.thy [acyclic_def] + "!!r. wf r ==> acyclic r"; +by(blast_tac (!claset addEs [wf_trancl RS wf_irrefl]) 1); +qed "wf_acyclic"; + +goalw WF.thy [acyclic_def] + "acyclic(insert (y,x) r) = (acyclic r & (x,y) ~: r^*)"; +by(simp_tac (!simpset addsimps [trancl_insert]) 1); +by(blast_tac (!claset addEs [make_elim rtrancl_trans]) 1); +qed "acyclic_insert"; +AddIffs [acyclic_insert]; + +goalw WF.thy [acyclic_def] "acyclic(converse r) = acyclic r"; +by(simp_tac (!simpset addsimps [trancl_converse]) 1); +qed "acyclic_converse"; (** cut **) @@ -272,4 +332,3 @@ by (assume_tac 1); by (assume_tac 1); qed "tfl_wfrec"; - diff -r 5b658dadf560 -r c1f63cc3a768 src/HOL/WF.thy --- a/src/HOL/WF.thy Thu Jun 05 14:06:23 1997 +0200 +++ b/src/HOL/WF.thy Thu Jun 05 14:39:22 1997 +0200 @@ -12,6 +12,9 @@ wf :: "('a * 'a)set => bool" "wf(r) == (!P. (!x. (!y. (y,x):r --> P(y)) --> P(x)) --> (!x.P(x)))" + acyclic :: "('a*'a)set => bool" + "acyclic r == !x. (x,x) ~: r^+" + cut :: "('a => 'b) => ('a * 'a)set => 'a => 'a => 'b" "cut f r x == (%y. if (y,x):r then f y else arbitrary)" diff -r 5b658dadf560 -r c1f63cc3a768 src/HOL/WF_Rel.ML --- a/src/HOL/WF_Rel.ML Thu Jun 05 14:06:23 1997 +0200 +++ b/src/HOL/WF_Rel.ML Thu Jun 05 14:39:22 1997 +0200 @@ -63,15 +63,10 @@ * Wellfoundedness of lexicographic combinations *---------------------------------------------------------------------------*) -goal Prod.thy "!!P. !a b. P((a,b)) ==> !p. P(p)"; -by (rtac allI 1); -by (rtac (surjective_pairing RS ssubst) 1); -by (Blast_tac 1); -qed "split_all_pair"; - val [wfa,wfb] = goalw thy [wf_def,lex_prod_def] "[| wf(ra); wf(rb) |] ==> wf(ra**rb)"; -by (EVERY1 [rtac allI,rtac impI, rtac split_all_pair]); +by (EVERY1 [rtac allI,rtac impI]); +by (simp_tac (HOL_basic_ss addsimps [split_paired_All]) 1); by (rtac (wfa RS spec RS mp) 1); by (EVERY1 [rtac allI,rtac impI]); by (rtac (wfb RS spec RS mp) 1); @@ -80,25 +75,6 @@ AddSIs [wf_lex_prod]; (*--------------------------------------------------------------------------- - * Wellfoundedness of subsets - *---------------------------------------------------------------------------*) - -goal thy "!!r. [| wf(r); p<=r |] ==> wf(p)"; -by (full_simp_tac (!simpset addsimps [wf_eq_minimal]) 1); -by (Fast_tac 1); -qed "wf_subset"; - -(*--------------------------------------------------------------------------- - * Wellfoundedness of the empty relation. - *---------------------------------------------------------------------------*) - -goal thy "wf({})"; -by (simp_tac (!simpset addsimps [wf_def]) 1); -qed "wf_empty"; -AddSIs [wf_empty]; - - -(*--------------------------------------------------------------------------- * Transitivity of WF combinators. *---------------------------------------------------------------------------*) goalw thy [trans_def, lex_prod_def] @@ -124,3 +100,58 @@ by (Blast_tac 1); qed "trans_finite_psubset"; +(*--------------------------------------------------------------------------- + * Wellfoundedness of finite acyclic relations + * Cannot go into WF because it needs Finite + *---------------------------------------------------------------------------*) + +goal thy "!!r. finite r ==> acyclic r --> wf r"; +be finite_induct 1; + by(Blast_tac 1); +by(split_all_tac 1); +by(Asm_full_simp_tac 1); +qed_spec_mp "finite_acyclic_wf"; + +goal thy "!!r. finite r ==> wf r = acyclic r"; +by(blast_tac (!claset addIs [finite_acyclic_wf,wf_acyclic]) 1); +qed "wf_iff_acyclic_if_finite"; + + +(*--------------------------------------------------------------------------- + * A relation is wellfounded iff it has no infinite descending chain + *---------------------------------------------------------------------------*) + +goalw thy [wf_eq_minimal RS eq_reflection] + "wf r = (~(? f. !i. (f(Suc i),f i) : r))"; +br iffI 1; + br notI 1; + be exE 1; + by(eres_inst_tac [("x","{w. ? i. w=f i}")] allE 1); + by(Blast_tac 1); +be swap 1; +by(Asm_full_simp_tac 1); +be exE 1; +be swap 1; +br impI 1; +be swap 1; +be exE 1; +by(rename_tac "x" 1); +by(subgoal_tac + "!i. nat_rec x (%i y. @z. z:Q & (z,y):r) (Suc i) : Q & \ +\ (nat_rec x (%i y. @z. z:Q & (z,y):r) (Suc i),\ +\ nat_rec x (%i y. @z. z:Q & (z,y):r) i): r" 1); + by(Blast_tac 1); +br allI 1; +by(induct_tac "i" 1); + by(Asm_simp_tac 1); + by(subgoal_tac "? y. y : Q & (y,x):r" 1); + by(Blast_tac 2); + be exE 1; + be selectI 1; +by(subgoal_tac "? y.y:Q & (y,nat_rec x (%i y. @z. z:Q & (z,y):r)(Suc i)):r" 1); + by(Blast_tac 2); +by(Asm_full_simp_tac 1); +be exE 1; +(* `be selectI 1' takes a long time; hence the instantiation: *) +by (eres_inst_tac[("P","%u.u:Q & (u,?v):r")]selectI 1); +qed "wf_iff_no_infinite_down_chain";