--- a/src/Pure/Isar/obtain.ML Tue Apr 26 11:56:06 2016 +0200
+++ b/src/Pure/Isar/obtain.ML Tue Apr 26 16:20:28 2016 +0200
@@ -193,27 +193,27 @@
local
-fun gen_obtain prep_spec prep_att that_binding raw_vars raw_asms int state =
+fun gen_obtain prep_statement prep_att that_binding raw_vars raw_asms int state =
let
val _ = Proof.assert_forward_or_chain state;
val ((_, thesis), thesis_ctxt) = obtain_thesis (Proof.context_of state);
+ val ((vars, propss, binds, binds'), params_ctxt) =
+ prep_statement raw_vars (map #2 raw_asms) thesis_ctxt;
+ val params = map #2 vars;
+ val that_prop =
+ Logic.list_rename_params (map #1 params)
+ (fold_rev Logic.all (map #2 params) (Logic.list_implies (flat propss, thesis)));
- val (((vars, xs, params), propss, binds, binds'), params_ctxt) =
- prep_spec raw_vars (map #2 raw_asms) thesis_ctxt;
- val cparams = map (Thm.cterm_of params_ctxt) params;
+ val cparams = map (Thm.cterm_of params_ctxt o #2 o #2) vars;
val asms =
map (fn ((b, raw_atts), _) => (b, map (prep_att params_ctxt) raw_atts)) raw_asms ~~
map (map (rpair [])) propss;
- val that_prop =
- Logic.list_rename_params xs
- (fold_rev Logic.all params (Logic.list_implies (flat propss, thesis)));
-
fun after_qed (result_ctxt, results) state' =
let val [rule] = Proof_Context.export result_ctxt (Proof.context_of state') (flat results) in
state'
- |> Proof.fix vars
+ |> Proof.fix (map #1 vars)
|> Proof.map_context (fold Variable.bind_term binds)
|> Proof.assm (obtain_export params_ctxt rule cparams) [] [] asms
end;
@@ -229,8 +229,8 @@
in
-val obtain = gen_obtain Proof_Context.cert_spec (K I);
-val obtain_cmd = gen_obtain Proof_Context.read_spec Attrib.attribute_cmd;
+val obtain = gen_obtain Proof_Context.cert_statement (K I);
+val obtain_cmd = gen_obtain Proof_Context.read_statement Attrib.attribute_cmd;
end;
--- a/src/Pure/Isar/proof.ML Tue Apr 26 11:56:06 2016 +0200
+++ b/src/Pure/Isar/proof.ML Tue Apr 26 16:20:28 2016 +0200
@@ -694,13 +694,9 @@
val ctxt = context_of state;
val bindings = map (apsnd (map (prep_att ctxt)) o fst) raw_concls;
- val (params, prems_propss, concl_propss, result_binds) =
- #1 (prep_clause prep_var prep_propp raw_fixes raw_prems (map snd raw_concls) ctxt);
-
- fun close prop =
- fold_rev Logic.dependent_all_name params
- (Logic.list_implies (flat prems_propss, prop));
- val propss = (map o map) close concl_propss;
+ val ((params, prems_propss, concl_propss, result_binds), _) =
+ prep_clause prep_var prep_propp raw_fixes raw_prems (map snd raw_concls) ctxt;
+ val propss = (map o map) (Logic.close_prop params (flat prems_propss)) concl_propss;
in
state
|> assert_forward
@@ -893,45 +889,37 @@
local
-fun match_defs (((b, _, mx), x) :: more_decls) ((((a, _), t), _) :: more_defs) =
- if x = a then ((b, mx), (Thm.empty_binding, t)) :: match_defs more_decls more_defs
- else error ("Mismatch of declaration " ^ quote x ^ " wrt. definition " ^ quote a)
- | match_defs [] [] = []
- | match_defs more_decls more_defs =
- error ("Mismatch of declarations " ^ commas_quote (map #2 more_decls) ^
- (if null more_decls then "" else " ") ^
- "wrt. definitions " ^ commas_quote (map (#1 o #1 o #1) more_defs));
-
-fun invisible_fixes vars ctxt = ctxt
- |> Context_Position.set_visible false
- |> Proof_Context.add_fixes vars |> #2
- |> Context_Position.restore_visible ctxt;
-
-fun gen_define prep_spec prep_att raw_vars raw_fixes raw_defs state =
+fun gen_define prep_statement prep_att raw_decls raw_fixes raw_defs state =
let
val _ = assert_forward state;
val ctxt = context_of state;
(*vars*)
- val n_vars = length raw_vars;
- val (((all_vars, _, all_params), defss, _, binds'), _) =
- prep_spec (raw_vars @ raw_fixes) (map snd raw_defs) ctxt;
- val (vars, fixes) = chop n_vars all_vars;
- val (params, _) = chop n_vars all_params;
+ val ((vars, propss, _, binds'), vars_ctxt) =
+ prep_statement (raw_decls @ raw_fixes) (map snd raw_defs) ctxt;
+ val (decls, fixes) = chop (length raw_decls) vars;
+ val show_term = Syntax.string_of_term vars_ctxt;
(*defs*)
- val derived_def = Local_Defs.derived_def (invisible_fixes vars ctxt) {conditional = false};
- val defs1 = map derived_def (flat defss);
- val defs2 = match_defs (vars ~~ map (#1 o dest_Free) params) defs1;
+ fun match_defs (((b, _, mx), (_, Free (x, T))) :: more_decls) ((((y, U), t), _) :: more_defs) =
+ if x = y then ((b, mx), (Thm.empty_binding, t)) :: match_defs more_decls more_defs
+ else
+ error ("Mismatch of declaration " ^ show_term (Free (x, T)) ^ " wrt. definition " ^
+ show_term (Free (y, U)))
+ | match_defs [] [] = []
+ | match_defs more_decls more_defs =
+ error ("Mismatch of declarations " ^ commas (map (show_term o #2 o #2) more_decls) ^
+ (if null more_decls then "" else " ") ^
+ "wrt. definitions " ^ commas (map (show_term o Free o #1 o #1) more_defs));
+
+ val derived_def = Local_Defs.derived_def ctxt {conditional = false};
+ val defs1 = map (derived_def o Logic.close_prop (map #2 fixes) []) (flat propss);
+ val defs2 = match_defs decls defs1;
val (defs3, defs_ctxt) = Local_Defs.add_defs defs2 ctxt;
- (*fixes*)
- val fixes_ctxt = invisible_fixes fixes defs_ctxt;
- val export = singleton (Variable.export fixes_ctxt defs_ctxt);
-
(*notes*)
val def_thmss =
- map (fn (((_, prove), ((b, _), _)), (_, (_, th))) => (b, export (prove fixes_ctxt th)))
+ map (fn (((_, prove), ((b, _), _)), (_, (_, th))) => (b, prove defs_ctxt th))
(defs1 ~~ defs2 ~~ defs3)
|> unflat (map snd raw_defs);
val notes =
@@ -947,8 +935,8 @@
in
-val define = gen_define Proof_Context.cert_spec (K I);
-val define_cmd = gen_define Proof_Context.read_spec Attrib.attribute_cmd;
+val define = gen_define Proof_Context.cert_statement (K I);
+val define_cmd = gen_define Proof_Context.read_statement Attrib.attribute_cmd;
end;
--- a/src/Pure/Isar/proof_context.ML Tue Apr 26 11:56:06 2016 +0200
+++ b/src/Pure/Isar/proof_context.ML Tue Apr 26 16:20:28 2016 +0200
@@ -166,12 +166,14 @@
val generic_add_abbrev: string -> binding * term -> Context.generic ->
(term * term) * Context.generic
val generic_revert_abbrev: string -> string -> Context.generic -> Context.generic
- val cert_spec: (binding * typ option * mixfix) list -> (term * term list) list list ->
- Proof.context -> (((binding * typ option * mixfix) list * string list * term list) *
- term list list * (indexname * term) list * (indexname * term) list) * Proof.context
- val read_spec: (binding * string option * mixfix) list -> (string * string list) list list ->
- Proof.context -> (((binding * typ option * mixfix) list * string list * term list) *
- term list list * (indexname * term) list * (indexname * term) list) * Proof.context
+ val cert_statement:
+ (binding * typ option * mixfix) list -> (term * term list) list list -> Proof.context ->
+ (((binding * typ option * mixfix) * (string * term)) list * term list list *
+ (indexname * term) list * (indexname * term) list) * Proof.context
+ val read_statement:
+ (binding * string option * mixfix) list -> (string * string list) list list -> Proof.context ->
+ (((binding * typ option * mixfix) * (string * term)) list * term list list *
+ (indexname * term) list * (indexname * term) list) * Proof.context
val print_syntax: Proof.context -> unit
val print_abbrevs: bool -> Proof.context -> unit
val pretty_term_bindings: Proof.context -> Pretty.T list
@@ -1326,38 +1328,32 @@
end;
-(* specification with parameters *)
+(* structured statement *)
local
-fun prep_spec prep_var prep_propp raw_vars raw_propps ctxt =
+fun prep_statement prep_var prep_propp raw_vars raw_propps ctxt =
let
- (*vars*)
- val ((xs', vars), vars_ctxt) = ctxt
- |> fold_map prep_var raw_vars
- |-> (fn vars => add_fixes vars ##>> pair vars);
+ val (vars, vars_ctxt) = fold_map prep_var raw_vars ctxt;
val xs = map (Variable.check_name o #1) vars;
-
- (*propps*)
- val (propss, binds) = prep_propp vars_ctxt raw_propps;
- val props = flat propss;
+ val (xs', fixes_ctxt) = add_fixes vars vars_ctxt;
- (*params*)
- val (ps, params_ctxt) = vars_ctxt
- |> fold Variable.declare_term props
- |> fold Variable.bind_term binds
+ val (propss, binds) = prep_propp fixes_ctxt raw_propps;
+ val (ps, params_ctxt) = fixes_ctxt
+ |> (fold o fold) Variable.declare_term propss
|> fold_map inferred_param xs';
- val params = map Free ps;
- val binds' = (map o apsnd) (fold_rev Term.dependent_lambda_name (xs ~~ params)) binds;
+ val params = xs ~~ map Free ps;
+
val vars' = map2 (fn (b, _, mx) => fn (_, T) => (b, SOME T, mx)) vars ps;
+ val binds' = (map o apsnd) (Logic.close_term params) binds;
- val _ = Variable.warn_extra_tfrees vars_ctxt params_ctxt;
- in (((vars', xs, params), propss, binds, binds'), params_ctxt) end;
+ val _ = Variable.warn_extra_tfrees fixes_ctxt params_ctxt;
+ in ((vars' ~~ params, propss, binds, binds'), params_ctxt) end;
in
-val cert_spec = prep_spec cert_var cert_propp;
-val read_spec = prep_spec read_var read_propp;
+val cert_statement = prep_statement cert_var cert_propp;
+val read_statement = prep_statement read_var read_propp;
end;
--- a/src/Pure/logic.ML Tue Apr 26 11:56:06 2016 +0200
+++ b/src/Pure/logic.ML Tue Apr 26 16:20:28 2016 +0200
@@ -26,6 +26,8 @@
val strip_prems: int * term list * term -> term list * term
val count_prems: term -> int
val nth_prem: int * term -> term
+ val close_term: (string * term) list -> term -> term
+ val close_prop: (string * term) list -> term list -> term -> term
val true_prop: term
val conjunction: term
val mk_conjunction: term * term -> term
@@ -147,7 +149,6 @@
end;
-
(** equality **)
fun mk_equals (t, u) =
@@ -204,6 +205,11 @@
fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
+(* close *)
+
+val close_term = fold_rev Term.dependent_lambda_name;
+fun close_prop xs As B = fold_rev dependent_all_name xs (list_implies (As, B));
+
(** conjunction **)