src/HOL/Transitive_Closure.thy
changeset 22422 ee19cdb07528
parent 22262 96ba62dff413
child 23743 52fbc991039f
     1.1 --- a/src/HOL/Transitive_Closure.thy	Tue Mar 06 16:40:32 2007 +0100
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Fri Mar 09 08:45:50 2007 +0100
     1.3 @@ -43,7 +43,7 @@
     1.4  
     1.5  abbreviation
     1.6    reflcl :: "('a => 'a => bool) => 'a => 'a => bool"  ("(_^==)" [1000] 1000) where
     1.7 -  "r^== == join r op ="
     1.8 +  "r^== == sup r op ="
     1.9  
    1.10  abbreviation
    1.11    reflcl_set :: "('a \<times> 'a) set => ('a \<times> 'a) set"  ("(_^=)" [1000] 999) where
    1.12 @@ -71,7 +71,7 @@
    1.13  lemma rtrancl_set_eq [pred_set_conv]: "(member2 r)^** = member2 (r^*)"
    1.14    by (simp add: rtrancl_set_def)
    1.15  
    1.16 -lemma reflcl_set_eq [pred_set_conv]: "(join (member2 r) op =) = member2 (r Un Id)"
    1.17 +lemma reflcl_set_eq [pred_set_conv]: "(sup (member2 r) op =) = member2 (r Un Id)"
    1.18    by (simp add: expand_fun_eq)
    1.19  
    1.20  lemmas rtrancl_refl [intro!, Pure.intro!, simp] = rtrancl_refl [to_set]
    1.21 @@ -190,7 +190,7 @@
    1.22  
    1.23  lemmas rtrancl_subset = rtrancl_subset' [to_set]
    1.24  
    1.25 -lemma rtrancl_Un_rtrancl': "(join (R^**) (S^**))^** = (join R S)^**"
    1.26 +lemma rtrancl_Un_rtrancl': "(sup (R^**) (S^**))^** = (sup R S)^**"
    1.27    by (blast intro!: rtrancl_subset' intro: rtrancl_mono' [THEN predicate2D])
    1.28  
    1.29  lemmas rtrancl_Un_rtrancl = rtrancl_Un_rtrancl' [to_set]
    1.30 @@ -208,7 +208,7 @@
    1.31    apply (blast intro!: r_into_rtrancl)
    1.32    done
    1.33  
    1.34 -lemma rtrancl_r_diff_Id': "(meet r op ~=)^** = r^**"
    1.35 +lemma rtrancl_r_diff_Id': "(inf r op ~=)^** = r^**"
    1.36    apply (rule sym)
    1.37    apply (rule rtrancl_subset')
    1.38    apply blast+