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