streamlined specification interfaces
authorhaftmann
Thu Feb 21 09:15:07 2019 +0000 (2 months ago ago)
changeset 700103bfa28b3a5b2
parent 70009 74d673b7d40e
child 70011 54d19f1f0ba6
child 70012 b35c3839d5d1
streamlined specification interfaces
NEWS
src/HOL/HOLCF/Tools/cpodef.ML
src/HOL/Import/import_rule.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Tools/Function/partial_function.ML
src/HOL/Tools/Old_Datatype/old_rep_datatype.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/record.ML
src/HOL/Tools/typedef.ML
src/Pure/Isar/class.ML
src/Pure/Isar/overloading.ML
     1.1 --- a/NEWS	Thu Feb 21 09:15:06 2019 +0000
     1.2 +++ b/NEWS	Thu Feb 21 09:15:07 2019 +0000
     1.3 @@ -104,6 +104,10 @@
     1.4  * Slightly more conventional naming schema in structure Inductive.
     1.5  Minor INCOMPATIBILITY.
     1.6  
     1.7 +* Various _global variants of specification tools have been removed.
     1.8 +Minor INCOMPATIBILITY, prefer combinators Named_Target.theory_map[_result]
     1.9 +to lift specifications to the global theory level.
    1.10 +
    1.11  * Code generation: command 'export_code' without file keyword exports
    1.12  code as regular theory export, which can be materialized using the
    1.13  command-line tools "isabelle export" or "isabelle build -e" (with
     2.1 --- a/src/HOL/HOLCF/Tools/cpodef.ML	Thu Feb 21 09:15:06 2019 +0000
     2.2 +++ b/src/HOL/HOLCF/Tools/cpodef.ML	Thu Feb 21 09:15:07 2019 +0000
     2.3 @@ -164,8 +164,10 @@
     2.4  fun add_podef typ set opt_bindings tac thy =
     2.5    let
     2.6      val name = #1 typ
     2.7 -    val ((full_tname, info as ({Rep_name, ...}, {type_definition, ...})), thy) = thy
     2.8 -      |> Typedef.add_typedef_global {overloaded = false} typ set opt_bindings tac
     2.9 +    val ((full_tname, info as ({Rep_name, ...}, {type_definition, ...})), thy) =
    2.10 +      thy
    2.11 +      |> Named_Target.theory_map_result (apsnd o Typedef.transform_info)
    2.12 +           (Typedef.add_typedef {overloaded = false} typ set opt_bindings tac)
    2.13      val oldT = #rep_type (#1 info)
    2.14      val newT = #abs_type (#1 info)
    2.15      val lhs_tfrees = map dest_TFree (snd (dest_Type newT))
     3.1 --- a/src/HOL/Import/import_rule.ML	Thu Feb 21 09:15:06 2019 +0000
     3.2 +++ b/src/HOL/Import/import_rule.ML	Thu Feb 21 09:15:07 2019 +0000
     3.3 @@ -223,9 +223,10 @@
     3.4        Abs_name = Binding.name abs_name,
     3.5        type_definition_name = Binding.name ("type_definition_" ^ tycname)}
     3.6      val ((_, typedef_info), thy') =
     3.7 -     Typedef.add_typedef_global {overloaded = false}
     3.8 +     Named_Target.theory_map_result (apsnd o Typedef.transform_info)
     3.9 +     (Typedef.add_typedef {overloaded = false}
    3.10         (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c
    3.11 -       (SOME typedef_bindings) (fn ctxt => resolve_tac ctxt [th2] 1) thy
    3.12 +       (SOME typedef_bindings) (fn ctxt => resolve_tac ctxt [th2] 1)) thy
    3.13      val aty = #abs_type (#1 typedef_info)
    3.14      val th = freezeT thy' (#type_definition (#2 typedef_info))
    3.15      val (th_s, _) = Thm.dest_comb (Thm.dest_arg (Thm.cprop_of th))
     4.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Thu Feb 21 09:15:06 2019 +0000
     4.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Thu Feb 21 09:15:07 2019 +0000
     4.3 @@ -535,12 +535,13 @@
     4.4      val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy4) =
     4.5        thy3
     4.6        |> Sign.concealed
     4.7 -      |> Inductive.add_inductive_global
     4.8 +      |> Named_Target.theory_map_result Inductive.transform_result
     4.9 +         (Inductive.add_inductive
    4.10            {quiet_mode = false, verbose = false, alt_name = Binding.name big_rep_name,
    4.11             coind = false, no_elim = true, no_ind = false, skip_mono = true}
    4.12            (map (fn (s, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn))
    4.13               (rep_set_names' ~~ recTs'))
    4.14 -          [] (map (fn x => (Binding.empty_atts, x)) intr_ts) []
    4.15 +          [] (map (fn x => (Binding.empty_atts, x)) intr_ts) [])
    4.16        ||> Sign.restore_naming thy3;
    4.17  
    4.18      (**** Prove that representing set is closed under permutation ****)
    4.19 @@ -582,7 +583,8 @@
    4.20      val (typedefs, thy6) =
    4.21        thy4
    4.22        |> fold_map (fn (((name, mx), tvs), (cname, U)) => fn thy =>
    4.23 -          Typedef.add_typedef_global {overloaded = false}
    4.24 +          Named_Target.theory_map_result (apsnd o Typedef.transform_info)
    4.25 +          (Typedef.add_typedef {overloaded = false}
    4.26              (name, map (fn (v, _) => (v, dummyS)) tvs, mx)  (* FIXME keep constraints!? *)
    4.27              (Const (\<^const_name>\<open>Collect\<close>, (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $
    4.28                 Const (cname, U --> HOLogic.boolT)) NONE
    4.29 @@ -590,7 +592,7 @@
    4.30                resolve_tac ctxt [exI] 1 THEN
    4.31                resolve_tac ctxt [CollectI] 1 THEN
    4.32                QUIET_BREADTH_FIRST (has_fewer_prems 1)
    4.33 -              (resolve_tac ctxt rep_intrs 1)) thy |> (fn ((_, r), thy) =>
    4.34 +              (resolve_tac ctxt rep_intrs 1))) thy |> (fn ((_, r), thy) =>
    4.35          let
    4.36            val permT = mk_permT
    4.37              (TFree (singleton (Name.variant_list (map fst tvs)) "'a", \<^sort>\<open>type\<close>));
    4.38 @@ -1523,12 +1525,12 @@
    4.39      val ({intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}, thy11) =
    4.40        thy10
    4.41        |> Sign.concealed
    4.42 -      |> Inductive.add_inductive_global
    4.43 -          {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name,
    4.44 +      |> Named_Target.theory_map_result Inductive.transform_result
    4.45 +          (Inductive.add_inductive {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name,
    4.46             coind = false, no_elim = false, no_ind = false, skip_mono = true}
    4.47            (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
    4.48            (map dest_Free rec_fns)
    4.49 -          (map (fn x => (Binding.empty_atts, x)) rec_intr_ts) []
    4.50 +          (map (fn x => (Binding.empty_atts, x)) rec_intr_ts) [])
    4.51        ||> Global_Theory.hide_fact true (Long_Name.append (Sign.full_bname thy10 big_rec_name) "induct")
    4.52        ||> Sign.restore_naming thy10;
    4.53  
     5.1 --- a/src/HOL/Tools/Function/partial_function.ML	Thu Feb 21 09:15:06 2019 +0000
     5.2 +++ b/src/HOL/Tools/Function/partial_function.ML	Thu Feb 21 09:15:07 2019 +0000
     5.3 @@ -12,6 +12,7 @@
     5.4      Attrib.binding * term -> local_theory -> (term * thm) * local_theory
     5.5    val add_partial_function_cmd: string -> (binding * string option * mixfix) list ->
     5.6      Attrib.binding * string -> local_theory -> (term * thm) * local_theory
     5.7 +  val transform_result: morphism -> term * thm -> term * thm
     5.8  end;
     5.9  
    5.10  structure Partial_Function: PARTIAL_FUNCTION =
    5.11 @@ -219,6 +220,8 @@
    5.12  
    5.13  (*** partial_function definition ***)
    5.14  
    5.15 +fun transform_result phi (t, thm) = (Morphism.term phi t, Morphism.thm phi thm);
    5.16 +
    5.17  fun gen_add_partial_function prep mode fixes_raw eqn_raw lthy =
    5.18    let
    5.19      val setup_data = the (lookup_mode lthy mode)
     6.1 --- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Thu Feb 21 09:15:06 2019 +0000
     6.2 +++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Thu Feb 21 09:15:07 2019 +0000
     6.3 @@ -150,12 +150,13 @@
     6.4      val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
     6.5        thy0
     6.6        |> Sign.concealed
     6.7 -      |> Inductive.add_inductive_global
     6.8 +      |> Named_Target.theory_map_result Inductive.transform_result
     6.9 +          (Inductive.add_inductive
    6.10            {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name',
    6.11              coind = false, no_elim = false, no_ind = true, skip_mono = true}
    6.12            (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
    6.13            (map dest_Free rec_fns)
    6.14 -          (map (fn x => (Binding.empty_atts, x)) rec_intr_ts) []
    6.15 +          (map (fn x => (Binding.empty_atts, x)) rec_intr_ts) [])
    6.16        ||> Sign.restore_naming thy0;
    6.17  
    6.18      (* prove uniqueness and termination of primrec combinators *)
     7.1 --- a/src/HOL/Tools/inductive.ML	Thu Feb 21 09:15:06 2019 +0000
     7.2 +++ b/src/HOL/Tools/inductive.ML	Thu Feb 21 09:15:07 2019 +0000
     7.3 @@ -52,10 +52,6 @@
     7.4      flags -> ((binding * typ) * mixfix) list ->
     7.5      (string * typ) list -> (Attrib.binding * term) list -> thm list -> local_theory ->
     7.6      result * local_theory
     7.7 -  val add_inductive_global:
     7.8 -    flags -> ((binding * typ) * mixfix) list ->
     7.9 -    (string * typ) list -> (Attrib.binding * term) list -> thm list -> theory ->
    7.10 -    result * theory
    7.11    val add_inductive_cmd: bool -> bool ->
    7.12      (binding * string option * mixfix) list ->
    7.13      (binding * string option * mixfix) list ->
    7.14 @@ -1226,16 +1222,6 @@
    7.15  val add_inductive = gen_add_inductive add_ind_def;
    7.16  val add_inductive_cmd = gen_add_inductive_cmd add_ind_def;
    7.17  
    7.18 -fun add_inductive_global flags cnames_syn pnames pre_intros monos thy =
    7.19 -  let
    7.20 -    val name = Sign.full_name thy (fst (fst (hd cnames_syn)));
    7.21 -    val ctxt' = thy
    7.22 -      |> Named_Target.theory_init
    7.23 -      |> add_inductive flags cnames_syn pnames pre_intros monos |> snd
    7.24 -      |> Local_Theory.exit;
    7.25 -    val info = #2 (the_inductive_global ctxt' name);
    7.26 -  in (info, Proof_Context.theory_of ctxt') end;
    7.27 -
    7.28  
    7.29  (* read off arities of inductive predicates from raw induction rule *)
    7.30  fun arities_of induct =
     8.1 --- a/src/HOL/Tools/inductive_realizer.ML	Thu Feb 21 09:15:06 2019 +0000
     8.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Thu Feb 21 09:15:07 2019 +0000
     8.3 @@ -352,13 +352,14 @@
     8.4      (** realizability predicate **)
     8.5  
     8.6      val (ind_info, thy3') = thy2 |>
     8.7 -      Inductive.add_inductive_global
     8.8 +      Named_Target.theory_map_result Inductive.transform_result
     8.9 +      (Inductive.add_inductive
    8.10          {quiet_mode = false, verbose = false, alt_name = Binding.empty, coind = false,
    8.11            no_elim = false, no_ind = false, skip_mono = false}
    8.12          rlzpreds rlzparams (map (fn (rintr, intr) =>
    8.13            ((Binding.name (Long_Name.base_name (name_of_thm intr)), []),
    8.14             subst_atomic rlzpreds' (Logic.unvarify_global rintr)))
    8.15 -             (rintrs ~~ maps snd rss)) [] ||>
    8.16 +             (rintrs ~~ maps snd rss)) []) ||>
    8.17        Sign.root_path;
    8.18      val thy3 = fold (Global_Theory.hide_fact false o name_of_thm) (#intrs ind_info) thy3';
    8.19  
     9.1 --- a/src/HOL/Tools/record.ML	Thu Feb 21 09:15:06 2019 +0000
     9.2 +++ b/src/HOL/Tools/record.ML	Thu Feb 21 09:15:07 2019 +0000
     9.3 @@ -102,8 +102,9 @@
     9.4      val vs = map (Proof_Context.check_tfree ctxt) raw_vs;
     9.5    in
     9.6      thy
     9.7 -    |> Typedef.add_typedef_global overloaded (raw_tyco, vs, NoSyn)
     9.8 -        (HOLogic.mk_UNIV repT) NONE (fn ctxt' => resolve_tac ctxt' [UNIV_witness] 1)
     9.9 +    |> Named_Target.theory_map_result (apsnd o Typedef.transform_info)
    9.10 +        (Typedef.add_typedef overloaded (raw_tyco, vs, NoSyn)
    9.11 +          (HOLogic.mk_UNIV repT) NONE (fn ctxt' => resolve_tac ctxt' [UNIV_witness] 1))
    9.12      |-> (fn (tyco, info) => get_typedef_info tyco vs info)
    9.13    end;
    9.14  
    10.1 --- a/src/HOL/Tools/typedef.ML	Thu Feb 21 09:15:06 2019 +0000
    10.2 +++ b/src/HOL/Tools/typedef.ML	Thu Feb 21 09:15:07 2019 +0000
    10.3 @@ -307,9 +307,8 @@
    10.4    in typedef_result inhabited lthy' end;
    10.5  
    10.6  fun add_typedef_global overloaded typ set opt_bindings tac =
    10.7 -  Named_Target.theory_init
    10.8 -  #> add_typedef overloaded typ set opt_bindings tac
    10.9 -  #> Local_Theory.exit_result_global (apsnd o transform_info);
   10.10 +  Named_Target.theory_map_result (apsnd o transform_info)
   10.11 +    (add_typedef overloaded typ set opt_bindings tac)
   10.12  
   10.13  
   10.14  (* typedef: proof interface *)
    11.1 --- a/src/Pure/Isar/class.ML	Thu Feb 21 09:15:06 2019 +0000
    11.2 +++ b/src/Pure/Isar/class.ML	Thu Feb 21 09:15:07 2019 +0000
    11.3 @@ -39,6 +39,9 @@
    11.4      -> string list * (string * sort) list * sort
    11.5    val instantiation_cmd: xstring list * xstring list * xstring -> theory -> local_theory
    11.6    val instance_arity_cmd: xstring list * xstring list * xstring -> theory -> Proof.state
    11.7 +  val theory_map_result: string list * (string * sort) list * sort
    11.8 +    -> (morphism -> 'a -> 'b) -> (local_theory -> 'a * local_theory)
    11.9 +    -> (Proof.context -> 'b -> tactic) -> theory -> 'b * theory
   11.10  
   11.11    (*subclasses*)
   11.12    val classrel: class * class -> theory -> Proof.state
   11.13 @@ -749,6 +752,11 @@
   11.14      |> pair y
   11.15    end;
   11.16  
   11.17 +fun theory_map_result arities f g tac =
   11.18 +  instantiation arities
   11.19 +  #> g
   11.20 +  #-> prove_instantiation_exit_result f tac;
   11.21 +
   11.22  
   11.23  (* simplified instantiation interface with no class parameter *)
   11.24  
    12.1 --- a/src/Pure/Isar/overloading.ML	Thu Feb 21 09:15:06 2019 +0000
    12.2 +++ b/src/Pure/Isar/overloading.ML	Thu Feb 21 09:15:07 2019 +0000
    12.3 @@ -15,6 +15,11 @@
    12.4  
    12.5    val overloading: (string * (string * typ) * bool) list -> theory -> local_theory
    12.6    val overloading_cmd: (string * string * bool) list -> theory -> local_theory
    12.7 +  val theory_map: (string * (string * typ) * bool) list
    12.8 +    -> (local_theory -> local_theory) -> theory -> theory
    12.9 +  val theory_map_result: (string * (string * typ) * bool) list
   12.10 +    -> (morphism -> 'a -> 'b) -> (local_theory -> 'a * local_theory)
   12.11 +    -> theory -> 'b * theory
   12.12  end;
   12.13  
   12.14  structure Overloading: OVERLOADING =
   12.15 @@ -185,19 +190,19 @@
   12.16            commas_quote (map (Syntax.string_of_term lthy o Const o fst) overloading));
   12.17    in lthy end;
   12.18  
   12.19 -fun gen_overloading prep_const raw_overloading thy =
   12.20 +fun gen_overloading prep_const raw_overloading_spec thy =
   12.21    let
   12.22      val ctxt = Proof_Context.init_global thy;
   12.23 -    val _ = if null raw_overloading then error "At least one parameter must be given" else ();
   12.24 -    val overloading = raw_overloading |> map (fn (v, const, checked) =>
   12.25 +    val _ = if null raw_overloading_spec then error "At least one parameter must be given" else ();
   12.26 +    val overloading_spec = raw_overloading_spec |> map (fn (v, const, checked) =>
   12.27        (Term.dest_Const (prep_const ctxt const), (v, checked)));
   12.28    in
   12.29      thy
   12.30      |> Generic_Target.init
   12.31         {background_naming = Sign.naming_of thy,
   12.32          setup = Proof_Context.init_global
   12.33 -          #> Data.put overloading
   12.34 -          #> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
   12.35 +          #> Data.put overloading_spec
   12.36 +          #> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading_spec
   12.37            #> activate_improvable_syntax
   12.38            #> synchronize_syntax,
   12.39          conclude = conclude}
   12.40 @@ -213,4 +218,9 @@
   12.41  val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const);
   12.42  val overloading_cmd = gen_overloading Syntax.read_term;
   12.43  
   12.44 +fun theory_map overloading_spec g =
   12.45 +  overloading overloading_spec #> g #> Local_Theory.exit_global;
   12.46 +fun theory_map_result overloading_spec f g =
   12.47 +  overloading overloading_spec #> g #> Local_Theory.exit_result_global f;
   12.48 +
   12.49  end;