1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/TFL/casesplit.ML	Fri Aug 20 12:20:09 2004 +0200
     1.3 @@ -0,0 +1,310 @@
     1.4 +(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
     1.5 +(*  Title:      TFL/casesplit.ML
     1.6 +    Author:     Lucas Dixon, University of Edinburgh
     1.7 +                lucas.dixon@ed.ac.uk
     1.8 +    Date:       17 Aug 2004
     1.9 +*)
    1.10 +(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
    1.11 +(*  DESCRIPTION:
    1.12 +
    1.13 +    A structure that defines a tactic to program case splits. 
    1.14 +
    1.15 +    casesplit_free :
    1.16 +      string * Term.type -> int -> Thm.thm -> Thm.thm Seq.seq
    1.17 +
    1.18 +    casesplit_name : 
    1.19 +      string -> int -> Thm.thm -> Thm.thm Seq.seq
    1.20 +
    1.21 +    These use the induction theorem associated with the recursive data
    1.22 +    type to be split. 
    1.23 +
    1.24 +    The structure includes a function to try and recursively split a
    1.25 +    conjecture into a list sub-theorems: 
    1.26 +
    1.27 +    splitto : Thm.thm list -> Thm.thm -> Thm.thm
    1.28 +*)
    1.29 +(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
    1.30 +
    1.31 +(* logic-specific *)
    1.32 +signature CASE_SPLIT_DATA =
    1.33 +sig
    1.34 +  val dest_Trueprop : Term.term -> Term.term
    1.35 +  val mk_Trueprop : Term.term -> Term.term
    1.36 +  val read_cterm : Sign.sg -> string -> Thm.cterm
    1.37 +end;
    1.38 +
    1.39 +(* for HOL *)
    1.40 +structure CaseSplitData_HOL : CASE_SPLIT_DATA = 
    1.41 +struct
    1.42 +val dest_Trueprop = HOLogic.dest_Trueprop;
    1.43 +val mk_Trueprop = HOLogic.mk_Trueprop;
    1.44 +val read_cterm = HOLogic.read_cterm;
    1.45 +end;
    1.46 +
    1.47 +
    1.48 +signature CASE_SPLIT =
    1.49 +sig
    1.50 +  (* failure to find a free to split on *)
    1.51 +  exception find_split_exp of string
    1.52 +
    1.53 +  (* getting a case split thm from the induction thm *)
    1.54 +  val case_thm_of_ty : Sign.sg -> Term.typ -> Thm.thm
    1.55 +  val cases_thm_of_induct_thm : Thm.thm -> Thm.thm
    1.56 +
    1.57 +  (* case split tactics *)
    1.58 +  val casesplit_free :
    1.59 +      string * Term.typ -> int -> Thm.thm -> Thm.thm Seq.seq
    1.60 +  val casesplit_name : string -> int -> Thm.thm -> Thm.thm Seq.seq
    1.61 +
    1.62 +  (* finding a free var to split *)
    1.63 +  val find_term_split :
    1.64 +      Term.term * Term.term -> (string * Term.typ) Library.option
    1.65 +  val find_thm_split :
    1.66 +      Thm.thm -> int -> Thm.thm -> (string * Term.typ) Library.option
    1.67 +  val find_thms_split :
    1.68 +      Thm.thm list -> int -> Thm.thm -> (string * Term.typ) Library.option
    1.69 +
    1.70 +  (* try to recursively split conjectured thm to given list of thms *)
    1.71 +  val splitto : Thm.thm list -> Thm.thm -> Thm.thm
    1.72 +
    1.73 +  (* for use with the recdef package *)
    1.74 +  val derive_init_eqs :
    1.75 +      Sign.sg ->
    1.76 +      (Thm.thm * int) list -> Term.term list -> (Thm.thm * int) list
    1.77 +end;
    1.78 +
    1.79 +functor CaseSplitFUN(Data : CASE_SPLIT_DATA) =
    1.80 +struct
    1.81 +
    1.82 +(* beta-eta contract the theorem *)
    1.83 +fun beta_eta_contract thm = 
    1.84 +    let
    1.85 +      val thm2 = equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm
    1.86 +      val thm3 = equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2
    1.87 +    in thm3 end;
    1.88 +
    1.89 +(* make a casethm from an induction thm *)
    1.90 +val cases_thm_of_induct_thm = 
    1.91 +     Seq.hd o (ALLGOALS (fn i => REPEAT (etac Drule.thin_rl i)));
    1.92 +
    1.93 +(* get the case_thm (my version) from a type *)
    1.94 +fun case_thm_of_ty sgn ty  = 
    1.95 +    let 
    1.96 +      val dtypestab = DatatypePackage.get_datatypes_sg sgn;
    1.97 +      val ty_str = case ty of 
    1.98 +                     Type(ty_str, _) => ty_str
    1.99 +                   | TFree(s,_)  => raise ERROR_MESSAGE 
   1.100 +                                            ("Free type: " ^ s)   
   1.101 +                   | TVar((s,i),_) => raise ERROR_MESSAGE 
   1.102 +                                            ("Free variable: " ^ s)   
   1.103 +      val dt = case (Symtab.lookup (dtypestab,ty_str))
   1.104 +                of Some dt => dt
   1.105 +                 | None => raise ERROR_MESSAGE ("Not a Datatype: " ^ ty_str)
   1.106 +    in
   1.107 +      cases_thm_of_induct_thm (#induction dt)
   1.108 +    end;
   1.109 +
   1.110 +(* 
   1.111 + val ty = (snd o hd o map Term.dest_Free o Term.term_frees) t;  
   1.112 +*)
   1.113 +
   1.114 +
   1.115 +(* for use when there are no prems to the subgoal *)
   1.116 +(* does a case split on the given variable *)
   1.117 +fun mk_casesplit_goal_thm sgn (vstr,ty) gt = 
   1.118 +    let 
   1.119 +      val x = Free(vstr,ty)
   1.120 +      val abst = Abs(vstr, ty, Term.abstract_over (x, gt));
   1.121 +
   1.122 +      val ctermify = Thm.cterm_of sgn;
   1.123 +      val ctypify = Thm.ctyp_of sgn;
   1.124 +      val case_thm = case_thm_of_ty sgn ty;
   1.125 +
   1.126 +      val abs_ct = ctermify abst;
   1.127 +      val free_ct = ctermify x;
   1.128 +
   1.129 +      val casethm_vars = rev (Term.term_vars (Thm.concl_of case_thm));
   1.130 +       
   1.131 +      val tsig = Sign.tsig_of sgn;
   1.132 +      val casethm_tvars = Term.term_tvars (Thm.concl_of case_thm);
   1.133 +      val (Pv, Dv, type_insts) = 
   1.134 +          case (Thm.concl_of case_thm) of 
   1.135 +            (_ $ ((Pv as Var(P,Pty)) $ (Dv as Var(D, Dty)))) => 
   1.136 +            (Pv, Dv, 
   1.137 +             Vartab.dest (Type.typ_match tsig (Vartab.empty, (Dty, ty))))
   1.138 +          | _ => raise ERROR_MESSAGE ("not a valid case thm");
   1.139 +      val type_cinsts = map (apsnd ctypify) type_insts;
   1.140 +      val cPv = ctermify (Sign.inst_term_tvars sgn type_insts Pv);
   1.141 +      val cDv = ctermify (Sign.inst_term_tvars sgn type_insts Dv);
   1.142 +    in
   1.143 +      (beta_eta_contract 
   1.144 +         (case_thm
   1.145 +            |> Thm.instantiate (type_cinsts, []) 
   1.146 +            |> Thm.instantiate ([], [(cPv, abs_ct), (cDv, free_ct)])))
   1.147 +    end;
   1.148 +
   1.149 +
   1.150 +(* for use when there are no prems to the subgoal *)
   1.151 +(* does a case split on the given variable (Free fv) *)
   1.152 +fun casesplit_free fv i th = 
   1.153 +    let 
   1.154 +      val gt = Data.dest_Trueprop (nth_elem( i - 1, Thm.prems_of th));
   1.155 +      val sgn = Thm.sign_of_thm th;
   1.156 +    in 
   1.157 +      Tactic.rtac (mk_casesplit_goal_thm sgn fv gt) i th
   1.158 +    end;
   1.159 +
   1.160 +(* for use when there are no prems to the subgoal *)
   1.161 +(* does a case split on the given variable *)
   1.162 +fun casesplit_name vstr i th = 
   1.163 +    let 
   1.164 +      val gt = Data.dest_Trueprop (nth_elem( i - 1, Thm.prems_of th));
   1.165 +      val freets = Term.term_frees gt;
   1.166 +      fun getter x = let val (n,ty) = Term.dest_Free x in 
   1.167 +                       if vstr = n then Some (n,ty) else None end;
   1.168 +      val (n,ty) = case Library.get_first getter freets 
   1.169 +                of Some (n, ty) => (n, ty)
   1.170 +                 | _ => raise ERROR_MESSAGE ("no such variable " ^ vstr);
   1.171 +      val sgn = Thm.sign_of_thm th;
   1.172 +    in 
   1.173 +      Tactic.rtac (mk_casesplit_goal_thm sgn (n,ty) gt) i th
   1.174 +    end;
   1.175 +
   1.176 +
   1.177 +(* small example: 
   1.178 +Goal "P (x :: nat) & (C y --> Q (y :: nat))";
   1.179 +by (rtac (thm "conjI") 1);
   1.180 +val th = topthm();
   1.181 +val i = 2;
   1.182 +val vstr = "y";
   1.183 +
   1.184 +by (casesplit_name "y" 2);
   1.185 +
   1.186 +val th = topthm();
   1.187 +val i = 1;
   1.188 +val th' = casesplit_name "x" i th;
   1.189 +*)
   1.190 +
   1.191 +
   1.192 +(* the find_XXX_split functions are simply doing a lightwieght (I
   1.193 +think) term matching equivalent to find where to do the next split *)
   1.194 +
   1.195 +(* assuming two twems are identical except for a free in one at a
   1.196 +subterm, or constant in another, ie assume that one term is a plit of
   1.197 +another, then gives back the free variable that has been split. *)
   1.198 +exception find_split_exp of string
   1.199 +fun find_term_split (Free v, _ $ _) = Some v
   1.200 +  | find_term_split (Free v, Const _) = Some v
   1.201 +  | find_term_split (Free v, Abs _) = Some v (* do we really want this case? *)
   1.202 +  | find_term_split (a $ b, a2 $ b2) = 
   1.203 +    (case find_term_split (a, a2) of 
   1.204 +       None => find_term_split (b,b2)  
   1.205 +     | vopt => vopt)
   1.206 +  | find_term_split (Abs(_,ty,t1), Abs(_,ty2,t2)) = 
   1.207 +    find_term_split (t1, t2)
   1.208 +  | find_term_split (Const (x,ty), Const(x2,ty2)) = 
   1.209 +    if x = x2 then None else (* keep searching *)
   1.210 +    raise find_split_exp (* stop now *)
   1.211 +            "Terms are not identical upto a free varaible! (Consts)"
   1.212 +  | find_term_split (Bound i, Bound j) =     
   1.213 +    if i = j then None else (* keep searching *)
   1.214 +    raise find_split_exp (* stop now *)
   1.215 +            "Terms are not identical upto a free varaible! (Bound)"
   1.216 +  | find_term_split (a, b) = 
   1.217 +    raise find_split_exp (* stop now *)
   1.218 +            "Terms are not identical upto a free varaible! (Other)";
   1.219 +
   1.220 +(* assume that "splitth" is a case split form of subgoal i of "genth",
   1.221 +then look for a free variable to split, breaking the subgoal closer to
   1.222 +splitth. *)
   1.223 +fun find_thm_split splitth i genth =
   1.224 +    find_term_split (Logic.get_goal (Thm.prop_of genth) i, 
   1.225 +                     Thm.concl_of splitth) handle find_split_exp _ => None;
   1.226 +
   1.227 +(* as above but searches "splitths" for a theorem that suggest a case split *)
   1.228 +fun find_thms_split splitths i genth =
   1.229 +    Library.get_first (fn sth => find_thm_split sth i genth) splitths;
   1.230 +
   1.231 +
   1.232 +(* split the subgoal i of "genth" until we get to a member of
   1.233 +splitths. Assumes that genth will be a general form of splitths, that
   1.234 +can be case-split, as needed. Otherwise fails. Note: We assume that
   1.235 +all of "splitths" are aplit to the same level, and thus it doesn't
   1.236 +matter which one we choose to look for the next split. Simply add
   1.237 +search on splitthms and plit variable, to change this.  *)
   1.238 +(* Note: possible efficiency measure: when a case theorem is no longer
   1.239 +useful, drop it? *)
   1.240 +(* Note: This should not be a separate tactic but integrated into the
   1.241 +case split done during recdef's case analysis, this would avoid us
   1.242 +having to (re)search for variables to split. *)
   1.243 +fun splitto splitths genth = 
   1.244 +    let 
   1.245 +      val _ = assert (not (null splitths)) "splitto: no given splitths";
   1.246 +      val sgn = Thm.sign_of_thm genth;
   1.247 +
   1.248 +      (* check if we are a member of splitths - FIXME: quicker and 
   1.249 +      more flexible with discrim net. *)
   1.250 +      fun solve_by_splitth th split = biresolution false [(false,split)] 1 th;
   1.251 +
   1.252 +      fun split th = 
   1.253 +          (case find_thms_split splitths 1 th of 
   1.254 +             None => raise ERROR_MESSAGE "splitto: cannot find variable to split on"
   1.255 +            | Some v => 
   1.256 +             let 
   1.257 +               val gt = Data.dest_Trueprop (nth_elem(0, Thm.prems_of th));
   1.258 +               val split_thm = mk_casesplit_goal_thm sgn v gt;
   1.259 +               val (subthms, expf) = IsaND.fixed_subgoal_thms split_thm;
   1.260 +             in 
   1.261 +               expf (map recsplitf subthms)
   1.262 +             end)
   1.263 +
   1.264 +      and recsplitf th = 
   1.265 +          (* note: multiple unifiers! we only take the first element,
   1.266 +             probably fine -- there is probably only one anyway. *)
   1.267 +          (case Library.get_first (Seq.pull o solve_by_splitth th) splitths of
   1.268 +             None => split th
   1.269 +           | Some (solved_th, more) => solved_th)
   1.270 +    in
   1.271 +      recsplitf genth
   1.272 +    end;
   1.273 +
   1.274 +
   1.275 +(* Note: We dont do this if wf conditions fail to be solved, as each
   1.276 +case may have a different wf condition - we could group the conditions
   1.277 +togeather and say that they must be true to solve the general case,
   1.278 +but that would hide from the user which sub-case they were related
   1.279 +to. Probably this is not important, and it would work fine, but I
   1.280 +prefer leaving more fine grain control to the user. *)
   1.281 +
   1.282 +(* derive eqs, assuming strict, ie the rules have no assumptions = all
   1.283 +   the well-foundness conditions have been solved. *)
   1.284 +local
   1.285 +  fun get_related_thms i = 
   1.286 +      mapfilter ((fn (r,x) => if x = i then Some r else None));
   1.287 +      
   1.288 +  fun solve_eq (th, [], i) = 
   1.289 +      raise ERROR_MESSAGE "derive_init_eqs: missing rules"
   1.290 +    | solve_eq (th, [a], i) = (a, i)
   1.291 +    | solve_eq (th, splitths as (_ :: _), i) = (splitto splitths th,i);
   1.292 +in
   1.293 +fun derive_init_eqs sgn rules eqs = 
   1.294 +    let 
   1.295 +      val eqths = map (Thm.trivial o (Thm.cterm_of sgn) o Data.mk_Trueprop) 
   1.296 +                      eqs
   1.297 +    in
   1.298 +      (rev o map solve_eq)
   1.299 +        (Library.foldln 
   1.300 +           (fn (e,i) => 
   1.301 +               (curry (op ::)) (e, (get_related_thms (i - 1) rules), i - 1)) 
   1.302 +           eqths [])
   1.303 +    end;
   1.304 +end;
   1.305 +(* 
   1.306 +    val (rs_hwfc, unhidefs) = Library.split_list (map hide_prems rules)
   1.307 +    (map2 (op |>) (ths, expfs))
   1.308 +*)
   1.309 +
   1.310 +end;
   1.311 +
   1.312 +
   1.313 +structure CaseSplit = CaseSplitFUN(CaseSplitData_HOL);

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/TFL/isand.ML	Fri Aug 20 12:20:09 2004 +0200
     2.3 @@ -0,0 +1,241 @@
     2.4 +(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
     2.5 +(*  Title:      TFL/isand.ML
     2.6 +    Author:     Lucas Dixon, University of Edinburgh
     2.7 +                lucas.dixon@ed.ac.uk
     2.8 +    Date:       6 Aug 2004
     2.9 +*)
    2.10 +(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
    2.11 +(*  DESCRIPTION:
    2.12 +
    2.13 +    Natural Deduction tools
    2.14 +
    2.15 +    For working with Isbaelle theorem in a natural detuction style,
    2.16 +    ie, not having to deal with meta level quantified varaibles,
    2.17 +    instead, we work with newly introduced frees, and hide the
    2.18 +    "all"'s, exporting results from theorems proved with the frees, to
    2.19 +    solve the all cases of the previous goal. 
    2.20 +
    2.21 +    Note: A nice idea: allow esxporting to solve any subgoal, thus
    2.22 +    allowing the interleaving of proof, or provide a structure for the
    2.23 +    ordering of proof, thus allowing proof attempts in parrelle, but
    2.24 +    recording the order to apply things in.
    2.25 +*)
    2.26 +
    2.27 +structure IsaND =
    2.28 +struct
    2.29 +
    2.30 +(* Solve *some* subgoal of "th" directly by "sol" *)
    2.31 +(* Note: this is probably what Markus ment to do upon export of a
    2.32 +"show" but maybe he used RS/rtac intead, which would wrongly lead to
    2.33 +failing if there are premices to the shown goal. *)
    2.34 +fun solve_with sol th = 
    2.35 +    let fun solvei 0 = Seq.empty
    2.36 +          | solvei i = 
    2.37 +            Seq.append (bicompose false (false,sol,0) i th, 
    2.38 +                        solvei (i - 1))
    2.39 +    in
    2.40 +      solvei (Thm.nprems_of th)
    2.41 +    end;
    2.42 +
    2.43 +
    2.44 +(* fix parameters of a subgoal "i", as free variables, and create an
    2.45 +exporting function that will use the result of this proved goal to
    2.46 +show the goal in the original theorem. 
    2.47 +
    2.48 +Note, an advantage of this over Isar is that it supports instantiation
    2.49 +of unkowns in the earlier theorem, ie we can do instantiation of meta
    2.50 +vars! *)
    2.51 +fun fix_alls' i th = 
    2.52 +    let 
    2.53 +      val t = (prop_of th); 
    2.54 +      val names = Term.add_term_names (t,[]);
    2.55 +      val gt = Logic.get_goal t i;
    2.56 +      val body = Term.strip_all_body gt;
    2.57 +      val alls = rev (Term.strip_all_vars gt);
    2.58 +      val fvs = map Free 
    2.59 +                    ((Term.variantlist (map fst alls, names)) 
    2.60 +                       ~~ (map snd alls));
    2.61 +      val sgn = Thm.sign_of_thm th;
    2.62 +      val ctermify = Thm.cterm_of sgn;
    2.63 +      val cfvs = rev (map ctermify fvs);
    2.64 +
    2.65 +      val body' = (subst_bounds (fvs,body));
    2.66 +      val gthi0 = Thm.trivial (ctermify body');
    2.67 +      
    2.68 +      (* Given a thm justifying subgoal i, solve subgoal i *)
    2.69 +      (* Note: fails if there are choices! *)
    2.70 +      fun exportf thi = 
    2.71 +          Drule.compose_single (Drule.forall_intr_list cfvs thi, 
    2.72 +                                i, th)
    2.73 +    in
    2.74 +      (gthi0, exportf)
    2.75 +    end;
    2.76 +
    2.77 +(* small example: 
    2.78 +Goal "!! x. [| False; C x |] ==> P x";
    2.79 +val th = topthm();
    2.80 +val i = 1;
    2.81 +val (goalth, expf) = fix_alls i (topthm());
    2.82 +*)
    2.83 +
    2.84 +
    2.85 +(* a nicer version of the above that leaves only a single subgoal (the
    2.86 +other subgoals are hidden hyps, that the exporter suffles about)
    2.87 +namely the subgoal that we were trying to solve. *)
    2.88 +
    2.89 +fun fix_alls i th = 
    2.90 +    let 
    2.91 +      val (gthi, exportf) = fix_alls' i th
    2.92 +      val gthi' = Drule.rotate_prems 1 gthi
    2.93 +
    2.94 +      val sgn = Thm.sign_of_thm th;
    2.95 +      val ctermify = Thm.cterm_of sgn;
    2.96 +
    2.97 +      val prems = tl (Thm.prems_of gthi)
    2.98 +      val cprems = map ctermify prems;
    2.99 +      val aprems = map Thm.assume cprems;
   2.100 +
   2.101 +      val exportf' = 
   2.102 +          exportf o (Drule.implies_intr_list cprems)
   2.103 +    in
   2.104 +      (Drule.implies_elim_list gthi' aprems, exportf')
   2.105 +    end;
   2.106 +
   2.107 +(* small example: 
   2.108 +Goal "P x";
   2.109 +val i = 1;
   2.110 +val th = topthm();
   2.111 +val x = fix_alls (topthm()) 1;
   2.112 +
   2.113 +Goal "!! x. [| False; C x |] ==> P x";
   2.114 +val th = topthm();
   2.115 +val i = 1;
   2.116 +val (goalth, expf) = fix_alls' th i;
   2.117 +
   2.118 +val (premths, goalth2, expf2) = assume_prems 1 goalth;
   2.119 +val False_th = nth_elem (0,premths);
   2.120 +val anything = False_th RS (thm "FalseE");
   2.121 +val th2 = anything RS goalth2;
   2.122 +val th1 = expf2 th2;
   2.123 +val final_th = flat (map expf th1);
   2.124 +*)
   2.125 +
   2.126 +
   2.127 +(* assume the premises of subgoal "i", this gives back a list of
   2.128 +assumed theorems that are the premices of subgoal i, it also gives
   2.129 +back a new goal thm and an exporter, the new goalthm is as the old
   2.130 +one, but without the premices, and the exporter will use a proof of
   2.131 +the new goalthm, possibly using the assumed premices, to shoe the
   2.132 +orginial goal. *)
   2.133 +
   2.134 +(* Note: Dealing with meta vars, need to meta-level-all them in the
   2.135 +shyps, which we can later instantiate with a specific value.... ? 
   2.136 +think about this... maybe need to introduce some new fixed vars and
   2.137 +then remove them again at the end... like I do with rw_inst. *)
   2.138 +fun assume_prems i th =
   2.139 +    let 
   2.140 +      val t = (prop_of th); 
   2.141 +      val gt = Logic.get_goal t i;
   2.142 +      val _ = case Term.strip_all_vars gt of [] => () 
   2.143 +              | _ => raise ERROR_MESSAGE "assume_prems: goal has params"
   2.144 +      val body = gt;
   2.145 +      val prems = Logic.strip_imp_prems body;
   2.146 +      val concl = Logic.strip_imp_concl body;
   2.147 +
   2.148 +      val sgn = Thm.sign_of_thm th;
   2.149 +      val ctermify = Thm.cterm_of sgn;
   2.150 +      val cprems = map ctermify prems;
   2.151 +      val aprems = map Thm.assume cprems;
   2.152 +      val gthi = Thm.trivial (ctermify concl);
   2.153 +
   2.154 +      fun explortf thi = 
   2.155 +          Drule.compose (Drule.implies_intr_list cprems thi, 
   2.156 +                         i, th)
   2.157 +    in
   2.158 +      (aprems, gthi, explortf)
   2.159 +    end;
   2.160 +(* small example: 
   2.161 +Goal "False ==> b";
   2.162 +val th = topthm();
   2.163 +val i = 1;
   2.164 +val (prems, goalth, expf) = assume_prems i (topthm());
   2.165 +val F = hd prems;
   2.166 +val FalseE = thm "FalseE";
   2.167 +val anything = F RS FalseE;
   2.168 +val thi = anything RS goalth;
   2.169 +val res' = expf thi;
   2.170 +*)
   2.171 +
   2.172 +
   2.173 +(* Fixme: allow different order of subgoals *)
   2.174 +fun subgoal_thms th = 
   2.175 +    let 
   2.176 +      val t = (prop_of th); 
   2.177 +
   2.178 +      val prems = Logic.strip_imp_prems t;
   2.179 +
   2.180 +      val sgn = Thm.sign_of_thm th;
   2.181 +      val ctermify = Thm.cterm_of sgn;
   2.182 +
   2.183 +      val aprems = map (Thm.trivial o ctermify) prems;
   2.184 +
   2.185 +      fun explortf premths = 
   2.186 +          Drule.implies_elim_list th premths
   2.187 +    in
   2.188 +      (aprems, explortf)
   2.189 +    end;
   2.190 +(* small example: 
   2.191 +Goal "A & B";
   2.192 +by (rtac conjI 1);
   2.193 +val th = topthm();
   2.194 +val (subgoals, expf) = subgoal_thms (topthm());
   2.195 +*)
   2.196 +
   2.197 +(* make all the premices of a theorem hidden, and provide an unhide
   2.198 +function, that will bring them back out at a later point. This is
   2.199 +useful if you want to get back these premices, after having used the
   2.200 +theorem with the premices hidden *)
   2.201 +fun hide_prems th = 
   2.202 +    let 
   2.203 +      val sgn = Thm.sign_of_thm th;
   2.204 +      val ctermify = Thm.cterm_of sgn;
   2.205 +
   2.206 +      val t = (prop_of th);
   2.207 +      val prems = Logic.strip_imp_prems t;
   2.208 +      val cprems = map ctermify prems;
   2.209 +      val aprems = map Thm.trivial cprems;
   2.210 +
   2.211 +      val unhidef = Drule.implies_intr_list cprems;
   2.212 +    in
   2.213 +      (Drule.implies_elim_list th aprems, unhidef)
   2.214 +    end;
   2.215 +
   2.216 +
   2.217 +
   2.218 +
   2.219 +(* Fixme: allow different order of subgoals *)
   2.220 +fun fixed_subgoal_thms th = 
   2.221 +    let 
   2.222 +      val (subgoals, expf) = subgoal_thms th;
   2.223 +
   2.224 +(*       fun export_sg (th, exp) = exp th; *)
   2.225 +      fun export_sgs expfs ths = 
   2.226 +          expf (map2 (op |>) (ths, expfs));
   2.227 +
   2.228 +(*           expf (map export_sg (ths ~~ expfs)); *)
   2.229 +
   2.230 +
   2.231 +
   2.232 +    in 
   2.233 +      apsnd export_sgs (Library.split_list (map (fix_alls 1) subgoals))
   2.234 +    end;
   2.235 +
   2.236 +
   2.237 +(* small example: 
   2.238 +Goal "(!! x. ((C x) ==> (A x)))";
   2.239 +val th = topthm();
   2.240 +val i = 1;
   2.241 +val (subgoals, expf) = fixed_subgoal_thms (topthm());
   2.242 +*)
   2.243 +
   2.244 +end;
   2.245 \ No newline at end of file

     3.1 --- a/TFL/post.ML	Thu Aug 19 12:35:45 2004 +0200
     3.2 +++ b/TFL/post.ML	Fri Aug 20 12:20:09 2004 +0200
     3.3 @@ -195,6 +195,42 @@
     3.4                 error (mesg ^
     3.5                        "\n    (In TFL function " ^ module ^ "." ^ func ^ ")");
     3.6  
     3.7 +
     3.8 +(* Derive the initial equations from the case-split rules to meet the
     3.9 +users specification of the recursive function. 
    3.10 + Note: We don't do this if the wf conditions fail to be solved, as each
    3.11 +case may have a different wf condition. We could group the conditions
    3.12 +together and say that they must be true to solve the general case,
    3.13 +but that would hide from the user which sub-case they were related
    3.14 +to. Probably this is not important, and it would work fine, but, for now, I
    3.15 +prefer leaving more fine-grain control to the user. *)
    3.16 +local
    3.17 +  fun get_related_thms i = 
    3.18 +      mapfilter ((fn (r,x) => if x = i then Some r else None));
    3.19 +
    3.20 +  fun solve_eq (th, [], i) = 
    3.21 +      raise ERROR_MESSAGE "derive_init_eqs: missing rules"
    3.22 +    | solve_eq (th, [a], i) = [(a, i)]
    3.23 +    | solve_eq (th, splitths as (_ :: _), i) = 
    3.24 +      [((standard o ObjectLogic.rulify_no_asm)
    3.25 +          (CaseSplit.splitto splitths th), i)]
    3.26 +      (* if there's an error, pretend nothing happened with this definition 
    3.27 +         We should probably print something out so that the user knows...? *)
    3.28 +      handle ERROR_MESSAGE _ => map (fn x => (x,i)) splitths; 
    3.29 +in
    3.30 +fun derive_init_eqs sgn rules eqs = 
    3.31 +    let 
    3.32 +      val eqths = map (Thm.trivial o (Thm.cterm_of sgn) o HOLogic.mk_Trueprop) 
    3.33 +                      eqs
    3.34 +      fun countlist l = 
    3.35 +          (rev o snd o (foldl (fn ((i,L), e) => (i + 1,(e,i) :: L)))) ((0,[]), l)
    3.36 +    in
    3.37 +      flat (map (fn (e,i) => solve_eq (e, (get_related_thms i rules), i))
    3.38 +                (countlist eqths))
    3.39 +    end;
    3.40 +end;
    3.41 +
    3.42 +
    3.43  (*---------------------------------------------------------------------------
    3.44   * Defining a function with an associated termination relation.
    3.45   *---------------------------------------------------------------------------*)

     4.1 --- a/src/HOL/IsaMakefile	Thu Aug 19 12:35:45 2004 +0200
     4.2 +++ b/src/HOL/IsaMakefile	Fri Aug 20 12:20:09 2004 +0200
     4.3 @@ -80,7 +80,8 @@
     4.4    $(SRC)/Provers/quasi.ML \
     4.5    $(SRC)/Provers/simplifier.ML $(SRC)/Provers/splitter.ML \
     4.6    $(SRC)/Provers/trancl.ML \
     4.7 -  $(SRC)/TFL/dcterm.ML $(SRC)/TFL/post.ML $(SRC)/TFL/rules.ML \
     4.8 +  $(SRC)/TFL/isand.ML $(SRC)/TFL/casesplit.ML $(SRC)/TFL/dcterm.ML\
     4.9 +  $(SRC)/TFL/post.ML $(SRC)/TFL/rules.ML \
    4.10    $(SRC)/TFL/tfl.ML $(SRC)/TFL/thms.ML $(SRC)/TFL/thry.ML \
    4.11    $(SRC)/TFL/usyntax.ML $(SRC)/TFL/utils.ML \
    4.12    Datatype.thy Datatype_Universe.ML Datatype_Universe.thy \
    4.13 @@ -96,7 +97,8 @@
    4.14    Nat.thy NatArith.ML NatArith.thy \
    4.15    Power.thy PreList.thy Product_Type.ML Product_Type.thy \
    4.16    Refute.thy ROOT.ML \
    4.17 -  Recdef.thy Record.thy Relation.ML Relation.thy Relation_Power.ML \
    4.18 +  Recdef.thy Reconstruction.thy Record.thy\
    4.19 +  Relation.ML Relation.thy Relation_Power.ML \
    4.20    Relation_Power.thy LOrder.thy OrderedGroup.thy OrderedGroup.ML Ring_and_Field.thy\
    4.21    Set.ML Set.thy SetInterval.ML SetInterval.thy \
    4.22    Sum_Type.ML Sum_Type.thy Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \
    4.23 @@ -107,7 +109,7 @@
    4.24    Tools/primrec_package.ML \
    4.25    Tools/prop_logic.ML \
    4.26    Tools/recdef_package.ML Tools/recfun_codegen.ML \
    4.27 -  Tools/record_package.ML \
    4.28 +  Tools/record_package.ML Tools/reconstruction.ML\
    4.29    Tools/refute.ML Tools/refute_isar.ML \
    4.30    Tools/rewrite_hol_proof.ML \
    4.31    Tools/sat_solver.ML \

     5.1 --- a/src/HOL/Recdef.thy	Thu Aug 19 12:35:45 2004 +0200
     5.2 +++ b/src/HOL/Recdef.thy	Fri Aug 20 12:20:09 2004 +0200
     5.3 @@ -8,6 +8,8 @@
     5.4  theory Recdef
     5.5  imports Wellfounded_Relations Datatype
     5.6  files
     5.7 +  ("../TFL/isand.ML")
     5.8 +  ("../TFL/casesplit.ML")
     5.9    ("../TFL/utils.ML")
    5.10    ("../TFL/usyntax.ML")
    5.11    ("../TFL/dcterm.ML")
    5.12 @@ -43,6 +45,8 @@
    5.13  lemma tfl_exE: "\<exists>x. P x ==> \<forall>x. P x --> Q ==> Q"
    5.14    by blast
    5.15  
    5.16 +use "../TFL/isand.ML"
    5.17 +use "../TFL/casesplit.ML"
    5.18  use "../TFL/utils.ML"
    5.19  use "../TFL/usyntax.ML"
    5.20  use "../TFL/dcterm.ML"