replaced FIRSTGOAL by FINDGOAL (backtracking!);
authorwenzelm
Fri Jan 28 12:06:52 2000 +0100 (2000-01-28)
changeset 8152ce3387fafebb
parent 8151 9a2bdaa3c379
child 8153 9bdbcb71dc56
replaced FIRSTGOAL by FINDGOAL (backtracking!);
improved flexflex handling;
tuned sig;
src/Pure/Isar/proof.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Fri Jan 28 12:04:17 2000 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Fri Jan 28 12:06:52 2000 +0100
     1.3 @@ -5,8 +5,14 @@
     1.4  Proof states and methods.
     1.5  *)
     1.6  
     1.7 +signature BASIC_PROOF =
     1.8 +sig
     1.9 +  val FINDGOAL: (int -> tactic) -> tactic
    1.10 +end;
    1.11 +
    1.12  signature PROOF =
    1.13  sig
    1.14 +  include BASIC_PROOF
    1.15    type context
    1.16    type state
    1.17    exception STATE of string * state
    1.18 @@ -86,13 +92,13 @@
    1.19    val next_block: state -> state
    1.20  end;
    1.21  
    1.22 -signature PROOF_PRIVATE =
    1.23 +signature PRIVATE_PROOF =
    1.24  sig
    1.25    include PROOF
    1.26    val put_data: Object.kind -> ('a -> Object.T) -> 'a -> state -> state
    1.27  end;
    1.28  
    1.29 -structure Proof: PROOF_PRIVATE =
    1.30 +structure Proof: PRIVATE_PROOF =
    1.31  struct
    1.32  
    1.33  
    1.34 @@ -380,6 +386,12 @@
    1.35      val leave_tfrees = foldr Term.add_term_tfree_names (frees, []);
    1.36    in thm |> Thm.varifyT' leave_tfrees end;
    1.37  
    1.38 +fun export fixes casms thm =
    1.39 +  thm
    1.40 +  |> Drule.implies_intr_list casms
    1.41 +  |> varify_frees fixes
    1.42 +  |> most_general_varify_tfrees;
    1.43 +
    1.44  fun diff_context inner None = (ProofContext.fixed_names inner, ProofContext.assumptions inner)
    1.45    | diff_context inner (Some outer) =
    1.46        (ProofContext.fixed_names inner \\ ProofContext.fixed_names outer,
    1.47 @@ -387,12 +399,6 @@
    1.48  
    1.49  in
    1.50  
    1.51 -fun export fixes casms thm =
    1.52 -  thm
    1.53 -  |> Drule.implies_intr_list casms
    1.54 -  |> varify_frees fixes
    1.55 -  |> most_general_varify_tfrees;
    1.56 -
    1.57  fun export_wrt inner opt_outer =
    1.58    let
    1.59      val (fixes, asms) = diff_context inner opt_outer;
    1.60 @@ -408,13 +414,17 @@
    1.61  fun RANGE [] _ = all_tac
    1.62    | RANGE (tac :: tacs) i = RANGE tacs (i + 1) THEN tac i;
    1.63  
    1.64 +fun FINDGOAL tac st =
    1.65 +  let fun find (i, n) = if i > n then no_tac else tac i APPEND find (i + 1, n)
    1.66 +  in find (1, nprems_of st) st end;
    1.67 +
    1.68  fun export_goal print_rule raw_rule inner state =
    1.69    let
    1.70      val (outer, (_, ((result, (facts, thm)), f))) = find_goal 0 state;
    1.71      val (exp, tacs) = export_wrt inner (Some outer);
    1.72      val rule = exp raw_rule;
    1.73      val _ = print_rule rule;
    1.74 -    val thmq = FIRSTGOAL (Tactic.rtac rule THEN' RANGE (map #1 tacs)) thm;
    1.75 +    val thmq = FINDGOAL (Tactic.rtac rule THEN' RANGE (map #1 tacs)) thm;
    1.76    in Seq.map (fn th => map_goal (K ((result, (facts, th)), f)) state) thmq end;
    1.77  
    1.78  
    1.79 @@ -467,17 +477,6 @@
    1.80    end;
    1.81  
    1.82  
    1.83 -(* prepare final result *)
    1.84 -
    1.85 -fun strip_flexflex thm =
    1.86 -  Seq.hd (Thm.flexflex_rule thm) handle THM _ => thm;
    1.87 -
    1.88 -fun final_result state thm =
    1.89 -  thm
    1.90 -  |> strip_flexflex
    1.91 -  |> Drule.standard;
    1.92 -
    1.93 -
    1.94  
    1.95  (*** structured proof commands ***)
    1.96  
    1.97 @@ -677,7 +676,7 @@
    1.98  fun finish_global state =
    1.99    let
   1.100      val (_, (((kind, name, t), (_, raw_thm)), _)) = current_goal state;   (*ignores after_qed!*)
   1.101 -    val result = final_result state (prep_result state t raw_thm);
   1.102 +    val result = Drule.standard (prep_result state t raw_thm);
   1.103  
   1.104      val atts =
   1.105        (case kind of
   1.106 @@ -730,3 +729,7 @@
   1.107  
   1.108  
   1.109  end;
   1.110 +
   1.111 +
   1.112 +structure BasicProof: BASIC_PROOF = Proof;
   1.113 +open BasicProof;