add type of unordered pairs
authorAndreas Lochbihler
Wed Aug 30 18:01:27 2017 +0200 (21 months ago)
changeset 6656387b9eb69d5ba
parent 66554 19bf4d5966dc
child 66564 090c4474f310
add type of unordered pairs
CONTRIBUTORS
NEWS
src/HOL/Library/Library.thy
src/HOL/Library/Uprod.thy
     1.1 --- a/CONTRIBUTORS	Tue Aug 29 20:34:43 2017 +0100
     1.2 +++ b/CONTRIBUTORS	Wed Aug 30 18:01:27 2017 +0200
     1.3 @@ -14,6 +14,9 @@
     1.4    Prover IDE improvements.
     1.5    Support for SQL databases in Isabelle/Scala: SQLite and PostgreSQL.
     1.6  
     1.7 +* August 2017: Andreas Lochbihler, ETH Zurich
     1.8 +  type of unordered pairs (HOL-Library.Uprod)
     1.9 +
    1.10  * August 2017: Manuel Eberl, TUM
    1.11    HOL-Analysis: infinite products over natural numbers,
    1.12    infinite sums over arbitrary sets, connection between formal
     2.1 --- a/NEWS	Tue Aug 29 20:34:43 2017 +0100
     2.2 +++ b/NEWS	Wed Aug 30 18:01:27 2017 +0200
     2.3 @@ -250,6 +250,8 @@
     2.4  * Theory "HOL-Library.Pattern_Aliases" provides input and output syntax
     2.5  for pattern aliases as known from Haskell, Scala and ML.
     2.6  
     2.7 +* Theory "HOL-Library.Uprod" formalizes the type of unordered pairs.
     2.8 +
     2.9  * Session HOL-Analysis: more material involving arcs, paths, covering
    2.10  spaces, innessential maps, retracts, material on infinite products.
    2.11  Major results include the Jordan Curve Theorem and the Great Picard
     3.1 --- a/src/HOL/Library/Library.thy	Tue Aug 29 20:34:43 2017 +0100
     3.2 +++ b/src/HOL/Library/Library.thy	Wed Aug 30 18:01:27 2017 +0200
     3.3 @@ -82,6 +82,7 @@
     3.4    Tree_Multiset
     3.5    Tree_Real
     3.6    Type_Length
     3.7 +  Uprod
     3.8    While_Combinator
     3.9  begin
    3.10  end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Library/Uprod.thy	Wed Aug 30 18:01:27 2017 +0200
     4.3 @@ -0,0 +1,219 @@
     4.4 +(* Title: HOL/Library/Uprod.thy
     4.5 +   Author: Andreas Lochbihler, ETH Zurich *)
     4.6 +
     4.7 +section \<open>Unordered pairs\<close>
     4.8 +
     4.9 +theory Uprod imports Main begin
    4.10 +
    4.11 +typedef ('a, 'b) commute = "{f :: 'a \<Rightarrow> 'a \<Rightarrow> 'b. \<forall>x y. f x y = f y x}"
    4.12 +  morphisms apply_commute Abs_commute
    4.13 +  by auto
    4.14 +
    4.15 +setup_lifting type_definition_commute
    4.16 +
    4.17 +lemma apply_commute_commute: "apply_commute f x y = apply_commute f y x"
    4.18 +by(transfer) simp
    4.19 +
    4.20 +context includes lifting_syntax begin
    4.21 +
    4.22 +lift_definition rel_commute :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a, 'c) commute \<Rightarrow> ('b, 'd) commute \<Rightarrow> bool"
    4.23 +is "\<lambda>A B. A ===> A ===> B" .
    4.24 +
    4.25 +end
    4.26 +
    4.27 +definition eq_upair :: "('a \<times> 'a) \<Rightarrow> ('a \<times> 'a) \<Rightarrow> bool"
    4.28 +where "eq_upair = (\<lambda>(a, b) (c, d). a = c \<and> b = d \<or> a = d \<and> b = c)"
    4.29 +
    4.30 +lemma eq_upair_simps [simp]:
    4.31 +  "eq_upair (a, b) (c, d) \<longleftrightarrow> a = c \<and> b = d \<or> a = d \<and> b = c"
    4.32 +by(simp add: eq_upair_def)
    4.33 +
    4.34 +lemma equivp_eq_upair: "equivp eq_upair"
    4.35 +by(auto simp add: equivp_def fun_eq_iff)
    4.36 +
    4.37 +quotient_type 'a uprod = "'a \<times> 'a" / eq_upair by(rule equivp_eq_upair)
    4.38 +
    4.39 +lift_definition Upair :: "'a \<Rightarrow> 'a \<Rightarrow> 'a uprod" is Pair parametric Pair_transfer[of "A" "A" for A] .
    4.40 +
    4.41 +lemma uprod_exhaust [case_names Upair, cases type: uprod]:
    4.42 +  obtains a b where "x = Upair a b"
    4.43 +by transfer fastforce
    4.44 +
    4.45 +lemma Upair_inject [simp]: "Upair a b = Upair c d \<longleftrightarrow> a = c \<and> b = d \<or> a = d \<and> b = c"
    4.46 +by transfer auto
    4.47 +
    4.48 +code_datatype Upair
    4.49 +
    4.50 +lift_definition case_uprod :: "('a, 'b) commute \<Rightarrow> 'a uprod \<Rightarrow> 'b" is case_prod
    4.51 +  parametric case_prod_transfer[of A A for A] by auto
    4.52 +
    4.53 +lemma case_uprod_simps [simp, code]: "case_uprod f (Upair x y) = apply_commute f x y"
    4.54 +by transfer auto
    4.55 +
    4.56 +lemma uprod_split: "P (case_uprod f x) \<longleftrightarrow> (\<forall>a b. x = Upair a b \<longrightarrow> P (apply_commute f a b))"
    4.57 +by transfer auto
    4.58 +
    4.59 +lemma uprod_split_asm: "P (case_uprod f x) \<longleftrightarrow> \<not> (\<exists>a b. x = Upair a b \<and> \<not> P (apply_commute f a b))"
    4.60 +by transfer auto
    4.61 +
    4.62 +lift_definition not_equal :: "('a, bool) commute" is "op \<noteq>" by auto
    4.63 +
    4.64 +lemma apply_not_equal [simp]: "apply_commute not_equal x y \<longleftrightarrow> x \<noteq> y"
    4.65 +by transfer simp
    4.66 +
    4.67 +definition proper_uprod :: "'a uprod \<Rightarrow> bool"
    4.68 +where "proper_uprod = case_uprod not_equal"
    4.69 +
    4.70 +lemma proper_uprod_simps [simp, code]: "proper_uprod (Upair x y) \<longleftrightarrow> x \<noteq> y"
    4.71 +by(simp add: proper_uprod_def)
    4.72 +
    4.73 +context includes lifting_syntax begin
    4.74 +
    4.75 +private lemma set_uprod_parametric':
    4.76 +  "(rel_prod A A ===> rel_set A) (\<lambda>(a, b). {a, b}) (\<lambda>(a, b). {a, b})"
    4.77 +by transfer_prover
    4.78 +
    4.79 +lift_definition set_uprod :: "'a uprod \<Rightarrow> 'a set" is "\<lambda>(a, b). {a, b}" 
    4.80 +  parametric set_uprod_parametric' by auto
    4.81 +
    4.82 +lemma set_uprod_simps [simp, code]: "set_uprod (Upair x y) = {x, y}"
    4.83 +by transfer simp
    4.84 +
    4.85 +lemma finite_set_uprod [simp]: "finite (set_uprod x)"
    4.86 +by(cases x) simp
    4.87 +
    4.88 +private lemma map_uprod_parametric':
    4.89 +  "((A ===> B) ===> rel_prod A A ===> rel_prod B B) (\<lambda>f. map_prod f f) (\<lambda>f. map_prod f f)"
    4.90 +by transfer_prover
    4.91 +
    4.92 +lift_definition map_uprod :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a uprod \<Rightarrow> 'b uprod" is "\<lambda>f. map_prod f f"
    4.93 +  parametric map_uprod_parametric' by auto
    4.94 +
    4.95 +lemma map_uprod_simps [simp, code]: "map_uprod f (Upair x y) = Upair (f x) (f y)"
    4.96 +by transfer simp
    4.97 +
    4.98 +private lemma rel_uprod_transfer':
    4.99 +  "((A ===> B ===> op =) ===> rel_prod A A ===> rel_prod B B ===> op =)
   4.100 +   (\<lambda>R (a, b) (c, d). R a c \<and> R b d \<or> R a d \<and> R b c) (\<lambda>R (a, b) (c, d). R a c \<and> R b d \<or> R a d \<and> R b c)"
   4.101 +by transfer_prover
   4.102 +
   4.103 +lift_definition rel_uprod :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a uprod \<Rightarrow> 'b uprod \<Rightarrow> bool"
   4.104 +  is "\<lambda>R (a, b) (c, d). R a c \<and> R b d \<or> R a d \<and> R b c" parametric rel_uprod_transfer'
   4.105 +by auto
   4.106 +
   4.107 +lemma rel_uprod_simps [simp, code]:
   4.108 +  "rel_uprod R (Upair a b) (Upair c d) \<longleftrightarrow> R a c \<and> R b d \<or> R a d \<and> R b c"
   4.109 +by transfer auto
   4.110 +
   4.111 +lemma Upair_parametric [transfer_rule]: "(A ===> A ===> rel_uprod A) Upair Upair"
   4.112 +unfolding rel_fun_def by transfer auto
   4.113 +
   4.114 +lemma case_uprod_parametric [transfer_rule]:
   4.115 +  "(rel_commute A B ===> rel_uprod A ===> B) case_uprod case_uprod"
   4.116 +unfolding rel_fun_def by transfer(force dest: rel_funD)
   4.117 +
   4.118 +end
   4.119 +
   4.120 +bnf uprod: "'a uprod" 
   4.121 +  map: map_uprod
   4.122 +  sets: set_uprod
   4.123 +  bd: natLeq
   4.124 +  rel: rel_uprod
   4.125 +proof -
   4.126 +  show "map_uprod id = id" unfolding fun_eq_iff by transfer auto
   4.127 +  show "map_uprod (g \<circ> f) = map_uprod g \<circ> map_uprod f" for f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'c"
   4.128 +    unfolding fun_eq_iff by transfer auto
   4.129 +  show "map_uprod f x = map_uprod g x" if "\<And>z. z \<in> set_uprod x \<Longrightarrow> f z = g z" 
   4.130 +    for f :: "'a \<Rightarrow> 'b" and g x using that by transfer auto
   4.131 +  show "set_uprod \<circ> map_uprod f = op ` f \<circ> set_uprod" for f :: "'a \<Rightarrow> 'b" by transfer auto
   4.132 +  show "card_order natLeq" by(rule natLeq_card_order)
   4.133 +  show "BNF_Cardinal_Arithmetic.cinfinite natLeq" by(rule natLeq_cinfinite)
   4.134 +  show "ordLeq3 (card_of (set_uprod x)) natLeq" for x :: "'a uprod"
   4.135 +    by (auto simp: finite_iff_ordLess_natLeq[symmetric] intro: ordLess_imp_ordLeq)
   4.136 +  show "rel_uprod R OO rel_uprod S \<le> rel_uprod (R OO S)"
   4.137 +    for R :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and S :: "'b \<Rightarrow> 'c \<Rightarrow> bool" by(rule predicate2I)(transfer; auto)
   4.138 +  show "rel_uprod R = (\<lambda>x y. \<exists>z. set_uprod z \<subseteq> {(x, y). R x y} \<and> map_uprod fst z = x \<and> map_uprod snd z = y)"
   4.139 +    for R :: "'a \<Rightarrow> 'b \<Rightarrow> bool" by transfer(auto simp add: fun_eq_iff)
   4.140 +qed
   4.141 +
   4.142 +lemma pred_uprod_code [simp, code]: "pred_uprod P (Upair x y) \<longleftrightarrow> P x \<and> P y"
   4.143 +by(simp add: pred_uprod_def)
   4.144 +
   4.145 +instantiation uprod :: (equal) equal begin
   4.146 +
   4.147 +definition equal_uprod :: "'a uprod \<Rightarrow> 'a uprod \<Rightarrow> bool"
   4.148 +where "equal_uprod = op ="
   4.149 +
   4.150 +lemma equal_uprod_code [code]:
   4.151 +  "HOL.equal (Upair x y) (Upair z u) \<longleftrightarrow> x = z \<and> y = u \<or> x = u \<and> y = z"
   4.152 +unfolding equal_uprod_def by simp
   4.153 +
   4.154 +instance by standard(simp add: equal_uprod_def)
   4.155 +end
   4.156 +
   4.157 +quickcheck_generator uprod constructors: Upair
   4.158 +
   4.159 +lemma UNIV_uprod: "UNIV = (\<lambda>x. Upair x x) ` UNIV \<union> (\<lambda>(x, y). Upair x y) ` Sigma UNIV (\<lambda>x. UNIV - {x})"
   4.160 +apply(rule set_eqI)
   4.161 +subgoal for x by(cases x) auto
   4.162 +done
   4.163 +
   4.164 +context begin
   4.165 +private lift_definition upair_inv :: "'a uprod \<Rightarrow> 'a"
   4.166 +is "\<lambda>(x, y). if x = y then x else undefined" by auto
   4.167 +
   4.168 +lemma finite_UNIV_prod [simp]:
   4.169 +  "finite (UNIV :: 'a uprod set) \<longleftrightarrow> finite (UNIV :: 'a set)" (is "?lhs = ?rhs")
   4.170 +proof
   4.171 +  assume ?lhs
   4.172 +  hence "finite (range (\<lambda>x :: 'a. Upair x x))" by(rule finite_subset[rotated]) simp
   4.173 +  hence "finite (upair_inv ` range (\<lambda>x :: 'a. Upair x x))" by(rule finite_imageI)
   4.174 +  also have "upair_inv (Upair x x) = x" for x :: 'a by transfer simp
   4.175 +  then have "upair_inv ` range (\<lambda>x :: 'a. Upair x x) = UNIV" by(auto simp add: image_image)
   4.176 +  finally show ?rhs .
   4.177 +qed(simp add: UNIV_uprod)
   4.178 +
   4.179 +end
   4.180 +
   4.181 +lemma card_UNIV_uprod:
   4.182 +  "card (UNIV :: 'a uprod set) = card (UNIV :: 'a set) * (card (UNIV :: 'a set) + 1) div 2"
   4.183 +  (is "?UPROD = ?A * _ div _")
   4.184 +proof(cases "finite (UNIV :: 'a set)")
   4.185 +  case True
   4.186 +  from True obtain f :: "nat \<Rightarrow> 'a" where bij: "bij_betw f {0..<?A} UNIV"
   4.187 +    by (blast dest: ex_bij_betw_nat_finite)
   4.188 +  hence [simp]: "f ` {0..<?A} = UNIV" by(rule bij_betw_imp_surj_on)
   4.189 +  have "UNIV = (\<lambda>(x, y). Upair (f x) (f y)) ` (SIGMA x:{0..<?A}. {..x})"
   4.190 +    apply(rule set_eqI)
   4.191 +    subgoal for x
   4.192 +      apply(cases x)
   4.193 +      apply(clarsimp)
   4.194 +      subgoal for a b
   4.195 +        apply(cases "inv_into {0..<?A} f a \<le> inv_into {0..<?A} f b")
   4.196 +        subgoal by(rule rev_image_eqI[where x="(inv_into {0..<?A} f _, inv_into {0..<?A} f _)"])
   4.197 +                  (auto simp add: inv_into_into[where A="{0..<?A}" and f=f, simplified] intro: f_inv_into_f[where f=f, symmetric])
   4.198 +        subgoal
   4.199 +          apply(simp only: not_le)
   4.200 +          apply(drule less_imp_le)
   4.201 +          apply(rule rev_image_eqI[where x="(inv_into {0..<?A} f _, inv_into {0..<?A} f _)"])
   4.202 +          apply(auto simp add: inv_into_into[where A="{0..<?A}" and f=f, simplified] intro: f_inv_into_f[where f=f, symmetric])
   4.203 +          done
   4.204 +        done
   4.205 +      done
   4.206 +    done
   4.207 +  hence "?UPROD = card \<dots>" by simp
   4.208 +  also have "\<dots> = card (SIGMA x:{0..<?A}. {..x})"
   4.209 +    apply(rule card_image)
   4.210 +    using bij[THEN bij_betw_imp_inj_on]
   4.211 +    by(simp add: inj_on_def Ball_def)(metis leD le_eq_less_or_eq le_less_trans)
   4.212 +  also have "\<dots> = sum (\<lambda>n. n + 1) {0..<?A}"
   4.213 +    by(subst card_SigmaI) simp_all
   4.214 +  also have "\<dots> = 2 * sum of_nat {1..?A} div 2"
   4.215 +    using sum.reindex[where g="of_nat :: nat \<Rightarrow> nat" and h="\<lambda>x. x + 1" and A="{0..<?A}", symmetric] True
   4.216 +    by(simp del: sum_op_ivl_Suc add: atLeastLessThanSuc_atLeastAtMost)
   4.217 +  also have "\<dots> = ?A * (?A + 1) div 2"
   4.218 +    by(subst gauss_sum) simp
   4.219 +  finally show ?thesis .
   4.220 +qed simp
   4.221 +
   4.222 +end