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