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 (string_of_thm_no_vars lthy' def); lthy' |
53 tracing (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 |
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 writeln (Syntax.string_of_term lthy def); lthy |
120 tracing (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 |
135 local_setup %gray {* fn lthy => |
135 local_setup %gray {* fn lthy => |
136 let |
136 let |
137 val def = defn_aux lthy fresh_orules |
137 val def = defn_aux lthy fresh_orules |
138 [fresh_pred] (fresh_pred, fresh_arg_tys) |
138 [fresh_pred] (fresh_pred, fresh_arg_tys) |
139 in |
139 in |
140 writeln (Syntax.string_of_term lthy def); lthy |
140 tracing (Syntax.string_of_term lthy def); lthy |
141 end *} |
141 end *} |
142 |
142 |
143 |
143 |
144 text {* |
144 text {* |
145 we obtain |
145 we obtain |
185 local_setup %gray {* fn lthy => |
185 local_setup %gray {* fn lthy => |
186 let |
186 let |
187 val (defs, lthy') = |
187 val (defs, lthy') = |
188 defns eo_rules eo_preds eo_prednames eo_mxs eo_arg_tyss lthy |
188 defns eo_rules eo_preds eo_prednames eo_mxs eo_arg_tyss lthy |
189 in |
189 in |
190 writeln (string_of_thms_no_vars lthy' defs); lthy |
190 tracing (string_of_thms_no_vars lthy' defs); lthy |
191 end *} |
191 end *} |
192 |
192 |
193 text {* |
193 text {* |
194 where we feed into the function all parameters corresponding to |
194 where we feed into the function all parameters corresponding to |
195 the @{text even}/@{text odd} example. The definitions we obtain |
195 the @{text even}/@{text odd} example. The definitions we obtain |
399 val newpred = @{term "P::nat \<Rightarrow> bool"} |
399 val newpred = @{term "P::nat \<Rightarrow> bool"} |
400 val srules = map (subst_free (eo_preds ~~ newpreds)) eo_rules |
400 val srules = map (subst_free (eo_preds ~~ newpreds)) eo_rules |
401 val intro = |
401 val intro = |
402 prove_ind lthy eo_defs srules cnewpreds ((e_pred, newpred), e_arg_tys) |
402 prove_ind lthy eo_defs srules cnewpreds ((e_pred, newpred), e_arg_tys) |
403 in |
403 in |
404 writeln (string_of_thm lthy intro); lthy |
404 tracing (string_of_thm lthy intro); lthy |
405 end *} |
405 end *} |
406 |
406 |
407 text {* |
407 text {* |
408 This prints out the theorem: |
408 This prints out the theorem: |
409 |
409 |
458 |
458 |
459 local_setup %gray {* fn lthy => |
459 local_setup %gray {* fn lthy => |
460 let |
460 let |
461 val ind_thms = inds eo_rules eo_defs eo_preds eo_arg_tyss lthy |
461 val ind_thms = inds eo_rules eo_defs eo_preds eo_arg_tyss lthy |
462 in |
462 in |
463 writeln (string_of_thms lthy ind_thms); lthy |
463 tracing (string_of_thms lthy ind_thms); lthy |
464 end *} |
464 end *} |
465 |
465 |
466 |
466 |
467 text {* |
467 text {* |
468 which prints out |
468 which prints out |
524 @{ML_response_fake [display, gray] |
524 @{ML_response_fake [display, gray] |
525 "let |
525 "let |
526 val ctrms = [@{cterm \"a::nat\"}, @{cterm \"b::nat\"}, @{cterm \"c::nat\"}] |
526 val ctrms = [@{cterm \"a::nat\"}, @{cterm \"b::nat\"}, @{cterm \"c::nat\"}] |
527 val new_thm = all_elims ctrms @{thm all_elims_test} |
527 val new_thm = all_elims ctrms @{thm all_elims_test} |
528 in |
528 in |
529 writeln (string_of_thm_no_vars @{context} new_thm) |
529 tracing (string_of_thm_no_vars @{context} new_thm) |
530 end" |
530 end" |
531 "P a b c"} |
531 "P a b c"} |
532 |
532 |
533 Note the difference with @{ML inst_spec_tac} from Page~\pageref{fun:instspectac}: |
533 Note the difference with @{ML inst_spec_tac} from Page~\pageref{fun:instspectac}: |
534 @{ML inst_spec_tac} is a tactic which operates on a goal state; in contrast |
534 @{ML inst_spec_tac} is a tactic which operates on a goal state; in contrast |
540 |
540 |
541 @{ML_response_fake [display, gray] |
541 @{ML_response_fake [display, gray] |
542 "let |
542 "let |
543 val res = imp_elims @{thms imp_elims_test'} @{thm imp_elims_test} |
543 val res = imp_elims @{thms imp_elims_test'} @{thm imp_elims_test} |
544 in |
544 in |
545 writeln (string_of_thm_no_vars @{context} res) |
545 tracing (string_of_thm_no_vars @{context} res) |
546 end" |
546 end" |
547 "C"} |
547 "C"} |
548 |
548 |
549 Now we set up the proof for the introduction rule as follows: |
549 Now we set up the proof for the introduction rule as follows: |
550 *} |
550 *} |