
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 \<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 {*




