451   the new local theory @{text "lthy'"}. From the local theory we extract

   451   the new local theory @{text "lthy'"}. From the local theory we extract

   452   the ambient theory in Line 6. We need this theory in order to certify 

   452   the ambient theory in Line 6. We need this theory in order to certify 

   453   the new predicates. In Line 8, we construct the types of these new predicates

   453   the new predicates. In Line 8, we construct the types of these new predicates

   454   using the given argument types. Next we turn them into terms and subsequently

   454   using the given argument types. Next we turn them into terms and subsequently

   455   certify them (Line 9 and 10). We can now produce the substituted introduction rules 

   455   certify them (Line 9 and 10). We can now produce the substituted introduction rules 

   457   the proofs for all predicates.

   457   the proofs for all predicates.

   458   From this we obtain a list of theorems. Finally we need to export the 

   458   From this we obtain a list of theorems. Finally we need to export the 

   459   fixed variables @{text "Ps"} to obtain the schematic variables @{text "?Ps"} 

   459   fixed variables @{text "Ps"} to obtain the schematic variables @{text "?Ps"} 

   460   (Line 16).

   460   (Line 16).

   461 

   461 

   597   first two) and assumptions from the definition of the predicate (assumption

   597   first two) and assumptions from the definition of the predicate (assumption

   598   three to six). We need to treat these parameters and assumptions

   598   three to six). We need to treat these parameters and assumptions

   599   differently. In the code below we will therefore separate them into @{text

   599   differently. In the code below we will therefore separate them into @{text

   600   "params1"} and @{text params2}, respectively @{text "prems1"} and @{text

   600   "params1"} and @{text params2}, respectively @{text "prems1"} and @{text

   601   "prems2"}. To do this separation, it is best to open a subproof with the

   601   "prems2"}. To do this separation, it is best to open a subproof with the

   603   list of @{ML_type cterm}s) and the assumptions (as list of @{ML_type thm}s). 

   603   list of @{ML_type cterm}s) and the assumptions (as list of @{ML_type thm}s). 

   604   The problem with @{ML SUBPROOF}, however, is that it always expects us to 

   604   The problem with @{ML SUBPROOF}, however, is that it always expects us to 

   605   completely discharge the goal (see Section~\ref{sec:simpletacs}). This is 

   605   completely discharge the goal (see Section~\ref{sec:simpletacs}). This is 

   606   a bit inconvenient for our gradual explanation of the proof here. Therefore

   606   a bit inconvenient for our gradual explanation of the proof here. Therefore

   607   we use first the function @{ML_ind  FOCUS in Subgoal}, which does s

   607   we use first the function @{ML_ind  FOCUS in Subgoal}, which does s

   636   First we calculate the values for @{text "params1/2"} and @{text "prems1/2"}

   636   First we calculate the values for @{text "params1/2"} and @{text "prems1/2"}

   637   from @{text "params"} and @{text "prems"}, respectively. To better see what is

   637   from @{text "params"} and @{text "prems"}, respectively. To better see what is

   638   going in our example, we will print out these values using the printing

   638   going in our example, we will print out these values using the printing

   639   function in Figure~\ref{fig:chopprint}. Since @{ML FOCUS in Subgoal} will

   639   function in Figure~\ref{fig:chopprint}. Since @{ML FOCUS in Subgoal} will

   640   supply us the @{text "params"} and @{text "prems"} as lists, we can 

   640   supply us the @{text "params"} and @{text "prems"} as lists, we can 

   642 *}

   642 *}

   643 

   643 

   644 ML %linenosgray{*fun chop_test_tac preds rules =

   644 ML %linenosgray{*fun chop_test_tac preds rules =

   645   Subgoal.FOCUS (fn {params, prems, context, ...} =>

   645   Subgoal.FOCUS (fn {params, prems, context, ...} =>

   646   let

   646   let

   867 

   867 

   868 text {*

   868 text {*

   869   In Line 4 we use the @{text prems} from the @{ML SUBPROOF} and resolve 

   869   In Line 4 we use the @{text prems} from the @{ML SUBPROOF} and resolve 

   870   them with @{text prem}. In the simple cases, that is where the @{text prem} 

   870   them with @{text prem}. In the simple cases, that is where the @{text prem} 

   871   comes from a non-recursive premise of the rule, @{text prems} will be 

   871   comes from a non-recursive premise of the rule, @{text prems} will be 

   873   cases where the recursive premises of the rule do not have preconditions. 

   873   cases where the recursive premises of the rule do not have preconditions. 

   874   In case there are preconditions, then Line 4 discharges them. After

   874   In case there are preconditions, then Line 4 discharges them. After

   875   that we can proceed as before, i.e., check whether the outermost

   875   that we can proceed as before, i.e., check whether the outermost

   876   connective is @{text "\<forall>"}.

   876   connective is @{text "\<forall>"}.

   877   

   877   

   946 in

   946 in

   947   map_index intros_aux rules

   947   map_index intros_aux rules

   948 end*}

   948 end*}

   949 

   949 

   950 text {*

   950 text {*

   952   need the introduction rule together with its number (counted from

   952   need the introduction rule together with its number (counted from

   953   @{text 0}). This completes the code for the functions deriving the

   953   @{text 0}). This completes the code for the functions deriving the

   954   reasoning infrastructure. It remains to implement some administrative

   954   reasoning infrastructure. It remains to implement some administrative

   955   code that strings everything together.

   955   code that strings everything together.

   956 *}

   956 *}