src/HOL/ex/Executable_Relation.thy
changeset 47433 07f4bf913230
parent 47097 987cb55cac44
child 47435 e1b761c216ac
     1.1 --- a/src/HOL/ex/Executable_Relation.thy	Tue Apr 03 08:55:06 2012 +0200
     1.2 +++ b/src/HOL/ex/Executable_Relation.thy	Tue Apr 03 17:26:30 2012 +0900
     1.3 @@ -27,7 +27,7 @@
     1.4  
     1.5  lemma comp_Id_on:
     1.6    "Id_on X O R = Set.project (%(x, y). x : X) R"
     1.7 -by (auto intro!: rel_compI)
     1.8 +by (auto intro!: relcompI)
     1.9  
    1.10  lemma comp_Id_on':
    1.11    "R O Id_on X = Set.project (%(x, y). y : X) R"
    1.12 @@ -37,7 +37,7 @@
    1.13    "Set.project (%(x, y). x : X) (Id_on Y) = Id_on (X Int Y)"
    1.14  by auto
    1.15  
    1.16 -lemma rel_comp_raw:
    1.17 +lemma relcomp_raw:
    1.18    "(rel_raw X R) O (rel_raw Y S) = rel_raw (X Int Y) (Set.project (%(x, y). y : Y) R Un (Set.project (%(x, y). x : X) S Un R O S))"
    1.19  unfolding rel_raw_def
    1.20  apply simp
    1.21 @@ -79,7 +79,7 @@
    1.22  
    1.23  subsubsection {* Constant definitions on relations *}
    1.24  
    1.25 -hide_const (open) converse rel_comp rtrancl Image
    1.26 +hide_const (open) converse relcomp rtrancl Image
    1.27  
    1.28  quotient_definition member :: "'a * 'a => 'a rel => bool" where
    1.29    "member" is "Set.member :: 'a * 'a => ('a * 'a) set => bool" done
    1.30 @@ -92,9 +92,9 @@
    1.31  where
    1.32    "union" is "Set.union :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set" done
    1.33  
    1.34 -quotient_definition rel_comp :: "'a rel => 'a rel => 'a rel"
    1.35 +quotient_definition relcomp :: "'a rel => 'a rel => 'a rel"
    1.36  where
    1.37 -  "rel_comp" is "Relation.rel_comp :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set" done
    1.38 +  "relcomp" is "Relation.relcomp :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set" done
    1.39  
    1.40  quotient_definition rtrancl :: "'a rel => 'a rel"
    1.41  where
    1.42 @@ -121,8 +121,8 @@
    1.43  by (lifting union_raw)
    1.44  
    1.45  lemma [code]:
    1.46 -   "rel_comp (rel X R) (rel Y S) = rel (X Int Y) (Set.project (%(x, y). y : Y) R Un (Set.project (%(x, y). x : X) S Un R O S))"
    1.47 -by (lifting rel_comp_raw)
    1.48 +   "relcomp (rel X R) (rel Y S) = rel (X Int Y) (Set.project (%(x, y). y : Y) R Un (Set.project (%(x, y). x : X) S Un R O S))"
    1.49 +by (lifting relcomp_raw)
    1.50  
    1.51  lemma [code]:
    1.52    "rtrancl (rel X R) = rel UNIV (R^+)"