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 warning (str_of_thm_no_vars lthy' def); lthy' |
53 writeln (str_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 |
115 |
115 |
116 local_setup %gray{* fn lthy => |
116 local_setup %gray{* fn lthy => |
117 let |
117 let |
118 val def = defn_aux lthy eo_orules eo_preds (e_pred, e_arg_tys) |
118 val def = defn_aux lthy eo_orules eo_preds (e_pred, e_arg_tys) |
119 in |
119 in |
120 warning (Syntax.string_of_term lthy def); lthy |
120 writeln (Syntax.string_of_term lthy def); lthy |
121 end *} |
121 end *} |
122 |
122 |
123 text {* |
123 text {* |
124 where we use the shorthands defined in Figure~\ref{fig:shorthands}. |
124 where we use the shorthands defined in Figure~\ref{fig:shorthands}. |
125 The testcase calls @{ML defn_aux} for the predicate @{text "even"} and prints |
125 The testcase calls @{ML defn_aux} for the predicate @{text "even"} and prints |
131 |
131 |
132 If we try out the function with the rules for freshness |
132 If we try out the function with the rules for freshness |
133 *} |
133 *} |
134 |
134 |
135 local_setup %gray{* fn lthy => |
135 local_setup %gray{* fn lthy => |
136 (warning (Syntax.string_of_term lthy |
136 (writeln (Syntax.string_of_term lthy |
137 (defn_aux lthy fresh_orules [fresh_pred] (fresh_pred, fresh_arg_tys))); |
137 (defn_aux lthy fresh_orules [fresh_pred] (fresh_pred, fresh_arg_tys))); |
138 lthy) *} |
138 lthy) *} |
139 |
139 |
140 text {* |
140 text {* |
141 we obtain |
141 we obtain |
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 warning (str_of_thms_no_vars lthy' defs); lthy |
185 writeln (str_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 warning (str_of_thm lthy intro); lthy |
394 writeln (str_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 warning (str_of_thms lthy ind_thms); lthy |
453 writeln (str_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 warning (str_of_thm_no_vars @{context} new_thm) |
519 writeln (str_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 "warning (str_of_thm_no_vars @{context} |
532 "writeln (str_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 *} |
609 @ ["Prems1 from the rule:"] @ (map (str_of_thm ctxt) prems1) |
609 @ ["Prems1 from the rule:"] @ (map (str_of_thm ctxt) prems1) |
610 @ ["Prems2 from the predicate:"] @ (map (str_of_thm ctxt) prems2) |
610 @ ["Prems2 from the predicate:"] @ (map (str_of_thm ctxt) prems2) |
611 in |
611 in |
612 s |> separate "\n" |
612 s |> separate "\n" |
613 |> implode |
613 |> implode |
614 |> warning |
614 |> writeln |
615 end*} |
615 end*} |
616 text_raw{* |
616 text_raw{* |
617 \end{isabelle} |
617 \end{isabelle} |
618 \end{minipage} |
618 \end{minipage} |
619 \caption{A helper function that prints out the parameters and premises that |
619 \caption{A helper function that prints out the parameters and premises that |