src/Pure/Isar/method.ML
changeset 8238 78fd6355ebb5
parent 8220 e04928747b18
child 8240 87e08624e209
     1.1 --- a/src/Pure/Isar/method.ML	Sun Feb 13 21:00:02 2000 +0100
     1.2 +++ b/src/Pure/Isar/method.ML	Sun Feb 13 21:01:26 2000 +0100
     1.3 @@ -74,7 +74,7 @@
     1.4      Try of text |
     1.5      Repeat1 of text
     1.6    val refine: text -> Proof.state -> Proof.state Seq.seq
     1.7 -  val refine_no_facts: text -> Proof.state -> Proof.state Seq.seq
     1.8 +  val refine_end: text -> Proof.state -> Proof.state Seq.seq
     1.9    val proof: text option -> Proof.state -> Proof.state Seq.seq
    1.10    val local_qed: text option
    1.11      -> ({kind: string, name: string, thm: thm} -> unit) * (thm -> unit)
    1.12 @@ -201,7 +201,7 @@
    1.13  
    1.14  (* shuffle *)
    1.15  
    1.16 -fun prefer i = METHOD (K (PRIMITIVE (Thm.permute_prems 0 (i - 1))));
    1.17 +fun prefer i = METHOD (K (Tactic.defer_tac i THEN PRIMITIVE (Thm.permute_prems 0 1)));
    1.18  fun defer opt_i = METHOD (K (Tactic.defer_tac (if_none opt_i 1)));
    1.19  
    1.20  
    1.21 @@ -301,6 +301,18 @@
    1.22  fun assumption ctxt = METHOD (FINDGOAL o assumption_tac ctxt);
    1.23  
    1.24  
    1.25 +(* res_inst tactic emulation *)
    1.26 +
    1.27 +(*Note: insts refer to the hidden (!) goal context; use with care*)
    1.28 +fun gen_res_inst tac ((i, insts), thm) =
    1.29 +  METHOD (fn facts => (insert_tac facts THEN' tac insts thm) i);
    1.30 +
    1.31 +val res_inst = gen_res_inst Tactic.res_inst_tac;
    1.32 +val eres_inst = gen_res_inst Tactic.eres_inst_tac;
    1.33 +val dres_inst = gen_res_inst Tactic.dres_inst_tac;
    1.34 +val forw_inst = gen_res_inst Tactic.forw_inst_tac;
    1.35 +
    1.36 +
    1.37  
    1.38  (** methods theory data **)
    1.39  
    1.40 @@ -428,6 +440,16 @@
    1.41  end;
    1.42  
    1.43  
    1.44 +(* insts *)
    1.45 +
    1.46 +val insts =
    1.47 +  Scan.lift (Scan.optional (Args.$$$ "(" |-- Args.!!! (Args.nat --| Args.$$$ ")")) 1) --
    1.48 +    Args.enum1 "and" (Scan.lift (Args.name -- Args.!!! (Args.$$$ "=" |-- Args.name))) --
    1.49 +    (Scan.lift (Args.$$$ "in") |-- Attrib.local_thm);
    1.50 +
    1.51 +fun inst_args f src ctxt = f ((#2 oo syntax insts) ctxt src);
    1.52 +
    1.53 +
    1.54  
    1.55  (** method text **)
    1.56  
    1.57 @@ -444,25 +466,20 @@
    1.58  
    1.59  (* refine *)
    1.60  
    1.61 -fun refine text state =
    1.62 +fun gen_refine f text state =
    1.63    let
    1.64      val thy = Proof.theory_of state;
    1.65  
    1.66 -    fun eval (Basic mth) = Proof.refine mth
    1.67 -      | eval (Source src) = Proof.refine (method thy src)
    1.68 +    fun eval (Basic mth) = f mth
    1.69 +      | eval (Source src) = f (method thy src)
    1.70        | eval (Then txts) = Seq.EVERY (map eval txts)
    1.71        | eval (Orelse txts) = Seq.FIRST (map eval txts)
    1.72        | eval (Try txt) = Seq.TRY (eval txt)
    1.73        | eval (Repeat1 txt) = Seq.REPEAT1 (eval txt);
    1.74    in eval text state end;
    1.75  
    1.76 -fun refine_no_facts text state =
    1.77 -  let val (_, (goal_facts, _)) = Proof.get_goal state in
    1.78 -    state
    1.79 -    |> Proof.goal_facts (K [])
    1.80 -    |> refine text
    1.81 -    |> Seq.map (Proof.goal_facts (K goal_facts))
    1.82 -  end;
    1.83 +val refine = gen_refine Proof.refine;
    1.84 +val refine_end = gen_refine Proof.refine_end;
    1.85  
    1.86  
    1.87  (* structured proof steps *)
    1.88 @@ -525,7 +542,11 @@
    1.89    ("drule", thms_ctxt_args some_drule, "apply some rule in destruct manner (improper!)"),
    1.90    ("frule", thms_ctxt_args some_frule, "apply some rule in forward manner (improper!)"),
    1.91    ("this", no_args this, "apply current facts as rules"),
    1.92 -  ("assumption", ctxt_args assumption, "proof by assumption, preferring facts")];
    1.93 +  ("assumption", ctxt_args assumption, "proof by assumption, preferring facts"),
    1.94 +  ("res_inst_tac", inst_args res_inst, "res_inst_tac emulation (beware!)"),
    1.95 +  ("eres_inst_tac", inst_args eres_inst, "eres_inst_tac emulation (beware!)"),
    1.96 +  ("dres_inst_tac", inst_args dres_inst, "dres_inst_tac emulation (beware!)"),
    1.97 +  ("forw_inst_tac", inst_args forw_inst, "forw_inst_tac emulation (beware!)")];
    1.98  
    1.99  
   1.100  (* setup *)