equal
deleted
inserted
replaced
48 local_setup %gray {* fn lthy => |
48 local_setup %gray {* fn lthy => |
49 let |
49 let |
50 val arg = ((@{binding "My_True"}, NoSyn), @{term True}) |
50 val arg = ((@{binding "My_True"}, NoSyn), @{term True}) |
51 val (def, lthy') = make_defn arg lthy |
51 val (def, lthy') = make_defn arg lthy |
52 in |
52 in |
53 writeln (str_of_thm_no_vars lthy' def); lthy' |
53 writeln (string_of_thm_no_vars lthy' def); lthy' |
54 end *} |
54 end *} |
55 |
55 |
56 text {* |
56 text {* |
57 which introduces the definition @{thm My_True_def} and then prints it out. |
57 which introduces the definition @{thm My_True_def} and then prints it out. |
58 Since we are testing the function inside \isacommand{local\_setup}, i.e., make |
58 Since we are testing the function inside \isacommand{local\_setup}, i.e., make |
180 local_setup %gray {* fn lthy => |
180 local_setup %gray {* fn lthy => |
181 let |
181 let |
182 val (defs, lthy') = |
182 val (defs, lthy') = |
183 defns eo_rules eo_preds eo_prednames eo_mxs eo_arg_tyss lthy |
183 defns eo_rules eo_preds eo_prednames eo_mxs eo_arg_tyss lthy |
184 in |
184 in |
185 writeln (str_of_thms_no_vars lthy' defs); lthy |
185 writeln (string_of_thms_no_vars lthy' defs); lthy |
186 end *} |
186 end *} |
187 |
187 |
188 text {* |
188 text {* |
189 where we feed into the function all parameters corresponding to |
189 where we feed into the function all parameters corresponding to |
190 the @{text even}-@{text odd} example. The definitions we obtain |
190 the @{text even}-@{text odd} example. The definitions we obtain |
389 val newpred = @{term "P::nat\<Rightarrow>bool"} |
389 val newpred = @{term "P::nat\<Rightarrow>bool"} |
390 val srules = map (subst_free (eo_preds ~~ newpreds)) eo_rules |
390 val srules = map (subst_free (eo_preds ~~ newpreds)) eo_rules |
391 val intro = |
391 val intro = |
392 prove_ind lthy eo_defs srules cnewpreds ((e_pred, newpred), e_arg_tys) |
392 prove_ind lthy eo_defs srules cnewpreds ((e_pred, newpred), e_arg_tys) |
393 in |
393 in |
394 writeln (str_of_thm lthy intro); lthy |
394 writeln (string_of_thm lthy intro); lthy |
395 end *} |
395 end *} |
396 |
396 |
397 text {* |
397 text {* |
398 This prints out the theorem: |
398 This prints out the theorem: |
399 |
399 |
448 |
448 |
449 local_setup %gray {* fn lthy => |
449 local_setup %gray {* fn lthy => |
450 let |
450 let |
451 val ind_thms = inds eo_rules eo_defs eo_preds eo_arg_tyss lthy |
451 val ind_thms = inds eo_rules eo_defs eo_preds eo_arg_tyss lthy |
452 in |
452 in |
453 writeln (str_of_thms lthy ind_thms); lthy |
453 writeln (string_of_thms lthy ind_thms); lthy |
454 end *} |
454 end *} |
455 |
455 |
456 |
456 |
457 text {* |
457 text {* |
458 which prints out |
458 which prints out |
514 @{ML_response_fake [display, gray] |
514 @{ML_response_fake [display, gray] |
515 "let |
515 "let |
516 val ctrms = [@{cterm \"a::nat\"}, @{cterm \"b::nat\"}, @{cterm \"c::nat\"}] |
516 val ctrms = [@{cterm \"a::nat\"}, @{cterm \"b::nat\"}, @{cterm \"c::nat\"}] |
517 val new_thm = all_elims ctrms @{thm all_elims_test} |
517 val new_thm = all_elims ctrms @{thm all_elims_test} |
518 in |
518 in |
519 writeln (str_of_thm_no_vars @{context} new_thm) |
519 writeln (string_of_thm_no_vars @{context} new_thm) |
520 end" |
520 end" |
521 "P a b c"} |
521 "P a b c"} |
522 |
522 |
523 Note the difference with @{ML inst_spec_tac} from Page~\pageref{fun:instspectac}: |
523 Note the difference with @{ML inst_spec_tac} from Page~\pageref{fun:instspectac}: |
524 @{ML inst_spec_tac} is a tactic which operates on a goal state; in contrast |
524 @{ML inst_spec_tac} is a tactic which operates on a goal state; in contrast |
527 Similarly, the function @{ML imp_elims} eliminates preconditions from implications. |
527 Similarly, the function @{ML imp_elims} eliminates preconditions from implications. |
528 For example we can eliminate the preconditions @{text "A"} and @{text "B"} from |
528 For example we can eliminate the preconditions @{text "A"} and @{text "B"} from |
529 @{thm [source] imp_elims_test}: |
529 @{thm [source] imp_elims_test}: |
530 |
530 |
531 @{ML_response_fake [display, gray] |
531 @{ML_response_fake [display, gray] |
532 "writeln (str_of_thm_no_vars @{context} |
532 "writeln (string_of_thm_no_vars @{context} |
533 (imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}))" |
533 (imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}))" |
534 "C"} |
534 "C"} |
535 |
535 |
536 Now we set up the proof for the introduction rule as follows: |
536 Now we set up the proof for the introduction rule as follows: |
537 *} |
537 *} |
602 \begin{minipage}{\textwidth} |
602 \begin{minipage}{\textwidth} |
603 \begin{isabelle} |
603 \begin{isabelle} |
604 *} |
604 *} |
605 ML{*fun chop_print params1 params2 prems1 prems2 ctxt = |
605 ML{*fun chop_print params1 params2 prems1 prems2 ctxt = |
606 let |
606 let |
607 val s = ["Params1 from the rule:", str_of_cterms ctxt params1] |
607 val s = ["Params1 from the rule:", string_of_cterms ctxt params1] |
608 @ ["Params2 from the predicate:", str_of_cterms ctxt params2] |
608 @ ["Params2 from the predicate:", string_of_cterms ctxt params2] |
609 @ ["Prems1 from the rule:"] @ (map (str_of_thm ctxt) prems1) |
609 @ ["Prems1 from the rule:"] @ (map (string_of_thm ctxt) prems1) |
610 @ ["Prems2 from the predicate:"] @ (map (str_of_thm ctxt) prems2) |
610 @ ["Prems2 from the predicate:"] @ (map (string_of_thm ctxt) prems2) |
611 in |
611 in |
612 s |> separate "\n" |
612 s |> separate "\n" |
613 |> implode |
613 |> implode |
614 |> writeln |
614 |> writeln |
615 end*} |
615 end*} |