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