--- a/src/HOL/Eisbach/Tests.thy Thu Sep 19 17:24:08 2019 +0100
+++ b/src/HOL/Eisbach/Tests.thy Thu Sep 19 17:24:15 2019 +0100
@@ -166,7 +166,7 @@
done
(* Cut tests *)
- fix A B C
+ fix A B C D
have "D \<and> C \<Longrightarrow> A \<and> B \<Longrightarrow> A \<longrightarrow> C \<Longrightarrow> D \<longrightarrow> True \<Longrightarrow> C"
by (((match premises in I: "P \<and> Q" (cut)
--- a/src/Pure/Isar/obtain.ML Thu Sep 19 17:24:08 2019 +0100
+++ b/src/Pure/Isar/obtain.ML Thu Sep 19 17:24:15 2019 +0100
@@ -201,7 +201,7 @@
val ((_, thesis), thesis_ctxt) = obtain_thesis (Proof.context_of state);
- val ((vars, propss, binds, binds'), params_ctxt) =
+ val ({vars, propss, binds, result_binds, ...}, params_ctxt) =
prep_stmt (raw_decls @ raw_fixes) (raw_prems @ map #2 raw_concls) thesis_ctxt;
val (decls, fixes) = chop (length raw_decls) vars ||> map #2;
val (premss, conclss) = chop (length raw_prems) propss;
@@ -230,7 +230,7 @@
[((that_binding, [Context_Rules.intro_query NONE]), [(that_prop, [])])]
[(Binding.empty_atts, [(thesis, [])])] int
|-> Proof.refine_insert
- |> Proof.map_context (fold Variable.bind_term binds')
+ |> Proof.map_context (fold Variable.bind_term result_binds)
end;
in
--- a/src/Pure/Isar/proof.ML Thu Sep 19 17:24:08 2019 +0100
+++ b/src/Pure/Isar/proof.ML Thu Sep 19 17:24:15 2019 +0100
@@ -557,16 +557,36 @@
local
-fun gen_bind bind args state =
- state
- |> assert_forward
- |> map_context (bind true args #> snd)
- |> reset_facts;
+fun gen_bind prep_terms raw_binds =
+ assert_forward #> map_context (fn ctxt =>
+ let
+ fun prep_bind (raw_pats, t) ctxt1 =
+ let
+ val T = Term.fastype_of t;
+ val ctxt2 = Variable.declare_term t ctxt1;
+ val pats = prep_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt2) T raw_pats;
+ val binds = Proof_Context.simult_matches ctxt2 (t, pats);
+ in (binds, ctxt2) end;
+
+ val ts = prep_terms ctxt dummyT (map snd raw_binds);
+ val (binds, ctxt') = apfst flat (fold_map prep_bind (map fst raw_binds ~~ ts) ctxt);
+ val binds' = map #1 binds ~~ Variable.exportT_terms ctxt' ctxt (map #2 binds);
+
+ val ctxt'' =
+ ctxt
+ |> fold Variable.declare_term (map #2 binds')
+ |> fold Proof_Context.bind_term binds';
+ val _ = Variable.warn_extra_tfrees ctxt ctxt'';
+ in ctxt'' end)
+ #> reset_facts;
+
+fun read_terms ctxt T =
+ map (Syntax.parse_term ctxt #> Type.constraint T) #> Syntax.check_terms ctxt;
in
-val let_bind = gen_bind Proof_Context.match_bind;
-val let_bind_cmd = gen_bind Proof_Context.match_bind_cmd;
+val let_bind = gen_bind (fn ctxt => fn _ => map (Proof_Context.cert_term ctxt));
+val let_bind_cmd = gen_bind read_terms;
end;
@@ -625,15 +645,15 @@
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), _) =
- prep_statement raw_fixes raw_prems (map snd raw_concls) ctxt;
+ val {fixes = params, assumes = prems_propss, shows = concl_propss, result_binds, text, ...} =
+ #1 (prep_statement 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
|> map_context_result (fn ctxt =>
ctxt
- |> (fold o fold) Variable.declare_term propss
+ |> Proof_Context.augment text
|> fold Variable.maybe_bind_term result_binds
|> fold_burrow (Assumption.add_assms export o map (Thm.cterm_of ctxt)) propss
|-> (fn premss =>
@@ -792,7 +812,7 @@
val ctxt = context_of state;
(*vars*)
- val ((vars, propss, _, binds'), vars_ctxt) =
+ val ({vars, propss, result_binds, ...}, vars_ctxt) =
prep_stmt (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;
@@ -826,7 +846,7 @@
raw_defs def_thmss;
in
state
- |> map_context (K defs_ctxt #> fold Variable.bind_term binds')
+ |> map_context (K defs_ctxt #> fold Variable.bind_term result_binds)
|> note_thmss notes
end;
@@ -1037,13 +1057,15 @@
(if strict_asm then Assumption.assume_export else Assumption.presume_export);
(*params*)
- val ((params, assumes_propss, shows_propss, result_binds), params_ctxt) = ctxt
+ val ({fixes = params, assumes = assumes_propss, shows = shows_propss,
+ result_binds, result_text, text}, params_ctxt) = ctxt
|> prep_statement raw_fixes (map snd raw_assumes) (map snd raw_shows);
(*prems*)
val (assumes_bindings, shows_bindings) =
apply2 (map (apsnd (map (prep_att ctxt)) o fst)) (raw_assumes, raw_shows);
val (that_fact, goal_ctxt) = params_ctxt
+ |> fold Proof_Context.augment (text :: flat (assumes_propss @ shows_propss))
|> fold_burrow add_assumes ((map o map) (Thm.cterm_of params_ctxt) assumes_propss)
|> (fn (premss, ctxt') =>
let
@@ -1063,12 +1085,13 @@
let
val ctxt' = context_of state';
val export0 =
- Assumption.export false result_ctxt ctxt' #>
+ Assumption.export false result_ctxt (Proof_Context.augment result_text ctxt') #>
fold_rev (fn (x, v) => Thm.forall_intr_name (x, Thm.cterm_of params_ctxt v)) params #>
Raw_Simplifier.norm_hhf_protect ctxt';
val export = map export0 #> Variable.export result_ctxt ctxt';
in
state'
+ |> map_context (Proof_Context.augment result_text)
|> local_results (results_bindings ~~ burrow export results)
|-> (fn res => tap (fn st => print_results (context_of st) ((kind, ""), res) : unit))
|> after_qed (result_ctxt, results)
--- a/src/Pure/Isar/proof_context.ML Thu Sep 19 17:24:08 2019 +0100
+++ b/src/Pure/Isar/proof_context.ML Thu Sep 19 17:24:15 2019 +0100
@@ -108,10 +108,9 @@
val norm_export_morphism: Proof.context -> Proof.context -> morphism
val auto_bind_goal: term list -> Proof.context -> Proof.context
val auto_bind_facts: term list -> Proof.context -> Proof.context
- val match_bind: bool -> (term list * term) list -> Proof.context ->
- term list * Proof.context
- val match_bind_cmd: bool -> (string list * string) list -> Proof.context ->
- term list * Proof.context
+ val simult_matches: Proof.context -> term * term list -> (indexname * term) list
+ val maybe_bind_term: indexname * term option -> Proof.context -> Proof.context
+ val bind_term: indexname * term -> Proof.context -> Proof.context
val cert_propp: Proof.context -> (term * term list) list list ->
(term list list * (indexname * term) list)
val read_propp: Proof.context -> (string * string list) list list ->
@@ -170,22 +169,28 @@
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_stmt:
- (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_stmt:
- (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
+ type stmt =
+ {vars: ((binding * typ option * mixfix) * (string * term)) list,
+ propss: term list list,
+ binds: (indexname * term) list,
+ result_binds: (indexname * term) list}
+ val cert_stmt: (binding * typ option * mixfix) list -> (term * term list) list list ->
+ Proof.context -> stmt * Proof.context
+ val read_stmt: (binding * string option * mixfix) list -> (string * string list) list list ->
+ Proof.context -> stmt * Proof.context
+ type statement =
+ {fixes: (string * term) list,
+ assumes: term list list,
+ shows: term list list,
+ result_binds: (indexname * term option) list,
+ text: term,
+ result_text: term}
val cert_statement: (binding * typ option * mixfix) list ->
(term * term list) list list -> (term * term list) list list -> Proof.context ->
- ((string * term) list * term list list * term list list * (indexname * term option) list) *
- Proof.context
+ statement * Proof.context
val read_statement: (binding * string option * mixfix) list ->
(string * string list) list list -> (string * string list) list list -> Proof.context ->
- ((string * term) list * term list list * term list list * (indexname * term option) list) *
- Proof.context
+ statement * Proof.context
val print_syntax: Proof.context -> unit
val print_abbrevs: bool -> Proof.context -> unit
val pretty_term_bindings: Proof.context -> Pretty.T list
@@ -418,8 +423,7 @@
(* augment context by implicit term declarations *)
fun augment t ctxt = ctxt
- |> not (Variable.is_body ctxt) ?
- Variable.add_fixes_direct (rev (Variable.add_free_names ctxt t []))
+ |> Variable.add_fixes_implicit t
|> Variable.declare_term t
|> Soft_Type_System.augment t;
@@ -849,15 +853,7 @@
(** term bindings **)
-(* simult_matches *)
-
-fun simult_matches ctxt (t, pats) =
- (case Seq.pull (Unify.matchers (Context.Proof ctxt) (map (rpair t) pats)) of
- NONE => error "Pattern match failed!"
- | SOME (env, _) => Vartab.fold (fn (v, (_, t)) => cons (v, t)) (Envir.term_env env) []);
-
-
-(* auto_bind *)
+(* auto bindings *)
fun auto_bind f props ctxt = fold Variable.maybe_bind_term (f ctxt props) ctxt;
@@ -865,52 +861,18 @@
val auto_bind_facts = auto_bind Auto_Bind.facts;
-(* bind terms (non-schematic) *)
+(* match bindings *)
-fun cert_maybe_bind_term (xi, t) ctxt =
+fun simult_matches ctxt (t, pats) =
+ (case Seq.pull (Unify.matchers (Context.Proof ctxt) (map (rpair t) pats)) of
+ NONE => error "Pattern match failed!"
+ | SOME (env, _) => Vartab.fold (fn (v, (_, t)) => cons (v, t)) (Envir.term_env env) []);
+
+fun maybe_bind_term (xi, t) ctxt =
ctxt
|> Variable.maybe_bind_term (xi, Option.map (cert_term (set_mode mode_default ctxt)) t);
-val cert_bind_term = cert_maybe_bind_term o apsnd SOME;
-
-
-(* match_bind *)
-
-local
-
-fun gen_bind prep_terms gen raw_binds ctxt =
- let
- fun prep_bind (raw_pats, t) ctxt1 =
- let
- val T = Term.fastype_of t;
- val ctxt2 = Variable.declare_term t ctxt1;
- val pats = prep_terms (set_mode mode_pattern ctxt2) T raw_pats;
- val binds = simult_matches ctxt2 (t, pats);
- in (binds, ctxt2) end;
-
- val ts = prep_terms ctxt dummyT (map snd raw_binds);
- val (binds, ctxt') = apfst flat (fold_map prep_bind (map fst raw_binds ~~ ts) ctxt);
- val binds' =
- if gen then map #1 binds ~~ Variable.exportT_terms ctxt' ctxt (map #2 binds)
- else binds;
- val ctxt'' =
- tap (Variable.warn_extra_tfrees ctxt)
- (if gen then
- ctxt (*sic!*)
- |> fold Variable.declare_term (map #2 binds')
- |> fold cert_bind_term binds'
- else ctxt' |> fold cert_bind_term binds');
- in (ts, ctxt'') end;
-
-in
-
-fun read_terms ctxt T =
- map (Syntax.parse_term ctxt #> Type.constraint T) #> Syntax.check_terms ctxt;
-
-val match_bind = gen_bind (fn ctxt => fn _ => map (cert_term ctxt));
-val match_bind_cmd = gen_bind read_terms;
-
-end;
+val bind_term = maybe_bind_term o apsnd SOME;
(* propositions with patterns *)
@@ -1347,7 +1309,7 @@
val Rule_Cases.Case {assumes, binds, cases, ...} = Rule_Cases.apply ts c;
in
ctxt'
- |> fold (cert_maybe_bind_term o drop_schematic) binds
+ |> fold (maybe_bind_term o drop_schematic) binds
|> update_cases (map (apsnd SOME) cases)
|> pair (assumes, (binds, cases))
end;
@@ -1378,6 +1340,20 @@
(* structured statements *)
+type stmt =
+ {vars: ((binding * typ option * mixfix) * (string * term)) list,
+ propss: term list list,
+ binds: (indexname * term) list,
+ result_binds: (indexname * term) list};
+
+type statement =
+ {fixes: (string * term) list,
+ assumes: term list list,
+ shows: term list list,
+ result_binds: (indexname * term option) list,
+ text: term,
+ result_text: term};
+
local
fun export_binds ctxt' ctxt params binds =
@@ -1407,13 +1383,15 @@
|> map (apsnd the);
val _ = Variable.warn_extra_tfrees fixes_ctxt params_ctxt;
- in ((vars' ~~ params, propss, binds, binds'), params_ctxt) end;
+ val result : stmt =
+ {vars = vars' ~~ params, propss = propss, binds = binds, result_binds = binds'};
+ in (result, params_ctxt) end;
fun prep_statement prep_var prep_propp raw_fixes raw_assumes raw_shows ctxt =
let
val ((fixes, (assumes, shows), binds), ctxt') = ctxt
|> prep_stmt prep_var prep_propp raw_fixes (raw_assumes @ raw_shows)
- |-> (fn (vars, propss, binds, _) =>
+ |-> (fn {vars, propss, binds, ...} =>
fold Variable.bind_term binds #>
pair (map #2 vars, chop (length raw_assumes) propss, binds));
val binds' =
@@ -1422,7 +1400,18 @@
NONE => []
| SOME prop => map (apsnd (SOME o Auto_Bind.abs_params prop)) binds))
|> export_binds ctxt' ctxt fixes;
- in ((fixes, assumes, shows, binds'), ctxt') end;
+
+ val text = Logic.close_prop fixes (flat assumes) (Logic.mk_conjunction_list (flat shows));
+ val text' = singleton (Variable.export_terms ctxt' ctxt) text;
+
+ val result : statement =
+ {fixes = fixes,
+ assumes = assumes,
+ shows = shows,
+ result_binds = binds',
+ text = text,
+ result_text = text'};
+ in (result, ctxt') end;
in
--- a/src/Pure/Isar/specification.ML Thu Sep 19 17:24:08 2019 +0100
+++ b/src/Pure/Isar/specification.ML Thu Sep 19 17:24:15 2019 +0100
@@ -204,7 +204,7 @@
fun gen_axioms prep_stmt prep_att raw_decls raw_fixes raw_prems raw_concls thy =
let
(*specification*)
- val ((vars, [prems, concls], _, _), vars_ctxt) =
+ val ({vars, propss = [prems, concls], ...}, vars_ctxt) =
Proof_Context.init_global thy
|> prep_stmt (raw_decls @ raw_fixes) ((map o map) (rpair []) [raw_prems, map snd raw_concls]);
val (decls, fixes) = chop (length raw_decls) vars;
--- a/src/Pure/assumption.ML Thu Sep 19 17:24:08 2019 +0100
+++ b/src/Pure/assumption.ML Thu Sep 19 17:24:15 2019 +0100
@@ -85,13 +85,33 @@
(* local assumptions *)
+local
+
+fun drop_prefix eq (args as (x :: xs, y :: ys)) =
+ if eq (x, y) then drop_prefix eq (xs, ys) else args
+ | drop_prefix _ args = args;
+
+fun check_result ctxt kind term_of res =
+ (case res of
+ ([], rest) => rest
+ | (bad :: _, _) =>
+ raise Fail ("Outer context disagrees on " ^ kind ^ ": " ^
+ Syntax.string_of_term ctxt (term_of bad)));
+
+in
+
fun local_assumptions_of inner outer =
- drop (length (all_assumptions_of outer)) (all_assumptions_of inner);
+ drop_prefix (eq_snd (eq_list Thm.aconvc)) (apply2 all_assumptions_of (outer, inner))
+ |>> maps #2
+ |> check_result outer "assumption" Thm.term_of;
val local_assms_of = maps #2 oo local_assumptions_of;
fun local_prems_of inner outer =
- drop (length (all_prems_of outer)) (all_prems_of inner);
+ drop_prefix Thm.eq_thm_prop (apply2 all_prems_of (outer, inner))
+ |> check_result outer "premise" Thm.prop_of;
+
+end;
(* add assumptions *)
--- a/src/Pure/variable.ML Thu Sep 19 17:24:08 2019 +0100
+++ b/src/Pure/variable.ML Thu Sep 19 17:24:15 2019 +0100
@@ -58,6 +58,7 @@
val add_fixes_binding: binding list -> Proof.context -> string list * Proof.context
val add_fixes: string list -> Proof.context -> string list * Proof.context
val add_fixes_direct: string list -> Proof.context -> Proof.context
+ val add_fixes_implicit: term -> Proof.context -> Proof.context
val fix_dummy_patterns: term -> Proof.context -> term * Proof.context
val variant_fixes: string list -> Proof.context -> string list * Proof.context
val gen_all: Proof.context -> thm -> thm
@@ -475,6 +476,9 @@
|> (snd o add_fixes xs)
|> restore_body ctxt;
+fun add_fixes_implicit t ctxt = ctxt
+ |> not (is_body ctxt) ? add_fixes_direct (rev (add_free_names ctxt t []));
+
(* dummy patterns *)