src/Tools/IsaPlanner/isand.ML
changeset 23171 861f63a35d31
child 23175 267ba70e7a9d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/IsaPlanner/isand.ML	Thu May 31 20:55:29 2007 +0200
     1.3 @@ -0,0 +1,642 @@
     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;