# HG changeset patch # User wenzelm # Date 1435269114 -7200 # Node ID d694f217ee41dd0db24efbe9e7118ada8ab6d885 # Parent 718b1ba06429bb3b7522a234d5f2988a68f0bcbd# Parent d2fbc021a44d3fff88f13c611f5b5e9428a3bed9 merged diff -r 718b1ba06429 -r d694f217ee41 Admin/isatest/settings/at64-poly --- 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 diff -r 718b1ba06429 -r d694f217ee41 NEWS --- 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. diff -r 718b1ba06429 -r d694f217ee41 src/Doc/Isar_Ref/Proof.thy --- 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 \"} \\[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 \ + @@{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 \ 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 \ a\<^sub>n"} composes some fact from @{text "a\<^sub>1, \, a\<^sub>n"} (or implicitly from the current proof context) diff -r 718b1ba06429 -r d694f217ee41 src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy --- 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 \Miscellaneous lemmas about indexes, decrementation, substitution etc ...\ lemma isnpolyh_polybound0: "isnpolyh p (Suc n) \ 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 \isnpolyh p n\ by simp - with goal1(2) show ?case + with prems(2) show ?case by simp qed diff -r 718b1ba06429 -r d694f217ee41 src/HOL/GCD.thy --- 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" "(\m n::nat. m dvd n \ \ 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" "(\m n::nat. m dvd n \ \ 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" "(\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 "\m n. m dvd n \ \ 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 (\m n. m dvd n \ \ 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 "\m n. m dvd n \ \ n dvd m" lcm 1 "0::nat" . diff -r 718b1ba06429 -r d694f217ee41 src/HOL/Library/Extended_Real.thy --- 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 + -\ = - \" | "-\ + ereal p = -(\::ereal)" | "-\ + -\ = -(\::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 < \ \ True" | " -\ < ereal r \ True" | " -\ < (\::ereal) \ 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 @@ | "-(\::ereal) * \ = -\" | "(\::ereal) * -\ = -\" | "-(\::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 simp_all termination by (relation "{}") simp diff -r 718b1ba06429 -r d694f217ee41 src/HOL/Library/Product_Order.thy --- 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 diff -r 718b1ba06429 -r d694f217ee41 src/HOL/Library/RBT_Set.thy --- 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 \ y \ set (RBT_Impl.keys t1) \ y \ 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 \ k" by (simp add: left_le_key rbt_min_opt_in_set) - moreover from goal3 have "k \ 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 \ set (RBT_Impl.keys t1)" | "y \ 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 \ k" + using left_non_empty by (simp add: left_le_key rbt_min_opt_in_set) + moreover have "k \ 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 \ y \ set (RBT_Impl.keys t2) \ y \ 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 \ k" by (simp add: key_le_right rbt_max_opt_in_set) - moreover from goal3 have "y \ 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 \ set (RBT_Impl.keys t2)" | "y \ 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 \ k" + using right_non_empty by (simp add: key_le_right rbt_max_opt_in_set) + moreover have "y \ 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: diff -r 718b1ba06429 -r d694f217ee41 src/HOL/Library/While_Combinator.thy --- 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: "\ 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 * diff -r 718b1ba06429 -r d694f217ee41 src/HOL/List.thy --- 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 @@ "\ \ i. \ i < n ; i < length xs \ \ P (xs ! i) ; n < length xs \ \ P (xs ! n) \ \ 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 "\ 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 \ \ P (xs ! length (takeWhile P xs))" diff -r 718b1ba06429 -r d694f217ee41 src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy --- 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 "\iir s. (\j r j \ r j \ q j + 1) \ (\j s j \ s j \ q j + 1) \ label r i \ label s i" proof - - let ?rl = "reduced n\label" + let ?rl = "reduced n \ label" let ?A = "{s. ksimplex p n s \ ?rl ` s = {..n}}" have "odd (card ?A)" using assms by (intro kuhn_combinatorial[of p n label]) auto then have "?A \ {}" - 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 \ {.. n}" "Suc i \ {.. n}" by auto then obtain u v where u: "u \ s" "Suc i = ?rl u" and v: "v \ s" "i = ?rl v" @@ -1363,10 +1366,11 @@ u(2)[symmetric] v(2)[symmetric] \i < n\ by auto moreover - { fix j assume "j < n" - then have "b j \ u j" "u j \ b j + 1" "b j \ v j" "v j \ b j + 1" - using base_le[OF \u\s\] le_Suc_base[OF \u\s\] base_le[OF \v\s\] le_Suc_base[OF \v\s\] by auto } - ultimately show ?case + have "b j \ u j" "u j \ b j + 1" "b j \ v j" "v j \ b j + 1" if "j < n" for j + using that base_le[OF \u\s\] le_Suc_base[OF \u\s\] base_le[OF \v\s\] le_Suc_base[OF \v\s\] + by auto + ultimately show "\r s. (\j r j \ r j \ b j + 1) \ + (\j s j \ s j \ b j + 1) \ label r i \ label s i" by blast qed qed @@ -1392,23 +1396,20 @@ apply rule apply rule proof - - case goal1 + fix x x' let ?R = "\y::nat. - (P x \ Q xa \ x xa = 0 \ y = 0) \ - (P x \ Q xa \ x xa = 1 \ y = 1) \ - (P x \ Q xa \ y = 0 \ x xa \ (f x) xa) \ - (P x \ Q xa \ y = 1 \ (f x) xa \ x xa)" - { - assume "P x" and "Q xa" - then have "0 \ f x xa \ f x xa \ 1" - using assms(2)[rule_format,of "f x" xa] - apply (drule_tac assms(1)[rule_format]) - apply auto - done - } + (P x \ Q x' \ x x' = 0 \ y = 0) \ + (P x \ Q x' \ x x' = 1 \ y = 1) \ + (P x \ Q x' \ y = 0 \ x x' \ (f x) x') \ + (P x \ Q x' \ y = 1 \ (f x) x' \ x x')" + have "0 \ f x x' \ f x x' \ 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 \ ?R 1" by auto - then show ?case + then show "\y\1. ?R y" by auto qed qed @@ -1988,17 +1989,17 @@ assumes "e > 0" shows "\ (frontier (cball a e) retract_of (cball a e))" proof - case goal1 - have *: "\xa. a - (2 *\<^sub>R a - xa) = - (a - xa)" + assume *: "frontier (cball a e) retract_of (cball a e)" + have **: "\xa. a - (2 *\<^sub>R a - xa) = - (a - xa)" using scaleR_left_distrib[of 1 1 a] by auto obtain x where x: "x \ {x. norm (a - x) = e}" "2 *\<^sub>R a - x = x" - apply (rule retract_fixpoint_property[OF goal1, of "\x. scaleR 2 a - x"]) + apply (rule retract_fixpoint_property[OF *, of "\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) diff -r 718b1ba06429 -r d694f217ee41 src/HOL/Nominal/Examples/Pattern.thy --- 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 diff -r 718b1ba06429 -r d694f217ee41 src/HOL/Nominal/Nominal.thy --- 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\(\x\X. f x) \ (\x\(pi\X). (pi\f) x)" apply(auto simp add: perm_set_def) apply(rule_tac x="pi\xb" in exI) @@ -2218,7 +2217,6 @@ apply(rule pt_fun_app_eq[OF pt, OF at]) done next - case goal2 show "(\x\(pi\X). (pi\f) x) \ pi\(\x\X. f x)" apply(auto simp add: perm_set_def) apply(rule_tac x="(rev pi)\x" in exI) diff -r 718b1ba06429 -r d694f217ee41 src/HOL/Number_Theory/Euclidean_Algorithm.thy --- 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 \ 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 diff -r 718b1ba06429 -r d694f217ee41 src/HOL/Probability/Embed_Measure.thy --- 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 \ sets M" "\A = space M" "\X. X\A \ emeasure M X \ \" 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 \ sets (embed_measure M f)" - by (auto simp: sets_embed_measure) - from A_props and inj show "\(op ` f`A) = space (embed_measure M f)" - by (auto simp: space_embed_measure intro!: imageI) - from A_props and inj show "\a\op ` f ` A. emeasure (embed_measure M f) a \ \" - 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 \ sets (embed_measure M f)" + by (auto simp: sets_embed_measure) + moreover + from A_props and inj have "\(op ` f`A) = space (embed_measure M f)" + by (auto simp: space_embed_measure intro!: imageI) + moreover + from A_props and inj have "\a\op ` f ` A. emeasure (embed_measure M f) a \ \" + 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': diff -r 718b1ba06429 -r d694f217ee41 src/HOL/Probability/Finite_Product_Measure.thy --- 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" "\x. x \ I \ 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 "\i. space (M i)" "\i. space (N i)"]) simp_all next - case goal2 + case 2 have "\K. K \ J \ (\ j\K. sets (M j)) = (\ j\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 diff -r 718b1ba06429 -r d694f217ee41 src/HOL/Probability/Information.thy --- 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 \ 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 \ 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 \ 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) diff -r 718b1ba06429 -r d694f217ee41 src/HOL/Probability/Measure_Space.thy --- 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 \ 'a set" where "range A \ sets M" "(\i. A i) = space M" "\i. emeasure M (A i) \ \" "disjoint_family A" -proof atomize_elim - case goal1 +proof - obtain A :: "nat \ 'a set" where range: "range A \ sets M" and space: "(\i. A i) = space M" and measure: "\i. emeasure M (A i) \ \" using sigma_finite by auto - note range' = sets.range_disjointed_sets[OF range] range - { fix i - have "emeasure M (disjointed A i) \ emeasure M (A i)" - using range' disjointed_subset[of A i] by (auto intro!: emeasure_mono) - then have "emeasure M (disjointed A i) \ \" - 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) \ sets M" + by (rule sets.range_disjointed_sets[OF range]) + show "(\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) \ \" for i + proof - + have "emeasure M (disjointed A i) \ 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 \ 'a set" where "range A \ sets M" "(\i. A i) = space M" "\i. emeasure M (A i) \ \" "incseq A" -proof atomize_elim - case goal1 +proof - obtain F :: "nat \ 'a set" where F: "range F \ sets M" "(\i. F i) = space M" "\i. emeasure M (F i) \ \" using sigma_finite by auto - then show ?case - proof (intro exI[of _ "\n. \i\n. F i"] conjI allI) - from F have "\x. x \ space M \ \i. x \ F i" by auto - then show "(\n. \ i\n. F i) = space M" - using F by fastforce - next - fix n - have "emeasure M (\ i\n. F i) \ (\i\n. emeasure M (F i))" using F - by (auto intro!: emeasure_subadditive_finite) - also have "\ < \" - using F by (auto simp: setsum_Pinfty) - finally show "emeasure M (\ i\n. F i) \ \" by simp - qed (force simp: incseq_def)+ + show thesis + proof (rule that[of "\n. \i\n. F i"]) + show "range (\n. \i\n. F i) \ sets M" + using F by (force simp: incseq_def) + show "(\n. \i\n. F i) = space M" + proof - + from F have "\x. x \ space M \ \i. x \ F i" by auto + with F show ?thesis by fastforce + qed + show "emeasure M (\ i\n. F i) \ \" for n + proof - + have "emeasure M (\ i\n. F i) \ (\i\n. emeasure M (F i))" + using F by (auto intro!: emeasure_subadditive_finite) + also have "\ < \" + using F by (auto simp: setsum_Pinfty) + finally show ?thesis by simp + qed + show "incseq (\n. \i\n. F i)" + by (force simp: incseq_def) + qed qed subsection {* Measure space induced by distribution of @{const measurable}-functions *} diff -r 718b1ba06429 -r d694f217ee41 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- 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 diff -r 718b1ba06429 -r d694f217ee41 src/HOL/ZF/Games.thy --- 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) \ option_of" by (auto) + proof (auto, goals) + {case prems: (1 y) + from prems have "(y, g) \ option_of" by (auto) with 1 have "ge_game (y, y)" by auto - with goal1 have "\ ge_game (g, y)" + with prems have "\ 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) \ option_of" by (auto) + {case prems: (2 y) + from prems have "(y, g) \ option_of" by (auto) with 1 have "ge_game (y, y)" by auto - with goal2 have "\ ge_game (y, g)" + with prems have "\ 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 "\ 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 "\ 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 \ 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 = "\ g. plus_game g zero_game" and g = "id"] - induct_hyp) - done - qed - } + have "H = zero_game \ 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 = "\ 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 "\ F G H. a = [F, G, H] \ 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) \ 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) \ 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) \ 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 \ 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 "\F G H. a = [F, G, H] \ 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) \ 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) \ 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) \ 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 \ 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 "\ (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 "\ (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 "\ (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 "\ (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: "\ (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: "\ (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: "\ (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: "\ (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 "\ x y z. a = [x,y,z] \ 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 "\ (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 "\ (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 "\ (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 "\ (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 "\x y z. a = [x,y,z] \ 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 "\ (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 "\ (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: "\ (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 "\ (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 "\ (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: "\ (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: "\ (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: "\ (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 "\ x y. a = [x, y] \ 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 "\x y. a = [x, y] \ 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 - diff -r 718b1ba06429 -r d694f217ee41 src/HOL/ex/Tree23.thy --- 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 \ 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 diff -r 718b1ba06429 -r d694f217ee41 src/Pure/Isar/args.ML --- 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; diff -r 718b1ba06429 -r d694f217ee41 src/Pure/Isar/method.ML --- 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)) diff -r 718b1ba06429 -r d694f217ee41 src/Pure/Isar/proof.ML --- 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 diff -r 718b1ba06429 -r d694f217ee41 src/Pure/Isar/proof_context.ML --- 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 diff -r 718b1ba06429 -r d694f217ee41 src/Pure/Isar/rule_cases.ML --- 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 *) diff -r 718b1ba06429 -r d694f217ee41 src/Tools/induct.ML --- 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