--- a/CONTRIBUTORS Wed Jul 01 13:09:56 2015 +0200
+++ b/CONTRIBUTORS Thu Jul 02 14:10:42 2015 +0200
@@ -6,13 +6,16 @@
Contributions to this Isabelle version
--------------------------------------
+* Summer 2015: Daniel Matichuk, NICTA and Makarius Wenzel
+ Isar subgoal command for proof structure within unstructured proof
+ scripts.
+
* Summer 2015: Florian Haftmann, TUM
- Generic partial division in rings as inverse operation
- of multiplication.
+ Generic partial division in rings as inverse operation of multiplication.
* Summer 2015: Manuel Eberl and Florian Haftmann, TUM
- Type class hierarchy with common algebraic notions of
- integral (semi)domains like units and associated elements.
+ Type class hierarchy with common algebraic notions of integral
+ (semi)domains like units and associated elements.
Contributions to Isabelle2015
--- a/NEWS Wed Jul 01 13:09:56 2015 +0200
+++ b/NEWS Thu Jul 02 14:10:42 2015 +0200
@@ -102,12 +102,27 @@
is still available as legacy for some time. Documentation now explains
'..' more accurately as "by standard" instead of "by rule".
+* Command 'subgoal' allows to impose some structure on backward
+refinements, to avoid proof scripts degenerating into long of 'apply'
+sequences. Further explanations and examples are given in the isar-ref
+manual.
+
* Proof method "goals" turns the current subgoals into cases within the
context; the conclusion is bound to variable ?case in each case.
For example:
lemma "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"
- and "\<And>y z. U y \<Longrightarrow> V u \<Longrightarrow> W y z"
+ and "\<And>y z. U y \<Longrightarrow> V z \<Longrightarrow> W y z"
+proof goals
+ case (1 x)
+ then show ?case using \<open>A x\<close> \<open>B x\<close> sorry
+next
+ case (2 y z)
+ then show ?case using \<open>U y\<close> \<open>V z\<close> sorry
+qed
+
+lemma "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"
+ and "\<And>y z. U y \<Longrightarrow> V z \<Longrightarrow> W y z"
proof goals
case prems: 1
then show ?case using prems sorry
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy Wed Jul 01 13:09:56 2015 +0200
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy Thu Jul 02 14:10:42 2015 +0200
@@ -438,6 +438,9 @@
@{rail \<open>
@{syntax_def axmdecl}: @{syntax name} @{syntax attributes}? ':'
;
+ @{syntax_def thmbind}:
+ @{syntax name} @{syntax attributes} | @{syntax name} | @{syntax attributes}
+ ;
@{syntax_def thmdecl}: thmbind ':'
;
@{syntax_def thmdef}: thmbind '='
@@ -449,9 +452,6 @@
;
@{syntax_def thmrefs}: @{syntax thmref} +
;
-
- thmbind: @{syntax name} @{syntax attributes} | @{syntax name} | @{syntax attributes}
- ;
selection: '(' ((@{syntax nat} | @{syntax nat} '-' @{syntax nat}?) + ',') ')'
\<close>}
\<close>
--- a/src/Doc/Isar_Ref/Proof_Script.thy Wed Jul 01 13:09:56 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof_Script.thy Thu Jul 02 14:10:42 2015 +0200
@@ -88,6 +88,103 @@
\<close>
+section \<open>Explicit subgoal structure\<close>
+
+text \<open>
+ \begin{matharray}{rcl}
+ @{command_def "subgoal"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
+ \end{matharray}
+
+ @{rail \<open>
+ @@{command subgoal} @{syntax thmbind}? prems? params?
+ ;
+ prems: @'premises' @{syntax thmbind}?
+ ;
+ params: @'for' '\<dots>'? (('_' | @{syntax name})+)
+ \<close>}
+
+ \begin{description}
+
+ \item @{command "subgoal"} allows to impose some structure on backward
+ refinements, to avoid proof scripts degenerating into long of @{command
+ apply} sequences.
+
+ The current goal state, which is essentially a hidden part of the Isar/VM
+ configurtation, is turned into a proof context and remaining conclusion.
+ This correponds to @{command fix}~/ @{command assume}~/ @{command show} in
+ structured proofs, but the text of the parameters, premises and conclusion
+ is not given explicitly.
+
+ Goal parameters may be specified separately, in order to allow referring
+ to them in the proof body: ``@{command subgoal}~@{keyword "for"}~@{text "x
+ y z"}'' names a \emph{prefix}, and ``@{command subgoal}~@{keyword
+ "for"}~@{text "\<dots> x y z"}'' names a \emph{suffix} of goal parameters. The
+ latter uses a literal @{verbatim "\<dots>"} symbol as notation. Parameter
+ positions may be skipped via dummies (underscore). Unspecified names
+ remain internal, and thus inaccessible in the proof text.
+
+ ``@{command subgoal}~@{keyword "premises"}~@{text prems}'' indicates that
+ goal premises should be turned into assumptions of the context (otherwise
+ the remaining conclusion is a Pure implication). The fact name and
+ attributes are optional; the particular name ``@{text prems}'' is a common
+ convention for the premises of an arbitrary goal context in proof scripts.
+
+ ``@{command subgoal}~@{text result}'' indicates a fact name for the result
+ of a proven subgoal. Thus it may be re-used in further reasoning, similar
+ to the result of @{command show} in structured Isar proofs.
+
+ \end{description}
+
+ Here are some abstract examples:
+\<close>
+
+lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
+ and "\<And>u v. X u \<Longrightarrow> Y v"
+ subgoal sorry
+ subgoal sorry
+ done
+
+lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
+ and "\<And>u v. X u \<Longrightarrow> Y v"
+ subgoal for x y z sorry
+ subgoal for u v sorry
+ done
+
+lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
+ and "\<And>u v. X u \<Longrightarrow> Y v"
+ subgoal premises for x y z
+ using \<open>A x\<close> \<open>B y\<close>
+ sorry
+ subgoal premises for u v
+ using \<open>X u\<close>
+ sorry
+ done
+
+lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
+ and "\<And>u v. X u \<Longrightarrow> Y v"
+ subgoal r premises prems for x y z
+ proof -
+ have "A x" by (fact prems)
+ moreover have "B y" by (fact prems)
+ ultimately show ?thesis sorry
+ qed
+ subgoal premises prems for u v
+ proof -
+ have "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z" by (fact r)
+ moreover
+ have "X u" by (fact prems)
+ ultimately show ?thesis sorry
+ qed
+ done
+
+lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
+ subgoal premises prems for \<dots> z
+ proof -
+ from prems show "C z" sorry
+ qed
+ done
+
+
section \<open>Tactics: improper proof methods \label{sec:tactics}\<close>
text \<open>
--- a/src/HOL/Eisbach/Eisbach.thy Wed Jul 01 13:09:56 2015 +0200
+++ b/src/HOL/Eisbach/Eisbach.thy Thu Jul 02 14:10:42 2015 +0200
@@ -9,7 +9,6 @@
keywords
"method" :: thy_decl and
"conclusion"
- "premises"
"declares"
"methods"
"\<bar>" "\<Rightarrow>"
--- a/src/Pure/Isar/isar_syn.ML Wed Jul 01 13:09:56 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML Thu Jul 02 14:10:42 2015 +0200
@@ -679,6 +679,33 @@
Toplevel.skip_proof (fn i => i + 1))));
+(* subgoal focus *)
+
+local
+
+val opt_fact_binding =
+ Scan.optional (Parse.binding -- Parse.opt_attribs || Parse.attribs >> pair Binding.empty)
+ Attrib.empty_binding;
+
+val for_params =
+ Scan.optional
+ (@{keyword "for"} |--
+ Parse.!!! ((Scan.option Parse.dots >> is_some) --
+ (Scan.repeat1 (Parse.position (Parse.maybe Parse.name)))))
+ (false, []);
+
+in
+
+val _ =
+ Outer_Syntax.command @{command_keyword subgoal}
+ "focus on first subgoal within backward refinement"
+ (opt_fact_binding -- (Scan.option (@{keyword "premises"} |-- Parse.!!! opt_fact_binding)) --
+ for_params >> (fn ((a, b), c) =>
+ Toplevel.proofs (Seq.make_results o Seq.single o #2 o Subgoal.subgoal_cmd a b c)));
+
+end;
+
+
(* proof navigation *)
fun report_back () =
--- a/src/Pure/Isar/keyword.ML Wed Jul 01 13:09:56 2015 +0200
+++ b/src/Pure/Isar/keyword.ML Thu Jul 02 14:10:42 2015 +0200
@@ -28,8 +28,9 @@
val prf_decl: string
val prf_asm: string
val prf_asm_goal: string
- val prf_asm_goal_script: string
val prf_script: string
+ val prf_script_goal: string
+ val prf_script_asm_goal: string
type spec = (string * string list) * string list
type keywords
val minor_keywords: keywords -> Scan.lexicon
@@ -95,13 +96,15 @@
val prf_decl = "prf_decl";
val prf_asm = "prf_asm";
val prf_asm_goal = "prf_asm_goal";
-val prf_asm_goal_script = "prf_asm_goal_script";
val prf_script = "prf_script";
+val prf_script_goal = "prf_script_goal";
+val prf_script_asm_goal = "prf_script_asm_goal";
val kinds =
[diag, document_heading, document_body, document_raw, thy_begin, thy_end, thy_load, thy_decl,
thy_decl_block, thy_goal, qed, qed_script, qed_block, qed_global, prf_goal, prf_block, prf_open,
- prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
+ prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal,
+ prf_script_asm_goal];
(* specifications *)
@@ -239,19 +242,21 @@
val is_proof = command_category
[qed, qed_script, qed_block, qed_global, prf_goal, prf_block, prf_open, prf_close,
- prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
+ prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal,
+ prf_script_asm_goal];
val is_proof_body = command_category
[diag, document_heading, document_body, document_raw, prf_block, prf_open, prf_close,
- prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
+ prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal,
+ prf_script_asm_goal];
val is_theory_goal = command_category [thy_goal];
-val is_proof_goal = command_category [prf_goal, prf_asm_goal, prf_asm_goal_script];
+val is_proof_goal = command_category [prf_goal, prf_asm_goal, prf_script_goal, prf_script_asm_goal];
val is_qed = command_category [qed, qed_script, qed_block];
val is_qed_global = command_category [qed_global];
val is_proof_asm = command_category [prf_asm, prf_asm_goal];
-val is_improper = command_category [qed_script, prf_script, prf_asm_goal_script];
+val is_improper = command_category [qed_script, prf_script, prf_script_goal, prf_script_asm_goal];
fun is_printed keywords = is_theory_goal keywords orf is_proof keywords;
--- a/src/Pure/Isar/keyword.scala Wed Jul 01 13:09:56 2015 +0200
+++ b/src/Pure/Isar/keyword.scala Thu Jul 02 14:10:42 2015 +0200
@@ -35,8 +35,9 @@
val PRF_DECL = "prf_decl"
val PRF_ASM = "prf_asm"
val PRF_ASM_GOAL = "prf_asm_goal"
- val PRF_ASM_GOAL_SCRIPT = "prf_asm_goal_script"
val PRF_SCRIPT = "prf_script"
+ val PRF_SCRIPT_GOAL = "prf_script_goal"
+ val PRF_SCRIPT_ASM_GOAL = "prf_script_asm_goal"
/* command categories */
@@ -63,14 +64,16 @@
val proof =
Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE,
- PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
+ PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT, PRF_SCRIPT_GOAL,
+ PRF_SCRIPT_ASM_GOAL)
val proof_body =
Set(DIAG, DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW, PRF_BLOCK, PRF_OPEN, PRF_CLOSE,
- PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
+ PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT, PRF_SCRIPT_GOAL,
+ PRF_SCRIPT_ASM_GOAL)
val theory_goal = Set(THY_GOAL)
- val proof_goal = Set(PRF_GOAL, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT)
+ val proof_goal = Set(PRF_GOAL, PRF_ASM_GOAL, PRF_SCRIPT_GOAL, PRF_SCRIPT_ASM_GOAL)
val qed = Set(QED, QED_SCRIPT, QED_BLOCK)
val qed_global = Set(QED_GLOBAL)
--- a/src/Pure/Isar/parse.ML Wed Jul 01 13:09:56 2015 +0200
+++ b/src/Pure/Isar/parse.ML Thu Jul 02 14:10:42 2015 +0200
@@ -23,6 +23,7 @@
val short_ident: string parser
val long_ident: string parser
val sym_ident: string parser
+ val dots: string parser
val minus: string parser
val term_var: string parser
val type_ident: string parser
@@ -220,7 +221,10 @@
group (fn () => "reserved identifier " ^ quote x)
(RESET_VALUE (Scan.one (Token.ident_with (fn y => x = y)) >> Token.content_of));
+val dots = sym_ident :-- (fn "\\<dots>" => Scan.succeed () | _ => Scan.fail) >> #1;
+
val minus = sym_ident :-- (fn "-" => Scan.succeed () | _ => Scan.fail) >> #1;
+
val underscore = sym_ident :-- (fn "_" => Scan.succeed () | _ => Scan.fail) >> #1;
fun maybe scan = underscore >> K NONE || scan >> SOME;
--- a/src/Pure/Isar/proof.ML Wed Jul 01 13:09:56 2015 +0200
+++ b/src/Pure/Isar/proof.ML Thu Jul 02 14:10:42 2015 +0200
@@ -33,10 +33,12 @@
val enter_chain: state -> state
val enter_backward: state -> state
val has_bottom_goal: state -> bool
+ val using_facts: thm list -> state -> state
val pretty_state: state -> Pretty.T list
val refine: Method.text -> state -> state Seq.seq
val refine_end: Method.text -> state -> state Seq.seq
val refine_insert: thm list -> state -> state
+ val refine_primitive: (Proof.context -> thm -> thm) -> state -> state
val raw_goal: state -> {context: context, facts: thm list, goal: thm}
val goal: state -> {context: context, facts: thm list, goal: thm}
val simple_goal: state -> {context: context, goal: thm}
@@ -430,6 +432,9 @@
fun refine_insert ths =
Seq.hd o refine (Method.Basic (K (Method.insert ths)));
+fun refine_primitive r = (* FIXME Seq.Error!? *)
+ Seq.hd o refine (Method.Basic (fn ctxt => fn _ => EMPTY_CASES (PRIMITIVE (r ctxt))));
+
end;
--- a/src/Pure/Isar/proof_context.ML Wed Jul 01 13:09:56 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML Thu Jul 02 14:10:42 2015 +0200
@@ -1241,7 +1241,7 @@
val apply_case = apfst fst oo case_result;
-fun check_case ctxt internal (name, pos) fxs =
+fun check_case ctxt internal (name, pos) param_specs =
let
val (_, ((Rule_Cases.Case {fixes, assumes, binds, cases}, {legacy}), _)) =
Name_Space.check (Context.Proof ctxt) (cases_of ctxt) (name, pos);
@@ -1251,12 +1251,12 @@
" -- use proof method \"goals\" instead")
else ();
- val _ = List.app (fn NONE => () | SOME b => ignore (check_var internal b)) fxs;
+ val _ = List.app (fn NONE => () | SOME b => ignore (check_var internal b)) param_specs;
fun replace (opt_x :: xs) ((y, T) :: ys) = (the_default y opt_x, T) :: replace xs ys
| replace [] ys = ys
| replace (_ :: _) [] =
error ("Too many parameters for case " ^ quote name ^ Position.here pos);
- val fixes' = replace fxs fixes;
+ val fixes' = replace param_specs fixes;
val binds' = map drop_schematic binds;
in
if null (fold (Term.add_tvarsT o snd) fixes []) andalso
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/subgoal.ML Thu Jul 02 14:10:42 2015 +0200
@@ -0,0 +1,256 @@
+(* Title: Pure/Isar/subgoal.ML
+ Author: Makarius
+ Author: Daniel Matichuk, NICTA/UNSW
+
+Tactical operations with explicit subgoal focus, based on canonical
+proof decomposition. The "visible" part of the text within the
+context is fixed, the remaining goal may be schematic.
+
+Isar subgoal command for proof structure within unstructured proof
+scripts.
+*)
+
+signature SUBGOAL =
+sig
+ type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
+ asms: cterm list, concl: cterm, schematics: (ctyp * ctyp) list * (cterm * cterm) list}
+ val focus_params: Proof.context -> int -> thm -> focus * thm
+ val focus_params_fixed: Proof.context -> int -> thm -> focus * thm
+ val focus_prems: Proof.context -> int -> thm -> focus * thm
+ val focus: Proof.context -> int -> thm -> focus * thm
+ val retrofit: Proof.context -> Proof.context -> (string * cterm) list -> cterm list ->
+ int -> thm -> thm -> thm Seq.seq
+ val FOCUS_PARAMS: (focus -> tactic) -> Proof.context -> int -> tactic
+ val FOCUS_PARAMS_FIXED: (focus -> tactic) -> Proof.context -> int -> tactic
+ val FOCUS_PREMS: (focus -> tactic) -> Proof.context -> int -> tactic
+ val FOCUS: (focus -> tactic) -> Proof.context -> int -> tactic
+ val SUBPROOF: (focus -> tactic) -> Proof.context -> int -> tactic
+ val subgoal: Attrib.binding -> Attrib.binding option ->
+ bool * (string option * Position.T) list -> Proof.state -> focus * Proof.state
+ val subgoal_cmd: Attrib.binding -> Attrib.binding option ->
+ bool * (string option * Position.T) list -> Proof.state -> focus * Proof.state
+end;
+
+structure Subgoal: SUBGOAL =
+struct
+
+(* focus *)
+
+type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
+ asms: cterm list, concl: cterm, schematics: (ctyp * ctyp) list * (cterm * cterm) list};
+
+fun gen_focus (do_prems, do_concl) ctxt i raw_st =
+ let
+ val st = raw_st
+ |> Thm.transfer (Proof_Context.theory_of ctxt)
+ |> Raw_Simplifier.norm_hhf_protect ctxt;
+ val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt;
+ val ((params, goal), ctxt2) = Variable.focus_cterm (Thm.cprem_of st' i) ctxt1;
+
+ val (asms, concl) =
+ if do_prems then (Drule.strip_imp_prems goal, Drule.strip_imp_concl goal)
+ else ([], goal);
+ val text = asms @ (if do_concl then [concl] else []);
+
+ val (inst, ctxt3) = Variable.import_inst true (map Thm.term_of text) ctxt2;
+ val (_, schematic_terms) = Thm.certify_inst ctxt3 inst;
+
+ val schematics = (schematic_types, schematic_terms);
+ val asms' = map (Thm.instantiate_cterm schematics) asms;
+ val concl' = Thm.instantiate_cterm schematics concl;
+ val (prems, context) = Assumption.add_assumes asms' ctxt3;
+ in
+ ({context = context, params = params, prems = prems,
+ asms = asms', concl = concl', schematics = schematics}, Goal.init concl')
+ end;
+
+val focus_params = gen_focus (false, false);
+val focus_params_fixed = gen_focus (false, true);
+val focus_prems = gen_focus (true, false);
+val focus = gen_focus (true, true);
+
+
+(* lift and retrofit *)
+
+(*
+ B [?'b, ?y]
+ ----------------
+ B ['b, y params]
+*)
+fun lift_import idx params th ctxt =
+ let
+ val ((_, [th']), ctxt') = Variable.importT [th] ctxt;
+
+ val Ts = map Thm.typ_of_cterm params;
+ val ts = map Thm.term_of params;
+
+ val prop = Thm.full_prop_of th';
+ val concl_vars = Term.add_vars (Logic.strip_imp_concl prop) [];
+ val vars = rev (Term.add_vars prop []);
+ val (ys, ctxt'') = Variable.variant_fixes (map (Name.clean o #1 o #1) vars) ctxt';
+
+ fun var_inst v y =
+ let
+ val ((x, i), T) = v;
+ val (U, args) =
+ if member (op =) concl_vars v then (T, [])
+ else (Ts ---> T, ts);
+ val u = Free (y, U);
+ in ((Var v, list_comb (u, args)), (u, Var ((x, i + idx), U))) end;
+ val (inst1, inst2) =
+ split_list (map (apply2 (apply2 (Thm.cterm_of ctxt))) (map2 var_inst vars ys));
+
+ val th'' = Thm.instantiate ([], inst1) th';
+ in ((inst2, th''), ctxt'') end;
+
+(*
+ [x, A x]
+ :
+ B x ==> C
+ ------------------
+ [!!x. A x ==> B x]
+ :
+ C
+*)
+fun lift_subgoals params asms th =
+ let
+ fun lift ct = fold_rev Thm.all_name params (Drule.list_implies (asms, ct));
+ val unlift =
+ fold (Thm.elim_implies o Thm.assume) asms o
+ Drule.forall_elim_list (map #2 params) o Thm.assume;
+ val subgoals = map lift (Drule.strip_imp_prems (Thm.cprop_of th));
+ val th' = fold (Thm.elim_implies o unlift) subgoals th;
+ in (subgoals, th') end;
+
+fun retrofit ctxt1 ctxt0 params asms i st1 st0 =
+ let
+ val idx = Thm.maxidx_of st0 + 1;
+ val ps = map #2 params;
+ val ((subgoal_inst, st2), ctxt2) = lift_import idx ps st1 ctxt1;
+ val (subgoals, st3) = lift_subgoals params asms st2;
+ val result = st3
+ |> Goal.conclude
+ |> Drule.implies_intr_list asms
+ |> Drule.forall_intr_list ps
+ |> Drule.implies_intr_list subgoals
+ |> fold_rev (Thm.forall_intr o #1) subgoal_inst
+ |> fold (Thm.forall_elim o #2) subgoal_inst
+ |> Thm.adjust_maxidx_thm idx
+ |> singleton (Variable.export ctxt2 ctxt0);
+ in
+ Thm.bicompose (SOME ctxt0) {flatten = true, match = false, incremented = false}
+ (false, result, Thm.nprems_of st1) i st0
+ end;
+
+
+(* tacticals *)
+
+fun GEN_FOCUS flags tac ctxt i st =
+ if Thm.nprems_of st < i then Seq.empty
+ else
+ let val (args as {context = ctxt', params, asms, ...}, st') = gen_focus flags ctxt i st;
+ in Seq.lifts (retrofit ctxt' ctxt params asms i) (tac args st') st end;
+
+val FOCUS_PARAMS = GEN_FOCUS (false, false);
+val FOCUS_PARAMS_FIXED = GEN_FOCUS (false, true);
+val FOCUS_PREMS = GEN_FOCUS (true, false);
+val FOCUS = GEN_FOCUS (true, true);
+
+fun SUBPROOF tac ctxt = FOCUS (Seq.map (Goal.check_finished ctxt) oo tac) ctxt;
+
+
+(* Isar subgoal command *)
+
+local
+
+fun rename_params ctxt (param_suffix, raw_param_specs) st =
+ let
+ val _ = if Thm.no_prems st then error "No subgoals!" else ();
+ val (subgoal, goal') = Logic.dest_implies (Thm.prop_of st);
+ val subgoal_params =
+ map (apfst (Name.internal o Name.clean)) (Term.strip_all_vars subgoal)
+ |> Term.variant_frees subgoal |> map #1;
+
+ val n = length subgoal_params;
+ val m = length raw_param_specs;
+ val _ =
+ m <= n orelse
+ error ("Excessive subgoal parameter specification" ^
+ Position.here_list (map snd (drop n raw_param_specs)));
+
+ val param_specs =
+ raw_param_specs |> map
+ (fn (NONE, _) => NONE
+ | (SOME x, pos) =>
+ let val b = #1 (#1 (Proof_Context.cert_var (Binding.make (x, pos), NONE, NoSyn) ctxt))
+ in SOME (Variable.check_name b) end)
+ |> param_suffix ? append (replicate (n - m) NONE);
+
+ fun rename_list (opt_x :: xs) (y :: ys) = (the_default y opt_x :: rename_list xs ys)
+ | rename_list _ ys = ys;
+
+ fun rename_prop (x :: xs) ((c as Const ("Pure.all", _)) $ Abs (_, T, t)) =
+ (c $ Abs (x, T, rename_prop xs t))
+ | rename_prop [] t = t;
+
+ val subgoal' = rename_prop (rename_list param_specs subgoal_params) subgoal;
+ in Thm.renamed_prop (Logic.mk_implies (subgoal', goal')) st end;
+
+fun gen_subgoal prep_atts raw_result_binding raw_prems_binding param_specs state =
+ let
+ val _ = Proof.assert_backward state;
+
+ val state1 = state |> Proof.refine_insert [];
+ val {context = ctxt, facts = facts, goal = st} = Proof.raw_goal state1;
+
+ val result_binding = apsnd (map (prep_atts ctxt)) raw_result_binding;
+ val (prems_binding, do_prems) =
+ (case raw_prems_binding of
+ SOME (b, raw_atts) => ((b, map (prep_atts ctxt) raw_atts), true)
+ | NONE => ((Binding.empty, []), false));
+
+ val (subgoal_focus, _) =
+ rename_params ctxt param_specs st
+ |> (if do_prems then focus else focus_params_fixed) ctxt 1;
+
+ fun after_qed (ctxt'', [[result]]) =
+ Proof.end_block #> (fn state' =>
+ let
+ val ctxt' = Proof.context_of state';
+ val results' =
+ Proof_Context.export ctxt'' ctxt' (Conjunction.elim_conjunctions result);
+ in
+ state'
+ |> Proof.refine_primitive (fn _ => fn _ =>
+ retrofit ctxt'' ctxt' (#params subgoal_focus) (#asms subgoal_focus) 1
+ (Goal.protect 0 result) st
+ |> Seq.hd)
+ |> Proof.map_context
+ (#2 o Proof_Context.note_thmss "" [(result_binding, [(results', [])])])
+ end)
+ #> Proof.reset_facts
+ #> Proof.enter_backward;
+ in
+ state1
+ |> Proof.enter_forward
+ |> Proof.using_facts []
+ |> Proof.begin_block
+ |> Proof.map_context (fn _ =>
+ #context subgoal_focus
+ |> Proof_Context.note_thmss "" [(prems_binding, [(#prems subgoal_focus, [])])] |> #2)
+ |> Proof.internal_goal (K (K ())) (Proof_Context.get_mode ctxt) true "subgoal"
+ NONE after_qed [] [] [(Thm.empty_binding, [(Thm.term_of (#concl subgoal_focus), [])])] |> #2
+ |> Proof.using_facts facts
+ |> pair subgoal_focus
+ end;
+
+in
+
+val subgoal = gen_subgoal Attrib.attribute;
+val subgoal_cmd = gen_subgoal Attrib.attribute_cmd;
+
+end;
+
+end;
+
+val SUBPROOF = Subgoal.SUBPROOF;
--- a/src/Pure/Pure.thy Wed Jul 01 13:09:56 2015 +0200
+++ b/src/Pure/Pure.thy Thu Jul 02 14:10:42 2015 +0200
@@ -11,7 +11,7 @@
"\<subseteq>" "]" "assumes" "attach" "binder" "constrains"
"defines" "fixes" "for" "identifier" "if" "in" "includes" "infix"
"infixl" "infixr" "is" "notes" "obtains" "open" "output"
- "overloaded" "pervasive" "private" "qualified" "shows"
+ "overloaded" "pervasive" "premises" "private" "qualified" "shows"
"structure" "unchecked" "where" "when" "|"
and "text" "txt" :: document_body
and "text_raw" :: document_raw
@@ -57,7 +57,7 @@
and "fix" "assume" "presume" "def" :: prf_asm % "proof"
and "consider" :: prf_goal % "proof"
and "obtain" :: prf_asm_goal % "proof"
- and "guess" :: prf_asm_goal_script % "proof"
+ and "guess" :: prf_script_asm_goal % "proof"
and "let" "write" :: prf_decl % "proof"
and "case" :: prf_asm % "proof"
and "{" :: prf_open % "proof"
@@ -69,6 +69,7 @@
and "oops" :: qed_global % "proof"
and "defer" "prefer" "apply" :: prf_script % "proof"
and "apply_end" :: prf_script % "proof" == ""
+ and "subgoal" :: prf_script_goal % "proof"
and "proof" :: prf_block % "proof"
and "also" "moreover" :: prf_decl % "proof"
and "finally" "ultimately" :: prf_chain % "proof"
--- a/src/Pure/ROOT Wed Jul 01 13:09:56 2015 +0200
+++ b/src/Pure/ROOT Thu Jul 02 14:10:42 2015 +0200
@@ -145,6 +145,7 @@
"Isar/runtime.ML"
"Isar/spec_rules.ML"
"Isar/specification.ML"
+ "Isar/subgoal.ML"
"Isar/token.ML"
"Isar/toplevel.ML"
"Isar/typedecl.ML"
@@ -253,7 +254,6 @@
"simplifier.ML"
"skip_proof.ML"
"sorts.ML"
- "subgoal.ML"
"tactic.ML"
"tactical.ML"
"term.ML"
--- a/src/Pure/ROOT.ML Wed Jul 01 13:09:56 2015 +0200
+++ b/src/Pure/ROOT.ML Thu Jul 02 14:10:42 2015 +0200
@@ -262,6 +262,7 @@
use "Isar/proof.ML";
use "Isar/element.ML";
use "Isar/obtain.ML";
+use "Isar/subgoal.ML";
(*local theories and targets*)
use "Isar/locale.ML";
@@ -317,8 +318,6 @@
(*theory and proof operations*)
use "Isar/isar_cmd.ML";
-use "subgoal.ML";
-
(* Isabelle/Isar system *)
--- a/src/Pure/conjunction.ML Wed Jul 01 13:09:56 2015 +0200
+++ b/src/Pure/conjunction.ML Thu Jul 02 14:10:42 2015 +0200
@@ -19,6 +19,7 @@
val intr: thm -> thm -> thm
val intr_balanced: thm list -> thm
val elim: thm -> thm * thm
+ val elim_conjunctions: thm -> thm list
val elim_balanced: int -> thm -> thm list
val curry_balanced: int -> thm -> thm
val uncurry_balanced: int -> thm -> thm
@@ -118,6 +119,11 @@
end;
+fun elim_conjunctions th =
+ (case try elim th of
+ NONE => [th]
+ | SOME (th1, th2) => elim_conjunctions th1 @ elim_conjunctions th2);
+
(* balanced conjuncts *)
--- a/src/Pure/subgoal.ML Wed Jul 01 13:09:56 2015 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,152 +0,0 @@
-(* Title: Pure/subgoal.ML
- Author: Makarius
-
-Tactical operations with explicit subgoal focus, based on canonical
-proof decomposition. The "visible" part of the text within the
-context is fixed, the remaining goal may be schematic.
-*)
-
-signature SUBGOAL =
-sig
- type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
- asms: cterm list, concl: cterm, schematics: (ctyp * ctyp) list * (cterm * cterm) list}
- val focus_params: Proof.context -> int -> thm -> focus * thm
- val focus_prems: Proof.context -> int -> thm -> focus * thm
- val focus: Proof.context -> int -> thm -> focus * thm
- val retrofit: Proof.context -> Proof.context -> (string * cterm) list -> cterm list ->
- int -> thm -> thm -> thm Seq.seq
- val FOCUS_PARAMS: (focus -> tactic) -> Proof.context -> int -> tactic
- val FOCUS_PREMS: (focus -> tactic) -> Proof.context -> int -> tactic
- val FOCUS: (focus -> tactic) -> Proof.context -> int -> tactic
- val SUBPROOF: (focus -> tactic) -> Proof.context -> int -> tactic
-end;
-
-structure Subgoal: SUBGOAL =
-struct
-
-(* focus *)
-
-type focus = {context: Proof.context, params: (string * cterm) list, prems: thm list,
- asms: cterm list, concl: cterm, schematics: (ctyp * ctyp) list * (cterm * cterm) list};
-
-fun gen_focus (do_prems, do_concl) ctxt i raw_st =
- let
- val st = raw_st
- |> Thm.transfer (Proof_Context.theory_of ctxt)
- |> Simplifier.norm_hhf_protect ctxt;
- val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt;
- val ((params, goal), ctxt2) = Variable.focus_cterm (Thm.cprem_of st' i) ctxt1;
-
- val (asms, concl) =
- if do_prems then (Drule.strip_imp_prems goal, Drule.strip_imp_concl goal)
- else ([], goal);
- val text = asms @ (if do_concl then [concl] else []);
-
- val (inst, ctxt3) = Variable.import_inst true (map Thm.term_of text) ctxt2;
- val (_, schematic_terms) = Thm.certify_inst ctxt3 inst;
-
- val schematics = (schematic_types, schematic_terms);
- val asms' = map (Thm.instantiate_cterm schematics) asms;
- val concl' = Thm.instantiate_cterm schematics concl;
- val (prems, context) = Assumption.add_assumes asms' ctxt3;
- in
- ({context = context, params = params, prems = prems,
- asms = asms', concl = concl', schematics = schematics}, Goal.init concl')
- end;
-
-val focus_params = gen_focus (false, false);
-val focus_prems = gen_focus (true, false);
-val focus = gen_focus (true, true);
-
-
-(* lift and retrofit *)
-
-(*
- B [?'b, ?y]
- ----------------
- B ['b, y params]
-*)
-fun lift_import idx params th ctxt =
- let
- val ((_, [th']), ctxt') = Variable.importT [th] ctxt;
-
- val Ts = map Thm.typ_of_cterm params;
- val ts = map Thm.term_of params;
-
- val prop = Thm.full_prop_of th';
- val concl_vars = Term.add_vars (Logic.strip_imp_concl prop) [];
- val vars = rev (Term.add_vars prop []);
- val (ys, ctxt'') = Variable.variant_fixes (map (Name.clean o #1 o #1) vars) ctxt';
-
- fun var_inst v y =
- let
- val ((x, i), T) = v;
- val (U, args) =
- if member (op =) concl_vars v then (T, [])
- else (Ts ---> T, ts);
- val u = Free (y, U);
- in ((Var v, list_comb (u, args)), (u, Var ((x, i + idx), U))) end;
- val (inst1, inst2) =
- split_list (map (apply2 (apply2 (Thm.cterm_of ctxt))) (map2 var_inst vars ys));
-
- val th'' = Thm.instantiate ([], inst1) th';
- in ((inst2, th''), ctxt'') end;
-
-(*
- [x, A x]
- :
- B x ==> C
- ------------------
- [!!x. A x ==> B x]
- :
- C
-*)
-fun lift_subgoals params asms th =
- let
- fun lift ct = fold_rev Thm.all_name params (Drule.list_implies (asms, ct));
- val unlift =
- fold (Thm.elim_implies o Thm.assume) asms o
- Drule.forall_elim_list (map #2 params) o Thm.assume;
- val subgoals = map lift (Drule.strip_imp_prems (Thm.cprop_of th));
- val th' = fold (Thm.elim_implies o unlift) subgoals th;
- in (subgoals, th') end;
-
-fun retrofit ctxt1 ctxt0 params asms i st1 st0 =
- let
- val idx = Thm.maxidx_of st0 + 1;
- val ps = map #2 params;
- val ((subgoal_inst, st2), ctxt2) = lift_import idx ps st1 ctxt1;
- val (subgoals, st3) = lift_subgoals params asms st2;
- val result = st3
- |> Goal.conclude
- |> Drule.implies_intr_list asms
- |> Drule.forall_intr_list ps
- |> Drule.implies_intr_list subgoals
- |> fold_rev (Thm.forall_intr o #1) subgoal_inst
- |> fold (Thm.forall_elim o #2) subgoal_inst
- |> Thm.adjust_maxidx_thm idx
- |> singleton (Variable.export ctxt2 ctxt0);
- in
- Thm.bicompose (SOME ctxt0) {flatten = true, match = false, incremented = false}
- (false, result, Thm.nprems_of st1) i st0
- end;
-
-
-(* tacticals *)
-
-fun GEN_FOCUS flags tac ctxt i st =
- if Thm.nprems_of st < i then Seq.empty
- else
- let val (args as {context = ctxt', params, asms, ...}, st') = gen_focus flags ctxt i st;
- in Seq.lifts (retrofit ctxt' ctxt params asms i) (tac args st') st end;
-
-val FOCUS_PARAMS = GEN_FOCUS (false, false);
-val FOCUS_PREMS = GEN_FOCUS (true, false);
-val FOCUS = GEN_FOCUS (true, true);
-
-fun SUBPROOF tac ctxt = FOCUS (Seq.map (Goal.check_finished ctxt) oo tac) ctxt;
-
-end;
-
-val SUBPROOF = Subgoal.SUBPROOF;
-