|
1 theory AbsRepTest |
|
2 imports "../QuotMain" "../QuotList" "../QuotOption" "../QuotSum" "../QuotProd" List |
|
3 begin |
|
4 |
|
5 |
|
6 (* |
|
7 quotient_type |
|
8 fset = "'a list" / "\<lambda>(xs::'a list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys" |
|
9 apply(rule equivpI) |
|
10 unfolding reflp_def symp_def transp_def |
|
11 apply(auto) |
|
12 sorry |
|
13 done |
|
14 *) |
|
15 |
|
16 inductive |
|
17 list_eq (infix "\<approx>" 50) |
|
18 where |
|
19 "a#b#xs \<approx> b#a#xs" |
|
20 | "[] \<approx> []" |
|
21 | "xs \<approx> ys \<Longrightarrow> ys \<approx> xs" |
|
22 | "a#a#xs \<approx> a#xs" |
|
23 | "xs \<approx> ys \<Longrightarrow> a#xs \<approx> a#ys" |
|
24 | "\<lbrakk>xs1 \<approx> xs2; xs2 \<approx> xs3\<rbrakk> \<Longrightarrow> xs1 \<approx> xs3" |
|
25 |
|
26 quotient_type |
|
27 fset = "'a list" / "list_eq" |
|
28 sorry |
|
29 |
|
30 |
|
31 fun |
|
32 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" |
|
33 where |
|
34 "intrel (x, y) (u, v) = (x + v = u + y)" |
|
35 |
|
36 quotient_type int = "nat \<times> nat" / intrel |
|
37 sorry |
|
38 |
|
39 |
|
40 ML {* |
|
41 open Quotient_Term; |
|
42 *} |
|
43 |
|
44 ML {* |
|
45 absrep_fun_chk absF @{context} (@{typ "(((nat * nat) list) * 'a) option"}, @{typ "((int fset) * 'a) option"}) |
|
46 |> Syntax.string_of_term @{context} |
|
47 |> writeln |
|
48 *} |
|
49 |
|
50 term "option_map (prod_fun (abs_fset \<circ> map abs_int) id)" |
|
51 term "option_map (prod_fun (map rep_int \<circ> rep_fset) id)" |
|
52 term "option_map (map rep_int \<circ> rep_fset)" |
|
53 term "option_map (abs_fset o (map abs_int))" |
|
54 term "abs_fset" |
|
55 |
|
56 ML {* |
|
57 absrep_fun_chk absF @{context} (@{typ "(nat * nat) list"}, @{typ "int fset"}) |
|
58 |> Syntax.string_of_term @{context} |
|
59 |> writeln |
|
60 *} |
|
61 |
|
62 term "map abs_int" |
|
63 term "abs_fset o map abs_int" |
|
64 |
|
65 |
|
66 ML {* |
|
67 absrep_fun_chk absF @{context} (@{typ "('a list) list"}, @{typ "('a fset) fset"}) |
|
68 |> Syntax.string_of_term @{context} |
|
69 |> writeln |
|
70 *} |
|
71 |
|
72 ML {* |
|
73 absrep_fun_chk absF @{context} (@{typ "('a list) list \<Rightarrow> 'a"}, @{typ "('a fset) fset \<Rightarrow> 'a"}) |
|
74 |> Syntax.string_of_term @{context} |
|
75 |> writeln |
|
76 *} |
|
77 |
|
78 end |