summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | dixon |

Mon, 18 Oct 2004 13:40:45 +0200 | |

changeset 15250 | 217bececa2bd |

parent 15249 | 0da6b3075bfa |

child 15251 | bb6f072c8d10 |

added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.

TFL/casesplit.ML | file | annotate | diff | comparison | revisions | |

TFL/isand.ML | file | annotate | diff | comparison | revisions |

--- a/TFL/casesplit.ML Mon Oct 18 11:43:40 2004 +0200 +++ b/TFL/casesplit.ML Mon Oct 18 13:40:45 2004 +0200 @@ -31,6 +31,13 @@ val dest_Trueprop : Term.term -> Term.term val mk_Trueprop : Term.term -> Term.term val read_cterm : Sign.sg -> string -> Thm.cterm + + val localize : Thm.thm list + val local_impI : Thm.thm + val atomize : Thm.thm list + val rulify1 : Thm.thm list + val rulify2 : Thm.thm list + end; (* for HOL *) @@ -39,6 +46,13 @@ val dest_Trueprop = HOLogic.dest_Trueprop; val mk_Trueprop = HOLogic.mk_Trueprop; val read_cterm = HOLogic.read_cterm; + +val localize = [Thm.symmetric (thm "induct_implies_def")]; +val local_impI = thm "induct_impliesI"; +val atomize = thms "induct_atomize"; +val rulify1 = thms "induct_rulify1"; +val rulify2 = thms "induct_rulify2"; + end; @@ -76,6 +90,23 @@ functor CaseSplitFUN(Data : CASE_SPLIT_DATA) = struct +val rulify_goals = Tactic.rewrite_goals_rule Data.rulify1; +val atomize_goals = Tactic.rewrite_goals_rule Data.atomize; + +(* +val localize = Tactic.norm_hhf_rule o Tactic.simplify false Data.localize; +fun atomize_term sg = + ObjectLogic.drop_judgment sg o MetaSimplifier.rewrite_term sg Data.atomize []; +val rulify_tac = Tactic.rewrite_goal_tac Data.rulify1; +val atomize_tac = Tactic.rewrite_goal_tac Data.atomize; +Tactic.simplify_goal +val rulify_tac = + Tactic.rewrite_goal_tac Data.rulify1 THEN' + Tactic.rewrite_goal_tac Data.rulify2 THEN' + Tactic.norm_hhf_tac; +val atomize = Tactic.norm_hhf_rule o Tactic.simplify true Data.atomize; +*) + (* beta-eta contract the theorem *) fun beta_eta_contract thm = let @@ -148,26 +179,49 @@ (* does a case split on the given variable (Free fv) *) fun casesplit_free fv i th = let - val gt = Data.dest_Trueprop (nth_elem( i - 1, Thm.prems_of th)); + val (subgoalth, exp) = IsaND.fix_alls i th; + val subgoalth' = atomize_goals subgoalth; + val gt = Data.dest_Trueprop (Logic.get_goal (Thm.prop_of subgoalth') 1); val sgn = Thm.sign_of_thm th; + + val splitter_thm = mk_casesplit_goal_thm sgn fv gt; + val nsplits = Thm.nprems_of splitter_thm; + + val split_goal_th = splitter_thm RS subgoalth'; + val rulified_split_goal_th = rulify_goals split_goal_th; in - Tactic.rtac (mk_casesplit_goal_thm sgn fv gt) i th + IsaND.export_back exp rulified_split_goal_th end; + (* for use when there are no prems to the subgoal *) (* does a case split on the given variable *) fun casesplit_name vstr i th = let - val gt = Data.dest_Trueprop (nth_elem( i - 1, Thm.prems_of th)); + val (subgoalth, exp) = IsaND.fix_alls i th; + val subgoalth' = atomize_goals subgoalth; + val gt = Data.dest_Trueprop (Logic.get_goal (Thm.prop_of subgoalth') 1); + val freets = Term.term_frees gt; - fun getter x = let val (n,ty) = Term.dest_Free x in - if vstr = n then Some (n,ty) else None end; + fun getter x = + let val (n,ty) = Term.dest_Free x in + (if vstr = n orelse vstr = Syntax.dest_skolem n + then Some (n,ty) else None ) + handle LIST _ => None + end; val (n,ty) = case Library.get_first getter freets of Some (n, ty) => (n, ty) | _ => raise ERROR_MESSAGE ("no such variable " ^ vstr); val sgn = Thm.sign_of_thm th; + + val splitter_thm = mk_casesplit_goal_thm sgn (n,ty) gt; + val nsplits = Thm.nprems_of splitter_thm; + + val split_goal_th = splitter_thm RS subgoalth'; + + val rulified_split_goal_th = rulify_goals split_goal_th; in - Tactic.rtac (mk_casesplit_goal_thm sgn (n,ty) gt) i th + IsaND.export_back exp rulified_split_goal_th end; @@ -196,6 +250,7 @@ fun find_term_split (Free v, _ $ _) = Some v | find_term_split (Free v, Const _) = Some v | find_term_split (Free v, Abs _) = Some v (* do we really want this case? *) + | find_term_split (Free v, Var _) = None (* keep searching *) | find_term_split (a $ b, a2 $ b2) = (case find_term_split (a, a2) of None => find_term_split (b,b2) @@ -229,9 +284,9 @@ (* split the subgoal i of "genth" until we get to a member of splitths. Assumes that genth will be a general form of splitths, that can be case-split, as needed. Otherwise fails. Note: We assume that -all of "splitths" are aplit to the same level, and thus it doesn't +all of "splitths" are split to the same level, and thus it doesn't matter which one we choose to look for the next split. Simply add -search on splitthms and plit variable, to change this. *) +search on splitthms and split variable, to change this. *) (* Note: possible efficiency measure: when a case theorem is no longer useful, drop it? *) (* Note: This should not be a separate tactic but integrated into the @@ -244,11 +299,16 @@ (* check if we are a member of splitths - FIXME: quicker and more flexible with discrim net. *) - fun solve_by_splitth th split = biresolution false [(false,split)] 1 th; + fun solve_by_splitth th split = + Thm.biresolution false [(false,split)] 1 th; fun split th = (case find_thms_split splitths 1 th of - None => raise ERROR_MESSAGE "splitto: cannot find variable to split on" + None => + (writeln "th:"; + print th; writeln "split ths:"; + print splitths; writeln "\n--"; + raise ERROR_MESSAGE "splitto: cannot find variable to split on") | Some v => let val gt = Data.dest_Trueprop (nth_elem(0, Thm.prems_of th));

--- a/TFL/isand.ML Mon Oct 18 11:43:40 2004 +0200 +++ b/TFL/isand.ML Mon Oct 18 13:40:45 2004 +0200 @@ -1,5 +1,5 @@ (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) -(* Title: TFL/isand.ML +(* Title: sys/isand.ML Author: Lucas Dixon, University of Edinburgh lucas.dixon@ed.ac.uk Date: 6 Aug 2004 @@ -19,6 +19,15 @@ allowing the interleaving of proof, or provide a structure for the ordering of proof, thus allowing proof attempts in parrelle, but recording the order to apply things in. + +debugging tools: +fun asm_mk t = (assume (cterm_of (Theory.sign_of (the_context())) t)); +fun asm_read s = + (assume (read_cterm (Theory.sign_of (Context.the_context())) (s,propT))); + + THINK: are we really ok with our varify name w.r.t the prop - do + we alos need to avoid named in the hidden hyps? + *) structure IsaND = @@ -26,7 +35,7 @@ (* Solve *some* subgoal of "th" directly by "sol" *) (* Note: this is probably what Markus ment to do upon export of a -"show" but maybe he used RS/rtac intead, which would wrongly lead to +"show" but maybe he used RS/rtac instead, which would wrongly lead to failing if there are premices to the shown goal. *) fun solve_with sol th = let fun solvei 0 = Seq.empty @@ -38,6 +47,213 @@ end; +(* Given ctertmify function, (string,type) pairs capturing the free +vars that need to be allified in the assumption, and a theorem with +assumptions possibly containing the free vars, then we give back the +assumptions allified as hidden hyps. *) +(* +Given: vs +th: A vs ==> B vs +Results in: "B vs" [!!x. A x] +*) +fun allify_conditions ctermify Ts th = + let + val premts = Thm.prems_of th + + fun allify_prem_var (vt as (n,ty),t) = + (Term.all ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t))) + + fun allify_prem Ts p = foldr allify_prem_var (Ts, p) + + val cTs = map (ctermify o Free) Ts + val cterm_asms = map (ctermify o allify_prem Ts) premts + val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms + in + (foldl (fn (x,y) => y RS x) (th, allifyied_asm_thms), cterm_asms) + end; + +fun allify_conditions' Ts th = + allify_conditions (Thm.cterm_of (Thm.sign_of_thm th)) Ts th; + + + +(* change schematic vars to fresh free vars *) +fun fix_vars_to_frees th = + let + val ctermify = Thm.cterm_of (Thm.sign_of_thm th) + val prop = Thm.prop_of th + val vars = map Term.dest_Var (Term.term_vars prop) + + val names = Term.add_term_names (prop, []) + + val (insts,names2) = + foldl (fn ((insts,names),v as ((n,i),ty)) => + let val n2 = Term.variant names n in + ((ctermify (Var v), ctermify (Free(n2,ty))) :: insts, + n2 :: names) + end) + (([],names), vars) + in (insts, Thm.instantiate ([], insts) th) end; + +(* *) +(* +val th = Thm.freezeT (topthm()); +val (insts, th') = fix_vars_to_frees th; +val Ts = map (Term.dest_Free o Thm.term_of o snd) insts; +allify_conditions' Ts th'; +*) + + +(* datatype to capture an exported result, ie a fix or assume. *) +datatype export = + export of {fixes : Thm.cterm list, (* fixed vars *) + assumes : Thm.cterm list, (* hidden hyps/assumed prems *) + sgid : int, + gth : Thm.thm}; (* subgoal/goalthm *) + + + +(* export the result of the new goal thm, ie if we reduced teh +subgoal, then we get a new reduced subtgoal with the old +all-quantified variables *) +local +fun allify_term (v, t) = + let val vt = #t (Thm.rep_cterm v) + val (n,ty) = Term.dest_Free vt + in (Term.all ty) $ (Abs(n,ty,Term.abstract_over (vt, t))) end; + +fun allify_for_sg_term ctermify vs t = + let val t_alls = foldr allify_term (vs,t); + val ct_alls = ctermify t_alls; + in + (ct_alls, Drule.forall_elim_list vs (Thm.assume ct_alls)) + end; + +fun lookupfree vs vn = + case Library.find_first (fn (n,ty) => n = vn) vs of + None => raise ERROR_MESSAGE ("prepare_goal_export:lookupfree: " + ^ vn ^ " does not occur in the term") + | Some x => x; +in +fun export_back (export {fixes = vs, assumes = hprems, + sgid = i, gth = gth}) newth = + let + val sgn = Thm.sign_of_thm newth; + val ctermify = Thm.cterm_of sgn; + + val sgs = prems_of newth; + val (sgallcts, sgthms) = + Library.split_list (map (allify_for_sg_term ctermify vs) sgs); + val minimal_newth = + (foldl (fn ( newth', sgthm) => + Drule.compose_single (sgthm, 1, newth')) + (newth, sgthms)); + val allified_newth = + minimal_newth + |> Drule.implies_intr_list hprems + |> Drule.forall_intr_list vs + + val newth' = Drule.implies_intr_list sgallcts allified_newth + in + bicompose false (false, newth', (length sgallcts)) i gth + end; + +(* given a thm of the form: +P1 vs; ...; Pn vs ==> Goal(C vs) + +Gives back: +n, +[| !! vs. P1 vs; !! vs. Pn vs |] + ==> !! C vs +*) +(* note: C may contain further premices etc +Note that cterms is the assumed facts, ie prems of "P1" that are +reintroduced. +*) +fun prepare_goal_export (vs, cterms) th = + let + val sgn = Thm.sign_of_thm th; + val ctermify = Thm.cterm_of sgn; + + val allfrees = map Term.dest_Free (Term.term_frees (Thm.prop_of th)) + val cfrees = map (ctermify o Free o lookupfree allfrees) vs + + val sgs = prems_of th; + val (sgallcts, sgthms) = + Library.split_list (map (allify_for_sg_term ctermify cfrees) sgs); + + val minimal_th = + (foldl (fn ( th', sgthm) => + Drule.compose_single (sgthm, 1, th')) + (th, sgthms)) RS Drule.rev_triv_goal; + + val allified_th = + minimal_th + |> Drule.implies_intr_list cterms + |> Drule.forall_intr_list cfrees + + val th' = Drule.implies_intr_list sgallcts allified_th + in + ((length sgallcts), th') + end; + +end; + +(* val exports_back = foldr (uncurry export_to_sg); *) + +(* test with: + +fun asm_mk t = (assume (cterm_of (Theory.sign_of (the_context())) t)); +fun asm_read s = + (assume (read_cterm (Theory.sign_of (Context.the_context())) (s,propT))); +use_thy "theories/dbg2"; +Goal "!! x :: nat. [| A x; B x; C x; D x |] ==> ((P1 x & P2 x) & P3 x)"; +by (rtac conjI 1); +by (rtac conjI 1); +val th = topthm(); +val i = 1; +val (gthi, exp) = IsaND.fix_alls i th; +val [th'] = Seq.list_of (rtac (thm "p321") 1 gthi); +val oldthewth = Seq.list_of (IsaND.export_back exp th'); + or +val [th'] = Seq.list_of (RWStepTac.rwstep_tac (thms "aa2") 1 gthi); +val oldthewth = Seq.list_of (IsaND.export_back exp th'); + + +val th = topthm(); +val i = 1; +val (goalth, exp1) = IsaND.fix_alls' i th; +val (newth, exp2) = IsaND.hide_other_goals 2 goalth; +val oldthewth = Seq.list_of (IsaND.export_back exp2 newth); +val (export {fixes = vs, assumes = hprems, + sgid = i, gth = gth}) = exp2; + + +Goal "!! x y. P (x + (Suc y)) ==> Z x y ==> Q ((Suc x) + y)"; +val th = topthm(); +val i = 1; +val (gthi, exp) = IsaND.fix_alls i th; +val newth = Seq.hd (Asm_full_simp_tac 1 gthi); +Seq.list_of (IsaND.export_back exp newth); +*) + + + +(* exporting function that takes a solution to the fixed/assumed goal, +and uses this to solve the subgoal in the main theorem *) +fun export_solution (export {fixes = cfvs, assumes = hcprems, + sgid = i, gth = gth}) solth = + let + val solth' = + solth |> Drule.implies_intr_list hcprems + |> Drule.forall_intr_list cfvs + in Drule.compose_single (solth', i, gth) end; + +val exports_solution = foldr (uncurry export_solution); + + + + (* fix parameters of a subgoal "i", as free variables, and create an exporting function that will use the result of this proved goal to show the goal in the original theorem. @@ -45,6 +261,14 @@ Note, an advantage of this over Isar is that it supports instantiation of unkowns in the earlier theorem, ie we can do instantiation of meta vars! *) +(* loosely corresponds to: +Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm +Result: + ("(As ==> SGi x') ==> (As ==> SGi x')" : thm, + expf : + ("As ==> SGi x'" : thm) -> + ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm) +*) fun fix_alls' i th = let val t = (prop_of th); @@ -64,55 +288,75 @@ (* Given a thm justifying subgoal i, solve subgoal i *) (* Note: fails if there are choices! *) - fun exportf thi = + (* fun exportf thi = Drule.compose_single (Drule.forall_intr_list cfvs thi, - i, th) + i, th) *) + in (gthi0, cfvs) end; + +(* small example: +Goal "!! x. [| False; C x |] ==> P x"; +val th = topthm(); +val i = 1; +val (goalth, fixes) = fix_alls' i (topthm()); + +Goal "!! x. P (x + (Suc y)) ==> Q ((Suc x) + y)"; +Goal "!! x. P x y = Q y x ==> P x y"; +val th = topthm(); +val i = 1; +val (prems, gthi, expf) = IsaND.fixes_and_assumes i th; +val gth2 = Seq.hd (RWStepTac.rwstep_tac prems 1 gthi); +*) + + +(* hide other goals *) +(* note the export goal is rotated by (i - 1) and will have to be +unrotated to get backto the originial position(s) *) +fun hide_other_goals th = + let + (* tl beacuse fst sg is the goal we are interested in *) + val cprems = tl (Drule.cprems_of th) + val aprems = map Thm.assume cprems in - (gthi0, exportf) + (Drule.implies_elim_list (Drule.rotate_prems 1 th) aprems, + cprems) + end; +(* test with: +Goal "!! x. [| False; C x |] ==> P x"; +val th = topthm(); +val i = 1; +val (goalth, fixedvars) = IsaND.fix_alls' i th; +val (newth, hiddenprems) = IsaND.hide_other_goals goalth; +*) + +(* a nicer version of the above that leaves only a single subgoal (the +other subgoals are hidden hyps, that the exporter suffles about) +namely the subgoal that we were trying to solve. *) +(* loosely corresponds to: +Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm +Result: + ("(As ==> SGi x') ==> SGi x'" : thm, + expf : + ("SGi x'" : thm) -> + ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm) +*) +fun fix_alls i th = + let + val (fixed_gth, fixedvars) = fix_alls' i th + val (sml_gth, othergoals) = hide_other_goals fixed_gth + in + (sml_gth, export {fixes = fixedvars, + assumes = othergoals, + sgid = i, gth = th}) end; (* small example: Goal "!! x. [| False; C x |] ==> P x"; val th = topthm(); val i = 1; -val (goalth, expf) = fix_alls i (topthm()); -*) - - -(* a nicer version of the above that leaves only a single subgoal (the -other subgoals are hidden hyps, that the exporter suffles about) -namely the subgoal that we were trying to solve. *) - -fun fix_alls i th = - let - val (gthi, exportf) = fix_alls' i th - val gthi' = Drule.rotate_prems 1 gthi - - val sgn = Thm.sign_of_thm th; - val ctermify = Thm.cterm_of sgn; +val (goalth, exp) = IsaND.fix_alls i th; +val oldthewth = Seq.list_of (IsaND.export_back exp goalth); - val prems = tl (Thm.prems_of gthi) - val cprems = map ctermify prems; - val aprems = map Thm.assume cprems; - - val exportf' = - exportf o (Drule.implies_intr_list cprems) - in - (Drule.implies_elim_list gthi' aprems, exportf') - end; - -(* small example: -Goal "P x"; -val i = 1; -val th = topthm(); -val x = fix_alls (topthm()) 1; - -Goal "!! x. [| False; C x |] ==> P x"; -val th = topthm(); -val i = 1; -val (goalth, expf) = fix_alls' th i; - -val (premths, goalth2, expf2) = assume_prems 1 goalth; +val (premths, goalth2, expf2) = IsaND.assume_prems 1 goalth; val False_th = nth_elem (0,premths); val anything = False_th RS (thm "FalseE"); val th2 = anything RS goalth2; @@ -132,6 +376,14 @@ shyps, which we can later instantiate with a specific value.... ? think about this... maybe need to introduce some new fixed vars and then remove them again at the end... like I do with rw_inst. *) +(* loosely corresponds to: +Given "[| SG0; ... [| A0; ... An |] ==> SGi; ... SGm |] ==> G" : thm +Result: +(["A0" [A0], ... ,"An" [An]] : thm list, -- assumptions + "SGi ==> SGi" : thm, -- new goal + "SGi" ["A0" ... "An"] : thm -> -- export function + ("[| SG0 ... SGi-1, SGi+1, SGm |] ==> G" : thm) list) +*) fun assume_prems i th = let val t = (prop_of th); @@ -148,17 +400,17 @@ val aprems = map Thm.assume cprems; val gthi = Thm.trivial (ctermify concl); - fun explortf thi = + (* fun explortf thi = Drule.compose (Drule.implies_intr_list cprems thi, - i, th) + i, th) *) in - (aprems, gthi, explortf) + (aprems, gthi, cprems) end; (* small example: Goal "False ==> b"; val th = topthm(); val i = 1; -val (prems, goalth, expf) = assume_prems i (topthm()); +val (prems, goalth, cprems) = IsaND.assume_prems i (topthm()); val F = hd prems; val FalseE = thm "FalseE"; val anything = F RS FalseE; @@ -167,7 +419,57 @@ *) -(* Fixme: allow different order of subgoals *) +(* first fix the variables, then assume the assumptions *) +(* loosely corresponds to: +Given + "[| SG0; ... + !! xs. [| A0 xs; ... An xs |] ==> SGi xs; + ... SGm |] ==> G" : thm +Result: +(["A0 xs'" [A0 xs'], ... ,"An xs'" [An xs']] : thm list, -- assumptions + "SGi xs' ==> SGi xs'" : thm, -- new goal + "SGi xs'" ["A0 xs'" ... "An xs'"] : thm -> -- export function + ("[| SG0 ... SGi-1, SGi+1, SGm |] ==> G" : thm) list) +*) + +(* Note: the fix_alls actually pulls through all the assumptions which +means that the second export is not needed. *) +fun fixes_and_assumes i th = + let + val (fixgth, exp1) = fix_alls i th + val (assumps, goalth, _) = assume_prems 1 fixgth + in + (assumps, goalth, exp1) + end; +(* test with: +Goal "!! x. [| False; C x |] ==> P x"; +val th = topthm(); +val i = 1; +val (fixgth, exp) = IsaND.fix_alls i th; +val (assumps, goalth, _) = assume_prems 1 fixgth; + +val oldthewth = Seq.list_of (IsaND.export_back exp fixgth); +val oldthewth = Seq.list_of (IsaND.export_back exp goalth); + + +val (prems, goalth, expf) = IsaND.fixes_and_assumes i th; +val F = hd prems; +val FalseE = thm "FalseE"; +val anything = F RS FalseE; +val thi = anything RS goalth; +val res' = expf thi; +*) + +(* Fixme: allow different order of subgoals given to expf *) +(* make each subgoal into a separate thm that needs to be proved *) +(* loosely corresponds to: +Given + "[| SG0; ... SGm |] ==> G" : thm +Result: +(["SG0 ==> SG0", ... ,"SGm ==> SGm"] : thm list, -- goals + ["SG0", ..., "SGm"] : thm list -> -- export function + "G" : thm) +*) fun subgoal_thms th = let val t = (prop_of th); @@ -195,6 +497,11 @@ function, that will bring them back out at a later point. This is useful if you want to get back these premices, after having used the theorem with the premices hidden *) +(* loosely corresponds to: +Given "As ==> G" : thm +Result: ("G [As]" : thm, + "G [As]" : thm -> "As ==> G" : thm +*) fun hide_prems th = let val sgn = Thm.sign_of_thm th; @@ -205,29 +512,39 @@ val cprems = map ctermify prems; val aprems = map Thm.trivial cprems; - val unhidef = Drule.implies_intr_list cprems; + (* val unhidef = Drule.implies_intr_list cprems; *) in - (Drule.implies_elim_list th aprems, unhidef) + (Drule.implies_elim_list th aprems, cprems) end; -(* Fixme: allow different order of subgoals *) +(* Fixme: allow different order of subgoals in exportf *) +(* as above, but also fix all parameters in all subgoals, and uses +fix_alls, not fix_alls', ie doesn't leave extra asumptions as apparent +subgoals. *) +(* loosely corresponds to: +Given + "[| !! x0s. A0s x0s ==> SG0 x0s; + ...; !! xms. Ams xms ==> SGm xms|] ==> G" : thm +Result: +(["(A0s x0s' ==> SG0 x0s') ==> SG0 x0s'", + ... ,"(Ams xms' ==> SGm xms') ==> SGm xms'"] : thm list, -- goals + ["SG0 x0s'", ..., "SGm xms'"] : thm list -> -- export function + "G" : thm) +*) +(* requires being given solutions! *) fun fixed_subgoal_thms th = let val (subgoals, expf) = subgoal_thms th; - (* fun export_sg (th, exp) = exp th; *) - fun export_sgs expfs ths = - expf (map2 (op |>) (ths, expfs)); - + fun export_sgs expfs solthms = + expf (map2 (op |>) (solthms, expfs)); (* expf (map export_sg (ths ~~ expfs)); *) - - - in - apsnd export_sgs (Library.split_list (map (fix_alls 1) subgoals)) + apsnd export_sgs (Library.split_list (map (apsnd export_solution o + fix_alls 1) subgoals)) end; @@ -238,4 +555,4 @@ val (subgoals, expf) = fixed_subgoal_thms (topthm()); *) -end; \ No newline at end of file +end;