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