# HG changeset patch # User huffman # Date 1288830145 25200 # Node ID a26503ac7c877c8befa8c940139b56ba3d995f52 # Parent f775e6e0dc998c1962ac592c9f2a5d1327c1be6e simplify some proofs diff -r f775e6e0dc99 -r a26503ac7c87 src/HOLCF/Adm.thy --- a/src/HOLCF/Adm.thy Wed Nov 03 17:06:21 2010 -0700 +++ b/src/HOLCF/Adm.thy Wed Nov 03 17:22:25 2010 -0700 @@ -112,25 +112,14 @@ lemma adm_below [simp]: "\cont (\x. u x); cont (\x. v x)\ \ adm (\x. u x \ v x)" -apply (rule admI) -apply (simp add: cont2contlubE) -apply (rule lub_mono) -apply (erule (1) ch2ch_cont) -apply (erule (1) ch2ch_cont) -apply (erule spec) -done +by (simp add: adm_def cont2contlubE lub_mono ch2ch_cont) lemma adm_eq [simp]: "\cont (\x. u x); cont (\x. v x)\ \ adm (\x. u x = v x)" by (simp add: po_eq_conv) lemma adm_subst: "\cont (\x. t x); adm P\ \ adm (\x. P (t x))" -apply (rule admI) -apply (simp add: cont2contlubE) -apply (erule admD) -apply (erule (1) ch2ch_cont) -apply (erule spec) -done +by (simp add: adm_def cont2contlubE ch2ch_cont) lemma adm_not_below [simp]: "cont (\x. t x) \ adm (\x. \ t x \ u)" by (rule admI, simp add: cont2contlubE ch2ch_cont lub_below_iff)