src/Pure/Isar/proof.ML
changeset 11917 9a0a736d820b
parent 11906 a71713885e3e
child 11924 b6def266cbb9
     1.1 --- a/src/Pure/Isar/proof.ML	Tue Oct 23 23:28:01 2001 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Tue Oct 23 23:28:59 2001 +0200
     1.3 @@ -8,7 +8,6 @@
     1.4  
     1.5  signature BASIC_PROOF =
     1.6  sig
     1.7 -  val RANGE: (int -> tactic) list -> int -> tactic
     1.8    val FINDGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
     1.9    val HEADGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
    1.10  end;
    1.11 @@ -398,10 +397,7 @@
    1.12  end;
    1.13  
    1.14  
    1.15 -(* tacticals *)
    1.16 -
    1.17 -fun RANGE [] _ = all_tac
    1.18 -  | RANGE (tac :: tacs) i = RANGE tacs (i + 1) THEN tac i;
    1.19 +(* goal addressing *)
    1.20  
    1.21  fun FINDGOAL tac st =
    1.22    let fun find (i, n) = if i > n then Seq.fail else Seq.APPEND (tac i, find (i + 1, n))
    1.23 @@ -515,8 +511,6 @@
    1.24  
    1.25  (* assume and presume *)
    1.26  
    1.27 -local
    1.28 -
    1.29  fun gen_assume f exp args state =
    1.30    state
    1.31    |> assert_forward
    1.32 @@ -525,40 +519,17 @@
    1.33      these_factss (st, factss)
    1.34      |> put_thms ("prems", prems));
    1.35  
    1.36 -fun export_assume true = Seq.single oo Drule.implies_intr_goals
    1.37 -  | export_assume false = Seq.single oo Drule.implies_intr_list;
    1.38 -
    1.39 -fun export_presume _ = export_assume false;
    1.40 -
    1.41 -in
    1.42 -
    1.43  val assm = gen_assume ProofContext.assume;
    1.44  val assm_i = gen_assume ProofContext.assume_i;
    1.45 -val assume = assm export_assume;
    1.46 -val assume_i = assm_i export_assume;
    1.47 -val presume = assm export_presume;
    1.48 -val presume_i = assm_i export_presume;
    1.49 +val assume = assm ProofContext.export_assume;
    1.50 +val assume_i = assm_i ProofContext.export_assume;
    1.51 +val presume = assm ProofContext.export_presume;
    1.52 +val presume_i = assm_i ProofContext.export_presume;
    1.53  
    1.54 -end;
    1.55  
    1.56  
    1.57  (** local definitions **)
    1.58  
    1.59 -local
    1.60 -
    1.61 -fun dest_lhs cprop =
    1.62 -  let val x = #1 (Logic.dest_equals (Thm.term_of cprop))
    1.63 -  in Term.dest_Free x; Thm.cterm_of (Thm.sign_of_cterm cprop) x end
    1.64 -  handle TERM _ => raise TERM ("Malformed definitional assumption encountered:\n" ^
    1.65 -      quote (Display.string_of_cterm cprop), []);
    1.66 -
    1.67 -fun export_def _ cprops thm =
    1.68 -  thm
    1.69 -  |> Drule.implies_intr_list cprops
    1.70 -  |> Drule.forall_intr_list (map dest_lhs cprops)
    1.71 -  |> Drule.forall_elim_vars 0
    1.72 -  |> RANGE (replicate (length cprops) (Tactic.rtac Drule.reflexive_thm)) 1;
    1.73 -
    1.74  fun gen_def fix prep_term prep_pats raw_name atts (x, (raw_rhs, raw_pats)) state =
    1.75    let
    1.76      val _ = assert_forward state;
    1.77 @@ -576,16 +547,12 @@
    1.78      state
    1.79      |> fix [([x], None)]
    1.80      |> match_bind_i [(pats, rhs)]
    1.81 -    |> assm_i export_def [((name, atts), [(Logic.mk_equals (lhs, rhs), ([], []))])]
    1.82 +    |> assm_i ProofContext.export_def [((name, atts), [(Logic.mk_equals (lhs, rhs), ([], []))])]
    1.83    end;
    1.84  
    1.85 -in
    1.86 -
    1.87  val def = gen_def fix ProofContext.read_term ProofContext.read_term_pats;
    1.88  val def_i = gen_def fix_i ProofContext.cert_term ProofContext.cert_term_pats;
    1.89  
    1.90 -end;
    1.91 -
    1.92  
    1.93  (* invoke_case *)
    1.94  
    1.95 @@ -801,6 +768,5 @@
    1.96  
    1.97  end;
    1.98  
    1.99 -
   1.100  structure BasicProof: BASIC_PROOF = Proof;
   1.101  open BasicProof;