src/Pure/Isar/method.ML
changeset 30165 6ee87f67d9cd
parent 29857 2cc976ed8a3c
child 30190 479806475f3c
     1.1 --- a/src/Pure/Isar/method.ML	Sat Feb 28 14:42:54 2009 +0100
     1.2 +++ b/src/Pure/Isar/method.ML	Sat Feb 28 14:52:21 2009 +0100
     1.3 @@ -49,7 +49,6 @@
     1.4    val erule: int -> thm list -> method
     1.5    val drule: int -> thm list -> method
     1.6    val frule: int -> thm list -> method
     1.7 -  val iprover_tac: Proof.context -> int option -> int -> tactic
     1.8    val set_tactic: (thm list -> tactic) -> Proof.context -> Proof.context
     1.9    val tactic: string * Position.T -> Proof.context -> method
    1.10    val raw_tactic: string * Position.T -> Proof.context -> method
    1.11 @@ -296,55 +295,6 @@
    1.12      THEN Tactic.distinct_subgoals_tac;
    1.13  
    1.14  
    1.15 -(* iprover -- intuitionistic proof search *)
    1.16 -
    1.17 -local
    1.18 -
    1.19 -val remdups_tac = SUBGOAL (fn (g, i) =>
    1.20 -  let val prems = Logic.strip_assums_hyp g in
    1.21 -    REPEAT_DETERM_N (length prems - length (distinct op aconv prems))
    1.22 -    (Tactic.ematch_tac [Drule.remdups_rl] i THEN Tactic.eq_assume_tac i)
    1.23 -  end);
    1.24 -
    1.25 -fun REMDUPS tac = tac THEN_ALL_NEW remdups_tac;
    1.26 -
    1.27 -val bires_tac = Tactic.biresolution_from_nets_tac ContextRules.orderlist;
    1.28 -
    1.29 -fun safe_step_tac ctxt =
    1.30 -  ContextRules.Swrap ctxt
    1.31 -   (eq_assume_tac ORELSE'
    1.32 -    bires_tac true (ContextRules.netpair_bang ctxt));
    1.33 -
    1.34 -fun unsafe_step_tac ctxt =
    1.35 -  ContextRules.wrap ctxt
    1.36 -   (assume_tac APPEND'
    1.37 -    bires_tac false (ContextRules.netpair_bang ctxt) APPEND'
    1.38 -    bires_tac false (ContextRules.netpair ctxt));
    1.39 -
    1.40 -fun step_tac ctxt i =
    1.41 -  REPEAT_DETERM1 (REMDUPS (safe_step_tac ctxt) i) ORELSE
    1.42 -  REMDUPS (unsafe_step_tac ctxt) i;
    1.43 -
    1.44 -fun intprover_tac ctxt gs d lim = SUBGOAL (fn (g, i) => if d > lim then no_tac else
    1.45 -  let
    1.46 -    val ps = Logic.strip_assums_hyp g;
    1.47 -    val c = Logic.strip_assums_concl g;
    1.48 -  in
    1.49 -    if member (fn ((ps1, c1), (ps2, c2)) =>
    1.50 -        c1 aconv c2 andalso
    1.51 -        length ps1 = length ps2 andalso
    1.52 -        gen_eq_set (op aconv) (ps1, ps2)) gs (ps, c) then no_tac
    1.53 -    else (step_tac ctxt THEN_ALL_NEW intprover_tac ctxt ((ps, c) :: gs) (d + 1) lim) i
    1.54 -  end);
    1.55 -
    1.56 -in
    1.57 -
    1.58 -fun iprover_tac ctxt opt_lim =
    1.59 -  SELECT_GOAL (DEEPEN (2, the_default 20 opt_lim) (intprover_tac ctxt [] 0) 4 1);
    1.60 -
    1.61 -end;
    1.62 -
    1.63 -
    1.64  (* ML tactics *)
    1.65  
    1.66  structure TacticData = ProofDataFun
    1.67 @@ -511,39 +461,6 @@
    1.68  end;
    1.69  
    1.70  
    1.71 -(* iprover syntax *)
    1.72 -
    1.73 -local
    1.74 -
    1.75 -val introN = "intro";
    1.76 -val elimN = "elim";
    1.77 -val destN = "dest";
    1.78 -val ruleN = "rule";
    1.79 -
    1.80 -fun modifier name kind kind' att =
    1.81 -  Args.$$$ name |-- (kind >> K NONE || kind' |-- P.nat --| Args.colon >> SOME)
    1.82 -    >> (pair (I: Proof.context -> Proof.context) o att);
    1.83 -
    1.84 -val iprover_modifiers =
    1.85 - [modifier destN Args.bang_colon Args.bang ContextRules.dest_bang,
    1.86 -  modifier destN Args.colon (Scan.succeed ()) ContextRules.dest,
    1.87 -  modifier elimN Args.bang_colon Args.bang ContextRules.elim_bang,
    1.88 -  modifier elimN Args.colon (Scan.succeed ()) ContextRules.elim,
    1.89 -  modifier introN Args.bang_colon Args.bang ContextRules.intro_bang,
    1.90 -  modifier introN Args.colon (Scan.succeed ()) ContextRules.intro,
    1.91 -  Args.del -- Args.colon >> K (I, ContextRules.rule_del)];
    1.92 -
    1.93 -in
    1.94 -
    1.95 -val iprover_meth =
    1.96 -  bang_sectioned_args' iprover_modifiers (Scan.lift (Scan.option P.nat))
    1.97 -    (fn n => fn prems => fn ctxt => METHOD (fn facts =>
    1.98 -      HEADGOAL (insert_tac (prems @ facts) THEN'
    1.99 -      ObjectLogic.atomize_prems_tac THEN' iprover_tac ctxt n)));
   1.100 -
   1.101 -end;
   1.102 -
   1.103 -
   1.104  (* tactic syntax *)
   1.105  
   1.106  fun nat_thms_args f = uncurry f oo
   1.107 @@ -599,7 +516,6 @@
   1.108      ("fold", thms_ctxt_args fold_meth, "fold definitions"),
   1.109      ("atomize", (atomize o fst) oo syntax (Args.mode "full"),
   1.110        "present local premises as object-level statements"),
   1.111 -    ("iprover", iprover_meth, "intuitionistic proof search"),
   1.112      ("rule", thms_ctxt_args some_rule, "apply some intro/elim rule"),
   1.113      ("erule", nat_thms_args erule, "apply rule in elimination manner (improper)"),
   1.114      ("drule", nat_thms_args drule, "apply rule in destruct manner (improper)"),