257 done |
262 done |
258 |
263 |
259 thm list.induct |
264 thm list.induct |
260 lemma list_induct_hol4: |
265 lemma list_induct_hol4: |
261 fixes P :: "'a list \<Rightarrow> bool" |
266 fixes P :: "'a list \<Rightarrow> bool" |
262 assumes "((P []) \<and> (\<forall>t. (P t) \<longrightarrow> (\<forall>h. (P (h # t)))))" |
267 assumes a: "((P []) \<and> (\<forall>t. (P t) \<longrightarrow> (\<forall>h. (P (h # t)))))" |
263 shows "(\<forall>l. (P l))" |
268 shows "\<forall>l. (P l)" |
264 sorry |
269 using a |
265 |
270 apply (rule_tac allI) |
266 ML {* atomize_thm @{thm list_induct_hol4} *} |
271 apply (induct_tac "l") |
|
272 apply (simp) |
|
273 apply (metis) |
|
274 done |
|
275 |
|
276 ML {* |
|
277 fun regularize thm rty rel rel_eqv lthy = |
|
278 let |
|
279 val g = build_regularize_goal thm rty rel lthy; |
|
280 val tac = |
|
281 (simp_tac ((Simplifier.context lthy HOL_ss) addsimps |
|
282 [(@{thm equiv_res_forall} OF [rel_eqv]), |
|
283 (@{thm equiv_res_exists} OF [rel_eqv])])) THEN' |
|
284 (rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' |
|
285 (RANGE [fn _ => all_tac, atac]) THEN' (MetisTools.metis_tac lthy []); |
|
286 val cgoal = cterm_of (ProofContext.theory_of lthy) g; |
|
287 val cthm = Goal.prove_internal [] cgoal (fn _ => tac 1); |
|
288 in |
|
289 cthm OF [thm] |
|
290 end |
|
291 *} |
|
292 |
267 |
293 |
268 prove list_induct_r: {* |
294 prove list_induct_r: {* |
269 build_regularize_goal (atomize_thm @{thm list_induct_hol4}) @{typ "'a List.list"} @{term "op \<approx>"} @{context} *} |
295 build_regularize_goal (atomize_thm @{thm list_induct_hol4}) @{typ "'a List.list"} @{term "op \<approx>"} @{context} *} |
270 apply (simp only: equiv_res_forall[OF equiv_list_eq]) |
296 apply (simp only: equiv_res_forall[OF equiv_list_eq]) |
271 thm RIGHT_RES_FORALL_REGULAR |
297 thm RIGHT_RES_FORALL_REGULAR |
312 (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN' |
346 (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN' |
313 (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI}) |
347 (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI}) |
314 | _ => fn _ => no_tac) i st |
348 | _ => fn _ => no_tac) i st |
315 *} |
349 *} |
316 |
350 |
317 |
351 ML {* |
318 ML {* |
352 fun WEAK_LAMBDA_RES_TAC ctxt i st = |
319 fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm res_thms = |
353 (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of |
|
354 (_ $ (_ $ _$(Abs(_,_,_)))) => |
|
355 (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN' |
|
356 (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI}) |
|
357 | (_ $ (_ $ (Abs(_,_,_))$_)) => |
|
358 (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN' |
|
359 (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI}) |
|
360 | _ => fn _ => no_tac) i st |
|
361 *} |
|
362 |
|
363 |
|
364 ML {* |
|
365 fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm rsp_thms = |
320 (FIRST' [ |
366 (FIRST' [ |
321 rtac @{thm FUN_QUOTIENT}, |
367 rtac @{thm FUN_QUOTIENT}, |
322 rtac quot_thm, |
368 rtac quot_thm, |
323 rtac @{thm IDENTITY_QUOTIENT}, |
369 rtac @{thm IDENTITY_QUOTIENT}, |
324 rtac @{thm ext}, |
370 rtac @{thm ext}, |
325 rtac trans_thm, |
371 rtac trans_thm, |
326 LAMBDA_RES_TAC ctxt, |
372 LAMBDA_RES_TAC ctxt, |
327 res_forall_rsp_tac ctxt, |
373 res_forall_rsp_tac ctxt, |
|
374 res_exists_rsp_tac ctxt, |
328 ( |
375 ( |
329 (simp_tac ((Simplifier.context @{context} HOL_ss) addsimps (res_thms @ @{thms ho_all_prs}))) |
376 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps (rsp_thms @ @{thms ho_all_prs ho_ex_prs}))) |
330 THEN_ALL_NEW (fn _ => no_tac) |
377 THEN_ALL_NEW (fn _ => no_tac) |
331 ), |
378 ), |
332 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])), |
379 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])), |
333 rtac refl, |
380 rtac refl, |
334 (instantiate_tac @{thm APPLY_RSP} ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])), |
381 (instantiate_tac @{thm APPLY_RSP} ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])), |
335 rtac reflex_thm, |
382 rtac reflex_thm, |
336 atac, |
383 atac, |
337 ( |
384 ( |
338 (simp_tac ((Simplifier.context @{context} HOL_ss) addsimps @{thms FUN_REL.simps})) |
385 (simp_tac ((Simplifier.context @{context} HOL_ss) addsimps @{thms FUN_REL.simps})) |
339 THEN_ALL_NEW (fn _ => no_tac) |
386 THEN_ALL_NEW (fn _ => no_tac) |
340 ) |
387 ), |
|
388 WEAK_LAMBDA_RES_TAC ctxt |
341 ]) |
389 ]) |
342 *} |
390 *} |
343 |
391 |
|
392 ML Goal.prove |
|
393 |
|
394 ML {* |
|
395 fun repabs lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms = |
|
396 let |
|
397 val rt = build_repabs_term lthy thm constructors rty qty; |
|
398 val rg = Logic.mk_equals ((Thm.prop_of thm), rt); |
|
399 fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN' |
|
400 (REPEAT_ALL_NEW (r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm rsp_thms)); |
|
401 val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1); |
|
402 (* val tac2 = |
|
403 (simp_tac ((Simplifier.context lthy HOL_ss) addsimps [cthm])) |
|
404 THEN' (rtac thm); |
|
405 val cgoal = cterm_of (ProofContext.theory_of lthy) rt; |
|
406 val cthm = Goal.prove_internal [] cgoal (fn _ => tac2); *) |
|
407 in |
|
408 cthm |
|
409 end |
|
410 *} |
|
411 |
344 ML {* |
412 ML {* |
345 fun r_mk_comb_tac_fset ctxt = |
413 fun r_mk_comb_tac_fset ctxt = |
346 r_mk_comb_tac ctxt @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} @{thms ho_memb_rsp ho_cons_rsp} |
414 r_mk_comb_tac ctxt @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp} |
347 *} |
415 *} |
348 |
416 |
349 |
417 |
350 ML {* val thm = @{thm list_induct_r} OF [atomize_thm @{thm list_induct_hol4}] *} |
418 ML {* val thm = @{thm list_induct_r} OF [atomize_thm @{thm list_induct_hol4}] *} |
351 ML {* val trm_r = build_repabs_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
419 ML {* val trm_r = build_repabs_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
352 ML {* val trm = build_repabs_term @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
420 ML {* val trm = build_repabs_term @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
353 |
421 |
354 ML {* trm_r *} |
422 ML {* trm_r *} |
355 prove list_induct_tr: trm_r |
423 prove list_induct_tr: trm_r |
356 apply (atomize(full)) |
424 apply (atomize(full)) |
357 (* APPLY_RSP_TAC *) |
|
358 ML_prf {* val ctxt = @{context} *} |
|
359 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
360 (* LAMBDA_RES_TAC *) |
|
361 apply (subst FUN_REL.simps) |
|
362 apply (rule allI) |
|
363 apply (rule allI) |
|
364 apply (rule impI) |
|
365 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
425 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
366 done |
426 done |
367 |
427 |
368 prove list_induct_t: trm |
428 prove list_induct_t: trm |
369 apply (simp only: list_induct_tr[symmetric]) |
429 apply (simp only: list_induct_tr[symmetric]) |
370 apply (tactic {* rtac thm 1 *}) |
430 apply (tactic {* rtac thm 1 *}) |
371 done |
431 done |
372 |
432 |
373 ML {* val nthm = MetaSimplifier.rewrite_rule fset_defs_sym (snd (no_vars (Context.Theory @{theory}, @{thm list_induct_t}))) *} |
433 ML {* val ind_r_a = atomize_thm @{thm list_induct_hol4} *} |
|
434 ML {* val ind_r_r = regularize ind_r_a @{typ "'a List.list"} @{term "op \<approx>"} @{thm equiv_list_eq} @{context} *} |
|
435 ML {* val ind_r_t = |
|
436 repabs @{context} ind_r_r consts @{typ "'a list"} @{typ "'a fset"} |
|
437 @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
|
438 @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp} |
|
439 *} |
374 |
440 |
375 thm list.recs(2) |
441 thm list.recs(2) |
|
442 |
376 thm m2 |
443 thm m2 |
377 ML {* atomize_thm @{thm m2} *} |
444 ML {* atomize_thm @{thm m2} *} |
378 |
445 |
379 prove m2_r_p: {* |
446 prove m2_r_p: {* |
380 build_regularize_goal (atomize_thm @{thm m2}) @{typ "'a List.list"} @{term "op \<approx>"} @{context} *} |
447 build_regularize_goal (atomize_thm @{thm m2}) @{typ "'a List.list"} @{term "op \<approx>"} @{context} *} |
395 done |
462 done |
396 |
463 |
397 lemma id_apply2 [simp]: "id x \<equiv> x" |
464 lemma id_apply2 [simp]: "id x \<equiv> x" |
398 by (simp add: id_def) |
465 by (simp add: id_def) |
399 |
466 |
400 thm LAMBDA_PRS |
|
401 ML {* |
467 ML {* |
402 val t = prop_of @{thm LAMBDA_PRS} |
468 val t = prop_of @{thm LAMBDA_PRS} |
403 val tt = Drule.instantiate' [SOME @{ctyp "'a list"}, SOME @{ctyp "'a fset"}] [] @{thm LAMBDA_PRS} |
469 val tt = Drule.instantiate' [SOME @{ctyp "'a list"}, SOME @{ctyp "'a fset"}, SOME @{ctyp "bool"}, SOME @{ctyp "bool"}] [] @{thm LAMBDA_PRS} |
404 val ttt = @{thm LAMBDA_PRS} OF [@{thm QUOTIENT_fset}, @{thm IDENTITY_QUOTIENT}] |
470 val ttt = @{thm LAMBDA_PRS} OF [@{thm QUOTIENT_fset}, @{thm IDENTITY_QUOTIENT}] |
405 val tttt = @{thm "HOL.sym"} OF [ttt] |
471 val tttt = @{thm "HOL.sym"} OF [ttt] |
406 *} |
472 *} |
407 ML {* |
473 ML {* |
408 val ttttt = MetaSimplifier.rewrite_rule [@{thm id_apply2}] tttt |
474 val ttttt = MetaSimplifier.rewrite_rule [@{thm id_apply2}] tttt |
409 val zzz = @{thm m2_t} |
475 val zzz = @{thm m2_t} |
410 *} |
476 *} |
|
477 prove asdfasdf : {* concl_of tt *} |
|
478 apply (tactic {* compose_tac (false, @{thm LAMBDA_PRS}, 2) 1 *}) |
|
479 apply (tactic {* quotient_tac @{thm QUOTIENT_fset} 1 *}) |
|
480 apply (tactic {* quotient_tac @{thm QUOTIENT_fset} 1 *}) |
|
481 done |
|
482 |
|
483 thm HOL.sym[OF asdfasdf,simplified] |
411 |
484 |
412 ML {* |
485 ML {* |
413 fun eqsubst_thm ctxt thms thm = |
486 fun eqsubst_thm ctxt thms thm = |
414 let |
487 let |
415 val goalstate = Goal.init (Thm.cprop_of thm) |
488 val goalstate = Goal.init (Thm.cprop_of thm) |
421 val rt = Toplevel.program (fn () => Goal.prove_internal [] cgoal (fn _ => tac)); |
494 val rt = Toplevel.program (fn () => Goal.prove_internal [] cgoal (fn _ => tac)); |
422 in |
495 in |
423 Simplifier.rewrite_rule [rt] thm |
496 Simplifier.rewrite_rule [rt] thm |
424 end |
497 end |
425 *} |
498 *} |
426 ML {* val m2_t' = eqsubst_thm @{context} [ttttt] @{thm m2_t} *} |
499 ML ttttt |
|
500 ML {* val m2_t' = eqsubst_thm @{context} @{thms HOL.sym[OF asdfasdf,simplified]} @{thm m2_t} *} |
427 ML {* val rwr = @{thm FORALL_PRS[OF QUOTIENT_fset]} *} |
501 ML {* val rwr = @{thm FORALL_PRS[OF QUOTIENT_fset]} *} |
428 ML {* val rwrs = @{thm "HOL.sym"} OF [ObjectLogic.rulify rwr] *} |
502 ML {* val rwrs = @{thm "HOL.sym"} OF [spec OF [rwr]] *} |
429 ML {* val ithm = eqsubst_thm @{context} [rwrs] m2_t' *} |
503 ML {* val ithm = eqsubst_thm @{context} [rwrs] m2_t' *} |
430 ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *} |
504 ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym ithm *} |
431 ML {* ObjectLogic.rulify rthm *} |
505 ML {* ObjectLogic.rulify rthm *} |
432 |
506 |
433 |
507 |
434 ML {* val card1_suc_f = Thm.freezeT (atomize_thm @{thm card1_suc}) *} |
508 ML {* val card1_suc_f = Thm.freezeT (atomize_thm @{thm card1_suc}) *} |
435 |
509 |
436 prove card1_suc_r: {* |
510 prove card1_suc_r_p: {* |
437 Logic.mk_implies |
511 build_regularize_goal (atomize_thm @{thm card1_suc}) @{typ "'a List.list"} @{term "op \<approx>"} @{context} *} |
438 ((prop_of card1_suc_f), |
|
439 (regularise (prop_of card1_suc_f) @{typ "'a List.list"} @{term "op \<approx>"} @{context})) *} |
|
440 apply (simp add: equiv_res_forall[OF equiv_list_eq] equiv_res_exists[OF equiv_list_eq]) |
512 apply (simp add: equiv_res_forall[OF equiv_list_eq] equiv_res_exists[OF equiv_list_eq]) |
441 done |
513 done |
442 |
514 |
443 ML {* @{thm card1_suc_r} OF [card1_suc_f] *} |
515 ML {* val card1_suc_r = @{thm card1_suc_r_p} OF [atomize_thm @{thm card1_suc}] *} |
|
516 ML {* val card1_suc_t_g = build_repabs_goal @{context} card1_suc_r consts @{typ "'a list"} @{typ "'a fset"} *} |
|
517 ML {* val card1_suc_t = build_repabs_term @{context} card1_suc_r consts @{typ "'a list"} @{typ "'a fset"} *} |
|
518 prove card1_suc_t_p: card1_suc_t_g |
|
519 apply (atomize(full)) |
|
520 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
521 done |
|
522 |
|
523 prove card1_suc_t: card1_suc_t |
|
524 apply (simp only: card1_suc_t_p[symmetric]) |
|
525 apply (tactic {* rtac card1_suc_r 1 *}) |
|
526 done |
|
527 |
|
528 |
|
529 ML {* val card1_suc_t_n = @{thm card1_suc_t} *} |
|
530 ML {* val card1_suc_t' = eqsubst_thm @{context} @{thms HOL.sym[OF asdfasdf,simplified]} @{thm card1_suc_t} *} |
|
531 ML {* val card1_suc_t'' = eqsubst_thm @{context} @{thms HOL.sym[OF asdfasdf,simplified]} card1_suc_t' *} |
|
532 ML {* val ithm = eqsubst_thm @{context} [rwrs] card1_suc_t'' *} |
|
533 ML {* val rwr = @{thm EXISTS_PRS[OF QUOTIENT_fset]} *} |
|
534 ML {* val rwrs = @{thm "HOL.sym"} OF [spec OF [rwr]] *} |
|
535 ML {* val jthm = eqsubst_thm @{context} [rwrs] ithm *} |
|
536 ML {* val rthm = MetaSimplifier.rewrite_rule fset_defs_sym jthm *} |
|
537 ML {* val qthm = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} rthm *} |
|
538 ML {* ObjectLogic.rulify qthm *} |
|
539 |
444 |
540 |
445 ML {* val li = Thm.freezeT (atomize_thm @{thm fold1.simps(2)}) *} |
541 ML {* val li = Thm.freezeT (atomize_thm @{thm fold1.simps(2)}) *} |
446 prove fold1_def_2_r: {* |
542 prove fold1_def_2_r: {* |
447 Logic.mk_implies |
543 Logic.mk_implies |
448 ((prop_of li), |
544 ((prop_of li), |