cleaned up
authorhuffman
Thu Sep 22 19:06:05 2005 +0200 (2005-09-22)
changeset 17585f12d7ac88eb4
parent 17584 6eab0f1cb0fe
child 17586 df8b2f0e462e
cleaned up
src/HOLCF/Fix.thy
src/HOLCF/Up.thy
     1.1 --- a/src/HOLCF/Fix.thy	Thu Sep 22 18:59:41 2005 +0200
     1.2 +++ b/src/HOLCF/Fix.thy	Thu Sep 22 19:06:05 2005 +0200
     1.3 @@ -228,7 +228,7 @@
     1.4  
     1.5  text {* computational induction for weak admissible formulae *}
     1.6  
     1.7 -lemma wfix_ind: "\<lbrakk>admw P; \<forall>n. P (iterate n F UU)\<rbrakk> \<Longrightarrow> P (fix\<cdot>F)"
     1.8 +lemma wfix_ind: "\<lbrakk>admw P; \<forall>n. P (iterate n F \<bottom>)\<rbrakk> \<Longrightarrow> P (fix\<cdot>F)"
     1.9  by (simp add: fix_def2 admw_def)
    1.10  
    1.11  lemma def_wfix_ind:
     2.1 --- a/src/HOLCF/Up.thy	Thu Sep 22 18:59:41 2005 +0200
     2.2 +++ b/src/HOLCF/Up.thy	Thu Sep 22 19:06:05 2005 +0200
     2.3 @@ -130,9 +130,7 @@
     2.4  apply (simp add: expand_fun_eq)
     2.5  apply (erule exE, rename_tac j)
     2.6  apply (rule_tac x="\<lambda>i. THE a. Iup a = Y (i + j)" in exI)
     2.7 -apply (rule conjI)
     2.8  apply (simp add: up_lemma4)
     2.9 -apply (rule conjI)
    2.10  apply (simp add: up_lemma6 [THEN thelubI])
    2.11  apply (rule_tac x=j in exI)
    2.12  apply (simp add: up_lemma3)
    2.13 @@ -143,8 +141,7 @@
    2.14  apply (rule_tac x="Iup (lub (range A))" in exI)
    2.15  apply (erule_tac j1="j" in is_lub_range_shift [THEN iffD1])
    2.16  apply (simp add: is_lub_Iup thelubE)
    2.17 -apply (rule_tac x="Ibottom" in exI)
    2.18 -apply (rule lub_const)
    2.19 +apply (rule exI, rule lub_const)
    2.20  done
    2.21  
    2.22  instance u :: (cpo) cpo
    2.23 @@ -152,7 +149,7 @@
    2.24  
    2.25  subsection {* Type @{typ "'a u"} is pointed *}
    2.26  
    2.27 -lemma least_up: "EX x::'a u. ALL y. x\<sqsubseteq>y"
    2.28 +lemma least_up: "\<exists>x::'a u. \<forall>y. x \<sqsubseteq> y"
    2.29  apply (rule_tac x = "Ibottom" in exI)
    2.30  apply (rule minimal_up [THEN allI])
    2.31  done