equal
deleted
inserted
replaced
130 ML {* val rel_eqv = @{thm equiv_intrel} *} |
130 ML {* val rel_eqv = @{thm equiv_intrel} *} |
131 ML {* val rel_refl = @{thm intrel_refl} *} |
131 ML {* val rel_refl = @{thm intrel_refl} *} |
132 ML {* val quot = @{thm QUOTIENT_my_int} *} |
132 ML {* val quot = @{thm QUOTIENT_my_int} *} |
133 ML {* val rsp_thms = @{thms ho_plus_rsp} @ @{thms ho_all_prs ho_ex_prs} *} |
133 ML {* val rsp_thms = @{thms ho_plus_rsp} @ @{thms ho_all_prs ho_ex_prs} *} |
134 ML {* val trans2 = @{thm QUOT_TYPE_I_my_int.R_trans2} *} |
134 ML {* val trans2 = @{thm QUOT_TYPE_I_my_int.R_trans2} *} |
|
135 ML {* val reps_same = @{thm QUOT_TYPE_I_my_int.REPS_same} *} |
|
136 ML {* val t_defs = @{thms PLUS_def} *} |
|
137 |
|
138 |
135 |
139 |
136 ML {* val t_a = atomize_thm @{thm plus_sym_pre} *} |
140 ML {* val t_a = atomize_thm @{thm plus_sym_pre} *} |
137 ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *} |
141 ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *} |
138 |
142 |
139 ML {* val (g, thm, othm) = |
143 ML {* val (g, thm, othm) = |
148 Toplevel.program (fn () => |
152 Toplevel.program (fn () => |
149 repabs_eq2 @{context} (g, thm, othm) |
153 repabs_eq2 @{context} (g, thm, othm) |
150 ) |
154 ) |
151 *} |
155 *} |
152 |
156 |
153 ML {* |
|
154 fun make_simp_lam_prs_thm lthy quot_thm typ = |
|
155 let |
|
156 val (_, [lty, rty]) = dest_Type typ; |
|
157 val thy = ProofContext.theory_of lthy; |
|
158 val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty) |
|
159 val inst = [SOME lcty, NONE, SOME rcty]; |
|
160 val lpi = Drule.instantiate' inst [] @{thm LAMBDA_PRS}; |
|
161 val tac = |
|
162 (compose_tac (false, @{thm LAMBDA_PRS}, 2)) THEN_ALL_NEW |
|
163 (quotient_tac quot_thm); |
|
164 val t = Goal.prove lthy [] [] (concl_of lpi) (fn _ => tac 1); |
|
165 val ts = @{thm HOL.sym} OF [t] |
|
166 in |
|
167 MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] ts |
|
168 end |
|
169 *} |
|
170 |
|
171 |
157 |
172 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm plus_sym_pre})) *} |
158 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm plus_sym_pre})) *} |
173 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *} |
159 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *} |
174 |
160 |
175 ML {* |
161 ML {* |
178 handle _ => thm |
164 handle _ => thm |
179 *} |
165 *} |
180 ML {* t_t2 *} |
166 ML {* t_t2 *} |
181 ML {* val t_l = simp_lam_prs @{context} t_t2 *} |
167 ML {* val t_l = simp_lam_prs @{context} t_t2 *} |
182 |
168 |
183 ML {* |
|
184 fun simp_allex_prs lthy quot thm = |
|
185 let |
|
186 val rwf = @{thm FORALL_PRS} OF [quot]; |
|
187 val rwfs = @{thm "HOL.sym"} OF [rwf]; |
|
188 val rwe = @{thm EXISTS_PRS} OF [quot]; |
|
189 val rwes = @{thm "HOL.sym"} OF [rwe] |
|
190 in |
|
191 (simp_allex_prs lthy quot (eqsubst_thm lthy [rwfs, rwes] thm)) |
|
192 end |
|
193 handle _ => thm |
|
194 *} |
|
195 |
|
196 ML {* val t_a = simp_allex_prs @{context} quot t_l *} |
169 ML {* val t_a = simp_allex_prs @{context} quot t_l *} |
197 |
170 |
198 ML {* val t_defs = @{thms PLUS_def} *} |
|
199 ML {* val t_defs_sym = add_lower_defs @{context} t_defs *} |
171 ML {* val t_defs_sym = add_lower_defs @{context} t_defs *} |
200 ML {* val t_d = MetaSimplifier.rewrite_rule t_defs_sym t_a *} |
172 ML {* val t_d = MetaSimplifier.rewrite_rule t_defs_sym t_a *} |
201 ML {* val t_r = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_my_int.REPS_same} t_d *} |
173 ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *} |
202 ML {* ObjectLogic.rulify t_r *} |
174 ML {* ObjectLogic.rulify t_r *} |
203 |
175 |
204 lemma |
176 lemma |
205 fixes i j k::"my_int" |
177 fixes i j k::"my_int" |
206 shows "(PLUS (PLUS i j) k) = (PLUS i (PLUS j k))" |
178 shows "(PLUS (PLUS i j) k) = (PLUS i (PLUS j k))" |