--- 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;