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