isabelle-cookbook: comparison ProgTutorial/Package/Ind

equal deleted inserted replaced

-:79202e2eab6a
+:de49d5780f57
 @{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 [index] define in LocalTheory}. The wrapper takes a predicate name, a syntax
+@{ML_ind [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 [index] internalK in Thm} is a flag
+definition has been made. In Line 4, @{ML_ind [index] internalK in Thm} is a flag
-attached to the theorem (other possibile flags are @{ML [index] definitionK in Thm}
+attached to the theorem (other possibile flags are @{ML_ind [index] definitionK in Thm}
-and @{ML [index] axiomK in Thm}). These flags just classify theorems and have no
+and @{ML_ind [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 [index] empty_binding in Attrib} in Line 3, since the definitions for
+also use @{ML_ind [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 =>
 text {*
 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 using the function @{ML [index] theory_of in ProofContext}
+behind the local theory using the function @{ML_ind [index] theory_of in ProofContext}
 (Line 3); with this theory we can use the function
-@{ML [index] atomize_term in ObjectLogic} to make the transformation (Line 4). The call
+@{ML_ind [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
 *}
 case that no introduction rules are given, the conclusion of this
 implication needs to be wrapped inside a @{term Trueprop}, otherwise
 the Isabelle's goal mechanism will fail.\footnote{FIXME: check with
 Stefan...is this so?}
-In Line 11 we set up the goal to be proved using the function @{ML [index]
+In Line 11 we set up the goal to be proved using the function @{ML_ind [index]
 prove in Goal}; in the next line we call the tactic for proving the
 induction principle. As mentioned before, this tactic expects the
 definitions, the premise and the (certified) predicates with which the
 introduction rules have been substituted. The code in these two lines will
 return a theorem. However, it is a theorem proved inside the local theory
 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 [index] subst_free}. Line 14 and 15 just iterate
+(Line 11) using the function @{ML_ind [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 [index] SUBPROOF}, since this tactic provides us with the parameters (as
+tactic @{ML_ind [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 with @{ML SUBPROOF}, however, is that it always expects us to
 completely discharge the goal (see Section~\ref{sec:simpletacs}). This is
 a bit inconvenient for our gradual explanation of the proof here. Therefore
-we use first the function @{ML [index] FOCUS in Subgoal}, which does s
+we use first the function @{ML_ind [index] FOCUS in Subgoal}, which does s
 ame as @{ML SUBPROOF}
 but does not require us to completely discharge the goal.
 *}
 (*<*)oops(*>*)
 text_raw {*
 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 @{ML FOCUS in Subgoal} will
 supply us the @{text "params"} and @{text "prems"} as lists, we can
-separate them using the function @{ML [index] chop}.
+separate them using the function @{ML_ind [index] chop}.
 *}
 ML %linenosgray{*fun chop_test_tac preds rules =
 Subgoal.FOCUS (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 [index] rulify in ObjectLogic}). So we can modify the
+format (using @{ML_ind [index] rulify in ObjectLogic}). So we can modify the
 code as follows:
 *}
 ML %linenosgray{*fun apply_prem_tac i preds rules =
 Subgoal.FOCUS (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 [index] MRS} does nothing. Similarly, in the
+just the empty list and the function @{ML_ind [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 [index] map_index} since we
+The iteration is done with the function @{ML_ind [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 [index] note in LocalTheory} does.
+@{ML_ind [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 [index] case_names in RuleCases}
+to use some specific attributes. The first @{ML_ind [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 315	de49d5780f57
parent 305	2ac9dc1a95b4
child 316	74f0a06f751f