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