--- a/ProgTutorial/Base.thy Wed Nov 18 14:06:01 2009 +0100
+++ b/ProgTutorial/Base.thy Thu Nov 19 14:11:50 2009 +0100
@@ -5,6 +5,10 @@
("antiquote_setup.ML")
begin
+notation (latex output)
+ Cons ("_ # _" [66,65] 65)
+
+
(* rebinding of writeln and tracing so that it can *)
(* be compared in intiquotations *)
ML {*
@@ -86,7 +90,7 @@
ML {*
fun propagate_env (context as Context.Proof lthy) =
- Context.Proof (LocalTheory.map_contexts (ML_Env.inherit context) lthy)
+ Context.Proof (Local_Theory.map_contexts (ML_Env.inherit context) lthy)
| propagate_env context = context
fun propagate_env_prf prf = Proof.map_contexts
--- a/ProgTutorial/FirstSteps.thy Wed Nov 18 14:06:01 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy Thu Nov 19 14:11:50 2009 +0100
@@ -888,13 +888,12 @@
"name"}
An example where a qualified name is needed is the function
- @{ML_ind define in LocalTheory}. This function is used below to define
+ @{ML_ind define in Local_Theory}. This function is used below to define
the constant @{term "TrueConj"} as the conjunction @{term "True \<and> True"}.
*}
local_setup %gray {*
- LocalTheory.define Thm.internalK
- ((@{binding "TrueConj"}, NoSyn),
+ Local_Theory.define "" ((@{binding "TrueConj"}, NoSyn),
(Attrib.empty_binding, @{term "True \<and> True"})) #> snd *}
text {*
--- a/ProgTutorial/General.thy Wed Nov 18 14:06:01 2009 +0100
+++ b/ProgTutorial/General.thy Thu Nov 19 14:11:50 2009 +0100
@@ -1333,23 +1333,22 @@
While we obtained a theorem as result, this theorem is not
yet stored in Isabelle's theorem database. Consequently, it cannot be
referenced on the user level. One way to store it in the theorem database is
- by using the function @{ML_ind note in LocalTheory}.\footnote{\bf FIXME: make sure a pointer
+ by using the function @{ML_ind note in Local_Theory}.\footnote{\bf FIXME: make sure a pointer
to the section about local-setup is given earlier.}
*}
local_setup %gray {*
- LocalTheory.note Thm.theoremK
- ((@{binding "my_thm"}, []), [my_thm]) #> snd *}
+ Local_Theory.note ((@{binding "my_thm"}, []), [my_thm]) #> snd *}
text {*
- The fourth argument of @{ML note in LocalTheory} is the list of theorems we
+ The fourth argument of @{ML note in Local_Theory} is the list of theorems we
want to store under a name. We can store more than one under a single name.
The first argument @{ML_ind theoremK in Thm} is
a kind indicator, which classifies the theorem. There are several such kind
indicators: for a theorem arising from a definition you should use @{ML_ind
- definitionK in Thm}, for an axiom @{ML_ind axiomK in Thm}, and for
+ definitionK in Thm}, and for
``normal'' theorems the kinds @{ML_ind theoremK in Thm} or @{ML_ind lemmaK
- in Thm}. The second argument of @{ML note in LocalTheory} is the name under
+ in Thm}. The second argument of @{ML note in Local_Theory} is the name under
which we store the theorem or theorems. The third argument can contain a
list of theorem attributes, which we will explain in detail in
Section~\ref{sec:attributes}. Below we just use one such attribute for
@@ -1357,13 +1356,12 @@
*}
local_setup %gray {*
- LocalTheory.note Thm.theoremK
- ((@{binding "my_thm_simp"},
+ Local_Theory.note ((@{binding "my_thm_simp"},
[Attrib.internal (K Simplifier.simp_add)]), [my_thm]) #> snd *}
text {*
Note that we have to use another name under which the theorem is stored,
- since Isabelle does not allow us to call @{ML_ind note in LocalTheory} twice
+ since Isabelle does not allow us to call @{ML_ind note in Local_Theory} twice
with the same name. The attribute needs to be wrapped inside the function @{ML_ind
internal in Attrib} from the structure @{ML_struct Attrib}. If we use the function
@{ML get_thm_names_from_ss} from
@@ -1392,7 +1390,7 @@
or with the @{text "@{thm \<dots>}"}-antiquotation on the ML-level. Otherwise the
user has no access to these theorems.
- Recall that Isabelle does not let you call @{ML note in LocalTheory} twice
+ Recall that Isabelle does not let you call @{ML note in Local_Theory} twice
with the same theorem name. In effect, once a theorem is stored under a name,
this association is fixed. While this is a ``safety-net'' to make sure a
theorem name refers to a particular theorem or collection of theorems, it is
@@ -1407,9 +1405,9 @@
(type T = thm list
val empty = []
val extend = I
- val merge = op @)
-
-fun update thm = Context.theory_map (MyThmList.map (fn thms => thm::thms))*}
+ val merge = merge Thm.eq_thm_prop)
+
+fun update thm = Context.theory_map (MyThmList.map (Thm.add_thm thm))*}
text {*
The function @{ML update} allows us to update the theorem list, for example
@@ -1650,10 +1648,9 @@
*}
local_setup %gray {*
- LocalTheory.note Thm.lemmaK
- ((@{binding "foo_data'"}, []),
- [(Rule_Cases.name ["foo_case_one", "foo_case_two"]
- @{thm foo_data})]) #> snd *}
+ Local_Theory.note ((@{binding "foo_data'"}, []),
+ [(Rule_Cases.name ["foo_case_one", "foo_case_two"]
+ @{thm foo_data})]) #> snd *}
text {*
The data of the theorem @{thm [source] foo_data'} is then as follows:
@@ -2139,6 +2136,9 @@
section {* Local Theories (TBD) *}
+text {*
+ @{ML_ind "Local_Theory.declaration"}
+*}
(*
setup {*
@@ -2477,6 +2477,50 @@
ML {* (Pretty.str "bar") |> Pretty.string_of |> tracing *}
*)
+section {* Morphisms (TBD) *}
+
+text {*
+ Morphisms are arbitrary transformations over terms, types, theorems and bindings.
+ They can be constructed using the function @{ML_ind morphism in Morphism},
+ which expects a record with functions of type
+
+ \begin{isabelle}
+ \begin{tabular}{rl}
+ @{text "binding:"} & @{text "binding -> binding"}\\
+ @{text "typ:"} & @{text "typ -> typ"}\\
+ @{text "term:"} & @{text "term -> term"}\\
+ @{text "fact:"} & @{text "thm list -> thm list"}
+ \end{tabular}
+ \end{isabelle}
+
+ The simplest morphism is the @{ML_ind identity in Morphism}-morphism defined as
+*}
+
+ML{*val identity = Morphism.morphism {binding = I, typ = I, term = I, fact = I}*}
+
+text {*
+ Morphisms can be composed with the function @{ML_ind "$>" in Morphism}
+*}
+
+ML{*fun trm_phi (Free (x, T)) = Var ((x, 0), T)
+ | trm_phi (Abs (x, T, t)) = Abs (x, T, trm_phi t)
+ | trm_phi (t $ s) = (trm_phi t) $ (trm_phi s)
+ | trm_phi t = t*}
+
+ML{*val phi = Morphism.term_morphism trm_phi*}
+
+ML{*Morphism.term phi @{term "P x y"}*}
+
+text {*
+ @{ML_ind term_morphism in Morphism}
+
+ @{ML_ind term in Morphism},
+ @{ML_ind thm in Morphism}
+
+ \begin{readmore}
+ Morphisms are implemented in the file @{ML_file "Pure/morphism.ML"}.
+ \end{readmore}
+*}
section {* Misc (TBD) *}
@@ -2501,6 +2545,8 @@
text {*
@{ML_ind "Binding.str_of"} returns the string with markup;
@{ML_ind "Binding.name_of"} returns the string without markup
+
+ @{ML_ind "Binding.conceal"}
*}
section {* Concurrency (TBD) *}
--- a/ProgTutorial/Helper/Command/Command.thy Wed Nov 18 14:06:01 2009 +0100
+++ b/ProgTutorial/Helper/Command/Command.thy Thu Nov 19 14:11:50 2009 +0100
@@ -4,7 +4,7 @@
ML {*
let
- val do_nothing = Scan.succeed (LocalTheory.theory I)
+ val do_nothing = Scan.succeed (Local_Theory.theory I)
val kind = OuterKeyword.thy_decl
in
OuterSyntax.local_theory "foobar" "description of foobar" kind do_nothing
@@ -14,7 +14,7 @@
ML {*
let
fun trace_prop str =
- LocalTheory.theory (fn lthy => (tracing str; lthy))
+ Local_Theory.theory (fn lthy => (tracing str; lthy))
val trace_prop_parser = OuterParse.prop >> trace_prop
val kind = OuterKeyword.thy_decl
in
@@ -45,7 +45,7 @@
ML{*
let
fun after_qed thm_name thms lthy =
- LocalTheory.note Thm.theoremK (thm_name, (flat thms)) lthy |> snd
+ Local_Theory.note (thm_name, (flat thms)) lthy |> snd
fun setup_proof (thm_name, (txt, pos)) lthy =
let
@@ -65,7 +65,7 @@
(*
ML {*
let
- val do_nothing = Scan.succeed (LocalTheory.theory I)
+ val do_nothing = Scan.succeed (Local_Theory.theory I)
val kind = OuterKeyword.thy_decl
in
OuterSyntax.local_theory "simple_inductive" "description of foobar" kind do_nothing
--- a/ProgTutorial/Package/Ind_Code.thy Wed Nov 18 14:06:01 2009 +0100
+++ b/ProgTutorial/Package/Ind_Code.thy Thu Nov 19 14:11:50 2009 +0100
@@ -21,27 +21,27 @@
and then ``register'' the definition inside a local theory.
To do the latter, we use the following wrapper for the function
- @{ML_ind define in LocalTheory}. The wrapper takes a predicate name, a syntax
+ @{ML_ind define in Local_Theory}. The wrapper takes a predicate name, a syntax
annotation and a term representing the right-hand side of the definition.
*}
ML %linenosgray{*fun make_defn ((predname, mx), trm) lthy =
let
val arg = ((predname, mx), (Attrib.empty_binding, trm))
- val ((_, (_ , thm)), lthy') = LocalTheory.define Thm.internalK arg lthy
+ val ((_, (_ , thm)), lthy') = Local_Theory.define "" arg lthy
in
(thm, lthy')
end*}
text {*
It returns the definition (as a theorem) and the local theory in which the
- definition has been made. In Line 4, @{ML_ind internalK in Thm} is a flag
+ definition has been made. In Line 4, the string @{ML "\"\""} is a flag
attached to the theorem (other possibile flags are @{ML_ind definitionK in Thm}
- and @{ML_ind axiomK in Thm}).\footnote{\bf FIXME: move to theorem section.}
+ and @{ML_ind theoremK in Thm}).\footnote{\bf FIXME: move to theorem section.}
These flags just classify theorems and have no
significant meaning, except for tools that, for example, find theorems in
the theorem database.\footnote{FIXME: put in the section about theorems.} We
- also use @{ML_ind empty_binding in Attrib} in Line 3, since the definitions for
+ also use @{ML_ind empty_binding in Attrib} 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. A testcase for this function is
*}
@@ -961,7 +961,7 @@
We have produced various theorems (definitions, induction principles and
introduction rules), but apart from the definitions, we have not yet
registered them with the theorem database. This is what the functions
- @{ML_ind note in LocalTheory} does.
+ @{ML_ind note in Local_Theory} does.
For convenience, we use the following
@@ -969,8 +969,7 @@
*}
ML{*fun note_many qname ((name, attrs), thms) =
- LocalTheory.note Thm.theoremK
- ((Binding.qualify false qname name, attrs), thms)
+ Local_Theory.note ((Binding.qualify false qname name, attrs), thms)
fun note_single1 qname ((name, attrs), thm) =
note_many qname ((name, attrs), [thm])
--- a/ProgTutorial/Package/simple_inductive_package.ML Wed Nov 18 14:06:01 2009 +0100
+++ b/ProgTutorial/Package/simple_inductive_package.ML Thu Nov 19 14:11:50 2009 +0100
@@ -22,7 +22,7 @@
fun make_defs ((binding, syn), trm) lthy =
let
val arg = ((binding, syn), (Attrib.empty_binding, trm))
- val ((_, (_ , thm)), lthy) = LocalTheory.define Thm.internalK arg lthy
+ val ((_, (_ , thm)), lthy) = Local_Theory.define "" arg lthy
in
(thm, lthy)
end
@@ -180,12 +180,12 @@
val case_names = map (Binding.name_of o fst o fst) specs
in
lthy1
- |> LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) =>
+ |> Local_Theory.notes (map (fn (((a, atts), _), th) =>
((Binding.qualify false mut_name a, atts), [([th], [])])) (specs ~~ intros))
- |-> (fn intross => LocalTheory.note Thm.theoremK
+ |-> (fn intross => Local_Theory.note
((Binding.qualify false mut_name (Binding.name "intros"), []), maps snd intross))
|>> snd
- ||>> (LocalTheory.notes Thm.theoremK (map (fn (((R, _), _), th) =>
+ ||>> (Local_Theory.notes (map (fn (((R, _), _), th) =>
((Binding.qualify false (Binding.name_of R) (Binding.name "induct"),
[Attrib.internal (K (Rule_Cases.case_names case_names)),
Attrib.internal (K (Rule_Cases.consumes 1)),
--- a/ProgTutorial/Parsing.thy Wed Nov 18 14:06:01 2009 +0100
+++ b/ProgTutorial/Parsing.thy Thu Nov 19 14:11:50 2009 +0100
@@ -939,7 +939,7 @@
*}
ML{*let
- val do_nothing = Scan.succeed (LocalTheory.theory I)
+ val do_nothing = Scan.succeed (Local_Theory.theory I)
val kind = OuterKeyword.thy_decl
in
OuterSyntax.local_theory "foobar" "description of foobar" kind do_nothing
@@ -976,7 +976,7 @@
\isacommand{ML}~@{text "\<verbopen>"}\\
@{ML
"let
- val do_nothing = Scan.succeed (LocalTheory.theory I)
+ val do_nothing = Scan.succeed (Local_Theory.theory I)
val kind = OuterKeyword.thy_decl
in
OuterSyntax.local_theory \"foobar\" \"description of foobar\" kind do_nothing
@@ -1093,7 +1093,7 @@
The crucial part of a command is the function that determines the behaviour
of the command. In the code above we used a ``do-nothing''-function, which
because of @{ML_ind succeed in Scan} does not parse any argument, but immediately
- returns the simple function @{ML "LocalTheory.theory I"}. We can
+ returns the simple function @{ML "Local_Theory.theory I"}. We can
replace this code by a function that first parses a proposition (using the
parser @{ML OuterParse.prop}), then prints out the tracing
information (using a new function @{text trace_prop}) and
@@ -1102,7 +1102,7 @@
ML{*let
fun trace_prop str =
- LocalTheory.theory (fn ctxt => (tracing str; ctxt))
+ Local_Theory.theory (fn ctxt => (tracing str; ctxt))
val kind = OuterKeyword.thy_decl
in
@@ -1181,14 +1181,14 @@
text {*
{\bf TBD below}
- (FIXME: read a name and show how to store theorems; see @{ML_ind note in LocalTheory})
+ (FIXME: read a name and show how to store theorems; see @{ML_ind note in Local_Theory})
*}
ML_val{*val r = Unsynchronized.ref (NONE:(unit -> term) option)*}
ML{*let
fun after_qed thm_name thms lthy =
- LocalTheory.note Thm.theoremK (thm_name, (flat thms)) lthy |> snd
+ Local_Theory.note (thm_name, (flat thms)) lthy |> snd
fun setup_proof (thm_name, (txt, pos)) lthy =
let
Binary file progtutorial.pdf has changed