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 |
|
922
|
5 |
|
|
6 |
(*
|
918
|
7 |
ML_command "ProofContext.debug := false"
|
|
8 |
ML_command "ProofContext.verbose := false"
|
922
|
9 |
*)
|
918
|
10 |
|
|
11 |
ML {*
|
|
12 |
val ctxt0 = @{context}
|
|
13 |
val ty = Syntax.read_typ ctxt0 "bool"
|
|
14 |
val ctxt1 = Variable.declare_typ ty ctxt0
|
|
15 |
val trm = Syntax.parse_term ctxt1 "A \<and> B"
|
|
16 |
val trm' = Syntax.type_constraint ty trm
|
|
17 |
val trm'' = Syntax.check_term ctxt1 trm'
|
|
18 |
val ctxt2 = Variable.declare_term trm'' ctxt1
|
|
19 |
*}
|
|
20 |
|
|
21 |
term "split"
|
|
22 |
|
|
23 |
term "Ex1 (\<lambda>(x, y). P x y)"
|
|
24 |
|
|
25 |
lemma "(Ex1 (\<lambda>(x, y). P x y)) \<Longrightarrow> (\<exists>! x. \<exists>! y. P x y)"
|
|
26 |
apply(erule ex1E)
|
|
27 |
apply(case_tac x)
|
|
28 |
apply(clarify)
|
|
29 |
apply(rule_tac a="aa" in ex1I)
|
|
30 |
apply(rule ex1I)
|
|
31 |
apply(assumption)
|
|
32 |
apply(blast)
|
|
33 |
apply(blast)
|
|
34 |
done
|
|
35 |
|
|
36 |
(*
|
|
37 |
lemma "(\<exists>! x. \<exists>! y. P x y) \<Longrightarrow> (Ex1 (\<lambda>(x, y). P x y))"
|
|
38 |
apply(erule ex1E)
|
|
39 |
apply(erule ex1E)
|
|
40 |
apply(rule_tac a="(x, y)" in ex1I)
|
|
41 |
apply(clarify)
|
|
42 |
apply(case_tac xa)
|
|
43 |
apply(clarify)
|
|
44 |
|
|
45 |
apply(rule ex1I)
|
|
46 |
apply(assumption)
|
|
47 |
apply(blast)
|
|
48 |
apply(blast)
|
|
49 |
done
|
|
50 |
|
|
51 |
apply(metis)
|
|
52 |
*)
|
|
53 |
|
790
|
54 |
ML {* open Quotient_Term *}
|
|
55 |
|
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
|
56 |
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
|
57 |
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
|
58 |
(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
|
59 |
|> 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
|
60 |
|> 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
|
61 |
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
|
62 |
|> 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
|
63 |
|> 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
|
64 |
*}
|
790
|
65 |
|
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 |
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
|
67 |
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
|
68 |
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
|
69 |
"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
|
70 |
|
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
|
71 |
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
|
72 |
'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
|
73 |
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
|
74 |
unfolding erel1_def reflp_def symp_def transp_def
|
790
|
75 |
by auto
|
|
76 |
|
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
|
77 |
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
|
78 |
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
|
79 |
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
|
80 |
"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
|
81 |
|
790
|
82 |
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
|
83 |
'a foo = "('a * 'a) list" / erel2
|
790
|
84 |
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
|
85 |
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
|
86 |
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
|
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>
diff
changeset
|
88 |
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
|
89 |
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
|
90 |
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
|
91 |
"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
|
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>
diff
changeset
|
93 |
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
|
94 |
'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
|
95 |
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
|
96 |
unfolding erel3_def reflp_def symp_def transp_def
|
790
|
97 |
by auto
|
|
98 |
|
|
99 |
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
|
100 |
intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" (infixl "\<approx>4" 50)
|
790
|
101 |
where
|
|
102 |
"intrel (x, y) (u, v) = (x + v = u + y)"
|
|
103 |
|
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
|
104 |
quotient_type myint = "nat \<times> nat" / intrel
|
790
|
105 |
by (auto simp add: equivp_def expand_fun_eq)
|
|
106 |
|
|
107 |
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>
diff
changeset
|
108 |
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>
diff
changeset
|
109 |
(@{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
|
110 |
@{typ "myint"})
|
790
|
111 |
*}
|
|
112 |
|
|
113 |
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>
diff
changeset
|
114 |
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>
diff
changeset
|
115 |
(@{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
|
116 |
@{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
|
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 {*
|
803
|
120 |
test_funs repF @{context}
|
|
121 |
(@{typ "(('a * 'a) list * 'b)"},
|
|
122 |
@{typ "('a foo * 'b)"})
|
|
123 |
*}
|
|
124 |
|
|
125 |
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>
diff
changeset
|
126 |
test_funs absF @{context}
|
790
|
127 |
(@{typ "(('a list) * int) list"},
|
|
128 |
@{typ "('a fset) bar"})
|
|
129 |
*}
|
|
130 |
|
|
131 |
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>
diff
changeset
|
132 |
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
|
133 |
(@{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
|
134 |
@{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
|
135 |
*}
|
a5495a323b49
added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
136 |
|
a5495a323b49
added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
137 |
ML {*
|
a5495a323b49
added a new version of equiv_relation (is not yet used anywhere except in AbsRepTest)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
138 |
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
|
139 |
(@{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
|
140 |
@{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
|
141 |
*}
|
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
|
142 |
|
808
90bde96f5dd1
proper handling of error messages (code copy - maybe this can be avoided)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
143 |
|
811
|
144 |
ML {*
|
|
145 |
test_funs absF @{context}
|
|
146 |
(@{typ "((nat * nat) list) list"},
|
|
147 |
@{typ "((myint) fset) fset"})
|
|
148 |
*}
|
808
90bde96f5dd1
proper handling of error messages (code copy - maybe this can be avoided)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
149 |
|
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
|
150 |
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
|
151 |
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>
diff
changeset
|
152 |
(@{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
|
153 |
@{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
|
154 |
*}
|
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
|
155 |
|
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
|
156 |
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
|
157 |
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>
diff
changeset
|
158 |
(@{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
|
159 |
@{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
|
160 |
*}
|
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
|
161 |
|
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
|
162 |
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
|
163 |
test_funs absF @{context}
|
796
|
164 |
(@{typ "('a list) list \<Rightarrow> 'a list"},
|
|
165 |
@{typ "('a fset) fset \<Rightarrow> 'a fset"})
|
790
|
166 |
*}
|
|
167 |
|
822
|
168 |
lemma OO_sym_inv:
|
809
|
169 |
assumes sr: "symp r"
|
|
170 |
and ss: "symp s"
|
|
171 |
shows "(r OO s) x y = (s OO r) y x"
|
822
|
172 |
using sr ss
|
|
173 |
unfolding symp_def
|
|
174 |
apply (metis pred_comp.intros pred_compE ss symp_def)
|
|
175 |
done
|
809
|
176 |
|
812
|
177 |
lemma abs_o_rep:
|
|
178 |
assumes a: "Quotient r absf repf"
|
|
179 |
shows "absf o repf = id"
|
|
180 |
apply(rule ext)
|
|
181 |
apply(simp add: Quotient_abs_rep[OF a])
|
822
|
182 |
done
|
812
|
183 |
|
824
|
184 |
lemma set_in_eq: "(\<forall>e. ((e \<in> A) \<longleftrightarrow> (e \<in> B))) \<equiv> A = B"
|
822
|
185 |
apply (rule eq_reflection)
|
|
186 |
apply auto
|
|
187 |
done
|
816
|
188 |
|
822
|
189 |
lemma map_rel_cong: "b \<approx>1 ba \<Longrightarrow> map f b \<approx>1 map f ba"
|
|
190 |
unfolding erel1_def
|
|
191 |
apply(simp only: set_map set_in_eq)
|
|
192 |
done
|
821
|
193 |
|
|
194 |
lemma quotient_compose_list_gen_pre:
|
|
195 |
assumes a: "equivp r2"
|
|
196 |
and b: "Quotient r2 abs2 rep2"
|
852
|
197 |
shows "(list_rel r2 OOO op \<approx>1) r s =
|
|
198 |
((list_rel r2 OOO op \<approx>1) r r \<and> (list_rel r2 OOO op \<approx>1) s s \<and>
|
821
|
199 |
abs_fset (map abs2 r) = abs_fset (map abs2 s))"
|
822
|
200 |
apply rule
|
|
201 |
apply rule
|
|
202 |
apply rule
|
|
203 |
apply (rule list_rel_refl)
|
|
204 |
apply (metis equivp_def a)
|
|
205 |
apply rule
|
|
206 |
apply (rule equivp_reflp[OF fset_equivp])
|
|
207 |
apply (rule list_rel_refl)
|
|
208 |
apply (metis equivp_def a)
|
|
209 |
apply(rule)
|
|
210 |
apply rule
|
|
211 |
apply (rule list_rel_refl)
|
|
212 |
apply (metis equivp_def a)
|
|
213 |
apply rule
|
|
214 |
apply (rule equivp_reflp[OF fset_equivp])
|
|
215 |
apply (rule list_rel_refl)
|
|
216 |
apply (metis equivp_def a)
|
|
217 |
apply (subgoal_tac "map abs2 r \<approx>1 map abs2 s")
|
|
218 |
apply (metis Quotient_rel[OF Quotient_fset])
|
|
219 |
apply (auto)[1]
|
|
220 |
apply (subgoal_tac "map abs2 r = map abs2 b")
|
|
221 |
prefer 2
|
|
222 |
apply (metis Quotient_rel[OF list_quotient[OF b]])
|
|
223 |
apply (subgoal_tac "map abs2 s = map abs2 ba")
|
|
224 |
prefer 2
|
|
225 |
apply (metis Quotient_rel[OF list_quotient[OF b]])
|
|
226 |
apply (simp add: map_rel_cong)
|
|
227 |
apply rule
|
|
228 |
apply (rule rep_abs_rsp[of "list_rel r2" "map abs2"])
|
|
229 |
apply (rule list_quotient)
|
|
230 |
apply (rule b)
|
|
231 |
apply (rule list_rel_refl)
|
|
232 |
apply (metis equivp_def a)
|
|
233 |
apply rule
|
|
234 |
prefer 2
|
|
235 |
apply (rule rep_abs_rsp_left[of "list_rel r2" "map abs2"])
|
|
236 |
apply (rule list_quotient)
|
|
237 |
apply (rule b)
|
|
238 |
apply (rule list_rel_refl)
|
|
239 |
apply (metis equivp_def a)
|
|
240 |
apply (erule conjE)+
|
|
241 |
apply (subgoal_tac "map abs2 r \<approx>1 map abs2 s")
|
|
242 |
apply (rule map_rel_cong)
|
|
243 |
apply (assumption)
|
|
244 |
apply (metis Quotient_def Quotient_fset equivp_reflp fset_equivp a b)
|
|
245 |
done
|
821
|
246 |
|
820
|
247 |
lemma quotient_compose_list_gen:
|
821
|
248 |
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
|
249 |
and b: "equivp r2" (* reflp is not enough *)
|
852
|
250 |
shows "Quotient ((list_rel r2) OOO (op \<approx>1))
|
811
|
251 |
(abs_fset \<circ> (map abs2)) ((map rep2) \<circ> rep_fset)"
|
812
|
252 |
unfolding Quotient_def comp_def
|
822
|
253 |
apply (rule)+
|
|
254 |
apply (simp add: abs_o_rep[OF a] id_simps Quotient_abs_rep[OF Quotient_fset])
|
|
255 |
apply (rule)
|
|
256 |
apply (rule)
|
|
257 |
apply (rule)
|
|
258 |
apply (rule list_rel_refl)
|
|
259 |
apply (metis b equivp_def)
|
|
260 |
apply (rule)
|
|
261 |
apply (rule equivp_reflp[OF fset_equivp])
|
|
262 |
apply (rule list_rel_refl)
|
|
263 |
apply (metis b equivp_def)
|
|
264 |
apply rule
|
|
265 |
apply rule
|
|
266 |
apply(rule quotient_compose_list_gen_pre[OF b a])
|
|
267 |
done
|
809
|
268 |
|
821
|
269 |
(* This is the general statement but the types of abs2 and rep2
|
|
270 |
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
|
271 |
lemma quotient_compose_general:
|
821
|
272 |
assumes a2: "Quotient r1 abs1 rep1"
|
810
|
273 |
and "Quotient r2 abs2 rep2"
|
852
|
274 |
shows "Quotient ((list_rel r2) OOO r1)
|
821
|
275 |
(abs1 \<circ> (map abs2)) ((map rep2) \<circ> rep1)"
|
810
|
276 |
sorry
|
|
277 |
|
822
|
278 |
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
|
279 |
thm quotient_compose_general[OF Quotient_fset]
|
817
|
280 |
(* Doesn't work: *)
|
818
9ab49dc166d6
More cleaning and commenting AbsRepTest. Now tests work; just slow.
Cezary Kaliszyk <kaliszyk@in.tum.de>
diff
changeset
|
281 |
(* 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
|
282 |
|
809
|
283 |
end
|