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
|
1128
|
2 |
imports "../Quotient" "../Quotient_List" "../Quotient_Option" "../Quotient_Sum" "../Quotient_Product" List
|
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
|
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 |
|
922
|
5 |
|
|
6 |
(*
|
918
|
7 |
ML_command "ProofContext.debug := false"
|
|
8 |
ML_command "ProofContext.verbose := false"
|
922
|
9 |
*)
|
918
|
10 |
|
790
|
11 |
ML {* open Quotient_Term *}
|
|
12 |
|
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>
diff
changeset
|
13 |
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>
diff
changeset
|
14 |
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>
diff
changeset
|
15 |
(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>
diff
changeset
|
16 |
|> 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>
diff
changeset
|
17 |
|> 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>
diff
changeset
|
18 |
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>
diff
changeset
|
19 |
|> 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>
diff
changeset
|
20 |
|> 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>
diff
changeset
|
21 |
*}
|
790
|
22 |
|
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>
diff
changeset
|
23 |
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>
diff
changeset
|
24 |
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>
diff
changeset
|
25 |
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>
diff
changeset
|
26 |
"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>
diff
changeset
|
27 |
|
5cf83fa5b36c
made the quotient_type definition more like typedef; now type variables need to be explicitly given
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
28 |
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>
diff
changeset
|
29 |
'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
|
30 |
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>
diff
changeset
|
31 |
unfolding erel1_def reflp_def symp_def transp_def
|
790
|
32 |
by auto
|
|
33 |
|
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>
diff
changeset
|
34 |
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>
diff
changeset
|
35 |
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>
diff
changeset
|
36 |
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>
diff
changeset
|
37 |
"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>
diff
changeset
|
38 |
|
790
|
39 |
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>
diff
changeset
|
40 |
'a foo = "('a * 'a) list" / erel2
|
790
|
41 |
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>
diff
changeset
|
42 |
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>
diff
changeset
|
43 |
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>
diff
changeset
|
44 |
|
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>
diff
changeset
|
45 |
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>
diff
changeset
|
46 |
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>
diff
changeset
|
47 |
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>
diff
changeset
|
48 |
"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>
diff
changeset
|
49 |
|
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>
diff
changeset
|
50 |
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>
diff
changeset
|
51 |
'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>
diff
changeset
|
52 |
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>
diff
changeset
|
53 |
unfolding erel3_def reflp_def symp_def transp_def
|
790
|
54 |
by auto
|
|
55 |
|
|
56 |
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>
diff
changeset
|
57 |
intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infixl "\<approx>4" 50)
|
790
|
58 |
where
|
|
59 |
"intrel (x, y) (u, v) = (x + v = u + y)"
|
|
60 |
|
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>
diff
changeset
|
61 |
quotient_type myint = "nat \<times> nat" / intrel
|
790
|
62 |
by (auto simp add: equivp_def expand_fun_eq)
|
|
63 |
|
|
64 |
ML {*
|
1097
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
65 |
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>
diff
changeset
|
66 |
(@{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>
diff
changeset
|
67 |
@{typ "myint"})
|
790
|
68 |
*}
|
|
69 |
|
|
70 |
ML {*
|
1097
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
71 |
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>
diff
changeset
|
72 |
(@{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>
diff
changeset
|
73 |
@{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>
diff
changeset
|
74 |
*}
|
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>
diff
changeset
|
75 |
|
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>
diff
changeset
|
76 |
ML {*
|
1097
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
77 |
test_funs RepF @{context}
|
803
|
78 |
(@{typ "(('a * 'a) list * 'b)"},
|
|
79 |
@{typ "('a foo * 'b)"})
|
|
80 |
*}
|
|
81 |
|
|
82 |
ML {*
|
1097
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
83 |
test_funs AbsF @{context}
|
790
|
84 |
(@{typ "(('a list) * int) list"},
|
|
85 |
@{typ "('a fset) bar"})
|
|
86 |
*}
|
|
87 |
|
|
88 |
ML {*
|
1097
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
89 |
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>
diff
changeset
|
90 |
(@{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>
diff
changeset
|
91 |
@{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>
diff
changeset
|
92 |
*}
|
a5495a323b49
added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
93 |
|
a5495a323b49
added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
94 |
ML {*
|
1097
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
95 |
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>
diff
changeset
|
96 |
(@{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>
diff
changeset
|
97 |
@{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>
diff
changeset
|
98 |
*}
|
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>
diff
changeset
|
99 |
|
808
90bde96f5dd1
proper handling of error messages (code copy - maybe this can be avoided)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
100 |
|
811
|
101 |
ML {*
|
1097
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
102 |
test_funs AbsF @{context}
|
811
|
103 |
(@{typ "((nat * nat) list) list"},
|
|
104 |
@{typ "((myint) fset) fset"})
|
|
105 |
*}
|
808
90bde96f5dd1
proper handling of error messages (code copy - maybe this can be avoided)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
106 |
|
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>
diff
changeset
|
107 |
ML {*
|
1097
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
108 |
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>
diff
changeset
|
109 |
(@{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>
diff
changeset
|
110 |
@{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>
diff
changeset
|
111 |
*}
|
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>
diff
changeset
|
112 |
|
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>
diff
changeset
|
113 |
ML {*
|
1097
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
114 |
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>
diff
changeset
|
115 |
(@{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>
diff
changeset
|
116 |
@{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>
diff
changeset
|
117 |
*}
|
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>
diff
changeset
|
118 |
|
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>
diff
changeset
|
119 |
ML {*
|
1097
551eacf071d7
More indentation, names and todo cleaning in the quotient package
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
120 |
test_funs AbsF @{context}
|
796
|
121 |
(@{typ "('a list) list \<Rightarrow> 'a list"},
|
|
122 |
@{typ "('a fset) fset \<Rightarrow> 'a fset"})
|
790
|
123 |
*}
|
|
124 |
|
822
|
125 |
lemma OO_sym_inv:
|
809
|
126 |
assumes sr: "symp r"
|
|
127 |
and ss: "symp s"
|
|
128 |
shows "(r OO s) x y = (s OO r) y x"
|
822
|
129 |
using sr ss
|
|
130 |
unfolding symp_def
|
|
131 |
apply (metis pred_comp.intros pred_compE ss symp_def)
|
|
132 |
done
|
809
|
133 |
|
812
|
134 |
lemma abs_o_rep:
|
|
135 |
assumes a: "Quotient r absf repf"
|
|
136 |
shows "absf o repf = id"
|
|
137 |
apply(rule ext)
|
|
138 |
apply(simp add: Quotient_abs_rep[OF a])
|
822
|
139 |
done
|
812
|
140 |
|
824
|
141 |
lemma set_in_eq: "(\<forall>e. ((e \<in> A) \<longleftrightarrow> (e \<in> B))) \<equiv> A = B"
|
822
|
142 |
apply (rule eq_reflection)
|
|
143 |
apply auto
|
|
144 |
done
|
816
|
145 |
|
822
|
146 |
lemma map_rel_cong: "b \<approx>1 ba \<Longrightarrow> map f b \<approx>1 map f ba"
|
|
147 |
unfolding erel1_def
|
|
148 |
apply(simp only: set_map set_in_eq)
|
|
149 |
done
|
821
|
150 |
|
|
151 |
lemma quotient_compose_list_gen_pre:
|
|
152 |
assumes a: "equivp r2"
|
|
153 |
and b: "Quotient r2 abs2 rep2"
|
852
|
154 |
shows "(list_rel r2 OOO op \<approx>1) r s =
|
|
155 |
((list_rel r2 OOO op \<approx>1) r r \<and> (list_rel r2 OOO op \<approx>1) s s \<and>
|
821
|
156 |
abs_fset (map abs2 r) = abs_fset (map abs2 s))"
|
822
|
157 |
apply rule
|
|
158 |
apply rule
|
|
159 |
apply rule
|
|
160 |
apply (rule list_rel_refl)
|
|
161 |
apply (metis equivp_def a)
|
|
162 |
apply rule
|
|
163 |
apply (rule equivp_reflp[OF fset_equivp])
|
|
164 |
apply (rule list_rel_refl)
|
|
165 |
apply (metis equivp_def a)
|
|
166 |
apply(rule)
|
|
167 |
apply rule
|
|
168 |
apply (rule list_rel_refl)
|
|
169 |
apply (metis equivp_def a)
|
|
170 |
apply rule
|
|
171 |
apply (rule equivp_reflp[OF fset_equivp])
|
|
172 |
apply (rule list_rel_refl)
|
|
173 |
apply (metis equivp_def a)
|
|
174 |
apply (subgoal_tac "map abs2 r \<approx>1 map abs2 s")
|
|
175 |
apply (metis Quotient_rel[OF Quotient_fset])
|
|
176 |
apply (auto)[1]
|
|
177 |
apply (subgoal_tac "map abs2 r = map abs2 b")
|
|
178 |
prefer 2
|
|
179 |
apply (metis Quotient_rel[OF list_quotient[OF b]])
|
|
180 |
apply (subgoal_tac "map abs2 s = map abs2 ba")
|
|
181 |
prefer 2
|
|
182 |
apply (metis Quotient_rel[OF list_quotient[OF b]])
|
|
183 |
apply (simp add: map_rel_cong)
|
|
184 |
apply rule
|
|
185 |
apply (rule rep_abs_rsp[of "list_rel r2" "map abs2"])
|
|
186 |
apply (rule list_quotient)
|
|
187 |
apply (rule b)
|
|
188 |
apply (rule list_rel_refl)
|
|
189 |
apply (metis equivp_def a)
|
|
190 |
apply rule
|
|
191 |
prefer 2
|
|
192 |
apply (rule rep_abs_rsp_left[of "list_rel r2" "map abs2"])
|
|
193 |
apply (rule list_quotient)
|
|
194 |
apply (rule b)
|
|
195 |
apply (rule list_rel_refl)
|
|
196 |
apply (metis equivp_def a)
|
|
197 |
apply (erule conjE)+
|
|
198 |
apply (subgoal_tac "map abs2 r \<approx>1 map abs2 s")
|
|
199 |
apply (rule map_rel_cong)
|
|
200 |
apply (assumption)
|
|
201 |
apply (metis Quotient_def Quotient_fset equivp_reflp fset_equivp a b)
|
|
202 |
done
|
821
|
203 |
|
820
|
204 |
lemma quotient_compose_list_gen:
|
821
|
205 |
assumes a: "Quotient r2 abs2 rep2"
|
823
ae3ed7a68e80
Replacing equivp by reflp in the assumptions leads to non-provable subgoals in the gen_pre lemmas.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
206 |
and b: "equivp r2" (* reflp is not enough *)
|
852
|
207 |
shows "Quotient ((list_rel r2) OOO (op \<approx>1))
|
811
|
208 |
(abs_fset \<circ> (map abs2)) ((map rep2) \<circ> rep_fset)"
|
812
|
209 |
unfolding Quotient_def comp_def
|
822
|
210 |
apply (rule)+
|
|
211 |
apply (simp add: abs_o_rep[OF a] id_simps Quotient_abs_rep[OF Quotient_fset])
|
|
212 |
apply (rule)
|
|
213 |
apply (rule)
|
|
214 |
apply (rule)
|
|
215 |
apply (rule list_rel_refl)
|
|
216 |
apply (metis b equivp_def)
|
|
217 |
apply (rule)
|
|
218 |
apply (rule equivp_reflp[OF fset_equivp])
|
|
219 |
apply (rule list_rel_refl)
|
|
220 |
apply (metis b equivp_def)
|
|
221 |
apply rule
|
|
222 |
apply rule
|
|
223 |
apply(rule quotient_compose_list_gen_pre[OF b a])
|
|
224 |
done
|
809
|
225 |
|
821
|
226 |
(* This is the general statement but the types of abs2 and rep2
|
|
227 |
are wrong as can be seen in following exanples *)
|
818
9ab49dc166d6
More cleaning and commenting AbsRepTest. Now tests work; just slow.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
228 |
lemma quotient_compose_general:
|
821
|
229 |
assumes a2: "Quotient r1 abs1 rep1"
|
810
|
230 |
and "Quotient r2 abs2 rep2"
|
852
|
231 |
shows "Quotient ((list_rel r2) OOO r1)
|
821
|
232 |
(abs1 \<circ> (map abs2)) ((map rep2) \<circ> rep1)"
|
810
|
233 |
sorry
|
|
234 |
|
822
|
235 |
thm quotient_compose_list_gen[OF Quotient_fset fset_equivp]
|
818
9ab49dc166d6
More cleaning and commenting AbsRepTest. Now tests work; just slow.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
236 |
thm quotient_compose_general[OF Quotient_fset]
|
817
|
237 |
(* Doesn't work: *)
|
818
9ab49dc166d6
More cleaning and commenting AbsRepTest. Now tests work; just slow.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
238 |
(* thm quotient_compose_general[OF Quotient_fset Quotient_fset] *)
|
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
|
239 |
|
809
|
240 |
end
|