# HG changeset patch
# User Andreas Lochbihler
# Date 1423659785 -3600
# Node ID 22c9e6cf5572c087b69da197cb7d6af102aac4f4
# Parent  d92b74f3f6e372bc3af620e98bd6a84a3e6625ed
add lemmas about flat_ord

diff -r d92b74f3f6e3 -r 22c9e6cf5572 src/HOL/Partial_Function.thy
--- a/src/HOL/Partial_Function.thy	Wed Feb 11 13:58:51 2015 +0100
+++ b/src/HOL/Partial_Function.thy	Wed Feb 11 14:03:05 2015 +0100
@@ -236,6 +236,15 @@
   qed
 qed (auto simp: flat_ord_def)
 
+lemma flat_ordI: "(x \<noteq> a \<Longrightarrow> x = y) \<Longrightarrow> flat_ord a x y"
+by(auto simp add: flat_ord_def)
+
+lemma flat_ord_antisym: "\<lbrakk> flat_ord a x y; flat_ord a y x \<rbrakk> \<Longrightarrow> x = y"
+by(auto simp add: flat_ord_def)
+
+lemma antisymP_flat_ord: "antisymP (flat_ord a)"
+by(rule antisymI)(auto dest: flat_ord_antisym)
+
 interpretation tailrec!:
   partial_function_definitions "flat_ord undefined" "flat_lub undefined"
   where "flat_lub undefined {} \<equiv> undefined"