isabelle-cookbook: comparison ProgTutorial/Advanced.thy

equal deleted inserted replaced

-:be23597e81db
+:f875a25aa72d
 not to a \emph{stale} one. Consider again the function inside the
 \isacommand{setup}-command:
 \begin{isabelle}
 \begin{graybox}
-\isacommand{setup}~\<open>\<verbopen>\<close> @{ML
+\isacommand{setup}~\<open>\<verbopen>\<close> @{ML \<open>fn thy =>
-"fn thy =>
 let
-val bar_const = ((@{binding \"BAR\"}, @{typ \"nat\"}), NoSyn)
+val bar_const = ((@{binding "BAR"}, @{typ "nat"}), NoSyn)
 val (_, thy') = Sign.declare_const @{context} bar_const thy
 in
 thy
-end"}~\<open>\<verbclose>\<close>\isanewline
+end\<close>}~\<open>\<verbclose>\<close>\isanewline
 \<open>> ERROR: "Stale theory encountered"\<close>
 \end{graybox}
 \end{isabelle}
 This time we erroneously return the original theory \<open>thy\<close>, instead of
 This function takes a term and a context as argument. Notice how the printing
 of the term changes according to which context is used.
 \begin{isabelle}
 \begin{graybox}
-@{ML "let
+@{ML \<open>let
-val trm = @{term \"(x, y, z, w)\"}
+val trm = @{term "(x, y, z, w)"}
 in
 pwriteln (Pretty.chunks
 [ pretty_term ctxt0 trm,
 pretty_term ctxt1 trm,
 pretty_term ctxt2 trm ])
-end"}\\
+end\<close>}\\
 \setlength{\fboxsep}{0mm}
 \<open>>\<close>~\<open>(\<close>\colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{\<open>x\<close>}}\<open>,\<close>~%
 \colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{\<open>y\<close>}}\<open>,\<close>~%
 \colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{\<open>z\<close>}}\<open>,\<close>~%
 \colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{\<open>w\<close>}}\<open>)\<close>\\
 \end{graybox}
 \end{isabelle}
 The term we are printing is in all three cases the same---a tuple containing
-four free variables. As you can see, however, in case of @{ML "ctxt0"} all
+four free variables. As you can see, however, in case of @{ML \<open>ctxt0\<close>} all
-variables are highlighted indicating a problem, while in case of @{ML
+variables are highlighted indicating a problem, while in case of @{ML \<open>ctxt1\<close>} \<open>x\<close> and \<open>y\<close> are printed as normal (blue) free
-"ctxt1"} \<open>x\<close> and \<open>y\<close> are printed as normal (blue) free
 variables, but not \<open>z\<close> and \<open>w\<close>. In the last case all variables
 are printed as expected. The point of this example is that the context
 contains the information which variables are fixed, and designates all other
 free variables as being alien or faulty.  Therefore the highlighting.
 While this seems like a minor detail, the concept of making the context aware
 of fixed variables is actually quite useful. For example it prevents us from
 fixing a variable twice
 @{ML_matchresult_fake [gray, display]
-"@{context}
+\<open>@{context}
-|> Variable.add_fixes [\"x\", \"x\"]"
+|> Variable.add_fixes ["x", "x"]\<close>
-"ERROR: Duplicate fixed variable(s): \"x\""}
+\<open>ERROR: Duplicate fixed variable(s): "x"\<close>}
 More importantly it also allows us to easily create fresh names for
 fixed variables.  For this you have to use the function @{ML_ind
 variant_fixes in Variable} from the structure @{ML_structure Variable}.
 @{ML_matchresult_fake [gray, display]
-"@{context}
+\<open>@{context}
-|> Variable.variant_fixes [\"y\", \"y\", \"z\"]"
+|> Variable.variant_fixes ["y", "y", "z"]\<close>
-"([\"y\", \"ya\", \"z\"], ...)"}
+\<open>(["y", "ya", "z"], ...)\<close>}
 Now a fresh variant for the second occurence of \<open>y\<close> is created
 avoiding any clash. In this way we can also create fresh free variables
 that avoid any clashes with fixed variables. In Line~3 below we fix
 the variable \<open>x\<close> in the context \<open>ctxt1\<close>. Next we want to
 create two fresh variables of type @{typ nat} as variants of the
 string @{text [quotes] "x"} (Lines 6 and 7).
 @{ML_matchresult_fake [display, gray, linenos]
-"let
+\<open>let
 val ctxt0 = @{context}
-val (_, ctxt1) = Variable.add_fixes [\"x\"] ctxt0
+val (_, ctxt1) = Variable.add_fixes ["x"] ctxt0
-val frees = replicate 2 (\"x\", @{typ nat})
+val frees = replicate 2 ("x", @{typ nat})
 in
 (Variable.variant_frees ctxt0 [] frees,
 Variable.variant_frees ctxt1 [] frees)
-end"
+end\<close>
-"([(\"x\", \"nat\"), (\"xa\", \"nat\")],
+\<open>([("x", "nat"), ("xa", "nat")],
-[(\"xa\", \"nat\"), (\"xb\", \"nat\")])"}
+[("xa", "nat"), ("xb", "nat")])\<close>}
 As you can see, if we create the fresh variables with the context \<open>ctxt0\<close>,
 then we obtain \<open>x\<close> and \<open>xa\<close>; but in \<open>ctxt1\<close> we obtain \<open>xa\<close>
 and \<open>xb\<close> avoiding \<open>x\<close>, which was fixed in this context.
 Often one has the problem that given some terms, create fresh variables
 avoiding any variable occurring in those terms. For this you can use the
 function @{ML_ind declare_term in Variable} from the structure @{ML_structure Variable}.
 @{ML_matchresult_fake [gray, display]
-"let
+\<open>let
-val ctxt1 = Variable.declare_term @{term \"(x, xa)\"} @{context}
+val ctxt1 = Variable.declare_term @{term "(x, xa)"} @{context}
-val frees = replicate 2 (\"x\", @{typ nat})
+val frees = replicate 2 ("x", @{typ nat})
 in
 Variable.variant_frees ctxt1 [] frees
-end"
+end\<close>
-"[(\"xb\", \"nat\"), (\"xc\", \"nat\")]"}
+\<open>[("xb", "nat"), ("xc", "nat")]\<close>}
 The result is \<open>xb\<close> and \<open>xc\<close> for the names of the fresh
 variables, since \<open>x\<close> and \<open>xa\<close> occur in the term we declared.
 Note that @{ML_ind declare_term in Variable} does not fix the
 variables; it just makes them ``known'' to the context. You can see
 that if you print out a declared term.
 \begin{isabelle}
 \begin{graybox}
-@{ML "let
+@{ML \<open>let
-val trm = @{term \"P x y z\"}
+val trm = @{term "P x y z"}
 val ctxt1 = Variable.declare_term trm @{context}
 in
 pwriteln (pretty_term ctxt1 trm)
-end"}\\
+end\<close>}\\
 \setlength{\fboxsep}{0mm}
 \<open>>\<close>~\colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{\<open>P\<close>}}~%
 \colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{\<open>x\<close>}}~%
 \colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{\<open>y\<close>}}~%
 \colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{\<open>z\<close>}}
 fixed. However, declaring a term is helpful when parsing terms using
 the function @{ML_ind read_term in Syntax} from the structure
 @{ML_structure Syntax}. Consider the following code:
 @{ML_matchresult_fake [gray, display]
-"let
+\<open>let
 val ctxt0 = @{context}
-val ctxt1 = Variable.declare_term @{term \"x::nat\"} ctxt0
+val ctxt1 = Variable.declare_term @{term "x::nat"} ctxt0
 in
-(Syntax.read_term ctxt0 \"x\",
+(Syntax.read_term ctxt0 "x",
-Syntax.read_term ctxt1 \"x\")
+Syntax.read_term ctxt1 "x")
-end"
+end\<close>
-"(Free (\"x\", \"'a\"), Free (\"x\", \"nat\"))"}
+\<open>(Free ("x", "'a"), Free ("x", "nat"))\<close>}
 Parsing the string in the context \<open>ctxt0\<close> results in a free variable
 with a default polymorphic type, but in case of \<open>ctxt1\<close> we obtain a
 free variable of type @{typ nat} as previously declared. Which
 type the parsed term receives depends upon the last declaration that
 is made, as the next example illustrates.
 @{ML_matchresult_fake [gray, display]
-"let
+\<open>let
-val ctxt1 = Variable.declare_term @{term \"x::nat\"} @{context}
+val ctxt1 = Variable.declare_term @{term "x::nat"} @{context}
-val ctxt2 = Variable.declare_term @{term \"x::int\"} ctxt1
+val ctxt2 = Variable.declare_term @{term "x::int"} ctxt1
 in
-(Syntax.read_term ctxt1 \"x\",
+(Syntax.read_term ctxt1 "x",
-Syntax.read_term ctxt2 \"x\")
+Syntax.read_term ctxt2 "x")
-end"
+end\<close>
-"(Free (\"x\", \"nat\"), Free (\"x\", \"int\"))"}
+\<open>(Free ("x", "nat"), Free ("x", "int"))\<close>}
 The most useful feature of contexts is that one can export, or transfer,
 terms and theorems between them. We show this first for terms.
 \begin{isabelle}
 \begin{graybox}
 \begin{linenos}
-@{ML "let
+@{ML \<open>let
 val ctxt0 = @{context}
-val (_, ctxt1) = Variable.add_fixes [\"x\", \"y\", \"z\"] ctxt0
+val (_, ctxt1) = Variable.add_fixes ["x", "y", "z"] ctxt0
-val foo_trm = @{term \"P x y z\"}
+val foo_trm = @{term "P x y z"}
 in
 singleton (Variable.export_terms ctxt1 ctxt0) foo_trm
 |> pretty_term ctxt0
 |> pwriteln
-end"}
+end\<close>}
 \end{linenos}
 \setlength{\fboxsep}{0mm}
 \<open>>\<close>~\colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{\<open>P\<close>}}~%
 \<open>?x ?y ?z\<close>
 \end{graybox}
 structure @{ML_structure Skip_Proof}. This function will turn an arbitray
 term, in our case @{term "P x y z x y z"}, into a theorem (disregarding
 whether it is actually provable).
 @{ML_matchresult_fake [display, gray]
-"let
+\<open>let
 val thy = @{theory}
 val ctxt0 = @{context}
-val (_, ctxt1) = Variable.add_fixes [\"P\", \"x\", \"y\", \"z\"] ctxt0
+val (_, ctxt1) = Variable.add_fixes ["P", "x", "y", "z"] ctxt0
-val foo_thm = Skip_Proof.make_thm thy @{prop \"P x y z x y z\"}
+val foo_thm = Skip_Proof.make_thm thy @{prop "P x y z x y z"}
 in
 singleton (Proof_Context.export ctxt1 ctxt0) foo_thm
-end"
+end\<close>
-"?P ?x ?y ?z ?x ?y ?z"}
+\<open>?P ?x ?y ?z ?x ?y ?z\<close>}
 Since we fixed all variables in \<open>ctxt1\<close>, in the exported
 result all of them are schematic. The great point of contexts is
 that exporting from one to another is not just restricted to
 variables, but also works with assumptions. For this we can use the
 function @{ML_ind export in Assumption} from the structure
 @{ML_structure Assumption}. Consider the following code.
 @{ML_matchresult_fake [display, gray, linenos]
-"let
+\<open>let
 val ctxt0 = @{context}
-val ([eq], ctxt1) = Assumption.add_assumes [@{cprop \"x \<equiv> y\"}] ctxt0
+val ([eq], ctxt1) = Assumption.add_assumes [@{cprop "x \<equiv> y"}] ctxt0
 val eq' = Thm.symmetric eq
 in
 Assumption.export false ctxt1 ctxt0 eq'
-end"
+end\<close>
-"x \<equiv> y \<Longrightarrow> y \<equiv> x"}
+\<open>x \<equiv> y \<Longrightarrow> y \<equiv> x\<close>}
 The function @{ML_ind add_assumes in Assumption} from the structure
 @{ML_structure Assumption} adds the assumption \mbox{\<open>x \<equiv> y\<close>}
 to the context \<open>ctxt1\<close> (Line 3). This function expects a list
 of @{ML_type cterm}s and returns them as theorems, together with the
 @{ML_structure Proof_Context} combines both export functions from
 @{ML_structure Variable} and @{ML_structure Assumption}. This can be seen
 in the following example.
 @{ML_matchresult_fake [display, gray]
-"let
+\<open>let
 val ctxt0 = @{context}
 val ((fvs, [eq]), ctxt1) = ctxt0
-|> Variable.add_fixes [\"x\", \"y\"]
+|> Variable.add_fixes ["x", "y"]
-||>> Assumption.add_assumes [@{cprop \"x \<equiv> y\"}]
+||>> Assumption.add_assumes [@{cprop "x \<equiv> y"}]
 val eq' = Thm.symmetric eq
 in
 Proof_Context.export ctxt1 ctxt0 [eq']
-end"
+end\<close>
-"[?x \<equiv> ?y \<Longrightarrow> ?y \<equiv> ?x]"}
+\<open>[?x \<equiv> ?y \<Longrightarrow> ?y \<equiv> ?x]\<close>}
 \<close>
 text \<open>
 variables and local assumptions that may be used by the package. The type
 @{ML_type local_theory} is identical to the type of \emph{proof contexts}
 @{ML_type "Proof.context"}, although not every proof context constitutes a
 valid local theory.
-@{ML "Context.>> o Context.map_theory"}
+@{ML \<open>Context.>> o Context.map_theory\<close>}
 @{ML_ind "Local_Theory.declaration"}
 A similar command is \isacommand{local\_setup}, which expects a function
 of type @{ML_type "local_theory -> local_theory"}. Later on we will also
 use the commands \isacommand{method\_setup} for installing methods in the
 These are strings with some additional information, such as positional
 information and qualifiers. Such qualified names can be generated with the
 antiquotation \<open>@{binding \<dots>}\<close>. For example
 @{ML_matchresult [display,gray]
-"@{binding \"name\"}"
+\<open>@{binding "name"}\<close>
-"name"}
+\<open>name\<close>}
 An example where a qualified name is needed is the function
 @{ML_ind define in Local_Theory}.  This function is used below to define
 the constant @{term "TrueConj"} as the conjunction @{term "True \<and> True"}.
 \<close>
 section and link with the comment in the antiquotation section.}
 Occasionally you have to calculate what the ``base'' name of a given
 constant is. For this you can use the function @{ML_ind  Long_Name.base_name}. For example:
-@{ML_matchresult [display,gray] "Long_Name.base_name \"List.list.Nil\"" "\"Nil\""}
+@{ML_matchresult [display,gray] \<open>Long_Name.base_name "List.list.Nil"\<close> \<open>"Nil"\<close>}
 \begin{readmore}
 Functions about naming are implemented in @{ML_file "Pure/General/name_space.ML"};
 functions about signatures in @{ML_file "Pure/sign.ML"}.
 \end{readmore}

changeset 569	f875a25aa72d
parent 567	f7c97e64cc2a
child 572	438703674711