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.
authordixon
Mon Oct 18 13:40:45 2004 +0200 (2004-10-18)
changeset 15250217bececa2bd
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
TFL/isand.ML
     1.1 --- a/TFL/casesplit.ML	Mon Oct 18 11:43:40 2004 +0200
     1.2 +++ b/TFL/casesplit.ML	Mon Oct 18 13:40:45 2004 +0200
     1.3 @@ -31,6 +31,13 @@
     1.4    val dest_Trueprop : Term.term -> Term.term
     1.5    val mk_Trueprop : Term.term -> Term.term
     1.6    val read_cterm : Sign.sg -> string -> Thm.cterm
     1.7 +
     1.8 +  val localize : Thm.thm list
     1.9 +  val local_impI : Thm.thm
    1.10 +  val atomize : Thm.thm list
    1.11 +  val rulify1 : Thm.thm list
    1.12 +  val rulify2 : Thm.thm list
    1.13 +
    1.14  end;
    1.15  
    1.16  (* for HOL *)
    1.17 @@ -39,6 +46,13 @@
    1.18  val dest_Trueprop = HOLogic.dest_Trueprop;
    1.19  val mk_Trueprop = HOLogic.mk_Trueprop;
    1.20  val read_cterm = HOLogic.read_cterm;
    1.21 +
    1.22 +val localize = [Thm.symmetric (thm "induct_implies_def")];
    1.23 +val local_impI = thm "induct_impliesI";
    1.24 +val atomize = thms "induct_atomize";
    1.25 +val rulify1 = thms "induct_rulify1";
    1.26 +val rulify2 = thms "induct_rulify2";
    1.27 +
    1.28  end;
    1.29  
    1.30  
    1.31 @@ -76,6 +90,23 @@
    1.32  functor CaseSplitFUN(Data : CASE_SPLIT_DATA) =
    1.33  struct
    1.34  
    1.35 +val rulify_goals = Tactic.rewrite_goals_rule Data.rulify1;
    1.36 +val atomize_goals = Tactic.rewrite_goals_rule Data.atomize;
    1.37 +
    1.38 +(* 
    1.39 +val localize = Tactic.norm_hhf_rule o Tactic.simplify false Data.localize;
    1.40 +fun atomize_term sg =
    1.41 +  ObjectLogic.drop_judgment sg o MetaSimplifier.rewrite_term sg Data.atomize [];
    1.42 +val rulify_tac =  Tactic.rewrite_goal_tac Data.rulify1;
    1.43 +val atomize_tac =  Tactic.rewrite_goal_tac Data.atomize;
    1.44 +Tactic.simplify_goal
    1.45 +val rulify_tac =
    1.46 +  Tactic.rewrite_goal_tac Data.rulify1 THEN'
    1.47 +  Tactic.rewrite_goal_tac Data.rulify2 THEN'
    1.48 +  Tactic.norm_hhf_tac;
    1.49 +val atomize = Tactic.norm_hhf_rule o Tactic.simplify true Data.atomize;
    1.50 +*)
    1.51 +
    1.52  (* beta-eta contract the theorem *)
    1.53  fun beta_eta_contract thm = 
    1.54      let
    1.55 @@ -148,26 +179,49 @@
    1.56  (* does a case split on the given variable (Free fv) *)
    1.57  fun casesplit_free fv i th = 
    1.58      let 
    1.59 -      val gt = Data.dest_Trueprop (nth_elem( i - 1, Thm.prems_of th));
    1.60 +      val (subgoalth, exp) = IsaND.fix_alls i th;
    1.61 +      val subgoalth' = atomize_goals subgoalth;
    1.62 +      val gt = Data.dest_Trueprop (Logic.get_goal (Thm.prop_of subgoalth') 1);
    1.63        val sgn = Thm.sign_of_thm th;
    1.64 +
    1.65 +      val splitter_thm = mk_casesplit_goal_thm sgn fv gt;
    1.66 +      val nsplits = Thm.nprems_of splitter_thm;
    1.67 +
    1.68 +      val split_goal_th = splitter_thm RS subgoalth';
    1.69 +      val rulified_split_goal_th = rulify_goals split_goal_th;
    1.70      in 
    1.71 -      Tactic.rtac (mk_casesplit_goal_thm sgn fv gt) i th
    1.72 +      IsaND.export_back exp rulified_split_goal_th
    1.73      end;
    1.74  
    1.75 +
    1.76  (* for use when there are no prems to the subgoal *)
    1.77  (* does a case split on the given variable *)
    1.78  fun casesplit_name vstr i th = 
    1.79      let 
    1.80 -      val gt = Data.dest_Trueprop (nth_elem( i - 1, Thm.prems_of th));
    1.81 +      val (subgoalth, exp) = IsaND.fix_alls i th;
    1.82 +      val subgoalth' = atomize_goals subgoalth;
    1.83 +      val gt = Data.dest_Trueprop (Logic.get_goal (Thm.prop_of subgoalth') 1);
    1.84 +
    1.85        val freets = Term.term_frees gt;
    1.86 -      fun getter x = let val (n,ty) = Term.dest_Free x in 
    1.87 -                       if vstr = n then Some (n,ty) else None end;
    1.88 +      fun getter x = 
    1.89 +          let val (n,ty) = Term.dest_Free x in 
    1.90 +            (if vstr = n orelse vstr = Syntax.dest_skolem n 
    1.91 +             then Some (n,ty) else None )
    1.92 +            handle LIST _ => None
    1.93 +          end;
    1.94        val (n,ty) = case Library.get_first getter freets 
    1.95                  of Some (n, ty) => (n, ty)
    1.96                   | _ => raise ERROR_MESSAGE ("no such variable " ^ vstr);
    1.97        val sgn = Thm.sign_of_thm th;
    1.98 +
    1.99 +      val splitter_thm = mk_casesplit_goal_thm sgn (n,ty) gt;
   1.100 +      val nsplits = Thm.nprems_of splitter_thm;
   1.101 +
   1.102 +      val split_goal_th = splitter_thm RS subgoalth';
   1.103 +
   1.104 +      val rulified_split_goal_th = rulify_goals split_goal_th;
   1.105      in 
   1.106 -      Tactic.rtac (mk_casesplit_goal_thm sgn (n,ty) gt) i th
   1.107 +      IsaND.export_back exp rulified_split_goal_th
   1.108      end;
   1.109  
   1.110  
   1.111 @@ -196,6 +250,7 @@
   1.112  fun find_term_split (Free v, _ $ _) = Some v
   1.113    | find_term_split (Free v, Const _) = Some v
   1.114    | find_term_split (Free v, Abs _) = Some v (* do we really want this case? *)
   1.115 +  | find_term_split (Free v, Var _) = None (* keep searching *)
   1.116    | find_term_split (a $ b, a2 $ b2) = 
   1.117      (case find_term_split (a, a2) of 
   1.118         None => find_term_split (b,b2)  
   1.119 @@ -229,9 +284,9 @@
   1.120  (* split the subgoal i of "genth" until we get to a member of
   1.121  splitths. Assumes that genth will be a general form of splitths, that
   1.122  can be case-split, as needed. Otherwise fails. Note: We assume that
   1.123 -all of "splitths" are aplit to the same level, and thus it doesn't
   1.124 +all of "splitths" are split to the same level, and thus it doesn't
   1.125  matter which one we choose to look for the next split. Simply add
   1.126 -search on splitthms and plit variable, to change this.  *)
   1.127 +search on splitthms and split variable, to change this.  *)
   1.128  (* Note: possible efficiency measure: when a case theorem is no longer
   1.129  useful, drop it? *)
   1.130  (* Note: This should not be a separate tactic but integrated into the
   1.131 @@ -244,11 +299,16 @@
   1.132  
   1.133        (* check if we are a member of splitths - FIXME: quicker and 
   1.134        more flexible with discrim net. *)
   1.135 -      fun solve_by_splitth th split = biresolution false [(false,split)] 1 th;
   1.136 +      fun solve_by_splitth th split = 
   1.137 +          Thm.biresolution false [(false,split)] 1 th;
   1.138  
   1.139        fun split th = 
   1.140            (case find_thms_split splitths 1 th of 
   1.141 -             None => raise ERROR_MESSAGE "splitto: cannot find variable to split on"
   1.142 +             None => 
   1.143 +             (writeln "th:";
   1.144 +              print th; writeln "split ths:";
   1.145 +             print splitths; writeln "\n--";
   1.146 +             raise ERROR_MESSAGE "splitto: cannot find variable to split on")
   1.147              | Some v => 
   1.148               let 
   1.149                 val gt = Data.dest_Trueprop (nth_elem(0, Thm.prems_of th));
     2.1 --- a/TFL/isand.ML	Mon Oct 18 11:43:40 2004 +0200
     2.2 +++ b/TFL/isand.ML	Mon Oct 18 13:40:45 2004 +0200
     2.3 @@ -1,5 +1,5 @@
     2.4  (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
     2.5 -(*  Title:      TFL/isand.ML
     2.6 +(*  Title:      sys/isand.ML
     2.7      Author:     Lucas Dixon, University of Edinburgh
     2.8                  lucas.dixon@ed.ac.uk
     2.9      Date:       6 Aug 2004
    2.10 @@ -19,6 +19,15 @@
    2.11      allowing the interleaving of proof, or provide a structure for the
    2.12      ordering of proof, thus allowing proof attempts in parrelle, but
    2.13      recording the order to apply things in.
    2.14 +
    2.15 +debugging tools:
    2.16 +fun asm_mk t = (assume (cterm_of (Theory.sign_of (the_context())) t)); 
    2.17 +fun asm_read s =  
    2.18 +    (assume (read_cterm (Theory.sign_of (Context.the_context())) (s,propT))); 
    2.19 +
    2.20 +    THINK: are we really ok with our varify name w.r.t the prop - do
    2.21 +    we alos need to avoid named in the hidden hyps?
    2.22 +
    2.23  *)
    2.24  
    2.25  structure IsaND =
    2.26 @@ -26,7 +35,7 @@
    2.27  
    2.28  (* Solve *some* subgoal of "th" directly by "sol" *)
    2.29  (* Note: this is probably what Markus ment to do upon export of a
    2.30 -"show" but maybe he used RS/rtac intead, which would wrongly lead to
    2.31 +"show" but maybe he used RS/rtac instead, which would wrongly lead to
    2.32  failing if there are premices to the shown goal. *)
    2.33  fun solve_with sol th = 
    2.34      let fun solvei 0 = Seq.empty
    2.35 @@ -38,6 +47,213 @@
    2.36      end;
    2.37  
    2.38  
    2.39 +(* Given ctertmify function, (string,type) pairs capturing the free
    2.40 +vars that need to be allified in the assumption, and a theorem with
    2.41 +assumptions possibly containing the free vars, then we give back the
    2.42 +assumptions allified as hidden hyps. *)
    2.43 +(* 
    2.44 +Given: vs 
    2.45 +th: A vs ==> B vs
    2.46 +Results in: "B vs" [!!x. A x]
    2.47 +*)
    2.48 +fun allify_conditions ctermify Ts th = 
    2.49 +    let 
    2.50 +      val premts = Thm.prems_of th
    2.51 +    
    2.52 +      fun allify_prem_var (vt as (n,ty),t)  = 
    2.53 +          (Term.all ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
    2.54 +
    2.55 +      fun allify_prem Ts p = foldr allify_prem_var (Ts, p)
    2.56 +
    2.57 +      val cTs = map (ctermify o Free) Ts
    2.58 +      val cterm_asms = map (ctermify o allify_prem Ts) premts
    2.59 +      val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms
    2.60 +    in
    2.61 +      (foldl (fn (x,y) => y RS x) (th, allifyied_asm_thms), cterm_asms)
    2.62 +    end;
    2.63 +
    2.64 +fun allify_conditions' Ts th = 
    2.65 +    allify_conditions (Thm.cterm_of (Thm.sign_of_thm th)) Ts th;
    2.66 +
    2.67 +
    2.68 +
    2.69 +(* change schematic vars to fresh free vars *)
    2.70 +fun fix_vars_to_frees th = 
    2.71 +    let 
    2.72 +      val ctermify = Thm.cterm_of (Thm.sign_of_thm th)
    2.73 +      val prop = Thm.prop_of th
    2.74 +      val vars = map Term.dest_Var (Term.term_vars prop)
    2.75 +
    2.76 +      val names = Term.add_term_names (prop, [])
    2.77 +
    2.78 +      val (insts,names2) = 
    2.79 +          foldl (fn ((insts,names),v as ((n,i),ty)) => 
    2.80 +                    let val n2 = Term.variant names n in
    2.81 +                      ((ctermify (Var v), ctermify (Free(n2,ty))) :: insts, 
    2.82 +                       n2 :: names)
    2.83 +                    end)
    2.84 +                (([],names), vars)
    2.85 +    in (insts, Thm.instantiate ([], insts) th) end;
    2.86 +
    2.87 +(* *)
    2.88 +(*
    2.89 +val th = Thm.freezeT (topthm());
    2.90 +val (insts, th') = fix_vars_to_frees th;
    2.91 +val Ts = map (Term.dest_Free o Thm.term_of o snd) insts;
    2.92 +allify_conditions' Ts th';
    2.93 +*)
    2.94 +
    2.95 +
    2.96 +(* datatype to capture an exported result, ie a fix or assume. *)
    2.97 +datatype export = 
    2.98 +         export of {fixes : Thm.cterm list, (* fixed vars *)
    2.99 +                    assumes : Thm.cterm list, (* hidden hyps/assumed prems *)
   2.100 +                    sgid : int,
   2.101 +                    gth :  Thm.thm}; (* subgoal/goalthm *)
   2.102 +
   2.103 +
   2.104 +
   2.105 +(* export the result of the new goal thm, ie if we reduced teh
   2.106 +subgoal, then we get a new reduced subtgoal with the old
   2.107 +all-quantified variables *)
   2.108 +local 
   2.109 +fun allify_term (v, t) = 
   2.110 +    let val vt = #t (Thm.rep_cterm v)
   2.111 +      val (n,ty) = Term.dest_Free vt
   2.112 +    in (Term.all ty) $ (Abs(n,ty,Term.abstract_over (vt, t))) end;
   2.113 +
   2.114 +fun allify_for_sg_term ctermify vs t =
   2.115 +    let val t_alls = foldr allify_term (vs,t);
   2.116 +        val ct_alls = ctermify t_alls; 
   2.117 +    in 
   2.118 +      (ct_alls, Drule.forall_elim_list vs (Thm.assume ct_alls))
   2.119 +    end;
   2.120 +
   2.121 +fun lookupfree vs vn  = 
   2.122 +    case Library.find_first (fn (n,ty) => n = vn) vs of 
   2.123 +      None => raise ERROR_MESSAGE ("prepare_goal_export:lookupfree: " 
   2.124 +                    ^ vn ^ " does not occur in the term")
   2.125 +    | Some x => x;
   2.126 +in
   2.127 +fun export_back (export {fixes = vs, assumes = hprems, 
   2.128 +                         sgid = i, gth = gth}) newth = 
   2.129 +    let 
   2.130 +      val sgn = Thm.sign_of_thm newth;
   2.131 +      val ctermify = Thm.cterm_of sgn;
   2.132 +
   2.133 +      val sgs = prems_of newth;
   2.134 +      val (sgallcts, sgthms) = 
   2.135 +          Library.split_list (map (allify_for_sg_term ctermify vs) sgs);
   2.136 +      val minimal_newth = 
   2.137 +          (foldl (fn ( newth', sgthm) => 
   2.138 +                          Drule.compose_single (sgthm, 1, newth'))
   2.139 +                      (newth, sgthms));
   2.140 +      val allified_newth = 
   2.141 +          minimal_newth 
   2.142 +            |> Drule.implies_intr_list hprems
   2.143 +            |> Drule.forall_intr_list vs 
   2.144 +
   2.145 +      val newth' = Drule.implies_intr_list sgallcts allified_newth
   2.146 +    in
   2.147 +      bicompose false (false, newth', (length sgallcts)) i gth
   2.148 +    end;
   2.149 +
   2.150 +(* given a thm of the form: 
   2.151 +P1 vs; ...; Pn vs ==> Goal(C vs)
   2.152 +
   2.153 +Gives back: 
   2.154 +n,
   2.155 +[| !! vs. P1 vs; !! vs. Pn vs |] 
   2.156 +  ==> !! C vs
   2.157 +*)
   2.158 +(* note: C may contain further premices etc 
   2.159 +Note that cterms is the assumed facts, ie prems of "P1" that are
   2.160 +reintroduced.
   2.161 +*)
   2.162 +fun prepare_goal_export (vs, cterms) th = 
   2.163 +    let 
   2.164 +      val sgn = Thm.sign_of_thm th;
   2.165 +      val ctermify = Thm.cterm_of sgn;
   2.166 +
   2.167 +      val allfrees = map Term.dest_Free (Term.term_frees (Thm.prop_of th))
   2.168 +      val cfrees = map (ctermify o Free o lookupfree allfrees) vs
   2.169 +
   2.170 +      val sgs = prems_of th;
   2.171 +      val (sgallcts, sgthms) = 
   2.172 +          Library.split_list (map (allify_for_sg_term ctermify cfrees) sgs);
   2.173 +
   2.174 +      val minimal_th = 
   2.175 +          (foldl (fn ( th', sgthm) => 
   2.176 +                          Drule.compose_single (sgthm, 1, th'))
   2.177 +                      (th, sgthms)) RS Drule.rev_triv_goal;
   2.178 +
   2.179 +      val allified_th = 
   2.180 +          minimal_th 
   2.181 +            |> Drule.implies_intr_list cterms
   2.182 +            |> Drule.forall_intr_list cfrees 
   2.183 +
   2.184 +      val th' = Drule.implies_intr_list sgallcts allified_th
   2.185 +    in
   2.186 +      ((length sgallcts), th')
   2.187 +    end;
   2.188 +
   2.189 +end;
   2.190 +
   2.191 +(* val exports_back = foldr (uncurry export_to_sg); *)
   2.192 +
   2.193 +(* test with:
   2.194 +
   2.195 +fun asm_mk t = (assume (cterm_of (Theory.sign_of (the_context())) t)); 
   2.196 +fun asm_read s =  
   2.197 +    (assume (read_cterm (Theory.sign_of (Context.the_context())) (s,propT))); 
   2.198 +use_thy "theories/dbg2";
   2.199 +Goal "!! x :: nat. [| A x; B x; C x; D x |] ==> ((P1 x & P2 x) & P3 x)";
   2.200 +by (rtac conjI 1);
   2.201 +by (rtac conjI 1);
   2.202 +val th = topthm();
   2.203 +val i = 1;
   2.204 +val (gthi, exp) = IsaND.fix_alls i th;
   2.205 +val [th'] = Seq.list_of (rtac (thm "p321") 1 gthi);
   2.206 +val oldthewth = Seq.list_of (IsaND.export_back exp th');
   2.207 + or 
   2.208 +val [th'] = Seq.list_of (RWStepTac.rwstep_tac (thms "aa2") 1 gthi);
   2.209 +val oldthewth = Seq.list_of (IsaND.export_back exp th');
   2.210 +
   2.211 +
   2.212 +val th = topthm();
   2.213 +val i = 1;
   2.214 +val (goalth, exp1) = IsaND.fix_alls' i th;
   2.215 +val (newth, exp2) = IsaND.hide_other_goals 2 goalth;
   2.216 +val oldthewth = Seq.list_of (IsaND.export_back exp2 newth);
   2.217 +val (export {fixes = vs, assumes = hprems, 
   2.218 +                            sgid = i, gth = gth}) = exp2;
   2.219 +
   2.220 +
   2.221 +Goal "!! x y. P (x + (Suc y)) ==> Z x y ==> Q ((Suc x) + y)"; 
   2.222 +val th = topthm();
   2.223 +val i = 1;
   2.224 +val (gthi, exp) = IsaND.fix_alls i th;
   2.225 +val newth = Seq.hd (Asm_full_simp_tac 1 gthi);
   2.226 +Seq.list_of (IsaND.export_back exp newth);
   2.227 +*)
   2.228 +
   2.229 +
   2.230 +
   2.231 +(* exporting function that takes a solution to the fixed/assumed goal,
   2.232 +and uses this to solve the subgoal in the main theorem *)
   2.233 +fun export_solution (export {fixes = cfvs, assumes = hcprems,
   2.234 +                             sgid = i, gth = gth}) solth = 
   2.235 +    let 
   2.236 +      val solth' = 
   2.237 +          solth |> Drule.implies_intr_list hcprems
   2.238 +                |> Drule.forall_intr_list cfvs
   2.239 +    in Drule.compose_single (solth', i, gth) end;
   2.240 +
   2.241 +val exports_solution = foldr (uncurry export_solution);
   2.242 +
   2.243 +
   2.244 +
   2.245 +
   2.246  (* fix parameters of a subgoal "i", as free variables, and create an
   2.247  exporting function that will use the result of this proved goal to
   2.248  show the goal in the original theorem. 
   2.249 @@ -45,6 +261,14 @@
   2.250  Note, an advantage of this over Isar is that it supports instantiation
   2.251  of unkowns in the earlier theorem, ie we can do instantiation of meta
   2.252  vars! *)
   2.253 +(* loosely corresponds to:
   2.254 +Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm
   2.255 +Result: 
   2.256 +  ("(As ==> SGi x') ==> (As ==> SGi x')" : thm, 
   2.257 +   expf : 
   2.258 +     ("As ==> SGi x'" : thm) -> 
   2.259 +     ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm)
   2.260 +*)
   2.261  fun fix_alls' i th = 
   2.262      let 
   2.263        val t = (prop_of th); 
   2.264 @@ -64,55 +288,75 @@
   2.265        
   2.266        (* Given a thm justifying subgoal i, solve subgoal i *)
   2.267        (* Note: fails if there are choices! *)
   2.268 -      fun exportf thi = 
   2.269 +      (* fun exportf thi = 
   2.270            Drule.compose_single (Drule.forall_intr_list cfvs thi, 
   2.271 -                                i, th)
   2.272 +                                i, th) *)
   2.273 +    in (gthi0, cfvs) end;
   2.274 +
   2.275 +(* small example: 
   2.276 +Goal "!! x. [| False; C x |] ==> P x";
   2.277 +val th = topthm();
   2.278 +val i = 1;
   2.279 +val (goalth, fixes) = fix_alls' i (topthm());
   2.280 +
   2.281 +Goal "!! x. P (x + (Suc y)) ==> Q ((Suc x) + y)";
   2.282 +Goal "!! x. P x y = Q y x ==> P x y";
   2.283 +val th = topthm();
   2.284 +val i = 1;
   2.285 +val (prems, gthi, expf) = IsaND.fixes_and_assumes i th;
   2.286 +val gth2 = Seq.hd (RWStepTac.rwstep_tac prems 1 gthi);
   2.287 +*)
   2.288 +
   2.289 +
   2.290 +(* hide other goals *) 
   2.291 +(* note the export goal is rotated by (i - 1) and will have to be
   2.292 +unrotated to get backto the originial position(s) *)
   2.293 +fun hide_other_goals th = 
   2.294 +    let
   2.295 +      (* tl beacuse fst sg is the goal we are interested in *)
   2.296 +      val cprems = tl (Drule.cprems_of th)
   2.297 +      val aprems = map Thm.assume cprems
   2.298      in
   2.299 -      (gthi0, exportf)
   2.300 +      (Drule.implies_elim_list (Drule.rotate_prems 1 th) aprems, 
   2.301 +       cprems)
   2.302 +    end;
   2.303 +(* test with: 
   2.304 +Goal "!! x. [| False; C x |] ==> P x";
   2.305 +val th = topthm();
   2.306 +val i = 1;
   2.307 +val (goalth, fixedvars) = IsaND.fix_alls' i th;
   2.308 +val (newth, hiddenprems) = IsaND.hide_other_goals goalth;
   2.309 +*)
   2.310 +
   2.311 +(* a nicer version of the above that leaves only a single subgoal (the
   2.312 +other subgoals are hidden hyps, that the exporter suffles about)
   2.313 +namely the subgoal that we were trying to solve. *)
   2.314 +(* loosely corresponds to:
   2.315 +Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm
   2.316 +Result: 
   2.317 +  ("(As ==> SGi x') ==> SGi x'" : thm, 
   2.318 +   expf : 
   2.319 +     ("SGi x'" : thm) -> 
   2.320 +     ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm)
   2.321 +*)
   2.322 +fun fix_alls i th = 
   2.323 +    let 
   2.324 +      val (fixed_gth, fixedvars) = fix_alls' i th
   2.325 +      val (sml_gth, othergoals) = hide_other_goals fixed_gth
   2.326 +    in
   2.327 +      (sml_gth, export {fixes = fixedvars, 
   2.328 +                        assumes = othergoals, 
   2.329 +                        sgid = i, gth = th})
   2.330      end;
   2.331  
   2.332  (* small example: 
   2.333  Goal "!! x. [| False; C x |] ==> P x";
   2.334  val th = topthm();
   2.335  val i = 1;
   2.336 -val (goalth, expf) = fix_alls i (topthm());
   2.337 -*)
   2.338 -
   2.339 -
   2.340 -(* a nicer version of the above that leaves only a single subgoal (the
   2.341 -other subgoals are hidden hyps, that the exporter suffles about)
   2.342 -namely the subgoal that we were trying to solve. *)
   2.343 -
   2.344 -fun fix_alls i th = 
   2.345 -    let 
   2.346 -      val (gthi, exportf) = fix_alls' i th
   2.347 -      val gthi' = Drule.rotate_prems 1 gthi
   2.348 -
   2.349 -      val sgn = Thm.sign_of_thm th;
   2.350 -      val ctermify = Thm.cterm_of sgn;
   2.351 +val (goalth, exp) = IsaND.fix_alls i th;
   2.352 +val oldthewth = Seq.list_of (IsaND.export_back exp goalth);
   2.353  
   2.354 -      val prems = tl (Thm.prems_of gthi)
   2.355 -      val cprems = map ctermify prems;
   2.356 -      val aprems = map Thm.assume cprems;
   2.357 -
   2.358 -      val exportf' = 
   2.359 -          exportf o (Drule.implies_intr_list cprems)
   2.360 -    in
   2.361 -      (Drule.implies_elim_list gthi' aprems, exportf')
   2.362 -    end;
   2.363 -
   2.364 -(* small example: 
   2.365 -Goal "P x";
   2.366 -val i = 1;
   2.367 -val th = topthm();
   2.368 -val x = fix_alls (topthm()) 1;
   2.369 -
   2.370 -Goal "!! x. [| False; C x |] ==> P x";
   2.371 -val th = topthm();
   2.372 -val i = 1;
   2.373 -val (goalth, expf) = fix_alls' th i;
   2.374 -
   2.375 -val (premths, goalth2, expf2) = assume_prems 1 goalth;
   2.376 +val (premths, goalth2, expf2) = IsaND.assume_prems 1 goalth;
   2.377  val False_th = nth_elem (0,premths);
   2.378  val anything = False_th RS (thm "FalseE");
   2.379  val th2 = anything RS goalth2;
   2.380 @@ -132,6 +376,14 @@
   2.381  shyps, which we can later instantiate with a specific value.... ? 
   2.382  think about this... maybe need to introduce some new fixed vars and
   2.383  then remove them again at the end... like I do with rw_inst. *)
   2.384 +(* loosely corresponds to:
   2.385 +Given "[| SG0; ... [| A0; ... An |] ==> SGi; ... SGm |] ==> G" : thm
   2.386 +Result: 
   2.387 +(["A0" [A0], ... ,"An" [An]] : thm list, -- assumptions
   2.388 + "SGi ==> SGi" : thm, -- new goal 
   2.389 + "SGi" ["A0" ... "An"] : thm ->   -- export function
   2.390 +    ("[| SG0 ... SGi-1, SGi+1, SGm |] ==> G" : thm) list)
   2.391 +*)
   2.392  fun assume_prems i th =
   2.393      let 
   2.394        val t = (prop_of th); 
   2.395 @@ -148,17 +400,17 @@
   2.396        val aprems = map Thm.assume cprems;
   2.397        val gthi = Thm.trivial (ctermify concl);
   2.398  
   2.399 -      fun explortf thi = 
   2.400 +      (* fun explortf thi = 
   2.401            Drule.compose (Drule.implies_intr_list cprems thi, 
   2.402 -                         i, th)
   2.403 +                         i, th) *)
   2.404      in
   2.405 -      (aprems, gthi, explortf)
   2.406 +      (aprems, gthi, cprems)
   2.407      end;
   2.408  (* small example: 
   2.409  Goal "False ==> b";
   2.410  val th = topthm();
   2.411  val i = 1;
   2.412 -val (prems, goalth, expf) = assume_prems i (topthm());
   2.413 +val (prems, goalth, cprems) = IsaND.assume_prems i (topthm());
   2.414  val F = hd prems;
   2.415  val FalseE = thm "FalseE";
   2.416  val anything = F RS FalseE;
   2.417 @@ -167,7 +419,57 @@
   2.418  *)
   2.419  
   2.420  
   2.421 -(* Fixme: allow different order of subgoals *)
   2.422 +(* first fix the variables, then assume the assumptions *)
   2.423 +(* loosely corresponds to:
   2.424 +Given 
   2.425 +  "[| SG0; ... 
   2.426 +      !! xs. [| A0 xs; ... An xs |] ==> SGi xs; 
   2.427 +      ... SGm |] ==> G" : thm
   2.428 +Result: 
   2.429 +(["A0 xs'" [A0 xs'], ... ,"An xs'" [An xs']] : thm list, -- assumptions
   2.430 + "SGi xs' ==> SGi xs'" : thm,  -- new goal 
   2.431 + "SGi xs'" ["A0 xs'" ... "An xs'"] : thm ->   -- export function
   2.432 +    ("[| SG0 ... SGi-1, SGi+1, SGm |] ==> G" : thm) list)
   2.433 +*)
   2.434 +
   2.435 +(* Note: the fix_alls actually pulls through all the assumptions which
   2.436 +means that the second export is not needed. *)
   2.437 +fun fixes_and_assumes i th = 
   2.438 +    let 
   2.439 +      val (fixgth, exp1) = fix_alls i th
   2.440 +      val (assumps, goalth, _) = assume_prems 1 fixgth
   2.441 +    in 
   2.442 +      (assumps, goalth, exp1)
   2.443 +    end;
   2.444 +(* test with: 
   2.445 +Goal "!! x. [| False; C x |] ==> P x";
   2.446 +val th = topthm();
   2.447 +val i = 1;
   2.448 +val (fixgth, exp) = IsaND.fix_alls i th;
   2.449 +val (assumps, goalth, _) = assume_prems 1 fixgth;
   2.450 +
   2.451 +val oldthewth = Seq.list_of (IsaND.export_back exp fixgth);
   2.452 +val oldthewth = Seq.list_of (IsaND.export_back exp goalth);
   2.453 +
   2.454 +
   2.455 +val (prems, goalth, expf) = IsaND.fixes_and_assumes i th;
   2.456 +val F = hd prems;
   2.457 +val FalseE = thm "FalseE";
   2.458 +val anything = F RS FalseE;
   2.459 +val thi = anything RS goalth;
   2.460 +val res' = expf thi;
   2.461 +*)
   2.462 +
   2.463 +(* Fixme: allow different order of subgoals given to expf *)
   2.464 +(* make each subgoal into a separate thm that needs to be proved *)
   2.465 +(* loosely corresponds to:
   2.466 +Given 
   2.467 +  "[| SG0; ... SGm |] ==> G" : thm
   2.468 +Result: 
   2.469 +(["SG0 ==> SG0", ... ,"SGm ==> SGm"] : thm list, -- goals
   2.470 + ["SG0", ..., "SGm"] : thm list ->   -- export function
   2.471 +   "G" : thm)
   2.472 +*)
   2.473  fun subgoal_thms th = 
   2.474      let 
   2.475        val t = (prop_of th); 
   2.476 @@ -195,6 +497,11 @@
   2.477  function, that will bring them back out at a later point. This is
   2.478  useful if you want to get back these premices, after having used the
   2.479  theorem with the premices hidden *)
   2.480 +(* loosely corresponds to:
   2.481 +Given "As ==> G" : thm
   2.482 +Result: ("G [As]" : thm, 
   2.483 +         "G [As]" : thm -> "As ==> G" : thm
   2.484 +*)
   2.485  fun hide_prems th = 
   2.486      let 
   2.487        val sgn = Thm.sign_of_thm th;
   2.488 @@ -205,29 +512,39 @@
   2.489        val cprems = map ctermify prems;
   2.490        val aprems = map Thm.trivial cprems;
   2.491  
   2.492 -      val unhidef = Drule.implies_intr_list cprems;
   2.493 +    (*   val unhidef = Drule.implies_intr_list cprems; *)
   2.494      in
   2.495 -      (Drule.implies_elim_list th aprems, unhidef)
   2.496 +      (Drule.implies_elim_list th aprems, cprems)
   2.497      end;
   2.498  
   2.499  
   2.500  
   2.501  
   2.502 -(* Fixme: allow different order of subgoals *)
   2.503 +(* Fixme: allow different order of subgoals in exportf *)
   2.504 +(* as above, but also fix all parameters in all subgoals, and uses
   2.505 +fix_alls, not fix_alls', ie doesn't leave extra asumptions as apparent
   2.506 +subgoals. *)
   2.507 +(* loosely corresponds to:
   2.508 +Given 
   2.509 +  "[| !! x0s. A0s x0s ==> SG0 x0s; 
   2.510 +      ...; !! xms. Ams xms ==> SGm xms|] ==> G" : thm
   2.511 +Result: 
   2.512 +(["(A0s x0s' ==> SG0 x0s') ==> SG0 x0s'", 
   2.513 +  ... ,"(Ams xms' ==> SGm xms') ==> SGm xms'"] : thm list, -- goals
   2.514 + ["SG0 x0s'", ..., "SGm xms'"] : thm list ->   -- export function
   2.515 +   "G" : thm)
   2.516 +*)
   2.517 +(* requires being given solutions! *)
   2.518  fun fixed_subgoal_thms th = 
   2.519      let 
   2.520        val (subgoals, expf) = subgoal_thms th;
   2.521 -
   2.522  (*       fun export_sg (th, exp) = exp th; *)
   2.523 -      fun export_sgs expfs ths = 
   2.524 -          expf (map2 (op |>) (ths, expfs));
   2.525 -
   2.526 +      fun export_sgs expfs solthms = 
   2.527 +          expf (map2 (op |>) (solthms, expfs));
   2.528  (*           expf (map export_sg (ths ~~ expfs)); *)
   2.529 -
   2.530 -
   2.531 -
   2.532      in 
   2.533 -      apsnd export_sgs (Library.split_list (map (fix_alls 1) subgoals))
   2.534 +      apsnd export_sgs (Library.split_list (map (apsnd export_solution o 
   2.535 +                                                 fix_alls 1) subgoals))
   2.536      end;
   2.537  
   2.538  
   2.539 @@ -238,4 +555,4 @@
   2.540  val (subgoals, expf) = fixed_subgoal_thms (topthm());
   2.541  *)
   2.542  
   2.543 -end;
   2.544 \ No newline at end of file
   2.545 +end;