1 theory AbsRepTest |
1 theory AbsRepTest |
2 imports "../QuotMain" "../QuotList" "../QuotOption" "../QuotSum" "../QuotProd" List |
2 imports "../QuotMain" "../QuotList" "../QuotOption" "../QuotSum" "../QuotProd" List |
3 begin |
3 begin |
4 |
4 |
|
5 ML {* open Quotient_Term *} |
|
6 |
5 print_maps |
7 print_maps |
|
8 |
6 |
9 |
7 quotient_type |
10 quotient_type |
8 'a fset = "'a list" / "\<lambda>xs ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys" |
11 'a fset = "'a list" / "\<lambda>xs ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys" |
9 apply(rule equivpI) |
12 apply(rule equivpI) |
10 unfolding reflp_def symp_def transp_def |
13 unfolding reflp_def symp_def transp_def |
11 apply(auto) |
14 by auto |
12 done |
|
13 |
15 |
14 quotient_type |
16 quotient_type |
15 'a foo = "('a * 'a) list" / "\<lambda>(xs::('a * 'a) list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys" |
17 'a foo = "('a * 'a) list" / "\<lambda>(xs::('a * 'a) list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys" |
16 apply(rule equivpI) |
18 apply(rule equivpI) |
17 unfolding reflp_def symp_def transp_def |
19 unfolding reflp_def symp_def transp_def |
18 apply(auto) |
20 by auto |
19 done |
21 |
|
22 quotient_type |
|
23 'a bar = "('a * int) list" / "\<lambda>(xs::('a * int) list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys" |
|
24 apply(rule equivpI) |
|
25 unfolding reflp_def symp_def transp_def |
|
26 by auto |
|
27 |
|
28 fun |
|
29 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" |
|
30 where |
|
31 "intrel (x, y) (u, v) = (x + v = u + y)" |
|
32 |
|
33 quotient_type int = "nat \<times> nat" / intrel |
|
34 by (auto simp add: equivp_def expand_fun_eq) |
|
35 |
|
36 print_quotients |
|
37 |
|
38 ML {* |
|
39 absrep_fun_chk absF @{context} |
|
40 (@{typ "('a * 'a) list"}, |
|
41 @{typ "'a foo"}) |
|
42 |> Syntax.string_of_term @{context} |
|
43 |> writeln |
|
44 *} |
|
45 |
|
46 (* PROBLEM |
|
47 ML {* |
|
48 absrep_fun_chk absF @{context} |
|
49 (@{typ "(('a list) * int) list"}, |
|
50 @{typ "('a fset) bar"}) |
|
51 |> Syntax.string_of_term @{context} |
|
52 |> writeln |
|
53 *}*) |
|
54 |
|
55 ML {* |
|
56 absrep_fun_chk absF @{context} |
|
57 (@{typ "('a list) list"}, |
|
58 @{typ "('a fset) fset"}) |
|
59 |> Syntax.string_of_term @{context} |
|
60 |> writeln |
|
61 *} |
|
62 |
|
63 ML {* |
|
64 absrep_fun_chk absF @{context} |
|
65 (@{typ "nat \<times> nat"}, |
|
66 @{typ "int"}) |
|
67 |> Syntax.string_of_term @{context} |
|
68 |> writeln |
|
69 *} |
|
70 |
|
71 |
|
72 term abs_foo |
|
73 term rep_foo |
|
74 term "abs_foo o map (prod_fun id id)" |
|
75 term "map (prod_fun id id) o rep_foo" |
|
76 |
|
77 ML {* |
|
78 absrep_fun_chk absF @{context} |
|
79 (@{typ "('a * 'a) list"}, |
|
80 @{typ "'a foo"}) |
|
81 |> Syntax.string_of_term @{context} |
|
82 |> writeln |
|
83 *} |
|
84 |
|
85 typ "('a fset) foo" |
20 |
86 |
21 print_quotients |
87 print_quotients |
22 |
88 |
23 ML{* |
89 ML{* |
24 Quotient_Info.quotient_rules_get @{context} |
90 Quotient_Info.quotient_rules_get @{context} |
25 *} |
91 *} |
26 |
|
27 quotient_type int = "nat \<times> nat" / "\<lambda>(x, y) (u, v). x + v = u + (y::nat)" |
|
28 apply(rule equivpI) |
|
29 unfolding reflp_def symp_def transp_def |
|
30 apply(auto) |
|
31 done |
|
32 |
92 |
33 print_quotients |
93 print_quotients |
34 |
94 |
35 ML {* |
95 ML {* |
36 open Quotient_Term; |
96 open Quotient_Term; |