205 |
213 |
206 (* It is just a test, it doesn't seem true... *) |
214 (* It is just a test, it doesn't seem true... *) |
207 lemma quotient_cheat: "QUOTIENT op = (option_map ABS_lam) (option_map REP_lam)" |
215 lemma quotient_cheat: "QUOTIENT op = (option_map ABS_lam) (option_map REP_lam)" |
208 sorry |
216 sorry |
209 |
217 |
210 |
|
211 ML {* val rsp_thms = @{thms abs_fun_rsp OPT_QUOTIENT eq_rsp2 quotient_cheat perm_rsp_eq fresh_rsp_eq} @ rsp_thms *} |
218 ML {* val rsp_thms = @{thms abs_fun_rsp OPT_QUOTIENT eq_rsp2 quotient_cheat perm_rsp_eq fresh_rsp_eq} @ rsp_thms *} |
212 ML {* |
219 ML {* |
213 fun lift_thm_lam lthy t = |
220 fun lift_thm_lam lthy t = |
214 lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same defs t |
221 lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same defs t |
215 *} |
222 *} |
216 |
223 |
217 thm a3 |
224 thm a3 |
218 ML {* Toplevel.program (fn () => lift_thm_lam @{context} @{thm a3}) *} |
225 ML {* Toplevel.program (fn () => lift_thm_lam @{context} @{thm a3}) *} |
219 ML {* val t_u = MetaSimplifier.rewrite_rule @{thms fresh_def supp_def} @{thm a3} *} |
226 thm a3 |
220 ML {* Toplevel.program (fn () => lift_thm_lam @{context} t_u) *} |
227 ML {* val t_u1 = eqsubst_thm @{context} @{thms abs_fresh(1)} (atomize_thm @{thm a3}) *} |
221 |
228 ML {* val t_u = MetaSimplifier.rewrite_rule @{thms fresh_def supp_def} t_u1 *} |
222 ML t_u |
229 |
223 ML {* val t_a = atomize_thm t_u *} |
230 ML {* val t_a = atomize_thm t_u *} |
224 ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *} |
231 ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *} |
225 ML {* val t = (fst o Thm.dest_comb o snd o Thm.dest_comb) (cprop_of t_u) *} |
232 ML {* fun r_mk_comb_tac_lam ctxt = |
226 ML {* val t = (snd o Thm.dest_comb o snd o Thm.dest_comb) t *} |
233 r_mk_comb_tac ctxt rty quot rel_refl trans2 rsp_thms |
227 ML {* val t = (snd o Thm.dest_comb o snd o Thm.dest_comb) t *} |
234 *} |
228 ML {* val t = (snd o (Thm.dest_abs NONE) o snd o Thm.dest_comb) t *} |
235 |
229 ML {* val t = (snd o Thm.dest_comb o snd o Thm.dest_comb) t *} |
236 instance lam :: fs_name |
230 ML {* val t = (snd o (Thm.dest_abs NONE) o snd o Thm.dest_comb) t *} |
237 apply(intro_classes) |
231 ML {* val t = (fst o Thm.dest_comb o snd o Thm.dest_comb) t *} |
238 sorry |
232 ML {* term_of t *} |
239 |
233 term "[b].(s::rlam)" |
240 prove asdf: {* Logic.mk_implies (concl_of t_r, (@{term "Trueprop (\<forall>t\<Colon>rlam\<in>Respects |
234 thm abs_fun_def |
241 alpha. |
235 ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *} |
242 \<forall>(a\<Colon>name) b\<Colon>name. |
236 |
243 \<forall>s\<Colon>rlam\<in>Respects |
|
244 alpha. |
|
245 t \<approx> ([(a, |
|
246 b)] \<bullet> s) \<longrightarrow> |
|
247 a = b \<or> |
|
248 a |
|
249 \<notin> {a\<Colon>name. |
|
250 infinite |
|
251 {b\<Colon>name. Not |
|
252 (([(a, b)] \<bullet> |
|
253 s) \<approx> |
|
254 s)}} \<longrightarrow> |
|
255 rLam a |
|
256 t \<approx> rLam |
|
257 b s)"})) *} |
|
258 apply (tactic {* full_simp_tac ((Simplifier.context @{context} HOL_ss) addsimps |
|
259 [(@{thm equiv_res_forall} OF [rel_eqv]), |
|
260 (@{thm equiv_res_exists} OF [rel_eqv])]) 1 *}) |
|
261 apply (rule allI) |
|
262 apply (drule_tac x="t" in spec) |
|
263 apply (rule allI) |
|
264 apply (drule_tac x="a" in spec) |
|
265 apply (rule allI) |
|
266 apply (drule_tac x="b" in spec) |
|
267 apply (rule allI) |
|
268 apply (drule_tac x="s" in spec) |
|
269 apply (rule impI) |
|
270 apply (drule_tac mp) |
|
271 apply (simp) |
|
272 apply (simp) |
|
273 apply (rule impI) |
|
274 apply (rule a3) |
|
275 apply (simp) |
|
276 apply (simp add: abs_fresh(1)) |
|
277 apply (case_tac "a = b") |
|
278 apply (simp) |
|
279 apply (simp) |
|
280 apply (auto) |
|
281 apply (unfold fresh_def) |
|
282 apply (unfold supp_def) |
|
283 apply (simp) |
|
284 prefer 2 |
|
285 apply (simp) |
|
286 sorry |
|
287 |
|
288 ML {* val abs = findabs rty (prop_of t_a) *} |
|
289 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *} |
|
290 ML {* val t_defs_sym = add_lower_defs @{context} defs *} |
|
291 |
|
292 ML {* val t_r' = @{thm asdf} OF [t_r] *} |
|
293 ML {* val t_t = repabs @{context} t_r' consts rty qty quot rel_refl trans2 rsp_thms *} |
|
294 ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_t *} |
|
295 ML {* val t_a = simp_allex_prs @{context} quot t_l *} |
|
296 ML {* val t_d = repeat_eqsubst_thm @{context} t_defs_sym t_a *} |
|
297 ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *} |
|
298 ML {* val tt = MetaSimplifier.rewrite_rule [symmetric @{thm supp_def}, symmetric @{thm fresh_def}] t_r *} |
|
299 ML {* val rr = @{thm sym} OF @{thms abs_fresh(1)} *} |
|
300 ML {* val ttt = eqsubst_thm @{context} [rr] tt *} |
|
301 ML {* ObjectLogic.rulify ttt *} |
|
302 |
|
303 lemma |
|
304 assumes a: "a \<notin> {a\<Colon>name. infinite {b\<Colon>name. \<not> ([(a, b)] \<bullet> s) \<approx> s}}" |
|
305 shows "a \<notin> {a\<Colon>name. infinite {b\<Colon>name. [(a, b)] \<bullet> s \<noteq> s}}" |
|
306 using a apply simp |
|
307 sorry (* Not true... *) |