ProgTutorial/Package/Ind_Code.thy
changeset 440 a0b280dd4bc7
parent 418 1d1e4cda8c54
child 441 520127b708e6
equal deleted inserted replaced
439:b83c75d051b7 440:a0b280dd4bc7
   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