isabelle-cookbook: comparison ProgTutorial/Package/Ind

equal deleted inserted replaced

-:ef1da1abee46
+:1fb8d62c88a0
 @{text [display] "pred \<equiv> \<lambda>zs. \<forall>preds. orules \<longrightarrow> pred zs"}
 and then ``register'' the definition inside a local theory.
 To do the latter, we use the following wrapper for the function
-@{ML LocalTheory.define}. The wrapper takes a predicate name, a syntax
+@{ML [index] define in LocalTheory}. 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
 (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 internalK in Thm} is a flag
+definition has been made. In Line 4, @{ML [index] internalK in Thm} is a flag
-attached to the theorem (others possibile flags are @{ML definitionK in Thm}
+attached to the theorem (others possibile flags are @{ML [index] definitionK in Thm}
-and @{ML axiomK in Thm}). These flags just classify theorems and have no
+and @{ML [index] axiomK in Thm}). 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 empty_binding in Attrib} in Line 3, since the definitions for
+also use @{ML [index] 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
 *}
 local_setup %gray {* fn lthy =>
 The user will state the introduction rules using meta-implications and
 meta-quanti\-fications. In Line 4, we transform these introduction rules
 into the object logic (since definitions cannot be stated with
 meta-connectives). To do this transformation we have to obtain the theory
 behind the local theory (Line 3); with this theory we can use the function
-@{ML ObjectLogic.atomize_term} to make the transformation (Line 4). The call
+@{ML [index] atomize_term in ObjectLogic} to make the transformation (Line 4). The call
 to @{ML defn_aux} in Line 5 produces all right-hand sides of the
 definitions. The actual definitions are then made in Line 7.  The result of
 the function is a list of theorems and a local theory (the theorems are
 registered with the local theory). A testcase for this function is
 *}
 the new local theory @{text "lthy'"}. From the local theory we extract
 the ambient theory in Line 6. We need this theory in order to certify
 the new predicates. In Line 8, we construct the types of these new predicates
 using the given argument types. Next we turn them into terms and subsequently
 certify them (Line 9 and 10). We can now produce the substituted introduction rules
-(Line 11) using the function @{ML subst_free}. Line 14 and 15 just iterate
+(Line 11) using the function @{ML [index] subst_free}. Line 14 and 15 just iterate
 the proofs for all predicates.
 From this we obtain a list of theorems. Finally we need to export the
 fixed variables @{text "Ps"} to obtain the schematic variables @{text "?Ps"}
 (Line 16).
 first two) and assumptions from the definition of the predicate (assumption
 three to six). We need to treat these parameters and assumptions
 differently. In the code below we will therefore separate them into @{text
 "params1"} and @{text params2}, respectively @{text "prems1"} and @{text
 "prems2"}. To do this separation, it is best to open a subproof with the
-tactic @{ML SUBPROOF}, since this tactic provides us with the parameters (as
+tactic @{ML [index] SUBPROOF}, since this tactic provides us with the parameters (as
 list of @{ML_type cterm}s) and the assumptions (as list of @{ML_type thm}s).
 The problem we have to overcome with @{ML SUBPROOF}
 is, however, that this tactic always expects us to completely discharge the
 goal (see Section~\ref{sec:simpletacs}). This is inconvenient for our
 gradual explanation of the proof here. To circumvent this inconvenience we
 First we calculate the values for @{text "params1/2"} and @{text "prems1/2"}
 from @{text "params"} and @{text "prems"}, respectively. To better see what is
 going in our example, we will print out these values using the printing
 function in Figure~\ref{fig:chopprint}. Since the tactic @{ML SUBPROOF} will
 supply us the @{text "params"} and @{text "prems"} as lists, we can
-separate them using the function @{ML chop}.
+separate them using the function @{ML [index] chop}.
 *}
 ML{*fun chop_test_tac preds rules =
 SUBPROOF_test (fn {params, prems, context, ...} =>
 let
 @{term [display] "\<forall>a b t. a \<noteq> b \<longrightarrow> fresh a t \<longrightarrow> fresh a (Lam a t)"}
 To use this premise with @{ML rtac}, we need to instantiate its
 quantifiers (with @{text params1}) and transform it into rule
-format (using @{ML "ObjectLogic.rulify"}. So we can modify the
+format (using @{ML [index] rulify in ObjectLogic}. So we can modify the
 subproof as follows:
 *}
 ML %linenosgray{*fun apply_prem_tac i preds rules =
 SUBPROOF_test (fn {params, prems, context, ...} =>
 text {*
 In Line 4 we use the @{text prems} from the @{ML SUBPROOF} and resolve
 them with @{text prem}. In the simple cases, that is where the @{text prem}
 comes from a non-recursive premise of the rule, @{text prems} will be
-just the empty list and the function @{ML MRS} does nothing. Similarly, in the
+just the empty list and the function @{ML [index] MRS} does nothing. Similarly, in the
 cases where the recursive premises of the rule do not have preconditions.
 In case there are preconditions, then Line 4 discharges them. After
 that we can proceed as before, i.e., check whether the outermost
 connective is @{text "\<forall>"}.
 in
 map_index intros_aux rules
 end*}
 text {*
-The iteration is done with the function @{ML map_index} since we
+The iteration is done with the function @{ML [index] map_index} since we
 need the introduction rule together with its number (counted from
 @{text 0}). This completes the code for the functions deriving the
 reasoning infrastructure. It remains to implement some administrative
 code that strings everything together.
 *}
 text {*
 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 LocalTheory.note} does.
+@{ML [index] note in LocalTheory} does.
 For convenience, we use the following
 three wrappers this function:
 *}
 @{text "mut_name.inducts"}, respectively (see previous paragraph).
 Line 20 add further every introduction rule under its own name
 (given by the user).\footnote{FIXME: what happens if the user did not give
 any name.} Line 21 registers the induction principles. For this we have
-to use some specific attributes. The first @{ML "case_names" in RuleCases}
+to use some specific attributes. The first @{ML [index] case_names in RuleCases}
 corresponds to the case names that are used by Isar to reference the proof
 obligations in the induction. The second @{ML "consumes 1" in RuleCases}
 indicates that the first premise of the induction principle (namely
 the predicate over which the induction proceeds) is eliminated.

changeset 256	1fb8d62c88a0
parent 250	ab9e09076462
child 294	ee9d53fbb56b