src/HOL/Transitive_Closure.thy
changeset 30240 5b25fee0362c
parent 29609 a010aab5bed0
child 30242 aea5d7fa7ef5
     1.1 --- a/src/HOL/Transitive_Closure.thy	Wed Mar 04 10:43:39 2009 +0100
     1.2 +++ b/src/HOL/Transitive_Closure.thy	Wed Mar 04 10:45:52 2009 +0100
     1.3 @@ -64,8 +64,8 @@
     1.4  
     1.5  subsection {* Reflexive closure *}
     1.6  
     1.7 -lemma reflexive_reflcl[simp]: "reflexive(r^=)"
     1.8 -by(simp add:refl_def)
     1.9 +lemma refl_reflcl[simp]: "refl(r^=)"
    1.10 +by(simp add:refl_on_def)
    1.11  
    1.12  lemma antisym_reflcl[simp]: "antisym(r^=) = antisym r"
    1.13  by(simp add:antisym_def)
    1.14 @@ -118,8 +118,8 @@
    1.15    rtrancl_induct[of "(ax,ay)" "(bx,by)", split_format (complete),
    1.16                   consumes 1, case_names refl step]
    1.17  
    1.18 -lemma reflexive_rtrancl: "reflexive (r^*)"
    1.19 -  by (unfold refl_def) fast
    1.20 +lemma refl_rtrancl: "refl (r^*)"
    1.21 +by (unfold refl_on_def) fast
    1.22  
    1.23  text {* Transitivity of transitive closure. *}
    1.24  lemma trans_rtrancl: "trans (r^*)"
    1.25 @@ -646,7 +646,7 @@
    1.26      val trancl_rtrancl_trancl = @{thm trancl_rtrancl_trancl};
    1.27      val rtrancl_trans = @{thm rtrancl_trans};
    1.28  
    1.29 -  fun decomp (Trueprop $ t) =
    1.30 +  fun decomp (@{const Trueprop} $ t) =
    1.31      let fun dec (Const ("op :", _) $ (Const ("Pair", _) $ a $ b) $ rel ) =
    1.32          let fun decr (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*")
    1.33                | decr (Const ("Transitive_Closure.trancl", _ ) $ r)  = (r,"r+")
    1.34 @@ -654,7 +654,8 @@
    1.35              val (rel,r) = decr (Envir.beta_eta_contract rel);
    1.36          in SOME (a,b,rel,r) end
    1.37        | dec _ =  NONE
    1.38 -    in dec t end;
    1.39 +    in dec t end
    1.40 +    | decomp _ = NONE;
    1.41  
    1.42    end);
    1.43  
    1.44 @@ -669,7 +670,7 @@
    1.45      val trancl_rtrancl_trancl = @{thm tranclp_rtranclp_tranclp};
    1.46      val rtrancl_trans = @{thm rtranclp_trans};
    1.47  
    1.48 -  fun decomp (Trueprop $ t) =
    1.49 +  fun decomp (@{const Trueprop} $ t) =
    1.50      let fun dec (rel $ a $ b) =
    1.51          let fun decr (Const ("Transitive_Closure.rtranclp", _ ) $ r) = (r,"r*")
    1.52                | decr (Const ("Transitive_Closure.tranclp", _ ) $ r)  = (r,"r+")
    1.53 @@ -677,7 +678,8 @@
    1.54              val (rel,r) = decr rel;
    1.55          in SOME (a, b, rel, r) end
    1.56        | dec _ =  NONE
    1.57 -    in dec t end;
    1.58 +    in dec t end
    1.59 +    | decomp _ = NONE;
    1.60  
    1.61    end);
    1.62  *}