# HG changeset patch # User Christian Urban # Date 1258636310 -3600 # Node ID 0019ebf76e10ff9d76250a4206dcee09ced4195a # Parent d8b6d5003823d434369edbff3e90959ce3b42226 updated to new Isabelle diff -r d8b6d5003823 -r 0019ebf76e10 ProgTutorial/Base.thy --- 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 diff -r d8b6d5003823 -r 0019ebf76e10 ProgTutorial/FirstSteps.thy --- 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 \ True"}. *} local_setup %gray {* - LocalTheory.define Thm.internalK - ((@{binding "TrueConj"}, NoSyn), + Local_Theory.define "" ((@{binding "TrueConj"}, NoSyn), (Attrib.empty_binding, @{term "True \ True"})) #> snd *} text {* diff -r d8b6d5003823 -r 0019ebf76e10 ProgTutorial/General.thy --- 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 \}"}-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) *} diff -r d8b6d5003823 -r 0019ebf76e10 ProgTutorial/Helper/Command/Command.thy --- 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 diff -r d8b6d5003823 -r 0019ebf76e10 ProgTutorial/Package/Ind_Code.thy --- 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]) diff -r d8b6d5003823 -r 0019ebf76e10 ProgTutorial/Package/simple_inductive_package.ML --- 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)), diff -r d8b6d5003823 -r 0019ebf76e10 ProgTutorial/Parsing.thy --- 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 "\"}\\ @{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 diff -r d8b6d5003823 -r 0019ebf76e10 progtutorial.pdf Binary file progtutorial.pdf has changed