# HG changeset patch
# User haftmann
# Date 1213101178 -7200
# Node ID 864d29f11c9d8532e06c2c28aa56d658d3ff2dbf
# Parent  889613625e2bab5b1b81d813ab5f4e98e73435e9
slightly tuning of some proofs involving case distinction and induction on natural numbers and similar

diff -r 889613625e2b -r 864d29f11c9d src/HOLCF/FOCUS/Buffer_adm.thy
--- a/src/HOLCF/FOCUS/Buffer_adm.thy	Mon Jun 09 17:39:35 2008 +0200
+++ b/src/HOLCF/FOCUS/Buffer_adm.thy	Tue Jun 10 14:32:58 2008 +0200
@@ -68,7 +68,7 @@
 prefer 2
 apply ( intro strip)
 apply ( drule slen_mono)
-apply ( drule (1) ile_trans)
+apply ( drule (1) order_trans)
 apply (force)+
 done
 
diff -r 889613625e2b -r 864d29f11c9d src/HOLCF/FOCUS/Stream_adm.thy
--- a/src/HOLCF/FOCUS/Stream_adm.thy	Mon Jun 09 17:39:35 2008 +0200
+++ b/src/HOLCF/FOCUS/Stream_adm.thy	Tue Jun 10 14:32:58 2008 +0200
@@ -53,13 +53,10 @@
 apply (drule not_ex [THEN iffD1])
 apply (subst slen_infinite)
 apply (erule thin_rl)
-apply (drule spec)
-apply (unfold linorder_not_less)
-apply (erule ile_iless_trans [THEN Infty_eq [THEN iffD1]])
-apply (simp)
+apply (erule_tac x = j in allE)
+apply auto
 done
 
-
 (* should be without reference to stream length? *)
 lemma flatstream_admI: "[|(!!Y. [| Porder.chain Y; !i. P (Y i); 
  !k. ? j. Fin k < #((Y j)::'a::flat stream)|] ==> P(lub (range Y)))|]==> adm P"
@@ -72,11 +69,7 @@
 
 (* context (theory "Nat_InFinity");*)
 lemma ile_lemma: "Fin (i + j) <= x ==> Fin i <= x"
-apply (rule ile_trans)
-prefer 2
-apply  (assumption)
-apply (simp)
-done
+  by (rule order_trans) auto
 
 lemma stream_monoP2I:
 "!!X. stream_monoP F ==> !i. ? l. !x y. 
@@ -91,7 +84,7 @@
 apply (erule allE, erule all_dupE, drule mp, erule ile_lemma)
 apply (drule_tac P="%x. x" in subst, assumption)
 apply (erule allE, drule mp, rule ile_lemma) back
-apply ( erule ile_trans)
+apply ( erule order_trans)
 apply ( erule slen_mono)
 apply (erule ssubst)
 apply (safe)
@@ -118,7 +111,7 @@
 apply (erule allE, erule exE)
 apply (erule allE, erule allE, drule mp) (* stream_monoP *)
 apply ( drule ileI1)
-apply ( drule ile_trans)
+apply ( drule order_trans)
 apply (  rule ile_iSuc)
 apply ( drule iSuc_ile_mono [THEN iffD1])
 apply ( assumption)