diff -r aec7073d4645 -r daf404920ab9 ProgTutorial/Package/Ind_Code.thy --- a/ProgTutorial/Package/Ind_Code.thy Fri Jun 03 15:15:17 2016 +0100 +++ b/ProgTutorial/Package/Ind_Code.thy Tue May 14 11:10:53 2019 +0200 @@ -27,7 +27,7 @@ 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') @@ -35,7 +35,7 @@ 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. @@ -136,8 +136,7 @@ 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 thy) rules + val orules = map (Object_Logic.atomize_term lthy) rules val defs = map (defn_aux lthy orules preds) (preds ~~ arg_typss) in fold_map make_defn (prednames ~~ mxs ~~ defs) lthy @@ -215,20 +214,20 @@ 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 = - EVERY' (map (dtac o inst_spec) ctrms)*} +ML %grayML{*fun inst_spec_tac ctxt 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 @@ -239,7 +238,7 @@ fixes P::"nat \ nat \ nat \ bool" shows "\x y z. P x y z \ 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 @@ -257,8 +256,8 @@ EVERY1 [Object_Logic.full_atomize_tac ctxt, cut_facts_tac prem, rewrite_goal_tac ctxt defs, - inst_spec_tac insts, - assume_tac]*} + inst_spec_tac ctxt insts, + assume_tac ctxt]*} text {* We have to give it as arguments the definitions, the premise (a list of @@ -405,11 +404,9 @@ 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 @@ -422,16 +419,14 @@ 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 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 + the new local theory @{text "lthy'"}. In Line 6, 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_ind subst_free in Term}. Line 14 and 15 just iterate + certify them (Line 7 and 8). We can now produce the substituted introduction rules + (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 *} @@ -542,7 +537,7 @@ 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} @@ -679,7 +674,7 @@ @{term [display] "\a b t. a \ b \ fresh a t \ 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: @@ -692,7 +687,7 @@ 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 {* @@ -744,12 +739,12 @@ we can implement the following function *} -ML %grayML{*fun prepare_prem params2 prems2 prem = - rtac (case prop_of prem of +ML %grayML{*fun prepare_prem ctxt params2 prems2 prem = + 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 @@ -765,8 +760,8 @@ 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 - THEN EVERY1 (map (prepare_prem params2 prems2) prems1) + resolve_tac context [Object_Logic.rulify context (all_elims params1 (nth prems2 i))] 1 + THEN EVERY1 (map (prepare_prem context params2 prems2) prems1) end) *} text {* @@ -835,11 +830,11 @@ 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 {* @@ -864,7 +859,7 @@ 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) *} @@ -887,7 +882,7 @@ 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 {*