Quelle  pair.thy   Sprache: Isabelle

(*  Title:      ZF/pair.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1992  University of Cambridge
*)

section‹Ordered Pairs›

theory pair imports upair
begin

ML_file ‹simpdata.ML›

setup ‹
  map_theory_simpset
    (Simplifier.set_mksimps (fn ctxt => map mk_eq o ZF_atomize o Variable.gen_all ctxt)
      #> Simplifier.add_cong @{thm if_weak_cong})
›

ML ‹val ZF_ss = simpset_of 🍋›

simproc_setup defined_Bex ("\x\A. P(x) \ Q(x)") = ‹
  K (Quantifier1.rearrange_Bex (fn ctxt => unfold_tac ctxt @{thms Bex_def}))
›

simproc_setup defined_Ball ("\x\A. P(x) \ Q(x)") = ‹
  K (Quantifier1.rearrange_Ball (fn ctxt => unfold_tac ctxt @{thms Ball_def}))
›


(** Lemmas for showing that \<langle>a,b\<rangle> uniquely determines a and b **)

lemma singleton_eq_iff [iff]: "{a} = {b} \ a=b"
by (rule extension [THEN iff_trans], blast)

lemma doubleton_eq_iff: "{a,b} = {c,d} \ (a=c \ b=d) | (a=d \ b=c)"
by (rule extension [THEN iff_trans], blast)

lemma Pair_iff [simp]: "\a,b\ = \c,d\ \ a=c \ b=d"
by (simp add: Pair_def doubleton_eq_iff, blast)

lemmas Pair_inject = Pair_iff [THEN iffD1, THEN conjE, elim!]

lemmas Pair_inject1 = Pair_iff [THEN iffD1, THEN conjunct1]
lemmas Pair_inject2 = Pair_iff [THEN iffD1, THEN conjunct2]

lemma Pair_not_0: "\a,b\ \ 0"
  unfolding Pair_def
apply (blast elim: equalityE)
done

lemmas Pair_neq_0 = Pair_not_0 [THEN notE, elim!]

declare sym [THEN Pair_neq_0, elim!]

lemma Pair_neq_fst: "\a,b\=a \ P"
proof (unfold Pair_def)
  assume eq: "{{a, a}, {a, b}} = a"
  have  "{a, a} \ {{a, a}, {a, b}}" by (rule consI1)
  hence "{a, a} \ a" by (simp add: eq)
  moreover have "a \ {a, a}" by (rule consI1)
  ultimately show "P" by (rule mem_asym)
qed

lemma Pair_neq_snd: "\a,b\=b \ P"
proof (unfold Pair_def)
  assume eq: "{{a, a}, {a, b}} = b"
  have  "{a, b} \ {{a, a}, {a, b}}" by blast
  hence "{a, b} \ b" by (simp add: eq)
  moreover have "b \ {a, b}" by blast
  ultimately show "P" by (rule mem_asym)
qed


subsection‹Sigma: Disjoint Union of a Family of Sets›

text‹Generalizes Cartesian product›

lemma Sigma_iff [simp]: "\a,b\: Sigma(A,B) \ a \ A \ b \ B(a)"
by (simp add: Sigma_def)

lemma SigmaI [TC,intro!]: "\a \ A; b \ B(a)\ \ \a,b\ \ Sigma(A,B)"
by simp

lemmas SigmaD1 = Sigma_iff [THEN iffD1, THEN conjunct1]
lemmas SigmaD2 = Sigma_iff [THEN iffD1, THEN conjunct2]

(*The general elimination rule*)
lemma SigmaE [elim!]:
    "\c \ Sigma(A,B);
        ∧x y.[x ∈ A;  y ∈ B(x);  c=⟨x,y⟩] ==> P
] ==> P"
by (unfold Sigma_def, blast)

lemma SigmaE2 [elim!]:
    "\\a,b\ \ Sigma(A,B);
        [a ∈ A;  b ∈ B(a)] ==> P
] ==> P"
by (unfold Sigma_def, blast)

lemma Sigma_cong:
    "\A=A'; \x. x \ A' \ B(x)=B'(x)\ \
     Sigma(A,B) = Sigma(A',B')"
by (simp add: Sigma_def)

(*Sigma_cong, Pi_cong NOT given to Addcongs: they cause
  flex-flex pairs and the "Check your prover" error.  Most
  Sigmas and Pis are abbreviated as * or -> *)

lemma Sigma_empty1 [simp]: "Sigma(0,B) = 0"
by blast

lemma Sigma_empty2 [simp]: "A*0 = 0"
by blast

lemma Sigma_empty_iff: "A*B=0 \ A=0 | B=0"
by blast


subsection‹Projections 🍋‹fst› and 🍋‹snd››

lemma fst_conv [simp]: "fst(\a,b\) = a"
by (simp add: fst_def)

lemma snd_conv [simp]: "snd(\a,b\) = b"
by (simp add: snd_def)

lemma fst_type [TC]: "p \ Sigma(A,B) \ fst(p) \ A"
by auto

lemma snd_type [TC]: "p \ Sigma(A,B) \ snd(p) \ B(fst(p))"
by auto

lemma Pair_fst_snd_eq: "a \ Sigma(A,B) \ = a"
by auto


subsection‹The Eliminator, 🍋‹split››

(*A META-equality, so that it applies to higher types as well...*)
lemma split [simp]: "split(\x y. c(x,y), \a,b\) \ c(a,b)"
by (simp add: split_def)

lemma split_type [TC]:
    "\p \ Sigma(A,B);
         ∧x y.[x ∈ A; y ∈ B(x)] ==> c(x,y):C(⟨x,y⟩)
] ==> split(λx y. c(x,y), p) ∈ C(p)"
by (erule SigmaE, auto)

lemma expand_split:
  "u \ A*B \
        R(split(c,u)) ⟷ (∀x∈A. ∀y∈B. u = ⟨x,y⟩ ⟶ R(c(x,y)))"
by (auto simp add: split_def)


subsection‹A version of 🍋‹split› for Formulae: Result Type 🍋‹o››

lemma splitI: "R(a,b) \ split(R, \a,b\)"
by (simp add: split_def)

lemma splitE:
    "\split(R,z); z \ Sigma(A,B);
        ∧x y. [z = ⟨x,y⟩;  R(x,y)] ==> P
] ==> P"
by (auto simp add: split_def)

lemma splitD: "split(R,\a,b\) \ R(a,b)"
by (simp add: split_def)

text ‹
  \bigskip Complex rules for Sigma.
›

lemma split_paired_Bex_Sigma [simp]:
     "(\z \ Sigma(A,B). P(z)) \ (\x \ A. \y \ B(x). P(\x,y\))"
by blast

lemma split_paired_Ball_Sigma [simp]:
     "(\z \ Sigma(A,B). P(z)) \ (\x \ A. \y \ B(x). P(\x,y\))"
by blast

end