Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Predicate.thy
changeset 41550 efa734d9b221
parent 41505 6d19301074cf
child 44007 b5e7594061ce
equal deleted inserted replaced
41549:2c65ad10bec8 41550:efa734d9b221 
    91 
    91 
    92 
    92 
    93 subsubsection {* Top and bottom elements *}
 
    93 subsubsection {* Top and bottom elements *}
 
    94 
    94 
    95 lemma bot1E [no_atp, elim!]: "bot x \<Longrightarrow> P"
 
    95 lemma bot1E [no_atp, elim!]: "bot x \<Longrightarrow> P"
 
    96   by (simp add: bot_fun_def bot_bool_def)
 
    96   by (simp add: bot_fun_def)
 
    97 
    97 
    98 lemma bot2E [elim!]: "bot x y \<Longrightarrow> P"
 
    98 lemma bot2E [elim!]: "bot x y \<Longrightarrow> P"
 
    99   by (simp add: bot_fun_def bot_bool_def)
 
    99   by (simp add: bot_fun_def)
 
   100 
   100 
   101 lemma bot_empty_eq: "bot = (\<lambda>x. x \<in> {})"
 
   101 lemma bot_empty_eq: "bot = (\<lambda>x. x \<in> {})"
 
   102   by (auto simp add: fun_eq_iff)
 
   102   by (auto simp add: fun_eq_iff)
 
   103 
   103 
   104 lemma bot_empty_eq2: "bot = (\<lambda>x y. (x, y) \<in> {})"
 
   104 lemma bot_empty_eq2: "bot = (\<lambda>x y. (x, y) \<in> {})"
 
   105   by (auto simp add: fun_eq_iff)
 
   105   by (auto simp add: fun_eq_iff)
 
   106 
   106 
   107 lemma top1I [intro!]: "top x"
 
   107 lemma top1I [intro!]: "top x"
 
   108   by (simp add: top_fun_def top_bool_def)
 
   108   by (simp add: top_fun_def)
 
   109 
   109 
   110 lemma top2I [intro!]: "top x y"
 
   110 lemma top2I [intro!]: "top x y"
 
   111   by (simp add: top_fun_def top_bool_def)
 
   111   by (simp add: top_fun_def)
 
   112 
   112 
   113 
   113 
   114 subsubsection {* Binary intersection *}
 
   114 subsubsection {* Binary intersection *}
 
   115 
   115 
   116 lemma inf1I [intro!]: "A x ==> B x ==> inf A B x"
 
   116 lemma inf1I [intro!]: "A x ==> B x ==> inf A B x"
 
   117   by (simp add: inf_fun_def inf_bool_def)
 
   117   by (simp add: inf_fun_def)
 
   118 
   118 
   119 lemma inf2I [intro!]: "A x y ==> B x y ==> inf A B x y"
 
   119 lemma inf2I [intro!]: "A x y ==> B x y ==> inf A B x y"
 
   120   by (simp add: inf_fun_def inf_bool_def)
 
   120   by (simp add: inf_fun_def)
 
   121 
   121 
   122 lemma inf1E [elim!]: "inf A B x ==> (A x ==> B x ==> P) ==> P"
 
   122 lemma inf1E [elim!]: "inf A B x ==> (A x ==> B x ==> P) ==> P"
 
   123   by (simp add: inf_fun_def inf_bool_def)
 
   123   by (simp add: inf_fun_def)
 
   124 
   124 
   125 lemma inf2E [elim!]: "inf A B x y ==> (A x y ==> B x y ==> P) ==> P"
 
   125 lemma inf2E [elim!]: "inf A B x y ==> (A x y ==> B x y ==> P) ==> P"
 
   126   by (simp add: inf_fun_def inf_bool_def)
 
   126   by (simp add: inf_fun_def)
 
   127 
   127 
   128 lemma inf1D1: "inf A B x ==> A x"
 
   128 lemma inf1D1: "inf A B x ==> A x"
 
   129   by (simp add: inf_fun_def inf_bool_def)
 
   129   by (simp add: inf_fun_def)
 
   130 
   130 
   131 lemma inf2D1: "inf A B x y ==> A x y"
 
   131 lemma inf2D1: "inf A B x y ==> A x y"
 
   132   by (simp add: inf_fun_def inf_bool_def)
 
   132   by (simp add: inf_fun_def)
 
   133 
   133 
   134 lemma inf1D2: "inf A B x ==> B x"
 
   134 lemma inf1D2: "inf A B x ==> B x"
 
   135   by (simp add: inf_fun_def inf_bool_def)
 
   135   by (simp add: inf_fun_def)
 
   136 
   136 
   137 lemma inf2D2: "inf A B x y ==> B x y"
 
   137 lemma inf2D2: "inf A B x y ==> B x y"
 
   138   by (simp add: inf_fun_def inf_bool_def)
 
   138   by (simp add: inf_fun_def)
 
   139 
   139 
   140 lemma inf_Int_eq: "inf (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
 
   140 lemma inf_Int_eq: "inf (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<inter> S)"
 
   141   by (simp add: inf_fun_def inf_bool_def mem_def)
 
   141   by (simp add: inf_fun_def mem_def)
 
   142 
   142 
   143 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)"
 
   143 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)"
 
   144   by (simp add: inf_fun_def inf_bool_def mem_def)
 
   144   by (simp add: inf_fun_def mem_def)
 
   145 
   145 
   146 
   146 
   147 subsubsection {* Binary union *}
 
   147 subsubsection {* Binary union *}
 
   148 
   148 
   149 lemma sup1I1 [elim?]: "A x \<Longrightarrow> sup A B x"
 
   149 lemma sup1I1 [elim?]: "A x \<Longrightarrow> sup A B x"
 
   150   by (simp add: sup_fun_def sup_bool_def)
 
   150   by (simp add: sup_fun_def)
 
   151 
   151 
   152 lemma sup2I1 [elim?]: "A x y \<Longrightarrow> sup A B x y"
 
   152 lemma sup2I1 [elim?]: "A x y \<Longrightarrow> sup A B x y"
 
   153   by (simp add: sup_fun_def sup_bool_def)
 
   153   by (simp add: sup_fun_def)
 
   154 
   154 
   155 lemma sup1I2 [elim?]: "B x \<Longrightarrow> sup A B x"
 
   155 lemma sup1I2 [elim?]: "B x \<Longrightarrow> sup A B x"
 
   156   by (simp add: sup_fun_def sup_bool_def)
 
   156   by (simp add: sup_fun_def)
 
   157 
   157 
   158 lemma sup2I2 [elim?]: "B x y \<Longrightarrow> sup A B x y"
 
   158 lemma sup2I2 [elim?]: "B x y \<Longrightarrow> sup A B x y"
 
   159   by (simp add: sup_fun_def sup_bool_def)
 
   159   by (simp add: sup_fun_def)
 
   160 
   160 
   161 lemma sup1E [elim!]: "sup A B x ==> (A x ==> P) ==> (B x ==> P) ==> P"
 
   161 lemma sup1E [elim!]: "sup A B x ==> (A x ==> P) ==> (B x ==> P) ==> P"
 
   162   by (simp add: sup_fun_def sup_bool_def) iprover
 
   162   by (simp add: sup_fun_def) iprover
 
   163 
   163 
   164 lemma sup2E [elim!]: "sup A B x y ==> (A x y ==> P) ==> (B x y ==> P) ==> P"
 
   164 lemma sup2E [elim!]: "sup A B x y ==> (A x y ==> P) ==> (B x y ==> P) ==> P"
 
   165   by (simp add: sup_fun_def sup_bool_def) iprover
 
   165   by (simp add: sup_fun_def) iprover
 
   166 
   166 
   167 text {*
 
   167 text {*
 
   168   \medskip Classical introduction rule: no commitment to @{text A} vs
 
   168   \medskip Classical introduction rule: no commitment to @{text A} vs
 
   169   @{text B}.
 
   169   @{text B}.
 
   170 *}
 
   170 *}
 
   171 
   171 
   172 lemma sup1CI [intro!]: "(~ B x ==> A x) ==> sup A B x"
 
   172 lemma sup1CI [intro!]: "(~ B x ==> A x) ==> sup A B x"
 
   173   by (auto simp add: sup_fun_def sup_bool_def)
 
   173   by (auto simp add: sup_fun_def)
 
   174 
   174 
   175 lemma sup2CI [intro!]: "(~ B x y ==> A x y) ==> sup A B x y"
 
   175 lemma sup2CI [intro!]: "(~ B x y ==> A x y) ==> sup A B x y"
 
   176   by (auto simp add: sup_fun_def sup_bool_def)
 
   176   by (auto simp add: sup_fun_def)
 
   177 
   177 
   178 lemma sup_Un_eq: "sup (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)"
 
   178 lemma sup_Un_eq: "sup (\<lambda>x. x \<in> R) (\<lambda>x. x \<in> S) = (\<lambda>x. x \<in> R \<union> S)"
 
   179   by (simp add: sup_fun_def sup_bool_def mem_def)
 
   179   by (simp add: sup_fun_def mem_def)
 
   180 
   180 
   181 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)"
 
   181 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)"
 
   182   by (simp add: sup_fun_def sup_bool_def mem_def)
 
   182   by (simp add: sup_fun_def mem_def)
 
   183 
   183 
   184 
   184 
   185 subsubsection {* Intersections of families *}
 
   185 subsubsection {* Intersections of families *}
 
   186 
   186 
   187 lemma INF1_iff: "(INF x:A. B x) b = (ALL x:A. B x b)"
 
   187 lemma INF1_iff: "(INF x:A. B x) b = (ALL x:A. B x b)"
 
   255 
   255 
   256 inductive_cases pred_compE [elim!]: "(r OO s) a c"
 
   256 inductive_cases pred_compE [elim!]: "(r OO s) a c"
 
   257 
   257 
   258 lemma pred_comp_rel_comp_eq [pred_set_conv]:
 
   258 lemma pred_comp_rel_comp_eq [pred_set_conv]:
 
   259   "((\<lambda>x y. (x, y) \<in> r) OO (\<lambda>x y. (x, y) \<in> s)) = (\<lambda>x y. (x, y) \<in> r O s)"
 
   259   "((\<lambda>x y. (x, y) \<in> r) OO (\<lambda>x y. (x, y) \<in> s)) = (\<lambda>x y. (x, y) \<in> r O s)"
 
   260   by (auto simp add: fun_eq_iff elim: pred_compE)
 
   260   by (auto simp add: fun_eq_iff)
 
   261 
   261 
   262 
   262 
   263 subsubsection {* Converse *}
 
   263 subsubsection {* Converse *}
 
   264 
   264 
   265 inductive
 
   265 inductive
 
   290 lemma converse_pred_comp: "(r OO s)^--1 = s^--1 OO r^--1"
 
   290 lemma converse_pred_comp: "(r OO s)^--1 = s^--1 OO r^--1"
 
   291   by (iprover intro: order_antisym conversepI pred_compI
 
   291   by (iprover intro: order_antisym conversepI pred_compI
 
   292     elim: pred_compE dest: conversepD)
 
   292     elim: pred_compE dest: conversepD)
 
   293 
   293 
   294 lemma converse_meet: "(inf r s)^--1 = inf r^--1 s^--1"
 
   294 lemma converse_meet: "(inf r s)^--1 = inf r^--1 s^--1"
 
   295   by (simp add: inf_fun_def inf_bool_def)
 
   295   by (simp add: inf_fun_def) (iprover intro: conversepI ext dest: conversepD)
 
   296     (iprover intro: conversepI ext dest: conversepD)
 
       
   297 
   296 
   298 lemma converse_join: "(sup r s)^--1 = sup r^--1 s^--1"
 
   297 lemma converse_join: "(sup r s)^--1 = sup r^--1 s^--1"
 
   299   by (simp add: sup_fun_def sup_bool_def)
 
   298   by (simp add: sup_fun_def) (iprover intro: conversepI ext dest: conversepD)
 
   300     (iprover intro: conversepI ext dest: conversepD)
 
       
   301 
   299 
   302 lemma conversep_noteq [simp]: "(op ~=)^--1 = op ~="
 
   300 lemma conversep_noteq [simp]: "(op ~=)^--1 = op ~="
 
   303   by (auto simp add: fun_eq_iff)
 
   301   by (auto simp add: fun_eq_iff)
 
   304 
   302 
   305 lemma conversep_eq [simp]: "(op =)^--1 = op ="
 
   303 lemma conversep_eq [simp]: "(op =)^--1 = op ="
 
   754     apply (simp add: unit_eq)
 
   752     apply (simp add: unit_eq)
 
   755     apply (rule disjI1)
 
   753     apply (rule disjI1)
 
   756     apply (rule ext)
 
   754     apply (rule ext)
 
   757     apply (simp add: unit_eq)
 
   755     apply (simp add: unit_eq)
 
   758     done
 
   756     done
 
   759   from this prems show ?thesis by blast
 
   757   from this assms show ?thesis by blast
 
   760 qed
 
   758 qed
 
   761 
   759 
   762 lemma unit_pred_cases:
 
   760 lemma unit_pred_cases:
 
   763 assumes "P \<bottom>"
 
   761 assumes "P \<bottom>"
 
   764 assumes "P (single ())"
 
   762 assumes "P (single ())"
isabelle