--- a/NEWS Wed Jun 10 15:50:17 2015 +0200
+++ b/NEWS Wed Jun 10 18:57:31 2015 +0200
@@ -7,14 +7,40 @@
New in this Isabelle version
----------------------------
+*** Isar ***
+
+* Command 'obtain' binds term abbreviations (via 'is' patterns) in the
+proof body as well, abstracted over relevant parameters.
+
+* Term abbreviations via 'is' patterns also work for schematic
+statements: result is abstracted over unknowns.
+
+* Local goals ('have', 'show', 'hence', 'thus') allow structured
+statements like fixes/assumes/shows in theorem specifications, but the
+notation is postfix with keywords 'if' and 'for'. For example:
+
+ have result: "C x y"
+ if "A x" and "B y"
+ for x :: 'a and y :: 'a
+ <proof>
+
+The local assumptions are always bound to the name "prems". The result
+is exported from context of the statement as usual. The above roughly
+corresponds to a raw proof block like this:
+
+ {
+ fix x :: 'a and y :: 'a
+ assume prems: "A x" "B y"
+ have "C x y" <proof>
+ }
+ note result = this
+
+* New command 'supply' supports fact definitions during goal refinement
+('apply' scripts).
+
+
*** Pure ***
-* Isar command 'obtain' binds term abbreviations (via 'is' patterns) in
-the proof body as well, abstracted over the hypothetical parameters.
-
-* New Isar command 'supply' supports fact definitions during goal
-refinement ('apply' scripts).
-
* Configuration option rule_insts_schematic has been discontinued
(intermediate legacy feature in Isabelle2015). INCOMPATIBILITY.
--- a/src/Doc/Isar_Ref/Proof.thy Wed Jun 10 15:50:17 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy Wed Jun 10 18:57:31 2015 +0200
@@ -432,19 +432,22 @@
@{rail \<open>
(@@{command lemma} | @@{command theorem} | @@{command corollary} |
@@{command schematic_lemma} | @@{command schematic_theorem} |
- @@{command schematic_corollary}) (goal | statement)
+ @@{command schematic_corollary}) (stmt | statement)
;
- (@@{command have} | @@{command show} | @@{command hence} | @@{command thus}) goal
+ (@@{command have} | @@{command show} | @@{command hence} | @@{command thus})
+ stmt if_prems @{syntax for_fixes}
;
@@{command print_statement} @{syntax modes}? @{syntax thmrefs}
;
- goal: (@{syntax props} + @'and')
+ stmt: (@{syntax props} + @'and')
+ ;
+ if_prems: (@'if' stmt)?
;
statement: @{syntax thmdecl}? (@{syntax_ref "includes"}?) (@{syntax context_elem} *) \<newline>
conclusion
;
- conclusion: @'shows' goal | @'obtains' (@{syntax par_name}? obtain_case + '|')
+ conclusion: @'shows' stmt | @'obtains' (@{syntax par_name}? obtain_case + '|')
;
obtain_case: (@{syntax vars} + @'and') @'where' (@{syntax thmdecl}? (@{syntax prop}+) + @'and')
\<close>}
--- a/src/HOL/Eisbach/match_method.ML Wed Jun 10 15:50:17 2015 +0200
+++ b/src/HOL/Eisbach/match_method.ML Wed Jun 10 18:57:31 2015 +0200
@@ -114,7 +114,7 @@
let
val fixes' = map (fn ((pb, otyp), _) => (Parse_Tools.the_parse_val pb, otyp, NoSyn)) fixes;
val (fixes'', ctxt1) = fold_map Proof_Context.read_var fixes' ctxt;
- val (fix_nms, ctxt2) = Proof_Context.add_fixes fixes'' ctxt1;
+ val (fix_names, ctxt2) = Proof_Context.add_fixes fixes'' ctxt1;
val ctxt3 = Proof_Context.set_mode Proof_Context.mode_schematic ctxt2;
@@ -147,15 +147,14 @@
map2 (fn nm => fn (_, pos) =>
member (op =) pat_fixes nm orelse
error ("For-fixed variable must be bound in some pattern" ^ Position.here pos))
- fix_nms fixes;
+ fix_names fixes;
val _ = map (Term.map_types Type.no_tvars) pats;
val ctxt4 = fold Variable.declare_term pats ctxt3;
- val (Ts, ctxt5) = ctxt4 |> fold_map Proof_Context.inferred_param fix_nms;
-
- val real_fixes = map Free (fix_nms ~~ Ts);
+ val (real_fixes, ctxt5) = ctxt4
+ |> fold_map Proof_Context.inferred_param fix_names |>> map Free;
fun reject_extra_free (Free (x, _)) () =
if Variable.is_fixed ctxt5 x then ()
--- a/src/HOL/Eisbach/method_closure.ML Wed Jun 10 15:50:17 2015 +0200
+++ b/src/HOL/Eisbach/method_closure.ML Wed Jun 10 18:57:31 2015 +0200
@@ -338,11 +338,10 @@
|> fold setup_local_method methods
|> fold_map setup_local_fact uses;
- val ((xs, Ts), lthy2) = lthy1
+ val (term_args, lthy2) = lthy1
|> fold_map prep_var vars |-> Proof_Context.add_fixes
- |-> (fn xs => fold_map Proof_Context.inferred_param xs #>> pair xs);
+ |-> fold_map Proof_Context.inferred_param |>> map Free;
- val term_args = map Free (xs ~~ Ts);
val (named_thms, modifiers) = map (check_attrib lthy2) (attribs @ uses) |> split_list;
val self_name :: method_names = map (Local_Theory.full_name lthy2) (name :: methods);
--- a/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy Wed Jun 10 15:50:17 2015 +0200
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy Wed Jun 10 18:57:31 2015 +0200
@@ -420,7 +420,7 @@
show ?L
proof
fix x assume x: "x \<in> H"
- show "\<And>a b :: real. - a \<le> b \<Longrightarrow> b \<le> a \<Longrightarrow> \<bar>b\<bar> \<le> a"
+ show "- a \<le> b \<Longrightarrow> b \<le> a \<Longrightarrow> \<bar>b\<bar> \<le> a" for a b :: real
by arith
from \<open>linearform H h\<close> and H x
have "- h x = h (- x)" by (rule linearform.neg [symmetric])
--- a/src/HOL/Hahn_Banach/Subspace.thy Wed Jun 10 15:50:17 2015 +0200
+++ b/src/HOL/Hahn_Banach/Subspace.thy Wed Jun 10 18:57:31 2015 +0200
@@ -132,7 +132,7 @@
qed
fix x y assume x: "x \<in> U" and y: "y \<in> U"
from uv and x y show "x + y \<in> U" by (rule subspace.add_closed)
- from uv and x show "\<And>a. a \<cdot> x \<in> U" by (rule subspace.mult_closed)
+ from uv and x show "a \<cdot> x \<in> U" for a by (rule subspace.mult_closed)
qed
@@ -152,8 +152,10 @@
lemma linI' [iff]: "a \<cdot> x \<in> lin x"
unfolding lin_def by blast
-lemma linE [elim]: "x \<in> lin v \<Longrightarrow> (\<And>a::real. x = a \<cdot> v \<Longrightarrow> C) \<Longrightarrow> C"
- unfolding lin_def by blast
+lemma linE [elim]:
+ assumes "x \<in> lin v"
+ obtains a :: real where "x = a \<cdot> v"
+ using assms unfolding lin_def by blast
text \<open>Every vector is contained in its linear closure.\<close>
@@ -263,7 +265,7 @@
qed
fix x y assume x: "x \<in> U" and "y \<in> U"
then show "x + y \<in> U" by simp
- from x show "\<And>a. a \<cdot> x \<in> U" by simp
+ from x show "a \<cdot> x \<in> U" for a by simp
qed
qed
--- a/src/HOL/Isar_Examples/Hoare_Ex.thy Wed Jun 10 15:50:17 2015 +0200
+++ b/src/HOL/Isar_Examples/Hoare_Ex.thy Wed Jun 10 18:57:31 2015 +0200
@@ -99,7 +99,7 @@
lemma "\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M := \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>"
proof -
- have "\<And>m n::nat. m = n \<longrightarrow> m + 1 \<noteq> n"
+ have "m = n \<longrightarrow> m + 1 \<noteq> n" for m n :: nat
-- \<open>inclusion of assertions expressed in ``pure'' logic,\<close>
-- \<open>without mentioning the state space\<close>
by simp
@@ -192,13 +192,13 @@
also have "\<turnstile> \<dots> ?while \<lbrace>?inv \<acute>S \<acute>I \<and> \<not> \<acute>I \<noteq> n\<rbrace>"
proof
let ?body = "\<acute>S := \<acute>S + \<acute>I; \<acute>I := \<acute>I + 1"
- have "\<And>s i. ?inv s i \<and> i \<noteq> n \<longrightarrow> ?inv (s + i) (i + 1)"
+ have "?inv s i \<and> i \<noteq> n \<longrightarrow> ?inv (s + i) (i + 1)" for s i
by simp
also have "\<turnstile> \<lbrace>\<acute>S + \<acute>I = ?sum (\<acute>I + 1)\<rbrace> ?body \<lbrace>?inv \<acute>S \<acute>I\<rbrace>"
by hoare
finally show "\<turnstile> \<lbrace>?inv \<acute>S \<acute>I \<and> \<acute>I \<noteq> n\<rbrace> ?body \<lbrace>?inv \<acute>S \<acute>I\<rbrace>" .
qed
- also have "\<And>s i. s = ?sum i \<and> \<not> i \<noteq> n \<longrightarrow> s = ?sum n"
+ also have "s = ?sum i \<and> \<not> i \<noteq> n \<longrightarrow> s = ?sum n" for s i
by simp
finally show ?thesis .
qed
@@ -220,18 +220,13 @@
proof -
let ?sum = "\<lambda>k::nat. \<Sum>j<k. j"
let ?inv = "\<lambda>s i::nat. s = ?sum i"
-
show ?thesis
proof hoare
show "?inv 0 1" by simp
- next
- fix s i
- assume "?inv s i \<and> i \<noteq> n"
- then show "?inv (s + i) (i + 1)" by simp
- next
- fix s i
- assume "?inv s i \<and> \<not> i \<noteq> n"
- then show "s = ?sum n" by simp
+ show "?inv (s + i) (i + 1)" if "?inv s i \<and> i \<noteq> n" for s i
+ using prems by simp
+ show "s = ?sum n" if "?inv s i \<and> \<not> i \<noteq> n" for s i
+ using prems by simp
qed
qed
--- a/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy Wed Jun 10 15:50:17 2015 +0200
+++ b/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy Wed Jun 10 18:57:31 2015 +0200
@@ -208,11 +208,8 @@
let ?e = evnodd
note hyp = \<open>card (?e t 0) = card (?e t 1)\<close>
and at = \<open>a \<subseteq> - t\<close>
- have card_suc:
- "\<And>b. b < 2 \<Longrightarrow> card (?e (a \<union> t) b) = Suc (card (?e t b))"
+ have card_suc: "card (?e (a \<union> t) b) = Suc (card (?e t b))" if "b < 2" for b :: nat
proof -
- fix b :: nat
- assume "b < 2"
have "?e (a \<union> t) b = ?e a b \<union> ?e t b" by (rule evnodd_Un)
also obtain i j where e: "?e a b = {(i, j)}"
proof -
@@ -230,7 +227,7 @@
from e have "(i, j) \<in> ?e a b" by simp
with at show "(i, j) \<notin> ?e t b" by (blast dest: evnoddD)
qed
- finally show "?thesis b" .
+ finally show ?thesis .
qed
then have "card (?e (a \<union> t) 0) = Suc (card (?e t 0))" by simp
also from hyp have "card (?e t 0) = card (?e t 1)" .
--- a/src/HOL/Isar_Examples/Nested_Datatype.thy Wed Jun 10 15:50:17 2015 +0200
+++ b/src/HOL/Isar_Examples/Nested_Datatype.thy Wed Jun 10 18:57:31 2015 +0200
@@ -37,17 +37,12 @@
subst_term_list f1 (subst_term_list f2 ts)"
show ?thesis
proof (induct t rule: subst_term.induct)
- fix a show "?P (Var a)" by simp
- next
- fix b ts assume "?Q ts"
- then show "?P (App b ts)"
- by (simp only: subst_simps)
- next
+ show "?P (Var a)" for a by simp
+ show "?P (App b ts)" if "?Q ts" for b ts
+ using prems by (simp only: subst_simps)
show "?Q []" by simp
- next
- fix t ts
- assume "?P t" "?Q ts" then show "?Q (t # ts)"
- by (simp only: subst_simps)
+ show "?Q (t # ts)" if "?P t" "?Q ts" for t ts
+ using prems by (simp only: subst_simps)
qed
qed
--- a/src/HOL/Isar_Examples/Puzzle.thy Wed Jun 10 15:50:17 2015 +0200
+++ b/src/HOL/Isar_Examples/Puzzle.thy Wed Jun 10 18:57:31 2015 +0200
@@ -16,52 +16,46 @@
assumes f_ax: "\<And>n. f (f n) < f (Suc n)"
shows "f n = n"
proof (rule order_antisym)
- {
- fix n show "n \<le> f n"
- proof (induct "f n" arbitrary: n rule: less_induct)
- case less
- show "n \<le> f n"
- proof (cases n)
- case (Suc m)
- from f_ax have "f (f m) < f n" by (simp only: Suc)
- with less have "f m \<le> f (f m)" .
- also from f_ax have "\<dots> < f n" by (simp only: Suc)
- finally have "f m < f n" .
- with less have "m \<le> f m" .
- also note \<open>\<dots> < f n\<close>
- finally have "m < f n" .
- then have "n \<le> f n" by (simp only: Suc)
- then show ?thesis .
- next
- case 0
- then show ?thesis by simp
- qed
+ show ge: "n \<le> f n" for n
+ proof (induct "f n" arbitrary: n rule: less_induct)
+ case less
+ show "n \<le> f n"
+ proof (cases n)
+ case (Suc m)
+ from f_ax have "f (f m) < f n" by (simp only: Suc)
+ with less have "f m \<le> f (f m)" .
+ also from f_ax have "\<dots> < f n" by (simp only: Suc)
+ finally have "f m < f n" .
+ with less have "m \<le> f m" .
+ also note \<open>\<dots> < f n\<close>
+ finally have "m < f n" .
+ then have "n \<le> f n" by (simp only: Suc)
+ then show ?thesis .
+ next
+ case 0
+ then show ?thesis by simp
qed
- } note ge = this
+ qed
- {
- fix m n :: nat
- assume "m \<le> n"
- then have "f m \<le> f n"
- proof (induct n)
- case 0
- then have "m = 0" by simp
- then show ?case by simp
+ have mono: "m \<le> n \<Longrightarrow> f m \<le> f n" for m n :: nat
+ proof (induct n)
+ case 0
+ then have "m = 0" by simp
+ then show ?case by simp
+ next
+ case (Suc n)
+ from Suc.prems show "f m \<le> f (Suc n)"
+ proof (rule le_SucE)
+ assume "m \<le> n"
+ with Suc.hyps have "f m \<le> f n" .
+ also from ge f_ax have "\<dots> < f (Suc n)"
+ by (rule le_less_trans)
+ finally show ?thesis by simp
next
- case (Suc n)
- from Suc.prems show "f m \<le> f (Suc n)"
- proof (rule le_SucE)
- assume "m \<le> n"
- with Suc.hyps have "f m \<le> f n" .
- also from ge f_ax have "\<dots> < f (Suc n)"
- by (rule le_less_trans)
- finally show ?thesis by simp
- next
- assume "m = Suc n"
- then show ?thesis by simp
- qed
+ assume "m = Suc n"
+ then show ?thesis by simp
qed
- } note mono = this
+ qed
show "f n \<le> n"
proof -
--- a/src/Pure/Isar/auto_bind.ML Wed Jun 10 15:50:17 2015 +0200
+++ b/src/Pure/Isar/auto_bind.ML Wed Jun 10 18:57:31 2015 +0200
@@ -8,10 +8,12 @@
sig
val thesisN: string
val thisN: string
+ val premsN: string
val assmsN: string
+ val abs_params: term -> term -> term
val goal: Proof.context -> term list -> (indexname * term option) list
val facts: Proof.context -> term list -> (indexname * term option) list
- val no_facts: (indexname * term option) list
+ val no_facts: indexname list
end;
structure Auto_Bind: AUTO_BIND =
@@ -22,11 +24,14 @@
val thesisN = "thesis";
val thisN = "this";
val assmsN = "assms";
+val premsN = "prems";
fun strip_judgment ctxt = Object_Logic.drop_judgment ctxt o Logic.strip_assums_concl;
+fun abs_params prop = fold_rev Term.abs (Logic.strip_params prop);
+
fun statement_binds ctxt name prop =
- [((name, 0), SOME (fold_rev Term.abs (Logic.strip_params prop) (strip_judgment ctxt prop)))];
+ [((name, 0), SOME (abs_params prop (strip_judgment ctxt prop)))];
(* goal *)
@@ -39,14 +44,15 @@
fun get_arg ctxt prop =
(case strip_judgment ctxt prop of
- _ $ t => SOME (fold_rev Term.abs (Logic.strip_params prop) t)
+ _ $ t => SOME (abs_params prop t)
| _ => NONE);
-fun facts _ [] = []
- | facts ctxt props =
- let val prop = List.last props
- in [(Syntax_Ext.dddot_indexname, get_arg ctxt prop)] @ statement_binds ctxt thisN prop end;
+fun facts ctxt props =
+ (case try List.last props of
+ NONE => []
+ | SOME prop =>
+ [(Syntax_Ext.dddot_indexname, get_arg ctxt prop)] @ statement_binds ctxt thisN prop);
-val no_facts = [(Syntax_Ext.dddot_indexname, NONE), ((thisN, 0), NONE)];
+val no_facts = [Syntax_Ext.dddot_indexname, (thisN, 0)];
end;
--- a/src/Pure/Isar/element.ML Wed Jun 10 15:50:17 2015 +0200
+++ b/src/Pure/Isar/element.ML Wed Jun 10 18:57:31 2015 +0200
@@ -278,10 +278,15 @@
in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end;
in proof after_qed' propss #> refine_witness #> Seq.hd end;
-fun proof_local cmd goal_ctxt int after_qed' propp =
- Proof.map_context (K goal_ctxt) #>
- Proof.local_goal (K (K ())) (K I) Proof_Context.cert_propp cmd NONE
- after_qed' (map (pair Thm.empty_binding) propp);
+fun proof_local cmd goal_ctxt int after_qed propp =
+ let
+ fun after_qed' (result_ctxt, results) state' =
+ after_qed (burrow (Proof_Context.export result_ctxt (Proof.context_of state')) results) state';
+ in
+ Proof.map_context (K goal_ctxt) #>
+ Proof.internal_goal (K (K ())) (Proof_Context.get_mode goal_ctxt) cmd
+ NONE after_qed' [] [] (map (pair Thm.empty_binding) propp)
+ end;
in
--- a/src/Pure/Isar/expression.ML Wed Jun 10 15:50:17 2015 +0200
+++ b/src/Pure/Isar/expression.ML Wed Jun 10 18:57:31 2015 +0200
@@ -410,11 +410,12 @@
val (elems, ctxt5) = fold_map prep_elem raw_elems ctxt4;
val (insts, elems', concl, ctxt6) = prep_concl raw_concl (insts', elems, ctxt5);
- (* Retrieve parameter types *)
+
+ (* parameters from expression and elements *)
+
val xs = maps (fn Fixes fixes => map (Variable.check_name o #1) fixes | _ => [])
(Fixes fors :: elems');
- val (Ts, ctxt7) = fold_map Proof_Context.inferred_param xs ctxt6;
- val parms = xs ~~ Ts; (* params from expression and elements *)
+ val (parms, ctxt7) = fold_map Proof_Context.inferred_param xs ctxt6;
val fors' = finish_fixes parms fors;
val fixed = map (fn (b, SOME T, mx) => ((Binding.name_of b, T), mx)) fors';
--- a/src/Pure/Isar/isar_cmd.ML Wed Jun 10 15:50:17 2015 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Wed Jun 10 18:57:31 2015 +0200
@@ -173,21 +173,10 @@
|> Context.proof_map;
-(* goals *)
-
-fun goal opt_chain goal stmt int =
- opt_chain #> goal NONE (K I) stmt int;
-
-val have = goal I Proof.have_cmd;
-val hence = goal Proof.chain Proof.have_cmd;
-val show = goal I Proof.show_cmd;
-val thus = goal Proof.chain Proof.show_cmd;
-
-
(* local endings *)
fun local_qed m = Toplevel.proof (Proof.local_qed (m, true));
-val local_terminal_proof = Toplevel.proof' o Proof.local_future_terminal_proof;
+val local_terminal_proof = Toplevel.proof o Proof.local_future_terminal_proof;
val local_default_proof = Toplevel.proof Proof.local_default_proof;
val local_immediate_proof = Toplevel.proof Proof.local_immediate_proof;
val local_done_proof = Toplevel.proof Proof.local_done_proof;
@@ -199,7 +188,7 @@
(* global endings *)
fun global_qed m = Toplevel.end_proof (K (Proof.global_qed (m, true)));
-val global_terminal_proof = Toplevel.end_proof o Proof.global_future_terminal_proof;
+val global_terminal_proof = Toplevel.end_proof o K o Proof.global_future_terminal_proof;
val global_default_proof = Toplevel.end_proof (K Proof.global_default_proof);
val global_immediate_proof = Toplevel.end_proof (K Proof.global_immediate_proof);
val global_skip_proof = Toplevel.end_proof Proof.global_skip_proof;
--- a/src/Pure/Isar/isar_syn.ML Wed Jun 10 15:50:17 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML Wed Jun 10 18:57:31 2015 +0200
@@ -464,6 +464,11 @@
(** proof commands **)
+val _ =
+ Outer_Syntax.local_theory_to_proof @{command_keyword notepad} "begin proof context"
+ (Parse.begin >> K Proof.begin_notepad);
+
+
(* statements *)
fun theorem spec schematic kind =
@@ -484,28 +489,29 @@
val _ = theorem @{command_keyword schematic_lemma} true Thm.lemmaK;
val _ = theorem @{command_keyword schematic_corollary} true Thm.corollaryK;
-val _ =
- Outer_Syntax.local_theory_to_proof @{command_keyword notepad} "begin proof context"
- (Parse.begin >> K Proof.begin_notepad);
+
+val structured_statement =
+ Parse_Spec.statement -- Parse_Spec.if_prems -- Parse.for_fixes >> (fn ((a, b), c) => (c, b, a));
val _ =
Outer_Syntax.command @{command_keyword have} "state local goal"
- (Parse_Spec.statement >> (Toplevel.proof' o Proof.have_cmd NONE (K I)));
+ (structured_statement >> (fn (fixes, assumes, shows) =>
+ Toplevel.proof' (fn int => Proof.have_cmd NONE (K I) fixes assumes shows int)));
+
+val _ =
+ Outer_Syntax.command @{command_keyword show} "state local goal, to refine pending subgoals"
+ (structured_statement >> (fn (fixes, assumes, shows) =>
+ Toplevel.proof' (fn int => Proof.show_cmd NONE (K I) fixes assumes shows int)));
val _ =
Outer_Syntax.command @{command_keyword hence} "old-style alias of \"then have\""
- (Parse_Spec.statement >> (fn stmt =>
- Toplevel.proof' (fn int => Proof.chain #> Proof.have_cmd NONE (K I) stmt int)));
-
-val _ =
- Outer_Syntax.command @{command_keyword show}
- "state local goal, solving current obligation"
- (Parse_Spec.statement >> (Toplevel.proof' o Proof.show_cmd NONE (K I)));
+ (structured_statement >> (fn (fixes, assumes, shows) =>
+ Toplevel.proof' (fn int => Proof.chain #> Proof.have_cmd NONE (K I) fixes assumes shows int)));
val _ =
Outer_Syntax.command @{command_keyword thus} "old-style alias of \"then show\""
- (Parse_Spec.statement >> (fn stmt =>
- Toplevel.proof' (fn int => Proof.chain #> Proof.show_cmd NONE (K I) stmt int)));
+ (structured_statement >> (fn (fixes, assumes, shows) =>
+ Toplevel.proof' (fn int => Proof.chain #> Proof.show_cmd NONE (K I) fixes assumes shows int)));
(* facts *)
--- a/src/Pure/Isar/obtain.ML Wed Jun 10 15:50:17 2015 +0200
+++ b/src/Pure/Isar/obtain.ML Wed Jun 10 18:57:31 2015 +0200
@@ -119,23 +119,23 @@
val xs = map (Variable.check_name o #1) vars;
(*obtain asms*)
- val (asm_propss, binds) = prep_propp fix_ctxt (map snd raw_asms);
- val asm_props = flat asm_propss;
- val declare_asms = fold Variable.declare_term asm_props #> Proof_Context.bind_terms binds;
+ val (propss, binds) = prep_propp fix_ctxt (map snd raw_asms);
+ val props = flat propss;
+ val declare_asms =
+ fold Variable.declare_term props #>
+ fold Variable.bind_term binds;
val asms =
map (fn ((b, raw_atts), _) => (b, map (prep_att fix_ctxt) raw_atts)) raw_asms ~~
- map (map (rpair [])) asm_propss;
+ map (map (rpair [])) propss;
(*obtain params*)
- val (Ts, params_ctxt) = fold_map Proof_Context.inferred_param xs' (declare_asms fix_ctxt);
- val params = map Free (xs' ~~ Ts);
+ val (params, params_ctxt) =
+ declare_asms fix_ctxt |> fold_map Proof_Context.inferred_param xs' |>> map Free;
val cparams = map (Thm.cterm_of params_ctxt) params;
+ val binds' = (map o apsnd) (fold_rev Term.dependent_lambda_name (xs ~~ params)) binds;
+
val _ = Variable.warn_extra_tfrees fix_ctxt params_ctxt;
- (*abstracted term bindings*)
- val abs_term = Term.close_schematic_term o fold_rev Term.lambda_name (xs ~~ params);
- val binds' = map (apsnd abs_term) binds;
-
(*obtain statements*)
val thesisN = singleton (Name.variant_list xs) Auto_Bind.thesisN;
val (thesis_var, thesis) = #1 (bind_judgment params_ctxt thesisN);
@@ -143,7 +143,7 @@
val that_name = if name = "" then thatN else name;
val that_prop =
Logic.list_rename_params xs
- (fold_rev Logic.all params (Logic.list_implies (asm_props, thesis)));
+ (fold_rev Logic.all params (Logic.list_implies (props, thesis)));
val obtain_prop =
Logic.list_rename_params [Auto_Bind.thesisN]
(Logic.all (Free thesis_var) (Logic.mk_implies (that_prop, thesis)));
@@ -157,15 +157,15 @@
in
state
|> Proof.enter_forward
- |> Proof.have NONE (K I) [(Thm.empty_binding, [(obtain_prop, [])])] int
- |> Proof.map_context (Proof_Context.bind_terms binds')
+ |> Proof.have NONE (K I) [] [] [(Thm.empty_binding, [(obtain_prop, [])])] int
+ |> Proof.map_context (fold Variable.bind_term binds')
|> Proof.proof (SOME Method.succeed_text) |> Seq.hd
|> Proof.fix [(Binding.name thesisN, NONE, NoSyn)]
|> Proof.assume
[((Binding.name that_name, [Context_Rules.intro_query NONE]), [(that_prop, [])])]
|> `Proof.the_facts
||> Proof.chain_facts chain_facts
- ||> Proof.show NONE after_qed [(Thm.empty_binding, [(thesis, [])])] false
+ ||> Proof.show NONE after_qed [] [] [(Thm.empty_binding, [(thesis, [])])] false
|-> Proof.refine_insert
end;
@@ -261,7 +261,7 @@
fun inferred_type (binding, _, mx) ctxt =
let
val x = Variable.check_name binding;
- val (T, ctxt') = Proof_Context.inferred_param x ctxt
+ val ((_, T), ctxt') = Proof_Context.inferred_param x ctxt
in ((x, T, mx), ctxt') end;
fun polymorphic ctxt vars =
@@ -297,7 +297,7 @@
|> `Proof.context_of |-> (fn fix_ctxt => Proof.assm
(obtain_export fix_ctxt rule (map (Thm.cterm_of ctxt) ts))
[(Thm.empty_binding, asms)])
- |> Proof.map_context (Proof_Context.maybe_bind_terms Auto_Bind.no_facts)
+ |> Proof.map_context (fold Variable.unbind_term Auto_Bind.no_facts)
end;
val goal = Var (("guess", 0), propT);
@@ -308,16 +308,21 @@
Method.primitive_text (fn ctxt =>
Goal.conclude #> Raw_Simplifier.norm_hhf ctxt #>
(fn th => Goal.protect 0 (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th)));
- fun after_qed [[_, res]] =
- Proof.end_block #> guess_context (check_result ctxt thesis res);
+ fun after_qed (result_ctxt, results) state' =
+ let val [_, res] = Proof_Context.export result_ctxt (Proof.context_of state') (flat results)
+ in
+ state'
+ |> Proof.end_block
+ |> guess_context (check_result ctxt thesis res)
+ end;
in
state
|> Proof.enter_forward
|> Proof.begin_block
|> Proof.fix [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)]
|> Proof.chain_facts chain_facts
- |> Proof.local_goal print_result (K I) (K (rpair []))
- "guess" (SOME before_qed) after_qed [(Thm.empty_binding, [Logic.mk_term goal, goal])]
+ |> Proof.internal_goal print_result Proof_Context.mode_schematic "guess"
+ (SOME before_qed) after_qed [] [] [(Thm.empty_binding, [(Logic.mk_term goal, []), (goal, [])])]
|> Proof.refine (Method.primitive_text (fn _ => fn _ =>
Goal.init (Thm.cterm_of ctxt thesis))) |> Seq.hd
end;
--- a/src/Pure/Isar/parse_spec.ML Wed Jun 10 15:50:17 2015 +0200
+++ b/src/Pure/Isar/parse_spec.ML Wed Jun 10 18:57:31 2015 +0200
@@ -24,6 +24,7 @@
val locale_expression: bool -> Expression.expression parser
val context_element: Element.context parser
val statement: (Attrib.binding * (string * string list) list) list parser
+ val if_prems: (Attrib.binding * (string * string list) list) list parser
val general_statement: (Element.context list * Element.statement) parser
val statement_keyword: string parser
end;
@@ -131,6 +132,8 @@
val statement = Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp);
+val if_prems = Scan.optional (Parse.$$$ "if" |-- Parse.!!! statement) [];
+
val obtain_case =
Parse.parbinding --
(Scan.optional (Parse.and_list1 Parse.params --| Parse.where_ >> flat) [] --
--- a/src/Pure/Isar/proof.ML Wed Jun 10 15:50:17 2015 +0200
+++ b/src/Pure/Isar/proof.ML Wed Jun 10 18:57:31 2015 +0200
@@ -33,11 +33,10 @@
val enter_chain: state -> state
val enter_backward: state -> state
val has_bottom_goal: state -> bool
- val pretty_state: int -> state -> Pretty.T list
+ val pretty_state: state -> Pretty.T list
val refine: Method.text -> state -> state Seq.seq
val refine_end: Method.text -> state -> state Seq.seq
val refine_insert: thm list -> state -> state
- val refine_goals: (context -> thm -> unit) -> context -> thm list -> state -> state Seq.seq
val raw_goal: state -> {context: context, facts: thm list, goal: thm}
val goal: state -> {context: context, facts: thm list, goal: thm}
val simple_goal: state -> {context: context, goal: thm}
@@ -89,11 +88,6 @@
val apply_end: Method.text -> state -> state Seq.seq
val apply_results: Method.text_range -> state -> state Seq.result Seq.seq
val apply_end_results: Method.text_range -> state -> state Seq.result Seq.seq
- val local_goal: (context -> ((string * string) * (string * thm list) list) -> unit) ->
- (context -> 'a -> attribute) ->
- (context -> 'b list -> (term list list * (indexname * term) list)) ->
- string -> Method.text option -> (thm list list -> state -> state) ->
- ((binding * 'a list) * 'b) list -> state -> state
val local_qed: Method.text_range option * bool -> state -> state
val theorem: Method.text option -> (thm list list -> context -> context) ->
(term * term list) list list -> context -> state
@@ -110,21 +104,33 @@
val global_immediate_proof: state -> context
val global_skip_proof: bool -> state -> context
val global_done_proof: state -> context
- val have: Method.text option -> (thm list list -> state -> state) ->
+ val internal_goal: (context -> (string * string) * (string * thm list) list -> unit) ->
+ Proof_Context.mode -> string -> Method.text option ->
+ (context * thm list list -> state -> state) ->
+ (binding * typ option * mixfix) list ->
+ (Thm.binding * (term * term list) list) list ->
+ (Thm.binding * (term * term list) list) list -> state -> state
+ val have: Method.text option -> (context * thm list list -> state -> state) ->
+ (binding * typ option * mixfix) list ->
+ (Thm.binding * (term * term list) list) list ->
(Thm.binding * (term * term list) list) list -> bool -> state -> state
- val have_cmd: Method.text option -> (thm list list -> state -> state) ->
+ val have_cmd: Method.text option -> (context * thm list list -> state -> state) ->
+ (binding * string option * mixfix) list ->
+ (Attrib.binding * (string * string list) list) list ->
(Attrib.binding * (string * string list) list) list -> bool -> state -> state
- val show: Method.text option -> (thm list list -> state -> state) ->
+ val show: Method.text option -> (context * thm list list -> state -> state) ->
+ (binding * typ option * mixfix) list ->
+ (Thm.binding * (term * term list) list) list ->
(Thm.binding * (term * term list) list) list -> bool -> state -> state
- val show_cmd: Method.text option -> (thm list list -> state -> state) ->
+ val show_cmd: Method.text option -> (context * thm list list -> state -> state) ->
+ (binding * string option * mixfix) list ->
+ (Attrib.binding * (string * string list) list) list ->
(Attrib.binding * (string * string list) list) list -> bool -> state -> state
val schematic_goal: state -> bool
val is_relevant: state -> bool
val future_proof: (state -> ('a * context) future) -> state -> 'a future * state
- val local_future_terminal_proof: Method.text_range * Method.text_range option -> bool ->
- state -> state
- val global_future_terminal_proof: Method.text_range * Method.text_range option -> bool ->
- state -> context
+ val local_future_terminal_proof: Method.text_range * Method.text_range option -> state -> state
+ val global_future_terminal_proof: Method.text_range * Method.text_range option -> state -> context
end;
structure Proof: PROOF =
@@ -156,8 +162,8 @@
goal: thm, (*subgoals ==> statement*)
before_qed: Method.text option,
after_qed:
- (thm list list -> state -> state) *
- (thm list list -> context -> context)};
+ ((context * thm list list) -> state -> state) *
+ ((context * thm list list) -> context -> context)};
fun make_goal (statement, using, goal, before_qed, after_qed) =
Goal {statement = statement, using = using, goal = goal,
@@ -282,7 +288,7 @@
fun current_goal state =
(case top state of
- {context, goal = SOME (Goal goal), ...} => (context, goal)
+ {context = ctxt, goal = SOME (Goal goal), ...} => (ctxt, goal)
| _ => error "No current goal");
fun assert_current_goal g state =
@@ -362,13 +368,12 @@
in
-fun pretty_state nr state =
+fun pretty_state state =
let
val {context = ctxt, facts, mode, goal = _} = top state;
val verbose = Config.get ctxt Proof_Context.verbose;
- fun prt_goal (SOME (_, (_,
- {statement = ((_, pos), _, _), using, goal, before_qed = _, after_qed = _}))) =
+ fun prt_goal (SOME (_, (_, {using, goal, ...}))) =
pretty_sep
(pretty_facts ctxt "using"
(if mode <> Backward orelse null using then NONE else SOME using))
@@ -455,13 +460,13 @@
in
-fun refine_goals print_rule inner raw_rules state =
+fun refine_goals print_rule result_ctxt result state =
let
- val (outer, (_, goal)) = get_goal state;
- fun refine rule st = (print_rule outer rule; FINDGOAL (goal_tac outer rule) st);
+ val (goal_ctxt, (_, goal)) = get_goal state;
+ fun refine rule st = (print_rule goal_ctxt rule; FINDGOAL (goal_tac goal_ctxt rule) st);
in
- raw_rules
- |> Proof_Context.goal_export inner outer
+ result
+ |> Proof_Context.goal_export result_ctxt goal_ctxt
|> (fn rules => Seq.lift provide_goal (EVERY (map refine rules) goal) state)
end;
@@ -769,7 +774,7 @@
in
state'
|> assume assumptions
- |> map_context (Proof_Context.maybe_bind_terms Auto_Bind.no_facts)
+ |> map_context (fold Variable.unbind_term Auto_Bind.no_facts)
|> `the_facts |-> (fn thms => note_thmss [((Binding.make (name, pos), []), [(thms, [])])])
end;
@@ -910,90 +915,133 @@
in
-fun generic_goal prep_propp kind before_qed after_qed propp state =
+fun generic_goal kind before_qed after_qed goal_ctxt goal_propss result_binds state =
let
- val ctxt = context_of state;
val chaining = can assert_chain state;
val pos = Position.thread_data ();
- val (propss, binds) = prep_propp ctxt propp;
- val props = flat propss;
-
val goal_state =
state
|> assert_forward_or_chain
|> enter_forward
|> open_block
- |> map_context (fold Variable.auto_fixes props #> Proof_Context.bind_terms binds);
- val goal_ctxt = context_of goal_state;
+ |> map_context (K goal_ctxt);
+ val goal_props = flat goal_propss;
- val vars = implicit_vars props;
- val propss' = vars :: propss;
+ val vars = implicit_vars goal_props;
+ val propss' = vars :: goal_propss;
val goal_propss = filter_out null propss';
val goal =
Logic.mk_conjunction_balanced (map Logic.mk_conjunction_balanced goal_propss)
- |> Thm.cterm_of ctxt
+ |> Thm.cterm_of goal_ctxt
|> Thm.weaken_sorts (Variable.sorts_of goal_ctxt);
val statement = ((kind, pos), propss', Thm.term_of goal);
+
val after_qed' = after_qed |>> (fn after_local => fn results =>
- map_context (Proof_Context.export_bind_terms binds goal_ctxt) #> after_local results);
+ map_context (fold Variable.maybe_bind_term result_binds) #> after_local results);
in
goal_state
|> map_context (init_context #> Variable.set_body true)
|> set_goal (make_goal (statement, [], Goal.init goal, before_qed, after_qed'))
- |> map_context (Proof_Context.auto_bind_goal props)
+ |> map_context (Proof_Context.auto_bind_goal goal_props)
|> chaining ? (`the_facts #-> using_facts)
|> reset_facts
|> open_block
|> reset_goal
|> enter_backward
|> not (null vars) ? refine_terms (length goal_propss)
- |> null props ? (refine (Method.Basic Method.assumption) #> Seq.hd)
+ |> null goal_props ? (refine (Method.Basic Method.assumption) #> Seq.hd)
end;
-fun generic_qed after_ctxt state =
+fun generic_qed state =
let
- val (goal_ctxt, {statement = (_, stmt, _), goal, after_qed, ...}) = current_goal state;
- val outer_state = state |> close_block;
- val outer_ctxt = context_of outer_state;
-
- val props =
- flat (tl stmt)
- |> Variable.exportT_terms goal_ctxt outer_ctxt;
- val results =
- tl (conclude_goal goal_ctxt goal stmt)
- |> burrow (Proof_Context.export goal_ctxt outer_ctxt);
- in
- outer_state
- |> map_context (after_ctxt props)
- |> pair (after_qed, results)
- end;
+ val (goal_ctxt, {statement = (_, propss, _), goal, after_qed, ...}) =
+ current_goal state;
+ val results = tl (conclude_goal goal_ctxt goal propss);
+ in state |> close_block |> pair (after_qed, (goal_ctxt, results)) end;
end;
(* local goals *)
-fun local_goal print_results prep_att prep_propp kind before_qed after_qed stmt state =
+local
+
+fun export_binds ctxt' ctxt binds =
+ let
+ val rhss =
+ map (the_list o snd) binds
+ |> burrow (Variable.export_terms ctxt' ctxt)
+ |> map (try the_single);
+ in map fst binds ~~ rhss end;
+
+in
+
+fun local_goal print_results prep_att prep_propp prep_var
+ kind before_qed after_qed raw_fixes raw_assumes raw_shows state =
let
- val ((names, attss), propp) =
- Attrib.map_specs (map (prep_att (context_of state))) stmt |> split_list |>> split_list;
+ val ctxt = context_of state;
+
+ val (assumes_bindings, shows_bindings) =
+ apply2 (map (apsnd (map (prep_att ctxt)) o fst)) (raw_assumes, raw_shows);
+ val (assumes_propp, shows_propp) = apply2 (map snd) (raw_assumes, raw_shows);
+
+ val (goal_ctxt, goal_propss, result_binds) =
+ let
+ (*fixed variables*)
+ val ((xs', vars), fix_ctxt) = ctxt
+ |> fold_map prep_var raw_fixes
+ |-> (fn vars => Proof_Context.add_fixes vars ##>> pair vars);
+
+ (*propositions with term bindings*)
+ val (all_propss, binds) = prep_propp fix_ctxt (assumes_propp @ shows_propp);
+ val (assumes_propss, shows_propss) = chop (length assumes_propp) all_propss;
- fun after_qed' results =
- local_results ((names ~~ attss) ~~ results)
- #-> (fn res => tap (fn st => print_results (context_of st) ((kind, ""), res) : unit))
- #> after_qed results;
- in
- state
- |> map_context (Variable.set_body true)
- |> generic_goal prep_propp kind before_qed (after_qed', K I) propp
- |> tap (Variable.warn_extra_tfrees (context_of state) o context_of)
- end;
+ (*params*)
+ val (ps, params_ctxt) = fix_ctxt
+ |> (fold o fold) Variable.declare_term all_propss
+ |> fold Variable.bind_term binds
+ |> fold_map Proof_Context.inferred_param xs';
+ val xs = map (Variable.check_name o #1) vars;
+ val params = xs ~~ map Free ps;
+
+ (*prems*)
+ val goal_ctxt = params_ctxt
+ |> fold_burrow (Assumption.add_assms Assumption.assume_export)
+ ((map o map) (Thm.cterm_of params_ctxt) assumes_propss)
+ |> (fn (premss, ctxt') => ctxt'
+ |> not (null assumes_propss) ?
+ (snd o Proof_Context.note_thmss ""
+ [((Binding.name Auto_Bind.premsN, []),
+ [(Assumption.local_prems_of ctxt' ctxt, [])])])
+ |> (snd o Proof_Context.note_thmss ""
+ (assumes_bindings ~~ map (map (fn th => ([th], []))) premss)));
+
+ val _ = Variable.warn_extra_tfrees fix_ctxt goal_ctxt;
+
+ (*result term bindings*)
+ val shows_props = flat shows_propss;
+ val binds' =
+ (case try List.last shows_props of
+ NONE => []
+ | SOME prop => map (apsnd (SOME o Auto_Bind.abs_params prop)) binds);
+ val result_binds =
+ (Auto_Bind.facts goal_ctxt shows_props @ binds')
+ |> (map o apsnd o Option.map) (fold_rev Term.dependent_lambda_name params)
+ |> export_binds goal_ctxt ctxt;
+ in (goal_ctxt, shows_propss, result_binds) end;
+
+ fun after_qed' (result_ctxt, results) state' = state'
+ |> local_results (shows_bindings ~~ burrow (Proof_Context.export result_ctxt ctxt) results)
+ |-> (fn res => tap (fn st => print_results (context_of st) ((kind, ""), res) : unit))
+ |> after_qed (result_ctxt, results);
+ in generic_goal kind before_qed (after_qed', K I) goal_ctxt goal_propss result_binds state end;
+
+end;
fun local_qeds arg =
end_proof false arg
- #> Seq.map_result (generic_qed Proof_Context.auto_bind_facts #->
- (fn ((after_qed, _), results) => after_qed results));
+ #> Seq.map_result (generic_qed #-> (fn ((after_qed, _), results) => after_qed results));
fun local_qed arg =
local_qeds (Position.none, arg) #> Seq.the_result finished_goal_error;
@@ -1001,17 +1049,27 @@
(* global goals *)
-fun global_goal prep_propp before_qed after_qed propp =
- init
- #> generic_goal (prep_propp o Proof_Context.set_mode Proof_Context.mode_schematic) ""
- before_qed (K I, after_qed) propp;
+fun global_goal prep_propp before_qed after_qed propp ctxt =
+ let
+ val (propss, binds) =
+ prep_propp (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) propp;
+ val goal_ctxt = ctxt
+ |> (fold o fold) Variable.auto_fixes propss
+ |> fold Variable.bind_term binds;
+ fun after_qed' (result_ctxt, results) ctxt' =
+ after_qed (burrow (Proof_Context.export result_ctxt ctxt') results) ctxt';
+ in
+ ctxt
+ |> init
+ |> generic_goal "" before_qed (K I, after_qed') goal_ctxt propss []
+ end;
val theorem = global_goal Proof_Context.cert_propp;
val theorem_cmd = global_goal Proof_Context.read_propp;
fun global_qeds arg =
end_proof true arg
- #> Seq.map_result (generic_qed (K I) #> (fn (((_, after_qed), results), state) =>
+ #> Seq.map_result (generic_qed #> (fn (((_, after_qed), results), state) =>
after_qed results (context_of state)));
fun global_qed arg =
@@ -1054,13 +1112,19 @@
(* common goal statements *)
+fun internal_goal print_results mode =
+ local_goal print_results (K I) (Proof_Context.cert_propp o Proof_Context.set_mode mode)
+ Proof_Context.cert_var;
+
local
-fun gen_have prep_att prep_propp before_qed after_qed stmt int =
+fun gen_have prep_att prep_propp prep_var
+ before_qed after_qed fixes assumes shows int =
local_goal (Proof_Display.print_results int (Position.thread_data ()))
- prep_att prep_propp "have" before_qed after_qed stmt;
+ prep_att prep_propp prep_var "have" before_qed after_qed fixes assumes shows;
-fun gen_show prep_att prep_propp before_qed after_qed stmt int state =
+fun gen_show prep_att prep_propp prep_var
+ before_qed after_qed fixes assumes shows int state =
let
val testing = Unsynchronized.ref false;
val rule = Unsynchronized.ref (NONE: thm option);
@@ -1085,13 +1149,14 @@
|> Unsynchronized.setmp testing true
|> Exn.interruptible_capture;
- fun after_qed' results =
- refine_goals print_rule (context_of state) (flat results)
- #> check_result "Failed to refine any pending goal"
- #> after_qed results;
+ fun after_qed' (result_ctxt, results) state' = state'
+ |> refine_goals print_rule result_ctxt (flat results)
+ |> check_result "Failed to refine any pending goal"
+ |> after_qed (result_ctxt, results);
in
state
- |> local_goal print_results prep_att prep_propp "show" before_qed after_qed' stmt
+ |> local_goal print_results prep_att prep_propp prep_var
+ "show" before_qed after_qed' fixes assumes shows
|> int ? (fn goal_state =>
(case test_proof (map_context (Context_Position.set_visible false) goal_state) of
Exn.Res _ => goal_state
@@ -1100,10 +1165,10 @@
in
-val have = gen_have (K I) Proof_Context.cert_propp;
-val have_cmd = gen_have Attrib.attribute_cmd Proof_Context.read_propp;
-val show = gen_show (K I) Proof_Context.cert_propp;
-val show_cmd = gen_show Attrib.attribute_cmd Proof_Context.read_propp;
+val have = gen_have (K I) Proof_Context.cert_propp Proof_Context.cert_var;
+val have_cmd = gen_have Attrib.attribute_cmd Proof_Context.read_propp Proof_Context.read_var;
+val show = gen_show (K I) Proof_Context.cert_propp Proof_Context.cert_var;
+val show_cmd = gen_show Attrib.attribute_cmd Proof_Context.read_propp Proof_Context.read_var;
end;
@@ -1147,28 +1212,22 @@
fun future_proof fork_proof state =
let
val _ = assert_backward state;
- val (goal_ctxt, (_, goal)) = find_goal state;
- val {statement as (kind, _, prop), using, goal, before_qed, after_qed} = goal;
- val goal_tfrees =
- fold Term.add_tfrees
- (prop :: map Thm.term_of (Assumption.all_assms_of goal_ctxt)) [];
+ val (goal_ctxt, (_, goal_info)) = find_goal state;
+ val {statement as (kind, _, prop), using, goal, before_qed, after_qed} = goal_info;
val _ = is_relevant state andalso error "Cannot fork relevant proof";
- val prop' = Logic.protect prop;
- val statement' = (kind, [[], [prop']], prop');
- val goal' = Thm.adjust_maxidx_thm (Thm.maxidx_of goal) (Goal.protect (Thm.nprems_of goal) goal);
- val after_qed' = (fn [[th]] => map_context (set_result th), fn [[th]] => set_result th);
-
+ val after_qed' =
+ (fn (_, [[th]]) => map_context (set_result th),
+ fn (_, [[th]]) => set_result th);
val result_ctxt =
state
|> map_context reset_result
- |> map_goal I (K (statement', using, goal', before_qed, after_qed'))
- (fold (Variable.declare_typ o TFree) goal_tfrees)
+ |> map_goal I (K ((kind, [[], [prop]], prop), using, goal, before_qed, after_qed')) I
|> fork_proof;
val future_thm = Future.map (the_result o snd) result_ctxt;
- val finished_goal = Goal.future_result goal_ctxt future_thm prop';
+ val finished_goal = Goal.protect 0 (Goal.future_result goal_ctxt future_thm prop);
val state' =
state
|> map_goal I (K (statement, using, finished_goal, NONE, after_qed)) I;
@@ -1181,7 +1240,7 @@
local
-fun future_terminal_proof proof1 proof2 done int state =
+fun future_terminal_proof proof1 proof2 done state =
if Goal.future_enabled 3 andalso not (is_relevant state) then
state |> future_proof (fn state' =>
let
--- a/src/Pure/Isar/proof_context.ML Wed Jun 10 15:50:17 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML Wed Jun 10 18:57:31 2015 +0200
@@ -74,7 +74,7 @@
val cert_typ_syntax: Proof.context -> typ -> typ
val cert_typ_abbrev: Proof.context -> typ -> typ
val infer_type: Proof.context -> string * typ -> typ
- val inferred_param: string -> Proof.context -> typ * Proof.context
+ val inferred_param: string -> Proof.context -> (string * typ) * Proof.context
val inferred_fixes: Proof.context -> (string * typ) list * Proof.context
val check_type_name: {proper: bool, strict: bool} -> Proof.context ->
xstring * Position.T -> typ * Position.report list
@@ -105,9 +105,6 @@
val export: Proof.context -> Proof.context -> thm list -> thm list
val export_morphism: Proof.context -> Proof.context -> morphism
val norm_export_morphism: Proof.context -> Proof.context -> morphism
- val maybe_bind_terms: (indexname * term option) list -> Proof.context -> Proof.context
- val bind_terms: (indexname * term) list -> Proof.context -> Proof.context
- val export_bind_terms: (indexname * term) list -> Proof.context -> Proof.context -> Proof.context
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 ->
@@ -459,14 +456,11 @@
Term.fastype_of (singleton (Syntax.check_terms (set_mode mode_schematic ctxt)) (Free x));
fun inferred_param x ctxt =
- let val T = infer_type ctxt (x, dummyT)
- in (T, ctxt |> Variable.declare_term (Free (x, T))) end;
+ let val p = (x, infer_type ctxt (x, dummyT))
+ in (p, ctxt |> Variable.declare_term (Free p)) end;
fun inferred_fixes ctxt =
- let
- val xs = map #2 (Variable.dest_fixes ctxt);
- val (Ts, ctxt') = fold_map inferred_param xs ctxt;
- in (xs ~~ Ts, ctxt') end;
+ fold_map inferred_param (map #2 (Variable.dest_fixes ctxt)) ctxt;
(* type names *)
@@ -819,30 +813,23 @@
| SOME (env, _) => Vartab.fold (fn (v, (_, t)) => cons (v, t)) (Envir.term_env env) []);
-(* bind_terms *)
-
-val maybe_bind_terms = fold (fn (xi, t) => fn ctxt =>
- ctxt
- |> Variable.bind_term (xi, Option.map (cert_term (set_mode mode_default ctxt)) t));
-
-val bind_terms = maybe_bind_terms o map (apsnd SOME);
-
-fun export_bind_terms binds ctxt ctxt0 =
- let val ts0 = map Term.close_schematic_term (Variable.export_terms ctxt ctxt0 (map snd binds))
- in bind_terms (map fst binds ~~ ts0) ctxt0 end;
-
-
(* auto_bind *)
-fun drop_schematic (b as (xi, SOME t)) = if Term.exists_subterm is_Var t then (xi, NONE) else b
- | drop_schematic b = b;
-
-fun auto_bind f ts ctxt = ctxt |> maybe_bind_terms (map drop_schematic (f ctxt ts));
+fun auto_bind f props ctxt = fold Variable.maybe_bind_term (f ctxt props) ctxt;
val auto_bind_goal = auto_bind Auto_Bind.goal;
val auto_bind_facts = auto_bind Auto_Bind.facts;
+(* bind terms (non-schematic) *)
+
+fun cert_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
@@ -865,8 +852,10 @@
val ctxt'' =
tap (Variable.warn_extra_tfrees ctxt)
(if gen then
- ctxt (*sic!*) |> fold Variable.declare_term (map #2 binds') |> bind_terms binds'
- else ctxt' |> bind_terms binds');
+ 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
@@ -1169,7 +1158,7 @@
|> fold_burrow (Assumption.add_assms exp o map (Thm.cterm_of ctxt)) propss
|-> (fn premss =>
auto_bind_facts props
- #> bind_terms binds
+ #> fold Variable.bind_term binds
#> note_thmss "" (map fst args ~~ map (map (fn th => ([th], []))) premss))
end;
@@ -1190,6 +1179,9 @@
local
+fun drop_schematic (b as (xi, SOME t)) = if Term.exists_subterm is_Var t then (xi, NONE) else b
+ | drop_schematic b = b;
+
fun update_case _ _ ("", _) res = res
| update_case _ _ (name, NONE) (cases, index) =
(Name_Space.del_table name cases, index)
@@ -1221,7 +1213,7 @@
val Rule_Cases.Case {assumes, binds, cases, ...} = Rule_Cases.apply ts c;
in
ctxt'
- |> maybe_bind_terms (map drop_schematic binds)
+ |> fold (cert_maybe_bind_term o drop_schematic) binds
|> update_cases true (map (apsnd SOME) cases)
|> pair (assumes, (binds, cases))
end;
@@ -1393,12 +1385,12 @@
else [Pretty.block (Pretty.str "fixed variables:" :: Pretty.brk 1 ::
Pretty.commas (map prt_fix fixes))];
- (*prems*)
- val prt_prems =
+ (*assumptions*)
+ val prt_assms =
(case Assumption.all_prems_of ctxt of
[] => []
- | prems => [Pretty.big_list "prems:" [pretty_fact ctxt ("", prems)]]);
- in prt_structs @ prt_fixes @ prt_prems end;
+ | prems => [Pretty.big_list "assumptions:" [pretty_fact ctxt ("", prems)]]);
+ in prt_structs @ prt_fixes @ prt_assms end;
(* main context *)
--- a/src/Pure/Isar/specification.ML Wed Jun 10 15:50:17 2015 +0200
+++ b/src/Pure/Isar/specification.ML Wed Jun 10 18:57:31 2015 +0200
@@ -150,8 +150,8 @@
|> flat |> burrow (Syntax.check_props params_ctxt);
val specs_ctxt = params_ctxt |> (fold o fold) Variable.declare_term specs;
- val Ts = specs_ctxt |> fold_map Proof_Context.inferred_param xs |> fst;
- val params = map2 (fn (b, _, mx) => fn T => ((b, T), mx)) vars Ts;
+ val ps = specs_ctxt |> fold_map Proof_Context.inferred_param xs |> fst;
+ val params = map2 (fn (b, _, mx) => fn (_, T) => ((b, T), mx)) vars ps;
val name_atts = map (fn ((name, atts), _) => (name, map (prep_att ctxt) atts)) (flat raw_specss);
in ((params, name_atts ~~ specs), specs_ctxt) end;
@@ -363,10 +363,10 @@
val bs = map fst vars;
val xs = map Variable.check_name bs;
val props = map fst asms;
- val (Ts, _) = ctxt'
+ val (params, _) = ctxt'
|> fold Variable.declare_term props
- |> fold_map Proof_Context.inferred_param xs;
- val params = map Free (xs ~~ Ts);
+ |> fold_map Proof_Context.inferred_param xs
+ |>> map Free;
val asm = fold_rev Logic.all params (Logic.list_implies (props, thesis));
val _ = ctxt' |> Proof_Context.add_fixes (map (fn b => (b, NONE, NoSyn)) bs);
in
--- a/src/Pure/Isar/toplevel.ML Wed Jun 10 15:50:17 2015 +0200
+++ b/src/Pure/Isar/toplevel.ML Wed Jun 10 18:57:31 2015 +0200
@@ -192,8 +192,7 @@
(case try node_of state of
NONE => []
| SOME (Theory _) => []
- | SOME (Proof (prf, _)) =>
- Proof.pretty_state (Proof_Node.position prf) (Proof_Node.current prf)
+ | SOME (Proof (prf, _)) => Proof.pretty_state (Proof_Node.current prf)
| SOME (Skipped_Proof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)]);
val print_state = pretty_state #> Pretty.chunks #> Pretty.string_of #> Output.state;
--- a/src/Pure/term.ML Wed Jun 10 15:50:17 2015 +0200
+++ b/src/Pure/term.ML Wed Jun 10 18:57:31 2015 +0200
@@ -152,6 +152,7 @@
val rename_abs: term -> term -> term -> term option
val is_open: term -> bool
val is_dependent: term -> bool
+ val dependent_lambda_name: string * term -> term -> term
val lambda_name: string * term -> term -> term
val close_schematic_term: term -> term
val maxidx_typ: typ -> int -> int
@@ -749,6 +750,10 @@
| term_name (Var ((x, _), _)) = x
| term_name _ = Name.uu;
+fun dependent_lambda_name (x, v) t =
+ let val t' = abstract_over (v, t)
+ in if is_dependent t' then Abs (if x = "" then term_name v else x, fastype_of v, t') else t end;
+
fun lambda_name (x, v) t =
Abs (if x = "" then term_name v else x, fastype_of v, abstract_over (v, t));
--- a/src/Pure/variable.ML Wed Jun 10 15:50:17 2015 +0200
+++ b/src/Pure/variable.ML Wed Jun 10 18:57:31 2015 +0200
@@ -24,7 +24,9 @@
val declare_prf: Proofterm.proof -> Proof.context -> Proof.context
val declare_thm: thm -> Proof.context -> Proof.context
val variant_frees: Proof.context -> term list -> (string * 'a) list -> (string * 'a) list
- val bind_term: indexname * term option -> Proof.context -> Proof.context
+ val bind_term: indexname * term -> Proof.context -> Proof.context
+ val unbind_term: indexname -> Proof.context -> Proof.context
+ val maybe_bind_term: indexname * term option -> Proof.context -> Proof.context
val expand_binds: Proof.context -> term -> term
val lookup_const: Proof.context -> string -> string option
val is_const: Proof.context -> string -> bool
@@ -274,12 +276,16 @@
(** term bindings **)
-fun bind_term (xi, NONE) = map_binds (Vartab.delete_safe xi)
- | bind_term ((x, i), SOME t) =
- let
- val u = Term.close_schematic_term t;
- val U = Term.fastype_of u;
- in declare_term u #> map_binds (Vartab.update ((x, i), (U, u))) end;
+fun bind_term ((x, i), t) =
+ let
+ val u = Term.close_schematic_term t;
+ val U = Term.fastype_of u;
+ in declare_term u #> map_binds (Vartab.update ((x, i), (U, u))) end;
+
+val unbind_term = map_binds o Vartab.delete_safe;
+
+fun maybe_bind_term (xi, SOME t) = bind_term (xi, t)
+ | maybe_bind_term (xi, NONE) = unbind_term xi;
fun expand_binds ctxt =
let
@@ -638,9 +644,8 @@
fun focus_subgoal i st =
let
val all_vars = Thm.fold_terms Term.add_vars st [];
- val no_binds = map (fn (xi, _) => (xi, NONE)) all_vars;
in
- fold bind_term no_binds #>
+ fold (unbind_term o #1) all_vars #>
fold (declare_constraints o Var) all_vars #>
focus_cterm (Thm.cprem_of st i)
end;