src/HOL/Predicate.thy
author berghofe
Wed Feb 07 17:25:39 2007 +0100 (2007-02-07)
changeset 22259 476604be7d88
child 22422 ee19cdb07528
permissions -rw-r--r--
New theory for converting between predicates and sets.
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
berghofe@22259
     9
imports Inductive
berghofe@22259
    10
begin
berghofe@22259
    11
berghofe@22259
    12
subsection {* Converting between predicates and sets *}
berghofe@22259
    13
berghofe@22259
    14
definition
berghofe@22259
    15
  member :: "'a set => 'a => bool" where
berghofe@22259
    16
  "member == %S x. x : S"
berghofe@22259
    17
berghofe@22259
    18
lemma memberI[intro!, Pure.intro!]: "x : S ==> member S x"
berghofe@22259
    19
  by (simp add: member_def)
berghofe@22259
    20
berghofe@22259
    21
lemma memberD[dest!, Pure.dest!]: "member S x ==> x : S"
berghofe@22259
    22
  by (simp add: member_def)
berghofe@22259
    23
berghofe@22259
    24
lemma member_eq[simp]: "member S x = (x : S)"
berghofe@22259
    25
  by (simp add: member_def)
berghofe@22259
    26
berghofe@22259
    27
lemma member_Collect_eq[simp]: "member (Collect P) = P"
berghofe@22259
    28
  by (simp add: member_def)
berghofe@22259
    29
berghofe@22259
    30
lemma Collect_member_eq[simp]: "Collect (member S) = S"
berghofe@22259
    31
  by (simp add: member_def)
berghofe@22259
    32
berghofe@22259
    33
lemma split_set: "(!!S. PROP P S) == (!!S. PROP P (Collect S))"
berghofe@22259
    34
proof
berghofe@22259
    35
  fix S
berghofe@22259
    36
  assume "!!S. PROP P S"
berghofe@22259
    37
  show "PROP P (Collect S)" .
berghofe@22259
    38
next
berghofe@22259
    39
  fix S
berghofe@22259
    40
  assume "!!S. PROP P (Collect S)"
berghofe@22259
    41
  have "PROP P {x. x : S}" .
berghofe@22259
    42
  thus "PROP P S" by simp
berghofe@22259
    43
qed
berghofe@22259
    44
berghofe@22259
    45
lemma split_predicate: "(!!S. PROP P S) == (!!S. PROP P (member S))"
berghofe@22259
    46
proof
berghofe@22259
    47
  fix S
berghofe@22259
    48
  assume "!!S. PROP P S"
berghofe@22259
    49
  show "PROP P (member S)" .
berghofe@22259
    50
next
berghofe@22259
    51
  fix S
berghofe@22259
    52
  assume "!!S. PROP P (member S)"
berghofe@22259
    53
  have "PROP P (member {x. S x})" .
berghofe@22259
    54
  thus "PROP P S" by simp
berghofe@22259
    55
qed
berghofe@22259
    56
berghofe@22259
    57
lemma member_right_eq: "(x == member y) == (Collect x == y)"
berghofe@22259
    58
  by (rule equal_intr_rule, simp, drule symmetric, simp)
berghofe@22259
    59
berghofe@22259
    60
definition
berghofe@22259
    61
  member2 :: "('a * 'b) set => 'a => 'b \<Rightarrow> bool" where
berghofe@22259
    62
  "member2 == %S x y. (x, y) : S"
berghofe@22259
    63
berghofe@22259
    64
definition
berghofe@22259
    65
  Collect2 :: "('a => 'b => bool) => ('a * 'b) set" where
berghofe@22259
    66
  "Collect2 == %P. {(x, y). P x y}"
berghofe@22259
    67
berghofe@22259
    68
lemma member2I[intro!, Pure.intro!]: "(x, y) : S ==> member2 S x y"
berghofe@22259
    69
  by (simp add: member2_def)
berghofe@22259
    70
berghofe@22259
    71
lemma member2D[dest!, Pure.dest!]: "member2 S x y ==> (x, y) : S"
berghofe@22259
    72
  by (simp add: member2_def)
berghofe@22259
    73
berghofe@22259
    74
lemma member2_eq[simp]: "member2 S x y = ((x, y) : S)"
berghofe@22259
    75
  by (simp add: member2_def)
berghofe@22259
    76
berghofe@22259
    77
lemma Collect2I: "P x y ==> (x, y) : Collect2 P"
berghofe@22259
    78
  by (simp add: Collect2_def)
berghofe@22259
    79
berghofe@22259
    80
lemma Collect2D: "(x, y) : Collect2 P ==> P x y"
berghofe@22259
    81
  by (simp add: Collect2_def)
berghofe@22259
    82
berghofe@22259
    83
lemma member2_Collect2_eq[simp]: "member2 (Collect2 P) = P"
berghofe@22259
    84
  by (simp add: member2_def Collect2_def)
berghofe@22259
    85
berghofe@22259
    86
lemma Collect2_member2_eq[simp]: "Collect2 (member2 S) = S"
berghofe@22259
    87
  by (auto simp add: member2_def Collect2_def)
berghofe@22259
    88
berghofe@22259
    89
lemma mem_Collect2_eq[iff]: "((x, y) : Collect2 P) = P x y"
berghofe@22259
    90
  by (iprover intro: Collect2I dest: Collect2D)
berghofe@22259
    91
berghofe@22259
    92
lemma member2_Collect_split_eq [simp]: "member2 (Collect (split P)) = P"
berghofe@22259
    93
  by (simp add: expand_fun_eq)
berghofe@22259
    94
berghofe@22259
    95
lemma split_set2: "(!!S. PROP P S) == (!!S. PROP P (Collect2 S))"
berghofe@22259
    96
proof
berghofe@22259
    97
  fix S
berghofe@22259
    98
  assume "!!S. PROP P S"
berghofe@22259
    99
  show "PROP P (Collect2 S)" .
berghofe@22259
   100
next
berghofe@22259
   101
  fix S
berghofe@22259
   102
  assume "!!S. PROP P (Collect2 S)"
berghofe@22259
   103
  have "PROP P (Collect2 (member2 S))" .
berghofe@22259
   104
  thus "PROP P S" by simp
berghofe@22259
   105
qed
berghofe@22259
   106
berghofe@22259
   107
lemma split_predicate2: "(!!S. PROP P S) == (!!S. PROP P (member2 S))"
berghofe@22259
   108
proof
berghofe@22259
   109
  fix S
berghofe@22259
   110
  assume "!!S. PROP P S"
berghofe@22259
   111
  show "PROP P (member2 S)" .
berghofe@22259
   112
next
berghofe@22259
   113
  fix S
berghofe@22259
   114
  assume "!!S. PROP P (member2 S)"
berghofe@22259
   115
  have "PROP P (member2 (Collect2 S))" .
berghofe@22259
   116
  thus "PROP P S" by simp
berghofe@22259
   117
qed
berghofe@22259
   118
berghofe@22259
   119
lemma member2_right_eq: "(x == member2 y) == (Collect2 x == y)"
berghofe@22259
   120
  by (rule equal_intr_rule, simp, drule symmetric, simp)
berghofe@22259
   121
berghofe@22259
   122
ML_setup {*
berghofe@22259
   123
local
berghofe@22259
   124
berghofe@22259
   125
fun vars_of b (v as Var _) = if b then [] else [v]
berghofe@22259
   126
  | vars_of b (t $ u) = vars_of true t union vars_of false u
berghofe@22259
   127
  | vars_of b (Abs (_, _, t)) = vars_of false t
berghofe@22259
   128
  | vars_of _ _ = [];
berghofe@22259
   129
berghofe@22259
   130
fun rew ths1 ths2 th = Drule.forall_elim_vars 0
berghofe@22259
   131
  (rewrite_rule ths2 (rewrite_rule ths1 (Drule.forall_intr_list
berghofe@22259
   132
    (map (cterm_of (theory_of_thm th)) (vars_of false (prop_of th))) th)));
berghofe@22259
   133
berghofe@22259
   134
val get_eq = Simpdata.mk_eq o thm;
berghofe@22259
   135
berghofe@22259
   136
val split_predicate = get_eq "split_predicate";
berghofe@22259
   137
val split_predicate2 = get_eq "split_predicate2";
berghofe@22259
   138
val split_set = get_eq "split_set";
berghofe@22259
   139
val split_set2 = get_eq "split_set2";
berghofe@22259
   140
val member_eq = get_eq "member_eq";
berghofe@22259
   141
val member2_eq = get_eq "member2_eq";
berghofe@22259
   142
val member_Collect_eq = get_eq "member_Collect_eq";
berghofe@22259
   143
val member2_Collect2_eq = get_eq "member2_Collect2_eq";
berghofe@22259
   144
val mem_Collect2_eq = get_eq "mem_Collect2_eq";
berghofe@22259
   145
val member_right_eq = thm "member_right_eq";
berghofe@22259
   146
val member2_right_eq = thm "member2_right_eq";
berghofe@22259
   147
berghofe@22259
   148
val rew' = Thm.symmetric o rew [split_set2] [split_set,
berghofe@22259
   149
  member_right_eq, member2_right_eq, member_Collect_eq, member2_Collect2_eq];
berghofe@22259
   150
berghofe@22259
   151
val rules1 = [split_predicate, split_predicate2, member_eq, member2_eq];
berghofe@22259
   152
val rules2 = [split_set, mk_meta_eq mem_Collect_eq, mem_Collect2_eq];
berghofe@22259
   153
berghofe@22259
   154
structure PredSetConvData = GenericDataFun
berghofe@22259
   155
(struct
berghofe@22259
   156
  val name = "HOL/pred_set_conv";
berghofe@22259
   157
  type T = thm list;
berghofe@22259
   158
  val empty = [];
berghofe@22259
   159
  val extend = I;
berghofe@22259
   160
  fun merge _ = Drule.merge_rules;
berghofe@22259
   161
  fun print _ _ = ()
berghofe@22259
   162
end)
berghofe@22259
   163
berghofe@22259
   164
fun mk_attr ths1 ths2 f = Attrib.syntax (Attrib.thms >> (fn ths =>
berghofe@22259
   165
  Thm.rule_attribute (fn ctxt => rew ths1 (map (f o Simpdata.mk_eq)
berghofe@22259
   166
    (ths @ PredSetConvData.get ctxt) @ ths2))));
berghofe@22259
   167
berghofe@22259
   168
val pred_set_conv_att = Attrib.no_args (Thm.declaration_attribute
berghofe@22259
   169
  (Drule.add_rule #> PredSetConvData.map));
berghofe@22259
   170
berghofe@22259
   171
in
berghofe@22259
   172
berghofe@22259
   173
val _ = ML_Context.>> (PredSetConvData.init #>
berghofe@22259
   174
  Attrib.add_attributes
berghofe@22259
   175
    [("pred_set_conv", pred_set_conv_att,
berghofe@22259
   176
        "declare rules for converting between predicate and set notation"),
berghofe@22259
   177
     ("to_set", mk_attr [] rules1 I, "convert rule to set notation"),
berghofe@22259
   178
     ("to_pred", mk_attr [split_set2] rules2 rew',
berghofe@22259
   179
        "convert rule to predicate notation")])
berghofe@22259
   180
berghofe@22259
   181
end;
berghofe@22259
   182
*}
berghofe@22259
   183
berghofe@22259
   184
lemma member_inject [pred_set_conv]: "(member R = member S) = (R = S)"
berghofe@22259
   185
  by (auto simp add: expand_fun_eq)
berghofe@22259
   186
berghofe@22259
   187
lemma member2_inject [pred_set_conv]: "(member2 R = member2 S) = (R = S)"
berghofe@22259
   188
  by (auto simp add: expand_fun_eq)
berghofe@22259
   189
berghofe@22259
   190
lemma member_mono [pred_set_conv]: "(member R <= member S) = (R <= S)"
berghofe@22259
   191
  by fast
berghofe@22259
   192
berghofe@22259
   193
lemma member2_mono [pred_set_conv]: "(member2 R <= member2 S) = (R <= S)"
berghofe@22259
   194
  by fast
berghofe@22259
   195
berghofe@22259
   196
lemma member_empty [pred_set_conv]: "(%x. False) = member {}"
berghofe@22259
   197
  by (simp add: expand_fun_eq)
berghofe@22259
   198
berghofe@22259
   199
lemma member2_empty [pred_set_conv]: "(%x y. False) = member2 {}"
berghofe@22259
   200
  by (simp add: expand_fun_eq)
berghofe@22259
   201
berghofe@22259
   202
berghofe@22259
   203
subsubsection {* Binary union *}
berghofe@22259
   204
berghofe@22259
   205
lemma member_Un [pred_set_conv]: "join (member R) (member S) = member (R Un S)"
berghofe@22259
   206
  by (simp add: expand_fun_eq join_fun_eq join_bool_eq)
berghofe@22259
   207
berghofe@22259
   208
lemma member2_Un [pred_set_conv]: "join (member2 R) (member2 S) = member2 (R Un S)"
berghofe@22259
   209
  by (simp add: expand_fun_eq join_fun_eq join_bool_eq)
berghofe@22259
   210
berghofe@22259
   211
lemma join1_iff [simp]: "(join A B x) = (A x | B x)"
berghofe@22259
   212
  by (simp add: join_fun_eq join_bool_eq)
berghofe@22259
   213
berghofe@22259
   214
lemma join2_iff [simp]: "(join A B x y) = (A x y | B x y)"
berghofe@22259
   215
  by (simp add: join_fun_eq join_bool_eq)
berghofe@22259
   216
berghofe@22259
   217
lemma join1I1 [elim?]: "A x ==> join A B x"
berghofe@22259
   218
  by simp
berghofe@22259
   219
berghofe@22259
   220
lemma join2I1 [elim?]: "A x y ==> join A B x y"
berghofe@22259
   221
  by simp
berghofe@22259
   222
berghofe@22259
   223
lemma join1I2 [elim?]: "B x ==> join A B x"
berghofe@22259
   224
  by simp
berghofe@22259
   225
berghofe@22259
   226
lemma join2I2 [elim?]: "B x y ==> join A B x y"
berghofe@22259
   227
  by simp
berghofe@22259
   228
berghofe@22259
   229
text {*
berghofe@22259
   230
  \medskip Classical introduction rule: no commitment to @{text A} vs
berghofe@22259
   231
  @{text B}.
berghofe@22259
   232
*}
berghofe@22259
   233
berghofe@22259
   234
lemma join1CI [intro!]: "(~ B x ==> A x) ==> join A B x"
berghofe@22259
   235
  by auto
berghofe@22259
   236
berghofe@22259
   237
lemma join2CI [intro!]: "(~ B x y ==> A x y) ==> join A B x y"
berghofe@22259
   238
  by auto
berghofe@22259
   239
berghofe@22259
   240
lemma join1E [elim!]: "join A B x ==> (A x ==> P) ==> (B x ==> P) ==> P"
berghofe@22259
   241
  by simp iprover
berghofe@22259
   242
berghofe@22259
   243
lemma join2E [elim!]: "join A B x y ==> (A x y ==> P) ==> (B x y ==> P) ==> P"
berghofe@22259
   244
  by simp iprover
berghofe@22259
   245
berghofe@22259
   246
berghofe@22259
   247
subsubsection {* Binary intersection *}
berghofe@22259
   248
berghofe@22259
   249
lemma member_Int [pred_set_conv]: "meet (member R) (member S) = member (R Int S)"
berghofe@22259
   250
  by (simp add: expand_fun_eq meet_fun_eq meet_bool_eq)
berghofe@22259
   251
berghofe@22259
   252
lemma member2_Int [pred_set_conv]: "meet (member2 R) (member2 S) = member2 (R Int S)"
berghofe@22259
   253
  by (simp add: expand_fun_eq meet_fun_eq meet_bool_eq)
berghofe@22259
   254
berghofe@22259
   255
lemma meet1_iff [simp]: "(meet A B x) = (A x & B x)"
berghofe@22259
   256
  by (simp add: meet_fun_eq meet_bool_eq)
berghofe@22259
   257
berghofe@22259
   258
lemma meet2_iff [simp]: "(meet A B x y) = (A x y & B x y)"
berghofe@22259
   259
  by (simp add: meet_fun_eq meet_bool_eq)
berghofe@22259
   260
berghofe@22259
   261
lemma meet1I [intro!]: "A x ==> B x ==> meet A B x"
berghofe@22259
   262
  by simp
berghofe@22259
   263
berghofe@22259
   264
lemma meet2I [intro!]: "A x y ==> B x y ==> meet A B x y"
berghofe@22259
   265
  by simp
berghofe@22259
   266
berghofe@22259
   267
lemma meet1D1: "meet A B x ==> A x"
berghofe@22259
   268
  by simp
berghofe@22259
   269
berghofe@22259
   270
lemma meet2D1: "meet A B x y ==> A x y"
berghofe@22259
   271
  by simp
berghofe@22259
   272
berghofe@22259
   273
lemma meet1D2: "meet A B x ==> B x"
berghofe@22259
   274
  by simp
berghofe@22259
   275
berghofe@22259
   276
lemma meet2D2: "meet A B x y ==> B x y"
berghofe@22259
   277
  by simp
berghofe@22259
   278
berghofe@22259
   279
lemma meet1E [elim!]: "meet A B x ==> (A x ==> B x ==> P) ==> P"
berghofe@22259
   280
  by simp
berghofe@22259
   281
berghofe@22259
   282
lemma meet2E [elim!]: "meet A B x y ==> (A x y ==> B x y ==> P) ==> P"
berghofe@22259
   283
  by simp
berghofe@22259
   284
berghofe@22259
   285
berghofe@22259
   286
subsubsection {* Unions of families *}
berghofe@22259
   287
berghofe@22259
   288
lemma member_SUP: "(SUP i. member (r i)) = member (UN i. r i)"
berghofe@22259
   289
  by (simp add: SUP_def Sup_fun_eq Sup_bool_eq expand_fun_eq) blast
berghofe@22259
   290
berghofe@22259
   291
lemma member2_SUP: "(SUP i. member2 (r i)) = member2 (UN i. r i)"
berghofe@22259
   292
  by (simp add: SUP_def Sup_fun_eq Sup_bool_eq expand_fun_eq) blast
berghofe@22259
   293
berghofe@22259
   294
lemma SUP1_iff [simp]: "((SUP x. B x) b) = (EX x. B x b)"
berghofe@22259
   295
  by (simp add: SUP_def Sup_fun_eq Sup_bool_eq) blast
berghofe@22259
   296
berghofe@22259
   297
lemma SUP2_iff [simp]: "((SUP x. B x) b c) = (EX x. B x b c)"
berghofe@22259
   298
  by (simp add: SUP_def Sup_fun_eq Sup_bool_eq) blast
berghofe@22259
   299
berghofe@22259
   300
lemma SUP1_I [intro]: "B a b ==> (SUP x. B x) b"
berghofe@22259
   301
  by auto
berghofe@22259
   302
berghofe@22259
   303
lemma SUP2_I [intro]: "B a b c ==> (SUP x. B x) b c"
berghofe@22259
   304
  by auto
berghofe@22259
   305
berghofe@22259
   306
lemma SUP1_E [elim!]: "(SUP x. B x) b ==> (!!x. B x b ==> R) ==> R"
berghofe@22259
   307
  by simp iprover
berghofe@22259
   308
berghofe@22259
   309
lemma SUP2_E [elim!]: "(SUP x. B x) b c ==> (!!x. B x b c ==> R) ==> R"
berghofe@22259
   310
  by simp iprover
berghofe@22259
   311
berghofe@22259
   312
berghofe@22259
   313
subsection {* Composition of two relations *}
berghofe@22259
   314
berghofe@22259
   315
inductive2
berghofe@22259
   316
  pred_comp  :: "['b => 'c => bool, 'a => 'b => bool] => 'a => 'c => bool"
berghofe@22259
   317
    (infixr "OO" 75)
berghofe@22259
   318
  for r :: "'b => 'c => bool" and s :: "'a => 'b => bool"
berghofe@22259
   319
where
berghofe@22259
   320
  pred_compI [intro]: "s a b ==> r b c ==> (r OO s) a c"
berghofe@22259
   321
berghofe@22259
   322
inductive_cases2 pred_compE [elim!]: "(r OO s) a c"
berghofe@22259
   323
berghofe@22259
   324
lemma pred_comp_rel_comp_eq [pred_set_conv]:
berghofe@22259
   325
  "(member2 r OO member2 s) = member2 (r O s)"
berghofe@22259
   326
  by (auto simp add: expand_fun_eq elim: pred_compE)
berghofe@22259
   327
berghofe@22259
   328
berghofe@22259
   329
subsection {* Converse *}
berghofe@22259
   330
berghofe@22259
   331
inductive2
berghofe@22259
   332
  conversep :: "('a => 'b => bool) => 'b => 'a => bool"
berghofe@22259
   333
    ("(_^--1)" [1000] 1000)
berghofe@22259
   334
  for r :: "'a => 'b => bool"
berghofe@22259
   335
where
berghofe@22259
   336
  conversepI: "r a b ==> r^--1 b a"
berghofe@22259
   337
berghofe@22259
   338
notation (xsymbols)
berghofe@22259
   339
  conversep  ("(_\<inverse>\<inverse>)" [1000] 1000)
berghofe@22259
   340
berghofe@22259
   341
lemma conversepD:
berghofe@22259
   342
  assumes ab: "r^--1 a b"
berghofe@22259
   343
  shows "r b a" using ab
berghofe@22259
   344
  by cases simp
berghofe@22259
   345
berghofe@22259
   346
lemma conversep_iff [iff]: "r^--1 a b = r b a"
berghofe@22259
   347
  by (iprover intro: conversepI dest: conversepD)
berghofe@22259
   348
berghofe@22259
   349
lemma conversep_converse_eq [pred_set_conv]:
berghofe@22259
   350
  "(member2 r)^--1 = member2 (r^-1)"
berghofe@22259
   351
  by (auto simp add: expand_fun_eq)
berghofe@22259
   352
berghofe@22259
   353
lemma conversep_conversep [simp]: "(r^--1)^--1 = r"
berghofe@22259
   354
  by (iprover intro: order_antisym conversepI dest: conversepD)
berghofe@22259
   355
berghofe@22259
   356
lemma converse_pred_comp: "(r OO s)^--1 = s^--1 OO r^--1"
berghofe@22259
   357
  by (iprover intro: order_antisym conversepI pred_compI
berghofe@22259
   358
    elim: pred_compE dest: conversepD)
berghofe@22259
   359
berghofe@22259
   360
lemma converse_meet: "(meet r s)^--1 = meet r^--1 s^--1"
berghofe@22259
   361
  by (simp add: meet_fun_eq meet_bool_eq)
berghofe@22259
   362
    (iprover intro: conversepI ext dest: conversepD)
berghofe@22259
   363
berghofe@22259
   364
lemma converse_join: "(join r s)^--1 = join r^--1 s^--1"
berghofe@22259
   365
  by (simp add: join_fun_eq join_bool_eq)
berghofe@22259
   366
    (iprover intro: conversepI ext dest: conversepD)
berghofe@22259
   367
berghofe@22259
   368
lemma conversep_noteq [simp]: "(op ~=)^--1 = op ~="
berghofe@22259
   369
  by (auto simp add: expand_fun_eq)
berghofe@22259
   370
berghofe@22259
   371
lemma conversep_eq [simp]: "(op =)^--1 = op ="
berghofe@22259
   372
  by (auto simp add: expand_fun_eq)
berghofe@22259
   373
berghofe@22259
   374
berghofe@22259
   375
subsection {* Domain *}
berghofe@22259
   376
berghofe@22259
   377
inductive2
berghofe@22259
   378
  DomainP :: "('a => 'b => bool) => 'a => bool"
berghofe@22259
   379
  for r :: "'a => 'b => bool"
berghofe@22259
   380
where
berghofe@22259
   381
  DomainPI [intro]: "r a b ==> DomainP r a"
berghofe@22259
   382
berghofe@22259
   383
inductive_cases2 DomainPE [elim!]: "DomainP r a"
berghofe@22259
   384
berghofe@22259
   385
lemma member2_DomainP [pred_set_conv]: "DomainP (member2 r) = member (Domain r)"
berghofe@22259
   386
  by (blast intro!: Orderings.order_antisym)
berghofe@22259
   387
berghofe@22259
   388
berghofe@22259
   389
subsection {* Range *}
berghofe@22259
   390
berghofe@22259
   391
inductive2
berghofe@22259
   392
  RangeP :: "('a => 'b => bool) => 'b => bool"
berghofe@22259
   393
  for r :: "'a => 'b => bool"
berghofe@22259
   394
where
berghofe@22259
   395
  RangePI [intro]: "r a b ==> RangeP r b"
berghofe@22259
   396
berghofe@22259
   397
inductive_cases2 RangePE [elim!]: "RangeP r b"
berghofe@22259
   398
berghofe@22259
   399
lemma member2_RangeP [pred_set_conv]: "RangeP (member2 r) = member (Range r)"
berghofe@22259
   400
  by (blast intro!: Orderings.order_antisym)
berghofe@22259
   401
berghofe@22259
   402
berghofe@22259
   403
subsection {* Inverse image *}
berghofe@22259
   404
berghofe@22259
   405
definition
berghofe@22259
   406
  inv_imagep :: "('b => 'b => bool) => ('a => 'b) => 'a => 'a => bool" where
berghofe@22259
   407
  "inv_imagep r f == %x y. r (f x) (f y)"
berghofe@22259
   408
berghofe@22259
   409
lemma [pred_set_conv]: "inv_imagep (member2 r) f = member2 (inv_image r f)"
berghofe@22259
   410
  by (simp add: inv_image_def inv_imagep_def)
berghofe@22259
   411
berghofe@22259
   412
lemma in_inv_imagep [simp]: "inv_imagep r f x y = r (f x) (f y)"
berghofe@22259
   413
  by (simp add: inv_imagep_def)
berghofe@22259
   414
berghofe@22259
   415
berghofe@22259
   416
subsection {* Properties of relations - predicate versions *}
berghofe@22259
   417
berghofe@22259
   418
abbreviation antisymP :: "('a => 'a => bool) => bool" where
berghofe@22259
   419
  "antisymP r == antisym (Collect2 r)"
berghofe@22259
   420
berghofe@22259
   421
abbreviation transP :: "('a => 'a => bool) => bool" where
berghofe@22259
   422
  "transP r == trans (Collect2 r)"
berghofe@22259
   423
berghofe@22259
   424
abbreviation single_valuedP :: "('a => 'b => bool) => bool" where
berghofe@22259
   425
  "single_valuedP r == single_valued (Collect2 r)"
berghofe@22259
   426
berghofe@22259
   427
berghofe@22259
   428
subsection {* Bounded quantifiers for predicates *}
berghofe@22259
   429
berghofe@22259
   430
text {*
berghofe@22259
   431
Bounded existential quantifier for predicates (executable).
berghofe@22259
   432
*}
berghofe@22259
   433
berghofe@22259
   434
inductive2 bexp :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
berghofe@22259
   435
  for P :: "'a \<Rightarrow> bool" and Q :: "'a \<Rightarrow> bool"
berghofe@22259
   436
where
berghofe@22259
   437
  bexpI [intro]: "P x \<Longrightarrow> Q x \<Longrightarrow> bexp P Q"
berghofe@22259
   438
berghofe@22259
   439
lemmas bexpE [elim!] = bexp.cases
berghofe@22259
   440
berghofe@22259
   441
syntax
berghofe@22259
   442
  Bexp :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool \<Rightarrow> bool" ("(3\<exists>_\<triangleright>_./ _)" [0, 0, 10] 10)
berghofe@22259
   443
berghofe@22259
   444
translations
berghofe@22259
   445
  "\<exists>x\<triangleright>P. Q" \<rightleftharpoons> "CONST bexp P (\<lambda>x. Q)"
berghofe@22259
   446
berghofe@22259
   447
constdefs
berghofe@22259
   448
  ballp :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
berghofe@22259
   449
  "ballp P Q \<equiv> \<forall>x. P x \<longrightarrow> Q x"
berghofe@22259
   450
berghofe@22259
   451
syntax
berghofe@22259
   452
  Ballp :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool \<Rightarrow> bool" ("(3\<forall>_\<triangleright>_./ _)" [0, 0, 10] 10)
berghofe@22259
   453
berghofe@22259
   454
translations
berghofe@22259
   455
  "\<forall>x\<triangleright>P. Q" \<rightleftharpoons> "CONST ballp P (\<lambda>x. Q)"
berghofe@22259
   456
berghofe@22259
   457
(* To avoid eta-contraction of body: *)
berghofe@22259
   458
print_translation {*
berghofe@22259
   459
let
berghofe@22259
   460
  fun btr' syn [A,Abs abs] =
berghofe@22259
   461
    let val (x,t) = atomic_abs_tr' abs
berghofe@22259
   462
    in Syntax.const syn $ x $ A $ t end
berghofe@22259
   463
in
berghofe@22259
   464
[("ballp", btr' "Ballp"),("bexp", btr' "Bexp")]
berghofe@22259
   465
end
berghofe@22259
   466
*}
berghofe@22259
   467
berghofe@22259
   468
lemma ballpI [intro!]: "(\<And>x. A x \<Longrightarrow> P x) \<Longrightarrow> \<forall>x\<triangleright>A. P x"
berghofe@22259
   469
  by (simp add: ballp_def)
berghofe@22259
   470
berghofe@22259
   471
lemma bspecp [dest?]: "\<forall>x\<triangleright>A. P x \<Longrightarrow> A x \<Longrightarrow> P x"
berghofe@22259
   472
  by (simp add: ballp_def)
berghofe@22259
   473
berghofe@22259
   474
lemma ballpE [elim]: "\<forall>x\<triangleright>A. P x \<Longrightarrow> (P x \<Longrightarrow> Q) \<Longrightarrow> (\<not> A x \<Longrightarrow> Q) \<Longrightarrow> Q"
berghofe@22259
   475
  by (unfold ballp_def) blast
berghofe@22259
   476
berghofe@22259
   477
lemma ballp_not_bexp_eq: "(\<forall>x\<triangleright>P. Q x) = (\<not> (\<exists>x\<triangleright>P. \<not> Q x))"
berghofe@22259
   478
  by (blast dest: bspecp)
berghofe@22259
   479
berghofe@22259
   480
declare ballp_not_bexp_eq [THEN eq_reflection, code unfold]
berghofe@22259
   481
berghofe@22259
   482
end