# HG changeset patch # User wenzelm # Date 1372277886 -7200 # Node ID 365ca7cb0d812adbb6d7b86913de6f8da6e058a4 # Parent b528a975b256b0df48edea54f84b9683107745c8# Parent 210bca64b894816ce7670780b86928d325b2023f merged diff -r b528a975b256 -r 365ca7cb0d81 src/Doc/IsarImplementation/Tactic.thy --- a/src/Doc/IsarImplementation/Tactic.thy Wed Jun 26 18:26:00 2013 +0200 +++ b/src/Doc/IsarImplementation/Tactic.thy Wed Jun 26 22:18:06 2013 +0200 @@ -53,8 +53,10 @@ with protected propositions: \[ - \infer[@{text "(protect)"}]{@{text "#C"}}{@{text "C"}} \qquad - \infer[@{text "(conclude)"}]{@{text "A\<^sub>1 \ \ \ A\<^sub>n \ C"}}{@{text "A\<^sub>1 \ \ \ A\<^sub>n \ #C"}} + \infer[@{text "(protect n)"}]{@{text "A\<^sub>1 \ \ \ A\<^sub>n \ #C"}}{@{text "A\<^sub>1 \ \ \ A\<^sub>n \ C"}} + \] + \[ + \infer[@{text "(conclude)"}]{@{text "A \ \ \ C"}}{@{text "A \ \ \ #C"}} \] *} @@ -62,7 +64,7 @@ \begin{mldecls} @{index_ML Goal.init: "cterm -> thm"} \\ @{index_ML Goal.finish: "Proof.context -> thm -> thm"} \\ - @{index_ML Goal.protect: "thm -> thm"} \\ + @{index_ML Goal.protect: "int -> thm -> thm"} \\ @{index_ML Goal.conclude: "thm -> thm"} \\ \end{mldecls} @@ -76,8 +78,9 @@ result by removing the goal protection. The context is only required for printing error messages. - \item @{ML "Goal.protect"}~@{text "thm"} protects the full statement - of theorem @{text "thm"}. + \item @{ML "Goal.protect"}~@{text "n thm"} protects the statement + of theorem @{text "thm"}. The parameter @{text n} indicates the + number of premises to be retained. \item @{ML "Goal.conclude"}~@{text "thm"} removes the goal protection, even if there are pending subgoals. diff -r b528a975b256 -r 365ca7cb0d81 src/FOLP/intprover.ML --- a/src/FOLP/intprover.ML Wed Jun 26 18:26:00 2013 +0200 +++ b/src/FOLP/intprover.ML Wed Jun 26 22:18:06 2013 +0200 @@ -9,7 +9,7 @@ Completeness (for propositional logic) is proved in Roy Dyckhoff. -Contraction-Free Sequent Calculi for IntPruitionistic Logic. +Contraction-Free Sequent Calculi for Intuitionistic Logic. J. Symbolic Logic (in press) *) diff -r b528a975b256 -r 365ca7cb0d81 src/HOL/Tools/Function/function_core.ML --- a/src/HOL/Tools/Function/function_core.ML Wed Jun 26 18:26:00 2013 +0200 +++ b/src/HOL/Tools/Function/function_core.ML Wed Jun 26 22:18:06 2013 +0200 @@ -425,7 +425,7 @@ val goalstate = Conjunction.intr graph_is_function complete |> Thm.close_derivation - |> Goal.protect + |> Goal.protect 0 |> fold_rev (Thm.implies_intr o cprop_of) compat |> Thm.implies_intr (cprop_of complete) in diff -r b528a975b256 -r 365ca7cb0d81 src/Pure/Isar/obtain.ML --- a/src/Pure/Isar/obtain.ML Wed Jun 26 18:26:00 2013 +0200 +++ b/src/Pure/Isar/obtain.ML Wed Jun 26 22:18:06 2013 +0200 @@ -301,7 +301,7 @@ fun print_result ctxt' (k, [(s, [_, th])]) = Proof_Display.print_results Markup.state int ctxt' (k, [(s, [th])]); val before_qed = SOME (Method.primitive_text (Goal.conclude #> Raw_Simplifier.norm_hhf #> - (fn th => Goal.protect (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th)))); + (fn th => Goal.protect 0 (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th)))); fun after_qed [[_, res]] = Proof.end_block #> guess_context (check_result ctxt thesis res); in diff -r b528a975b256 -r 365ca7cb0d81 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Wed Jun 26 18:26:00 2013 +0200 +++ b/src/Pure/Isar/proof.ML Wed Jun 26 22:18:06 2013 +0200 @@ -402,10 +402,10 @@ ALLGOALS Goal.conjunction_tac (#2 (#2 (get_goal state))) |> Seq.maps (fn goal => state - |> Seq.lift provide_goal (Goal.extract 1 n goal |> Seq.maps (Goal.conjunction_tac 1)) + |> Seq.lift provide_goal ((PRIMITIVE (Goal.restrict 1 n) THEN Goal.conjunction_tac 1) goal) |> Seq.maps meth |> Seq.maps (fn state' => state' - |> Seq.lift provide_goal (Goal.retrofit 1 n (#2 (#2 (get_goal state'))) goal)) + |> Seq.lift provide_goal (PRIMITIVE (Goal.unrestrict 1) (#2 (#2 (get_goal state'))))) |> Seq.maps (apply_method true (K Method.succeed))); fun apply_text cc text state = @@ -1133,8 +1133,7 @@ val prop' = Logic.protect prop; val statement' = (kind, [[], [prop']], prop'); - val goal' = Thm.adjust_maxidx_thm (Thm.maxidx_of goal) - (Drule.comp_no_flatten (goal, Thm.nprems_of goal) 1 Drule.protectI); + val goal' = Thm.adjust_maxidx_thm (Thm.maxidx_of goal) (Goal.protect (Thm.nprems_of goal) goal); val after_qed' = (fn [[th]] => map_context (set_result th), fn [[th]] => set_result th); val result_ctxt = diff -r b528a975b256 -r 365ca7cb0d81 src/Pure/goal.ML --- a/src/Pure/goal.ML Wed Jun 26 18:26:00 2013 +0200 +++ b/src/Pure/goal.ML Wed Jun 26 22:18:06 2013 +0200 @@ -9,6 +9,7 @@ val skip_proofs: bool Unsynchronized.ref val parallel_proofs: int Unsynchronized.ref val SELECT_GOAL: tactic -> int -> tactic + val PREFER_GOAL: tactic -> int -> tactic val CONJUNCTS: tactic -> int -> tactic val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic val PARALLEL_CHOICE: tactic list -> tactic @@ -19,7 +20,7 @@ sig include BASIC_GOAL val init: cterm -> thm - val protect: thm -> thm + val protect: int -> thm -> thm val conclude: thm -> thm val check_finished: Proof.context -> thm -> thm val finish: Proof.context -> thm -> thm @@ -52,6 +53,8 @@ ({prems: thm list, context: Proof.context} -> tactic) -> thm val extract: int -> int -> thm -> thm Seq.seq val retrofit: int -> int -> thm -> thm -> thm Seq.seq + val restrict: int -> int -> thm -> thm + val unrestrict: int -> thm -> thm val conjunction_tac: int -> tactic val precise_conjunction_tac: int -> int -> tactic val recover_conjunction_tac: tactic @@ -73,11 +76,11 @@ in fn C => Thm.instantiate ([], [(A, C)]) Drule.protectI end; (* - C - --- (protect) - #C + A1 ==> ... ==> An ==> C + ------------------------ (protect n) + A1 ==> ... ==> An ==> #C *) -fun protect th = Drule.comp_no_flatten (th, 0) 1 Drule.protectI; +fun protect n th = Drule.comp_no_flatten (th, n) 1 Drule.protectI; (* A ==> ... ==> #C @@ -361,9 +364,25 @@ |> Thm.bicompose {flatten = false, match = false, incremented = false} (false, conclude st', Thm.nprems_of st') i; + +(* rearrange subgoals *) + +fun restrict i n st = + if i < 1 orelse n < 1 orelse i + n - 1 > Thm.nprems_of st + then raise THM ("Goal.restrict", i, [st]) + else rotate_prems (i - 1) st |> protect n; + +fun unrestrict i = conclude #> rotate_prems (1 - i); + +(*with structural marker*) fun SELECT_GOAL tac i st = if Thm.nprems_of st = 1 andalso i = 1 then tac st - else Seq.lifts (retrofit i 1) (Seq.maps tac (extract i 1 st)) st; + else (PRIMITIVE (restrict i 1) THEN tac THEN PRIMITIVE (unrestrict i)) st; + +(*without structural marker*) +fun PREFER_GOAL tac i st = + if i < 1 orelse i > Thm.nprems_of st then Seq.empty + else (PRIMITIVE (rotate_prems (i - 1)) THEN tac THEN PRIMITIVE (rotate_prems (1 - i))) st; (* multiple goals *) diff -r b528a975b256 -r 365ca7cb0d81 src/Pure/pure_syn.ML --- a/src/Pure/pure_syn.ML Wed Jun 26 18:26:00 2013 +0200 +++ b/src/Pure/pure_syn.ML Wed Jun 26 22:18:06 2013 +0200 @@ -9,7 +9,8 @@ val _ = Outer_Syntax.command - (("theory", Keyword.tag_theory Keyword.thy_begin), Position.none) "begin theory context" + (("theory", Keyword.tag_theory Keyword.thy_begin), Position.file "pure_syn.ML") + "begin theory context" (Thy_Header.args >> (fn header => Toplevel.print o Toplevel.init_theory @@ -17,7 +18,8 @@ val _ = Outer_Syntax.command - (("ML_file", Keyword.tag_ml Keyword.thy_load), Position.none) "ML text from file" + (("ML_file", Keyword.tag_ml Keyword.thy_load), Position.file "pure_syn.ML") + "ML text from file" (Thy_Load.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy => let val [{src_path, text, pos}] = files (Context.theory_of gthy); diff -r b528a975b256 -r 365ca7cb0d81 src/Pure/simplifier.ML --- a/src/Pure/simplifier.ML Wed Jun 26 18:26:00 2013 +0200 +++ b/src/Pure/simplifier.ML Wed Jun 26 22:18:06 2013 +0200 @@ -220,7 +220,7 @@ fun simp_loop_tac i = Raw_Simplifier.generic_rewrite_goal_tac mode (solve_all_tac unsafe_solvers) ctxt i THEN (solve_tac i ORELSE TRY ((loop_tac THEN_ALL_NEW simp_loop_tac) i)); - in SELECT_GOAL (simp_loop_tac 1) end; + in PREFER_GOAL (simp_loop_tac 1) end; local diff -r b528a975b256 -r 365ca7cb0d81 src/ZF/Constructible/Relative.thy --- a/src/ZF/Constructible/Relative.thy Wed Jun 26 18:26:00 2013 +0200 +++ b/src/ZF/Constructible/Relative.thy Wed Jun 26 22:18:06 2013 +0200 @@ -753,8 +753,6 @@ "[| strong_replacement(M, \x y. y = f(x)); M(A); \x\A. M(f(x)) |] ==> M(RepFun(A,f))" apply (simp add: RepFun_def) -apply (rule strong_replacement_closed) -apply (auto dest: transM simp add: univalent_def) done lemma Replace_conj_eq: "{y . x \ A, x\A & y=f(x)} = {y . x\A, y=f(x)}"