Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: raw_simplifier.ML Sprache: SML

Original von: Isabelle^©

(*  Title:      Pure/context_tactic.ML
    Author:     Makarius

Tactics with proof context / cases -- as basis for Isar proof methods.
*)

infix 1 CONTEXT_THEN_ALL_NEW;

signature BASIC_CONTEXT_TACTIC =
sig
  type context_state = Proof.context * thm
  type context_tactic = context_state -> context_state Seq.result Seq.seq
  val TACTIC_CONTEXT: Proof.context -> thm Seq.seq -> context_state Seq.result Seq.seq
  val CONTEXT_TACTIC: tactic -> context_tactic
  val NO_CONTEXT_TACTIC: Proof.context -> context_tactic -> tactic
  val CONTEXT_CASES: Rule_Cases.cases -> tactic -> context_tactic
  val CONTEXT_SUBGOAL: (term * int -> context_tactic) -> int -> context_tactic
  val CONTEXT_THEN_ALL_NEW: (int -> context_tactic) * (int -> tactic) -> int -> context_tactic
  val SUBPROOFS: context_tactic -> context_tactic
end;

signature CONTEXT_TACTIC =
sig
  include BASIC_CONTEXT_TACTIC
end;

structure Context_Tactic: CONTEXT_TACTIC =
struct

(* type context_tactic *)

type context_state = Proof.context * thm;
type context_tactic = context_state -> context_state Seq.result Seq.seq;

fun TACTIC_CONTEXT ctxt : thm Seq.seq -> context_state Seq.result Seq.seq =
  Seq.map (Seq.Result o pair ctxt);

fun CONTEXT_TACTIC tac : context_tactic =
  fn (ctxt, st) => TACTIC_CONTEXT ctxt (tac st);

fun NO_CONTEXT_TACTIC ctxt (tac: context_tactic) st =
  tac (ctxt, st) |> Seq.filter_results |> Seq.map snd;

fun CONTEXT_CASES cases tac : context_tactic =
  fn (ctxt, st) => TACTIC_CONTEXT (Proof_Context.update_cases cases ctxt) (tac st);

fun CONTEXT_SUBGOAL tac i : context_tactic =
  fn (ctxt, st) =>
    (case try Logic.nth_prem (i, Thm.prop_of st) of
      SOME goal => tac (goal, i) (ctxt, st)
    | NONE => Seq.empty);

fun (tac1 CONTEXT_THEN_ALL_NEW tac2) i : context_tactic =
  fn (ctxt, st) =>
    (ctxt, st) |> tac1 i |> Seq.maps_results (fn (ctxt', st') =>
      TACTIC_CONTEXT ctxt' ((Seq.INTERVAL tac2 i (i + Thm.nprems_of st' - Thm.nprems_of st)) st'));

(* subproofs with closed derivation *)

fun SUBPROOFS tac : context_tactic =
  let
    fun apply (g :: gs) (SOME (Seq.Result (results, ctxt))) =
          (case Seq.pull (tac (ctxt, Goal.init g)) of
            SOME (Seq.Result (ctxt', st'), _) =>
              apply gs (SOME (Seq.Result (st' :: results, ctxt')))
          | SOME (Seq.Error msg, _) => SOME (Seq.Error msg)
          | NONE => NONE)
      | apply _ x = x;
  in
    fn (ctxt, st) =>
      (case Par_Tactical.strip_goals st of
        SOME goals =>
          (case apply goals (SOME (Seq.Result ([], ctxt))) of
            SOME (Seq.Result (results, ctxt')) =>
              TACTIC_CONTEXT ctxt' (Par_Tactical.retrofit_tac {close = true} results st)
          | SOME (Seq.Error msg) => Seq.single (Seq.Error msg)
          | NONE => Seq.empty)
      | NONE => Seq.DETERM tac (ctxt, st))
  end;

end;

structure Basic_Context_Tactic: BASIC_CONTEXT_TACTIC = Context_Tactic;
open Basic_Context_Tactic;

¤ Dauer der Verarbeitung: 0.19 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
Eigene Datei ansehen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.