auto_bind_goal, auto_bind_facts;
authorwenzelm
Sat Jun 05 20:34:53 1999 +0200 (1999-06-05)
changeset 67900a39f22f847a
parent 6789 0e5a965de17a
child 6791 2be411437c60
auto_bind_goal, auto_bind_facts;
varify_tfrees: no longer generalize types of free term variables;
let_thms: no bindings;
src/Pure/Isar/proof.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Sat Jun 05 20:33:27 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Sat Jun 05 20:34:53 1999 +0200
     1.3 @@ -151,15 +151,17 @@
     1.4  fun put_data kind f = map_context o ProofContext.put_data kind f;
     1.5  val declare_term = map_context o ProofContext.declare_term;
     1.6  val add_binds = map_context o ProofContext.add_binds_i;
     1.7 +val auto_bind_goal = map_context o ProofContext.auto_bind_goal;
     1.8 +val auto_bind_facts = map_context o ProofContext.auto_bind_facts;
     1.9  val put_thms = map_context o ProofContext.put_thms;
    1.10  val put_thmss = map_context o ProofContext.put_thmss;
    1.11  
    1.12  
    1.13  (* bind statements *)
    1.14  
    1.15 +(* FIXME
    1.16  fun bind_props bs state =
    1.17 -  let val mk_bind = map (fn (x, t) => ((Syntax.binding x, 0), t)) o ObjectLogic.dest_statement
    1.18 -  in state |> add_binds (flat (map mk_bind bs)) end;
    1.19 +  state |> add_binds (flat (map ObjectLogic.statement_bindings bs)) end;
    1.20  
    1.21  fun bind_thms (name, thms) state =
    1.22    let
    1.23 @@ -174,6 +176,13 @@
    1.24    state
    1.25    |> put_thms name_thms
    1.26    |> bind_thms name_thms;
    1.27 +*)
    1.28 +
    1.29 +(* FIXME elim (!?) *)
    1.30 +
    1.31 +fun let_thms name_thms state =
    1.32 +  state
    1.33 +  |> put_thms name_thms;
    1.34  
    1.35  
    1.36  (* facts *)
    1.37 @@ -352,6 +361,13 @@
    1.38      |> Drule.forall_elim_vars (maxidx + 1)
    1.39    end;
    1.40  
    1.41 +fun varify_tfrees thm =
    1.42 +  let
    1.43 +    val {hyps, prop, ...} = Thm.rep_thm thm;
    1.44 +    val frees = foldr Term.add_term_frees (prop :: hyps, []);
    1.45 +    val leave_tfrees = foldr Term.add_term_tfree_names (frees, []);
    1.46 +  in thm |> Thm.varifyT' leave_tfrees end;
    1.47 +
    1.48  fun implies_elim_hyps thm =
    1.49    foldl (uncurry Thm.implies_elim) (thm, map Thm.assume (Drule.cprems_of thm));
    1.50  
    1.51 @@ -370,7 +386,7 @@
    1.52        |> implies_elim_hyps
    1.53        |> Drule.implies_intr_list asms
    1.54        |> varify_frees (ProofContext.fixed_names ctxt)
    1.55 -      |> Thm.varifyT;
    1.56 +      |> varify_tfrees;
    1.57  
    1.58      val {hyps, prop, sign, ...} = Thm.rep_thm thm;
    1.59      val tsig = Sign.tsig_of sign;
    1.60 @@ -384,7 +400,7 @@
    1.61        err ("Additional hypotheses:\n" ^ cat_lines (map (Sign.string_of_term sign) hyps))
    1.62  (* FIXME    else if not (Pattern.matches tsig (t, Logic.skip_flexpairs prop)) then
    1.63        err ("Proved a different theorem: " ^ Sign.string_of_term sign prop) *)
    1.64 -    else thm
    1.65 +    else (thm, prop)
    1.66    end;
    1.67  
    1.68  
    1.69 @@ -509,7 +525,7 @@
    1.70    in
    1.71      state'
    1.72      |> put_goal (Some ((kind atts, (PureThy.default_name name), casms @ cprems, prop), ([], thm)))
    1.73 -    |> bind_props [("thesis", prop)]
    1.74 +    |> auto_bind_goal prop
    1.75      |> (if is_chain state then use_facts else reset_facts)
    1.76      |> new_block
    1.77      |> enter_backward
    1.78 @@ -614,7 +630,7 @@
    1.79  fun finish_local print_result state =
    1.80    let
    1.81      val ((kind, name, asms, t), (_, raw_thm)) = current_goal state;
    1.82 -    val result = prep_result state asms t raw_thm;
    1.83 +    val (result, result_prop) = prep_result state asms t raw_thm;
    1.84      val (atts, opt_solve) =
    1.85        (case kind of
    1.86          Goal atts => (atts, solve_goal result)
    1.87 @@ -624,6 +640,7 @@
    1.88      print_result {kind = kind_name kind, name = name, thm = result};
    1.89      state
    1.90      |> close_block
    1.91 +    |> auto_bind_facts [result_prop]
    1.92      |> have_thmss name atts [Thm.no_attributes [result]]
    1.93      |> opt_solve
    1.94    end;
    1.95 @@ -639,7 +656,7 @@
    1.96  fun finish_global alt_name alt_atts state =
    1.97    let
    1.98      val ((kind, def_name, asms, t), (_, raw_thm)) = current_goal state;
    1.99 -    val result = final_result state (prep_result state asms t raw_thm);
   1.100 +    val result = final_result state (#1 (prep_result state asms t raw_thm));
   1.101  
   1.102      val name = if_none alt_name def_name;
   1.103      val atts =