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