dropped Instance.instantiate
authorhaftmann
Fri Dec 07 15:07:54 2007 +0100 (2007-12-07)
changeset 25569c597835d5de4
parent 25568 7bb10db582cf
child 25570 fdfbbb92dadf
dropped Instance.instantiate
src/HOL/Library/Eval.thy
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/function_package/size.ML
src/HOL/Tools/typecopy_package.ML
src/Pure/Isar/instance.ML
     1.1 --- a/src/HOL/Library/Eval.thy	Fri Dec 07 10:59:03 2007 +0100
     1.2 +++ b/src/HOL/Library/Eval.thy	Fri Dec 07 15:07:54 2007 +0100
     1.3 @@ -40,8 +40,12 @@
     1.4        val ty = Type (tyco, map TFree (Name.names Name.context "'a" sorts));
     1.5      in
     1.6        thy
     1.7 -      |> Instance.instantiate ([tyco], sorts, @{sort typ_of})
     1.8 -           (define_typ_of ty) ((K o K) (Class.intro_classes_tac []))
     1.9 +      |> TheoryTarget.instantiation ([tyco], sorts, @{sort typ_of})
    1.10 +      |> define_typ_of ty
    1.11 +      |> snd
    1.12 +      |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
    1.13 +      |> LocalTheory.exit
    1.14 +      |> ProofContext.theory_of
    1.15      end;
    1.16  in TypedefPackage.interpretation interpretator end
    1.17  *}
    1.18 @@ -158,8 +162,12 @@
    1.19    fun interpretator tycos thy = case prep thy tycos
    1.20     of SOME (sorts, defs) =>
    1.21        thy
    1.22 -      |> Instance.instantiate (tycos, sorts, @{sort term_of})
    1.23 -           (primrec defs) ((K o K) (Class.intro_classes_tac []))
    1.24 +      |> TheoryTarget.instantiation (tycos, sorts, @{sort term_of})
    1.25 +      |> primrec defs
    1.26 +      |> snd
    1.27 +      |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
    1.28 +      |> LocalTheory.exit
    1.29 +      |> ProofContext.theory_of
    1.30      | NONE => thy;
    1.31    in DatatypePackage.interpretation interpretator end
    1.32  *}
    1.33 @@ -185,13 +193,20 @@
    1.34  by pat_completeness auto
    1.35  termination by (relation "measure (nat o abs)") (auto simp add: divAlg_mod_div)
    1.36  
    1.37 -instance int :: term_of
    1.38 -  "term_of k \<equiv> STR ''Numeral.number_class.number_of'' \<Colon>\<subseteq> intT \<rightarrow> intT \<bullet> mk_int k" ..
    1.39 +instantiation int :: term_of
    1.40 +begin
    1.41 +
    1.42 +definition
    1.43 +  "term_of k = STR ''Numeral.number_class.number_of'' \<Colon>\<subseteq> intT \<rightarrow> intT \<bullet> mk_int k"
    1.44 +
    1.45 +instance ..
    1.46 +
    1.47 +end
    1.48  
    1.49  
    1.50  text {* Adaption for @{typ message_string}s *}
    1.51  
    1.52 -lemmas [code func del] = term_of_messagestring.simps
    1.53 +lemmas [code func del] = term_of_message_string.simps
    1.54  
    1.55  
    1.56  subsection {* Evaluation infrastructure *}
     2.1 --- a/src/HOL/Tools/datatype_codegen.ML	Fri Dec 07 10:59:03 2007 +0100
     2.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Fri Dec 07 15:07:54 2007 +0100
     2.3 @@ -435,8 +435,10 @@
     2.4        map (curry (Sorts.inter_sort (Sign.classes_of thy)) [HOLogic.class_eq] o snd) vs;
     2.5    in
     2.6      thy
     2.7 -    |> Instance.instantiate (dtcos, sorts_eq, [HOLogic.class_eq]) (pair ())
     2.8 -         ((K o K) (Class.intro_classes_tac []))
     2.9 +    |> TheoryTarget.instantiation (dtcos, sorts_eq, [HOLogic.class_eq])
    2.10 +    |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
    2.11 +    |> LocalTheory.exit
    2.12 +    |> ProofContext.theory_of
    2.13      |> fold add_eq_thms dtcos
    2.14    end;
    2.15  
     3.1 --- a/src/HOL/Tools/function_package/size.ML	Fri Dec 07 10:59:03 2007 +0100
     3.2 +++ b/src/HOL/Tools/function_package/size.ML	Fri Dec 07 15:07:54 2007 +0100
     3.3 @@ -33,9 +33,13 @@
     3.4  val size_name_base = NameSpace.base size_name;
     3.5  val size_suffix = "_" ^ size_name_base;
     3.6  
     3.7 -fun instance_size_class tyco thy = thy |> Instance.instantiate
     3.8 -  ([tyco], replicate (Sign.arity_number thy tyco) HOLogic.typeS, [HOLogic.class_size])
     3.9 -    (pair ()) ((K o K) (Class.intro_classes_tac []));
    3.10 +fun instance_size_class tyco thy =
    3.11 +  thy
    3.12 +  |> TheoryTarget.instantiation
    3.13 +       ([tyco], replicate (Sign.arity_number thy tyco) HOLogic.typeS, [HOLogic.class_size])
    3.14 +  |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
    3.15 +  |> LocalTheory.exit
    3.16 +  |> ProofContext.theory_of;
    3.17  
    3.18  fun plus (t1, t2) = Const ("HOL.plus_class.plus",
    3.19    HOLogic.natT --> HOLogic.natT --> HOLogic.natT) $ t1 $ t2;
     4.1 --- a/src/HOL/Tools/typecopy_package.ML	Fri Dec 07 10:59:03 2007 +0100
     4.2 +++ b/src/HOL/Tools/typecopy_package.ML	Fri Dec 07 15:07:54 2007 +0100
     4.3 @@ -131,8 +131,10 @@
     4.4      thy
     4.5      |> Code.add_datatype [(constr, ty)]
     4.6      |> Code.add_func proj_def
     4.7 -    |> Instance.instantiate ([tyco], sorts_eq, [HOLogic.class_eq]) (pair ())
     4.8 -         ((K o K) (Class.intro_classes_tac []))
     4.9 +    |> TheoryTarget.instantiation ([tyco], sorts_eq, [HOLogic.class_eq])
    4.10 +    |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
    4.11 +    |> LocalTheory.exit
    4.12 +    |> ProofContext.theory_of
    4.13      |> Code.add_func (CodeUnit.constrain_thm [HOLogic.class_eq] inject)
    4.14    end;
    4.15  
     5.1 --- a/src/Pure/Isar/instance.ML	Fri Dec 07 10:59:03 2007 +0100
     5.2 +++ b/src/Pure/Isar/instance.ML	Fri Dec 07 15:07:54 2007 +0100
     5.3 @@ -7,9 +7,6 @@
     5.4  
     5.5  signature INSTANCE =
     5.6  sig
     5.7 -  val instantiate: string list * sort list * sort -> (local_theory -> 'a * local_theory)
     5.8 -    -> (Proof.context -> 'a -> tactic) -> theory -> theory
     5.9 -
    5.10    val instantiation_cmd: xstring list * sort * xstring -> theory -> local_theory
    5.11    val instance_cmd: xstring * sort * xstring -> ((bstring * Attrib.src list) * xstring) list
    5.12      -> theory -> Proof.state
    5.13 @@ -29,13 +26,6 @@
    5.14  fun instantiation_cmd raw_arities thy =
    5.15    TheoryTarget.instantiation (read_multi_arity thy raw_arities) thy;
    5.16  
    5.17 -fun instantiate arities f tac =
    5.18 -  TheoryTarget.instantiation arities
    5.19 -  #> f
    5.20 -  #-> (fn result => Class.prove_instantiation_instance (fn ctxt => tac ctxt result))
    5.21 -  #> LocalTheory.exit
    5.22 -  #> ProofContext.theory_of;
    5.23 -
    5.24  fun gen_instance prep_arity prep_attr parse_term do_proof do_proof' raw_arities defs thy =
    5.25    let
    5.26      val (tyco, sorts, sort) = prep_arity thy raw_arities;
    5.27 @@ -56,6 +46,8 @@
    5.28        let
    5.29          val def' = (apsnd o apsnd) (Syntax.check_prop ctxt) def;
    5.30        in Specification.definition def' ctxt end;
    5.31 +    val _ = if not (null defs) then Output.legacy_feature
    5.32 +      "Instance command with attached attached definitions; use instantiation instead." else ();
    5.33    in if not (null defs) orelse forall (Class.is_class thy) sort
    5.34    then
    5.35      thy