premises in 'show' are treated like 'assume';
authorwenzelm
Sat Jun 27 00:10:24 2015 +0200 (2015-06-27)
changeset 60595804dfdc82835
parent 60594 c1a6c23f70a5
child 60596 54168997757f
premises in 'show' are treated like 'assume';
NEWS
src/HOL/Bali/DefiniteAssignment.thy
src/HOL/Finite_Set.thy
src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy
src/HOL/Probability/Probability_Mass_Function.thy
src/HOL/Proofs/Extraction/Warshall.thy
src/Pure/Isar/proof.ML
     1.1 --- a/NEWS	Fri Jun 26 18:54:23 2015 +0200
     1.2 +++ b/NEWS	Sat Jun 27 00:10:24 2015 +0200
     1.3 @@ -42,6 +42,20 @@
     1.4  The keyword 'when' may be used instead of 'if', to indicate 'presume'
     1.5  instead of 'assume' above.
     1.6  
     1.7 +* The meaning of 'show' with Pure rule statements has changed: premises
     1.8 +are treated in the sense of 'assume', instead of 'presume'. This means,
     1.9 +a goal like "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x" can be solved completely as follows:
    1.10 +
    1.11 +  show "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"
    1.12 +
    1.13 +or:
    1.14 +
    1.15 +  show "C x" if "A x" "B x" for x
    1.16 +
    1.17 +Rare INCOMPATIBILITY, the old behaviour may be recovered as follows:
    1.18 +
    1.19 +  show "C x" when "A x" "B x" for x
    1.20 +
    1.21  * New command 'supply' supports fact definitions during goal refinement
    1.22  ('apply' scripts).
    1.23  
     2.1 --- a/src/HOL/Bali/DefiniteAssignment.thy	Fri Jun 26 18:54:23 2015 +0200
     2.2 +++ b/src/HOL/Bali/DefiniteAssignment.thy	Sat Jun 27 00:10:24 2015 +0200
     2.3 @@ -1055,7 +1055,7 @@
     2.4    shows "(nrm A \<subseteq> nrm A') \<and> (\<forall> l. (brk A l \<subseteq> brk A' l))"
     2.5  proof -
     2.6    from da
     2.7 -  show "\<And> B' A'. \<lbrakk>Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'; B \<subseteq> B'\<rbrakk> 
     2.8 +  have "\<And> B' A'. \<lbrakk>Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'; B \<subseteq> B'\<rbrakk> 
     2.9                    \<Longrightarrow> (nrm A \<subseteq> nrm A') \<and> (\<forall> l. (brk A l \<subseteq> brk A' l))"
    2.10         (is "PROP ?Hyp Env B t A")  
    2.11    proof (induct)
    2.12 @@ -1326,7 +1326,8 @@
    2.13    next
    2.14      case Cons thus ?case by (elim da_elim_cases) auto
    2.15    qed
    2.16 -qed (rule da', rule `B \<subseteq> B'`)
    2.17 +  from this [OF da' `B \<subseteq> B'`] show ?thesis .
    2.18 +qed
    2.19    
    2.20  lemma da_weaken:     
    2.21    assumes da: "Env\<turnstile> B \<guillemotright>t\<guillemotright> A" and "B \<subseteq> B'" 
    2.22 @@ -1334,7 +1335,7 @@
    2.23  proof -
    2.24    note assigned.select_convs [Pure.intro]
    2.25    from da  
    2.26 -  show "\<And> B'. B \<subseteq> B' \<Longrightarrow> \<exists> A'. Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'" (is "PROP ?Hyp Env B t")
    2.27 +  have "\<And> B'. B \<subseteq> B' \<Longrightarrow> \<exists> A'. Env\<turnstile> B' \<guillemotright>t\<guillemotright> A'" (is "PROP ?Hyp Env B t")
    2.28    proof (induct) 
    2.29      case Skip thus ?case by (iprover intro: da.Skip)
    2.30    next
    2.31 @@ -1799,7 +1800,8 @@
    2.32        by (iprover intro: da.Cons)
    2.33      thus ?case ..
    2.34    qed
    2.35 -qed (rule `B \<subseteq> B'`)
    2.36 +  from this [OF `B \<subseteq> B'`] show ?thesis .
    2.37 +qed
    2.38  
    2.39  (* Remarks about the proof style:
    2.40  
     3.1 --- a/src/HOL/Finite_Set.thy	Fri Jun 26 18:54:23 2015 +0200
     3.2 +++ b/src/HOL/Finite_Set.thy	Sat Jun 27 00:10:24 2015 +0200
     3.3 @@ -167,7 +167,8 @@
     3.4      also have "insert x (A - {x}) = A" using x by (rule insert_Diff)
     3.5      finally show ?thesis .
     3.6    next
     3.7 -    show "A \<subseteq> F ==> ?thesis" by fact
     3.8 +    show ?thesis when "A \<subseteq> F"
     3.9 +      using that by fact
    3.10      assume "x \<notin> A"
    3.11      with A show "A \<subseteq> F" by (simp add: subset_insert_iff)
    3.12    qed
     4.1 --- a/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Fri Jun 26 18:54:23 2015 +0200
     4.2 +++ b/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Sat Jun 27 00:10:24 2015 +0200
     4.3 @@ -423,8 +423,8 @@
     4.4      show ?L
     4.5      proof
     4.6        fix x assume x: "x \<in> H"
     4.7 -      show "- a \<le> b \<Longrightarrow> b \<le> a \<Longrightarrow> \<bar>b\<bar> \<le> a" for a b :: real
     4.8 -        by arith
     4.9 +      show "\<bar>b\<bar> \<le> a" when "- a \<le> b" "b \<le> a" for a b :: real
    4.10 +        using that by arith
    4.11        from \<open>linearform H h\<close> and H x
    4.12        have "- h x = h (- x)" by (rule linearform.neg [symmetric])
    4.13        also
     5.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Fri Jun 26 18:54:23 2015 +0200
     5.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Sat Jun 27 00:10:24 2015 +0200
     5.3 @@ -1043,52 +1043,53 @@
     5.4    show "\<And>f::'a \<Rightarrow> 'b. set_pmf \<circ> map_pmf f = op ` f \<circ> set_pmf"
     5.5      by (rule pmf_set_map)
     5.6  
     5.7 -  { fix p :: "'s pmf"
     5.8 +  show "(card_of (set_pmf p), natLeq) \<in> ordLeq" for p :: "'s pmf"
     5.9 +  proof -
    5.10      have "(card_of (set_pmf p), card_of (UNIV :: nat set)) \<in> ordLeq"
    5.11        by (rule card_of_ordLeqI[where f="to_nat_on (set_pmf p)"])
    5.12           (auto intro: countable_set_pmf)
    5.13      also have "(card_of (UNIV :: nat set), natLeq) \<in> ordLeq"
    5.14        by (metis Field_natLeq card_of_least natLeq_Well_order)
    5.15 -    finally show "(card_of (set_pmf p), natLeq) \<in> ordLeq" . }
    5.16 +    finally show ?thesis .
    5.17 +  qed
    5.18  
    5.19    show "\<And>R. rel_pmf R =
    5.20           (BNF_Def.Grp {x. set_pmf x \<subseteq> {(x, y). R x y}} (map_pmf fst))\<inverse>\<inverse> OO
    5.21           BNF_Def.Grp {x. set_pmf x \<subseteq> {(x, y). R x y}} (map_pmf snd)"
    5.22       by (auto simp add: fun_eq_iff BNF_Def.Grp_def OO_def rel_pmf.simps)
    5.23  
    5.24 -  { fix p :: "'a pmf" and f :: "'a \<Rightarrow> 'b" and g x
    5.25 -    assume p: "\<And>z. z \<in> set_pmf p \<Longrightarrow> f z = g z"
    5.26 -      and x: "x \<in> set_pmf p"
    5.27 -    thus "f x = g x" by simp }
    5.28 -
    5.29 -  fix R :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and S :: "'b \<Rightarrow> 'c \<Rightarrow> bool"
    5.30 -  { fix p q r
    5.31 -    assume pq: "rel_pmf R p q"
    5.32 -      and qr:"rel_pmf S q r"
    5.33 -    from pq obtain pq where pq: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> R x y"
    5.34 -      and p: "p = map_pmf fst pq" and q: "q = map_pmf snd pq" by cases auto
    5.35 -    from qr obtain qr where qr: "\<And>y z. (y, z) \<in> set_pmf qr \<Longrightarrow> S y z"
    5.36 -      and q': "q = map_pmf fst qr" and r: "r = map_pmf snd qr" by cases auto
    5.37 -
    5.38 -    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)))"
    5.39 -    have pr_welldefined: "\<And>y. y \<in> q \<Longrightarrow> qr \<inter> {yz. fst yz = y} \<noteq> {}"
    5.40 -      by (force simp: q')
    5.41 -
    5.42 -    have "rel_pmf (R OO S) p r"
    5.43 -    proof (rule rel_pmf.intros)
    5.44 -      fix x z assume "(x, z) \<in> pr"
    5.45 -      then have "\<exists>y. (x, y) \<in> pq \<and> (y, z) \<in> qr"
    5.46 -        by (auto simp: q pr_welldefined pr_def split_beta)
    5.47 -      with pq qr show "(R OO S) x z"
    5.48 -        by blast
    5.49 -    next
    5.50 -      have "map_pmf snd pr = map_pmf snd (bind_pmf q (\<lambda>y. cond_pmf qr {yz. fst yz = y}))"
    5.51 -        by (simp add: pr_def q split_beta bind_map_pmf map_pmf_def[symmetric] map_bind_pmf map_pmf_comp)
    5.52 -      then show "map_pmf snd pr = r"
    5.53 -        unfolding r q' bind_map_pmf by (subst (asm) bind_cond_pmf_cancel) (auto simp: eq_commute)
    5.54 -    qed (simp add: pr_def map_bind_pmf split_beta map_pmf_def[symmetric] p map_pmf_comp) }
    5.55 -  then show "rel_pmf R OO rel_pmf S \<le> rel_pmf (R OO S)"
    5.56 -    by(auto simp add: le_fun_def)
    5.57 +  show "rel_pmf R OO rel_pmf S \<le> rel_pmf (R OO S)"
    5.58 +    for R :: "'a \<Rightarrow> 'b \<Rightarrow> bool" and S :: "'b \<Rightarrow> 'c \<Rightarrow> bool"
    5.59 +  proof -
    5.60 +    { fix p q r
    5.61 +      assume pq: "rel_pmf R p q"
    5.62 +        and qr:"rel_pmf S q r"
    5.63 +      from pq obtain pq where pq: "\<And>x y. (x, y) \<in> set_pmf pq \<Longrightarrow> R x y"
    5.64 +        and p: "p = map_pmf fst pq" and q: "q = map_pmf snd pq" by cases auto
    5.65 +      from qr obtain qr where qr: "\<And>y z. (y, z) \<in> set_pmf qr \<Longrightarrow> S y z"
    5.66 +        and q': "q = map_pmf fst qr" and r: "r = map_pmf snd qr" by cases auto
    5.67 +  
    5.68 +      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)))"
    5.69 +      have pr_welldefined: "\<And>y. y \<in> q \<Longrightarrow> qr \<inter> {yz. fst yz = y} \<noteq> {}"
    5.70 +        by (force simp: q')
    5.71 +  
    5.72 +      have "rel_pmf (R OO S) p r"
    5.73 +      proof (rule rel_pmf.intros)
    5.74 +        fix x z assume "(x, z) \<in> pr"
    5.75 +        then have "\<exists>y. (x, y) \<in> pq \<and> (y, z) \<in> qr"
    5.76 +          by (auto simp: q pr_welldefined pr_def split_beta)
    5.77 +        with pq qr show "(R OO S) x z"
    5.78 +          by blast
    5.79 +      next
    5.80 +        have "map_pmf snd pr = map_pmf snd (bind_pmf q (\<lambda>y. cond_pmf qr {yz. fst yz = y}))"
    5.81 +          by (simp add: pr_def q split_beta bind_map_pmf map_pmf_def[symmetric] map_bind_pmf map_pmf_comp)
    5.82 +        then show "map_pmf snd pr = r"
    5.83 +          unfolding r q' bind_map_pmf by (subst (asm) bind_cond_pmf_cancel) (auto simp: eq_commute)
    5.84 +      qed (simp add: pr_def map_bind_pmf split_beta map_pmf_def[symmetric] p map_pmf_comp)
    5.85 +    }
    5.86 +    then show ?thesis
    5.87 +      by(auto simp add: le_fun_def)
    5.88 +  qed
    5.89  qed (fact natLeq_card_order natLeq_cinfinite)+
    5.90  
    5.91  lemma rel_pmf_conj[simp]:
     6.1 --- a/src/HOL/Proofs/Extraction/Warshall.thy	Fri Jun 26 18:54:23 2015 +0200
     6.2 +++ b/src/HOL/Proofs/Extraction/Warshall.thy	Sat Jun 27 00:10:24 2015 +0200
     6.3 @@ -119,7 +119,7 @@
     6.4    show "(\<exists>ys. list_all (\<lambda>x. x < i) ys \<and> is_path' r j ys i) \<and>
     6.5      (\<exists>ys. list_all (\<lambda>x. x < i) ys \<and> is_path' r i ys k)"
     6.6    proof
     6.7 -    show "\<And>j. list_all (\<lambda>x. x < Suc i) xs \<Longrightarrow> is_path' r j xs k \<Longrightarrow>
     6.8 +    have "\<And>j. list_all (\<lambda>x. x < Suc i) xs \<Longrightarrow> is_path' r j xs k \<Longrightarrow>
     6.9        \<not> list_all (\<lambda>x. x < i) xs \<Longrightarrow>
    6.10      \<exists>ys. list_all (\<lambda>x. x < i) ys \<and> is_path' r j ys i" (is "PROP ?ih xs")
    6.11      proof (induct xs)
    6.12 @@ -151,7 +151,8 @@
    6.13          qed
    6.14        qed
    6.15      qed
    6.16 -    show "\<And>k. list_all (\<lambda>x. x < Suc i) xs \<Longrightarrow> is_path' r j xs k \<Longrightarrow>
    6.17 +    from this asms show "\<exists>ys. list_all (\<lambda>x. x < i) ys \<and> is_path' r j ys i" .
    6.18 +    have "\<And>k. list_all (\<lambda>x. x < Suc i) xs \<Longrightarrow> is_path' r j xs k \<Longrightarrow>
    6.19        \<not> list_all (\<lambda>x. x < i) xs \<Longrightarrow>
    6.20        \<exists>ys. list_all (\<lambda>x. x < i) ys \<and> is_path' r i ys k" (is "PROP ?ih xs")
    6.21      proof (induct xs rule: rev_induct)
    6.22 @@ -184,7 +185,8 @@
    6.23          qed
    6.24        qed
    6.25      qed
    6.26 -  qed (rule asms)+
    6.27 +    from this asms show "\<exists>ys. list_all (\<lambda>x. x < i) ys \<and> is_path' r i ys k" .
    6.28 +  qed
    6.29  qed
    6.30  
    6.31  theorem lemma5':
     7.1 --- a/src/Pure/Isar/proof.ML	Fri Jun 26 18:54:23 2015 +0200
     7.2 +++ b/src/Pure/Isar/proof.ML	Sat Jun 27 00:10:24 2015 +0200
     7.3 @@ -458,6 +458,14 @@
     7.4    let fun find i n = if i > n then Seq.fail else Seq.APPEND (tac i, find (i + 1) n)
     7.5    in find 1 (Thm.nprems_of st) st end;
     7.6  
     7.7 +fun protect_prem i th =
     7.8 +  Thm.bicompose NONE {flatten = false, match = false, incremented = true}
     7.9 +    (false, Drule.incr_indexes th Drule.protectD, 1) i th
    7.10 +  |> Seq.hd;
    7.11 +
    7.12 +fun protect_prems th =
    7.13 +  fold_rev protect_prem (1 upto Thm.nprems_of th) th;
    7.14 +
    7.15  in
    7.16  
    7.17  fun refine_goals print_rule result_ctxt result state =
    7.18 @@ -467,6 +475,7 @@
    7.19        (print_rule goal_ctxt rule; FINDGOAL (goal_tac goal_ctxt rule) st);
    7.20    in
    7.21      result
    7.22 +    |> map (Raw_Simplifier.norm_hhf result_ctxt #> protect_prems)
    7.23      |> Proof_Context.goal_export result_ctxt goal_ctxt
    7.24      |> (fn rules => Seq.lift provide_goal (EVERY (map refine rules) goal) state)
    7.25    end;
    7.26 @@ -1284,4 +1293,3 @@
    7.27  end;
    7.28  
    7.29  end;
    7.30 -