# HG changeset patch # User huffman # Date 1131139660 -3600 # Node ID e5b23b85e9324b4bbb14535d61925116d35435d6 # Parent 577d57e51f899f692d63c72dd331abd44eacf16e cleaned up diff -r 577d57e51f89 -r e5b23b85e932 src/HOLCF/Cont.thy --- a/src/HOLCF/Cont.thy Fri Nov 04 22:26:09 2005 +0100 +++ b/src/HOLCF/Cont.thy Fri Nov 04 22:27:40 2005 +0100 @@ -92,10 +92,8 @@ lemma monocontlub2cont: "\monofun f; contlub f\ \ cont f" apply (rule contI) apply (rule thelubE) -apply (erule ch2ch_monofun) -apply assumption -apply (erule contlubE [symmetric]) -apply assumption +apply (erule (1) ch2ch_monofun) +apply (erule (1) contlubE [symmetric]) done text {* first a lemma about binary chains *} @@ -115,7 +113,7 @@ lemma cont2mono: "cont f \ monofun f" apply (rule monofunI) -apply (drule binchain_cont, assumption) +apply (drule (1) binchain_cont) apply (drule_tac i=0 in is_ub_lub) apply simp done @@ -128,8 +126,7 @@ lemma cont2contlub: "cont f \ contlub f" apply (rule contlubI) apply (rule thelubI [symmetric]) -apply (erule contE) -apply assumption +apply (erule (1) contE) done lemmas cont2contlubE = cont2contlub [THEN contlubE] @@ -190,8 +187,7 @@ apply (rule monocontlub2cont) apply (erule monofun_lub_fun) apply (simp add: cont2mono) -apply (erule contlub_lub_fun) -apply assumption +apply (erule (1) contlub_lub_fun) done lemma cont2cont_lub: @@ -231,18 +227,16 @@ done lemma cont2cont_lambda: "(\y. cont (\x. f x y)) \ cont (\x. (\y. f x y))" -apply (rule cont2cont_CF1L_rev) -apply simp -done +by (rule cont2cont_CF1L_rev, simp) text {* What D.A.Schmidt calls continuity of abstraction; never used here *} lemma contlub_abstraction: "\chain Y; \y. cont (\x.(c::'a::cpo\'b::type\'c::cpo) x y)\ \ (\y. \i. c (Y i) y) = (\i. (\y. c (Y i) y))" +apply (drule cont2cont_CF1L_rev) apply (rule thelub_fun [symmetric]) -apply (rule ch2ch_cont) -apply (erule (1) cont2cont_CF1L_rev) +apply (erule (1) ch2ch_cont) done lemma mono2mono_app: diff -r 577d57e51f89 -r e5b23b85e932 src/HOLCF/Porder.thy --- a/src/HOLCF/Porder.thy Fri Nov 04 22:26:09 2005 +0100 +++ b/src/HOLCF/Porder.thy Fri Nov 04 22:27:40 2005 +0100 @@ -38,10 +38,7 @@ by simp lemma box_less: "\(a::'a::po) \ b; c \ a; b \ d\ \ c \ d" -apply (erule trans_less) -apply (erule trans_less) -apply assumption -done +by (rule trans_less [OF trans_less]) lemma po_eq_conv: "((x::'a::po) = y) = (x \ y \ y \ x)" by (fast elim!: antisym_less_inverse intro!: antisym_less) @@ -128,11 +125,7 @@ done lemma thelubI: "M <<| l \ lub M = l" -apply (rule unique_lub) -apply (rule lubI) -apply assumption -apply assumption -done +by (rule unique_lub [OF lubI]) lemma lub_singleton [simp]: "lub {x} = x" by (simp add: thelubI is_lub_def is_ub_def)