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