--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Thu Jun 25 22:56:33 2015 +0200
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Thu Jun 25 23:33:47 2015 +0200
@@ -908,13 +908,13 @@
subsection \<open>Miscellaneous lemmas about indexes, decrementation, substitution etc ...\<close>
lemma isnpolyh_polybound0: "isnpolyh p (Suc n) \<Longrightarrow> polybound0 p"
-proof (induct p arbitrary: n rule: poly.induct, auto)
- case (goal1 c n p n')
+proof (induct p arbitrary: n rule: poly.induct, auto, goals)
+ case prems: (1 c n p n')
then have "n = Suc (n - 1)"
by simp
then have "isnpolyh p (Suc (n - 1))"
using \<open>isnpolyh p n\<close> by simp
- with goal1(2) show ?case
+ with prems(2) show ?case
by simp
qed
--- a/src/HOL/GCD.thy Thu Jun 25 22:56:33 2015 +0200
+++ b/src/HOL/GCD.thy Thu Jun 25 23:33:47 2015 +0200
@@ -1451,17 +1451,19 @@
subsection {* The complete divisibility lattice *}
-interpretation gcd_semilattice_nat: semilattice_inf gcd "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)"
-proof
- case goal3 thus ?case by(metis gcd_unique_nat)
+interpretation gcd_semilattice_nat: semilattice_inf gcd "op dvd" "(\<lambda>m n::nat. m dvd n \<and> \<not> n dvd m)"
+proof (default, goals)
+ case 3
+ thus ?case by(metis gcd_unique_nat)
qed auto
-interpretation lcm_semilattice_nat: semilattice_sup lcm "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)"
-proof
- case goal3 thus ?case by(metis lcm_unique_nat)
+interpretation lcm_semilattice_nat: semilattice_sup lcm "op dvd" "(\<lambda>m n::nat. m dvd n \<and> \<not> n dvd m)"
+proof (default, goals)
+ case 3
+ thus ?case by(metis lcm_unique_nat)
qed auto
-interpretation gcd_lcm_lattice_nat: lattice gcd "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" lcm ..
+interpretation gcd_lcm_lattice_nat: lattice gcd "op dvd" "(\<lambda>m n::nat. m dvd n & ~ n dvd m)" lcm ..
text{* Lifting gcd and lcm to sets (Gcd/Lcm).
Gcd is defined via Lcm to facilitate the proof that we have a complete lattice.
@@ -1522,23 +1524,28 @@
interpretation gcd_lcm_complete_lattice_nat:
complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat"
-where
- "Inf.INFIMUM Gcd A f = Gcd (f ` A :: nat set)"
+where "Inf.INFIMUM Gcd A f = Gcd (f ` A :: nat set)"
and "Sup.SUPREMUM Lcm A f = Lcm (f ` A)"
proof -
show "class.complete_lattice Gcd Lcm gcd Rings.dvd (\<lambda>m n. m dvd n \<and> \<not> n dvd m) lcm 1 (0::nat)"
- proof
- case goal1 thus ?case by (simp add: Gcd_nat_def)
+ proof (default, goals)
+ case 1
+ thus ?case by (simp add: Gcd_nat_def)
next
- case goal2 thus ?case by (simp add: Gcd_nat_def)
+ case 2
+ thus ?case by (simp add: Gcd_nat_def)
next
- case goal5 show ?case by (simp add: Gcd_nat_def Lcm_nat_infinite)
+ case 5
+ show ?case by (simp add: Gcd_nat_def Lcm_nat_infinite)
next
- case goal6 show ?case by (simp add: Lcm_nat_empty)
+ case 6
+ show ?case by (simp add: Lcm_nat_empty)
next
- case goal3 thus ?case by simp
+ case 3
+ thus ?case by simp
next
- case goal4 thus ?case by simp
+ case 4
+ thus ?case by simp
qed
then interpret gcd_lcm_complete_lattice_nat:
complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat" .
--- a/src/HOL/Library/Extended_Real.thy Thu Jun 25 22:56:33 2015 +0200
+++ b/src/HOL/Library/Extended_Real.thy Thu Jun 25 23:33:47 2015 +0200
@@ -333,11 +333,11 @@
| "ereal r + -\<infinity> = - \<infinity>"
| "-\<infinity> + ereal p = -(\<infinity>::ereal)"
| "-\<infinity> + -\<infinity> = -(\<infinity>::ereal)"
-proof -
- case (goal1 P x)
+proof goals
+ case prems: (1 P x)
then obtain a b where "x = (a, b)"
by (cases x) auto
- with goal1 show P
+ with prems show P
by (cases rule: ereal2_cases[of a b]) auto
qed auto
termination by default (rule wf_empty)
@@ -437,10 +437,10 @@
| "ereal x < \<infinity> \<longleftrightarrow> True"
| " -\<infinity> < ereal r \<longleftrightarrow> True"
| " -\<infinity> < (\<infinity>::ereal) \<longleftrightarrow> True"
-proof -
- case (goal1 P x)
+proof goals
+ case prems: (1 P x)
then obtain a b where "x = (a,b)" by (cases x) auto
- with goal1 show P by (cases rule: ereal2_cases[of a b]) auto
+ with prems show P by (cases rule: ereal2_cases[of a b]) auto
qed simp_all
termination by (relation "{}") simp
@@ -860,11 +860,11 @@
| "-(\<infinity>::ereal) * \<infinity> = -\<infinity>"
| "(\<infinity>::ereal) * -\<infinity> = -\<infinity>"
| "-(\<infinity>::ereal) * -\<infinity> = \<infinity>"
-proof -
- case (goal1 P x)
+proof goals
+ case prems: (1 P x)
then obtain a b where "x = (a, b)"
by (cases x) auto
- with goal1 show P
+ with prems show P
by (cases rule: ereal2_cases[of a b]) auto
qed simp_all
termination by (relation "{}") simp
--- a/src/HOL/Library/Product_Order.thy Thu Jun 25 22:56:33 2015 +0200
+++ b/src/HOL/Library/Product_Order.thy Thu Jun 25 23:33:47 2015 +0200
@@ -233,11 +233,13 @@
instance prod ::
(complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice
-proof
- case goal1 thus ?case
+proof (default, goals)
+ case 1
+ then show ?case
by (auto simp: sup_prod_def Inf_prod_def INF_prod_alt_def sup_Inf sup_INF comp_def)
next
- case goal2 thus ?case
+ case 2
+ then show ?case
by (auto simp: inf_prod_def Sup_prod_def SUP_prod_alt_def inf_Sup inf_SUP comp_def)
qed
--- a/src/HOL/Library/RBT_Set.thy Thu Jun 25 22:56:33 2015 +0200
+++ b/src/HOL/Library/RBT_Set.thy Thu Jun 25 23:33:47 2015 +0200
@@ -294,27 +294,32 @@
using assms
proof (induction t rule: rbt_min_opt_induct)
case empty
- then show ?case by simp
+ then show ?case by simp
next
case left_empty
- then show ?case by (auto intro: key_le_right simp del: rbt_sorted.simps)
+ then show ?case by (auto intro: key_le_right simp del: rbt_sorted.simps)
next
case (left_non_empty c t1 k v t2 y)
- then have "y = k \<or> y \<in> set (RBT_Impl.keys t1) \<or> y \<in> set (RBT_Impl.keys t2)" by auto
- with left_non_empty show ?case
- proof(elim disjE)
- case goal1 then show ?case
- by (auto simp add: rbt_min_opt_Branch intro: left_le_key rbt_min_opt_in_set)
- next
- case goal2 with left_non_empty show ?case by (auto simp add: rbt_min_opt_Branch)
- next
- case goal3 show ?case
- proof -
- from goal3 have "rbt_min_opt t1 \<le> k" by (simp add: left_le_key rbt_min_opt_in_set)
- moreover from goal3 have "k \<le> y" by (simp add: key_le_right)
- ultimately show ?thesis using goal3 by (simp add: rbt_min_opt_Branch)
- qed
- qed
+ then consider "y = k" | "y \<in> set (RBT_Impl.keys t1)" | "y \<in> set (RBT_Impl.keys t2)"
+ by auto
+ then show ?case
+ proof cases
+ case 1
+ with left_non_empty show ?thesis
+ by (auto simp add: rbt_min_opt_Branch intro: left_le_key rbt_min_opt_in_set)
+ next
+ case 2
+ with left_non_empty show ?thesis
+ by (auto simp add: rbt_min_opt_Branch)
+ next
+ case y: 3
+ have "rbt_min_opt t1 \<le> k"
+ using left_non_empty by (simp add: left_le_key rbt_min_opt_in_set)
+ moreover have "k \<le> y"
+ using left_non_empty y by (simp add: key_le_right)
+ ultimately show ?thesis
+ using left_non_empty y by (simp add: rbt_min_opt_Branch)
+ qed
qed
lemma rbt_min_eq_rbt_min_opt:
@@ -388,27 +393,32 @@
using assms
proof (induction t rule: rbt_max_opt_induct)
case empty
- then show ?case by simp
+ then show ?case by simp
next
case right_empty
- then show ?case by (auto intro: left_le_key simp del: rbt_sorted.simps)
+ then show ?case by (auto intro: left_le_key simp del: rbt_sorted.simps)
next
case (right_non_empty c t1 k v t2 y)
- then have "y = k \<or> y \<in> set (RBT_Impl.keys t2) \<or> y \<in> set (RBT_Impl.keys t1)" by auto
- with right_non_empty show ?case
- proof(elim disjE)
- case goal1 then show ?case
- by (auto simp add: rbt_max_opt_Branch intro: key_le_right rbt_max_opt_in_set)
- next
- case goal2 with right_non_empty show ?case by (auto simp add: rbt_max_opt_Branch)
- next
- case goal3 show ?case
- proof -
- from goal3 have "rbt_max_opt t2 \<ge> k" by (simp add: key_le_right rbt_max_opt_in_set)
- moreover from goal3 have "y \<le> k" by (simp add: left_le_key)
- ultimately show ?thesis using goal3 by (simp add: rbt_max_opt_Branch)
- qed
- qed
+ then consider "y = k" | "y \<in> set (RBT_Impl.keys t2)" | "y \<in> set (RBT_Impl.keys t1)"
+ by auto
+ then show ?case
+ proof cases
+ case 1
+ with right_non_empty show ?thesis
+ by (auto simp add: rbt_max_opt_Branch intro: key_le_right rbt_max_opt_in_set)
+ next
+ case 2
+ with right_non_empty show ?thesis
+ by (auto simp add: rbt_max_opt_Branch)
+ next
+ case y: 3
+ have "rbt_max_opt t2 \<ge> k"
+ using right_non_empty by (simp add: key_le_right rbt_max_opt_in_set)
+ moreover have "y \<le> k"
+ using right_non_empty y by (simp add: left_le_key)
+ ultimately show ?thesis
+ using right_non_empty by (simp add: rbt_max_opt_Branch)
+ qed
qed
lemma rbt_max_eq_rbt_max_opt:
--- a/src/HOL/Library/While_Combinator.thy Thu Jun 25 22:56:33 2015 +0200
+++ b/src/HOL/Library/While_Combinator.thy Thu Jun 25 23:33:47 2015 +0200
@@ -157,14 +157,15 @@
note b = this(1) and body = this(2) and inv = this(3)
hence k': "f ((c ^^ k') s) = (c' ^^ k') (f s)" by auto
ultimately show ?thesis unfolding Suc using b
- proof (intro Least_equality[symmetric])
- case goal1
+ proof (intro Least_equality[symmetric], goals)
+ case 1
hence Test: "\<not> b' (f ((c ^^ Suc k') s))"
by (auto simp: BodyCommute inv b)
have "P ((c ^^ Suc k') s)" by (auto simp: Invariant inv b)
with Test show ?case by (auto simp: TestCommute)
next
- case goal2 thus ?case by (metis not_less_eq_eq)
+ case 2
+ thus ?case by (metis not_less_eq_eq)
qed
qed
have "f ((c ^^ ?k) s) = (c' ^^ ?k') (f s)" unfolding *
--- a/src/HOL/List.thy Thu Jun 25 22:56:33 2015 +0200
+++ b/src/HOL/List.thy Thu Jun 25 23:33:47 2015 +0200
@@ -2308,19 +2308,29 @@
"\<lbrakk> \<And> i. \<lbrakk> i < n ; i < length xs \<rbrakk> \<Longrightarrow> P (xs ! i) ; n < length xs \<Longrightarrow> \<not> P (xs ! n) \<rbrakk> \<Longrightarrow>
takeWhile P xs = take n xs"
proof (induct xs arbitrary: n)
+ case Nil
+ thus ?case by simp
+next
case (Cons x xs)
- thus ?case
+ show ?case
proof (cases n)
- case (Suc n') note this[simp]
+ case 0
+ with Cons show ?thesis by simp
+ next
+ case [simp]: (Suc n')
have "P x" using Cons.prems(1)[of 0] by simp
moreover have "takeWhile P xs = take n' xs"
proof (rule Cons.hyps)
- case goal1 thus "P (xs ! i)" using Cons.prems(1)[of "Suc i"] by simp
- next case goal2 thus ?case using Cons by auto
+ fix i
+ assume "i < n'" "i < length xs"
+ thus "P (xs ! i)" using Cons.prems(1)[of "Suc i"] by simp
+ next
+ assume "n' < length xs"
+ thus "\<not> P (xs ! n')" using Cons by auto
qed
ultimately show ?thesis by simp
- qed simp
-qed simp
+ qed
+qed
lemma nth_length_takeWhile:
"length (takeWhile P xs) < length xs \<Longrightarrow> \<not> P (xs ! length (takeWhile P xs))"
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Thu Jun 25 22:56:33 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Thu Jun 25 23:33:47 2015 +0200
@@ -1337,22 +1337,25 @@
obtains q where "\<forall>i<n. q i < p"
and "\<forall>i<n. \<exists>r s. (\<forall>j<n. q j \<le> r j \<and> r j \<le> q j + 1) \<and> (\<forall>j<n. q j \<le> s j \<and> s j \<le> q j + 1) \<and> label r i \<noteq> label s i"
proof -
- let ?rl = "reduced n\<circ>label"
+ let ?rl = "reduced n \<circ> label"
let ?A = "{s. ksimplex p n s \<and> ?rl ` s = {..n}}"
have "odd (card ?A)"
using assms by (intro kuhn_combinatorial[of p n label]) auto
then have "?A \<noteq> {}"
- by (intro notI) simp
+ by fastforce
then obtain s b u where "kuhn_simplex p n b u s" and rl: "?rl ` s = {..n}"
by (auto elim: ksimplex.cases)
interpret kuhn_simplex p n b u s by fact
show ?thesis
proof (intro that[of b] allI impI)
- fix i assume "i < n" then show "b i < p"
+ fix i
+ assume "i < n"
+ then show "b i < p"
using base by auto
next
- case goal2
+ fix i
+ assume "i < n"
then have "i \<in> {.. n}" "Suc i \<in> {.. n}"
by auto
then obtain u v where u: "u \<in> s" "Suc i = ?rl u" and v: "v \<in> s" "i = ?rl v"
@@ -1363,10 +1366,11 @@
u(2)[symmetric] v(2)[symmetric] \<open>i < n\<close>
by auto
moreover
- { fix j assume "j < n"
- then have "b j \<le> u j" "u j \<le> b j + 1" "b j \<le> v j" "v j \<le> b j + 1"
- using base_le[OF \<open>u\<in>s\<close>] le_Suc_base[OF \<open>u\<in>s\<close>] base_le[OF \<open>v\<in>s\<close>] le_Suc_base[OF \<open>v\<in>s\<close>] by auto }
- ultimately show ?case
+ have "b j \<le> u j" "u j \<le> b j + 1" "b j \<le> v j" "v j \<le> b j + 1" if "j < n" for j
+ using that base_le[OF \<open>u\<in>s\<close>] le_Suc_base[OF \<open>u\<in>s\<close>] base_le[OF \<open>v\<in>s\<close>] le_Suc_base[OF \<open>v\<in>s\<close>]
+ by auto
+ ultimately show "\<exists>r s. (\<forall>j<n. b j \<le> r j \<and> r j \<le> b j + 1) \<and>
+ (\<forall>j<n. b j \<le> s j \<and> s j \<le> b j + 1) \<and> label r i \<noteq> label s i"
by blast
qed
qed
@@ -1392,23 +1396,20 @@
apply rule
apply rule
proof -
- case goal1
+ fix x x'
let ?R = "\<lambda>y::nat.
- (P x \<and> Q xa \<and> x xa = 0 \<longrightarrow> y = 0) \<and>
- (P x \<and> Q xa \<and> x xa = 1 \<longrightarrow> y = 1) \<and>
- (P x \<and> Q xa \<and> y = 0 \<longrightarrow> x xa \<le> (f x) xa) \<and>
- (P x \<and> Q xa \<and> y = 1 \<longrightarrow> (f x) xa \<le> x xa)"
- {
- assume "P x" and "Q xa"
- then have "0 \<le> f x xa \<and> f x xa \<le> 1"
- using assms(2)[rule_format,of "f x" xa]
- apply (drule_tac assms(1)[rule_format])
- apply auto
- done
- }
+ (P x \<and> Q x' \<and> x x' = 0 \<longrightarrow> y = 0) \<and>
+ (P x \<and> Q x' \<and> x x' = 1 \<longrightarrow> y = 1) \<and>
+ (P x \<and> Q x' \<and> y = 0 \<longrightarrow> x x' \<le> (f x) x') \<and>
+ (P x \<and> Q x' \<and> y = 1 \<longrightarrow> (f x) x' \<le> x x')"
+ have "0 \<le> f x x' \<and> f x x' \<le> 1" if "P x" "Q x'"
+ using assms(2)[rule_format,of "f x" x'] that
+ apply (drule_tac assms(1)[rule_format])
+ apply auto
+ done
then have "?R 0 \<or> ?R 1"
by auto
- then show ?case
+ then show "\<exists>y\<le>1. ?R y"
by auto
qed
qed
@@ -1988,17 +1989,17 @@
assumes "e > 0"
shows "\<not> (frontier (cball a e) retract_of (cball a e))"
proof
- case goal1
- have *: "\<And>xa. a - (2 *\<^sub>R a - xa) = - (a - xa)"
+ assume *: "frontier (cball a e) retract_of (cball a e)"
+ have **: "\<And>xa. a - (2 *\<^sub>R a - xa) = - (a - xa)"
using scaleR_left_distrib[of 1 1 a] by auto
obtain x where x:
"x \<in> {x. norm (a - x) = e}"
"2 *\<^sub>R a - x = x"
- apply (rule retract_fixpoint_property[OF goal1, of "\<lambda>x. scaleR 2 a - x"])
+ apply (rule retract_fixpoint_property[OF *, of "\<lambda>x. scaleR 2 a - x"])
apply (blast intro: brouwer_ball[OF assms])
apply (intro continuous_intros)
unfolding frontier_cball subset_eq Ball_def image_iff dist_norm
- apply (auto simp add: * norm_minus_commute)
+ apply (auto simp add: ** norm_minus_commute)
done
then have "scaleR 2 a = scaleR 1 x + scaleR 1 x"
by (auto simp add: algebra_simps)
--- a/src/HOL/Nominal/Examples/Pattern.thy Thu Jun 25 22:56:33 2015 +0200
+++ b/src/HOL/Nominal/Examples/Pattern.thy Thu Jun 25 23:33:47 2015 +0200
@@ -62,20 +62,20 @@
by (simp add: supp_def Collect_disj_eq del: disj_not1)
instance pat :: pt_name
-proof intro_classes
- case goal1
+proof (default, goals)
+ case (1 x)
show ?case by (induct x) simp_all
next
- case goal2
+ case (2 _ _ x)
show ?case by (induct x) (simp_all add: pt_name2)
next
- case goal3
+ case (3 _ _ x)
then show ?case by (induct x) (simp_all add: pt_name3)
qed
instance pat :: fs_name
-proof intro_classes
- case goal1
+proof (default, goals)
+ case (1 x)
show ?case by (induct x) (simp_all add: fin_supp)
qed
--- a/src/HOL/Nominal/Nominal.thy Thu Jun 25 22:56:33 2015 +0200
+++ b/src/HOL/Nominal/Nominal.thy Thu Jun 25 23:33:47 2015 +0200
@@ -2202,7 +2202,6 @@
have pt_x: "pt TYPE('x) TYPE('x)" by (force intro: at_pt_inst at)
show ?thesis
proof (rule equalityI)
- case goal1
show "pi\<bullet>(\<Union>x\<in>X. f x) \<subseteq> (\<Union>x\<in>(pi\<bullet>X). (pi\<bullet>f) x)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="pi\<bullet>xb" in exI)
@@ -2218,7 +2217,6 @@
apply(rule pt_fun_app_eq[OF pt, OF at])
done
next
- case goal2
show "(\<Union>x\<in>(pi\<bullet>X). (pi\<bullet>f) x) \<subseteq> pi\<bullet>(\<Union>x\<in>X. f x)"
apply(auto simp add: perm_set_def)
apply(rule_tac x="(rev pi)\<bullet>x" in exI)
--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy Thu Jun 25 22:56:33 2015 +0200
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy Thu Jun 25 23:33:47 2015 +0200
@@ -1527,14 +1527,19 @@
definition [simp]:
"normalization_factor_int = (sgn :: int \<Rightarrow> int)"
-instance proof
- case goal2 then show ?case by (auto simp add: abs_mult nat_mult_distrib)
+instance
+proof (default, goals)
+ case 2
+ then show ?case by (auto simp add: abs_mult nat_mult_distrib)
next
- case goal3 then show ?case by (simp add: zsgn_def)
+ case 3
+ then show ?case by (simp add: zsgn_def)
next
- case goal5 then show ?case by (auto simp: zsgn_def)
+ case 5
+ then show ?case by (auto simp: zsgn_def)
next
- case goal6 then show ?case by (auto split: abs_split simp: zsgn_def)
+ case 6
+ then show ?case by (auto split: abs_split simp: zsgn_def)
qed (auto simp: sgn_times split: abs_split)
end
--- a/src/HOL/Probability/Embed_Measure.thy Thu Jun 25 22:56:33 2015 +0200
+++ b/src/HOL/Probability/Embed_Measure.thy Thu Jun 25 23:33:47 2015 +0200
@@ -154,22 +154,22 @@
lemma sigma_finite_embed_measure:
assumes "sigma_finite_measure M" and inj: "inj f"
shows "sigma_finite_measure (embed_measure M f)"
-proof
- case goal1
+proof -
from assms(1) interpret sigma_finite_measure M .
from sigma_finite_countable obtain A where
A_props: "countable A" "A \<subseteq> sets M" "\<Union>A = space M" "\<And>X. X\<in>A \<Longrightarrow> emeasure M X \<noteq> \<infinity>" by blast
- show ?case
- proof (intro exI[of _ "op ` f`A"] conjI allI)
- from A_props show "countable (op ` f`A)" by auto
- from inj and A_props show "op ` f`A \<subseteq> sets (embed_measure M f)"
- by (auto simp: sets_embed_measure)
- from A_props and inj show "\<Union>(op ` f`A) = space (embed_measure M f)"
- by (auto simp: space_embed_measure intro!: imageI)
- from A_props and inj show "\<forall>a\<in>op ` f ` A. emeasure (embed_measure M f) a \<noteq> \<infinity>"
- by (intro ballI, subst emeasure_embed_measure)
- (auto simp: inj_vimage_image_eq intro: in_sets_embed_measure)
- qed
+ from A_props have "countable (op ` f`A)" by auto
+ moreover
+ from inj and A_props have "op ` f`A \<subseteq> sets (embed_measure M f)"
+ by (auto simp: sets_embed_measure)
+ moreover
+ from A_props and inj have "\<Union>(op ` f`A) = space (embed_measure M f)"
+ by (auto simp: space_embed_measure intro!: imageI)
+ moreover
+ from A_props and inj have "\<forall>a\<in>op ` f ` A. emeasure (embed_measure M f) a \<noteq> \<infinity>"
+ by (intro ballI, subst emeasure_embed_measure)
+ (auto simp: inj_vimage_image_eq intro: in_sets_embed_measure)
+ ultimately show ?thesis by - (default, blast)
qed
lemma embed_measure_count_space':
--- a/src/HOL/Probability/Finite_Product_Measure.thy Thu Jun 25 22:56:33 2015 +0200
+++ b/src/HOL/Probability/Finite_Product_Measure.thy Thu Jun 25 23:33:47 2015 +0200
@@ -192,20 +192,22 @@
lemma PiM_cong:
assumes "I = J" "\<And>x. x \<in> I \<Longrightarrow> M x = N x"
shows "PiM I M = PiM J N"
-unfolding PiM_def
-proof (rule extend_measure_cong)
- case goal1 show ?case using assms
+ unfolding PiM_def
+proof (rule extend_measure_cong, goals)
+ case 1
+ show ?case using assms
by (subst assms(1), intro PiE_cong[of J "\<lambda>i. space (M i)" "\<lambda>i. space (N i)"]) simp_all
next
- case goal2
+ case 2
have "\<And>K. K \<subseteq> J \<Longrightarrow> (\<Pi> j\<in>K. sets (M j)) = (\<Pi> j\<in>K. sets (N j))"
using assms by (intro Pi_cong_sets) auto
thus ?case by (auto simp: assms)
next
- case goal3 show ?case using assms
+ case 3
+ show ?case using assms
by (intro ext) (auto simp: prod_emb_def dest: PiE_mem)
next
- case (goal4 x)
+ case (4 x)
thus ?case using assms
by (auto intro!: setprod.cong split: split_if_asm)
qed
--- a/src/HOL/Probability/Information.thy Thu Jun 25 22:56:33 2015 +0200
+++ b/src/HOL/Probability/Information.thy Thu Jun 25 23:33:47 2015 +0200
@@ -1022,11 +1022,12 @@
Pxyz x * log b (Pxz (fst x, snd (snd x)) / (Px (fst x) * Pz (snd (snd x)))) =
Pxyz x * log b (Pxyz x * Pz (snd (snd x)) / (Pxz (fst x, snd (snd x)) * Pyz (snd x))) "
proof eventually_elim
- case (goal1 x)
+ case (elim x)
show ?case
proof cases
assume "Pxyz x \<noteq> 0"
- with goal1 have "0 < Px (fst x)" "0 < Pz (snd (snd x))" "0 < Pxz (fst x, snd (snd x))" "0 < Pyz (snd x)" "0 < Pxyz x"
+ with elim have "0 < Px (fst x)" "0 < Pz (snd (snd x))" "0 < Pxz (fst x, snd (snd x))"
+ "0 < Pyz (snd x)" "0 < Pxyz x"
by auto
then show ?thesis
using b_gt_1 by (simp add: log_simps less_imp_le field_simps)
@@ -1252,11 +1253,12 @@
Pxyz x * log b (Pxz (fst x, snd (snd x)) / (Px (fst x) * Pz (snd (snd x)))) =
Pxyz x * log b (Pxyz x * Pz (snd (snd x)) / (Pxz (fst x, snd (snd x)) * Pyz (snd x))) "
proof eventually_elim
- case (goal1 x)
+ case (elim x)
show ?case
proof cases
assume "Pxyz x \<noteq> 0"
- with goal1 have "0 < Px (fst x)" "0 < Pz (snd (snd x))" "0 < Pxz (fst x, snd (snd x))" "0 < Pyz (snd x)" "0 < Pxyz x"
+ with elim have "0 < Px (fst x)" "0 < Pz (snd (snd x))" "0 < Pxz (fst x, snd (snd x))"
+ "0 < Pyz (snd x)" "0 < Pxyz x"
by auto
then show ?thesis
using b_gt_1 by (simp add: log_simps less_imp_le field_simps)
@@ -1730,11 +1732,11 @@
Pxy x * log b (Pxy x / (Px (fst x) * Py (snd x)))"
(is "AE x in _. ?f x = ?g x")
proof eventually_elim
- case (goal1 x)
+ case (elim x)
show ?case
proof cases
assume "Pxy x \<noteq> 0"
- with goal1 have "0 < Px (fst x)" "0 < Py (snd x)" "0 < Pxy x"
+ with elim have "0 < Px (fst x)" "0 < Py (snd x)" "0 < Pxy x"
by auto
then show ?thesis
using b_gt_1 by (simp add: log_simps less_imp_le field_simps)
--- a/src/HOL/Probability/Measure_Space.thy Thu Jun 25 22:56:33 2015 +0200
+++ b/src/HOL/Probability/Measure_Space.thy Thu Jun 25 23:33:47 2015 +0200
@@ -1134,44 +1134,56 @@
lemma (in sigma_finite_measure) sigma_finite_disjoint:
obtains A :: "nat \<Rightarrow> 'a set"
where "range A \<subseteq> sets M" "(\<Union>i. A i) = space M" "\<And>i. emeasure M (A i) \<noteq> \<infinity>" "disjoint_family A"
-proof atomize_elim
- case goal1
+proof -
obtain A :: "nat \<Rightarrow> 'a set" where
range: "range A \<subseteq> sets M" and
space: "(\<Union>i. A i) = space M" and
measure: "\<And>i. emeasure M (A i) \<noteq> \<infinity>"
using sigma_finite by auto
- note range' = sets.range_disjointed_sets[OF range] range
- { fix i
- have "emeasure M (disjointed A i) \<le> emeasure M (A i)"
- using range' disjointed_subset[of A i] by (auto intro!: emeasure_mono)
- then have "emeasure M (disjointed A i) \<noteq> \<infinity>"
- using measure[of i] by auto }
- with disjoint_family_disjointed UN_disjointed_eq[of A] space range'
- show ?case by (auto intro!: exI[of _ "disjointed A"])
+ show thesis
+ proof (rule that[of "disjointed A"])
+ show "range (disjointed A) \<subseteq> sets M"
+ by (rule sets.range_disjointed_sets[OF range])
+ show "(\<Union>i. disjointed A i) = space M"
+ and "disjoint_family (disjointed A)"
+ using disjoint_family_disjointed UN_disjointed_eq[of A] space range
+ by auto
+ show "emeasure M (disjointed A i) \<noteq> \<infinity>" for i
+ proof -
+ have "emeasure M (disjointed A i) \<le> emeasure M (A i)"
+ using range disjointed_subset[of A i] by (auto intro!: emeasure_mono)
+ then show ?thesis using measure[of i] by auto
+ qed
+ qed
qed
lemma (in sigma_finite_measure) sigma_finite_incseq:
obtains A :: "nat \<Rightarrow> 'a set"
where "range A \<subseteq> sets M" "(\<Union>i. A i) = space M" "\<And>i. emeasure M (A i) \<noteq> \<infinity>" "incseq A"
-proof atomize_elim
- case goal1
+proof -
obtain F :: "nat \<Rightarrow> 'a set" where
F: "range F \<subseteq> sets M" "(\<Union>i. F i) = space M" "\<And>i. emeasure M (F i) \<noteq> \<infinity>"
using sigma_finite by auto
- then show ?case
- proof (intro exI[of _ "\<lambda>n. \<Union>i\<le>n. F i"] conjI allI)
- from F have "\<And>x. x \<in> space M \<Longrightarrow> \<exists>i. x \<in> F i" by auto
- then show "(\<Union>n. \<Union> i\<le>n. F i) = space M"
- using F by fastforce
- next
- fix n
- have "emeasure M (\<Union> i\<le>n. F i) \<le> (\<Sum>i\<le>n. emeasure M (F i))" using F
- by (auto intro!: emeasure_subadditive_finite)
- also have "\<dots> < \<infinity>"
- using F by (auto simp: setsum_Pinfty)
- finally show "emeasure M (\<Union> i\<le>n. F i) \<noteq> \<infinity>" by simp
- qed (force simp: incseq_def)+
+ show thesis
+ proof (rule that[of "\<lambda>n. \<Union>i\<le>n. F i"])
+ show "range (\<lambda>n. \<Union>i\<le>n. F i) \<subseteq> sets M"
+ using F by (force simp: incseq_def)
+ show "(\<Union>n. \<Union>i\<le>n. F i) = space M"
+ proof -
+ from F have "\<And>x. x \<in> space M \<Longrightarrow> \<exists>i. x \<in> F i" by auto
+ with F show ?thesis by fastforce
+ qed
+ show "emeasure M (\<Union> i\<le>n. F i) \<noteq> \<infinity>" for n
+ proof -
+ have "emeasure M (\<Union> i\<le>n. F i) \<le> (\<Sum>i\<le>n. emeasure M (F i))"
+ using F by (auto intro!: emeasure_subadditive_finite)
+ also have "\<dots> < \<infinity>"
+ using F by (auto simp: setsum_Pinfty)
+ finally show ?thesis by simp
+ qed
+ show "incseq (\<lambda>n. \<Union>i\<le>n. F i)"
+ by (force simp: incseq_def)
+ qed
qed
subsection {* Measure space induced by distribution of @{const measurable}-functions *}
--- a/src/HOL/ZF/Games.thy Thu Jun 25 22:56:33 2015 +0200
+++ b/src/HOL/ZF/Games.thy Thu Jun 25 23:33:47 2015 +0200
@@ -418,22 +418,22 @@
proof (induct x rule: wf_induct[OF wf_option_of])
case (1 "g")
show ?case
- proof (auto)
- {case (goal1 y)
- from goal1 have "(y, g) \<in> option_of" by (auto)
+ proof (auto, goals)
+ {case prems: (1 y)
+ from prems have "(y, g) \<in> option_of" by (auto)
with 1 have "ge_game (y, y)" by auto
- with goal1 have "\<not> ge_game (g, y)"
+ with prems have "\<not> ge_game (g, y)"
by (subst ge_game_eq, auto)
- with goal1 show ?case by auto}
+ with prems show ?case by auto}
note right = this
- {case (goal2 y)
- from goal2 have "(y, g) \<in> option_of" by (auto)
+ {case prems: (2 y)
+ from prems have "(y, g) \<in> option_of" by (auto)
with 1 have "ge_game (y, y)" by auto
- with goal2 have "\<not> ge_game (y, g)"
+ with prems have "\<not> ge_game (y, g)"
by (subst ge_game_eq, auto)
- with goal2 show ?case by auto}
+ with prems show ?case by auto}
note left = this
- {case goal3
+ {case 3
from left right show ?case
by (subst ge_game_eq, auto)
}
@@ -462,8 +462,8 @@
proof (induct a rule: induct_game)
case (1 a)
show ?case
- proof (rule allI | rule impI)+
- case (goal1 x y z)
+ proof ((rule allI | rule impI)+, goals)
+ case prems: (1 x y z)
show ?case
proof -
{ fix xr
@@ -471,10 +471,10 @@
assume a: "ge_game (z, xr)"
have "ge_game (y, xr)"
apply (rule 1[rule_format, where y="[y,z,xr]"])
- apply (auto intro: xr lprod_3_1 simp add: goal1 a)
+ apply (auto intro: xr lprod_3_1 simp add: prems a)
done
moreover from xr have "\<not> ge_game (y, xr)"
- by (simp add: goal1(2)[simplified ge_game_eq[of x y], rule_format, of xr, simplified xr])
+ by (simp add: prems(2)[simplified ge_game_eq[of x y], rule_format, of xr, simplified xr])
ultimately have "False" by auto
}
note xr = this
@@ -483,10 +483,10 @@
assume a: "ge_game (zl, x)"
have "ge_game (zl, y)"
apply (rule 1[rule_format, where y="[zl,x,y]"])
- apply (auto intro: zl lprod_3_2 simp add: goal1 a)
+ apply (auto intro: zl lprod_3_2 simp add: prems a)
done
moreover from zl have "\<not> ge_game (zl, y)"
- by (simp add: goal1(3)[simplified ge_game_eq[of y z], rule_format, of zl, simplified zl])
+ by (simp add: prems(3)[simplified ge_game_eq[of y z], rule_format, of zl, simplified zl])
ultimately have "False" by auto
}
note zl = this
@@ -542,21 +542,18 @@
lemma plus_game_zero_right[simp]: "plus_game G zero_game = G"
proof -
- {
- fix G H
- have "H = zero_game \<longrightarrow> plus_game G H = G "
- proof (induct G H rule: plus_game.induct, rule impI)
- case (goal1 G H)
- note induct_hyp = this[simplified goal1, simplified] and this
- show ?case
- apply (simp only: plus_game.simps[where G=G and H=H])
- apply (simp add: game_ext_eq goal1)
- apply (auto simp add:
- zimage_cong [where f = "\<lambda> g. plus_game g zero_game" and g = "id"]
- induct_hyp)
- done
- qed
- }
+ have "H = zero_game \<longrightarrow> plus_game G H = G " for G H
+ proof (induct G H rule: plus_game.induct, rule impI, goals)
+ case prems: (1 G H)
+ note induct_hyp = this[simplified prems, simplified] and this
+ show ?case
+ apply (simp only: plus_game.simps[where G=G and H=H])
+ apply (simp add: game_ext_eq prems)
+ apply (auto simp add:
+ zimage_cong [where f = "\<lambda> g. plus_game g zero_game" and g = "id"]
+ induct_hyp)
+ done
+ qed
then show ?thesis by auto
qed
@@ -585,36 +582,33 @@
lemma plus_game_assoc: "plus_game (plus_game F G) H = plus_game F (plus_game G H)"
proof -
- {
- fix a
- have "\<forall> F G H. a = [F, G, H] \<longrightarrow> plus_game (plus_game F G) H = plus_game F (plus_game G H)"
- proof (induct a rule: induct_game, (rule impI | rule allI)+)
- case (goal1 x F G H)
- let ?L = "plus_game (plus_game F G) H"
- let ?R = "plus_game F (plus_game G H)"
- note options_plus = left_options_plus right_options_plus
- {
- fix opt
- note hyp = goal1(1)[simplified goal1(2), rule_format]
- have F: "zin opt (options F) \<Longrightarrow> plus_game (plus_game opt G) H = plus_game opt (plus_game G H)"
- by (blast intro: hyp lprod_3_3)
- have G: "zin opt (options G) \<Longrightarrow> plus_game (plus_game F opt) H = plus_game F (plus_game opt H)"
- by (blast intro: hyp lprod_3_4)
- have H: "zin opt (options H) \<Longrightarrow> plus_game (plus_game F G) opt = plus_game F (plus_game G opt)"
- by (blast intro: hyp lprod_3_5)
- note F and G and H
- }
- note induct_hyp = this
- have "left_options ?L = left_options ?R \<and> right_options ?L = right_options ?R"
- by (auto simp add:
- plus_game.simps[where G="plus_game F G" and H=H]
- plus_game.simps[where G="F" and H="plus_game G H"]
- zet_ext_eq zunion zimage_iff options_plus
- induct_hyp left_imp_options right_imp_options)
- then show ?case
- by (simp add: game_ext_eq)
- qed
- }
+ have "\<forall>F G H. a = [F, G, H] \<longrightarrow> plus_game (plus_game F G) H = plus_game F (plus_game G H)" for a
+ proof (induct a rule: induct_game, (rule impI | rule allI)+, goals)
+ case prems: (1 x F G H)
+ let ?L = "plus_game (plus_game F G) H"
+ let ?R = "plus_game F (plus_game G H)"
+ note options_plus = left_options_plus right_options_plus
+ {
+ fix opt
+ note hyp = prems(1)[simplified prems(2), rule_format]
+ have F: "zin opt (options F) \<Longrightarrow> plus_game (plus_game opt G) H = plus_game opt (plus_game G H)"
+ by (blast intro: hyp lprod_3_3)
+ have G: "zin opt (options G) \<Longrightarrow> plus_game (plus_game F opt) H = plus_game F (plus_game opt H)"
+ by (blast intro: hyp lprod_3_4)
+ have H: "zin opt (options H) \<Longrightarrow> plus_game (plus_game F G) opt = plus_game F (plus_game G opt)"
+ by (blast intro: hyp lprod_3_5)
+ note F and G and H
+ }
+ note induct_hyp = this
+ have "left_options ?L = left_options ?R \<and> right_options ?L = right_options ?R"
+ by (auto simp add:
+ plus_game.simps[where G="plus_game F G" and H=H]
+ plus_game.simps[where G="F" and H="plus_game G H"]
+ zet_ext_eq zunion zimage_iff options_plus
+ induct_hyp left_imp_options right_imp_options)
+ then show ?case
+ by (simp add: game_ext_eq)
+ qed
then show ?thesis by auto
qed
@@ -632,58 +626,38 @@
qed
lemma eq_game_plus_inverse: "eq_game (plus_game x (neg_game x)) zero_game"
-proof (induct x rule: wf_induct[OF wf_option_of])
- case (goal1 x)
- { fix y
- assume "zin y (options x)"
- then have "eq_game (plus_game y (neg_game y)) zero_game"
- by (auto simp add: goal1)
- }
- note ihyp = this
- {
- fix y
- assume y: "zin y (right_options x)"
- have "\<not> (ge_game (zero_game, plus_game y (neg_game x)))"
- apply (subst ge_game.simps, simp)
- apply (rule exI[where x="plus_game y (neg_game y)"])
- apply (auto simp add: ihyp[of y, simplified y right_imp_options eq_game_def])
- apply (auto simp add: left_options_plus left_options_neg zunion zimage_iff intro: y)
- done
- }
- note case1 = this
- {
- fix y
- assume y: "zin y (left_options x)"
- have "\<not> (ge_game (zero_game, plus_game x (neg_game y)))"
- apply (subst ge_game.simps, simp)
- apply (rule exI[where x="plus_game y (neg_game y)"])
- apply (auto simp add: ihyp[of y, simplified y left_imp_options eq_game_def])
- apply (auto simp add: left_options_plus zunion zimage_iff intro: y)
- done
- }
- note case2 = this
- {
- fix y
- assume y: "zin y (left_options x)"
- have "\<not> (ge_game (plus_game y (neg_game x), zero_game))"
- apply (subst ge_game.simps, simp)
- apply (rule exI[where x="plus_game y (neg_game y)"])
- apply (auto simp add: ihyp[of y, simplified y left_imp_options eq_game_def])
- apply (auto simp add: right_options_plus right_options_neg zunion zimage_iff intro: y)
- done
- }
- note case3 = this
- {
- fix y
- assume y: "zin y (right_options x)"
- have "\<not> (ge_game (plus_game x (neg_game y), zero_game))"
- apply (subst ge_game.simps, simp)
- apply (rule exI[where x="plus_game y (neg_game y)"])
- apply (auto simp add: ihyp[of y, simplified y right_imp_options eq_game_def])
- apply (auto simp add: right_options_plus zunion zimage_iff intro: y)
- done
- }
- note case4 = this
+proof (induct x rule: wf_induct[OF wf_option_of], goals)
+ case prems: (1 x)
+ then have ihyp: "eq_game (plus_game y (neg_game y)) zero_game" if "zin y (options x)" for y
+ using that by (auto simp add: prems)
+ have case1: "\<not> (ge_game (zero_game, plus_game y (neg_game x)))"
+ if y: "zin y (right_options x)" for y
+ apply (subst ge_game.simps, simp)
+ apply (rule exI[where x="plus_game y (neg_game y)"])
+ apply (auto simp add: ihyp[of y, simplified y right_imp_options eq_game_def])
+ apply (auto simp add: left_options_plus left_options_neg zunion zimage_iff intro: y)
+ done
+ have case2: "\<not> (ge_game (zero_game, plus_game x (neg_game y)))"
+ if y: "zin y (left_options x)" for y
+ apply (subst ge_game.simps, simp)
+ apply (rule exI[where x="plus_game y (neg_game y)"])
+ apply (auto simp add: ihyp[of y, simplified y left_imp_options eq_game_def])
+ apply (auto simp add: left_options_plus zunion zimage_iff intro: y)
+ done
+ have case3: "\<not> (ge_game (plus_game y (neg_game x), zero_game))"
+ if y: "zin y (left_options x)" for y
+ apply (subst ge_game.simps, simp)
+ apply (rule exI[where x="plus_game y (neg_game y)"])
+ apply (auto simp add: ihyp[of y, simplified y left_imp_options eq_game_def])
+ apply (auto simp add: right_options_plus right_options_neg zunion zimage_iff intro: y)
+ done
+ have case4: "\<not> (ge_game (plus_game x (neg_game y), zero_game))"
+ if y: "zin y (right_options x)" for y
+ apply (subst ge_game.simps, simp)
+ apply (rule exI[where x="plus_game y (neg_game y)"])
+ apply (auto simp add: ihyp[of y, simplified y right_imp_options eq_game_def])
+ apply (auto simp add: right_options_plus zunion zimage_iff intro: y)
+ done
show ?case
apply (simp add: eq_game_def)
apply (simp add: ge_game.simps[of "plus_game x (neg_game x)" "zero_game"])
@@ -695,112 +669,109 @@
lemma ge_plus_game_left: "ge_game (y,z) = ge_game (plus_game x y, plus_game x z)"
proof -
- { fix a
- have "\<forall> x y z. a = [x,y,z] \<longrightarrow> ge_game (y,z) = ge_game (plus_game x y, plus_game x z)"
- proof (induct a rule: induct_game, (rule impI | rule allI)+)
- case (goal1 a x y z)
- note induct_hyp = goal1(1)[rule_format, simplified goal1(2)]
- {
- assume hyp: "ge_game(plus_game x y, plus_game x z)"
- have "ge_game (y, z)"
- proof -
- { fix yr
- assume yr: "zin yr (right_options y)"
- from hyp have "\<not> (ge_game (plus_game x z, plus_game x yr))"
- by (auto simp add: ge_game_eq[of "plus_game x y" "plus_game x z"]
- right_options_plus zunion zimage_iff intro: yr)
- then have "\<not> (ge_game (z, yr))"
- apply (subst induct_hyp[where y="[x, z, yr]", of "x" "z" "yr"])
- apply (simp_all add: yr lprod_3_6)
- done
- }
- note yr = this
- { fix zl
- assume zl: "zin zl (left_options z)"
- from hyp have "\<not> (ge_game (plus_game x zl, plus_game x y))"
- by (auto simp add: ge_game_eq[of "plus_game x y" "plus_game x z"]
- left_options_plus zunion zimage_iff intro: zl)
- then have "\<not> (ge_game (zl, y))"
- apply (subst goal1(1)[rule_format, where y="[x, zl, y]", of "x" "zl" "y"])
- apply (simp_all add: goal1(2) zl lprod_3_7)
- done
- }
- note zl = this
- show "ge_game (y, z)"
- apply (subst ge_game_eq)
- apply (auto simp add: yr zl)
+ have "\<forall>x y z. a = [x,y,z] \<longrightarrow> ge_game (y,z) = ge_game (plus_game x y, plus_game x z)" for a
+ proof (induct a rule: induct_game, (rule impI | rule allI)+, goals)
+ case prems: (1 a x y z)
+ note induct_hyp = prems(1)[rule_format, simplified prems(2)]
+ {
+ assume hyp: "ge_game(plus_game x y, plus_game x z)"
+ have "ge_game (y, z)"
+ proof -
+ { fix yr
+ assume yr: "zin yr (right_options y)"
+ from hyp have "\<not> (ge_game (plus_game x z, plus_game x yr))"
+ by (auto simp add: ge_game_eq[of "plus_game x y" "plus_game x z"]
+ right_options_plus zunion zimage_iff intro: yr)
+ then have "\<not> (ge_game (z, yr))"
+ apply (subst induct_hyp[where y="[x, z, yr]", of "x" "z" "yr"])
+ apply (simp_all add: yr lprod_3_6)
done
- qed
- }
- note right_imp_left = this
- {
- assume yz: "ge_game (y, z)"
- {
- fix x'
- assume x': "zin x' (right_options x)"
- assume hyp: "ge_game (plus_game x z, plus_game x' y)"
- then have n: "\<not> (ge_game (plus_game x' y, plus_game x' z))"
- by (auto simp add: ge_game_eq[of "plus_game x z" "plus_game x' y"]
- right_options_plus zunion zimage_iff intro: x')
- have t: "ge_game (plus_game x' y, plus_game x' z)"
- apply (subst induct_hyp[symmetric])
- apply (auto intro: lprod_3_3 x' yz)
+ }
+ note yr = this
+ { fix zl
+ assume zl: "zin zl (left_options z)"
+ from hyp have "\<not> (ge_game (plus_game x zl, plus_game x y))"
+ by (auto simp add: ge_game_eq[of "plus_game x y" "plus_game x z"]
+ left_options_plus zunion zimage_iff intro: zl)
+ then have "\<not> (ge_game (zl, y))"
+ apply (subst prems(1)[rule_format, where y="[x, zl, y]", of "x" "zl" "y"])
+ apply (simp_all add: prems(2) zl lprod_3_7)
done
- from n t have "False" by blast
- }
- note case1 = this
- {
- fix x'
- assume x': "zin x' (left_options x)"
- assume hyp: "ge_game (plus_game x' z, plus_game x y)"
- then have n: "\<not> (ge_game (plus_game x' y, plus_game x' z))"
- by (auto simp add: ge_game_eq[of "plus_game x' z" "plus_game x y"]
- left_options_plus zunion zimage_iff intro: x')
- have t: "ge_game (plus_game x' y, plus_game x' z)"
- apply (subst induct_hyp[symmetric])
- apply (auto intro: lprod_3_3 x' yz)
- done
- from n t have "False" by blast
- }
- note case3 = this
- {
- fix y'
- assume y': "zin y' (right_options y)"
- assume hyp: "ge_game (plus_game x z, plus_game x y')"
- then have "ge_game(z, y')"
- apply (subst induct_hyp[of "[x, z, y']" "x" "z" "y'"])
- apply (auto simp add: hyp lprod_3_6 y')
- done
- with yz have "ge_game (y, y')"
- by (blast intro: ge_game_trans)
- with y' have "False" by (auto simp add: ge_game_leftright_refl)
- }
- note case2 = this
- {
- fix z'
- assume z': "zin z' (left_options z)"
- assume hyp: "ge_game (plus_game x z', plus_game x y)"
- then have "ge_game(z', y)"
- apply (subst induct_hyp[of "[x, z', y]" "x" "z'" "y"])
- apply (auto simp add: hyp lprod_3_7 z')
- done
- with yz have "ge_game (z', z)"
- by (blast intro: ge_game_trans)
- with z' have "False" by (auto simp add: ge_game_leftright_refl)
- }
- note case4 = this
- have "ge_game(plus_game x y, plus_game x z)"
+ }
+ note zl = this
+ show "ge_game (y, z)"
apply (subst ge_game_eq)
- apply (auto simp add: right_options_plus left_options_plus zunion zimage_iff)
- apply (auto intro: case1 case2 case3 case4)
+ apply (auto simp add: yr zl)
done
+ qed
+ }
+ note right_imp_left = this
+ {
+ assume yz: "ge_game (y, z)"
+ {
+ fix x'
+ assume x': "zin x' (right_options x)"
+ assume hyp: "ge_game (plus_game x z, plus_game x' y)"
+ then have n: "\<not> (ge_game (plus_game x' y, plus_game x' z))"
+ by (auto simp add: ge_game_eq[of "plus_game x z" "plus_game x' y"]
+ right_options_plus zunion zimage_iff intro: x')
+ have t: "ge_game (plus_game x' y, plus_game x' z)"
+ apply (subst induct_hyp[symmetric])
+ apply (auto intro: lprod_3_3 x' yz)
+ done
+ from n t have "False" by blast
+ }
+ note case1 = this
+ {
+ fix x'
+ assume x': "zin x' (left_options x)"
+ assume hyp: "ge_game (plus_game x' z, plus_game x y)"
+ then have n: "\<not> (ge_game (plus_game x' y, plus_game x' z))"
+ by (auto simp add: ge_game_eq[of "plus_game x' z" "plus_game x y"]
+ left_options_plus zunion zimage_iff intro: x')
+ have t: "ge_game (plus_game x' y, plus_game x' z)"
+ apply (subst induct_hyp[symmetric])
+ apply (auto intro: lprod_3_3 x' yz)
+ done
+ from n t have "False" by blast
}
- note left_imp_right = this
- show ?case by (auto intro: right_imp_left left_imp_right)
- qed
- }
- note a = this[of "[x, y, z]"]
- then show ?thesis by blast
+ note case3 = this
+ {
+ fix y'
+ assume y': "zin y' (right_options y)"
+ assume hyp: "ge_game (plus_game x z, plus_game x y')"
+ then have "ge_game(z, y')"
+ apply (subst induct_hyp[of "[x, z, y']" "x" "z" "y'"])
+ apply (auto simp add: hyp lprod_3_6 y')
+ done
+ with yz have "ge_game (y, y')"
+ by (blast intro: ge_game_trans)
+ with y' have "False" by (auto simp add: ge_game_leftright_refl)
+ }
+ note case2 = this
+ {
+ fix z'
+ assume z': "zin z' (left_options z)"
+ assume hyp: "ge_game (plus_game x z', plus_game x y)"
+ then have "ge_game(z', y)"
+ apply (subst induct_hyp[of "[x, z', y]" "x" "z'" "y"])
+ apply (auto simp add: hyp lprod_3_7 z')
+ done
+ with yz have "ge_game (z', z)"
+ by (blast intro: ge_game_trans)
+ with z' have "False" by (auto simp add: ge_game_leftright_refl)
+ }
+ note case4 = this
+ have "ge_game(plus_game x y, plus_game x z)"
+ apply (subst ge_game_eq)
+ apply (auto simp add: right_options_plus left_options_plus zunion zimage_iff)
+ apply (auto intro: case1 case2 case3 case4)
+ done
+ }
+ note left_imp_right = this
+ show ?case by (auto intro: right_imp_left left_imp_right)
+ qed
+ from this[of "[x, y, z]"] show ?thesis by blast
qed
lemma ge_plus_game_right: "ge_game (y,z) = ge_game(plus_game y x, plus_game z x)"
@@ -808,34 +779,31 @@
lemma ge_neg_game: "ge_game (neg_game x, neg_game y) = ge_game (y, x)"
proof -
- { fix a
- have "\<forall> x y. a = [x, y] \<longrightarrow> ge_game (neg_game x, neg_game y) = ge_game (y, x)"
- proof (induct a rule: induct_game, (rule impI | rule allI)+)
- case (goal1 a x y)
- note ihyp = goal1(1)[rule_format, simplified goal1(2)]
- { fix xl
- assume xl: "zin xl (left_options x)"
- have "ge_game (neg_game y, neg_game xl) = ge_game (xl, y)"
- apply (subst ihyp)
- apply (auto simp add: lprod_2_1 xl)
- done
- }
- note xl = this
- { fix yr
- assume yr: "zin yr (right_options y)"
- have "ge_game (neg_game yr, neg_game x) = ge_game (x, yr)"
- apply (subst ihyp)
- apply (auto simp add: lprod_2_2 yr)
- done
- }
- note yr = this
- show ?case
- by (auto simp add: ge_game_eq[of "neg_game x" "neg_game y"] ge_game_eq[of "y" "x"]
- right_options_neg left_options_neg zimage_iff xl yr)
- qed
- }
- note a = this[of "[x,y]"]
- then show ?thesis by blast
+ have "\<forall>x y. a = [x, y] \<longrightarrow> ge_game (neg_game x, neg_game y) = ge_game (y, x)" for a
+ proof (induct a rule: induct_game, (rule impI | rule allI)+, goals)
+ case prems: (1 a x y)
+ note ihyp = prems(1)[rule_format, simplified prems(2)]
+ { fix xl
+ assume xl: "zin xl (left_options x)"
+ have "ge_game (neg_game y, neg_game xl) = ge_game (xl, y)"
+ apply (subst ihyp)
+ apply (auto simp add: lprod_2_1 xl)
+ done
+ }
+ note xl = this
+ { fix yr
+ assume yr: "zin yr (right_options y)"
+ have "ge_game (neg_game yr, neg_game x) = ge_game (x, yr)"
+ apply (subst ihyp)
+ apply (auto simp add: lprod_2_2 yr)
+ done
+ }
+ note yr = this
+ show ?case
+ by (auto simp add: ge_game_eq[of "neg_game x" "neg_game y"] ge_game_eq[of "y" "x"]
+ right_options_neg left_options_neg zimage_iff xl yr)
+ qed
+ from this[of "[x,y]"] show ?thesis by blast
qed
definition eq_game_rel :: "(game * game) set" where
@@ -974,4 +942,3 @@
qed
end
-
--- a/src/HOL/ex/Tree23.thy Thu Jun 25 22:56:33 2015 +0200
+++ b/src/HOL/ex/Tree23.thy Thu Jun 25 23:33:47 2015 +0200
@@ -377,16 +377,26 @@
done
} note B = this
show "full (Suc n) t \<Longrightarrow> dfull n (del k t)"
- proof (induct k t arbitrary: n rule: del.induct)
- { case goal1 thus "dfull n (del (Some k) Empty)" by simp }
- { case goal2 thus "dfull n (del None (Branch2 Empty p Empty))" by simp }
- { case goal3 thus "dfull n (del None (Branch3 Empty p Empty q Empty))"
- by simp }
- { case goal4 thus "dfull n (del (Some v) (Branch2 Empty p Empty))"
- by (simp split: ord.split) }
- { case goal5 thus "dfull n (del (Some v) (Branch3 Empty p Empty q Empty))"
- by (simp split: ord.split) }
- { case goal26 thus ?case by simp }
+ proof (induct k t arbitrary: n rule: del.induct, goals)
+ case (1 k n)
+ thus "dfull n (del (Some k) Empty)" by simp
+ next
+ case (2 p n)
+ thus "dfull n (del None (Branch2 Empty p Empty))" by simp
+ next
+ case (3 p q n)
+ thus "dfull n (del None (Branch3 Empty p Empty q Empty))" by simp
+ next
+ case (4 v p n)
+ thus "dfull n (del (Some v) (Branch2 Empty p Empty))"
+ by (simp split: ord.split)
+ next
+ case (5 v p q n)
+ thus "dfull n (del (Some v) (Branch3 Empty p Empty q Empty))"
+ by (simp split: ord.split)
+ next
+ case (26 n)
+ thus ?case by simp
qed (fact A | fact B)+
qed