src/HOL/Predicate.thy
author haftmann
Tue Jul 10 17:30:49 2007 +0200 (2007-07-10)
changeset 23708 b5eb0b4dd17d
parent 23389 aaca6a8e5414
child 23741 1801a921df13
permissions -rw-r--r--
clarified import
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@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"
wenzelm@23389
    37
  then show "PROP P (Collect S)" .
berghofe@22259
    38
next
berghofe@22259
    39
  fix S
berghofe@22259
    40
  assume "!!S. PROP P (Collect S)"
wenzelm@23389
    41
  then 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"
wenzelm@23389
    49
  then show "PROP P (member S)" .
berghofe@22259
    50
next
berghofe@22259
    51
  fix S
berghofe@22259
    52
  assume "!!S. PROP P (member S)"
wenzelm@23389
    53
  then 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"
wenzelm@23389
    99
  then show "PROP P (Collect2 S)" .
berghofe@22259
   100
next
berghofe@22259
   101
  fix S
berghofe@22259
   102
  assume "!!S. PROP P (Collect2 S)"
wenzelm@23389
   103
  then 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"
wenzelm@23389
   111
  then show "PROP P (member2 S)" .
berghofe@22259
   112
next
berghofe@22259
   113
  fix S
berghofe@22259
   114
  assume "!!S. PROP P (member2 S)"
wenzelm@23389
   115
  then 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
wenzelm@22846
   155
(
berghofe@22259
   156
  type T = thm list;
berghofe@22259
   157
  val empty = [];
berghofe@22259
   158
  val extend = I;
berghofe@22259
   159
  fun merge _ = Drule.merge_rules;
wenzelm@22846
   160
);
berghofe@22259
   161
berghofe@22259
   162
fun mk_attr ths1 ths2 f = Attrib.syntax (Attrib.thms >> (fn ths =>
berghofe@22259
   163
  Thm.rule_attribute (fn ctxt => rew ths1 (map (f o Simpdata.mk_eq)
berghofe@22259
   164
    (ths @ PredSetConvData.get ctxt) @ ths2))));
berghofe@22259
   165
berghofe@22259
   166
val pred_set_conv_att = Attrib.no_args (Thm.declaration_attribute
berghofe@22259
   167
  (Drule.add_rule #> PredSetConvData.map));
berghofe@22259
   168
berghofe@22259
   169
in
berghofe@22259
   170
wenzelm@22846
   171
val _ = ML_Context.>> (
berghofe@22259
   172
  Attrib.add_attributes
berghofe@22259
   173
    [("pred_set_conv", pred_set_conv_att,
berghofe@22259
   174
        "declare rules for converting between predicate and set notation"),
berghofe@22259
   175
     ("to_set", mk_attr [] rules1 I, "convert rule to set notation"),
berghofe@22259
   176
     ("to_pred", mk_attr [split_set2] rules2 rew',
berghofe@22259
   177
        "convert rule to predicate notation")])
berghofe@22259
   178
berghofe@22259
   179
end;
berghofe@22259
   180
*}
berghofe@22259
   181
berghofe@22259
   182
lemma member_inject [pred_set_conv]: "(member R = member S) = (R = S)"
berghofe@22259
   183
  by (auto simp add: expand_fun_eq)
berghofe@22259
   184
berghofe@22259
   185
lemma member2_inject [pred_set_conv]: "(member2 R = member2 S) = (R = S)"
berghofe@22259
   186
  by (auto simp add: expand_fun_eq)
berghofe@22259
   187
berghofe@22259
   188
lemma member_mono [pred_set_conv]: "(member R <= member S) = (R <= S)"
berghofe@22259
   189
  by fast
berghofe@22259
   190
berghofe@22259
   191
lemma member2_mono [pred_set_conv]: "(member2 R <= member2 S) = (R <= S)"
berghofe@22259
   192
  by fast
berghofe@22259
   193
berghofe@22259
   194
lemma member_empty [pred_set_conv]: "(%x. False) = member {}"
berghofe@22259
   195
  by (simp add: expand_fun_eq)
berghofe@22259
   196
berghofe@22259
   197
lemma member2_empty [pred_set_conv]: "(%x y. False) = member2 {}"
berghofe@22259
   198
  by (simp add: expand_fun_eq)
berghofe@22259
   199
berghofe@22259
   200
berghofe@22259
   201
subsubsection {* Binary union *}
berghofe@22259
   202
haftmann@22422
   203
lemma member_Un [pred_set_conv]: "sup (member R) (member S) = member (R Un S)"
haftmann@22422
   204
  by (simp add: expand_fun_eq sup_fun_eq sup_bool_eq)
berghofe@22259
   205
haftmann@22422
   206
lemma member2_Un [pred_set_conv]: "sup (member2 R) (member2 S) = member2 (R Un S)"
haftmann@22422
   207
  by (simp add: expand_fun_eq sup_fun_eq sup_bool_eq)
berghofe@22259
   208
haftmann@22422
   209
lemma sup1_iff [simp]: "sup A B x \<longleftrightarrow> A x | B x"
haftmann@22422
   210
  by (simp add: sup_fun_eq sup_bool_eq)
berghofe@22259
   211
haftmann@22422
   212
lemma sup2_iff [simp]: "sup A B x y \<longleftrightarrow> A x y | B x y"
haftmann@22422
   213
  by (simp add: sup_fun_eq sup_bool_eq)
berghofe@22259
   214
haftmann@22422
   215
lemma sup1I1 [elim?]: "A x \<Longrightarrow> sup A B x"
berghofe@22259
   216
  by simp
berghofe@22259
   217
haftmann@22422
   218
lemma sup2I1 [elim?]: "A x y \<Longrightarrow> sup A B x y"
berghofe@22259
   219
  by simp
berghofe@22259
   220
haftmann@22422
   221
lemma join1I2 [elim?]: "B x \<Longrightarrow> sup A B x"
berghofe@22259
   222
  by simp
berghofe@22259
   223
haftmann@22422
   224
lemma sup1I2 [elim?]: "B x y \<Longrightarrow> sup A B x y"
berghofe@22259
   225
  by simp
berghofe@22259
   226
berghofe@22259
   227
text {*
berghofe@22259
   228
  \medskip Classical introduction rule: no commitment to @{text A} vs
berghofe@22259
   229
  @{text B}.
berghofe@22259
   230
*}
berghofe@22259
   231
haftmann@22422
   232
lemma sup1CI [intro!]: "(~ B x ==> A x) ==> sup A B x"
berghofe@22259
   233
  by auto
berghofe@22259
   234
haftmann@22422
   235
lemma sup2CI [intro!]: "(~ B x y ==> A x y) ==> sup A B x y"
berghofe@22259
   236
  by auto
berghofe@22259
   237
haftmann@22422
   238
lemma sup1E [elim!]: "sup A B x ==> (A x ==> P) ==> (B x ==> P) ==> P"
berghofe@22259
   239
  by simp iprover
berghofe@22259
   240
haftmann@22422
   241
lemma sup2E [elim!]: "sup A B x y ==> (A x y ==> P) ==> (B x y ==> P) ==> P"
berghofe@22259
   242
  by simp iprover
berghofe@22259
   243
berghofe@22259
   244
berghofe@22259
   245
subsubsection {* Binary intersection *}
berghofe@22259
   246
haftmann@22422
   247
lemma member_Int [pred_set_conv]: "inf (member R) (member S) = member (R Int S)"
haftmann@22422
   248
  by (simp add: expand_fun_eq inf_fun_eq inf_bool_eq)
berghofe@22259
   249
haftmann@22422
   250
lemma member2_Int [pred_set_conv]: "inf (member2 R) (member2 S) = member2 (R Int S)"
haftmann@22422
   251
  by (simp add: expand_fun_eq inf_fun_eq inf_bool_eq)
berghofe@22259
   252
haftmann@22422
   253
lemma inf1_iff [simp]: "inf A B x \<longleftrightarrow> A x \<and> B x"
haftmann@22422
   254
  by (simp add: inf_fun_eq inf_bool_eq)
berghofe@22259
   255
haftmann@22422
   256
lemma inf2_iff [simp]: "inf A B x y \<longleftrightarrow> A x y \<and> B x y"
haftmann@22422
   257
  by (simp add: inf_fun_eq inf_bool_eq)
berghofe@22259
   258
haftmann@22422
   259
lemma inf1I [intro!]: "A x ==> B x ==> inf A B x"
berghofe@22259
   260
  by simp
berghofe@22259
   261
haftmann@22422
   262
lemma inf2I [intro!]: "A x y ==> B x y ==> inf A B x y"
berghofe@22259
   263
  by simp
berghofe@22259
   264
haftmann@22422
   265
lemma inf1D1: "inf A B x ==> A x"
berghofe@22259
   266
  by simp
berghofe@22259
   267
haftmann@22422
   268
lemma inf2D1: "inf A B x y ==> A x y"
berghofe@22259
   269
  by simp
berghofe@22259
   270
haftmann@22422
   271
lemma inf1D2: "inf A B x ==> B x"
berghofe@22259
   272
  by simp
berghofe@22259
   273
haftmann@22422
   274
lemma inf2D2: "inf A B x y ==> B x y"
berghofe@22259
   275
  by simp
berghofe@22259
   276
haftmann@22422
   277
lemma inf1E [elim!]: "inf A B x ==> (A x ==> B x ==> P) ==> P"
berghofe@22259
   278
  by simp
berghofe@22259
   279
haftmann@22422
   280
lemma inf2E [elim!]: "inf A B x y ==> (A x y ==> B x y ==> P) ==> P"
berghofe@22259
   281
  by simp
berghofe@22259
   282
berghofe@22259
   283
berghofe@22259
   284
subsubsection {* Unions of families *}
berghofe@22259
   285
berghofe@22259
   286
lemma member_SUP: "(SUP i. member (r i)) = member (UN i. r i)"
berghofe@22430
   287
  by (simp add: SUPR_def Sup_fun_eq Sup_bool_eq expand_fun_eq) blast
berghofe@22259
   288
berghofe@22259
   289
lemma member2_SUP: "(SUP i. member2 (r i)) = member2 (UN i. r i)"
berghofe@22430
   290
  by (simp add: SUPR_def Sup_fun_eq Sup_bool_eq expand_fun_eq) blast
berghofe@22259
   291
berghofe@22430
   292
lemma SUP1_iff [simp]: "(SUP x:A. B x) b = (EX x:A. B x b)"
berghofe@22430
   293
  by (simp add: SUPR_def Sup_fun_eq Sup_bool_eq) blast
berghofe@22430
   294
berghofe@22430
   295
lemma SUP2_iff [simp]: "(SUP x:A. B x) b c = (EX x:A. B x b c)"
berghofe@22430
   296
  by (simp add: SUPR_def Sup_fun_eq Sup_bool_eq) blast
berghofe@22259
   297
berghofe@22430
   298
lemma SUP1_I [intro]: "a : A ==> B a b ==> (SUP x:A. B x) b"
berghofe@22430
   299
  by auto
berghofe@22259
   300
berghofe@22430
   301
lemma SUP2_I [intro]: "a : A ==> B a b c ==> (SUP x:A. B x) b c"
berghofe@22430
   302
  by auto
berghofe@22430
   303
berghofe@22430
   304
lemma SUP1_E [elim!]: "(SUP x:A. B x) b ==> (!!x. x : A ==> B x b ==> R) ==> R"
berghofe@22430
   305
  by auto
berghofe@22430
   306
berghofe@22430
   307
lemma SUP2_E [elim!]: "(SUP x:A. B x) b c ==> (!!x. x : A ==> B x b c ==> R) ==> R"
berghofe@22259
   308
  by auto
berghofe@22259
   309
berghofe@22430
   310
berghofe@22430
   311
subsubsection {* Intersections of families *}
berghofe@22430
   312
berghofe@22430
   313
lemma member_INF: "(INF i. member (r i)) = member (INT i. r i)"
berghofe@22430
   314
  by (simp add: INFI_def Inf_fun_def Inf_bool_def expand_fun_eq) blast
berghofe@22430
   315
berghofe@22430
   316
lemma member2_INF: "(INF i. member2 (r i)) = member2 (INT i. r i)"
berghofe@22430
   317
  by (simp add: INFI_def Inf_fun_def Inf_bool_def expand_fun_eq) blast
berghofe@22430
   318
berghofe@22430
   319
lemma INF1_iff [simp]: "(INF x:A. B x) b = (ALL x:A. B x b)"
berghofe@22430
   320
  by (simp add: INFI_def Inf_fun_def Inf_bool_def) blast
berghofe@22430
   321
berghofe@22430
   322
lemma INF2_iff [simp]: "(INF x:A. B x) b c = (ALL x:A. B x b c)"
berghofe@22430
   323
  by (simp add: INFI_def Inf_fun_def Inf_bool_def) blast
berghofe@22430
   324
berghofe@22430
   325
lemma INF1_I [intro!]: "(!!x. x : A ==> B x b) ==> (INF x:A. B x) b"
berghofe@22259
   326
  by auto
berghofe@22259
   327
berghofe@22430
   328
lemma INF2_I [intro!]: "(!!x. x : A ==> B x b c) ==> (INF x:A. B x) b c"
berghofe@22430
   329
  by auto
berghofe@22430
   330
berghofe@22430
   331
lemma INF1_D [elim]: "(INF x:A. B x) b ==> a : A ==> B a b"
berghofe@22430
   332
  by auto
berghofe@22259
   333
berghofe@22430
   334
lemma INF2_D [elim]: "(INF x:A. B x) b c ==> a : A ==> B a b c"
berghofe@22430
   335
  by auto
berghofe@22430
   336
berghofe@22430
   337
lemma INF1_E [elim]: "(INF x:A. B x) b ==> (B a b ==> R) ==> (a ~: A ==> R) ==> R"
berghofe@22430
   338
  by auto
berghofe@22430
   339
berghofe@22430
   340
lemma INF2_E [elim]: "(INF x:A. B x) b c ==> (B a b c ==> R) ==> (a ~: A ==> R) ==> R"
berghofe@22430
   341
  by auto
berghofe@22259
   342
berghofe@22259
   343
berghofe@22259
   344
subsection {* Composition of two relations *}
berghofe@22259
   345
berghofe@22259
   346
inductive2
berghofe@22259
   347
  pred_comp  :: "['b => 'c => bool, 'a => 'b => bool] => 'a => 'c => bool"
berghofe@22259
   348
    (infixr "OO" 75)
berghofe@22259
   349
  for r :: "'b => 'c => bool" and s :: "'a => 'b => bool"
berghofe@22259
   350
where
berghofe@22259
   351
  pred_compI [intro]: "s a b ==> r b c ==> (r OO s) a c"
berghofe@22259
   352
berghofe@22259
   353
inductive_cases2 pred_compE [elim!]: "(r OO s) a c"
berghofe@22259
   354
berghofe@22259
   355
lemma pred_comp_rel_comp_eq [pred_set_conv]:
berghofe@22259
   356
  "(member2 r OO member2 s) = member2 (r O s)"
berghofe@22259
   357
  by (auto simp add: expand_fun_eq elim: pred_compE)
berghofe@22259
   358
berghofe@22259
   359
berghofe@22259
   360
subsection {* Converse *}
berghofe@22259
   361
berghofe@22259
   362
inductive2
berghofe@22259
   363
  conversep :: "('a => 'b => bool) => 'b => 'a => bool"
berghofe@22259
   364
    ("(_^--1)" [1000] 1000)
berghofe@22259
   365
  for r :: "'a => 'b => bool"
berghofe@22259
   366
where
berghofe@22259
   367
  conversepI: "r a b ==> r^--1 b a"
berghofe@22259
   368
berghofe@22259
   369
notation (xsymbols)
berghofe@22259
   370
  conversep  ("(_\<inverse>\<inverse>)" [1000] 1000)
berghofe@22259
   371
berghofe@22259
   372
lemma conversepD:
berghofe@22259
   373
  assumes ab: "r^--1 a b"
berghofe@22259
   374
  shows "r b a" using ab
berghofe@22259
   375
  by cases simp
berghofe@22259
   376
berghofe@22259
   377
lemma conversep_iff [iff]: "r^--1 a b = r b a"
berghofe@22259
   378
  by (iprover intro: conversepI dest: conversepD)
berghofe@22259
   379
berghofe@22259
   380
lemma conversep_converse_eq [pred_set_conv]:
berghofe@22259
   381
  "(member2 r)^--1 = member2 (r^-1)"
berghofe@22259
   382
  by (auto simp add: expand_fun_eq)
berghofe@22259
   383
berghofe@22259
   384
lemma conversep_conversep [simp]: "(r^--1)^--1 = r"
berghofe@22259
   385
  by (iprover intro: order_antisym conversepI dest: conversepD)
berghofe@22259
   386
berghofe@22259
   387
lemma converse_pred_comp: "(r OO s)^--1 = s^--1 OO r^--1"
berghofe@22259
   388
  by (iprover intro: order_antisym conversepI pred_compI
berghofe@22259
   389
    elim: pred_compE dest: conversepD)
berghofe@22259
   390
haftmann@22422
   391
lemma converse_meet: "(inf r s)^--1 = inf r^--1 s^--1"
haftmann@22422
   392
  by (simp add: inf_fun_eq inf_bool_eq)
berghofe@22259
   393
    (iprover intro: conversepI ext dest: conversepD)
berghofe@22259
   394
haftmann@22422
   395
lemma converse_join: "(sup r s)^--1 = sup r^--1 s^--1"
haftmann@22422
   396
  by (simp add: sup_fun_eq sup_bool_eq)
berghofe@22259
   397
    (iprover intro: conversepI ext dest: conversepD)
berghofe@22259
   398
berghofe@22259
   399
lemma conversep_noteq [simp]: "(op ~=)^--1 = op ~="
berghofe@22259
   400
  by (auto simp add: expand_fun_eq)
berghofe@22259
   401
berghofe@22259
   402
lemma conversep_eq [simp]: "(op =)^--1 = op ="
berghofe@22259
   403
  by (auto simp add: expand_fun_eq)
berghofe@22259
   404
berghofe@22259
   405
berghofe@22259
   406
subsection {* Domain *}
berghofe@22259
   407
berghofe@22259
   408
inductive2
berghofe@22259
   409
  DomainP :: "('a => 'b => bool) => 'a => bool"
berghofe@22259
   410
  for r :: "'a => 'b => bool"
berghofe@22259
   411
where
berghofe@22259
   412
  DomainPI [intro]: "r a b ==> DomainP r a"
berghofe@22259
   413
berghofe@22259
   414
inductive_cases2 DomainPE [elim!]: "DomainP r a"
berghofe@22259
   415
berghofe@22259
   416
lemma member2_DomainP [pred_set_conv]: "DomainP (member2 r) = member (Domain r)"
berghofe@22259
   417
  by (blast intro!: Orderings.order_antisym)
berghofe@22259
   418
berghofe@22259
   419
berghofe@22259
   420
subsection {* Range *}
berghofe@22259
   421
berghofe@22259
   422
inductive2
berghofe@22259
   423
  RangeP :: "('a => 'b => bool) => 'b => bool"
berghofe@22259
   424
  for r :: "'a => 'b => bool"
berghofe@22259
   425
where
berghofe@22259
   426
  RangePI [intro]: "r a b ==> RangeP r b"
berghofe@22259
   427
berghofe@22259
   428
inductive_cases2 RangePE [elim!]: "RangeP r b"
berghofe@22259
   429
berghofe@22259
   430
lemma member2_RangeP [pred_set_conv]: "RangeP (member2 r) = member (Range r)"
berghofe@22259
   431
  by (blast intro!: Orderings.order_antisym)
berghofe@22259
   432
berghofe@22259
   433
berghofe@22259
   434
subsection {* Inverse image *}
berghofe@22259
   435
berghofe@22259
   436
definition
berghofe@22259
   437
  inv_imagep :: "('b => 'b => bool) => ('a => 'b) => 'a => 'a => bool" where
berghofe@22259
   438
  "inv_imagep r f == %x y. r (f x) (f y)"
berghofe@22259
   439
berghofe@22259
   440
lemma [pred_set_conv]: "inv_imagep (member2 r) f = member2 (inv_image r f)"
berghofe@22259
   441
  by (simp add: inv_image_def inv_imagep_def)
berghofe@22259
   442
berghofe@22259
   443
lemma in_inv_imagep [simp]: "inv_imagep r f x y = r (f x) (f y)"
berghofe@22259
   444
  by (simp add: inv_imagep_def)
berghofe@22259
   445
berghofe@22259
   446
berghofe@22259
   447
subsection {* Properties of relations - predicate versions *}
berghofe@22259
   448
berghofe@22259
   449
abbreviation antisymP :: "('a => 'a => bool) => bool" where
berghofe@22259
   450
  "antisymP r == antisym (Collect2 r)"
berghofe@22259
   451
berghofe@22259
   452
abbreviation transP :: "('a => 'a => bool) => bool" where
berghofe@22259
   453
  "transP r == trans (Collect2 r)"
berghofe@22259
   454
berghofe@22259
   455
abbreviation single_valuedP :: "('a => 'b => bool) => bool" where
berghofe@22259
   456
  "single_valuedP r == single_valued (Collect2 r)"
berghofe@22259
   457
berghofe@22259
   458
berghofe@22259
   459
subsection {* Bounded quantifiers for predicates *}
berghofe@22259
   460
berghofe@22259
   461
text {*
berghofe@22259
   462
Bounded existential quantifier for predicates (executable).
berghofe@22259
   463
*}
berghofe@22259
   464
berghofe@22259
   465
inductive2 bexp :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
berghofe@22259
   466
  for P :: "'a \<Rightarrow> bool" and Q :: "'a \<Rightarrow> bool"
berghofe@22259
   467
where
berghofe@22259
   468
  bexpI [intro]: "P x \<Longrightarrow> Q x \<Longrightarrow> bexp P Q"
berghofe@22259
   469
berghofe@22259
   470
lemmas bexpE [elim!] = bexp.cases
berghofe@22259
   471
berghofe@22259
   472
syntax
berghofe@22259
   473
  Bexp :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool \<Rightarrow> bool" ("(3\<exists>_\<triangleright>_./ _)" [0, 0, 10] 10)
berghofe@22259
   474
berghofe@22259
   475
translations
berghofe@22259
   476
  "\<exists>x\<triangleright>P. Q" \<rightleftharpoons> "CONST bexp P (\<lambda>x. Q)"
berghofe@22259
   477
berghofe@22259
   478
constdefs
berghofe@22259
   479
  ballp :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
berghofe@22259
   480
  "ballp P Q \<equiv> \<forall>x. P x \<longrightarrow> Q x"
berghofe@22259
   481
berghofe@22259
   482
syntax
berghofe@22259
   483
  Ballp :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool \<Rightarrow> bool" ("(3\<forall>_\<triangleright>_./ _)" [0, 0, 10] 10)
berghofe@22259
   484
berghofe@22259
   485
translations
berghofe@22259
   486
  "\<forall>x\<triangleright>P. Q" \<rightleftharpoons> "CONST ballp P (\<lambda>x. Q)"
berghofe@22259
   487
berghofe@22259
   488
(* To avoid eta-contraction of body: *)
berghofe@22259
   489
print_translation {*
berghofe@22259
   490
let
berghofe@22259
   491
  fun btr' syn [A,Abs abs] =
berghofe@22259
   492
    let val (x,t) = atomic_abs_tr' abs
berghofe@22259
   493
    in Syntax.const syn $ x $ A $ t end
berghofe@22259
   494
in
berghofe@22259
   495
[("ballp", btr' "Ballp"),("bexp", btr' "Bexp")]
berghofe@22259
   496
end
berghofe@22259
   497
*}
berghofe@22259
   498
berghofe@22259
   499
lemma ballpI [intro!]: "(\<And>x. A x \<Longrightarrow> P x) \<Longrightarrow> \<forall>x\<triangleright>A. P x"
berghofe@22259
   500
  by (simp add: ballp_def)
berghofe@22259
   501
berghofe@22259
   502
lemma bspecp [dest?]: "\<forall>x\<triangleright>A. P x \<Longrightarrow> A x \<Longrightarrow> P x"
berghofe@22259
   503
  by (simp add: ballp_def)
berghofe@22259
   504
berghofe@22259
   505
lemma ballpE [elim]: "\<forall>x\<triangleright>A. P x \<Longrightarrow> (P x \<Longrightarrow> Q) \<Longrightarrow> (\<not> A x \<Longrightarrow> Q) \<Longrightarrow> Q"
berghofe@22259
   506
  by (unfold ballp_def) blast
berghofe@22259
   507
berghofe@22259
   508
lemma ballp_not_bexp_eq: "(\<forall>x\<triangleright>P. Q x) = (\<not> (\<exists>x\<triangleright>P. \<not> Q x))"
berghofe@22259
   509
  by (blast dest: bspecp)
berghofe@22259
   510
berghofe@22259
   511
declare ballp_not_bexp_eq [THEN eq_reflection, code unfold]
berghofe@22259
   512
berghofe@22259
   513
end