replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
authorwenzelm
Sat Apr 12 17:00:40 2008 +0200 (2008-04-12)
changeset 2662863306cb94313
parent 26627 dac6d56b7c8d
child 26629 6e93fbd4c96a
replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
src/HOL/Tools/function_package/fundef_core.ML
src/HOL/Tools/function_package/fundef_package.ML
src/Pure/Isar/class.ML
src/Pure/Isar/element.ML
src/Pure/goal.ML
src/Pure/more_thm.ML
     1.1 --- a/src/HOL/Tools/function_package/fundef_core.ML	Sat Apr 12 17:00:38 2008 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_core.ML	Sat Apr 12 17:00:40 2008 +0200
     1.3 @@ -311,7 +311,7 @@
     1.4                                  |> fold_rev (implies_intr o cprop_of) h_assums
     1.5                                  |> fold_rev (implies_intr o cprop_of) ags
     1.6                                  |> fold_rev forall_intr cqs
     1.7 -                                |> Goal.close_result
     1.8 +                                |> Thm.close_derivation
     1.9      in
    1.10        replace_lemma
    1.11      end
    1.12 @@ -439,7 +439,7 @@
    1.13                                    |> (fn it => fold (forall_intr o cterm_of thy) (term_vars (prop_of it)) it)
    1.14  
    1.15          val goalstate =  Conjunction.intr graph_is_function complete
    1.16 -                          |> Goal.close_result
    1.17 +                          |> Thm.close_derivation
    1.18                            |> Goal.protect
    1.19                            |> fold_rev (implies_intr o cprop_of) compat
    1.20                            |> implies_intr (cprop_of complete)
     2.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Sat Apr 12 17:00:38 2008 +0200
     2.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Sat Apr 12 17:00:40 2008 +0200
     2.3 @@ -63,7 +63,7 @@
     2.4  fun fundef_afterqed do_print fixes post defname cont sort_cont cnames [[proof]] lthy =
     2.5      let
     2.6        val FundefResult {fs, R, psimps, trsimps,  simple_pinducts, termination, domintros, cases, ...} = 
     2.7 -          cont (Goal.close_result proof)
     2.8 +          cont (Thm.close_derivation proof)
     2.9  
    2.10        val fnames = map (fst o fst) fixes
    2.11        val qualify = NameSpace.qualified defname
    2.12 @@ -115,7 +115,7 @@
    2.13      let
    2.14        val FundefCtxData { add_simps, case_names, psimps, pinducts, defname, ... } = data
    2.15  
    2.16 -      val totality = Goal.close_result totality
    2.17 +      val totality = Thm.close_derivation totality
    2.18  
    2.19        val remove_domain_condition = full_simplify (HOL_basic_ss addsimps [totality, True_implies_equals])
    2.20  
     3.1 --- a/src/Pure/Isar/class.ML	Sat Apr 12 17:00:38 2008 +0200
     3.2 +++ b/src/Pure/Isar/class.ML	Sat Apr 12 17:00:40 2008 +0200
     3.3 @@ -314,7 +314,7 @@
     3.4      val assm_intro = proto_assm_intro
     3.5        |> Option.map instantiate_base_sort
     3.6        |> Option.map (MetaSimplifier.rewrite_rule defs)
     3.7 -      |> Option.map Goal.close_result;
     3.8 +      |> Option.map Thm.close_derivation;
     3.9      val class_intro = (#intro o AxClass.get_info thy) class;
    3.10      val fixate = Thm.instantiate
    3.11        (map (pairself (Thm.ctyp_of thy)) [(TVar ((Name.aT, 0), []), TFree (Name.aT, base_sort)),
    3.12 @@ -334,7 +334,7 @@
    3.13          |> replicate num_trivs;
    3.14      val of_class = (fixate class_intro OF of_class_sups OF locale_dests OF pred_trivs)
    3.15        |> Drule.standard'
    3.16 -      |> Goal.close_result;
    3.17 +      |> Thm.close_derivation;
    3.18      val this_intro = assm_intro |> the_default class_intro;
    3.19    in
    3.20      thy
     4.1 --- a/src/Pure/Isar/element.ML	Sat Apr 12 17:00:38 2008 +0200
     4.2 +++ b/src/Pure/Isar/element.ML	Sat Apr 12 17:00:40 2008 +0200
     4.3 @@ -291,13 +291,13 @@
     4.4    Witness (t, Goal.protect (Thm.assume (Thm.cterm_of thy t)));
     4.5  
     4.6  fun prove_witness ctxt t tac =
     4.7 -  Witness (t, Goal.close_result (Goal.prove ctxt [] [] (Logic.protect t) (fn _ =>
     4.8 +  Witness (t, Thm.close_derivation (Goal.prove ctxt [] [] (Logic.protect t) (fn _ =>
     4.9      Tactic.rtac Drule.protectI 1 THEN tac)));
    4.10  
    4.11 -val close_witness = map_witness (fn (t, th) => (t, Goal.close_result th));
    4.12 +val close_witness = map_witness (fn (t, th) => (t, Thm.close_derivation th));
    4.13  
    4.14  fun conclude_witness (Witness (_, th)) =
    4.15 -  Goal.close_result (MetaSimplifier.norm_hhf_protect (Goal.conclude th));
    4.16 +  Thm.close_derivation (MetaSimplifier.norm_hhf_protect (Goal.conclude th));
    4.17  
    4.18  fun compose_witness (Witness (_, th)) r =
    4.19    let
     5.1 --- a/src/Pure/goal.ML	Sat Apr 12 17:00:38 2008 +0200
     5.2 +++ b/src/Pure/goal.ML	Sat Apr 12 17:00:40 2008 +0200
     5.3 @@ -20,7 +20,6 @@
     5.4    val conclude: thm -> thm
     5.5    val finish: thm -> thm
     5.6    val norm_result: thm -> thm
     5.7 -  val close_result: thm -> thm
     5.8    val prove_internal: cterm list -> cterm -> (thm list -> tactic) -> thm
     5.9    val prove_multi: Proof.context -> string list -> term list -> term list ->
    5.10      ({prems: thm list, context: Proof.context} -> tactic) -> thm list
    5.11 @@ -84,18 +83,12 @@
    5.12  
    5.13  (** results **)
    5.14  
    5.15 -(* normal form *)
    5.16 -
    5.17  val norm_result =
    5.18    Drule.flexflex_unique
    5.19    #> MetaSimplifier.norm_hhf_protect
    5.20    #> Thm.strip_shyps
    5.21    #> Drule.zero_var_indexes;
    5.22  
    5.23 -val close_result =
    5.24 -  Thm.compress
    5.25 -  #> Drule.close_derivation;
    5.26 -
    5.27  
    5.28  
    5.29  (** tactical theorem proving **)
     6.1 --- a/src/Pure/more_thm.ML	Sat Apr 12 17:00:38 2008 +0200
     6.2 +++ b/src/Pure/more_thm.ML	Sat Apr 12 17:00:40 2008 +0200
     6.3 @@ -53,6 +53,7 @@
     6.4    val read_cterm: theory -> string * typ -> cterm
     6.5    val elim_implies: thm -> thm -> thm
     6.6    val unvarify: thm -> thm
     6.7 +  val close_derivation: thm -> thm
     6.8    val add_axiom: term list -> bstring * term -> theory -> thm * theory
     6.9    val add_def: bool -> bool -> bstring * term -> theory -> thm * theory
    6.10  end;
    6.11 @@ -250,6 +251,10 @@
    6.12        in (cert (Var ((a, i), T')), cert (Free ((a, T')))) end);
    6.13    in Thm.instantiate (instT, inst) th end;
    6.14  
    6.15 +fun close_derivation thm =
    6.16 +  if Thm.get_name thm = "" then Thm.put_name "" thm
    6.17 +  else thm;
    6.18 +
    6.19  
    6.20  
    6.21  (** specification primitives **)