src/Pure/Isar/proof.ML
changeset 7605 8bbfcb54054e
parent 7580 536499cf71af
child 7632 25a0d2ba3a87
     1.1 --- a/src/Pure/Isar/proof.ML	Sat Sep 25 13:18:38 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Sat Sep 25 13:19:33 1999 +0200
     1.3 @@ -15,6 +15,7 @@
     1.4    val context_of: state -> context
     1.5    val theory_of: state -> theory
     1.6    val sign_of: state -> Sign.sg
     1.7 +  val reset_thms: string -> state -> state
     1.8    val the_facts: state -> thm list
     1.9    val get_goal: state -> thm list * thm
    1.10    val goal_facts: (state -> thm list) -> state -> state
    1.11 @@ -183,6 +184,7 @@
    1.12  val auto_bind_facts = map_context oo ProofContext.auto_bind_facts;
    1.13  val put_thms = map_context o ProofContext.put_thms;
    1.14  val put_thmss = map_context o ProofContext.put_thmss;
    1.15 +val reset_thms = map_context o ProofContext.reset_thms;
    1.16  val assumptions = ProofContext.assumptions o context_of;
    1.17  
    1.18  
    1.19 @@ -194,10 +196,13 @@
    1.20  fun assert_facts state = (the_facts state; state);
    1.21  fun get_facts (State (Node {facts, ...}, _)) = facts;
    1.22  
    1.23 +
    1.24 +val thisN = "this";
    1.25 +
    1.26  fun put_facts facts state =
    1.27    state
    1.28    |> map_current (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal))
    1.29 -  |> put_thms ("this", if_none facts []);
    1.30 +  |> (case facts of None => reset_thms thisN | Some ths => put_thms (thisN, ths));
    1.31  
    1.32  val reset_facts = put_facts None;
    1.33  
    1.34 @@ -456,8 +461,8 @@
    1.35    in
    1.36      if not (null bad_hyps) then
    1.37        err ("Additional hypotheses:\n" ^ cat_lines (map (Sign.string_of_term sign) bad_hyps))
    1.38 -(* FIXME    else if not (Pattern.matches tsig (t, Logic.skip_flexpairs prop)) then
    1.39 -      err ("Proved a different theorem: " ^ Sign.string_of_term sign prop) *)
    1.40 +    else if not (t aconv prop) then
    1.41 +      err ("Proved a different theorem: " ^ Sign.string_of_term sign prop)
    1.42      else Drule.forall_elim_vars (maxidx + 1) thm
    1.43    end;
    1.44  
    1.45 @@ -497,8 +502,8 @@
    1.46    |> map_context (f x)
    1.47    |> reset_facts;
    1.48  
    1.49 -val bind = gen_bind ProofContext.add_binds;
    1.50 -val bind_i = gen_bind ProofContext.add_binds_i;
    1.51 +val bind = gen_bind (ProofContext.add_binds o map (apsnd Some))
    1.52 +val bind_i = gen_bind (ProofContext.add_binds_i o map (apsnd Some))
    1.53  
    1.54  val match_bind = gen_bind ProofContext.match_binds;
    1.55  val match_bind_i = gen_bind ProofContext.match_binds_i;
    1.56 @@ -588,14 +593,6 @@
    1.57        |> enter_forward
    1.58        |> map_context_result (fn c => prepp (c, raw_propp));
    1.59      val cprop = Thm.cterm_of (sign_of state') prop;
    1.60 -(* FIXME
    1.61 -    val casms = map #1 (assumptions state');
    1.62 -
    1.63 -    val revcut_rl = Drule.incr_indexes_wrt [] [] (cprop :: casms) [] Drule.revcut_rl;
    1.64 -    fun cut_asm (casm, thm) = Thm.rotate_rule ~1 1 ((Drule.assume_goal casm COMP revcut_rl) RS thm);
    1.65 -
    1.66 -    val goal = foldr cut_asm (casms, Drule.mk_triv_goal cprop);
    1.67 -*)
    1.68      val goal = Drule.mk_triv_goal cprop;
    1.69    in
    1.70      state'