equal
deleted
inserted
replaced
441 | _ => Conv.sub_conv (Conv.top_sweep_conv if_context_conv) ctxt) ct |
441 | _ => Conv.sub_conv (Conv.top_sweep_conv if_context_conv) ctxt) ct |
442 |
442 |
443 fun lift_ite_rewrite ctxt t = |
443 fun lift_ite_rewrite ctxt t = |
444 prove ctxt t (fn ctxt => |
444 prove ctxt t (fn ctxt => |
445 CONVERSION (HOLogic.Trueprop_conv (Conv.binop_conv (if_context_conv ctxt))) |
445 CONVERSION (HOLogic.Trueprop_conv (Conv.binop_conv (if_context_conv ctxt))) |
446 THEN' rtac @{thm refl}) |
446 THEN' resolve_tac ctxt @{thms refl}) |
447 |
447 |
448 fun prove_conj_disj_perm ctxt t = prove ctxt t (fn _ => Conj_Disj_Perm.conj_disj_perm_tac) |
448 fun prove_conj_disj_perm ctxt t = prove ctxt t Conj_Disj_Perm.conj_disj_perm_tac |
449 |
449 |
450 fun rewrite ctxt _ = try_provers ctxt Z3_Proof.Rewrite [ |
450 fun rewrite ctxt _ = try_provers ctxt Z3_Proof.Rewrite [ |
451 ("rules", apply_rule ctxt), |
451 ("rules", apply_rule ctxt), |
452 ("conj_disj_perm", prove_conj_disj_perm ctxt), |
452 ("conj_disj_perm", prove_conj_disj_perm ctxt), |
453 ("prop_rewrite", prove_prop_rewrite ctxt), |
453 ("prop_rewrite", prove_prop_rewrite ctxt), |
490 (* quantifier instantiation *) |
490 (* quantifier instantiation *) |
491 |
491 |
492 val quant_inst_rule = @{lemma "~P x | Q ==> ~(ALL x. P x) | Q" by fast} |
492 val quant_inst_rule = @{lemma "~P x | Q ==> ~(ALL x. P x) | Q" by fast} |
493 |
493 |
494 fun quant_inst ctxt _ t = prove ctxt t (fn _ => |
494 fun quant_inst ctxt _ t = prove ctxt t (fn _ => |
495 REPEAT_ALL_NEW (rtac quant_inst_rule) |
495 REPEAT_ALL_NEW (resolve_tac ctxt [quant_inst_rule]) |
496 THEN' rtac @{thm excluded_middle}) |
496 THEN' resolve_tac ctxt @{thms excluded_middle}) |
497 |
497 |
498 |
498 |
499 (* propositional lemma *) |
499 (* propositional lemma *) |
500 |
500 |
501 exception LEMMA of unit |
501 exception LEMMA of unit |