isabelle-cookbook: comparison ProgTutorial/Package/Ind

equal deleted inserted replaced

-:aec7073d4645
+:daf404920ab9
 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 arg = ((predname, mx), (Binding.empty_atts, trm))
 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. We use @{ML_ind empty_binding in Attrib} in Line 3,
+definition has been made. We use @{ML_ind empty_atts in Binding} 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.
 The next two functions construct the right-hand sides of the definitions,
 which are terms whose general form is:
 @{text "arg_tyss"} is the list of argument-type-lists.
 *}
 ML %linenosgray{*fun defns rules preds prednames mxs arg_typss lthy =
 let
-val thy = Proof_Context.theory_of lthy
+val orules = map (Object_Logic.atomize_term lthy) rules
-val orules = map (Object_Logic.atomize_term thy) rules
 val defs = map (defn_aux lthy orules preds) (preds ~~ arg_typss)
 in
 fold_map make_defn (prednames ~~ mxs ~~ defs) lthy
 end*}
 quantifiers.
 *}
 ML %grayML{*fun inst_spec ctrm =
 let
-val cty = ctyp_of_term ctrm
+val cty = Thm.ctyp_of_cterm ctrm
 in
-Drule.instantiate' [SOME cty] [NONE, SOME ctrm] @{thm spec}
+Thm.instantiate' [SOME cty] [NONE, SOME ctrm] @{thm spec}
 end*}
 text {*
-This helper function uses the function @{ML_ind instantiate' in Drule}
+This helper function uses the function @{ML_ind instantiate' in Thm}
 and instantiates the @{text "?x"} in the theorem @{thm spec} with a given
 @{ML_type cterm}. We call this helper function in the following
 tactic.\label{fun:instspectac}.
 *}
-ML %grayML{*fun inst_spec_tac ctrms =
+ML %grayML{*fun inst_spec_tac ctxt ctrms =
-EVERY' (map (dtac o inst_spec) ctrms)*}
+EVERY' (map (dresolve_tac ctxt o single o inst_spec) ctrms)*}
 text {*
 This tactic expects a list of @{ML_type cterm}s. It allows us in the
 proof below to instantiate the three quantifiers in the assumption.
 *}
 lemma
 fixes P::"nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool"
 shows "\<forall>x y z. P x y z \<Longrightarrow> True"
 apply (tactic {*
-inst_spec_tac [@{cterm "a::nat"},@{cterm "b::nat"},@{cterm "c::nat"}] 1 *})
+inst_spec_tac @{context} [@{cterm "a::nat"},@{cterm "b::nat"},@{cterm "c::nat"}] 1 *})
 txt {*
 We obtain the goal state
 \begin{minipage}{\textwidth}
 @{subgoals}
 ML %linenosgray{*fun ind_tac ctxt defs prem insts =
 EVERY1 [Object_Logic.full_atomize_tac ctxt,
 cut_facts_tac prem,
 rewrite_goal_tac ctxt defs,
-inst_spec_tac insts,
+inst_spec_tac ctxt insts,
-assume_tac]*}
+assume_tac ctxt]*}
 text {*
 We have to give it as arguments the definitions, the premise (a list of
 formulae) and the instantiations. The premise is @{text "even n"} in lemma
 @{thm [source] manual_ind_prin_even} shown above; in our code it will always be a list
 ML %linenosgray{*fun inds rules defs preds arg_tyss lthy  =
 let
 val Ps = replicate (length preds) "P"
 val (newprednames, lthy') = Variable.variant_fixes Ps lthy
-val thy = Proof_Context.theory_of lthy'
 val tyss' = map (fn tys => tys ---> HOLogic.boolT) arg_tyss
 val newpreds = map Free (newprednames ~~ tyss')
-val cnewpreds = map (cterm_of thy) newpreds
+val cnewpreds = map (Thm.cterm_of lthy') newpreds
 val srules = map (subst_free (preds ~~ newpreds)) rules
 in
 map (prove_ind lthy' defs srules cnewpreds)
 (preds ~~ newpreds ~~ arg_tyss)
 text {*
 In Line 3, we generate a string @{text [quotes] "P"} for each predicate.
 In Line 4, we use the same trick as in the previous function, that is making the
 @{text "Ps"} fresh and declaring them as free, but fixed, in
-the new local theory @{text "lthy'"}. From the local theory we extract
+the new local theory @{text "lthy'"}. In Line 6, we construct the types of these new predicates
-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
+certify them (Line 7 and 8). We can now produce the substituted introduction rules
-(Line 11) using the function @{ML_ind subst_free in Term}. Line 14 and 15 just iterate
+(Line 9) using the function @{ML_ind subst_free in Term}. Line 12 and 13 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).
+(Line 14).
 A testcase for this function is
 *}
 local_setup %gray {* fn lthy =>
 *}
 ML %linenosgray{*fun expand_tac ctxt defs =
 Object_Logic.rulify_tac ctxt 1
 THEN rewrite_goal_tac ctxt defs 1
-THEN (REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1)) *}
+THEN (REPEAT (resolve_tac ctxt [@{thm allI}, @{thm impI}] 1)) *}
 text {*
 The function in Line 2 ``rulifies'' the lemma.\footnote{FIXME: explain this better}
 This will turn out to
 be important later on. Applying this tactic in our proof of @{text "fresh_Lem"}
 We now have to select from @{text prems2} the premise
 that corresponds to the introduction rule we prove, namely:
 @{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
+To use this premise with @{ML resolve_tac}, we need to instantiate its
 quantifiers (with @{text params1}) and transform it into rule
 format (using @{ML_ind  rulify in Object_Logic}). So we can modify the
 code as follows:
 *}
 let
 val cparams = map snd params
 val (params1, params2) = chop (length cparams - length preds) cparams
 val (prems1, prems2) = chop (length prems - length rules) prems
 in
-rtac (Object_Logic.rulify context (all_elims params1 (nth prems2 i))) 1
+resolve_tac  context [Object_Logic.rulify context (all_elims params1 (nth prems2 i))] 1
 end) *}
 text {*
 The argument @{text i} corresponds to the number of the
 introduction we want to prove. We will later on let it range
 The premise of the complicated case must have at least one  @{text "\<forall>"}
 coming from the quantification over the @{text preds}. So
 we can implement the following function
 *}
-ML %grayML{*fun prepare_prem params2 prems2 prem =
+ML %grayML{*fun prepare_prem ctxt params2 prems2 prem =
-rtac (case prop_of prem of
+resolve_tac ctxt [case Thm.prop_of prem of
 _ $ (Const (@{const_name All}, _) $ _) =>
 prem |> all_elims params2
 |> imp_elims prems2
-| _ => prem) *}
+| _ => prem] *}
 text {*
 which either applies the premise outright (the default case) or if
 it has an outermost universial quantification, instantiates it first
 with  @{text "params1"} and then @{text "prems1"}. The following
 let
 val cparams = map snd params
 val (params1, params2) = chop (length cparams - length preds) cparams
 val (prems1, prems2) = chop (length prems - length rules) prems
 in
-rtac (Object_Logic.rulify context (all_elims params1 (nth prems2 i))) 1
+resolve_tac context [Object_Logic.rulify context (all_elims params1 (nth prems2 i))] 1
-THEN EVERY1 (map (prepare_prem params2 prems2) prems1)
+THEN EVERY1 (map (prepare_prem context params2 prems2) prems1)
 end) *}
 text {*
 Note that the tactic is now @{ML SUBPROOF}, not @{ML FOCUS in Subgoal} anymore.
 The full proof of the introduction rule is as follows:
 ML %linenosgray{*fun prepare_prem params2 prems2 ctxt prem =
 SUBPROOF (fn {prems, ...} =>
 let
 val prem' = prems MRS prem
 in
-rtac (case prop_of prem' of
+resolve_tac ctxt [case Thm.prop_of prem' of
 _ $ (Const (@{const_name All}, _) $ _) =>
 prem' |> all_elims params2
 |> imp_elims prems2
-| _ => prem') 1
+| _ => prem'] 1
 end) ctxt *}
 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}
 let
 val cparams = map snd params
 val (params1, params2) = chop (length cparams - length preds) cparams
 val (prems1, prems2) = chop (length prems - length rules) prems
 in
-rtac (Object_Logic.rulify context (all_elims params1 (nth prems2 i))) 1
+resolve_tac context [Object_Logic.rulify context (all_elims params1 (nth prems2 i))] 1
 THEN EVERY1 (map (prepare_prem params2 prems2 context) prems1)
 end) *}
 text {*
 With these two functions we can now also prove the introduction
 *}
 ML %linenosgray{*fun intro_tac defs rules preds i ctxt =
 EVERY1 [Object_Logic.rulify_tac ctxt,
 rewrite_goal_tac ctxt defs,
-REPEAT o (resolve_tac [@{thm allI}, @{thm impI}]),
+REPEAT o (resolve_tac ctxt [@{thm allI}, @{thm impI}]),
 prove_intro_tac i preds rules ctxt]*}
 text {*
 Lines 2 to 4 in this tactic correspond to the function @{ML expand_tac}.
 Some testcases for this tactic are:

changeset 562	daf404920ab9
parent 552	82c482467d75
child 565	cecd7a941885