--- a/NEWS Sat Mar 28 21:32:48 2015 +0100
+++ b/NEWS Sun Mar 29 22:38:18 2015 +0200
@@ -61,15 +61,19 @@
*** Pure ***
-* Proof methods with explicit instantiation ("rule_tac", "subgoal_tac"
-etc.) allow an optional context of local variables ('for' declaration):
-these variables become schematic in the instantiated theorem. This
-behaviour is analogous to 'for' in attributes "where" and "of".
-
* Explicit instantiation via attributes "where", "of", and proof methods
"rule_tac" with derivatives like "subgoal_tac" etc. admit dummy patterns
("_") that stand for anonymous local variables.
+* Proof methods with explicit instantiation ("rule_tac", "subgoal_tac"
+etc.) allow an optional context of local variables ('for' declaration):
+these variables become schematic in the instantiated theorem; this
+behaviour is analogous to 'for' in attributes "where" and "of".
+Configuration option rule_insts_schematic (default false) controls use
+of schematic variables outside the context. Minor INCOMPATIBILITY,
+declare rule_insts_schematic = true temporarily and update to use local
+variable declarations or dummy patterns instead.
+
* Configuration option "rule_insts_schematic" determines whether proof
methods like "rule_tac" may refer to undeclared schematic variables
implicitly, instead of using proper 'for' declarations. This historic
--- a/src/Doc/Isar_Ref/HOL_Specific.thy Sat Mar 28 21:32:48 2015 +0100
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Sun Mar 29 22:38:18 2015 +0200
@@ -2338,7 +2338,7 @@
;
@@{method (HOL) induct_tac} @{syntax goal_spec}? (@{syntax insts} * @'and') rule?
;
- @@{method (HOL) ind_cases} (@{syntax prop}+) (@'for' (@{syntax name}+))?
+ @@{method (HOL) ind_cases} (@{syntax prop}+) @{syntax for_fixes}
;
@@{command (HOL) inductive_cases} (@{syntax thmdecl}? (@{syntax prop}+) + @'and')
;
--- a/src/HOL/Codegenerator_Test/Candidates.thy Sat Mar 28 21:32:48 2015 +0100
+++ b/src/HOL/Codegenerator_Test/Candidates.thy Sun Mar 29 22:38:18 2015 +0200
@@ -13,11 +13,12 @@
begin
setup \<open>
+fn thy =>
let
- val tycos = (#log_types o Type.rep_tsig o Sign.tsig_of) @{theory};
- val consts = map_filter (try (curry (Axclass.param_of_inst @{theory})
+ val tycos = Sign.logical_types thy;
+ val consts = map_filter (try (curry (Axclass.param_of_inst thy)
@{const_name "Quickcheck_Narrowing.partial_term_of"})) tycos;
-in fold Code.del_eqns consts end
+in fold Code.del_eqns consts thy end
\<close> -- \<open>drop technical stuff from @{text Quickcheck_Narrowing} which is tailored towards Haskell\<close>
inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
--- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy Sat Mar 28 21:32:48 2015 +0100
+++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy Sun Mar 29 22:38:18 2015 +0200
@@ -12,11 +12,12 @@
begin
setup \<open>
+fn thy =>
let
- val tycos = (#log_types o Type.rep_tsig o Sign.tsig_of) @{theory};
- val consts = map_filter (try (curry (Axclass.param_of_inst @{theory})
+ val tycos = Sign.logical_types thy;
+ val consts = map_filter (try (curry (Axclass.param_of_inst thy)
@{const_name "Quickcheck_Narrowing.partial_term_of"})) tycos;
-in fold Code.del_eqns consts end
+in fold Code.del_eqns consts thy end
\<close> -- \<open>drop technical stuff from @{text Quickcheck_Narrowing} which is tailored towards Haskell\<close>
(*
--- a/src/HOL/Probability/measurable.ML Sat Mar 28 21:32:48 2015 +0100
+++ b/src/HOL/Probability/measurable.ML Sun Mar 29 22:38:18 2015 +0200
@@ -147,8 +147,9 @@
| indep (Abs (_,_,t)) top bot = indep t (top + 1) (bot + 1)
| indep _ _ _ = true;
-fun cnt_prefixes ctxt (Abs (n, T, t)) = let
- fun is_countable t = Type.of_sort (Proof_Context.tsig_of ctxt) (t, @{sort countable})
+fun cnt_prefixes ctxt (Abs (n, T, t)) =
+ let
+ fun is_countable ty = Sign.of_sort (Proof_Context.theory_of ctxt) (ty, @{sort countable})
fun cnt_walk (Abs (ns, T, t)) Ts =
map (fn (t', t'') => (Abs (ns, T, t'), t'')) (cnt_walk t (T::Ts))
| cnt_walk (f $ g) Ts = let
--- a/src/HOL/Tools/functor.ML Sat Mar 28 21:32:48 2015 +0100
+++ b/src/HOL/Tools/functor.ML Sun Mar 29 22:38:18 2015 +0200
@@ -41,8 +41,9 @@
(* type analysis *)
-fun term_with_typ ctxt T t = Envir.subst_term_types
- (Type.typ_match (Proof_Context.tsig_of ctxt) (fastype_of t, T) Vartab.empty) t;
+fun term_with_typ ctxt T t =
+ Envir.subst_term_types
+ (Sign.typ_match (Proof_Context.theory_of ctxt) (fastype_of t, T) Vartab.empty) t;
fun find_atomic ctxt T =
let
--- a/src/HOL/Tools/inductive.ML Sat Mar 28 21:32:48 2015 +0100
+++ b/src/HOL/Tools/inductive.ML Sun Mar 29 22:38:18 2015 +0200
@@ -38,6 +38,8 @@
(string * thm list) list * local_theory
val inductive_cases_i: (Attrib.binding * term list) list -> local_theory ->
(string * thm list) list * local_theory
+ val ind_cases_rules: Proof.context ->
+ string list -> (binding * string option * mixfix) list -> thm list
val inductive_simps: (Attrib.binding * string list) list -> local_theory ->
(string * thm list) list * local_theory
val inductive_simps_i: (Attrib.binding * term list) list -> local_theory ->
@@ -600,19 +602,22 @@
val inductive_cases = gen_inductive_cases Attrib.check_src Syntax.read_prop;
val inductive_cases_i = gen_inductive_cases (K I) Syntax.check_prop;
+
+(* ind_cases *)
+
+fun ind_cases_rules ctxt raw_props raw_fixes =
+ let
+ val (props, ctxt' ) = Specification.read_props raw_props raw_fixes ctxt;
+ val rules = Proof_Context.export ctxt' ctxt (map (mk_cases ctxt') props);
+ in rules end;
+
val _ =
Theory.setup
(Method.setup @{binding ind_cases}
- (Scan.lift (Scan.repeat1 Args.name_inner_syntax --
- Scan.optional (Args.$$$ "for" |-- Scan.repeat1 Args.binding) []) >>
- (fn (raw_props, fixes) => fn ctxt =>
- let
- val (_, ctxt') = Variable.add_fixes_binding fixes ctxt;
- val props = Syntax.read_props ctxt' raw_props;
- val ctxt'' = fold Variable.declare_term props ctxt';
- val rules = Proof_Context.export ctxt'' ctxt (map (mk_cases ctxt'') props)
- in Method.erule ctxt 0 rules end))
- "dynamic case analysis on predicates");
+ (Scan.lift (Scan.repeat1 Parse.prop -- Parse.for_fixes) >>
+ (fn (props, fixes) => fn ctxt =>
+ Method.erule ctxt 0 (ind_cases_rules ctxt props fixes)))
+ "case analysis for inductive definitions, based on simplified elimination rule");
(* derivation of simplified equation *)
--- a/src/Pure/Isar/element.ML Sat Mar 28 21:32:48 2015 +0100
+++ b/src/Pure/Isar/element.ML Sun Mar 29 22:38:18 2015 +0200
@@ -236,7 +236,7 @@
val concl_term = Object_Logic.drop_judgment thy concl;
val fixes = fold_aterms (fn v as Free (x, T) =>
- if Variable.newly_fixed ctxt' ctxt x andalso not (v aconv concl_term)
+ if Variable.is_newly_fixed ctxt' ctxt x andalso not (v aconv concl_term)
then insert (op =) (Variable.revert_fixed ctxt' x, T) else I | _ => I) prop [] |> rev;
val (assumes, cases) = take_suffix (fn prem =>
is_elim andalso concl aconv Logic.strip_assums_concl prem) prems;
--- a/src/Pure/Isar/proof_context.ML Sat Mar 28 21:32:48 2015 +0100
+++ b/src/Pure/Isar/proof_context.ML Sun Mar 29 22:38:18 2015 +0200
@@ -26,6 +26,7 @@
val tsig_of: Proof.context -> Type.tsig
val set_defsort: sort -> Proof.context -> Proof.context
val default_sort: Proof.context -> indexname -> sort
+ val arity_sorts: Proof.context -> string -> sort -> sort list
val consts_of: Proof.context -> Consts.T
val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context
val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
@@ -289,6 +290,7 @@
val tsig_of = #1 o #tsig o rep_data;
val set_defsort = map_tsig o apfst o Type.set_defsort;
fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt;
+fun arity_sorts ctxt = Type.arity_sorts (Context.pretty ctxt) (tsig_of ctxt);
val consts_of = #1 o #consts o rep_data;
val cases_of = #cases o rep_data;
--- a/src/Pure/Isar/specification.ML Sat Mar 28 21:32:48 2015 +0100
+++ b/src/Pure/Isar/specification.ML Sun Mar 29 22:38:18 2015 +0200
@@ -7,6 +7,10 @@
signature SPECIFICATION =
sig
+ val read_props: string list -> (binding * string option * mixfix) list -> Proof.context ->
+ term list * Proof.context
+ val read_prop: string -> (binding * string option * mixfix) list -> Proof.context ->
+ term * Proof.context
val check_spec:
(binding * typ option * mixfix) list -> (Attrib.binding * term) list -> Proof.context ->
(((binding * typ) * mixfix) list * (Attrib.binding * term) list) * Proof.context
@@ -79,6 +83,22 @@
structure Specification: SPECIFICATION =
struct
+(* prepare propositions *)
+
+fun read_props raw_props raw_fixes ctxt =
+ let
+ val ctxt1 = ctxt |> Proof_Context.read_vars raw_fixes |-> Proof_Context.add_fixes |> #2;
+ val props1 = map (Syntax.parse_prop ctxt1) raw_props;
+ val (props2, ctxt2) = ctxt1 |> fold_map Variable.fix_dummy_patterns props1;
+ val props3 = Syntax.check_props ctxt2 props2;
+ val ctxt3 = ctxt2 |> fold Variable.declare_term props3;
+ in (props3, ctxt3) end;
+
+fun read_prop raw_prop raw_fixes ctxt =
+ let val ([prop], ctxt') = read_props [raw_prop] raw_fixes ctxt
+ in (prop, ctxt') end;
+
+
(* prepare specification *)
local
--- a/src/Pure/Syntax/local_syntax.ML Sat Mar 28 21:32:48 2015 +0100
+++ b/src/Pure/Syntax/local_syntax.ML Sun Mar 29 22:38:18 2015 +0200
@@ -55,7 +55,7 @@
val thy_syntax = Sign.syn_of thy;
fun update_gram ((true, add, m), decls) = Syntax.update_type_gram add m decls
| update_gram ((false, add, m), decls) =
- Syntax.update_const_gram add (Sign.is_logtype thy) m decls;
+ Syntax.update_const_gram add (Sign.logical_types thy) m decls;
val local_syntax = thy_syntax
|> fold update_gram (AList.coalesce (op =) (rev (map snd mixfixes)));
--- a/src/Pure/Syntax/mixfix.ML Sat Mar 28 21:32:48 2015 +0100
+++ b/src/Pure/Syntax/mixfix.ML Sun Mar 29 22:38:18 2015 +0200
@@ -26,7 +26,7 @@
val make_type: int -> typ
val binder_name: string -> string
val syn_ext_types: (string * typ * mixfix) list -> Syntax_Ext.syn_ext
- val syn_ext_consts: (string -> bool) -> (string * typ * mixfix) list -> Syntax_Ext.syn_ext
+ val syn_ext_consts: string list -> (string * typ * mixfix) list -> Syntax_Ext.syn_ext
end;
structure Mixfix: MIXFIX =
@@ -119,7 +119,7 @@
val binder_stamp = stamp ();
val binder_name = suffix "_binder";
-fun syn_ext_consts is_logtype const_decls =
+fun syn_ext_consts logical_types const_decls =
let
fun mk_infix sy ty c p1 p2 p3 =
[Syntax_Ext.Mfix ("op " ^ sy, ty, c, [], 1000),
@@ -152,7 +152,7 @@
val consts = binders @ map (fn (c, _, _) => (c, "")) const_decls;
in
- Syntax_Ext.syn_ext' is_logtype mfix consts ([], binder_trs, binder_trs', []) ([], [])
+ Syntax_Ext.syn_ext' logical_types mfix consts ([], binder_trs, binder_trs', []) ([], [])
end;
end;
--- a/src/Pure/Syntax/syntax.ML Sat Mar 28 21:32:48 2015 +0100
+++ b/src/Pure/Syntax/syntax.ML Sun Mar 29 22:38:18 2015 +0200
@@ -108,7 +108,7 @@
(string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
(string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> syntax -> syntax
val update_type_gram: bool -> mode -> (string * typ * mixfix) list -> syntax -> syntax
- val update_const_gram: bool -> (string -> bool) ->
+ val update_const_gram: bool -> string list ->
mode -> (string * typ * mixfix) list -> syntax -> syntax
val update_trrules: Ast.ast trrule list -> syntax -> syntax
val remove_trrules: Ast.ast trrule list -> syntax -> syntax
@@ -659,8 +659,8 @@
fun update_type_gram add prmode decls =
(if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_types decls);
-fun update_const_gram add is_logtype prmode decls =
- (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_consts is_logtype decls);
+fun update_const_gram add logical_types prmode decls =
+ (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_consts logical_types decls);
val update_trrules = update_syntax mode_default o Syntax_Ext.syn_ext_rules o check_rules;
val remove_trrules = remove_syntax mode_default o Syntax_Ext.syn_ext_rules o check_rules;
--- a/src/Pure/Syntax/syntax_ext.ML Sat Mar 28 21:32:48 2015 +0100
+++ b/src/Pure/Syntax/syntax_ext.ML Sun Mar 29 22:38:18 2015 +0200
@@ -31,7 +31,7 @@
val mfix_delims: string -> string list
val mfix_args: string -> int
val escape: string -> string
- val syn_ext': (string -> bool) -> mfix list ->
+ val syn_ext': string list -> mfix list ->
(string * string) list -> (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
(string * ((Proof.context -> term list -> term) * stamp)) list *
(string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
@@ -184,8 +184,10 @@
(* mfix_to_xprod *)
-fun mfix_to_xprod is_logtype (mfix as Mfix (sy, typ, const, pris, pri)) =
+fun mfix_to_xprod logical_types (mfix as Mfix (sy, typ, const, pris, pri)) =
let
+ val is_logtype = member (op =) logical_types;
+
fun check_pri p =
if p >= 0 andalso p <= 1000 then ()
else err_in_mfix ("Precedence out of range: " ^ string_of_int p) mfix;
@@ -288,12 +290,12 @@
(* syn_ext *)
-fun syn_ext' is_logtype mfixes consts trfuns (parse_rules, print_rules) =
+fun syn_ext' logical_types mfixes consts trfuns (parse_rules, print_rules) =
let
val (parse_ast_translation, parse_translation, print_translation,
print_ast_translation) = trfuns;
- val xprod_results = map (mfix_to_xprod is_logtype) mfixes;
+ val xprod_results = map (mfix_to_xprod logical_types) mfixes;
val xprods = map #1 xprod_results;
val consts' = map_filter #2 xprod_results;
val parse_rules' = rev (map_filter #3 xprod_results);
@@ -311,7 +313,7 @@
end;
-val syn_ext = syn_ext' (K false);
+val syn_ext = syn_ext' [];
fun syn_ext_rules rules = syn_ext [] [] ([], [], [], []) rules;
fun syn_ext_trfuns trfuns = syn_ext [] [] trfuns ([], []);
--- a/src/Pure/Tools/rule_insts.ML Sat Mar 28 21:32:48 2015 +0100
+++ b/src/Pure/Tools/rule_insts.ML Sun Mar 29 22:38:18 2015 +0200
@@ -92,7 +92,7 @@
|> Syntax.check_terms ctxt'
|> Variable.polymorphic ctxt';
val Ts' = map Term.fastype_of ts';
- val tyenv = fold Type.raw_match (Ts ~~ Ts') Vartab.empty;
+ val tyenv = fold (Sign.typ_match (Proof_Context.theory_of ctxt)) (Ts ~~ Ts') Vartab.empty;
val tyenv' = Vartab.fold (fn (xi, (S, T)) => cons ((xi, S), T)) tyenv [];
in ((ts', tyenv'), ctxt') end;
@@ -209,7 +209,8 @@
(* goal context *)
-val schematic = Attrib.setup_config_bool @{binding rule_insts_schematic} (K true);
+(*legacy*)
+val schematic = Attrib.setup_config_bool @{binding rule_insts_schematic} (K false);
fun goal_context goal ctxt =
let
@@ -228,29 +229,24 @@
let
(* goal context *)
- val (params, param_ctxt) = goal_context (Thm.term_of cgoal) ctxt;
+ val (params, goal_ctxt) = goal_context (Thm.term_of cgoal) ctxt;
val paramTs = map #2 params;
- (* local fixes *)
-
- val fixes_ctxt = param_ctxt
- |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2;
+ (* instantiation context *)
- val ((inst_tvars, inst_vars), inst_ctxt) = read_insts thm mixed_insts fixes_ctxt;
+ val ((inst_tvars, inst_vars), inst_ctxt) = goal_ctxt
+ |> Proof_Context.read_vars fixes |-> Proof_Context.add_fixes |> #2
+ |> read_insts thm mixed_insts;
- fun add_fixed (Free (x, _)) =
- if Variable.newly_fixed inst_ctxt param_ctxt x
- then insert (op =) x else I
- | add_fixed _ = I;
- val fixed = fold (Term.fold_aterms add_fixed o #2) inst_vars [];
+ val fixed = map #1 (fold (Variable.add_newly_fixed inst_ctxt goal_ctxt o #2) inst_vars []);
(* lift and instantiate rule *)
val inc = Thm.maxidx_of st + 1;
val lift_type = Logic.incr_tvar inc;
- fun lift_var ((a, j), T) = Var ((a, j + inc), paramTs ---> Logic.incr_tvar inc T);
+ fun lift_var ((a, j), T) = Var ((a, j + inc), paramTs ---> lift_type T);
fun lift_term t = fold_rev Term.absfree params (Logic.incr_indexes (fixed, paramTs, inc) t);
val inst_tvars' = inst_tvars
@@ -260,10 +256,8 @@
val thm' = Thm.lift_rule cgoal thm
|> Drule.instantiate_normalize (inst_tvars', inst_vars')
- |> singleton (Variable.export inst_ctxt param_ctxt);
- in
- compose_tac param_ctxt (bires_flag, thm', Thm.nprems_of thm) i
- end) i st;
+ |> singleton (Variable.export inst_ctxt ctxt);
+ in compose_tac ctxt (bires_flag, thm', Thm.nprems_of thm) i end) i st;
val res_inst_tac = bires_inst_tac false;
val eres_inst_tac = bires_inst_tac true;
--- a/src/Pure/sign.ML Sat Mar 28 21:32:48 2015 +0100
+++ b/src/Pure/sign.ML Sun Mar 29 22:38:18 2015 +0200
@@ -24,7 +24,7 @@
val of_sort: theory -> typ * sort -> bool
val inter_sort: theory -> sort * sort -> sort
val witness_sorts: theory -> (typ * sort) list -> sort list -> (typ * sort) list
- val is_logtype: theory -> string -> bool
+ val logical_types: theory -> string list
val typ_instance: theory -> typ * typ -> bool
val typ_equiv: theory -> typ * typ -> bool
val typ_match: theory -> typ * typ -> Type.tyenv -> Type.tyenv
@@ -190,7 +190,7 @@
val of_sort = Type.of_sort o tsig_of;
val inter_sort = Type.inter_sort o tsig_of;
val witness_sorts = Type.witness_sorts o tsig_of;
-val is_logtype = member (op =) o Type.logical_types o tsig_of;
+val logical_types = Type.logical_types o tsig_of;
val typ_instance = Type.typ_instance o tsig_of;
fun typ_equiv thy (T, U) = typ_instance thy (T, U) andalso typ_instance thy (U, T);
@@ -369,7 +369,7 @@
val ctxt = Type.set_mode Type.mode_syntax (Proof_Context.init_global thy);
fun prep (c, T, mx) = (c, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt T), mx)
handle ERROR msg => cat_error msg ("in syntax declaration " ^ quote c);
- in thy |> map_syn (change_gram (is_logtype thy) mode (map prep args)) end;
+ in thy |> map_syn (change_gram (logical_types thy) mode (map prep args)) end;
fun gen_add_syntax x = gen_syntax (Syntax.update_const_gram true) x;
--- a/src/Pure/type.ML Sat Mar 28 21:32:48 2015 +0100
+++ b/src/Pure/type.ML Sun Mar 29 22:38:18 2015 +0200
@@ -49,7 +49,6 @@
val restore_mode: Proof.context -> Proof.context -> Proof.context
val type_space: tsig -> Name_Space.T
val type_alias: Name_Space.naming -> binding -> string -> tsig -> tsig
- val is_logtype: tsig -> string -> bool
val check_decl: Context.generic -> tsig ->
xstring * Position.T -> (string * Position.report list) * decl
val the_decl: tsig -> string * Position.T -> decl
@@ -252,8 +251,6 @@
fun type_alias naming binding name = map_tsig (fn (classes, default, types) =>
(classes, default, (Name_Space.alias_table naming binding name types)));
-val is_logtype = member (op =) o logical_types;
-
fun undecl_type c = "Undeclared type constructor: " ^ quote c;
--- a/src/Pure/type_infer_context.ML Sat Mar 28 21:32:48 2015 +0100
+++ b/src/Pure/type_infer_context.ML Sun Mar 29 22:38:18 2015 +0200
@@ -169,7 +169,7 @@
fun unify ctxt =
let
val thy = Proof_Context.theory_of ctxt;
- val arity_sorts = Type.arity_sorts (Context.pretty ctxt) (Sign.tsig_of thy);
+ val arity_sorts = Proof_Context.arity_sorts ctxt;
(* adjust sorts of parameters *)
--- a/src/Pure/variable.ML Sat Mar 28 21:32:48 2015 +0100
+++ b/src/Pure/variable.ML Sun Mar 29 22:38:18 2015 +0200
@@ -38,7 +38,7 @@
val restore_proper_fixes: Proof.context -> Proof.context -> Proof.context
val is_improper: Proof.context -> string -> bool
val is_fixed: Proof.context -> string -> bool
- val newly_fixed: Proof.context -> Proof.context -> string -> bool
+ val is_newly_fixed: Proof.context -> Proof.context -> string -> bool
val fixed_ord: Proof.context -> string * string -> order
val intern_fixed: Proof.context -> string -> string
val markup_fixed: Proof.context -> string -> Markup.T
@@ -46,6 +46,8 @@
val revert_fixed: Proof.context -> string -> string
val add_fixed_names: Proof.context -> term -> string list -> string list
val add_fixed: Proof.context -> term -> (string * typ) list -> (string * typ) list
+ val add_newly_fixed: Proof.context -> Proof.context ->
+ term -> (string * typ) list -> (string * typ) list
val add_free_names: Proof.context -> term -> string list -> string list
val add_frees: Proof.context -> term -> (string * typ) list -> (string * typ) list
val add_fixes_binding: binding list -> Proof.context -> string list * Proof.context
@@ -346,7 +348,7 @@
(* specialized name space *)
val is_fixed = Name_Space.defined_entry o fixes_space;
-fun newly_fixed inner outer = is_fixed inner andf (not o is_fixed outer);
+fun is_newly_fixed inner outer = is_fixed inner andf (not o is_fixed outer);
val fixed_ord = Name_Space.entry_ord o fixes_space;
val intern_fixed = Name_Space.intern o fixes_space;
@@ -383,6 +385,9 @@
fun add_fixed ctxt =
fold_aterms (fn Free (x, T) => is_fixed ctxt x ? insert (op =) (x, T) | _ => I);
+fun add_newly_fixed ctxt' ctxt =
+ fold_aterms (fn Free (x, T) => is_newly_fixed ctxt' ctxt x ? insert (op =) (x, T) | _ => I);
+
(* declarations *)
@@ -474,7 +479,7 @@
fun export_inst inner outer =
let
val declared_outer = is_declared outer;
- val still_fixed = not o newly_fixed inner outer;
+ val still_fixed = not o is_newly_fixed inner outer;
val gen_fixes =
Name_Space.fold_table (fn (y, _) => not (is_fixed outer y) ? cons y)
--- a/src/Tools/Code/code_preproc.ML Sat Mar 28 21:32:48 2015 +0100
+++ b/src/Tools/Code/code_preproc.ML Sun Mar 29 22:38:18 2015 +0200
@@ -371,8 +371,9 @@
val thy = Proof_Context.theory_of ctxt;
val all_classes = complete_proper_sort thy [class];
val super_classes = remove (op =) class all_classes;
- val classess = map (complete_proper_sort thy)
- (Sign.arity_sorts thy tyco [class]);
+ val classess =
+ map (complete_proper_sort thy)
+ (Proof_Context.arity_sorts ctxt tyco [class]);
val inst_params = inst_params thy tyco all_classes;
in (classess, (super_classes, inst_params)) end;
@@ -410,7 +411,7 @@
|> apfst (Vargraph.add_edge (c_k, c_k'))
end
and ensure_typmatch_inst ctxt arities eqngr (tyco, styps) class vardeps_data =
- if can (Sign.arity_sorts (Proof_Context.theory_of ctxt) tyco) [class]
+ if can (Proof_Context.arity_sorts ctxt tyco) [class]
then vardeps_data
|> ensure_inst ctxt arities eqngr (class, tyco)
|> fold_index (fn (k, styp) =>
--- a/src/Tools/induct.ML Sat Mar 28 21:32:48 2015 +0100
+++ b/src/Tools/induct.ML Sun Mar 29 22:38:18 2015 +0200
@@ -394,12 +394,11 @@
fun prep_inst ctxt align tune (tm, ts) =
let
- val cert = Thm.global_cterm_of (Proof_Context.theory_of ctxt);
fun prep_var (x, SOME t) =
let
- val cx = cert x;
+ val cx = Thm.cterm_of ctxt x;
val xT = Thm.typ_of_cterm cx;
- val ct = cert (tune t);
+ val ct = Thm.cterm_of ctxt (tune t);
val tT = Thm.typ_of_cterm ct;
in
if Type.could_unify (tT, xT) then SOME (cx, ct)
@@ -478,8 +477,6 @@
fun cases_tac ctxt simp insts opt_rule facts =
let
- val thy = Proof_Context.theory_of ctxt;
-
fun inst_rule r =
(if null insts then r
else
@@ -505,7 +502,7 @@
val rule' = rule
|> simp ? (simplified_rule' ctxt #> unmark_constraints ctxt);
in
- CASES (Rule_Cases.make_common (thy,
+ CASES (Rule_Cases.make_common (Proof_Context.theory_of ctxt,
Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
((Method.insert_tac more_facts THEN' resolve_tac ctxt [rule'] THEN_ALL_NEW
(if simp then TRY o trivial_tac ctxt else K all_tac)) i) st
@@ -569,21 +566,18 @@
local
-fun dest_env thy env =
+fun dest_env ctxt env =
let
- val cert = Thm.global_cterm_of thy;
- val certT = Thm.global_ctyp_of thy;
val pairs = Vartab.dest (Envir.term_env env);
val types = Vartab.dest (Envir.type_env env);
- val ts = map (cert o Envir.norm_term env o #2 o #2) pairs;
- val xs = map2 (curry (cert o Var)) (map #1 pairs) (map Thm.typ_of_cterm ts);
- in (map (fn (xi, (S, T)) => (certT (TVar (xi, S)), certT T)) types, xs ~~ ts) end;
+ val ts = map (Thm.cterm_of ctxt o Envir.norm_term env o #2 o #2) pairs;
+ val xs = map2 (curry (Thm.cterm_of ctxt o Var)) (map #1 pairs) (map Thm.typ_of_cterm ts);
+ in (map (fn (xi, (S, T)) => apply2 (Thm.ctyp_of ctxt) (TVar (xi, S), T)) types, xs ~~ ts) end;
in
fun guess_instance ctxt rule i st =
let
- val thy = Proof_Context.theory_of ctxt;
val maxidx = Thm.maxidx_of st;
val goal = Thm.term_of (Thm.cprem_of st i); (*exception Subscript*)
val params = rev (Term.rename_wrt_term goal (Logic.strip_params goal));
@@ -599,7 +593,7 @@
in
Unify.smash_unifiers (Context.Proof ctxt)
[(Thm.concl_of rule', concl)] (Envir.empty (Thm.maxidx_of rule'))
- |> Seq.map (fn env => Drule.instantiate_normalize (dest_env thy env) rule')
+ |> Seq.map (fn env => Drule.instantiate_normalize (dest_env ctxt env) rule')
end
end
handle General.Subscript => Seq.empty;
@@ -654,19 +648,17 @@
fun meta_spec_tac ctxt n (x, T) = SUBGOAL (fn (goal, i) =>
let
- val thy = Proof_Context.theory_of ctxt;
- val cert = Thm.global_cterm_of thy;
-
val v = Free (x, T);
fun spec_rule prfx (xs, body) =
@{thm Pure.meta_spec}
|> Thm.rename_params_rule ([Name.clean (Variable.revert_fixed ctxt x)], 1)
- |> Thm.lift_rule (cert prfx)
+ |> Thm.lift_rule (Thm.cterm_of ctxt prfx)
|> `(Thm.prop_of #> Logic.strip_assums_concl)
|-> (fn pred $ arg =>
Drule.cterm_instantiate
- [(cert (Term.head_of pred), cert (Logic.rlist_abs (xs, body))),
- (cert (Term.head_of arg), cert (Logic.rlist_abs (xs, v)))]);
+ (map (apply2 (Thm.cterm_of ctxt))
+ [(Term.head_of pred, Logic.rlist_abs (xs, body)),
+ (Term.head_of arg, Logic.rlist_abs (xs, v))]));
fun goal_concl k xs (Const (@{const_name Pure.all}, _) $ Abs (a, T, B)) =
goal_concl k ((a, T) :: xs) B
@@ -835,8 +827,6 @@
fun coinduct_tac ctxt inst taking opt_rule facts = SUBGOAL_CASES (fn (goal, i, st) =>
let
- val thy = Proof_Context.theory_of ctxt;
-
fun inst_rule r =
if null inst then `Rule_Cases.get r
else Drule.cterm_instantiate (prep_inst ctxt align_right I (main_prop_of r, inst)) r
@@ -857,7 +847,7 @@
guess_instance ctxt rule i st
|> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
|> Seq.maps (fn rule' =>
- CASES (Rule_Cases.make_common (thy,
+ CASES (Rule_Cases.make_common (Proof_Context.theory_of ctxt,
Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
(Method.insert_tac more_facts i THEN resolve_tac ctxt [rule'] i) st))
end);
--- a/src/Tools/subtyping.ML Sat Mar 28 21:32:48 2015 +0100
+++ b/src/Tools/subtyping.ML Sun Mar 29 22:38:18 2015 +0200
@@ -144,7 +144,7 @@
fun unify weak ctxt =
let
val thy = Proof_Context.theory_of ctxt;
- val arity_sorts = Type.arity_sorts (Context.pretty ctxt) (Sign.tsig_of thy);
+ val arity_sorts = Proof_Context.arity_sorts ctxt;
(* adjust sorts of parameters *)
@@ -344,7 +344,7 @@
val coes_graph = coes_graph_of ctxt;
val tmaps = tmaps_of ctxt;
- val arity_sorts = Type.arity_sorts (Context.pretty ctxt) (Sign.tsig_of thy);
+ val arity_sorts = Proof_Context.arity_sorts ctxt;
fun split_cs _ [] = ([], [])
| split_cs f (c :: cs) =