src/Pure/Isar/proof.ML
changeset 11816 545aab7410ac
parent 11793 5f0ab6f5c280
child 11891 99569e5f0ab5
     1.1 --- a/src/Pure/Isar/proof.ML	Tue Oct 16 23:00:21 2001 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Tue Oct 16 23:02:14 2001 +0200
     1.3 @@ -62,8 +62,6 @@
     1.4      (thm list * context attribute list) list) list -> state -> state
     1.5    val fix: (string list * string option) list -> state -> state
     1.6    val fix_i: (string list * typ option) list -> state -> state
     1.7 -  val hard_asm_tac: int -> tactic
     1.8 -  val soft_asm_tac: int -> tactic
     1.9    val assm: ProofContext.exporter
    1.10      -> ((string * context attribute list) * (string * (string list * string list)) list) list
    1.11      -> state -> state
    1.12 @@ -413,20 +411,26 @@
    1.13  
    1.14  (* export results *)
    1.15  
    1.16 +fun refine_tac rule =
    1.17 +  Tactic.rtac rule THEN_ALL_NEW (SUBGOAL (fn (goal, i) =>
    1.18 +    if can Logic.dest_goal (Logic.strip_assums_concl goal) then
    1.19 +      Tactic.etac Drule.triv_goal i
    1.20 +    else all_tac));
    1.21 +
    1.22  fun export_goal print_rule raw_rule inner state =
    1.23    let
    1.24      val (outer, (_, ((result, (facts, thm)), f))) = find_goal state;
    1.25 -    val (exp_tac, tacs) = ProofContext.export_wrt true inner (Some outer);
    1.26 +    val exp_tac = ProofContext.export_wrt true inner (Some outer);
    1.27      fun exp_rule rule =
    1.28        let
    1.29          val _ = print_rule rule;
    1.30 -        val thmq = FINDGOAL (Tactic.rtac rule THEN' RANGE tacs) thm;
    1.31 +        val thmq = FINDGOAL (refine_tac rule) thm;
    1.32        in Seq.map (fn th => map_goal I (K ((result, (facts, th)), f)) state) thmq end;
    1.33    in raw_rule |> exp_tac |> (Seq.flat o Seq.map exp_rule) end;
    1.34  
    1.35  fun export_thm inner thm =
    1.36 -  let val (exp_tac, tacs) = ProofContext.export_wrt false inner None in
    1.37 -    (case Seq.chop (2, (exp_tac THEN RANGE tacs 1) thm) of
    1.38 +  let val exp_tac = ProofContext.export_wrt false inner None in
    1.39 +    (case Seq.chop (2, exp_tac thm) of
    1.40        ([thm'], _) => thm'
    1.41      | ([], _) => raise THM ("export: failed", 0, [thm])
    1.42      | _ => raise THM ("export: more than one result", 0, [thm]))
    1.43 @@ -437,9 +441,9 @@
    1.44      None => Seq.single (reset_facts state)
    1.45    | Some thms =>
    1.46        let
    1.47 -        val (exp_tac, tacs) =
    1.48 +        val exp_tac =
    1.49            ProofContext.export_wrt false (context_of inner_state) (Some (context_of state));
    1.50 -        val thmqs = map (exp_tac THEN RANGE tacs 1) thms;
    1.51 +        val thmqs = map exp_tac thms;
    1.52        in Seq.map (fn ths => put_facts (Some ths) state) (Seq.commute thmqs) end);
    1.53  
    1.54  
    1.55 @@ -460,7 +464,7 @@
    1.56      val tsig = Sign.tsig_of sign;
    1.57  
    1.58      val casms = flat (map #1 (assumptions state));
    1.59 -    val bad_hyps = Library.gen_rems Term.aconv (hyps, map (Thm.term_of o Drule.mk_cgoal) casms);
    1.60 +    val bad_hyps = Library.gen_rems Term.aconv (hyps, map Thm.term_of casms);
    1.61    in
    1.62      if not (null bad_hyps) then
    1.63        err ("Additional hypotheses:\n" ^ cat_lines (map (Sign.string_of_term sign) bad_hyps))
    1.64 @@ -518,9 +522,6 @@
    1.65  
    1.66  (* assume *)
    1.67  
    1.68 -val hard_asm_tac = Tactic.etac Drule.triv_goal;
    1.69 -val soft_asm_tac = Tactic.rtac Drule.triv_goal THEN' Tactic.norm_hhf_tac;
    1.70 -
    1.71  local
    1.72  
    1.73  fun gen_assume f exp args state =
    1.74 @@ -531,18 +532,19 @@
    1.75      these_factss (st, factss)
    1.76      |> put_thms ("prems", prems));
    1.77  
    1.78 -fun simple_exporter tac1 tac2 =
    1.79 -  (Seq.single oo Drule.implies_intr_list, fn is_goal => fn n =>
    1.80 -    replicate n (Tactic.norm_hhf_tac THEN' (if is_goal then tac1 else tac2)));
    1.81 +fun export_assume true = Seq.single oo Drule.implies_intr_goals
    1.82 +  | export_assume false = Seq.single oo Drule.implies_intr_list;
    1.83 +
    1.84 +fun export_presume _ = export_assume false;
    1.85  
    1.86  in
    1.87  
    1.88  val assm = gen_assume ProofContext.assume;
    1.89  val assm_i = gen_assume ProofContext.assume_i;
    1.90 -val assume = assm (simple_exporter hard_asm_tac soft_asm_tac);
    1.91 -val assume_i = assm_i (simple_exporter hard_asm_tac soft_asm_tac);
    1.92 -val presume = assm (simple_exporter soft_asm_tac soft_asm_tac);
    1.93 -val presume_i = assm_i (simple_exporter soft_asm_tac soft_asm_tac);
    1.94 +val assume = assm export_assume;
    1.95 +val assume_i = assm_i export_assume;
    1.96 +val presume = assm export_presume;
    1.97 +val presume_i = assm_i export_presume;
    1.98  
    1.99  end;
   1.100  
   1.101 @@ -676,7 +678,7 @@
   1.102      val outer_ctxt = context_of outer_state;
   1.103  
   1.104      val result = prep_result state t raw_thm;
   1.105 -    val resultq = #1 (ProofContext.export_wrt false goal_ctxt (Some outer_ctxt)) result;
   1.106 +    val resultq = ProofContext.export_wrt false goal_ctxt (Some outer_ctxt) result;
   1.107  
   1.108      val (atts, opt_solve) =
   1.109        (case kind of