# HG changeset patch # User paulson # Date 912764720 -3600 # Node ID dbb33359a7ab3c005c53da2dbf004463ca329fa1 # Parent 797c76d6ff041c39010069cf4852b75ea48af518 better export for nested locales diff -r 797c76d6ff04 -r dbb33359a7ab src/Pure/Thy/context.ML --- a/src/Pure/Thy/context.ML Fri Dec 04 10:44:02 1998 +0100 +++ b/src/Pure/Thy/context.ML Fri Dec 04 10:45:20 1998 +0100 @@ -15,6 +15,7 @@ val Goalw: thm list -> string -> thm list val Open_locale: xstring -> unit val Close_locale: unit -> unit + val Export: thm -> thm end; signature CONTEXT = @@ -89,7 +90,7 @@ fun Open_locale xname = (Locale.open_locale xname (the_context ()); ()); fun Close_locale () = (Locale.close_locale (the_context ()); ()); - +fun Export th = export_thy (the_context ()) th; end; diff -r 797c76d6ff04 -r dbb33359a7ab src/Pure/goals.ML --- a/src/Pure/goals.ML Fri Dec 04 10:44:02 1998 +0100 +++ b/src/Pure/goals.ML Fri Dec 04 10:45:20 1998 +0100 @@ -28,6 +28,7 @@ val byev : tactic list -> unit val chop : unit -> unit val choplev : int -> unit + val export_thy : theory -> thm -> thm val export : thm -> thm val fa : unit -> unit val fd : thm -> unit @@ -141,8 +142,40 @@ end; (** exporting a theorem out of a locale means turning all meta-hyps into assumptions - and expand and cancel the locale definitions. It's relatively easy, because - a definiendum is a locale const, hence Free, hence Var, after standard **) + and expand and cancel the locale definitions. + export goes through all levels in case of nested locales, whereas + export_thy just goes one up. (Here the version with theory parameter, the real export + resides in Thy/context.ML **) + +fun get_top_scope_thms thy = + let val sc = (Locale.get_scope_sg (sign_of thy)) + in if (null sc) then (warning "No locale in theory"; []) + else map (#prop o rep_thm) (map #2 (#thms(snd(hd sc)))) + end; + +fun implies_intr_some_hyps thy A_set th = + let + val sign = sign_of thy; + val used_As = A_set inter #hyps(rep_thm(th)); + val ctl = map (cterm_of sign) used_As + in foldl (fn (x, y) => Thm.implies_intr y x) (th, ctl) + end; + +fun standard_some thy A_set th = + let val {maxidx,...} = rep_thm th + in + th |> implies_intr_some_hyps thy A_set + |> forall_intr_frees |> forall_elim_vars (maxidx + 1) + |> Thm.strip_shyps |> Thm.implies_intr_shyps + |> zero_var_indexes |> Thm.varifyT |> Thm.compress + end; + +fun export_thy thy th = + let val A_set = get_top_scope_thms thy + in + standard_some thy [] (Seq.hd ((REPEAT (FIRSTGOAL (rtac reflexive_thm))) (standard_some thy A_set th))) + end; + val export = standard o Seq.hd o (REPEAT (FIRSTGOAL (rtac reflexive_thm))) o standard; (*Common treatment of "goal" and "prove_goal":