# HG changeset patch # User haftmann # Date 1330626892 -3600 # Node ID e9e7209eb3750b003709f6bafb80d19607163dd9 # Parent 6b94c39b73666755e388a2e857e8d8e7124bb98b more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS) diff -r 6b94c39b7366 -r e9e7209eb375 NEWS --- a/NEWS Thu Mar 01 17:13:54 2012 +0000 +++ b/NEWS Thu Mar 01 19:34:52 2012 +0100 @@ -90,6 +90,18 @@ * New type synonym 'a rel = ('a * 'a) set +* More default pred/set conversions on a couple of relation operations +and predicates. Consolidation of some relation theorems: + + converse_def ~> converse_unfold + rel_comp_def ~> rel_comp_unfold + symp_def ~> (dropped, use symp_def and sym_def instead) + transp_def ~> transp_trans + Domain_def ~> Domain_unfold + Range_def ~> Domain_converse [symmetric] + +INCOMPATIBILITY. + * Consolidated various theorem names relating to Finite_Set.fold combinator: @@ -99,7 +111,7 @@ SUPR_fold_sup ~> SUP_fold_sup union_set ~> union_set_fold minus_set ~> minus_set_fold - + INCOMPATIBILITY. * Consolidated theorem names concerning fold combinators: diff -r 6b94c39b7366 -r e9e7209eb375 src/HOL/Equiv_Relations.thy --- a/src/HOL/Equiv_Relations.thy Thu Mar 01 17:13:54 2012 +0000 +++ b/src/HOL/Equiv_Relations.thy Thu Mar 01 19:34:52 2012 +0100 @@ -31,7 +31,7 @@ lemma sym_trans_comp_subset: "sym r ==> trans r ==> r\ O r \ r" - by (unfold trans_def sym_def converse_def) blast + by (unfold trans_def sym_def converse_unfold) blast lemma refl_on_comp_subset: "refl_on A r ==> r \ r\ O r" by (unfold refl_on_def) blast @@ -426,7 +426,7 @@ lemma equivp_equiv: "equiv UNIV A \ equivp (\x y. (x, y) \ A)" - by (auto intro: equivpI elim: equivpE simp add: equiv_def reflp_def symp_def transp_def) + by (auto intro!: equivI equivpI [to_set] elim!: equivE equivpE [to_set]) lemma equivp_reflp_symp_transp: shows "equivp R \ reflp R \ symp R \ transp R" @@ -449,3 +449,4 @@ by (erule equivpE, erule transpE) end + diff -r 6b94c39b7366 -r e9e7209eb375 src/HOL/Library/Zorn.thy --- a/src/HOL/Library/Zorn.thy Thu Mar 01 17:13:54 2012 +0000 +++ b/src/HOL/Library/Zorn.thy Thu Mar 01 19:34:52 2012 +0100 @@ -453,7 +453,7 @@ proof assume "m={}" moreover have "Well_order {(x,x)}" - by(simp add:order_on_defs refl_on_def trans_def antisym_def total_on_def Field_def Domain_def Range_def) + by(simp add:order_on_defs refl_on_def trans_def antisym_def total_on_def Field_def Domain_unfold Domain_converse [symmetric]) ultimately show False using max by (auto simp:I_def init_seg_of_def simp del:Field_insert) qed @@ -470,14 +470,14 @@ --{*We show that the extension is a well-order*} have "Refl ?m" using `Refl m` Fm by(auto simp:refl_on_def) moreover have "trans ?m" using `trans m` `x \ Field m` - unfolding trans_def Field_def Domain_def Range_def by blast + unfolding trans_def Field_def Domain_unfold Domain_converse [symmetric] by blast moreover have "antisym ?m" using `antisym m` `x \ Field m` - unfolding antisym_def Field_def Domain_def Range_def by blast + unfolding antisym_def Field_def Domain_unfold Domain_converse [symmetric] by blast moreover have "Total ?m" using `Total m` Fm by(auto simp: total_on_def) moreover have "wf(?m-Id)" proof- have "wf ?s" using `x \ Field m` - by(auto simp add:wf_eq_minimal Field_def Domain_def Range_def) metis + by(auto simp add:wf_eq_minimal Field_def Domain_unfold Domain_converse [symmetric]) metis thus ?thesis using `wf(m-Id)` `x \ Field m` wf_subset[OF `wf ?s` Diff_subset] by (fastforce intro!: wf_Un simp add: Un_Diff Field_def) @@ -485,7 +485,7 @@ ultimately have "Well_order ?m" by(simp add:order_on_defs) --{*We show that the extension is above m*} moreover hence "(m,?m) : I" using `Well_order m` `x \ Field m` - by(fastforce simp:I_def init_seg_of_def Field_def Domain_def Range_def) + by(fastforce simp:I_def init_seg_of_def Field_def Domain_unfold Domain_converse [symmetric]) ultimately --{*This contradicts maximality of m:*} have False using max `x \ Field m` unfolding Field_def by blast @@ -501,7 +501,7 @@ using well_ordering[where 'a = "'a"] by blast let ?r = "{(x,y). x:A & y:A & (x,y):r}" have 1: "Field ?r = A" using wo univ - by(fastforce simp: Field_def Domain_def Range_def order_on_defs refl_on_def) + by(fastforce simp: Field_def Domain_unfold Domain_converse [symmetric] order_on_defs refl_on_def) have "Refl r" "trans r" "antisym r" "Total r" "wf(r-Id)" using `Well_order r` by(simp_all add:order_on_defs) have "Refl ?r" using `Refl r` by(auto simp:refl_on_def 1 univ) diff -r 6b94c39b7366 -r e9e7209eb375 src/HOL/Metis_Examples/Tarski.thy --- a/src/HOL/Metis_Examples/Tarski.thy Thu Mar 01 17:13:54 2012 +0000 +++ b/src/HOL/Metis_Examples/Tarski.thy Thu Mar 01 19:34:52 2012 +0100 @@ -189,10 +189,10 @@ by (simp add: glb_def greatest_def isGlb_def some_eq_ex [symmetric]) lemma isGlb_dual_isLub: "isGlb S cl = isLub S (dual cl)" -by (simp add: isLub_def isGlb_def dual_def converse_def) +by (simp add: isLub_def isGlb_def dual_def converse_unfold) lemma isLub_dual_isGlb: "isLub S cl = isGlb S (dual cl)" -by (simp add: isLub_def isGlb_def dual_def converse_def) +by (simp add: isLub_def isGlb_def dual_def converse_unfold) lemma (in PO) dualPO: "dual cl \ PartialOrder" apply (insert cl_po) @@ -212,10 +212,10 @@ done lemma lub_dual_glb: "lub S cl = glb S (dual cl)" -by (simp add: lub_def glb_def least_def greatest_def dual_def converse_def) +by (simp add: lub_def glb_def least_def greatest_def dual_def converse_unfold) lemma glb_dual_lub: "glb S cl = lub S (dual cl)" -by (simp add: lub_def glb_def least_def greatest_def dual_def converse_def) +by (simp add: lub_def glb_def least_def greatest_def dual_def converse_unfold) lemma CL_subset_PO: "CompleteLattice \ PartialOrder" by (simp add: PartialOrder_def CompleteLattice_def, fast) diff -r 6b94c39b7366 -r e9e7209eb375 src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Thu Mar 01 17:13:54 2012 +0000 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Thu Mar 01 19:34:52 2012 +0100 @@ -1043,14 +1043,14 @@ (i => bool) => o * i => bool, (i => bool) => i => bool) [inductify] Id_on . thm Id_on.equation -thm Domain_def +thm Domain_unfold code_pred (modes: (o * o => bool) => o => bool, (o * o => bool) => i => bool, (i * o => bool) => i => bool) [inductify] Domain . thm Domain.equation -thm Range_def +thm Domain_converse [symmetric] code_pred (modes: (o * o => bool) => o => bool, (o * o => bool) => i => bool, diff -r 6b94c39b7366 -r e9e7209eb375 src/HOL/Quotient_Examples/FSet.thy --- a/src/HOL/Quotient_Examples/FSet.thy Thu Mar 01 17:13:54 2012 +0000 +++ b/src/HOL/Quotient_Examples/FSet.thy Thu Mar 01 19:34:52 2012 +0100 @@ -534,7 +534,7 @@ assumes "(R1 ===> R2 ===> R3) C C" and "(R4 ===> R5 ===> R6) C C" shows "(R1 OOO R4 ===> R2 OOO R5 ===> R3 OOO R6) C C" by (auto intro!: fun_relI) - (metis (full_types) assms fun_relE pred_comp.intros) + (metis (full_types) assms fun_relE pred_compI) lemma append_rsp2 [quot_respect]: "(list_all2 op \ OOO op \ ===> list_all2 op \ OOO op \ ===> list_all2 op \ OOO op \) append append" @@ -560,7 +560,7 @@ by (induct y ya rule: list_induct2') (simp_all, metis apply_rsp' list_eq_def) show "(list_all2 op \ OOO op \) (map f xa) (map f' ya)" - by (metis a b c list_eq_def pred_comp.intros) + by (metis a b c list_eq_def pred_compI) qed lemma map_prs2 [quot_preserve]: diff -r 6b94c39b7366 -r e9e7209eb375 src/HOL/Relation.thy --- a/src/HOL/Relation.thy Thu Mar 01 17:13:54 2012 +0000 +++ b/src/HOL/Relation.thy Thu Mar 01 19:34:52 2012 +0100 @@ -113,28 +113,33 @@ subsubsection {* Reflexivity *} -definition - refl_on :: "'a set \ ('a \ 'a) set \ bool" where - "refl_on A r \ r \ A \ A & (ALL x: A. (x,x) : r)" +definition refl_on :: "'a set \ 'a rel \ bool" +where + "refl_on A r \ r \ A \ A \ (\x\A. (x, x) \ r)" -abbreviation - refl :: "('a * 'a) set => bool" where -- {* reflexivity over a type *} +abbreviation refl :: "'a rel \ bool" +where -- {* reflexivity over a type *} "refl \ refl_on UNIV" -definition reflp :: "('a \ 'a \ bool) \ bool" where +definition reflp :: "('a \ 'a \ bool) \ bool" +where "reflp r \ refl {(x, y). r x y}" +lemma reflp_refl_eq [pred_set_conv]: + "reflp (\x y. (x, y) \ r) \ refl r" + by (simp add: refl_on_def reflp_def) + lemma refl_onI: "r \ A \ A ==> (!!x. x : A ==> (x, x) : r) ==> refl_on A r" -by (unfold refl_on_def) (iprover intro!: ballI) + by (unfold refl_on_def) (iprover intro!: ballI) lemma refl_onD: "refl_on A r ==> a : A ==> (a, a) : r" -by (unfold refl_on_def) blast + by (unfold refl_on_def) blast lemma refl_onD1: "refl_on A r ==> (x, y) : r ==> x : A" -by (unfold refl_on_def) blast + by (unfold refl_on_def) blast lemma refl_onD2: "refl_on A r ==> (x, y) : r ==> y : A" -by (unfold refl_on_def) blast + by (unfold refl_on_def) blast lemma reflpI: "(\x. r x x) \ reflp r" @@ -146,32 +151,40 @@ using assms by (auto dest: refl_onD simp add: reflp_def) lemma refl_on_Int: "refl_on A r ==> refl_on B s ==> refl_on (A \ B) (r \ s)" -by (unfold refl_on_def) blast + by (unfold refl_on_def) blast + +lemma reflp_inf: + "reflp r \ reflp s \ reflp (r \ s)" + by (auto intro: reflpI elim: reflpE) lemma refl_on_Un: "refl_on A r ==> refl_on B s ==> refl_on (A \ B) (r \ s)" -by (unfold refl_on_def) blast + by (unfold refl_on_def) blast + +lemma reflp_sup: + "reflp r \ reflp s \ reflp (r \ s)" + by (auto intro: reflpI elim: reflpE) lemma refl_on_INTER: "ALL x:S. refl_on (A x) (r x) ==> refl_on (INTER S A) (INTER S r)" -by (unfold refl_on_def) fast + by (unfold refl_on_def) fast lemma refl_on_UNION: "ALL x:S. refl_on (A x) (r x) \ refl_on (UNION S A) (UNION S r)" -by (unfold refl_on_def) blast + by (unfold refl_on_def) blast -lemma refl_on_empty[simp]: "refl_on {} {}" -by(simp add:refl_on_def) +lemma refl_on_empty [simp]: "refl_on {} {}" + by (simp add:refl_on_def) lemma refl_on_def' [nitpick_unfold, code]: - "refl_on A r = ((\(x, y) \ r. x : A \ y : A) \ (\x \ A. (x, x) : r))" -by (auto intro: refl_onI dest: refl_onD refl_onD1 refl_onD2) + "refl_on A r \ (\(x, y) \ r. x \ A \ y \ A) \ (\x \ A. (x, x) \ r)" + by (auto intro: refl_onI dest: refl_onD refl_onD1 refl_onD2) subsubsection {* Irreflexivity *} -definition - irrefl :: "('a * 'a) set => bool" where - "irrefl r \ (\x. (x,x) \ r)" +definition irrefl :: "'a rel \ bool" +where + "irrefl r \ (\x. (x, x) \ r)" lemma irrefl_distinct [code]: "irrefl r \ (\(x, y) \ r. x \ y)" @@ -180,166 +193,231 @@ subsubsection {* Symmetry *} -definition - sym :: "('a * 'a) set => bool" where - "sym r \ (ALL x y. (x,y): r --> (y,x): r)" +definition sym :: "'a rel \ bool" +where + "sym r \ (\x y. (x, y) \ r \ (y, x) \ r)" + +definition symp :: "('a \ 'a \ bool) \ bool" +where + "symp r \ (\x y. r x y \ r y x)" -lemma symI: "(!!a b. (a, b) : r ==> (b, a) : r) ==> sym r" -by (unfold sym_def) iprover +lemma symp_sym_eq [pred_set_conv]: + "symp (\x y. (x, y) \ r) \ sym r" + by (simp add: sym_def symp_def) -lemma symD: "sym r ==> (a, b) : r ==> (b, a) : r" -by (unfold sym_def, blast) - -definition symp :: "('a \ 'a \ bool) \ bool" where - "symp r \ sym {(x, y). r x y}" +lemma symI: + "(\a b. (a, b) \ r \ (b, a) \ r) \ sym r" + by (unfold sym_def) iprover lemma sympI: - "(\x y. r x y \ r y x) \ symp r" - by (auto intro: symI simp add: symp_def) + "(\a b. r a b \ r b a) \ symp r" + by (fact symI [to_pred]) + +lemma symE: + assumes "sym r" and "(b, a) \ r" + obtains "(a, b) \ r" + using assms by (simp add: sym_def) lemma sympE: - assumes "symp r" and "r x y" - obtains "r y x" - using assms by (auto dest: symD simp add: symp_def) + assumes "symp r" and "r b a" + obtains "r a b" + using assms by (rule symE [to_pred]) + +lemma symD: + assumes "sym r" and "(b, a) \ r" + shows "(a, b) \ r" + using assms by (rule symE) -lemma sym_Int: "sym r ==> sym s ==> sym (r \ s)" -by (fast intro: symI dest: symD) +lemma sympD: + assumes "symp r" and "r b a" + shows "r a b" + using assms by (rule symD [to_pred]) + +lemma sym_Int: + "sym r \ sym s \ sym (r \ s)" + by (fast intro: symI elim: symE) -lemma sym_Un: "sym r ==> sym s ==> sym (r \ s)" -by (fast intro: symI dest: symD) +lemma symp_inf: + "symp r \ symp s \ symp (r \ s)" + by (fact sym_Int [to_pred]) + +lemma sym_Un: + "sym r \ sym s \ sym (r \ s)" + by (fast intro: symI elim: symE) + +lemma symp_sup: + "symp r \ symp s \ symp (r \ s)" + by (fact sym_Un [to_pred]) -lemma sym_INTER: "ALL x:S. sym (r x) ==> sym (INTER S r)" -by (fast intro: symI dest: symD) +lemma sym_INTER: + "\x\S. sym (r x) \ sym (INTER S r)" + by (fast intro: symI elim: symE) + +(* FIXME thm sym_INTER [to_pred] *) -lemma sym_UNION: "ALL x:S. sym (r x) ==> sym (UNION S r)" -by (fast intro: symI dest: symD) +lemma sym_UNION: + "\x\S. sym (r x) \ sym (UNION S r)" + by (fast intro: symI elim: symE) + +(* FIXME thm sym_UNION [to_pred] *) subsubsection {* Antisymmetry *} -definition - antisym :: "('a * 'a) set => bool" where - "antisym r \ (ALL x y. (x,y):r --> (y,x):r --> x=y)" +definition antisym :: "'a rel \ bool" +where + "antisym r \ (\x y. (x, y) \ r \ (y, x) \ r \ x = y)" + +abbreviation antisymP :: "('a \ 'a \ bool) \ bool" +where + "antisymP r \ antisym {(x, y). r x y}" lemma antisymI: "(!!x y. (x, y) : r ==> (y, x) : r ==> x=y) ==> antisym r" -by (unfold antisym_def) iprover + by (unfold antisym_def) iprover lemma antisymD: "antisym r ==> (a, b) : r ==> (b, a) : r ==> a = b" -by (unfold antisym_def) iprover - -abbreviation antisymP :: "('a \ 'a \ bool) \ bool" where - "antisymP r \ antisym {(x, y). r x y}" + by (unfold antisym_def) iprover lemma antisym_subset: "r \ s ==> antisym s ==> antisym r" -by (unfold antisym_def) blast + by (unfold antisym_def) blast lemma antisym_empty [simp]: "antisym {}" -by (unfold antisym_def) blast + by (unfold antisym_def) blast subsubsection {* Transitivity *} -definition - trans :: "('a * 'a) set => bool" where - "trans r \ (ALL x y z. (x,y):r --> (y,z):r --> (x,z):r)" +definition trans :: "'a rel \ bool" +where + "trans r \ (\x y z. (x, y) \ r \ (y, z) \ r \ (x, z) \ r)" + +definition transp :: "('a \ 'a \ bool) \ bool" +where + "transp r \ (\x y z. r x y \ r y z \ r x z)" + +lemma transp_trans_eq [pred_set_conv]: + "transp (\x y. (x, y) \ r) \ trans r" + by (simp add: trans_def transp_def) + +abbreviation transP :: "('a \ 'a \ bool) \ bool" +where -- {* FIXME drop *} + "transP r \ trans {(x, y). r x y}" lemma transI: - "(!!x y z. (x, y) : r ==> (y, z) : r ==> (x, z) : r) ==> trans r" -by (unfold trans_def) iprover - -lemma transD: "trans r ==> (a, b) : r ==> (b, c) : r ==> (a, c) : r" -by (unfold trans_def) iprover - -abbreviation transP :: "('a \ 'a \ bool) \ bool" where - "transP r \ trans {(x, y). r x y}" - -definition transp :: "('a \ 'a \ bool) \ bool" where - "transp r \ trans {(x, y). r x y}" + "(\x y z. (x, y) \ r \ (y, z) \ r \ (x, z) \ r) \ trans r" + by (unfold trans_def) iprover lemma transpI: "(\x y z. r x y \ r y z \ r x z) \ transp r" - by (auto intro: transI simp add: transp_def) - + by (fact transI [to_pred]) + +lemma transE: + assumes "trans r" and "(x, y) \ r" and "(y, z) \ r" + obtains "(x, z) \ r" + using assms by (unfold trans_def) iprover + lemma transpE: assumes "transp r" and "r x y" and "r y z" obtains "r x z" - using assms by (auto dest: transD simp add: transp_def) + using assms by (rule transE [to_pred]) + +lemma transD: + assumes "trans r" and "(x, y) \ r" and "(y, z) \ r" + shows "(x, z) \ r" + using assms by (rule transE) + +lemma transpD: + assumes "transp r" and "r x y" and "r y z" + shows "r x z" + using assms by (rule transD [to_pred]) -lemma trans_Int: "trans r ==> trans s ==> trans (r \ s)" -by (fast intro: transI elim: transD) +lemma trans_Int: + "trans r \ trans s \ trans (r \ s)" + by (fast intro: transI elim: transE) -lemma trans_INTER: "ALL x:S. trans (r x) ==> trans (INTER S r)" -by (fast intro: transI elim: transD) +lemma transp_inf: + "transp r \ transp s \ transp (r \ s)" + by (fact trans_Int [to_pred]) + +lemma trans_INTER: + "\x\S. trans (r x) \ trans (INTER S r)" + by (fast intro: transI elim: transD) + +(* FIXME thm trans_INTER [to_pred] *) lemma trans_join [code]: "trans r \ (\(x, y1) \ r. \(y2, z) \ r. y1 = y2 \ (x, z) \ r)" by (auto simp add: trans_def) +lemma transp_trans: + "transp r \ trans {(x, y). r x y}" + by (simp add: trans_def transp_def) + subsubsection {* Totality *} -definition - total_on :: "'a set => ('a * 'a) set => bool" where - "total_on A r \ (\x\A.\y\A. x\y \ (x,y)\r \ (y,x)\r)" +definition total_on :: "'a set \ 'a rel \ bool" +where + "total_on A r \ (\x\A. \y\A. x \ y \ (x, y) \ r \ (y, x) \ r)" abbreviation "total \ total_on UNIV" -lemma total_on_empty[simp]: "total_on {} r" -by(simp add:total_on_def) +lemma total_on_empty [simp]: "total_on {} r" + by (simp add: total_on_def) subsubsection {* Single valued relations *} -definition - single_valued :: "('a * 'b) set => bool" where - "single_valued r \ (ALL x y. (x,y):r --> (ALL z. (x,z):r --> y=z))" - -lemma single_valuedI: - "ALL x y. (x,y):r --> (ALL z. (x,z):r --> y=z) ==> single_valued r" -by (unfold single_valued_def) - -lemma single_valuedD: - "single_valued r ==> (x, y) : r ==> (x, z) : r ==> y = z" -by (simp add: single_valued_def) +definition single_valued :: "('a \ 'b) set \ bool" +where + "single_valued r \ (\x y. (x, y) \ r \ (\z. (x, z) \ r \ y = z))" abbreviation single_valuedP :: "('a \ 'b \ bool) \ bool" where "single_valuedP r \ single_valued {(x, y). r x y}" +lemma single_valuedI: + "ALL x y. (x,y):r --> (ALL z. (x,z):r --> y=z) ==> single_valued r" + by (unfold single_valued_def) + +lemma single_valuedD: + "single_valued r ==> (x, y) : r ==> (x, z) : r ==> y = z" + by (simp add: single_valued_def) + lemma single_valued_subset: "r \ s ==> single_valued s ==> single_valued r" -by (unfold single_valued_def) blast + by (unfold single_valued_def) blast subsection {* Relation operations *} subsubsection {* The identity relation *} -definition - Id :: "('a * 'a) set" where - "Id = {p. EX x. p = (x,x)}" +definition Id :: "'a rel" +where + "Id = {p. \x. p = (x, x)}" lemma IdI [intro]: "(a, a) : Id" -by (simp add: Id_def) + by (simp add: Id_def) lemma IdE [elim!]: "p : Id ==> (!!x. p = (x, x) ==> P) ==> P" -by (unfold Id_def) (iprover elim: CollectE) + by (unfold Id_def) (iprover elim: CollectE) lemma pair_in_Id_conv [iff]: "((a, b) : Id) = (a = b)" -by (unfold Id_def) blast + by (unfold Id_def) blast lemma refl_Id: "refl Id" -by (simp add: refl_on_def) + by (simp add: refl_on_def) lemma antisym_Id: "antisym Id" -- {* A strange result, since @{text Id} is also symmetric. *} -by (simp add: antisym_def) + by (simp add: antisym_def) lemma sym_Id: "sym Id" -by (simp add: sym_def) + by (simp add: sym_def) lemma trans_Id: "trans Id" -by (simp add: trans_def) + by (simp add: trans_def) lemma single_valued_Id [simp]: "single_valued Id" by (unfold single_valued_def) blast @@ -356,45 +434,45 @@ subsubsection {* Diagonal: identity over a set *} -definition - Id_on :: "'a set => ('a * 'a) set" where - "Id_on A = (\x\A. {(x,x)})" +definition Id_on :: "'a set \ 'a rel" +where + "Id_on A = (\x\A. {(x, x)})" lemma Id_on_empty [simp]: "Id_on {} = {}" -by (simp add: Id_on_def) + by (simp add: Id_on_def) lemma Id_on_eqI: "a = b ==> a : A ==> (a, b) : Id_on A" -by (simp add: Id_on_def) + by (simp add: Id_on_def) lemma Id_onI [intro!,no_atp]: "a : A ==> (a, a) : Id_on A" -by (rule Id_on_eqI) (rule refl) + by (rule Id_on_eqI) (rule refl) lemma Id_onE [elim!]: "c : Id_on A ==> (!!x. x : A ==> c = (x, x) ==> P) ==> P" -- {* The general elimination rule. *} -by (unfold Id_on_def) (iprover elim!: UN_E singletonE) + by (unfold Id_on_def) (iprover elim!: UN_E singletonE) lemma Id_on_iff: "((x, y) : Id_on A) = (x = y & x : A)" -by blast + by blast lemma Id_on_def' [nitpick_unfold]: "Id_on {x. A x} = Collect (\(x, y). x = y \ A x)" -by auto + by auto lemma Id_on_subset_Times: "Id_on A \ A \ A" -by blast + by blast lemma refl_on_Id_on: "refl_on A (Id_on A)" -by (rule refl_onI [OF Id_on_subset_Times Id_onI]) + by (rule refl_onI [OF Id_on_subset_Times Id_onI]) lemma antisym_Id_on [simp]: "antisym (Id_on A)" -by (unfold antisym_def) blast + by (unfold antisym_def) blast lemma sym_Id_on [simp]: "sym (Id_on A)" -by (rule symI) clarify + by (rule symI) clarify lemma trans_Id_on [simp]: "trans (Id_on A)" -by (fast intro: transI elim: transD) + by (fast intro: transI elim: transD) lemma single_valued_Id_on [simp]: "single_valued (Id_on A)" by (unfold single_valued_def) blast @@ -402,184 +480,228 @@ subsubsection {* Composition *} -definition rel_comp :: "('a \ 'b) set \ ('b \ 'c) set \ ('a * 'c) set" (infixr "O" 75) +inductive_set rel_comp :: "('a \ 'b) set \ ('b \ 'c) set \ ('a \ 'c) set" (infixr "O" 75) + for r :: "('a \ 'b) set" and s :: "('b \ 'c) set" where - "r O s = {(x, z). \y. (x, y) \ r \ (y, z) \ s}" + rel_compI [intro]: "(a, b) \ r \ (b, c) \ s \ (a, c) \ r O s" -lemma rel_compI [intro]: - "(a, b) : r ==> (b, c) : s ==> (a, c) : r O s" -by (unfold rel_comp_def) blast +abbreviation pred_comp (infixr "OO" 75) where + "pred_comp \ rel_compp" -lemma rel_compE [elim!]: "xz : r O s ==> - (!!x y z. xz = (x, z) ==> (x, y) : r ==> (y, z) : s ==> P) ==> P" -by (unfold rel_comp_def) (iprover elim!: CollectE splitE exE conjE) +lemmas pred_compI = rel_compp.intros -inductive pred_comp :: "('a \ 'b \ bool) \ ('b \ 'c \ bool) \ 'a \ 'c \ bool" (infixr "OO" 75) -for r :: "'a \ 'b \ bool" and s :: "'b \ 'c \ bool" -where - pred_compI [intro]: "r a b \ s b c \ (r OO s) a c" +text {* + For historic reasons, the elimination rules are not wholly corresponding. + Feel free to consolidate this. +*} +inductive_cases rel_compEpair: "(a, c) \ r O s" inductive_cases pred_compE [elim!]: "(r OO s) a c" -lemma pred_comp_rel_comp_eq [pred_set_conv]: - "((\x y. (x, y) \ r) OO (\x y. (x, y) \ s)) = (\x y. (x, y) \ r O s)" - by (auto simp add: fun_eq_iff) +lemma rel_compE [elim!]: "xz \ r O s \ + (\x y z. xz = (x, z) \ (x, y) \ r \ (y, z) \ s \ P) \ P" + by (cases xz) (simp, erule rel_compEpair, iprover) + +lemmas pred_comp_rel_comp_eq = rel_compp_rel_comp_eq + +lemma R_O_Id [simp]: + "R O Id = R" + by fast -lemma rel_compEpair: - "(a, c) : r O s ==> (!!y. (a, y) : r ==> (y, c) : s ==> P) ==> P" -by (iprover elim: rel_compE Pair_inject ssubst) +lemma Id_O_R [simp]: + "Id O R = R" + by fast + +lemma rel_comp_empty1 [simp]: + "{} O R = {}" + by blast -lemma R_O_Id [simp]: "R O Id = R" -by fast +(* CANDIDATE lemma pred_comp_bot1 [simp]: + "" + by (fact rel_comp_empty1 [to_pred]) *) -lemma Id_O_R [simp]: "Id O R = R" -by fast +lemma rel_comp_empty2 [simp]: + "R O {} = {}" + by blast -lemma rel_comp_empty1[simp]: "{} O R = {}" -by blast +(* CANDIDATE lemma pred_comp_bot2 [simp]: + "" + by (fact rel_comp_empty2 [to_pred]) *) -lemma rel_comp_empty2[simp]: "R O {} = {}" -by blast +lemma O_assoc: + "(R O S) O T = R O (S O T)" + by blast + +lemma pred_comp_assoc: + "(r OO s) OO t = r OO (s OO t)" + by (fact O_assoc [to_pred]) -lemma O_assoc: "(R O S) O T = R O (S O T)" -by blast +lemma trans_O_subset: + "trans r \ r O r \ r" + by (unfold trans_def) blast + +lemma transp_pred_comp_less_eq: + "transp r \ r OO r \ r " + by (fact trans_O_subset [to_pred]) -lemma trans_O_subset: "trans r ==> r O r \ r" -by (unfold trans_def) blast +lemma rel_comp_mono: + "r' \ r \ s' \ s \ r' O s' \ r O s" + by blast -lemma rel_comp_mono: "r' \ r ==> s' \ s ==> (r' O s') \ (r O s)" -by blast +lemma pred_comp_mono: + "r' \ r \ s' \ s \ r' OO s' \ r OO s " + by (fact rel_comp_mono [to_pred]) lemma rel_comp_subset_Sigma: - "r \ A \ B ==> s \ B \ C ==> (r O s) \ A \ C" -by blast + "r \ A \ B \ s \ B \ C \ r O s \ A \ C" + by blast + +lemma rel_comp_distrib [simp]: + "R O (S \ T) = (R O S) \ (R O T)" + by auto -lemma rel_comp_distrib[simp]: "R O (S \ T) = (R O S) \ (R O T)" -by auto +lemma pred_comp_distrib (* CANDIDATE [simp] *): + "R OO (S \ T) = R OO S \ R OO T" + by (fact rel_comp_distrib [to_pred]) + +lemma rel_comp_distrib2 [simp]: + "(S \ T) O R = (S O R) \ (T O R)" + by auto -lemma rel_comp_distrib2[simp]: "(S \ T) O R = (S O R) \ (T O R)" -by auto +lemma pred_comp_distrib2 (* CANDIDATE [simp] *): + "(S \ T) OO R = S OO R \ T OO R" + by (fact rel_comp_distrib2 [to_pred]) + +lemma rel_comp_UNION_distrib: + "s O UNION I r = (\i\I. s O r i) " + by auto -lemma rel_comp_UNION_distrib: "s O UNION I r = UNION I (%i. s O r i)" -by auto +(* FIXME thm rel_comp_UNION_distrib [to_pred] *) -lemma rel_comp_UNION_distrib2: "UNION I r O s = UNION I (%i. r i O s)" -by auto +lemma rel_comp_UNION_distrib2: + "UNION I r O s = (\i\I. r i O s) " + by auto + +(* FIXME thm rel_comp_UNION_distrib2 [to_pred] *) lemma single_valued_rel_comp: - "single_valued r ==> single_valued s ==> single_valued (r O s)" -by (unfold single_valued_def) blast + "single_valued r \ single_valued s \ single_valued (r O s)" + by (unfold single_valued_def) blast + +lemma rel_comp_unfold: + "r O s = {(x, z). \y. (x, y) \ r \ (y, z) \ s}" + by (auto simp add: set_eq_iff) subsubsection {* Converse *} -definition - converse :: "('a * 'b) set => ('b * 'a) set" - ("(_^-1)" [1000] 999) where - "r^-1 = {(y, x). (x, y) : r}" +inductive_set converse :: "('a \ 'b) set \ ('b \ 'a) set" ("(_^-1)" [1000] 999) + for r :: "('a \ 'b) set" +where + "(a, b) \ r \ (b, a) \ r^-1" notation (xsymbols) converse ("(_\)" [1000] 999) -lemma converseI [sym]: "(a, b) : r ==> (b, a) : r^-1" - by (simp add: converse_def) - -lemma converseD [sym]: "(a,b) : r^-1 ==> (b, a) : r" - by (simp add: converse_def) - -lemma converseE [elim!]: - "yx : r^-1 ==> (!!x y. yx = (y, x) ==> (x, y) : r ==> P) ==> P" - -- {* More general than @{text converseD}, as it ``splits'' the member of the relation. *} - by (unfold converse_def) (iprover elim!: CollectE splitE bexE) - -lemma converse_iff [iff]: "((a,b): r^-1) = ((b,a) : r)" - by (simp add: converse_def) - -inductive conversep :: "('a \ 'b \ bool) \ 'b \ 'a \ bool" ("(_^--1)" [1000] 1000) - for r :: "'a \ 'b \