--- 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]
\<open>@{thm my_conjIa}
|> get_all_names |> sort string_ord\<close>
- \<open>["", "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",
+ \<open>["", "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"]\<close>}
The theorems @{thm [source] Pure.protectD} and @{thm [source]
@@ -2112,8 +2113,9 @@
@{ML_response [display,gray]
\<open>@{thm my_conjIc}
|> get_all_names\<close>
- \<open>["HOL.simp_thms_25", "Pure.conjunctionD1", "Pure.conjunctionD2", "Pure.conjunctionI",
- "HOL.rev_mp", "HOL.exI", "HOL.allE", "HOL.exE",\<dots>]\<close>}
+ \<open>["HOL.simp_thms_25", "Pure.conjunctionD1", "Pure.conjunctionD2",
+ "Pure.conjunctionI", "HOL.rev_mp", "HOL.exI", "HOL.allE",
+ "HOL.exE",\<dots>]\<close>}
\begin{exercise}
--- 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.
--- 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 @@
\<close>
ML %grayML\<open>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 @@
\<open>fresh\<close>\\
\<open>Prems1 from the rule:\<close>\\
@{term "a \<noteq> b"}\\
- @{text [break]
-"\<forall>fresh.
- (\<forall>a b. a \<noteq> b \<longrightarrow> fresh a (Var b)) \<longrightarrow>
- (\<forall>a t s. fresh a t \<longrightarrow> fresh a s \<longrightarrow> fresh a (App t s)) \<longrightarrow>
- (\<forall>a t. fresh a (Lam a t)) \<longrightarrow>
- (\<forall>a b t. a \<noteq> b \<longrightarrow> fresh a t \<longrightarrow> fresh a (Lam b t)) \<longrightarrow> fresh a t"}\\
+ @{text "\<forall>fresh."}\\
+ @{text "(\<forall>a b. a \<noteq> b \<longrightarrow> fresh a (Var b)) \<longrightarrow>"}\\
+ @{text "(\<forall>a t s. fresh a t \<longrightarrow> fresh a s \<longrightarrow> fresh a (App t s)) \<longrightarrow>"}\\
+ @{text "(\<forall>a t. fresh a (Lam a t)) \<longrightarrow> "}\\
+ @{text "(\<forall>a b t. a \<noteq> b \<longrightarrow> fresh a t \<longrightarrow> fresh a (Lam b t)) \<longrightarrow> fresh a t"}\\
\<open>Prems2 from the predicate:\<close>\\
@{term "\<forall>a b. a \<noteq> b \<longrightarrow> fresh a (Var b)"}\\
@{term "\<forall>a t s. fresh a t \<longrightarrow> fresh a s \<longrightarrow> 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)\<close>
text \<open>
@@ -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)\<close>
@@ -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)\<close>
--- 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]
\<open>filtered_input' "foo \n bar"\<close>
-\<open>[Token (("foo", ({line=7, offset=1, end_offset=4}, {line=7, offset=4})), (Ident, "foo"),\<dots>),
- Token (("bar", ({line=8, offset=7, end_offset=10}, {line=8, offset=10})), (Ident, "bar"),\<dots>)]\<close>}
+\<open>[Token (("foo", ({line=7, offset=1, end_offset=4},
+ {line=7, offset=4})), (Ident, "foo"),\<dots>),
+ Token (("bar", ({line=8, offset=7, end_offset=10},
+ {line=8, offset=10})), (Ident, "bar"),\<dots>)]\<close>}
in which the @{text [quotes] "\\n"} causes the second token to be in
line 8.
@@ -1327,9 +1329,10 @@
\<close>
method_setup %gray foo =
- \<open>Scan.succeed
- (fn ctxt => (SIMPLE_METHOD ((eresolve_tac ctxt [@{thm conjE}] THEN' resolve_tac ctxt [@{thm conjI}]) 1)))\<close>
- "foo method for conjE and conjI"
+ \<open>Scan.succeed (fn ctxt =>
+ (SIMPLE_METHOD ((eresolve_tac ctxt [@{thm conjE}] THEN'
+ resolve_tac ctxt [@{thm conjI}]) 1)))\<close>
+ "foo method for conjE and conjI"
text \<open>
It defines the method \<open>foo\<close>, which takes no arguments (therefore the
--- 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\<close>
+val ml_checked_setup = Thy_Output.antiquotation_pretty_source
+ @{binding "ML_checked"} (Scan.lift Args.text_input) output_ml\<close>
setup \<open>ml_checked_setup\<close>
@@ -80,25 +82,7 @@
information about the line number, in case an error is detected. We
can improve the code above slightly by writing
\<close>
-(* 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 \<open>
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 @@
\<close>
ML%linenosgray\<open>fun ml_pat pat code =
- ML_Lex.read "val" @ ML_Lex.read_source pat @ ML_Lex.read " = " @ ML_Lex.read_source code\<close>
+ ML_Lex.read "val" @
+ ML_Lex.read_source pat @
+ ML_Lex.read " = " @
+ ML_Lex.read_source code\<close>
-(*
-ML %grayML{*fun ml_pat code_txt pat =
-let val pat' =
- implode (map (fn "\<dots>" => "_" | s => s) (Symbol.explode pat))
-in
- ml_enclose ("val " ^ pat' ^ " = ") "" code_txt
-end*}
-*)
text \<open>
Next we add a response indicator to the result using:
\<close>
@@ -153,36 +132,21 @@
ML %linenosgray\<open>
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
\<close>
-(*
-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 \<open>ml_response_setup\<close>
(* FIXME *)
--- 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 @@
\<close>
ML %grayML\<open>val (pform', table') =
- Prop_Logic.prop_formula_of_term @{term "\<forall>x::nat. P x"} Termtab.empty\<close>
+ Prop_Logic.prop_formula_of_term @{term "\<forall>x::nat. P x"}
+ Termtab.empty\<close>
text \<open>
returns @{ML \<open>BoolVar 1\<close> in Prop_Logic} for @{ML pform'} and the table
@{ML table'} is:
@{ML_response [display,gray]
- \<open>map (apfst (YXML.content_of o Syntax.string_of_term @{context})) (Termtab.dest table')\<close>
+ \<open>map (apfst (YXML.content_of o Syntax.string_of_term @{context}))
+ (Termtab.dest table')\<close>
\<open>("\<forall>x. P x", 1)\<close>}
In the print out of the tabel, we used some pretty printing scaffolding
--- 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:
\<close>
-ML %grayML\<open>val _ = Goal.prove @{context} [] [] (goal 8) (fn {context, ...} => c_tac context)
-val _ = Goal.prove @{context} [] [] (goal 8) (fn {context, ...} => s_tac context)\<close>
+ML %grayML\<open>val _ = Goal.prove @{context} [] [] (goal 8)
+ (fn {context, ...} => c_tac context)
+val _ = Goal.prove @{context} [] [] (goal 8)
+ (fn {context, ...} => s_tac context)\<close>
text \<open>
If you do the exercise, you can see that both ways of simplifying additions
--- 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 \<Longrightarrow> True \<and> A"
apply(tactic \<open>(resolve_tac @{context} [@{thm conjI}]
- THEN' RANGE [resolve_tac @{context} [@{thm TrueI}], assume_tac @{context}]) 1\<close>)
+ THEN' RANGE [resolve_tac @{context} [@{thm TrueI}],
+ assume_tac @{context}]) 1\<close>)
txt \<open>\begin{minipage}{\textwidth}
@{subgoals [display]}
\end{minipage}\<close>
@@ -976,8 +977,11 @@
\<close>
ML %grayML\<open>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]\<close>
+ EVERY' [eresolve_tac ctxt [@{thm disjE}],
+ resolve_tac ctxt [@{thm disjI2}],
+ assume_tac ctxt,
+ resolve_tac ctxt [@{thm disjI1}],
+ assume_tac ctxt]\<close>
text \<open>
There is even another way of implementing this tactic: in automatic proof
@@ -988,8 +992,11 @@
\<close>
ML %grayML\<open>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]\<close>
+ EVERY1 [eresolve_tac ctxt [@{thm disjE}],
+ resolve_tac ctxt [@{thm disjI2}],
+ assume_tac ctxt,
+ resolve_tac ctxt [@{thm disjI1}],
+ assume_tac ctxt]\<close>
text \<open>
and call @{ML foo_tac1}.
@@ -1073,8 +1080,10 @@
\<close>
ML %grayML\<open>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}]]\<close>
+ TRY o FIRST' [resolve_tac ctxt [@{thm conjI}],
+ resolve_tac ctxt [@{thm impI}],
+ resolve_tac ctxt [@{thm notI}],
+ resolve_tac ctxt [@{thm allI}]]\<close>
text_raw\<open>\label{tac:selectprimeprime}\<close>
text \<open>
@@ -1472,7 +1481,8 @@
the simplification rule @{thm [source] Diff_Int} as follows:
\<close>
-ML %grayML\<open>val ss1 = put_simpset empty_ss @{context} addsimps [@{thm Diff_Int} RS @{thm eq_reflection}]\<close>
+ML %grayML\<open>val ss1 = put_simpset empty_ss @{context} addsimps
+ [@{thm Diff_Int} RS @{thm eq_reflection}]\<close>
thm "INF_cong"
text \<open>
@@ -1490,7 +1500,8 @@
Adding also the congruence rule @{thm [source] INF_cong}
\<close>
-ML %grayML\<open>val ss2 = ss1 |> Simplifier.add_cong (@{thm INF_cong} RS @{thm eq_reflection})\<close>
+ML %grayML\<open>val ss2 = ss1 |>
+ Simplifier.add_cong (@{thm INF_cong} RS @{thm eq_reflection})\<close>
text \<open>
gives
@@ -1501,7 +1512,8 @@
??.unknown: A1 - B1 \<inter> C1 \<equiv> A1 - B1 \<union> (A1 - C1)
Congruences rules:
Complete_Lattices.Inf_class.Inf:
- \<lbrakk>A1 = B1; \<And>x. x \<in> B1 \<Longrightarrow> C1 x = D1 x\<rbrakk> \<Longrightarrow> Inf (C1 ` A1) \<equiv> Inf (D1 ` B1)
+ \<lbrakk>A1 = B1; \<And>x. x \<in> B1 \<Longrightarrow> C1 x = D1 x\<rbrakk>
+ \<Longrightarrow> Inf (C1 ` A1) \<equiv> Inf (D1 ` B1)
Simproc patterns:\<close>}
Notice that we had to add these lemmas as meta-equations. The @{ML empty_ss}
--- 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;