140 val t_t2 = |
140 val t_t2 = |
141 Toplevel.program (fn () => |
141 Toplevel.program (fn () => |
142 repabs_eq2 @{context} (g, thm, othm) |
142 repabs_eq2 @{context} (g, thm, othm) |
143 ) |
143 ) |
144 *} |
144 *} |
145 ML {* |
|
146 val lpi = Drule.instantiate' |
|
147 [SOME @{ctyp "nat \<times> nat"}, NONE, SOME @{ctyp "bool"}, NONE] [] @{thm LAMBDA_PRS}; |
|
148 *} |
|
149 prove lambda_prs_mn_b : {* concl_of lpi *} |
|
150 apply (tactic {* compose_tac (false, @{thm LAMBDA_PRS}, 2) 1 *}) |
|
151 apply (tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *}) |
|
152 apply (tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *}) |
|
153 done |
|
154 |
145 |
155 ML {* |
146 ML {* |
156 fun make_simp_lam_prs_thm lthy quot_thm typ = |
147 fun make_simp_lam_prs_thm lthy quot_thm typ = |
157 let |
148 let |
158 val (_, [lty, rty]) = dest_Type typ; |
149 val (_, [lty, rty]) = dest_Type typ; |
164 (compose_tac (false, @{thm LAMBDA_PRS}, 2)) THEN_ALL_NEW |
155 (compose_tac (false, @{thm LAMBDA_PRS}, 2)) THEN_ALL_NEW |
165 (quotient_tac quot_thm); |
156 (quotient_tac quot_thm); |
166 val t = Goal.prove lthy [] [] (concl_of lpi) (fn _ => tac 1); |
157 val t = Goal.prove lthy [] [] (concl_of lpi) (fn _ => tac 1); |
167 val ts = @{thm HOL.sym} OF [t] |
158 val ts = @{thm HOL.sym} OF [t] |
168 in |
159 in |
169 MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_def}] ts |
160 MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] ts |
170 end |
161 end |
171 *} |
162 *} |
172 |
163 |
173 |
164 |
174 |
165 thm id_apply |
175 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm plus_sym_pre})) *} |
166 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm plus_sym_pre})) *} |
176 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *} |
167 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *} |
177 thm HOL.sym[OF lambda_prs_mn_b,simplified] |
168 thm HOL.sym[OF lambda_prs_mn_b,simplified] |
178 |
169 |
179 ML {* |
170 ML {* |
180 fun simp_lam_prs lthy thm = |
171 fun simp_lam_prs lthy thm = |
181 simp_lam_prs lthy (eqsubst_thm lthy |
172 simp_lam_prs lthy (eqsubst_thm lthy simp_lam_prs_thms thm) |
182 @{thms HOL.sym[OF lambda_prs_mn_b,simplified]} |
|
183 thm) |
|
184 handle _ => thm |
173 handle _ => thm |
185 *} |
174 *} |
186 ML {* t_t2 *} |
175 ML {* t_t2 *} |
187 ML {* val t_l = simp_lam_prs @{context} t_t2 *} |
176 ML {* val t_l = simp_lam_prs @{context} t_t2 *} |
188 ML {* findabs rty (prop_of (atomize_thm @{thm plus_sym_pre})) *} |
|
189 |
177 |
190 ML {* |
178 ML {* |
191 fun simp_allex_prs lthy thm = |
179 fun simp_allex_prs lthy thm = |
192 let |
180 let |
193 val rwf = @{thm FORALL_PRS[OF QUOTIENT_my_int]}; |
181 val rwf = @{thm FORALL_PRS[OF QUOTIENT_my_int]}; |