--- a/ProgTutorial/Advanced.thy Fri Jun 03 15:15:17 2016 +0100
+++ b/ProgTutorial/Advanced.thy Tue May 14 11:10:53 2019 +0200
@@ -646,7 +646,7 @@
text {*
@{ML_ind "Binding.name_of"} returns the string without markup
- @{ML_ind "Binding.conceal"}
+ @{ML_ind "Binding.concealed"}
*}
section {* Concurrency (TBD) *}
--- a/ProgTutorial/Base.thy Fri Jun 03 15:15:17 2016 +0100
+++ b/ProgTutorial/Base.thy Tue May 14 11:10:53 2019 +0200
@@ -3,11 +3,21 @@
"~~/src/HOL/Library/LaTeXsugar"
begin
+ML \<open>@{assert} true\<close>
+ML \<open>@{print} (2 + 3 +4)\<close>
+
+
+print_ML_antiquotations
+text \<open>
+Can we put an ML-val into the text?
+
+@{ML [display] \<open>2 + 3\<close>}
+
+\<close>
notation (latex output)
Cons ("_ # _" [66,65] 65)
-ML {*
-fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n)
+ML %linenosgrayML{*fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n)
fun rhs 1 = P 1
| rhs n = HOLogic.mk_conj (P n, rhs (n - 1))
@@ -17,13 +27,20 @@
(HOLogic.mk_eq (P (m - 1), P m), rhs n), lhs (m - 1) n)
fun de_bruijn n =
- HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))
-*}
+ HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))*}
ML_file "output_tutorial.ML"
+text \<open>
+Can we put an ML-val into the text?
+
+@{ML [gray] \<open>2 + 3\<close>}
+\<close>
+
ML_file "antiquote_setup.ML"
-setup {* OutputTutorial.setup *}
+
+(*setup {* OutputTutorial.setup *}*) (* Seems to be standard now, we don't need this anymoe *)
setup {* AntiquoteSetup.setup *}
+
end
\ No newline at end of file
--- a/ProgTutorial/Essential.thy Fri Jun 03 15:15:17 2016 +0100
+++ b/ProgTutorial/Essential.thy Tue May 14 11:10:53 2019 +0200
@@ -253,12 +253,13 @@
text {*
We can install this pretty printer with the function
- @{ML_ind addPrettyPrinter in PolyML} as follows.
+ @{ML_ind ML_system_pp} as follows.
*}
-ML %grayML{*PolyML.addPrettyPrinter
- (fn _ => fn _ => ml_pretty o Pretty.to_ML o raw_pp_typ)*}
-
+ML %grayML{*ML_system_pp
+ (fn _ => fn _ => Pretty.to_polyml o raw_pp_typ)*}
+
+ML \<open>@{typ "bool"}\<close>
text {*
Now the type bool is printed out in full detail.
@@ -286,8 +287,8 @@
with the code
*}
-ML %grayML{*PolyML.addPrettyPrinter
- (fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy)*}
+ML %grayML{*ML_system_pp
+ (fn depth => fn _ => ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_typ Theory.get_pure)*}
text {*
After that the types for booleans, lists and so on are printed out again
@@ -817,7 +818,7 @@
fun pretty_tyenv ctxt tyenv =
let
fun get_typs (v, (s, T)) = (TVar (v, s), T)
- val print = pairself (pretty_typ ctxt)
+ val print = apply2 (pretty_typ ctxt)
in
pretty_helper (print o get_typs) tyenv
end*}
@@ -997,7 +998,7 @@
ML %grayML{*fun pretty_env ctxt env =
let
fun get_trms (v, (T, t)) = (Var (v, T), t)
- val print = pairself (pretty_term ctxt)
+ val print = apply2 (pretty_term ctxt)
in
pretty_helper (print o get_trms) env
end*}
@@ -1080,8 +1081,8 @@
val trm_list =
[@{term_pat \"?X\"}, @{term_pat \"a\"},
@{term_pat \"f (\<lambda>a b. ?X a b) c\"},
- @{term_pat \"\<lambda>a b. (op +) a b\"},
- @{term_pat \"\<lambda>a. (op +) a ?Y\"}, @{term_pat \"?X ?Y\"},
+ @{term_pat \"\<lambda>a b. (+) a b\"},
+ @{term_pat \"\<lambda>a. (+) a ?Y\"}, @{term_pat \"?X ?Y\"},
@{term_pat \"\<lambda>a b. ?X a b ?Y\"}, @{term_pat \"\<lambda>a. ?X a a\"},
@{term_pat \"?X a\"}]
in
@@ -1106,7 +1107,7 @@
val trm1 = @{term_pat \"\<lambda>x y. g (?X y x) (f (?Y x))\"}
val trm2 = @{term_pat \"\<lambda>u v. g u (f u)\"}
val init = Envir.empty 0
- val env = Pattern.unify @{theory} (trm1, trm2) init
+ val env = Pattern.unify (Context.Proof @{context}) (trm1, trm2) init (* FIXME: Reference to generic context *)
in
pretty_env @{context} (Envir.term_env env)
end"
@@ -1134,7 +1135,7 @@
val trm2 = @{term "f a"}
val init = Envir.empty 0
in
- Unify.unifiers (@{theory}, init, [(trm1, trm2)])
+ Unify.unifiers (Context.Proof @{context}, init, [(trm1, trm2)])
end *}
text {*
@@ -1171,7 +1172,7 @@
val trm2 = @{term \"b\"}
val init = Envir.empty 0
in
- Unify.unifiers (@{theory}, init, [(trm1, trm2)])
+ Unify.unifiers (Context.Proof @{context}, init, [(trm1, trm2)])
|> Seq.pull
end"
"NONE"}
@@ -1215,12 +1216,12 @@
@{text "?x"}. Instantiation function for theorems is
@{ML_ind instantiate_normalize in Drule} from the structure
@{ML_struct Drule}. One problem, however, is
- that this function expects the instantiations as lists of @{ML_type ctyp}
- and @{ML_type cterm} pairs:
+ that this function expects the instantiations as lists of @{ML_type "((indexname * sort) * ctyp)"}
+ respective @{ML_type "(indexname * typ) * cterm"}:
\begin{isabelle}
@{ML instantiate_normalize in Drule}@{text ":"}
- @{ML_type "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"}
+ @{ML_type "((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> thm -> thm"}
\end{isabelle}
This means we have to transform the environment the higher-order matching
@@ -1231,30 +1232,31 @@
@{ML_type ctyp}-pairs with the function
*}
-ML %grayML{*fun prep_trm thy (x, (T, t)) =
- (cterm_of thy (Var (x, T)), cterm_of thy t)*}
+ML %grayML{*fun prep_trm ctxt (x, (T, t)) =
+ ((x, T), Thm.cterm_of ctxt t)*}
text {*
and into proper @{ML_type cterm}-pairs with
*}
-ML %grayML{*fun prep_ty thy (x, (S, ty)) =
- (ctyp_of thy (TVar (x, S)), ctyp_of thy ty)*}
+ML %grayML{*fun prep_ty ctxt (x, (S, ty)) =
+ ((x, S), Thm.ctyp_of ctxt ty)*}
text {*
We can now calculate the instantiations from the matching function.
*}
-ML %linenosgray{*fun matcher_inst thy pat trm i =
+ML %linenosgray{*fun matcher_inst ctxt pat trm i =
let
- val univ = Unify.matchers thy [(pat, trm)]
+ val univ = Unify.matchers (Context.Proof ctxt) [(pat, trm)]
val env = nth (Seq.list_of univ) i
val tenv = Vartab.dest (Envir.term_env env)
val tyenv = Vartab.dest (Envir.type_env env)
in
- (map (prep_ty thy) tyenv, map (prep_trm thy) tenv)
+ (map (prep_ty ctxt) tyenv, map (prep_trm ctxt) tenv)
end*}
+ML \<open>Context.get_generic_context\<close>
text {*
In Line 3 we obtain the higher-order matcher. We assume there is a finite
number of them and select the one we are interested in via the parameter
@@ -1268,9 +1270,9 @@
@{ML_response_fake [gray,display,linenos]
"let
- val pat = Logic.strip_imp_concl (prop_of @{thm spec})
+ val pat = Logic.strip_imp_concl (Thm.prop_of @{thm spec})
val trm = @{term \"Trueprop (Q True)\"}
- val inst = matcher_inst @{theory} pat trm 1
+ val inst = matcher_inst @{context} pat trm 1
in
Drule.instantiate_normalize inst @{thm spec}
end"
@@ -1429,11 +1431,11 @@
abstract objects that are guaranteed to be type-correct, and they can only
be constructed via ``official interfaces''.
- Certification is always relative to a theory context. For example you can
+ Certification is always relative to a context. For example you can
write:
@{ML_response_fake [display,gray]
- "cterm_of @{theory} @{term \"(a::nat) + b = c\"}"
+ "Thm.cterm_of @{context} @{term \"(a::nat) + b = c\"}"
"a + b = c"}
This can also be written with an antiquotation:
@@ -1457,7 +1459,7 @@
val zero = @{term \"0::nat\"}
val plus = Const (@{const_name plus}, [natT, natT] ---> natT)
in
- cterm_of @{theory} (plus $ zero $ zero)
+ Thm.cterm_of @{context} (plus $ zero $ zero)
end"
"0 + 0"}
@@ -1466,7 +1468,7 @@
the ML-level as follows:
@{ML_response_fake [display,gray]
- "ctyp_of @{theory} (@{typ nat} --> @{typ bool})"
+ "Thm.ctyp_of @{context} (@{typ nat} --> @{typ bool})"
"nat \<Rightarrow> bool"}
or with the antiquotation:
@@ -1575,8 +1577,18 @@
Section~\ref{sec:local}).
*}
+(*FIXME: add forward reference to Proof_Context.export *)
+ML %linenosgray{*val my_thm_vars =
+let
+ val ctxt0 = @{context}
+ val (_, ctxt1) = Variable.add_fixes ["P", "Q", "t"] ctxt0
+in
+ singleton (Proof_Context.export ctxt1 ctxt0) my_thm
+end*}
+
local_setup %gray {*
- Local_Theory.note ((@{binding "my_thm"}, []), [my_thm]) #> snd *}
+ Local_Theory.note ((@{binding "my_thm"}, []), [my_thm_vars]) #> snd *}
+
text {*
The third argument of @{ML note in Local_Theory} is the list of theorems we
@@ -1590,7 +1602,7 @@
local_setup %gray {*
Local_Theory.note ((@{binding "my_thm_simp"},
- [Attrib.internal (K Simplifier.simp_add)]), [my_thm]) #> snd *}
+ [Attrib.internal (K Simplifier.simp_add)]), [my_thm_vars]) #> snd *}
text {*
Note that we have to use another name under which the theorem is stored,
@@ -1720,7 +1732,7 @@
val eq = @{thm True_def}
in
(Thm.lhs_of eq, Thm.rhs_of eq)
- |> pairself (Pretty.string_of o (pretty_cterm @{context}))
+ |> apply2 (Pretty.string_of o (pretty_cterm @{context}))
end"
"(True, (\<lambda>x. x) = (\<lambda>x. x))"}
@@ -1795,7 +1807,7 @@
@{ML_response_fake [display,gray]
"let
val thm = @{thm foo_test1}
- val meta_eq = Object_Logic.atomize @{context} (cprop_of thm)
+ val meta_eq = Object_Logic.atomize @{context} (Thm.cprop_of thm)
in
Raw_Simplifier.rewrite_rule @{context} [meta_eq] thm
end"
@@ -1819,7 +1831,7 @@
ML %grayML{*fun atomize_thm ctxt thm =
let
val thm' = forall_intr_vars thm
- val thm'' = Object_Logic.atomize ctxt (cprop_of thm')
+ val thm'' = Object_Logic.atomize ctxt (Thm.cprop_of thm')
in
Raw_Simplifier.rewrite_rule ctxt [thm''] thm'
end*}
@@ -1839,7 +1851,7 @@
@{ML_response_fake [display,gray]
"let
val trm = @{term \"P \<Longrightarrow> P::bool\"}
- val tac = K (atac 1)
+ val tac = K (assume_tac @{context} 1)
in
Goal.prove @{context} [\"P\"] [] trm tac
end"
@@ -1853,15 +1865,15 @@
theorem by assumption.
There is also the possibility of proving multiple goals at the same time
- using the function @{ML_ind prove_multi in Goal}. For this let us define the
+ using the function @{ML_ind prove_common in Goal}. For this let us define the
following three helper functions.
*}
ML %grayML{*fun rep_goals i = replicate i @{prop "f x = f x"}
-fun rep_tacs i = replicate i (rtac @{thm refl})
+fun rep_tacs i = replicate i (resolve_tac @{context} [@{thm refl}])
fun multi_test ctxt i =
- Goal.prove_multi ctxt ["f", "x"] [] (rep_goals i)
+ Goal.prove_common ctxt NONE ["f", "x"] [] (rep_goals i)
(K ((Goal.conjunction_tac THEN' RANGE (rep_tacs i)) 1))*}
text {*
@@ -1872,7 +1884,7 @@
"multi_test @{context} 3"
"[\"?f ?x = ?f ?x\", \"?f ?x = ?f ?x\", \"?f ?x = ?f ?x\"]"}
- However you should be careful with @{ML prove_multi in Goal} and very
+ However you should be careful with @{ML prove_common in Goal} and very
large goals. If you increase the counter in the code above to @{text 3000},
you will notice that takes approximately ten(!) times longer than
using @{ML map} and @{ML prove in Goal}.
@@ -1880,7 +1892,7 @@
ML %grayML{*let
fun test_prove ctxt thm =
- Goal.prove ctxt ["P", "x"] [] thm (K (rtac @{thm refl} 1))
+ Goal.prove ctxt ["P", "x"] [] thm (K (resolve_tac @{context} [@{thm refl}] 1))
in
map (test_prove @{context}) (rep_goals 3000)
end*}
@@ -1991,8 +2003,8 @@
*}
ML %grayML{*fun pthms_of (PBody {thms, ...}) = map #2 thms
-val get_names = map #1 o pthms_of
-val get_pbodies = map (Future.join o #3) o pthms_of *}
+val get_names = (map Proofterm.thm_node_name) o pthms_of
+val get_pbodies = map (Future.join o Proofterm.thm_node_body) o pthms_of *}
text {*
To see what their purpose is, consider the following three short proofs.
@@ -2248,7 +2260,7 @@
this attribute is
*}
-ML %grayML{*val my_symmetric = Thm.rule_attribute (fn _ => fn thm => thm RS @{thm sym})*}
+ML %grayML{*val my_symmetric = Thm.rule_attribute [] (fn _ => fn thm => thm RS @{thm sym})*}
text {*
where the function @{ML_ind rule_attribute in Thm} expects a function taking a
@@ -2313,7 +2325,7 @@
let
fun RS_rev thm1 thm2 = thm2 RS thm1
in
- Thm.rule_attribute (fn _ => fn thm => fold RS_rev thms thm)
+ Thm.rule_attribute [] (fn _ => fn thm => fold RS_rev thms thm)
end*}
text {*
@@ -2715,8 +2727,8 @@
and type. For example:
@{ML_response_fake [display,gray]
- "tell_type @{context} @{term \"op = (op = (op = (op = (op = op =))))\"}"
- "The term \"op = (op = (op = (op = (op = op =))))\" has type
+ "tell_type @{context} @{term \"(=) ((=) ((=) ((=) ((=) (=)))))\"}"
+ "The term \"(=) ((=) ((=) ((=) ((=) (=)))))\" has type
\"((((('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool\"."}
\begin{readmore}
--- a/ProgTutorial/First_Steps.thy Fri Jun 03 15:15:17 2016 +0100
+++ b/ProgTutorial/First_Steps.thy Tue May 14 11:10:53 2019 +0200
@@ -4,6 +4,8 @@
chapter {* First Steps\label{chp:firststeps} *}
+
+
text {*
\begin{flushright}
{\em ``The most effective debugging tool is still careful thought,\\
@@ -12,7 +14,7 @@
\end{flushright}
\medskip
- Isabelle programming is done in ML. Just like lemmas and proofs, ML-code for
+ Isabelle programming is done in ML @{cite "isa-imp"}. Just like lemmas and proofs, ML-code for
Isabelle must be part of a theory. If you want to follow the code given in
this chapter, we assume you are working inside the theory starting with
@@ -179,7 +181,7 @@
*}
ML %grayML %grayML{*fun pretty_cterm ctxt ctrm =
- pretty_term ctxt (term_of ctrm)*}
+ pretty_term ctxt (Thm.term_of ctrm)*}
text {*
Here the function @{ML_ind term_of in Thm} extracts the @{ML_type
@@ -196,7 +198,7 @@
*}
ML %grayML{*fun pretty_thm ctxt thm =
- pretty_term ctxt (prop_of thm)*}
+ pretty_term ctxt (Thm.prop_of thm)*}
text {*
Theorems include schematic variables, such as @{text "?P"},
@@ -217,7 +219,7 @@
let
val ctxt' = Config.put show_question_marks false ctxt
in
- pretty_term ctxt' (prop_of thm)
+ pretty_term ctxt' (Thm.prop_of thm)
end*}
text {*
@@ -249,7 +251,7 @@
respectively @{ML_type ctyp}
*}
-ML %grayML{*fun pretty_ctyp ctxt cty = pretty_typ ctxt (typ_of cty)
+ML %grayML{*fun pretty_ctyp ctxt cty = pretty_typ ctxt (Thm.typ_of cty)
fun pretty_ctyps ctxt ctys =
Pretty.block (Pretty.commas (map (pretty_ctyp ctxt) ctys))*}
@@ -626,24 +628,24 @@
A more realistic example for this combinator is the following code
*}
-ML %grayML{*val (((one_def, two_def), three_def), ctxt') =
+ML %grayML{*val ((([one_def], [two_def]), [three_def]), ctxt') =
@{context}
- |> Local_Defs.add_def ((@{binding "One"}, NoSyn), @{term "1::nat"})
- ||>> Local_Defs.add_def ((@{binding "Two"}, NoSyn), @{term "2::nat"})
- ||>> Local_Defs.add_def ((@{binding "Three"}, NoSyn), @{term "3::nat"})*}
+ |> Local_Defs.define [((@{binding "One"}, NoSyn), (Binding.empty_atts, @{term "1::nat"}))]
+ ||>> Local_Defs.define [((@{binding "Two"}, NoSyn), (Binding.empty_atts,@{term "2::nat"}))]
+ ||>> Local_Defs.define [((@{binding "Three"}, NoSyn), (Binding.empty_atts,@{term "3::nat"}))]*}
text {*
where we make three definitions, namely @{term "One \<equiv> 1::nat"}, @{term "Two \<equiv> 2::nat"}
and @{term "Three \<equiv> 3::nat"}. The point of this code is that we augment the initial
context with the definitions. The result we are interested in is the
augmented context, that is @{ML_text "ctxt'"}, but also the side-results containing
- information about the definitions---the function @{ML_ind add_def in Local_Defs} returns
+ information about the definitions---the function @{ML_ind define in Local_Defs} returns
both as pairs. We can use this information for example to print out the definiens and
the theorem corresponding to the definitions. For example for the first definition:
@{ML_response_fake [display, gray]
"let
- val (one_trm, one_thm) = one_def
+ val (one_trm, (_, one_thm)) = one_def
in
pwriteln (pretty_term ctxt' one_trm);
pwriteln (pretty_thm ctxt' one_thm)
@@ -775,7 +777,7 @@
defined abbreviations. For example
@{ML_response_fake [display, gray]
- "Proof_Context.print_abbrevs @{context}"
+ "Proof_Context.print_abbrevs false @{context}"
"\<dots>
INTER \<equiv> INFI
Inter \<equiv> Inf
@@ -864,7 +866,7 @@
ML %linenosgray{*val term_pat_setup =
let
- val parser = Args.context -- Scan.lift Args.name_inner_syntax
+ val parser = Args.context -- Scan.lift Args.embedded_inner_syntax
fun term_pat (ctxt, str) =
str |> Proof_Context.read_term_pattern ctxt
@@ -897,7 +899,7 @@
ML %grayML{*val type_pat_setup =
let
- val parser = Args.context -- Scan.lift Args.name_inner_syntax
+ val parser = Args.context -- Scan.lift Args.embedded_inner_syntax
fun typ_pat (ctxt, str) =
let
@@ -921,7 +923,7 @@
However, a word of warning is in order: new antiquotations should be introduced only after
careful deliberations. They can potentially make your code harder, rather than easier, to read.
- \begin{readmore}
+ \begin{readmore} @{url "Norbert/ML/ml_antiquotation.ML"}
The files @{ML_file "Pure/ML/ml_antiquotation.ML"} and @{ML_file "Pure/ML/ml_antiquotations.ML"}
contain the infrastructure and definitions for most antiquotations. Most of the basic operations
on ML-syntax are implemented in @{ML_file "Pure/ML/ml_syntax.ML"}.
@@ -947,9 +949,8 @@
in a type-safe manner...though run-time checks are needed for that.
\begin{readmore}
- In Isabelle the universal type is implemented as the type @{ML_type
- Universal.universal} in the file
- @{ML_file "Pure/ML-Systems/universal.ML"}.
+ In ML the universal type is implemented as the type @{ML_type
+ Universal.universal}.
\end{readmore}
We will show the usage of the universal type by storing an integer and
@@ -1344,6 +1345,7 @@
in the simplifier. This can be used for example in the following proof
*}
+
lemma
shows "(False \<or> True) \<and> True"
proof (rule conjI)
--- a/ProgTutorial/Package/Ind_Code.thy Fri Jun 03 15:15:17 2016 +0100
+++ b/ProgTutorial/Package/Ind_Code.thy Tue May 14 11:10:53 2019 +0200
@@ -27,7 +27,7 @@
ML %linenosgray{*fun make_defn ((predname, mx), trm) lthy =
let
- val arg = ((predname, mx), (Attrib.empty_binding, trm))
+ val arg = ((predname, mx), (Binding.empty_atts, trm))
val ((_, (_ , thm)), lthy') = Local_Theory.define arg lthy
in
(thm, lthy')
@@ -35,7 +35,7 @@
text {*
It returns the definition (as a theorem) and the local theory in which the
- definition has been made. We use @{ML_ind empty_binding in Attrib} in Line 3,
+ definition has been made. We use @{ML_ind empty_atts in Binding} in Line 3,
since the definitions for our inductive predicates are not meant to be seen
by the user and therefore do not need to have any theorem attributes.
@@ -136,8 +136,7 @@
ML %linenosgray{*fun defns rules preds prednames mxs arg_typss lthy =
let
- val thy = Proof_Context.theory_of lthy
- val orules = map (Object_Logic.atomize_term thy) rules
+ val orules = map (Object_Logic.atomize_term lthy) rules
val defs = map (defn_aux lthy orules preds) (preds ~~ arg_typss)
in
fold_map make_defn (prednames ~~ mxs ~~ defs) lthy
@@ -215,20 +214,20 @@
ML %grayML{*fun inst_spec ctrm =
let
- val cty = ctyp_of_term ctrm
+ val cty = Thm.ctyp_of_cterm ctrm
in
- Drule.instantiate' [SOME cty] [NONE, SOME ctrm] @{thm spec}
+ Thm.instantiate' [SOME cty] [NONE, SOME ctrm] @{thm spec}
end*}
text {*
- This helper function uses the function @{ML_ind instantiate' in Drule}
+ This helper function uses the function @{ML_ind instantiate' in Thm}
and instantiates the @{text "?x"} in the theorem @{thm spec} with a given
@{ML_type cterm}. We call this helper function in the following
tactic.\label{fun:instspectac}.
*}
-ML %grayML{*fun inst_spec_tac ctrms =
- EVERY' (map (dtac o inst_spec) ctrms)*}
+ML %grayML{*fun inst_spec_tac ctxt ctrms =
+ EVERY' (map (dresolve_tac ctxt o single o inst_spec) ctrms)*}
text {*
This tactic expects a list of @{ML_type cterm}s. It allows us in the
@@ -239,7 +238,7 @@
fixes P::"nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
shows "\<forall>x y z. P x y z \<Longrightarrow> True"
apply (tactic {*
- inst_spec_tac [@{cterm "a::nat"},@{cterm "b::nat"},@{cterm "c::nat"}] 1 *})
+ inst_spec_tac @{context} [@{cterm "a::nat"},@{cterm "b::nat"},@{cterm "c::nat"}] 1 *})
txt {*
We obtain the goal state
@@ -257,8 +256,8 @@
EVERY1 [Object_Logic.full_atomize_tac ctxt,
cut_facts_tac prem,
rewrite_goal_tac ctxt defs,
- inst_spec_tac insts,
- assume_tac]*}
+ inst_spec_tac ctxt insts,
+ assume_tac ctxt]*}
text {*
We have to give it as arguments the definitions, the premise (a list of
@@ -405,11 +404,9 @@
val Ps = replicate (length preds) "P"
val (newprednames, lthy') = Variable.variant_fixes Ps lthy
- val thy = Proof_Context.theory_of lthy'
-
val tyss' = map (fn tys => tys ---> HOLogic.boolT) arg_tyss
val newpreds = map Free (newprednames ~~ tyss')
- val cnewpreds = map (cterm_of thy) newpreds
+ val cnewpreds = map (Thm.cterm_of lthy') newpreds
val srules = map (subst_free (preds ~~ newpreds)) rules
in
@@ -422,16 +419,14 @@
In Line 3, we generate a string @{text [quotes] "P"} for each predicate.
In Line 4, we use the same trick as in the previous function, that is making the
@{text "Ps"} fresh and declaring them as free, but fixed, in
- the new local theory @{text "lthy'"}. From the local theory we extract
- the ambient theory in Line 6. We need this theory in order to certify
- the new predicates. In Line 8, we construct the types of these new predicates
+ the new local theory @{text "lthy'"}. In Line 6, we construct the types of these new predicates
using the given argument types. Next we turn them into terms and subsequently
- certify them (Line 9 and 10). We can now produce the substituted introduction rules
- (Line 11) using the function @{ML_ind subst_free in Term}. Line 14 and 15 just iterate
+ certify them (Line 7 and 8). We can now produce the substituted introduction rules
+ (Line 9) using the function @{ML_ind subst_free in Term}. Line 12 and 13 just iterate
the proofs for all predicates.
From this we obtain a list of theorems. Finally we need to export the
fixed variables @{text "Ps"} to obtain the schematic variables @{text "?Ps"}
- (Line 16).
+ (Line 14).
A testcase for this function is
*}
@@ -542,7 +537,7 @@
ML %linenosgray{*fun expand_tac ctxt defs =
Object_Logic.rulify_tac ctxt 1
THEN rewrite_goal_tac ctxt defs 1
- THEN (REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1)) *}
+ THEN (REPEAT (resolve_tac ctxt [@{thm allI}, @{thm impI}] 1)) *}
text {*
The function in Line 2 ``rulifies'' the lemma.\footnote{FIXME: explain this better}
@@ -679,7 +674,7 @@
@{term [display] "\<forall>a b t. a \<noteq> b \<longrightarrow> fresh a t \<longrightarrow> fresh a (Lam a t)"}
- To use this premise with @{ML rtac}, we need to instantiate its
+ To use this premise with @{ML resolve_tac}, we need to instantiate its
quantifiers (with @{text params1}) and transform it into rule
format (using @{ML_ind rulify in Object_Logic}). So we can modify the
code as follows:
@@ -692,7 +687,7 @@
val (params1, params2) = chop (length cparams - length preds) cparams
val (prems1, prems2) = chop (length prems - length rules) prems
in
- rtac (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 {*
@@ -744,12 +739,12 @@
we can implement the following function
*}
-ML %grayML{*fun prepare_prem params2 prems2 prem =
- rtac (case prop_of prem of
+ML %grayML{*fun prepare_prem ctxt params2 prems2 prem =
+ resolve_tac ctxt [case Thm.prop_of prem of
_ $ (Const (@{const_name All}, _) $ _) =>
prem |> all_elims params2
|> imp_elims prems2
- | _ => prem) *}
+ | _ => prem] *}
text {*
which either applies the premise outright (the default case) or if
@@ -765,8 +760,8 @@
val (params1, params2) = chop (length cparams - length preds) cparams
val (prems1, prems2) = chop (length prems - length rules) prems
in
- rtac (Object_Logic.rulify context (all_elims params1 (nth prems2 i))) 1
- THEN EVERY1 (map (prepare_prem params2 prems2) prems1)
+ resolve_tac context [Object_Logic.rulify context (all_elims params1 (nth prems2 i))] 1
+ THEN EVERY1 (map (prepare_prem context params2 prems2) prems1)
end) *}
text {*
@@ -835,11 +830,11 @@
let
val prem' = prems MRS prem
in
- rtac (case prop_of prem' of
+ resolve_tac ctxt [case Thm.prop_of prem' of
_ $ (Const (@{const_name All}, _) $ _) =>
prem' |> all_elims params2
|> imp_elims prems2
- | _ => prem') 1
+ | _ => prem'] 1
end) ctxt *}
text {*
@@ -864,7 +859,7 @@
val (params1, params2) = chop (length cparams - length preds) cparams
val (prems1, prems2) = chop (length prems - length rules) prems
in
- rtac (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) *}
@@ -887,7 +882,7 @@
ML %linenosgray{*fun intro_tac defs rules preds i ctxt =
EVERY1 [Object_Logic.rulify_tac ctxt,
rewrite_goal_tac ctxt defs,
- REPEAT o (resolve_tac [@{thm allI}, @{thm impI}]),
+ REPEAT o (resolve_tac ctxt [@{thm allI}, @{thm impI}]),
prove_intro_tac i preds rules ctxt]*}
text {*
--- a/ProgTutorial/Package/Ind_Extensions.thy Fri Jun 03 15:15:17 2016 +0100
+++ b/ProgTutorial/Package/Ind_Extensions.thy Tue May 14 11:10:53 2019 +0200
@@ -208,7 +208,7 @@
datatype foo = Foo nat
local_setup{*Function.add_function [(@{binding "baz"}, NONE, NoSyn)]
- [(Attrib.empty_binding, @{term "\<And>x. baz (Foo x) = x"})]
+ [((Binding.empty_atts,@{term "\<And>x. baz (Foo x) = x"}),[],[])]
conf pat_completeness_auto #> snd*}
(*<*)end(*>*)
--- a/ProgTutorial/Package/Ind_General_Scheme.thy Fri Jun 03 15:15:17 2016 +0100
+++ b/ProgTutorial/Package/Ind_General_Scheme.thy Tue May 14 11:10:53 2019 +0200
@@ -57,8 +57,8 @@
\begin{isabelle}
@{text "rule ::=
- \<And>xs. \<^raw:$\underbrace{\mbox{>As\<^raw:}}_{\text{\makebox[0mm]{\rm non-recursive premises}}}$> \<Longrightarrow>
- \<^raw:$\underbrace{\mbox{>(\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>*\<^raw:}}_{\text{\rm recursive premises}}$>
+ \<And>xs. \<^latex>\<open>$\\underbrace{\\mbox{\<close>As\<^latex>\<open>}}_{\\text{\\makebox[0mm]{\\rm non-recursive premises}}}$\<close> \<Longrightarrow>
+ \<^latex>\<open>$\\underbrace{\\mbox{\<close>(\<And>ys. Bs \<Longrightarrow> pred ss)\<^sup>*\<^latex>\<open>}}_{\\text{\\rm recursive premises}}$>\<close>
\<Longrightarrow> pred ts"}
\end{isabelle}
--- a/ProgTutorial/Package/Ind_Interface.thy Fri Jun 03 15:15:17 2016 +0100
+++ b/ProgTutorial/Package/Ind_Interface.thy Tue May 14 11:10:53 2019 +0200
@@ -62,7 +62,7 @@
*}
ML %grayML{*val spec_parser =
- Parse.fixes --
+ Parse.vars --
Scan.optional
(Parse.$$$ "where" |--
Parse.!!!
@@ -96,7 +96,7 @@
where
accpartI: "(\<And>y. R y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x"
(*<*)ML %no{*fun filtered_input str =
- filter Token.is_proper (Outer_Syntax.scan (Keyword.get_lexicons ()) Position.none str)
+ filter Token.is_proper (Token.explode (Thy_Header.get_keywords' @{context}) Position.none str)
fun parse p input = Scan.finite Token.stopper (Scan.error p) input*}(*>*)
text {*
Note that in these definitions the parameter @{text R}, standing for the
@@ -129,12 +129,12 @@
done in Lines 5 to 7 in the code below.
*}
(*<*)ML %no{*fun add_inductive_cmd pred_specs rule_specs lthy = lthy
- fun add_inductive pred_specs rule_specs lthy = lthy*}(*>*)
-ML_val %linenosgray{*val specification : (local_theory -> local_theory) parser =
+ fun add_inductive pred_specs rule_specs lthy = lthy*}(*>*) (* FIXME: Is the dummy simple_inductive2 installed with ML, before there was ML_val*)
+ML %linenosgray{*val specification : (local_theory -> local_theory) parser =
spec_parser >>
(fn (pred_specs, rule_specs) => add_inductive_cmd pred_specs rule_specs)
-val _ = Outer_Syntax.local_theory @{command_spec "simple_inductive2"}
+val _ = Outer_Syntax.local_theory @{command_keyword "simple_inductive2"}
"definition of simple inductive predicates"
specification*}
@@ -152,19 +152,19 @@
eventually will be). Also the introduction rules are just strings. What we have
to do first is to transform the parser's output into some internal
datastructures that can be processed further. For this we can use the
- function @{ML_ind read_spec in Specification}. This function takes some strings
+ function @{ML_ind read_multi_specs in Specification}. This function takes some strings
(with possible typing annotations) and some rule specifications, and attempts
to find a typing according to the given type constraints given by the
user and the type constraints by the ``ambient'' theory. It returns
the type for the predicates and also returns typed terms for the
introduction rules. So at the heart of the function
- @{text "add_inductive_cmd"} is a call to @{ML read_spec in Specification}.
+ @{text "add_inductive_cmd"} is a call to @{ML read_multi_specs in Specification}.
*}
ML_val%grayML{*fun add_inductive_cmd pred_specs rule_specs lthy =
let
val ((pred_specs', rule_specs'), _) =
- Specification.read_spec pred_specs rule_specs lthy
+ Specification.read_multi_specs pred_specs rule_specs lthy
in
add_inductive pred_specs' rule_specs' lthy
end*}
--- a/ProgTutorial/Package/Ind_Prelims.thy Fri Jun 03 15:15:17 2016 +0100
+++ b/ProgTutorial/Package/Ind_Prelims.thy Tue May 14 11:10:53 2019 +0200
@@ -169,7 +169,7 @@
apply(unfold trcl_def)
apply(blast)
done
-
+term "even"
text {*
Experience has shown that it is generally a bad idea to rely heavily on
@{text blast}, @{text auto} and the like in automated proofs. The reason is
@@ -194,7 +194,10 @@
below @{text "P"} and @{text "Q"}).
*}
-definition "even \<equiv>
+hide_const even
+hide_const odd
+
+definition "even \<equiv>
\<lambda>n. \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m))
\<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> P n"
--- a/ProgTutorial/Package/Simple_Inductive_Package.thy Fri Jun 03 15:15:17 2016 +0100
+++ b/ProgTutorial/Package/Simple_Inductive_Package.thy Tue May 14 11:10:53 2019 +0200
@@ -5,7 +5,7 @@
ML_file "simple_inductive_package.ML"
-(*
+
simple_inductive
trcl :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
where
@@ -16,6 +16,7 @@
thm trcl.induct
thm trcl.intros
+(*
simple_inductive
even and odd
where
--- a/ProgTutorial/Package/simple_inductive_package.ML Fri Jun 03 15:15:17 2016 +0100
+++ b/ProgTutorial/Package/simple_inductive_package.ML Tue May 14 11:10:53 2019 +0200
@@ -49,8 +49,7 @@
(* @chunk definitions *)
fun definitions rules params preds prednames syns arg_typess lthy =
let
- val thy = Proof_Context.theory_of lthy
- val orules = map (Object_Logic.atomize_term thy) rules
+ val orules = map (Object_Logic.atomize_term lthy) rules
val defs =
map (defs_aux lthy orules preds params) (preds ~~ arg_typess)
in
@@ -59,15 +58,18 @@
(* @end *)
fun inst_spec ct =
- Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec};
+ Thm.instantiate' [SOME (Thm.ctyp_of_cterm ct)] [NONE, SOME ct] @{thm spec};
+
+fun dtac ctxt thm = dresolve_tac ctxt [thm]
+fun rtac ctxt thm = resolve_tac ctxt [thm]
(* @chunk induction_tac *)
fun induction_tac ctxt defs prems insts =
EVERY1 [Object_Logic.full_atomize_tac ctxt,
cut_facts_tac prems,
rewrite_goal_tac ctxt defs,
- EVERY' (map (dtac o inst_spec) insts),
- assume_tac]
+ EVERY' (map (dtac ctxt o inst_spec) insts),
+ assume_tac ctxt]
(* @end *)
(* @chunk induction_rules *)
@@ -77,12 +79,10 @@
val Ps = replicate (length preds) "P"
val (newprednames, lthy3) = Variable.variant_fixes Ps lthy2
-
- val thy = Proof_Context.theory_of lthy3
-
+
val Tss' = map (fn Ts => Ts ---> HOLogic.boolT) Tss
val newpreds = map Free (newprednames ~~ Tss')
- val cnewpreds = map (cterm_of thy) newpreds
+ val cnewpreds = map (Thm.cterm_of lthy3) newpreds
val rules' = map (subst_free (preds ~~ newpreds)) rules
fun prove_induction ((pred, newpred), Ts) =
@@ -110,17 +110,17 @@
(* @chunk subproof1 *)
fun subproof2 prem params2 prems2 =
- SUBPROOF (fn {prems, ...} =>
+ SUBPROOF (fn {prems, context, ...} =>
let
val prem' = prems MRS prem;
val prem'' =
- case prop_of prem' of
+ case Thm.prop_of prem' of
_ $ (Const (@{const_name All}, _) $ _) =>
prem' |> all_elims params2
|> imp_elims prems2
| _ => prem';
in
- rtac prem'' 1
+ rtac context prem'' 1
end)
(* @end *)
@@ -131,7 +131,7 @@
val (prems1, prems2) = chop (length prems - length rules) prems;
val (params1, params2) = chop (length params - length preds) (map snd params);
in
- rtac (Object_Logic.rulify ctxt' (all_elims params1 (nth prems2 i))) 1
+ rtac ctxt' (Object_Logic.rulify ctxt' (all_elims params1 (nth prems2 i))) 1
THEN
EVERY1 (map (fn prem => subproof2 prem params2 prems2 ctxt') prems1)
end)
@@ -140,7 +140,7 @@
fun introductions_tac defs rules preds i ctxt =
EVERY1 [Object_Logic.rulify_tac ctxt,
rewrite_goal_tac ctxt defs,
- REPEAT o (resolve_tac [@{thm allI},@{thm impI}]),
+ REPEAT o (resolve_tac ctxt [@{thm allI},@{thm impI}]),
subproof1 rules preds i ctxt]
@@ -194,16 +194,15 @@
|> snd
end
(* @end *)
-
+val _ = Proof_Context.read_stmt
(* @chunk read_specification *)
fun read_specification' vars specs lthy =
let
- val specs' = map (fn (a, s) => (a, [s])) specs
- val ((varst, specst), _) =
- Specification.read_specification vars specs' lthy
- val specst' = map (apsnd the_single) specst
+ val specs' = map (fn (a, s) => ((a, s), [],[])) specs
+ val ((varst, specst),_) =
+ Specification.read_multi_specs vars specs' lthy
in
- (varst, specst')
+ (varst, specst)
end
(* @end *)
@@ -221,7 +220,7 @@
(* @chunk parser *)
val spec_parser =
Parse.opt_target --
- Parse.fixes --
+ Parse.vars --
Parse.for_fixes --
Scan.optional
(Parse.$$$ "where" |--
@@ -234,10 +233,11 @@
val specification =
spec_parser >>
(fn (((loc, preds), params), specs) =>
- Toplevel.local_theory loc (add_inductive preds params specs))
+ Toplevel.local_theory NONE loc (add_inductive preds params specs))
-val _ = Outer_Syntax.command @{command_spec "simple_inductive"} "define inductive predicates"
+val _ = Outer_Syntax.command @{command_keyword "simple_inductive"} "define inductive predicates"
specification
+
(* @end *)
end;
--- a/ProgTutorial/ROOT.ML Fri Jun 03 15:15:17 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-quick_and_dirty := true;
-
-no_document use_thy "Base";
-no_document use_thy "Package/Simple_Inductive_Package";
-no_document use_thy "~~/src/HOL/Number_Theory/Primes";
-no_document use_thy "~~/src/HOL/Library/Efficient_Nat";
-
-use_thy "Intro";
-use_thy "First_Steps";
-use_thy "Essential";
-use_thy "Advanced";
-
-no_document use_thy "Helper/Command/Command";
-use_thy "Parsing";
-use_thy "Tactical";
-
-use_thy "Package/Ind_Intro";
-use_thy "Package/Ind_Prelims";
-use_thy "Package/Ind_Interface";
-use_thy "Package/Ind_General_Scheme";
-use_thy "Package/Ind_Code";
-use_thy "Package/Ind_Extensions";
-
-use_thy "Appendix";
-use_thy "Recipes/Antiquotes";
-use_thy "Recipes/TimeLimit";
-use_thy "Recipes/Timing";
-use_thy "Recipes/CallML";
-use_thy "Recipes/ExternalSolver";
-use_thy "Recipes/Oracle";
-use_thy "Recipes/Sat";
-use_thy "Recipes/USTypes";
-
-use_thy "Solutions";
-(*use_thy "Readme";*)
-
--- a/ProgTutorial/Recipes/Antiquotes.thy Fri Jun 03 15:15:17 2016 +0100
+++ b/ProgTutorial/Recipes/Antiquotes.thy Tue May 14 11:10:53 2019 +0200
@@ -39,21 +39,24 @@
document antiquotation is as follows:
*}
+ML \<open>Input.pos_of\<close>
+ML%linenosgray{*fun ml_enclose bg en source =
+ ML_Lex.read bg @ ML_Lex.read_source false source @ ML_Lex.read en;*}
-ML%linenosgray{*fun ml_val code_txt = "val _ = " ^ code_txt
+ML%linenosgray{*fun ml_val code_txt = (ml_enclose "val _ = " "" code_txt)
-fun output_ml {context = ctxt, ...} code_txt =
+fun output_ml ctxt code_txt =
let
- val srcpos = {delimited = false, text = (ml_val code_txt), pos = Position.none}
-in
- (ML_Context.eval_source_in (SOME ctxt) ML_Compiler.flags srcpos;
- Thy_Output.output ctxt (map Pretty.str (space_explode "\n" code_txt)))
+ 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)
end
-val ml_checked_setup = Thy_Output.antiquotation @{binding "ML_checked"} (Scan.lift Args.name) 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 *}
+
text {*
The parser @{ML "(Scan.lift Args.name)"} in Line 7 parses a string, in this
case the code, and then calls the function @{ML output_ml}. As mentioned
@@ -61,13 +64,13 @@
function @{ML ml_val}, which constructs the appropriate ML-expression, and
using @{ML "eval_in" in ML_Context}, which calls the compiler. If the code is
``approved'' by the compiler, then the output function @{ML "output" in
- Thy_Output} in the next line pretty prints the code. This function expects
+ Document_Antiquotation} in the next line pretty prints the code. This function expects
that the code is a list of (pretty)strings where each string correspond to a
line in the output. Therefore the use of @{ML "(space_explode \"\\n\" txt)"
for txt} which produces such a list according to linebreaks. There are a
number of options for antiquotations that are observed by the function
- @{ML "output" in Thy_Output} when printing the code (including @{text "[display]"}
- and @{text "[quotes]"}). The function @{ML "antiquotation" in Thy_Output} in
+ @{ML "output" in Document_Antiquotation} when printing the code (including @{text "[display]"}
+ and @{text "[quotes]"}). The function @{ML "antiquotation_raw" in Thy_Output} in
Line 7 sets up the new document antiquotation.
\begin{readmore}
@@ -78,27 +81,32 @@
information about the line number, in case an error is detected. We
can improve the code above slightly by writing
*}
-
-ML%linenosgray{*fun output_ml {context = ctxt, ...} (code_txt, pos) =
+(* 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;
- Thy_Output.output ctxt (map Pretty.str (space_explode "\n" code_txt)))
+ 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
result.
We can now write @{text "@{ML_checked2 \"2 + 3\"}"} in a document in order to
- obtain @{ML_checked2 "2 + 3"} and be sure that this code compiles until
+ obtain @{ML_checked "2 + 3"} and be sure that this code compiles until
somebody changes the definition of addition.
@@ -121,13 +129,17 @@
function will do this:
*}
-ML %grayML{*fun ml_pat (code_txt, pat) =
+ML%linenosgray{*fun ml_pat pat code =
+ ML_Lex.read "val" @ ML_Lex.read_source false pat @ ML_Lex.read " = " @ ML_Lex.read_source false code*}
+
+(*
+ML %grayML{*fun ml_pat code_txt pat =
let val pat' =
implode (map (fn "\<dots>" => "_" | s => s) (Symbol.explode pat))
in
- "val " ^ pat' ^ " = " ^ code_txt
+ ml_enclose ("val " ^ pat' ^ " = ") "" code_txt
end*}
-
+*)
text {*
Next we add a response indicator to the result using:
*}
@@ -139,6 +151,21 @@
The rest of the code of @{text "ML_resp"} is:
*}
+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 code = space_explode "\n" (Input.source_content code_txt)
+ val resp = add_resp (space_explode "\n" (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
+
+\<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}
@@ -154,13 +181,14 @@
val ml_resp_setup = Thy_Output.antiquotation @{binding "ML_resp"}
- (Scan.lift (Parse.position (Args.name -- Args.name)))
+ (Scan.lift (Parse.position (Args.text_input -- Args.text_input)))
output_ml_resp*}
+*)
+setup {* ml_response_setup *}
-setup {* ml_resp_setup *}
-
-text {*
- In comparison with @{text "ML_checked2"}, we only changed the line about
+(* FIXME *)
+text {*
+ In comparison with @{text "ML_checked"}, we only changed the line about
the compiler (Line~2), the lines about
the output (Lines 4 to 7) and the parser in the setup (Line 11). Now
you can write
@@ -177,7 +205,7 @@
to obtain
- @{ML_resp [display] "let val i = 3 in (i * i, \"foo\") end" "(9, \<dots>)"}
+ @{ML_resp [display] "let val i = 3 in (i * i, \"foo\") end" "(9, _)"}
In both cases, the check by the compiler ensures that code and result
match. A limitation of this document antiquotation, however, is that the
--- a/ProgTutorial/Recipes/ExternalSolver.thy Fri Jun 03 15:15:17 2016 +0100
+++ b/ProgTutorial/Recipes/ExternalSolver.thy Tue May 14 11:10:53 2019 +0200
@@ -28,8 +28,8 @@
one second:
@{ML_response_fake [display,gray]
- "TimeLimit.timeLimit (Time.fromSeconds 1) Isabelle_System.bash_output \"sleep 30\"
- handle TimeLimit.TimeOut => (\"timeout\", ~1)" "(\"timeout\", ~1)"}
+ "Timeout.apply (Time.fromSeconds 1) Isabelle_System.bash_output \"sleep 30\"
+ handle TIMEOUT => (\"timeout\", ~1)" "(\"timeout\", ~1)"}
The function @{ML bash_output in Isabelle_System} can also be used for more reasonable
applications, e.g. coupling external solvers with Isabelle. In that case,
--- a/ProgTutorial/Recipes/Introspection.thy Fri Jun 03 15:15:17 2016 +0100
+++ b/ProgTutorial/Recipes/Introspection.thy Tue May 14 11:10:53 2019 +0200
@@ -17,8 +17,8 @@
*}
ML %grayML{*fun pthms_of (PBody {thms, ...}) = map #2 thms
-val get_names = map #1 o pthms_of
-val get_pbodies = map (Future.join o #3) o pthms_of *}
+val get_names = (map Proofterm.thm_node_name) o pthms_of
+val get_pbodies = map (Future.join o Proofterm.thm_node_body) o pthms_of *}
text {*
To see what their purpose is, consider the following three short proofs.
@@ -57,7 +57,8 @@
|> Thm.proof_body_of
|> get_names"
"[\"Introspection.my_conjIa\"]"}
-
+*}
+text {*
whereby @{text "Introspection"} refers to the theory name in which
we established the theorem @{thm [source] my_conjIa}. The function @{ML_ind
proof_body_of in Thm} returns a part of the data that is stored in a
@@ -66,7 +67,7 @@
and @{thm [source] conjunct2}. We can obtain them by descending into the
first level of the proof-tree, as follows.
- @{ML_response [display,gray]
+ @{ML_response_fake [display,gray]
"@{thm my_conjIa}
|> Thm.proof_body_of
|> get_pbodies
@@ -74,41 +75,44 @@
|> List.concat"
"[\"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.conjI\", \"Pure.protectD\",
\"Pure.protectI\"]"}
-
+*}
+text {*
The theorems @{thm [source] protectD} and @{thm [source]
protectI} that are internal theorems are always part of a
proof in Isabelle. Note also that applications of @{text assumption} do not
count as a separate theorem, as you can see in the following code.
- @{ML_response [display,gray]
+ @{ML_response_fake [display,gray]
"@{thm my_conjIb}
|> Thm.proof_body_of
|> get_pbodies
|> map get_names
|> List.concat"
"[\"Pure.protectD\", \"Pure.protectI\"]"}
-
+*}
+text {*
Interestingly, but not surprisingly, the proof of @{thm [source]
my_conjIc} procceeds quite differently from @{thm [source] my_conjIa}
and @{thm [source] my_conjIb}, as can be seen by the theorems that
are returned for @{thm [source] my_conjIc}.
- @{ML_response [display,gray]
+ @{ML_response_fake [display,gray]
"@{thm my_conjIc}
|> Thm.proof_body_of
|> get_pbodies
|> map get_names
|> List.concat"
- "[\"HOL.Eq_TrueI\", \"HOL.simp_thms_25\", \"HOL.eq_reflection\",
- \"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.TrueI\", \"Pure.protectD\",
- \"Pure.protectI\"]"}
-
+ "[\"HOL.implies_True_equals\", \"HOL.Eq_TrueI\", \"HOL.simp_thms_25\", \"HOL.eq_reflection\",
+ \"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.TrueI\", \"Pure.protectD\",
+ \"Pure.protectI\"]"}
+*}
+text {*
Of course we can also descend into the second level of the tree
``behind'' @{thm [source] my_conjIa} say, which
means we obtain the theorems that are used in order to prove
@{thm [source] conjunct1}, @{thm [source] conjunct2} and @{thm [source] conjI}.
- @{ML_response [display, gray]
+ @{ML_response_fake [display, gray]
"@{thm my_conjIa}
|> Thm.proof_body_of
|> get_pbodies
@@ -116,10 +120,11 @@
|> (map o map) get_names
|> List.concat
|> List.concat
- |> duplicates (op=)"
- "[\"HOL.spec\", \"HOL.and_def\", \"HOL.mp\", \"HOL.impI\", \"Pure.protectD\",
- \"Pure.protectI\"]"}
-
+ |> duplicates (op =)"
+ "[\"\", \"Pure.protectD\",
+ \"Pure.protectI\"]"}
+*}
+text {*
\begin{readmore}
The data-structure @{ML_type proof_body} is implemented
in the file @{ML_file "Pure/proofterm.ML"}. The implementation
--- a/ProgTutorial/Recipes/Oracle.thy Fri Jun 03 15:15:17 2016 +0100
+++ b/ProgTutorial/Recipes/Oracle.thy Tue May 14 11:10:53 2019 +0200
@@ -60,7 +60,7 @@
let
fun trans t =
(case t of
- @{term "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t $ u =>
+ @{term "(=) :: bool \<Rightarrow> bool \<Rightarrow> bool"} $ t $ u =>
Buffer.add " (" #>
trans t #>
Buffer.add "<=>" #>
@@ -120,18 +120,18 @@
To be able to use our oracle for Isar proofs, we wrap it into a tactic:
*}
-ML %grayML{*val iff_oracle_tac =
+ML %grayML{*fun iff_oracle_tac ctxt =
CSUBGOAL (fn (goal, i) =>
(case try iff_oracle goal of
NONE => no_tac
- | SOME thm => rtac thm i))*}
+ | SOME thm => resolve_tac ctxt [thm] i))*}
text {*
and create a new method solely based on this tactic:
*}
method_setup iff_oracle = {*
- Scan.succeed (K (Method.SIMPLE_METHOD' iff_oracle_tac))
+ Scan.succeed (fn ctxt => (Method.SIMPLE_METHOD' (iff_oracle_tac ctxt)))
*} "Oracle-based decision procedure for chains of equivalences"
text {*
--- a/ProgTutorial/Recipes/Sat.thy Fri Jun 03 15:15:17 2016 +0100
+++ b/ProgTutorial/Recipes/Sat.thy Tue May 14 11:10:53 2019 +0200
@@ -71,7 +71,9 @@
@{ML_response_fake [display,gray]
"SAT_Solver.invoke_solver \"minisat\" pform"
"SAT_Solver.SATISFIABLE assg"}
+*}
+text {*
determines that the formula @{ML pform} is satisfiable. If we inspect
the returned function @{text assg}
@@ -81,7 +83,7 @@
in
(assg 1, assg 2, assg 3)
end"
- "(SOME true, SOME true, NONE)"}
+ "(NONE, SOME true, NONE)"}
we obtain a possible assignment for the variables @{text "A"} an @{text "B"}
that makes the formula satisfiable.
--- a/ProgTutorial/Recipes/TimeLimit.thy Fri Jun 03 15:15:17 2016 +0100
+++ b/ProgTutorial/Recipes/TimeLimit.thy Tue May 14 11:10:53 2019 +0200
@@ -3,13 +3,12 @@
begin
section {* Restricting the Runtime of a Function\label{rec:timeout} *}
-
text {*
{\bf Problem:}
Your tool should run only a specified amount of time.\smallskip
- {\bf Solution:} In PolyML 5.2.1 and later, this can be achieved
- using the function @{ML timeLimit in TimeLimit}.\smallskip
+ {\bf Solution:} In Isabelle 2016-1 and later, this can be achieved
+ using the function @{ML apply in Timeout}.\smallskip
Assume you defined the Ackermann function on the ML-level.
*}
@@ -28,21 +27,21 @@
in a time limit of five seconds. For this you have to write
@{ML_response_fake_both [display,gray]
-"TimeLimit.timeLimit (Time.fromSeconds 5) ackermann (4, 12)
- handle TimeLimit.TimeOut => ~1"
+"Timeout.apply (Time.fromSeconds 5) ackermann (4, 12)
+ handle TIMEOUT => ~1"
"~1"}
where @{text TimeOut} is the exception raised when the time limit
is reached.
- Note that @{ML "timeLimit" in TimeLimit} is only meaningful when you use PolyML 5.2.1
+ Note that @{ML "apply" in Timeout} is only meaningful when you use PolyML 5.2.1
or later, because this version of PolyML has the infrastructure for multithreaded
- programming on which @{ML "timeLimit" in TimeLimit} relies.
+ programming on which @{ML "apply" in Timeout} relies.
\begin{readmore}
- The function @{ML "timeLimit" in TimeLimit} is defined in the structure
- @{ML_struct TimeLimit} which can be found in the file
- @{ML_file "Pure/ML-Systems/multithreading_polyml.ML"}.
+ The function @{ML "apply" in Timeout} is defined in the structure
+ @{ML_struct Timeout} which can be found in the file
+ @{ML_file "Pure/concurrent/timeout.ML"}.
\end{readmore}
--- a/ProgTutorial/Solutions.thy Fri Jun 03 15:15:17 2016 +0100
+++ b/ProgTutorial/Solutions.thy Tue May 14 11:10:53 2019 +0200
@@ -141,7 +141,7 @@
text {* \solution{ex:dyckhoff} *}
text {*
- The axiom rule can be implemented with the function @{ML atac}. The other
+ The axiom rule can be implemented with the function @{ML assume_tac}. The other
rules correspond to the theorems:
\begin{center}
@@ -182,26 +182,26 @@
as follows.
*}
-ML %linenosgray{*val apply_tac =
+ML %linenosgray{*fun apply_tac ctxt =
let
val intros = @{thms conjI disjI1 disjI2 impI iffI}
val elims = @{thms FalseE conjE disjE iffE impE2}
in
- atac
- ORELSE' resolve_tac intros
- ORELSE' eresolve_tac elims
- ORELSE' (etac @{thm impE1} THEN' atac)
+ assume_tac ctxt
+ ORELSE' resolve_tac ctxt intros
+ ORELSE' eresolve_tac ctxt elims
+ ORELSE' (eresolve_tac ctxt [@{thm impE1}] THEN' assume_tac ctxt)
end*}
text {*
In Line 11 we apply the rule @{thm [source] impE1} in concjunction
- with @{ML atac} in order to reduce the number of possibilities that
+ with @{ML assume_tac} in order to reduce the number of possibilities that
need to be explored. You can use the tactic as follows.
*}
lemma
shows "((((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P) \<longrightarrow> Q) \<longrightarrow> Q"
-apply(tactic {* (DEPTH_SOLVE o apply_tac) 1 *})
+apply(tactic {* (DEPTH_SOLVE o apply_tac @{context}) 1 *})
done
text {*
@@ -214,7 +214,7 @@
val goal = HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))
in
Goal.prove ctxt ["P"] [] goal
- (fn _ => (DEPTH_SOLVE o apply_tac) 1)
+ (fn _ => (DEPTH_SOLVE o apply_tac ctxt) 1)
end*}
text {*
@@ -227,7 +227,7 @@
ML %grayML{*fun dest_sum term =
case term of
- (@{term "(op +):: nat \<Rightarrow> nat \<Rightarrow> nat"} $ t1 $ t2) =>
+ (@{term "(+):: nat \<Rightarrow> nat \<Rightarrow> nat"} $ t1 $ t2) =>
(snd (HOLogic.dest_number t1), snd (HOLogic.dest_number t2))
| _ => raise TERM ("dest_sum", [term])
@@ -241,7 +241,7 @@
fun add_sp_aux ctxt t =
let
- val t' = term_of t
+ val t' = Thm.term_of t
in
SOME (get_sum_thm ctxt t' (dest_sum t'))
handle TERM _ => NONE
@@ -275,7 +275,7 @@
val trm = Thm.term_of ctrm
in
case trm of
- @{term "(op +)::nat \<Rightarrow> nat \<Rightarrow> nat"} $ _ $ _ =>
+ @{term "(+)::nat \<Rightarrow> nat \<Rightarrow> nat"} $ _ $ _ =>
get_sum_thm ctxt trm (dest_sum trm)
| _ => Conv.all_conv ctrm
end
@@ -350,11 +350,11 @@
ML Skip_Proof.cheat_tac
ML %grayML{*local
- fun mk_tac tac =
- timing_wrapper (EVERY1 [tac, Skip_Proof.cheat_tac])
+ fun mk_tac ctxt tac =
+ timing_wrapper (EVERY1 [tac, Skip_Proof.cheat_tac ctxt])
in
- fun c_tac ctxt = mk_tac (add_tac ctxt)
- fun s_tac ctxt = mk_tac (simp_tac
+ fun c_tac ctxt = mk_tac ctxt (add_tac ctxt)
+ fun s_tac ctxt = mk_tac ctxt (simp_tac
(put_simpset HOL_basic_ss ctxt addsimprocs [@{simproc add_sp}]))
end*}
--- a/ProgTutorial/Tactical.thy Fri Jun 03 15:15:17 2016 +0100
+++ b/ProgTutorial/Tactical.thy Tue May 14 11:10:53 2019 +0200
@@ -44,8 +44,6 @@
apply(assumption)
done
-
-
text {*
This proof translates to the following ML-code.
@@ -55,11 +53,11 @@
val goal = @{prop \"P \<or> Q \<Longrightarrow> Q \<or> P\"}
in
Goal.prove ctxt [\"P\", \"Q\"] [] goal
- (fn _ => etac @{thm disjE} 1
- THEN rtac @{thm disjI2} 1
- THEN atac 1
- THEN rtac @{thm disjI1} 1
- THEN atac 1)
+ (fn _ => eresolve_tac @{context} [@{thm disjE}] 1
+ THEN resolve_tac @{context} [@{thm disjI2}] 1
+ THEN assume_tac @{context} 1
+ THEN resolve_tac @{context} [@{thm disjI1}] 1
+ THEN assume_tac @{context} 1)
end" "?P \<or> ?Q \<Longrightarrow> ?Q \<or> ?P"}
To start the proof, the function @{ML_ind prove in Goal} sets up a goal
@@ -70,12 +68,12 @@
into schematic variables once the goal is proved (in our case @{text P} and
@{text Q}). The last argument is the tactic that proves the goal. This
tactic can make use of the local assumptions (there are none in this
- example). The tactics @{ML_ind etac in Tactic}, @{ML_ind rtac in Tactic} and
- @{ML_ind atac in Tactic} in the code above correspond roughly to @{text
+ example). The tactics @{ML_ind eresolve_tac in Tactic}, @{ML_ind resolve_tac in Tactic} and
+ @{ML_ind assume_tac in Tactic} in the code above correspond roughly to @{text
erule}, @{text rule} and @{text assumption}, respectively. The combinator
@{ML THEN} strings the tactics together.
- TBD: Write something about @{ML_ind prove_multi in Goal}.
+ TBD: Write something about @{ML_ind prove_common in Goal}.
\begin{readmore}
To learn more about the function @{ML_ind prove in Goal} see
@@ -96,18 +94,18 @@
*}
-ML %grayML{*val foo_tac =
- (etac @{thm disjE} 1
- THEN rtac @{thm disjI2} 1
- THEN atac 1
- THEN rtac @{thm disjI1} 1
- THEN atac 1)*}
+ML %grayML{*fun foo_tac ctxt =
+ (eresolve_tac ctxt [@{thm disjE}] 1
+ THEN resolve_tac ctxt [@{thm disjI2}] 1
+ THEN assume_tac ctxt 1
+ THEN resolve_tac ctxt [@{thm disjI1}] 1
+ THEN assume_tac ctxt 1)*}
text {* and the Isabelle proof: *}
lemma
shows "P \<or> Q \<Longrightarrow> Q \<or> P"
-apply(tactic {* foo_tac *})
+apply(tactic {* foo_tac @{context} *})
done
text {*
@@ -125,12 +123,12 @@
you can write
*}
-ML %grayML{*val foo_tac' =
- (etac @{thm disjE}
- THEN' rtac @{thm disjI2}
- THEN' atac
- THEN' rtac @{thm disjI1}
- THEN' atac)*}text_raw{*\label{tac:footacprime}*}
+ML %grayML{*fun foo_tac' ctxt =
+ (eresolve_tac ctxt [@{thm disjE}]
+ THEN' resolve_tac ctxt [@{thm disjI2}]
+ THEN' assume_tac ctxt
+ THEN' resolve_tac ctxt [@{thm disjI1}]
+ THEN' assume_tac ctxt)*}text_raw{*\label{tac:footacprime}*}
text {*
where @{ML_ind THEN' in Tactical} is used instead of @{ML THEN in
@@ -144,8 +142,8 @@
lemma
shows "P1 \<or> Q1 \<Longrightarrow> Q1 \<or> P1"
and "P2 \<or> Q2 \<Longrightarrow> Q2 \<or> P2"
-apply(tactic {* foo_tac' 2 *})
-apply(tactic {* foo_tac' 1 *})
+apply(tactic {* foo_tac' @{context} 2 *})
+apply(tactic {* foo_tac' @{context} 1 *})
done
text {*
@@ -203,7 +201,7 @@
lemma
shows "\<lbrakk>P \<or> Q; P \<or> Q\<rbrakk> \<Longrightarrow> Q \<or> P"
-apply(tactic {* foo_tac' 1 *})
+apply(tactic {* foo_tac' @{context} 1 *})
back
done
@@ -350,7 +348,7 @@
where
"EQ_TRUE X \<equiv> (X = True)"
-schematic_lemma test:
+schematic_goal test:
shows "EQ_TRUE ?X"
unfolding EQ_TRUE_def
by (rule refl)
@@ -407,28 +405,28 @@
lemma
shows "False" and "Goldbach_conjecture"
-apply(tactic {* Skip_Proof.cheat_tac 1 *})
+apply(tactic {* Skip_Proof.cheat_tac @{context} 1 *})
txt{*\begin{minipage}{\textwidth}
@{subgoals [display]}
\end{minipage}*}
(*<*)oops(*>*)
text {*
- Another simple tactic is the function @{ML_ind atac in Tactic}, which, as shown
+ Another simple tactic is the function @{ML_ind assume_tac in Tactic}, which, as shown
earlier, corresponds to the assumption method.
*}
lemma
shows "P \<Longrightarrow> P"
-apply(tactic {* atac 1 *})
+apply(tactic {* assume_tac @{context} 1 *})
txt{*\begin{minipage}{\textwidth}
@{subgoals [display]}
\end{minipage}*}
(*<*)oops(*>*)
text {*
- Similarly, @{ML_ind rtac in Tactic}, @{ML_ind dtac in Tactic}, @{ML_ind etac
- in Tactic} and @{ML_ind ftac in Tactic} correspond (roughly) to @{text
+ Similarly, @{ML_ind resolve_tac in Tactic}, @{ML_ind dresolve_tac in Tactic}, @{ML_ind eresolve_tac
+ in Tactic} and @{ML_ind forward_tac in Tactic} correspond (roughly) to @{text
rule}, @{text drule}, @{text erule} and @{text frule}, respectively. Each of
them takes a theorem as argument and attempts to apply it to a goal. Below
are three self-explanatory examples.
@@ -436,7 +434,7 @@
lemma
shows "P \<and> Q"
-apply(tactic {* rtac @{thm conjI} 1 *})
+apply(tactic {* resolve_tac @{context} [@{thm conjI}] 1 *})
txt{*\begin{minipage}{\textwidth}
@{subgoals [display]}
\end{minipage}*}
@@ -444,7 +442,7 @@
lemma
shows "P \<and> Q \<Longrightarrow> False"
-apply(tactic {* etac @{thm conjE} 1 *})
+apply(tactic {* eresolve_tac @{context} [@{thm conjE}] 1 *})
txt{*\begin{minipage}{\textwidth}
@{subgoals [display]}
\end{minipage}*}
@@ -452,20 +450,20 @@
lemma
shows "False \<and> True \<Longrightarrow> False"
-apply(tactic {* dtac @{thm conjunct2} 1 *})
+apply(tactic {* dresolve_tac @{context} [@{thm conjunct2}] 1 *})
txt{*\begin{minipage}{\textwidth}
@{subgoals [display]}
\end{minipage}*}
(*<*)oops(*>*)
text {*
- The function @{ML_ind resolve_tac in Tactic} is similar to @{ML rtac}, except that it
+ The function @{ML_ind resolve_tac in Tactic}
expects a list of theorems as argument. From this list it will apply the
first applicable theorem (later theorems that are also applicable can be
explored via the lazy sequences mechanism). Given the code
*}
-ML %grayML{*val resolve_xmp_tac = resolve_tac [@{thm impI}, @{thm conjI}]*}
+ML %grayML{*fun resolve_xmp_tac ctxt = resolve_tac ctxt [@{thm impI}, @{thm conjI}]*}
text {*
an example for @{ML resolve_tac} is the following proof where first an outermost
@@ -475,8 +473,8 @@
lemma
shows "C \<longrightarrow> (A \<and> B)"
and "(A \<longrightarrow> B) \<and> C"
-apply(tactic {* resolve_xmp_tac 1 *})
-apply(tactic {* resolve_xmp_tac 2 *})
+apply(tactic {* resolve_xmp_tac @{context} 1 *})
+apply(tactic {* resolve_xmp_tac @{context} 2 *})
txt{*\begin{minipage}{\textwidth}
@{subgoals [display]}
\end{minipage}*}
@@ -484,8 +482,8 @@
text {*
Similar versions taking a list of theorems exist for the tactics
- @{ML dtac} (@{ML_ind dresolve_tac in Tactic}), @{ML etac}
- (@{ML_ind eresolve_tac in Tactic}) and so on.
+ @{ML_ind dresolve_tac in Tactic},
+ @{ML_ind eresolve_tac in Tactic} and so on.
Another simple tactic is @{ML_ind cut_facts_tac in Tactic}. It inserts a
list of theorems into the assumptions of the current goal state. Below we
@@ -521,7 +519,7 @@
\begin{isabelle}
*}
-ML %grayML{*fun foc_tac {prems, params, asms, concl, context, schematics} =
+ML %grayML{*fun foc_tac {context, params, prems, asms, concl, schematics} =
let
fun assgn1 f1 f2 xs =
let
@@ -530,7 +528,7 @@
Pretty.list "" "" out
end
- fun assgn2 f xs = assgn1 f f xs
+ fun assgn2 f xs = assgn1 (fn (n,T) => pretty_term context (Var (n,T))) f xs
val pps = map (fn (s, pp) => Pretty.block [Pretty.str s, pp])
[("params: ", assgn1 Pretty.str (pretty_cterm context) params),
@@ -552,7 +550,7 @@
\end{figure}
*}
-schematic_lemma
+schematic_goal
shows "\<And>x y. A x y \<Longrightarrow> B y x \<longrightarrow> C (?z y) x"
apply(tactic {* Subgoal.FOCUS foc_tac @{context} 1 *})
@@ -608,15 +606,15 @@
variables.
Observe that inside @{ML FOCUS in Subgoal} and @{ML SUBPROOF}, we are in a goal
- state where there is only a conclusion. This means the tactics @{ML dtac} and
+ state where there is only a conclusion. This means the tactics @{ML dresolve_tac} and
the like are of no use for manipulating the goal state. The assumptions inside
@{ML FOCUS in Subgoal} and @{ML SUBPROOF} are given as cterms and theorems in
the arguments @{text "asms"} and @{text "prems"}, respectively. This
means we can apply them using the usual assumption tactics. With this you can
- for example easily implement a tactic that behaves almost like @{ML atac}:
+ for example easily implement a tactic that behaves almost like @{ML assume_tac}:
*}
-ML %grayML{*val atac' = Subgoal.FOCUS (fn {prems, ...} => resolve_tac prems 1)*}
+ML %grayML{*val atac' = Subgoal.FOCUS (fn {prems, context, ...} => resolve_tac context prems 1)*}
text {*
If you apply @{ML atac'} to the next lemma
@@ -656,7 +654,7 @@
\begin{readmore}
The functions @{ML FOCUS in Subgoal} and @{ML SUBPROOF} are defined in
- @{ML_file "Pure/subgoal.ML"} and also described in
+ @{ML_file "Pure/Isar/subgoal.ML"} and also described in
\isccite{sec:results}.
\end{readmore}
@@ -669,14 +667,14 @@
analyse a few connectives). The code of the tactic is as follows.
*}
-ML %linenosgray{*fun select_tac (t, i) =
+ML %linenosgray{*fun select_tac ctxt (t, i) =
case t of
- @{term "Trueprop"} $ t' => select_tac (t', i)
- | @{term "op \<Longrightarrow>"} $ _ $ t' => select_tac (t', i)
- | @{term "op \<and>"} $ _ $ _ => rtac @{thm conjI} i
- | @{term "op \<longrightarrow>"} $ _ $ _ => rtac @{thm impI} i
- | @{term "Not"} $ _ => rtac @{thm notI} i
- | Const (@{const_name "All"}, _) $ _ => rtac @{thm allI} i
+ @{term "Trueprop"} $ t' => select_tac ctxt (t', i)
+ | @{term "(\<Longrightarrow>)"} $ _ $ t' => select_tac ctxt (t', i)
+ | @{term "(\<and>)"} $ _ $ _ => resolve_tac ctxt [@{thm conjI}] i
+ | @{term "(\<longrightarrow>)"} $ _ $ _ => resolve_tac ctxt [@{thm impI}] i
+ | @{term "Not"} $ _ => resolve_tac ctxt [@{thm notI}] i
+ | Const (@{const_name "All"}, _) $ _ => resolve_tac ctxt [@{thm allI}] i
| _ => all_tac*}text_raw{*\label{tac:selecttac}*}
text {*
@@ -702,10 +700,10 @@
lemma
shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
-apply(tactic {* SUBGOAL select_tac 4 *})
-apply(tactic {* SUBGOAL select_tac 3 *})
-apply(tactic {* SUBGOAL select_tac 2 *})
-apply(tactic {* SUBGOAL select_tac 1 *})
+apply(tactic {* SUBGOAL (select_tac @{context}) 4 *})
+apply(tactic {* SUBGOAL (select_tac @{context}) 3 *})
+apply(tactic {* SUBGOAL (select_tac @{context}) 2 *})
+apply(tactic {* SUBGOAL (select_tac @{context}) 1 *})
txt{* \begin{minipage}{\textwidth}
@{subgoals [display]}
\end{minipage} *}
@@ -720,10 +718,10 @@
lemma
shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
-apply(tactic {* SUBGOAL select_tac 1 *})
-apply(tactic {* SUBGOAL select_tac 3 *})
-apply(tactic {* SUBGOAL select_tac 4 *})
-apply(tactic {* SUBGOAL select_tac 5 *})
+apply(tactic {* SUBGOAL (select_tac @{context}) 1 *})
+apply(tactic {* SUBGOAL (select_tac @{context}) 3 *})
+apply(tactic {* SUBGOAL (select_tac @{context}) 4 *})
+apply(tactic {* SUBGOAL (select_tac @{context}) 5 *})
(*<*)oops(*>*)
text {*
@@ -743,7 +741,7 @@
\end{readmore}
- Since @{ML_ind rtac in Tactic} and the like use higher-order unification, an
+ Since @{ML_ind resolve_tac in Tactic} and the like use higher-order unification, an
automatic proof procedure based on them might become too fragile, if it just
applies theorems as shown above. The reason is that a number of theorems
introduce schematic variables into the goal state. Consider for example the
@@ -752,7 +750,7 @@
lemma
shows "\<forall>x \<in> A. P x \<Longrightarrow> Q x"
-apply(tactic {* dtac @{thm bspec} 1 *})
+apply(tactic {* dresolve_tac @{context} [@{thm bspec}] 1 *})
txt{*\begin{minipage}{\textwidth}
@{subgoals [display]}
\end{minipage}*}
@@ -849,7 +847,7 @@
lemma
fixes x y u w::"'a"
shows "t x y = s u w"
-apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
+apply(tactic {* Cong_Tac.cong_tac @{context} @{thm cong} 1 *})
txt{*\begin{minipage}{\textwidth}
@{subgoals [display]}
\end{minipage}*}
@@ -881,12 +879,12 @@
this we implement the following function.
*}
-ML %linenosgray{*fun fo_rtac thm = Subgoal.FOCUS (fn {concl, ...} =>
+ML %linenosgray{*fun fo_rtac thm = Subgoal.FOCUS (fn {context, concl, ...} =>
let
- val concl_pat = Drule.strip_imp_concl (cprop_of thm)
+ val concl_pat = Drule.strip_imp_concl (Thm.cprop_of thm)
val insts = Thm.first_order_match (concl_pat, concl)
in
- rtac (Drule.instantiate_normalize insts thm) 1
+ resolve_tac context [(Drule.instantiate_normalize insts thm)] 1
end)*}
text {*
@@ -930,7 +928,7 @@
lemma
shows "(Foo \<and> Bar) \<and> False"
-apply(tactic {* rtac @{thm conjI} 1 THEN rtac @{thm conjI} 1 *})
+apply(tactic {* resolve_tac @{context} [@{thm conjI}] 1 THEN resolve_tac @{context} [@{thm conjI}] 1 *})
txt {* \begin{minipage}{\textwidth}
@{subgoals [display]}
\end{minipage} *}
@@ -944,7 +942,7 @@
lemma
shows "(Foo \<and> Bar) \<and> False"
-apply(tactic {* (rtac @{thm conjI} THEN' rtac @{thm conjI}) 1 *})
+apply(tactic {* (resolve_tac @{context} [@{thm conjI}] THEN' resolve_tac @{context} [@{thm conjI}]) 1 *})
txt {* \begin{minipage}{\textwidth}
@{subgoals [display]}
\end{minipage} *}
@@ -964,8 +962,8 @@
lemma
shows "A \<Longrightarrow> True \<and> A"
-apply(tactic {* (rtac @{thm conjI}
- THEN' RANGE [rtac @{thm TrueI}, atac]) 1 *})
+apply(tactic {* (resolve_tac @{context} [@{thm conjI}]
+ THEN' RANGE [resolve_tac @{context} [@{thm TrueI}], assume_tac @{context}]) 1 *})
txt {* \begin{minipage}{\textwidth}
@{subgoals [display]}
\end{minipage} *}
@@ -978,19 +976,21 @@
page~\pageref{tac:footacprime} can also be written as:
*}
-ML %grayML{*val foo_tac'' = EVERY' [etac @{thm disjE}, rtac @{thm disjI2},
- atac, rtac @{thm disjI1}, atac]*}
+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]*}
text {*
There is even another way of implementing this tactic: in automatic proof
procedures (in contrast to tactics that might be called by the user) there
are often long lists of tactics that are applied to the first
- subgoal. Instead of writing the code above and then calling @{ML "foo_tac'' 1"},
+ subgoal. Instead of writing the code above and then calling @{ML "foo_tac'' @{context} 1"},
you can also just write
*}
-ML %grayML{*val foo_tac1 = EVERY1 [etac @{thm disjE}, rtac @{thm disjI2},
- atac, rtac @{thm disjI1}, atac]*}
+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]*}
text {*
and call @{ML foo_tac1}.
@@ -1003,7 +1003,8 @@
*}
-ML %grayML{*val orelse_xmp_tac = rtac @{thm disjI1} ORELSE' rtac @{thm conjI}*}
+ML %grayML{*fun orelse_xmp_tac ctxt =
+ resolve_tac ctxt [@{thm disjI1}] ORELSE' resolve_tac ctxt [@{thm conjI}]*}
text {*
will first try out whether theorem @{text disjI} applies and in case of failure
@@ -1012,8 +1013,8 @@
lemma
shows "True \<and> False" and "Foo \<or> Bar"
-apply(tactic {* orelse_xmp_tac 2 *})
-apply(tactic {* orelse_xmp_tac 1 *})
+apply(tactic {* orelse_xmp_tac @{context} 2 *})
+apply(tactic {* orelse_xmp_tac @{context} 1 *})
txt {* which results in the goal state
\begin{isabelle}
@{subgoals [display]}
@@ -1027,8 +1028,9 @@
as follows:
*}
-ML %grayML{*val select_tac' = FIRST' [rtac @{thm conjI}, rtac @{thm impI},
- rtac @{thm notI}, rtac @{thm allI}, K all_tac]*}text_raw{*\label{tac:selectprime}*}
+ML %grayML{*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]*}text_raw{*\label{tac:selectprime}*}
text {*
Since we like to mimic the behaviour of @{ML select_tac} as closely as possible,
@@ -1040,10 +1042,10 @@
lemma
shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
-apply(tactic {* select_tac' 4 *})
-apply(tactic {* select_tac' 3 *})
-apply(tactic {* select_tac' 2 *})
-apply(tactic {* select_tac' 1 *})
+apply(tactic {* select_tac' @{context} 4 *})
+apply(tactic {* select_tac' @{context} 3 *})
+apply(tactic {* select_tac' @{context} 2 *})
+apply(tactic {* select_tac' @{context} 1 *})
txt{* \begin{minipage}{\textwidth}
@{subgoals [display]}
\end{minipage} *}
@@ -1057,7 +1059,7 @@
lemma
shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
-apply(tactic {* ALLGOALS select_tac' *})
+apply(tactic {* ALLGOALS (select_tac' @{context}) *})
txt{* \begin{minipage}{\textwidth}
@{subgoals [display]}
\end{minipage} *}
@@ -1070,8 +1072,9 @@
For example:
*}
-ML %grayML{*val select_tac'' = TRY o FIRST' [rtac @{thm conjI}, rtac @{thm impI},
- rtac @{thm notI}, rtac @{thm allI}]*}
+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}]]*}
text_raw{*\label{tac:selectprimeprime}*}
text {*
@@ -1084,7 +1087,7 @@
lemma
shows "E \<Longrightarrow> F"
-apply(tactic {* select_tac' 1 *})
+apply(tactic {* select_tac' @{context} 1 *})
txt{* \begin{minipage}{\textwidth}
@{subgoals [display]}
\end{minipage} *}
@@ -1107,7 +1110,7 @@
lemma
shows "E \<Longrightarrow> F"
-apply(tactic {* CHANGED (select_tac' 1) *})(*<*)?(*>*)
+apply(tactic {* CHANGED (select_tac' @{context} 1) *})(*<*)?(*>*)
txt{* gives the error message:
\begin{isabelle}
@{text "*** empty result sequence -- proof command failed"}\\
@@ -1123,13 +1126,13 @@
suppose the following tactic
*}
-ML %grayML{*val repeat_xmp_tac = REPEAT (CHANGED (select_tac' 1)) *}
+ML %grayML{*fun repeat_xmp_tac ctxt = REPEAT (CHANGED (select_tac' ctxt 1)) *}
text {* which applied to the proof *}
lemma
shows "((\<not>A) \<and> (\<forall>x. B x)) \<and> (C \<longrightarrow> D)"
-apply(tactic {* repeat_xmp_tac *})
+apply(tactic {* repeat_xmp_tac @{context} *})
txt{* produces
\begin{isabelle}
@{subgoals [display]}
@@ -1147,7 +1150,7 @@
can implement it as
*}
-ML %grayML{*val repeat_xmp_tac' = REPEAT o CHANGED o select_tac'*}
+ML %grayML{*fun repeat_xmp_tac' ctxt = REPEAT o CHANGED o select_tac' ctxt*}
text {*
since there are no ``primed'' versions of @{ML REPEAT} and @{ML CHANGED}.
@@ -1160,7 +1163,7 @@
Supposing the tactic
*}
-ML %grayML{*val repeat_all_new_xmp_tac = REPEAT_ALL_NEW (CHANGED o select_tac')*}
+ML %grayML{*fun repeat_all_new_xmp_tac ctxt = REPEAT_ALL_NEW (CHANGED o select_tac' ctxt)*}
text {*
you can see that the following goal
@@ -1168,7 +1171,7 @@
lemma
shows "((\<not>A) \<and> (\<forall>x. B x)) \<and> (C \<longrightarrow> D)"
-apply(tactic {* repeat_all_new_xmp_tac 1 *})
+apply(tactic {* repeat_all_new_xmp_tac @{context} 1 *})
txt{* \begin{minipage}{\textwidth}
@{subgoals [display]}
\end{minipage} *}
@@ -1185,7 +1188,7 @@
lemma
shows "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
-apply(tactic {* etac @{thm disjE} 1 *})
+apply(tactic {* eresolve_tac @{context} [@{thm disjE}] 1 *})
txt{* applies the rule to the first assumption yielding the goal state:
\begin{isabelle}
@{subgoals [display]}
@@ -1197,7 +1200,7 @@
oops
lemma
shows "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
-apply(tactic {* etac @{thm disjE} 1 *})
+apply(tactic {* eresolve_tac @{context} [@{thm disjE}] 1 *})
(*>*)
back
txt{* the rule now applies to the second assumption.
@@ -1215,7 +1218,7 @@
lemma
shows "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
-apply(tactic {* DETERM (etac @{thm disjE} 1) *})
+apply(tactic {* DETERM (eresolve_tac @{context} [@{thm disjE}] 1) *})
txt {*\begin{minipage}{\textwidth}
@{subgoals [display]}
\end{minipage} *}
@@ -1434,12 +1437,12 @@
Pretty.enclose (nm ^ ": ") "" [pretty_thm_no_vars ctxt thm]
fun name_cthm ((_, nm), thm) =
Pretty.enclose (nm ^ ": ") "" [pretty_thm_no_vars ctxt thm]
- fun name_ctrm (nm, ctrm) =
- Pretty.enclose (nm ^ ": ") "" [pretty_cterms ctxt ctrm]
+ fun name_trm (nm, trm) =
+ Pretty.enclose (nm ^ ": ") "" [pretty_terms ctxt trm]
val pps = [Pretty.big_list "Simplification rules:" (map name_sthm simps),
Pretty.big_list "Congruences rules:" (map name_cthm congs),
- Pretty.big_list "Simproc patterns:" (map name_ctrm procs)]
+ Pretty.big_list "Simproc patterns:" (map name_trm procs)]
in
pps |> Pretty.chunks
|> pwriteln
@@ -1748,7 +1751,7 @@
often be done easier by implementing a simproc or a conversion. Both will be
explained in the next two chapters.
- (FIXME: Is it interesting to say something about @{term "op =simp=>"}?)
+ (FIXME: Is it interesting to say something about @{term "(=simp=>)"}?)
(FIXME: What are the second components of the congruence rules---something to
do with weak congruence constants?)
@@ -1846,10 +1849,10 @@
to
*}
-ML %grayML{*fun fail_simproc' ctxt redex =
+ML %grayML{*fun fail_simproc' _ ctxt redex =
let
val _ = pwriteln (Pretty.block
- [Pretty.str "The redex:", pretty_term ctxt redex])
+ [Pretty.str "The redex:", pretty_cterm ctxt redex])
in
NONE
end*}
@@ -1858,17 +1861,12 @@
Here the redex is given as a @{ML_type term}, instead of a @{ML_type cterm}
(therefore we printing it out using the function @{ML pretty_term in Pretty}).
We can turn this function into a proper simproc using the function
- @{ML Simplifier.simproc_global_i}:
+ @{ML Simplifier.make_simproc}:
*}
-
-ML %grayML{*fun fail' ctxt =
-let
- val thy = @{theory}
- val pat = [@{term "Suc n"}]
-in
- Simplifier.simproc_global_i thy "fail_simproc'" pat (K fail_simproc' ctxt)
-end*}
+ML %grayML{*val fail' =
+ Simplifier.make_simproc @{context} "fail_simproc'"
+ {lhss = [@{term "Suc n"}], proc = fail_simproc'}*}
text {*
Here the pattern is given as @{ML_type term} (instead of @{ML_type cterm}).
@@ -1883,7 +1881,7 @@
lemma
shows "Suc (Suc 0) = (Suc 1)"
-apply(tactic {* simp_tac ((put_simpset HOL_basic_ss @{context}) addsimprocs [fail' @{context}]) 1*})
+apply(tactic {* simp_tac ((put_simpset HOL_basic_ss @{context}) addsimprocs [fail']) 1*})
(*<*)oops(*>*)
text {*
@@ -1910,8 +1908,8 @@
*}
-ML %grayML{*fun plus_one_simproc ctxt redex =
- case redex of
+ML %grayML{*fun plus_one_simproc _ ctxt redex =
+ case Thm.term_of redex of
@{term "Suc 0"} => NONE
| _ => SOME @{thm plus_one}*}
@@ -1919,13 +1917,9 @@
and set up the simproc as follows.
*}
-ML %grayML{*fun plus_one ctxt =
-let
- val thy = @{theory}
- val pat = [@{term "Suc n"}]
-in
- Simplifier.simproc_global_i thy "sproc +1" pat (K plus_one_simproc ctxt)
-end*}
+ML %grayML{*val plus_one =
+ Simplifier.make_simproc @{context} "sproc +1"
+ {lhss = [@{term "Suc n"}], proc = plus_one_simproc}*}
text {*
Now the simproc is set up so that it is triggered by terms
@@ -1936,7 +1930,7 @@
lemma
shows "P (Suc (Suc (Suc 0))) (Suc 0)"
-apply(tactic {* simp_tac (put_simpset HOL_basic_ss @{context} addsimprocs [plus_one @{context}]) 1*})
+apply(tactic {* simp_tac (put_simpset HOL_basic_ss @{context} addsimprocs [plus_one]) 1*})
txt{*
where the simproc produces the goal state
\begin{isabelle}
@@ -2011,8 +2005,8 @@
theorem for the simproc.
*}
-ML %grayML{*fun nat_number_simproc ctxt t =
- SOME (get_thm_alt ctxt (t, dest_suc_trm t))
+ML %grayML{*fun nat_number_simproc _ ctxt ct =
+ SOME (get_thm_alt ctxt (Thm.term_of ct, dest_suc_trm (Thm.term_of ct)))
handle TERM _ => NONE *}
text {*
@@ -2022,13 +2016,10 @@
on an example, you can set it up as follows:
*}
-ML %grayML{*fun nat_number ctxt =
-let
- val thy = @{theory}
- val pat = [@{term "Suc n"}]
-in
- Simplifier.simproc_global_i thy "nat_number" pat (K nat_number_simproc ctxt)
-end*}
+ML %grayML{*val nat_number =
+ Simplifier.make_simproc @{context} "nat_number"
+ {lhss = [@{term "Suc n"}], proc = nat_number_simproc}*}
+
text {*
Now in the lemma
@@ -2036,7 +2027,7 @@
lemma
shows "P (Suc (Suc 2)) (Suc 99) (0::nat) (Suc 4 + Suc 0) (Suc (0 + 0))"
-apply(tactic {* simp_tac (put_simpset HOL_ss @{context} addsimprocs [nat_number @{context}]) 1*})
+apply(tactic {* simp_tac (put_simpset HOL_ss @{context} addsimprocs [nat_number]) 1*})
txt {*
you obtain the more legible goal state
\begin{isabelle}
@@ -2276,7 +2267,7 @@
ML %linenosgray{*fun true_conj1_conv ctxt ctrm =
case (Thm.term_of ctrm) of
- @{term "op \<and>"} $ @{term True} $ _ =>
+ @{term "(\<and>)"} $ @{term True} $ _ =>
(Conv.arg_conv (true_conj1_conv ctxt) then_conv
Conv.rewr_conv @{thm true_conj1}) ctrm
| _ $ _ => Conv.comb_conv (true_conj1_conv ctxt) ctrm
@@ -2491,12 +2482,11 @@
ML %linenosgray{*fun unabs_def ctxt def =
let
- val (lhs, rhs) = Thm.dest_equals (cprop_of def)
- val xs = strip_abs_vars (term_of rhs)
+ val (lhs, rhs) = Thm.dest_equals (Thm.cprop_of def)
+ val xs = strip_abs_vars (Thm.term_of rhs)
val (_, ctxt') = Variable.add_fixes (map fst xs) ctxt
- val thy = Proof_Context.theory_of ctxt'
- val cxs = map (cterm_of thy o Free) xs
+ val cxs = map (Thm.cterm_of ctxt' o Free) xs
val new_lhs = Drule.list_comb (lhs, cxs)
fun get_conv [] = Conv.rewr_conv def
--- a/ProgTutorial/antiquote_setup.ML Fri Jun 03 15:15:17 2016 +0100
+++ b/ProgTutorial/antiquote_setup.ML Tue May 14 11:10:53 2019 +0200
@@ -31,16 +31,13 @@
fun ml_type txt =
implode ["val _ = NONE : (", txt, ") option"];
-fun ml_out txt =
- implode ["val _ = Pretty.writeln ((Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation ((", txt, "), ML_Options.get_print_depth ()))))) handle _ => writeln \"exception\""]
-
(* eval function *)
fun eval_fn ctxt exp =
ML_Context.eval_source_in (SOME ctxt) ML_Compiler.flags
- {delimited = false, text = exp, pos = Position.none}
+ (Input.source false exp Position.no_range)
(* checks and prints a possibly open expressions, no index *)
-fun output_ml {context = ctxt, ...} (txt, (vs, stru)) =
+fun output_ml ctxt (txt, (vs, stru)) =
(eval_fn ctxt (ml_val vs stru txt);
output ctxt (split_lines txt))
@@ -49,10 +46,10 @@
Scan.option (Args.$$$ "in" |-- Parse.!!! Args.name)))
(* checks and prints a single ML-item and produces an index entry *)
-fun output_ml_ind {context = ctxt, ...} (txt, stru) =
+fun output_ml_ind ctxt (txt, stru) =
(eval_fn ctxt (ml_val [] stru txt);
case (stru, Long_Name.base_name txt, Long_Name.qualifier txt) of
- (NONE, bn, "") => output_indexed ctxt {main = Code txt, minor = NoString} (split_lines txt)
+ (NONE, _, "") => output_indexed ctxt {main = Code txt, minor = NoString} (split_lines txt)
| (NONE, bn, qn) => output_indexed ctxt {main = Code bn, minor = Struct qn} (split_lines txt)
| (SOME st, _, _) => output_indexed ctxt {main = Code txt, minor = Struct st} (split_lines txt))
@@ -64,126 +61,130 @@
(eval_fn ctxt (ml_struct txt);
outfn {main = Code txt, minor = Plain "structure"} (split_lines txt))
-fun output_struct {context = ctxt, ...} = gen_output_struct (K (output ctxt)) ctxt
-fun output_struct_ind {context = ctxt, ...} = gen_output_struct (output_indexed ctxt) ctxt
+fun output_struct ctxt = gen_output_struct (K (output ctxt)) ctxt
+fun output_struct_ind ctxt = gen_output_struct (output_indexed ctxt) ctxt
(* prints functors; no checks *)
fun gen_output_funct outfn txt =
(outfn {main = Code txt, minor = Plain "functor"} (split_lines txt))
-fun output_funct {context = ctxt, ...} = gen_output_funct (K (output ctxt))
-fun output_funct_ind {context = ctxt, ...} = gen_output_funct (output_indexed ctxt)
+fun output_funct ctxt = gen_output_funct (K (output ctxt))
+fun output_funct_ind ctxt = gen_output_funct (output_indexed ctxt)
(* checks and prints types *)
fun gen_output_type outfn ctxt txt =
(eval_fn ctxt (ml_type txt);
outfn {main = Code txt, minor = Plain "type"} (split_lines txt))
-fun output_type {context = ctxt, ...} = gen_output_type (K (output ctxt)) ctxt
-fun output_type_ind {context = ctxt, ...} = gen_output_type (output_indexed ctxt) ctxt
+fun output_type ctxt = gen_output_type (K (output ctxt)) ctxt
+fun output_type_ind ctxt = gen_output_type (output_indexed ctxt) ctxt
(* checks and expression agains a result pattern *)
-fun output_response {context = ctxt, ...} (lhs, pat) =
+fun output_response ctxt (lhs, pat) =
(eval_fn ctxt (ml_pat (lhs, pat));
- eval_fn ctxt (ml_out lhs);
+ (*eval_fn ctxt (ml_out lhs);*) (*FIXME remove*)
output ctxt ((prefix_lines "" lhs) @ (prefix_lines "> " pat)))
(* checks the expressions, but does not check it against a result pattern *)
-fun output_response_fake {context = ctxt, ...} (lhs, pat) =
+fun output_response_fake ctxt (lhs, pat) =
(eval_fn ctxt (ml_val [] NONE lhs);
- eval_fn ctxt (ml_out lhs);
+ (*eval_fn ctxt (ml_out lhs);*) (* FIXME remove *)
output ctxt ((split_lines lhs) @ (prefix_lines "> " pat)))
(* checks the expressions, but does not check it against a result pattern *)
-fun ouput_response_fake_both {context = ctxt, ...} (lhs, pat) =
+fun ouput_response_fake_both ctxt (lhs, pat) =
(output ctxt ((split_lines lhs) @ (prefix_lines "> " pat)))
val single_arg = Scan.lift (Args.name)
val two_args = Scan.lift (Args.name -- Args.name)
val test = Scan.lift (Args.name -- Args.name -- Scan.option (Args.$$$ "with" |-- Args.name))
+
+
+
val ml_setup =
- Thy_Output.antiquotation @{binding "ML"} parser_ml output_ml
- #> Thy_Output.antiquotation @{binding "ML_ind"} parser_ml_ind output_ml_ind
- #> Thy_Output.antiquotation @{binding "ML_type"} single_arg output_type
- #> Thy_Output.antiquotation @{binding "ML_type_ind"} single_arg output_type_ind
- #> Thy_Output.antiquotation @{binding "ML_struct"} single_arg output_struct
- #> Thy_Output.antiquotation @{binding "ML_struct_ind"} single_arg output_struct_ind
- #> Thy_Output.antiquotation @{binding "ML_funct"} single_arg output_funct
- #> Thy_Output.antiquotation @{binding "ML_funct_ind"} single_arg output_funct_ind
- #> Thy_Output.antiquotation @{binding "ML_response"} two_args output_response
- #> Thy_Output.antiquotation @{binding "ML_response_fake"} two_args output_response_fake
- #> Thy_Output.antiquotation @{binding "ML_response_fake_both"} two_args ouput_response_fake_both
+ Thy_Output.antiquotation_raw @{binding "ML"} parser_ml output_ml
+ #> Thy_Output.antiquotation_raw @{binding "ML_ind"} parser_ml_ind output_ml_ind
+ #> Thy_Output.antiquotation_raw @{binding "ML_type"} single_arg output_type
+ #> Thy_Output.antiquotation_raw @{binding "ML_type_ind"} single_arg output_type_ind
+ #> Thy_Output.antiquotation_raw @{binding "ML_struct"} single_arg output_struct
+ #> Thy_Output.antiquotation_raw @{binding "ML_struct_ind"} single_arg output_struct_ind
+ #> Thy_Output.antiquotation_raw @{binding "ML_funct"} single_arg output_funct
+ #> Thy_Output.antiquotation_raw @{binding "ML_funct_ind"} single_arg output_funct_ind
+ #> Thy_Output.antiquotation_raw @{binding "ML_response"} two_args output_response
+ #> Thy_Output.antiquotation_raw @{binding "ML_response_fake"} two_args output_response_fake
+ #> Thy_Output.antiquotation_raw @{binding "ML_response_fake_both"} two_args ouput_response_fake_both
(* FIXME: experimental *)
fun ml_eq (lhs, pat, eq) =
implode ["val true = ((", eq, ") (", lhs, ",", pat, "))"]
-fun output_response_eq {context = ctxt, ...} ((lhs, pat), eq) =
+fun output_response_eq ctxt ((lhs, pat), eq) =
(case eq of
NONE => eval_fn ctxt (ml_pat (lhs, pat))
| SOME e => eval_fn ctxt (ml_eq (lhs, pat, e));
output ctxt ((prefix_lines "" lhs) @ (prefix_lines "> " pat)))
val ml_response_setup =
- Thy_Output.antiquotation @{binding "ML_response_eq"} test output_response_eq
+ Thy_Output.antiquotation_raw @{binding "ML_response_eq"} test output_response_eq
(* checks whether a file exists in the Isabelle distribution *)
fun href_link txt =
let
- val raw = Symbol.encode_raw
+ val raw = I (* FIXME: Symbol.encode_raw *)
val path = "http://isabelle.in.tum.de/repos/isabelle/raw-file/tip/src/"
in
- implode [raw "\\href{", raw path, raw txt, raw "}{", txt, raw "}"]
+ implode [raw "\\href{", raw path, raw txt, raw "}{", get_word txt, raw "}"]
end
-fun check_file_exists {context = ctxt, ...} txt =
+fun check_file_exists _ txt =
(if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt))
- then output ctxt [href_link txt]
+ then Latex.string (href_link txt)
else error (implode ["Source file ", quote txt, " does not exist."]))
-val ml_file_setup = Thy_Output.antiquotation @{binding "ML_file"} single_arg check_file_exists
+val ml_file_setup = Thy_Output.antiquotation_raw @{binding "ML_file"} single_arg check_file_exists
(* replaces the official subgoal antiquotation with one *)
(* that is closer to the actual output *)
+
fun proof_state state =
(case try (Proof.goal o Toplevel.proof_of) state of
SOME {goal, ...} => goal
| _ => error "No proof state");
-fun output_goals {state = node, context = ctxt, ...} _ =
+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 node
+ val state = proof_state (Toplevel.presentation_state ctxt)
val goals = Goal_Display.pretty_goal ctxt state
- val {prop, ...} = rep_thm state;
+ val prop = Thm.prop_of state;
val (As, _) = Logic.strip_horn prop;
- val output = (case (length As) of
- 0 => [goals]
- | n => [Pretty.str (subgoals n), goals])
+ val out = (case (length As) of
+ 0 => goals
+ | n => Pretty.big_list (subgoals n) [goals]) (* FIXME: improve printing? *)
in
- Thy_Output.output ctxt output
+ output ctxt [Pretty.string_of out]
end
-fun output_raw_goal_state {state, context = ctxt, ...} _ =
+fun output_raw_goal_state ctxt _ =
let
- val goals = proof_state state
- val output = [Pretty.str (Syntax.string_of_term ctxt (prop_of goals))]
+ val goals = proof_state (Toplevel.presentation_state ctxt)
+ val out = Syntax.string_of_term ctxt (Thm.prop_of goals)
in
- Thy_Output.output ctxt output
+ output ctxt [out]
end
val subgoals_setup =
- Thy_Output.antiquotation @{binding "subgoals"} (Scan.succeed ()) output_goals
+ Thy_Output.antiquotation_raw @{binding "subgoals"} (Scan.succeed ()) output_goals
val raw_goal_state_setup =
- Thy_Output.antiquotation @{binding "raw_goal_state"} (Scan.succeed ()) output_raw_goal_state
+ Thy_Output.antiquotation_raw @{binding "raw_goal_state"} (Scan.succeed ()) output_raw_goal_state
val setup =
ml_setup #>
--- a/ProgTutorial/document/root.tex Fri Jun 03 15:15:17 2016 +0100
+++ b/ProgTutorial/document/root.tex Tue May 14 11:10:53 2019 +0200
@@ -105,6 +105,9 @@
\renewcommand{\isataggrayML}{\begin{vanishML}\begin{graybox}}
\renewcommand{\endisataggrayML}{\end{graybox}\end{vanishML}}
+\isakeeptag{linenosgrayML}
+\renewcommand{\isataglinenosgrayML}{\begin{vanishML}\begin{graybox}\begin{linenos}}
+\renewcommand{\endisataglinenosgrayML}{\end{linenos}\end{graybox}\end{vanishML}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% for code that has line numbers
--- a/ProgTutorial/output_tutorial.ML Fri Jun 03 15:15:17 2016 +0100
+++ b/ProgTutorial/output_tutorial.ML Tue May 14 11:10:53 2019 +0200
@@ -5,28 +5,29 @@
(* rebuilding the output function from Thy_Output in order to *)
(* enable the options [gray, linenos] *)
-val gray = Unsynchronized.ref false
-val linenos = Unsynchronized.ref false
+val thy_output_linenos = Attrib.setup_config_bool @{binding linenos} (K false)
+val thy_output_gray = Attrib.setup_config_bool @{binding gray} (K false)
-
-fun output ctxt txt =
+fun output_raw ctxt txt =
let
val prts = map Pretty.str txt
in
prts
- |> (if Config.get ctxt Thy_Output.quotes then map Pretty.quote else I)
- |> (if Config.get ctxt Thy_Output.display then
- map (Output.output o Pretty.string_of o Pretty.indent (Config.get ctxt Thy_Output.indent))
+ |> (if Config.get ctxt Document_Antiquotation.thy_output_quotes then map Pretty.quote else I)
+ |> (if Config.get ctxt Document_Antiquotation.thy_output_display then
+ map (Output.output o Pretty.string_of o Pretty.indent (Config.get ctxt Document_Antiquotation.thy_output_indent))
#> space_implode "\\isasep\\isanewline%\n"
- #> (if ! linenos then (enclose "\\begin{linenos}%\n" "%\n\\end{linenos}") else I)
- #> (if ! gray then (enclose "\\begin{graybox}%\n" "%\n\\end{graybox}") else I)
+ #> (if Config.get ctxt thy_output_linenos then (enclose "\\begin{linenos}%\n" "%\n\\end{linenos}") else I)
+ #> (if Config.get ctxt thy_output_gray then (enclose "\\begin{graybox}%\n" "%\n\\end{graybox}") else I)
#> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
else
- map (Output.output o (if Config.get ctxt Thy_Output.break then Pretty.string_of else Pretty.str_of))
+ map (Output.output o (if Config.get ctxt Document_Antiquotation.thy_output_break then Pretty.string_of else Pretty.unformatted_string_of))
#> space_implode "\\isasep\\isanewline%\n"
#> enclose "\\isa{" "}")
end
+fun output ctxt txt = Latex.string (output_raw ctxt txt)
+
datatype indstring =
NoString
| Plain of string
@@ -75,22 +76,19 @@
| _ => "")
fun output_indexed ctxt ind txt =
- txt |> output ctxt
+ txt |> output_raw ctxt
|> prefix (get_index ind)
|> prefix (get_str_index ind)
+ |> Latex.string
fun boolean "" = true
| boolean "true" = true
| boolean "false" = false
| boolean s = error ("Bad boolean value: " ^ quote s);
-val gray_setup = Thy_Output.add_option @{binding "gray"}
- (Thy_Output.add_wrapper o Library.setmp_CRITICAL gray o boolean)
-val linenos_setup = Thy_Output.add_option @{binding "linenos"}
- (Thy_Output.add_wrapper o Library.setmp_CRITICAL linenos o boolean)
+val _ = Theory.setup
+ (Document_Antiquotation.setup_option @{binding gray} (Config.put thy_output_gray o boolean) #>
+ Document_Antiquotation.setup_option @{binding linenos} (Config.put thy_output_linenos o boolean) );
-val setup =
- gray_setup #>
- linenos_setup
end
\ No newline at end of file
--- a/ROOT Fri Jun 03 15:15:17 2016 +0100
+++ b/ROOT Tue May 14 11:10:53 2019 +0200
@@ -1,22 +1,19 @@
-session "Session" in "ProgTutorial" = HOL +
+session "Cookbook" in "ProgTutorial" = HOL +
+ options [document = pdf, browser_info = false, document_output = ".."]
theories [document = false]
"Base"
"Package/Simple_Inductive_Package"
- "~~/src/HOL/Number_Theory/Primes"
- "~~/src/HOL/Library/Code_Target_Numeral"
- "~~/src/HOL/Library/Code_Abstract_Nat"
- theories [quick_and_dirty, document = false]
+ theories [quick_and_dirty, document = true]
"Intro"
"First_Steps"
"Essential"
"Advanced"
- "Parsing"
"Tactical"
"Package/Ind_Intro"
"Package/Ind_Prelims"
"Package/Ind_Interface"
"Package/Ind_General_Scheme"
- "Package/Ind_Code"
+ "Package/Ind_Code"
"Package/Ind_Extensions"
"Appendix"
"Recipes/Antiquotes"
@@ -27,40 +24,9 @@
"Recipes/Sat"
"Recipes/USTypes"
"Solutions"
-
-session "Cookbook" in "ProgTutorial" = HOL +
- options [document = pdf, browser_info = false, document_output = ".."]
- theories [document = false]
- "Base"
- "Package/Simple_Inductive_Package"
- "~~/src/HOL/Number_Theory/Primes"
- "~~/src/HOL/Library/Code_Target_Numeral"
- "~~/src/HOL/Library/Code_Abstract_Nat"
- theories [quick_and_dirty, document = true]
- "Intro"
- "First_Steps"
- "Essential"
- "Advanced"
- "Parsing"
- "Tactical"
- "Package/Ind_Intro"
- "Package/Ind_Prelims"
- "Package/Ind_Interface"
- "Package/Ind_General_Scheme"
- "Package/Ind_Code"
- "Package/Ind_Extensions"
- "Appendix"
- "Recipes/Antiquotes"
- "Recipes/TimeLimit"
- "Recipes/Timing"
- "Recipes/ExternalSolver"
- "Recipes/Oracle"
- "Recipes/Sat"
- "Recipes/USTypes"
- "Solutions"
- document_files
- "root.bib"
- "root.tex"
- "build"
+ document_files
+ "root.bib"
+ "root.tex"
+ "tutorial-logo.jpg"