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