# HG changeset patch
# User wenzelm
# Date 1435356624 -7200
# Node ID 804dfdc82835ac71bbbf59c07f58fcfec7a42d8d
# Parent  c1a6c23f70a56fb168c4c42c31cc9f9cef0e4dba
premises in 'show' are treated like 'assume';

diff -r c1a6c23f70a5 -r 804dfdc82835 NEWS
--- 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).
 
diff -r c1a6c23f70a5 -r 804dfdc82835 src/HOL/Bali/DefiniteAssignment.thy
--- 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:
 
diff -r c1a6c23f70a5 -r 804dfdc82835 src/HOL/Finite_Set.thy
--- 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
diff -r c1a6c23f70a5 -r 804dfdc82835 src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy
--- 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
diff -r c1a6c23f70a5 -r 804dfdc82835 src/HOL/Probability/Probability_Mass_Function.thy
--- 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]:
diff -r c1a6c23f70a5 -r 804dfdc82835 src/HOL/Proofs/Extraction/Warshall.thy
--- 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':
diff -r c1a6c23f70a5 -r 804dfdc82835 src/Pure/Isar/proof.ML
--- 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;
-