eliminated some old material that is unused in the visible universe;
authorwenzelm
Wed Sep 12 22:00:29 2012 +0200 (2012-09-12)
changeset 49339d1fcb4de8349
parent 49338 4a922800531d
child 49340 25fc6e0da459
child 49341 d406979024d1
eliminated some old material that is unused in the visible universe;
src/FOL/IFOL.thy
src/HOL/HOL.thy
src/Tools/IsaPlanner/isand.ML
src/Tools/IsaPlanner/rw_inst.ML
src/Tools/IsaPlanner/rw_tools.ML
src/Tools/eqsubst.ML
     1.1 --- a/src/FOL/IFOL.thy	Wed Sep 12 17:26:05 2012 +0200
     1.2 +++ b/src/FOL/IFOL.thy	Wed Sep 12 22:00:29 2012 +0200
     1.3 @@ -13,7 +13,6 @@
     1.4  ML_file "~~/src/Provers/hypsubst.ML"
     1.5  ML_file "~~/src/Tools/IsaPlanner/zipper.ML"
     1.6  ML_file "~~/src/Tools/IsaPlanner/isand.ML"
     1.7 -ML_file "~~/src/Tools/IsaPlanner/rw_tools.ML"
     1.8  ML_file "~~/src/Tools/IsaPlanner/rw_inst.ML"
     1.9  ML_file "~~/src/Tools/eqsubst.ML"
    1.10  ML_file "~~/src/Provers/quantifier1.ML"
     2.1 --- a/src/HOL/HOL.thy	Wed Sep 12 17:26:05 2012 +0200
     2.2 +++ b/src/HOL/HOL.thy	Wed Sep 12 22:00:29 2012 +0200
     2.3 @@ -18,7 +18,6 @@
     2.4  ML_file "~~/src/Tools/solve_direct.ML"
     2.5  ML_file "~~/src/Tools/IsaPlanner/zipper.ML"
     2.6  ML_file "~~/src/Tools/IsaPlanner/isand.ML"
     2.7 -ML_file "~~/src/Tools/IsaPlanner/rw_tools.ML"
     2.8  ML_file "~~/src/Tools/IsaPlanner/rw_inst.ML"
     2.9  ML_file "~~/src/Provers/hypsubst.ML"
    2.10  ML_file "~~/src/Provers/splitter.ML"
     3.1 --- a/src/Tools/IsaPlanner/isand.ML	Wed Sep 12 17:26:05 2012 +0200
     3.2 +++ b/src/Tools/IsaPlanner/isand.ML	Wed Sep 12 22:00:29 2012 +0200
     3.3 @@ -8,7 +8,7 @@
     3.4  instead, we work with newly introduced frees, and hide the
     3.5  "all"'s, exporting results from theorems proved with the frees, to
     3.6  solve the all cases of the previous goal. This allows resolution
     3.7 -to do proof search normally. 
     3.8 +to do proof search normally.
     3.9  
    3.10  Note: A nice idea: allow exporting to solve any subgoal, thus
    3.11  allowing the interleaving of proof, or provide a structure for the
    3.12 @@ -23,113 +23,35 @@
    3.13  
    3.14  signature ISA_ND =
    3.15  sig
    3.16 -
    3.17 -  (* export data *)
    3.18 -  datatype export = export of
    3.19 -           {gth: Thm.thm, (* initial goal theorem *)
    3.20 -            sgid: int, (* subgoal id which has been fixed etc *)
    3.21 -            fixes: Thm.cterm list, (* frees *)
    3.22 -            assumes: Thm.cterm list} (* assumptions *)
    3.23 -  val fixes_of_exp : export -> Thm.cterm list
    3.24 -  val export_back : export -> Thm.thm -> Thm.thm Seq.seq
    3.25 -  val export_solution : export -> Thm.thm -> Thm.thm
    3.26 -  val export_solutions : export list * Thm.thm -> Thm.thm
    3.27 -
    3.28    (* inserting meta level params for frees in the conditions *)
    3.29 -  val allify_conditions :
    3.30 -      (Term.term -> Thm.cterm) ->
    3.31 -      (string * Term.typ) list -> Thm.thm -> Thm.thm * Thm.cterm list
    3.32 -  val allify_conditions' :
    3.33 -      (string * Term.typ) list -> Thm.thm -> Thm.thm * Thm.cterm list
    3.34 -  val assume_allified :
    3.35 -      theory -> (string * Term.sort) list * (string * Term.typ) list
    3.36 -      -> Term.term -> (Thm.cterm * Thm.thm)
    3.37 +  val allify_conditions : (term -> cterm) -> (string * typ) list -> thm -> thm * cterm list
    3.38  
    3.39    (* meta level fixed params (i.e. !! vars) *)
    3.40 -  val fix_alls_in_term : Term.term -> Term.term * Term.term list
    3.41 -  val fix_alls_term : int -> Term.term -> Term.term * Term.term list
    3.42 -  val fix_alls_cterm : int -> Thm.thm -> Thm.cterm * Thm.cterm list
    3.43 -  val fix_alls' : int -> Thm.thm -> Thm.thm * Thm.cterm list
    3.44 -  val fix_alls : int -> Thm.thm -> Thm.thm * export
    3.45 +  val fix_alls_term : int -> term -> term * term list
    3.46  
    3.47 -  (* meta variables in types and terms *)
    3.48 -  val fix_tvars_to_tfrees_in_terms 
    3.49 -      : string list (* avoid these names *)
    3.50 -        -> Term.term list -> 
    3.51 -        (((string * int) * Term.sort) * (string * Term.sort)) list (* renamings *)
    3.52 -  val fix_vars_to_frees_in_terms
    3.53 -      : string list (* avoid these names *)
    3.54 -        -> Term.term list ->
    3.55 -        (((string * int) * Term.typ) * (string * Term.typ)) list (* renamings *)
    3.56 -  val fix_tvars_to_tfrees : Thm.thm -> Thm.ctyp list * Thm.thm
    3.57 -  val fix_vars_to_frees : Thm.thm -> Thm.cterm list * Thm.thm
    3.58 -  val fix_vars_and_tvars : 
    3.59 -      Thm.thm -> (Thm.cterm list * Thm.ctyp list) * Thm.thm
    3.60 -  val fix_vars_upto_idx : int -> Thm.thm -> Thm.thm
    3.61 -  val fix_tvars_upto_idx : int -> Thm.thm -> Thm.thm
    3.62 -  val unfix_frees : Thm.cterm list -> Thm.thm -> Thm.thm
    3.63 -  val unfix_tfrees : Thm.ctyp list -> Thm.thm -> Thm.thm
    3.64 -  val unfix_frees_and_tfrees :
    3.65 -      (Thm.cterm list * Thm.ctyp list) -> Thm.thm -> Thm.thm
    3.66 +  val unfix_frees : cterm list -> thm -> thm
    3.67  
    3.68    (* assumptions/subgoals *)
    3.69 -  val assume_prems :
    3.70 -      int -> Thm.thm -> Thm.thm list * Thm.thm * Thm.cterm list
    3.71 -  val fixed_subgoal_thms : Thm.thm -> Thm.thm list * (Thm.thm list -> Thm.thm)
    3.72 -  val fixes_and_assumes : int -> Thm.thm -> Thm.thm list * Thm.thm * export
    3.73 -  val hide_other_goals : Thm.thm -> Thm.thm * Thm.cterm list
    3.74 -  val hide_prems : Thm.thm -> Thm.thm * Thm.cterm list
    3.75 -
    3.76 -  (* abstracts cterms (vars) to locally meta-all bounds *)
    3.77 -  val prepare_goal_export : string list * Thm.cterm list -> Thm.thm 
    3.78 -                            -> int * Thm.thm
    3.79 -  val solve_with : Thm.thm -> Thm.thm -> Thm.thm Seq.seq
    3.80 -  val subgoal_thms : Thm.thm -> Thm.thm list * (Thm.thm list -> Thm.thm)
    3.81 +  val fixed_subgoal_thms : thm -> thm list * (thm list -> thm)
    3.82  end
    3.83  
    3.84 -
    3.85 -structure IsaND 
    3.86 -: ISA_ND
    3.87 -= struct
    3.88 -
    3.89 -(* Solve *some* subgoal of "th" directly by "sol" *)
    3.90 -(* Note: this is probably what Markus ment to do upon export of a
    3.91 -"show" but maybe he used RS/rtac instead, which would wrongly lead to
    3.92 -failing if there are premices to the shown goal. 
    3.93 -
    3.94 -given: 
    3.95 -sol : Thm.thm = [| Ai... |] ==> Ci
    3.96 -th : Thm.thm = 
    3.97 -  [| ... [| Ai... |] ==> Ci ... |] ==> G
    3.98 -results in: 
    3.99 -  [| ... [| Ai-1... |] ==> Ci-1
   3.100 -    [| Ai+1... |] ==> Ci+1 ...
   3.101 -  |] ==> G
   3.102 -i.e. solves some subgoal of th that is identical to sol. 
   3.103 -*)
   3.104 -fun solve_with sol th = 
   3.105 -    let fun solvei 0 = Seq.empty
   3.106 -          | solvei i = 
   3.107 -            Seq.append (Thm.bicompose false (false,sol,0) i th) (solvei (i - 1))
   3.108 -    in
   3.109 -      solvei (Thm.nprems_of th)
   3.110 -    end;
   3.111 -
   3.112 +structure IsaND : ISA_ND =
   3.113 +struct
   3.114  
   3.115  (* Given ctertmify function, (string,type) pairs capturing the free
   3.116  vars that need to be allified in the assumption, and a theorem with
   3.117  assumptions possibly containing the free vars, then we give back the
   3.118 -assumptions allified as hidden hyps. 
   3.119 +assumptions allified as hidden hyps.
   3.120  
   3.121 -Given: x 
   3.122 -th: A vs ==> B vs 
   3.123 +Given: x
   3.124 +th: A vs ==> B vs
   3.125  Results in: "B vs" [!!x. A x]
   3.126  *)
   3.127 -fun allify_conditions ctermify Ts th = 
   3.128 -    let 
   3.129 +fun allify_conditions ctermify Ts th =
   3.130 +    let
   3.131        val premts = Thm.prems_of th;
   3.132 -    
   3.133 -      fun allify_prem_var (vt as (n,ty),t)  = 
   3.134 +
   3.135 +      fun allify_prem_var (vt as (n,ty),t)  =
   3.136            (Logic.all_const ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
   3.137  
   3.138        fun allify_prem Ts p = List.foldr allify_prem_var p Ts
   3.139 @@ -137,308 +59,64 @@
   3.140        val cTs = map (ctermify o Free) Ts
   3.141        val cterm_asms = map (ctermify o allify_prem Ts) premts
   3.142        val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms
   3.143 -    in 
   3.144 +    in
   3.145        (Library.foldl (fn (x,y) => y COMP x) (th, allifyied_asm_thms), cterm_asms)
   3.146      end;
   3.147  
   3.148 -fun allify_conditions' Ts th = 
   3.149 -    allify_conditions (Thm.cterm_of (Thm.theory_of_thm th)) Ts th;
   3.150 -
   3.151 -(* allify types *)
   3.152 -fun allify_typ ts ty = 
   3.153 -    let 
   3.154 -      fun trec (x as (TFree (s,srt))) = 
   3.155 -          (case Library.find_first (fn (s2,srt2) => s = s2) ts
   3.156 -            of NONE => x
   3.157 -             | SOME (s2,_) => TVar ((s,0),srt))
   3.158 -            (*  Maybe add in check here for bad sorts? 
   3.159 -             if srt = srt2 then TVar ((s,0),srt) 
   3.160 -               else raise  ("thaw_typ", ts, ty) *)
   3.161 -          | trec (Type (s,typs)) = Type (s, map trec typs)
   3.162 -          | trec (v as TVar _) = v;
   3.163 -    in trec ty end;
   3.164 -
   3.165 -(* implicit types and term *)
   3.166 -fun allify_term_typs ty = Term.map_types (allify_typ ty);
   3.167 -
   3.168 -(* allified version of term, given frees to allify over. Note that we
   3.169 -only allify over the types on the given allified cterm, we can't do
   3.170 -this for the theorem as we are not allowed type-vars in the hyp. *)
   3.171 -(* FIXME: make the allified term keep the same conclusion as it
   3.172 -started with, rather than a strictly more general version (ie use
   3.173 -instantiate with initial params we abstracted from, rather than
   3.174 -forall_elim_vars. *)
   3.175 -fun assume_allified sgn (tyvs,vs) t = 
   3.176 -    let
   3.177 -      fun allify_var (vt as (n,ty),t)  = 
   3.178 -          (Logic.all_const ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
   3.179 -      fun allify Ts p = List.foldr allify_var p Ts
   3.180 -
   3.181 -      val ctermify = Thm.cterm_of sgn;
   3.182 -      val cvars = map (fn (n,ty) => ctermify (Var ((n,0),ty))) vs
   3.183 -      val allified_term = t |> allify vs;
   3.184 -      val ct = ctermify allified_term;
   3.185 -      val typ_allified_ct = ctermify (allify_term_typs tyvs allified_term);
   3.186 -    in (typ_allified_ct, 
   3.187 -        Thm.forall_elim_vars 0 (Thm.assume ct)) end;
   3.188 -
   3.189 -
   3.190 -(* change type-vars to fresh type frees *)
   3.191 -fun fix_tvars_to_tfrees_in_terms names ts = 
   3.192 -    let 
   3.193 -      val tfree_names = map fst (List.foldr Misc_Legacy.add_term_tfrees [] ts);
   3.194 -      val tvars = List.foldr Misc_Legacy.add_term_tvars [] ts;
   3.195 -      val (names',renamings) = 
   3.196 -          List.foldr (fn (tv as ((n,i),s),(Ns,Rs)) => 
   3.197 -                         let val n2 = singleton (Name.variant_list Ns) n in 
   3.198 -                           (n2::Ns, (tv, (n2,s))::Rs)
   3.199 -                         end) (tfree_names @ names,[]) tvars;
   3.200 -    in renamings end;
   3.201 -fun fix_tvars_to_tfrees th = 
   3.202 -    let 
   3.203 -      val sign = Thm.theory_of_thm th;
   3.204 -      val ctypify = Thm.ctyp_of sign;
   3.205 -      val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
   3.206 -      val renamings = fix_tvars_to_tfrees_in_terms 
   3.207 -                        [] ((Thm.prop_of th) :: tpairs);
   3.208 -      val crenamings = 
   3.209 -          map (fn (v,f) => (ctypify (TVar v), ctypify (TFree f)))
   3.210 -              renamings;
   3.211 -      val fixedfrees = map snd crenamings;
   3.212 -    in (fixedfrees, Thm.instantiate (crenamings, []) th) end;
   3.213 -
   3.214 -
   3.215 -(* change type-free's to type-vars in th, skipping the ones in "ns" *)
   3.216 -fun unfix_tfrees ns th = 
   3.217 -    let 
   3.218 -      val varfiytfrees = map (Term.dest_TFree o Thm.typ_of) ns
   3.219 -      val skiptfrees = subtract (op =) varfiytfrees (Misc_Legacy.add_term_tfrees (Thm.prop_of th,[]));
   3.220 -    in #2 (Thm.varifyT_global' skiptfrees th) end;
   3.221 -
   3.222 -(* change schematic/meta vars to fresh free vars, avoiding name clashes 
   3.223 -   with "names" *)
   3.224 -fun fix_vars_to_frees_in_terms names ts = 
   3.225 -    let 
   3.226 -      val vars = map Term.dest_Var (List.foldr Misc_Legacy.add_term_vars [] ts);
   3.227 -      val Ns = List.foldr Misc_Legacy.add_term_names names ts;
   3.228 -      val (_,renamings) = 
   3.229 -          Library.foldl (fn ((Ns,Rs),v as ((n,i),ty)) => 
   3.230 -                    let val n2 = singleton (Name.variant_list Ns) n in
   3.231 -                      (n2 :: Ns, (v, (n2,ty)) :: Rs)
   3.232 -                    end) ((Ns,[]), vars);
   3.233 -    in renamings end;
   3.234 -fun fix_vars_to_frees th = 
   3.235 -    let 
   3.236 -      val ctermify = Thm.cterm_of (Thm.theory_of_thm th)
   3.237 -      val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
   3.238 -      val renamings = fix_vars_to_frees_in_terms 
   3.239 -                        [] ([Thm.prop_of th] @ tpairs);
   3.240 -      val crenamings = 
   3.241 -          map (fn (v,f) => (ctermify (Var v), ctermify (Free f)))
   3.242 -              renamings;
   3.243 -      val fixedfrees = map snd crenamings;
   3.244 -    in (fixedfrees, Thm.instantiate ([], crenamings) th) end;
   3.245 -
   3.246 -fun fix_tvars_upto_idx ix th = 
   3.247 -    let 
   3.248 -      val sgn = Thm.theory_of_thm th;
   3.249 -      val ctypify = Thm.ctyp_of sgn
   3.250 -      val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
   3.251 -      val prop = (Thm.prop_of th);
   3.252 -      val tvars = List.foldr Misc_Legacy.add_term_tvars [] (prop :: tpairs);
   3.253 -      val ctyfixes = 
   3.254 -          map_filter 
   3.255 -            (fn (v as ((s,i),ty)) => 
   3.256 -                if i <= ix then SOME (ctypify (TVar v), ctypify (TFree (s,ty)))
   3.257 -                else NONE) tvars;
   3.258 -    in Thm.instantiate (ctyfixes, []) th end;
   3.259 -fun fix_vars_upto_idx ix th = 
   3.260 -    let 
   3.261 -      val sgn = Thm.theory_of_thm th;
   3.262 -      val ctermify = Thm.cterm_of sgn
   3.263 -      val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
   3.264 -      val prop = (Thm.prop_of th);
   3.265 -      val vars = map Term.dest_Var (List.foldr Misc_Legacy.add_term_vars 
   3.266 -                                               [] (prop :: tpairs));
   3.267 -      val cfixes = 
   3.268 -          map_filter 
   3.269 -            (fn (v as ((s,i),ty)) => 
   3.270 -                if i <= ix then SOME (ctermify (Var v), ctermify (Free (s,ty)))
   3.271 -                else NONE) vars;
   3.272 -    in Thm.instantiate ([], cfixes) th end;
   3.273 -
   3.274 -
   3.275  (* make free vars into schematic vars with index zero *)
   3.276 - fun unfix_frees frees = 
   3.277 +fun unfix_frees frees =
   3.278       fold (K (Thm.forall_elim_var 0)) frees
   3.279       o Drule.forall_intr_list frees;
   3.280  
   3.281 -(* fix term and type variables *)
   3.282 -fun fix_vars_and_tvars th = 
   3.283 -    let val (tvars, th') = fix_tvars_to_tfrees th
   3.284 -      val (vars, th'') = fix_vars_to_frees th' 
   3.285 -    in ((vars, tvars), th'') end;
   3.286 -
   3.287 -(* implicit Thm.thm argument *)
   3.288 -(* assumes: vars may contain fixed versions of the frees *)
   3.289 -(* THINK: what if vs already has types varified? *)
   3.290 -fun unfix_frees_and_tfrees (vs,tvs) = 
   3.291 -    (unfix_tfrees tvs o unfix_frees vs);
   3.292 -
   3.293  (* datatype to capture an exported result, ie a fix or assume. *)
   3.294 -datatype export = 
   3.295 +datatype export =
   3.296           export of {fixes : Thm.cterm list, (* fixed vars *)
   3.297                      assumes : Thm.cterm list, (* hidden hyps/assumed prems *)
   3.298                      sgid : int,
   3.299                      gth :  Thm.thm}; (* subgoal/goalthm *)
   3.300  
   3.301 -fun fixes_of_exp (export rep) = #fixes rep;
   3.302 -
   3.303 -(* export the result of the new goal thm, ie if we reduced teh
   3.304 -subgoal, then we get a new reduced subtgoal with the old
   3.305 -all-quantified variables *)
   3.306 -local 
   3.307 -
   3.308 -(* allify puts in a meta level univ quantifier for a free variavble *)
   3.309 -fun allify_term (v, t) = 
   3.310 -    let val vt = #t (Thm.rep_cterm v)
   3.311 -      val (n,ty) = Term.dest_Free vt
   3.312 -    in (Logic.all_const ty) $ (Abs(n,ty,Term.abstract_over (vt, t))) end;
   3.313 -
   3.314 -fun allify_for_sg_term ctermify vs t =
   3.315 -    let val t_alls = List.foldr allify_term t vs;
   3.316 -        val ct_alls = ctermify t_alls; 
   3.317 -    in 
   3.318 -      (ct_alls, Drule.forall_elim_list vs (Thm.assume ct_alls))
   3.319 -    end;
   3.320 -(* lookup type of a free var name from a list *)
   3.321 -fun lookupfree vs vn  = 
   3.322 -    case Library.find_first (fn (n,ty) => n = vn) vs of 
   3.323 -      NONE => error ("prepare_goal_export:lookupfree: " ^ vn ^ " does not occur in the term")
   3.324 -    | SOME x => x;
   3.325 -in
   3.326 -fun export_back (export {fixes = vs, assumes = hprems, 
   3.327 -                         sgid = i, gth = gth}) newth = 
   3.328 -    let 
   3.329 -      val sgn = Thm.theory_of_thm newth;
   3.330 -      val ctermify = Thm.cterm_of sgn;
   3.331 -
   3.332 -      val sgs = prems_of newth;
   3.333 -      val (sgallcts, sgthms) = 
   3.334 -          Library.split_list (map (allify_for_sg_term ctermify vs) sgs);
   3.335 -      val minimal_newth = 
   3.336 -          (Library.foldl (fn ( newth', sgthm) => 
   3.337 -                          Drule.compose_single (sgthm, 1, newth'))
   3.338 -                      (newth, sgthms));
   3.339 -      val allified_newth = 
   3.340 -          minimal_newth 
   3.341 -            |> Drule.implies_intr_list hprems
   3.342 -            |> Drule.forall_intr_list vs 
   3.343 -
   3.344 -      val newth' = Drule.implies_intr_list sgallcts allified_newth
   3.345 -    in
   3.346 -      Thm.bicompose false (false, newth', (length sgallcts)) i gth
   3.347 -    end;
   3.348 -
   3.349 -(* 
   3.350 -Given "vs" : names of free variables to abstract over,
   3.351 -Given cterms : premices to abstract over (P1... Pn) in terms of vs,
   3.352 -Given a thm of the form: 
   3.353 -P1 vs; ...; Pn vs ==> Goal(C vs)
   3.354 -
   3.355 -Gives back: 
   3.356 -(n, length of given cterms which have been allified
   3.357 - [| !! vs. P1 vs; !! vs. Pn vs |] ==> !! C vs) the allified thm
   3.358 -*)
   3.359 -(* note: C may contain further premices etc 
   3.360 -Note that cterms is the assumed facts, ie prems of "P1" that are
   3.361 -reintroduced in allified form.
   3.362 -*)
   3.363 -fun prepare_goal_export (vs, cterms) th = 
   3.364 -    let 
   3.365 -      val sgn = Thm.theory_of_thm th;
   3.366 -      val ctermify = Thm.cterm_of sgn;
   3.367 -
   3.368 -      val allfrees = map Term.dest_Free (Misc_Legacy.term_frees (Thm.prop_of th))
   3.369 -      val cfrees = map (ctermify o Free o lookupfree allfrees) vs
   3.370 -
   3.371 -      val sgs = prems_of th;
   3.372 -      val (sgallcts, sgthms) = 
   3.373 -          Library.split_list (map (allify_for_sg_term ctermify cfrees) sgs);
   3.374 -
   3.375 -      val minimal_th = 
   3.376 -          Goal.conclude (Library.foldl (fn ( th', sgthm) => 
   3.377 -                          Drule.compose_single (sgthm, 1, th'))
   3.378 -                      (th, sgthms));
   3.379 -
   3.380 -      val allified_th = 
   3.381 -          minimal_th 
   3.382 -            |> Drule.implies_intr_list cterms
   3.383 -            |> Drule.forall_intr_list cfrees 
   3.384 -
   3.385 -      val th' = Drule.implies_intr_list sgallcts allified_th
   3.386 -    in
   3.387 -      ((length sgallcts), th')
   3.388 -    end;
   3.389 -
   3.390 -end;
   3.391 -
   3.392 -
   3.393  (* exporting function that takes a solution to the fixed/assumed goal,
   3.394  and uses this to solve the subgoal in the main theorem *)
   3.395  fun export_solution (export {fixes = cfvs, assumes = hcprems,
   3.396 -                             sgid = i, gth = gth}) solth = 
   3.397 -    let 
   3.398 -      val solth' = 
   3.399 +                             sgid = i, gth = gth}) solth =
   3.400 +    let
   3.401 +      val solth' =
   3.402            solth |> Drule.implies_intr_list hcprems
   3.403                  |> Drule.forall_intr_list cfvs
   3.404      in Drule.compose_single (solth', i, gth) end;
   3.405  
   3.406 -fun export_solutions (xs,th) = List.foldr (uncurry export_solution) th xs;
   3.407 -
   3.408  
   3.409  (* fix parameters of a subgoal "i", as free variables, and create an
   3.410  exporting function that will use the result of this proved goal to
   3.411 -show the goal in the original theorem. 
   3.412 +show the goal in the original theorem.
   3.413  
   3.414  Note, an advantage of this over Isar is that it supports instantiation
   3.415  of unkowns in the earlier theorem, ie we can do instantiation of meta
   3.416 -vars! 
   3.417 +vars!
   3.418  
   3.419 -avoids constant, free and vars names. 
   3.420 +avoids constant, free and vars names.
   3.421  
   3.422  loosely corresponds to:
   3.423  Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm
   3.424 -Result: 
   3.425 -  ("(As ==> SGi x') ==> (As ==> SGi x')" : thm, 
   3.426 -   expf : 
   3.427 -     ("As ==> SGi x'" : thm) -> 
   3.428 +Result:
   3.429 +  ("(As ==> SGi x') ==> (As ==> SGi x')" : thm,
   3.430 +   expf :
   3.431 +     ("As ==> SGi x'" : thm) ->
   3.432       ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm)
   3.433  *)
   3.434 -fun fix_alls_in_term alledt = 
   3.435 +fun fix_alls_term i t =
   3.436      let
   3.437 -      val t = Term.strip_all_body alledt;
   3.438 -      val alls = rev (Term.strip_all_vars alledt);
   3.439 -      val varnames = map (fst o fst o Term.dest_Var) (Misc_Legacy.term_vars t)
   3.440 -      val names = Misc_Legacy.add_term_names (t,varnames);
   3.441 -      val fvs = map Free 
   3.442 -                    (Name.variant_list names (map fst alls)
   3.443 -                       ~~ (map snd alls));
   3.444 -    in ((subst_bounds (fvs,t)), fvs) end;
   3.445 -
   3.446 -fun fix_alls_term i t = 
   3.447 -    let 
   3.448        val varnames = map (fst o fst o Term.dest_Var) (Misc_Legacy.term_vars t)
   3.449        val names = Misc_Legacy.add_term_names (t,varnames);
   3.450        val gt = Logic.get_goal t i;
   3.451        val body = Term.strip_all_body gt;
   3.452        val alls = rev (Term.strip_all_vars gt);
   3.453 -      val fvs = map Free 
   3.454 +      val fvs = map Free
   3.455                      (Name.variant_list names (map fst alls)
   3.456                         ~~ (map snd alls));
   3.457      in ((subst_bounds (fvs,body)), fvs) end;
   3.458  
   3.459 -fun fix_alls_cterm i th = 
   3.460 +fun fix_alls_cterm i th =
   3.461      let
   3.462        val ctermify = Thm.cterm_of (Thm.theory_of_thm th);
   3.463        val (fixedbody, fvs) = fix_alls_term i (Thm.prop_of th);
   3.464 @@ -448,20 +126,20 @@
   3.465        (ct_body, cfvs)
   3.466      end;
   3.467  
   3.468 -fun fix_alls' i = 
   3.469 +fun fix_alls' i =
   3.470       (apfst Thm.trivial) o (fix_alls_cterm i);
   3.471  
   3.472  
   3.473 -(* hide other goals *) 
   3.474 +(* hide other goals *)
   3.475  (* note the export goal is rotated by (i - 1) and will have to be
   3.476  unrotated to get backto the originial position(s) *)
   3.477 -fun hide_other_goals th = 
   3.478 +fun hide_other_goals th =
   3.479      let
   3.480        (* tl beacuse fst sg is the goal we are interested in *)
   3.481        val cprems = tl (Drule.cprems_of th)
   3.482        val aprems = map Thm.assume cprems
   3.483      in
   3.484 -      (Drule.implies_elim_list (Drule.rotate_prems 1 th) aprems, 
   3.485 +      (Drule.implies_elim_list (Drule.rotate_prems 1 th) aprems,
   3.486         cprems)
   3.487      end;
   3.488  
   3.489 @@ -470,104 +148,36 @@
   3.490  namely the subgoal that we were trying to solve. *)
   3.491  (* loosely corresponds to:
   3.492  Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm
   3.493 -Result: 
   3.494 -  ("(As ==> SGi x') ==> SGi x'" : thm, 
   3.495 -   expf : 
   3.496 -     ("SGi x'" : thm) -> 
   3.497 +Result:
   3.498 +  ("(As ==> SGi x') ==> SGi x'" : thm,
   3.499 +   expf :
   3.500 +     ("SGi x'" : thm) ->
   3.501       ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm)
   3.502  *)
   3.503 -fun fix_alls i th = 
   3.504 -    let 
   3.505 +fun fix_alls i th =
   3.506 +    let
   3.507        val (fixed_gth, fixedvars) = fix_alls' i th
   3.508        val (sml_gth, othergoals) = hide_other_goals fixed_gth
   3.509      in
   3.510 -      (sml_gth, export {fixes = fixedvars, 
   3.511 -                        assumes = othergoals, 
   3.512 +      (sml_gth, export {fixes = fixedvars,
   3.513 +                        assumes = othergoals,
   3.514                          sgid = i, gth = th})
   3.515      end;
   3.516  
   3.517  
   3.518 -(* assume the premises of subgoal "i", this gives back a list of
   3.519 -assumed theorems that are the premices of subgoal i, it also gives
   3.520 -back a new goal thm and an exporter, the new goalthm is as the old
   3.521 -one, but without the premices, and the exporter will use a proof of
   3.522 -the new goalthm, possibly using the assumed premices, to shoe the
   3.523 -orginial goal.
   3.524 -
   3.525 -Note: Dealing with meta vars, need to meta-level-all them in the
   3.526 -shyps, which we can later instantiate with a specific value.... ? 
   3.527 -think about this... maybe need to introduce some new fixed vars and
   3.528 -then remove them again at the end... like I do with rw_inst. 
   3.529 -
   3.530 -loosely corresponds to:
   3.531 -Given "[| SG0; ... [| A0; ... An |] ==> SGi; ... SGm |] ==> G" : thm
   3.532 -Result: 
   3.533 -(["A0" [A0], ... ,"An" [An]] : thm list, -- assumptions
   3.534 - "SGi ==> SGi" : thm, -- new goal 
   3.535 - "SGi" ["A0" ... "An"] : thm ->   -- export function
   3.536 -    ("[| SG0 ... SGi-1, SGi+1, SGm |] ==> G" : thm) list)
   3.537 -*)
   3.538 -fun assume_prems i th =
   3.539 -    let 
   3.540 -      val t = (prop_of th); 
   3.541 -      val gt = Logic.get_goal t i;
   3.542 -      val _ = case Term.strip_all_vars gt of [] => () 
   3.543 -              | _ => error "assume_prems: goal has params"
   3.544 -      val body = gt;
   3.545 -      val prems = Logic.strip_imp_prems body;
   3.546 -      val concl = Logic.strip_imp_concl body;
   3.547 -
   3.548 -      val sgn = Thm.theory_of_thm th;
   3.549 -      val ctermify = Thm.cterm_of sgn;
   3.550 -      val cprems = map ctermify prems;
   3.551 -      val aprems = map Thm.assume cprems;
   3.552 -      val gthi = Thm.trivial (ctermify concl);
   3.553 -
   3.554 -      (* fun explortf thi = 
   3.555 -          Drule.compose (Drule.implies_intr_list cprems thi, 
   3.556 -                         i, th) *)
   3.557 -    in
   3.558 -      (aprems, gthi, cprems)
   3.559 -    end;
   3.560 -
   3.561 -
   3.562 -(* first fix the variables, then assume the assumptions *)
   3.563 -(* loosely corresponds to:
   3.564 -Given 
   3.565 -  "[| SG0; ... 
   3.566 -      !! xs. [| A0 xs; ... An xs |] ==> SGi xs; 
   3.567 -      ... SGm |] ==> G" : thm
   3.568 -Result: 
   3.569 -(["A0 xs'" [A0 xs'], ... ,"An xs'" [An xs']] : thm list, -- assumptions
   3.570 - "SGi xs' ==> SGi xs'" : thm,  -- new goal 
   3.571 - "SGi xs'" ["A0 xs'" ... "An xs'"] : thm ->   -- export function
   3.572 -    ("[| SG0 ... SGi-1, SGi+1, SGm |] ==> G" : thm) list)
   3.573 -*)
   3.574 -
   3.575 -(* Note: the fix_alls actually pulls through all the assumptions which
   3.576 -means that the second export is not needed. *)
   3.577 -fun fixes_and_assumes i th = 
   3.578 -    let 
   3.579 -      val (fixgth, exp1) = fix_alls i th
   3.580 -      val (assumps, goalth, _) = assume_prems 1 fixgth
   3.581 -    in 
   3.582 -      (assumps, goalth, exp1)
   3.583 -    end;
   3.584 -
   3.585 -
   3.586  (* Fixme: allow different order of subgoals given to expf *)
   3.587  (* make each subgoal into a separate thm that needs to be proved *)
   3.588  (* loosely corresponds to:
   3.589 -Given 
   3.590 +Given
   3.591    "[| SG0; ... SGm |] ==> G" : thm
   3.592 -Result: 
   3.593 +Result:
   3.594  (["SG0 ==> SG0", ... ,"SGm ==> SGm"] : thm list, -- goals
   3.595   ["SG0", ..., "SGm"] : thm list ->   -- export function
   3.596     "G" : thm)
   3.597  *)
   3.598 -fun subgoal_thms th = 
   3.599 -    let 
   3.600 -      val t = (prop_of th); 
   3.601 +fun subgoal_thms th =
   3.602 +    let
   3.603 +      val t = (prop_of th);
   3.604  
   3.605        val prems = Logic.strip_imp_prems t;
   3.606  
   3.607 @@ -576,58 +186,37 @@
   3.608  
   3.609        val aprems = map (Thm.trivial o ctermify) prems;
   3.610  
   3.611 -      fun explortf premths = 
   3.612 +      fun explortf premths =
   3.613            Drule.implies_elim_list th premths
   3.614      in
   3.615        (aprems, explortf)
   3.616      end;
   3.617  
   3.618  
   3.619 -(* make all the premices of a theorem hidden, and provide an unhide
   3.620 -function, that will bring them back out at a later point. This is
   3.621 -useful if you want to get back these premices, after having used the
   3.622 -theorem with the premices hidden *)
   3.623 -(* loosely corresponds to:
   3.624 -Given "As ==> G" : thm
   3.625 -Result: ("G [As]" : thm, 
   3.626 -         "G [As]" : thm -> "As ==> G" : thm
   3.627 -*)
   3.628 -fun hide_prems th = 
   3.629 -    let 
   3.630 -      val cprems = Drule.cprems_of th;
   3.631 -      val aprems = map Thm.assume cprems;
   3.632 -    (*   val unhidef = Drule.implies_intr_list cprems; *)
   3.633 -    in
   3.634 -      (Drule.implies_elim_list th aprems, cprems)
   3.635 -    end;
   3.636 -
   3.637 -
   3.638 -
   3.639 -
   3.640  (* Fixme: allow different order of subgoals in exportf *)
   3.641  (* as above, but also fix all parameters in all subgoals, and uses
   3.642  fix_alls, not fix_alls', ie doesn't leave extra asumptions as apparent
   3.643  subgoals. *)
   3.644  (* loosely corresponds to:
   3.645 -Given 
   3.646 -  "[| !! x0s. A0s x0s ==> SG0 x0s; 
   3.647 +Given
   3.648 +  "[| !! x0s. A0s x0s ==> SG0 x0s;
   3.649        ...; !! xms. Ams xms ==> SGm xms|] ==> G" : thm
   3.650 -Result: 
   3.651 -(["(A0s x0s' ==> SG0 x0s') ==> SG0 x0s'", 
   3.652 +Result:
   3.653 +(["(A0s x0s' ==> SG0 x0s') ==> SG0 x0s'",
   3.654    ... ,"(Ams xms' ==> SGm xms') ==> SGm xms'"] : thm list, -- goals
   3.655   ["SG0 x0s'", ..., "SGm xms'"] : thm list ->   -- export function
   3.656     "G" : thm)
   3.657  *)
   3.658  (* requires being given solutions! *)
   3.659 -fun fixed_subgoal_thms th = 
   3.660 -    let 
   3.661 +fun fixed_subgoal_thms th =
   3.662 +    let
   3.663        val (subgoals, expf) = subgoal_thms th;
   3.664  (*       fun export_sg (th, exp) = exp th; *)
   3.665 -      fun export_sgs expfs solthms = 
   3.666 +      fun export_sgs expfs solthms =
   3.667            expf (map2 (curry (op |>)) solthms expfs);
   3.668  (*           expf (map export_sg (ths ~~ expfs)); *)
   3.669 -    in 
   3.670 -      apsnd export_sgs (Library.split_list (map (apsnd export_solution o 
   3.671 +    in
   3.672 +      apsnd export_sgs (Library.split_list (map (apsnd export_solution o
   3.673                                                   fix_alls 1) subgoals))
   3.674      end;
   3.675  
     4.1 --- a/src/Tools/IsaPlanner/rw_inst.ML	Wed Sep 12 17:26:05 2012 +0200
     4.2 +++ b/src/Tools/IsaPlanner/rw_inst.ML	Wed Sep 12 22:00:29 2012 +0200
     4.3 @@ -3,61 +3,34 @@
     4.4  
     4.5  Rewriting using a conditional meta-equality theorem which supports
     4.6  schematic variable instantiation.
     4.7 -*)   
     4.8 +*)
     4.9  
    4.10  signature RW_INST =
    4.11  sig
    4.12  
    4.13 +  val beta_eta_contract : thm -> thm
    4.14 +
    4.15    (* Rewrite: give it instantiation infromation, a rule, and the
    4.16    target thm, and it will return the rewritten target thm *)
    4.17    val rw :
    4.18 -      ((Term.indexname * (Term.sort * Term.typ)) list *  (* type var instantiations *)
    4.19 -       (Term.indexname * (Term.typ * Term.term)) list)  (* schematic var instantiations *)
    4.20 -      * (string * Term.typ) list           (* Fake named bounds + types *)
    4.21 -      * (string * Term.typ) list           (* names of bound + types *)
    4.22 -      * Term.term ->                       (* outer term for instantiation *)
    4.23 -      Thm.thm ->                           (* rule with indexies lifted *)
    4.24 -      Thm.thm ->                           (* target thm *)
    4.25 -      Thm.thm                              (* rewritten theorem possibly 
    4.26 -                                              with additional premises for 
    4.27 -                                              rule conditions *)
    4.28 -
    4.29 -  (* used tools *)
    4.30 -  val mk_abstractedrule :
    4.31 -      (string * Term.typ) list (* faked outer bound *)
    4.32 -      -> (string * Term.typ) list (* hopeful name of outer bounds *)
    4.33 -      -> Thm.thm -> Thm.cterm list * Thm.thm
    4.34 -  val mk_fixtvar_tyinsts :
    4.35 -      (Term.indexname * (Term.sort * Term.typ)) list ->
    4.36 -      Term.term list -> ((string * int) * (Term.sort * Term.typ)) list 
    4.37 -                        * (string * Term.sort) list
    4.38 -  val mk_renamings :
    4.39 -      Term.term -> Thm.thm -> (((string * int) * Term.typ) * Term.term) list
    4.40 -  val new_tfree :
    4.41 -      ((string * int) * Term.sort) *
    4.42 -      (((string * int) * (Term.sort * Term.typ)) list * string list) ->
    4.43 -      ((string * int) * (Term.sort * Term.typ)) list * string list
    4.44 -  val cross_inst : (Term.indexname * (Term.typ * Term.term)) list 
    4.45 -                   -> (Term.indexname *(Term.typ * Term.term)) list
    4.46 -  val cross_inst_typs : (Term.indexname * (Term.sort * Term.typ)) list 
    4.47 -                   -> (Term.indexname * (Term.sort * Term.typ)) list
    4.48 -
    4.49 -  val beta_contract : Thm.thm -> Thm.thm
    4.50 -  val beta_eta_contract : Thm.thm -> Thm.thm
    4.51 -
    4.52 +      ((indexname * (sort * typ)) list *  (* type var instantiations *)
    4.53 +       (indexname * (typ * term)) list)  (* schematic var instantiations *)
    4.54 +      * (string * typ) list           (* Fake named bounds + types *)
    4.55 +      * (string * typ) list           (* names of bound + types *)
    4.56 +      * term ->                       (* outer term for instantiation *)
    4.57 +      thm ->                           (* rule with indexies lifted *)
    4.58 +      thm ->                           (* target thm *)
    4.59 +      thm                              (* rewritten theorem possibly
    4.60 +                                          with additional premises for
    4.61 +                                          rule conditions *)
    4.62  end;
    4.63  
    4.64 -structure RWInst 
    4.65 -: RW_INST
    4.66 -= struct
    4.67 +structure RWInst : RW_INST =
    4.68 +struct
    4.69  
    4.70  
    4.71 -(* beta contract the theorem *)
    4.72 -fun beta_contract thm = 
    4.73 -    Thm.equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm;
    4.74 -
    4.75  (* beta-eta contract the theorem *)
    4.76 -fun beta_eta_contract thm = 
    4.77 +fun beta_eta_contract thm =
    4.78      let
    4.79        val thm2 = Thm.equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm
    4.80        val thm3 = Thm.equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2
    4.81 @@ -79,7 +52,7 @@
    4.82  creates an abstracted version of the theorem, with local bound vars as
    4.83  lambda-params:
    4.84  
    4.85 -Ts: 
    4.86 +Ts:
    4.87  ("x", ty)
    4.88  
    4.89  rule::
    4.90 @@ -91,19 +64,18 @@
    4.91  note: assumes rule is instantiated
    4.92  *)
    4.93  (* Note, we take abstraction in the order of last abstraction first *)
    4.94 -fun mk_abstractedrule TsFake Ts rule = 
    4.95 -    let 
    4.96 +fun mk_abstractedrule TsFake Ts rule =
    4.97 +    let
    4.98        val ctermify = Thm.cterm_of (Thm.theory_of_thm rule);
    4.99  
   4.100 -      (* now we change the names of temporary free vars that represent 
   4.101 +      (* now we change the names of temporary free vars that represent
   4.102           bound vars with binders outside the redex *)
   4.103 -      val prop = Thm.prop_of rule;
   4.104        val names = usednames_of_thm rule;
   4.105 -      val (fromnames,tonames,names2,Ts') = 
   4.106 -          Library.foldl (fn ((rnf,rnt,names, Ts''),((faken,_),(n,ty))) => 
   4.107 +      val (fromnames,tonames,_,Ts') =
   4.108 +          Library.foldl (fn ((rnf,rnt,names, Ts''),((faken,_),(n,ty))) =>
   4.109                      let val n2 = singleton (Name.variant_list names) n in
   4.110                        (ctermify (Free(faken,ty)) :: rnf,
   4.111 -                       ctermify (Free(n2,ty)) :: rnt, 
   4.112 +                       ctermify (Free(n2,ty)) :: rnt,
   4.113                         n2 :: names,
   4.114                         (n2,ty) :: Ts'')
   4.115                      end)
   4.116 @@ -113,14 +85,14 @@
   4.117        with introduced vars from bounds outside in redex *)
   4.118        val rule' = rule |> Drule.forall_intr_list fromnames
   4.119                         |> Drule.forall_elim_list tonames;
   4.120 -      
   4.121 +
   4.122        (* make unconditional rule and prems *)
   4.123 -      val (uncond_rule, cprems) = IsaND.allify_conditions ctermify (rev Ts') 
   4.124 +      val (uncond_rule, cprems) = IsaND.allify_conditions ctermify (rev Ts')
   4.125                                                            rule';
   4.126  
   4.127        (* using these names create lambda-abstracted version of the rule *)
   4.128        val abstractions = rev (Ts' ~~ tonames);
   4.129 -      val abstract_rule = Library.foldl (fn (th,((n,ty),ct)) => 
   4.130 +      val abstract_rule = Library.foldl (fn (th,((n,ty),ct)) =>
   4.131                                      Thm.abstract_rule n ct th)
   4.132                                  (uncond_rule, abstractions);
   4.133      in (cprems, abstract_rule) end;
   4.134 @@ -131,21 +103,21 @@
   4.135  variables *)
   4.136  (* make fixed unique free variable instantiations for non-ground vars *)
   4.137  (* Create a table of vars to be renamed after instantiation - ie
   4.138 -      other uninstantiated vars in the hyps of the rule 
   4.139 +      other uninstantiated vars in the hyps of the rule
   4.140        ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *)
   4.141 -fun mk_renamings tgt rule_inst = 
   4.142 +fun mk_renamings tgt rule_inst =
   4.143      let
   4.144        val rule_conds = Thm.prems_of rule_inst
   4.145        val names = List.foldr Misc_Legacy.add_term_names [] (tgt :: rule_conds);
   4.146 -      val (conds_tyvs,cond_vs) = 
   4.147 -          Library.foldl (fn ((tyvs, vs), t) => 
   4.148 +      val (_, cond_vs) =
   4.149 +          Library.foldl (fn ((tyvs, vs), t) =>
   4.150                      (union (op =) (Misc_Legacy.term_tvars t) tyvs,
   4.151                       union (op =) (map Term.dest_Var (Misc_Legacy.term_vars t)) vs))
   4.152                  (([],[]), rule_conds);
   4.153 -      val termvars = map Term.dest_Var (Misc_Legacy.term_vars tgt); 
   4.154 +      val termvars = map Term.dest_Var (Misc_Legacy.term_vars tgt);
   4.155        val vars_to_fix = union (op =) termvars cond_vs;
   4.156 -      val (renamings, names2) = 
   4.157 -          List.foldr (fn (((n,i),ty), (vs, names')) => 
   4.158 +      val (renamings, _) =
   4.159 +          List.foldr (fn (((n,i),ty), (vs, names')) =>
   4.160                      let val n' = singleton (Name.variant_list names') n in
   4.161                        ((((n,i),ty), Free (n', ty)) :: vs, n'::names')
   4.162                      end)
   4.163 @@ -158,17 +130,17 @@
   4.164        in  ((ix,(sort,TFree(v,sort)))::pairs, v::used)  end;
   4.165  
   4.166  
   4.167 -(* make instantiations to fix type variables that are not 
   4.168 +(* make instantiations to fix type variables that are not
   4.169     already instantiated (in ignore_ixs) from the list of terms. *)
   4.170 -fun mk_fixtvar_tyinsts ignore_insts ts = 
   4.171 -    let 
   4.172 +fun mk_fixtvar_tyinsts ignore_insts ts =
   4.173 +    let
   4.174        val ignore_ixs = map fst ignore_insts;
   4.175 -      val (tvars, tfrees) = 
   4.176 -            List.foldr (fn (t, (varixs, tfrees)) => 
   4.177 +      val (tvars, tfrees) =
   4.178 +            List.foldr (fn (t, (varixs, tfrees)) =>
   4.179                        (Misc_Legacy.add_term_tvars (t,varixs),
   4.180                         Misc_Legacy.add_term_tfrees (t,tfrees)))
   4.181                    ([],[]) ts;
   4.182 -        val unfixed_tvars = 
   4.183 +        val unfixed_tvars =
   4.184              filter (fn (ix,s) => not (member (op =) ignore_ixs ix)) tvars;
   4.185          val (fixtyinsts, _) = List.foldr new_tfree ([], map fst tfrees) unfixed_tvars
   4.186      in (fixtyinsts, tfrees) end;
   4.187 @@ -177,27 +149,27 @@
   4.188  (* cross-instantiate the instantiations - ie for each instantiation
   4.189  replace all occurances in other instantiations - no loops are possible
   4.190  and thus only one-parsing of the instantiations is necessary. *)
   4.191 -fun cross_inst insts = 
   4.192 -    let 
   4.193 -      fun instL (ix, (ty,t)) = 
   4.194 -          map (fn (ix2,(ty2,t2)) => 
   4.195 +fun cross_inst insts =
   4.196 +    let
   4.197 +      fun instL (ix, (ty,t)) =
   4.198 +          map (fn (ix2,(ty2,t2)) =>
   4.199                    (ix2, (ty2,Term.subst_vars ([], [(ix, t)]) t2)));
   4.200  
   4.201        fun cross_instL ([], l) = rev l
   4.202 -        | cross_instL ((ix, t) :: insts, l) = 
   4.203 +        | cross_instL ((ix, t) :: insts, l) =
   4.204            cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l));
   4.205  
   4.206      in cross_instL (insts, []) end;
   4.207  
   4.208  (* as above but for types -- I don't know if this is needed, will we ever incur mixed up types? *)
   4.209 -fun cross_inst_typs insts = 
   4.210 -    let 
   4.211 -      fun instL (ix, (srt,ty)) = 
   4.212 -          map (fn (ix2,(srt2,ty2)) => 
   4.213 +fun cross_inst_typs insts =
   4.214 +    let
   4.215 +      fun instL (ix, (srt,ty)) =
   4.216 +          map (fn (ix2,(srt2,ty2)) =>
   4.217                    (ix2, (srt2,Term.typ_subst_TVars [(ix, ty)] ty2)));
   4.218  
   4.219        fun cross_instL ([], l) = rev l
   4.220 -        | cross_instL ((ix, t) :: insts, l) = 
   4.221 +        | cross_instL ((ix, t) :: insts, l) =
   4.222            cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l));
   4.223  
   4.224      in cross_instL (insts, []) end;
   4.225 @@ -212,42 +184,40 @@
   4.226  first abstraction first.  FakeTs has abstractions using the fake name
   4.227  - ie the name distinct from all other abstractions. *)
   4.228  
   4.229 -fun rw ((nonfixed_typinsts, unprepinsts), FakeTs, Ts, outerterm) rule target_thm = 
   4.230 -    let 
   4.231 +fun rw ((nonfixed_typinsts, unprepinsts), FakeTs, Ts, outerterm) rule target_thm =
   4.232 +    let
   4.233        (* general signature info *)
   4.234        val target_sign = (Thm.theory_of_thm target_thm);
   4.235        val ctermify = Thm.cterm_of target_sign;
   4.236        val ctypeify = Thm.ctyp_of target_sign;
   4.237  
   4.238        (* fix all non-instantiated tvars *)
   4.239 -      val (fixtyinsts, othertfrees) = 
   4.240 +      val (fixtyinsts, othertfrees) =
   4.241            mk_fixtvar_tyinsts nonfixed_typinsts
   4.242                               [Thm.prop_of rule, Thm.prop_of target_thm];
   4.243 -      val new_fixed_typs = map (fn ((s,i),(srt,ty)) => (Term.dest_TFree ty))
   4.244 -                               fixtyinsts;
   4.245        val typinsts = cross_inst_typs (nonfixed_typinsts @ fixtyinsts);
   4.246  
   4.247        (* certified instantiations for types *)
   4.248 -      val ctyp_insts = 
   4.249 -          map (fn (ix,(s,ty)) => (ctypeify (TVar (ix,s)), ctypeify ty)) 
   4.250 +      val ctyp_insts =
   4.251 +          map (fn (ix,(s,ty)) => (ctypeify (TVar (ix,s)), ctypeify ty))
   4.252                typinsts;
   4.253  
   4.254        (* type instantiated versions *)
   4.255        val tgt_th_tyinst = Thm.instantiate (ctyp_insts,[]) target_thm;
   4.256        val rule_tyinst =  Thm.instantiate (ctyp_insts,[]) rule;
   4.257  
   4.258 -      val term_typ_inst = map (fn (ix,(srt,ty)) => (ix,ty)) typinsts;
   4.259 +      val term_typ_inst = map (fn (ix,(_,ty)) => (ix,ty)) typinsts;
   4.260        (* type instanitated outer term *)
   4.261        val outerterm_tyinst = Term.subst_TVars term_typ_inst outerterm;
   4.262  
   4.263 -      val FakeTs_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) 
   4.264 +      val FakeTs_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst))
   4.265                                FakeTs;
   4.266 -      val Ts_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) 
   4.267 +      val Ts_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst))
   4.268                            Ts;
   4.269  
   4.270        (* type-instantiate the var instantiations *)
   4.271 -      val insts_tyinst = List.foldr (fn ((ix,(ty,t)),insts_tyinst) => 
   4.272 -                            (ix, (Term.typ_subst_TVars term_typ_inst ty, 
   4.273 +      val insts_tyinst = List.foldr (fn ((ix,(ty,t)),insts_tyinst) =>
   4.274 +                            (ix, (Term.typ_subst_TVars term_typ_inst ty,
   4.275                                    Term.subst_TVars term_typ_inst t))
   4.276                              :: insts_tyinst)
   4.277                          [] unprepinsts;
   4.278 @@ -256,36 +226,36 @@
   4.279        val insts_tyinst_inst = cross_inst insts_tyinst;
   4.280  
   4.281        (* create certms of instantiations *)
   4.282 -      val cinsts_tyinst = 
   4.283 -          map (fn (ix,(ty,t)) => (ctermify (Var (ix, ty)), 
   4.284 +      val cinsts_tyinst =
   4.285 +          map (fn (ix,(ty,t)) => (ctermify (Var (ix, ty)),
   4.286                                    ctermify t)) insts_tyinst_inst;
   4.287  
   4.288        (* The instantiated rule *)
   4.289        val rule_inst = rule_tyinst |> Thm.instantiate ([], cinsts_tyinst);
   4.290  
   4.291        (* Create a table of vars to be renamed after instantiation - ie
   4.292 -      other uninstantiated vars in the hyps the *instantiated* rule 
   4.293 +      other uninstantiated vars in the hyps the *instantiated* rule
   4.294        ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *)
   4.295 -      val renamings = mk_renamings (Thm.prop_of tgt_th_tyinst) 
   4.296 +      val renamings = mk_renamings (Thm.prop_of tgt_th_tyinst)
   4.297                                     rule_inst;
   4.298 -      val cterm_renamings = 
   4.299 +      val cterm_renamings =
   4.300            map (fn (x,y) => (ctermify (Var x), ctermify y)) renamings;
   4.301  
   4.302        (* Create the specific version of the rule for this target application *)
   4.303 -      val outerterm_inst = 
   4.304 -          outerterm_tyinst 
   4.305 +      val outerterm_inst =
   4.306 +          outerterm_tyinst
   4.307              |> Term.subst_Vars (map (fn (ix,(ty,t)) => (ix,t)) insts_tyinst_inst)
   4.308              |> Term.subst_Vars (map (fn ((ix,ty),t) => (ix,t)) renamings);
   4.309        val couter_inst = Thm.reflexive (ctermify outerterm_inst);
   4.310 -      val (cprems, abstract_rule_inst) = 
   4.311 +      val (cprems, abstract_rule_inst) =
   4.312            rule_inst |> Thm.instantiate ([], cterm_renamings)
   4.313                      |> mk_abstractedrule FakeTs_tyinst Ts_tyinst;
   4.314 -      val specific_tgt_rule = 
   4.315 +      val specific_tgt_rule =
   4.316            beta_eta_contract
   4.317              (Thm.combination couter_inst abstract_rule_inst);
   4.318  
   4.319        (* create an instantiated version of the target thm *)
   4.320 -      val tgt_th_inst = 
   4.321 +      val tgt_th_inst =
   4.322            tgt_th_tyinst |> Thm.instantiate ([], cinsts_tyinst)
   4.323                          |> Thm.instantiate ([], cterm_renamings);
   4.324  
   4.325 @@ -302,4 +272,4 @@
   4.326      end;
   4.327  
   4.328  
   4.329 -end; (* struct *)
   4.330 +end;
     5.1 --- a/src/Tools/IsaPlanner/rw_tools.ML	Wed Sep 12 17:26:05 2012 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,179 +0,0 @@
     5.4 -(*  Title:      Tools/IsaPlanner/rw_tools.ML
     5.5 -    Author:     Lucas Dixon, University of Edinburgh
     5.6 -
     5.7 -Term related tools used for rewriting.
     5.8 -*)   
     5.9 -
    5.10 -signature RWTOOLS =
    5.11 -sig
    5.12 -end;
    5.13 -
    5.14 -structure RWTools 
    5.15 -= struct
    5.16 -
    5.17 -(* fake free variable names for locally bound variables - these work
    5.18 -as placeholders. *)
    5.19 -
    5.20 -(* don't use dest_fake.. - we should instead be working with numbers
    5.21 -and a list... else we rely on naming conventions which can break, or
    5.22 -be violated - in contrast list locations are correct by
    5.23 -construction/definition. *)
    5.24 -(*
    5.25 -fun dest_fake_bound_name n = 
    5.26 -    case (raw_explode n) of   (* FIXME Symbol.explode (?) *)
    5.27 -      (":" :: realchars) => implode realchars
    5.28 -    | _ => n; *)
    5.29 -fun is_fake_bound_name n = (hd (raw_explode n) = ":");  (* FIXME Symbol.explode (?) *)
    5.30 -fun mk_fake_bound_name n = ":b_" ^ n;
    5.31 -
    5.32 -
    5.33 -
    5.34 -(* fake free variable names for local meta variables - these work
    5.35 -as placeholders. *)
    5.36 -fun dest_fake_fix_name n = 
    5.37 -    case (raw_explode n) of  (* FIXME Symbol.explode (?) *)
    5.38 -      ("@" :: realchars) => implode realchars
    5.39 -    | _ => n;
    5.40 -fun is_fake_fix_name n = (hd (raw_explode n) = "@");  (* FIXME Symbol.explode (?) *)
    5.41 -fun mk_fake_fix_name n = "@" ^ n;
    5.42 -
    5.43 -
    5.44 -
    5.45 -(* fake free variable names for meta level bound variables *)
    5.46 -fun dest_fake_all_name n = 
    5.47 -    case (raw_explode n) of   (* FIXME Symbol.explode (?) *)
    5.48 -      ("+" :: realchars) => implode realchars
    5.49 -    | _ => n;
    5.50 -fun is_fake_all_name n = (hd (raw_explode n) = "+");  (* FIXME Symbol.explode (?) *)
    5.51 -fun mk_fake_all_name n = "+" ^ n;
    5.52 -
    5.53 -
    5.54 -
    5.55 -
    5.56 -(* Ys and Ts not used, Ns are real names of faked local bounds, the
    5.57 -idea is that this will be mapped to free variables thus if a free
    5.58 -variable is a faked local bound then we change it to being a meta
    5.59 -variable so that it can later be instantiated *)
    5.60 -(* FIXME: rename this - avoid the word fix! *)
    5.61 -(* note we are not really "fix"'ing the free, more like making it variable! *)
    5.62 -(* fun trymkvar_of_fakefree (Ns, Ts) Ys (n,ty) = 
    5.63 -    if n mem Ns then Var((n,0),ty) else Free (n,ty);
    5.64 -*)
    5.65 -
    5.66 -(* make a var into a fixed free (ie prefixed with "@") *)
    5.67 -fun mk_fakefixvar Ts ((n,i),ty) = Free(mk_fake_fix_name n, ty);
    5.68 -
    5.69 -
    5.70 -(* mk_frees_bound: string list -> Term.term -> Term.term *)
    5.71 -(* This function changes free variables to being represented as bound
    5.72 -variables if the free's variable name is in the given list. The debruijn 
    5.73 -index is simply the position in the list *)
    5.74 -(* THINKABOUT: danger of an existing free variable with the same name: fix
    5.75 -this so that name conflict are avoided automatically! In the meantime,
    5.76 -don't have free variables named starting with a ":" *)
    5.77 -fun bounds_of_fakefrees Ys (a $ b) = 
    5.78 -    (bounds_of_fakefrees Ys a) $ (bounds_of_fakefrees Ys b)
    5.79 -  | bounds_of_fakefrees Ys (Abs(n,ty,t)) = 
    5.80 -    Abs(n,ty, bounds_of_fakefrees (n::Ys) t)
    5.81 -  | bounds_of_fakefrees Ys (Free (n,ty)) = 
    5.82 -    let fun try_mk_bound_of_free (i,[]) = Free (n,ty)
    5.83 -          | try_mk_bound_of_free (i,(y::ys)) = 
    5.84 -            if n = y then Bound i else try_mk_bound_of_free (i+1,ys)
    5.85 -    in try_mk_bound_of_free (0,Ys) end
    5.86 -  | bounds_of_fakefrees Ys t = t;
    5.87 -
    5.88 -
    5.89 -(* map a function f onto each free variables *)
    5.90 -fun map_to_frees f Ys (a $ b) = 
    5.91 -    (map_to_frees f Ys a) $ (map_to_frees f Ys b)
    5.92 -  | map_to_frees f Ys (Abs(n,ty,t)) = 
    5.93 -    Abs(n,ty, map_to_frees f ((n,ty)::Ys) t)
    5.94 -  | map_to_frees f Ys (Free a) = 
    5.95 -    f Ys a
    5.96 -  | map_to_frees f Ys t = t;
    5.97 -
    5.98 -
    5.99 -(* map a function f onto each meta variable  *)
   5.100 -fun map_to_vars f Ys (a $ b) = 
   5.101 -    (map_to_vars f Ys a) $ (map_to_vars f Ys b)
   5.102 -  | map_to_vars f Ys (Abs(n,ty,t)) = 
   5.103 -    Abs(n,ty, map_to_vars f ((n,ty)::Ys) t)
   5.104 -  | map_to_vars f Ys (Var a) = 
   5.105 -    f Ys a
   5.106 -  | map_to_vars f Ys t = t;
   5.107 -
   5.108 -(* map a function f onto each free variables *)
   5.109 -fun map_to_alls f (Const("all",allty) $ Abs(n,ty,t)) = 
   5.110 -    let val (n2,ty2) = f (n,ty) 
   5.111 -    in (Const("all",allty) $ Abs(n2,ty2,map_to_alls f t)) end
   5.112 -  | map_to_alls f x = x;
   5.113 -
   5.114 -(* map a function f to each type variable in a term *)
   5.115 -(* implicit arg: term *)
   5.116 -fun map_to_term_tvars f =
   5.117 -    Term.map_types (fn TVar(ix,ty) => f (ix,ty) | x => x);   (* FIXME map_atyps !? *)
   5.118 -
   5.119 -
   5.120 -
   5.121 -(* what if a param desn't occur in the concl? think about! Note: This
   5.122 -simply fixes meta level univ bound vars as Frees.  At the end, we will
   5.123 -change them back to schematic vars that will then unify
   5.124 -appropriactely, ie with unfake_vars *)
   5.125 -fun fake_concl_of_goal gt i = 
   5.126 -    let 
   5.127 -      val prems = Logic.strip_imp_prems gt
   5.128 -      val sgt = nth prems (i - 1)
   5.129 -
   5.130 -      val tbody = Logic.strip_imp_concl (Term.strip_all_body sgt)
   5.131 -      val tparams = Term.strip_all_vars sgt
   5.132 -
   5.133 -      val fakefrees = map (fn (n, ty) => Free(mk_fake_all_name n, ty)) 
   5.134 -                          tparams
   5.135 -    in
   5.136 -      Term.subst_bounds (rev fakefrees,tbody)
   5.137 -    end;
   5.138 -
   5.139 -(* what if a param desn't occur in the concl? think about! Note: This
   5.140 -simply fixes meta level univ bound vars as Frees.  At the end, we will
   5.141 -change them back to schematic vars that will then unify
   5.142 -appropriactely, ie with unfake_vars *)
   5.143 -fun fake_goal gt i = 
   5.144 -    let 
   5.145 -      val prems = Logic.strip_imp_prems gt
   5.146 -      val sgt = nth prems (i - 1)
   5.147 -
   5.148 -      val tbody = Term.strip_all_body sgt
   5.149 -      val tparams = Term.strip_all_vars sgt
   5.150 -
   5.151 -      val fakefrees = map (fn (n, ty) => Free(mk_fake_all_name n, ty)) 
   5.152 -                          tparams
   5.153 -    in
   5.154 -      Term.subst_bounds (rev fakefrees,tbody)
   5.155 -    end;
   5.156 -
   5.157 -
   5.158 -(* hand written - for some reason the Isabelle version in drule is broken!
   5.159 -Example? something to do with Bin Yangs examples? 
   5.160 - *)
   5.161 -fun rename_term_bvars ns (Abs(s,ty,t)) = 
   5.162 -    let val s2opt = Library.find_first (fn (x,y) => s = x) ns
   5.163 -    in case s2opt of 
   5.164 -         NONE => (Abs(s,ty,rename_term_bvars  ns t))
   5.165 -       | SOME (_,s2) => Abs(s2,ty, rename_term_bvars ns t) end
   5.166 -  | rename_term_bvars ns (a$b) = 
   5.167 -    (rename_term_bvars ns a) $ (rename_term_bvars ns b)
   5.168 -  | rename_term_bvars _ x = x;
   5.169 -
   5.170 -fun rename_thm_bvars ns th = 
   5.171 -    let val t = Thm.prop_of th 
   5.172 -    in Thm.rename_boundvars t (rename_term_bvars ns t) th end;
   5.173 -
   5.174 -(* Finish this to show how it breaks! (raises the exception): 
   5.175 -
   5.176 -exception rename_thm_bvars_exp of ((string * string) list * Thm.thm)
   5.177 -
   5.178 -    Drule.rename_bvars ns th 
   5.179 -    handle TERM _ => raise rename_thm_bvars_exp (ns, th); 
   5.180 -*)
   5.181 -
   5.182 -end;
     6.1 --- a/src/Tools/eqsubst.ML	Wed Sep 12 17:26:05 2012 +0200
     6.2 +++ b/src/Tools/eqsubst.ML	Wed Sep 12 22:00:29 2012 +0200
     6.3 @@ -19,99 +19,47 @@
     6.4         * int (* maxidx *)
     6.5         * Zipper.T (* focusterm to search under *)
     6.6  
     6.7 -    exception eqsubst_occL_exp of
     6.8 -       string * int list * thm list * int * thm
     6.9 -    
    6.10 -    (* low level substitution functions *)
    6.11 -    val apply_subst_in_asm :
    6.12 -       int ->
    6.13 -       thm ->
    6.14 -       thm ->
    6.15 -       (cterm list * int * 'a * thm) * match -> thm Seq.seq
    6.16 -    val apply_subst_in_concl :
    6.17 -       int ->
    6.18 -       thm ->
    6.19 -       cterm list * thm ->
    6.20 -       thm -> match -> thm Seq.seq
    6.21 +  datatype 'a skipseq = SkipMore of int | SkipSeq of 'a Seq.seq Seq.seq
    6.22  
    6.23 -    (* matching/unification within zippers *)
    6.24 -    val clean_match_z :
    6.25 -       theory -> term -> Zipper.T -> match option
    6.26 -    val clean_unify_z :
    6.27 -       theory -> int -> term -> Zipper.T -> match Seq.seq
    6.28 -
    6.29 -    (* skipping things in seq seq's *)
    6.30 -
    6.31 -   (* skipping non-empty sub-sequences but when we reach the end
    6.32 -      of the seq, remembering how much we have left to skip. *)
    6.33 -    datatype 'a skipseq = SkipMore of int
    6.34 -      | SkipSeq of 'a Seq.seq Seq.seq;
    6.35 -
    6.36 -    val skip_first_asm_occs_search :
    6.37 -       ('a -> 'b -> 'c Seq.seq Seq.seq) ->
    6.38 -       'a -> int -> 'b -> 'c skipseq
    6.39 -    val skip_first_occs_search :
    6.40 -       int -> ('a -> 'b -> 'c Seq.seq Seq.seq) -> 'a -> 'b -> 'c Seq.seq
    6.41 -    val skipto_skipseq : int -> 'a Seq.seq Seq.seq -> 'a skipseq
    6.42 +  val skip_first_asm_occs_search :
    6.43 +     ('a -> 'b -> 'c Seq.seq Seq.seq) ->
    6.44 +     'a -> int -> 'b -> 'c skipseq
    6.45 +  val skip_first_occs_search :
    6.46 +     int -> ('a -> 'b -> 'c Seq.seq Seq.seq) -> 'a -> 'b -> 'c Seq.seq
    6.47 +  val skipto_skipseq : int -> 'a Seq.seq Seq.seq -> 'a skipseq
    6.48  
    6.49 -    (* tactics *)
    6.50 -    val eqsubst_asm_tac :
    6.51 -       Proof.context ->
    6.52 -       int list -> thm list -> int -> tactic
    6.53 -    val eqsubst_asm_tac' :
    6.54 -       Proof.context ->
    6.55 -       (searchinfo -> int -> term -> match skipseq) ->
    6.56 -       int -> thm -> int -> tactic
    6.57 -    val eqsubst_tac :
    6.58 -       Proof.context ->
    6.59 -       int list -> (* list of occurences to rewrite, use [0] for any *)
    6.60 -       thm list -> int -> tactic
    6.61 -    val eqsubst_tac' :
    6.62 -       Proof.context -> (* proof context *)
    6.63 -       (searchinfo -> term -> match Seq.seq) (* search function *)
    6.64 -       -> thm (* equation theorem to rewrite with *)
    6.65 -       -> int (* subgoal number in goal theorem *)
    6.66 -       -> thm (* goal theorem *)
    6.67 -       -> thm Seq.seq (* rewritten goal theorem *)
    6.68 -
    6.69 -
    6.70 -    val fakefree_badbounds :
    6.71 -       (string * typ) list ->
    6.72 -       term ->
    6.73 -       (string * typ) list * (string * typ) list * term
    6.74 +  (* tactics *)
    6.75 +  val eqsubst_asm_tac :
    6.76 +     Proof.context ->
    6.77 +     int list -> thm list -> int -> tactic
    6.78 +  val eqsubst_asm_tac' :
    6.79 +     Proof.context ->
    6.80 +     (searchinfo -> int -> term -> match skipseq) ->
    6.81 +     int -> thm -> int -> tactic
    6.82 +  val eqsubst_tac :
    6.83 +     Proof.context ->
    6.84 +     int list -> (* list of occurences to rewrite, use [0] for any *)
    6.85 +     thm list -> int -> tactic
    6.86 +  val eqsubst_tac' :
    6.87 +     Proof.context -> (* proof context *)
    6.88 +     (searchinfo -> term -> match Seq.seq) (* search function *)
    6.89 +     -> thm (* equation theorem to rewrite with *)
    6.90 +     -> int (* subgoal number in goal theorem *)
    6.91 +     -> thm (* goal theorem *)
    6.92 +     -> thm Seq.seq (* rewritten goal theorem *)
    6.93  
    6.94 -    val mk_foo_match :
    6.95 -       (term -> term) ->
    6.96 -       ('a * typ) list -> term -> term
    6.97 +  (* search for substitutions *)
    6.98 +  val valid_match_start : Zipper.T -> bool
    6.99 +  val search_lr_all : Zipper.T -> Zipper.T Seq.seq
   6.100 +  val search_lr_valid : (Zipper.T -> bool) -> Zipper.T -> Zipper.T Seq.seq
   6.101 +  val searchf_lr_unify_all :
   6.102 +     searchinfo -> term -> match Seq.seq Seq.seq
   6.103 +  val searchf_lr_unify_valid :
   6.104 +     searchinfo -> term -> match Seq.seq Seq.seq
   6.105 +  val searchf_bt_unify_valid :
   6.106 +     searchinfo -> term -> match Seq.seq Seq.seq
   6.107  
   6.108 -    (* preparing substitution *)
   6.109 -    val prep_meta_eq : Proof.context -> thm -> thm list
   6.110 -    val prep_concl_subst :
   6.111 -       int -> thm -> (cterm list * thm) * searchinfo
   6.112 -    val prep_subst_in_asm :
   6.113 -       int -> thm -> int ->
   6.114 -       (cterm list * int * int * thm) * searchinfo
   6.115 -    val prep_subst_in_asms :
   6.116 -       int -> thm ->
   6.117 -       ((cterm list * int * int * thm) * searchinfo) list
   6.118 -    val prep_zipper_match :
   6.119 -       Zipper.T -> term * ((string * typ) list * (string * typ) list * term)
   6.120 -
   6.121 -    (* search for substitutions *)
   6.122 -    val valid_match_start : Zipper.T -> bool
   6.123 -    val search_lr_all : Zipper.T -> Zipper.T Seq.seq
   6.124 -    val search_lr_valid : (Zipper.T -> bool) -> Zipper.T -> Zipper.T Seq.seq
   6.125 -    val searchf_lr_unify_all :
   6.126 -       searchinfo -> term -> match Seq.seq Seq.seq
   6.127 -    val searchf_lr_unify_valid :
   6.128 -       searchinfo -> term -> match Seq.seq Seq.seq
   6.129 -    val searchf_bt_unify_valid :
   6.130 -       searchinfo -> term -> match Seq.seq Seq.seq
   6.131 -
   6.132 -    (* Isar level hooks *)
   6.133 -    val eqsubst_asm_meth : Proof.context -> int list -> thm list -> Proof.method
   6.134 -    val eqsubst_meth : Proof.context -> int list -> thm list -> Proof.method
   6.135 -    val setup : theory -> theory
   6.136 +  val setup : theory -> theory
   6.137  
   6.138  end;
   6.139  
   6.140 @@ -142,25 +90,25 @@
   6.141  datatype 'a skipseq = SkipMore of int
   6.142    | SkipSeq of 'a Seq.seq Seq.seq;
   6.143  (* given a seqseq, skip the first m non-empty seq's, note deficit *)
   6.144 -fun skipto_skipseq m s = 
   6.145 -    let 
   6.146 -      fun skip_occs n sq = 
   6.147 -          case Seq.pull sq of 
   6.148 +fun skipto_skipseq m s =
   6.149 +    let
   6.150 +      fun skip_occs n sq =
   6.151 +          case Seq.pull sq of
   6.152              NONE => SkipMore n
   6.153 -          | SOME (h,t) => 
   6.154 +          | SOME (h,t) =>
   6.155              (case Seq.pull h of NONE => skip_occs n t
   6.156               | SOME _ => if n <= 1 then SkipSeq (Seq.cons h t)
   6.157                           else skip_occs (n - 1) t)
   6.158      in (skip_occs m s) end;
   6.159  
   6.160 -(* note: outerterm is the taget with the match replaced by a bound 
   6.161 -         variable : ie: "P lhs" beocmes "%x. P x" 
   6.162 +(* note: outerterm is the taget with the match replaced by a bound
   6.163 +         variable : ie: "P lhs" beocmes "%x. P x"
   6.164           insts is the types of instantiations of vars in lhs
   6.165           and typinsts is the type instantiations of types in the lhs
   6.166 -         Note: Final rule is the rule lifted into the ontext of the 
   6.167 +         Note: Final rule is the rule lifted into the ontext of the
   6.168           taget thm. *)
   6.169 -fun mk_foo_match mkuptermfunc Ts t = 
   6.170 -    let 
   6.171 +fun mk_foo_match mkuptermfunc Ts t =
   6.172 +    let
   6.173        val ty = Term.type_of t
   6.174        val bigtype = (rev (map snd Ts)) ---> ty
   6.175        fun mk_foo 0 t = t
   6.176 @@ -172,12 +120,13 @@
   6.177  
   6.178  (* T is outer bound vars, n is number of locally bound vars *)
   6.179  (* THINK: is order of Ts correct...? or reversed? *)
   6.180 -fun fakefree_badbounds Ts t = 
   6.181 -    let val (FakeTs,Ts,newnames) = 
   6.182 -            List.foldr (fn ((n,ty),(FakeTs,Ts,usednames)) => 
   6.183 +fun mk_fake_bound_name n = ":b_" ^ n;
   6.184 +fun fakefree_badbounds Ts t =
   6.185 +    let val (FakeTs,Ts,newnames) =
   6.186 +            List.foldr (fn ((n,ty),(FakeTs,Ts,usednames)) =>
   6.187                             let val newname = singleton (Name.variant_list usednames) n
   6.188 -                           in ((RWTools.mk_fake_bound_name newname,ty)::FakeTs,
   6.189 -                               (newname,ty)::Ts, 
   6.190 +                           in ((mk_fake_bound_name newname,ty)::FakeTs,
   6.191 +                               (newname,ty)::Ts,
   6.192                                 newname::usednames) end)
   6.193                         ([],[],[])
   6.194                         Ts
   6.195 @@ -187,9 +136,9 @@
   6.196  abstraction. In this function we additionally construct the
   6.197  abstraction environment, and an outer context term (with the focus
   6.198  abstracted out) for use in rewriting with RWInst.rw *)
   6.199 -fun prep_zipper_match z = 
   6.200 -    let 
   6.201 -      val t = Zipper.trm z  
   6.202 +fun prep_zipper_match z =
   6.203 +    let
   6.204 +      val t = Zipper.trm z
   6.205        val c = Zipper.ctxt z
   6.206        val Ts = Zipper.C.nty_ctxt c
   6.207        val (FakeTs', Ts', t') = fakefree_badbounds Ts t
   6.208 @@ -198,12 +147,7 @@
   6.209        (t', (FakeTs', Ts', absterm))
   6.210      end;
   6.211  
   6.212 -(* Matching and Unification with exception handled *)
   6.213 -fun clean_match thy (a as (pat, t)) =
   6.214 -  let val (tyenv, tenv) = Pattern.match thy a (Vartab.empty, Vartab.empty)
   6.215 -  in SOME (Vartab.dest tyenv, Vartab.dest tenv)
   6.216 -  end handle Pattern.MATCH => NONE;
   6.217 -
   6.218 +(* Unification with exception handled *)
   6.219  (* given theory, max var index, pat, tgt; returns Seq of instantiations *)
   6.220  fun clean_unify thry ix (a as (pat, tgt)) =
   6.221      let
   6.222 @@ -242,41 +186,18 @@
   6.223        | NONE => Seq.empty
   6.224      end;
   6.225  
   6.226 -(* Matching and Unification for zippers *)
   6.227 +(* Unification for zippers *)
   6.228  (* Note: Ts is a modified version of the original names of the outer
   6.229  bound variables. New names have been introduced to make sure they are
   6.230  unique w.r.t all names in the term and each other. usednames' is
   6.231  oldnames + new names. *)
   6.232 -fun clean_match_z thy pat z = 
   6.233 -    let val (t, (FakeTs,Ts,absterm)) = prep_zipper_match z in
   6.234 -      case clean_match thy (pat, t) of 
   6.235 -        NONE => NONE 
   6.236 -      | SOME insts => SOME (insts, FakeTs, Ts, absterm) end;
   6.237  (* ix = max var index *)
   6.238 -fun clean_unify_z sgn ix pat z = 
   6.239 +fun clean_unify_z sgn ix pat z =
   6.240      let val (t, (FakeTs, Ts,absterm)) = prep_zipper_match z in
   6.241 -    Seq.map (fn insts => (insts, FakeTs, Ts, absterm)) 
   6.242 +    Seq.map (fn insts => (insts, FakeTs, Ts, absterm))
   6.243              (clean_unify sgn ix (t, pat)) end;
   6.244  
   6.245  
   6.246 -(* FOR DEBUGGING...
   6.247 -type trace_subst_errT = int (* subgoal *)
   6.248 -        * thm (* thm with all goals *)
   6.249 -        * (cterm list (* certified free var placeholders for vars *)
   6.250 -           * thm)  (* trivial thm of goal concl *)
   6.251 -            (* possible matches/unifiers *)
   6.252 -        * thm (* rule *)
   6.253 -        * (((indexname * typ) list (* type instantiations *)
   6.254 -              * (indexname * term) list ) (* term instantiations *)
   6.255 -             * (string * typ) list (* Type abs env *)
   6.256 -             * term) (* outer term *);
   6.257 -
   6.258 -val trace_subst_err = (Unsynchronized.ref NONE : trace_subst_errT option Unsynchronized.ref);
   6.259 -val trace_subst_search = Unsynchronized.ref false;
   6.260 -exception trace_subst_exp of trace_subst_errT;
   6.261 -*)
   6.262 -
   6.263 -
   6.264  fun bot_left_leaf_of (l $ r) = bot_left_leaf_of l
   6.265    | bot_left_leaf_of (Abs(s,ty,t)) = bot_left_leaf_of t
   6.266    | bot_left_leaf_of x = x;
   6.267 @@ -284,8 +205,8 @@
   6.268  (* Avoid considering replacing terms which have a var at the head as
   6.269     they always succeed trivially, and uninterestingly. *)
   6.270  fun valid_match_start z =
   6.271 -    (case bot_left_leaf_of (Zipper.trm z) of 
   6.272 -      Var _ => false 
   6.273 +    (case bot_left_leaf_of (Zipper.trm z) of
   6.274 +      Var _ => false
   6.275        | _ => true);
   6.276  
   6.277  (* search from top, left to right, then down *)
   6.278 @@ -293,12 +214,12 @@
   6.279  
   6.280  (* search from top, left to right, then down *)
   6.281  fun search_lr_valid validf =
   6.282 -    let 
   6.283 -      fun sf_valid_td_lr z = 
   6.284 +    let
   6.285 +      fun sf_valid_td_lr z =
   6.286            let val here = if validf z then [Zipper.Here z] else [] in
   6.287 -            case Zipper.trm z 
   6.288 -             of _ $ _ => [Zipper.LookIn (Zipper.move_down_left z)] 
   6.289 -                         @ here 
   6.290 +            case Zipper.trm z
   6.291 +             of _ $ _ => [Zipper.LookIn (Zipper.move_down_left z)]
   6.292 +                         @ here
   6.293                           @ [Zipper.LookIn (Zipper.move_down_right z)]
   6.294                | Abs _ => here @ [Zipper.LookIn (Zipper.move_down_abs z)]
   6.295                | _ => here
   6.296 @@ -308,11 +229,11 @@
   6.297  (* search from bottom to top, left to right *)
   6.298  
   6.299  fun search_bt_valid validf =
   6.300 -    let 
   6.301 -      fun sf_valid_td_lr z = 
   6.302 +    let
   6.303 +      fun sf_valid_td_lr z =
   6.304            let val here = if validf z then [Zipper.Here z] else [] in
   6.305 -            case Zipper.trm z 
   6.306 -             of _ $ _ => [Zipper.LookIn (Zipper.move_down_left z), 
   6.307 +            case Zipper.trm z
   6.308 +             of _ $ _ => [Zipper.LookIn (Zipper.move_down_left z),
   6.309                            Zipper.LookIn (Zipper.move_down_right z)] @ here
   6.310                | Abs _ => [Zipper.LookIn (Zipper.move_down_abs z)] @ here
   6.311                | _ => here
   6.312 @@ -320,7 +241,7 @@
   6.313      in Zipper.lzy_search sf_valid_td_lr end;
   6.314  
   6.315  fun searchf_unify_gen f (sgn, maxidx, z) lhs =
   6.316 -    Seq.map (clean_unify_z sgn maxidx lhs) 
   6.317 +    Seq.map (clean_unify_z sgn maxidx lhs)
   6.318              (Zipper.limit_apply f z);
   6.319  
   6.320  (* search all unifications *)
   6.321 @@ -328,7 +249,7 @@
   6.322      searchf_unify_gen search_lr_all;
   6.323  
   6.324  (* search only for 'valid' unifiers (non abs subterms and non vars) *)
   6.325 -val searchf_lr_unify_valid = 
   6.326 +val searchf_lr_unify_valid =
   6.327      searchf_unify_gen (search_lr_valid valid_match_start);
   6.328  
   6.329  val searchf_bt_unify_valid =
   6.330 @@ -390,8 +311,6 @@
   6.331     the given theorems*)
   6.332  
   6.333  
   6.334 -exception eqsubst_occL_exp of
   6.335 -          string * (int list) * (thm list) * int * thm;
   6.336  fun skip_first_occs_search occ srchf sinfo lhs =
   6.337      case (skipto_skipseq occ (srchf sinfo lhs)) of
   6.338        SkipMore _ => Seq.empty
   6.339 @@ -408,8 +327,8 @@
   6.340        let val thmseq = (Seq.of_list thms)
   6.341          fun apply_occ occ th =
   6.342              thmseq |> Seq.maps
   6.343 -                    (fn r => eqsubst_tac' 
   6.344 -                               ctxt 
   6.345 +                    (fn r => eqsubst_tac'
   6.346 +                               ctxt
   6.347                                 (skip_first_occs_search
   6.348                                    occ searchf_lr_unify_valid) r
   6.349                                   (i + ((Thm.nprems_of th) - nprems))
   6.350 @@ -419,8 +338,7 @@
   6.351        in
   6.352          Seq.map distinct_subgoals (Seq.EVERY (map apply_occ sortedoccL) th)
   6.353        end
   6.354 -    end
   6.355 -    handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
   6.356 +    end;
   6.357  
   6.358  
   6.359  (* inthms are the given arguments in Isar, and treated as eqstep with
   6.360 @@ -534,8 +452,7 @@
   6.361          Seq.map distinct_subgoals
   6.362                  (Seq.EVERY (map apply_occ sortedoccs) th)
   6.363        end
   6.364 -    end
   6.365 -    handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
   6.366 +    end;
   6.367  
   6.368  (* inthms are the given arguments in Isar, and treated as eqstep with
   6.369     the first one, then the second etc *)