--- a/NEWS Fri Jun 26 18:54:23 2015 +0200
+++ b/NEWS Sat Jun 27 00:10:24 2015 +0200
@@ -42,6 +42,20 @@
The keyword 'when' may be used instead of 'if', to indicate 'presume'
instead of 'assume' above.
+* The meaning of 'show' with Pure rule statements has changed: premises
+are treated in the sense of 'assume', instead of 'presume'. This means,
+a goal like "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x" can be solved completely as follows:
+
+ show "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"
+
+or:
+
+ show "C x" if "A x" "B x" for x
+
+Rare INCOMPATIBILITY, the old behaviour may be recovered as follows:
+
+ show "C x" when "A x" "B x" for x
+
* New command 'supply' supports fact definitions during goal refinement
('apply' scripts).
--- a/src/HOL/Bali/DefiniteAssignment.thy Fri Jun 26 18:54:23 2015 +0200
+++ b/src/HOL/Bali/DefiniteAssignment.thy Sat Jun 27 00:10:24 2015 +0200
@@ -1055,7 +1055,7 @@
shows "(nrm A \<subseteq> nrm A') \<and> (\<forall> l. (brk A l \<subseteq> brk A' l))"
proof -
from da
- show "\<And> B' A'. \<lbrakk>Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'; B \<subseteq> B'\<rbrakk>
+ have "\<And> B' A'. \<lbrakk>Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'; B \<subseteq> B'\<rbrakk>
\<Longrightarrow> (nrm A \<subseteq> nrm A') \<and> (\<forall> l. (brk A l \<subseteq> brk A' l))"
(is "PROP ?Hyp Env B t A")
proof (induct)
@@ -1326,7 +1326,8 @@
next
case Cons thus ?case by (elim da_elim_cases) auto
qed
-qed (rule da', rule `B \<subseteq> B'`)
+ from this [OF da' `B \<subseteq> B'`] show ?thesis .
+qed
lemma da_weaken:
assumes da: "Env\<turnstile> B \<guillemotright>t\<guillemotright> A" and "B \<subseteq> B'"
@@ -1334,7 +1335,7 @@
proof -
note assigned.select_convs [Pure.intro]
from da
- show "\<And> B'. B \<subseteq> B' \<Longrightarrow> \<exists> A'. Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'" (is "PROP ?Hyp Env B t")
+ have "\<And> B'. B \<subseteq> B' \<Longrightarrow> \<exists> A'. Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'" (is "PROP ?Hyp Env B t")
proof (induct)
case Skip thus ?case by (iprover intro: da.Skip)
next
@@ -1799,7 +1800,8 @@
by (iprover intro: da.Cons)
thus ?case ..
qed
-qed (rule `B \<subseteq> B'`)
+ from this [OF `B \<subseteq> B'`] show ?thesis .
+qed
(* Remarks about the proof style:
--- a/src/HOL/Finite_Set.thy Fri Jun 26 18:54:23 2015 +0200
+++ b/src/HOL/Finite_Set.thy Sat Jun 27 00:10:24 2015 +0200
@@ -167,7 +167,8 @@
also have "insert x (A - {x}) = A" using x by (rule insert_Diff)
finally show ?thesis .
next
- show "A \<subseteq> F ==> ?thesis" by fact
+ show ?thesis when "A \<subseteq> F"
+ using that by fact
assume "x \<notin> A"
with A show "A \<subseteq> F" by (simp add: subset_insert_iff)
qed
--- a/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy Fri Jun 26 18:54:23 2015 +0200
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy Sat Jun 27 00:10:24 2015 +0200
@@ -423,8 +423,8 @@
show ?L
proof
fix x assume x: "x \<in> H"
- show "- a \<le> b \<Longrightarrow> b \<le> a \<Longrightarrow> \<bar>b\<bar> \<le> a" for a b :: real
- by arith
+ show "\<bar>b\<bar> \<le> a" when "- a \<le> b" "b \<le> a" for a b :: real
+ using that by arith
from \<open>linearform H h\<close> and H x
have "- h x = h (- x)" by (rule linearform.neg [symmetric])
also
--- a/src/HOL/Probability/Probability_Mass_Function.thy Fri Jun 26 18:54:23 2015 +0200
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Sat Jun 27 00:10:24 2015 +0200
@@ -1043,52 +1043,53 @@
show "\<And>f::'a \<Rightarrow> 'b. set_pmf \<circ> map_pmf f = op ` f \<circ> set_pmf"
by (rule pmf_set_map)
- { fix p :: "'s pmf"
+ show "(card_of (set_pmf p), natLeq) \<in> ordLeq" for p :: "'s pmf"
+ proof -
have "(card_of (set_pmf p), card_of (UNIV :: nat set)) \<in> ordLeq"
by (rule card_of_ordLeqI[where f="to_nat_on (set_pmf p)"])
(auto intro: countable_set_pmf)
also have "(card_of (UNIV :: nat set), natLeq) \<in> ordLeq"
by (metis Field_natLeq card_of_least natLeq_Well_order)
- finally show "(card_of (set_pmf p), natLeq) \<in> ordLeq" . }
+ finally show ?thesis .
+ qed
show "\<And>R. rel_pmf R =
(BNF_Def.Grp {x. set_pmf x \<subseteq> {(x, y). R x y}} (map_pmf fst))\<inverse>\<inverse> OO
BNF_Def.Grp {x. set_pmf x \<subseteq> {(x, y). R x y}} (map_pmf snd)"
by (auto simp add: fun_eq_iff BNF_Def.Grp_def OO_def rel_pmf.simps)
- { fix p :: "'a pmf" and f :: "'a \<Rightarrow> 'b" and g x
- assume p: "\<And>z. z \<in> set_pmf p \<Longrightarrow> f z = g z"
- and x: "x \<in> set_pmf p"
- thus "f x = g x" by simp }
-
- fix R :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and S :: "'b \<Rightarrow> 'c \<Rightarrow> bool"
- { fix p q r
- assume pq: "rel_pmf R p q"
- and qr:"rel_pmf S q r"
- from pq obtain pq where pq: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> R x y"
- and p: "p = map_pmf fst pq" and q: "q = map_pmf snd pq" by cases auto
- from qr obtain qr where qr: "\<And>y z. (y, z) \<in> set_pmf qr \<Longrightarrow> S y z"
- and q': "q = map_pmf fst qr" and r: "r = map_pmf snd qr" by cases auto
-
- def pr \<equiv> "bind_pmf pq (\<lambda>xy. bind_pmf (cond_pmf qr {yz. fst yz = snd xy}) (\<lambda>yz. return_pmf (fst xy, snd yz)))"
- have pr_welldefined: "\<And>y. y \<in> q \<Longrightarrow> qr \<inter> {yz. fst yz = y} \<noteq> {}"
- by (force simp: q')
-
- have "rel_pmf (R OO S) p r"
- proof (rule rel_pmf.intros)
- fix x z assume "(x, z) \<in> pr"
- then have "\<exists>y. (x, y) \<in> pq \<and> (y, z) \<in> qr"
- by (auto simp: q pr_welldefined pr_def split_beta)
- with pq qr show "(R OO S) x z"
- by blast
- next
- have "map_pmf snd pr = map_pmf snd (bind_pmf q (\<lambda>y. cond_pmf qr {yz. fst yz = y}))"
- by (simp add: pr_def q split_beta bind_map_pmf map_pmf_def[symmetric] map_bind_pmf map_pmf_comp)
- then show "map_pmf snd pr = r"
- unfolding r q' bind_map_pmf by (subst (asm) bind_cond_pmf_cancel) (auto simp: eq_commute)
- qed (simp add: pr_def map_bind_pmf split_beta map_pmf_def[symmetric] p map_pmf_comp) }
- then show "rel_pmf R OO rel_pmf S \<le> rel_pmf (R OO S)"
- by(auto simp add: le_fun_def)
+ show "rel_pmf R OO rel_pmf S \<le> rel_pmf (R OO S)"
+ for R :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and S :: "'b \<Rightarrow> 'c \<Rightarrow> bool"
+ proof -
+ { fix p q r
+ assume pq: "rel_pmf R p q"
+ and qr:"rel_pmf S q r"
+ from pq obtain pq where pq: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> R x y"
+ and p: "p = map_pmf fst pq" and q: "q = map_pmf snd pq" by cases auto
+ from qr obtain qr where qr: "\<And>y z. (y, z) \<in> set_pmf qr \<Longrightarrow> S y z"
+ and q': "q = map_pmf fst qr" and r: "r = map_pmf snd qr" by cases auto
+
+ def pr \<equiv> "bind_pmf pq (\<lambda>xy. bind_pmf (cond_pmf qr {yz. fst yz = snd xy}) (\<lambda>yz. return_pmf (fst xy, snd yz)))"
+ have pr_welldefined: "\<And>y. y \<in> q \<Longrightarrow> qr \<inter> {yz. fst yz = y} \<noteq> {}"
+ by (force simp: q')
+
+ have "rel_pmf (R OO S) p r"
+ proof (rule rel_pmf.intros)
+ fix x z assume "(x, z) \<in> pr"
+ then have "\<exists>y. (x, y) \<in> pq \<and> (y, z) \<in> qr"
+ by (auto simp: q pr_welldefined pr_def split_beta)
+ with pq qr show "(R OO S) x z"
+ by blast
+ next
+ have "map_pmf snd pr = map_pmf snd (bind_pmf q (\<lambda>y. cond_pmf qr {yz. fst yz = y}))"
+ by (simp add: pr_def q split_beta bind_map_pmf map_pmf_def[symmetric] map_bind_pmf map_pmf_comp)
+ then show "map_pmf snd pr = r"
+ unfolding r q' bind_map_pmf by (subst (asm) bind_cond_pmf_cancel) (auto simp: eq_commute)
+ qed (simp add: pr_def map_bind_pmf split_beta map_pmf_def[symmetric] p map_pmf_comp)
+ }
+ then show ?thesis
+ by(auto simp add: le_fun_def)
+ qed
qed (fact natLeq_card_order natLeq_cinfinite)+
lemma rel_pmf_conj[simp]:
--- a/src/HOL/Proofs/Extraction/Warshall.thy Fri Jun 26 18:54:23 2015 +0200
+++ b/src/HOL/Proofs/Extraction/Warshall.thy Sat Jun 27 00:10:24 2015 +0200
@@ -119,7 +119,7 @@
show "(\<exists>ys. list_all (\<lambda>x. x < i) ys \<and> is_path' r j ys i) \<and>
(\<exists>ys. list_all (\<lambda>x. x < i) ys \<and> is_path' r i ys k)"
proof
- show "\<And>j. list_all (\<lambda>x. x < Suc i) xs \<Longrightarrow> is_path' r j xs k \<Longrightarrow>
+ have "\<And>j. list_all (\<lambda>x. x < Suc i) xs \<Longrightarrow> is_path' r j xs k \<Longrightarrow>
\<not> list_all (\<lambda>x. x < i) xs \<Longrightarrow>
\<exists>ys. list_all (\<lambda>x. x < i) ys \<and> is_path' r j ys i" (is "PROP ?ih xs")
proof (induct xs)
@@ -151,7 +151,8 @@
qed
qed
qed
- show "\<And>k. list_all (\<lambda>x. x < Suc i) xs \<Longrightarrow> is_path' r j xs k \<Longrightarrow>
+ from this asms show "\<exists>ys. list_all (\<lambda>x. x < i) ys \<and> is_path' r j ys i" .
+ have "\<And>k. list_all (\<lambda>x. x < Suc i) xs \<Longrightarrow> is_path' r j xs k \<Longrightarrow>
\<not> list_all (\<lambda>x. x < i) xs \<Longrightarrow>
\<exists>ys. list_all (\<lambda>x. x < i) ys \<and> is_path' r i ys k" (is "PROP ?ih xs")
proof (induct xs rule: rev_induct)
@@ -184,7 +185,8 @@
qed
qed
qed
- qed (rule asms)+
+ from this asms show "\<exists>ys. list_all (\<lambda>x. x < i) ys \<and> is_path' r i ys k" .
+ qed
qed
theorem lemma5':
--- a/src/Pure/Isar/proof.ML Fri Jun 26 18:54:23 2015 +0200
+++ b/src/Pure/Isar/proof.ML Sat Jun 27 00:10:24 2015 +0200
@@ -458,6 +458,14 @@
let fun find i n = if i > n then Seq.fail else Seq.APPEND (tac i, find (i + 1) n)
in find 1 (Thm.nprems_of st) st end;
+fun protect_prem i th =
+ Thm.bicompose NONE {flatten = false, match = false, incremented = true}
+ (false, Drule.incr_indexes th Drule.protectD, 1) i th
+ |> Seq.hd;
+
+fun protect_prems th =
+ fold_rev protect_prem (1 upto Thm.nprems_of th) th;
+
in
fun refine_goals print_rule result_ctxt result state =
@@ -467,6 +475,7 @@
(print_rule goal_ctxt rule; FINDGOAL (goal_tac goal_ctxt rule) st);
in
result
+ |> map (Raw_Simplifier.norm_hhf result_ctxt #> protect_prems)
|> Proof_Context.goal_export result_ctxt goal_ctxt
|> (fn rules => Seq.lift provide_goal (EVERY (map refine rules) goal) state)
end;
@@ -1284,4 +1293,3 @@
end;
end;
-