src/HOL/Predicate.thy
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 26797 a6cb51c314f2
child 30328 ab47f43f7581
permissions -rw-r--r--
added lemmas
berghofe@22259
     1
(*  Title:      HOL/Predicate.thy
berghofe@22259
     2
    ID:         $Id$
berghofe@22259
     3
    Author:     Stefan Berghofer, TU Muenchen
berghofe@22259
     4
*)
berghofe@22259
     5
berghofe@22259
     6
header {* Predicates *}
berghofe@22259
     7
berghofe@22259
     8
theory Predicate
haftmann@23708
     9
imports Inductive Relation
berghofe@22259
    10
begin
berghofe@22259
    11
berghofe@23741
    12
subsection {* Equality and Subsets *}
berghofe@22259
    13
berghofe@26797
    14
lemma pred_equals_eq: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) = (R = S)"
berghofe@26797
    15
  by (simp add: mem_def)
berghofe@22259
    16
berghofe@23741
    17
lemma pred_equals_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) = (\<lambda>x y. (x, y) \<in> S)) = (R = S)"
berghofe@26797
    18
  by (simp add: expand_fun_eq mem_def)
berghofe@22259
    19
berghofe@26797
    20
lemma pred_subset_eq: "((\<lambda>x. x \<in> R) <= (\<lambda>x. x \<in> S)) = (R <= S)"
berghofe@26797
    21
  by (simp add: mem_def)
berghofe@22259
    22
berghofe@23741
    23
lemma pred_subset_eq2 [pred_set_conv]: "((\<lambda>x y. (x, y) \<in> R) <= (\<lambda>x y. (x, y) \<in> S)) = (R <= S)"
berghofe@22259
    24
  by fast
berghofe@22259
    25
berghofe@23741
    26
berghofe@23741
    27
subsection {* Top and bottom elements *}
berghofe@23741
    28
berghofe@23741
    29
lemma top1I [intro!]: "top x"
berghofe@23741
    30
  by (simp add: top_fun_eq top_bool_eq)
berghofe@22259
    31
berghofe@23741
    32
lemma top2I [intro!]: "top x y"
berghofe@23741
    33
  by (simp add: top_fun_eq top_bool_eq)
berghofe@23741
    34
berghofe@23741
    35
lemma bot1E [elim!]: "bot x \<Longrightarrow> P"
berghofe@23741
    36
  by (simp add: bot_fun_eq bot_bool_eq)
berghofe@23741
    37
berghofe@23741
    38
lemma bot2E [elim!]: "bot x y \<Longrightarrow> P"
berghofe@23741
    39
  by (simp add: bot_fun_eq bot_bool_eq)
berghofe@22259
    40
berghofe@22259
    41
berghofe@23741
    42
subsection {* The empty set *}
berghofe@23741
    43
berghofe@23741
    44
lemma bot_empty_eq: "bot = (\<lambda>x. x \<in> {})"
berghofe@23741
    45
  by (auto simp add: expand_fun_eq)
berghofe@22259
    46
berghofe@23741
    47
lemma bot_empty_eq2: "bot = (\<lambda>x y. (x, y) \<in> {})"
berghofe@23741
    48
  by (auto simp add: expand_fun_eq)
berghofe@22259
    49
berghofe@23741
    50
berghofe@23741
    51
subsection {* Binary union *}
berghofe@22259
    52
haftmann@22422
    53
lemma sup1_iff [simp]: "sup A B x \<longleftrightarrow> A x | B x"
haftmann@22422
    54
  by (simp add: sup_fun_eq sup_bool_eq)
berghofe@22259
    55
haftmann@22422
    56
lemma sup2_iff [simp]: "sup A B x y \<longleftrightarrow> A x y | B x y"
haftmann@22422
    57
  by (simp add: sup_fun_eq sup_bool_eq)
berghofe@22259
    58
berghofe@23741
    59
lemma sup_Un_eq [pred_set_conv]: "sup (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)"
berghofe@23741
    60
  by (simp add: expand_fun_eq)
berghofe@23741
    61
berghofe@23741
    62
lemma sup_Un_eq2 [pred_set_conv]: "sup (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<union> S)"
berghofe@23741
    63
  by (simp add: expand_fun_eq)
berghofe@23741
    64
haftmann@22422
    65
lemma sup1I1 [elim?]: "A x \<Longrightarrow> sup A B x"
berghofe@22259
    66
  by simp
berghofe@22259
    67
haftmann@22422
    68
lemma sup2I1 [elim?]: "A x y \<Longrightarrow> sup A B x y"
berghofe@22259
    69
  by simp
berghofe@22259
    70
berghofe@23741
    71
lemma sup1I2 [elim?]: "B x \<Longrightarrow> sup A B x"
berghofe@22259
    72
  by simp
berghofe@22259
    73
berghofe@23741
    74
lemma sup2I2 [elim?]: "B x y \<Longrightarrow> sup A B x y"
berghofe@22259
    75
  by simp
berghofe@22259
    76
berghofe@22259
    77
text {*
berghofe@22259
    78
  \medskip Classical introduction rule: no commitment to @{text A} vs
berghofe@22259
    79
  @{text B}.
berghofe@22259
    80
*}
berghofe@22259
    81
haftmann@22422
    82
lemma sup1CI [intro!]: "(~ B x ==> A x) ==> sup A B x"
berghofe@22259
    83
  by auto
berghofe@22259
    84
haftmann@22422
    85
lemma sup2CI [intro!]: "(~ B x y ==> A x y) ==> sup A B x y"
berghofe@22259
    86
  by auto
berghofe@22259
    87
haftmann@22422
    88
lemma sup1E [elim!]: "sup A B x ==> (A x ==> P) ==> (B x ==> P) ==> P"
berghofe@22259
    89
  by simp iprover
berghofe@22259
    90
haftmann@22422
    91
lemma sup2E [elim!]: "sup A B x y ==> (A x y ==> P) ==> (B x y ==> P) ==> P"
berghofe@22259
    92
  by simp iprover
berghofe@22259
    93
berghofe@22259
    94
berghofe@23741
    95
subsection {* Binary intersection *}
berghofe@22259
    96
haftmann@22422
    97
lemma inf1_iff [simp]: "inf A B x \<longleftrightarrow> A x \<and> B x"
haftmann@22422
    98
  by (simp add: inf_fun_eq inf_bool_eq)
berghofe@22259
    99
haftmann@22422
   100
lemma inf2_iff [simp]: "inf A B x y \<longleftrightarrow> A x y \<and> B x y"
haftmann@22422
   101
  by (simp add: inf_fun_eq inf_bool_eq)
berghofe@22259
   102
berghofe@23741
   103
lemma inf_Int_eq [pred_set_conv]: "inf (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
berghofe@23741
   104
  by (simp add: expand_fun_eq)
berghofe@23741
   105
berghofe@23741
   106
lemma inf_Int_eq2 [pred_set_conv]: "inf (\<lambda>x y. (x, y) \<in> R) (\<lambda>x y. (x, y) \<in> S) = (\<lambda>x y. (x, y) \<in> R \<inter> S)"
berghofe@23741
   107
  by (simp add: expand_fun_eq)
berghofe@23741
   108
haftmann@22422
   109
lemma inf1I [intro!]: "A x ==> B x ==> inf A B x"
berghofe@22259
   110
  by simp
berghofe@22259
   111
haftmann@22422
   112
lemma inf2I [intro!]: "A x y ==> B x y ==> inf A B x y"
berghofe@22259
   113
  by simp
berghofe@22259
   114
haftmann@22422
   115
lemma inf1D1: "inf A B x ==> A x"
berghofe@22259
   116
  by simp
berghofe@22259
   117
haftmann@22422
   118
lemma inf2D1: "inf A B x y ==> A x y"
berghofe@22259
   119
  by simp
berghofe@22259
   120
haftmann@22422
   121
lemma inf1D2: "inf A B x ==> B x"
berghofe@22259
   122
  by simp
berghofe@22259
   123
haftmann@22422
   124
lemma inf2D2: "inf A B x y ==> B x y"
berghofe@22259
   125
  by simp
berghofe@22259
   126
haftmann@22422
   127
lemma inf1E [elim!]: "inf A B x ==> (A x ==> B x ==> P) ==> P"
berghofe@22259
   128
  by simp
berghofe@22259
   129
haftmann@22422
   130
lemma inf2E [elim!]: "inf A B x y ==> (A x y ==> B x y ==> P) ==> P"
berghofe@22259
   131
  by simp
berghofe@22259
   132
berghofe@22259
   133
berghofe@23741
   134
subsection {* Unions of families *}
berghofe@22259
   135
berghofe@22430
   136
lemma SUP1_iff [simp]: "(SUP x:A. B x) b = (EX x:A. B x b)"
haftmann@24345
   137
  by (simp add: SUPR_def Sup_fun_def Sup_bool_def) blast
berghofe@22430
   138
berghofe@22430
   139
lemma SUP2_iff [simp]: "(SUP x:A. B x) b c = (EX x:A. B x b c)"
haftmann@24345
   140
  by (simp add: SUPR_def Sup_fun_def Sup_bool_def) blast
berghofe@22259
   141
berghofe@22430
   142
lemma SUP1_I [intro]: "a : A ==> B a b ==> (SUP x:A. B x) b"
berghofe@22430
   143
  by auto
berghofe@22259
   144
berghofe@22430
   145
lemma SUP2_I [intro]: "a : A ==> B a b c ==> (SUP x:A. B x) b c"
berghofe@22430
   146
  by auto
berghofe@22430
   147
berghofe@22430
   148
lemma SUP1_E [elim!]: "(SUP x:A. B x) b ==> (!!x. x : A ==> B x b ==> R) ==> R"
berghofe@22430
   149
  by auto
berghofe@22430
   150
berghofe@22430
   151
lemma SUP2_E [elim!]: "(SUP x:A. B x) b c ==> (!!x. x : A ==> B x b c ==> R) ==> R"
berghofe@22259
   152
  by auto
berghofe@22259
   153
berghofe@23741
   154
lemma SUP_UN_eq: "(SUP i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (UN i. r i))"
berghofe@23741
   155
  by (simp add: expand_fun_eq)
berghofe@22430
   156
berghofe@23741
   157
lemma SUP_UN_eq2: "(SUP i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (UN i. r i))"
berghofe@23741
   158
  by (simp add: expand_fun_eq)
berghofe@22430
   159
berghofe@23741
   160
berghofe@23741
   161
subsection {* Intersections of families *}
berghofe@22430
   162
berghofe@22430
   163
lemma INF1_iff [simp]: "(INF x:A. B x) b = (ALL x:A. B x b)"
berghofe@22430
   164
  by (simp add: INFI_def Inf_fun_def Inf_bool_def) blast
berghofe@22430
   165
berghofe@22430
   166
lemma INF2_iff [simp]: "(INF x:A. B x) b c = (ALL x:A. B x b c)"
berghofe@22430
   167
  by (simp add: INFI_def Inf_fun_def Inf_bool_def) blast
berghofe@22430
   168
berghofe@22430
   169
lemma INF1_I [intro!]: "(!!x. x : A ==> B x b) ==> (INF x:A. B x) b"
berghofe@22259
   170
  by auto
berghofe@22259
   171
berghofe@22430
   172
lemma INF2_I [intro!]: "(!!x. x : A ==> B x b c) ==> (INF x:A. B x) b c"
berghofe@22430
   173
  by auto
berghofe@22430
   174
berghofe@22430
   175
lemma INF1_D [elim]: "(INF x:A. B x) b ==> a : A ==> B a b"
berghofe@22430
   176
  by auto
berghofe@22259
   177
berghofe@22430
   178
lemma INF2_D [elim]: "(INF x:A. B x) b c ==> a : A ==> B a b c"
berghofe@22430
   179
  by auto
berghofe@22430
   180
berghofe@22430
   181
lemma INF1_E [elim]: "(INF x:A. B x) b ==> (B a b ==> R) ==> (a ~: A ==> R) ==> R"
berghofe@22430
   182
  by auto
berghofe@22430
   183
berghofe@22430
   184
lemma INF2_E [elim]: "(INF x:A. B x) b c ==> (B a b c ==> R) ==> (a ~: A ==> R) ==> R"
berghofe@22430
   185
  by auto
berghofe@22259
   186
berghofe@23741
   187
lemma INF_INT_eq: "(INF i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (INT i. r i))"
berghofe@23741
   188
  by (simp add: expand_fun_eq)
berghofe@23741
   189
berghofe@23741
   190
lemma INF_INT_eq2: "(INF i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (INT i. r i))"
berghofe@23741
   191
  by (simp add: expand_fun_eq)
berghofe@23741
   192
berghofe@22259
   193
berghofe@22259
   194
subsection {* Composition of two relations *}
berghofe@22259
   195
berghofe@23741
   196
inductive
berghofe@22259
   197
  pred_comp  :: "['b => 'c => bool, 'a => 'b => bool] => 'a => 'c => bool"
berghofe@22259
   198
    (infixr "OO" 75)
berghofe@22259
   199
  for r :: "'b => 'c => bool" and s :: "'a => 'b => bool"
berghofe@22259
   200
where
berghofe@22259
   201
  pred_compI [intro]: "s a b ==> r b c ==> (r OO s) a c"
berghofe@22259
   202
berghofe@23741
   203
inductive_cases pred_compE [elim!]: "(r OO s) a c"
berghofe@22259
   204
berghofe@22259
   205
lemma pred_comp_rel_comp_eq [pred_set_conv]:
berghofe@23741
   206
  "((\<lambda>x y. (x, y) \<in> r) OO (\<lambda>x y. (x, y) \<in> s)) = (\<lambda>x y. (x, y) \<in> r O s)"
berghofe@22259
   207
  by (auto simp add: expand_fun_eq elim: pred_compE)
berghofe@22259
   208
berghofe@22259
   209
berghofe@22259
   210
subsection {* Converse *}
berghofe@22259
   211
berghofe@23741
   212
inductive
berghofe@22259
   213
  conversep :: "('a => 'b => bool) => 'b => 'a => bool"
berghofe@22259
   214
    ("(_^--1)" [1000] 1000)
berghofe@22259
   215
  for r :: "'a => 'b => bool"
berghofe@22259
   216
where
berghofe@22259
   217
  conversepI: "r a b ==> r^--1 b a"
berghofe@22259
   218
berghofe@22259
   219
notation (xsymbols)
berghofe@22259
   220
  conversep  ("(_\<inverse>\<inverse>)" [1000] 1000)
berghofe@22259
   221
berghofe@22259
   222
lemma conversepD:
berghofe@22259
   223
  assumes ab: "r^--1 a b"
berghofe@22259
   224
  shows "r b a" using ab
berghofe@22259
   225
  by cases simp
berghofe@22259
   226
berghofe@22259
   227
lemma conversep_iff [iff]: "r^--1 a b = r b a"
berghofe@22259
   228
  by (iprover intro: conversepI dest: conversepD)
berghofe@22259
   229
berghofe@22259
   230
lemma conversep_converse_eq [pred_set_conv]:
berghofe@23741
   231
  "(\<lambda>x y. (x, y) \<in> r)^--1 = (\<lambda>x y. (x, y) \<in> r^-1)"
berghofe@22259
   232
  by (auto simp add: expand_fun_eq)
berghofe@22259
   233
berghofe@22259
   234
lemma conversep_conversep [simp]: "(r^--1)^--1 = r"
berghofe@22259
   235
  by (iprover intro: order_antisym conversepI dest: conversepD)
berghofe@22259
   236
berghofe@22259
   237
lemma converse_pred_comp: "(r OO s)^--1 = s^--1 OO r^--1"
berghofe@22259
   238
  by (iprover intro: order_antisym conversepI pred_compI
berghofe@22259
   239
    elim: pred_compE dest: conversepD)
berghofe@22259
   240
haftmann@22422
   241
lemma converse_meet: "(inf r s)^--1 = inf r^--1 s^--1"
haftmann@22422
   242
  by (simp add: inf_fun_eq inf_bool_eq)
berghofe@22259
   243
    (iprover intro: conversepI ext dest: conversepD)
berghofe@22259
   244
haftmann@22422
   245
lemma converse_join: "(sup r s)^--1 = sup r^--1 s^--1"
haftmann@22422
   246
  by (simp add: sup_fun_eq sup_bool_eq)
berghofe@22259
   247
    (iprover intro: conversepI ext dest: conversepD)
berghofe@22259
   248
berghofe@22259
   249
lemma conversep_noteq [simp]: "(op ~=)^--1 = op ~="
berghofe@22259
   250
  by (auto simp add: expand_fun_eq)
berghofe@22259
   251
berghofe@22259
   252
lemma conversep_eq [simp]: "(op =)^--1 = op ="
berghofe@22259
   253
  by (auto simp add: expand_fun_eq)
berghofe@22259
   254
berghofe@22259
   255
berghofe@22259
   256
subsection {* Domain *}
berghofe@22259
   257
berghofe@23741
   258
inductive
berghofe@22259
   259
  DomainP :: "('a => 'b => bool) => 'a => bool"
berghofe@22259
   260
  for r :: "'a => 'b => bool"
berghofe@22259
   261
where
berghofe@22259
   262
  DomainPI [intro]: "r a b ==> DomainP r a"
berghofe@22259
   263
berghofe@23741
   264
inductive_cases DomainPE [elim!]: "DomainP r a"
berghofe@22259
   265
berghofe@23741
   266
lemma DomainP_Domain_eq [pred_set_conv]: "DomainP (\<lambda>x y. (x, y) \<in> r) = (\<lambda>x. x \<in> Domain r)"
berghofe@26797
   267
  by (blast intro!: Orderings.order_antisym predicate1I)
berghofe@22259
   268
berghofe@22259
   269
berghofe@22259
   270
subsection {* Range *}
berghofe@22259
   271
berghofe@23741
   272
inductive
berghofe@22259
   273
  RangeP :: "('a => 'b => bool) => 'b => bool"
berghofe@22259
   274
  for r :: "'a => 'b => bool"
berghofe@22259
   275
where
berghofe@22259
   276
  RangePI [intro]: "r a b ==> RangeP r b"
berghofe@22259
   277
berghofe@23741
   278
inductive_cases RangePE [elim!]: "RangeP r b"
berghofe@22259
   279
berghofe@23741
   280
lemma RangeP_Range_eq [pred_set_conv]: "RangeP (\<lambda>x y. (x, y) \<in> r) = (\<lambda>x. x \<in> Range r)"
berghofe@26797
   281
  by (blast intro!: Orderings.order_antisym predicate1I)
berghofe@22259
   282
berghofe@22259
   283
berghofe@22259
   284
subsection {* Inverse image *}
berghofe@22259
   285
berghofe@22259
   286
definition
berghofe@22259
   287
  inv_imagep :: "('b => 'b => bool) => ('a => 'b) => 'a => 'a => bool" where
berghofe@22259
   288
  "inv_imagep r f == %x y. r (f x) (f y)"
berghofe@22259
   289
berghofe@23741
   290
lemma [pred_set_conv]: "inv_imagep (\<lambda>x y. (x, y) \<in> r) f = (\<lambda>x y. (x, y) \<in> inv_image r f)"
berghofe@22259
   291
  by (simp add: inv_image_def inv_imagep_def)
berghofe@22259
   292
berghofe@22259
   293
lemma in_inv_imagep [simp]: "inv_imagep r f x y = r (f x) (f y)"
berghofe@22259
   294
  by (simp add: inv_imagep_def)
berghofe@22259
   295
berghofe@22259
   296
berghofe@23741
   297
subsection {* The Powerset operator *}
berghofe@23741
   298
berghofe@23741
   299
definition Powp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool" where
berghofe@23741
   300
  "Powp A == \<lambda>B. \<forall>x \<in> B. A x"
berghofe@23741
   301
berghofe@23741
   302
lemma Powp_Pow_eq [pred_set_conv]: "Powp (\<lambda>x. x \<in> A) = (\<lambda>x. x \<in> Pow A)"
berghofe@23741
   303
  by (auto simp add: Powp_def expand_fun_eq)
berghofe@23741
   304
berghofe@26797
   305
lemmas Powp_mono [mono] = Pow_mono [to_pred pred_subset_eq]
berghofe@26797
   306
berghofe@23741
   307
berghofe@22259
   308
subsection {* Properties of relations - predicate versions *}
berghofe@22259
   309
berghofe@22259
   310
abbreviation antisymP :: "('a => 'a => bool) => bool" where
berghofe@23741
   311
  "antisymP r == antisym {(x, y). r x y}"
berghofe@22259
   312
berghofe@22259
   313
abbreviation transP :: "('a => 'a => bool) => bool" where
berghofe@23741
   314
  "transP r == trans {(x, y). r x y}"
berghofe@22259
   315
berghofe@22259
   316
abbreviation single_valuedP :: "('a => 'b => bool) => bool" where
berghofe@23741
   317
  "single_valuedP r == single_valued {(x, y). r x y}"
berghofe@22259
   318
berghofe@22259
   319
end