1.1 --- a/src/HOL/ex/Executable_Relation.thy	Fri Mar 23 14:25:31 2012 +0100
     1.2 +++ b/src/HOL/ex/Executable_Relation.thy	Fri Mar 23 14:26:09 2012 +0100
     1.3 @@ -12,6 +12,7 @@
     1.4    "(x, y) : (rel_raw X R) = ((x = y \<and> x : X) \<or> (x, y) : R)"
     1.5  unfolding rel_raw_def by auto
     1.6  
     1.7 +
     1.8  lemma Id_raw:
     1.9    "Id = rel_raw UNIV {}"
    1.10  unfolding rel_raw_def by auto
    1.11 @@ -74,36 +75,34 @@
    1.12  
    1.13  lemmas rel_raw_of_set_eqI[intro!] = arg_cong[where f="rel_of_set"]
    1.14  
    1.15 -definition rel :: "'a set => ('a * 'a) set => 'a rel"
    1.16 -where
    1.17 -  "rel X R = rel_of_set (rel_raw X R)"
    1.18 +quotient_definition rel where "rel :: 'a set => ('a * 'a) set => 'a rel" is rel_raw done
    1.19  
    1.20  subsubsection {* Constant definitions on relations *}
    1.21  
    1.22  hide_const (open) converse rel_comp rtrancl Image
    1.23  
    1.24  quotient_definition member :: "'a * 'a => 'a rel => bool" where
    1.25 -  "member" is "Set.member :: 'a * 'a => ('a * 'a) set => bool"
    1.26 +  "member" is "Set.member :: 'a * 'a => ('a * 'a) set => bool" done
    1.27  
    1.28  quotient_definition converse :: "'a rel => 'a rel"
    1.29  where
    1.30 -  "converse" is "Relation.converse :: ('a * 'a) set => ('a * 'a) set"
    1.31 +  "converse" is "Relation.converse :: ('a * 'a) set => ('a * 'a) set" done
    1.32  
    1.33  quotient_definition union :: "'a rel => 'a rel => 'a rel"
    1.34  where
    1.35 -  "union" is "Set.union :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set"
    1.36 +  "union" is "Set.union :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set" done
    1.37  
    1.38  quotient_definition rel_comp :: "'a rel => 'a rel => 'a rel"
    1.39  where
    1.40 -  "rel_comp" is "Relation.rel_comp :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set"
    1.41 +  "rel_comp" is "Relation.rel_comp :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set" done
    1.42  
    1.43  quotient_definition rtrancl :: "'a rel => 'a rel"
    1.44  where
    1.45 -  "rtrancl" is "Transitive_Closure.rtrancl :: ('a * 'a) set => ('a * 'a) set"
    1.46 +  "rtrancl" is "Transitive_Closure.rtrancl :: ('a * 'a) set => ('a * 'a) set" done
    1.47  
    1.48  quotient_definition Image :: "'a rel => 'a set => 'a set"
    1.49  where
    1.50 -  "Image" is "Relation.Image :: ('a * 'a) set => 'a set => 'a set"
    1.51 +  "Image" is "Relation.Image :: ('a * 'a) set => 'a set => 'a set" done
    1.52  
    1.53  subsubsection {* Code generation *}
    1.54  
    1.55 @@ -111,33 +110,27 @@
    1.56  
    1.57  lemma [code]:
    1.58    "member (x, y) (rel X R) = ((x = y \<and> x : X) \<or> (x, y) : R)"
    1.59 -unfolding rel_def member_def
    1.60 -by (simp add: member_raw)
    1.61 +by (lifting member_raw)
    1.62  
    1.63  lemma [code]:
    1.64    "converse (rel X R) = rel X (R^-1)"
    1.65 -unfolding rel_def converse_def
    1.66 -by (simp add: converse_raw)
    1.67 +by (lifting converse_raw)
    1.68  
    1.69  lemma [code]:
    1.70    "union (rel X R) (rel Y S) = rel (X Un Y) (R Un S)"
    1.71 -unfolding rel_def union_def
    1.72 -by (simp add: union_raw)
    1.73 +by (lifting union_raw)
    1.74  
    1.75  lemma [code]:
    1.76     "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.77 -unfolding rel_def rel_comp_def
    1.78 -by (simp add: rel_comp_raw)
    1.79 +by (lifting rel_comp_raw)
    1.80  
    1.81  lemma [code]:
    1.82    "rtrancl (rel X R) = rel UNIV (R^+)"
    1.83 -unfolding rel_def rtrancl_def
    1.84 -by (simp add: rtrancl_raw)
    1.85 +by (lifting rtrancl_raw)
    1.86  
    1.87  lemma [code]:
    1.88    "Image (rel X R) S = (X Int S) Un (R `` S)"
    1.89 -unfolding rel_def Image_def
    1.90 -by (simp add: Image_raw)
    1.91 +by (lifting Image_raw)
    1.92  
    1.93  quickcheck_generator rel constructors: rel
    1.94