src/ZF/upair.thy
author wenzelm
Wed, 27 Mar 2013 16:38:25 +0100
changeset 51553 63327f679cff
parent 48891 c0eafbd55de3
child 58828 6d076fdd933d
permissions -rw-r--r--
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 124
diff changeset
     1
(*  Title:      ZF/upair.thy
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 124
diff changeset
     2
    Author:     Lawrence C Paulson and Martin D Coen, CU Computer Laboratory
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 124
diff changeset
     3
    Copyright   1993  University of Cambridge
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
     4
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
     5
Observe the order of dependence:
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
     6
    Upair is defined in terms of Replace
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
     7
    \<union> is defined in terms of Upair and \<Union>(similarly for Int)
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
     8
    cons is defined in terms of Upair and Un
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
     9
    Ordered pairs and descriptions are defined using cons ("set notation")
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 124
diff changeset
    10
*)
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 124
diff changeset
    11
13357
6f54e992777e Removal of mono.thy
paulson
parents: 13356
diff changeset
    12
header{*Unordered Pairs*}
6f54e992777e Removal of mono.thy
paulson
parents: 13356
diff changeset
    13
46950
d0181abdbdac declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents: 46821
diff changeset
    14
theory upair
d0181abdbdac declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents: 46821
diff changeset
    15
imports ZF
d0181abdbdac declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents: 46821
diff changeset
    16
keywords "print_tcset" :: diag
d0181abdbdac declare command keywords via theory header, including strict checking outside Pure;
wenzelm
parents: 46821
diff changeset
    17
begin
6153
bff90585cce5 new typechecking solver for the simplifier
paulson
parents: 3924
diff changeset
    18
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 46955
diff changeset
    19
ML_file "Tools/typechk.ML"
9907
473a6604da94 tuned ML code (the_context, bind_thms(s));
wenzelm
parents: 9570
diff changeset
    20
setup TypeCheck.setup
6153
bff90585cce5 new typechecking solver for the simplifier
paulson
parents: 3924
diff changeset
    21
13780
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
    22
lemma atomize_ball [symmetric, rulify]:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
    23
     "(!!x. x \<in> A ==> P(x)) == Trueprop (\<forall>x\<in>A. P(x))"
13780
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
    24
by (simp add: Ball_def atomize_all atomize_imp)
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    25
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    26
13357
6f54e992777e Removal of mono.thy
paulson
parents: 13356
diff changeset
    27
subsection{*Unordered Pairs: constant @{term Upair}*}
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    28
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
    29
lemma Upair_iff [simp]: "c \<in> Upair(a,b) \<longleftrightarrow> (c=a | c=b)"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    30
by (unfold Upair_def, blast)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    31
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
    32
lemma UpairI1: "a \<in> Upair(a,b)"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    33
by simp
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    34
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
    35
lemma UpairI2: "b \<in> Upair(a,b)"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    36
by simp
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    37
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
    38
lemma UpairE: "[| a \<in> Upair(b,c);  a=b ==> P;  a=c ==> P |] ==> P"
13780
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
    39
by (simp, blast)
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    40
13357
6f54e992777e Removal of mono.thy
paulson
parents: 13356
diff changeset
    41
subsection{*Rules for Binary Union, Defined via @{term Upair}*}
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    42
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
    43
lemma Un_iff [simp]: "c \<in> A \<union> B \<longleftrightarrow> (c \<in> A | c \<in> B)"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    44
apply (simp add: Un_def)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    45
apply (blast intro: UpairI1 UpairI2 elim: UpairE)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    46
done
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    47
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
    48
lemma UnI1: "c \<in> A ==> c \<in> A \<union> B"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    49
by simp
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    50
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
    51
lemma UnI2: "c \<in> B ==> c \<in> A \<union> B"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    52
by simp
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    53
13356
c9cfe1638bf2 improved presentation markup
paulson
parents: 13259
diff changeset
    54
declare UnI1 [elim?]  UnI2 [elim?]
c9cfe1638bf2 improved presentation markup
paulson
parents: 13259
diff changeset
    55
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
    56
lemma UnE [elim!]: "[| c \<in> A \<union> B;  c \<in> A ==> P;  c \<in> B ==> P |] ==> P"
13780
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
    57
by (simp, blast)
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    58
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    59
(*Stronger version of the rule above*)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
    60
lemma UnE': "[| c \<in> A \<union> B;  c \<in> A ==> P;  [| c \<in> B;  c\<notin>A |] ==> P |] ==> P"
13780
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
    61
by (simp, blast)
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    62
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    63
(*Classical introduction rule: no commitment to A vs B*)
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
    64
lemma UnCI [intro!]: "(c \<notin> B ==> c \<in> A) ==> c \<in> A \<union> B"
13780
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
    65
by (simp, blast)
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    66
13357
6f54e992777e Removal of mono.thy
paulson
parents: 13356
diff changeset
    67
subsection{*Rules for Binary Intersection, Defined via @{term Upair}*}
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    68
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
    69
lemma Int_iff [simp]: "c \<in> A \<inter> B \<longleftrightarrow> (c \<in> A & c \<in> B)"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    70
apply (unfold Int_def)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    71
apply (blast intro: UpairI1 UpairI2 elim: UpairE)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    72
done
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    73
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
    74
lemma IntI [intro!]: "[| c \<in> A;  c \<in> B |] ==> c \<in> A \<inter> B"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    75
by simp
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    76
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
    77
lemma IntD1: "c \<in> A \<inter> B ==> c \<in> A"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    78
by simp
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    79
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
    80
lemma IntD2: "c \<in> A \<inter> B ==> c \<in> B"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    81
by simp
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    82
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
    83
lemma IntE [elim!]: "[| c \<in> A \<inter> B;  [| c \<in> A; c \<in> B |] ==> P |] ==> P"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    84
by simp
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    85
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    86
13357
6f54e992777e Removal of mono.thy
paulson
parents: 13356
diff changeset
    87
subsection{*Rules for Set Difference, Defined via @{term Upair}*}
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    88
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
    89
lemma Diff_iff [simp]: "c \<in> A-B \<longleftrightarrow> (c \<in> A & c\<notin>B)"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    90
by (unfold Diff_def, blast)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    91
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
    92
lemma DiffI [intro!]: "[| c \<in> A;  c \<notin> B |] ==> c \<in> A - B"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    93
by simp
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    94
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
    95
lemma DiffD1: "c \<in> A - B ==> c \<in> A"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    96
by simp
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    97
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
    98
lemma DiffD2: "c \<in> A - B ==> c \<notin> B"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
    99
by simp
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   100
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   101
lemma DiffE [elim!]: "[| c \<in> A - B;  [| c \<in> A; c\<notin>B |] ==> P |] ==> P"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   102
by simp
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   103
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   104
13357
6f54e992777e Removal of mono.thy
paulson
parents: 13356
diff changeset
   105
subsection{*Rules for @{term cons}*}
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   106
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   107
lemma cons_iff [simp]: "a \<in> cons(b,A) \<longleftrightarrow> (a=b | a \<in> A)"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   108
apply (unfold cons_def)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   109
apply (blast intro: UpairI1 UpairI2 elim: UpairE)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   110
done
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   111
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   112
(*risky as a typechecking rule, but solves otherwise unconstrained goals of
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   113
the form x \<in> ?A*)
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   114
lemma consI1 [simp,TC]: "a \<in> cons(a,B)"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   115
by simp
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   116
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   117
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   118
lemma consI2: "a \<in> B ==> a \<in> cons(b,B)"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   119
by simp
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   120
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   121
lemma consE [elim!]: "[| a \<in> cons(b,A);  a=b ==> P;  a \<in> A ==> P |] ==> P"
13780
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   122
by (simp, blast)
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   123
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   124
(*Stronger version of the rule above*)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   125
lemma consE':
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   126
    "[| a \<in> cons(b,A);  a=b ==> P;  [| a \<in> A;  a\<noteq>b |] ==> P |] ==> P"
13780
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   127
by (simp, blast)
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   128
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   129
(*Classical introduction rule*)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   130
lemma consCI [intro!]: "(a\<notin>B ==> a=b) ==> a \<in> cons(b,B)"
13780
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   131
by (simp, blast)
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   132
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   133
lemma cons_not_0 [simp]: "cons(a,B) \<noteq> 0"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   134
by (blast elim: equalityE)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   135
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 32960
diff changeset
   136
lemmas cons_neq_0 = cons_not_0 [THEN notE]
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   137
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   138
declare cons_not_0 [THEN not_sym, simp]
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   139
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   140
13357
6f54e992777e Removal of mono.thy
paulson
parents: 13356
diff changeset
   141
subsection{*Singletons*}
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   142
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   143
lemma singleton_iff: "a \<in> {b} \<longleftrightarrow> a=b"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   144
by simp
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   145
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   146
lemma singletonI [intro!]: "a \<in> {a}"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   147
by (rule consI1)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   148
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 32960
diff changeset
   149
lemmas singletonE = singleton_iff [THEN iffD1, elim_format, elim!]
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   150
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   151
14883
ca000a495448 Groups, Rings and supporting lemmas
paulson
parents: 14153
diff changeset
   152
subsection{*Descriptions*}
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   153
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   154
lemma the_equality [intro]:
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   155
    "[| P(a);  !!x. P(x) ==> x=a |] ==> (THE x. P(x)) = a"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   156
apply (unfold the_def)
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   157
apply (fast dest: subst)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   158
done
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   159
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   160
(* Only use this if you already know EX!x. P(x) *)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   161
lemma the_equality2: "[| EX! x. P(x);  P(a) |] ==> (THE x. P(x)) = a"
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   162
by blast
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   163
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   164
lemma theI: "EX! x. P(x) ==> P(THE x. P(x))"
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   165
apply (erule ex1E)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   166
apply (subst the_equality)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   167
apply (blast+)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   168
done
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   169
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   170
(*No congruence rule is necessary: if @{term"\<forall>y.P(y)\<longleftrightarrow>Q(y)"} then
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   171
  @{term "THE x.P(x)"}  rewrites to @{term "THE x.Q(x)"} *)
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   172
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   173
(*If it's "undefined", it's zero!*)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   174
lemma the_0: "~ (EX! x. P(x)) ==> (THE x. P(x))=0"
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   175
apply (unfold the_def)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   176
apply (blast elim!: ReplaceE)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   177
done
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   178
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   179
(*Easier to apply than theI: conclusion has only one occurrence of P*)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   180
lemma theI2:
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   181
    assumes p1: "~ Q(0) ==> EX! x. P(x)"
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   182
        and p2: "!!x. P(x) ==> Q(x)"
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   183
    shows "Q(THE x. P(x))"
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   184
apply (rule classical)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   185
apply (rule p2)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   186
apply (rule theI)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   187
apply (rule classical)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   188
apply (rule p1)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   189
apply (erule the_0 [THEN subst], assumption)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   190
done
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   191
13357
6f54e992777e Removal of mono.thy
paulson
parents: 13356
diff changeset
   192
lemma the_eq_trivial [simp]: "(THE x. x = a) = a"
6f54e992777e Removal of mono.thy
paulson
parents: 13356
diff changeset
   193
by blast
6f54e992777e Removal of mono.thy
paulson
parents: 13356
diff changeset
   194
13544
895994073bdf various new lemmas for Constructible
paulson
parents: 13357
diff changeset
   195
lemma the_eq_trivial2 [simp]: "(THE x. a = x) = a"
895994073bdf various new lemmas for Constructible
paulson
parents: 13357
diff changeset
   196
by blast
895994073bdf various new lemmas for Constructible
paulson
parents: 13357
diff changeset
   197
13780
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   198
13357
6f54e992777e Removal of mono.thy
paulson
parents: 13356
diff changeset
   199
subsection{*Conditional Terms: @{text "if-then-else"}*}
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   200
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   201
lemma if_true [simp]: "(if True then a else b) = a"
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   202
by (unfold if_def, blast)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   203
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   204
lemma if_false [simp]: "(if False then a else b) = b"
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   205
by (unfold if_def, blast)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   206
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   207
(*Never use with case splitting, or if P is known to be true or false*)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   208
lemma if_cong:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   209
    "[| P\<longleftrightarrow>Q;  Q ==> a=c;  ~Q ==> b=d |]
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   210
     ==> (if P then a else b) = (if Q then c else d)"
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   211
by (simp add: if_def cong add: conj_cong)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   212
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   213
(*Prevents simplification of x and y \<in> faster and allows the execution
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   214
  of functional programs. NOW THE DEFAULT.*)
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   215
lemma if_weak_cong: "P\<longleftrightarrow>Q ==> (if P then x else y) = (if Q then x else y)"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   216
by simp
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   217
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   218
(*Not needed for rewriting, since P would rewrite to True anyway*)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   219
lemma if_P: "P ==> (if P then a else b) = a"
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   220
by (unfold if_def, blast)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   221
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   222
(*Not needed for rewriting, since P would rewrite to False anyway*)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   223
lemma if_not_P: "~P ==> (if P then a else b) = b"
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   224
by (unfold if_def, blast)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   225
13780
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   226
lemma split_if [split]:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   227
     "P(if Q then x else y) \<longleftrightarrow> ((Q \<longrightarrow> P(x)) & (~Q \<longrightarrow> P(y)))"
14153
76a6ba67bd15 new case_tac
paulson
parents: 13780
diff changeset
   228
by (case_tac Q, simp_all)
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   229
45620
f2a587696afb modernized some old-style infix operations, which were left over from the time of ML proof scripts;
wenzelm
parents: 45602
diff changeset
   230
(** Rewrite rules for boolean case-splitting: faster than split_if [split]
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   231
**)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   232
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 32960
diff changeset
   233
lemmas split_if_eq1 = split_if [of "%x. x = b"] for b
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 32960
diff changeset
   234
lemmas split_if_eq2 = split_if [of "%x. a = x"] for x
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   235
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   236
lemmas split_if_mem1 = split_if [of "%x. x \<in> b"] for b
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   237
lemmas split_if_mem2 = split_if [of "%x. a \<in> x"] for x
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   238
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   239
lemmas split_ifs = split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   240
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   241
(*Logically equivalent to split_if_mem2*)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   242
lemma if_iff: "a: (if P then x else y) \<longleftrightarrow> P & a \<in> x | ~P & a \<in> y"
13780
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   243
by simp
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   244
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   245
lemma if_type [TC]:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   246
    "[| P ==> a \<in> A;  ~P ==> b \<in> A |] ==> (if P then a else b): A"
13780
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   247
by simp
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   248
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   249
(** Splitting IFs in the assumptions **)
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   250
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   251
lemma split_if_asm: "P(if Q then x else y) \<longleftrightarrow> (~((Q & ~P(x)) | (~Q & ~P(y))))"
13780
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   252
by simp
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   253
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   254
lemmas if_splits = split_if split_if_asm
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   255
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   256
13357
6f54e992777e Removal of mono.thy
paulson
parents: 13356
diff changeset
   257
subsection{*Consequences of Foundation*}
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   258
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   259
(*was called mem_anti_sym*)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   260
lemma mem_asym: "[| a \<in> b;  ~P ==> b \<in> a |] ==> P"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   261
apply (rule classical)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   262
apply (rule_tac A1 = "{a,b}" in foundation [THEN disjE])
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   263
apply (blast elim!: equalityE)+
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   264
done
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   265
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   266
(*was called mem_anti_refl*)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   267
lemma mem_irrefl: "a \<in> a ==> P"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   268
by (blast intro: mem_asym)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   269
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   270
(*mem_irrefl should NOT be added to default databases:
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   271
      it would be tried on most goals, making proofs slower!*)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   272
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   273
lemma mem_not_refl: "a \<notin> a"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   274
apply (rule notI)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   275
apply (erule mem_irrefl)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   276
done
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   277
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   278
(*Good for proving inequalities by rewriting*)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   279
lemma mem_imp_not_eq: "a \<in> A ==> a \<noteq> A"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   280
by (blast elim!: mem_irrefl)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   281
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   282
lemma eq_imp_not_mem: "a=A ==> a \<notin> A"
13357
6f54e992777e Removal of mono.thy
paulson
parents: 13356
diff changeset
   283
by (blast intro: elim: mem_irrefl)
6f54e992777e Removal of mono.thy
paulson
parents: 13356
diff changeset
   284
6f54e992777e Removal of mono.thy
paulson
parents: 13356
diff changeset
   285
subsection{*Rules for Successor*}
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   286
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   287
lemma succ_iff: "i \<in> succ(j) \<longleftrightarrow> i=j | i \<in> j"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   288
by (unfold succ_def, blast)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   289
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   290
lemma succI1 [simp]: "i \<in> succ(i)"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   291
by (simp add: succ_iff)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   292
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   293
lemma succI2: "i \<in> j ==> i \<in> succ(j)"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   294
by (simp add: succ_iff)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   295
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   296
lemma succE [elim!]:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   297
    "[| i \<in> succ(j);  i=j ==> P;  i \<in> j ==> P |] ==> P"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   298
apply (simp add: succ_iff, blast)
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   299
done
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   300
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   301
(*Classical introduction rule*)
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   302
lemma succCI [intro!]: "(i\<notin>j ==> i=j) ==> i \<in> succ(j)"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   303
by (simp add: succ_iff, blast)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   304
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   305
lemma succ_not_0 [simp]: "succ(n) \<noteq> 0"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   306
by (blast elim!: equalityE)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   307
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 32960
diff changeset
   308
lemmas succ_neq_0 = succ_not_0 [THEN notE, elim!]
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   309
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   310
declare succ_not_0 [THEN not_sym, simp]
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   311
declare sym [THEN succ_neq_0, elim!]
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   312
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   313
(* @{term"succ(c) \<subseteq> B ==> c \<in> B"} *)
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   314
lemmas succ_subsetD = succI1 [THEN [2] subsetD]
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   315
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   316
(* @{term"succ(b) \<noteq> b"} *)
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 32960
diff changeset
   317
lemmas succ_neq_self = succI1 [THEN mem_imp_not_eq, THEN not_sym]
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   318
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   319
lemma succ_inject_iff [simp]: "succ(m) = succ(n) \<longleftrightarrow> m=n"
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   320
by (blast elim: mem_asym elim!: equalityE)
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   321
45602
2a858377c3d2 eliminated obsolete "standard";
wenzelm
parents: 32960
diff changeset
   322
lemmas succ_inject = succ_inject_iff [THEN iffD1, dest!]
13259
01fa0c8dbc92 conversion of many files to Isar format
paulson
parents: 11770
diff changeset
   323
13780
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   324
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   325
subsection{*Miniscoping of the Bounded Universal Quantifier*}
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   326
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   327
lemma ball_simps1:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   328
     "(\<forall>x\<in>A. P(x) & Q)   \<longleftrightarrow> (\<forall>x\<in>A. P(x)) & (A=0 | Q)"
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   329
     "(\<forall>x\<in>A. P(x) | Q)   \<longleftrightarrow> ((\<forall>x\<in>A. P(x)) | Q)"
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   330
     "(\<forall>x\<in>A. P(x) \<longrightarrow> Q) \<longleftrightarrow> ((\<exists>x\<in>A. P(x)) \<longrightarrow> Q)"
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   331
     "(~(\<forall>x\<in>A. P(x))) \<longleftrightarrow> (\<exists>x\<in>A. ~P(x))"
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   332
     "(\<forall>x\<in>0.P(x)) \<longleftrightarrow> True"
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   333
     "(\<forall>x\<in>succ(i).P(x)) \<longleftrightarrow> P(i) & (\<forall>x\<in>i. P(x))"
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   334
     "(\<forall>x\<in>cons(a,B).P(x)) \<longleftrightarrow> P(a) & (\<forall>x\<in>B. P(x))"
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   335
     "(\<forall>x\<in>RepFun(A,f). P(x)) \<longleftrightarrow> (\<forall>y\<in>A. P(f(y)))"
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   336
     "(\<forall>x\<in>\<Union>(A).P(x)) \<longleftrightarrow> (\<forall>y\<in>A. \<forall>x\<in>y. P(x))"
13780
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   337
by blast+
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   338
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   339
lemma ball_simps2:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   340
     "(\<forall>x\<in>A. P & Q(x))   \<longleftrightarrow> (A=0 | P) & (\<forall>x\<in>A. Q(x))"
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   341
     "(\<forall>x\<in>A. P | Q(x))   \<longleftrightarrow> (P | (\<forall>x\<in>A. Q(x)))"
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   342
     "(\<forall>x\<in>A. P \<longrightarrow> Q(x)) \<longleftrightarrow> (P \<longrightarrow> (\<forall>x\<in>A. Q(x)))"
13780
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   343
by blast+
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   344
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   345
lemma ball_simps3:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   346
     "(\<forall>x\<in>Collect(A,Q).P(x)) \<longleftrightarrow> (\<forall>x\<in>A. Q(x) \<longrightarrow> P(x))"
13780
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   347
by blast+
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   348
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   349
lemmas ball_simps [simp] = ball_simps1 ball_simps2 ball_simps3
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   350
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   351
lemma ball_conj_distrib:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   352
    "(\<forall>x\<in>A. P(x) & Q(x)) \<longleftrightarrow> ((\<forall>x\<in>A. P(x)) & (\<forall>x\<in>A. Q(x)))"
13780
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   353
by blast
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   354
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   355
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   356
subsection{*Miniscoping of the Bounded Existential Quantifier*}
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   357
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   358
lemma bex_simps1:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   359
     "(\<exists>x\<in>A. P(x) & Q) \<longleftrightarrow> ((\<exists>x\<in>A. P(x)) & Q)"
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   360
     "(\<exists>x\<in>A. P(x) | Q) \<longleftrightarrow> (\<exists>x\<in>A. P(x)) | (A\<noteq>0 & Q)"
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   361
     "(\<exists>x\<in>A. P(x) \<longrightarrow> Q) \<longleftrightarrow> ((\<forall>x\<in>A. P(x)) \<longrightarrow> (A\<noteq>0 & Q))"
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   362
     "(\<exists>x\<in>0.P(x)) \<longleftrightarrow> False"
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   363
     "(\<exists>x\<in>succ(i).P(x)) \<longleftrightarrow> P(i) | (\<exists>x\<in>i. P(x))"
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   364
     "(\<exists>x\<in>cons(a,B).P(x)) \<longleftrightarrow> P(a) | (\<exists>x\<in>B. P(x))"
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   365
     "(\<exists>x\<in>RepFun(A,f). P(x)) \<longleftrightarrow> (\<exists>y\<in>A. P(f(y)))"
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   366
     "(\<exists>x\<in>\<Union>(A).P(x)) \<longleftrightarrow> (\<exists>y\<in>A. \<exists>x\<in>y.  P(x))"
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   367
     "(~(\<exists>x\<in>A. P(x))) \<longleftrightarrow> (\<forall>x\<in>A. ~P(x))"
13780
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   368
by blast+
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   369
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   370
lemma bex_simps2:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   371
     "(\<exists>x\<in>A. P & Q(x)) \<longleftrightarrow> (P & (\<exists>x\<in>A. Q(x)))"
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   372
     "(\<exists>x\<in>A. P | Q(x)) \<longleftrightarrow> (A\<noteq>0 & P) | (\<exists>x\<in>A. Q(x))"
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   373
     "(\<exists>x\<in>A. P \<longrightarrow> Q(x)) \<longleftrightarrow> ((A=0 | P) \<longrightarrow> (\<exists>x\<in>A. Q(x)))"
13780
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   374
by blast+
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   375
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   376
lemma bex_simps3:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   377
     "(\<exists>x\<in>Collect(A,Q).P(x)) \<longleftrightarrow> (\<exists>x\<in>A. Q(x) & P(x))"
13780
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   378
by blast
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   379
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   380
lemmas bex_simps [simp] = bex_simps1 bex_simps2 bex_simps3
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   381
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   382
lemma bex_disj_distrib:
46821
ff6b0c1087f2 Using mathematical notation for <-> and cardinal arithmetic
paulson
parents: 46820
diff changeset
   383
    "(\<exists>x\<in>A. P(x) | Q(x)) \<longleftrightarrow> ((\<exists>x\<in>A. P(x)) | (\<exists>x\<in>A. Q(x)))"
13780
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   384
by blast
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   385
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   386
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   387
(** One-point rule for bounded quantifiers: see HOL/Set.ML **)
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   388
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   389
lemma bex_triv_one_point1 [simp]: "(\<exists>x\<in>A. x=a) \<longleftrightarrow> (a \<in> A)"
13780
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   390
by blast
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   391
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   392
lemma bex_triv_one_point2 [simp]: "(\<exists>x\<in>A. a=x) \<longleftrightarrow> (a \<in> A)"
13780
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   393
by blast
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   394
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   395
lemma bex_one_point1 [simp]: "(\<exists>x\<in>A. x=a & P(x)) \<longleftrightarrow> (a \<in> A & P(a))"
13780
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   396
by blast
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   397
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   398
lemma bex_one_point2 [simp]: "(\<exists>x\<in>A. a=x & P(x)) \<longleftrightarrow> (a \<in> A & P(a))"
13780
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   399
by blast
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   400
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   401
lemma ball_one_point1 [simp]: "(\<forall>x\<in>A. x=a \<longrightarrow> P(x)) \<longleftrightarrow> (a \<in> A \<longrightarrow> P(a))"
13780
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   402
by blast
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   403
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   404
lemma ball_one_point2 [simp]: "(\<forall>x\<in>A. a=x \<longrightarrow> P(x)) \<longleftrightarrow> (a \<in> A \<longrightarrow> P(a))"
13780
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   405
by blast
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   406
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   407
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   408
subsection{*Miniscoping of the Replacement Operator*}
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   409
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   410
text{*These cover both @{term Replace} and @{term Collect}*}
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   411
lemma Rep_simps [simp]:
46953
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   412
     "{x. y \<in> 0, R(x,y)} = 0"
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   413
     "{x \<in> 0. P(x)} = 0"
2b6e55924af3 replacing ":" by "\<in>"
paulson
parents: 46821
diff changeset
   414
     "{x \<in> A. Q} = (if Q then A else 0)"
13780
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   415
     "RepFun(0,f) = 0"
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   416
     "RepFun(succ(i),f) = cons(f(i), RepFun(i,f))"
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   417
     "RepFun(cons(a,B),f) = cons(f(a), RepFun(B,f))"
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   418
by (simp_all, blast+)
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   419
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   420
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   421
subsection{*Miniscoping of Unions*}
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   422
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   423
lemma UN_simps1:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   424
     "(\<Union>x\<in>C. cons(a, B(x))) = (if C=0 then 0 else cons(a, \<Union>x\<in>C. B(x)))"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   425
     "(\<Union>x\<in>C. A(x) \<union> B')   = (if C=0 then 0 else (\<Union>x\<in>C. A(x)) \<union> B')"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   426
     "(\<Union>x\<in>C. A' \<union> B(x))   = (if C=0 then 0 else A' \<union> (\<Union>x\<in>C. B(x)))"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   427
     "(\<Union>x\<in>C. A(x) \<inter> B')  = ((\<Union>x\<in>C. A(x)) \<inter> B')"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   428
     "(\<Union>x\<in>C. A' \<inter> B(x))  = (A' \<inter> (\<Union>x\<in>C. B(x)))"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   429
     "(\<Union>x\<in>C. A(x) - B')    = ((\<Union>x\<in>C. A(x)) - B')"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   430
     "(\<Union>x\<in>C. A' - B(x))    = (if C=0 then 0 else A' - (\<Inter>x\<in>C. B(x)))"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   431
apply (simp_all add: Inter_def)
13780
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   432
apply (blast intro!: equalityI )+
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   433
done
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   434
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   435
lemma UN_simps2:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   436
      "(\<Union>x\<in>\<Union>(A). B(x)) = (\<Union>y\<in>A. \<Union>x\<in>y. B(x))"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   437
      "(\<Union>z\<in>(\<Union>x\<in>A. B(x)). C(z)) = (\<Union>x\<in>A. \<Union>z\<in>B(x). C(z))"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   438
      "(\<Union>x\<in>RepFun(A,f). B(x))     = (\<Union>a\<in>A. B(f(a)))"
13780
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   439
by blast+
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   440
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   441
lemmas UN_simps [simp] = UN_simps1 UN_simps2
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   442
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   443
text{*Opposite of miniscoping: pull the operator out*}
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   444
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   445
lemma UN_extend_simps1:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   446
     "(\<Union>x\<in>C. A(x)) \<union> B   = (if C=0 then B else (\<Union>x\<in>C. A(x) \<union> B))"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   447
     "((\<Union>x\<in>C. A(x)) \<inter> B) = (\<Union>x\<in>C. A(x) \<inter> B)"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   448
     "((\<Union>x\<in>C. A(x)) - B) = (\<Union>x\<in>C. A(x) - B)"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   449
apply simp_all
13780
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   450
apply blast+
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   451
done
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   452
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   453
lemma UN_extend_simps2:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   454
     "cons(a, \<Union>x\<in>C. B(x)) = (if C=0 then {a} else (\<Union>x\<in>C. cons(a, B(x))))"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   455
     "A \<union> (\<Union>x\<in>C. B(x))   = (if C=0 then A else (\<Union>x\<in>C. A \<union> B(x)))"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   456
     "(A \<inter> (\<Union>x\<in>C. B(x))) = (\<Union>x\<in>C. A \<inter> B(x))"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   457
     "A - (\<Inter>x\<in>C. B(x))    = (if C=0 then A else (\<Union>x\<in>C. A - B(x)))"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   458
     "(\<Union>y\<in>A. \<Union>x\<in>y. B(x)) = (\<Union>x\<in>\<Union>(A). B(x))"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   459
     "(\<Union>a\<in>A. B(f(a))) = (\<Union>x\<in>RepFun(A,f). B(x))"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   460
apply (simp_all add: Inter_def)
13780
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   461
apply (blast intro!: equalityI)+
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   462
done
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   463
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   464
lemma UN_UN_extend:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   465
     "(\<Union>x\<in>A. \<Union>z\<in>B(x). C(z)) = (\<Union>z\<in>(\<Union>x\<in>A. B(x)). C(z))"
13780
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   466
by blast
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   467
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   468
lemmas UN_extend_simps = UN_extend_simps1 UN_extend_simps2 UN_UN_extend
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   469
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   470
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   471
subsection{*Miniscoping of Intersections*}
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   472
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   473
lemma INT_simps1:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   474
     "(\<Inter>x\<in>C. A(x) \<inter> B) = (\<Inter>x\<in>C. A(x)) \<inter> B"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   475
     "(\<Inter>x\<in>C. A(x) - B)   = (\<Inter>x\<in>C. A(x)) - B"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   476
     "(\<Inter>x\<in>C. A(x) \<union> B)  = (if C=0 then 0 else (\<Inter>x\<in>C. A(x)) \<union> B)"
13780
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   477
by (simp_all add: Inter_def, blast+)
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   478
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   479
lemma INT_simps2:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   480
     "(\<Inter>x\<in>C. A \<inter> B(x)) = A \<inter> (\<Inter>x\<in>C. B(x))"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   481
     "(\<Inter>x\<in>C. A - B(x))   = (if C=0 then 0 else A - (\<Union>x\<in>C. B(x)))"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   482
     "(\<Inter>x\<in>C. cons(a, B(x))) = (if C=0 then 0 else cons(a, \<Inter>x\<in>C. B(x)))"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   483
     "(\<Inter>x\<in>C. A \<union> B(x))  = (if C=0 then 0 else A \<union> (\<Inter>x\<in>C. B(x)))"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   484
apply (simp_all add: Inter_def)
13780
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   485
apply (blast intro!: equalityI)+
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   486
done
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   487
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   488
lemmas INT_simps [simp] = INT_simps1 INT_simps2
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   489
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   490
text{*Opposite of miniscoping: pull the operator out*}
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   491
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   492
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   493
lemma INT_extend_simps1:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   494
     "(\<Inter>x\<in>C. A(x)) \<inter> B = (\<Inter>x\<in>C. A(x) \<inter> B)"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   495
     "(\<Inter>x\<in>C. A(x)) - B = (\<Inter>x\<in>C. A(x) - B)"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   496
     "(\<Inter>x\<in>C. A(x)) \<union> B  = (if C=0 then B else (\<Inter>x\<in>C. A(x) \<union> B))"
13780
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   497
apply (simp_all add: Inter_def, blast+)
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   498
done
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   499
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   500
lemma INT_extend_simps2:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   501
     "A \<inter> (\<Inter>x\<in>C. B(x)) = (\<Inter>x\<in>C. A \<inter> B(x))"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   502
     "A - (\<Union>x\<in>C. B(x))   = (if C=0 then A else (\<Inter>x\<in>C. A - B(x)))"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   503
     "cons(a, \<Inter>x\<in>C. B(x)) = (if C=0 then {a} else (\<Inter>x\<in>C. cons(a, B(x))))"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   504
     "A \<union> (\<Inter>x\<in>C. B(x))  = (if C=0 then A else (\<Inter>x\<in>C. A \<union> B(x)))"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   505
apply (simp_all add: Inter_def)
13780
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   506
apply (blast intro!: equalityI)+
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   507
done
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   508
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   509
lemmas INT_extend_simps = INT_extend_simps1 INT_extend_simps2
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   510
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   511
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   512
subsection{*Other simprules*}
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   513
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   514
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   515
(*** Miniscoping: pushing in big Unions, Intersections, quantifiers, etc. ***)
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   516
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   517
lemma misc_simps [simp]:
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   518
     "0 \<union> A = A"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   519
     "A \<union> 0 = A"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   520
     "0 \<inter> A = 0"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   521
     "A \<inter> 0 = 0"
13780
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   522
     "0 - A = 0"
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   523
     "A - 0 = A"
46820
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   524
     "\<Union>(0) = 0"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   525
     "\<Union>(cons(b,A)) = b \<union> \<Union>(A)"
c656222c4dc1 mathematical symbols instead of ASCII
paulson
parents: 45620
diff changeset
   526
     "\<Inter>({b}) = b"
13780
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   527
by blast+
af7b79271364 more new-style theories
paulson
parents: 13544
diff changeset
   528
6153
bff90585cce5 new typechecking solver for the simplifier
paulson
parents: 3924
diff changeset
   529
end