equal
deleted
inserted
replaced
160 local_setup %gray {* fn lthy => |
160 local_setup %gray {* fn lthy => |
161 let |
161 let |
162 val (defs, lthy') = |
162 val (defs, lthy') = |
163 defns eo_rules eo_preds eo_prednames eo_mxs eo_arg_tyss lthy |
163 defns eo_rules eo_preds eo_prednames eo_mxs eo_arg_tyss lthy |
164 in |
164 in |
165 tracing (string_of_thms_no_vars lthy' defs); lthy |
165 pwriteln (pretty_thms_no_vars lthy' defs); lthy |
166 end *} |
166 end *} |
167 |
167 |
168 text {* |
168 text {* |
169 where we feed into the function all parameters corresponding to |
169 where we feed into the function all parameters corresponding to |
170 the @{text even}/@{text odd} example. The definitions we obtain |
170 the @{text even}/@{text odd} example. The definitions we obtain |
379 val newpred = @{term "P::nat \<Rightarrow> bool"} |
379 val newpred = @{term "P::nat \<Rightarrow> bool"} |
380 val srules = map (subst_free (eo_preds ~~ newpreds)) eo_rules |
380 val srules = map (subst_free (eo_preds ~~ newpreds)) eo_rules |
381 val intro = |
381 val intro = |
382 prove_ind lthy eo_defs srules cnewpreds ((e_pred, newpred), e_arg_tys) |
382 prove_ind lthy eo_defs srules cnewpreds ((e_pred, newpred), e_arg_tys) |
383 in |
383 in |
384 tracing (string_of_thm lthy intro); lthy |
384 pwriteln (pretty_thm lthy intro); lthy |
385 end *} |
385 end *} |
386 |
386 |
387 text {* |
387 text {* |
388 This prints out the theorem: |
388 This prints out the theorem: |
389 |
389 |
438 |
438 |
439 local_setup %gray {* fn lthy => |
439 local_setup %gray {* fn lthy => |
440 let |
440 let |
441 val ind_thms = inds eo_rules eo_defs eo_preds eo_arg_tyss lthy |
441 val ind_thms = inds eo_rules eo_defs eo_preds eo_arg_tyss lthy |
442 in |
442 in |
443 tracing (string_of_thms lthy ind_thms); lthy |
443 pwriteln (pretty_thms lthy ind_thms); lthy |
444 end *} |
444 end *} |
445 |
445 |
446 |
446 |
447 text {* |
447 text {* |
448 which prints out |
448 which prints out |
504 @{ML_response_fake [display, gray] |
504 @{ML_response_fake [display, gray] |
505 "let |
505 "let |
506 val ctrms = [@{cterm \"a::nat\"}, @{cterm \"b::nat\"}, @{cterm \"c::nat\"}] |
506 val ctrms = [@{cterm \"a::nat\"}, @{cterm \"b::nat\"}, @{cterm \"c::nat\"}] |
507 val new_thm = all_elims ctrms @{thm all_elims_test} |
507 val new_thm = all_elims ctrms @{thm all_elims_test} |
508 in |
508 in |
509 tracing (string_of_thm_no_vars @{context} new_thm) |
509 pwriteln (pretty_thm_no_vars @{context} new_thm) |
510 end" |
510 end" |
511 "P a b c"} |
511 "P a b c"} |
512 |
512 |
513 Note the difference with @{ML inst_spec_tac} from Page~\pageref{fun:instspectac}: |
513 Note the difference with @{ML inst_spec_tac} from Page~\pageref{fun:instspectac}: |
514 @{ML inst_spec_tac} is a tactic which operates on a goal state; in contrast |
514 @{ML inst_spec_tac} is a tactic which operates on a goal state; in contrast |
520 |
520 |
521 @{ML_response_fake [display, gray] |
521 @{ML_response_fake [display, gray] |
522 "let |
522 "let |
523 val res = imp_elims @{thms imp_elims_test'} @{thm imp_elims_test} |
523 val res = imp_elims @{thms imp_elims_test'} @{thm imp_elims_test} |
524 in |
524 in |
525 tracing (string_of_thm_no_vars @{context} res) |
525 pwriteln (pretty_thm_no_vars @{context} res) |
526 end" |
526 end" |
527 "C"} |
527 "C"} |
528 |
528 |
529 Now we set up the proof for the introduction rule as follows: |
529 Now we set up the proof for the introduction rule as follows: |
530 *} |
530 *} |
588 \begin{minipage}{\textwidth} |
588 \begin{minipage}{\textwidth} |
589 \begin{isabelle} |
589 \begin{isabelle} |
590 *} |
590 *} |
591 ML{*fun chop_print params1 params2 prems1 prems2 ctxt = |
591 ML{*fun chop_print params1 params2 prems1 prems2 ctxt = |
592 let |
592 let |
593 val s = ["Params1 from the rule:", string_of_cterms ctxt params1] |
593 val pps = [Pretty.big_list "Params1 from the rule:" (map (pretty_cterm ctxt) params1), |
594 @ ["Params2 from the predicate:", string_of_cterms ctxt params2] |
594 Pretty.big_list "Params2 from the predicate:" (map (pretty_cterm ctxt) params2), |
595 @ ["Prems1 from the rule:"] @ (map (string_of_thm ctxt) prems1) |
595 Pretty.big_list "Prems1 from the rule:" (map (pretty_thm ctxt) prems1), |
596 @ ["Prems2 from the predicate:"] @ (map (string_of_thm ctxt) prems2) |
596 Pretty.big_list "Prems2 from the predicate:" (map (pretty_thm ctxt) prems2)] |
597 in |
597 in |
598 s |> cat_lines |
598 pps |> Pretty.chunks |
599 |> tracing |
599 |> tracing o Pretty.string_of |
600 end*} |
600 end*} |
601 text_raw{* |
601 text_raw{* |
602 \end{isabelle} |
602 \end{isabelle} |
603 \end{minipage} |
603 \end{minipage} |
604 \caption{A helper function that prints out the parameters and premises that |
604 \caption{A helper function that prints out the parameters and premises that |