1 theory IntEx |
1 theory IntEx |
2 imports QuotMain |
2 imports QuotMain |
3 begin |
3 begin |
4 |
4 |
5 fun |
5 fun |
6 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" |
6 intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool" |
7 where |
7 where |
8 "intrel (x, y) (u, v) = (x + v = u + y)" |
8 "intrel (x, y) (u, v) = (x + v = u + y)" |
9 |
9 |
10 quotient my_int = "nat \<times> nat" / intrel |
10 quotient my_int = "nat \<times> nat" / intrel |
11 apply(unfold EQUIV_def) |
11 apply(unfold EQUIV_def) |
166 text {* Below is the construction site code used if things do now work *} |
166 text {* Below is the construction site code used if things do now work *} |
167 |
167 |
168 ML {* val t_a = atomize_thm @{thm plus_assoc_pre} *} |
168 ML {* val t_a = atomize_thm @{thm plus_assoc_pre} *} |
169 ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *} |
169 ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *} |
170 |
170 |
171 ML {* val (g, thm, othm) = |
171 ML {* val t_t = |
172 Toplevel.program (fn () => |
172 Toplevel.program (fn () => |
173 repabs_eq @{context} t_r consts rty qty |
173 repabs @{context} t_r consts rty qty |
174 quot rel_refl trans2 |
174 quot rel_refl trans2 |
175 rsp_thms |
175 rsp_thms |
176 ) |
176 ) |
177 *} |
177 *} |
178 ML {* |
|
179 val t_t2 = |
|
180 Toplevel.program (fn () => |
|
181 repabs_eq2 @{context} (g, thm, othm) |
|
182 ) |
|
183 *} |
|
184 |
|
185 |
178 |
186 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm plus_sym_pre})) *} |
179 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm plus_sym_pre})) *} |
|
180 |
187 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *} |
181 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *} |
188 |
182 |
189 ML {* |
183 ML {* |
190 fun simp_lam_prs lthy thm = |
184 fun simp_lam_prs lthy thm = |
191 simp_lam_prs lthy (eqsubst_thm lthy simp_lam_prs_thms thm) |
185 simp_lam_prs lthy (eqsubst_thm lthy simp_lam_prs_thms thm) |
192 handle _ => thm |
186 handle _ => thm |
193 *} |
187 *} |
194 ML {* t_t2 *} |
188 ML {* t_t *} |
195 ML {* val t_l = simp_lam_prs @{context} t_t2 *} |
189 ML {* val t_l = simp_lam_prs @{context} t_t *} |
196 |
190 |
197 ML {* val t_a = simp_allex_prs @{context} quot t_l *} |
191 ML {* val t_a = simp_allex_prs @{context} quot t_l *} |
198 |
192 |
199 ML {* val t_defs_sym = add_lower_defs @{context} t_defs *} |
193 ML {* val t_defs_sym = add_lower_defs @{context} t_defs *} |
200 ML {* val t_d = MetaSimplifier.rewrite_rule t_defs_sym t_a *} |
194 ML {* val t_d = MetaSimplifier.rewrite_rule t_defs_sym t_a *} |