# HG changeset patch # User Norbert Schirmer # Date 1558521531 -7200 # Node ID 034150db9d91a70cf34e9e987f597f19f762b6cc # Parent 321e220a6baa6c8b704c49de63818949789bf670 polish document diff -r 321e220a6baa -r 034150db9d91 ProgTutorial/Essential.thy --- a/ProgTutorial/Essential.thy Tue May 21 16:22:30 2019 +0200 +++ b/ProgTutorial/Essential.thy Wed May 22 12:38:51 2019 +0200 @@ -2082,12 +2082,13 @@ @{ML_response [display,gray] \@{thm my_conjIa} |> get_all_names |> sort string_ord\ - \["", "HOL.All_def", "HOL.FalseE", "HOL.False_def", "HOL.TrueI", "HOL.True_def", - "HOL.True_or_False", "HOL.allI", "HOL.and_def", "HOL.conjI", - "HOL.conjunct1", "HOL.conjunct2", "HOL.disjE", "HOL.eqTrueE", "HOL.eqTrueI", - "HOL.ext", "HOL.fun_cong", "HOL.iffD1", "HOL.iffD2", "HOL.iffI", - "HOL.impI", "HOL.mp", "HOL.or_def", "HOL.refl", "HOL.rev_iffD1", - "HOL.rev_iffD2", "HOL.spec", "HOL.ssubst", "HOL.subst", "HOL.sym", + \["", "HOL.All_def", "HOL.FalseE", "HOL.False_def", "HOL.TrueI", + "HOL.True_def", "HOL.True_or_False", "HOL.allI", "HOL.and_def", + "HOL.conjI", "HOL.conjunct1", "HOL.conjunct2", "HOL.disjE", + "HOL.eqTrueE", "HOL.eqTrueI", "HOL.ext", "HOL.fun_cong", "HOL.iffD1", + "HOL.iffD2", "HOL.iffI", "HOL.impI", "HOL.mp", "HOL.or_def", + "HOL.refl", "HOL.rev_iffD1", "HOL.rev_iffD2", "HOL.spec", + "HOL.ssubst", "HOL.subst", "HOL.sym", "Pure.protectD", "Pure.protectI"]\} The theorems @{thm [source] Pure.protectD} and @{thm [source] @@ -2112,8 +2113,9 @@ @{ML_response [display,gray] \@{thm my_conjIc} |> get_all_names\ - \["HOL.simp_thms_25", "Pure.conjunctionD1", "Pure.conjunctionD2", "Pure.conjunctionI", - "HOL.rev_mp", "HOL.exI", "HOL.allE", "HOL.exE",\]\} + \["HOL.simp_thms_25", "Pure.conjunctionD1", "Pure.conjunctionD2", + "Pure.conjunctionI", "HOL.rev_mp", "HOL.exI", "HOL.allE", + "HOL.exE",\]\} \begin{exercise} diff -r 321e220a6baa -r 034150db9d91 ProgTutorial/Intro.thy --- a/ProgTutorial/Intro.thy Tue May 21 16:22:30 2019 +0200 +++ b/ProgTutorial/Intro.thy Wed May 22 12:38:51 2019 +0200 @@ -344,7 +344,7 @@ \item {\bf Jasmin Blanchette} helped greatly with section \ref{sec:pretty} and exercise \ref{fun:killqnt}. - \item {\bf Sascha Böhme} contributed the recipes in \ref{rec:timeout}, + \item {\bf Sascha B\"ohme} contributed the recipes in \ref{rec:timeout}, \ref{rec:external} and \ref{rec:oracle}. He also wrote section \ref{sec:conversion} and helped with recipe \ref{rec:timing}. Parts of section \ref{sec:storing} are by him. diff -r 321e220a6baa -r 034150db9d91 ProgTutorial/Package/Ind_Code.thy --- a/ProgTutorial/Package/Ind_Code.thy Tue May 21 16:22:30 2019 +0200 +++ b/ProgTutorial/Package/Ind_Code.thy Wed May 22 12:38:51 2019 +0200 @@ -580,10 +580,14 @@ \ ML %grayML\fun chop_print params1 params2 prems1 prems2 ctxt = let - val pps = [Pretty.big_list "Params1 from the rule:" (map (pretty_cterm ctxt) params1), - Pretty.big_list "Params2 from the predicate:" (map (pretty_cterm ctxt) params2), - Pretty.big_list "Prems1 from the rule:" (map (pretty_thm ctxt) prems1), - Pretty.big_list "Prems2 from the predicate:" (map (pretty_thm ctxt) prems2)] + val pps = [Pretty.big_list "Params1 from the rule:" + (map (pretty_cterm ctxt) params1), + Pretty.big_list "Params2 from the predicate:" + (map (pretty_cterm ctxt) params2), + Pretty.big_list "Prems1 from the rule:" + (map (pretty_thm ctxt) prems1), + Pretty.big_list "Prems2 from the predicate:" + (map (pretty_thm ctxt) prems2)] in pps |> Pretty.chunks |> Pretty.string_of @@ -650,12 +654,11 @@ \fresh\\\ \Prems1 from the rule:\\\ @{term "a \ b"}\\ - @{text [break] -"\fresh. - (\a b. a \ b \ fresh a (Var b)) \ - (\a t s. fresh a t \ fresh a s \ fresh a (App t s)) \ - (\a t. fresh a (Lam a t)) \ - (\a b t. a \ b \ fresh a t \ fresh a (Lam b t)) \ fresh a t"}\\ + @{text "\fresh."}\\ + @{text "(\a b. a \ b \ fresh a (Var b)) \"}\\ + @{text "(\a t s. fresh a t \ fresh a s \ fresh a (App t s)) \"}\\ + @{text "(\a t. fresh a (Lam a t)) \ "}\\ + @{text "(\a b t. a \ b \ fresh a t \ fresh a (Lam b t)) \ fresh a t"}\\ \Prems2 from the predicate:\\\ @{term "\a b. a \ b \ fresh a (Var b)"}\\ @{term "\a t s. fresh a t \ fresh a s \ fresh a (App t s)"}\\ @@ -682,7 +685,8 @@ val (params1, params2) = chop (length cparams - length preds) cparams val (prems1, prems2) = chop (length prems - length rules) prems in - resolve_tac context [Object_Logic.rulify context (all_elims params1 (nth prems2 i))] 1 + resolve_tac context + [Object_Logic.rulify context (all_elims params1 (nth prems2 i))] 1 end)\ text \ @@ -755,7 +759,8 @@ val (params1, params2) = chop (length cparams - length preds) cparams val (prems1, prems2) = chop (length prems - length rules) prems in - resolve_tac context [Object_Logic.rulify context (all_elims params1 (nth prems2 i))] 1 + resolve_tac context + [Object_Logic.rulify context (all_elims params1 (nth prems2 i))] 1 THEN EVERY1 (map (prepare_prem context params2 prems2) prems1) end)\ @@ -854,7 +859,8 @@ val (params1, params2) = chop (length cparams - length preds) cparams val (prems1, prems2) = chop (length prems - length rules) prems in - resolve_tac context [Object_Logic.rulify context (all_elims params1 (nth prems2 i))] 1 + resolve_tac context + [Object_Logic.rulify context (all_elims params1 (nth prems2 i))] 1 THEN EVERY1 (map (prepare_prem params2 prems2 context) prems1) end)\ diff -r 321e220a6baa -r 034150db9d91 ProgTutorial/Parsing.thy --- a/ProgTutorial/Parsing.thy Tue May 21 16:22:30 2019 +0200 +++ b/ProgTutorial/Parsing.thy Wed May 22 12:38:51 2019 +0200 @@ -670,8 +670,10 @@ @{ML_response [display,gray] \filtered_input' "foo \n bar"\ -\[Token (("foo", ({line=7, offset=1, end_offset=4}, {line=7, offset=4})), (Ident, "foo"),\), - Token (("bar", ({line=8, offset=7, end_offset=10}, {line=8, offset=10})), (Ident, "bar"),\)]\} +\[Token (("foo", ({line=7, offset=1, end_offset=4}, + {line=7, offset=4})), (Ident, "foo"),\), + Token (("bar", ({line=8, offset=7, end_offset=10}, + {line=8, offset=10})), (Ident, "bar"),\)]\} in which the @{text [quotes] "\\n"} causes the second token to be in line 8. @@ -1327,9 +1329,10 @@ \ method_setup %gray foo = - \Scan.succeed - (fn ctxt => (SIMPLE_METHOD ((eresolve_tac ctxt [@{thm conjE}] THEN' resolve_tac ctxt [@{thm conjI}]) 1)))\ - "foo method for conjE and conjI" + \Scan.succeed (fn ctxt => + (SIMPLE_METHOD ((eresolve_tac ctxt [@{thm conjE}] THEN' + resolve_tac ctxt [@{thm conjI}]) 1)))\ + "foo method for conjE and conjI" text \ It defines the method \foo\, which takes no arguments (therefore the diff -r 321e220a6baa -r 034150db9d91 ProgTutorial/Recipes/Antiquotes.thy --- a/ProgTutorial/Recipes/Antiquotes.thy Tue May 21 16:22:30 2019 +0200 +++ b/ProgTutorial/Recipes/Antiquotes.thy Wed May 22 12:38:51 2019 +0200 @@ -46,12 +46,14 @@ fun output_ml ctxt code_txt = let - val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of code_txt) (ml_val code_txt) + val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags + (Input.pos_of code_txt) (ml_val code_txt) in Pretty.str (fst (Input.source_content code_txt)) end -val ml_checked_setup = Thy_Output.antiquotation_pretty_source @{binding "ML_checked"} (Scan.lift Args.text_input) output_ml\ +val ml_checked_setup = Thy_Output.antiquotation_pretty_source + @{binding "ML_checked"} (Scan.lift Args.text_input) output_ml\ setup \ml_checked_setup\ @@ -80,25 +82,7 @@ information about the line number, in case an error is detected. We can improve the code above slightly by writing \ -(* FIXME: remove -ML%linenosgray{*fun output_ml ctxt (code_txt, pos) = -let - val srcpos = {delimited = false, pos = pos, text = ml_val code_txt} -in - (ML_Context.eval_source_in (SOME ctxt) ML_Compiler.flags srcpos; - code_txt - |> space_explode "\n" - |> map Pretty.str - |> Pretty.list "" "" - |> Document_Antiquotation.output ctxt - |> Latex.string) -end -val ml_checked_setup2 = Thy_Output.antiquotation @{binding "ML_checked2"} - (Scan.lift (Parse.position Args.name)) output_ml *} - -setup {* ml_checked_setup2 *} -*) text \ where in Lines 1 and 2 the positional information is properly treated. The parser @{ML Parse.position} encodes the positional information in the @@ -129,16 +113,11 @@ \ ML%linenosgray\fun ml_pat pat code = - ML_Lex.read "val" @ ML_Lex.read_source pat @ ML_Lex.read " = " @ ML_Lex.read_source code\ + ML_Lex.read "val" @ + ML_Lex.read_source pat @ + ML_Lex.read " = " @ + ML_Lex.read_source code\ -(* -ML %grayML{*fun ml_pat code_txt pat = -let val pat' = - implode (map (fn "\" => "_" | s => s) (Symbol.explode pat)) -in - ml_enclose ("val " ^ pat' ^ " = ") "" code_txt -end*} -*) text \ Next we add a response indicator to the result using: \ @@ -153,36 +132,21 @@ ML %linenosgray\ fun output_ml_resp ctxt (code_txt, pat) = let - val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of code_txt) (ml_pat pat code_txt) + val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags + (Input.pos_of code_txt) (ml_pat pat code_txt) val code = space_explode "\n" (fst (Input.source_content code_txt)) val resp = add_resp (space_explode "\n" (fst (Input.source_content pat))) in Pretty.str (cat_lines (code @ resp)) end -val ml_response_setup = Thy_Output.antiquotation_pretty_source @{binding "ML_resp"} (Scan.lift (Args.text_input -- Args.text_input)) output_ml_resp +val ml_response_setup = Thy_Output.antiquotation_pretty_source + @{binding "ML_resp"} + (Scan.lift (Args.text_input -- Args.text_input)) + output_ml_resp \ -(* -ML %linenosgray{*fun output_ml_resp {context = ctxt, ...} ((code_txt, pat), pos) = - (let - val srcpos = {delimited = false, text = ml_pat (code_txt, pat), pos = pos} - in - ML_Context.eval_source_in (SOME ctxt) ML_Compiler.flags srcpos - end; - let - val code_output = space_explode "\n" code_txt - val resp_output = add_resp (space_explode "\n" pat) - in - Thy_Output.output ctxt (map Pretty.str (code_output @ resp_output)) - end) - - -val ml_resp_setup = Thy_Output.antiquotation @{binding "ML_resp"} - (Scan.lift (Parse.position (Args.text_input -- Args.text_input))) - output_ml_resp*} -*) setup \ml_response_setup\ (* FIXME *) diff -r 321e220a6baa -r 034150db9d91 ProgTutorial/Recipes/Sat.thy --- a/ProgTutorial/Recipes/Sat.thy Tue May 21 16:22:30 2019 +0200 +++ b/ProgTutorial/Recipes/Sat.thy Wed May 22 12:38:51 2019 +0200 @@ -52,14 +52,16 @@ \ ML %grayML\val (pform', table') = - Prop_Logic.prop_formula_of_term @{term "\x::nat. P x"} Termtab.empty\ + Prop_Logic.prop_formula_of_term @{term "\x::nat. P x"} + Termtab.empty\ text \ returns @{ML \BoolVar 1\ in Prop_Logic} for @{ML pform'} and the table @{ML table'} is: @{ML_response [display,gray] - \map (apfst (YXML.content_of o Syntax.string_of_term @{context})) (Termtab.dest table')\ + \map (apfst (YXML.content_of o Syntax.string_of_term @{context})) + (Termtab.dest table')\ \("\x. P x", 1)\} In the print out of the tabel, we used some pretty printing scaffolding diff -r 321e220a6baa -r 034150db9d91 ProgTutorial/Solutions.thy --- a/ProgTutorial/Solutions.thy Tue May 21 16:22:30 2019 +0200 +++ b/ProgTutorial/Solutions.thy Wed May 22 12:38:51 2019 +0200 @@ -362,8 +362,10 @@ This is all we need to let the conversion run against the simproc: \ -ML %grayML\val _ = Goal.prove @{context} [] [] (goal 8) (fn {context, ...} => c_tac context) -val _ = Goal.prove @{context} [] [] (goal 8) (fn {context, ...} => s_tac context)\ +ML %grayML\val _ = Goal.prove @{context} [] [] (goal 8) + (fn {context, ...} => c_tac context) +val _ = Goal.prove @{context} [] [] (goal 8) + (fn {context, ...} => s_tac context)\ text \ If you do the exercise, you can see that both ways of simplifying additions diff -r 321e220a6baa -r 034150db9d91 ProgTutorial/Tactical.thy --- a/ProgTutorial/Tactical.thy Tue May 21 16:22:30 2019 +0200 +++ b/ProgTutorial/Tactical.thy Wed May 22 12:38:51 2019 +0200 @@ -962,7 +962,8 @@ lemma shows "A \ True \ A" apply(tactic \(resolve_tac @{context} [@{thm conjI}] - THEN' RANGE [resolve_tac @{context} [@{thm TrueI}], assume_tac @{context}]) 1\) + THEN' RANGE [resolve_tac @{context} [@{thm TrueI}], + assume_tac @{context}]) 1\) txt \\begin{minipage}{\textwidth} @{subgoals [display]} \end{minipage}\ @@ -976,8 +977,11 @@ \ ML %grayML\fun foo_tac'' ctxt = - EVERY' [eresolve_tac ctxt [@{thm disjE}], resolve_tac ctxt [@{thm disjI2}], - assume_tac ctxt, resolve_tac ctxt [@{thm disjI1}], assume_tac ctxt]\ + EVERY' [eresolve_tac ctxt [@{thm disjE}], + resolve_tac ctxt [@{thm disjI2}], + assume_tac ctxt, + resolve_tac ctxt [@{thm disjI1}], + assume_tac ctxt]\ text \ There is even another way of implementing this tactic: in automatic proof @@ -988,8 +992,11 @@ \ ML %grayML\fun foo_tac1 ctxt = - EVERY1 [eresolve_tac ctxt [@{thm disjE}], resolve_tac ctxt [@{thm disjI2}], - assume_tac ctxt, resolve_tac ctxt [@{thm disjI1}], assume_tac ctxt]\ + EVERY1 [eresolve_tac ctxt [@{thm disjE}], + resolve_tac ctxt [@{thm disjI2}], + assume_tac ctxt, + resolve_tac ctxt [@{thm disjI1}], + assume_tac ctxt]\ text \ and call @{ML foo_tac1}. @@ -1073,8 +1080,10 @@ \ ML %grayML\fun select_tac'' ctxt = - TRY o FIRST' [resolve_tac ctxt [@{thm conjI}], resolve_tac ctxt [@{thm impI}], - resolve_tac ctxt [@{thm notI}], resolve_tac ctxt [@{thm allI}]]\ + TRY o FIRST' [resolve_tac ctxt [@{thm conjI}], + resolve_tac ctxt [@{thm impI}], + resolve_tac ctxt [@{thm notI}], + resolve_tac ctxt [@{thm allI}]]\ text_raw\\label{tac:selectprimeprime}\ text \ @@ -1472,7 +1481,8 @@ the simplification rule @{thm [source] Diff_Int} as follows: \ -ML %grayML\val ss1 = put_simpset empty_ss @{context} addsimps [@{thm Diff_Int} RS @{thm eq_reflection}]\ +ML %grayML\val ss1 = put_simpset empty_ss @{context} addsimps + [@{thm Diff_Int} RS @{thm eq_reflection}]\ thm "INF_cong" text \ @@ -1490,7 +1500,8 @@ Adding also the congruence rule @{thm [source] INF_cong} \ -ML %grayML\val ss2 = ss1 |> Simplifier.add_cong (@{thm INF_cong} RS @{thm eq_reflection})\ +ML %grayML\val ss2 = ss1 |> + Simplifier.add_cong (@{thm INF_cong} RS @{thm eq_reflection})\ text \ gives @@ -1501,7 +1512,8 @@ ??.unknown: A1 - B1 \ C1 \ A1 - B1 \ (A1 - C1) Congruences rules: Complete_Lattices.Inf_class.Inf: - \A1 = B1; \x. x \ B1 \ C1 x = D1 x\ \ Inf (C1 ` A1) \ Inf (D1 ` B1) + \A1 = B1; \x. x \ B1 \ C1 x = D1 x\ + \ Inf (C1 ` A1) \ Inf (D1 ` B1) Simproc patterns:\} Notice that we had to add these lemmas as meta-equations. The @{ML empty_ss} diff -r 321e220a6baa -r 034150db9d91 ProgTutorial/antiquote_setup.ML --- a/ProgTutorial/antiquote_setup.ML Tue May 21 16:22:30 2019 +0200 +++ b/ProgTutorial/antiquote_setup.ML Wed May 22 12:38:51 2019 +0200 @@ -220,26 +220,6 @@ SOME {goal, ...} => goal | _ => error "No proof state"); - -fun output_goals ctxt _ = -let - fun subgoals 0 = "" - | subgoals 1 = "goal (1 subgoal):" - | subgoals n = "goal (" ^ string_of_int n ^ " subgoals):" - - val state = proof_state (Toplevel.presentation_state ctxt) - val goals = Goal_Display.pretty_goal ctxt state - - val prop = Thm.prop_of state; - val (As, _) = Logic.strip_horn prop; - val out = (case (length As) of - 0 => goals - | n => Pretty.big_list (subgoals n) [goals]) (* FIXME: improve printing? *) -in - output ctxt [Pretty.string_of out] -end - - fun output_raw_goal_state ctxt _ = let val goals = proof_state (Toplevel.presentation_state ctxt) @@ -248,14 +228,11 @@ output ctxt [out] end -val subgoals_setup = - Thy_Output.antiquotation_raw @{binding "subgoals"} (Scan.succeed ()) output_goals val raw_goal_state_setup = Thy_Output.antiquotation_raw @{binding "raw_goal_state"} (Scan.succeed ()) output_raw_goal_state val setup = ml_setup #> ml_file_setup #> - subgoals_setup #> raw_goal_state_setup end;