src/Tools/IsaPlanner/isand.ML
author wenzelm
Sat Oct 06 16:50:04 2007 +0200 (2007-10-06)
changeset 24867 e5b55d7be9bb
parent 23175 267ba70e7a9d
child 26653 60e0cf6bef89
permissions -rw-r--r--
simplified interfaces for outer syntax;
     1 (*  Title:      Tools/IsaPlanner/isand.ML
     2     ID:		$Id$
     3     Author:     Lucas Dixon, University of Edinburgh
     4 
     5 Natural Deduction tools.
     6 
     7 For working with Isabelle theorems in a natural detuction style.
     8 ie, not having to deal with meta level quantified varaibles,
     9 instead, we work with newly introduced frees, and hide the
    10 "all"'s, exporting results from theorems proved with the frees, to
    11 solve the all cases of the previous goal. This allows resolution
    12 to do proof search normally. 
    13 
    14 Note: A nice idea: allow exporting to solve any subgoal, thus
    15 allowing the interleaving of proof, or provide a structure for the
    16 ordering of proof, thus allowing proof attempts in parrell, but
    17 recording the order to apply things in.
    18 
    19 THINK: are we really ok with our varify name w.r.t the prop - do
    20 we also need to avoid names in the hidden hyps? What about
    21 unification contraints in flex-flex pairs - might they also have
    22 extra free vars?
    23 *)
    24 
    25 signature ISA_ND =
    26 sig
    27 
    28   (* export data *)
    29   datatype export = export of
    30            {gth: Thm.thm, (* initial goal theorem *)
    31             sgid: int, (* subgoal id which has been fixed etc *)
    32             fixes: Thm.cterm list, (* frees *)
    33             assumes: Thm.cterm list} (* assumptions *)
    34   val fixes_of_exp : export -> Thm.cterm list
    35   val export_back : export -> Thm.thm -> Thm.thm Seq.seq
    36   val export_solution : export -> Thm.thm -> Thm.thm
    37   val export_solutions : export list * Thm.thm -> Thm.thm
    38 
    39   (* inserting meta level params for frees in the conditions *)
    40   val allify_conditions :
    41       (Term.term -> Thm.cterm) ->
    42       (string * Term.typ) list -> Thm.thm -> Thm.thm * Thm.cterm list
    43   val allify_conditions' :
    44       (string * Term.typ) list -> Thm.thm -> Thm.thm * Thm.cterm list
    45   val assume_allified :
    46       theory -> (string * Term.sort) list * (string * Term.typ) list
    47       -> Term.term -> (Thm.cterm * Thm.thm)
    48 
    49   (* meta level fixed params (i.e. !! vars) *)
    50   val fix_alls_in_term : Term.term -> Term.term * Term.term list
    51   val fix_alls_term : int -> Term.term -> Term.term * Term.term list
    52   val fix_alls_cterm : int -> Thm.thm -> Thm.cterm * Thm.cterm list
    53   val fix_alls' : int -> Thm.thm -> Thm.thm * Thm.cterm list
    54   val fix_alls : int -> Thm.thm -> Thm.thm * export
    55 
    56   (* meta variables in types and terms *)
    57   val fix_tvars_to_tfrees_in_terms 
    58       : string list (* avoid these names *)
    59         -> Term.term list -> 
    60         (((string * int) * Term.sort) * (string * Term.sort)) list (* renamings *)
    61   val fix_vars_to_frees_in_terms
    62       : string list (* avoid these names *)
    63         -> Term.term list ->
    64         (((string * int) * Term.typ) * (string * Term.typ)) list (* renamings *)
    65   val fix_tvars_to_tfrees : Thm.thm -> Thm.ctyp list * Thm.thm
    66   val fix_vars_to_frees : Thm.thm -> Thm.cterm list * Thm.thm
    67   val fix_vars_and_tvars : 
    68       Thm.thm -> (Thm.cterm list * Thm.ctyp list) * Thm.thm
    69   val fix_vars_upto_idx : int -> Thm.thm -> Thm.thm
    70   val fix_tvars_upto_idx : int -> Thm.thm -> Thm.thm
    71   val unfix_frees : Thm.cterm list -> Thm.thm -> Thm.thm
    72   val unfix_tfrees : Thm.ctyp list -> Thm.thm -> Thm.thm
    73   val unfix_frees_and_tfrees :
    74       (Thm.cterm list * Thm.ctyp list) -> Thm.thm -> Thm.thm
    75 
    76   (* assumptions/subgoals *)
    77   val assume_prems :
    78       int -> Thm.thm -> Thm.thm list * Thm.thm * Thm.cterm list
    79   val fixed_subgoal_thms : Thm.thm -> Thm.thm list * (Thm.thm list -> Thm.thm)
    80   val fixes_and_assumes : int -> Thm.thm -> Thm.thm list * Thm.thm * export
    81   val hide_other_goals : Thm.thm -> Thm.thm * Thm.cterm list
    82   val hide_prems : Thm.thm -> Thm.thm * Thm.cterm list
    83 
    84   (* abstracts cterms (vars) to locally meta-all bounds *)
    85   val prepare_goal_export : string list * Thm.cterm list -> Thm.thm 
    86                             -> int * Thm.thm
    87   val solve_with : Thm.thm -> Thm.thm -> Thm.thm Seq.seq
    88   val subgoal_thms : Thm.thm -> Thm.thm list * (Thm.thm list -> Thm.thm)
    89 end
    90 
    91 
    92 structure IsaND 
    93 : ISA_ND
    94 = struct
    95 
    96 (* Solve *some* subgoal of "th" directly by "sol" *)
    97 (* Note: this is probably what Markus ment to do upon export of a
    98 "show" but maybe he used RS/rtac instead, which would wrongly lead to
    99 failing if there are premices to the shown goal. 
   100 
   101 given: 
   102 sol : Thm.thm = [| Ai... |] ==> Ci
   103 th : Thm.thm = 
   104   [| ... [| Ai... |] ==> Ci ... |] ==> G
   105 results in: 
   106   [| ... [| Ai-1... |] ==> Ci-1
   107     [| Ai+1... |] ==> Ci+1 ...
   108   |] ==> G
   109 i.e. solves some subgoal of th that is identical to sol. 
   110 *)
   111 fun solve_with sol th = 
   112     let fun solvei 0 = Seq.empty
   113           | solvei i = 
   114             Seq.append (bicompose false (false,sol,0) i th) (solvei (i - 1))
   115     in
   116       solvei (Thm.nprems_of th)
   117     end;
   118 
   119 
   120 (* Given ctertmify function, (string,type) pairs capturing the free
   121 vars that need to be allified in the assumption, and a theorem with
   122 assumptions possibly containing the free vars, then we give back the
   123 assumptions allified as hidden hyps. 
   124 
   125 Given: x 
   126 th: A vs ==> B vs 
   127 Results in: "B vs" [!!x. A x]
   128 *)
   129 fun allify_conditions ctermify Ts th = 
   130     let 
   131       val premts = Thm.prems_of th;
   132     
   133       fun allify_prem_var (vt as (n,ty),t)  = 
   134           (Term.all ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
   135 
   136       fun allify_prem Ts p = foldr allify_prem_var p Ts
   137 
   138       val cTs = map (ctermify o Free) Ts
   139       val cterm_asms = map (ctermify o allify_prem Ts) premts
   140       val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms
   141     in 
   142       (Library.foldl (fn (x,y) => y COMP x) (th, allifyied_asm_thms), cterm_asms)
   143     end;
   144 
   145 fun allify_conditions' Ts th = 
   146     allify_conditions (Thm.cterm_of (Thm.theory_of_thm th)) Ts th;
   147 
   148 (* allify types *)
   149 fun allify_typ ts ty = 
   150     let 
   151       fun trec (x as (TFree (s,srt))) = 
   152           (case Library.find_first (fn (s2,srt2) => s = s2) ts
   153             of NONE => x
   154              | SOME (s2,_) => TVar ((s,0),srt))
   155             (*  Maybe add in check here for bad sorts? 
   156              if srt = srt2 then TVar ((s,0),srt) 
   157                else raise  ("thaw_typ", ts, ty) *)
   158           | trec (Type (s,typs)) = Type (s, map trec typs)
   159           | trec (v as TVar _) = v;
   160     in trec ty end;
   161 
   162 (* implicit types and term *)
   163 fun allify_term_typs ty = Term.map_types (allify_typ ty);
   164 
   165 (* allified version of term, given frees to allify over. Note that we
   166 only allify over the types on the given allified cterm, we can't do
   167 this for the theorem as we are not allowed type-vars in the hyp. *)
   168 (* FIXME: make the allified term keep the same conclusion as it
   169 started with, rather than a strictly more general version (ie use
   170 instantiate with initial params we abstracted from, rather than
   171 forall_elim_vars. *)
   172 fun assume_allified sgn (tyvs,vs) t = 
   173     let
   174       fun allify_var (vt as (n,ty),t)  = 
   175           (Term.all ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
   176       fun allify Ts p = List.foldr allify_var p Ts
   177 
   178       val ctermify = Thm.cterm_of sgn;
   179       val cvars = map (fn (n,ty) => ctermify (Var ((n,0),ty))) vs
   180       val allified_term = t |> allify vs;
   181       val ct = ctermify allified_term;
   182       val typ_allified_ct = ctermify (allify_term_typs tyvs allified_term);
   183     in (typ_allified_ct, 
   184         Drule.forall_elim_vars 0 (Thm.assume ct)) end;
   185 
   186 
   187 (* change type-vars to fresh type frees *)
   188 fun fix_tvars_to_tfrees_in_terms names ts = 
   189     let 
   190       val tfree_names = map fst (List.foldr Term.add_term_tfrees [] ts);
   191       val tvars = List.foldr Term.add_term_tvars [] ts;
   192       val (names',renamings) = 
   193           List.foldr (fn (tv as ((n,i),s),(Ns,Rs)) => 
   194                          let val n2 = Name.variant Ns n in 
   195                            (n2::Ns, (tv, (n2,s))::Rs)
   196                          end) (tfree_names @ names,[]) tvars;
   197     in renamings end;
   198 fun fix_tvars_to_tfrees th = 
   199     let 
   200       val sign = Thm.theory_of_thm th;
   201       val ctypify = Thm.ctyp_of sign;
   202       val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
   203       val renamings = fix_tvars_to_tfrees_in_terms 
   204                         [] ((Thm.prop_of th) :: tpairs);
   205       val crenamings = 
   206           map (fn (v,f) => (ctypify (TVar v), ctypify (TFree f)))
   207               renamings;
   208       val fixedfrees = map snd crenamings;
   209     in (fixedfrees, Thm.instantiate (crenamings, []) th) end;
   210 
   211 
   212 (* change type-free's to type-vars in th, skipping the ones in "ns" *)
   213 fun unfix_tfrees ns th = 
   214     let 
   215       val varfiytfrees = map (Term.dest_TFree o Thm.typ_of) ns
   216       val skiptfrees = subtract (op =) varfiytfrees (Term.add_term_tfrees (Thm.prop_of th,[]));
   217     in #2 (Thm.varifyT' skiptfrees th) end;
   218 
   219 (* change schematic/meta vars to fresh free vars, avoiding name clashes 
   220    with "names" *)
   221 fun fix_vars_to_frees_in_terms names ts = 
   222     let 
   223       val vars = map Term.dest_Var (List.foldr Term.add_term_vars [] ts);
   224       val Ns = List.foldr Term.add_term_names names ts;
   225       val (_,renamings) = 
   226           Library.foldl (fn ((Ns,Rs),v as ((n,i),ty)) => 
   227                     let val n2 = Name.variant Ns n in
   228                       (n2 :: Ns, (v, (n2,ty)) :: Rs)
   229                     end) ((Ns,[]), vars);
   230     in renamings end;
   231 fun fix_vars_to_frees th = 
   232     let 
   233       val ctermify = Thm.cterm_of (Thm.theory_of_thm th)
   234       val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
   235       val renamings = fix_vars_to_frees_in_terms 
   236                         [] ([Thm.prop_of th] @ tpairs);
   237       val crenamings = 
   238           map (fn (v,f) => (ctermify (Var v), ctermify (Free f)))
   239               renamings;
   240       val fixedfrees = map snd crenamings;
   241     in (fixedfrees, Thm.instantiate ([], crenamings) th) end;
   242 
   243 fun fix_tvars_upto_idx ix th = 
   244     let 
   245       val sgn = Thm.theory_of_thm th;
   246       val ctypify = Thm.ctyp_of sgn
   247       val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
   248       val prop = (Thm.prop_of th);
   249       val tvars = List.foldr Term.add_term_tvars [] (prop :: tpairs);
   250       val ctyfixes = 
   251           map_filter 
   252             (fn (v as ((s,i),ty)) => 
   253                 if i <= ix then SOME (ctypify (TVar v), ctypify (TFree (s,ty)))
   254                 else NONE) tvars;
   255     in Thm.instantiate (ctyfixes, []) th end;
   256 fun fix_vars_upto_idx ix th = 
   257     let 
   258       val sgn = Thm.theory_of_thm th;
   259       val ctermify = Thm.cterm_of sgn
   260       val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
   261       val prop = (Thm.prop_of th);
   262       val vars = map Term.dest_Var (List.foldr Term.add_term_vars 
   263                                                [] (prop :: tpairs));
   264       val cfixes = 
   265           map_filter 
   266             (fn (v as ((s,i),ty)) => 
   267                 if i <= ix then SOME (ctermify (Var v), ctermify (Free (s,ty)))
   268                 else NONE) vars;
   269     in Thm.instantiate ([], cfixes) th end;
   270 
   271 
   272 (* make free vars into schematic vars with index zero *)
   273  fun unfix_frees frees = 
   274      apply (map (K (Drule.forall_elim_var 0)) frees) 
   275      o Drule.forall_intr_list frees;
   276 
   277 (* fix term and type variables *)
   278 fun fix_vars_and_tvars th = 
   279     let val (tvars, th') = fix_tvars_to_tfrees th
   280       val (vars, th'') = fix_vars_to_frees th' 
   281     in ((vars, tvars), th'') end;
   282 
   283 (* implicit Thm.thm argument *)
   284 (* assumes: vars may contain fixed versions of the frees *)
   285 (* THINK: what if vs already has types varified? *)
   286 fun unfix_frees_and_tfrees (vs,tvs) = 
   287     (unfix_tfrees tvs o unfix_frees vs);
   288 
   289 (* datatype to capture an exported result, ie a fix or assume. *)
   290 datatype export = 
   291          export of {fixes : Thm.cterm list, (* fixed vars *)
   292                     assumes : Thm.cterm list, (* hidden hyps/assumed prems *)
   293                     sgid : int,
   294                     gth :  Thm.thm}; (* subgoal/goalthm *)
   295 
   296 fun fixes_of_exp (export rep) = #fixes rep;
   297 
   298 (* export the result of the new goal thm, ie if we reduced teh
   299 subgoal, then we get a new reduced subtgoal with the old
   300 all-quantified variables *)
   301 local 
   302 
   303 (* allify puts in a meta level univ quantifier for a free variavble *)
   304 fun allify_term (v, t) = 
   305     let val vt = #t (Thm.rep_cterm v)
   306       val (n,ty) = Term.dest_Free vt
   307     in (Term.all ty) $ (Abs(n,ty,Term.abstract_over (vt, t))) end;
   308 
   309 fun allify_for_sg_term ctermify vs t =
   310     let val t_alls = foldr allify_term t vs;
   311         val ct_alls = ctermify t_alls; 
   312     in 
   313       (ct_alls, Drule.forall_elim_list vs (Thm.assume ct_alls))
   314     end;
   315 (* lookup type of a free var name from a list *)
   316 fun lookupfree vs vn  = 
   317     case Library.find_first (fn (n,ty) => n = vn) vs of 
   318       NONE => error ("prepare_goal_export:lookupfree: " ^ vn ^ " does not occur in the term")
   319     | SOME x => x;
   320 in
   321 fun export_back (export {fixes = vs, assumes = hprems, 
   322                          sgid = i, gth = gth}) newth = 
   323     let 
   324       val sgn = Thm.theory_of_thm newth;
   325       val ctermify = Thm.cterm_of sgn;
   326 
   327       val sgs = prems_of newth;
   328       val (sgallcts, sgthms) = 
   329           Library.split_list (map (allify_for_sg_term ctermify vs) sgs);
   330       val minimal_newth = 
   331           (Library.foldl (fn ( newth', sgthm) => 
   332                           Drule.compose_single (sgthm, 1, newth'))
   333                       (newth, sgthms));
   334       val allified_newth = 
   335           minimal_newth 
   336             |> Drule.implies_intr_list hprems
   337             |> Drule.forall_intr_list vs 
   338 
   339       val newth' = Drule.implies_intr_list sgallcts allified_newth
   340     in
   341       bicompose false (false, newth', (length sgallcts)) i gth
   342     end;
   343 
   344 (* 
   345 Given "vs" : names of free variables to abstract over,
   346 Given cterms : premices to abstract over (P1... Pn) in terms of vs,
   347 Given a thm of the form: 
   348 P1 vs; ...; Pn vs ==> Goal(C vs)
   349 
   350 Gives back: 
   351 (n, length of given cterms which have been allified
   352  [| !! vs. P1 vs; !! vs. Pn vs |] ==> !! C vs) the allified thm
   353 *)
   354 (* note: C may contain further premices etc 
   355 Note that cterms is the assumed facts, ie prems of "P1" that are
   356 reintroduced in allified form.
   357 *)
   358 fun prepare_goal_export (vs, cterms) th = 
   359     let 
   360       val sgn = Thm.theory_of_thm th;
   361       val ctermify = Thm.cterm_of sgn;
   362 
   363       val allfrees = map Term.dest_Free (Term.term_frees (Thm.prop_of th))
   364       val cfrees = map (ctermify o Free o lookupfree allfrees) vs
   365 
   366       val sgs = prems_of th;
   367       val (sgallcts, sgthms) = 
   368           Library.split_list (map (allify_for_sg_term ctermify cfrees) sgs);
   369 
   370       val minimal_th = 
   371           Goal.conclude (Library.foldl (fn ( th', sgthm) => 
   372                           Drule.compose_single (sgthm, 1, th'))
   373                       (th, sgthms));
   374 
   375       val allified_th = 
   376           minimal_th 
   377             |> Drule.implies_intr_list cterms
   378             |> Drule.forall_intr_list cfrees 
   379 
   380       val th' = Drule.implies_intr_list sgallcts allified_th
   381     in
   382       ((length sgallcts), th')
   383     end;
   384 
   385 end;
   386 
   387 
   388 (* exporting function that takes a solution to the fixed/assumed goal,
   389 and uses this to solve the subgoal in the main theorem *)
   390 fun export_solution (export {fixes = cfvs, assumes = hcprems,
   391                              sgid = i, gth = gth}) solth = 
   392     let 
   393       val solth' = 
   394           solth |> Drule.implies_intr_list hcprems
   395                 |> Drule.forall_intr_list cfvs
   396     in Drule.compose_single (solth', i, gth) end;
   397 
   398 fun export_solutions (xs,th) = foldr (uncurry export_solution) th xs;
   399 
   400 
   401 (* fix parameters of a subgoal "i", as free variables, and create an
   402 exporting function that will use the result of this proved goal to
   403 show the goal in the original theorem. 
   404 
   405 Note, an advantage of this over Isar is that it supports instantiation
   406 of unkowns in the earlier theorem, ie we can do instantiation of meta
   407 vars! 
   408 
   409 avoids constant, free and vars names. 
   410 
   411 loosely corresponds to:
   412 Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm
   413 Result: 
   414   ("(As ==> SGi x') ==> (As ==> SGi x')" : thm, 
   415    expf : 
   416      ("As ==> SGi x'" : thm) -> 
   417      ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm)
   418 *)
   419 fun fix_alls_in_term alledt = 
   420     let
   421       val t = Term.strip_all_body alledt;
   422       val alls = rev (Term.strip_all_vars alledt);
   423       val varnames = map (fst o fst o Term.dest_Var) (Term.term_vars t)
   424       val names = Term.add_term_names (t,varnames);
   425       val fvs = map Free 
   426                     (Name.variant_list names (map fst alls)
   427                        ~~ (map snd alls));
   428     in ((subst_bounds (fvs,t)), fvs) end;
   429 
   430 fun fix_alls_term i t = 
   431     let 
   432       val varnames = map (fst o fst o Term.dest_Var) (Term.term_vars t)
   433       val names = Term.add_term_names (t,varnames);
   434       val gt = Logic.get_goal t i;
   435       val body = Term.strip_all_body gt;
   436       val alls = rev (Term.strip_all_vars gt);
   437       val fvs = map Free 
   438                     (Name.variant_list names (map fst alls)
   439                        ~~ (map snd alls));
   440     in ((subst_bounds (fvs,body)), fvs) end;
   441 
   442 fun fix_alls_cterm i th = 
   443     let
   444       val ctermify = Thm.cterm_of (Thm.theory_of_thm th);
   445       val (fixedbody, fvs) = fix_alls_term i (Thm.prop_of th);
   446       val cfvs = rev (map ctermify fvs);
   447       val ct_body = ctermify fixedbody
   448     in
   449       (ct_body, cfvs)
   450     end;
   451 
   452 fun fix_alls' i = 
   453      (apfst Thm.trivial) o (fix_alls_cterm i);
   454 
   455 
   456 (* hide other goals *) 
   457 (* note the export goal is rotated by (i - 1) and will have to be
   458 unrotated to get backto the originial position(s) *)
   459 fun hide_other_goals th = 
   460     let
   461       (* tl beacuse fst sg is the goal we are interested in *)
   462       val cprems = tl (Drule.cprems_of th)
   463       val aprems = map Thm.assume cprems
   464     in
   465       (Drule.implies_elim_list (Drule.rotate_prems 1 th) aprems, 
   466        cprems)
   467     end;
   468 
   469 (* a nicer version of the above that leaves only a single subgoal (the
   470 other subgoals are hidden hyps, that the exporter suffles about)
   471 namely the subgoal that we were trying to solve. *)
   472 (* loosely corresponds to:
   473 Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm
   474 Result: 
   475   ("(As ==> SGi x') ==> SGi x'" : thm, 
   476    expf : 
   477      ("SGi x'" : thm) -> 
   478      ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm)
   479 *)
   480 fun fix_alls i th = 
   481     let 
   482       val (fixed_gth, fixedvars) = fix_alls' i th
   483       val (sml_gth, othergoals) = hide_other_goals fixed_gth
   484     in
   485       (sml_gth, export {fixes = fixedvars, 
   486                         assumes = othergoals, 
   487                         sgid = i, gth = th})
   488     end;
   489 
   490 
   491 (* assume the premises of subgoal "i", this gives back a list of
   492 assumed theorems that are the premices of subgoal i, it also gives
   493 back a new goal thm and an exporter, the new goalthm is as the old
   494 one, but without the premices, and the exporter will use a proof of
   495 the new goalthm, possibly using the assumed premices, to shoe the
   496 orginial goal.
   497 
   498 Note: Dealing with meta vars, need to meta-level-all them in the
   499 shyps, which we can later instantiate with a specific value.... ? 
   500 think about this... maybe need to introduce some new fixed vars and
   501 then remove them again at the end... like I do with rw_inst. 
   502 
   503 loosely corresponds to:
   504 Given "[| SG0; ... [| A0; ... An |] ==> SGi; ... SGm |] ==> G" : thm
   505 Result: 
   506 (["A0" [A0], ... ,"An" [An]] : thm list, -- assumptions
   507  "SGi ==> SGi" : thm, -- new goal 
   508  "SGi" ["A0" ... "An"] : thm ->   -- export function
   509     ("[| SG0 ... SGi-1, SGi+1, SGm |] ==> G" : thm) list)
   510 *)
   511 fun assume_prems i th =
   512     let 
   513       val t = (prop_of th); 
   514       val gt = Logic.get_goal t i;
   515       val _ = case Term.strip_all_vars gt of [] => () 
   516               | _ => error "assume_prems: goal has params"
   517       val body = gt;
   518       val prems = Logic.strip_imp_prems body;
   519       val concl = Logic.strip_imp_concl body;
   520 
   521       val sgn = Thm.theory_of_thm th;
   522       val ctermify = Thm.cterm_of sgn;
   523       val cprems = map ctermify prems;
   524       val aprems = map Thm.assume cprems;
   525       val gthi = Thm.trivial (ctermify concl);
   526 
   527       (* fun explortf thi = 
   528           Drule.compose (Drule.implies_intr_list cprems thi, 
   529                          i, th) *)
   530     in
   531       (aprems, gthi, cprems)
   532     end;
   533 
   534 
   535 (* first fix the variables, then assume the assumptions *)
   536 (* loosely corresponds to:
   537 Given 
   538   "[| SG0; ... 
   539       !! xs. [| A0 xs; ... An xs |] ==> SGi xs; 
   540       ... SGm |] ==> G" : thm
   541 Result: 
   542 (["A0 xs'" [A0 xs'], ... ,"An xs'" [An xs']] : thm list, -- assumptions
   543  "SGi xs' ==> SGi xs'" : thm,  -- new goal 
   544  "SGi xs'" ["A0 xs'" ... "An xs'"] : thm ->   -- export function
   545     ("[| SG0 ... SGi-1, SGi+1, SGm |] ==> G" : thm) list)
   546 *)
   547 
   548 (* Note: the fix_alls actually pulls through all the assumptions which
   549 means that the second export is not needed. *)
   550 fun fixes_and_assumes i th = 
   551     let 
   552       val (fixgth, exp1) = fix_alls i th
   553       val (assumps, goalth, _) = assume_prems 1 fixgth
   554     in 
   555       (assumps, goalth, exp1)
   556     end;
   557 
   558 
   559 (* Fixme: allow different order of subgoals given to expf *)
   560 (* make each subgoal into a separate thm that needs to be proved *)
   561 (* loosely corresponds to:
   562 Given 
   563   "[| SG0; ... SGm |] ==> G" : thm
   564 Result: 
   565 (["SG0 ==> SG0", ... ,"SGm ==> SGm"] : thm list, -- goals
   566  ["SG0", ..., "SGm"] : thm list ->   -- export function
   567    "G" : thm)
   568 *)
   569 fun subgoal_thms th = 
   570     let 
   571       val t = (prop_of th); 
   572 
   573       val prems = Logic.strip_imp_prems t;
   574 
   575       val sgn = Thm.theory_of_thm th;
   576       val ctermify = Thm.cterm_of sgn;
   577 
   578       val aprems = map (Thm.trivial o ctermify) prems;
   579 
   580       fun explortf premths = 
   581           Drule.implies_elim_list th premths
   582     in
   583       (aprems, explortf)
   584     end;
   585 
   586 
   587 (* make all the premices of a theorem hidden, and provide an unhide
   588 function, that will bring them back out at a later point. This is
   589 useful if you want to get back these premices, after having used the
   590 theorem with the premices hidden *)
   591 (* loosely corresponds to:
   592 Given "As ==> G" : thm
   593 Result: ("G [As]" : thm, 
   594          "G [As]" : thm -> "As ==> G" : thm
   595 *)
   596 fun hide_prems th = 
   597     let 
   598       val cprems = Drule.cprems_of th;
   599       val aprems = map Thm.assume cprems;
   600     (*   val unhidef = Drule.implies_intr_list cprems; *)
   601     in
   602       (Drule.implies_elim_list th aprems, cprems)
   603     end;
   604 
   605 
   606 
   607 
   608 (* Fixme: allow different order of subgoals in exportf *)
   609 (* as above, but also fix all parameters in all subgoals, and uses
   610 fix_alls, not fix_alls', ie doesn't leave extra asumptions as apparent
   611 subgoals. *)
   612 (* loosely corresponds to:
   613 Given 
   614   "[| !! x0s. A0s x0s ==> SG0 x0s; 
   615       ...; !! xms. Ams xms ==> SGm xms|] ==> G" : thm
   616 Result: 
   617 (["(A0s x0s' ==> SG0 x0s') ==> SG0 x0s'", 
   618   ... ,"(Ams xms' ==> SGm xms') ==> SGm xms'"] : thm list, -- goals
   619  ["SG0 x0s'", ..., "SGm xms'"] : thm list ->   -- export function
   620    "G" : thm)
   621 *)
   622 (* requires being given solutions! *)
   623 fun fixed_subgoal_thms th = 
   624     let 
   625       val (subgoals, expf) = subgoal_thms th;
   626 (*       fun export_sg (th, exp) = exp th; *)
   627       fun export_sgs expfs solthms = 
   628           expf (map2 (curry (op |>)) solthms expfs);
   629 (*           expf (map export_sg (ths ~~ expfs)); *)
   630     in 
   631       apsnd export_sgs (Library.split_list (map (apsnd export_solution o 
   632                                                  fix_alls 1) subgoals))
   633     end;
   634 
   635 end;