equal
deleted
inserted
replaced
95 local_setup %gray {* fn lthy => |
95 local_setup %gray {* fn lthy => |
96 let |
96 let |
97 val arg = ((@{binding "MyTrue"}, NoSyn), @{term True}) |
97 val arg = ((@{binding "MyTrue"}, NoSyn), @{term True}) |
98 val (def, lthy') = make_defs arg lthy |
98 val (def, lthy') = make_defs arg lthy |
99 in |
99 in |
100 warning (str_of_thm lthy' def); lthy' |
100 warning (str_of_thm_no_vars lthy' def); lthy' |
101 end *} |
101 end *} |
102 |
102 |
103 text {* |
103 text {* |
104 which makes the definition @{prop "MyTrue \<equiv> True"} and then prints it out. |
104 which makes the definition @{prop "MyTrue \<equiv> True"} and then prints it out. |
105 Since we are testing the function inside \isacommand{local\_setup}, i.e.~make |
105 Since we are testing the function inside \isacommand{local\_setup}, i.e.~make |
216 val prednames = [@{binding "even"}, @{binding "odd"}] |
216 val prednames = [@{binding "even"}, @{binding "odd"}] |
217 val syns = [NoSyn, NoSyn] |
217 val syns = [NoSyn, NoSyn] |
218 val arg_tyss = [[@{typ "nat"}], [@{typ "nat"}]] |
218 val arg_tyss = [[@{typ "nat"}], [@{typ "nat"}]] |
219 val (defs, lthy') = definitions rules preds prednames syns arg_tyss lthy |
219 val (defs, lthy') = definitions rules preds prednames syns arg_tyss lthy |
220 in |
220 in |
221 warning (str_of_thms lthy' defs); lthy' |
221 warning (str_of_thms_no_vars lthy' defs); lthy' |
222 end *} |
222 end *} |
223 |
223 |
224 text {* |
224 text {* |
225 where we feed into the functions all parameters corresponding to |
225 where we feed into the functions all parameters corresponding to |
226 the @{text even}-@{text odd} example. The definitions we obtain |
226 the @{text even}-@{text odd} example. The definitions we obtain |
411 val newpred = @{term "P::nat\<Rightarrow>bool"} |
411 val newpred = @{term "P::nat\<Rightarrow>bool"} |
412 val arg_tys = [@{typ "nat"}] |
412 val arg_tys = [@{typ "nat"}] |
413 val intro = |
413 val intro = |
414 prove_induction lthy defs srules cnewpreds ((pred, newpred), arg_tys) |
414 prove_induction lthy defs srules cnewpreds ((pred, newpred), arg_tys) |
415 in |
415 in |
416 warning (str_of_thm_raw lthy intro); lthy |
416 warning (str_of_thm lthy intro); lthy |
417 end *} |
417 end *} |
418 |
418 |
419 text {* |
419 text {* |
420 This prints out: |
420 This prints out: |
421 |
421 |
475 val defs = [@{thm even_def}, @{thm odd_def}] |
475 val defs = [@{thm even_def}, @{thm odd_def}] |
476 val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}] |
476 val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}] |
477 val tyss = [[@{typ "nat"}], [@{typ "nat"}]] |
477 val tyss = [[@{typ "nat"}], [@{typ "nat"}]] |
478 val ind_thms = inductions rules defs preds tyss lthy |
478 val ind_thms = inductions rules defs preds tyss lthy |
479 in |
479 in |
480 warning (str_of_thms_raw lthy ind_thms); lthy |
480 warning (str_of_thms lthy ind_thms); lthy |
481 end *} |
481 end *} |
482 |
482 |
483 |
483 |
484 text {* |
484 text {* |
485 which prints out |
485 which prints out |
528 @{ML_response_fake [display, gray] |
528 @{ML_response_fake [display, gray] |
529 "let |
529 "let |
530 val ctrms = [@{cterm \"a::nat\"}, @{cterm \"b::nat\"}, @{cterm \"c::nat\"}] |
530 val ctrms = [@{cterm \"a::nat\"}, @{cterm \"b::nat\"}, @{cterm \"c::nat\"}] |
531 val new_thm = all_elims ctrms @{thm all_elims_test} |
531 val new_thm = all_elims ctrms @{thm all_elims_test} |
532 in |
532 in |
533 warning (str_of_thm @{context} new_thm) |
533 warning (str_of_thm_no_vars @{context} new_thm) |
534 end" |
534 end" |
535 "P a b c"} |
535 "P a b c"} |
536 |
536 |
537 Similarly, the function @{ML imp_elims} eliminates preconditions from implications. |
537 Similarly, the function @{ML imp_elims} eliminates preconditions from implications. |
538 For example |
538 For example |
539 |
539 |
540 @{ML_response_fake [display, gray] |
540 @{ML_response_fake [display, gray] |
541 "warning (str_of_thm @{context} |
541 "warning (str_of_thm_no_vars @{context} |
542 (imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}))" |
542 (imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}))" |
543 "C"} |
543 "C"} |
544 *} |
544 *} |
545 |
545 |
546 ML {* prems_of *} |
546 ML {* prems_of *} |
569 ML {* METAHYPS *} |
569 ML {* METAHYPS *} |
570 |
570 |
571 ML {* |
571 ML {* |
572 fun chop_print_tac2 ctxt prems = |
572 fun chop_print_tac2 ctxt prems = |
573 let |
573 let |
574 val _ = warning (commas (map (str_of_thm ctxt) prems)) |
574 val _ = warning (commas (map (str_of_thm_no_vars ctxt) prems)) |
575 in |
575 in |
576 all_tac |
576 all_tac |
577 end |
577 end |
578 *} |
578 *} |
579 |
579 |