Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added lemmas antisym_if_asym and antisymp_if_asymp
authordesharna
Sun, 09 Oct 2022 16:24:50 +0200
changeset 76254 7ae89ee919a7
parent 76253 08f555c6f3b5
child 76255 b3ff4f171eda
added lemmas antisym_if_asym and antisymp_if_asymp
NEWS file | annotate | diff | comparison | revisions
src/HOL/Relation.thy file | annotate | diff | comparison | revisions 
--- a/NEWS	Sun Oct 09 16:10:52 2022 +0200
+++ b/NEWS	Sun Oct 09 16:24:50 2022 +0200
@@ -11,7 +11,9 @@
 
 * Theory "HOL.Relation":
   - Strengthened total_on_singleton. Minor INCOMPATIBILITY.
-  - Added lemma.
+  - Added lemmas.
+      antisym_if_asymp
+      antisymp_if_asymp
       totalp_on_singleton[simp]
 
 
--- a/src/HOL/Relation.thy	Sun Oct 09 16:10:52 2022 +0200
+++ b/src/HOL/Relation.thy	Sun Oct 09 16:24:50 2022 +0200
@@ -423,6 +423,12 @@
   "antisym {x}"
   by (blast intro: antisymI)
 
+lemma antisym_if_asym: "asym r \<Longrightarrow> antisym r"
+  by (auto intro: antisymI elim: asym.cases)
+
+lemma antisymp_if_asymp: "asymp R \<Longrightarrow> antisymp R"
+  by (rule antisym_if_asym[to_pred])
+
 
 subsubsection \<open>Transitivity\<close>
isabelle