542 \begin{isabelle} |
542 \begin{isabelle} |
543 *} |
543 *} |
544 |
544 |
545 ML{*fun foc_tac {prems, params, asms, concl, context, schematics} = |
545 ML{*fun foc_tac {prems, params, asms, concl, context, schematics} = |
546 let |
546 let |
547 fun pairs1 f1 f2 xs = |
547 fun assgn1 f1 f2 xs = |
548 commas (map (fn (x, y) => f1 x ^ ":=" ^ f2 y) xs) |
548 Pretty.list "" "" (map (fn (x, y) => Pretty.enum ":=" "" "" [f1 x, f2 y]) xs) |
549 |
549 |
550 fun pairs2 f xs = pairs1 f f xs |
550 fun assgn2 f xs = assgn1 f f xs |
551 |
551 |
552 val string_of_params = pairs1 I (string_of_cterm context) params |
552 val pps = map (fn (s, pp) => Pretty.block [Pretty.str s, pp]) |
553 val string_of_asms = string_of_cterms context asms |
553 [("params: ", assgn1 Pretty.str (pretty_cterm context) params), |
554 val string_of_concl = string_of_cterm context concl |
554 ("assumptions: ", pretty_cterms context asms), |
555 val string_of_prems = string_of_thms_no_vars context prems |
555 ("conclusion: ", pretty_cterm context concl), |
556 val string_of_schms = pairs2 (string_of_cterm context) (snd schematics) |
556 ("premises: ", pretty_thms_no_vars context prems), |
557 |
557 ("schematics: ", assgn2 (pretty_cterm context) (snd schematics))] |
558 val strs = ["params: " ^ string_of_params, |
|
559 "schematics: " ^ string_of_schms, |
|
560 "assumptions: " ^ string_of_asms, |
|
561 "conclusion: " ^ string_of_concl, |
|
562 "premises: " ^ string_of_prems] |
|
563 in |
558 in |
564 tracing (cat_lines strs); all_tac |
559 tracing (Pretty.string_of (Pretty.chunks pps)); all_tac |
565 end*} |
560 end*} |
566 |
561 |
567 text_raw{* |
562 text_raw{* |
568 \end{isabelle} |
563 \end{isabelle} |
569 \end{minipage} |
564 \end{minipage} |
581 txt {* |
576 txt {* |
582 The tactic produces the following printout: |
577 The tactic produces the following printout: |
583 |
578 |
584 \begin{quote}\small |
579 \begin{quote}\small |
585 \begin{tabular}{ll} |
580 \begin{tabular}{ll} |
586 params: & @{text "x:=x"}, @{text "y:=y"}\\ |
581 params: & @{text "x:= x"}, @{text "y:= y"}\\ |
587 schematics: & @{text "?z:=z"}\\ |
582 schematics: & @{text "?z:=z"}\\ |
588 assumptions: & @{term "A x y"}\\ |
583 assumptions: & @{term "A x y"}\\ |
589 conclusion: & @{term "B y x \<longrightarrow> C (z y) x"}\\ |
584 conclusion: & @{term "B y x \<longrightarrow> C (z y) x"}\\ |
590 premises: & @{term "A x y"} |
585 premises: & @{term "A x y"} |
591 \end{tabular} |
586 \end{tabular} |
609 txt {* |
604 txt {* |
610 then the tactic prints out: |
605 then the tactic prints out: |
611 |
606 |
612 \begin{quote}\small |
607 \begin{quote}\small |
613 \begin{tabular}{ll} |
608 \begin{tabular}{ll} |
614 params: & @{text "x:=x"}, @{text "y:=y"}\\ |
609 params: & @{text "x:= x"}, @{text "y:= y"}\\ |
615 schematics: & @{text "?z:=z"}\\ |
610 schematics: & @{text "?z:=z"}\\ |
616 assumptions: & @{term "A x y"}, @{term "B y x"}\\ |
611 assumptions: & @{term "A x y"}, @{term "B y x"}\\ |
617 conclusion: & @{term "C (z y) x"}\\ |
612 conclusion: & @{term "C (z y) x"}\\ |
618 premises: & @{term "A x y"}, @{term "B y x"} |
613 premises: & @{term "A x y"}, @{term "B y x"} |
619 \end{tabular} |
614 \end{tabular} |
1491 ML{*fun print_ss ctxt ss = |
1486 ML{*fun print_ss ctxt ss = |
1492 let |
1487 let |
1493 val {simps, congs, procs, ...} = MetaSimplifier.dest_ss ss |
1488 val {simps, congs, procs, ...} = MetaSimplifier.dest_ss ss |
1494 |
1489 |
1495 fun name_thm (nm, thm) = |
1490 fun name_thm (nm, thm) = |
1496 " " ^ nm ^ ": " ^ (string_of_thm_no_vars ctxt thm) |
1491 Pretty.enclose (nm ^ ": ") "" [pretty_thm_no_vars ctxt thm] |
1497 fun name_ctrm (nm, ctrm) = |
1492 fun name_ctrm (nm, ctrm) = |
1498 " " ^ nm ^ ": " ^ (string_of_cterms ctxt ctrm) |
1493 Pretty.enclose (nm ^ ": ") "" [pretty_cterms ctxt ctrm] |
1499 |
1494 |
1500 val s = ["Simplification rules:"] @ map name_thm simps @ |
1495 val pps = [Pretty.big_list "Simplification rules:" (map name_thm simps), |
1501 ["Congruences rules:"] @ map name_thm congs @ |
1496 Pretty.big_list "Congruences rules:" (map name_thm congs), |
1502 ["Simproc patterns:"] @ map name_ctrm procs |
1497 Pretty.big_list "Simproc patterns:" (map name_ctrm procs)] |
1503 in |
1498 in |
1504 s |> cat_lines |
1499 pps |> Pretty.chunks |
1505 |> tracing |
1500 |> pwriteln |
1506 end*} |
1501 end*} |
1507 text_raw {* |
1502 text_raw {* |
1508 \end{isabelle} |
1503 \end{isabelle} |
1509 \end{minipage} |
1504 \end{minipage} |
1510 \caption{The function @{ML_ind dest_ss in MetaSimplifier} returns a record containing |
1505 \caption{The function @{ML_ind dest_ss in MetaSimplifier} returns a record containing |