src/HOL/Library/Quotient_Set.thy
author krauss
Sat, 10 Sep 2011 22:43:17 +0200
changeset 44873 045fedcfadf6
parent 44459 079ccfb074d9
child 45970 b6d0cff57d96
permissions -rw-r--r--
mem_prs and mem_rsp in accordance with sets-as-predicates representation (backported from AFP/Coinductive)
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
44413
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     1
(*  Title:      HOL/Library/Quotient_Set.thy
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     2
    Author:     Cezary Kaliszyk and Christian Urban
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     3
*)
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     4
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     5
header {* Quotient infrastructure for the set type *}
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     6
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     7
theory Quotient_Set
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     8
imports Main Quotient_Syntax
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     9
begin
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    10
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    11
lemma set_quotient [quot_thm]:
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    12
  assumes "Quotient R Abs Rep"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    13
  shows "Quotient (set_rel R) (vimage Rep) (vimage Abs)"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    14
proof (rule QuotientI)
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    15
  from assms have "\<And>x. Abs (Rep x) = x" by (rule Quotient_abs_rep)
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    16
  then show "\<And>xs. Rep -` (Abs -` xs) = xs"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    17
    unfolding vimage_def by auto
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    18
next
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    19
  show "\<And>xs. set_rel R (Abs -` xs) (Abs -` xs)"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    20
    unfolding set_rel_def vimage_def
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    21
    by auto (metis Quotient_rel_abs[OF assms])+
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    22
next
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    23
  fix r s
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    24
  show "set_rel R r s = (set_rel R r r \<and> set_rel R s s \<and> Rep -` r = Rep -` s)"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    25
    unfolding set_rel_def vimage_def set_eq_iff
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    26
    by auto (metis rep_abs_rsp[OF assms] assms[simplified Quotient_def])+
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    27
qed
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    28
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    29
lemma empty_set_rsp[quot_respect]:
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    30
  "set_rel R {} {}"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    31
  unfolding set_rel_def by simp
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    32
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    33
lemma collect_rsp[quot_respect]:
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    34
  assumes "Quotient R Abs Rep"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    35
  shows "((R ===> op =) ===> set_rel R) Collect Collect"
44459
079ccfb074d9 Quotient Package: add mem_rsp, mem_prs, tune proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 44413
diff changeset
    36
  by (intro fun_relI) (simp add: fun_rel_def set_rel_def)
44413
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    37
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    38
lemma collect_prs[quot_preserve]:
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    39
  assumes "Quotient R Abs Rep"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    40
  shows "((Abs ---> id) ---> op -` Rep) Collect = Collect"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    41
  unfolding fun_eq_iff
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    42
  by (simp add: Quotient_abs_rep[OF assms])
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    43
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    44
lemma union_rsp[quot_respect]:
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    45
  assumes "Quotient R Abs Rep"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    46
  shows "(set_rel R ===> set_rel R ===> set_rel R) op \<union> op \<union>"
44459
079ccfb074d9 Quotient Package: add mem_rsp, mem_prs, tune proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 44413
diff changeset
    47
  by (intro fun_relI) (simp add: set_rel_def)
44413
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    48
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    49
lemma union_prs[quot_preserve]:
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    50
  assumes "Quotient R Abs Rep"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    51
  shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op \<union> = op \<union>"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    52
  unfolding fun_eq_iff
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    53
  by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]])
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    54
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    55
lemma diff_rsp[quot_respect]:
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    56
  assumes "Quotient R Abs Rep"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    57
  shows "(set_rel R ===> set_rel R ===> set_rel R) op - op -"
44459
079ccfb074d9 Quotient Package: add mem_rsp, mem_prs, tune proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 44413
diff changeset
    58
  by (intro fun_relI) (simp add: set_rel_def)
44413
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    59
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    60
lemma diff_prs[quot_preserve]:
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    61
  assumes "Quotient R Abs Rep"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    62
  shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op - = op -"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    63
  unfolding fun_eq_iff
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    64
  by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]] vimage_Diff)
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    65
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    66
lemma inter_rsp[quot_respect]:
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    67
  assumes "Quotient R Abs Rep"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    68
  shows "(set_rel R ===> set_rel R ===> set_rel R) op \<inter> op \<inter>"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    69
  by (intro fun_relI) (auto simp add: set_rel_def)
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    70
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    71
lemma inter_prs[quot_preserve]:
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    72
  assumes "Quotient R Abs Rep"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    73
  shows "(op -` Abs ---> op -` Abs ---> op -` Rep) op \<inter> = op \<inter>"
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    74
  unfolding fun_eq_iff
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    75
  by (simp add: Quotient_abs_rep[OF set_quotient[OF assms]])
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    76
44459
079ccfb074d9 Quotient Package: add mem_rsp, mem_prs, tune proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 44413
diff changeset
    77
lemma mem_prs[quot_preserve]:
079ccfb074d9 Quotient Package: add mem_rsp, mem_prs, tune proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 44413
diff changeset
    78
  assumes "Quotient R Abs Rep"
44873
045fedcfadf6 mem_prs and mem_rsp in accordance with sets-as-predicates representation (backported from AFP/Coinductive)
krauss
parents: 44459
diff changeset
    79
  shows "(Rep ---> (Abs ---> id) ---> id) (op \<in>) = op \<in>"
045fedcfadf6 mem_prs and mem_rsp in accordance with sets-as-predicates representation (backported from AFP/Coinductive)
krauss
parents: 44459
diff changeset
    80
using Quotient_abs_rep[OF assms]
045fedcfadf6 mem_prs and mem_rsp in accordance with sets-as-predicates representation (backported from AFP/Coinductive)
krauss
parents: 44459
diff changeset
    81
by(simp add: fun_eq_iff mem_def)
045fedcfadf6 mem_prs and mem_rsp in accordance with sets-as-predicates representation (backported from AFP/Coinductive)
krauss
parents: 44459
diff changeset
    82
045fedcfadf6 mem_prs and mem_rsp in accordance with sets-as-predicates representation (backported from AFP/Coinductive)
krauss
parents: 44459
diff changeset
    83
lemma mem_rsp[quot_respect]:
045fedcfadf6 mem_prs and mem_rsp in accordance with sets-as-predicates representation (backported from AFP/Coinductive)
krauss
parents: 44459
diff changeset
    84
  "(R ===> (R ===> op =) ===> op =) (op \<in>) (op \<in>)"
045fedcfadf6 mem_prs and mem_rsp in accordance with sets-as-predicates representation (backported from AFP/Coinductive)
krauss
parents: 44459
diff changeset
    85
  by (auto simp add: fun_eq_iff mem_def intro!: fun_relI elim: fun_relE)
045fedcfadf6 mem_prs and mem_rsp in accordance with sets-as-predicates representation (backported from AFP/Coinductive)
krauss
parents: 44459
diff changeset
    86
045fedcfadf6 mem_prs and mem_rsp in accordance with sets-as-predicates representation (backported from AFP/Coinductive)
krauss
parents: 44459
diff changeset
    87
lemma mem_prs2:
045fedcfadf6 mem_prs and mem_rsp in accordance with sets-as-predicates representation (backported from AFP/Coinductive)
krauss
parents: 44459
diff changeset
    88
  assumes "Quotient R Abs Rep"
44459
079ccfb074d9 Quotient Package: add mem_rsp, mem_prs, tune proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 44413
diff changeset
    89
  shows "(Rep ---> op -` Abs ---> id) op \<in> = op \<in>"
079ccfb074d9 Quotient Package: add mem_rsp, mem_prs, tune proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 44413
diff changeset
    90
  by (simp add: fun_eq_iff Quotient_abs_rep[OF assms])
079ccfb074d9 Quotient Package: add mem_rsp, mem_prs, tune proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 44413
diff changeset
    91
44873
045fedcfadf6 mem_prs and mem_rsp in accordance with sets-as-predicates representation (backported from AFP/Coinductive)
krauss
parents: 44459
diff changeset
    92
lemma mem_rsp2:
44459
079ccfb074d9 Quotient Package: add mem_rsp, mem_prs, tune proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 44413
diff changeset
    93
  shows "(R ===> set_rel R ===> op =) op \<in> op \<in>"
079ccfb074d9 Quotient Package: add mem_rsp, mem_prs, tune proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 44413
diff changeset
    94
  by (intro fun_relI) (simp add: set_rel_def)
079ccfb074d9 Quotient Package: add mem_rsp, mem_prs, tune proofs.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 44413
diff changeset
    95
44413
80d460bc6fa8 Quotient Package: some infrastructure for lifting inside sets
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    96
end