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