src/HOL/ex/Executable_Relation.thy
author nipkow
Fri, 21 Jun 2013 09:00:26 +0200
changeset 52402 c2f30ba4bb98
parent 49834 b27bbb021df1
child 61343 5b5656a63bd6
permissions -rw-r--r--
tuned
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
46395
f56be74d7f51 adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type
bulwahn
parents:
diff changeset
     1
theory Executable_Relation
f56be74d7f51 adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type
bulwahn
parents:
diff changeset
     2
imports Main
f56be74d7f51 adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type
bulwahn
parents:
diff changeset
     3
begin
f56be74d7f51 adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type
bulwahn
parents:
diff changeset
     4
46871
9100e6aa9272 renewing Executable_Relation
bulwahn
parents: 46395
diff changeset
     5
subsection {* A dedicated type for relations *}
9100e6aa9272 renewing Executable_Relation
bulwahn
parents: 46395
diff changeset
     6
9100e6aa9272 renewing Executable_Relation
bulwahn
parents: 46395
diff changeset
     7
subsubsection {* Definition of the dedicated type for relations *}
46395
f56be74d7f51 adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type
bulwahn
parents:
diff changeset
     8
49834
b27bbb021df1 discontinued obsolete typedef (open) syntax;
wenzelm
parents: 49757
diff changeset
     9
typedef 'a rel = "UNIV :: (('a * 'a) set) set"
47894
2c6454643be6 defining and proving Executable_Relation with lift_definition and transfer
bulwahn
parents: 47435
diff changeset
    10
morphisms set_of_rel rel_of_set by simp
46395
f56be74d7f51 adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type
bulwahn
parents:
diff changeset
    11
47894
2c6454643be6 defining and proving Executable_Relation with lift_definition and transfer
bulwahn
parents: 47435
diff changeset
    12
setup_lifting type_definition_rel
46395
f56be74d7f51 adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type
bulwahn
parents:
diff changeset
    13
47894
2c6454643be6 defining and proving Executable_Relation with lift_definition and transfer
bulwahn
parents: 47435
diff changeset
    14
lift_definition Rel :: "'a set => ('a * 'a) set => 'a rel" is "\<lambda> X R. Id_on X Un R" .
46871
9100e6aa9272 renewing Executable_Relation
bulwahn
parents: 46395
diff changeset
    15
9100e6aa9272 renewing Executable_Relation
bulwahn
parents: 46395
diff changeset
    16
subsubsection {* Constant definitions on relations *}
9100e6aa9272 renewing Executable_Relation
bulwahn
parents: 46395
diff changeset
    17
47433
07f4bf913230 renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
griff
parents: 47097
diff changeset
    18
hide_const (open) converse relcomp rtrancl Image
46395
f56be74d7f51 adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type
bulwahn
parents:
diff changeset
    19
47894
2c6454643be6 defining and proving Executable_Relation with lift_definition and transfer
bulwahn
parents: 47435
diff changeset
    20
lift_definition member :: "'a * 'a => 'a rel => bool" is "Set.member" .
46395
f56be74d7f51 adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type
bulwahn
parents:
diff changeset
    21
47894
2c6454643be6 defining and proving Executable_Relation with lift_definition and transfer
bulwahn
parents: 47435
diff changeset
    22
lift_definition converse :: "'a rel => 'a rel" is "Relation.converse" .
46395
f56be74d7f51 adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type
bulwahn
parents:
diff changeset
    23
47894
2c6454643be6 defining and proving Executable_Relation with lift_definition and transfer
bulwahn
parents: 47435
diff changeset
    24
lift_definition union :: "'a rel => 'a rel => 'a rel" is "Set.union" .
46395
f56be74d7f51 adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type
bulwahn
parents:
diff changeset
    25
47894
2c6454643be6 defining and proving Executable_Relation with lift_definition and transfer
bulwahn
parents: 47435
diff changeset
    26
lift_definition relcomp :: "'a rel => 'a rel => 'a rel" is "Relation.relcomp" .
46871
9100e6aa9272 renewing Executable_Relation
bulwahn
parents: 46395
diff changeset
    27
47894
2c6454643be6 defining and proving Executable_Relation with lift_definition and transfer
bulwahn
parents: 47435
diff changeset
    28
lift_definition rtrancl :: "'a rel => 'a rel" is "Transitive_Closure.rtrancl" .
46395
f56be74d7f51 adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type
bulwahn
parents:
diff changeset
    29
47894
2c6454643be6 defining and proving Executable_Relation with lift_definition and transfer
bulwahn
parents: 47435
diff changeset
    30
lift_definition Image :: "'a rel => 'a set => 'a set" is "Relation.Image" .
46871
9100e6aa9272 renewing Executable_Relation
bulwahn
parents: 46395
diff changeset
    31
9100e6aa9272 renewing Executable_Relation
bulwahn
parents: 46395
diff changeset
    32
subsubsection {* Code generation *}
46395
f56be74d7f51 adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type
bulwahn
parents:
diff changeset
    33
47894
2c6454643be6 defining and proving Executable_Relation with lift_definition and transfer
bulwahn
parents: 47435
diff changeset
    34
code_datatype Rel
2c6454643be6 defining and proving Executable_Relation with lift_definition and transfer
bulwahn
parents: 47435
diff changeset
    35
2c6454643be6 defining and proving Executable_Relation with lift_definition and transfer
bulwahn
parents: 47435
diff changeset
    36
lemma [code]:
2c6454643be6 defining and proving Executable_Relation with lift_definition and transfer
bulwahn
parents: 47435
diff changeset
    37
  "member (x, y) (Rel X R) = ((x = y \<and> x : X) \<or> (x, y) : R)"
2c6454643be6 defining and proving Executable_Relation with lift_definition and transfer
bulwahn
parents: 47435
diff changeset
    38
by transfer auto
46395
f56be74d7f51 adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type
bulwahn
parents:
diff changeset
    39
46871
9100e6aa9272 renewing Executable_Relation
bulwahn
parents: 46395
diff changeset
    40
lemma [code]:
47894
2c6454643be6 defining and proving Executable_Relation with lift_definition and transfer
bulwahn
parents: 47435
diff changeset
    41
  "converse (Rel X R) = Rel X (R^-1)"
2c6454643be6 defining and proving Executable_Relation with lift_definition and transfer
bulwahn
parents: 47435
diff changeset
    42
by transfer auto
46395
f56be74d7f51 adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type
bulwahn
parents:
diff changeset
    43
46871
9100e6aa9272 renewing Executable_Relation
bulwahn
parents: 46395
diff changeset
    44
lemma [code]:
47894
2c6454643be6 defining and proving Executable_Relation with lift_definition and transfer
bulwahn
parents: 47435
diff changeset
    45
  "union (Rel X R) (Rel Y S) = Rel (X Un Y) (R Un S)"
2c6454643be6 defining and proving Executable_Relation with lift_definition and transfer
bulwahn
parents: 47435
diff changeset
    46
by transfer auto
46871
9100e6aa9272 renewing Executable_Relation
bulwahn
parents: 46395
diff changeset
    47
9100e6aa9272 renewing Executable_Relation
bulwahn
parents: 46395
diff changeset
    48
lemma [code]:
49757
73ab6d4a9236 rename Set.project to Set.filter - more appropriate name
kuncar
parents: 47894
diff changeset
    49
   "relcomp (Rel X R) (Rel Y S) = Rel (X Int Y) (Set.filter (%(x, y). y : Y) R Un (Set.filter (%(x, y). x : X) S Un R O S))"
47894
2c6454643be6 defining and proving Executable_Relation with lift_definition and transfer
bulwahn
parents: 47435
diff changeset
    50
by transfer (auto simp add: Id_on_eqI relcomp.simps)
46395
f56be74d7f51 adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type
bulwahn
parents:
diff changeset
    51
46871
9100e6aa9272 renewing Executable_Relation
bulwahn
parents: 46395
diff changeset
    52
lemma [code]:
47894
2c6454643be6 defining and proving Executable_Relation with lift_definition and transfer
bulwahn
parents: 47435
diff changeset
    53
  "rtrancl (Rel X R) = Rel UNIV (R^+)"
2c6454643be6 defining and proving Executable_Relation with lift_definition and transfer
bulwahn
parents: 47435
diff changeset
    54
apply transfer
2c6454643be6 defining and proving Executable_Relation with lift_definition and transfer
bulwahn
parents: 47435
diff changeset
    55
apply auto
2c6454643be6 defining and proving Executable_Relation with lift_definition and transfer
bulwahn
parents: 47435
diff changeset
    56
apply (metis Id_on_iff Un_commute UNIV_I rtrancl_Un_separatorE rtrancl_eq_or_trancl)
2c6454643be6 defining and proving Executable_Relation with lift_definition and transfer
bulwahn
parents: 47435
diff changeset
    57
by (metis in_rtrancl_UnI trancl_into_rtrancl)
46395
f56be74d7f51 adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type
bulwahn
parents:
diff changeset
    58
46871
9100e6aa9272 renewing Executable_Relation
bulwahn
parents: 46395
diff changeset
    59
lemma [code]:
47894
2c6454643be6 defining and proving Executable_Relation with lift_definition and transfer
bulwahn
parents: 47435
diff changeset
    60
  "Image (Rel X R) S = (X Int S) Un (R `` S)"
2c6454643be6 defining and proving Executable_Relation with lift_definition and transfer
bulwahn
parents: 47435
diff changeset
    61
by transfer auto
46871
9100e6aa9272 renewing Executable_Relation
bulwahn
parents: 46395
diff changeset
    62
47894
2c6454643be6 defining and proving Executable_Relation with lift_definition and transfer
bulwahn
parents: 47435
diff changeset
    63
quickcheck_generator rel constructors: Rel
46395
f56be74d7f51 adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type
bulwahn
parents:
diff changeset
    64
f56be74d7f51 adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type
bulwahn
parents:
diff changeset
    65
lemma
46871
9100e6aa9272 renewing Executable_Relation
bulwahn
parents: 46395
diff changeset
    66
  "member (x, (y :: nat)) (rtrancl (union R S)) \<Longrightarrow> member (x, y) (union (rtrancl R) (rtrancl S))"
9100e6aa9272 renewing Executable_Relation
bulwahn
parents: 46395
diff changeset
    67
quickcheck[exhaustive, expect = counterexample]
46395
f56be74d7f51 adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type
bulwahn
parents:
diff changeset
    68
oops
f56be74d7f51 adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type
bulwahn
parents:
diff changeset
    69
f56be74d7f51 adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type
bulwahn
parents:
diff changeset
    70
end