src/HOL/UNITY/ProgressSets.thy
changeset 30198 922f944f03b2
parent 23767 7272a839ccd9
child 32139 e271a64f03ff
     1.1 --- a/src/HOL/UNITY/ProgressSets.thy	Mon Mar 02 08:26:03 2009 +0100
     1.2 +++ b/src/HOL/UNITY/ProgressSets.thy	Mon Mar 02 16:53:55 2009 +0100
     1.3 @@ -344,8 +344,8 @@
     1.4  apply (blast intro: clD cl_in_lattice)
     1.5  done
     1.6  
     1.7 -lemma refl_relcl: "lattice L ==> refl UNIV (relcl L)"
     1.8 -by (simp add: reflI relcl_def subset_cl [THEN subsetD])
     1.9 +lemma refl_relcl: "lattice L ==> refl (relcl L)"
    1.10 +by (simp add: refl_onI relcl_def subset_cl [THEN subsetD])
    1.11  
    1.12  lemma trans_relcl: "lattice L ==> trans (relcl L)"
    1.13  by (blast intro: relcl_trans transI)
    1.14 @@ -362,12 +362,12 @@
    1.15  
    1.16  text{*Equation (4.71) of Meier's thesis.  He gives no proof.*}
    1.17  lemma cl_latticeof:
    1.18 -     "[|refl UNIV r; trans r|] 
    1.19 +     "[|refl r; trans r|] 
    1.20        ==> cl (latticeof r) X = {t. \<exists>s. s\<in>X & (s,t) \<in> r}" 
    1.21  apply (rule equalityI) 
    1.22   apply (rule cl_least) 
    1.23    apply (simp (no_asm_use) add: latticeof_def trans_def, blast)
    1.24 - apply (simp add: latticeof_def refl_def, blast)
    1.25 + apply (simp add: latticeof_def refl_on_def, blast)
    1.26  apply (simp add: latticeof_def, clarify)
    1.27  apply (unfold cl_def, blast) 
    1.28  done
    1.29 @@ -400,7 +400,7 @@
    1.30  done
    1.31  
    1.32  theorem relcl_latticeof_eq:
    1.33 -     "[|refl UNIV r; trans r|] ==> relcl (latticeof r) = r"
    1.34 +     "[|refl r; trans r|] ==> relcl (latticeof r) = r"
    1.35  by (simp add: relcl_def cl_latticeof)
    1.36  
    1.37