src/HOL/Orderings.thy
changeset 16796 140f1e0ea846
parent 16743 21dbff595bf6
child 16861 7446b4be013b
equal deleted inserted replaced
16795:b400b53d8f7d 16796:140f1e0ea846
   266 lemma linorder_antisym_conv2: "(x::'a::linorder) <= y ==> (~ x < y) = (x = y)"
   266 lemma linorder_antisym_conv2: "(x::'a::linorder) <= y ==> (~ x < y) = (x = y)"
   267 by(blast intro:order_antisym dest:linorder_not_less[THEN iffD1])
   267 by(blast intro:order_antisym dest:linorder_not_less[THEN iffD1])
   268 
   268 
   269 lemma linorder_antisym_conv3: "~ (y::'a::linorder) < x ==> (~ x < y) = (x = y)"
   269 lemma linorder_antisym_conv3: "~ (y::'a::linorder) < x ==> (~ x < y) = (x = y)"
   270 by(blast intro:order_antisym dest:linorder_not_less[THEN iffD1])
   270 by(blast intro:order_antisym dest:linorder_not_less[THEN iffD1])
       
   271 
       
   272 text{*Replacing the old Nat.leI*}
       
   273 lemma leI: "~ x < y ==> y <= (x::'a::linorder)"
       
   274   by (simp only: linorder_not_less)
       
   275 
       
   276 lemma leD: "y <= (x::'a::linorder) ==> ~ x < y"
       
   277   by (simp only: linorder_not_less)
       
   278 
       
   279 (*FIXME inappropriate name (or delete altogether)*)
       
   280 lemma not_leE: "~ y <= (x::'a::linorder) ==> x < y"
       
   281   by (simp only: linorder_not_le)
   271 
   282 
   272 use "antisym_setup.ML";
   283 use "antisym_setup.ML";
   273 setup antisym_setup
   284 setup antisym_setup
   274 
   285 
   275 subsection {* Setup of transitivity reasoner as Solver *}
   286 subsection {* Setup of transitivity reasoner as Solver *}