| author | Christian Urban <urbanc@in.tum.de> |
| Tue, 05 Jan 2010 14:09:04 +0100 | |
| changeset 807 | a5495a323b49 |
| parent 803 | 6f6ee78c7357 |
| child 808 | 90bde96f5dd1 |
| 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 |
|
807
a5495a323b49
added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
Christian Urban <urbanc@in.tum.de>
parents:
803
diff
changeset
|
14 |
|> writeln; |
|
a5495a323b49
added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
Christian Urban <urbanc@in.tum.de>
parents:
803
diff
changeset
|
15 |
new_equiv_relation_chk ctxt (rty, qty) |
|
a5495a323b49
added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
Christian Urban <urbanc@in.tum.de>
parents:
803
diff
changeset
|
16 |
|> Syntax.string_of_term ctxt |
|
a5495a323b49
added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
Christian Urban <urbanc@in.tum.de>
parents:
803
diff
changeset
|
17 |
|> writeln) |
|
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
|
18 |
*} |
|
790
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
19 |
|
|
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
|
20 |
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
|
21 |
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
|
22 |
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
|
23 |
"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
|
24 |
|
|
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
|
25 |
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
|
26 |
'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
|
27 |
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
|
28 |
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
|
29 |
by auto |
|
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
30 |
|
|
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
|
31 |
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
|
32 |
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
|
33 |
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
|
34 |
"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
|
35 |
|
|
790
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
36 |
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
|
37 |
'a foo = "('a * 'a) list" / erel2
|
|
790
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
38 |
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
|
39 |
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
|
40 |
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
|
41 |
|
|
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 |
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
|
43 |
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
|
44 |
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
|
45 |
"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
|
46 |
|
|
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 |
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
|
48 |
'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
|
49 |
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
|
50 |
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
|
51 |
by auto |
|
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
52 |
|
|
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
53 |
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
|
54 |
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
|
55 |
where |
|
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
56 |
"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
|
57 |
|
|
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
|
58 |
quotient_type myint = "nat \<times> nat" / intrel |
|
790
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
59 |
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
|
60 |
|
|
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
61 |
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
|
62 |
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
|
63 |
(@{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
|
64 |
@{typ "myint"})
|
|
790
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
65 |
*} |
|
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
66 |
|
|
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
67 |
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
|
68 |
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
|
69 |
(@{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
|
70 |
@{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
|
71 |
*} |
|
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
|
72 |
|
|
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
|
73 |
ML {*
|
|
803
6f6ee78c7357
a slight change to abs/rep generation
Christian Urban <urbanc@in.tum.de>
parents:
796
diff
changeset
|
74 |
test_funs repF @{context}
|
|
6f6ee78c7357
a slight change to abs/rep generation
Christian Urban <urbanc@in.tum.de>
parents:
796
diff
changeset
|
75 |
(@{typ "(('a * 'a) list * 'b)"},
|
|
6f6ee78c7357
a slight change to abs/rep generation
Christian Urban <urbanc@in.tum.de>
parents:
796
diff
changeset
|
76 |
@{typ "('a foo * 'b)"})
|
|
6f6ee78c7357
a slight change to abs/rep generation
Christian Urban <urbanc@in.tum.de>
parents:
796
diff
changeset
|
77 |
*} |
|
6f6ee78c7357
a slight change to abs/rep generation
Christian Urban <urbanc@in.tum.de>
parents:
796
diff
changeset
|
78 |
|
|
6f6ee78c7357
a slight change to abs/rep generation
Christian Urban <urbanc@in.tum.de>
parents:
796
diff
changeset
|
79 |
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
|
80 |
test_funs absF @{context}
|
|
790
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
81 |
(@{typ "(('a list) * int) list"},
|
|
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
82 |
@{typ "('a fset) bar"})
|
|
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
83 |
*} |
|
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
84 |
|
|
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
85 |
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
|
86 |
test_funs absF @{context}
|
|
807
a5495a323b49
added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
Christian Urban <urbanc@in.tum.de>
parents:
803
diff
changeset
|
87 |
(@{typ "('a list)"},
|
|
a5495a323b49
added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
Christian Urban <urbanc@in.tum.de>
parents:
803
diff
changeset
|
88 |
@{typ "('a fset)"})
|
|
a5495a323b49
added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
Christian Urban <urbanc@in.tum.de>
parents:
803
diff
changeset
|
89 |
*} |
|
a5495a323b49
added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
Christian Urban <urbanc@in.tum.de>
parents:
803
diff
changeset
|
90 |
|
|
a5495a323b49
added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
Christian Urban <urbanc@in.tum.de>
parents:
803
diff
changeset
|
91 |
ML {*
|
|
a5495a323b49
added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
Christian Urban <urbanc@in.tum.de>
parents:
803
diff
changeset
|
92 |
test_funs absF @{context}
|
|
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
|
93 |
(@{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
|
94 |
@{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
|
95 |
*} |
|
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 |
|
|
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 |
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
|
98 |
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
|
99 |
(@{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
|
100 |
@{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
|
101 |
*} |
|
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
|
102 |
|
|
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
|
103 |
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
|
104 |
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
|
105 |
(@{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
|
106 |
@{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
|
107 |
*} |
|
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
|
108 |
|
|
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
|
109 |
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
|
110 |
test_funs absF @{context}
|
|
796
64f9c76f70c7
corrected wrong [quot_respect] attribute; tuned
Christian Urban <urbanc@in.tum.de>
parents:
795
diff
changeset
|
111 |
(@{typ "('a list) list \<Rightarrow> 'a list"},
|
|
64f9c76f70c7
corrected wrong [quot_respect] attribute; tuned
Christian Urban <urbanc@in.tum.de>
parents:
795
diff
changeset
|
112 |
@{typ "('a fset) fset \<Rightarrow> 'a fset"})
|
|
790
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
113 |
*} |
|
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
114 |
|
|
3a48ffcf0f9a
generalised absrep function; needs consolidation
Christian Urban <urbanc@in.tum.de>
parents:
787
diff
changeset
|
115 |
|
|
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
|
116 |
|
|
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
117 |
|
|
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
118 |
|
|
3b21b24a5fb6
corrected map declarations for Sum and Prod; moved absrep_fun examples in separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
119 |
end |