1(* Title: ZF/pair.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1992 University of Cambridge 4*) 5 6section\<open>Ordered Pairs\<close> 7 8theory pair imports upair 9begin 10 11ML_file \<open>simpdata.ML\<close> 12 13setup \<open> 14 map_theory_simpset 15 (Simplifier.set_mksimps (fn ctxt => map mk_eq o ZF_atomize o Variable.gen_all ctxt) 16 #> Simplifier.add_cong @{thm if_weak_cong}) 17\<close> 18 19ML \<open>val ZF_ss = simpset_of \<^context>\<close> 20 21simproc_setup defined_Bex ("\<exists>x\<in>A. P(x) & Q(x)") = \<open> 22 fn _ => Quantifier1.rearrange_bex 23 (fn ctxt => 24 unfold_tac ctxt @{thms Bex_def} THEN 25 Quantifier1.prove_one_point_ex_tac ctxt) 26\<close> 27 28simproc_setup defined_Ball ("\<forall>x\<in>A. P(x) \<longrightarrow> Q(x)") = \<open> 29 fn _ => Quantifier1.rearrange_ball 30 (fn ctxt => 31 unfold_tac ctxt @{thms Ball_def} THEN 32 Quantifier1.prove_one_point_all_tac ctxt) 33\<close> 34 35 36(** Lemmas for showing that <a,b> uniquely determines a and b **) 37 38lemma singleton_eq_iff [iff]: "{a} = {b} \<longleftrightarrow> a=b" 39by (rule extension [THEN iff_trans], blast) 40 41lemma doubleton_eq_iff: "{a,b} = {c,d} \<longleftrightarrow> (a=c & b=d) | (a=d & b=c)" 42by (rule extension [THEN iff_trans], blast) 43 44lemma Pair_iff [simp]: "<a,b> = <c,d> \<longleftrightarrow> a=c & b=d" 45by (simp add: Pair_def doubleton_eq_iff, blast) 46 47lemmas Pair_inject = Pair_iff [THEN iffD1, THEN conjE, elim!] 48 49lemmas Pair_inject1 = Pair_iff [THEN iffD1, THEN conjunct1] 50lemmas Pair_inject2 = Pair_iff [THEN iffD1, THEN conjunct2] 51 52lemma Pair_not_0: "<a,b> \<noteq> 0" 53apply (unfold Pair_def) 54apply (blast elim: equalityE) 55done 56 57lemmas Pair_neq_0 = Pair_not_0 [THEN notE, elim!] 58 59declare sym [THEN Pair_neq_0, elim!] 60 61lemma Pair_neq_fst: "<a,b>=a ==> P" 62proof (unfold Pair_def) 63 assume eq: "{{a, a}, {a, b}} = a" 64 have "{a, a} \<in> {{a, a}, {a, b}}" by (rule consI1) 65 hence "{a, a} \<in> a" by (simp add: eq) 66 moreover have "a \<in> {a, a}" by (rule consI1) 67 ultimately show "P" by (rule mem_asym) 68qed 69 70lemma Pair_neq_snd: "<a,b>=b ==> P" 71proof (unfold Pair_def) 72 assume eq: "{{a, a}, {a, b}} = b" 73 have "{a, b} \<in> {{a, a}, {a, b}}" by blast 74 hence "{a, b} \<in> b" by (simp add: eq) 75 moreover have "b \<in> {a, b}" by blast 76 ultimately show "P" by (rule mem_asym) 77qed 78 79 80subsection\<open>Sigma: Disjoint Union of a Family of Sets\<close> 81 82text\<open>Generalizes Cartesian product\<close> 83 84lemma Sigma_iff [simp]: "<a,b>: Sigma(A,B) \<longleftrightarrow> a \<in> A & b \<in> B(a)" 85by (simp add: Sigma_def) 86 87lemma SigmaI [TC,intro!]: "[| a \<in> A; b \<in> B(a) |] ==> <a,b> \<in> Sigma(A,B)" 88by simp 89 90lemmas SigmaD1 = Sigma_iff [THEN iffD1, THEN conjunct1] 91lemmas SigmaD2 = Sigma_iff [THEN iffD1, THEN conjunct2] 92 93(*The general elimination rule*) 94lemma SigmaE [elim!]: 95 "[| c \<in> Sigma(A,B); 96 !!x y.[| x \<in> A; y \<in> B(x); c=<x,y> |] ==> P 97 |] ==> P" 98by (unfold Sigma_def, blast) 99 100lemma SigmaE2 [elim!]: 101 "[| <a,b> \<in> Sigma(A,B); 102 [| a \<in> A; b \<in> B(a) |] ==> P 103 |] ==> P" 104by (unfold Sigma_def, blast) 105 106lemma Sigma_cong: 107 "[| A=A'; !!x. x \<in> A' ==> B(x)=B'(x) |] ==> 108 Sigma(A,B) = Sigma(A',B')" 109by (simp add: Sigma_def) 110 111(*Sigma_cong, Pi_cong NOT given to Addcongs: they cause 112 flex-flex pairs and the "Check your prover" error. Most 113 Sigmas and Pis are abbreviated as * or -> *) 114 115lemma Sigma_empty1 [simp]: "Sigma(0,B) = 0" 116by blast 117 118lemma Sigma_empty2 [simp]: "A*0 = 0" 119by blast 120 121lemma Sigma_empty_iff: "A*B=0 \<longleftrightarrow> A=0 | B=0" 122by blast 123 124 125subsection\<open>Projections \<^term>\<open>fst\<close> and \<^term>\<open>snd\<close>\<close> 126 127lemma fst_conv [simp]: "fst(<a,b>) = a" 128by (simp add: fst_def) 129 130lemma snd_conv [simp]: "snd(<a,b>) = b" 131by (simp add: snd_def) 132 133lemma fst_type [TC]: "p \<in> Sigma(A,B) ==> fst(p) \<in> A" 134by auto 135 136lemma snd_type [TC]: "p \<in> Sigma(A,B) ==> snd(p) \<in> B(fst(p))" 137by auto 138 139lemma Pair_fst_snd_eq: "a \<in> Sigma(A,B) ==> <fst(a),snd(a)> = a" 140by auto 141 142 143subsection\<open>The Eliminator, \<^term>\<open>split\<close>\<close> 144 145(*A META-equality, so that it applies to higher types as well...*) 146lemma split [simp]: "split(%x y. c(x,y), <a,b>) == c(a,b)" 147by (simp add: split_def) 148 149lemma split_type [TC]: 150 "[| p \<in> Sigma(A,B); 151 !!x y.[| x \<in> A; y \<in> B(x) |] ==> c(x,y):C(<x,y>) 152 |] ==> split(%x y. c(x,y), p) \<in> C(p)" 153by (erule SigmaE, auto) 154 155lemma expand_split: 156 "u \<in> A*B ==> 157 R(split(c,u)) \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. u = <x,y> \<longrightarrow> R(c(x,y)))" 158by (auto simp add: split_def) 159 160 161subsection\<open>A version of \<^term>\<open>split\<close> for Formulae: Result Type \<^typ>\<open>o\<close>\<close> 162 163lemma splitI: "R(a,b) ==> split(R, <a,b>)" 164by (simp add: split_def) 165 166lemma splitE: 167 "[| split(R,z); z \<in> Sigma(A,B); 168 !!x y. [| z = <x,y>; R(x,y) |] ==> P 169 |] ==> P" 170by (auto simp add: split_def) 171 172lemma splitD: "split(R,<a,b>) ==> R(a,b)" 173by (simp add: split_def) 174 175text \<open> 176 \bigskip Complex rules for Sigma. 177\<close> 178 179lemma split_paired_Bex_Sigma [simp]: 180 "(\<exists>z \<in> Sigma(A,B). P(z)) \<longleftrightarrow> (\<exists>x \<in> A. \<exists>y \<in> B(x). P(<x,y>))" 181by blast 182 183lemma split_paired_Ball_Sigma [simp]: 184 "(\<forall>z \<in> Sigma(A,B). P(z)) \<longleftrightarrow> (\<forall>x \<in> A. \<forall>y \<in> B(x). P(<x,y>))" 185by blast 186 187end 188 189 190