--- a/ProgTutorial/Essential.thy Sat Aug 28 13:37:25 2010 +0800
+++ b/ProgTutorial/Essential.thy Fri Oct 29 11:00:37 2010 +0100
@@ -38,7 +38,7 @@
@{ML_response [display,gray]
"@{term \"(a::nat) + b = c\"}"
-"Const (\"op =\", \<dots>) $
+"Const (\"HOL.eq\", \<dots>) $
(Const (\"Groups.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
constructs the term @{term "(a::nat) + b = c"}. The resulting term is printed using
@@ -1092,10 +1092,10 @@
also tries first to solve the problem by higher-order pattern
unification. Only in case of failure full higher-order unification is
called. This function has a built-in bound, which can be accessed and
- manipulated as a configuration value:
+ manipulated as a configuration value. For example
@{ML_response_fake [display,gray]
- "Config.get_global @{theory} (Unify.search_bound_value)"
+ "Config.get_global @{theory} (Unify.search_bound)"
"Int 60"}
If this bound is reached during unification, Isabelle prints out the
@@ -1538,7 +1538,7 @@
also a bit too restrictive in cases where a theorem name should refer to a
dynamically expanding list of theorems (like a simpset). Therefore Isabelle
also implements a mechanism where a theorem name can refer to a custom theorem
- list. For this you can use the function @{ML_ind add_thms_dynamic in PureThy}.
+ list. For this you can use the function @{ML_ind add_thms_dynamic in Global_Theory}.
To see how it works let us assume we defined our own theorem list @{text MyThmList}.
*}
@@ -1560,11 +1560,11 @@
text {*
We can now install the theorem list so that it is visible to the user and
can be refered to by a theorem name. For this need to call
- @{ML_ind add_thms_dynamic in PureThy}
+ @{ML_ind add_thms_dynamic in Global_Theory}
*}
setup %gray {*
- PureThy.add_thms_dynamic (@{binding "mythmlist"}, MyThmList.get)
+ Global_Theory.add_thms_dynamic (@{binding "mythmlist"}, MyThmList.get)
*}
text {*
--- a/ProgTutorial/First_Steps.thy Sat Aug 28 13:37:25 2010 +0800
+++ b/ProgTutorial/First_Steps.thy Fri Oct 29 11:00:37 2010 +0100
@@ -259,17 +259,17 @@
text {*
You can also print out terms together with their typing information.
- For this you need to set the reference @{ML_ind show_types in Syntax}
- to @{ML true}.
+ For this you need to set the configuration value
+ @{ML_ind show_types in Syntax} to @{ML true}.
*}
-ML{*show_types := true*}
+ML{*val show_types_ctxt = Config.put show_types true @{context}*}
text {*
- Now @{ML pretty_term} prints out
+ Now by using this context @{ML pretty_term} prints out
@{ML_response_fake [display, gray]
- "pwriteln (pretty_term @{context} @{term \"(1::nat, x)\"})"
+ "pwriteln (pretty_term show_types_ctxt @{term \"(1::nat, x)\"})"
"(1::nat, x::'a)"}
where @{text 1} and @{text x} are displayed with their inferred type.
@@ -277,19 +277,18 @@
the reference @{ML_ind show_all_types in Syntax} to @{ML true}.
In this case we obtain
*}
-(*<*)ML %linenos {*show_all_types := true*}
-(*>*)
+
text {*
@{ML_response_fake [display, gray]
- "pwriteln (pretty_term @{context} @{term \"(1::nat, x)\"})"
+ "pwriteln (pretty_term
+ (Config.put show_all_types true @{context}) @{term \"(1::nat, x)\"})"
"(Pair::nat \<Rightarrow> 'a \<Rightarrow> nat \<times> 'a) (1::nat) (x::'a)"}
where @{term Pair} is the term-constructor for products.
- Other references that influence printing of terms are
+ Other configuration values that influence printing of terms are
@{ML_ind show_brackets in Syntax} and @{ML_ind show_sorts in Syntax}.
*}
-(*<*)ML %linenos {*show_types := false; show_all_types := false*}
-(*>*)
+
text {*
A @{ML_type cterm} can be printed with the following function.
*}
--- a/ProgTutorial/Helper/Command/Command.thy Sat Aug 28 13:37:25 2010 +0800
+++ b/ProgTutorial/Helper/Command/Command.thy Fri Oct 29 11:00:37 2010 +0100
@@ -40,8 +40,13 @@
*}
ML {*
-val r = Unsynchronized.ref (NONE:(unit -> term) option)
+structure Result = Proof_Data(
+ type T = unit -> term
+ fun init thy () = error "Result")
+
+val result_cookie = (Result.get, Result.put, "Result.put")
*}
+
ML{*
let
fun after_qed thm_name thms lthy =
@@ -49,7 +54,7 @@
fun setup_proof (thm_name, (txt, pos)) lthy =
let
- val trm = ML_Context.evaluate lthy true ("r", r) txt
+ val trm = Code_Runtime.value lthy result_cookie ("", txt)
in
Proof.theorem NONE (after_qed thm_name) [[(trm,[])]] lthy
end
@@ -63,4 +68,5 @@
+
end
--- a/ProgTutorial/Parsing.thy Sat Aug 28 13:37:25 2010 +0800
+++ b/ProgTutorial/Parsing.thy Fri Oct 29 11:00:37 2010 +0100
@@ -802,6 +802,7 @@
for inductive predicates of the form:
*}
+
simple_inductive
even and odd
where
@@ -809,7 +810,6 @@
| evenS: "odd n \<Longrightarrow> even (Suc n)"
| oddS: "even n \<Longrightarrow> odd (Suc n)"
-
text {*
For this we are going to use the parser:
*}
@@ -1202,27 +1202,37 @@
*}
-ML_val{*val r = Unsynchronized.ref (NONE:(unit -> term) option)*}
+ML {*
+structure Result = Proof_Data(
+ type T = unit -> term
+ fun init thy () = error "Result")
+
+val result_cookie = (Result.get, Result.put, "Result.put")
+*}
+
ML{*let
fun after_qed thm_name thms lthy =
Local_Theory.note (thm_name, (flat thms)) lthy |> snd
fun setup_proof (thm_name, (txt, pos)) lthy =
let
- val trm = ML_Context.evaluate lthy true ("r", r) txt
+ val trm = Code_Runtime.value lthy result_cookie ("", txt)
in
Proof.theorem NONE (after_qed thm_name) [[(trm,[])]] lthy
end
val parser = Parse_Spec.opt_thm_name ":" -- Parse.ML_source
+
in
Outer_Syntax.local_theory_to_proof "foobar_prove" "proving a proposition"
Keyword.thy_goal (parser >> setup_proof)
end*}
+(*
foobar_prove test: {* @{prop "True"} *}
apply(rule TrueI)
done
+*)
(*
ML {*
--- a/ProgTutorial/Tactical.thy Sat Aug 28 13:37:25 2010 +0800
+++ b/ProgTutorial/Tactical.thy Fri Oct 29 11:00:37 2010 +0100
@@ -39,6 +39,8 @@
apply(assumption)
done
+
+
text {*
This proof translates to the following ML-code.
@@ -79,34 +81,6 @@
Manual.
\end{readmore}
- Note that in the code above we use antiquotations for referencing the
- theorems. We could also just have written @{ML "etac disjE 1"} because
- many of the basic theorems have a corresponding ML-binding:
-
- @{ML_response_fake [gray,display]
- "disjE"
- "\<lbrakk>?P \<or> ?Q; ?P \<Longrightarrow> ?R; ?Q \<Longrightarrow> ?R\<rbrakk> \<Longrightarrow> ?R"}
-
- In case where no ML-binding exists, theorems can also be looked up dynamically
- using the function @{ML thm} and the (string) name of the theorem. For example:
-
- @{ML_response_fake [gray,display]
- "thm \"disjE\""
- "\<lbrakk>?P \<or> ?Q; ?P \<Longrightarrow> ?R; ?Q \<Longrightarrow> ?R\<rbrakk> \<Longrightarrow> ?R"}
-
- Both ways however are considered \emph{bad} style! The reason is that the binding
- for @{ML disjE} can be re-assigned and thus one does not have
- complete control over which theorem is actually applied. Similarly with the
- lookup of @{text [quotes] "disjE"}. Although theorems must have a unique name
- in the theorem database, the string can stand for a dynamically updatable
- theorem list. Also in this case we cannot be sure which theorem is applied.
- These problems can be nicely prevented by using antiquotations
-
- @{ML_response_fake [gray,display]
- "@{thm \"disjE\"}"
- "\<lbrakk>?P \<or> ?Q; ?P \<Longrightarrow> ?R; ?Q \<Longrightarrow> ?R\<rbrakk> \<Longrightarrow> ?R"}
-
- because then the theorems are fixed statically at compile-time.
\index{tactic@ {\tt\slshape{}tactic}}
\index{raw\_tactic@ {\tt\slshape{}raw\_tactic}}
@@ -664,39 +638,8 @@
apply(rule TrueI)
done
-
text {*
- There is one peculiarity about @{ML FOCUS in Subgoal} and @{ML SUBPROOF}.
- If we apply @{text "rtac @{thm allI}"} in the proof below
-*}
-
-lemma
- shows "B \<Longrightarrow> \<forall>x. A x"
-apply(tactic {* rtac @{thm allI} 1 *})
-txt{* it will produce the expected goal state
- @{subgoals [display]} *}
-(*<*)oops(*>*)
-
-text {* But if we apply the same tactic inside @{ML FOCUS in Subgoal}
- we obtain
-*}
-
-lemma
- shows "B \<Longrightarrow> \<forall>x. A x"
-apply(tactic {* Subgoal.FOCUS (fn _ => rtac @{thm allI} 1) @{context} 1 *})
-txt{* it will produce the goal state
- @{subgoals [display]}
-
- If we want to imitate the behaviour of the ``plain'' tactic, then we
- can apply the tactic @{ML norm_hhf_tac in Goal}. This gives
-*}
-apply(tactic {* Goal.norm_hhf_tac 1 *})
-txt{*@{subgoals [display]}*}
-(*<*)oops(*>*)
-
-text {*
- This tactic transforms the goal state into a \emph{hereditary Harrop normal
- form}. To sum up, both @{ML FOCUS in Subgoal} and @{ML SUBPROOF} are rather
+ To sum up, both @{ML FOCUS in Subgoal} and @{ML SUBPROOF} are rather
convenient, but can impose a considerable run-time penalty in automatic
proofs. If speed is of the essence, then maybe the two lower level combinators
described next are more appropriate.
Binary file progtutorial.pdf has changed