src/HOL/ex/Executable_Relation.thy
author bulwahn
Sun Mar 11 20:18:38 2012 +0100 (2012-03-11)
changeset 46871 9100e6aa9272
parent 46395 f56be74d7f51
child 47097 987cb55cac44
permissions -rw-r--r--
renewing Executable_Relation
     1 theory Executable_Relation
     2 imports Main
     3 begin
     4 
     5 subsection {* Preliminaries on the raw type of relations *}
     6 
     7 definition rel_raw :: "'a set => ('a * 'a) set => ('a * 'a) set"
     8 where
     9   "rel_raw X R = Id_on X Un R"
    10 
    11 lemma member_raw:
    12   "(x, y) : (rel_raw X R) = ((x = y \<and> x : X) \<or> (x, y) : R)"
    13 unfolding rel_raw_def by auto
    14 
    15 lemma Id_raw:
    16   "Id = rel_raw UNIV {}"
    17 unfolding rel_raw_def by auto
    18 
    19 lemma converse_raw:
    20   "converse (rel_raw X R) = rel_raw X (converse R)"
    21 unfolding rel_raw_def by auto
    22 
    23 lemma union_raw:
    24   "(rel_raw X R) Un (rel_raw Y S) = rel_raw (X Un Y) (R Un S)"
    25 unfolding rel_raw_def by auto
    26 
    27 lemma comp_Id_on:
    28   "Id_on X O R = Set.project (%(x, y). x : X) R"
    29 by (auto intro!: rel_compI)
    30 
    31 lemma comp_Id_on':
    32   "R O Id_on X = Set.project (%(x, y). y : X) R"
    33 by auto
    34 
    35 lemma project_Id_on:
    36   "Set.project (%(x, y). x : X) (Id_on Y) = Id_on (X Int Y)"
    37 by auto
    38 
    39 lemma rel_comp_raw:
    40   "(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))"
    41 unfolding rel_raw_def
    42 apply simp
    43 apply (simp add: comp_Id_on)
    44 apply (simp add: project_Id_on)
    45 apply (simp add: comp_Id_on')
    46 apply auto
    47 done
    48 
    49 lemma rtrancl_raw:
    50   "(rel_raw X R)^* = rel_raw UNIV (R^+)"
    51 unfolding rel_raw_def
    52 apply auto
    53 apply (metis Id_on_iff Un_commute iso_tuple_UNIV_I rtrancl_Un_separatorE rtrancl_eq_or_trancl)
    54 by (metis in_rtrancl_UnI trancl_into_rtrancl)
    55 
    56 lemma Image_raw:
    57   "(rel_raw X R) `` S = (X Int S) Un (R `` S)"
    58 unfolding rel_raw_def by auto
    59 
    60 subsection {* A dedicated type for relations *}
    61 
    62 subsubsection {* Definition of the dedicated type for relations *}
    63 
    64 quotient_type 'a rel = "('a * 'a) set" / "(op =)"
    65 morphisms set_of_rel rel_of_set by (metis identity_equivp)
    66 
    67 lemma [simp]:
    68   "rel_of_set (set_of_rel S) = S"
    69 by (rule Quotient_abs_rep[OF Quotient_rel])
    70 
    71 lemma [simp]:
    72   "set_of_rel (rel_of_set R) = R"
    73 by (rule Quotient_rep_abs[OF Quotient_rel]) (rule refl)
    74 
    75 lemmas rel_raw_of_set_eqI[intro!] = arg_cong[where f="rel_of_set"]
    76 
    77 definition rel :: "'a set => ('a * 'a) set => 'a rel"
    78 where
    79   "rel X R = rel_of_set (rel_raw X R)"
    80 
    81 subsubsection {* Constant definitions on relations *}
    82 
    83 hide_const (open) converse rel_comp rtrancl Image
    84 
    85 quotient_definition member :: "'a * 'a => 'a rel => bool" where
    86   "member" is "Set.member :: 'a * 'a => ('a * 'a) set => bool"
    87 
    88 quotient_definition converse :: "'a rel => 'a rel"
    89 where
    90   "converse" is "Relation.converse :: ('a * 'a) set => ('a * 'a) set"
    91 
    92 quotient_definition union :: "'a rel => 'a rel => 'a rel"
    93 where
    94   "union" is "Set.union :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set"
    95 
    96 quotient_definition rel_comp :: "'a rel => 'a rel => 'a rel"
    97 where
    98   "rel_comp" is "Relation.rel_comp :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set"
    99 
   100 quotient_definition rtrancl :: "'a rel => 'a rel"
   101 where
   102   "rtrancl" is "Transitive_Closure.rtrancl :: ('a * 'a) set => ('a * 'a) set"
   103 
   104 quotient_definition Image :: "'a rel => 'a set => 'a set"
   105 where
   106   "Image" is "Relation.Image :: ('a * 'a) set => 'a set => 'a set"
   107 
   108 subsubsection {* Code generation *}
   109 
   110 code_datatype rel
   111 
   112 lemma [code]:
   113   "member (x, y) (rel X R) = ((x = y \<and> x : X) \<or> (x, y) : R)"
   114 unfolding rel_def member_def
   115 by (simp add: member_raw)
   116 
   117 lemma [code]:
   118   "converse (rel X R) = rel X (R^-1)"
   119 unfolding rel_def converse_def
   120 by (simp add: converse_raw)
   121 
   122 lemma [code]:
   123   "union (rel X R) (rel Y S) = rel (X Un Y) (R Un S)"
   124 unfolding rel_def union_def
   125 by (simp add: union_raw)
   126 
   127 lemma [code]:
   128    "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))"
   129 unfolding rel_def rel_comp_def
   130 by (simp add: rel_comp_raw)
   131 
   132 lemma [code]:
   133   "rtrancl (rel X R) = rel UNIV (R^+)"
   134 unfolding rel_def rtrancl_def
   135 by (simp add: rtrancl_raw)
   136 
   137 lemma [code]:
   138   "Image (rel X R) S = (X Int S) Un (R `` S)"
   139 unfolding rel_def Image_def
   140 by (simp add: Image_raw)
   141 
   142 quickcheck_generator rel constructors: rel
   143 
   144 lemma
   145   "member (x, (y :: nat)) (rtrancl (union R S)) \<Longrightarrow> member (x, y) (union (rtrancl R) (rtrancl S))"
   146 quickcheck[exhaustive, expect = counterexample]
   147 oops
   148 
   149 end