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