--- a/NEWS Thu Jun 25 16:56:04 2015 +0200
+++ b/NEWS Thu Jun 25 21:45:00 2015 +0200
@@ -77,6 +77,9 @@
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.
+
* 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 16:56:04 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy Thu Jun 25 21:45:00 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/Pure/Isar/method.ML Thu Jun 25 16:56:04 2015 +0200
+++ b/src/Pure/Isar/method.ML Thu Jun 25 21:45:00 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))