src/Provers/IsaPlanner/isand.ML
changeset 23171 861f63a35d31
parent 23170 94e9413bd7fc
child 23172 f1ae6a8648ef
     1.1 --- a/src/Provers/IsaPlanner/isand.ML	Thu May 31 19:11:19 2007 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,642 +0,0 @@
     1.4 -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
     1.5 -(*  Title:      Pure/IsaPlanner/isand.ML
     1.6 -    ID:		$Id$
     1.7 -    Author:     Lucas Dixon, University of Edinburgh
     1.8 -                lucas.dixon@ed.ac.uk
     1.9 -    Updated:    26 Apr 2005
    1.10 -    Date:       6 Aug 2004
    1.11 -*)
    1.12 -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
    1.13 -(*  DESCRIPTION:
    1.14 -
    1.15 -    Natural Deduction tools
    1.16 -
    1.17 -    For working with Isabelle theorems in a natural detuction style.
    1.18 -    ie, not having to deal with meta level quantified varaibles,
    1.19 -    instead, we work with newly introduced frees, and hide the
    1.20 -    "all"'s, exporting results from theorems proved with the frees, to
    1.21 -    solve the all cases of the previous goal. This allows resolution
    1.22 -    to do proof search normally. 
    1.23 -
    1.24 -    Note: A nice idea: allow exporting to solve any subgoal, thus
    1.25 -    allowing the interleaving of proof, or provide a structure for the
    1.26 -    ordering of proof, thus allowing proof attempts in parrell, but
    1.27 -    recording the order to apply things in.
    1.28 -
    1.29 -    THINK: are we really ok with our varify name w.r.t the prop - do
    1.30 -    we also need to avoid names in the hidden hyps? What about
    1.31 -    unification contraints in flex-flex pairs - might they also have
    1.32 -    extra free vars?
    1.33 -*)
    1.34 -
    1.35 -signature ISA_ND =
    1.36 -sig
    1.37 -
    1.38 -  (* export data *)
    1.39 -  datatype export = export of
    1.40 -           {gth: Thm.thm, (* initial goal theorem *)
    1.41 -            sgid: int, (* subgoal id which has been fixed etc *)
    1.42 -            fixes: Thm.cterm list, (* frees *)
    1.43 -            assumes: Thm.cterm list} (* assumptions *)
    1.44 -  val fixes_of_exp : export -> Thm.cterm list
    1.45 -  val export_back : export -> Thm.thm -> Thm.thm Seq.seq
    1.46 -  val export_solution : export -> Thm.thm -> Thm.thm
    1.47 -  val export_solutions : export list * Thm.thm -> Thm.thm
    1.48 -
    1.49 -  (* inserting meta level params for frees in the conditions *)
    1.50 -  val allify_conditions :
    1.51 -      (Term.term -> Thm.cterm) ->
    1.52 -      (string * Term.typ) list -> Thm.thm -> Thm.thm * Thm.cterm list
    1.53 -  val allify_conditions' :
    1.54 -      (string * Term.typ) list -> Thm.thm -> Thm.thm * Thm.cterm list
    1.55 -  val assume_allified :
    1.56 -      theory -> (string * Term.sort) list * (string * Term.typ) list
    1.57 -      -> Term.term -> (Thm.cterm * Thm.thm)
    1.58 -
    1.59 -  (* meta level fixed params (i.e. !! vars) *)
    1.60 -  val fix_alls_in_term : Term.term -> Term.term * Term.term list
    1.61 -  val fix_alls_term : int -> Term.term -> Term.term * Term.term list
    1.62 -  val fix_alls_cterm : int -> Thm.thm -> Thm.cterm * Thm.cterm list
    1.63 -  val fix_alls' : int -> Thm.thm -> Thm.thm * Thm.cterm list
    1.64 -  val fix_alls : int -> Thm.thm -> Thm.thm * export
    1.65 -
    1.66 -  (* meta variables in types and terms *)
    1.67 -  val fix_tvars_to_tfrees_in_terms 
    1.68 -      : string list (* avoid these names *)
    1.69 -        -> Term.term list -> 
    1.70 -        (((string * int) * Term.sort) * (string * Term.sort)) list (* renamings *)
    1.71 -  val fix_vars_to_frees_in_terms
    1.72 -      : string list (* avoid these names *)
    1.73 -        -> Term.term list ->
    1.74 -        (((string * int) * Term.typ) * (string * Term.typ)) list (* renamings *)
    1.75 -  val fix_tvars_to_tfrees : Thm.thm -> Thm.ctyp list * Thm.thm
    1.76 -  val fix_vars_to_frees : Thm.thm -> Thm.cterm list * Thm.thm
    1.77 -  val fix_vars_and_tvars : 
    1.78 -      Thm.thm -> (Thm.cterm list * Thm.ctyp list) * Thm.thm
    1.79 -  val fix_vars_upto_idx : int -> Thm.thm -> Thm.thm
    1.80 -  val fix_tvars_upto_idx : int -> Thm.thm -> Thm.thm
    1.81 -  val unfix_frees : Thm.cterm list -> Thm.thm -> Thm.thm
    1.82 -  val unfix_tfrees : Thm.ctyp list -> Thm.thm -> Thm.thm
    1.83 -  val unfix_frees_and_tfrees :
    1.84 -      (Thm.cterm list * Thm.ctyp list) -> Thm.thm -> Thm.thm
    1.85 -
    1.86 -  (* assumptions/subgoals *)
    1.87 -  val assume_prems :
    1.88 -      int -> Thm.thm -> Thm.thm list * Thm.thm * Thm.cterm list
    1.89 -  val fixed_subgoal_thms : Thm.thm -> Thm.thm list * (Thm.thm list -> Thm.thm)
    1.90 -  val fixes_and_assumes : int -> Thm.thm -> Thm.thm list * Thm.thm * export
    1.91 -  val hide_other_goals : Thm.thm -> Thm.thm * Thm.cterm list
    1.92 -  val hide_prems : Thm.thm -> Thm.thm * Thm.cterm list
    1.93 -
    1.94 -  (* abstracts cterms (vars) to locally meta-all bounds *)
    1.95 -  val prepare_goal_export : string list * Thm.cterm list -> Thm.thm 
    1.96 -                            -> int * Thm.thm
    1.97 -  val solve_with : Thm.thm -> Thm.thm -> Thm.thm Seq.seq
    1.98 -  val subgoal_thms : Thm.thm -> Thm.thm list * (Thm.thm list -> Thm.thm)
    1.99 -end
   1.100 -
   1.101 -
   1.102 -structure IsaND 
   1.103 -: ISA_ND
   1.104 -= struct
   1.105 -
   1.106 -(* Solve *some* subgoal of "th" directly by "sol" *)
   1.107 -(* Note: this is probably what Markus ment to do upon export of a
   1.108 -"show" but maybe he used RS/rtac instead, which would wrongly lead to
   1.109 -failing if there are premices to the shown goal. 
   1.110 -
   1.111 -given: 
   1.112 -sol : Thm.thm = [| Ai... |] ==> Ci
   1.113 -th : Thm.thm = 
   1.114 -  [| ... [| Ai... |] ==> Ci ... |] ==> G
   1.115 -results in: 
   1.116 -  [| ... [| Ai-1... |] ==> Ci-1
   1.117 -    [| Ai+1... |] ==> Ci+1 ...
   1.118 -  |] ==> G
   1.119 -i.e. solves some subgoal of th that is identical to sol. 
   1.120 -*)
   1.121 -fun solve_with sol th = 
   1.122 -    let fun solvei 0 = Seq.empty
   1.123 -          | solvei i = 
   1.124 -            Seq.append (bicompose false (false,sol,0) i th) (solvei (i - 1))
   1.125 -    in
   1.126 -      solvei (Thm.nprems_of th)
   1.127 -    end;
   1.128 -
   1.129 -
   1.130 -(* Given ctertmify function, (string,type) pairs capturing the free
   1.131 -vars that need to be allified in the assumption, and a theorem with
   1.132 -assumptions possibly containing the free vars, then we give back the
   1.133 -assumptions allified as hidden hyps. 
   1.134 -
   1.135 -Given: x 
   1.136 -th: A vs ==> B vs 
   1.137 -Results in: "B vs" [!!x. A x]
   1.138 -*)
   1.139 -fun allify_conditions ctermify Ts th = 
   1.140 -    let 
   1.141 -      val premts = Thm.prems_of th;
   1.142 -    
   1.143 -      fun allify_prem_var (vt as (n,ty),t)  = 
   1.144 -          (Term.all ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
   1.145 -
   1.146 -      fun allify_prem Ts p = foldr allify_prem_var p Ts
   1.147 -
   1.148 -      val cTs = map (ctermify o Free) Ts
   1.149 -      val cterm_asms = map (ctermify o allify_prem Ts) premts
   1.150 -      val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms
   1.151 -    in 
   1.152 -      (Library.foldl (fn (x,y) => y COMP x) (th, allifyied_asm_thms), cterm_asms)
   1.153 -    end;
   1.154 -
   1.155 -fun allify_conditions' Ts th = 
   1.156 -    allify_conditions (Thm.cterm_of (Thm.theory_of_thm th)) Ts th;
   1.157 -
   1.158 -(* allify types *)
   1.159 -fun allify_typ ts ty = 
   1.160 -    let 
   1.161 -      fun trec (x as (TFree (s,srt))) = 
   1.162 -          (case Library.find_first (fn (s2,srt2) => s = s2) ts
   1.163 -            of NONE => x
   1.164 -             | SOME (s2,_) => TVar ((s,0),srt))
   1.165 -            (*  Maybe add in check here for bad sorts? 
   1.166 -             if srt = srt2 then TVar ((s,0),srt) 
   1.167 -               else raise  ("thaw_typ", ts, ty) *)
   1.168 -          | trec (Type (s,typs)) = Type (s, map trec typs)
   1.169 -          | trec (v as TVar _) = v;
   1.170 -    in trec ty end;
   1.171 -
   1.172 -(* implicit types and term *)
   1.173 -fun allify_term_typs ty = Term.map_types (allify_typ ty);
   1.174 -
   1.175 -(* allified version of term, given frees to allify over. Note that we
   1.176 -only allify over the types on the given allified cterm, we can't do
   1.177 -this for the theorem as we are not allowed type-vars in the hyp. *)
   1.178 -(* FIXME: make the allified term keep the same conclusion as it
   1.179 -started with, rather than a strictly more general version (ie use
   1.180 -instantiate with initial params we abstracted from, rather than
   1.181 -forall_elim_vars. *)
   1.182 -fun assume_allified sgn (tyvs,vs) t = 
   1.183 -    let
   1.184 -      fun allify_var (vt as (n,ty),t)  = 
   1.185 -          (Term.all ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
   1.186 -      fun allify Ts p = List.foldr allify_var p Ts
   1.187 -
   1.188 -      val ctermify = Thm.cterm_of sgn;
   1.189 -      val cvars = map (fn (n,ty) => ctermify (Var ((n,0),ty))) vs
   1.190 -      val allified_term = t |> allify vs;
   1.191 -      val ct = ctermify allified_term;
   1.192 -      val typ_allified_ct = ctermify (allify_term_typs tyvs allified_term);
   1.193 -    in (typ_allified_ct, 
   1.194 -        Drule.forall_elim_vars 0 (Thm.assume ct)) end;
   1.195 -
   1.196 -
   1.197 -(* change type-vars to fresh type frees *)
   1.198 -fun fix_tvars_to_tfrees_in_terms names ts = 
   1.199 -    let 
   1.200 -      val tfree_names = map fst (List.foldr Term.add_term_tfrees [] ts);
   1.201 -      val tvars = List.foldr Term.add_term_tvars [] ts;
   1.202 -      val (names',renamings) = 
   1.203 -          List.foldr (fn (tv as ((n,i),s),(Ns,Rs)) => 
   1.204 -                         let val n2 = Name.variant Ns n in 
   1.205 -                           (n2::Ns, (tv, (n2,s))::Rs)
   1.206 -                         end) (tfree_names @ names,[]) tvars;
   1.207 -    in renamings end;
   1.208 -fun fix_tvars_to_tfrees th = 
   1.209 -    let 
   1.210 -      val sign = Thm.theory_of_thm th;
   1.211 -      val ctypify = Thm.ctyp_of sign;
   1.212 -      val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
   1.213 -      val renamings = fix_tvars_to_tfrees_in_terms 
   1.214 -                        [] ((Thm.prop_of th) :: tpairs);
   1.215 -      val crenamings = 
   1.216 -          map (fn (v,f) => (ctypify (TVar v), ctypify (TFree f)))
   1.217 -              renamings;
   1.218 -      val fixedfrees = map snd crenamings;
   1.219 -    in (fixedfrees, Thm.instantiate (crenamings, []) th) end;
   1.220 -
   1.221 -
   1.222 -(* change type-free's to type-vars in th, skipping the ones in "ns" *)
   1.223 -fun unfix_tfrees ns th = 
   1.224 -    let 
   1.225 -      val varfiytfrees = map (Term.dest_TFree o Thm.typ_of) ns
   1.226 -      val skiptfrees = subtract (op =) varfiytfrees (Term.add_term_tfrees (Thm.prop_of th,[]));
   1.227 -    in #2 (Thm.varifyT' skiptfrees th) end;
   1.228 -
   1.229 -(* change schematic/meta vars to fresh free vars, avoiding name clashes 
   1.230 -   with "names" *)
   1.231 -fun fix_vars_to_frees_in_terms names ts = 
   1.232 -    let 
   1.233 -      val vars = map Term.dest_Var (List.foldr Term.add_term_vars [] ts);
   1.234 -      val Ns = List.foldr Term.add_term_names names ts;
   1.235 -      val (_,renamings) = 
   1.236 -          Library.foldl (fn ((Ns,Rs),v as ((n,i),ty)) => 
   1.237 -                    let val n2 = Name.variant Ns n in
   1.238 -                      (n2 :: Ns, (v, (n2,ty)) :: Rs)
   1.239 -                    end) ((Ns,[]), vars);
   1.240 -    in renamings end;
   1.241 -fun fix_vars_to_frees th = 
   1.242 -    let 
   1.243 -      val ctermify = Thm.cterm_of (Thm.theory_of_thm th)
   1.244 -      val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
   1.245 -      val renamings = fix_vars_to_frees_in_terms 
   1.246 -                        [] ([Thm.prop_of th] @ tpairs);
   1.247 -      val crenamings = 
   1.248 -          map (fn (v,f) => (ctermify (Var v), ctermify (Free f)))
   1.249 -              renamings;
   1.250 -      val fixedfrees = map snd crenamings;
   1.251 -    in (fixedfrees, Thm.instantiate ([], crenamings) th) end;
   1.252 -
   1.253 -fun fix_tvars_upto_idx ix th = 
   1.254 -    let 
   1.255 -      val sgn = Thm.theory_of_thm th;
   1.256 -      val ctypify = Thm.ctyp_of sgn
   1.257 -      val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
   1.258 -      val prop = (Thm.prop_of th);
   1.259 -      val tvars = List.foldr Term.add_term_tvars [] (prop :: tpairs);
   1.260 -      val ctyfixes = 
   1.261 -          map_filter 
   1.262 -            (fn (v as ((s,i),ty)) => 
   1.263 -                if i <= ix then SOME (ctypify (TVar v), ctypify (TFree (s,ty)))
   1.264 -                else NONE) tvars;
   1.265 -    in Thm.instantiate (ctyfixes, []) th end;
   1.266 -fun fix_vars_upto_idx ix th = 
   1.267 -    let 
   1.268 -      val sgn = Thm.theory_of_thm th;
   1.269 -      val ctermify = Thm.cterm_of sgn
   1.270 -      val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
   1.271 -      val prop = (Thm.prop_of th);
   1.272 -      val vars = map Term.dest_Var (List.foldr Term.add_term_vars 
   1.273 -                                               [] (prop :: tpairs));
   1.274 -      val cfixes = 
   1.275 -          map_filter 
   1.276 -            (fn (v as ((s,i),ty)) => 
   1.277 -                if i <= ix then SOME (ctermify (Var v), ctermify (Free (s,ty)))
   1.278 -                else NONE) vars;
   1.279 -    in Thm.instantiate ([], cfixes) th end;
   1.280 -
   1.281 -
   1.282 -(* make free vars into schematic vars with index zero *)
   1.283 - fun unfix_frees frees = 
   1.284 -     apply (map (K (Drule.forall_elim_var 0)) frees) 
   1.285 -     o Drule.forall_intr_list frees;
   1.286 -
   1.287 -(* fix term and type variables *)
   1.288 -fun fix_vars_and_tvars th = 
   1.289 -    let val (tvars, th') = fix_tvars_to_tfrees th
   1.290 -      val (vars, th'') = fix_vars_to_frees th' 
   1.291 -    in ((vars, tvars), th'') end;
   1.292 -
   1.293 -(* implicit Thm.thm argument *)
   1.294 -(* assumes: vars may contain fixed versions of the frees *)
   1.295 -(* THINK: what if vs already has types varified? *)
   1.296 -fun unfix_frees_and_tfrees (vs,tvs) = 
   1.297 -    (unfix_tfrees tvs o unfix_frees vs);
   1.298 -
   1.299 -(* datatype to capture an exported result, ie a fix or assume. *)
   1.300 -datatype export = 
   1.301 -         export of {fixes : Thm.cterm list, (* fixed vars *)
   1.302 -                    assumes : Thm.cterm list, (* hidden hyps/assumed prems *)
   1.303 -                    sgid : int,
   1.304 -                    gth :  Thm.thm}; (* subgoal/goalthm *)
   1.305 -
   1.306 -fun fixes_of_exp (export rep) = #fixes rep;
   1.307 -
   1.308 -(* export the result of the new goal thm, ie if we reduced teh
   1.309 -subgoal, then we get a new reduced subtgoal with the old
   1.310 -all-quantified variables *)
   1.311 -local 
   1.312 -
   1.313 -(* allify puts in a meta level univ quantifier for a free variavble *)
   1.314 -fun allify_term (v, t) = 
   1.315 -    let val vt = #t (Thm.rep_cterm v)
   1.316 -      val (n,ty) = Term.dest_Free vt
   1.317 -    in (Term.all ty) $ (Abs(n,ty,Term.abstract_over (vt, t))) end;
   1.318 -
   1.319 -fun allify_for_sg_term ctermify vs t =
   1.320 -    let val t_alls = foldr allify_term t vs;
   1.321 -        val ct_alls = ctermify t_alls; 
   1.322 -    in 
   1.323 -      (ct_alls, Drule.forall_elim_list vs (Thm.assume ct_alls))
   1.324 -    end;
   1.325 -(* lookup type of a free var name from a list *)
   1.326 -fun lookupfree vs vn  = 
   1.327 -    case Library.find_first (fn (n,ty) => n = vn) vs of 
   1.328 -      NONE => error ("prepare_goal_export:lookupfree: " ^ vn ^ " does not occur in the term")
   1.329 -    | SOME x => x;
   1.330 -in
   1.331 -fun export_back (export {fixes = vs, assumes = hprems, 
   1.332 -                         sgid = i, gth = gth}) newth = 
   1.333 -    let 
   1.334 -      val sgn = Thm.theory_of_thm newth;
   1.335 -      val ctermify = Thm.cterm_of sgn;
   1.336 -
   1.337 -      val sgs = prems_of newth;
   1.338 -      val (sgallcts, sgthms) = 
   1.339 -          Library.split_list (map (allify_for_sg_term ctermify vs) sgs);
   1.340 -      val minimal_newth = 
   1.341 -          (Library.foldl (fn ( newth', sgthm) => 
   1.342 -                          Drule.compose_single (sgthm, 1, newth'))
   1.343 -                      (newth, sgthms));
   1.344 -      val allified_newth = 
   1.345 -          minimal_newth 
   1.346 -            |> Drule.implies_intr_list hprems
   1.347 -            |> Drule.forall_intr_list vs 
   1.348 -
   1.349 -      val newth' = Drule.implies_intr_list sgallcts allified_newth
   1.350 -    in
   1.351 -      bicompose false (false, newth', (length sgallcts)) i gth
   1.352 -    end;
   1.353 -
   1.354 -(* 
   1.355 -Given "vs" : names of free variables to abstract over,
   1.356 -Given cterms : premices to abstract over (P1... Pn) in terms of vs,
   1.357 -Given a thm of the form: 
   1.358 -P1 vs; ...; Pn vs ==> Goal(C vs)
   1.359 -
   1.360 -Gives back: 
   1.361 -(n, length of given cterms which have been allified
   1.362 - [| !! vs. P1 vs; !! vs. Pn vs |] ==> !! C vs) the allified thm
   1.363 -*)
   1.364 -(* note: C may contain further premices etc 
   1.365 -Note that cterms is the assumed facts, ie prems of "P1" that are
   1.366 -reintroduced in allified form.
   1.367 -*)
   1.368 -fun prepare_goal_export (vs, cterms) th = 
   1.369 -    let 
   1.370 -      val sgn = Thm.theory_of_thm th;
   1.371 -      val ctermify = Thm.cterm_of sgn;
   1.372 -
   1.373 -      val allfrees = map Term.dest_Free (Term.term_frees (Thm.prop_of th))
   1.374 -      val cfrees = map (ctermify o Free o lookupfree allfrees) vs
   1.375 -
   1.376 -      val sgs = prems_of th;
   1.377 -      val (sgallcts, sgthms) = 
   1.378 -          Library.split_list (map (allify_for_sg_term ctermify cfrees) sgs);
   1.379 -
   1.380 -      val minimal_th = 
   1.381 -          Goal.conclude (Library.foldl (fn ( th', sgthm) => 
   1.382 -                          Drule.compose_single (sgthm, 1, th'))
   1.383 -                      (th, sgthms));
   1.384 -
   1.385 -      val allified_th = 
   1.386 -          minimal_th 
   1.387 -            |> Drule.implies_intr_list cterms
   1.388 -            |> Drule.forall_intr_list cfrees 
   1.389 -
   1.390 -      val th' = Drule.implies_intr_list sgallcts allified_th
   1.391 -    in
   1.392 -      ((length sgallcts), th')
   1.393 -    end;
   1.394 -
   1.395 -end;
   1.396 -
   1.397 -
   1.398 -(* exporting function that takes a solution to the fixed/assumed goal,
   1.399 -and uses this to solve the subgoal in the main theorem *)
   1.400 -fun export_solution (export {fixes = cfvs, assumes = hcprems,
   1.401 -                             sgid = i, gth = gth}) solth = 
   1.402 -    let 
   1.403 -      val solth' = 
   1.404 -          solth |> Drule.implies_intr_list hcprems
   1.405 -                |> Drule.forall_intr_list cfvs
   1.406 -    in Drule.compose_single (solth', i, gth) end;
   1.407 -
   1.408 -fun export_solutions (xs,th) = foldr (uncurry export_solution) th xs;
   1.409 -
   1.410 -
   1.411 -(* fix parameters of a subgoal "i", as free variables, and create an
   1.412 -exporting function that will use the result of this proved goal to
   1.413 -show the goal in the original theorem. 
   1.414 -
   1.415 -Note, an advantage of this over Isar is that it supports instantiation
   1.416 -of unkowns in the earlier theorem, ie we can do instantiation of meta
   1.417 -vars! 
   1.418 -
   1.419 -avoids constant, free and vars names. 
   1.420 -
   1.421 -loosely corresponds to:
   1.422 -Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm
   1.423 -Result: 
   1.424 -  ("(As ==> SGi x') ==> (As ==> SGi x')" : thm, 
   1.425 -   expf : 
   1.426 -     ("As ==> SGi x'" : thm) -> 
   1.427 -     ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm)
   1.428 -*)
   1.429 -fun fix_alls_in_term alledt = 
   1.430 -    let
   1.431 -      val t = Term.strip_all_body alledt;
   1.432 -      val alls = rev (Term.strip_all_vars alledt);
   1.433 -      val varnames = map (fst o fst o Term.dest_Var) (Term.term_vars t)
   1.434 -      val names = Term.add_term_names (t,varnames);
   1.435 -      val fvs = map Free 
   1.436 -                    (Name.variant_list names (map fst alls)
   1.437 -                       ~~ (map snd alls));
   1.438 -    in ((subst_bounds (fvs,t)), fvs) end;
   1.439 -
   1.440 -fun fix_alls_term i t = 
   1.441 -    let 
   1.442 -      val varnames = map (fst o fst o Term.dest_Var) (Term.term_vars t)
   1.443 -      val names = Term.add_term_names (t,varnames);
   1.444 -      val gt = Logic.get_goal t i;
   1.445 -      val body = Term.strip_all_body gt;
   1.446 -      val alls = rev (Term.strip_all_vars gt);
   1.447 -      val fvs = map Free 
   1.448 -                    (Name.variant_list names (map fst alls)
   1.449 -                       ~~ (map snd alls));
   1.450 -    in ((subst_bounds (fvs,body)), fvs) end;
   1.451 -
   1.452 -fun fix_alls_cterm i th = 
   1.453 -    let
   1.454 -      val ctermify = Thm.cterm_of (Thm.theory_of_thm th);
   1.455 -      val (fixedbody, fvs) = fix_alls_term i (Thm.prop_of th);
   1.456 -      val cfvs = rev (map ctermify fvs);
   1.457 -      val ct_body = ctermify fixedbody
   1.458 -    in
   1.459 -      (ct_body, cfvs)
   1.460 -    end;
   1.461 -
   1.462 -fun fix_alls' i = 
   1.463 -     (apfst Thm.trivial) o (fix_alls_cterm i);
   1.464 -
   1.465 -
   1.466 -(* hide other goals *) 
   1.467 -(* note the export goal is rotated by (i - 1) and will have to be
   1.468 -unrotated to get backto the originial position(s) *)
   1.469 -fun hide_other_goals th = 
   1.470 -    let
   1.471 -      (* tl beacuse fst sg is the goal we are interested in *)
   1.472 -      val cprems = tl (Drule.cprems_of th)
   1.473 -      val aprems = map Thm.assume cprems
   1.474 -    in
   1.475 -      (Drule.implies_elim_list (Drule.rotate_prems 1 th) aprems, 
   1.476 -       cprems)
   1.477 -    end;
   1.478 -
   1.479 -(* a nicer version of the above that leaves only a single subgoal (the
   1.480 -other subgoals are hidden hyps, that the exporter suffles about)
   1.481 -namely the subgoal that we were trying to solve. *)
   1.482 -(* loosely corresponds to:
   1.483 -Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm
   1.484 -Result: 
   1.485 -  ("(As ==> SGi x') ==> SGi x'" : thm, 
   1.486 -   expf : 
   1.487 -     ("SGi x'" : thm) -> 
   1.488 -     ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm)
   1.489 -*)
   1.490 -fun fix_alls i th = 
   1.491 -    let 
   1.492 -      val (fixed_gth, fixedvars) = fix_alls' i th
   1.493 -      val (sml_gth, othergoals) = hide_other_goals fixed_gth
   1.494 -    in
   1.495 -      (sml_gth, export {fixes = fixedvars, 
   1.496 -                        assumes = othergoals, 
   1.497 -                        sgid = i, gth = th})
   1.498 -    end;
   1.499 -
   1.500 -
   1.501 -(* assume the premises of subgoal "i", this gives back a list of
   1.502 -assumed theorems that are the premices of subgoal i, it also gives
   1.503 -back a new goal thm and an exporter, the new goalthm is as the old
   1.504 -one, but without the premices, and the exporter will use a proof of
   1.505 -the new goalthm, possibly using the assumed premices, to shoe the
   1.506 -orginial goal.
   1.507 -
   1.508 -Note: Dealing with meta vars, need to meta-level-all them in the
   1.509 -shyps, which we can later instantiate with a specific value.... ? 
   1.510 -think about this... maybe need to introduce some new fixed vars and
   1.511 -then remove them again at the end... like I do with rw_inst. 
   1.512 -
   1.513 -loosely corresponds to:
   1.514 -Given "[| SG0; ... [| A0; ... An |] ==> SGi; ... SGm |] ==> G" : thm
   1.515 -Result: 
   1.516 -(["A0" [A0], ... ,"An" [An]] : thm list, -- assumptions
   1.517 - "SGi ==> SGi" : thm, -- new goal 
   1.518 - "SGi" ["A0" ... "An"] : thm ->   -- export function
   1.519 -    ("[| SG0 ... SGi-1, SGi+1, SGm |] ==> G" : thm) list)
   1.520 -*)
   1.521 -fun assume_prems i th =
   1.522 -    let 
   1.523 -      val t = (prop_of th); 
   1.524 -      val gt = Logic.get_goal t i;
   1.525 -      val _ = case Term.strip_all_vars gt of [] => () 
   1.526 -              | _ => error "assume_prems: goal has params"
   1.527 -      val body = gt;
   1.528 -      val prems = Logic.strip_imp_prems body;
   1.529 -      val concl = Logic.strip_imp_concl body;
   1.530 -
   1.531 -      val sgn = Thm.theory_of_thm th;
   1.532 -      val ctermify = Thm.cterm_of sgn;
   1.533 -      val cprems = map ctermify prems;
   1.534 -      val aprems = map Thm.assume cprems;
   1.535 -      val gthi = Thm.trivial (ctermify concl);
   1.536 -
   1.537 -      (* fun explortf thi = 
   1.538 -          Drule.compose (Drule.implies_intr_list cprems thi, 
   1.539 -                         i, th) *)
   1.540 -    in
   1.541 -      (aprems, gthi, cprems)
   1.542 -    end;
   1.543 -
   1.544 -
   1.545 -(* first fix the variables, then assume the assumptions *)
   1.546 -(* loosely corresponds to:
   1.547 -Given 
   1.548 -  "[| SG0; ... 
   1.549 -      !! xs. [| A0 xs; ... An xs |] ==> SGi xs; 
   1.550 -      ... SGm |] ==> G" : thm
   1.551 -Result: 
   1.552 -(["A0 xs'" [A0 xs'], ... ,"An xs'" [An xs']] : thm list, -- assumptions
   1.553 - "SGi xs' ==> SGi xs'" : thm,  -- new goal 
   1.554 - "SGi xs'" ["A0 xs'" ... "An xs'"] : thm ->   -- export function
   1.555 -    ("[| SG0 ... SGi-1, SGi+1, SGm |] ==> G" : thm) list)
   1.556 -*)
   1.557 -
   1.558 -(* Note: the fix_alls actually pulls through all the assumptions which
   1.559 -means that the second export is not needed. *)
   1.560 -fun fixes_and_assumes i th = 
   1.561 -    let 
   1.562 -      val (fixgth, exp1) = fix_alls i th
   1.563 -      val (assumps, goalth, _) = assume_prems 1 fixgth
   1.564 -    in 
   1.565 -      (assumps, goalth, exp1)
   1.566 -    end;
   1.567 -
   1.568 -
   1.569 -(* Fixme: allow different order of subgoals given to expf *)
   1.570 -(* make each subgoal into a separate thm that needs to be proved *)
   1.571 -(* loosely corresponds to:
   1.572 -Given 
   1.573 -  "[| SG0; ... SGm |] ==> G" : thm
   1.574 -Result: 
   1.575 -(["SG0 ==> SG0", ... ,"SGm ==> SGm"] : thm list, -- goals
   1.576 - ["SG0", ..., "SGm"] : thm list ->   -- export function
   1.577 -   "G" : thm)
   1.578 -*)
   1.579 -fun subgoal_thms th = 
   1.580 -    let 
   1.581 -      val t = (prop_of th); 
   1.582 -
   1.583 -      val prems = Logic.strip_imp_prems t;
   1.584 -
   1.585 -      val sgn = Thm.theory_of_thm th;
   1.586 -      val ctermify = Thm.cterm_of sgn;
   1.587 -
   1.588 -      val aprems = map (Thm.trivial o ctermify) prems;
   1.589 -
   1.590 -      fun explortf premths = 
   1.591 -          Drule.implies_elim_list th premths
   1.592 -    in
   1.593 -      (aprems, explortf)
   1.594 -    end;
   1.595 -
   1.596 -
   1.597 -(* make all the premices of a theorem hidden, and provide an unhide
   1.598 -function, that will bring them back out at a later point. This is
   1.599 -useful if you want to get back these premices, after having used the
   1.600 -theorem with the premices hidden *)
   1.601 -(* loosely corresponds to:
   1.602 -Given "As ==> G" : thm
   1.603 -Result: ("G [As]" : thm, 
   1.604 -         "G [As]" : thm -> "As ==> G" : thm
   1.605 -*)
   1.606 -fun hide_prems th = 
   1.607 -    let 
   1.608 -      val cprems = Drule.cprems_of th;
   1.609 -      val aprems = map Thm.assume cprems;
   1.610 -    (*   val unhidef = Drule.implies_intr_list cprems; *)
   1.611 -    in
   1.612 -      (Drule.implies_elim_list th aprems, cprems)
   1.613 -    end;
   1.614 -
   1.615 -
   1.616 -
   1.617 -
   1.618 -(* Fixme: allow different order of subgoals in exportf *)
   1.619 -(* as above, but also fix all parameters in all subgoals, and uses
   1.620 -fix_alls, not fix_alls', ie doesn't leave extra asumptions as apparent
   1.621 -subgoals. *)
   1.622 -(* loosely corresponds to:
   1.623 -Given 
   1.624 -  "[| !! x0s. A0s x0s ==> SG0 x0s; 
   1.625 -      ...; !! xms. Ams xms ==> SGm xms|] ==> G" : thm
   1.626 -Result: 
   1.627 -(["(A0s x0s' ==> SG0 x0s') ==> SG0 x0s'", 
   1.628 -  ... ,"(Ams xms' ==> SGm xms') ==> SGm xms'"] : thm list, -- goals
   1.629 - ["SG0 x0s'", ..., "SGm xms'"] : thm list ->   -- export function
   1.630 -   "G" : thm)
   1.631 -*)
   1.632 -(* requires being given solutions! *)
   1.633 -fun fixed_subgoal_thms th = 
   1.634 -    let 
   1.635 -      val (subgoals, expf) = subgoal_thms th;
   1.636 -(*       fun export_sg (th, exp) = exp th; *)
   1.637 -      fun export_sgs expfs solthms = 
   1.638 -          expf (map2 (curry (op |>)) solthms expfs);
   1.639 -(*           expf (map export_sg (ths ~~ expfs)); *)
   1.640 -    in 
   1.641 -      apsnd export_sgs (Library.split_list (map (apsnd export_solution o 
   1.642 -                                                 fix_alls 1) subgoals))
   1.643 -    end;
   1.644 -
   1.645 -end;