defining and proving Executable_Relation with lift_definition and transfer
authorbulwahn
Tue May 08 14:35:13 2012 +0200 (2012-05-08)
changeset 478942c6454643be6
parent 47893 4cf901b1089a
child 47895 68f5aaf7cdd2
defining and proving Executable_Relation with lift_definition and transfer
src/HOL/ex/Executable_Relation.thy
     1.1 --- a/src/HOL/ex/Executable_Relation.thy	Tue May 08 14:31:03 2012 +0200
     1.2 +++ b/src/HOL/ex/Executable_Relation.thy	Tue May 08 14:35:13 2012 +0200
     1.3 @@ -2,137 +2,65 @@
     1.4  imports Main
     1.5  begin
     1.6  
     1.7 -subsection {* Preliminaries on the raw type of relations *}
     1.8 -
     1.9 -definition rel_raw :: "'a set => ('a * 'a) set => ('a * 'a) set"
    1.10 -where
    1.11 -  "rel_raw X R = Id_on X Un R"
    1.12 -
    1.13 -lemma member_raw:
    1.14 -  "(x, y) : (rel_raw X R) = ((x = y \<and> x : X) \<or> (x, y) : R)"
    1.15 -unfolding rel_raw_def by auto
    1.16 -
    1.17 -
    1.18 -lemma Id_raw:
    1.19 -  "Id = rel_raw UNIV {}"
    1.20 -unfolding rel_raw_def by auto
    1.21 -
    1.22 -lemma converse_raw:
    1.23 -  "converse (rel_raw X R) = rel_raw X (converse R)"
    1.24 -unfolding rel_raw_def by auto
    1.25 -
    1.26 -lemma union_raw:
    1.27 -  "(rel_raw X R) Un (rel_raw Y S) = rel_raw (X Un Y) (R Un S)"
    1.28 -unfolding rel_raw_def by auto
    1.29 -
    1.30 -lemma comp_Id_on:
    1.31 -  "Id_on X O R = Set.project (%(x, y). x : X) R"
    1.32 -by (auto intro!: relcompI)
    1.33 -
    1.34 -lemma comp_Id_on':
    1.35 -  "R O Id_on X = Set.project (%(x, y). y : X) R"
    1.36 -by auto
    1.37 -
    1.38 -lemma project_Id_on:
    1.39 -  "Set.project (%(x, y). x : X) (Id_on Y) = Id_on (X Int Y)"
    1.40 -by auto
    1.41 -
    1.42 -lemma relcomp_raw:
    1.43 -  "(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.44 -unfolding rel_raw_def
    1.45 -apply simp
    1.46 -apply (simp add: comp_Id_on)
    1.47 -apply (simp add: project_Id_on)
    1.48 -apply (simp add: comp_Id_on')
    1.49 -apply auto
    1.50 -done
    1.51 -
    1.52 -lemma rtrancl_raw:
    1.53 -  "(rel_raw X R)^* = rel_raw UNIV (R^+)"
    1.54 -unfolding rel_raw_def
    1.55 -apply auto
    1.56 -apply (metis Id_on_iff Un_commute iso_tuple_UNIV_I rtrancl_Un_separatorE rtrancl_eq_or_trancl)
    1.57 -by (metis in_rtrancl_UnI trancl_into_rtrancl)
    1.58 -
    1.59 -lemma Image_raw:
    1.60 -  "(rel_raw X R) `` S = (X Int S) Un (R `` S)"
    1.61 -unfolding rel_raw_def by auto
    1.62 -
    1.63  subsection {* A dedicated type for relations *}
    1.64  
    1.65  subsubsection {* Definition of the dedicated type for relations *}
    1.66  
    1.67 -quotient_type 'a rel = "('a * 'a) set" / "(op =)"
    1.68 -morphisms set_of_rel rel_of_set by (metis identity_equivp)
    1.69 -
    1.70 -lemma [simp]:
    1.71 -  "rel_of_set (set_of_rel S) = S"
    1.72 -by (rule Quotient3_abs_rep[OF Quotient3_rel])
    1.73 +typedef (open) 'a rel = "UNIV :: (('a * 'a) set) set"
    1.74 +morphisms set_of_rel rel_of_set by simp
    1.75  
    1.76 -lemma [simp]:
    1.77 -  "set_of_rel (rel_of_set R) = R"
    1.78 -by (rule Quotient3_rep_abs[OF Quotient3_rel]) (rule refl)
    1.79 +setup_lifting type_definition_rel
    1.80  
    1.81 -lemmas rel_raw_of_set_eqI[intro!] = arg_cong[where f="rel_of_set"]
    1.82 -
    1.83 -quotient_definition rel where "rel :: 'a set => ('a * 'a) set => 'a rel" is rel_raw done
    1.84 +lift_definition Rel :: "'a set => ('a * 'a) set => 'a rel" is "\<lambda> X R. Id_on X Un R" .
    1.85  
    1.86  subsubsection {* Constant definitions on relations *}
    1.87  
    1.88  hide_const (open) converse relcomp rtrancl Image
    1.89  
    1.90 -quotient_definition member :: "'a * 'a => 'a rel => bool" where
    1.91 -  "member" is "Set.member :: 'a * 'a => ('a * 'a) set => bool" done
    1.92 +lift_definition member :: "'a * 'a => 'a rel => bool" is "Set.member" .
    1.93  
    1.94 -quotient_definition converse :: "'a rel => 'a rel"
    1.95 -where
    1.96 -  "converse" is "Relation.converse :: ('a * 'a) set => ('a * 'a) set" done
    1.97 +lift_definition converse :: "'a rel => 'a rel" is "Relation.converse" .
    1.98  
    1.99 -quotient_definition union :: "'a rel => 'a rel => 'a rel"
   1.100 -where
   1.101 -  "union" is "Set.union :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set" done
   1.102 +lift_definition union :: "'a rel => 'a rel => 'a rel" is "Set.union" .
   1.103  
   1.104 -quotient_definition relcomp :: "'a rel => 'a rel => 'a rel"
   1.105 -where
   1.106 -  "relcomp" is "Relation.relcomp :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set" done
   1.107 +lift_definition relcomp :: "'a rel => 'a rel => 'a rel" is "Relation.relcomp" .
   1.108  
   1.109 -quotient_definition rtrancl :: "'a rel => 'a rel"
   1.110 -where
   1.111 -  "rtrancl" is "Transitive_Closure.rtrancl :: ('a * 'a) set => ('a * 'a) set" done
   1.112 +lift_definition rtrancl :: "'a rel => 'a rel" is "Transitive_Closure.rtrancl" .
   1.113  
   1.114 -quotient_definition Image :: "'a rel => 'a set => 'a set"
   1.115 -where
   1.116 -  "Image" is "Relation.Image :: ('a * 'a) set => 'a set => 'a set" done
   1.117 +lift_definition Image :: "'a rel => 'a set => 'a set" is "Relation.Image" .
   1.118  
   1.119  subsubsection {* Code generation *}
   1.120  
   1.121 -code_datatype rel
   1.122 +code_datatype Rel
   1.123 +
   1.124 +lemma [code]:
   1.125 +  "member (x, y) (Rel X R) = ((x = y \<and> x : X) \<or> (x, y) : R)"
   1.126 +by transfer auto
   1.127  
   1.128  lemma [code]:
   1.129 -  "member (x, y) (rel X R) = ((x = y \<and> x : X) \<or> (x, y) : R)"
   1.130 -by (lifting member_raw)
   1.131 +  "converse (Rel X R) = Rel X (R^-1)"
   1.132 +by transfer auto
   1.133  
   1.134  lemma [code]:
   1.135 -  "converse (rel X R) = rel X (R^-1)"
   1.136 -by (lifting converse_raw)
   1.137 +  "union (Rel X R) (Rel Y S) = Rel (X Un Y) (R Un S)"
   1.138 +by transfer auto
   1.139  
   1.140  lemma [code]:
   1.141 -  "union (rel X R) (rel Y S) = rel (X Un Y) (R Un S)"
   1.142 -by (lifting union_raw)
   1.143 -
   1.144 -lemma [code]:
   1.145 -   "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.146 -by (lifting relcomp_raw)
   1.147 +   "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.148 +by transfer (auto simp add: Id_on_eqI relcomp.simps)
   1.149  
   1.150  lemma [code]:
   1.151 -  "rtrancl (rel X R) = rel UNIV (R^+)"
   1.152 -by (lifting rtrancl_raw)
   1.153 +  "rtrancl (Rel X R) = Rel UNIV (R^+)"
   1.154 +apply transfer
   1.155 +apply auto
   1.156 +apply (metis Id_on_iff Un_commute UNIV_I rtrancl_Un_separatorE rtrancl_eq_or_trancl)
   1.157 +by (metis in_rtrancl_UnI trancl_into_rtrancl)
   1.158  
   1.159  lemma [code]:
   1.160 -  "Image (rel X R) S = (X Int S) Un (R `` S)"
   1.161 -by (lifting Image_raw)
   1.162 +  "Image (Rel X R) S = (X Int S) Un (R `` S)"
   1.163 +by transfer auto
   1.164  
   1.165 -quickcheck_generator rel constructors: rel
   1.166 +quickcheck_generator rel constructors: Rel
   1.167  
   1.168  lemma
   1.169    "member (x, (y :: nat)) (rtrancl (union R S)) \<Longrightarrow> member (x, y) (union (rtrancl R) (rtrancl S))"