# HG changeset patch # User paulson # Date 1021887957 -7200 # Node ID 31d020705affb41774424e7294762bef9ef2ea0f # Parent dfc399c684e498594bf0f197f7ea6b687e9dc2f3 conversion of equalities and WF to Isar diff -r dfc399c684e4 -r 31d020705aff src/ZF/IsaMakefile --- a/src/ZF/IsaMakefile Sat May 18 22:22:23 2002 +0200 +++ b/src/ZF/IsaMakefile Mon May 20 11:45:57 2002 +0200 @@ -44,9 +44,9 @@ Sum.thy Tools/cartprod.ML Tools/datatype_package.ML \ Tools/ind_cases.ML Tools/induct_tacs.ML Tools/inductive_package.ML \ Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/typechk.ML \ - Trancl.ML Trancl.thy Univ.thy Update.ML Update.thy WF.ML \ + Trancl.ML Trancl.thy Univ.thy Update.ML Update.thy \ WF.thy ZF.ML ZF.thy Zorn.thy arith_data.ML domrange.ML \ - domrange.thy equalities.ML equalities.thy func.thy \ + domrange.thy equalities.thy func.thy \ ind_syntax.ML mono.ML mono.thy pair.ML pair.thy simpdata.ML \ subset.ML subset.thy thy_syntax.ML upair.ML upair.thy @$(ISATOOL) usedir -b -r $(OUT)/FOL ZF diff -r dfc399c684e4 -r 31d020705aff src/ZF/WF.thy --- a/src/ZF/WF.thy Sat May 18 22:22:23 2002 +0200 +++ b/src/ZF/WF.thy Mon May 20 11:45:57 2002 +0200 @@ -1,38 +1,394 @@ -(* Title: ZF/wf.thy +(* Title: ZF/WF.thy ID: $Id$ Author: Tobias Nipkow and Lawrence C Paulson Copyright 1994 University of Cambridge Well-founded Recursion + +Derived first for transitive relations, and finally for arbitrary WF relations +via wf_trancl and trans_trancl. + +It is difficult to derive this general case directly, using r^+ instead of +r. In is_recfun, the two occurrences of the relation must have the same +form. Inserting r^+ in the_recfun or wftrec yields a recursion rule with +r^+ -`` {a} instead of r-``{a}. This recursion rule is stronger in +principle, but harder to use, especially to prove wfrec_eclose_eq in +epsilon.ML. Expanding out the definition of wftrec in wfrec would yield +a mess. *) -WF = Trancl + mono + equalities + -consts - wf :: i=>o - wf_on :: [i,i]=>o ("wf[_]'(_')") +theory WF = Trancl + mono + equalities: + +constdefs + wf :: "i=>o" + (*r is a well-founded relation*) + "wf(r) == ALL Z. Z=0 | (EX x:Z. ALL y. :r --> ~ y:Z)" + + wf_on :: "[i,i]=>o" ("wf[_]'(_')") + (*r is well-founded on A*) + "wf_on(A,r) == wf(r Int A*A)" + + is_recfun :: "[i, i, [i,i]=>i, i] =>o" + "is_recfun(r,a,H,f) == (f = (lam x: r-``{a}. H(x, restrict(f, r-``{x}))))" + + the_recfun :: "[i, i, [i,i]=>i] =>i" + "the_recfun(r,a,H) == (THE f. is_recfun(r,a,H,f))" + + wftrec :: "[i, i, [i,i]=>i] =>i" + "wftrec(r,a,H) == H(a, the_recfun(r,a,H))" + + wfrec :: "[i, i, [i,i]=>i] =>i" + (*public version. Does not require r to be transitive*) + "wfrec(r,a,H) == wftrec(r^+, a, %x f. H(x, restrict(f,r-``{x})))" + + wfrec_on :: "[i, i, i, [i,i]=>i] =>i" ("wfrec[_]'(_,_,_')") + "wfrec[A](r,a,H) == wfrec(r Int A*A, a, H)" + + +(*** Well-founded relations ***) + +(** Equivalences between wf and wf_on **) + +lemma wf_imp_wf_on: "wf(r) ==> wf[A](r)" +apply (unfold wf_def wf_on_def, clarify) (*needed for blast's efficiency*) +apply blast +done + +lemma wf_on_field_imp_wf: "wf[field(r)](r) ==> wf(r)" +by (unfold wf_def wf_on_def, fast) + +lemma wf_iff_wf_on_field: "wf(r) <-> wf[field(r)](r)" +by (blast intro: wf_imp_wf_on wf_on_field_imp_wf) + +lemma wf_on_subset_A: "[| wf[A](r); B<=A |] ==> wf[B](r)" +by (unfold wf_on_def wf_def, fast) + +lemma wf_on_subset_r: "[| wf[A](r); s<=r |] ==> wf[A](s)" +by (unfold wf_on_def wf_def, fast) + +(** Introduction rules for wf_on **) + +lemma wf_onI: +(*If every non-empty subset of A has an r-minimal element then wf[A](r).*) + assumes prem: "!!Z u. [| Z<=A; u:Z; ALL x:Z. EX y:Z. :r |] ==> False" + shows "wf[A](r)" +apply (unfold wf_on_def wf_def) +apply (rule equals0I [THEN disjCI, THEN allI]) +apply (rule_tac Z = "Z" in prem, blast+) +done + +(*If r allows well-founded induction over A then wf[A](r) + Premise is equivalent to + !!B. ALL x:A. (ALL y. : r --> y:B) --> x:B ==> A<=B *) +lemma wf_onI2: + assumes prem: "!!y B. [| ALL x:A. (ALL y:A. :r --> y:B) --> x:B; y:A |] + ==> y:B" + shows "wf[A](r)" +apply (rule wf_onI) +apply (rule_tac c=u in prem [THEN DiffE]) + prefer 3 apply blast + apply fast+ +done + + +(** Well-founded Induction **) + +(*Consider the least z in domain(r) Un {a} such that P(z) does not hold...*) +lemma wf_induct: + "[| wf(r); + !!x.[| ALL y. : r --> P(y) |] ==> P(x) + |] ==> P(a)" +apply (unfold wf_def) +apply (erule_tac x = "{z:domain (r) Un {a}. ~P (z) }" in allE) +apply blast +done - wftrec,wfrec :: [i, i, [i,i]=>i] =>i - wfrec_on :: [i, i, i, [i,i]=>i] =>i ("wfrec[_]'(_,_,_')") - is_recfun :: [i, i, [i,i]=>i, i] =>o - the_recfun :: [i, i, [i,i]=>i] =>i +(*The form of this rule is designed to match wfI*) +lemma wf_induct2: + "[| wf(r); a:A; field(r)<=A; + !!x.[| x: A; ALL y. : r --> P(y) |] ==> P(x) |] + ==> P(a)" +apply (erule_tac P="a:A" in rev_mp) +apply (erule_tac a=a in wf_induct, blast) +done + +lemma field_Int_square: "field(r Int A*A) <= A" +by blast + +lemma wf_on_induct: + "[| wf[A](r); a:A; + !!x.[| x: A; ALL y:A. : r --> P(y) |] ==> P(x) + |] ==> P(a)" +apply (unfold wf_on_def) +apply (erule wf_induct2, assumption) +apply (rule field_Int_square, blast) +done + +(*If r allows well-founded induction then wf(r)*) +lemma wfI: + "[| field(r)<=A; + !!y B. [| ALL x:A. (ALL y:A. :r --> y:B) --> x:B; y:A|] + ==> y:B |] + ==> wf(r)" +apply (rule wf_on_subset_A [THEN wf_on_field_imp_wf]) +apply (rule wf_onI2) + prefer 2 apply blast +apply blast +done + + +(*** Properties of well-founded relations ***) + +lemma wf_not_refl: "wf(r) ==> ~: r" +by (erule_tac a=a in wf_induct, blast) + +lemma wf_not_sym [rule_format]: "wf(r) ==> ALL x. :r --> ~: r" +by (erule_tac a=a in wf_induct, blast) + +(* [| wf(r); : r; ~P ==> : r |] ==> P *) +lemmas wf_asym = wf_not_sym [THEN swap, standard] + +lemma wf_on_not_refl: "[| wf[A](r); a: A |] ==> ~: r" +apply (erule_tac a=a in wf_on_induct, assumption) +apply blast +done -defs - (*r is a well-founded relation*) - wf_def "wf(r) == ALL Z. Z=0 | (EX x:Z. ALL y. :r --> ~ y:Z)" +lemma wf_on_not_sym [rule_format]: + "[| wf[A](r); a:A |] ==> ALL b:A. :r --> ~:r" +apply (erule_tac a=a in wf_on_induct, assumption) +apply blast +done + +lemma wf_on_asym: + "[| wf[A](r); ~Z ==> : r; + ~: r ==> Z; ~Z ==> a : A; ~Z ==> b : A |] ==> Z" +by (blast dest: wf_on_not_sym); + + +(*Needed to prove well_ordI. Could also reason that wf[A](r) means + wf(r Int A*A); thus wf( (r Int A*A)^+ ) and use wf_not_refl *) +lemma wf_on_chain3: + "[| wf[A](r); :r; :r; :r; a:A; b:A; c:A |] ==> P" +apply (subgoal_tac "ALL y:A. ALL z:A. :r --> :r --> :r --> P", + blast) +apply (erule_tac a=a in wf_on_induct, assumption) +apply blast +done + + + + +(*transitive closure of a WF relation is WF provided A is downwards closed*) +lemma wf_on_trancl: + "[| wf[A](r); r-``A <= A |] ==> wf[A](r^+)" +apply (rule wf_onI2) +apply (frule bspec [THEN mp], assumption+) +apply (erule_tac a = "y" in wf_on_induct, assumption) +apply (blast elim: tranclE, blast) +done + +lemma wf_trancl: "wf(r) ==> wf(r^+)" +apply (simp add: wf_iff_wf_on_field) +apply (rule wf_on_subset_A) + apply (erule wf_on_trancl) + apply blast +apply (rule trancl_type [THEN field_rel_subset]) +done + + + +(** r-``{a} is the set of everything under a in r **) + +lemmas underI = vimage_singleton_iff [THEN iffD2, standard] +lemmas underD = vimage_singleton_iff [THEN iffD1, standard] + +(** is_recfun **) - (*r is well-founded relation over A*) - wf_on_def "wf_on(A,r) == wf(r Int A*A)" +lemma is_recfun_type: "is_recfun(r,a,H,f) ==> f: r-``{a} -> range(f)" +apply (unfold is_recfun_def) +apply (erule ssubst) +apply (rule lamI [THEN rangeI, THEN lam_type], assumption) +done + +lemma apply_recfun: + "[| is_recfun(r,a,H,f); :r |] ==> f`x = H(x, restrict(f,r-``{x}))" +apply (unfold is_recfun_def) +apply (erule_tac P = "%x.?t (x) = (?u::i) " in ssubst) +apply (erule underI [THEN beta]) +done + +lemma is_recfun_equal [rule_format]: + "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,b,H,g) |] + ==> :r --> :r --> f`x=g`x" +apply (frule_tac f = "f" in is_recfun_type) +apply (frule_tac f = "g" in is_recfun_type) +apply (simp add: is_recfun_def) +apply (erule_tac a=x in wf_induct) +apply (intro impI) +apply (elim ssubst) +apply (simp (no_asm_simp) add: vimage_singleton_iff restrict_def) +apply (rule_tac t = "%z. H (?x,z) " in subst_context) +apply (subgoal_tac "ALL y : r-``{x}. ALL z. :f <-> :g") + apply (blast dest: transD) +apply (simp add: apply_iff) +apply (blast dest: transD intro: sym) +done + +lemma is_recfun_cut: + "[| wf(r); trans(r); + is_recfun(r,a,H,f); is_recfun(r,b,H,g); :r |] + ==> restrict(f, r-``{b}) = g" +apply (frule_tac f = "f" in is_recfun_type) +apply (rule fun_extension) + apply (blast dest: transD intro: restrict_type2) + apply (erule is_recfun_type, simp) +apply (blast dest: transD intro: is_recfun_equal) +done + +(*** Main Existence Lemma ***) - is_recfun_def "is_recfun(r,a,H,f) == - (f = (lam x: r-``{a}. H(x, restrict(f, r-``{x}))))" +lemma is_recfun_functional: + "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,a,H,g) |] ==> f=g" +by (blast intro: fun_extension is_recfun_type is_recfun_equal) + +(*If some f satisfies is_recfun(r,a,H,-) then so does the_recfun(r,a,H) *) +lemma is_the_recfun: + "[| is_recfun(r,a,H,f); wf(r); trans(r) |] + ==> is_recfun(r, a, H, the_recfun(r,a,H))" +apply (unfold the_recfun_def) +apply (rule ex1I [THEN theI], assumption) +apply (blast intro: is_recfun_functional) +done + +lemma unfold_the_recfun: + "[| wf(r); trans(r) |] ==> is_recfun(r, a, H, the_recfun(r,a,H))" +apply (rule_tac a=a in wf_induct, assumption) +apply (rename_tac a1) +apply (rule_tac f = "lam y: r-``{a1}. wftrec (r,y,H)" in is_the_recfun) + apply typecheck +apply (unfold is_recfun_def wftrec_def) +(*Applying the substitution: must keep the quantified assumption!!*) +apply (rule lam_cong [OF refl]) +apply (drule underD) +apply (fold is_recfun_def) +apply (rule_tac t = "%z. H(?x,z)" in subst_context) +apply (rule fun_extension) + apply (blast intro: is_recfun_type) + apply (rule lam_type [THEN restrict_type2]) + apply blast + apply (blast dest: transD) +apply (frule spec [THEN mp], assumption) +apply (subgoal_tac " : r") + apply (drule_tac x1 = "xa" in spec [THEN mp], assumption) +apply (simp add: vimage_singleton_iff underI [THEN beta] + apply_recfun is_recfun_cut) +apply (blast dest: transD) +done + + +(*** Unfolding wftrec ***) + +lemma the_recfun_cut: + "[| wf(r); trans(r); :r |] + ==> restrict(the_recfun(r,a,H), r-``{b}) = the_recfun(r,b,H)" +by (blast intro: is_recfun_cut unfold_the_recfun); - the_recfun_def "the_recfun(r,a,H) == (THE f. is_recfun(r,a,H,f))" +(*NOT SUITABLE FOR REWRITING: it is recursive!*) +lemma wftrec: + "[| wf(r); trans(r) |] ==> + wftrec(r,a,H) = H(a, lam x: r-``{a}. wftrec(r,x,H))" +apply (unfold wftrec_def) +apply (subst unfold_the_recfun [unfolded is_recfun_def]) +apply (simp_all add: vimage_singleton_iff [THEN iff_sym] the_recfun_cut) +done + +(** Removal of the premise trans(r) **) + +(*NOT SUITABLE FOR REWRITING: it is recursive!*) +lemma wfrec: + "wf(r) ==> wfrec(r,a,H) = H(a, lam x:r-``{a}. wfrec(r,x,H))" +apply (unfold wfrec_def) +apply (erule wf_trancl [THEN wftrec, THEN ssubst]) + apply (rule trans_trancl) +apply (rule vimage_pair_mono [THEN restrict_lam_eq, THEN subst_context]) + apply (erule r_into_trancl) +apply (rule subset_refl) +done - wftrec_def "wftrec(r,a,H) == H(a, the_recfun(r,a,H))" +(*This form avoids giant explosions in proofs. NOTE USE OF == *) +lemma def_wfrec: + "[| !!x. h(x)==wfrec(r,x,H); wf(r) |] ==> + h(a) = H(a, lam x: r-``{a}. h(x))" +apply simp +apply (elim wfrec) +done + +lemma wfrec_type: + "[| wf(r); a:A; field(r)<=A; + !!x u. [| x: A; u: Pi(r-``{x}, B) |] ==> H(x,u) : B(x) + |] ==> wfrec(r,a,H) : B(a)" +apply (rule_tac a = "a" in wf_induct2, assumption+) +apply (subst wfrec, assumption) +apply (simp add: lam_type underD) +done + + +lemma wfrec_on: + "[| wf[A](r); a: A |] ==> + wfrec[A](r,a,H) = H(a, lam x: (r-``{a}) Int A. wfrec[A](r,x,H))" +apply (unfold wf_on_def wfrec_on_def) +apply (erule wfrec [THEN trans]) +apply (simp add: vimage_Int_square cons_subset_iff) +done - (*public version. Does not require r to be transitive*) - wfrec_def "wfrec(r,a,H) == wftrec(r^+, a, %x f. H(x, restrict(f,r-``{x})))" +(*Minimal-element characterization of well-foundedness*) +lemma wf_eq_minimal: + "wf(r) <-> (ALL Q x. x:Q --> (EX z:Q. ALL y. :r --> y~:Q))" +apply (unfold wf_def, blast) +done + +ML +{* +val wf_def = thm "wf_def"; +val wf_on_def = thm "wf_on_def"; - wfrec_on_def "wfrec[A](r,a,H) == wfrec(r Int A*A, a, H)" +val wf_imp_wf_on = thm "wf_imp_wf_on"; +val wf_on_field_imp_wf = thm "wf_on_field_imp_wf"; +val wf_iff_wf_on_field = thm "wf_iff_wf_on_field"; +val wf_on_subset_A = thm "wf_on_subset_A"; +val wf_on_subset_r = thm "wf_on_subset_r"; +val wf_onI = thm "wf_onI"; +val wf_onI2 = thm "wf_onI2"; +val wf_induct = thm "wf_induct"; +val wf_induct2 = thm "wf_induct2"; +val field_Int_square = thm "field_Int_square"; +val wf_on_induct = thm "wf_on_induct"; +val wfI = thm "wfI"; +val wf_not_refl = thm "wf_not_refl"; +val wf_not_sym = thm "wf_not_sym"; +val wf_asym = thm "wf_asym"; +val wf_on_not_refl = thm "wf_on_not_refl"; +val wf_on_not_sym = thm "wf_on_not_sym"; +val wf_on_asym = thm "wf_on_asym"; +val wf_on_chain3 = thm "wf_on_chain3"; +val wf_on_trancl = thm "wf_on_trancl"; +val wf_trancl = thm "wf_trancl"; +val underI = thm "underI"; +val underD = thm "underD"; +val is_recfun_type = thm "is_recfun_type"; +val apply_recfun = thm "apply_recfun"; +val is_recfun_equal = thm "is_recfun_equal"; +val is_recfun_cut = thm "is_recfun_cut"; +val is_recfun_functional = thm "is_recfun_functional"; +val is_the_recfun = thm "is_the_recfun"; +val unfold_the_recfun = thm "unfold_the_recfun"; +val the_recfun_cut = thm "the_recfun_cut"; +val wftrec = thm "wftrec"; +val wfrec = thm "wfrec"; +val def_wfrec = thm "def_wfrec"; +val wfrec_type = thm "wfrec_type"; +val wfrec_on = thm "wfrec_on"; +val wf_eq_minimal = thm "wf_eq_minimal"; +*} end diff -r dfc399c684e4 -r 31d020705aff src/ZF/equalities.thy --- a/src/ZF/equalities.thy Sat May 18 22:22:23 2002 +0200 +++ b/src/ZF/equalities.thy Mon May 20 11:45:57 2002 +0200 @@ -1,4 +1,761 @@ -(*Dummy theory to document dependencies *) +(* Title: ZF/equalities + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1992 University of Cambridge + +Set Theory examples: Union, Intersection, Inclusion, etc. + (Thanks also to Philippe de Groote.) +*) + +theory equalities = domrange: + +(** Finite Sets **) + +(* cons_def refers to Upair; reversing the equality LOOPS in rewriting!*) +lemma cons_eq: "{a} Un B = cons(a,B)" +by blast + +lemma cons_commute: "cons(a, cons(b, C)) = cons(b, cons(a, C))" +by blast + +lemma cons_absorb: "a: B ==> cons(a,B) = B" +by blast + +lemma cons_Diff: "a: B ==> cons(a, B-{a}) = B" +by blast + +lemma equal_singleton [rule_format]: "[| a: C; ALL y:C. y=b |] ==> C = {b}" +by blast + + +(** Binary Intersection **) + +(*NOT an equality, but it seems to belong here...*) +lemma Int_cons: "cons(a,B) Int C <= cons(a, B Int C)" +by blast + +lemma Int_absorb [simp]: "A Int A = A" +by blast + +lemma Int_left_absorb: "A Int (A Int B) = A Int B" +by blast + +lemma Int_commute: "A Int B = B Int A" +by blast + +lemma Int_left_commute: "A Int (B Int C) = B Int (A Int C)" +by blast + +lemma Int_assoc: "(A Int B) Int C = A Int (B Int C)" +by blast + +(*Intersection is an AC-operator*) +lemmas Int_ac= Int_assoc Int_left_absorb Int_commute Int_left_commute + +lemma Int_Un_distrib: "A Int (B Un C) = (A Int B) Un (A Int C)" +by blast + +lemma Int_Un_distrib2: "(B Un C) Int A = (B Int A) Un (C Int A)" +by blast + +lemma subset_Int_iff: "A<=B <-> A Int B = A" +by (blast elim!: equalityE) + +lemma subset_Int_iff2: "A<=B <-> B Int A = A" +by (blast elim!: equalityE) + +lemma Int_Diff_eq: "C<=A ==> (A-B) Int C = C-B" +by blast + +(** Binary Union **) + +lemma Un_cons: "cons(a,B) Un C = cons(a, B Un C)" +by blast + +lemma Un_absorb [simp]: "A Un A = A" +by blast + +lemma Un_left_absorb: "A Un (A Un B) = A Un B" +by blast + +lemma Un_commute: "A Un B = B Un A" +by blast + +lemma Un_left_commute: "A Un (B Un C) = B Un (A Un C)" +by blast + +lemma Un_assoc: "(A Un B) Un C = A Un (B Un C)" +by blast + +(*Union is an AC-operator*) +lemmas Un_ac = Un_assoc Un_left_absorb Un_commute Un_left_commute + +lemma Un_Int_distrib: "(A Int B) Un C = (A Un C) Int (B Un C)" +by blast + +lemma subset_Un_iff: "A<=B <-> A Un B = B" +by (blast elim!: equalityE) + +lemma subset_Un_iff2: "A<=B <-> B Un A = B" +by (blast elim!: equalityE) + +lemma Un_empty [iff]: "(A Un B = 0) <-> (A = 0 & B = 0)" +by blast + +lemma Un_eq_Union: "A Un B = Union({A, B})" +by blast + +(** Simple properties of Diff -- set difference **) + +lemma Diff_cancel: "A - A = 0" +by blast + +lemma Diff_triv: "A Int B = 0 ==> A - B = A" +by blast + +lemma empty_Diff [simp]: "0 - A = 0" +by blast + +lemma Diff_0 [simp]: "A - 0 = A" +by blast + +lemma Diff_eq_0_iff: "A - B = 0 <-> A <= B" +by (blast elim: equalityE) + +(*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*) +lemma Diff_cons: "A - cons(a,B) = A - B - {a}" +by blast + +(*NOT SUITABLE FOR REWRITING since {a} == cons(a,0)*) +lemma Diff_cons2: "A - cons(a,B) = A - {a} - B" +by blast + +lemma Diff_disjoint: "A Int (B-A) = 0" +by blast + +lemma Diff_partition: "A<=B ==> A Un (B-A) = B" +by blast + +lemma subset_Un_Diff: "A <= B Un (A - B)" +by blast + +lemma double_complement: "[| A<=B; B<=C |] ==> B-(C-A) = A" +by blast + +lemma double_complement_Un: "(A Un B) - (B-A) = A" +by blast + +lemma Un_Int_crazy: + "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)" +apply blast +done + +lemma Diff_Un: "A - (B Un C) = (A-B) Int (A-C)" +by blast + +lemma Diff_Int: "A - (B Int C) = (A-B) Un (A-C)" +by blast + +lemma Un_Diff: "(A Un B) - C = (A - C) Un (B - C)" +by blast + +lemma Int_Diff: "(A Int B) - C = A Int (B - C)" +by blast + +lemma Diff_Int_distrib: "C Int (A-B) = (C Int A) - (C Int B)" +by blast + +lemma Diff_Int_distrib2: "(A-B) Int C = (A Int C) - (B Int C)" +by blast + +(*Halmos, Naive Set Theory, page 16.*) +lemma Un_Int_assoc_iff: "(A Int B) Un C = A Int (B Un C) <-> C<=A" +by (blast elim!: equalityE) + + +(** Big Union and Intersection **) + +lemma Union_cons [simp]: "Union(cons(a,B)) = a Un Union(B)" +by blast + +lemma Union_Un_distrib: "Union(A Un B) = Union(A) Un Union(B)" +by blast + +lemma Union_Int_subset: "Union(A Int B) <= Union(A) Int Union(B)" +by blast + +lemma Union_disjoint: "Union(C) Int A = 0 <-> (ALL B:C. B Int A = 0)" +by (blast elim!: equalityE) + +lemma Union_empty_iff: "Union(A) = 0 <-> (ALL B:A. B=0)" +by blast + +lemma Inter_0: "Inter(0) = 0" +by (unfold Inter_def, blast) + +lemma Inter_Un_subset: "[| z:A; z:B |] ==> Inter(A) Un Inter(B) <= Inter(A Int B)" +by blast + +(* A good challenge: Inter is ill-behaved on the empty set *) +lemma Inter_Un_distrib: + "[| a:A; b:B |] ==> Inter(A Un B) = Inter(A) Int Inter(B)" +by blast + +lemma Union_singleton: "Union({b}) = b" +by blast + +lemma Inter_singleton: "Inter({b}) = b" +by blast + +lemma Inter_cons [simp]: + "Inter(cons(a,B)) = (if B=0 then a else a Int Inter(B))" +by force + +(** Unions and Intersections of Families **) + +lemma Union_eq_UN: "Union(A) = (UN x:A. x)" +by blast + +lemma Inter_eq_INT: "Inter(A) = (INT x:A. x)" +by (unfold Inter_def, blast) + +lemma UN_0 [simp]: "(UN i:0. A(i)) = 0" +by blast + +lemma UN_singleton: "(UN x:A. {x}) = A" +by blast + +lemma UN_Un: "(UN i: A Un B. C(i)) = (UN i: A. C(i)) Un (UN i:B. C(i))" +by blast + +lemma INT_Un: "(INT i:I Un J. A(i)) = (if I=0 then INT j:J. A(j) + else if J=0 then INT i:I. A(i) + else ((INT i:I. A(i)) Int (INT j:J. A(j))))" +apply auto +apply (blast intro!: equalityI) +done + +lemma UN_UN_flatten: "(UN x : (UN y:A. B(y)). C(x)) = (UN y:A. UN x: B(y). C(x))" +by blast + +(*Halmos, Naive Set Theory, page 35.*) +lemma Int_UN_distrib: "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))" +by blast + +lemma Un_INT_distrib: "i:I ==> B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))" +by blast + +lemma Int_UN_distrib2: + "(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))" +by blast + +lemma Un_INT_distrib2: "[| i:I; j:J |] ==> + (INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))" +by blast + +lemma UN_constant: "a: A ==> (UN y:A. c) = c" +by blast + +lemma INT_constant: "a: A ==> (INT y:A. c) = c" +by blast + +lemma UN_RepFun [simp]: "(UN y: RepFun(A,f). B(y)) = (UN x:A. B(f(x)))" +by blast + +lemma INT_RepFun [simp]: "(INT x:RepFun(A,f). B(x)) = (INT a:A. B(f(a)))" +by (auto simp add: Inter_def) + +lemma INT_Union_eq: + "0 ~: A ==> (INT x: Union(A). B(x)) = (INT y:A. INT x:y. B(x))" +apply (simp add: Inter_def) +apply (subgoal_tac "ALL x:A. x~=0") +prefer 2 apply blast +apply force +done + +lemma INT_UN_eq: "(ALL x:A. B(x) ~= 0) + ==> (INT z: (UN x:A. B(x)). C(z)) = (INT x:A. INT z: B(x). C(z))" +apply (subst INT_Union_eq, blast) +apply (simp add: Inter_def) +done + + +(** Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: + Union of a family of unions **) + +lemma UN_Un_distrib: + "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i)) Un (UN i:I. B(i))" +by blast + +lemma INT_Int_distrib: + "i:I ==> (INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))" +by blast + +lemma UN_Int_subset: + "(UN z:I Int J. A(z)) <= (UN z:I. A(z)) Int (UN z:J. A(z))" +by blast + +(** Devlin, page 12, exercise 5: Complements **) + +lemma Diff_UN: "i:I ==> B - (UN i:I. A(i)) = (INT i:I. B - A(i))" +by blast + +lemma Diff_INT: "i:I ==> B - (INT i:I. A(i)) = (UN i:I. B - A(i))" +by blast + +(** Unions and Intersections with General Sum **) + +(*Not suitable for rewriting: LOOPS!*) +lemma Sigma_cons1: "Sigma(cons(a,B), C) = ({a}*C(a)) Un Sigma(B,C)" +by blast + +(*Not suitable for rewriting: LOOPS!*) +lemma Sigma_cons2: "A * cons(b,B) = A*{b} Un A*B" +by blast + +lemma Sigma_succ1: "Sigma(succ(A), B) = ({A}*B(A)) Un Sigma(A,B)" +by blast + +lemma Sigma_succ2: "A * succ(B) = A*{B} Un A*B" +by blast + +lemma SUM_UN_distrib1: + "(SUM x:(UN y:A. C(y)). B(x)) = (UN y:A. SUM x:C(y). B(x))" +by blast + +lemma SUM_UN_distrib2: + "(SUM i:I. UN j:J. C(i,j)) = (UN j:J. SUM i:I. C(i,j))" +by blast + +lemma SUM_Un_distrib1: + "(SUM i:I Un J. C(i)) = (SUM i:I. C(i)) Un (SUM j:J. C(j))" +by blast + +lemma SUM_Un_distrib2: + "(SUM i:I. A(i) Un B(i)) = (SUM i:I. A(i)) Un (SUM i:I. B(i))" +by blast + +(*First-order version of the above, for rewriting*) +lemma prod_Un_distrib2: "I * (A Un B) = I*A Un I*B" +by (rule SUM_Un_distrib2) + +lemma SUM_Int_distrib1: + "(SUM i:I Int J. C(i)) = (SUM i:I. C(i)) Int (SUM j:J. C(j))" +by blast + +lemma SUM_Int_distrib2: + "(SUM i:I. A(i) Int B(i)) = (SUM i:I. A(i)) Int (SUM i:I. B(i))" +by blast + +(*First-order version of the above, for rewriting*) +lemma prod_Int_distrib2: "I * (A Int B) = I*A Int I*B" +by (rule SUM_Int_distrib2) + +(*Cf Aczel, Non-Well-Founded Sets, page 115*) +lemma SUM_eq_UN: "(SUM i:I. A(i)) = (UN i:I. {i} * A(i))" +by blast + +(** Domain **) + +lemma domain_of_prod: "b:B ==> domain(A*B) = A" +by blast + +lemma domain_0 [simp]: "domain(0) = 0" +by blast + +lemma domain_cons [simp]: "domain(cons(,r)) = cons(a, domain(r))" +by blast + +lemma domain_Un_eq [simp]: "domain(A Un B) = domain(A) Un domain(B)" +by blast + +lemma domain_Int_subset: "domain(A Int B) <= domain(A) Int domain(B)" +by blast + +lemma domain_Diff_subset: "domain(A) - domain(B) <= domain(A - B)" +by blast + +lemma domain_converse [simp]: "domain(converse(r)) = range(r)" +by blast -equalities = domrange +lemma domain_UN: "domain(UN x:A. B(x)) = (UN x:A. domain(B(x)))" +by blast + +lemma domain_Union: "domain(Union(A)) = (UN x:A. domain(x))" +by blast + + +(** Range **) + +lemma range_of_prod: "a:A ==> range(A*B) = B" +by blast + +lemma range_0 [simp]: "range(0) = 0" +by blast + +lemma range_cons [simp]: "range(cons(,r)) = cons(b, range(r))" +by blast + +lemma range_Un_eq [simp]: "range(A Un B) = range(A) Un range(B)" +by blast + +lemma range_Int_subset: "range(A Int B) <= range(A) Int range(B)" +by blast + +lemma range_Diff_subset: "range(A) - range(B) <= range(A - B)" +by blast + +lemma range_converse [simp]: "range(converse(r)) = domain(r)" +by blast + + +(** Field **) + +lemma field_of_prod: "field(A*A) = A" +by blast + +lemma field_0 [simp]: "field(0) = 0" +by blast + +lemma field_cons [simp]: "field(cons(,r)) = cons(a, cons(b, field(r)))" +by blast + +lemma field_Un_eq [simp]: "field(A Un B) = field(A) Un field(B)" +by blast + +lemma field_Int_subset: "field(A Int B) <= field(A) Int field(B)" +by blast + +lemma field_Diff_subset: "field(A) - field(B) <= field(A - B)" +by blast + +lemma field_converse [simp]: "field(converse(r)) = field(r)" +by blast + + +(** Image **) + +lemma image_0 [simp]: "r``0 = 0" +by blast + +lemma image_Un [simp]: "r``(A Un B) = (r``A) Un (r``B)" +by blast + +lemma image_Int_subset: "r``(A Int B) <= (r``A) Int (r``B)" +by blast + +lemma image_Int_square_subset: "(r Int A*A)``B <= (r``B) Int A" +by blast + +lemma image_Int_square: "B<=A ==> (r Int A*A)``B = (r``B) Int A" +by blast + + +(*Image laws for special relations*) +lemma image_0_left [simp]: "0``A = 0" +by blast + +lemma image_Un_left: "(r Un s)``A = (r``A) Un (s``A)" +by blast + +lemma image_Int_subset_left: "(r Int s)``A <= (r``A) Int (s``A)" +by blast + + +(** Inverse Image **) + +lemma vimage_0 [simp]: "r-``0 = 0" +by blast + +lemma vimage_Un [simp]: "r-``(A Un B) = (r-``A) Un (r-``B)" +by blast + +lemma vimage_Int_subset: "r-``(A Int B) <= (r-``A) Int (r-``B)" +by blast + +(*NOT suitable for rewriting*) +lemma vimage_eq_UN: "f -``B = (UN y:B. f-``{y})" +by blast + +lemma function_vimage_Int: + "function(f) ==> f-``(A Int B) = (f-``A) Int (f-``B)" +by (unfold function_def, blast) + +lemma function_vimage_Diff: "function(f) ==> f-``(A-B) = (f-``A) - (f-``B)" +by (unfold function_def, blast) + +lemma function_image_vimage: "function(f) ==> f `` (f-`` A) <= A" +by (unfold function_def, blast) + +lemma vimage_Int_square_subset: "(r Int A*A)-``B <= (r-``B) Int A" +by blast + +lemma vimage_Int_square: "B<=A ==> (r Int A*A)-``B = (r-``B) Int A" +by blast + + + +(*Invese image laws for special relations*) +lemma vimage_0_left [simp]: "0-``A = 0" +by blast + +lemma vimage_Un_left: "(r Un s)-``A = (r-``A) Un (s-``A)" +by blast + +lemma vimage_Int_subset_left: "(r Int s)-``A <= (r-``A) Int (s-``A)" +by blast + + +(** Converse **) + +lemma converse_Un [simp]: "converse(A Un B) = converse(A) Un converse(B)" +by blast + +lemma converse_Int [simp]: "converse(A Int B) = converse(A) Int converse(B)" +by blast + +lemma converse_Diff [simp]: "converse(A - B) = converse(A) - converse(B)" +by blast + +lemma converse_UN [simp]: "converse(UN x:A. B(x)) = (UN x:A. converse(B(x)))" +by blast + +(*Unfolding Inter avoids using excluded middle on A=0*) +lemma converse_INT [simp]: + "converse(INT x:A. B(x)) = (INT x:A. converse(B(x)))" +apply (unfold Inter_def, blast) +done + +(** Pow **) + +lemma Pow_0 [simp]: "Pow(0) = {0}" +by blast + +lemma Pow_insert: "Pow (cons(a,A)) = Pow(A) Un {cons(a,X) . X: Pow(A)}" +apply (rule equalityI, safe) +apply (erule swap) +apply (rule_tac a = "x-{a}" in RepFun_eqI, auto) +done + +lemma Un_Pow_subset: "Pow(A) Un Pow(B) <= Pow(A Un B)" +by blast + +lemma UN_Pow_subset: "(UN x:A. Pow(B(x))) <= Pow(UN x:A. B(x))" +by blast + +lemma subset_Pow_Union: "A <= Pow(Union(A))" +by blast + +lemma Union_Pow_eq [simp]: "Union(Pow(A)) = A" +by blast + +lemma Pow_Int_eq [simp]: "Pow(A Int B) = Pow(A) Int Pow(B)" +by blast + +lemma Pow_INT_eq: "x:A ==> Pow(INT x:A. B(x)) = (INT x:A. Pow(B(x)))" +by blast + +(** RepFun **) + +lemma RepFun_eq_0_iff [simp]: "{f(x).x:A}=0 <-> A=0" +by blast + +lemma RepFun_constant [simp]: "{c. x:A} = (if A=0 then 0 else {c})" +apply auto +apply blast +done + +(** Collect **) +lemma Collect_Un: "Collect(A Un B, P) = Collect(A,P) Un Collect(B,P)" +by blast + +lemma Collect_Int: "Collect(A Int B, P) = Collect(A,P) Int Collect(B,P)" +by blast + +lemma Collect_Diff: "Collect(A - B, P) = Collect(A,P) - Collect(B,P)" +by blast + +lemma Collect_cons: "{x:cons(a,B). P(x)} = + (if P(a) then cons(a, {x:B. P(x)}) else {x:B. P(x)})" +by (simp, blast) + +lemma Int_Collect_self_eq: "A Int Collect(A,P) = Collect(A,P)" +by blast + +lemma Collect_Collect_eq [simp]: + "Collect(Collect(A,P), Q) = Collect(A, %x. P(x) & Q(x))" +by blast + +lemma Collect_Int_Collect_eq: + "Collect(A,P) Int Collect(A,Q) = Collect(A, %x. P(x) & Q(x))" +by blast + +ML +{* +val cons_eq = thm "cons_eq"; +val cons_commute = thm "cons_commute"; +val cons_absorb = thm "cons_absorb"; +val cons_Diff = thm "cons_Diff"; +val equal_singleton = thm "equal_singleton"; +val Int_cons = thm "Int_cons"; +val Int_absorb = thm "Int_absorb"; +val Int_left_absorb = thm "Int_left_absorb"; +val Int_commute = thm "Int_commute"; +val Int_left_commute = thm "Int_left_commute"; +val Int_assoc = thm "Int_assoc"; +val Int_Un_distrib = thm "Int_Un_distrib"; +val Int_Un_distrib2 = thm "Int_Un_distrib2"; +val subset_Int_iff = thm "subset_Int_iff"; +val subset_Int_iff2 = thm "subset_Int_iff2"; +val Int_Diff_eq = thm "Int_Diff_eq"; +val Un_cons = thm "Un_cons"; +val Un_absorb = thm "Un_absorb"; +val Un_left_absorb = thm "Un_left_absorb"; +val Un_commute = thm "Un_commute"; +val Un_left_commute = thm "Un_left_commute"; +val Un_assoc = thm "Un_assoc"; +val Un_Int_distrib = thm "Un_Int_distrib"; +val subset_Un_iff = thm "subset_Un_iff"; +val subset_Un_iff2 = thm "subset_Un_iff2"; +val Un_empty = thm "Un_empty"; +val Un_eq_Union = thm "Un_eq_Union"; +val Diff_cancel = thm "Diff_cancel"; +val Diff_triv = thm "Diff_triv"; +val empty_Diff = thm "empty_Diff"; +val Diff_0 = thm "Diff_0"; +val Diff_eq_0_iff = thm "Diff_eq_0_iff"; +val Diff_cons = thm "Diff_cons"; +val Diff_cons2 = thm "Diff_cons2"; +val Diff_disjoint = thm "Diff_disjoint"; +val Diff_partition = thm "Diff_partition"; +val subset_Un_Diff = thm "subset_Un_Diff"; +val double_complement = thm "double_complement"; +val double_complement_Un = thm "double_complement_Un"; +val Un_Int_crazy = thm "Un_Int_crazy"; +val Diff_Un = thm "Diff_Un"; +val Diff_Int = thm "Diff_Int"; +val Un_Diff = thm "Un_Diff"; +val Int_Diff = thm "Int_Diff"; +val Diff_Int_distrib = thm "Diff_Int_distrib"; +val Diff_Int_distrib2 = thm "Diff_Int_distrib2"; +val Un_Int_assoc_iff = thm "Un_Int_assoc_iff"; +val Union_cons = thm "Union_cons"; +val Union_Un_distrib = thm "Union_Un_distrib"; +val Union_Int_subset = thm "Union_Int_subset"; +val Union_disjoint = thm "Union_disjoint"; +val Union_empty_iff = thm "Union_empty_iff"; +val Inter_0 = thm "Inter_0"; +val Inter_Un_subset = thm "Inter_Un_subset"; +val Inter_Un_distrib = thm "Inter_Un_distrib"; +val Union_singleton = thm "Union_singleton"; +val Inter_singleton = thm "Inter_singleton"; +val Inter_cons = thm "Inter_cons"; +val Union_eq_UN = thm "Union_eq_UN"; +val Inter_eq_INT = thm "Inter_eq_INT"; +val UN_0 = thm "UN_0"; +val UN_singleton = thm "UN_singleton"; +val UN_Un = thm "UN_Un"; +val INT_Un = thm "INT_Un"; +val UN_UN_flatten = thm "UN_UN_flatten"; +val Int_UN_distrib = thm "Int_UN_distrib"; +val Un_INT_distrib = thm "Un_INT_distrib"; +val Int_UN_distrib2 = thm "Int_UN_distrib2"; +val Un_INT_distrib2 = thm "Un_INT_distrib2"; +val UN_constant = thm "UN_constant"; +val INT_constant = thm "INT_constant"; +val UN_RepFun = thm "UN_RepFun"; +val INT_RepFun = thm "INT_RepFun"; +val INT_Union_eq = thm "INT_Union_eq"; +val INT_UN_eq = thm "INT_UN_eq"; +val UN_Un_distrib = thm "UN_Un_distrib"; +val INT_Int_distrib = thm "INT_Int_distrib"; +val UN_Int_subset = thm "UN_Int_subset"; +val Diff_UN = thm "Diff_UN"; +val Diff_INT = thm "Diff_INT"; +val Sigma_cons1 = thm "Sigma_cons1"; +val Sigma_cons2 = thm "Sigma_cons2"; +val Sigma_succ1 = thm "Sigma_succ1"; +val Sigma_succ2 = thm "Sigma_succ2"; +val SUM_UN_distrib1 = thm "SUM_UN_distrib1"; +val SUM_UN_distrib2 = thm "SUM_UN_distrib2"; +val SUM_Un_distrib1 = thm "SUM_Un_distrib1"; +val SUM_Un_distrib2 = thm "SUM_Un_distrib2"; +val prod_Un_distrib2 = thm "prod_Un_distrib2"; +val SUM_Int_distrib1 = thm "SUM_Int_distrib1"; +val SUM_Int_distrib2 = thm "SUM_Int_distrib2"; +val prod_Int_distrib2 = thm "prod_Int_distrib2"; +val SUM_eq_UN = thm "SUM_eq_UN"; +val domain_of_prod = thm "domain_of_prod"; +val domain_0 = thm "domain_0"; +val domain_cons = thm "domain_cons"; +val domain_Un_eq = thm "domain_Un_eq"; +val domain_Int_subset = thm "domain_Int_subset"; +val domain_Diff_subset = thm "domain_Diff_subset"; +val domain_converse = thm "domain_converse"; +val domain_UN = thm "domain_UN"; +val domain_Union = thm "domain_Union"; +val range_of_prod = thm "range_of_prod"; +val range_0 = thm "range_0"; +val range_cons = thm "range_cons"; +val range_Un_eq = thm "range_Un_eq"; +val range_Int_subset = thm "range_Int_subset"; +val range_Diff_subset = thm "range_Diff_subset"; +val range_converse = thm "range_converse"; +val field_of_prod = thm "field_of_prod"; +val field_0 = thm "field_0"; +val field_cons = thm "field_cons"; +val field_Un_eq = thm "field_Un_eq"; +val field_Int_subset = thm "field_Int_subset"; +val field_Diff_subset = thm "field_Diff_subset"; +val field_converse = thm "field_converse"; +val image_0 = thm "image_0"; +val image_Un = thm "image_Un"; +val image_Int_subset = thm "image_Int_subset"; +val image_Int_square_subset = thm "image_Int_square_subset"; +val image_Int_square = thm "image_Int_square"; +val image_0_left = thm "image_0_left"; +val image_Un_left = thm "image_Un_left"; +val image_Int_subset_left = thm "image_Int_subset_left"; +val vimage_0 = thm "vimage_0"; +val vimage_Un = thm "vimage_Un"; +val vimage_Int_subset = thm "vimage_Int_subset"; +val vimage_eq_UN = thm "vimage_eq_UN"; +val function_vimage_Int = thm "function_vimage_Int"; +val function_vimage_Diff = thm "function_vimage_Diff"; +val function_image_vimage = thm "function_image_vimage"; +val vimage_Int_square_subset = thm "vimage_Int_square_subset"; +val vimage_Int_square = thm "vimage_Int_square"; +val vimage_0_left = thm "vimage_0_left"; +val vimage_Un_left = thm "vimage_Un_left"; +val vimage_Int_subset_left = thm "vimage_Int_subset_left"; +val converse_Un = thm "converse_Un"; +val converse_Int = thm "converse_Int"; +val converse_Diff = thm "converse_Diff"; +val converse_UN = thm "converse_UN"; +val converse_INT = thm "converse_INT"; +val Pow_0 = thm "Pow_0"; +val Pow_insert = thm "Pow_insert"; +val Un_Pow_subset = thm "Un_Pow_subset"; +val UN_Pow_subset = thm "UN_Pow_subset"; +val subset_Pow_Union = thm "subset_Pow_Union"; +val Union_Pow_eq = thm "Union_Pow_eq"; +val Pow_Int_eq = thm "Pow_Int_eq"; +val Pow_INT_eq = thm "Pow_INT_eq"; +val RepFun_eq_0_iff = thm "RepFun_eq_0_iff"; +val RepFun_constant = thm "RepFun_constant"; +val Collect_Un = thm "Collect_Un"; +val Collect_Int = thm "Collect_Int"; +val Collect_Diff = thm "Collect_Diff"; +val Collect_cons = thm "Collect_cons"; +val Int_Collect_self_eq = thm "Int_Collect_self_eq"; +val Collect_Collect_eq = thm "Collect_Collect_eq"; +val Collect_Int_Collect_eq = thm "Collect_Int_Collect_eq"; + +val Int_ac = thms "Int_ac"; +val Un_ac = thms "Un_ac"; + +*} + +end +