Quelle Uprod.thy Sprache: Isabelle

(* Title: HOL/Library/Uprod.thy
   Author: Andreas Lochbihler, ETH Zurich *)

section \<open>Unordered pairs\<close>

theory Uprod imports Main begin

typedef ('a, 'b) commute = "{f :: 'a \ 'a \ 'b. \x y. f x y = f y x}"
  morphisms apply_commute Abs_commute
  by auto

setup_lifting type_definition_commute

lemma apply_commute_commute: "apply_commute f x y = apply_commute f y x"
by(transfer) simp

context includes lifting_syntax begin

lift_definition rel_commute :: "('a \ 'b \ bool) \ ('c \ 'd \ bool) \ ('a, 'c) commute \ ('b, 'd) commute \ bool"
is "\A B. A ===> A ===> B" .

end

definition eq_upair :: "('a \ 'a) \ ('a \ 'a) \ bool"
where "eq_upair = (\(a, b) (c, d). a = c \ b = d \ a = d \ b = c)"

lemma eq_upair_simps [simp]:
  "eq_upair (a, b) (c, d) \ a = c \ b = d \ a = d \ b = c"
by(simp add: eq_upair_def)

lemma equivp_eq_upair: "equivp eq_upair"
by(auto simp add: equivp_def fun_eq_iff)

quotient_type 'a uprod = "'a \<times> 'a" / eq_upair by(rule equivp_eq_upair)

lift_definition Upair :: "'a \ 'a \ 'a uprod" is Pair parametric Pair_transfer[of "A" "A" for A] .

lemma uprod_exhaust [case_names Upair, cases type: uprod]:
  obtains a b where "x = Upair a b"
by transfer fastforce

lemma Upair_inject [simp]: "Upair a b = Upair c d \ a = c \ b = d \ a = d \ b = c"
by transfer auto

code_datatype Upair

lift_definition case_uprod :: "('a, 'b) commute \ 'a uprod \ 'b" is case_prod
  parametric case_prod_transfer[of A A for A] by auto

lemma case_uprod_simps [simp, code]: "case_uprod f (Upair x y) = apply_commute f x y"
by transfer auto

lemma uprod_split: "P (case_uprod f x) \ (\a b. x = Upair a b \ P (apply_commute f a b))"
by transfer auto

lemma uprod_split_asm: "P (case_uprod f x) \ \ (\a b. x = Upair a b \ \ P (apply_commute f a b))"
by transfer auto

lift_definition not_equal :: "('a, bool) commute" is "(\)" by auto

lemma apply_not_equal [simp]: "apply_commute not_equal x y \ x \ y"
by transfer simp

definition proper_uprod :: "'a uprod \ bool"
where "proper_uprod = case_uprod not_equal"

lemma proper_uprod_simps [simp, code]: "proper_uprod (Upair x y) \ x \ y"
by(simp add: proper_uprod_def)

context includes lifting_syntax begin

private lemma set_uprod_parametric':
  "(rel_prod A A ===> rel_set A) (\(a, b). {a, b}) (\(a, b). {a, b})"
by transfer_prover

lift_definition set_uprod :: "'a uprod \ 'a set" is "\(a, b). {a, b}"
  parametric set_uprod_parametric' by auto

lemma set_uprod_simps [simp, code]: "set_uprod (Upair x y) = {x, y}"
by transfer simp

lemma finite_set_uprod [simp]: "finite (set_uprod x)"
by(cases x) simp

private lemma map_uprod_parametric':
  "((A ===> B) ===> rel_prod A A ===> rel_prod B B) (\f. map_prod f f) (\f. map_prod f f)"
by transfer_prover

lift_definition map_uprod :: "('a \ 'b) \ 'a uprod \ 'b uprod" is "\f. map_prod f f"
  parametric map_uprod_parametric' by auto

lemma map_uprod_simps [simp, code]: "map_uprod f (Upair x y) = Upair (f x) (f y)"
by transfer simp

private lemma rel_uprod_transfer':
  "((A ===> B ===> (=)) ===> rel_prod A A ===> rel_prod B B ===> (=))
   (\<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)"
by transfer_prover

lift_definition rel_uprod :: "('a \ 'b \ bool) \ 'a uprod \ 'b uprod \ bool"
  is "\R (a, b) (c, d). R a c \ R b d \ R a d \ R b c" parametric rel_uprod_transfer'
by auto

lemma rel_uprod_simps [simp, code]:
  "rel_uprod R (Upair a b) (Upair c d) \ R a c \ R b d \ R a d \ R b c"
by transfer auto

lemma Upair_parametric [transfer_rule]: "(A ===> A ===> rel_uprod A) Upair Upair"
unfolding rel_fun_def by transfer auto

lemma case_uprod_parametric [transfer_rule]:
  "(rel_commute A B ===> rel_uprod A ===> B) case_uprod case_uprod"
unfolding rel_fun_def by transfer(force dest: rel_funD)

end

bnf uprod: "'a uprod"
  map: map_uprod
  sets: set_uprod
  bd: natLeq
  rel: rel_uprod
proof -
  show "map_uprod id = id" unfolding fun_eq_iff by transfer auto
  show "map_uprod (g \ f) = map_uprod g \ map_uprod f" for f :: "'a \ 'b" and g :: "'b \ 'c"
    unfolding fun_eq_iff by transfer auto
  show "map_uprod f x = map_uprod g x" if "\z. z \ set_uprod x \ f z = g z"
    for f :: "'a \ 'b" and g x using that by transfer auto
  show "set_uprod \ map_uprod f = (`) f \ set_uprod" for f :: "'a \ 'b" by transfer auto
  show "card_order natLeq" by(rule natLeq_card_order)
  show "BNF_Cardinal_Arithmetic.cinfinite natLeq" by(rule natLeq_cinfinite)
  show "regularCard natLeq" by(rule regularCard_natLeq)
  show "ordLess2 (card_of (set_uprod x)) natLeq" for x :: "'a uprod"
    by (auto simp flip: finite_iff_ordLess_natLeq)
  show "rel_uprod R OO rel_uprod S \ rel_uprod (R OO S)"
    for R :: "'a \ 'b \ bool" and S :: "'b \ 'c \ bool" by(rule predicate2I)(transfer; auto)
  show "rel_uprod R = (\x y. \z. set_uprod z \ {(x, y). R x y} \ map_uprod fst z = x \ map_uprod snd z = y)"
    for R :: "'a \ 'b \ bool" by transfer(auto simp add: fun_eq_iff)
qed

lemma pred_uprod_code [simp, code]: "pred_uprod P (Upair x y) \ P x \ P y"
by(simp add: pred_uprod_def)

instantiation uprod :: (equal) equal begin

definition equal_uprod :: "'a uprod \ 'a uprod \ bool"
where "equal_uprod = (=)"

lemma equal_uprod_code [code]:
  "HOL.equal (Upair x y) (Upair z u) \ x = z \ y = u \ x = u \ y = z"
unfolding equal_uprod_def by simp

instance by standard(simp add: equal_uprod_def)
end

quickcheck_generator uprod constructors: Upair

lemma UNIV_uprod: "UNIV = (\x. Upair x x) ` UNIV \ (\(x, y). Upair x y) ` Sigma UNIV (\x. UNIV - {x})"
apply(rule set_eqI)
subgoal for x by(cases x) auto
done

context begin
private lift_definition upair_inv :: "'a uprod \ 'a"
is "\(x, y). if x = y then x else undefined" by auto

lemma finite_UNIV_prod [simp]:
  "finite (UNIV :: 'a uprod set) \ finite (UNIV :: 'a set)" (is "?lhs = ?rhs")
proof
  assume ?lhs
  hence "finite (range (\x :: 'a. Upair x x))" by(rule finite_subset[rotated]) simp
  hence "finite (upair_inv ` range (\x :: 'a. Upair x x))" by(rule finite_imageI)
  also have "upair_inv (Upair x x) = x" for x :: 'a by transfer simp
  then have "upair_inv ` range (\x :: 'a. Upair x x) = UNIV" by(auto simp add: image_image)
  finally show ?rhs .
qed(simp add: UNIV_uprod)

end

lemma card_UNIV_uprod:
  "card (UNIV :: 'a uprod set) = card (UNIV :: 'a set) * (card (UNIV :: 'a set) + 1) div 2"
  (is "?UPROD = ?A * _ div _")
proof(cases "finite (UNIV :: 'a set)")
  case True
  from True obtain f :: "nat \ 'a" where bij: "bij_betw f {0..
    by (blast dest: ex_bij_betw_nat_finite)
  hence [simp]: "f ` {0.. by(rule bij_betw_imp_surj_on)
  have "UNIV = (\(x, y). Upair (f x) (f y)) ` (SIGMA x:{0..
    apply(rule set_eqI)
    subgoal for x
      apply(cases x)
      apply(clarsimp)
      subgoal for a b
        apply(cases "inv_into {0.. inv_into {0..
        subgoal by(rule rev_image_eqI[where x="(inv_into {0..])
                  (auto simp add: inv_into_into[where A="{0.. and f=f, simplified] intro: f_inv_into_f[where f=f, symmetric])
        subgoal
          apply(simp only: not_le)
          apply(drule less_imp_le)
          apply(rule rev_image_eqI[where x="(inv_into {0..])
          apply(auto simp add: inv_into_into[where A="{0.. and f=f, simplified] intro: f_inv_into_f[where f=f, symmetric])
          done
        done
      done
    done
  hence "?UPROD = card \" by simp
  also have "\ = card (SIGMA x:{0..
    apply(rule card_image)
    using bij[THEN bij_betw_imp_inj_on]
    by(simp add: inj_on_def Ball_def)(metis leD le_eq_less_or_eq le_less_trans)
  also have "\ = sum Suc {0..
    by (subst card_SigmaI) simp_all
  also have "\ = sum of_nat {Suc 0..?A}"
    using sum.atLeastLessThan_reindex [symmetric, of Suc 0 ?A id]
    by (simp del: sum.op_ivl_Suc add: atLeastLessThanSuc_atLeastAtMost)
  also have "\ = ?A * (?A + 1) div 2"
    using gauss_sum_from_Suc_0 [of ?A, where ?'a = nat] by simp
  finally show ?thesis .
qed simp

end

quality100%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.