--- a/ProgTutorial/Base.thy Tue May 21 14:37:39 2019 +0200
+++ b/ProgTutorial/Base.thy Tue May 21 16:22:30 2019 +0200
@@ -3,6 +3,7 @@
"~~/src/HOL/Library/LaTeXsugar"
begin
+
notation (latex output)
Cons ("_ # _" [66,65] 65)
--- a/ProgTutorial/Essential.thy Tue May 21 14:37:39 2019 +0200
+++ b/ProgTutorial/Essential.thy Tue May 21 16:22:30 2019 +0200
@@ -2098,10 +2098,10 @@
Note also that applications of \<open>assumption\<close> do not
count as a separate theorem, as you can see in the following code.
- @{ML_matchresult [display,gray]
+ @{ML_response [display,gray]
\<open>@{thm my_conjIb}
|> get_all_names |> sort string_ord\<close>
- \<open>["", "Pure.protectD", "Pure.protectI"]\<close>}
+ \<open>[ "Pure.protectD", "Pure.protectI"]\<close>}
Interestingly, but not surprisingly, the proof of @{thm [source]
--- a/ProgTutorial/Package/Ind_Prelims.thy Tue May 21 14:37:39 2019 +0200
+++ b/ProgTutorial/Package/Ind_Prelims.thy Tue May 21 16:22:30 2019 +0200
@@ -117,8 +117,8 @@
by starting a subproof.
\<close>
+ subgoal premises for P
proof -
- case (goal1 P)
have p1: "R x y" by fact
have p2: "\<forall>P. (\<forall>x. P x x)
\<longrightarrow> (\<forall>x y z. R x y \<longrightarrow> P y z \<longrightarrow> P x z) \<longrightarrow> P y z" by fact
@@ -155,6 +155,7 @@
apply(rule p2[THEN spec[where x=P], THEN mp, THEN mp, OF r1, OF r2])
done
qed
+done
text \<open>
Now we are done. It might be surprising that we are not using the automatic
@@ -231,8 +232,8 @@
shows "odd m \<Longrightarrow> even (Suc m)"
apply (unfold odd_def even_def)
apply (rule allI impI)+
+subgoal premises for P Q
proof -
- case (goal1 P Q)
have p1: "\<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m))
\<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> Q m" by fact
have r1: "P 0" by fact
@@ -244,6 +245,7 @@
THEN mp, THEN mp, THEN mp, OF r1, OF r2, OF r3])
done
qed
+done
text \<open>
The interesting lines are 7 to 15. Again, the assumptions fall into two categories:
@@ -280,21 +282,23 @@
shows "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
apply (unfold accpart_def)
apply (rule allI impI)+
+subgoal premises for P
proof -
- case (goal1 P)
have p1: "\<And>y. R y x \<Longrightarrow>
(\<forall>P. (\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x) \<longrightarrow> P y)" by fact
have r1: "\<forall>x. (\<forall>y. R y x \<longrightarrow> P y) \<longrightarrow> P x" by fact
show "P x"
apply(rule r1[rule_format])
+ subgoal premises for y
proof -
- case (goal1 y)
have r1_prem: "R y x" by fact
show "P y"
- apply(rule p1[OF r1_prem, THEN spec[where x=P], THEN mp, OF r1])
+ apply(rule p1[OF r1_prem, THEN spec[where x=P], THEN mp, OF r1])
done
- qed
+ qed
+ done
qed
+done
text \<open>
As you can see, there are now two subproofs. The assumptions fall as usual into
--- a/ProgTutorial/Parsing.thy Tue May 21 14:37:39 2019 +0200
+++ b/ProgTutorial/Parsing.thy Tue May 21 16:22:30 2019 +0200
@@ -1124,7 +1124,7 @@
fun setup_proof (thm_name, src) lthy =
let
- val text = Input.source_content src
+ val (text, _) = Input.source_content src
val trm = Code_Runtime.value lthy result_cookie ("", text)
in
Proof.theorem NONE (after_qed thm_name) [[(trm, [])]] lthy
--- a/ProgTutorial/Readme.thy Tue May 21 14:37:39 2019 +0200
+++ b/ProgTutorial/Readme.thy Tue May 21 16:22:30 2019 +0200
@@ -160,7 +160,7 @@
So as a rule of thumb, to facilitate result checking use prefer this order:
\begin{enumerate}
- \item \<open>@{ML_matchresult \<open>expr\<close> \<open>pat\<close>}\<close>
+ \item \<open>@{ML_matchresult \<open>expr\<close> \<open>pat\<close>}\<close>
\item \<open>@{ML_response \<open>expr\<close> \<open>string\<close>}\<close>
\item \<open>@{ML_matchresult_fake \<open>expr\<close> \<open>pat\<close>}\<close> or \<open>@{ML_response \<open>expr\<close>}\<close>
\item \<open>@{ML_matchresult_fake_both \<open>expr\<close> \<open>pat\<close>}\<close>
--- a/ProgTutorial/Recipes/Antiquotes.thy Tue May 21 14:37:39 2019 +0200
+++ b/ProgTutorial/Recipes/Antiquotes.thy Tue May 21 16:22:30 2019 +0200
@@ -40,7 +40,7 @@
\<close>
ML \<open>Input.pos_of\<close>
ML%linenosgray\<open>fun ml_enclose bg en source =
- ML_Lex.read bg @ ML_Lex.read_source false source @ ML_Lex.read en;\<close>
+ ML_Lex.read bg @ ML_Lex.read_source source @ ML_Lex.read en;\<close>
ML%linenosgray\<open>fun ml_val code_txt = (ml_enclose "val _ = " "" code_txt)
@@ -48,7 +48,7 @@
let
val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of code_txt) (ml_val code_txt)
in
- Pretty.str (Input.source_content code_txt)
+ 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>
@@ -129,7 +129,7 @@
\<close>
ML%linenosgray\<open>fun ml_pat pat code =
- ML_Lex.read "val" @ ML_Lex.read_source false pat @ ML_Lex.read " = " @ ML_Lex.read_source false 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 =
@@ -154,8 +154,8 @@
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 code = space_explode "\n" (Input.source_content code_txt)
- val resp = add_resp (space_explode "\n" (Input.source_content pat))
+ 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
--- a/ProgTutorial/Tactical.thy Tue May 21 14:37:39 2019 +0200
+++ b/ProgTutorial/Tactical.thy Tue May 21 16:22:30 2019 +0200
@@ -1029,7 +1029,8 @@
ML %grayML\<open>fun select_tac' ctxt =
FIRST' [resolve_tac ctxt [@{thm conjI}], resolve_tac ctxt [@{thm impI}],
- resolve_tac ctxt [@{thm notI}], resolve_tac ctxt [@{thm allI}], K all_tac]\<close>text_raw\<open>\label{tac:selectprime}\<close>
+ resolve_tac ctxt [@{thm notI}], resolve_tac ctxt [@{thm allI}],
+ K all_tac]\<close>text_raw\<open>\label{tac:selectprime}\<close>
text \<open>
Since we like to mimic the behaviour of @{ML select_tac} as closely as possible,
@@ -1473,6 +1474,7 @@
ML %grayML\<open>val ss1 = put_simpset empty_ss @{context} addsimps [@{thm Diff_Int} RS @{thm eq_reflection}]\<close>
+thm "INF_cong"
text \<open>
Printing then out the components of the simpset gives:
@@ -1485,10 +1487,10 @@
\footnote{\bf FIXME: Why does it print out ??.unknown}
- Adding also the congruence rule @{thm [source] strong_INF_cong}
+ Adding also the congruence rule @{thm [source] INF_cong}
\<close>
-ML %grayML\<open>val ss2 = ss1 |> Simplifier.add_cong (@{thm strong_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
@@ -1499,7 +1501,7 @@
??.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 =simp=> C1 x = D1 x\<rbrakk> \<Longrightarrow> INFIMUM A1 C1 \<equiv> INFIMUM B1 D1
+ \<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 14:37:39 2019 +0200
+++ b/ProgTutorial/antiquote_setup.ML Tue May 21 16:22:30 2019 +0200
@@ -40,27 +40,27 @@
ML_Lex.read "fn " @ ML_Lex.read (case ys of [] => "_" | _ => enclose "(" ")" (commas ys)) @
ML_Lex.read " => (" @ src @ ML_Lex.read ")"
-fun ml_with_struct (NONE) src = ML_Lex.read_source false src
+fun ml_with_struct (NONE) src = ML_Lex.read_source src
| ml_with_struct (SOME st) src =
- ML_Lex.read ("let open " ^ st ^ " in ") @ ML_Lex.read_source false src @ ML_Lex.read " end"
+ ML_Lex.read ("let open " ^ st ^ " in ") @ ML_Lex.read_source src @ ML_Lex.read " end"
fun ml_val vs stru txt =
txt |> ml_with_struct stru
|> ml_with_vars vs
fun ml_pat pat lhs =
- ML_Lex.read "val " @ ML_Lex.read_source false pat @
+ ML_Lex.read "val " @ ML_Lex.read_source pat @
ML_Lex.read " = " @
- ML_Lex.read_source false lhs
+ ML_Lex.read_source lhs
fun ml_struct src =
ML_Lex.read "functor DUMMY_FUNCTOR() = struct structure DUMMY = " @
- ML_Lex.read_source false src @
+ ML_Lex.read_source src @
ML_Lex.read " end"
fun ml_type src =
- ML_Lex.read "val _ = NONE : (" @ ML_Lex.read_source false src @ ML_Lex.read ") option"
+ ML_Lex.read "val _ = NONE : (" @ ML_Lex.read_source src @ ML_Lex.read ") option"
(* eval function *)
fun eval_fn ctxt prep exp =
@@ -71,7 +71,7 @@
let
fun compute exp =
let
- val input = ML_Lex.read "(let val r = " @ ML_Lex.read_source false exp @
+ val input = ML_Lex.read "(let val r = " @ ML_Lex.read_source exp @
ML_Lex.read " in (raise ERROR (@{make_string} r); ()) end )"
val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of exp) input
in ""
@@ -85,7 +85,7 @@
fun output_ml ctxt (src, (vs, stru)) =
(eval_fn ctxt (ml_val vs stru) src;
- output ctxt (split_lines (Input.source_content src)))
+ output ctxt (split_lines (fst (Input.source_content src))))
val parser_ml = Scan.lift (Args.text_input --
(Scan.optional (Args.$$$ "for" |-- Parse.!!! (Scan.repeat1 Args.name)) [] --
@@ -97,18 +97,18 @@
val _ = writeln res
val cnt = YXML.content_of res
val pat = case opat of NONE => cnt
- | SOME p => p |> Input.source_content
+ | SOME p => p |> fst o Input.source_content
val _ = if ignore_pat orelse Print_Mode.print_mode_active Latex.latexN orelse match_string is_sep pat cnt then ()
else error (cat_lines ["Substring:", pat, "not contained in:", cnt])
val out = if ignore_pat then cnt else pat
in
- OutputTutorial.output ctxt ([Input.source_content src] @ [Library.prefix_lines "> " out])
+ OutputTutorial.output ctxt ([fst (Input.source_content src)] @ [Library.prefix_lines "> " out])
end
(* checks and prints a single ML-item and produces an index entry *)
fun output_ml_ind ctxt (src, stru) =
let
- val txt = Input.source_content src
+ val (txt,_) = Input.source_content src
in
(eval_fn ctxt (ml_val [] stru) src;
case (stru, Long_Name.base_name txt, Long_Name.qualifier txt) of
@@ -123,7 +123,7 @@
(* checks and prints structures *)
fun gen_output_struct outfn ctxt src =
let
- val txt = Input.source_content src
+ val (txt, _) = Input.source_content src
in
(eval_fn ctxt ml_struct src;
outfn {main = Code txt, minor = Plain "structure"} (split_lines txt))
@@ -135,7 +135,7 @@
(* prints functors; no checks *)
fun gen_output_funct outfn src =
let
- val txt = Input.source_content src
+ val (txt, _) = Input.source_content src
in
(outfn {main = Code txt, minor = Plain "functor"} (split_lines txt))
end
@@ -146,7 +146,7 @@
(* checks and prints types *)
fun gen_output_type outfn ctxt src =
let
- val txt = Input.source_content src
+ val (txt, _) = Input.source_content src
in
(eval_fn ctxt ml_type src;
outfn {main = Code txt, minor = Plain "type"} (split_lines txt))
@@ -160,19 +160,19 @@
(* checks and expression against a result pattern *)
fun output_response ctxt (lhs, pat) =
(eval_fn ctxt (ml_pat pat) lhs;
- output ctxt ((prefix_lines "" (Input.source_content lhs)) @
- (prefix_lines "> " (dots_pat (Input.source_content pat)))))
+ output ctxt ((prefix_lines "" (fst (Input.source_content lhs))) @
+ (prefix_lines "> " (dots_pat (fst (Input.source_content pat))))))
(* checks the expressions, but does not check it against a result pattern *)
fun output_response_fake ctxt (lhs, pat) =
(eval_fn ctxt (ml_val [] NONE) lhs;
- output ctxt ( (split_lines (Input.source_content lhs)) @
- (prefix_lines "> " (dots_pat (Input.source_content pat)))))
+ output ctxt ( (split_lines (fst (Input.source_content lhs))) @
+ (prefix_lines "> " (dots_pat (fst (Input.source_content pat))))))
(* checks the expressions, but does not check it against a result pattern *)
fun ouput_response_fake_both ctxt (lhs, pat) =
- (output ctxt ((split_lines (Input.source_content lhs)) @
- (prefix_lines "> " (dots_pat (Input.source_content pat)))))
+ (output ctxt ((split_lines (fst (Input.source_content lhs))) @
+ (prefix_lines "> " (dots_pat (fst ((Input.source_content pat)))))))
val single_arg = Scan.lift (Args.text_input)
val two_args = Scan.lift (Args.text_input -- Args.text_input)
@@ -202,7 +202,7 @@
fun check_file_exists _ src =
let
- val txt = Input.source_content src
+ val (txt, _) = Input.source_content src
in
(if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt))
then Latex.string (href_link txt)