--- 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 \<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
@@ -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] "\<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:
@@ -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 {*