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 *} |
5 ML {* open Quotient_Term *} |
6 |
6 |
7 print_maps |
7 ML {* |
|
8 fun test_funs flag ctxt (rty, qty) = |
|
9 (absrep_fun_chk flag ctxt (rty, qty) |
|
10 |> Syntax.string_of_term ctxt |
|
11 |> writeln; |
|
12 equiv_relation_chk ctxt (rty, qty) |
|
13 |> Syntax.string_of_term ctxt |
|
14 |> writeln) |
|
15 *} |
8 |
16 |
|
17 definition |
|
18 erel1 (infixl "\<approx>1" 50) |
|
19 where |
|
20 "erel1 \<equiv> \<lambda>xs ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys" |
9 |
21 |
10 quotient_type |
22 quotient_type |
11 'a fset = "'a list" / "\<lambda>xs ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys" |
23 'a fset = "'a list" / erel1 |
12 apply(rule equivpI) |
24 apply(rule equivpI) |
13 unfolding reflp_def symp_def transp_def |
25 unfolding erel1_def reflp_def symp_def transp_def |
14 by auto |
26 by auto |
15 |
27 |
|
28 definition |
|
29 erel2 (infixl "\<approx>2" 50) |
|
30 where |
|
31 "erel2 \<equiv> \<lambda>(xs::('a * 'a) list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys" |
|
32 |
16 quotient_type |
33 quotient_type |
17 'a foo = "('a * 'a) list" / "\<lambda>(xs::('a * 'a) list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys" |
34 'a foo = "('a * 'a) list" / erel2 |
18 apply(rule equivpI) |
35 apply(rule equivpI) |
19 unfolding reflp_def symp_def transp_def |
36 unfolding erel2_def reflp_def symp_def transp_def |
20 by auto |
37 by auto |
21 |
38 |
|
39 definition |
|
40 erel3 (infixl "\<approx>3" 50) |
|
41 where |
|
42 "erel3 \<equiv> \<lambda>(xs::('a * int) list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys" |
|
43 |
22 quotient_type |
44 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" |
45 'a bar = "('a * int) list" / "erel3" |
24 apply(rule equivpI) |
46 apply(rule equivpI) |
25 unfolding reflp_def symp_def transp_def |
47 unfolding erel3_def reflp_def symp_def transp_def |
26 by auto |
48 by auto |
27 |
49 |
28 fun |
50 fun |
29 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" |
51 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infixl "\<approx>4" 50) |
30 where |
52 where |
31 "intrel (x, y) (u, v) = (x + v = u + y)" |
53 "intrel (x, y) (u, v) = (x + v = u + y)" |
32 |
54 |
33 quotient_type int = "nat \<times> nat" / intrel |
55 quotient_type myint = "nat \<times> nat" / intrel |
34 by (auto simp add: equivp_def expand_fun_eq) |
56 by (auto simp add: equivp_def expand_fun_eq) |
35 |
57 |
36 print_quotients |
|
37 |
|
38 ML {* |
58 ML {* |
39 absrep_fun_chk absF @{context} |
59 test_funs absF @{context} |
40 (@{typ "('a * 'a) list"}, |
60 (@{typ "nat \<times> nat"}, |
41 @{typ "'a foo"}) |
61 @{typ "myint"}) |
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 *} |
62 |
63 |
63 ML {* |
64 ML {* |
64 absrep_fun_chk absF @{context} |
65 test_funs absF @{context} |
65 (@{typ "nat \<times> nat"}, |
66 (@{typ "('a * 'a) list"}, |
66 @{typ "int"}) |
67 @{typ "'a foo"}) |
67 |> Syntax.string_of_term @{context} |
68 *} |
68 |> writeln |
69 |
|
70 ML {* |
|
71 test_funs absF @{context} |
|
72 (@{typ "(('a list) * int) list"}, |
|
73 @{typ "('a fset) bar"}) |
|
74 *} |
|
75 |
|
76 ML {* |
|
77 test_funs absF @{context} |
|
78 (@{typ "('a list) list"}, |
|
79 @{typ "('a fset) fset"}) |
|
80 *} |
|
81 |
|
82 ML {* |
|
83 test_funs absF @{context} |
|
84 (@{typ "(('a * 'a) list) list"}, |
|
85 @{typ "(('a * 'a) fset) fset"}) |
|
86 *} |
|
87 |
|
88 ML {* |
|
89 test_funs absF @{context} |
|
90 (@{typ "(nat * nat) list"}, |
|
91 @{typ "myint fset"}) |
|
92 *} |
|
93 |
|
94 ML {* |
|
95 test_funs absF @{context} |
|
96 (@{typ "('a list) list \<Rightarrow> 'a"}, |
|
97 @{typ "('a fset) fset \<Rightarrow> 'a"}) |
69 *} |
98 *} |
70 |
99 |
71 |
100 |
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" |
|
86 |
|
87 print_quotients |
|
88 |
|
89 ML{* |
|
90 Quotient_Info.quotient_rules_get @{context} |
|
91 *} |
|
92 |
|
93 print_quotients |
|
94 |
|
95 ML {* |
|
96 open Quotient_Term; |
|
97 *} |
|
98 |
|
99 ML {* |
|
100 absrep_fun_chk absF @{context} |
|
101 (@{typ "(('a * 'a) list) list"}, |
|
102 @{typ "(('a * 'a) fset) fset"}) |
|
103 |> Syntax.string_of_term @{context} |
|
104 |> writeln |
|
105 *} |
|
106 |
|
107 (* |
|
108 ML {* |
|
109 absrep_fun_chk absF @{context} |
|
110 (@{typ "('a * 'a) list"}, |
|
111 @{typ "'a foo"}) |
|
112 |> Syntax.string_of_term @{context} |
|
113 |> writeln |
|
114 *} |
|
115 *) |
|
116 |
|
117 term "option_map (prod_fun (abs_fset \<circ> map abs_int) id)" |
|
118 term "option_map (prod_fun (map rep_int \<circ> rep_fset) id)" |
|
119 term "option_map (map rep_int \<circ> rep_fset)" |
|
120 term "option_map (abs_fset o (map abs_int))" |
|
121 term "abs_fset" |
|
122 |
|
123 ML {* |
|
124 absrep_fun_chk absF @{context} (@{typ "(nat * nat) list"}, @{typ "int fset"}) |
|
125 |> Syntax.string_of_term @{context} |
|
126 |> writeln |
|
127 *} |
|
128 |
|
129 term "map abs_int" |
|
130 term "abs_fset o map abs_int" |
|
131 |
101 |
132 |
102 |
133 ML {* |
|
134 absrep_fun_chk absF @{context} (@{typ "('a list) list"}, @{typ "('a fset) fset"}) |
|
135 |> Syntax.string_of_term @{context} |
|
136 |> writeln |
|
137 *} |
|
138 |
|
139 ML {* |
|
140 absrep_fun_chk absF @{context} (@{typ "('a list) list \<Rightarrow> 'a"}, @{typ "('a fset) fset \<Rightarrow> 'a"}) |
|
141 |> Syntax.string_of_term @{context} |
|
142 |> writeln |
|
143 *} |
|
144 |
103 |
145 end |
104 end |