src/HOL/Library/Uprod.thy
author haftmann
Fri Mar 22 19:18:08 2019 +0000 (3 months ago)
changeset 69946 494934c30f38
parent 68406 6beb45f6cf67
child 70113 c8deb8ba6d05
permissions -rw-r--r--
improved code equations taken over from AFP
     1 (* Title: HOL/Library/Uprod.thy
     2    Author: Andreas Lochbihler, ETH Zurich *)
     3 
     4 section \<open>Unordered pairs\<close>
     5 
     6 theory Uprod imports Main begin
     7 
     8 typedef ('a, 'b) commute = "{f :: 'a \<Rightarrow> 'a \<Rightarrow> 'b. \<forall>x y. f x y = f y x}"
     9   morphisms apply_commute Abs_commute
    10   by auto
    11 
    12 setup_lifting type_definition_commute
    13 
    14 lemma apply_commute_commute: "apply_commute f x y = apply_commute f y x"
    15 by(transfer) simp
    16 
    17 context includes lifting_syntax begin
    18 
    19 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"
    20 is "\<lambda>A B. A ===> A ===> B" .
    21 
    22 end
    23 
    24 definition eq_upair :: "('a \<times> 'a) \<Rightarrow> ('a \<times> 'a) \<Rightarrow> bool"
    25 where "eq_upair = (\<lambda>(a, b) (c, d). a = c \<and> b = d \<or> a = d \<and> b = c)"
    26 
    27 lemma eq_upair_simps [simp]:
    28   "eq_upair (a, b) (c, d) \<longleftrightarrow> a = c \<and> b = d \<or> a = d \<and> b = c"
    29 by(simp add: eq_upair_def)
    30 
    31 lemma equivp_eq_upair: "equivp eq_upair"
    32 by(auto simp add: equivp_def fun_eq_iff)
    33 
    34 quotient_type 'a uprod = "'a \<times> 'a" / eq_upair by(rule equivp_eq_upair)
    35 
    36 lift_definition Upair :: "'a \<Rightarrow> 'a \<Rightarrow> 'a uprod" is Pair parametric Pair_transfer[of "A" "A" for A] .
    37 
    38 lemma uprod_exhaust [case_names Upair, cases type: uprod]:
    39   obtains a b where "x = Upair a b"
    40 by transfer fastforce
    41 
    42 lemma Upair_inject [simp]: "Upair a b = Upair c d \<longleftrightarrow> a = c \<and> b = d \<or> a = d \<and> b = c"
    43 by transfer auto
    44 
    45 code_datatype Upair
    46 
    47 lift_definition case_uprod :: "('a, 'b) commute \<Rightarrow> 'a uprod \<Rightarrow> 'b" is case_prod
    48   parametric case_prod_transfer[of A A for A] by auto
    49 
    50 lemma case_uprod_simps [simp, code]: "case_uprod f (Upair x y) = apply_commute f x y"
    51 by transfer auto
    52 
    53 lemma uprod_split: "P (case_uprod f x) \<longleftrightarrow> (\<forall>a b. x = Upair a b \<longrightarrow> P (apply_commute f a b))"
    54 by transfer auto
    55 
    56 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))"
    57 by transfer auto
    58 
    59 lift_definition not_equal :: "('a, bool) commute" is "(\<noteq>)" by auto
    60 
    61 lemma apply_not_equal [simp]: "apply_commute not_equal x y \<longleftrightarrow> x \<noteq> y"
    62 by transfer simp
    63 
    64 definition proper_uprod :: "'a uprod \<Rightarrow> bool"
    65 where "proper_uprod = case_uprod not_equal"
    66 
    67 lemma proper_uprod_simps [simp, code]: "proper_uprod (Upair x y) \<longleftrightarrow> x \<noteq> y"
    68 by(simp add: proper_uprod_def)
    69 
    70 context includes lifting_syntax begin
    71 
    72 private lemma set_uprod_parametric':
    73   "(rel_prod A A ===> rel_set A) (\<lambda>(a, b). {a, b}) (\<lambda>(a, b). {a, b})"
    74 by transfer_prover
    75 
    76 lift_definition set_uprod :: "'a uprod \<Rightarrow> 'a set" is "\<lambda>(a, b). {a, b}" 
    77   parametric set_uprod_parametric' by auto
    78 
    79 lemma set_uprod_simps [simp, code]: "set_uprod (Upair x y) = {x, y}"
    80 by transfer simp
    81 
    82 lemma finite_set_uprod [simp]: "finite (set_uprod x)"
    83 by(cases x) simp
    84 
    85 private lemma map_uprod_parametric':
    86   "((A ===> B) ===> rel_prod A A ===> rel_prod B B) (\<lambda>f. map_prod f f) (\<lambda>f. map_prod f f)"
    87 by transfer_prover
    88 
    89 lift_definition map_uprod :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a uprod \<Rightarrow> 'b uprod" is "\<lambda>f. map_prod f f"
    90   parametric map_uprod_parametric' by auto
    91 
    92 lemma map_uprod_simps [simp, code]: "map_uprod f (Upair x y) = Upair (f x) (f y)"
    93 by transfer simp
    94 
    95 private lemma rel_uprod_transfer':
    96   "((A ===> B ===> (=)) ===> rel_prod A A ===> rel_prod B B ===> (=))
    97    (\<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)"
    98 by transfer_prover
    99 
   100 lift_definition rel_uprod :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a uprod \<Rightarrow> 'b uprod \<Rightarrow> bool"
   101   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'
   102 by auto
   103 
   104 lemma rel_uprod_simps [simp, code]:
   105   "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"
   106 by transfer auto
   107 
   108 lemma Upair_parametric [transfer_rule]: "(A ===> A ===> rel_uprod A) Upair Upair"
   109 unfolding rel_fun_def by transfer auto
   110 
   111 lemma case_uprod_parametric [transfer_rule]:
   112   "(rel_commute A B ===> rel_uprod A ===> B) case_uprod case_uprod"
   113 unfolding rel_fun_def by transfer(force dest: rel_funD)
   114 
   115 end
   116 
   117 bnf uprod: "'a uprod" 
   118   map: map_uprod
   119   sets: set_uprod
   120   bd: natLeq
   121   rel: rel_uprod
   122 proof -
   123   show "map_uprod id = id" unfolding fun_eq_iff by transfer auto
   124   show "map_uprod (g \<circ> f) = map_uprod g \<circ> map_uprod f" for f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'c"
   125     unfolding fun_eq_iff by transfer auto
   126   show "map_uprod f x = map_uprod g x" if "\<And>z. z \<in> set_uprod x \<Longrightarrow> f z = g z" 
   127     for f :: "'a \<Rightarrow> 'b" and g x using that by transfer auto
   128   show "set_uprod \<circ> map_uprod f = (`) f \<circ> set_uprod" for f :: "'a \<Rightarrow> 'b" by transfer auto
   129   show "card_order natLeq" by(rule natLeq_card_order)
   130   show "BNF_Cardinal_Arithmetic.cinfinite natLeq" by(rule natLeq_cinfinite)
   131   show "ordLeq3 (card_of (set_uprod x)) natLeq" for x :: "'a uprod"
   132     by (auto simp flip: finite_iff_ordLess_natLeq intro: ordLess_imp_ordLeq)
   133   show "rel_uprod R OO rel_uprod S \<le> rel_uprod (R OO S)"
   134     for R :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and S :: "'b \<Rightarrow> 'c \<Rightarrow> bool" by(rule predicate2I)(transfer; auto)
   135   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)"
   136     for R :: "'a \<Rightarrow> 'b \<Rightarrow> bool" by transfer(auto simp add: fun_eq_iff)
   137 qed
   138 
   139 lemma pred_uprod_code [simp, code]: "pred_uprod P (Upair x y) \<longleftrightarrow> P x \<and> P y"
   140 by(simp add: pred_uprod_def)
   141 
   142 instantiation uprod :: (equal) equal begin
   143 
   144 definition equal_uprod :: "'a uprod \<Rightarrow> 'a uprod \<Rightarrow> bool"
   145 where "equal_uprod = (=)"
   146 
   147 lemma equal_uprod_code [code]:
   148   "HOL.equal (Upair x y) (Upair z u) \<longleftrightarrow> x = z \<and> y = u \<or> x = u \<and> y = z"
   149 unfolding equal_uprod_def by simp
   150 
   151 instance by standard(simp add: equal_uprod_def)
   152 end
   153 
   154 quickcheck_generator uprod constructors: Upair
   155 
   156 lemma UNIV_uprod: "UNIV = (\<lambda>x. Upair x x) ` UNIV \<union> (\<lambda>(x, y). Upair x y) ` Sigma UNIV (\<lambda>x. UNIV - {x})"
   157 apply(rule set_eqI)
   158 subgoal for x by(cases x) auto
   159 done
   160 
   161 context begin
   162 private lift_definition upair_inv :: "'a uprod \<Rightarrow> 'a"
   163 is "\<lambda>(x, y). if x = y then x else undefined" by auto
   164 
   165 lemma finite_UNIV_prod [simp]:
   166   "finite (UNIV :: 'a uprod set) \<longleftrightarrow> finite (UNIV :: 'a set)" (is "?lhs = ?rhs")
   167 proof
   168   assume ?lhs
   169   hence "finite (range (\<lambda>x :: 'a. Upair x x))" by(rule finite_subset[rotated]) simp
   170   hence "finite (upair_inv ` range (\<lambda>x :: 'a. Upair x x))" by(rule finite_imageI)
   171   also have "upair_inv (Upair x x) = x" for x :: 'a by transfer simp
   172   then have "upair_inv ` range (\<lambda>x :: 'a. Upair x x) = UNIV" by(auto simp add: image_image)
   173   finally show ?rhs .
   174 qed(simp add: UNIV_uprod)
   175 
   176 end
   177 
   178 lemma card_UNIV_uprod:
   179   "card (UNIV :: 'a uprod set) = card (UNIV :: 'a set) * (card (UNIV :: 'a set) + 1) div 2"
   180   (is "?UPROD = ?A * _ div _")
   181 proof(cases "finite (UNIV :: 'a set)")
   182   case True
   183   from True obtain f :: "nat \<Rightarrow> 'a" where bij: "bij_betw f {0..<?A} UNIV"
   184     by (blast dest: ex_bij_betw_nat_finite)
   185   hence [simp]: "f ` {0..<?A} = UNIV" by(rule bij_betw_imp_surj_on)
   186   have "UNIV = (\<lambda>(x, y). Upair (f x) (f y)) ` (SIGMA x:{0..<?A}. {..x})"
   187     apply(rule set_eqI)
   188     subgoal for x
   189       apply(cases x)
   190       apply(clarsimp)
   191       subgoal for a b
   192         apply(cases "inv_into {0..<?A} f a \<le> inv_into {0..<?A} f b")
   193         subgoal by(rule rev_image_eqI[where x="(inv_into {0..<?A} f _, inv_into {0..<?A} f _)"])
   194                   (auto simp add: inv_into_into[where A="{0..<?A}" and f=f, simplified] intro: f_inv_into_f[where f=f, symmetric])
   195         subgoal
   196           apply(simp only: not_le)
   197           apply(drule less_imp_le)
   198           apply(rule rev_image_eqI[where x="(inv_into {0..<?A} f _, inv_into {0..<?A} f _)"])
   199           apply(auto simp add: inv_into_into[where A="{0..<?A}" and f=f, simplified] intro: f_inv_into_f[where f=f, symmetric])
   200           done
   201         done
   202       done
   203     done
   204   hence "?UPROD = card \<dots>" by simp
   205   also have "\<dots> = card (SIGMA x:{0..<?A}. {..x})"
   206     apply(rule card_image)
   207     using bij[THEN bij_betw_imp_inj_on]
   208     by(simp add: inj_on_def Ball_def)(metis leD le_eq_less_or_eq le_less_trans)
   209   also have "\<dots> = sum Suc {0..<?A}"
   210     by (subst card_SigmaI) simp_all
   211   also have "\<dots> = sum of_nat {Suc 0..?A}"
   212     using sum.atLeastLessThan_reindex [symmetric, of Suc 0 ?A id]
   213     by (simp del: sum_op_ivl_Suc add: atLeastLessThanSuc_atLeastAtMost)
   214   also have "\<dots> = ?A * (?A + 1) div 2"
   215     using gauss_sum_from_Suc_0 [of ?A, where ?'a = nat] by simp
   216   finally show ?thesis .
   217 qed simp
   218 
   219 end