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