src/HOL/Predicate.thy
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 26797 a6cb51c314f2
child 30328 ab47f43f7581
permissions -rw-r--r--
added lemmas
     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: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) = (R = S)"
    15   by (simp add: mem_def)
    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 (simp add: expand_fun_eq mem_def)
    19 
    20 lemma pred_subset_eq: "((\<lambda>x. x \<in> R) <= (\<lambda>x. x \<in> S)) = (R <= S)"
    21   by (simp add: mem_def)
    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 predicate1I)
   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 predicate1I)
   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 lemmas Powp_mono [mono] = Pow_mono [to_pred pred_subset_eq]
   306 
   307 
   308 subsection {* Properties of relations - predicate versions *}
   309 
   310 abbreviation antisymP :: "('a => 'a => bool) => bool" where
   311   "antisymP r == antisym {(x, y). r x y}"
   312 
   313 abbreviation transP :: "('a => 'a => bool) => bool" where
   314   "transP r == trans {(x, y). r x y}"
   315 
   316 abbreviation single_valuedP :: "('a => 'b => bool) => bool" where
   317   "single_valuedP r == single_valued {(x, y). r x y}"
   318 
   319 end