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