moved IsaPlanner from Provers to Tools;
authorwenzelm
Thu May 31 20:55:29 2007 +0200 (2007-05-31)
changeset 23171861f63a35d31
parent 23170 94e9413bd7fc
child 23172 f1ae6a8648ef
moved IsaPlanner from Provers to Tools;
src/FOL/IFOL.thy
src/FOL/IsaMakefile
src/HOL/HOL.thy
src/Provers/IsaPlanner/ROOT.ML
src/Provers/IsaPlanner/isand.ML
src/Provers/IsaPlanner/rw_inst.ML
src/Provers/IsaPlanner/rw_tools.ML
src/Provers/IsaPlanner/zipper.ML
src/Tools/IsaPlanner/README
src/Tools/IsaPlanner/isand.ML
src/Tools/IsaPlanner/rw_inst.ML
src/Tools/IsaPlanner/rw_tools.ML
src/Tools/IsaPlanner/zipper.ML
     1.1 --- a/src/FOL/IFOL.thy	Thu May 31 19:11:19 2007 +0200
     1.2 +++ b/src/FOL/IFOL.thy	Thu May 31 20:55:29 2007 +0200
     1.3 @@ -10,10 +10,10 @@
     1.4  uses
     1.5    "~~/src/Provers/splitter.ML"
     1.6    "~~/src/Provers/hypsubst.ML"
     1.7 -  "~~/src/Provers/IsaPlanner/zipper.ML"
     1.8 -  "~~/src/Provers/IsaPlanner/isand.ML"
     1.9 -  "~~/src/Provers/IsaPlanner/rw_tools.ML"
    1.10 -  "~~/src/Provers/IsaPlanner/rw_inst.ML"
    1.11 +  "~~/src/Tools/IsaPlanner/zipper.ML"
    1.12 +  "~~/src/Tools/IsaPlanner/isand.ML"
    1.13 +  "~~/src/Tools/IsaPlanner/rw_tools.ML"
    1.14 +  "~~/src/Tools/IsaPlanner/rw_inst.ML"
    1.15    "~~/src/Provers/eqsubst.ML"
    1.16    "~~/src/Provers/induct_method.ML"
    1.17    "~~/src/Provers/classical.ML"
     2.1 --- a/src/FOL/IsaMakefile	Thu May 31 19:11:19 2007 +0200
     2.2 +++ b/src/FOL/IsaMakefile	Thu May 31 20:55:29 2007 +0200
     2.3 @@ -30,10 +30,10 @@
     2.4  
     2.5  $(OUT)/FOL$(ML_SUFFIX): $(OUT)/Pure$(ML_SUFFIX) $(SRC)/Provers/blast.ML	\
     2.6    $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML			\
     2.7 -  $(SRC)/Provers/IsaPlanner/zipper.ML \
     2.8 -  $(SRC)/Provers/IsaPlanner/isand.ML \
     2.9 -  $(SRC)/Provers/IsaPlanner/rw_tools.ML	\
    2.10 -  $(SRC)/Provers/IsaPlanner/rw_inst.ML \
    2.11 +  $(SRC)/Tools/IsaPlanner/zipper.ML \
    2.12 +  $(SRC)/Tools/IsaPlanner/isand.ML \
    2.13 +  $(SRC)/Tools/IsaPlanner/rw_tools.ML	\
    2.14 +  $(SRC)/Tools/IsaPlanner/rw_inst.ML \
    2.15    $(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML			\
    2.16    $(SRC)/Provers/induct_method.ML			\
    2.17    $(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML		\
     3.1 --- a/src/HOL/HOL.thy	Thu May 31 19:11:19 2007 +0200
     3.2 +++ b/src/HOL/HOL.thy	Thu May 31 20:55:29 2007 +0200
     3.3 @@ -11,10 +11,10 @@
     3.4    "hologic.ML"
     3.5    "~~/src/Provers/splitter.ML"
     3.6    "~~/src/Provers/hypsubst.ML"
     3.7 -  "~~/src/Provers/IsaPlanner/zipper.ML"
     3.8 -  "~~/src/Provers/IsaPlanner/isand.ML"
     3.9 -  "~~/src/Provers/IsaPlanner/rw_tools.ML"
    3.10 -  "~~/src/Provers/IsaPlanner/rw_inst.ML"
    3.11 +  "~~/src/Tools/IsaPlanner/zipper.ML"
    3.12 +  "~~/src/Tools/IsaPlanner/isand.ML"
    3.13 +  "~~/src/Tools/IsaPlanner/rw_tools.ML"
    3.14 +  "~~/src/Tools/IsaPlanner/rw_inst.ML"
    3.15    "~~/src/Provers/eqsubst.ML"
    3.16    "~~/src/Provers/induct_method.ML"
    3.17    "~~/src/Provers/classical.ML"
     4.1 --- a/src/Provers/IsaPlanner/ROOT.ML	Thu May 31 19:11:19 2007 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,16 +0,0 @@
     4.4 -(*  ID:         $Id$
     4.5 -    Author:     Lucas Dixon, University of Edinburgh
     4.6 -                lucas.dixon@ed.ac.uk
     4.7 -
     4.8 -The IsaPlanner subsystem.
     4.9 -*)
    4.10 -
    4.11 -(* Generic notion of term Zippers *)
    4.12 -use "zipper.ML";
    4.13 -
    4.14 -(* Some tools for manipulation of proofs following a ND style *)
    4.15 -use "isand.ML";
    4.16 -
    4.17 -(* some tools for rewriting *)
    4.18 -use "rw_tools.ML";
    4.19 -use "rw_inst.ML";
     5.1 --- a/src/Provers/IsaPlanner/isand.ML	Thu May 31 19:11:19 2007 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,642 +0,0 @@
     5.4 -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
     5.5 -(*  Title:      Pure/IsaPlanner/isand.ML
     5.6 -    ID:		$Id$
     5.7 -    Author:     Lucas Dixon, University of Edinburgh
     5.8 -                lucas.dixon@ed.ac.uk
     5.9 -    Updated:    26 Apr 2005
    5.10 -    Date:       6 Aug 2004
    5.11 -*)
    5.12 -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
    5.13 -(*  DESCRIPTION:
    5.14 -
    5.15 -    Natural Deduction tools
    5.16 -
    5.17 -    For working with Isabelle theorems in a natural detuction style.
    5.18 -    ie, not having to deal with meta level quantified varaibles,
    5.19 -    instead, we work with newly introduced frees, and hide the
    5.20 -    "all"'s, exporting results from theorems proved with the frees, to
    5.21 -    solve the all cases of the previous goal. This allows resolution
    5.22 -    to do proof search normally. 
    5.23 -
    5.24 -    Note: A nice idea: allow exporting to solve any subgoal, thus
    5.25 -    allowing the interleaving of proof, or provide a structure for the
    5.26 -    ordering of proof, thus allowing proof attempts in parrell, but
    5.27 -    recording the order to apply things in.
    5.28 -
    5.29 -    THINK: are we really ok with our varify name w.r.t the prop - do
    5.30 -    we also need to avoid names in the hidden hyps? What about
    5.31 -    unification contraints in flex-flex pairs - might they also have
    5.32 -    extra free vars?
    5.33 -*)
    5.34 -
    5.35 -signature ISA_ND =
    5.36 -sig
    5.37 -
    5.38 -  (* export data *)
    5.39 -  datatype export = export of
    5.40 -           {gth: Thm.thm, (* initial goal theorem *)
    5.41 -            sgid: int, (* subgoal id which has been fixed etc *)
    5.42 -            fixes: Thm.cterm list, (* frees *)
    5.43 -            assumes: Thm.cterm list} (* assumptions *)
    5.44 -  val fixes_of_exp : export -> Thm.cterm list
    5.45 -  val export_back : export -> Thm.thm -> Thm.thm Seq.seq
    5.46 -  val export_solution : export -> Thm.thm -> Thm.thm
    5.47 -  val export_solutions : export list * Thm.thm -> Thm.thm
    5.48 -
    5.49 -  (* inserting meta level params for frees in the conditions *)
    5.50 -  val allify_conditions :
    5.51 -      (Term.term -> Thm.cterm) ->
    5.52 -      (string * Term.typ) list -> Thm.thm -> Thm.thm * Thm.cterm list
    5.53 -  val allify_conditions' :
    5.54 -      (string * Term.typ) list -> Thm.thm -> Thm.thm * Thm.cterm list
    5.55 -  val assume_allified :
    5.56 -      theory -> (string * Term.sort) list * (string * Term.typ) list
    5.57 -      -> Term.term -> (Thm.cterm * Thm.thm)
    5.58 -
    5.59 -  (* meta level fixed params (i.e. !! vars) *)
    5.60 -  val fix_alls_in_term : Term.term -> Term.term * Term.term list
    5.61 -  val fix_alls_term : int -> Term.term -> Term.term * Term.term list
    5.62 -  val fix_alls_cterm : int -> Thm.thm -> Thm.cterm * Thm.cterm list
    5.63 -  val fix_alls' : int -> Thm.thm -> Thm.thm * Thm.cterm list
    5.64 -  val fix_alls : int -> Thm.thm -> Thm.thm * export
    5.65 -
    5.66 -  (* meta variables in types and terms *)
    5.67 -  val fix_tvars_to_tfrees_in_terms 
    5.68 -      : string list (* avoid these names *)
    5.69 -        -> Term.term list -> 
    5.70 -        (((string * int) * Term.sort) * (string * Term.sort)) list (* renamings *)
    5.71 -  val fix_vars_to_frees_in_terms
    5.72 -      : string list (* avoid these names *)
    5.73 -        -> Term.term list ->
    5.74 -        (((string * int) * Term.typ) * (string * Term.typ)) list (* renamings *)
    5.75 -  val fix_tvars_to_tfrees : Thm.thm -> Thm.ctyp list * Thm.thm
    5.76 -  val fix_vars_to_frees : Thm.thm -> Thm.cterm list * Thm.thm
    5.77 -  val fix_vars_and_tvars : 
    5.78 -      Thm.thm -> (Thm.cterm list * Thm.ctyp list) * Thm.thm
    5.79 -  val fix_vars_upto_idx : int -> Thm.thm -> Thm.thm
    5.80 -  val fix_tvars_upto_idx : int -> Thm.thm -> Thm.thm
    5.81 -  val unfix_frees : Thm.cterm list -> Thm.thm -> Thm.thm
    5.82 -  val unfix_tfrees : Thm.ctyp list -> Thm.thm -> Thm.thm
    5.83 -  val unfix_frees_and_tfrees :
    5.84 -      (Thm.cterm list * Thm.ctyp list) -> Thm.thm -> Thm.thm
    5.85 -
    5.86 -  (* assumptions/subgoals *)
    5.87 -  val assume_prems :
    5.88 -      int -> Thm.thm -> Thm.thm list * Thm.thm * Thm.cterm list
    5.89 -  val fixed_subgoal_thms : Thm.thm -> Thm.thm list * (Thm.thm list -> Thm.thm)
    5.90 -  val fixes_and_assumes : int -> Thm.thm -> Thm.thm list * Thm.thm * export
    5.91 -  val hide_other_goals : Thm.thm -> Thm.thm * Thm.cterm list
    5.92 -  val hide_prems : Thm.thm -> Thm.thm * Thm.cterm list
    5.93 -
    5.94 -  (* abstracts cterms (vars) to locally meta-all bounds *)
    5.95 -  val prepare_goal_export : string list * Thm.cterm list -> Thm.thm 
    5.96 -                            -> int * Thm.thm
    5.97 -  val solve_with : Thm.thm -> Thm.thm -> Thm.thm Seq.seq
    5.98 -  val subgoal_thms : Thm.thm -> Thm.thm list * (Thm.thm list -> Thm.thm)
    5.99 -end
   5.100 -
   5.101 -
   5.102 -structure IsaND 
   5.103 -: ISA_ND
   5.104 -= struct
   5.105 -
   5.106 -(* Solve *some* subgoal of "th" directly by "sol" *)
   5.107 -(* Note: this is probably what Markus ment to do upon export of a
   5.108 -"show" but maybe he used RS/rtac instead, which would wrongly lead to
   5.109 -failing if there are premices to the shown goal. 
   5.110 -
   5.111 -given: 
   5.112 -sol : Thm.thm = [| Ai... |] ==> Ci
   5.113 -th : Thm.thm = 
   5.114 -  [| ... [| Ai... |] ==> Ci ... |] ==> G
   5.115 -results in: 
   5.116 -  [| ... [| Ai-1... |] ==> Ci-1
   5.117 -    [| Ai+1... |] ==> Ci+1 ...
   5.118 -  |] ==> G
   5.119 -i.e. solves some subgoal of th that is identical to sol. 
   5.120 -*)
   5.121 -fun solve_with sol th = 
   5.122 -    let fun solvei 0 = Seq.empty
   5.123 -          | solvei i = 
   5.124 -            Seq.append (bicompose false (false,sol,0) i th) (solvei (i - 1))
   5.125 -    in
   5.126 -      solvei (Thm.nprems_of th)
   5.127 -    end;
   5.128 -
   5.129 -
   5.130 -(* Given ctertmify function, (string,type) pairs capturing the free
   5.131 -vars that need to be allified in the assumption, and a theorem with
   5.132 -assumptions possibly containing the free vars, then we give back the
   5.133 -assumptions allified as hidden hyps. 
   5.134 -
   5.135 -Given: x 
   5.136 -th: A vs ==> B vs 
   5.137 -Results in: "B vs" [!!x. A x]
   5.138 -*)
   5.139 -fun allify_conditions ctermify Ts th = 
   5.140 -    let 
   5.141 -      val premts = Thm.prems_of th;
   5.142 -    
   5.143 -      fun allify_prem_var (vt as (n,ty),t)  = 
   5.144 -          (Term.all ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
   5.145 -
   5.146 -      fun allify_prem Ts p = foldr allify_prem_var p Ts
   5.147 -
   5.148 -      val cTs = map (ctermify o Free) Ts
   5.149 -      val cterm_asms = map (ctermify o allify_prem Ts) premts
   5.150 -      val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms
   5.151 -    in 
   5.152 -      (Library.foldl (fn (x,y) => y COMP x) (th, allifyied_asm_thms), cterm_asms)
   5.153 -    end;
   5.154 -
   5.155 -fun allify_conditions' Ts th = 
   5.156 -    allify_conditions (Thm.cterm_of (Thm.theory_of_thm th)) Ts th;
   5.157 -
   5.158 -(* allify types *)
   5.159 -fun allify_typ ts ty = 
   5.160 -    let 
   5.161 -      fun trec (x as (TFree (s,srt))) = 
   5.162 -          (case Library.find_first (fn (s2,srt2) => s = s2) ts
   5.163 -            of NONE => x
   5.164 -             | SOME (s2,_) => TVar ((s,0),srt))
   5.165 -            (*  Maybe add in check here for bad sorts? 
   5.166 -             if srt = srt2 then TVar ((s,0),srt) 
   5.167 -               else raise  ("thaw_typ", ts, ty) *)
   5.168 -          | trec (Type (s,typs)) = Type (s, map trec typs)
   5.169 -          | trec (v as TVar _) = v;
   5.170 -    in trec ty end;
   5.171 -
   5.172 -(* implicit types and term *)
   5.173 -fun allify_term_typs ty = Term.map_types (allify_typ ty);
   5.174 -
   5.175 -(* allified version of term, given frees to allify over. Note that we
   5.176 -only allify over the types on the given allified cterm, we can't do
   5.177 -this for the theorem as we are not allowed type-vars in the hyp. *)
   5.178 -(* FIXME: make the allified term keep the same conclusion as it
   5.179 -started with, rather than a strictly more general version (ie use
   5.180 -instantiate with initial params we abstracted from, rather than
   5.181 -forall_elim_vars. *)
   5.182 -fun assume_allified sgn (tyvs,vs) t = 
   5.183 -    let
   5.184 -      fun allify_var (vt as (n,ty),t)  = 
   5.185 -          (Term.all ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
   5.186 -      fun allify Ts p = List.foldr allify_var p Ts
   5.187 -
   5.188 -      val ctermify = Thm.cterm_of sgn;
   5.189 -      val cvars = map (fn (n,ty) => ctermify (Var ((n,0),ty))) vs
   5.190 -      val allified_term = t |> allify vs;
   5.191 -      val ct = ctermify allified_term;
   5.192 -      val typ_allified_ct = ctermify (allify_term_typs tyvs allified_term);
   5.193 -    in (typ_allified_ct, 
   5.194 -        Drule.forall_elim_vars 0 (Thm.assume ct)) end;
   5.195 -
   5.196 -
   5.197 -(* change type-vars to fresh type frees *)
   5.198 -fun fix_tvars_to_tfrees_in_terms names ts = 
   5.199 -    let 
   5.200 -      val tfree_names = map fst (List.foldr Term.add_term_tfrees [] ts);
   5.201 -      val tvars = List.foldr Term.add_term_tvars [] ts;
   5.202 -      val (names',renamings) = 
   5.203 -          List.foldr (fn (tv as ((n,i),s),(Ns,Rs)) => 
   5.204 -                         let val n2 = Name.variant Ns n in 
   5.205 -                           (n2::Ns, (tv, (n2,s))::Rs)
   5.206 -                         end) (tfree_names @ names,[]) tvars;
   5.207 -    in renamings end;
   5.208 -fun fix_tvars_to_tfrees th = 
   5.209 -    let 
   5.210 -      val sign = Thm.theory_of_thm th;
   5.211 -      val ctypify = Thm.ctyp_of sign;
   5.212 -      val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
   5.213 -      val renamings = fix_tvars_to_tfrees_in_terms 
   5.214 -                        [] ((Thm.prop_of th) :: tpairs);
   5.215 -      val crenamings = 
   5.216 -          map (fn (v,f) => (ctypify (TVar v), ctypify (TFree f)))
   5.217 -              renamings;
   5.218 -      val fixedfrees = map snd crenamings;
   5.219 -    in (fixedfrees, Thm.instantiate (crenamings, []) th) end;
   5.220 -
   5.221 -
   5.222 -(* change type-free's to type-vars in th, skipping the ones in "ns" *)
   5.223 -fun unfix_tfrees ns th = 
   5.224 -    let 
   5.225 -      val varfiytfrees = map (Term.dest_TFree o Thm.typ_of) ns
   5.226 -      val skiptfrees = subtract (op =) varfiytfrees (Term.add_term_tfrees (Thm.prop_of th,[]));
   5.227 -    in #2 (Thm.varifyT' skiptfrees th) end;
   5.228 -
   5.229 -(* change schematic/meta vars to fresh free vars, avoiding name clashes 
   5.230 -   with "names" *)
   5.231 -fun fix_vars_to_frees_in_terms names ts = 
   5.232 -    let 
   5.233 -      val vars = map Term.dest_Var (List.foldr Term.add_term_vars [] ts);
   5.234 -      val Ns = List.foldr Term.add_term_names names ts;
   5.235 -      val (_,renamings) = 
   5.236 -          Library.foldl (fn ((Ns,Rs),v as ((n,i),ty)) => 
   5.237 -                    let val n2 = Name.variant Ns n in
   5.238 -                      (n2 :: Ns, (v, (n2,ty)) :: Rs)
   5.239 -                    end) ((Ns,[]), vars);
   5.240 -    in renamings end;
   5.241 -fun fix_vars_to_frees th = 
   5.242 -    let 
   5.243 -      val ctermify = Thm.cterm_of (Thm.theory_of_thm th)
   5.244 -      val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
   5.245 -      val renamings = fix_vars_to_frees_in_terms 
   5.246 -                        [] ([Thm.prop_of th] @ tpairs);
   5.247 -      val crenamings = 
   5.248 -          map (fn (v,f) => (ctermify (Var v), ctermify (Free f)))
   5.249 -              renamings;
   5.250 -      val fixedfrees = map snd crenamings;
   5.251 -    in (fixedfrees, Thm.instantiate ([], crenamings) th) end;
   5.252 -
   5.253 -fun fix_tvars_upto_idx ix th = 
   5.254 -    let 
   5.255 -      val sgn = Thm.theory_of_thm th;
   5.256 -      val ctypify = Thm.ctyp_of sgn
   5.257 -      val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
   5.258 -      val prop = (Thm.prop_of th);
   5.259 -      val tvars = List.foldr Term.add_term_tvars [] (prop :: tpairs);
   5.260 -      val ctyfixes = 
   5.261 -          map_filter 
   5.262 -            (fn (v as ((s,i),ty)) => 
   5.263 -                if i <= ix then SOME (ctypify (TVar v), ctypify (TFree (s,ty)))
   5.264 -                else NONE) tvars;
   5.265 -    in Thm.instantiate (ctyfixes, []) th end;
   5.266 -fun fix_vars_upto_idx ix th = 
   5.267 -    let 
   5.268 -      val sgn = Thm.theory_of_thm th;
   5.269 -      val ctermify = Thm.cterm_of sgn
   5.270 -      val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
   5.271 -      val prop = (Thm.prop_of th);
   5.272 -      val vars = map Term.dest_Var (List.foldr Term.add_term_vars 
   5.273 -                                               [] (prop :: tpairs));
   5.274 -      val cfixes = 
   5.275 -          map_filter 
   5.276 -            (fn (v as ((s,i),ty)) => 
   5.277 -                if i <= ix then SOME (ctermify (Var v), ctermify (Free (s,ty)))
   5.278 -                else NONE) vars;
   5.279 -    in Thm.instantiate ([], cfixes) th end;
   5.280 -
   5.281 -
   5.282 -(* make free vars into schematic vars with index zero *)
   5.283 - fun unfix_frees frees = 
   5.284 -     apply (map (K (Drule.forall_elim_var 0)) frees) 
   5.285 -     o Drule.forall_intr_list frees;
   5.286 -
   5.287 -(* fix term and type variables *)
   5.288 -fun fix_vars_and_tvars th = 
   5.289 -    let val (tvars, th') = fix_tvars_to_tfrees th
   5.290 -      val (vars, th'') = fix_vars_to_frees th' 
   5.291 -    in ((vars, tvars), th'') end;
   5.292 -
   5.293 -(* implicit Thm.thm argument *)
   5.294 -(* assumes: vars may contain fixed versions of the frees *)
   5.295 -(* THINK: what if vs already has types varified? *)
   5.296 -fun unfix_frees_and_tfrees (vs,tvs) = 
   5.297 -    (unfix_tfrees tvs o unfix_frees vs);
   5.298 -
   5.299 -(* datatype to capture an exported result, ie a fix or assume. *)
   5.300 -datatype export = 
   5.301 -         export of {fixes : Thm.cterm list, (* fixed vars *)
   5.302 -                    assumes : Thm.cterm list, (* hidden hyps/assumed prems *)
   5.303 -                    sgid : int,
   5.304 -                    gth :  Thm.thm}; (* subgoal/goalthm *)
   5.305 -
   5.306 -fun fixes_of_exp (export rep) = #fixes rep;
   5.307 -
   5.308 -(* export the result of the new goal thm, ie if we reduced teh
   5.309 -subgoal, then we get a new reduced subtgoal with the old
   5.310 -all-quantified variables *)
   5.311 -local 
   5.312 -
   5.313 -(* allify puts in a meta level univ quantifier for a free variavble *)
   5.314 -fun allify_term (v, t) = 
   5.315 -    let val vt = #t (Thm.rep_cterm v)
   5.316 -      val (n,ty) = Term.dest_Free vt
   5.317 -    in (Term.all ty) $ (Abs(n,ty,Term.abstract_over (vt, t))) end;
   5.318 -
   5.319 -fun allify_for_sg_term ctermify vs t =
   5.320 -    let val t_alls = foldr allify_term t vs;
   5.321 -        val ct_alls = ctermify t_alls; 
   5.322 -    in 
   5.323 -      (ct_alls, Drule.forall_elim_list vs (Thm.assume ct_alls))
   5.324 -    end;
   5.325 -(* lookup type of a free var name from a list *)
   5.326 -fun lookupfree vs vn  = 
   5.327 -    case Library.find_first (fn (n,ty) => n = vn) vs of 
   5.328 -      NONE => error ("prepare_goal_export:lookupfree: " ^ vn ^ " does not occur in the term")
   5.329 -    | SOME x => x;
   5.330 -in
   5.331 -fun export_back (export {fixes = vs, assumes = hprems, 
   5.332 -                         sgid = i, gth = gth}) newth = 
   5.333 -    let 
   5.334 -      val sgn = Thm.theory_of_thm newth;
   5.335 -      val ctermify = Thm.cterm_of sgn;
   5.336 -
   5.337 -      val sgs = prems_of newth;
   5.338 -      val (sgallcts, sgthms) = 
   5.339 -          Library.split_list (map (allify_for_sg_term ctermify vs) sgs);
   5.340 -      val minimal_newth = 
   5.341 -          (Library.foldl (fn ( newth', sgthm) => 
   5.342 -                          Drule.compose_single (sgthm, 1, newth'))
   5.343 -                      (newth, sgthms));
   5.344 -      val allified_newth = 
   5.345 -          minimal_newth 
   5.346 -            |> Drule.implies_intr_list hprems
   5.347 -            |> Drule.forall_intr_list vs 
   5.348 -
   5.349 -      val newth' = Drule.implies_intr_list sgallcts allified_newth
   5.350 -    in
   5.351 -      bicompose false (false, newth', (length sgallcts)) i gth
   5.352 -    end;
   5.353 -
   5.354 -(* 
   5.355 -Given "vs" : names of free variables to abstract over,
   5.356 -Given cterms : premices to abstract over (P1... Pn) in terms of vs,
   5.357 -Given a thm of the form: 
   5.358 -P1 vs; ...; Pn vs ==> Goal(C vs)
   5.359 -
   5.360 -Gives back: 
   5.361 -(n, length of given cterms which have been allified
   5.362 - [| !! vs. P1 vs; !! vs. Pn vs |] ==> !! C vs) the allified thm
   5.363 -*)
   5.364 -(* note: C may contain further premices etc 
   5.365 -Note that cterms is the assumed facts, ie prems of "P1" that are
   5.366 -reintroduced in allified form.
   5.367 -*)
   5.368 -fun prepare_goal_export (vs, cterms) th = 
   5.369 -    let 
   5.370 -      val sgn = Thm.theory_of_thm th;
   5.371 -      val ctermify = Thm.cterm_of sgn;
   5.372 -
   5.373 -      val allfrees = map Term.dest_Free (Term.term_frees (Thm.prop_of th))
   5.374 -      val cfrees = map (ctermify o Free o lookupfree allfrees) vs
   5.375 -
   5.376 -      val sgs = prems_of th;
   5.377 -      val (sgallcts, sgthms) = 
   5.378 -          Library.split_list (map (allify_for_sg_term ctermify cfrees) sgs);
   5.379 -
   5.380 -      val minimal_th = 
   5.381 -          Goal.conclude (Library.foldl (fn ( th', sgthm) => 
   5.382 -                          Drule.compose_single (sgthm, 1, th'))
   5.383 -                      (th, sgthms));
   5.384 -
   5.385 -      val allified_th = 
   5.386 -          minimal_th 
   5.387 -            |> Drule.implies_intr_list cterms
   5.388 -            |> Drule.forall_intr_list cfrees 
   5.389 -
   5.390 -      val th' = Drule.implies_intr_list sgallcts allified_th
   5.391 -    in
   5.392 -      ((length sgallcts), th')
   5.393 -    end;
   5.394 -
   5.395 -end;
   5.396 -
   5.397 -
   5.398 -(* exporting function that takes a solution to the fixed/assumed goal,
   5.399 -and uses this to solve the subgoal in the main theorem *)
   5.400 -fun export_solution (export {fixes = cfvs, assumes = hcprems,
   5.401 -                             sgid = i, gth = gth}) solth = 
   5.402 -    let 
   5.403 -      val solth' = 
   5.404 -          solth |> Drule.implies_intr_list hcprems
   5.405 -                |> Drule.forall_intr_list cfvs
   5.406 -    in Drule.compose_single (solth', i, gth) end;
   5.407 -
   5.408 -fun export_solutions (xs,th) = foldr (uncurry export_solution) th xs;
   5.409 -
   5.410 -
   5.411 -(* fix parameters of a subgoal "i", as free variables, and create an
   5.412 -exporting function that will use the result of this proved goal to
   5.413 -show the goal in the original theorem. 
   5.414 -
   5.415 -Note, an advantage of this over Isar is that it supports instantiation
   5.416 -of unkowns in the earlier theorem, ie we can do instantiation of meta
   5.417 -vars! 
   5.418 -
   5.419 -avoids constant, free and vars names. 
   5.420 -
   5.421 -loosely corresponds to:
   5.422 -Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm
   5.423 -Result: 
   5.424 -  ("(As ==> SGi x') ==> (As ==> SGi x')" : thm, 
   5.425 -   expf : 
   5.426 -     ("As ==> SGi x'" : thm) -> 
   5.427 -     ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm)
   5.428 -*)
   5.429 -fun fix_alls_in_term alledt = 
   5.430 -    let
   5.431 -      val t = Term.strip_all_body alledt;
   5.432 -      val alls = rev (Term.strip_all_vars alledt);
   5.433 -      val varnames = map (fst o fst o Term.dest_Var) (Term.term_vars t)
   5.434 -      val names = Term.add_term_names (t,varnames);
   5.435 -      val fvs = map Free 
   5.436 -                    (Name.variant_list names (map fst alls)
   5.437 -                       ~~ (map snd alls));
   5.438 -    in ((subst_bounds (fvs,t)), fvs) end;
   5.439 -
   5.440 -fun fix_alls_term i t = 
   5.441 -    let 
   5.442 -      val varnames = map (fst o fst o Term.dest_Var) (Term.term_vars t)
   5.443 -      val names = Term.add_term_names (t,varnames);
   5.444 -      val gt = Logic.get_goal t i;
   5.445 -      val body = Term.strip_all_body gt;
   5.446 -      val alls = rev (Term.strip_all_vars gt);
   5.447 -      val fvs = map Free 
   5.448 -                    (Name.variant_list names (map fst alls)
   5.449 -                       ~~ (map snd alls));
   5.450 -    in ((subst_bounds (fvs,body)), fvs) end;
   5.451 -
   5.452 -fun fix_alls_cterm i th = 
   5.453 -    let
   5.454 -      val ctermify = Thm.cterm_of (Thm.theory_of_thm th);
   5.455 -      val (fixedbody, fvs) = fix_alls_term i (Thm.prop_of th);
   5.456 -      val cfvs = rev (map ctermify fvs);
   5.457 -      val ct_body = ctermify fixedbody
   5.458 -    in
   5.459 -      (ct_body, cfvs)
   5.460 -    end;
   5.461 -
   5.462 -fun fix_alls' i = 
   5.463 -     (apfst Thm.trivial) o (fix_alls_cterm i);
   5.464 -
   5.465 -
   5.466 -(* hide other goals *) 
   5.467 -(* note the export goal is rotated by (i - 1) and will have to be
   5.468 -unrotated to get backto the originial position(s) *)
   5.469 -fun hide_other_goals th = 
   5.470 -    let
   5.471 -      (* tl beacuse fst sg is the goal we are interested in *)
   5.472 -      val cprems = tl (Drule.cprems_of th)
   5.473 -      val aprems = map Thm.assume cprems
   5.474 -    in
   5.475 -      (Drule.implies_elim_list (Drule.rotate_prems 1 th) aprems, 
   5.476 -       cprems)
   5.477 -    end;
   5.478 -
   5.479 -(* a nicer version of the above that leaves only a single subgoal (the
   5.480 -other subgoals are hidden hyps, that the exporter suffles about)
   5.481 -namely the subgoal that we were trying to solve. *)
   5.482 -(* loosely corresponds to:
   5.483 -Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm
   5.484 -Result: 
   5.485 -  ("(As ==> SGi x') ==> SGi x'" : thm, 
   5.486 -   expf : 
   5.487 -     ("SGi x'" : thm) -> 
   5.488 -     ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm)
   5.489 -*)
   5.490 -fun fix_alls i th = 
   5.491 -    let 
   5.492 -      val (fixed_gth, fixedvars) = fix_alls' i th
   5.493 -      val (sml_gth, othergoals) = hide_other_goals fixed_gth
   5.494 -    in
   5.495 -      (sml_gth, export {fixes = fixedvars, 
   5.496 -                        assumes = othergoals, 
   5.497 -                        sgid = i, gth = th})
   5.498 -    end;
   5.499 -
   5.500 -
   5.501 -(* assume the premises of subgoal "i", this gives back a list of
   5.502 -assumed theorems that are the premices of subgoal i, it also gives
   5.503 -back a new goal thm and an exporter, the new goalthm is as the old
   5.504 -one, but without the premices, and the exporter will use a proof of
   5.505 -the new goalthm, possibly using the assumed premices, to shoe the
   5.506 -orginial goal.
   5.507 -
   5.508 -Note: Dealing with meta vars, need to meta-level-all them in the
   5.509 -shyps, which we can later instantiate with a specific value.... ? 
   5.510 -think about this... maybe need to introduce some new fixed vars and
   5.511 -then remove them again at the end... like I do with rw_inst. 
   5.512 -
   5.513 -loosely corresponds to:
   5.514 -Given "[| SG0; ... [| A0; ... An |] ==> SGi; ... SGm |] ==> G" : thm
   5.515 -Result: 
   5.516 -(["A0" [A0], ... ,"An" [An]] : thm list, -- assumptions
   5.517 - "SGi ==> SGi" : thm, -- new goal 
   5.518 - "SGi" ["A0" ... "An"] : thm ->   -- export function
   5.519 -    ("[| SG0 ... SGi-1, SGi+1, SGm |] ==> G" : thm) list)
   5.520 -*)
   5.521 -fun assume_prems i th =
   5.522 -    let 
   5.523 -      val t = (prop_of th); 
   5.524 -      val gt = Logic.get_goal t i;
   5.525 -      val _ = case Term.strip_all_vars gt of [] => () 
   5.526 -              | _ => error "assume_prems: goal has params"
   5.527 -      val body = gt;
   5.528 -      val prems = Logic.strip_imp_prems body;
   5.529 -      val concl = Logic.strip_imp_concl body;
   5.530 -
   5.531 -      val sgn = Thm.theory_of_thm th;
   5.532 -      val ctermify = Thm.cterm_of sgn;
   5.533 -      val cprems = map ctermify prems;
   5.534 -      val aprems = map Thm.assume cprems;
   5.535 -      val gthi = Thm.trivial (ctermify concl);
   5.536 -
   5.537 -      (* fun explortf thi = 
   5.538 -          Drule.compose (Drule.implies_intr_list cprems thi, 
   5.539 -                         i, th) *)
   5.540 -    in
   5.541 -      (aprems, gthi, cprems)
   5.542 -    end;
   5.543 -
   5.544 -
   5.545 -(* first fix the variables, then assume the assumptions *)
   5.546 -(* loosely corresponds to:
   5.547 -Given 
   5.548 -  "[| SG0; ... 
   5.549 -      !! xs. [| A0 xs; ... An xs |] ==> SGi xs; 
   5.550 -      ... SGm |] ==> G" : thm
   5.551 -Result: 
   5.552 -(["A0 xs'" [A0 xs'], ... ,"An xs'" [An xs']] : thm list, -- assumptions
   5.553 - "SGi xs' ==> SGi xs'" : thm,  -- new goal 
   5.554 - "SGi xs'" ["A0 xs'" ... "An xs'"] : thm ->   -- export function
   5.555 -    ("[| SG0 ... SGi-1, SGi+1, SGm |] ==> G" : thm) list)
   5.556 -*)
   5.557 -
   5.558 -(* Note: the fix_alls actually pulls through all the assumptions which
   5.559 -means that the second export is not needed. *)
   5.560 -fun fixes_and_assumes i th = 
   5.561 -    let 
   5.562 -      val (fixgth, exp1) = fix_alls i th
   5.563 -      val (assumps, goalth, _) = assume_prems 1 fixgth
   5.564 -    in 
   5.565 -      (assumps, goalth, exp1)
   5.566 -    end;
   5.567 -
   5.568 -
   5.569 -(* Fixme: allow different order of subgoals given to expf *)
   5.570 -(* make each subgoal into a separate thm that needs to be proved *)
   5.571 -(* loosely corresponds to:
   5.572 -Given 
   5.573 -  "[| SG0; ... SGm |] ==> G" : thm
   5.574 -Result: 
   5.575 -(["SG0 ==> SG0", ... ,"SGm ==> SGm"] : thm list, -- goals
   5.576 - ["SG0", ..., "SGm"] : thm list ->   -- export function
   5.577 -   "G" : thm)
   5.578 -*)
   5.579 -fun subgoal_thms th = 
   5.580 -    let 
   5.581 -      val t = (prop_of th); 
   5.582 -
   5.583 -      val prems = Logic.strip_imp_prems t;
   5.584 -
   5.585 -      val sgn = Thm.theory_of_thm th;
   5.586 -      val ctermify = Thm.cterm_of sgn;
   5.587 -
   5.588 -      val aprems = map (Thm.trivial o ctermify) prems;
   5.589 -
   5.590 -      fun explortf premths = 
   5.591 -          Drule.implies_elim_list th premths
   5.592 -    in
   5.593 -      (aprems, explortf)
   5.594 -    end;
   5.595 -
   5.596 -
   5.597 -(* make all the premices of a theorem hidden, and provide an unhide
   5.598 -function, that will bring them back out at a later point. This is
   5.599 -useful if you want to get back these premices, after having used the
   5.600 -theorem with the premices hidden *)
   5.601 -(* loosely corresponds to:
   5.602 -Given "As ==> G" : thm
   5.603 -Result: ("G [As]" : thm, 
   5.604 -         "G [As]" : thm -> "As ==> G" : thm
   5.605 -*)
   5.606 -fun hide_prems th = 
   5.607 -    let 
   5.608 -      val cprems = Drule.cprems_of th;
   5.609 -      val aprems = map Thm.assume cprems;
   5.610 -    (*   val unhidef = Drule.implies_intr_list cprems; *)
   5.611 -    in
   5.612 -      (Drule.implies_elim_list th aprems, cprems)
   5.613 -    end;
   5.614 -
   5.615 -
   5.616 -
   5.617 -
   5.618 -(* Fixme: allow different order of subgoals in exportf *)
   5.619 -(* as above, but also fix all parameters in all subgoals, and uses
   5.620 -fix_alls, not fix_alls', ie doesn't leave extra asumptions as apparent
   5.621 -subgoals. *)
   5.622 -(* loosely corresponds to:
   5.623 -Given 
   5.624 -  "[| !! x0s. A0s x0s ==> SG0 x0s; 
   5.625 -      ...; !! xms. Ams xms ==> SGm xms|] ==> G" : thm
   5.626 -Result: 
   5.627 -(["(A0s x0s' ==> SG0 x0s') ==> SG0 x0s'", 
   5.628 -  ... ,"(Ams xms' ==> SGm xms') ==> SGm xms'"] : thm list, -- goals
   5.629 - ["SG0 x0s'", ..., "SGm xms'"] : thm list ->   -- export function
   5.630 -   "G" : thm)
   5.631 -*)
   5.632 -(* requires being given solutions! *)
   5.633 -fun fixed_subgoal_thms th = 
   5.634 -    let 
   5.635 -      val (subgoals, expf) = subgoal_thms th;
   5.636 -(*       fun export_sg (th, exp) = exp th; *)
   5.637 -      fun export_sgs expfs solthms = 
   5.638 -          expf (map2 (curry (op |>)) solthms expfs);
   5.639 -(*           expf (map export_sg (ths ~~ expfs)); *)
   5.640 -    in 
   5.641 -      apsnd export_sgs (Library.split_list (map (apsnd export_solution o 
   5.642 -                                                 fix_alls 1) subgoals))
   5.643 -    end;
   5.644 -
   5.645 -end;
     6.1 --- a/src/Provers/IsaPlanner/rw_inst.ML	Thu May 31 19:11:19 2007 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,315 +0,0 @@
     6.4 -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
     6.5 -(*  Title:      Pure/IsaPlanner/rw_inst.ML
     6.6 -    ID:         $Id$
     6.7 -    Author:     Lucas Dixon, University of Edinburgh
     6.8 -                lucas.dixon@ed.ac.uk
     6.9 -    Created:    25 Aug 2004
    6.10 -*)
    6.11 -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
    6.12 -(*  DESCRIPTION:
    6.13 -
    6.14 -    rewriting using a conditional meta-equality theorem which supports 
    6.15 -    schematic variable instantiation.
    6.16 -
    6.17 -*)   
    6.18 -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
    6.19 -signature RW_INST =
    6.20 -sig
    6.21 -
    6.22 -  (* Rewrite: give it instantiation infromation, a rule, and the
    6.23 -  target thm, and it will return the rewritten target thm *)
    6.24 -  val rw :
    6.25 -      ((Term.indexname * (Term.sort * Term.typ)) list *  (* type var instantiations *)
    6.26 -       (Term.indexname * (Term.typ * Term.term)) list)  (* schematic var instantiations *)
    6.27 -      * (string * Term.typ) list           (* Fake named bounds + types *)
    6.28 -      * (string * Term.typ) list           (* names of bound + types *)
    6.29 -      * Term.term ->                       (* outer term for instantiation *)
    6.30 -      Thm.thm ->                           (* rule with indexies lifted *)
    6.31 -      Thm.thm ->                           (* target thm *)
    6.32 -      Thm.thm                              (* rewritten theorem possibly 
    6.33 -                                              with additional premises for 
    6.34 -                                              rule conditions *)
    6.35 -
    6.36 -  (* used tools *)
    6.37 -  val mk_abstractedrule :
    6.38 -      (string * Term.typ) list (* faked outer bound *)
    6.39 -      -> (string * Term.typ) list (* hopeful name of outer bounds *)
    6.40 -      -> Thm.thm -> Thm.cterm list * Thm.thm
    6.41 -  val mk_fixtvar_tyinsts :
    6.42 -      (Term.indexname * (Term.sort * Term.typ)) list ->
    6.43 -      Term.term list -> ((string * int) * (Term.sort * Term.typ)) list 
    6.44 -                        * (string * Term.sort) list
    6.45 -  val mk_renamings :
    6.46 -      Term.term -> Thm.thm -> (((string * int) * Term.typ) * Term.term) list
    6.47 -  val new_tfree :
    6.48 -      ((string * int) * Term.sort) *
    6.49 -      (((string * int) * (Term.sort * Term.typ)) list * string list) ->
    6.50 -      ((string * int) * (Term.sort * Term.typ)) list * string list
    6.51 -  val cross_inst : (Term.indexname * (Term.typ * Term.term)) list 
    6.52 -                   -> (Term.indexname *(Term.typ * Term.term)) list
    6.53 -  val cross_inst_typs : (Term.indexname * (Term.sort * Term.typ)) list 
    6.54 -                   -> (Term.indexname * (Term.sort * Term.typ)) list
    6.55 -
    6.56 -  val beta_contract : Thm.thm -> Thm.thm
    6.57 -  val beta_eta_contract : Thm.thm -> Thm.thm
    6.58 -
    6.59 -end;
    6.60 -
    6.61 -structure RWInst 
    6.62 -: RW_INST
    6.63 -= struct
    6.64 -
    6.65 -
    6.66 -(* beta contract the theorem *)
    6.67 -fun beta_contract thm = 
    6.68 -    equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm;
    6.69 -
    6.70 -(* beta-eta contract the theorem *)
    6.71 -fun beta_eta_contract thm = 
    6.72 -    let
    6.73 -      val thm2 = equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm
    6.74 -      val thm3 = equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2
    6.75 -    in thm3 end;
    6.76 -
    6.77 -
    6.78 -(* to get the free names of a theorem (including hyps and flexes) *)
    6.79 -fun usednames_of_thm th =
    6.80 -    let val rep = Thm.rep_thm th
    6.81 -      val hyps = #hyps rep
    6.82 -      val (tpairl,tpairr) = Library.split_list (#tpairs rep)
    6.83 -      val prop = #prop rep
    6.84 -    in
    6.85 -      List.foldr Term.add_term_names [] (prop :: (tpairl @ (tpairr @ hyps)))
    6.86 -    end;
    6.87 -
    6.88 -(* Given a list of variables that were bound, and a that has been
    6.89 -instantiated with free variable placeholders for the bound vars, it
    6.90 -creates an abstracted version of the theorem, with local bound vars as
    6.91 -lambda-params:
    6.92 -
    6.93 -Ts: 
    6.94 -("x", ty)
    6.95 -
    6.96 -rule::
    6.97 -C :x ==> P :x = Q :x
    6.98 -
    6.99 -results in:
   6.100 -("!! x. C x", (%x. p x = %y. p y) [!! x. C x])
   6.101 -
   6.102 -note: assumes rule is instantiated
   6.103 -*)
   6.104 -(* Note, we take abstraction in the order of last abstraction first *)
   6.105 -fun mk_abstractedrule TsFake Ts rule = 
   6.106 -    let 
   6.107 -      val ctermify = Thm.cterm_of (Thm.theory_of_thm rule);
   6.108 -
   6.109 -      (* now we change the names of temporary free vars that represent 
   6.110 -         bound vars with binders outside the redex *)
   6.111 -      val prop = Thm.prop_of rule;
   6.112 -      val names = usednames_of_thm rule;
   6.113 -      val (fromnames,tonames,names2,Ts') = 
   6.114 -          Library.foldl (fn ((rnf,rnt,names, Ts''),((faken,_),(n,ty))) => 
   6.115 -                    let val n2 = Name.variant names n in
   6.116 -                      (ctermify (Free(faken,ty)) :: rnf,
   6.117 -                       ctermify (Free(n2,ty)) :: rnt, 
   6.118 -                       n2 :: names,
   6.119 -                       (n2,ty) :: Ts'')
   6.120 -                    end)
   6.121 -                (([],[],names, []), TsFake~~Ts);
   6.122 -
   6.123 -      (* rename conflicting free's in the rule to avoid cconflicts
   6.124 -      with introduced vars from bounds outside in redex *)
   6.125 -      val rule' = rule |> Drule.forall_intr_list fromnames
   6.126 -                       |> Drule.forall_elim_list tonames;
   6.127 -      
   6.128 -      (* make unconditional rule and prems *)
   6.129 -      val (uncond_rule, cprems) = IsaND.allify_conditions ctermify (rev Ts') 
   6.130 -                                                          rule';
   6.131 -
   6.132 -      (* using these names create lambda-abstracted version of the rule *)
   6.133 -      val abstractions = rev (Ts' ~~ tonames);
   6.134 -      val abstract_rule = Library.foldl (fn (th,((n,ty),ct)) => 
   6.135 -                                    Thm.abstract_rule n ct th)
   6.136 -                                (uncond_rule, abstractions);
   6.137 -    in (cprems, abstract_rule) end;
   6.138 -
   6.139 -
   6.140 -(* given names to avoid, and vars that need to be fixed, it gives
   6.141 -unique new names to the vars so that they can be fixed as free
   6.142 -variables *)
   6.143 -(* make fixed unique free variable instantiations for non-ground vars *)
   6.144 -(* Create a table of vars to be renamed after instantiation - ie
   6.145 -      other uninstantiated vars in the hyps of the rule 
   6.146 -      ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *)
   6.147 -fun mk_renamings tgt rule_inst = 
   6.148 -    let
   6.149 -      val rule_conds = Thm.prems_of rule_inst
   6.150 -      val names = foldr Term.add_term_names [] (tgt :: rule_conds);
   6.151 -      val (conds_tyvs,cond_vs) = 
   6.152 -          Library.foldl (fn ((tyvs, vs), t) => 
   6.153 -                    (Library.union
   6.154 -                       (Term.term_tvars t, tyvs),
   6.155 -                     Library.union 
   6.156 -                       (map Term.dest_Var (Term.term_vars t), vs))) 
   6.157 -                (([],[]), rule_conds);
   6.158 -      val termvars = map Term.dest_Var (Term.term_vars tgt); 
   6.159 -      val vars_to_fix = Library.union (termvars, cond_vs);
   6.160 -      val (renamings, names2) = 
   6.161 -          foldr (fn (((n,i),ty), (vs, names')) => 
   6.162 -                    let val n' = Name.variant names' n in
   6.163 -                      ((((n,i),ty), Free (n', ty)) :: vs, n'::names')
   6.164 -                    end)
   6.165 -                ([], names) vars_to_fix;
   6.166 -    in renamings end;
   6.167 -
   6.168 -(* make a new fresh typefree instantiation for the given tvar *)
   6.169 -fun new_tfree (tv as (ix,sort), (pairs,used)) =
   6.170 -      let val v = Name.variant used (string_of_indexname ix)
   6.171 -      in  ((ix,(sort,TFree(v,sort)))::pairs, v::used)  end;
   6.172 -
   6.173 -
   6.174 -(* make instantiations to fix type variables that are not 
   6.175 -   already instantiated (in ignore_ixs) from the list of terms. *)
   6.176 -fun mk_fixtvar_tyinsts ignore_insts ts = 
   6.177 -    let 
   6.178 -      val ignore_ixs = map fst ignore_insts;
   6.179 -      val (tvars, tfrees) = 
   6.180 -            foldr (fn (t, (varixs, tfrees)) => 
   6.181 -                      (Term.add_term_tvars (t,varixs),
   6.182 -                       Term.add_term_tfrees (t,tfrees)))
   6.183 -                  ([],[]) ts;
   6.184 -        val unfixed_tvars = 
   6.185 -            List.filter (fn (ix,s) => not (member (op =) ignore_ixs ix)) tvars;
   6.186 -        val (fixtyinsts, _) = foldr new_tfree ([], map fst tfrees) unfixed_tvars
   6.187 -    in (fixtyinsts, tfrees) end;
   6.188 -
   6.189 -
   6.190 -(* cross-instantiate the instantiations - ie for each instantiation
   6.191 -replace all occurances in other instantiations - no loops are possible
   6.192 -and thus only one-parsing of the instantiations is necessary. *)
   6.193 -fun cross_inst insts = 
   6.194 -    let 
   6.195 -      fun instL (ix, (ty,t)) = 
   6.196 -          map (fn (ix2,(ty2,t2)) => 
   6.197 -                  (ix2, (ty2,Term.subst_vars ([], [(ix, t)]) t2)));
   6.198 -
   6.199 -      fun cross_instL ([], l) = rev l
   6.200 -        | cross_instL ((ix, t) :: insts, l) = 
   6.201 -          cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l));
   6.202 -
   6.203 -    in cross_instL (insts, []) end;
   6.204 -
   6.205 -(* as above but for types -- I don't know if this is needed, will we ever incur mixed up types? *)
   6.206 -fun cross_inst_typs insts = 
   6.207 -    let 
   6.208 -      fun instL (ix, (srt,ty)) = 
   6.209 -          map (fn (ix2,(srt2,ty2)) => 
   6.210 -                  (ix2, (srt2,Term.typ_subst_TVars [(ix, ty)] ty2)));
   6.211 -
   6.212 -      fun cross_instL ([], l) = rev l
   6.213 -        | cross_instL ((ix, t) :: insts, l) = 
   6.214 -          cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l));
   6.215 -
   6.216 -    in cross_instL (insts, []) end;
   6.217 -
   6.218 -
   6.219 -(* assume that rule and target_thm have distinct var names. THINK:
   6.220 -efficient version with tables for vars for: target vars, introduced
   6.221 -vars, and rule vars, for quicker instantiation?  The outerterm defines
   6.222 -which part of the target_thm was modified.  Note: we take Ts in the
   6.223 -upterm order, ie last abstraction first., and with an outeterm where
   6.224 -the abstracted subterm has the arguments in the revered order, ie
   6.225 -first abstraction first.  FakeTs has abstractions using the fake name
   6.226 -- ie the name distinct from all other abstractions. *)
   6.227 -
   6.228 -fun rw ((nonfixed_typinsts, unprepinsts), FakeTs, Ts, outerterm) rule target_thm = 
   6.229 -    let 
   6.230 -      (* general signature info *)
   6.231 -      val target_sign = (Thm.theory_of_thm target_thm);
   6.232 -      val ctermify = Thm.cterm_of target_sign;
   6.233 -      val ctypeify = Thm.ctyp_of target_sign;
   6.234 -
   6.235 -      (* fix all non-instantiated tvars *)
   6.236 -      val (fixtyinsts, othertfrees) = 
   6.237 -          mk_fixtvar_tyinsts nonfixed_typinsts
   6.238 -                             [Thm.prop_of rule, Thm.prop_of target_thm];
   6.239 -      val new_fixed_typs = map (fn ((s,i),(srt,ty)) => (Term.dest_TFree ty))
   6.240 -                               fixtyinsts;
   6.241 -      val typinsts = cross_inst_typs (nonfixed_typinsts @ fixtyinsts);
   6.242 -
   6.243 -      (* certified instantiations for types *)
   6.244 -      val ctyp_insts = 
   6.245 -          map (fn (ix,(s,ty)) => (ctypeify (TVar (ix,s)), ctypeify ty)) 
   6.246 -              typinsts;
   6.247 -
   6.248 -      (* type instantiated versions *)
   6.249 -      val tgt_th_tyinst = Thm.instantiate (ctyp_insts,[]) target_thm;
   6.250 -      val rule_tyinst =  Thm.instantiate (ctyp_insts,[]) rule;
   6.251 -
   6.252 -      val term_typ_inst = map (fn (ix,(srt,ty)) => (ix,ty)) typinsts;
   6.253 -      (* type instanitated outer term *)
   6.254 -      val outerterm_tyinst = Term.subst_TVars term_typ_inst outerterm;
   6.255 -
   6.256 -      val FakeTs_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) 
   6.257 -                              FakeTs;
   6.258 -      val Ts_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) 
   6.259 -                          Ts;
   6.260 -
   6.261 -      (* type-instantiate the var instantiations *)
   6.262 -      val insts_tyinst = foldr (fn ((ix,(ty,t)),insts_tyinst) => 
   6.263 -                            (ix, (Term.typ_subst_TVars term_typ_inst ty, 
   6.264 -                                  Term.subst_TVars term_typ_inst t))
   6.265 -                            :: insts_tyinst)
   6.266 -                        [] unprepinsts;
   6.267 -
   6.268 -      (* cross-instantiate *)
   6.269 -      val insts_tyinst_inst = cross_inst insts_tyinst;
   6.270 -
   6.271 -      (* create certms of instantiations *)
   6.272 -      val cinsts_tyinst = 
   6.273 -          map (fn (ix,(ty,t)) => (ctermify (Var (ix, ty)), 
   6.274 -                                  ctermify t)) insts_tyinst_inst;
   6.275 -
   6.276 -      (* The instantiated rule *)
   6.277 -      val rule_inst = rule_tyinst |> Thm.instantiate ([], cinsts_tyinst);
   6.278 -
   6.279 -      (* Create a table of vars to be renamed after instantiation - ie
   6.280 -      other uninstantiated vars in the hyps the *instantiated* rule 
   6.281 -      ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *)
   6.282 -      val renamings = mk_renamings (Thm.prop_of tgt_th_tyinst) 
   6.283 -                                   rule_inst;
   6.284 -      val cterm_renamings = 
   6.285 -          map (fn (x,y) => (ctermify (Var x), ctermify y)) renamings;
   6.286 -
   6.287 -      (* Create the specific version of the rule for this target application *)
   6.288 -      val outerterm_inst = 
   6.289 -          outerterm_tyinst 
   6.290 -            |> Term.subst_Vars (map (fn (ix,(ty,t)) => (ix,t)) insts_tyinst_inst)
   6.291 -            |> Term.subst_Vars (map (fn ((ix,ty),t) => (ix,t)) renamings);
   6.292 -      val couter_inst = Thm.reflexive (ctermify outerterm_inst);
   6.293 -      val (cprems, abstract_rule_inst) = 
   6.294 -          rule_inst |> Thm.instantiate ([], cterm_renamings)
   6.295 -                    |> mk_abstractedrule FakeTs_tyinst Ts_tyinst;
   6.296 -      val specific_tgt_rule = 
   6.297 -          beta_eta_contract
   6.298 -            (Thm.combination couter_inst abstract_rule_inst);
   6.299 -
   6.300 -      (* create an instantiated version of the target thm *)
   6.301 -      val tgt_th_inst = 
   6.302 -          tgt_th_tyinst |> Thm.instantiate ([], cinsts_tyinst)
   6.303 -                        |> Thm.instantiate ([], cterm_renamings);
   6.304 -
   6.305 -      val (vars,frees_of_fixed_vars) = Library.split_list cterm_renamings;
   6.306 -
   6.307 -    in
   6.308 -      (beta_eta_contract tgt_th_inst)
   6.309 -        |> Thm.equal_elim specific_tgt_rule
   6.310 -        |> Drule.implies_intr_list cprems
   6.311 -        |> Drule.forall_intr_list frees_of_fixed_vars
   6.312 -        |> Drule.forall_elim_list vars
   6.313 -        |> Thm.varifyT' othertfrees
   6.314 -        |-> K Drule.zero_var_indexes
   6.315 -    end;
   6.316 -
   6.317 -
   6.318 -end; (* struct *)
     7.1 --- a/src/Provers/IsaPlanner/rw_tools.ML	Thu May 31 19:11:19 2007 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,188 +0,0 @@
     7.4 -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
     7.5 -(*  Title:      Pure/IsaPlanner/rw_tools.ML
     7.6 -    ID:		$Id$
     7.7 -    Author:     Lucas Dixon, University of Edinburgh
     7.8 -                lucas.dixon@ed.ac.uk
     7.9 -    Created:    28 May 2004
    7.10 -*)
    7.11 -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
    7.12 -(*  DESCRIPTION:
    7.13 -
    7.14 -    term related tools used for rewriting
    7.15 -
    7.16 -*)   
    7.17 -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
    7.18 -
    7.19 -signature RWTOOLS =
    7.20 -sig
    7.21 -end;
    7.22 -
    7.23 -structure RWTools 
    7.24 -= struct
    7.25 -
    7.26 -(* fake free variable names for locally bound variables - these work
    7.27 -as placeholders. *)
    7.28 -
    7.29 -(* don't use dest_fake.. - we should instead be working with numbers
    7.30 -and a list... else we rely on naming conventions which can break, or
    7.31 -be violated - in contrast list locations are correct by
    7.32 -construction/definition. *)
    7.33 -(*
    7.34 -fun dest_fake_bound_name n = 
    7.35 -    case (explode n) of 
    7.36 -      (":" :: realchars) => implode realchars
    7.37 -    | _ => n; *)
    7.38 -fun is_fake_bound_name n = (hd (explode n) = ":");
    7.39 -fun mk_fake_bound_name n = ":b_" ^ n;
    7.40 -
    7.41 -
    7.42 -
    7.43 -(* fake free variable names for local meta variables - these work
    7.44 -as placeholders. *)
    7.45 -fun dest_fake_fix_name n = 
    7.46 -    case (explode n) of 
    7.47 -      ("@" :: realchars) => implode realchars
    7.48 -    | _ => n;
    7.49 -fun is_fake_fix_name n = (hd (explode n) = "@");
    7.50 -fun mk_fake_fix_name n = "@" ^ n;
    7.51 -
    7.52 -
    7.53 -
    7.54 -(* fake free variable names for meta level bound variables *)
    7.55 -fun dest_fake_all_name n = 
    7.56 -    case (explode n) of 
    7.57 -      ("+" :: realchars) => implode realchars
    7.58 -    | _ => n;
    7.59 -fun is_fake_all_name n = (hd (explode n) = "+");
    7.60 -fun mk_fake_all_name n = "+" ^ n;
    7.61 -
    7.62 -
    7.63 -
    7.64 -
    7.65 -(* Ys and Ts not used, Ns are real names of faked local bounds, the
    7.66 -idea is that this will be mapped to free variables thus if a free
    7.67 -variable is a faked local bound then we change it to being a meta
    7.68 -variable so that it can later be instantiated *)
    7.69 -(* FIXME: rename this - avoid the word fix! *)
    7.70 -(* note we are not really "fix"'ing the free, more like making it variable! *)
    7.71 -(* fun trymkvar_of_fakefree (Ns, Ts) Ys (n,ty) = 
    7.72 -    if n mem Ns then Var((n,0),ty) else Free (n,ty);
    7.73 -*)
    7.74 -
    7.75 -(* make a var into a fixed free (ie prefixed with "@") *)
    7.76 -fun mk_fakefixvar Ts ((n,i),ty) = Free(mk_fake_fix_name n, ty);
    7.77 -
    7.78 -
    7.79 -(* mk_frees_bound: string list -> Term.term -> Term.term *)
    7.80 -(* This function changes free variables to being represented as bound
    7.81 -variables if the free's variable name is in the given list. The debruijn 
    7.82 -index is simply the position in the list *)
    7.83 -(* THINKABOUT: danger of an existing free variable with the same name: fix
    7.84 -this so that name conflict are avoided automatically! In the meantime,
    7.85 -don't have free variables named starting with a ":" *)
    7.86 -fun bounds_of_fakefrees Ys (a $ b) = 
    7.87 -    (bounds_of_fakefrees Ys a) $ (bounds_of_fakefrees Ys b)
    7.88 -  | bounds_of_fakefrees Ys (Abs(n,ty,t)) = 
    7.89 -    Abs(n,ty, bounds_of_fakefrees (n::Ys) t)
    7.90 -  | bounds_of_fakefrees Ys (Free (n,ty)) = 
    7.91 -    let fun try_mk_bound_of_free (i,[]) = Free (n,ty)
    7.92 -          | try_mk_bound_of_free (i,(y::ys)) = 
    7.93 -            if n = y then Bound i else try_mk_bound_of_free (i+1,ys)
    7.94 -    in try_mk_bound_of_free (0,Ys) end
    7.95 -  | bounds_of_fakefrees Ys t = t;
    7.96 -
    7.97 -
    7.98 -(* map a function f onto each free variables *)
    7.99 -fun map_to_frees f Ys (a $ b) = 
   7.100 -    (map_to_frees f Ys a) $ (map_to_frees f Ys b)
   7.101 -  | map_to_frees f Ys (Abs(n,ty,t)) = 
   7.102 -    Abs(n,ty, map_to_frees f ((n,ty)::Ys) t)
   7.103 -  | map_to_frees f Ys (Free a) = 
   7.104 -    f Ys a
   7.105 -  | map_to_frees f Ys t = t;
   7.106 -
   7.107 -
   7.108 -(* map a function f onto each meta variable  *)
   7.109 -fun map_to_vars f Ys (a $ b) = 
   7.110 -    (map_to_vars f Ys a) $ (map_to_vars f Ys b)
   7.111 -  | map_to_vars f Ys (Abs(n,ty,t)) = 
   7.112 -    Abs(n,ty, map_to_vars f ((n,ty)::Ys) t)
   7.113 -  | map_to_vars f Ys (Var a) = 
   7.114 -    f Ys a
   7.115 -  | map_to_vars f Ys t = t;
   7.116 -
   7.117 -(* map a function f onto each free variables *)
   7.118 -fun map_to_alls f (Const("all",allty) $ Abs(n,ty,t)) = 
   7.119 -    let val (n2,ty2) = f (n,ty) 
   7.120 -    in (Const("all",allty) $ Abs(n2,ty2,map_to_alls f t)) end
   7.121 -  | map_to_alls f x = x;
   7.122 -
   7.123 -(* map a function f to each type variable in a term *)
   7.124 -(* implicit arg: term *)
   7.125 -fun map_to_term_tvars f =
   7.126 -    Term.map_types (fn TVar(ix,ty) => f (ix,ty) | x => x);   (* FIXME map_atyps !? *)
   7.127 -
   7.128 -
   7.129 -
   7.130 -(* what if a param desn't occur in the concl? think about! Note: This
   7.131 -simply fixes meta level univ bound vars as Frees.  At the end, we will
   7.132 -change them back to schematic vars that will then unify
   7.133 -appropriactely, ie with unfake_vars *)
   7.134 -fun fake_concl_of_goal gt i = 
   7.135 -    let 
   7.136 -      val prems = Logic.strip_imp_prems gt
   7.137 -      val sgt = List.nth (prems, i - 1)
   7.138 -
   7.139 -      val tbody = Logic.strip_imp_concl (Term.strip_all_body sgt)
   7.140 -      val tparams = Term.strip_all_vars sgt
   7.141 -
   7.142 -      val fakefrees = map (fn (n, ty) => Free(mk_fake_all_name n, ty)) 
   7.143 -                          tparams
   7.144 -    in
   7.145 -      Term.subst_bounds (rev fakefrees,tbody)
   7.146 -    end;
   7.147 -
   7.148 -(* what if a param desn't occur in the concl? think about! Note: This
   7.149 -simply fixes meta level univ bound vars as Frees.  At the end, we will
   7.150 -change them back to schematic vars that will then unify
   7.151 -appropriactely, ie with unfake_vars *)
   7.152 -fun fake_goal gt i = 
   7.153 -    let 
   7.154 -      val prems = Logic.strip_imp_prems gt
   7.155 -      val sgt = List.nth (prems, i - 1)
   7.156 -
   7.157 -      val tbody = Term.strip_all_body sgt
   7.158 -      val tparams = Term.strip_all_vars sgt
   7.159 -
   7.160 -      val fakefrees = map (fn (n, ty) => Free(mk_fake_all_name n, ty)) 
   7.161 -                          tparams
   7.162 -    in
   7.163 -      Term.subst_bounds (rev fakefrees,tbody)
   7.164 -    end;
   7.165 -
   7.166 -
   7.167 -(* hand written - for some reason the Isabelle version in drule is broken!
   7.168 -Example? something to do with Bin Yangs examples? 
   7.169 - *)
   7.170 -fun rename_term_bvars ns (Abs(s,ty,t)) = 
   7.171 -    let val s2opt = Library.find_first (fn (x,y) => s = x) ns
   7.172 -    in case s2opt of 
   7.173 -         NONE => (Abs(s,ty,rename_term_bvars  ns t))
   7.174 -       | SOME (_,s2) => Abs(s2,ty, rename_term_bvars ns t) end
   7.175 -  | rename_term_bvars ns (a$b) = 
   7.176 -    (rename_term_bvars ns a) $ (rename_term_bvars ns b)
   7.177 -  | rename_term_bvars _ x = x;
   7.178 -
   7.179 -fun rename_thm_bvars ns th = 
   7.180 -    let val t = Thm.prop_of th 
   7.181 -    in Thm.rename_boundvars t (rename_term_bvars ns t) th end;
   7.182 -
   7.183 -(* Finish this to show how it breaks! (raises the exception): 
   7.184 -
   7.185 -exception rename_thm_bvars_exp of ((string * string) list * Thm.thm)
   7.186 -
   7.187 -    Drule.rename_bvars ns th 
   7.188 -    handle TERM _ => raise rename_thm_bvars_exp (ns, th); 
   7.189 -*)
   7.190 -
   7.191 -end;
     8.1 --- a/src/Provers/IsaPlanner/zipper.ML	Thu May 31 19:11:19 2007 +0200
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,491 +0,0 @@
     8.4 -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
     8.5 -(*  Title:      Pure/IsaPlanner/zipper.ML
     8.6 -    ID:		$Id$
     8.7 -    Author:     Lucas Dixon, University of Edinburgh
     8.8 -                lucas.dixon@ed.ac.uk
     8.9 -    Created:    24 Mar 2006
    8.10 -*)
    8.11 -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
    8.12 -(*  DESCRIPTION:
    8.13 -    A notion roughly based on Huet's Zippers for Isabelle terms.
    8.14 -*)   
    8.15 -
    8.16 -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
    8.17 -
    8.18 -(* abstract term for no more than pattern matching *)
    8.19 -signature ABSTRACT_TRM = 
    8.20 -sig
    8.21 -type typ   (* types *)
    8.22 -type aname (* abstraction names *)
    8.23 -type fname (* parameter/free variable names *)
    8.24 -type cname (* constant names *)
    8.25 -type vname (* meta variable names *)
    8.26 -type bname (* bound var name *)
    8.27 -datatype term = Const of cname * typ
    8.28 -           | Abs of aname * typ * term
    8.29 -           | Free of fname * typ
    8.30 -           | Var of vname * typ
    8.31 -           | Bound of bname
    8.32 -           | $ of term * term;
    8.33 -type T = term;
    8.34 -end;
    8.35 -
    8.36 -structure IsabelleTrmWrap : ABSTRACT_TRM= 
    8.37 -struct 
    8.38 -open Term;
    8.39 -type typ   = Term.typ; (* types *)
    8.40 -type aname = string; (* abstraction names *)
    8.41 -type fname = string; (* parameter/free variable names *)
    8.42 -type cname = string; (* constant names *)
    8.43 -type vname = string * int; (* meta variable names *)
    8.44 -type bname = int; (* bound var name *)
    8.45 -type T = term;
    8.46 -end;
    8.47 -
    8.48 -(* Concrete version for the Trm structure *)
    8.49 -signature TRM_CTXT_DATA = 
    8.50 -sig
    8.51 -
    8.52 -  structure Trm : ABSTRACT_TRM
    8.53 -  datatype dtrm = Abs of Trm.aname * Trm.typ
    8.54 -                | AppL of Trm.T
    8.55 -                | AppR of Trm.T;
    8.56 -  val apply : dtrm -> Trm.T -> Trm.T
    8.57 -  val eq_pos : dtrm * dtrm -> bool
    8.58 -end;
    8.59 -
    8.60 -(* A trm context = list of derivatives *)
    8.61 -signature TRM_CTXT =
    8.62 -sig
    8.63 -  structure D : TRM_CTXT_DATA
    8.64 -  type T = D.dtrm list;
    8.65 -
    8.66 -  val empty : T;
    8.67 -  val is_empty : T -> bool;
    8.68 -
    8.69 -  val add_abs : D.Trm.aname * D.Trm.typ -> T -> T;
    8.70 -  val add_appl : D.Trm.T -> T -> T;
    8.71 -  val add_appr : D.Trm.T -> T -> T;
    8.72 -
    8.73 -  val add_dtrm : D.dtrm -> T -> T;
    8.74 -
    8.75 -  val eq_path : T * T -> bool
    8.76 -
    8.77 -  val add_outerctxt : T -> T -> T
    8.78 -
    8.79 -  val apply : T -> D.Trm.T -> D.Trm.T
    8.80 -
    8.81 -  val nty_ctxt : T -> (D.Trm.aname * D.Trm.typ) list;
    8.82 -  val ty_ctxt : T -> D.Trm.typ list;
    8.83 -
    8.84 -  val depth : T -> int;
    8.85 -  val map : (D.dtrm -> D.dtrm) -> T -> T
    8.86 -  val fold_up : (D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a
    8.87 -  val fold_down : (D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a
    8.88 -
    8.89 -end;
    8.90 -
    8.91 -(* A zipper = a term looked at, at a particular point in the term *)
    8.92 -signature ZIPPER =
    8.93 -sig
    8.94 -  structure C : TRM_CTXT
    8.95 -  type T
    8.96 -
    8.97 -  val mktop : C.D.Trm.T -> T
    8.98 -  val mk : (C.D.Trm.T * C.T) -> T
    8.99 -
   8.100 -  val goto_top : T -> T 
   8.101 -  val at_top : T -> bool
   8.102 -
   8.103 -  val split : T -> T * C.T
   8.104 -  val add_outerctxt : C.T -> T -> T
   8.105 -
   8.106 -  val set_trm : C.D.Trm.T -> T -> T
   8.107 -  val set_ctxt : C.T -> T -> T
   8.108 -
   8.109 -  val ctxt : T -> C.T
   8.110 -  val trm : T -> C.D.Trm.T
   8.111 -  val top_trm : T -> C.D.Trm.T
   8.112 -
   8.113 -  val zipto : C.T -> T -> T (* follow context down *)
   8.114 -
   8.115 -  val nty_ctxt : T -> (C.D.Trm.aname * C.D.Trm.typ) list;
   8.116 -  val ty_ctxt : T -> C.D.Trm.typ list;
   8.117 -
   8.118 -  val depth_of_ctxt : T -> int;
   8.119 -  val map_on_ctxt : (C.D.dtrm -> C.D.dtrm) -> T -> T
   8.120 -  val fold_up_ctxt : (C.D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a
   8.121 -  val fold_down_ctxt : (C.D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a
   8.122 -
   8.123 -  (* searching through a zipper *)
   8.124 -  datatype zsearch = Here of T | LookIn of T;
   8.125 -  (* lazily search through the zipper *)
   8.126 -  val lzy_search : (T -> zsearch list) -> T -> T Seq.seq
   8.127 -  (* lazy search with folded data *)
   8.128 -  val pf_lzy_search : ('a -> T -> ('a * zsearch list)) 
   8.129 -                      -> 'a -> T -> T Seq.seq
   8.130 -  (* zsearch list is or-choices *)
   8.131 -  val searchfold : ('a -> T -> (('a * zsearch) list)) 
   8.132 -                      -> 'a -> T -> ('a * T) Seq.seq
   8.133 -  (* limit function to the current focus of the zipper, 
   8.134 -     but give function the zipper's context *)
   8.135 -  val limit_pcapply : (C.T -> T -> ('a * T) Seq.seq) 
   8.136 -                      -> T -> ('a * T) Seq.seq
   8.137 -  val limit_apply : (T -> T Seq.seq) -> T -> T Seq.seq
   8.138 -  val limit_capply : (C.T -> T -> T Seq.seq) -> T -> T Seq.seq
   8.139 -
   8.140 -  (* moving around zippers with option types *)
   8.141 -  val omove_up : T -> T option
   8.142 -  val omove_up_abs : T -> T option
   8.143 -  val omove_up_app : T -> T option
   8.144 -  val omove_up_left : T -> T option
   8.145 -  val omove_up_right : T -> T option
   8.146 -  val omove_up_left_or_abs : T -> T option
   8.147 -  val omove_up_right_or_abs : T -> T option
   8.148 -  val omove_down_abs : T -> T option
   8.149 -  val omove_down_left : T -> T option
   8.150 -  val omove_down_right : T -> T option
   8.151 -  val omove_down_app : T -> (T * T) option
   8.152 -
   8.153 -  (* moving around zippers, raising exceptions *)
   8.154 -  exception move of string * T
   8.155 -  val move_up : T -> T
   8.156 -  val move_up_abs : T -> T
   8.157 -  val move_up_app : T -> T
   8.158 -  val move_up_left : T -> T
   8.159 -  val move_up_right : T -> T
   8.160 -  val move_up_left_or_abs : T -> T
   8.161 -  val move_up_right_or_abs : T -> T
   8.162 -  val move_down_abs : T -> T
   8.163 -  val move_down_left : T -> T
   8.164 -  val move_down_right : T -> T
   8.165 -  val move_down_app : T -> T * T
   8.166 -
   8.167 -end;
   8.168 -
   8.169 -
   8.170 -(* Zipper data for an generic trm *)
   8.171 -functor TrmCtxtDataFUN(Trm : ABSTRACT_TRM) 
   8.172 -: TRM_CTXT_DATA 
   8.173 -= struct
   8.174 -  
   8.175 -  structure Trm = Trm;
   8.176 -
   8.177 -  (* a dtrm is, in McBridge-speak, a differentiated term. It represents
   8.178 -  the different ways a term can occur within its datatype constructors *)
   8.179 -  datatype dtrm = Abs of Trm.aname * Trm.typ
   8.180 -                | AppL of Trm.T
   8.181 -                | AppR of Trm.T;
   8.182 -
   8.183 -  (* apply a dtrm to a term, ie put the dtrm above it, building context *)
   8.184 -  fun apply (Abs (s,ty)) t = Trm.Abs (s,ty,t)
   8.185 -    | apply (AppL tl) tr = Trm.$ (tl, tr)
   8.186 -    | apply (AppR tr) tl = Trm.$ (tl, tr);
   8.187 -
   8.188 -  fun eq_pos (Abs _, Abs _) = true
   8.189 -    | eq_pos (AppL _, AppL _) = true
   8.190 -    | eq_pos (AppR _, AppR _) = true
   8.191 -    | eq_pos _ = false;
   8.192 -
   8.193 -end;
   8.194 -
   8.195 -
   8.196 -(* functor for making term contexts given term data *)
   8.197 -functor TrmCtxtFUN(D : TRM_CTXT_DATA) 
   8.198 - : TRM_CTXT =
   8.199 -struct 
   8.200 -  structure D = D;
   8.201 -
   8.202 -  type T = D.dtrm list;
   8.203 -
   8.204 -  val empty = [];
   8.205 -  val is_empty = List.null;
   8.206 -
   8.207 -  fun add_abs d l = (D.Abs d) :: l;
   8.208 -  fun add_appl d l = (D.AppL d) :: l;
   8.209 -  fun add_appr d l = (D.AppR d) :: l;
   8.210 -
   8.211 -  fun add_dtrm d l = d::l;
   8.212 -
   8.213 -  fun eq_path ([], []) = true
   8.214 -    | eq_path ([], _::_) = false
   8.215 -    | eq_path ( _::_, []) = false
   8.216 -    | eq_path (h::t, h2::t2) = 
   8.217 -      D.eq_pos(h,h2) andalso eq_path (t, t2);
   8.218 -
   8.219 -  (* add context to outside of existing context *) 
   8.220 -  fun add_outerctxt ctop cbottom = cbottom @ ctop; 
   8.221 -
   8.222 -  (* mkterm : zipper -> trm -> trm *)
   8.223 -  val apply = Basics.fold D.apply;
   8.224 -  
   8.225 -  (* named type context *)
   8.226 -  val nty_ctxt = List.foldr (fn (D.Abs nty,ntys) => nty::ntys
   8.227 -                             | (_,ntys) => ntys) [];
   8.228 -  (* type context *)
   8.229 -  val ty_ctxt = List.foldr (fn (D.Abs (_,ty),tys) => ty::tys
   8.230 -                           | (_,tys) => tys) [];
   8.231 -
   8.232 -  val depth = length : T -> int;
   8.233 -
   8.234 -  val map = List.map : (D.dtrm -> D.dtrm) -> T -> T
   8.235 -
   8.236 -  val fold_up = Basics.fold : (D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a;
   8.237 -  val fold_down = Basics.fold_rev : (D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a;
   8.238 -
   8.239 -end;
   8.240 -
   8.241 -(* zippers in terms of term contexts *)
   8.242 -functor ZipperFUN(C : TRM_CTXT) 
   8.243 - : ZIPPER
   8.244 -= struct 
   8.245 -
   8.246 -  structure C = C;
   8.247 -  structure D = C.D;
   8.248 -  structure Trm = D.Trm;
   8.249 -
   8.250 -  type T = C.D.Trm.T * C.T;
   8.251 -
   8.252 -  fun mktop t = (t, C.empty) : T
   8.253 -
   8.254 -  val mk = I;
   8.255 -  fun set_trm x = apfst (K x);
   8.256 -  fun set_ctxt x = apsnd (K x);
   8.257 -
   8.258 -  fun goto_top (z as (t,c)) = 
   8.259 -      if C.is_empty c then z else (C.apply c t, C.empty);
   8.260 -
   8.261 -  fun at_top (_,c) = C.is_empty c;
   8.262 -
   8.263 -  fun split (t,c) = ((t,C.empty) : T, c : C.T) 
   8.264 -  fun add_outerctxt c (t,c2) = (t, C.add_outerctxt c c2) : T
   8.265 -
   8.266 -  val ctxt = snd;
   8.267 -  val trm = fst;
   8.268 -  val top_trm = trm o goto_top;
   8.269 -
   8.270 -  fun nty_ctxt x = C.nty_ctxt (ctxt x);
   8.271 -  fun ty_ctxt x = C.ty_ctxt (ctxt x);
   8.272 -
   8.273 -  fun depth_of_ctxt x = C.depth (ctxt x);
   8.274 -  fun map_on_ctxt x = apsnd (C.map x);
   8.275 -  fun fold_up_ctxt f = C.fold_up f o ctxt;
   8.276 -  fun fold_down_ctxt f = C.fold_down f o ctxt;
   8.277 -
   8.278 -  fun omove_up (t,(d::c)) = SOME (D.apply d t, c)
   8.279 -    | omove_up (z as (_,[])) = NONE;
   8.280 -  fun omove_up_abs (t,((D.Abs(n,ty))::c)) = SOME (Trm.Abs(n,ty,t), c)
   8.281 -    | omove_up_abs z = NONE;
   8.282 -  fun omove_up_app (t,(D.AppL tl)::c) = SOME(Trm.$(tl,t), c)
   8.283 -    | omove_up_app (t,(D.AppR tr)::c) = SOME(Trm.$(t,tr), c)
   8.284 -    | omove_up_app z = NONE;
   8.285 -  fun omove_up_left (t,(D.AppL tl)::c) = SOME(Trm.$(tl,t), c)
   8.286 -    | omove_up_left z = NONE;
   8.287 -  fun omove_up_right (t,(D.AppR tr)::c) = SOME(Trm.$(t,tr), c)
   8.288 -    | omove_up_right _ = NONE;
   8.289 -  fun omove_up_left_or_abs (t,(D.AppL tl)::c) = 
   8.290 -      SOME (Trm.$(tl,t), c)
   8.291 -    | omove_up_left_or_abs (t,(D.Abs (n,ty))::c) = 
   8.292 -      SOME (Trm.Abs(n,ty,t), c)
   8.293 -    | omove_up_left_or_abs z = NONE;
   8.294 -  fun omove_up_right_or_abs (t,(D.Abs (n,ty))::c) = 
   8.295 -      SOME (Trm.Abs(n,ty,t), c) 
   8.296 -    | omove_up_right_or_abs (t,(D.AppR tr)::c) = 
   8.297 -      SOME (Trm.$(t,tr), c)
   8.298 -    | omove_up_right_or_abs _ = NONE;
   8.299 -  fun omove_down_abs (Trm.Abs(s,ty,t),c) = SOME (t,(D.Abs(s,ty))::c)
   8.300 -    | omove_down_abs _ = NONE;
   8.301 -  fun omove_down_left (Trm.$(l,r),c) = SOME (l,(D.AppR r)::c)
   8.302 -    | omove_down_left _ = NONE;
   8.303 -  fun omove_down_right (Trm.$(l,r),c) = SOME (r,(D.AppL l)::c)
   8.304 -    | omove_down_right _ = NONE;
   8.305 -  fun omove_down_app (Trm.$(l,r),c) = 
   8.306 -      SOME ((l,(D.AppR r)::c),(r,(D.AppL l)::c))
   8.307 -    | omove_down_app _ = NONE;
   8.308 -
   8.309 -  exception move of string * T
   8.310 -  fun move_up (t,(d::c)) = (D.apply d t, c)
   8.311 -    | move_up (z as (_,[])) = raise move ("move_up",z);
   8.312 -  fun move_up_abs (t,((D.Abs(n,ty))::c)) = (Trm.Abs(n,ty,t), c)
   8.313 -    | move_up_abs z = raise move ("move_up_abs",z);
   8.314 -  fun move_up_app (t,(D.AppL tl)::c) = (Trm.$(tl,t), c)
   8.315 -    | move_up_app (t,(D.AppR tr)::c) = (Trm.$(t,tr), c)
   8.316 -    | move_up_app z = raise move ("move_up_app",z);
   8.317 -  fun move_up_left (t,((D.AppL tl)::c)) = (Trm.$(tl,t), c)
   8.318 -    | move_up_left z = raise move ("move_up_left",z);
   8.319 -  fun move_up_right (t,(D.AppR tr)::c) = (Trm.$(t,tr), c)
   8.320 -    | move_up_right z = raise move ("move_up_right",z);
   8.321 -  fun move_up_left_or_abs (t,(D.AppL tl)::c) = (Trm.$(tl,t), c)
   8.322 -    | move_up_left_or_abs (t,(D.Abs (n,ty))::c) = (Trm.Abs(n,ty,t), c)
   8.323 -    | move_up_left_or_abs z = raise move ("move_up_left_or_abs",z);
   8.324 -  fun move_up_right_or_abs (t,(D.Abs (n,ty))::c) = (Trm.Abs(n,ty,t), c) 
   8.325 -    | move_up_right_or_abs (t,(D.AppR tr)::c) = (Trm.$(t,tr), c)
   8.326 -    | move_up_right_or_abs z = raise move ("move_up_right_or_abs",z);
   8.327 -  fun move_down_abs (Trm.Abs(s,ty,t),c) = (t,(D.Abs(s,ty))::c)
   8.328 -    | move_down_abs z = raise move ("move_down_abs",z);
   8.329 -  fun move_down_left (Trm.$(l,r),c) = (l,(D.AppR r)::c)
   8.330 -    | move_down_left z = raise move ("move_down_left",z);
   8.331 -  fun move_down_right (Trm.$(l,r),c) = (r,(D.AppL l)::c)
   8.332 -    | move_down_right z = raise move ("move_down_right",z);
   8.333 -  fun move_down_app (Trm.$(l,r),c) = 
   8.334 -      ((l,(D.AppR r)::c),(r,(D.AppL l)::c))
   8.335 -    | move_down_app z = raise move ("move_down_app",z);
   8.336 -
   8.337 -  (* follow the given path down the given zipper *)
   8.338 -  (* implicit arguments: C.D.dtrm list, then T *)
   8.339 -  val zipto = C.fold_down 
   8.340 -                (fn C.D.Abs _ => move_down_abs 
   8.341 -                  | C.D.AppL _ => move_down_right
   8.342 -                  | C.D.AppR _ => move_down_left); 
   8.343 -
   8.344 -  (* Note: interpretted as being examined depth first *)
   8.345 -  datatype zsearch = Here of T | LookIn of T;
   8.346 -
   8.347 -  (* lazy search *)
   8.348 -  fun lzy_search fsearch = 
   8.349 -      let 
   8.350 -        fun lzyl [] () = NONE
   8.351 -          | lzyl ((Here z) :: more) () = SOME(z, Seq.make (lzyl more))
   8.352 -          | lzyl ((LookIn z) :: more) () =
   8.353 -            (case lzy z
   8.354 -              of NONE => NONE
   8.355 -               | SOME (hz,mz) => 
   8.356 -                 SOME (hz, Seq.append mz (Seq.make (lzyl more))))
   8.357 -        and lzy z = lzyl (fsearch z) ()
   8.358 -      in Seq.make o lzyl o fsearch end;
   8.359 -
   8.360 -  (* path folded lazy search - the search list is defined in terms of
   8.361 -  the path passed through: the data a is updated with every zipper
   8.362 -  considered *)
   8.363 -  fun pf_lzy_search fsearch a0 z = 
   8.364 -      let 
   8.365 -        fun lzyl a [] () = NONE
   8.366 -          | lzyl a ((Here z) :: more) () = SOME(z, Seq.make (lzyl a more))
   8.367 -          | lzyl a ((LookIn z) :: more) () =
   8.368 -            (case lzy a z
   8.369 -              of NONE => lzyl a more ()
   8.370 -               | SOME(hz,mz) => SOME(hz,Seq.append mz (Seq.make(lzyl a more))))
   8.371 -        and lzy a z = 
   8.372 -            let val (a2, slist) = (fsearch a z) in lzyl a2 slist () end
   8.373 -
   8.374 -        val (a,slist) = fsearch a0 z
   8.375 -      in Seq.make (lzyl a slist) end;
   8.376 -
   8.377 -  (* Note: depth first over zsearch results *)
   8.378 -  fun searchfold fsearch a0 z = 
   8.379 -      let 
   8.380 -        fun lzyl [] () = NONE
   8.381 -          | lzyl ((a, Here z) :: more) () = 
   8.382 -            SOME((a,z), Seq.make (lzyl more))
   8.383 -          | lzyl ((a, LookIn z) :: more) () =
   8.384 -            (case lzyl (fsearch a z) () of 
   8.385 -               NONE => lzyl more ()
   8.386 -             | SOME (z,mz) => SOME (z,Seq.append mz (Seq.make (lzyl more))))
   8.387 -      in Seq.make (lzyl (fsearch a0 z)) end;
   8.388 -
   8.389 -
   8.390 -  fun limit_pcapply f z = 
   8.391 -      let val (z2,c) = split z
   8.392 -      in Seq.map (apsnd (add_outerctxt c)) (f c z2) end;
   8.393 -  fun limit_capply (f : C.T -> T -> T Seq.seq) (z : T) = 
   8.394 -      let val ((z2 : T),(c : C.T)) = split z
   8.395 -      in Seq.map (add_outerctxt c) (f c z2) end
   8.396 -
   8.397 -  val limit_apply = limit_capply o K;
   8.398 -
   8.399 -end;
   8.400 -
   8.401 -(* now build these for Isabelle terms *)
   8.402 -structure TrmCtxtData = TrmCtxtDataFUN(IsabelleTrmWrap);
   8.403 -structure TrmCtxt = TrmCtxtFUN(TrmCtxtData);
   8.404 -structure Zipper = ZipperFUN(TrmCtxt);
   8.405 -
   8.406 -
   8.407 -
   8.408 -(* For searching through Zippers below the current focus...
   8.409 -   KEY for naming scheme:    
   8.410 -
   8.411 -   td = starting at the top down
   8.412 -   lr = going from left to right
   8.413 -   rl = going from right to left
   8.414 -
   8.415 -   bl = starting at the bottom left
   8.416 -   br = starting at the bottom right
   8.417 -   ul = going up then left
   8.418 -   ur = going up then right
   8.419 -   ru = going right then up
   8.420 -   lu = going left then up
   8.421 -*)
   8.422 -signature ZIPPER_SEARCH =
   8.423 -sig
   8.424 -  structure Z : ZIPPER;
   8.425 -  
   8.426 -  val leaves_lr : Z.T -> Z.T Seq.seq
   8.427 -  val leaves_rl : Z.T -> Z.T Seq.seq
   8.428 -
   8.429 -  val all_bl_ru : Z.T -> Z.T Seq.seq
   8.430 -  val all_bl_ur : Z.T -> Z.T Seq.seq
   8.431 -  val all_td_lr : Z.T -> Z.T Seq.seq
   8.432 -  val all_td_rl : Z.T -> Z.T Seq.seq
   8.433 -  
   8.434 -end;
   8.435 -
   8.436 -functor ZipperSearchFUN(Zipper : ZIPPER) : ZIPPER_SEARCH
   8.437 -= struct
   8.438 -
   8.439 -structure Z = Zipper;
   8.440 -structure C = Z.C;
   8.441 -structure D = C.D; 
   8.442 -structure Trm = D.Trm; 
   8.443 -
   8.444 -fun sf_leaves_lr z = 
   8.445 -    case Z.trm z 
   8.446 -     of Trm.$ _ => [Z.LookIn (Z.move_down_left z),
   8.447 -                    Z.LookIn (Z.move_down_right z)]
   8.448 -      | Trm.Abs _ => [Z.LookIn (Z.move_down_abs z)]
   8.449 -      | _ => [Z.Here z];
   8.450 -fun sf_leaves_rl z = 
   8.451 -    case Z.trm z 
   8.452 -     of Trm.$ _ => [Z.LookIn (Z.move_down_right z),
   8.453 -                    Z.LookIn (Z.move_down_left z)]
   8.454 -      | Trm.Abs _ => [Z.LookIn (Z.move_down_abs z)]
   8.455 -      | _ => [Z.Here z];
   8.456 -val leaves_lr = Z.lzy_search sf_leaves_lr;
   8.457 -val leaves_rl = Z.lzy_search sf_leaves_rl;
   8.458 -
   8.459 -
   8.460 -fun sf_all_td_lr z = 
   8.461 -    case Z.trm z 
   8.462 -     of Trm.$ _ => [Z.Here z, Z.LookIn (Z.move_down_left z),
   8.463 -                    Z.LookIn (Z.move_down_right z)]
   8.464 -      | Trm.Abs _ => [Z.Here z, Z.LookIn (Z.move_down_abs z)]
   8.465 -      | _ => [Z.Here z];
   8.466 -fun sf_all_td_rl z = 
   8.467 -    case Z.trm z 
   8.468 -     of Trm.$ _ => [Z.Here z, Z.LookIn (Z.move_down_right z),
   8.469 -                    Z.LookIn (Z.move_down_left z)]
   8.470 -      | Trm.Abs _ => [Z.Here z, Z.LookIn (Z.move_down_abs z)]
   8.471 -      | _ => [Z.Here z];
   8.472 -fun sf_all_bl_ur z = 
   8.473 -    case Z.trm z 
   8.474 -     of Trm.$ _ => [Z.LookIn (Z.move_down_left z), Z.Here z,
   8.475 -                    Z.LookIn (Z.move_down_right z)]
   8.476 -      | Trm.Abs _ => [Z.LookIn (Z.move_down_abs z),
   8.477 -                      Z.Here z]
   8.478 -      | _ => [Z.Here z];
   8.479 -fun sf_all_bl_ru z = 
   8.480 -    case Z.trm z 
   8.481 -     of Trm.$ _ => [Z.LookIn (Z.move_down_left z),
   8.482 -                    Z.LookIn (Z.move_down_right z), Z.Here z]
   8.483 -      | Trm.Abs _ => [Z.LookIn (Z.move_down_abs z), Z.Here z]
   8.484 -      | _ => [Z.Here z];
   8.485 -
   8.486 -val all_td_lr = Z.lzy_search sf_all_td_lr;
   8.487 -val all_td_rl = Z.lzy_search sf_all_td_rl;
   8.488 -val all_bl_ur = Z.lzy_search sf_all_bl_ru;
   8.489 -val all_bl_ru = Z.lzy_search sf_all_bl_ur;
   8.490 -
   8.491 -end;
   8.492 -
   8.493 -
   8.494 -structure ZipperSearch = ZipperSearchFUN(Zipper);
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/Tools/IsaPlanner/README	Thu May 31 20:55:29 2007 +0200
     9.3 @@ -0,0 +1,4 @@
     9.4 +ID:         $Id$
     9.5 +Author:     Lucas Dixon, University of Edinburgh
     9.6 +
     9.7 +Support files for IsaPlanner (see http://isaplanner.sourceforge.net).
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/Tools/IsaPlanner/isand.ML	Thu May 31 20:55:29 2007 +0200
    10.3 @@ -0,0 +1,642 @@
    10.4 +(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
    10.5 +(*  Title:      Pure/IsaPlanner/isand.ML
    10.6 +    ID:		$Id$
    10.7 +    Author:     Lucas Dixon, University of Edinburgh
    10.8 +                lucas.dixon@ed.ac.uk
    10.9 +    Updated:    26 Apr 2005
   10.10 +    Date:       6 Aug 2004
   10.11 +*)
   10.12 +(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
   10.13 +(*  DESCRIPTION:
   10.14 +
   10.15 +    Natural Deduction tools
   10.16 +
   10.17 +    For working with Isabelle theorems in a natural detuction style.
   10.18 +    ie, not having to deal with meta level quantified varaibles,
   10.19 +    instead, we work with newly introduced frees, and hide the
   10.20 +    "all"'s, exporting results from theorems proved with the frees, to
   10.21 +    solve the all cases of the previous goal. This allows resolution
   10.22 +    to do proof search normally. 
   10.23 +
   10.24 +    Note: A nice idea: allow exporting to solve any subgoal, thus
   10.25 +    allowing the interleaving of proof, or provide a structure for the
   10.26 +    ordering of proof, thus allowing proof attempts in parrell, but
   10.27 +    recording the order to apply things in.
   10.28 +
   10.29 +    THINK: are we really ok with our varify name w.r.t the prop - do
   10.30 +    we also need to avoid names in the hidden hyps? What about
   10.31 +    unification contraints in flex-flex pairs - might they also have
   10.32 +    extra free vars?
   10.33 +*)
   10.34 +
   10.35 +signature ISA_ND =
   10.36 +sig
   10.37 +
   10.38 +  (* export data *)
   10.39 +  datatype export = export of
   10.40 +           {gth: Thm.thm, (* initial goal theorem *)
   10.41 +            sgid: int, (* subgoal id which has been fixed etc *)
   10.42 +            fixes: Thm.cterm list, (* frees *)
   10.43 +            assumes: Thm.cterm list} (* assumptions *)
   10.44 +  val fixes_of_exp : export -> Thm.cterm list
   10.45 +  val export_back : export -> Thm.thm -> Thm.thm Seq.seq
   10.46 +  val export_solution : export -> Thm.thm -> Thm.thm
   10.47 +  val export_solutions : export list * Thm.thm -> Thm.thm
   10.48 +
   10.49 +  (* inserting meta level params for frees in the conditions *)
   10.50 +  val allify_conditions :
   10.51 +      (Term.term -> Thm.cterm) ->
   10.52 +      (string * Term.typ) list -> Thm.thm -> Thm.thm * Thm.cterm list
   10.53 +  val allify_conditions' :
   10.54 +      (string * Term.typ) list -> Thm.thm -> Thm.thm * Thm.cterm list
   10.55 +  val assume_allified :
   10.56 +      theory -> (string * Term.sort) list * (string * Term.typ) list
   10.57 +      -> Term.term -> (Thm.cterm * Thm.thm)
   10.58 +
   10.59 +  (* meta level fixed params (i.e. !! vars) *)
   10.60 +  val fix_alls_in_term : Term.term -> Term.term * Term.term list
   10.61 +  val fix_alls_term : int -> Term.term -> Term.term * Term.term list
   10.62 +  val fix_alls_cterm : int -> Thm.thm -> Thm.cterm * Thm.cterm list
   10.63 +  val fix_alls' : int -> Thm.thm -> Thm.thm * Thm.cterm list
   10.64 +  val fix_alls : int -> Thm.thm -> Thm.thm * export
   10.65 +
   10.66 +  (* meta variables in types and terms *)
   10.67 +  val fix_tvars_to_tfrees_in_terms 
   10.68 +      : string list (* avoid these names *)
   10.69 +        -> Term.term list -> 
   10.70 +        (((string * int) * Term.sort) * (string * Term.sort)) list (* renamings *)
   10.71 +  val fix_vars_to_frees_in_terms
   10.72 +      : string list (* avoid these names *)
   10.73 +        -> Term.term list ->
   10.74 +        (((string * int) * Term.typ) * (string * Term.typ)) list (* renamings *)
   10.75 +  val fix_tvars_to_tfrees : Thm.thm -> Thm.ctyp list * Thm.thm
   10.76 +  val fix_vars_to_frees : Thm.thm -> Thm.cterm list * Thm.thm
   10.77 +  val fix_vars_and_tvars : 
   10.78 +      Thm.thm -> (Thm.cterm list * Thm.ctyp list) * Thm.thm
   10.79 +  val fix_vars_upto_idx : int -> Thm.thm -> Thm.thm
   10.80 +  val fix_tvars_upto_idx : int -> Thm.thm -> Thm.thm
   10.81 +  val unfix_frees : Thm.cterm list -> Thm.thm -> Thm.thm
   10.82 +  val unfix_tfrees : Thm.ctyp list -> Thm.thm -> Thm.thm
   10.83 +  val unfix_frees_and_tfrees :
   10.84 +      (Thm.cterm list * Thm.ctyp list) -> Thm.thm -> Thm.thm
   10.85 +
   10.86 +  (* assumptions/subgoals *)
   10.87 +  val assume_prems :
   10.88 +      int -> Thm.thm -> Thm.thm list * Thm.thm * Thm.cterm list
   10.89 +  val fixed_subgoal_thms : Thm.thm -> Thm.thm list * (Thm.thm list -> Thm.thm)
   10.90 +  val fixes_and_assumes : int -> Thm.thm -> Thm.thm list * Thm.thm * export
   10.91 +  val hide_other_goals : Thm.thm -> Thm.thm * Thm.cterm list
   10.92 +  val hide_prems : Thm.thm -> Thm.thm * Thm.cterm list
   10.93 +
   10.94 +  (* abstracts cterms (vars) to locally meta-all bounds *)
   10.95 +  val prepare_goal_export : string list * Thm.cterm list -> Thm.thm 
   10.96 +                            -> int * Thm.thm
   10.97 +  val solve_with : Thm.thm -> Thm.thm -> Thm.thm Seq.seq
   10.98 +  val subgoal_thms : Thm.thm -> Thm.thm list * (Thm.thm list -> Thm.thm)
   10.99 +end
  10.100 +
  10.101 +
  10.102 +structure IsaND 
  10.103 +: ISA_ND
  10.104 += struct
  10.105 +
  10.106 +(* Solve *some* subgoal of "th" directly by "sol" *)
  10.107 +(* Note: this is probably what Markus ment to do upon export of a
  10.108 +"show" but maybe he used RS/rtac instead, which would wrongly lead to
  10.109 +failing if there are premices to the shown goal. 
  10.110 +
  10.111 +given: 
  10.112 +sol : Thm.thm = [| Ai... |] ==> Ci
  10.113 +th : Thm.thm = 
  10.114 +  [| ... [| Ai... |] ==> Ci ... |] ==> G
  10.115 +results in: 
  10.116 +  [| ... [| Ai-1... |] ==> Ci-1
  10.117 +    [| Ai+1... |] ==> Ci+1 ...
  10.118 +  |] ==> G
  10.119 +i.e. solves some subgoal of th that is identical to sol. 
  10.120 +*)
  10.121 +fun solve_with sol th = 
  10.122 +    let fun solvei 0 = Seq.empty
  10.123 +          | solvei i = 
  10.124 +            Seq.append (bicompose false (false,sol,0) i th) (solvei (i - 1))
  10.125 +    in
  10.126 +      solvei (Thm.nprems_of th)
  10.127 +    end;
  10.128 +
  10.129 +
  10.130 +(* Given ctertmify function, (string,type) pairs capturing the free
  10.131 +vars that need to be allified in the assumption, and a theorem with
  10.132 +assumptions possibly containing the free vars, then we give back the
  10.133 +assumptions allified as hidden hyps. 
  10.134 +
  10.135 +Given: x 
  10.136 +th: A vs ==> B vs 
  10.137 +Results in: "B vs" [!!x. A x]
  10.138 +*)
  10.139 +fun allify_conditions ctermify Ts th = 
  10.140 +    let 
  10.141 +      val premts = Thm.prems_of th;
  10.142 +    
  10.143 +      fun allify_prem_var (vt as (n,ty),t)  = 
  10.144 +          (Term.all ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
  10.145 +
  10.146 +      fun allify_prem Ts p = foldr allify_prem_var p Ts
  10.147 +
  10.148 +      val cTs = map (ctermify o Free) Ts
  10.149 +      val cterm_asms = map (ctermify o allify_prem Ts) premts
  10.150 +      val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms
  10.151 +    in 
  10.152 +      (Library.foldl (fn (x,y) => y COMP x) (th, allifyied_asm_thms), cterm_asms)
  10.153 +    end;
  10.154 +
  10.155 +fun allify_conditions' Ts th = 
  10.156 +    allify_conditions (Thm.cterm_of (Thm.theory_of_thm th)) Ts th;
  10.157 +
  10.158 +(* allify types *)
  10.159 +fun allify_typ ts ty = 
  10.160 +    let 
  10.161 +      fun trec (x as (TFree (s,srt))) = 
  10.162 +          (case Library.find_first (fn (s2,srt2) => s = s2) ts
  10.163 +            of NONE => x
  10.164 +             | SOME (s2,_) => TVar ((s,0),srt))
  10.165 +            (*  Maybe add in check here for bad sorts? 
  10.166 +             if srt = srt2 then TVar ((s,0),srt) 
  10.167 +               else raise  ("thaw_typ", ts, ty) *)
  10.168 +          | trec (Type (s,typs)) = Type (s, map trec typs)
  10.169 +          | trec (v as TVar _) = v;
  10.170 +    in trec ty end;
  10.171 +
  10.172 +(* implicit types and term *)
  10.173 +fun allify_term_typs ty = Term.map_types (allify_typ ty);
  10.174 +
  10.175 +(* allified version of term, given frees to allify over. Note that we
  10.176 +only allify over the types on the given allified cterm, we can't do
  10.177 +this for the theorem as we are not allowed type-vars in the hyp. *)
  10.178 +(* FIXME: make the allified term keep the same conclusion as it
  10.179 +started with, rather than a strictly more general version (ie use
  10.180 +instantiate with initial params we abstracted from, rather than
  10.181 +forall_elim_vars. *)
  10.182 +fun assume_allified sgn (tyvs,vs) t = 
  10.183 +    let
  10.184 +      fun allify_var (vt as (n,ty),t)  = 
  10.185 +          (Term.all ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
  10.186 +      fun allify Ts p = List.foldr allify_var p Ts
  10.187 +
  10.188 +      val ctermify = Thm.cterm_of sgn;
  10.189 +      val cvars = map (fn (n,ty) => ctermify (Var ((n,0),ty))) vs
  10.190 +      val allified_term = t |> allify vs;
  10.191 +      val ct = ctermify allified_term;
  10.192 +      val typ_allified_ct = ctermify (allify_term_typs tyvs allified_term);
  10.193 +    in (typ_allified_ct, 
  10.194 +        Drule.forall_elim_vars 0 (Thm.assume ct)) end;
  10.195 +
  10.196 +
  10.197 +(* change type-vars to fresh type frees *)
  10.198 +fun fix_tvars_to_tfrees_in_terms names ts = 
  10.199 +    let 
  10.200 +      val tfree_names = map fst (List.foldr Term.add_term_tfrees [] ts);
  10.201 +      val tvars = List.foldr Term.add_term_tvars [] ts;
  10.202 +      val (names',renamings) = 
  10.203 +          List.foldr (fn (tv as ((n,i),s),(Ns,Rs)) => 
  10.204 +                         let val n2 = Name.variant Ns n in 
  10.205 +                           (n2::Ns, (tv, (n2,s))::Rs)
  10.206 +                         end) (tfree_names @ names,[]) tvars;
  10.207 +    in renamings end;
  10.208 +fun fix_tvars_to_tfrees th = 
  10.209 +    let 
  10.210 +      val sign = Thm.theory_of_thm th;
  10.211 +      val ctypify = Thm.ctyp_of sign;
  10.212 +      val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
  10.213 +      val renamings = fix_tvars_to_tfrees_in_terms 
  10.214 +                        [] ((Thm.prop_of th) :: tpairs);
  10.215 +      val crenamings = 
  10.216 +          map (fn (v,f) => (ctypify (TVar v), ctypify (TFree f)))
  10.217 +              renamings;
  10.218 +      val fixedfrees = map snd crenamings;
  10.219 +    in (fixedfrees, Thm.instantiate (crenamings, []) th) end;
  10.220 +
  10.221 +
  10.222 +(* change type-free's to type-vars in th, skipping the ones in "ns" *)
  10.223 +fun unfix_tfrees ns th = 
  10.224 +    let 
  10.225 +      val varfiytfrees = map (Term.dest_TFree o Thm.typ_of) ns
  10.226 +      val skiptfrees = subtract (op =) varfiytfrees (Term.add_term_tfrees (Thm.prop_of th,[]));
  10.227 +    in #2 (Thm.varifyT' skiptfrees th) end;
  10.228 +
  10.229 +(* change schematic/meta vars to fresh free vars, avoiding name clashes 
  10.230 +   with "names" *)
  10.231 +fun fix_vars_to_frees_in_terms names ts = 
  10.232 +    let 
  10.233 +      val vars = map Term.dest_Var (List.foldr Term.add_term_vars [] ts);
  10.234 +      val Ns = List.foldr Term.add_term_names names ts;
  10.235 +      val (_,renamings) = 
  10.236 +          Library.foldl (fn ((Ns,Rs),v as ((n,i),ty)) => 
  10.237 +                    let val n2 = Name.variant Ns n in
  10.238 +                      (n2 :: Ns, (v, (n2,ty)) :: Rs)
  10.239 +                    end) ((Ns,[]), vars);
  10.240 +    in renamings end;
  10.241 +fun fix_vars_to_frees th = 
  10.242 +    let 
  10.243 +      val ctermify = Thm.cterm_of (Thm.theory_of_thm th)
  10.244 +      val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
  10.245 +      val renamings = fix_vars_to_frees_in_terms 
  10.246 +                        [] ([Thm.prop_of th] @ tpairs);
  10.247 +      val crenamings = 
  10.248 +          map (fn (v,f) => (ctermify (Var v), ctermify (Free f)))
  10.249 +              renamings;
  10.250 +      val fixedfrees = map snd crenamings;
  10.251 +    in (fixedfrees, Thm.instantiate ([], crenamings) th) end;
  10.252 +
  10.253 +fun fix_tvars_upto_idx ix th = 
  10.254 +    let 
  10.255 +      val sgn = Thm.theory_of_thm th;
  10.256 +      val ctypify = Thm.ctyp_of sgn
  10.257 +      val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
  10.258 +      val prop = (Thm.prop_of th);
  10.259 +      val tvars = List.foldr Term.add_term_tvars [] (prop :: tpairs);
  10.260 +      val ctyfixes = 
  10.261 +          map_filter 
  10.262 +            (fn (v as ((s,i),ty)) => 
  10.263 +                if i <= ix then SOME (ctypify (TVar v), ctypify (TFree (s,ty)))
  10.264 +                else NONE) tvars;
  10.265 +    in Thm.instantiate (ctyfixes, []) th end;
  10.266 +fun fix_vars_upto_idx ix th = 
  10.267 +    let 
  10.268 +      val sgn = Thm.theory_of_thm th;
  10.269 +      val ctermify = Thm.cterm_of sgn
  10.270 +      val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
  10.271 +      val prop = (Thm.prop_of th);
  10.272 +      val vars = map Term.dest_Var (List.foldr Term.add_term_vars 
  10.273 +                                               [] (prop :: tpairs));
  10.274 +      val cfixes = 
  10.275 +          map_filter 
  10.276 +            (fn (v as ((s,i),ty)) => 
  10.277 +                if i <= ix then SOME (ctermify (Var v), ctermify (Free (s,ty)))
  10.278 +                else NONE) vars;
  10.279 +    in Thm.instantiate ([], cfixes) th end;
  10.280 +
  10.281 +
  10.282 +(* make free vars into schematic vars with index zero *)
  10.283 + fun unfix_frees frees = 
  10.284 +     apply (map (K (Drule.forall_elim_var 0)) frees) 
  10.285 +     o Drule.forall_intr_list frees;
  10.286 +
  10.287 +(* fix term and type variables *)
  10.288 +fun fix_vars_and_tvars th = 
  10.289 +    let val (tvars, th') = fix_tvars_to_tfrees th
  10.290 +      val (vars, th'') = fix_vars_to_frees th' 
  10.291 +    in ((vars, tvars), th'') end;
  10.292 +
  10.293 +(* implicit Thm.thm argument *)
  10.294 +(* assumes: vars may contain fixed versions of the frees *)
  10.295 +(* THINK: what if vs already has types varified? *)
  10.296 +fun unfix_frees_and_tfrees (vs,tvs) = 
  10.297 +    (unfix_tfrees tvs o unfix_frees vs);
  10.298 +
  10.299 +(* datatype to capture an exported result, ie a fix or assume. *)
  10.300 +datatype export = 
  10.301 +         export of {fixes : Thm.cterm list, (* fixed vars *)
  10.302 +                    assumes : Thm.cterm list, (* hidden hyps/assumed prems *)
  10.303 +                    sgid : int,
  10.304 +                    gth :  Thm.thm}; (* subgoal/goalthm *)
  10.305 +
  10.306 +fun fixes_of_exp (export rep) = #fixes rep;
  10.307 +
  10.308 +(* export the result of the new goal thm, ie if we reduced teh
  10.309 +subgoal, then we get a new reduced subtgoal with the old
  10.310 +all-quantified variables *)
  10.311 +local 
  10.312 +
  10.313 +(* allify puts in a meta level univ quantifier for a free variavble *)
  10.314 +fun allify_term (v, t) = 
  10.315 +    let val vt = #t (Thm.rep_cterm v)
  10.316 +      val (n,ty) = Term.dest_Free vt
  10.317 +    in (Term.all ty) $ (Abs(n,ty,Term.abstract_over (vt, t))) end;
  10.318 +
  10.319 +fun allify_for_sg_term ctermify vs t =
  10.320 +    let val t_alls = foldr allify_term t vs;
  10.321 +        val ct_alls = ctermify t_alls; 
  10.322 +    in 
  10.323 +      (ct_alls, Drule.forall_elim_list vs (Thm.assume ct_alls))
  10.324 +    end;
  10.325 +(* lookup type of a free var name from a list *)
  10.326 +fun lookupfree vs vn  = 
  10.327 +    case Library.find_first (fn (n,ty) => n = vn) vs of 
  10.328 +      NONE => error ("prepare_goal_export:lookupfree: " ^ vn ^ " does not occur in the term")
  10.329 +    | SOME x => x;
  10.330 +in
  10.331 +fun export_back (export {fixes = vs, assumes = hprems, 
  10.332 +                         sgid = i, gth = gth}) newth = 
  10.333 +    let 
  10.334 +      val sgn = Thm.theory_of_thm newth;
  10.335 +      val ctermify = Thm.cterm_of sgn;
  10.336 +
  10.337 +      val sgs = prems_of newth;
  10.338 +      val (sgallcts, sgthms) = 
  10.339 +          Library.split_list (map (allify_for_sg_term ctermify vs) sgs);
  10.340 +      val minimal_newth = 
  10.341 +          (Library.foldl (fn ( newth', sgthm) => 
  10.342 +                          Drule.compose_single (sgthm, 1, newth'))
  10.343 +                      (newth, sgthms));
  10.344 +      val allified_newth = 
  10.345 +          minimal_newth 
  10.346 +            |> Drule.implies_intr_list hprems
  10.347 +            |> Drule.forall_intr_list vs 
  10.348 +
  10.349 +      val newth' = Drule.implies_intr_list sgallcts allified_newth
  10.350 +    in
  10.351 +      bicompose false (false, newth', (length sgallcts)) i gth
  10.352 +    end;
  10.353 +
  10.354 +(* 
  10.355 +Given "vs" : names of free variables to abstract over,
  10.356 +Given cterms : premices to abstract over (P1... Pn) in terms of vs,
  10.357 +Given a thm of the form: 
  10.358 +P1 vs; ...; Pn vs ==> Goal(C vs)
  10.359 +
  10.360 +Gives back: 
  10.361 +(n, length of given cterms which have been allified
  10.362 + [| !! vs. P1 vs; !! vs. Pn vs |] ==> !! C vs) the allified thm
  10.363 +*)
  10.364 +(* note: C may contain further premices etc 
  10.365 +Note that cterms is the assumed facts, ie prems of "P1" that are
  10.366 +reintroduced in allified form.
  10.367 +*)
  10.368 +fun prepare_goal_export (vs, cterms) th = 
  10.369 +    let 
  10.370 +      val sgn = Thm.theory_of_thm th;
  10.371 +      val ctermify = Thm.cterm_of sgn;
  10.372 +
  10.373 +      val allfrees = map Term.dest_Free (Term.term_frees (Thm.prop_of th))
  10.374 +      val cfrees = map (ctermify o Free o lookupfree allfrees) vs
  10.375 +
  10.376 +      val sgs = prems_of th;
  10.377 +      val (sgallcts, sgthms) = 
  10.378 +          Library.split_list (map (allify_for_sg_term ctermify cfrees) sgs);
  10.379 +
  10.380 +      val minimal_th = 
  10.381 +          Goal.conclude (Library.foldl (fn ( th', sgthm) => 
  10.382 +                          Drule.compose_single (sgthm, 1, th'))
  10.383 +                      (th, sgthms));
  10.384 +
  10.385 +      val allified_th = 
  10.386 +          minimal_th 
  10.387 +            |> Drule.implies_intr_list cterms
  10.388 +            |> Drule.forall_intr_list cfrees 
  10.389 +
  10.390 +      val th' = Drule.implies_intr_list sgallcts allified_th
  10.391 +    in
  10.392 +      ((length sgallcts), th')
  10.393 +    end;
  10.394 +
  10.395 +end;
  10.396 +
  10.397 +
  10.398 +(* exporting function that takes a solution to the fixed/assumed goal,
  10.399 +and uses this to solve the subgoal in the main theorem *)
  10.400 +fun export_solution (export {fixes = cfvs, assumes = hcprems,
  10.401 +                             sgid = i, gth = gth}) solth = 
  10.402 +    let 
  10.403 +      val solth' = 
  10.404 +          solth |> Drule.implies_intr_list hcprems
  10.405 +                |> Drule.forall_intr_list cfvs
  10.406 +    in Drule.compose_single (solth', i, gth) end;
  10.407 +
  10.408 +fun export_solutions (xs,th) = foldr (uncurry export_solution) th xs;
  10.409 +
  10.410 +
  10.411 +(* fix parameters of a subgoal "i", as free variables, and create an
  10.412 +exporting function that will use the result of this proved goal to
  10.413 +show the goal in the original theorem. 
  10.414 +
  10.415 +Note, an advantage of this over Isar is that it supports instantiation
  10.416 +of unkowns in the earlier theorem, ie we can do instantiation of meta
  10.417 +vars! 
  10.418 +
  10.419 +avoids constant, free and vars names. 
  10.420 +
  10.421 +loosely corresponds to:
  10.422 +Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm
  10.423 +Result: 
  10.424 +  ("(As ==> SGi x') ==> (As ==> SGi x')" : thm, 
  10.425 +   expf : 
  10.426 +     ("As ==> SGi x'" : thm) -> 
  10.427 +     ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm)
  10.428 +*)
  10.429 +fun fix_alls_in_term alledt = 
  10.430 +    let
  10.431 +      val t = Term.strip_all_body alledt;
  10.432 +      val alls = rev (Term.strip_all_vars alledt);
  10.433 +      val varnames = map (fst o fst o Term.dest_Var) (Term.term_vars t)
  10.434 +      val names = Term.add_term_names (t,varnames);
  10.435 +      val fvs = map Free 
  10.436 +                    (Name.variant_list names (map fst alls)
  10.437 +                       ~~ (map snd alls));
  10.438 +    in ((subst_bounds (fvs,t)), fvs) end;
  10.439 +
  10.440 +fun fix_alls_term i t = 
  10.441 +    let 
  10.442 +      val varnames = map (fst o fst o Term.dest_Var) (Term.term_vars t)
  10.443 +      val names = Term.add_term_names (t,varnames);
  10.444 +      val gt = Logic.get_goal t i;
  10.445 +      val body = Term.strip_all_body gt;
  10.446 +      val alls = rev (Term.strip_all_vars gt);
  10.447 +      val fvs = map Free 
  10.448 +                    (Name.variant_list names (map fst alls)
  10.449 +                       ~~ (map snd alls));
  10.450 +    in ((subst_bounds (fvs,body)), fvs) end;
  10.451 +
  10.452 +fun fix_alls_cterm i th = 
  10.453 +    let
  10.454 +      val ctermify = Thm.cterm_of (Thm.theory_of_thm th);
  10.455 +      val (fixedbody, fvs) = fix_alls_term i (Thm.prop_of th);
  10.456 +      val cfvs = rev (map ctermify fvs);
  10.457 +      val ct_body = ctermify fixedbody
  10.458 +    in
  10.459 +      (ct_body, cfvs)
  10.460 +    end;
  10.461 +
  10.462 +fun fix_alls' i = 
  10.463 +     (apfst Thm.trivial) o (fix_alls_cterm i);
  10.464 +
  10.465 +
  10.466 +(* hide other goals *) 
  10.467 +(* note the export goal is rotated by (i - 1) and will have to be
  10.468 +unrotated to get backto the originial position(s) *)
  10.469 +fun hide_other_goals th = 
  10.470 +    let
  10.471 +      (* tl beacuse fst sg is the goal we are interested in *)
  10.472 +      val cprems = tl (Drule.cprems_of th)
  10.473 +      val aprems = map Thm.assume cprems
  10.474 +    in
  10.475 +      (Drule.implies_elim_list (Drule.rotate_prems 1 th) aprems, 
  10.476 +       cprems)
  10.477 +    end;
  10.478 +
  10.479 +(* a nicer version of the above that leaves only a single subgoal (the
  10.480 +other subgoals are hidden hyps, that the exporter suffles about)
  10.481 +namely the subgoal that we were trying to solve. *)
  10.482 +(* loosely corresponds to:
  10.483 +Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm
  10.484 +Result: 
  10.485 +  ("(As ==> SGi x') ==> SGi x'" : thm, 
  10.486 +   expf : 
  10.487 +     ("SGi x'" : thm) -> 
  10.488 +     ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm)
  10.489 +*)
  10.490 +fun fix_alls i th = 
  10.491 +    let 
  10.492 +      val (fixed_gth, fixedvars) = fix_alls' i th
  10.493 +      val (sml_gth, othergoals) = hide_other_goals fixed_gth
  10.494 +    in
  10.495 +      (sml_gth, export {fixes = fixedvars, 
  10.496 +                        assumes = othergoals, 
  10.497 +                        sgid = i, gth = th})
  10.498 +    end;
  10.499 +
  10.500 +
  10.501 +(* assume the premises of subgoal "i", this gives back a list of
  10.502 +assumed theorems that are the premices of subgoal i, it also gives
  10.503 +back a new goal thm and an exporter, the new goalthm is as the old
  10.504 +one, but without the premices, and the exporter will use a proof of
  10.505 +the new goalthm, possibly using the assumed premices, to shoe the
  10.506 +orginial goal.
  10.507 +
  10.508 +Note: Dealing with meta vars, need to meta-level-all them in the
  10.509 +shyps, which we can later instantiate with a specific value.... ? 
  10.510 +think about this... maybe need to introduce some new fixed vars and
  10.511 +then remove them again at the end... like I do with rw_inst. 
  10.512 +
  10.513 +loosely corresponds to:
  10.514 +Given "[| SG0; ... [| A0; ... An |] ==> SGi; ... SGm |] ==> G" : thm
  10.515 +Result: 
  10.516 +(["A0" [A0], ... ,"An" [An]] : thm list, -- assumptions
  10.517 + "SGi ==> SGi" : thm, -- new goal 
  10.518 + "SGi" ["A0" ... "An"] : thm ->   -- export function
  10.519 +    ("[| SG0 ... SGi-1, SGi+1, SGm |] ==> G" : thm) list)
  10.520 +*)
  10.521 +fun assume_prems i th =
  10.522 +    let 
  10.523 +      val t = (prop_of th); 
  10.524 +      val gt = Logic.get_goal t i;
  10.525 +      val _ = case Term.strip_all_vars gt of [] => () 
  10.526 +              | _ => error "assume_prems: goal has params"
  10.527 +      val body = gt;
  10.528 +      val prems = Logic.strip_imp_prems body;
  10.529 +      val concl = Logic.strip_imp_concl body;
  10.530 +
  10.531 +      val sgn = Thm.theory_of_thm th;
  10.532 +      val ctermify = Thm.cterm_of sgn;
  10.533 +      val cprems = map ctermify prems;
  10.534 +      val aprems = map Thm.assume cprems;
  10.535 +      val gthi = Thm.trivial (ctermify concl);
  10.536 +
  10.537 +      (* fun explortf thi = 
  10.538 +          Drule.compose (Drule.implies_intr_list cprems thi, 
  10.539 +                         i, th) *)
  10.540 +    in
  10.541 +      (aprems, gthi, cprems)
  10.542 +    end;
  10.543 +
  10.544 +
  10.545 +(* first fix the variables, then assume the assumptions *)
  10.546 +(* loosely corresponds to:
  10.547 +Given 
  10.548 +  "[| SG0; ... 
  10.549 +      !! xs. [| A0 xs; ... An xs |] ==> SGi xs; 
  10.550 +      ... SGm |] ==> G" : thm
  10.551 +Result: 
  10.552 +(["A0 xs'" [A0 xs'], ... ,"An xs'" [An xs']] : thm list, -- assumptions
  10.553 + "SGi xs' ==> SGi xs'" : thm,  -- new goal 
  10.554 + "SGi xs'" ["A0 xs'" ... "An xs'"] : thm ->   -- export function
  10.555 +    ("[| SG0 ... SGi-1, SGi+1, SGm |] ==> G" : thm) list)
  10.556 +*)
  10.557 +
  10.558 +(* Note: the fix_alls actually pulls through all the assumptions which
  10.559 +means that the second export is not needed. *)
  10.560 +fun fixes_and_assumes i th = 
  10.561 +    let 
  10.562 +      val (fixgth, exp1) = fix_alls i th
  10.563 +      val (assumps, goalth, _) = assume_prems 1 fixgth
  10.564 +    in 
  10.565 +      (assumps, goalth, exp1)
  10.566 +    end;
  10.567 +
  10.568 +
  10.569 +(* Fixme: allow different order of subgoals given to expf *)
  10.570 +(* make each subgoal into a separate thm that needs to be proved *)
  10.571 +(* loosely corresponds to:
  10.572 +Given 
  10.573 +  "[| SG0; ... SGm |] ==> G" : thm
  10.574 +Result: 
  10.575 +(["SG0 ==> SG0", ... ,"SGm ==> SGm"] : thm list, -- goals
  10.576 + ["SG0", ..., "SGm"] : thm list ->   -- export function
  10.577 +   "G" : thm)
  10.578 +*)
  10.579 +fun subgoal_thms th = 
  10.580 +    let 
  10.581 +      val t = (prop_of th); 
  10.582 +
  10.583 +      val prems = Logic.strip_imp_prems t;
  10.584 +
  10.585 +      val sgn = Thm.theory_of_thm th;
  10.586 +      val ctermify = Thm.cterm_of sgn;
  10.587 +
  10.588 +      val aprems = map (Thm.trivial o ctermify) prems;
  10.589 +
  10.590 +      fun explortf premths = 
  10.591 +          Drule.implies_elim_list th premths
  10.592 +    in
  10.593 +      (aprems, explortf)
  10.594 +    end;
  10.595 +
  10.596 +
  10.597 +(* make all the premices of a theorem hidden, and provide an unhide
  10.598 +function, that will bring them back out at a later point. This is
  10.599 +useful if you want to get back these premices, after having used the
  10.600 +theorem with the premices hidden *)
  10.601 +(* loosely corresponds to:
  10.602 +Given "As ==> G" : thm
  10.603 +Result: ("G [As]" : thm, 
  10.604 +         "G [As]" : thm -> "As ==> G" : thm
  10.605 +*)
  10.606 +fun hide_prems th = 
  10.607 +    let 
  10.608 +      val cprems = Drule.cprems_of th;
  10.609 +      val aprems = map Thm.assume cprems;
  10.610 +    (*   val unhidef = Drule.implies_intr_list cprems; *)
  10.611 +    in
  10.612 +      (Drule.implies_elim_list th aprems, cprems)
  10.613 +    end;
  10.614 +
  10.615 +
  10.616 +
  10.617 +
  10.618 +(* Fixme: allow different order of subgoals in exportf *)
  10.619 +(* as above, but also fix all parameters in all subgoals, and uses
  10.620 +fix_alls, not fix_alls', ie doesn't leave extra asumptions as apparent
  10.621 +subgoals. *)
  10.622 +(* loosely corresponds to:
  10.623 +Given 
  10.624 +  "[| !! x0s. A0s x0s ==> SG0 x0s; 
  10.625 +      ...; !! xms. Ams xms ==> SGm xms|] ==> G" : thm
  10.626 +Result: 
  10.627 +(["(A0s x0s' ==> SG0 x0s') ==> SG0 x0s'", 
  10.628 +  ... ,"(Ams xms' ==> SGm xms') ==> SGm xms'"] : thm list, -- goals
  10.629 + ["SG0 x0s'", ..., "SGm xms'"] : thm list ->   -- export function
  10.630 +   "G" : thm)
  10.631 +*)
  10.632 +(* requires being given solutions! *)
  10.633 +fun fixed_subgoal_thms th = 
  10.634 +    let 
  10.635 +      val (subgoals, expf) = subgoal_thms th;
  10.636 +(*       fun export_sg (th, exp) = exp th; *)
  10.637 +      fun export_sgs expfs solthms = 
  10.638 +          expf (map2 (curry (op |>)) solthms expfs);
  10.639 +(*           expf (map export_sg (ths ~~ expfs)); *)
  10.640 +    in 
  10.641 +      apsnd export_sgs (Library.split_list (map (apsnd export_solution o 
  10.642 +                                                 fix_alls 1) subgoals))
  10.643 +    end;
  10.644 +
  10.645 +end;
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/Tools/IsaPlanner/rw_inst.ML	Thu May 31 20:55:29 2007 +0200
    11.3 @@ -0,0 +1,315 @@
    11.4 +(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
    11.5 +(*  Title:      Pure/IsaPlanner/rw_inst.ML
    11.6 +    ID:         $Id$
    11.7 +    Author:     Lucas Dixon, University of Edinburgh
    11.8 +                lucas.dixon@ed.ac.uk
    11.9 +    Created:    25 Aug 2004
   11.10 +*)
   11.11 +(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
   11.12 +(*  DESCRIPTION:
   11.13 +
   11.14 +    rewriting using a conditional meta-equality theorem which supports 
   11.15 +    schematic variable instantiation.
   11.16 +
   11.17 +*)   
   11.18 +(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
   11.19 +signature RW_INST =
   11.20 +sig
   11.21 +
   11.22 +  (* Rewrite: give it instantiation infromation, a rule, and the
   11.23 +  target thm, and it will return the rewritten target thm *)
   11.24 +  val rw :
   11.25 +      ((Term.indexname * (Term.sort * Term.typ)) list *  (* type var instantiations *)
   11.26 +       (Term.indexname * (Term.typ * Term.term)) list)  (* schematic var instantiations *)
   11.27 +      * (string * Term.typ) list           (* Fake named bounds + types *)
   11.28 +      * (string * Term.typ) list           (* names of bound + types *)
   11.29 +      * Term.term ->                       (* outer term for instantiation *)
   11.30 +      Thm.thm ->                           (* rule with indexies lifted *)
   11.31 +      Thm.thm ->                           (* target thm *)
   11.32 +      Thm.thm                              (* rewritten theorem possibly 
   11.33 +                                              with additional premises for 
   11.34 +                                              rule conditions *)
   11.35 +
   11.36 +  (* used tools *)
   11.37 +  val mk_abstractedrule :
   11.38 +      (string * Term.typ) list (* faked outer bound *)
   11.39 +      -> (string * Term.typ) list (* hopeful name of outer bounds *)
   11.40 +      -> Thm.thm -> Thm.cterm list * Thm.thm
   11.41 +  val mk_fixtvar_tyinsts :
   11.42 +      (Term.indexname * (Term.sort * Term.typ)) list ->
   11.43 +      Term.term list -> ((string * int) * (Term.sort * Term.typ)) list 
   11.44 +                        * (string * Term.sort) list
   11.45 +  val mk_renamings :
   11.46 +      Term.term -> Thm.thm -> (((string * int) * Term.typ) * Term.term) list
   11.47 +  val new_tfree :
   11.48 +      ((string * int) * Term.sort) *
   11.49 +      (((string * int) * (Term.sort * Term.typ)) list * string list) ->
   11.50 +      ((string * int) * (Term.sort * Term.typ)) list * string list
   11.51 +  val cross_inst : (Term.indexname * (Term.typ * Term.term)) list 
   11.52 +                   -> (Term.indexname *(Term.typ * Term.term)) list
   11.53 +  val cross_inst_typs : (Term.indexname * (Term.sort * Term.typ)) list 
   11.54 +                   -> (Term.indexname * (Term.sort * Term.typ)) list
   11.55 +
   11.56 +  val beta_contract : Thm.thm -> Thm.thm
   11.57 +  val beta_eta_contract : Thm.thm -> Thm.thm
   11.58 +
   11.59 +end;
   11.60 +
   11.61 +structure RWInst 
   11.62 +: RW_INST
   11.63 += struct
   11.64 +
   11.65 +
   11.66 +(* beta contract the theorem *)
   11.67 +fun beta_contract thm = 
   11.68 +    equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm;
   11.69 +
   11.70 +(* beta-eta contract the theorem *)
   11.71 +fun beta_eta_contract thm = 
   11.72 +    let
   11.73 +      val thm2 = equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm
   11.74 +      val thm3 = equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2
   11.75 +    in thm3 end;
   11.76 +
   11.77 +
   11.78 +(* to get the free names of a theorem (including hyps and flexes) *)
   11.79 +fun usednames_of_thm th =
   11.80 +    let val rep = Thm.rep_thm th
   11.81 +      val hyps = #hyps rep
   11.82 +      val (tpairl,tpairr) = Library.split_list (#tpairs rep)
   11.83 +      val prop = #prop rep
   11.84 +    in
   11.85 +      List.foldr Term.add_term_names [] (prop :: (tpairl @ (tpairr @ hyps)))
   11.86 +    end;
   11.87 +
   11.88 +(* Given a list of variables that were bound, and a that has been
   11.89 +instantiated with free variable placeholders for the bound vars, it
   11.90 +creates an abstracted version of the theorem, with local bound vars as
   11.91 +lambda-params:
   11.92 +
   11.93 +Ts: 
   11.94 +("x", ty)
   11.95 +
   11.96 +rule::
   11.97 +C :x ==> P :x = Q :x
   11.98 +
   11.99 +results in:
  11.100 +("!! x. C x", (%x. p x = %y. p y) [!! x. C x])
  11.101 +
  11.102 +note: assumes rule is instantiated
  11.103 +*)
  11.104 +(* Note, we take abstraction in the order of last abstraction first *)
  11.105 +fun mk_abstractedrule TsFake Ts rule = 
  11.106 +    let 
  11.107 +      val ctermify = Thm.cterm_of (Thm.theory_of_thm rule);
  11.108 +
  11.109 +      (* now we change the names of temporary free vars that represent 
  11.110 +         bound vars with binders outside the redex *)
  11.111 +      val prop = Thm.prop_of rule;
  11.112 +      val names = usednames_of_thm rule;
  11.113 +      val (fromnames,tonames,names2,Ts') = 
  11.114 +          Library.foldl (fn ((rnf,rnt,names, Ts''),((faken,_),(n,ty))) => 
  11.115 +                    let val n2 = Name.variant names n in
  11.116 +                      (ctermify (Free(faken,ty)) :: rnf,
  11.117 +                       ctermify (Free(n2,ty)) :: rnt, 
  11.118 +                       n2 :: names,
  11.119 +                       (n2,ty) :: Ts'')
  11.120 +                    end)
  11.121 +                (([],[],names, []), TsFake~~Ts);
  11.122 +
  11.123 +      (* rename conflicting free's in the rule to avoid cconflicts
  11.124 +      with introduced vars from bounds outside in redex *)
  11.125 +      val rule' = rule |> Drule.forall_intr_list fromnames
  11.126 +                       |> Drule.forall_elim_list tonames;
  11.127 +      
  11.128 +      (* make unconditional rule and prems *)
  11.129 +      val (uncond_rule, cprems) = IsaND.allify_conditions ctermify (rev Ts') 
  11.130 +                                                          rule';
  11.131 +
  11.132 +      (* using these names create lambda-abstracted version of the rule *)
  11.133 +      val abstractions = rev (Ts' ~~ tonames);
  11.134 +      val abstract_rule = Library.foldl (fn (th,((n,ty),ct)) => 
  11.135 +                                    Thm.abstract_rule n ct th)
  11.136 +                                (uncond_rule, abstractions);
  11.137 +    in (cprems, abstract_rule) end;
  11.138 +
  11.139 +
  11.140 +(* given names to avoid, and vars that need to be fixed, it gives
  11.141 +unique new names to the vars so that they can be fixed as free
  11.142 +variables *)
  11.143 +(* make fixed unique free variable instantiations for non-ground vars *)
  11.144 +(* Create a table of vars to be renamed after instantiation - ie
  11.145 +      other uninstantiated vars in the hyps of the rule 
  11.146 +      ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *)
  11.147 +fun mk_renamings tgt rule_inst = 
  11.148 +    let
  11.149 +      val rule_conds = Thm.prems_of rule_inst
  11.150 +      val names = foldr Term.add_term_names [] (tgt :: rule_conds);
  11.151 +      val (conds_tyvs,cond_vs) = 
  11.152 +          Library.foldl (fn ((tyvs, vs), t) => 
  11.153 +                    (Library.union
  11.154 +                       (Term.term_tvars t, tyvs),
  11.155 +                     Library.union 
  11.156 +                       (map Term.dest_Var (Term.term_vars t), vs))) 
  11.157 +                (([],[]), rule_conds);
  11.158 +      val termvars = map Term.dest_Var (Term.term_vars tgt); 
  11.159 +      val vars_to_fix = Library.union (termvars, cond_vs);
  11.160 +      val (renamings, names2) = 
  11.161 +          foldr (fn (((n,i),ty), (vs, names')) => 
  11.162 +                    let val n' = Name.variant names' n in
  11.163 +                      ((((n,i),ty), Free (n', ty)) :: vs, n'::names')
  11.164 +                    end)
  11.165 +                ([], names) vars_to_fix;
  11.166 +    in renamings end;
  11.167 +
  11.168 +(* make a new fresh typefree instantiation for the given tvar *)
  11.169 +fun new_tfree (tv as (ix,sort), (pairs,used)) =
  11.170 +      let val v = Name.variant used (string_of_indexname ix)
  11.171 +      in  ((ix,(sort,TFree(v,sort)))::pairs, v::used)  end;
  11.172 +
  11.173 +
  11.174 +(* make instantiations to fix type variables that are not 
  11.175 +   already instantiated (in ignore_ixs) from the list of terms. *)
  11.176 +fun mk_fixtvar_tyinsts ignore_insts ts = 
  11.177 +    let 
  11.178 +      val ignore_ixs = map fst ignore_insts;
  11.179 +      val (tvars, tfrees) = 
  11.180 +            foldr (fn (t, (varixs, tfrees)) => 
  11.181 +                      (Term.add_term_tvars (t,varixs),
  11.182 +                       Term.add_term_tfrees (t,tfrees)))
  11.183 +                  ([],[]) ts;
  11.184 +        val unfixed_tvars = 
  11.185 +            List.filter (fn (ix,s) => not (member (op =) ignore_ixs ix)) tvars;
  11.186 +        val (fixtyinsts, _) = foldr new_tfree ([], map fst tfrees) unfixed_tvars
  11.187 +    in (fixtyinsts, tfrees) end;
  11.188 +
  11.189 +
  11.190 +(* cross-instantiate the instantiations - ie for each instantiation
  11.191 +replace all occurances in other instantiations - no loops are possible
  11.192 +and thus only one-parsing of the instantiations is necessary. *)
  11.193 +fun cross_inst insts = 
  11.194 +    let 
  11.195 +      fun instL (ix, (ty,t)) = 
  11.196 +          map (fn (ix2,(ty2,t2)) => 
  11.197 +                  (ix2, (ty2,Term.subst_vars ([], [(ix, t)]) t2)));
  11.198 +
  11.199 +      fun cross_instL ([], l) = rev l
  11.200 +        | cross_instL ((ix, t) :: insts, l) = 
  11.201 +          cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l));
  11.202 +
  11.203 +    in cross_instL (insts, []) end;
  11.204 +
  11.205 +(* as above but for types -- I don't know if this is needed, will we ever incur mixed up types? *)
  11.206 +fun cross_inst_typs insts = 
  11.207 +    let 
  11.208 +      fun instL (ix, (srt,ty)) = 
  11.209 +          map (fn (ix2,(srt2,ty2)) => 
  11.210 +                  (ix2, (srt2,Term.typ_subst_TVars [(ix, ty)] ty2)));
  11.211 +
  11.212 +      fun cross_instL ([], l) = rev l
  11.213 +        | cross_instL ((ix, t) :: insts, l) = 
  11.214 +          cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l));
  11.215 +
  11.216 +    in cross_instL (insts, []) end;
  11.217 +
  11.218 +
  11.219 +(* assume that rule and target_thm have distinct var names. THINK:
  11.220 +efficient version with tables for vars for: target vars, introduced
  11.221 +vars, and rule vars, for quicker instantiation?  The outerterm defines
  11.222 +which part of the target_thm was modified.  Note: we take Ts in the
  11.223 +upterm order, ie last abstraction first., and with an outeterm where
  11.224 +the abstracted subterm has the arguments in the revered order, ie
  11.225 +first abstraction first.  FakeTs has abstractions using the fake name
  11.226 +- ie the name distinct from all other abstractions. *)
  11.227 +
  11.228 +fun rw ((nonfixed_typinsts, unprepinsts), FakeTs, Ts, outerterm) rule target_thm = 
  11.229 +    let 
  11.230 +      (* general signature info *)
  11.231 +      val target_sign = (Thm.theory_of_thm target_thm);
  11.232 +      val ctermify = Thm.cterm_of target_sign;
  11.233 +      val ctypeify = Thm.ctyp_of target_sign;
  11.234 +
  11.235 +      (* fix all non-instantiated tvars *)
  11.236 +      val (fixtyinsts, othertfrees) = 
  11.237 +          mk_fixtvar_tyinsts nonfixed_typinsts
  11.238 +                             [Thm.prop_of rule, Thm.prop_of target_thm];
  11.239 +      val new_fixed_typs = map (fn ((s,i),(srt,ty)) => (Term.dest_TFree ty))
  11.240 +                               fixtyinsts;
  11.241 +      val typinsts = cross_inst_typs (nonfixed_typinsts @ fixtyinsts);
  11.242 +
  11.243 +      (* certified instantiations for types *)
  11.244 +      val ctyp_insts = 
  11.245 +          map (fn (ix,(s,ty)) => (ctypeify (TVar (ix,s)), ctypeify ty)) 
  11.246 +              typinsts;
  11.247 +
  11.248 +      (* type instantiated versions *)
  11.249 +      val tgt_th_tyinst = Thm.instantiate (ctyp_insts,[]) target_thm;
  11.250 +      val rule_tyinst =  Thm.instantiate (ctyp_insts,[]) rule;
  11.251 +
  11.252 +      val term_typ_inst = map (fn (ix,(srt,ty)) => (ix,ty)) typinsts;
  11.253 +      (* type instanitated outer term *)
  11.254 +      val outerterm_tyinst = Term.subst_TVars term_typ_inst outerterm;
  11.255 +
  11.256 +      val FakeTs_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) 
  11.257 +                              FakeTs;
  11.258 +      val Ts_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst)) 
  11.259 +                          Ts;
  11.260 +
  11.261 +      (* type-instantiate the var instantiations *)
  11.262 +      val insts_tyinst = foldr (fn ((ix,(ty,t)),insts_tyinst) => 
  11.263 +                            (ix, (Term.typ_subst_TVars term_typ_inst ty, 
  11.264 +                                  Term.subst_TVars term_typ_inst t))
  11.265 +                            :: insts_tyinst)
  11.266 +                        [] unprepinsts;
  11.267 +
  11.268 +      (* cross-instantiate *)
  11.269 +      val insts_tyinst_inst = cross_inst insts_tyinst;
  11.270 +
  11.271 +      (* create certms of instantiations *)
  11.272 +      val cinsts_tyinst = 
  11.273 +          map (fn (ix,(ty,t)) => (ctermify (Var (ix, ty)), 
  11.274 +                                  ctermify t)) insts_tyinst_inst;
  11.275 +
  11.276 +      (* The instantiated rule *)
  11.277 +      val rule_inst = rule_tyinst |> Thm.instantiate ([], cinsts_tyinst);
  11.278 +
  11.279 +      (* Create a table of vars to be renamed after instantiation - ie
  11.280 +      other uninstantiated vars in the hyps the *instantiated* rule 
  11.281 +      ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *)
  11.282 +      val renamings = mk_renamings (Thm.prop_of tgt_th_tyinst) 
  11.283 +                                   rule_inst;
  11.284 +      val cterm_renamings = 
  11.285 +          map (fn (x,y) => (ctermify (Var x), ctermify y)) renamings;
  11.286 +
  11.287 +      (* Create the specific version of the rule for this target application *)
  11.288 +      val outerterm_inst = 
  11.289 +          outerterm_tyinst 
  11.290 +            |> Term.subst_Vars (map (fn (ix,(ty,t)) => (ix,t)) insts_tyinst_inst)
  11.291 +            |> Term.subst_Vars (map (fn ((ix,ty),t) => (ix,t)) renamings);
  11.292 +      val couter_inst = Thm.reflexive (ctermify outerterm_inst);
  11.293 +      val (cprems, abstract_rule_inst) = 
  11.294 +          rule_inst |> Thm.instantiate ([], cterm_renamings)
  11.295 +                    |> mk_abstractedrule FakeTs_tyinst Ts_tyinst;
  11.296 +      val specific_tgt_rule = 
  11.297 +          beta_eta_contract
  11.298 +            (Thm.combination couter_inst abstract_rule_inst);
  11.299 +
  11.300 +      (* create an instantiated version of the target thm *)
  11.301 +      val tgt_th_inst = 
  11.302 +          tgt_th_tyinst |> Thm.instantiate ([], cinsts_tyinst)
  11.303 +                        |> Thm.instantiate ([], cterm_renamings);
  11.304 +
  11.305 +      val (vars,frees_of_fixed_vars) = Library.split_list cterm_renamings;
  11.306 +
  11.307 +    in
  11.308 +      (beta_eta_contract tgt_th_inst)
  11.309 +        |> Thm.equal_elim specific_tgt_rule
  11.310 +        |> Drule.implies_intr_list cprems
  11.311 +        |> Drule.forall_intr_list frees_of_fixed_vars
  11.312 +        |> Drule.forall_elim_list vars
  11.313 +        |> Thm.varifyT' othertfrees
  11.314 +        |-> K Drule.zero_var_indexes
  11.315 +    end;
  11.316 +
  11.317 +
  11.318 +end; (* struct *)
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/Tools/IsaPlanner/rw_tools.ML	Thu May 31 20:55:29 2007 +0200
    12.3 @@ -0,0 +1,188 @@
    12.4 +(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
    12.5 +(*  Title:      Pure/IsaPlanner/rw_tools.ML
    12.6 +    ID:		$Id$
    12.7 +    Author:     Lucas Dixon, University of Edinburgh
    12.8 +                lucas.dixon@ed.ac.uk
    12.9 +    Created:    28 May 2004
   12.10 +*)
   12.11 +(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
   12.12 +(*  DESCRIPTION:
   12.13 +
   12.14 +    term related tools used for rewriting
   12.15 +
   12.16 +*)   
   12.17 +(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
   12.18 +
   12.19 +signature RWTOOLS =
   12.20 +sig
   12.21 +end;
   12.22 +
   12.23 +structure RWTools 
   12.24 += struct
   12.25 +
   12.26 +(* fake free variable names for locally bound variables - these work
   12.27 +as placeholders. *)
   12.28 +
   12.29 +(* don't use dest_fake.. - we should instead be working with numbers
   12.30 +and a list... else we rely on naming conventions which can break, or
   12.31 +be violated - in contrast list locations are correct by
   12.32 +construction/definition. *)
   12.33 +(*
   12.34 +fun dest_fake_bound_name n = 
   12.35 +    case (explode n) of 
   12.36 +      (":" :: realchars) => implode realchars
   12.37 +    | _ => n; *)
   12.38 +fun is_fake_bound_name n = (hd (explode n) = ":");
   12.39 +fun mk_fake_bound_name n = ":b_" ^ n;
   12.40 +
   12.41 +
   12.42 +
   12.43 +(* fake free variable names for local meta variables - these work
   12.44 +as placeholders. *)
   12.45 +fun dest_fake_fix_name n = 
   12.46 +    case (explode n) of 
   12.47 +      ("@" :: realchars) => implode realchars
   12.48 +    | _ => n;
   12.49 +fun is_fake_fix_name n = (hd (explode n) = "@");
   12.50 +fun mk_fake_fix_name n = "@" ^ n;
   12.51 +
   12.52 +
   12.53 +
   12.54 +(* fake free variable names for meta level bound variables *)
   12.55 +fun dest_fake_all_name n = 
   12.56 +    case (explode n) of 
   12.57 +      ("+" :: realchars) => implode realchars
   12.58 +    | _ => n;
   12.59 +fun is_fake_all_name n = (hd (explode n) = "+");
   12.60 +fun mk_fake_all_name n = "+" ^ n;
   12.61 +
   12.62 +
   12.63 +
   12.64 +
   12.65 +(* Ys and Ts not used, Ns are real names of faked local bounds, the
   12.66 +idea is that this will be mapped to free variables thus if a free
   12.67 +variable is a faked local bound then we change it to being a meta
   12.68 +variable so that it can later be instantiated *)
   12.69 +(* FIXME: rename this - avoid the word fix! *)
   12.70 +(* note we are not really "fix"'ing the free, more like making it variable! *)
   12.71 +(* fun trymkvar_of_fakefree (Ns, Ts) Ys (n,ty) = 
   12.72 +    if n mem Ns then Var((n,0),ty) else Free (n,ty);
   12.73 +*)
   12.74 +
   12.75 +(* make a var into a fixed free (ie prefixed with "@") *)
   12.76 +fun mk_fakefixvar Ts ((n,i),ty) = Free(mk_fake_fix_name n, ty);
   12.77 +
   12.78 +
   12.79 +(* mk_frees_bound: string list -> Term.term -> Term.term *)
   12.80 +(* This function changes free variables to being represented as bound
   12.81 +variables if the free's variable name is in the given list. The debruijn 
   12.82 +index is simply the position in the list *)
   12.83 +(* THINKABOUT: danger of an existing free variable with the same name: fix
   12.84 +this so that name conflict are avoided automatically! In the meantime,
   12.85 +don't have free variables named starting with a ":" *)
   12.86 +fun bounds_of_fakefrees Ys (a $ b) = 
   12.87 +    (bounds_of_fakefrees Ys a) $ (bounds_of_fakefrees Ys b)
   12.88 +  | bounds_of_fakefrees Ys (Abs(n,ty,t)) = 
   12.89 +    Abs(n,ty, bounds_of_fakefrees (n::Ys) t)
   12.90 +  | bounds_of_fakefrees Ys (Free (n,ty)) = 
   12.91 +    let fun try_mk_bound_of_free (i,[]) = Free (n,ty)
   12.92 +          | try_mk_bound_of_free (i,(y::ys)) = 
   12.93 +            if n = y then Bound i else try_mk_bound_of_free (i+1,ys)
   12.94 +    in try_mk_bound_of_free (0,Ys) end
   12.95 +  | bounds_of_fakefrees Ys t = t;
   12.96 +
   12.97 +
   12.98 +(* map a function f onto each free variables *)
   12.99 +fun map_to_frees f Ys (a $ b) = 
  12.100 +    (map_to_frees f Ys a) $ (map_to_frees f Ys b)
  12.101 +  | map_to_frees f Ys (Abs(n,ty,t)) = 
  12.102 +    Abs(n,ty, map_to_frees f ((n,ty)::Ys) t)
  12.103 +  | map_to_frees f Ys (Free a) = 
  12.104 +    f Ys a
  12.105 +  | map_to_frees f Ys t = t;
  12.106 +
  12.107 +
  12.108 +(* map a function f onto each meta variable  *)
  12.109 +fun map_to_vars f Ys (a $ b) = 
  12.110 +    (map_to_vars f Ys a) $ (map_to_vars f Ys b)
  12.111 +  | map_to_vars f Ys (Abs(n,ty,t)) = 
  12.112 +    Abs(n,ty, map_to_vars f ((n,ty)::Ys) t)
  12.113 +  | map_to_vars f Ys (Var a) = 
  12.114 +    f Ys a
  12.115 +  | map_to_vars f Ys t = t;
  12.116 +
  12.117 +(* map a function f onto each free variables *)
  12.118 +fun map_to_alls f (Const("all",allty) $ Abs(n,ty,t)) = 
  12.119 +    let val (n2,ty2) = f (n,ty) 
  12.120 +    in (Const("all",allty) $ Abs(n2,ty2,map_to_alls f t)) end
  12.121 +  | map_to_alls f x = x;
  12.122 +
  12.123 +(* map a function f to each type variable in a term *)
  12.124 +(* implicit arg: term *)
  12.125 +fun map_to_term_tvars f =
  12.126 +    Term.map_types (fn TVar(ix,ty) => f (ix,ty) | x => x);   (* FIXME map_atyps !? *)
  12.127 +
  12.128 +
  12.129 +
  12.130 +(* what if a param desn't occur in the concl? think about! Note: This
  12.131 +simply fixes meta level univ bound vars as Frees.  At the end, we will
  12.132 +change them back to schematic vars that will then unify
  12.133 +appropriactely, ie with unfake_vars *)
  12.134 +fun fake_concl_of_goal gt i = 
  12.135 +    let 
  12.136 +      val prems = Logic.strip_imp_prems gt
  12.137 +      val sgt = List.nth (prems, i - 1)
  12.138 +
  12.139 +      val tbody = Logic.strip_imp_concl (Term.strip_all_body sgt)
  12.140 +      val tparams = Term.strip_all_vars sgt
  12.141 +
  12.142 +      val fakefrees = map (fn (n, ty) => Free(mk_fake_all_name n, ty)) 
  12.143 +                          tparams
  12.144 +    in
  12.145 +      Term.subst_bounds (rev fakefrees,tbody)
  12.146 +    end;
  12.147 +
  12.148 +(* what if a param desn't occur in the concl? think about! Note: This
  12.149 +simply fixes meta level univ bound vars as Frees.  At the end, we will
  12.150 +change them back to schematic vars that will then unify
  12.151 +appropriactely, ie with unfake_vars *)
  12.152 +fun fake_goal gt i = 
  12.153 +    let 
  12.154 +      val prems = Logic.strip_imp_prems gt
  12.155 +      val sgt = List.nth (prems, i - 1)
  12.156 +
  12.157 +      val tbody = Term.strip_all_body sgt
  12.158 +      val tparams = Term.strip_all_vars sgt
  12.159 +
  12.160 +      val fakefrees = map (fn (n, ty) => Free(mk_fake_all_name n, ty)) 
  12.161 +                          tparams
  12.162 +    in
  12.163 +      Term.subst_bounds (rev fakefrees,tbody)
  12.164 +    end;
  12.165 +
  12.166 +
  12.167 +(* hand written - for some reason the Isabelle version in drule is broken!
  12.168 +Example? something to do with Bin Yangs examples? 
  12.169 + *)
  12.170 +fun rename_term_bvars ns (Abs(s,ty,t)) = 
  12.171 +    let val s2opt = Library.find_first (fn (x,y) => s = x) ns
  12.172 +    in case s2opt of 
  12.173 +         NONE => (Abs(s,ty,rename_term_bvars  ns t))
  12.174 +       | SOME (_,s2) => Abs(s2,ty, rename_term_bvars ns t) end
  12.175 +  | rename_term_bvars ns (a$b) = 
  12.176 +    (rename_term_bvars ns a) $ (rename_term_bvars ns b)
  12.177 +  | rename_term_bvars _ x = x;
  12.178 +
  12.179 +fun rename_thm_bvars ns th = 
  12.180 +    let val t = Thm.prop_of th 
  12.181 +    in Thm.rename_boundvars t (rename_term_bvars ns t) th end;
  12.182 +
  12.183 +(* Finish this to show how it breaks! (raises the exception): 
  12.184 +
  12.185 +exception rename_thm_bvars_exp of ((string * string) list * Thm.thm)
  12.186 +
  12.187 +    Drule.rename_bvars ns th 
  12.188 +    handle TERM _ => raise rename_thm_bvars_exp (ns, th); 
  12.189 +*)
  12.190 +
  12.191 +end;
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/Tools/IsaPlanner/zipper.ML	Thu May 31 20:55:29 2007 +0200
    13.3 @@ -0,0 +1,491 @@
    13.4 +(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
    13.5 +(*  Title:      Pure/IsaPlanner/zipper.ML
    13.6 +    ID:		$Id$
    13.7 +    Author:     Lucas Dixon, University of Edinburgh
    13.8 +                lucas.dixon@ed.ac.uk
    13.9 +    Created:    24 Mar 2006
   13.10 +*)
   13.11 +(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
   13.12 +(*  DESCRIPTION:
   13.13 +    A notion roughly based on Huet's Zippers for Isabelle terms.
   13.14 +*)   
   13.15 +
   13.16 +(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
   13.17 +
   13.18 +(* abstract term for no more than pattern matching *)
   13.19 +signature ABSTRACT_TRM = 
   13.20 +sig
   13.21 +type typ   (* types *)
   13.22 +type aname (* abstraction names *)
   13.23 +type fname (* parameter/free variable names *)
   13.24 +type cname (* constant names *)
   13.25 +type vname (* meta variable names *)
   13.26 +type bname (* bound var name *)
   13.27 +datatype term = Const of cname * typ
   13.28 +           | Abs of aname * typ * term
   13.29 +           | Free of fname * typ
   13.30 +           | Var of vname * typ
   13.31 +           | Bound of bname
   13.32 +           | $ of term * term;
   13.33 +type T = term;
   13.34 +end;
   13.35 +
   13.36 +structure IsabelleTrmWrap : ABSTRACT_TRM= 
   13.37 +struct 
   13.38 +open Term;
   13.39 +type typ   = Term.typ; (* types *)
   13.40 +type aname = string; (* abstraction names *)
   13.41 +type fname = string; (* parameter/free variable names *)
   13.42 +type cname = string; (* constant names *)
   13.43 +type vname = string * int; (* meta variable names *)
   13.44 +type bname = int; (* bound var name *)
   13.45 +type T = term;
   13.46 +end;
   13.47 +
   13.48 +(* Concrete version for the Trm structure *)
   13.49 +signature TRM_CTXT_DATA = 
   13.50 +sig
   13.51 +
   13.52 +  structure Trm : ABSTRACT_TRM
   13.53 +  datatype dtrm = Abs of Trm.aname * Trm.typ
   13.54 +                | AppL of Trm.T
   13.55 +                | AppR of Trm.T;
   13.56 +  val apply : dtrm -> Trm.T -> Trm.T
   13.57 +  val eq_pos : dtrm * dtrm -> bool
   13.58 +end;
   13.59 +
   13.60 +(* A trm context = list of derivatives *)
   13.61 +signature TRM_CTXT =
   13.62 +sig
   13.63 +  structure D : TRM_CTXT_DATA
   13.64 +  type T = D.dtrm list;
   13.65 +
   13.66 +  val empty : T;
   13.67 +  val is_empty : T -> bool;
   13.68 +
   13.69 +  val add_abs : D.Trm.aname * D.Trm.typ -> T -> T;
   13.70 +  val add_appl : D.Trm.T -> T -> T;
   13.71 +  val add_appr : D.Trm.T -> T -> T;
   13.72 +
   13.73 +  val add_dtrm : D.dtrm -> T -> T;
   13.74 +
   13.75 +  val eq_path : T * T -> bool
   13.76 +
   13.77 +  val add_outerctxt : T -> T -> T
   13.78 +
   13.79 +  val apply : T -> D.Trm.T -> D.Trm.T
   13.80 +
   13.81 +  val nty_ctxt : T -> (D.Trm.aname * D.Trm.typ) list;
   13.82 +  val ty_ctxt : T -> D.Trm.typ list;
   13.83 +
   13.84 +  val depth : T -> int;
   13.85 +  val map : (D.dtrm -> D.dtrm) -> T -> T
   13.86 +  val fold_up : (D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a
   13.87 +  val fold_down : (D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a
   13.88 +
   13.89 +end;
   13.90 +
   13.91 +(* A zipper = a term looked at, at a particular point in the term *)
   13.92 +signature ZIPPER =
   13.93 +sig
   13.94 +  structure C : TRM_CTXT
   13.95 +  type T
   13.96 +
   13.97 +  val mktop : C.D.Trm.T -> T
   13.98 +  val mk : (C.D.Trm.T * C.T) -> T
   13.99 +
  13.100 +  val goto_top : T -> T 
  13.101 +  val at_top : T -> bool
  13.102 +
  13.103 +  val split : T -> T * C.T
  13.104 +  val add_outerctxt : C.T -> T -> T
  13.105 +
  13.106 +  val set_trm : C.D.Trm.T -> T -> T
  13.107 +  val set_ctxt : C.T -> T -> T
  13.108 +
  13.109 +  val ctxt : T -> C.T
  13.110 +  val trm : T -> C.D.Trm.T
  13.111 +  val top_trm : T -> C.D.Trm.T
  13.112 +
  13.113 +  val zipto : C.T -> T -> T (* follow context down *)
  13.114 +
  13.115 +  val nty_ctxt : T -> (C.D.Trm.aname * C.D.Trm.typ) list;
  13.116 +  val ty_ctxt : T -> C.D.Trm.typ list;
  13.117 +
  13.118 +  val depth_of_ctxt : T -> int;
  13.119 +  val map_on_ctxt : (C.D.dtrm -> C.D.dtrm) -> T -> T
  13.120 +  val fold_up_ctxt : (C.D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a
  13.121 +  val fold_down_ctxt : (C.D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a
  13.122 +
  13.123 +  (* searching through a zipper *)
  13.124 +  datatype zsearch = Here of T | LookIn of T;
  13.125 +  (* lazily search through the zipper *)
  13.126 +  val lzy_search : (T -> zsearch list) -> T -> T Seq.seq
  13.127 +  (* lazy search with folded data *)
  13.128 +  val pf_lzy_search : ('a -> T -> ('a * zsearch list)) 
  13.129 +                      -> 'a -> T -> T Seq.seq
  13.130 +  (* zsearch list is or-choices *)
  13.131 +  val searchfold : ('a -> T -> (('a * zsearch) list)) 
  13.132 +                      -> 'a -> T -> ('a * T) Seq.seq
  13.133 +  (* limit function to the current focus of the zipper, 
  13.134 +     but give function the zipper's context *)
  13.135 +  val limit_pcapply : (C.T -> T -> ('a * T) Seq.seq) 
  13.136 +                      -> T -> ('a * T) Seq.seq
  13.137 +  val limit_apply : (T -> T Seq.seq) -> T -> T Seq.seq
  13.138 +  val limit_capply : (C.T -> T -> T Seq.seq) -> T -> T Seq.seq
  13.139 +
  13.140 +  (* moving around zippers with option types *)
  13.141 +  val omove_up : T -> T option
  13.142 +  val omove_up_abs : T -> T option
  13.143 +  val omove_up_app : T -> T option
  13.144 +  val omove_up_left : T -> T option
  13.145 +  val omove_up_right : T -> T option
  13.146 +  val omove_up_left_or_abs : T -> T option
  13.147 +  val omove_up_right_or_abs : T -> T option
  13.148 +  val omove_down_abs : T -> T option
  13.149 +  val omove_down_left : T -> T option
  13.150 +  val omove_down_right : T -> T option
  13.151 +  val omove_down_app : T -> (T * T) option
  13.152 +
  13.153 +  (* moving around zippers, raising exceptions *)
  13.154 +  exception move of string * T
  13.155 +  val move_up : T -> T
  13.156 +  val move_up_abs : T -> T
  13.157 +  val move_up_app : T -> T
  13.158 +  val move_up_left : T -> T
  13.159 +  val move_up_right : T -> T
  13.160 +  val move_up_left_or_abs : T -> T
  13.161 +  val move_up_right_or_abs : T -> T
  13.162 +  val move_down_abs : T -> T
  13.163 +  val move_down_left : T -> T
  13.164 +  val move_down_right : T -> T
  13.165 +  val move_down_app : T -> T * T
  13.166 +
  13.167 +end;
  13.168 +
  13.169 +
  13.170 +(* Zipper data for an generic trm *)
  13.171 +functor TrmCtxtDataFUN(Trm : ABSTRACT_TRM) 
  13.172 +: TRM_CTXT_DATA 
  13.173 += struct
  13.174 +  
  13.175 +  structure Trm = Trm;
  13.176 +
  13.177 +  (* a dtrm is, in McBridge-speak, a differentiated term. It represents
  13.178 +  the different ways a term can occur within its datatype constructors *)
  13.179 +  datatype dtrm = Abs of Trm.aname * Trm.typ
  13.180 +                | AppL of Trm.T
  13.181 +                | AppR of Trm.T;
  13.182 +
  13.183 +  (* apply a dtrm to a term, ie put the dtrm above it, building context *)
  13.184 +  fun apply (Abs (s,ty)) t = Trm.Abs (s,ty,t)
  13.185 +    | apply (AppL tl) tr = Trm.$ (tl, tr)
  13.186 +    | apply (AppR tr) tl = Trm.$ (tl, tr);
  13.187 +
  13.188 +  fun eq_pos (Abs _, Abs _) = true
  13.189 +    | eq_pos (AppL _, AppL _) = true
  13.190 +    | eq_pos (AppR _, AppR _) = true
  13.191 +    | eq_pos _ = false;
  13.192 +
  13.193 +end;
  13.194 +
  13.195 +
  13.196 +(* functor for making term contexts given term data *)
  13.197 +functor TrmCtxtFUN(D : TRM_CTXT_DATA) 
  13.198 + : TRM_CTXT =
  13.199 +struct 
  13.200 +  structure D = D;
  13.201 +
  13.202 +  type T = D.dtrm list;
  13.203 +
  13.204 +  val empty = [];
  13.205 +  val is_empty = List.null;
  13.206 +
  13.207 +  fun add_abs d l = (D.Abs d) :: l;
  13.208 +  fun add_appl d l = (D.AppL d) :: l;
  13.209 +  fun add_appr d l = (D.AppR d) :: l;
  13.210 +
  13.211 +  fun add_dtrm d l = d::l;
  13.212 +
  13.213 +  fun eq_path ([], []) = true
  13.214 +    | eq_path ([], _::_) = false
  13.215 +    | eq_path ( _::_, []) = false
  13.216 +    | eq_path (h::t, h2::t2) = 
  13.217 +      D.eq_pos(h,h2) andalso eq_path (t, t2);
  13.218 +
  13.219 +  (* add context to outside of existing context *) 
  13.220 +  fun add_outerctxt ctop cbottom = cbottom @ ctop; 
  13.221 +
  13.222 +  (* mkterm : zipper -> trm -> trm *)
  13.223 +  val apply = Basics.fold D.apply;
  13.224 +  
  13.225 +  (* named type context *)
  13.226 +  val nty_ctxt = List.foldr (fn (D.Abs nty,ntys) => nty::ntys
  13.227 +                             | (_,ntys) => ntys) [];
  13.228 +  (* type context *)
  13.229 +  val ty_ctxt = List.foldr (fn (D.Abs (_,ty),tys) => ty::tys
  13.230 +                           | (_,tys) => tys) [];
  13.231 +
  13.232 +  val depth = length : T -> int;
  13.233 +
  13.234 +  val map = List.map : (D.dtrm -> D.dtrm) -> T -> T
  13.235 +
  13.236 +  val fold_up = Basics.fold : (D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a;
  13.237 +  val fold_down = Basics.fold_rev : (D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a;
  13.238 +
  13.239 +end;
  13.240 +
  13.241 +(* zippers in terms of term contexts *)
  13.242 +functor ZipperFUN(C : TRM_CTXT) 
  13.243 + : ZIPPER
  13.244 += struct 
  13.245 +
  13.246 +  structure C = C;
  13.247 +  structure D = C.D;
  13.248 +  structure Trm = D.Trm;
  13.249 +
  13.250 +  type T = C.D.Trm.T * C.T;
  13.251 +
  13.252 +  fun mktop t = (t, C.empty) : T
  13.253 +
  13.254 +  val mk = I;
  13.255 +  fun set_trm x = apfst (K x);
  13.256 +  fun set_ctxt x = apsnd (K x);
  13.257 +
  13.258 +  fun goto_top (z as (t,c)) = 
  13.259 +      if C.is_empty c then z else (C.apply c t, C.empty);
  13.260 +
  13.261 +  fun at_top (_,c) = C.is_empty c;
  13.262 +
  13.263 +  fun split (t,c) = ((t,C.empty) : T, c : C.T) 
  13.264 +  fun add_outerctxt c (t,c2) = (t, C.add_outerctxt c c2) : T
  13.265 +
  13.266 +  val ctxt = snd;
  13.267 +  val trm = fst;
  13.268 +  val top_trm = trm o goto_top;
  13.269 +
  13.270 +  fun nty_ctxt x = C.nty_ctxt (ctxt x);
  13.271 +  fun ty_ctxt x = C.ty_ctxt (ctxt x);
  13.272 +
  13.273 +  fun depth_of_ctxt x = C.depth (ctxt x);
  13.274 +  fun map_on_ctxt x = apsnd (C.map x);
  13.275 +  fun fold_up_ctxt f = C.fold_up f o ctxt;
  13.276 +  fun fold_down_ctxt f = C.fold_down f o ctxt;
  13.277 +
  13.278 +  fun omove_up (t,(d::c)) = SOME (D.apply d t, c)
  13.279 +    | omove_up (z as (_,[])) = NONE;
  13.280 +  fun omove_up_abs (t,((D.Abs(n,ty))::c)) = SOME (Trm.Abs(n,ty,t), c)
  13.281 +    | omove_up_abs z = NONE;
  13.282 +  fun omove_up_app (t,(D.AppL tl)::c) = SOME(Trm.$(tl,t), c)
  13.283 +    | omove_up_app (t,(D.AppR tr)::c) = SOME(Trm.$(t,tr), c)
  13.284 +    | omove_up_app z = NONE;
  13.285 +  fun omove_up_left (t,(D.AppL tl)::c) = SOME(Trm.$(tl,t), c)
  13.286 +    | omove_up_left z = NONE;
  13.287 +  fun omove_up_right (t,(D.AppR tr)::c) = SOME(Trm.$(t,tr), c)
  13.288 +    | omove_up_right _ = NONE;
  13.289 +  fun omove_up_left_or_abs (t,(D.AppL tl)::c) = 
  13.290 +      SOME (Trm.$(tl,t), c)
  13.291 +    | omove_up_left_or_abs (t,(D.Abs (n,ty))::c) = 
  13.292 +      SOME (Trm.Abs(n,ty,t), c)
  13.293 +    | omove_up_left_or_abs z = NONE;
  13.294 +  fun omove_up_right_or_abs (t,(D.Abs (n,ty))::c) = 
  13.295 +      SOME (Trm.Abs(n,ty,t), c) 
  13.296 +    | omove_up_right_or_abs (t,(D.AppR tr)::c) = 
  13.297 +      SOME (Trm.$(t,tr), c)
  13.298 +    | omove_up_right_or_abs _ = NONE;
  13.299 +  fun omove_down_abs (Trm.Abs(s,ty,t),c) = SOME (t,(D.Abs(s,ty))::c)
  13.300 +    | omove_down_abs _ = NONE;
  13.301 +  fun omove_down_left (Trm.$(l,r),c) = SOME (l,(D.AppR r)::c)
  13.302 +    | omove_down_left _ = NONE;
  13.303 +  fun omove_down_right (Trm.$(l,r),c) = SOME (r,(D.AppL l)::c)
  13.304 +    | omove_down_right _ = NONE;
  13.305 +  fun omove_down_app (Trm.$(l,r),c) = 
  13.306 +      SOME ((l,(D.AppR r)::c),(r,(D.AppL l)::c))
  13.307 +    | omove_down_app _ = NONE;
  13.308 +
  13.309 +  exception move of string * T
  13.310 +  fun move_up (t,(d::c)) = (D.apply d t, c)
  13.311 +    | move_up (z as (_,[])) = raise move ("move_up",z);
  13.312 +  fun move_up_abs (t,((D.Abs(n,ty))::c)) = (Trm.Abs(n,ty,t), c)
  13.313 +    | move_up_abs z = raise move ("move_up_abs",z);
  13.314 +  fun move_up_app (t,(D.AppL tl)::c) = (Trm.$(tl,t), c)
  13.315 +    | move_up_app (t,(D.AppR tr)::c) = (Trm.$(t,tr), c)
  13.316 +    | move_up_app z = raise move ("move_up_app",z);
  13.317 +  fun move_up_left (t,((D.AppL tl)::c)) = (Trm.$(tl,t), c)
  13.318 +    | move_up_left z = raise move ("move_up_left",z);
  13.319 +  fun move_up_right (t,(D.AppR tr)::c) = (Trm.$(t,tr), c)
  13.320 +    | move_up_right z = raise move ("move_up_right",z);
  13.321 +  fun move_up_left_or_abs (t,(D.AppL tl)::c) = (Trm.$(tl,t), c)
  13.322 +    | move_up_left_or_abs (t,(D.Abs (n,ty))::c) = (Trm.Abs(n,ty,t), c)
  13.323 +    | move_up_left_or_abs z = raise move ("move_up_left_or_abs",z);
  13.324 +  fun move_up_right_or_abs (t,(D.Abs (n,ty))::c) = (Trm.Abs(n,ty,t), c) 
  13.325 +    | move_up_right_or_abs (t,(D.AppR tr)::c) = (Trm.$(t,tr), c)
  13.326 +    | move_up_right_or_abs z = raise move ("move_up_right_or_abs",z);
  13.327 +  fun move_down_abs (Trm.Abs(s,ty,t),c) = (t,(D.Abs(s,ty))::c)
  13.328 +    | move_down_abs z = raise move ("move_down_abs",z);
  13.329 +  fun move_down_left (Trm.$(l,r),c) = (l,(D.AppR r)::c)
  13.330 +    | move_down_left z = raise move ("move_down_left",z);
  13.331 +  fun move_down_right (Trm.$(l,r),c) = (r,(D.AppL l)::c)
  13.332 +    | move_down_right z = raise move ("move_down_right",z);
  13.333 +  fun move_down_app (Trm.$(l,r),c) = 
  13.334 +      ((l,(D.AppR r)::c),(r,(D.AppL l)::c))
  13.335 +    | move_down_app z = raise move ("move_down_app",z);
  13.336 +
  13.337 +  (* follow the given path down the given zipper *)
  13.338 +  (* implicit arguments: C.D.dtrm list, then T *)
  13.339 +  val zipto = C.fold_down 
  13.340 +                (fn C.D.Abs _ => move_down_abs 
  13.341 +                  | C.D.AppL _ => move_down_right
  13.342 +                  | C.D.AppR _ => move_down_left); 
  13.343 +
  13.344 +  (* Note: interpretted as being examined depth first *)
  13.345 +  datatype zsearch = Here of T | LookIn of T;
  13.346 +
  13.347 +  (* lazy search *)
  13.348 +  fun lzy_search fsearch = 
  13.349 +      let 
  13.350 +        fun lzyl [] () = NONE
  13.351 +          | lzyl ((Here z) :: more) () = SOME(z, Seq.make (lzyl more))
  13.352 +          | lzyl ((LookIn z) :: more) () =
  13.353 +            (case lzy z
  13.354 +              of NONE => NONE
  13.355 +               | SOME (hz,mz) => 
  13.356 +                 SOME (hz, Seq.append mz (Seq.make (lzyl more))))
  13.357 +        and lzy z = lzyl (fsearch z) ()
  13.358 +      in Seq.make o lzyl o fsearch end;
  13.359 +
  13.360 +  (* path folded lazy search - the search list is defined in terms of
  13.361 +  the path passed through: the data a is updated with every zipper
  13.362 +  considered *)
  13.363 +  fun pf_lzy_search fsearch a0 z = 
  13.364 +      let 
  13.365 +        fun lzyl a [] () = NONE
  13.366 +          | lzyl a ((Here z) :: more) () = SOME(z, Seq.make (lzyl a more))
  13.367 +          | lzyl a ((LookIn z) :: more) () =
  13.368 +            (case lzy a z
  13.369 +              of NONE => lzyl a more ()
  13.370 +               | SOME(hz,mz) => SOME(hz,Seq.append mz (Seq.make(lzyl a more))))
  13.371 +        and lzy a z = 
  13.372 +            let val (a2, slist) = (fsearch a z) in lzyl a2 slist () end
  13.373 +
  13.374 +        val (a,slist) = fsearch a0 z
  13.375 +      in Seq.make (lzyl a slist) end;
  13.376 +
  13.377 +  (* Note: depth first over zsearch results *)
  13.378 +  fun searchfold fsearch a0 z = 
  13.379 +      let 
  13.380 +        fun lzyl [] () = NONE
  13.381 +          | lzyl ((a, Here z) :: more) () = 
  13.382 +            SOME((a,z), Seq.make (lzyl more))
  13.383 +          | lzyl ((a, LookIn z) :: more) () =
  13.384 +            (case lzyl (fsearch a z) () of 
  13.385 +               NONE => lzyl more ()
  13.386 +             | SOME (z,mz) => SOME (z,Seq.append mz (Seq.make (lzyl more))))
  13.387 +      in Seq.make (lzyl (fsearch a0 z)) end;
  13.388 +
  13.389 +
  13.390 +  fun limit_pcapply f z = 
  13.391 +      let val (z2,c) = split z
  13.392 +      in Seq.map (apsnd (add_outerctxt c)) (f c z2) end;
  13.393 +  fun limit_capply (f : C.T -> T -> T Seq.seq) (z : T) = 
  13.394 +      let val ((z2 : T),(c : C.T)) = split z
  13.395 +      in Seq.map (add_outerctxt c) (f c z2) end
  13.396 +
  13.397 +  val limit_apply = limit_capply o K;
  13.398 +
  13.399 +end;
  13.400 +
  13.401 +(* now build these for Isabelle terms *)
  13.402 +structure TrmCtxtData = TrmCtxtDataFUN(IsabelleTrmWrap);
  13.403 +structure TrmCtxt = TrmCtxtFUN(TrmCtxtData);
  13.404 +structure Zipper = ZipperFUN(TrmCtxt);
  13.405 +
  13.406 +
  13.407 +
  13.408 +(* For searching through Zippers below the current focus...
  13.409 +   KEY for naming scheme:    
  13.410 +
  13.411 +   td = starting at the top down
  13.412 +   lr = going from left to right
  13.413 +   rl = going from right to left
  13.414 +
  13.415 +   bl = starting at the bottom left
  13.416 +   br = starting at the bottom right
  13.417 +   ul = going up then left
  13.418 +   ur = going up then right
  13.419 +   ru = going right then up
  13.420 +   lu = going left then up
  13.421 +*)
  13.422 +signature ZIPPER_SEARCH =
  13.423 +sig
  13.424 +  structure Z : ZIPPER;
  13.425 +  
  13.426 +  val leaves_lr : Z.T -> Z.T Seq.seq
  13.427 +  val leaves_rl : Z.T -> Z.T Seq.seq
  13.428 +
  13.429 +  val all_bl_ru : Z.T -> Z.T Seq.seq
  13.430 +  val all_bl_ur : Z.T -> Z.T Seq.seq
  13.431 +  val all_td_lr : Z.T -> Z.T Seq.seq
  13.432 +  val all_td_rl : Z.T -> Z.T Seq.seq
  13.433 +  
  13.434 +end;
  13.435 +
  13.436 +functor ZipperSearchFUN(Zipper : ZIPPER) : ZIPPER_SEARCH
  13.437 += struct
  13.438 +
  13.439 +structure Z = Zipper;
  13.440 +structure C = Z.C;
  13.441 +structure D = C.D; 
  13.442 +structure Trm = D.Trm; 
  13.443 +
  13.444 +fun sf_leaves_lr z = 
  13.445 +    case Z.trm z 
  13.446 +     of Trm.$ _ => [Z.LookIn (Z.move_down_left z),
  13.447 +                    Z.LookIn (Z.move_down_right z)]
  13.448 +      | Trm.Abs _ => [Z.LookIn (Z.move_down_abs z)]
  13.449 +      | _ => [Z.Here z];
  13.450 +fun sf_leaves_rl z = 
  13.451 +    case Z.trm z 
  13.452 +     of Trm.$ _ => [Z.LookIn (Z.move_down_right z),
  13.453 +                    Z.LookIn (Z.move_down_left z)]
  13.454 +      | Trm.Abs _ => [Z.LookIn (Z.move_down_abs z)]
  13.455 +      | _ => [Z.Here z];
  13.456 +val leaves_lr = Z.lzy_search sf_leaves_lr;
  13.457 +val leaves_rl = Z.lzy_search sf_leaves_rl;
  13.458 +
  13.459 +
  13.460 +fun sf_all_td_lr z = 
  13.461 +    case Z.trm z 
  13.462 +     of Trm.$ _ => [Z.Here z, Z.LookIn (Z.move_down_left z),
  13.463 +                    Z.LookIn (Z.move_down_right z)]
  13.464 +      | Trm.Abs _ => [Z.Here z, Z.LookIn (Z.move_down_abs z)]
  13.465 +      | _ => [Z.Here z];
  13.466 +fun sf_all_td_rl z = 
  13.467 +    case Z.trm z 
  13.468 +     of Trm.$ _ => [Z.Here z, Z.LookIn (Z.move_down_right z),
  13.469 +                    Z.LookIn (Z.move_down_left z)]
  13.470 +      | Trm.Abs _ => [Z.Here z, Z.LookIn (Z.move_down_abs z)]
  13.471 +      | _ => [Z.Here z];
  13.472 +fun sf_all_bl_ur z = 
  13.473 +    case Z.trm z 
  13.474 +     of Trm.$ _ => [Z.LookIn (Z.move_down_left z), Z.Here z,
  13.475 +                    Z.LookIn (Z.move_down_right z)]
  13.476 +      | Trm.Abs _ => [Z.LookIn (Z.move_down_abs z),
  13.477 +                      Z.Here z]
  13.478 +      | _ => [Z.Here z];
  13.479 +fun sf_all_bl_ru z = 
  13.480 +    case Z.trm z 
  13.481 +     of Trm.$ _ => [Z.LookIn (Z.move_down_left z),
  13.482 +                    Z.LookIn (Z.move_down_right z), Z.Here z]
  13.483 +      | Trm.Abs _ => [Z.LookIn (Z.move_down_abs z), Z.Here z]
  13.484 +      | _ => [Z.Here z];
  13.485 +
  13.486 +val all_td_lr = Z.lzy_search sf_all_td_lr;
  13.487 +val all_td_rl = Z.lzy_search sf_all_td_rl;
  13.488 +val all_bl_ur = Z.lzy_search sf_all_bl_ru;
  13.489 +val all_bl_ru = Z.lzy_search sf_all_bl_ur;
  13.490 +
  13.491 +end;
  13.492 +
  13.493 +
  13.494 +structure ZipperSearch = ZipperSearchFUN(Zipper);