--- a/Admin/isatest/settings/at64-poly Thu Jun 25 15:01:43 2015 +0200
+++ b/Admin/isatest/settings/at64-poly Thu Jun 25 23:51:54 2015 +0200
@@ -4,7 +4,7 @@
ML_PLATFORM="$ISABELLE_PLATFORM64"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
-ML_OPTIONS="--minheap 2000 --maxheap 8000 --gcthreads 1"
+ML_OPTIONS="--minheap 4000 --maxheap 16000 --gcthreads 1"
ISABELLE_HOME_USER=~/isabelle-at64-poly
--- a/NEWS Thu Jun 25 15:01:43 2015 +0200
+++ b/NEWS Thu Jun 25 23:51:54 2015 +0200
@@ -77,6 +77,13 @@
INCOMPATIBILITY, need to adapt uses of case facts in exotic situations,
and always put attributes in front.
+* Proof method "goals" turns the current subgoals into cases within the
+context; the conclusion is bound to variable ?case in each case.
+
+* The undocumented feature of implicit cases goal1, goal2, goal3, etc.
+is marked as legacy, and will be removed eventually. Note that proof
+method "goals" achieves a similar effect within regular Isar.
+
* Nesting of Isar goal structure has been clarified: the context after
the initial backwards refinement is retained for the whole proof, within
all its context sections (as indicated via 'next'). This is e.g.
--- a/src/Doc/Isar_Ref/Proof.thy Thu Jun 25 15:01:43 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy Thu Jun 25 23:51:54 2015 +0200
@@ -818,6 +818,7 @@
\begin{matharray}{rcl}
@{command_def "print_rules"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\[0.5ex]
@{method_def "-"} & : & @{text method} \\
+ @{method_def "goals"} & : & @{text method} \\
@{method_def "fact"} & : & @{text method} \\
@{method_def "assumption"} & : & @{text method} \\
@{method_def "this"} & : & @{text method} \\
@@ -832,6 +833,8 @@
\end{matharray}
@{rail \<open>
+ @@{method goals} (@{syntax name}*)
+ ;
@@{method fact} @{syntax thmrefs}?
;
@@{method (Pure) rule} @{syntax thmrefs}?
@@ -861,12 +864,23 @@
rule declarations of the classical reasoner
(\secref{sec:classical}).
- \item ``@{method "-"}'' (minus) does nothing but insert the forward
- chaining facts as premises into the goal. Note that command
- @{command_ref "proof"} without any method actually performs a single
- reduction step using the @{method_ref (Pure) rule} method; thus a plain
- \emph{do-nothing} proof step would be ``@{command "proof"}~@{text
- "-"}'' rather than @{command "proof"} alone.
+ \item ``@{method "-"}'' (minus) inserts the forward chaining facts as
+ premises into the goal, and nothing else.
+
+ Note that command @{command_ref "proof"} without any method actually
+ performs a single reduction step using the @{method_ref (Pure) rule}
+ method; thus a plain \emph{do-nothing} proof step would be ``@{command
+ "proof"}~@{text "-"}'' rather than @{command "proof"} alone.
+
+ \item @{method "goals"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} is like ``@{method "-"}'', but
+ the current subgoals are turned into cases within the context (see also
+ \secref{sec:cases-induct}). The specified case names are used if present;
+ otherwise cases are numbered starting from 1.
+
+ Invoking cases in the subsequent proof body via the @{command_ref case}
+ command will @{command fix} goal parameters, @{command assume} goal
+ premises, and @{command let} variable @{variable_ref ?case} refer to the
+ conclusion.
\item @{method "fact"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} composes some fact from
@{text "a\<^sub>1, \<dots>, a\<^sub>n"} (or implicitly from the current proof context)
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Thu Jun 25 15:01:43 2015 +0200
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Thu Jun 25 23:51:54 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 15:01:43 2015 +0200
+++ b/src/HOL/GCD.thy Thu Jun 25 23:51:54 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 15:01:43 2015 +0200
+++ b/src/HOL/Library/Extended_Real.thy Thu Jun 25 23:51:54 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 15:01:43 2015 +0200
+++ b/src/HOL/Library/Product_Order.thy Thu Jun 25 23:51:54 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 15:01:43 2015 +0200
+++ b/src/HOL/Library/RBT_Set.thy Thu Jun 25 23:51:54 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 15:01:43 2015 +0200
+++ b/src/HOL/Library/While_Combinator.thy Thu Jun 25 23:51:54 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 15:01:43 2015 +0200
+++ b/src/HOL/List.thy Thu Jun 25 23:51:54 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 15:01:43 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy Thu Jun 25 23:51:54 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 15:01:43 2015 +0200
+++ b/src/HOL/Nominal/Examples/Pattern.thy Thu Jun 25 23:51:54 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 15:01:43 2015 +0200
+++ b/src/HOL/Nominal/Nominal.thy Thu Jun 25 23:51:54 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 15:01:43 2015 +0200
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy Thu Jun 25 23:51:54 2015 +0200
@@ -1584,14 +1584,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 15:01:43 2015 +0200
+++ b/src/HOL/Probability/Embed_Measure.thy Thu Jun 25 23:51:54 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 15:01:43 2015 +0200
+++ b/src/HOL/Probability/Finite_Product_Measure.thy Thu Jun 25 23:51:54 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 15:01:43 2015 +0200
+++ b/src/HOL/Probability/Information.thy Thu Jun 25 23:51:54 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 15:01:43 2015 +0200
+++ b/src/HOL/Probability/Measure_Space.thy Thu Jun 25 23:51:54 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/Tools/Predicate_Compile/predicate_compile_core.ML Thu Jun 25 15:01:43 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Jun 25 23:51:54 2015 +0200
@@ -1649,7 +1649,7 @@
val case_env = map2 (fn p => fn c => (Long_Name.base_name p, SOME c)) preds cases
val lthy'' = lthy'
|> fold Variable.auto_fixes cases_rules
- |> Proof_Context.update_cases true case_env
+ |> Proof_Context.update_cases case_env
fun after_qed thms goal_ctxt =
let
val global_thms = Proof_Context.export goal_ctxt
--- a/src/HOL/ZF/Games.thy Thu Jun 25 15:01:43 2015 +0200
+++ b/src/HOL/ZF/Games.thy Thu Jun 25 23:51:54 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 15:01:43 2015 +0200
+++ b/src/HOL/ex/Tree23.thy Thu Jun 25 23:51:54 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
--- a/src/Pure/Isar/args.ML Thu Jun 25 15:01:43 2015 +0200
+++ b/src/Pure/Isar/args.ML Thu Jun 25 23:51:54 2015 +0200
@@ -21,14 +21,15 @@
val bracks: 'a parser -> 'a parser
val mode: string -> bool parser
val maybe: 'a parser -> 'a option parser
+ val name_token: Token.T parser
+ val name_inner_syntax: string parser
+ val name_input: Input.source parser
+ val name: string parser
val cartouche_inner_syntax: string parser
val cartouche_input: Input.source parser
val text_token: Token.T parser
val text_input: Input.source parser
val text: string parser
- val name_inner_syntax: string parser
- val name_input: Input.source parser
- val name: string parser
val binding: binding parser
val alt_name: string parser
val symbol: string parser
@@ -92,8 +93,6 @@
else Scan.fail
end);
-val named = ident || string;
-
val add = $$$ "add";
val del = $$$ "del";
val colon = $$$ ":";
@@ -107,18 +106,19 @@
fun mode s = Scan.optional (parens ($$$ s) >> K true) false;
fun maybe scan = $$$ "_" >> K NONE || scan >> SOME;
+val name_token = ident || string;
+val name_inner_syntax = name_token >> Token.inner_syntax_of;
+val name_input = name_token >> Token.input_of;
+val name = name_token >> Token.content_of;
+
val cartouche = Parse.token Parse.cartouche;
val cartouche_inner_syntax = cartouche >> Token.inner_syntax_of;
val cartouche_input = cartouche >> Token.input_of;
-val text_token = named || Parse.token (Parse.verbatim || Parse.cartouche);
+val text_token = name_token || Parse.token (Parse.verbatim || Parse.cartouche);
val text_input = text_token >> Token.input_of;
val text = text_token >> Token.content_of;
-val name_inner_syntax = named >> Token.inner_syntax_of;
-val name_input = named >> Token.input_of;
-
-val name = named >> Token.content_of;
val binding = Parse.position name >> Binding.make;
val alt_name = alt_string >> Token.content_of;
val symbol = symbolic >> Token.content_of;
@@ -144,19 +144,22 @@
val internal_attribute = value (fn Token.Attribute att => att);
val internal_declaration = value (fn Token.Declaration decl => decl);
-fun named_source read = internal_source || named >> evaluate Token.Source read;
+fun named_source read = internal_source || name_token >> evaluate Token.Source read;
-fun named_typ read = internal_typ || named >> evaluate Token.Typ (read o Token.inner_syntax_of);
-fun named_term read = internal_term || named >> evaluate Token.Term (read o Token.inner_syntax_of);
+fun named_typ read =
+ internal_typ || name_token >> evaluate Token.Typ (read o Token.inner_syntax_of);
+
+fun named_term read =
+ internal_term || name_token >> evaluate Token.Term (read o Token.inner_syntax_of);
fun named_fact get =
internal_fact ||
- named >> evaluate Token.Fact (get o Token.content_of) >> #2 ||
+ name_token >> evaluate Token.Fact (get o Token.content_of) >> #2 ||
alt_string >> evaluate Token.Fact (get o Token.inner_syntax_of) >> #2;
fun named_attribute att =
internal_attribute ||
- named >> evaluate Token.Attribute (fn tok => att (Token.content_of tok, Token.pos_of tok));
+ name_token >> evaluate Token.Attribute (fn tok => att (Token.content_of tok, Token.pos_of tok));
fun text_declaration read =
internal_declaration || text_token >> evaluate Token.Declaration (read o Token.input_of);
@@ -203,7 +206,7 @@
fun attribs check =
let
fun intern tok = check (Token.content_of tok, Token.pos_of tok);
- val attrib_name = internal_name >> #1 || (symbolic || named) >> evaluate Token.name0 intern;
+ val attrib_name = internal_name >> #1 || (symbolic || name_token) >> evaluate Token.name0 intern;
val attrib = Parse.position attrib_name -- Parse.!!! Parse.args >> uncurry Token.src;
in $$$ "[" |-- Parse.!!! (Parse.list attrib --| $$$ "]") end;
--- a/src/Pure/Isar/method.ML Thu Jun 25 15:01:43 2015 +0200
+++ b/src/Pure/Isar/method.ML Thu Jun 25 23:51:54 2015 +0200
@@ -17,6 +17,7 @@
val SIMPLE_METHOD: tactic -> method
val SIMPLE_METHOD': (int -> tactic) -> method
val SIMPLE_METHOD'': ((int -> tactic) -> tactic) -> (int -> tactic) -> method
+ val goals_tac: Proof.context -> string list -> cases_tactic
val cheating: Proof.context -> bool -> method
val intro: Proof.context -> thm list -> method
val elim: Proof.context -> thm list -> method
@@ -126,6 +127,17 @@
end;
+(* goals as cases *)
+
+fun goals_tac ctxt case_names st =
+ let
+ val cases =
+ (if null case_names then map string_of_int (1 upto Thm.nprems_of st) else case_names)
+ |> map (rpair [] o rpair [])
+ |> Rule_Cases.make_common ctxt (Thm.prop_of (Rule_Cases.internalize_params st));
+ in Seq.single (cases, st) end;
+
+
(* cheating *)
fun cheating ctxt int = METHOD (fn _ => fn st =>
@@ -676,9 +688,21 @@
setup @{binding sleep} (Scan.lift Parse.real >> (fn s => fn _ => fn _ => sleep (seconds s)))
"succeed after delay (in seconds)" #>
setup @{binding "-"} (Scan.succeed (K insert_facts))
- "do nothing (insert current facts only)" #>
+ "insert current facts, nothing else" #>
+ setup @{binding goals} (Scan.lift (Scan.repeat Args.name_token) >> (fn names => fn ctxt =>
+ METHOD_CASES (fn facts =>
+ Seq.THEN (ALLGOALS (insert_tac facts), fn st =>
+ let
+ val _ =
+ (case drop (Thm.nprems_of st) names of
+ [] => ()
+ | bad => (* FIXME Seq.Error *)
+ error ("Excessive case names: " ^ commas_quote (map Token.content_of bad) ^
+ Position.here (Position.set_range (Token.range_of bad))));
+ in goals_tac ctxt (map Token.content_of names) st end))))
+ "insert facts and bind cases for goals" #>
setup @{binding insert} (Attrib.thms >> (K o insert))
- "insert theorems, ignoring facts (improper)" #>
+ "insert theorems, ignoring facts" #>
setup @{binding intro} (Attrib.thms >> (fn ths => fn ctxt => intro ctxt ths))
"repeatedly apply introduction rules" #>
setup @{binding elim} (Attrib.thms >> (fn ths => fn ctxt => elim ctxt ths))
--- a/src/Pure/Isar/proof.ML Thu Jun 25 15:01:43 2015 +0200
+++ b/src/Pure/Isar/proof.ML Thu Jun 25 23:51:54 2015 +0200
@@ -422,8 +422,8 @@
|> Seq.map (fn (meth_cases, goal') =>
state
|> map_goal
- (Proof_Context.update_cases false (no_goal_cases goal @ goal_cases ctxt goal') #>
- Proof_Context.update_cases true meth_cases)
+ (Proof_Context.update_cases_legacy (no_goal_cases goal @ goal_cases ctxt goal') #>
+ Proof_Context.update_cases meth_cases)
(K (statement, using, goal', before_qed, after_qed)) I));
in
--- a/src/Pure/Isar/proof_context.ML Thu Jun 25 15:01:43 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML Thu Jun 25 23:51:54 2015 +0200
@@ -139,8 +139,8 @@
val add_assms_cmd: Assumption.export ->
(Thm.binding * (string * string list) list) list ->
Proof.context -> (string * thm list) list * Proof.context
- val dest_cases: Proof.context -> (string * (Rule_Cases.T * bool)) list
- val update_cases: bool -> (string * Rule_Cases.T option) list -> Proof.context -> Proof.context
+ val update_cases: (string * Rule_Cases.T option) list -> Proof.context -> Proof.context
+ val update_cases_legacy: (string * Rule_Cases.T option) list -> Proof.context -> Proof.context
val apply_case: Rule_Cases.T -> Proof.context -> (string * term list) list * Proof.context
val check_case: Proof.context -> bool ->
string * Position.T -> binding option list -> Rule_Cases.T
@@ -203,7 +203,7 @@
(** Isar proof context information **)
-type cases = ((Rule_Cases.T * bool) * int) Name_Space.table;
+type cases = ((Rule_Cases.T * {legacy: bool}) * int) Name_Space.table;
val empty_cases: cases = Name_Space.empty_table Markup.caseN;
datatype data =
@@ -213,7 +213,7 @@
tsig: Type.tsig * Type.tsig, (*local/global type signature -- local name space / defsort only*)
consts: Consts.T * Consts.T, (*local/global consts -- local name space / abbrevs only*)
facts: Facts.T, (*local facts, based on initial global facts*)
- cases: cases}; (*named case contexts: case, is_proper, running index*)
+ cases: cases}; (*named case contexts: case, legacy, running index*)
fun make_data (mode, syntax, tsig, consts, facts, cases) =
Data {mode = mode, syntax = syntax, tsig = tsig, consts = consts, facts = facts, cases = cases};
@@ -1202,26 +1202,30 @@
fun update_case _ _ ("", _) res = res
| update_case _ _ (name, NONE) (cases, index) =
(Name_Space.del_table name cases, index)
- | update_case context is_proper (name, SOME c) (cases, index) =
+ | update_case context legacy (name, SOME c) (cases, index) =
let
- val binding = Binding.name name |> not is_proper ? Binding.concealed;
- val (_, cases') = Name_Space.define context false (binding, ((c, is_proper), index)) cases;
+ val binding = Binding.name name |> legacy ? Binding.concealed;
+ val (_, cases') = cases
+ |> Name_Space.define context false (binding, ((c, {legacy = legacy}), index));
val index' = index + 1;
in (cases', index') end;
+fun update_cases' legacy args ctxt =
+ let
+ val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.global_naming);
+ val cases = cases_of ctxt;
+ val index = Name_Space.fold_table (fn _ => Integer.add 1) cases 0;
+ val (cases', _) = fold (update_case context legacy) args (cases, index);
+ in map_cases (K cases') ctxt end;
+
fun fix (b, T) ctxt =
let val ([x], ctxt') = add_fixes [(b, SOME T, NoSyn)] ctxt
in (Free (x, T), ctxt') end;
in
-fun update_cases is_proper args ctxt =
- let
- val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.global_naming);
- val cases = cases_of ctxt;
- val index = Name_Space.fold_table (fn _ => Integer.add 1) cases 0;
- val (cases', _) = fold (update_case context is_proper) args (cases, index);
- in map_cases (K cases') ctxt end;
+val update_cases = update_cases' false;
+val update_cases_legacy = update_cases' true;
fun case_result c ctxt =
let
@@ -1231,7 +1235,7 @@
in
ctxt'
|> fold (cert_maybe_bind_term o drop_schematic) binds
- |> update_cases true (map (apsnd SOME) cases)
+ |> update_cases (map (apsnd SOME) cases)
|> pair (assumes, (binds, cases))
end;
@@ -1239,9 +1243,13 @@
fun check_case ctxt internal (name, pos) fxs =
let
- val (_, ((Rule_Cases.Case {fixes, assumes, binds, cases}, is_proper), _)) =
+ val (_, ((Rule_Cases.Case {fixes, assumes, binds, cases}, {legacy}), _)) =
Name_Space.check (Context.Proof ctxt) (cases_of ctxt) (name, pos);
- val _ = if is_proper then () else Context_Position.report ctxt pos Markup.improper;
+ val _ =
+ if legacy then
+ legacy_feature ("Bad case " ^ quote name ^ Position.here pos ^
+ " -- use proof method \"goals\" instead")
+ else ();
val _ = List.app (fn NONE => () | SOME b => ignore (check_var internal b)) fxs;
fun replace (opt_x :: xs) ((y, T) :: ys) = (the_default y opt_x, T) :: replace xs ys
@@ -1357,8 +1365,8 @@
fun pretty_cases ctxt =
let
- fun mk_case (_, (_, false)) = NONE
- | mk_case (name, (c as Rule_Cases.Case {fixes, ...}, true)) =
+ fun mk_case (_, (_, {legacy = true})) = NONE
+ | mk_case (name, (c as Rule_Cases.Case {fixes, ...}, {legacy = false})) =
SOME (name, (fixes, case_result c ctxt));
val cases = dest_cases ctxt |> map_filter mk_case;
in
--- a/src/Pure/Isar/rule_cases.ML Thu Jun 25 15:01:43 2015 +0200
+++ b/src/Pure/Isar/rule_cases.ML Thu Jun 25 23:51:54 2015 +0200
@@ -27,10 +27,9 @@
cases: (string * T) list}
val case_hypsN: string
val strip_params: term -> (string * typ) list
- val make_common: Proof.context -> term ->
- ((string * string list) * string list) list -> cases
- val make_nested: Proof.context -> term -> term ->
- ((string * string list) * string list) list -> cases
+ type info = ((string * string list) * string list) list
+ val make_common: Proof.context -> term -> info -> cases
+ val make_nested: Proof.context -> term -> term -> info -> cases
val apply: term list -> T -> T
val consume: Proof.context -> thm list -> thm list -> ('a * int) * thm ->
(('a * (int * thm list)) * thm) Seq.seq
@@ -51,7 +50,7 @@
val cases_open: attribute
val internalize_params: thm -> thm
val save: thm -> thm -> thm
- val get: thm -> ((string * string list) * string list) list * int
+ val get: thm -> info * int
val rename_params: string list list -> thm -> thm
val params: string list list -> attribute
val mutual_rule: Proof.context -> thm list -> (int list * thm) option
@@ -77,6 +76,8 @@
val strip_params = map (apfst (perhaps (try Name.dest_skolem))) o Logic.strip_params;
+type info = ((string * string list) * string list) list;
+
local
fun app us t = Term.betapplys (t, us);
@@ -221,13 +222,13 @@
in
-fun consume ctxt defs facts ((xx, n), th) =
+fun consume ctxt defs facts ((a, n), th) =
let val m = Int.min (length facts, n) in
th
|> unfold_prems ctxt n defs
|> unfold_prems_concls ctxt defs
|> Drule.multi_resolve (SOME ctxt) (take m facts)
- |> Seq.map (pair (xx, (n - m, drop m facts)))
+ |> Seq.map (pair (a, (n - m, drop m facts)))
end;
end;
@@ -424,8 +425,8 @@
(case lookup_cases_hyp_names th of
NONE => replicate (length cases) []
| SOME names => names);
- fun regroup ((name,concls),hyps) = ((name,hyps),concls)
- in (map regroup (cases ~~ cases_hyps), n) end;
+ fun regroup (name, concls) hyps = ((name, hyps), concls);
+ in (map2 regroup cases cases_hyps, n) end;
(* params *)
--- a/src/Tools/induct.ML Thu Jun 25 15:01:43 2015 +0200
+++ b/src/Tools/induct.ML Thu Jun 25 23:51:54 2015 +0200
@@ -74,8 +74,7 @@
val cases_tac: Proof.context -> bool -> term option list list -> thm option ->
thm list -> int -> cases_tactic
val get_inductT: Proof.context -> term option list list -> thm list list
- type case_data = (((string * string list) * string list) list * int) (* FIXME -> rule_cases.ML *)
- val gen_induct_tac: (case_data * thm -> case_data * thm) ->
+ val gen_induct_tac: ((Rule_Cases.info * int) * thm -> (Rule_Cases.info * int) * thm) ->
Proof.context -> bool -> (binding option * (term * bool)) option list list ->
(string * typ) list list -> term option list -> thm list option ->
thm list -> int -> cases_tactic
@@ -127,15 +126,15 @@
fun conv1 0 ctxt = Conv.forall_conv (cv o snd) ctxt
| conv1 k ctxt =
Conv.rewr_conv @{thm swap_params} then_conv
- Conv.forall_conv (conv1 (k - 1) o snd) ctxt
+ Conv.forall_conv (conv1 (k - 1) o snd) ctxt;
fun conv2 0 ctxt = conv1 j ctxt
- | conv2 k ctxt = Conv.forall_conv (conv2 (k - 1) o snd) ctxt
+ | conv2 k ctxt = Conv.forall_conv (conv2 (k - 1) o snd) ctxt;
in conv2 i ctxt end;
fun swap_prems_conv 0 = Conv.all_conv
| swap_prems_conv i =
Conv.implies_concl_conv (swap_prems_conv (i - 1)) then_conv
- Conv.rewr_conv Drule.swap_prems_eq
+ Conv.rewr_conv Drule.swap_prems_eq;
fun find_eq ctxt t =
let
@@ -622,7 +621,9 @@
val xs = rename_params (Logic.strip_params A);
val xs' =
(case filter (fn x' => x' = x) xs of
- [] => xs | [_] => xs | _ => index 1 xs);
+ [] => xs
+ | [_] => xs
+ | _ => index 1 xs);
in Logic.list_rename_params xs' A end;
fun rename_prop prop =
let val (As, C) = Logic.strip_horn prop
@@ -733,8 +734,6 @@
fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact))
| get_inductP _ _ = [];
-type case_data = (((string * string list) * string list) list * int);
-
fun gen_induct_tac mod_cases ctxt simp def_insts arbitrary taking opt_rule facts =
SUBGOAL_CASES (fn (_, i) =>
let
@@ -778,7 +777,7 @@
val adefs = nth_list atomized_defs (j - 1);
val frees = fold (Term.add_frees o Thm.prop_of) adefs [];
val xs = nth_list arbitrary (j - 1);
- val k = nth concls (j - 1) + more_consumes
+ val k = nth concls (j - 1) + more_consumes;
in
Method.insert_tac (more_facts @ adefs) THEN'
(if simp then