--- 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}