| author | Christian Urban <urbanc@in.tum.de> |
| Sat, 26 Dec 2009 21:36:20 +0100 | |
| changeset 795 | a28f805df355 |
| parent 790 | 3a48ffcf0f9a |
| child 796 | 64f9c76f70c7 |
| permissions | -rw-r--r-- |
|
779
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
theory AbsRepTest |
|
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
2 |
imports "../QuotMain" "../QuotList" "../QuotOption" "../QuotSum" "../QuotProd" List |
|
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
3 |
begin |
|
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
|
|
790
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
5 |
ML {* open Quotient_Term *}
|
|
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
6 |
|
|
795
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
7 |
ML {*
|
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
8 |
fun test_funs flag ctxt (rty, qty) = |
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
9 |
(absrep_fun_chk flag ctxt (rty, qty) |
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
10 |
|> Syntax.string_of_term ctxt |
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
11 |
|> writeln; |
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
12 |
equiv_relation_chk ctxt (rty, qty) |
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
13 |
|> Syntax.string_of_term ctxt |
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
14 |
|> writeln) |
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
15 |
*} |
|
790
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
16 |
|
|
795
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
17 |
definition |
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
18 |
erel1 (infixl "\<approx>1" 50) |
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
19 |
where |
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
20 |
"erel1 \<equiv> \<lambda>xs ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys" |
|
787
5cf83fa5b36c
made the quotient_type definition more like typedef; now type variables need to be explicitly given
Christian Urban <urbanc@in.tum.de>
parents:
786
diff
changeset
|
21 |
|
|
5cf83fa5b36c
made the quotient_type definition more like typedef; now type variables need to be explicitly given
Christian Urban <urbanc@in.tum.de>
parents:
786
diff
changeset
|
22 |
quotient_type |
|
795
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
23 |
'a fset = "'a list" / erel1 |
|
779
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
24 |
apply(rule equivpI) |
|
795
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
25 |
unfolding erel1_def reflp_def symp_def transp_def |
|
790
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
26 |
by auto |
|
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
27 |
|
|
795
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
28 |
definition |
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
29 |
erel2 (infixl "\<approx>2" 50) |
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
30 |
where |
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
31 |
"erel2 \<equiv> \<lambda>(xs::('a * 'a) list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys"
|
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
32 |
|
|
790
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
33 |
quotient_type |
|
795
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
34 |
'a foo = "('a * 'a) list" / erel2
|
|
790
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
35 |
apply(rule equivpI) |
|
795
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
36 |
unfolding erel2_def reflp_def symp_def transp_def |
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
37 |
by auto |
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
38 |
|
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
39 |
definition |
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
40 |
erel3 (infixl "\<approx>3" 50) |
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
41 |
where |
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
42 |
"erel3 \<equiv> \<lambda>(xs::('a * int) list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys"
|
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
43 |
|
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
44 |
quotient_type |
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
45 |
'a bar = "('a * int) list" / "erel3"
|
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
46 |
apply(rule equivpI) |
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
47 |
unfolding erel3_def reflp_def symp_def transp_def |
|
790
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
48 |
by auto |
|
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
49 |
|
|
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
50 |
fun |
|
795
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
51 |
intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infixl "\<approx>4" 50) |
|
790
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
52 |
where |
|
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
53 |
"intrel (x, y) (u, v) = (x + v = u + y)" |
|
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
54 |
|
|
795
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
55 |
quotient_type myint = "nat \<times> nat" / intrel |
|
790
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
56 |
by (auto simp add: equivp_def expand_fun_eq) |
|
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
57 |
|
|
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
58 |
ML {*
|
|
795
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
59 |
test_funs absF @{context}
|
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
60 |
(@{typ "nat \<times> nat"},
|
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
61 |
@{typ "myint"})
|
|
790
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
62 |
*} |
|
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
63 |
|
|
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
64 |
ML {*
|
|
795
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
65 |
test_funs absF @{context}
|
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
66 |
(@{typ "('a * 'a) list"},
|
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
67 |
@{typ "'a foo"})
|
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
68 |
*} |
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
69 |
|
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
70 |
ML {*
|
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
71 |
test_funs absF @{context}
|
|
790
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
72 |
(@{typ "(('a list) * int) list"},
|
|
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
73 |
@{typ "('a fset) bar"})
|
|
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
74 |
*} |
|
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
75 |
|
|
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
76 |
ML {*
|
|
795
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
77 |
test_funs absF @{context}
|
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
78 |
(@{typ "('a list) list"},
|
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
79 |
@{typ "('a fset) fset"})
|
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
80 |
*} |
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
81 |
|
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
82 |
ML {*
|
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
83 |
test_funs absF @{context}
|
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
84 |
(@{typ "(('a * 'a) list) list"},
|
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
85 |
@{typ "(('a * 'a) fset) fset"})
|
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
86 |
*} |
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
87 |
|
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
88 |
ML {*
|
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
89 |
test_funs absF @{context}
|
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
90 |
(@{typ "(nat * nat) list"},
|
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
91 |
@{typ "myint fset"})
|
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
92 |
*} |
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
93 |
|
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
94 |
ML {*
|
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
95 |
test_funs absF @{context}
|
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
96 |
(@{typ "('a list) list \<Rightarrow> 'a"},
|
|
a28f805df355
renamed mk_resp_arg to equiv_relation and exported it in the signature; added tests in AbsRepFun.thy
Christian Urban <urbanc@in.tum.de>
parents:
790
diff
changeset
|
97 |
@{typ "('a fset) fset \<Rightarrow> 'a"})
|
|
790
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
98 |
*} |
|
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
99 |
|
|
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
100 |
|
|
779
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
101 |
|
|
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
102 |
|
|
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
103 |
|
|
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
104 |
end |