|
1 theory Executable_Relation |
|
2 imports Main |
|
3 begin |
|
4 |
|
5 text {* |
|
6 Current problem: rtrancl is not executable on an infinite type. |
|
7 *} |
|
8 |
|
9 lemma |
|
10 "(x, (y :: nat)) : rtrancl (R Un S) \<Longrightarrow> (x, y) : (rtrancl R) Un (rtrancl S)" |
|
11 (* quickcheck[exhaustive] fails ! *) |
|
12 oops |
|
13 |
|
14 code_thms rtrancl |
|
15 |
|
16 hide_const (open) rtrancl trancl |
|
17 |
|
18 quotient_type 'a rel = "('a * 'a) set" / "(op =)" |
|
19 morphisms set_of_rel rel_of_set by (metis identity_equivp) |
|
20 |
|
21 lemma [simp]: |
|
22 "rel_of_set (set_of_rel S) = S" |
|
23 by (rule Quotient_abs_rep[OF Quotient_rel]) |
|
24 |
|
25 lemma [simp]: |
|
26 "set_of_rel (rel_of_set R) = R" |
|
27 by (rule Quotient_rep_abs[OF Quotient_rel]) (rule refl) |
|
28 |
|
29 no_notation |
|
30 Set.member ("(_/ : _)" [50, 51] 50) |
|
31 |
|
32 quotient_definition member :: "'a * 'a => 'a rel => bool" where |
|
33 "member" is "Set.member :: 'a * 'a => ('a * 'a) set => bool" |
|
34 |
|
35 notation |
|
36 member ("(_/ : _)" [50, 51] 50) |
|
37 |
|
38 quotient_definition union :: "'a rel => 'a rel => 'a rel" where |
|
39 "union" is "Set.union :: ('a * 'a) set => ('a * 'a) set => ('a * 'a) set" |
|
40 |
|
41 quotient_definition rtrancl :: "'a rel => 'a rel" where |
|
42 "rtrancl" is "Transitive_Closure.rtrancl :: ('a * 'a) set => ('a * 'a) set" |
|
43 |
|
44 definition reflcl_raw |
|
45 where "reflcl_raw R = R \<union> Id" |
|
46 |
|
47 quotient_definition reflcl :: "('a * 'a) set => 'a rel" where |
|
48 "reflcl" is "reflcl_raw :: ('a * 'a) set => ('a * 'a) set" |
|
49 |
|
50 code_datatype reflcl rel_of_set |
|
51 |
|
52 lemma member_code[code]: |
|
53 "(x, y) : rel_of_set R = Set.member (x, y) R" |
|
54 "(x, y) : reflcl R = ((x = y) \<or> Set.member (x, y) R)" |
|
55 unfolding member_def reflcl_def reflcl_raw_def map_fun_def_raw o_def id_def |
|
56 by auto |
|
57 |
|
58 lemma union_code[code]: |
|
59 "union (rel_of_set R) (rel_of_set S) = rel_of_set (Set.union R S)" |
|
60 "union (reflcl R) (rel_of_set S) = reflcl (Set.union R S)" |
|
61 "union (reflcl R) (reflcl S) = reflcl (Set.union R S)" |
|
62 "union (rel_of_set R) (reflcl S) = reflcl (Set.union R S)" |
|
63 unfolding union_def reflcl_def reflcl_raw_def map_fun_def_raw o_def id_def |
|
64 by (auto intro: arg_cong[where f=rel_of_set]) |
|
65 |
|
66 lemma rtrancl_code[code]: |
|
67 "rtrancl (rel_of_set R) = reflcl (Transitive_Closure.trancl R)" |
|
68 "rtrancl (reflcl R) = reflcl (Transitive_Closure.trancl R)" |
|
69 unfolding rtrancl_def reflcl_def reflcl_raw_def map_fun_def_raw o_def id_def |
|
70 by (auto intro: arg_cong[where f=rel_of_set]) |
|
71 |
|
72 quickcheck_generator rel constructors: rel_of_set |
|
73 |
|
74 lemma |
|
75 "(x, (y :: nat)) : rtrancl (union R S) \<Longrightarrow> (x, y) : (union (rtrancl R) (rtrancl S))" |
|
76 quickcheck[exhaustive] |
|
77 oops |
|
78 |
|
79 end |