added updated version of IsaPlanner and substitution.
--- a/src/FOL/ROOT.ML Fri Jun 09 17:32:38 2006 +0200
+++ b/src/FOL/ROOT.ML Sun Jun 11 00:28:18 2006 +0200
@@ -11,6 +11,10 @@
use "~~/src/Provers/splitter.ML";
use "~~/src/Provers/ind.ML";
use "~~/src/Provers/hypsubst.ML";
+use "~~/src/Provers/IsaPlanner/zipper.ML";
+use "~~/src/Provers/IsaPlanner/isand.ML";
+use "~~/src/Provers/IsaPlanner/rw_tools.ML";
+use "~~/src/Provers/IsaPlanner/rw_inst.ML";
use "~~/src/Provers/eqsubst.ML";
use "~~/src/Provers/induct_method.ML";
use "~~/src/Provers/classical.ML";
--- a/src/HOL/ROOT.ML Fri Jun 09 17:32:38 2006 +0200
+++ b/src/HOL/ROOT.ML Sun Jun 11 00:28:18 2006 +0200
@@ -13,6 +13,10 @@
use "~~/src/Provers/splitter.ML";
use "~~/src/Provers/hypsubst.ML";
+use "~~/src/Provers/IsaPlanner/zipper.ML";
+use "~~/src/Provers/IsaPlanner/isand.ML";
+use "~~/src/Provers/IsaPlanner/rw_tools.ML";
+use "~~/src/Provers/IsaPlanner/rw_inst.ML";
use "~~/src/Provers/eqsubst.ML";
use "~~/src/Provers/induct_method.ML";
use "~~/src/Provers/classical.ML";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Provers/IsaPlanner/ROOT.ML Sun Jun 11 00:28:18 2006 +0200
@@ -0,0 +1,16 @@
+(* ID: $Id$
+ Author: Lucas Dixon, University of Edinburgh
+ lucas.dixon@ed.ac.uk
+
+The IsaPlanner subsystem.
+*)
+
+(* Generic notion of term Zippers *)
+use "zipper.ML";
+
+(* Some tools for manipulation of proofs following a ND style *)
+use "isand.ML";
+
+(* some tools for rewriting *)
+use "rw_tools.ML";
+use "rw_inst.ML";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Provers/IsaPlanner/isand.ML Sun Jun 11 00:28:18 2006 +0200
@@ -0,0 +1,649 @@
+(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
+(* Title: Pure/IsaPlanner/isand.ML
+ ID: $Id$
+ Author: Lucas Dixon, University of Edinburgh
+ lucas.dixon@ed.ac.uk
+ Updated: 26 Apr 2005
+ Date: 6 Aug 2004
+*)
+(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
+(* DESCRIPTION:
+
+ Natural Deduction tools
+
+ For working with Isabelle theorems in a natural detuction style.
+ ie, not having to deal with meta level quantified varaibles,
+ instead, we work with newly introduced frees, and hide the
+ "all"'s, exporting results from theorems proved with the frees, to
+ solve the all cases of the previous goal. This allows resolution
+ to do proof search normally.
+
+ Note: A nice idea: allow exporting to solve any subgoal, thus
+ allowing the interleaving of proof, or provide a structure for the
+ ordering of proof, thus allowing proof attempts in parrell, but
+ recording the order to apply things in.
+
+ debugging tools:
+
+ fun asm_mk t = (assume (cterm_of (Theory.sign_of (the_context())) t));
+ fun asm_read s =
+ (assume (read_cterm (Theory.sign_of (Context.the_context())) (s,propT)));
+
+ THINK: are we really ok with our varify name w.r.t the prop - do
+ we also need to avoid names in the hidden hyps? What about
+ unification contraints in flex-flex pairs - might they also have
+ extra free vars?
+*)
+
+signature ISA_ND =
+sig
+
+ (* export data *)
+ datatype export = export of
+ {gth: Thm.thm, (* initial goal theorem *)
+ sgid: int, (* subgoal id which has been fixed etc *)
+ fixes: Thm.cterm list, (* frees *)
+ assumes: Thm.cterm list} (* assumptions *)
+ val fixes_of_exp : export -> Thm.cterm list
+ val export_back : export -> Thm.thm -> Thm.thm Seq.seq
+ val export_solution : export -> Thm.thm -> Thm.thm
+ val export_solutions : export list * Thm.thm -> Thm.thm
+
+ (* inserting meta level params for frees in the conditions *)
+ val allify_conditions :
+ (Term.term -> Thm.cterm) ->
+ (string * Term.typ) list -> Thm.thm -> Thm.thm * Thm.cterm list
+ val allify_conditions' :
+ (string * Term.typ) list -> Thm.thm -> Thm.thm * Thm.cterm list
+ val assume_allified :
+ theory -> (string * Term.sort) list * (string * Term.typ) list
+ -> Term.term -> (Thm.cterm * Thm.thm)
+
+ (* meta level fixed params (i.e. !! vars) *)
+ val fix_alls_in_term : Term.term -> Term.term * Term.term list
+ val fix_alls_term : int -> Term.term -> Term.term * Term.term list
+ val fix_alls_cterm : int -> Thm.thm -> Thm.cterm * Thm.cterm list
+ val fix_alls' : int -> Thm.thm -> Thm.thm * Thm.cterm list
+ val fix_alls : int -> Thm.thm -> Thm.thm * export
+
+ (* meta variables in types and terms *)
+ val fix_tvars_to_tfrees_in_terms
+ : string list (* avoid these names *)
+ -> Term.term list ->
+ (((string * int) * Term.sort) * (string * Term.sort)) list (* renamings *)
+ val fix_vars_to_frees_in_terms
+ : string list (* avoid these names *)
+ -> Term.term list ->
+ (((string * int) * Term.typ) * (string * Term.typ)) list (* renamings *)
+ val fix_tvars_to_tfrees : Thm.thm -> Thm.ctyp list * Thm.thm
+ val fix_vars_to_frees : Thm.thm -> Thm.cterm list * Thm.thm
+ val fix_vars_and_tvars :
+ Thm.thm -> (Thm.cterm list * Thm.ctyp list) * Thm.thm
+ val fix_vars_upto_idx : int -> Thm.thm -> Thm.thm
+ val fix_tvars_upto_idx : int -> Thm.thm -> Thm.thm
+ val unfix_frees : Thm.cterm list -> Thm.thm -> Thm.thm
+ val unfix_tfrees : Thm.ctyp list -> Thm.thm -> Thm.thm
+ val unfix_frees_and_tfrees :
+ (Thm.cterm list * Thm.ctyp list) -> Thm.thm -> Thm.thm
+
+ (* assumptions/subgoals *)
+ val assume_prems :
+ int -> Thm.thm -> Thm.thm list * Thm.thm * Thm.cterm list
+ val fixed_subgoal_thms : Thm.thm -> Thm.thm list * (Thm.thm list -> Thm.thm)
+ val fixes_and_assumes : int -> Thm.thm -> Thm.thm list * Thm.thm * export
+ val hide_other_goals : Thm.thm -> Thm.thm * Thm.cterm list
+ val hide_prems : Thm.thm -> Thm.thm * Thm.cterm list
+
+ (* abstracts cterms (vars) to locally meta-all bounds *)
+ val prepare_goal_export : string list * Thm.cterm list -> Thm.thm
+ -> int * Thm.thm
+ val solve_with : Thm.thm -> Thm.thm -> Thm.thm Seq.seq
+ val subgoal_thms : Thm.thm -> Thm.thm list * (Thm.thm list -> Thm.thm)
+end
+
+
+structure IsaND
+: ISA_ND
+= struct
+
+(* Solve *some* subgoal of "th" directly by "sol" *)
+(* Note: this is probably what Markus ment to do upon export of a
+"show" but maybe he used RS/rtac instead, which would wrongly lead to
+failing if there are premices to the shown goal.
+
+given:
+sol : Thm.thm = [| Ai... |] ==> Ci
+th : Thm.thm =
+ [| ... [| Ai... |] ==> Ci ... |] ==> G
+results in:
+ [| ... [| Ai-1... |] ==> Ci-1
+ [| Ai+1... |] ==> Ci+1 ...
+ |] ==> G
+i.e. solves some subgoal of th that is identical to sol.
+*)
+fun solve_with sol th =
+ let fun solvei 0 = Seq.empty
+ | solvei i =
+ Seq.append (bicompose false (false,sol,0) i th,
+ solvei (i - 1))
+ in
+ solvei (Thm.nprems_of th)
+ end;
+
+
+(* Given ctertmify function, (string,type) pairs capturing the free
+vars that need to be allified in the assumption, and a theorem with
+assumptions possibly containing the free vars, then we give back the
+assumptions allified as hidden hyps.
+
+Given: x
+th: A vs ==> B vs
+Results in: "B vs" [!!x. A x]
+*)
+fun allify_conditions ctermify Ts th =
+ let
+ val premts = Thm.prems_of th;
+
+ fun allify_prem_var (vt as (n,ty),t) =
+ (Term.all ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
+
+ fun allify_prem Ts p = foldr allify_prem_var p Ts
+
+ val cTs = map (ctermify o Free) Ts
+ val cterm_asms = map (ctermify o allify_prem Ts) premts
+ val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms
+ in
+ (Library.foldl (fn (x,y) => y COMP x) (th, allifyied_asm_thms), cterm_asms)
+ end;
+
+fun allify_conditions' Ts th =
+ allify_conditions (Thm.cterm_of (Thm.sign_of_thm th)) Ts th;
+
+(* allify types *)
+fun allify_typ ts ty =
+ let
+ fun trec (x as (TFree (s,srt))) =
+ (case Library.find_first (fn (s2,srt2) => s = s2) ts
+ of NONE => x
+ | SOME (s2,_) => TVar ((s,0),srt))
+ (* Maybe add in check here for bad sorts?
+ if srt = srt2 then TVar ((s,0),srt)
+ else raise ("thaw_typ", ts, ty) *)
+ | trec (Type (s,typs)) = Type (s, map trec typs)
+ | trec (v as TVar _) = v;
+ in trec ty end;
+
+(* implicit types and term *)
+fun allify_term_typs ty = Term.map_term_types (allify_typ ty);
+
+(* allified version of term, given frees to allify over. Note that we
+only allify over the types on the given allified cterm, we can't do
+this for the theorem as we are not allowed type-vars in the hyp. *)
+(* FIXME: make the allified term keep the same conclusion as it
+started with, rather than a strictly more general version (ie use
+instantiate with initial params we abstracted from, rather than
+forall_elim_vars. *)
+fun assume_allified sgn (tyvs,vs) t =
+ let
+ fun allify_var (vt as (n,ty),t) =
+ (Term.all ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
+ fun allify Ts p = List.foldr allify_var p Ts
+
+ val ctermify = Thm.cterm_of sgn;
+ val cvars = map (fn (n,ty) => ctermify (Var ((n,0),ty))) vs
+ val allified_term = t |> allify vs;
+ val ct = ctermify allified_term;
+ val typ_allified_ct = ctermify (allify_term_typs tyvs allified_term);
+ in (typ_allified_ct,
+ Drule.forall_elim_vars 0 (Thm.assume ct)) end;
+
+
+(* change type-vars to fresh type frees *)
+fun fix_tvars_to_tfrees_in_terms names ts =
+ let
+ val tfree_names = map fst (List.foldr Term.add_term_tfrees [] ts);
+ val tvars = List.foldr Term.add_term_tvars [] ts;
+ val (names',renamings) =
+ List.foldr (fn (tv as ((n,i),s),(Ns,Rs)) =>
+ let val n2 = Term.variant Ns n in
+ (n2::Ns, (tv, (n2,s))::Rs)
+ end) (tfree_names @ names,[]) tvars;
+ in renamings end;
+fun fix_tvars_to_tfrees th =
+ let
+ val sign = Thm.sign_of_thm th;
+ val ctypify = Thm.ctyp_of sign;
+ val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
+ val renamings = fix_tvars_to_tfrees_in_terms
+ [] ((Thm.prop_of th) :: tpairs);
+ val crenamings =
+ map (fn (v,f) => (ctypify (TVar v), ctypify (TFree f)))
+ renamings;
+ val fixedfrees = map snd crenamings;
+ in (fixedfrees, Thm.instantiate (crenamings, []) th) end;
+
+
+(* change type-free's to type-vars in th, skipping the ones in "ns" *)
+fun unfix_tfrees ns th =
+ let
+ val varfiytfrees = map (Term.dest_TFree o Thm.typ_of) ns
+ val skiptfrees = subtract (op =) varfiytfrees (Term.add_term_tfrees (Thm.prop_of th,[]));
+ in #2 (Thm.varifyT' skiptfrees th) end;
+
+(* change schematic/meta vars to fresh free vars, avoiding name clashes
+ with "names" *)
+fun fix_vars_to_frees_in_terms names ts =
+ let
+ val vars = map Term.dest_Var (List.foldr Term.add_term_vars [] ts);
+ val Ns = List.foldr Term.add_term_names names ts;
+ val (_,renamings) =
+ Library.foldl (fn ((Ns,Rs),v as ((n,i),ty)) =>
+ let val n2 = Term.variant Ns n in
+ (n2 :: Ns, (v, (n2,ty)) :: Rs)
+ end) ((Ns,[]), vars);
+ in renamings end;
+fun fix_vars_to_frees th =
+ let
+ val ctermify = Thm.cterm_of (Thm.sign_of_thm th)
+ val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
+ val renamings = fix_vars_to_frees_in_terms
+ [] ([Thm.prop_of th] @ tpairs);
+ val crenamings =
+ map (fn (v,f) => (ctermify (Var v), ctermify (Free f)))
+ renamings;
+ val fixedfrees = map snd crenamings;
+ in (fixedfrees, Thm.instantiate ([], crenamings) th) end;
+
+fun fix_tvars_upto_idx ix th =
+ let
+ val sgn = Thm.sign_of_thm th;
+ val ctypify = Thm.ctyp_of sgn
+ val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
+ val prop = (Thm.prop_of th);
+ val tvars = List.foldr Term.add_term_tvars [] (prop :: tpairs);
+ val ctyfixes =
+ map_filter
+ (fn (v as ((s,i),ty)) =>
+ if i <= ix then SOME (ctypify (TVar v), ctypify (TFree (s,ty)))
+ else NONE) tvars;
+ in Thm.instantiate (ctyfixes, []) th end;
+fun fix_vars_upto_idx ix th =
+ let
+ val sgn = Thm.sign_of_thm th;
+ val ctermify = Thm.cterm_of sgn
+ val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
+ val prop = (Thm.prop_of th);
+ val vars = map Term.dest_Var (List.foldr Term.add_term_vars
+ [] (prop :: tpairs));
+ val cfixes =
+ map_filter
+ (fn (v as ((s,i),ty)) =>
+ if i <= ix then SOME (ctermify (Var v), ctermify (Free (s,ty)))
+ else NONE) vars;
+ in Thm.instantiate ([], cfixes) th end;
+
+
+(* make free vars into schematic vars with index zero *)
+ fun unfix_frees frees =
+ apply (map (K (Drule.forall_elim_var 0)) frees)
+ o Drule.forall_intr_list frees;
+
+(* fix term and type variables *)
+fun fix_vars_and_tvars th =
+ let val (tvars, th') = fix_tvars_to_tfrees th
+ val (vars, th'') = fix_vars_to_frees th'
+ in ((vars, tvars), th'') end;
+
+(* implicit Thm.thm argument *)
+(* assumes: vars may contain fixed versions of the frees *)
+(* THINK: what if vs already has types varified? *)
+fun unfix_frees_and_tfrees (vs,tvs) =
+ (unfix_tfrees tvs o unfix_frees vs);
+
+(* datatype to capture an exported result, ie a fix or assume. *)
+datatype export =
+ export of {fixes : Thm.cterm list, (* fixed vars *)
+ assumes : Thm.cterm list, (* hidden hyps/assumed prems *)
+ sgid : int,
+ gth : Thm.thm}; (* subgoal/goalthm *)
+
+fun fixes_of_exp (export rep) = #fixes rep;
+
+(* export the result of the new goal thm, ie if we reduced teh
+subgoal, then we get a new reduced subtgoal with the old
+all-quantified variables *)
+local
+
+(* allify puts in a meta level univ quantifier for a free variavble *)
+fun allify_term (v, t) =
+ let val vt = #t (Thm.rep_cterm v)
+ val (n,ty) = Term.dest_Free vt
+ in (Term.all ty) $ (Abs(n,ty,Term.abstract_over (vt, t))) end;
+
+fun allify_for_sg_term ctermify vs t =
+ let val t_alls = foldr allify_term t vs;
+ val ct_alls = ctermify t_alls;
+ in
+ (ct_alls, Drule.forall_elim_list vs (Thm.assume ct_alls))
+ end;
+(* lookup type of a free var name from a list *)
+fun lookupfree vs vn =
+ case Library.find_first (fn (n,ty) => n = vn) vs of
+ NONE => error ("prepare_goal_export:lookupfree: " ^ vn ^ " does not occur in the term")
+ | SOME x => x;
+in
+fun export_back (export {fixes = vs, assumes = hprems,
+ sgid = i, gth = gth}) newth =
+ let
+ val sgn = Thm.sign_of_thm newth;
+ val ctermify = Thm.cterm_of sgn;
+
+ val sgs = prems_of newth;
+ val (sgallcts, sgthms) =
+ Library.split_list (map (allify_for_sg_term ctermify vs) sgs);
+ val minimal_newth =
+ (Library.foldl (fn ( newth', sgthm) =>
+ Drule.compose_single (sgthm, 1, newth'))
+ (newth, sgthms));
+ val allified_newth =
+ minimal_newth
+ |> Drule.implies_intr_list hprems
+ |> Drule.forall_intr_list vs
+
+ val newth' = Drule.implies_intr_list sgallcts allified_newth
+ in
+ bicompose false (false, newth', (length sgallcts)) i gth
+ end;
+
+(*
+Given "vs" : names of free variables to abstract over,
+Given cterms : premices to abstract over (P1... Pn) in terms of vs,
+Given a thm of the form:
+P1 vs; ...; Pn vs ==> Goal(C vs)
+
+Gives back:
+(n, length of given cterms which have been allified
+ [| !! vs. P1 vs; !! vs. Pn vs |] ==> !! C vs) the allified thm
+*)
+(* note: C may contain further premices etc
+Note that cterms is the assumed facts, ie prems of "P1" that are
+reintroduced in allified form.
+*)
+fun prepare_goal_export (vs, cterms) th =
+ let
+ val sgn = Thm.sign_of_thm th;
+ val ctermify = Thm.cterm_of sgn;
+
+ val allfrees = map Term.dest_Free (Term.term_frees (Thm.prop_of th))
+ val cfrees = map (ctermify o Free o lookupfree allfrees) vs
+
+ val sgs = prems_of th;
+ val (sgallcts, sgthms) =
+ Library.split_list (map (allify_for_sg_term ctermify cfrees) sgs);
+
+ val minimal_th =
+ Goal.conclude (Library.foldl (fn ( th', sgthm) =>
+ Drule.compose_single (sgthm, 1, th'))
+ (th, sgthms));
+
+ val allified_th =
+ minimal_th
+ |> Drule.implies_intr_list cterms
+ |> Drule.forall_intr_list cfrees
+
+ val th' = Drule.implies_intr_list sgallcts allified_th
+ in
+ ((length sgallcts), th')
+ end;
+
+end;
+
+
+(* exporting function that takes a solution to the fixed/assumed goal,
+and uses this to solve the subgoal in the main theorem *)
+fun export_solution (export {fixes = cfvs, assumes = hcprems,
+ sgid = i, gth = gth}) solth =
+ let
+ val solth' =
+ solth |> Drule.implies_intr_list hcprems
+ |> Drule.forall_intr_list cfvs
+ in Drule.compose_single (solth', i, gth) end;
+
+fun export_solutions (xs,th) = foldr (uncurry export_solution) th xs;
+
+
+(* fix parameters of a subgoal "i", as free variables, and create an
+exporting function that will use the result of this proved goal to
+show the goal in the original theorem.
+
+Note, an advantage of this over Isar is that it supports instantiation
+of unkowns in the earlier theorem, ie we can do instantiation of meta
+vars!
+
+avoids constant, free and vars names.
+
+loosely corresponds to:
+Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm
+Result:
+ ("(As ==> SGi x') ==> (As ==> SGi x')" : thm,
+ expf :
+ ("As ==> SGi x'" : thm) ->
+ ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm)
+*)
+fun fix_alls_in_term alledt =
+ let
+ val t = Term.strip_all_body alledt;
+ val alls = rev (Term.strip_all_vars alledt);
+ val varnames = map (fst o fst o Term.dest_Var) (Term.term_vars t)
+ val names = Term.add_term_names (t,varnames);
+ val fvs = map Free
+ ((Term.variantlist (map fst alls, names))
+ ~~ (map snd alls));
+ in ((subst_bounds (fvs,t)), fvs) end;
+
+fun fix_alls_term i t =
+ let
+ val varnames = map (fst o fst o Term.dest_Var) (Term.term_vars t)
+ val names = Term.add_term_names (t,varnames);
+ val gt = Logic.get_goal t i;
+ val body = Term.strip_all_body gt;
+ val alls = rev (Term.strip_all_vars gt);
+ val fvs = map Free
+ ((Term.variantlist (map fst alls, names))
+ ~~ (map snd alls));
+ in ((subst_bounds (fvs,body)), fvs) end;
+
+fun fix_alls_cterm i th =
+ let
+ val ctermify = Thm.cterm_of (Thm.sign_of_thm th);
+ val (fixedbody, fvs) = fix_alls_term i (Thm.prop_of th);
+ val cfvs = rev (map ctermify fvs);
+ val ct_body = ctermify fixedbody
+ in
+ (ct_body, cfvs)
+ end;
+
+fun fix_alls' i =
+ (apfst Thm.trivial) o (fix_alls_cterm i);
+
+
+(* hide other goals *)
+(* note the export goal is rotated by (i - 1) and will have to be
+unrotated to get backto the originial position(s) *)
+fun hide_other_goals th =
+ let
+ (* tl beacuse fst sg is the goal we are interested in *)
+ val cprems = tl (Drule.cprems_of th)
+ val aprems = map Thm.assume cprems
+ in
+ (Drule.implies_elim_list (Drule.rotate_prems 1 th) aprems,
+ cprems)
+ end;
+
+(* a nicer version of the above that leaves only a single subgoal (the
+other subgoals are hidden hyps, that the exporter suffles about)
+namely the subgoal that we were trying to solve. *)
+(* loosely corresponds to:
+Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm
+Result:
+ ("(As ==> SGi x') ==> SGi x'" : thm,
+ expf :
+ ("SGi x'" : thm) ->
+ ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm)
+*)
+fun fix_alls i th =
+ let
+ val (fixed_gth, fixedvars) = fix_alls' i th
+ val (sml_gth, othergoals) = hide_other_goals fixed_gth
+ in
+ (sml_gth, export {fixes = fixedvars,
+ assumes = othergoals,
+ sgid = i, gth = th})
+ end;
+
+
+(* assume the premises of subgoal "i", this gives back a list of
+assumed theorems that are the premices of subgoal i, it also gives
+back a new goal thm and an exporter, the new goalthm is as the old
+one, but without the premices, and the exporter will use a proof of
+the new goalthm, possibly using the assumed premices, to shoe the
+orginial goal.
+
+Note: Dealing with meta vars, need to meta-level-all them in the
+shyps, which we can later instantiate with a specific value.... ?
+think about this... maybe need to introduce some new fixed vars and
+then remove them again at the end... like I do with rw_inst.
+
+loosely corresponds to:
+Given "[| SG0; ... [| A0; ... An |] ==> SGi; ... SGm |] ==> G" : thm
+Result:
+(["A0" [A0], ... ,"An" [An]] : thm list, -- assumptions
+ "SGi ==> SGi" : thm, -- new goal
+ "SGi" ["A0" ... "An"] : thm -> -- export function
+ ("[| SG0 ... SGi-1, SGi+1, SGm |] ==> G" : thm) list)
+*)
+fun assume_prems i th =
+ let
+ val t = (prop_of th);
+ val gt = Logic.get_goal t i;
+ val _ = case Term.strip_all_vars gt of [] => ()
+ | _ => error "assume_prems: goal has params"
+ val body = gt;
+ val prems = Logic.strip_imp_prems body;
+ val concl = Logic.strip_imp_concl body;
+
+ val sgn = Thm.sign_of_thm th;
+ val ctermify = Thm.cterm_of sgn;
+ val cprems = map ctermify prems;
+ val aprems = map Thm.assume cprems;
+ val gthi = Thm.trivial (ctermify concl);
+
+ (* fun explortf thi =
+ Drule.compose (Drule.implies_intr_list cprems thi,
+ i, th) *)
+ in
+ (aprems, gthi, cprems)
+ end;
+
+
+(* first fix the variables, then assume the assumptions *)
+(* loosely corresponds to:
+Given
+ "[| SG0; ...
+ !! xs. [| A0 xs; ... An xs |] ==> SGi xs;
+ ... SGm |] ==> G" : thm
+Result:
+(["A0 xs'" [A0 xs'], ... ,"An xs'" [An xs']] : thm list, -- assumptions
+ "SGi xs' ==> SGi xs'" : thm, -- new goal
+ "SGi xs'" ["A0 xs'" ... "An xs'"] : thm -> -- export function
+ ("[| SG0 ... SGi-1, SGi+1, SGm |] ==> G" : thm) list)
+*)
+
+(* Note: the fix_alls actually pulls through all the assumptions which
+means that the second export is not needed. *)
+fun fixes_and_assumes i th =
+ let
+ val (fixgth, exp1) = fix_alls i th
+ val (assumps, goalth, _) = assume_prems 1 fixgth
+ in
+ (assumps, goalth, exp1)
+ end;
+
+
+(* Fixme: allow different order of subgoals given to expf *)
+(* make each subgoal into a separate thm that needs to be proved *)
+(* loosely corresponds to:
+Given
+ "[| SG0; ... SGm |] ==> G" : thm
+Result:
+(["SG0 ==> SG0", ... ,"SGm ==> SGm"] : thm list, -- goals
+ ["SG0", ..., "SGm"] : thm list -> -- export function
+ "G" : thm)
+*)
+fun subgoal_thms th =
+ let
+ val t = (prop_of th);
+
+ val prems = Logic.strip_imp_prems t;
+
+ val sgn = Thm.sign_of_thm th;
+ val ctermify = Thm.cterm_of sgn;
+
+ val aprems = map (Thm.trivial o ctermify) prems;
+
+ fun explortf premths =
+ Drule.implies_elim_list th premths
+ in
+ (aprems, explortf)
+ end;
+
+
+(* make all the premices of a theorem hidden, and provide an unhide
+function, that will bring them back out at a later point. This is
+useful if you want to get back these premices, after having used the
+theorem with the premices hidden *)
+(* loosely corresponds to:
+Given "As ==> G" : thm
+Result: ("G [As]" : thm,
+ "G [As]" : thm -> "As ==> G" : thm
+*)
+fun hide_prems th =
+ let
+ val cprems = Drule.cprems_of th;
+ val aprems = map Thm.assume cprems;
+ (* val unhidef = Drule.implies_intr_list cprems; *)
+ in
+ (Drule.implies_elim_list th aprems, cprems)
+ end;
+
+
+
+
+(* Fixme: allow different order of subgoals in exportf *)
+(* as above, but also fix all parameters in all subgoals, and uses
+fix_alls, not fix_alls', ie doesn't leave extra asumptions as apparent
+subgoals. *)
+(* loosely corresponds to:
+Given
+ "[| !! x0s. A0s x0s ==> SG0 x0s;
+ ...; !! xms. Ams xms ==> SGm xms|] ==> G" : thm
+Result:
+(["(A0s x0s' ==> SG0 x0s') ==> SG0 x0s'",
+ ... ,"(Ams xms' ==> SGm xms') ==> SGm xms'"] : thm list, -- goals
+ ["SG0 x0s'", ..., "SGm xms'"] : thm list -> -- export function
+ "G" : thm)
+*)
+(* requires being given solutions! *)
+fun fixed_subgoal_thms th =
+ let
+ val (subgoals, expf) = subgoal_thms th;
+(* fun export_sg (th, exp) = exp th; *)
+ fun export_sgs expfs solthms =
+ expf (map2 (curry (op |>)) solthms expfs);
+(* expf (map export_sg (ths ~~ expfs)); *)
+ in
+ apsnd export_sgs (Library.split_list (map (apsnd export_solution o
+ fix_alls 1) subgoals))
+ end;
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Provers/IsaPlanner/rw_inst.ML Sun Jun 11 00:28:18 2006 +0200
@@ -0,0 +1,315 @@
+(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
+(* Title: Pure/IsaPlanner/rw_inst.ML
+ ID: $Id$
+ Author: Lucas Dixon, University of Edinburgh
+ lucas.dixon@ed.ac.uk
+ Created: 25 Aug 2004
+*)
+(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
+(* DESCRIPTION:
+
+ rewriting using a conditional meta-equality theorem which supports
+ schematic variable instantiation.
+
+*)
+(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
+signature RW_INST =
+sig
+
+ (* Rewrite: give it instantiation infromation, a rule, and the
+ target thm, and it will return the rewritten target thm *)
+ val rw :
+ ((Term.indexname * (Term.sort * Term.typ)) list * (* type var instantiations *)
+ (Term.indexname * (Term.typ * Term.term)) list) (* schematic var instantiations *)
+ * (string * Term.typ) list (* Fake named bounds + types *)
+ * (string * Term.typ) list (* names of bound + types *)
+ * Term.term -> (* outer term for instantiation *)
+ Thm.thm -> (* rule with indexies lifted *)
+ Thm.thm -> (* target thm *)
+ Thm.thm (* rewritten theorem possibly
+ with additional premises for
+ rule conditions *)
+
+ (* used tools *)
+ val mk_abstractedrule :
+ (string * Term.typ) list (* faked outer bound *)
+ -> (string * Term.typ) list (* hopeful name of outer bounds *)
+ -> Thm.thm -> Thm.cterm list * Thm.thm
+ val mk_fixtvar_tyinsts :
+ (Term.indexname * (Term.sort * Term.typ)) list ->
+ Term.term list -> ((string * int) * (Term.sort * Term.typ)) list
+ * (string * Term.sort) list
+ val mk_renamings :
+ Term.term -> Thm.thm -> (((string * int) * Term.typ) * Term.term) list
+ val new_tfree :
+ ((string * int) * Term.sort) *
+ (((string * int) * (Term.sort * Term.typ)) list * string list) ->
+ ((string * int) * (Term.sort * Term.typ)) list * string list
+ val cross_inst : (Term.indexname * (Term.typ * Term.term)) list
+ -> (Term.indexname *(Term.typ * Term.term)) list
+ val cross_inst_typs : (Term.indexname * (Term.sort * Term.typ)) list
+ -> (Term.indexname * (Term.sort * Term.typ)) list
+
+ val beta_contract : Thm.thm -> Thm.thm
+ val beta_eta_contract : Thm.thm -> Thm.thm
+
+end;
+
+structure RWInst
+: RW_INST
+= struct
+
+
+(* beta contract the theorem *)
+fun beta_contract thm =
+ equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm;
+
+(* beta-eta contract the theorem *)
+fun beta_eta_contract thm =
+ let
+ val thm2 = equal_elim (Thm.beta_conversion true (Thm.cprop_of thm)) thm
+ val thm3 = equal_elim (Thm.eta_conversion (Thm.cprop_of thm2)) thm2
+ in thm3 end;
+
+
+(* to get the free names of a theorem (including hyps and flexes) *)
+fun usednames_of_thm th =
+ let val rep = Thm.rep_thm th
+ val hyps = #hyps rep
+ val (tpairl,tpairr) = Library.split_list (#tpairs rep)
+ val prop = #prop rep
+ in
+ List.foldr Term.add_term_names [] (prop :: (tpairl @ (tpairr @ hyps)))
+ end;
+
+(* Given a list of variables that were bound, and a that has been
+instantiated with free variable placeholders for the bound vars, it
+creates an abstracted version of the theorem, with local bound vars as
+lambda-params:
+
+Ts:
+("x", ty)
+
+rule::
+C :x ==> P :x = Q :x
+
+results in:
+("!! x. C x", (%x. p x = %y. p y) [!! x. C x])
+
+note: assumes rule is instantiated
+*)
+(* Note, we take abstraction in the order of last abstraction first *)
+fun mk_abstractedrule TsFake Ts rule =
+ let
+ val ctermify = Thm.cterm_of (Thm.sign_of_thm rule);
+
+ (* now we change the names of temporary free vars that represent
+ bound vars with binders outside the redex *)
+ val prop = Thm.prop_of rule;
+ val names = usednames_of_thm rule;
+ val (fromnames,tonames,names2,Ts') =
+ Library.foldl (fn ((rnf,rnt,names, Ts''),((faken,_),(n,ty))) =>
+ let val n2 = Term.variant names n in
+ (ctermify (Free(faken,ty)) :: rnf,
+ ctermify (Free(n2,ty)) :: rnt,
+ n2 :: names,
+ (n2,ty) :: Ts'')
+ end)
+ (([],[],names, []), TsFake~~Ts);
+
+ (* rename conflicting free's in the rule to avoid cconflicts
+ with introduced vars from bounds outside in redex *)
+ val rule' = rule |> Drule.forall_intr_list fromnames
+ |> Drule.forall_elim_list tonames;
+
+ (* make unconditional rule and prems *)
+ val (uncond_rule, cprems) = IsaND.allify_conditions ctermify (rev Ts')
+ rule';
+
+ (* using these names create lambda-abstracted version of the rule *)
+ val abstractions = rev (Ts' ~~ tonames);
+ val abstract_rule = Library.foldl (fn (th,((n,ty),ct)) =>
+ Thm.abstract_rule n ct th)
+ (uncond_rule, abstractions);
+ in (cprems, abstract_rule) end;
+
+
+(* given names to avoid, and vars that need to be fixed, it gives
+unique new names to the vars so that they can be fixed as free
+variables *)
+(* make fixed unique free variable instantiations for non-ground vars *)
+(* Create a table of vars to be renamed after instantiation - ie
+ other uninstantiated vars in the hyps of the rule
+ ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *)
+fun mk_renamings tgt rule_inst =
+ let
+ val rule_conds = Thm.prems_of rule_inst
+ val names = foldr Term.add_term_names [] (tgt :: rule_conds);
+ val (conds_tyvs,cond_vs) =
+ Library.foldl (fn ((tyvs, vs), t) =>
+ (Library.union
+ (Term.term_tvars t, tyvs),
+ Library.union
+ (map Term.dest_Var (Term.term_vars t), vs)))
+ (([],[]), rule_conds);
+ val termvars = map Term.dest_Var (Term.term_vars tgt);
+ val vars_to_fix = Library.union (termvars, cond_vs);
+ val (renamings, names2) =
+ foldr (fn (((n,i),ty), (vs, names')) =>
+ let val n' = Term.variant names' n in
+ ((((n,i),ty), Free (n', ty)) :: vs, n'::names')
+ end)
+ ([], names) vars_to_fix;
+ in renamings end;
+
+(* make a new fresh typefree instantiation for the given tvar *)
+fun new_tfree (tv as (ix,sort), (pairs,used)) =
+ let val v = variant used (string_of_indexname ix)
+ in ((ix,(sort,TFree(v,sort)))::pairs, v::used) end;
+
+
+(* make instantiations to fix type variables that are not
+ already instantiated (in ignore_ixs) from the list of terms. *)
+fun mk_fixtvar_tyinsts ignore_insts ts =
+ let
+ val ignore_ixs = map fst ignore_insts;
+ val (tvars, tfrees) =
+ foldr (fn (t, (varixs, tfrees)) =>
+ (Term.add_term_tvars (t,varixs),
+ Term.add_term_tfrees (t,tfrees)))
+ ([],[]) ts;
+ val unfixed_tvars =
+ List.filter (fn (ix,s) => not (ix mem ignore_ixs)) tvars;
+ val (fixtyinsts, _) = foldr new_tfree ([], map fst tfrees) unfixed_tvars
+ in (fixtyinsts, tfrees) end;
+
+
+(* cross-instantiate the instantiations - ie for each instantiation
+replace all occurances in other instantiations - no loops are possible
+and thus only one-parsing of the instantiations is necessary. *)
+fun cross_inst insts =
+ let
+ fun instL (ix, (ty,t)) =
+ map (fn (ix2,(ty2,t2)) =>
+ (ix2, (ty2,Term.subst_vars ([], [(ix, t)]) t2)));
+
+ fun cross_instL ([], l) = rev l
+ | cross_instL ((ix, t) :: insts, l) =
+ cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l));
+
+ in cross_instL (insts, []) end;
+
+(* as above but for types -- I don't know if this is needed, will we ever incur mixed up types? *)
+fun cross_inst_typs insts =
+ let
+ fun instL (ix, (srt,ty)) =
+ map (fn (ix2,(srt2,ty2)) =>
+ (ix2, (srt2,Term.typ_subst_TVars [(ix, ty)] ty2)));
+
+ fun cross_instL ([], l) = rev l
+ | cross_instL ((ix, t) :: insts, l) =
+ cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l));
+
+ in cross_instL (insts, []) end;
+
+
+(* assume that rule and target_thm have distinct var names. THINK:
+efficient version with tables for vars for: target vars, introduced
+vars, and rule vars, for quicker instantiation? The outerterm defines
+which part of the target_thm was modified. Note: we take Ts in the
+upterm order, ie last abstraction first., and with an outeterm where
+the abstracted subterm has the arguments in the revered order, ie
+first abstraction first. FakeTs has abstractions using the fake name
+- ie the name distinct from all other abstractions. *)
+
+fun rw ((nonfixed_typinsts, unprepinsts), FakeTs, Ts, outerterm) rule target_thm =
+ let
+ (* general signature info *)
+ val target_sign = (Thm.sign_of_thm target_thm);
+ val ctermify = Thm.cterm_of target_sign;
+ val ctypeify = Thm.ctyp_of target_sign;
+
+ (* fix all non-instantiated tvars *)
+ val (fixtyinsts, othertfrees) =
+ mk_fixtvar_tyinsts nonfixed_typinsts
+ [Thm.prop_of rule, Thm.prop_of target_thm];
+ val new_fixed_typs = map (fn ((s,i),(srt,ty)) => (Term.dest_TFree ty))
+ fixtyinsts;
+ val typinsts = cross_inst_typs (nonfixed_typinsts @ fixtyinsts);
+
+ (* certified instantiations for types *)
+ val ctyp_insts =
+ map (fn (ix,(s,ty)) => (ctypeify (TVar (ix,s)), ctypeify ty))
+ typinsts;
+
+ (* type instantiated versions *)
+ val tgt_th_tyinst = Thm.instantiate (ctyp_insts,[]) target_thm;
+ val rule_tyinst = Thm.instantiate (ctyp_insts,[]) rule;
+
+ val term_typ_inst = map (fn (ix,(srt,ty)) => (ix,ty)) typinsts;
+ (* type instanitated outer term *)
+ val outerterm_tyinst = Term.subst_TVars term_typ_inst outerterm;
+
+ val FakeTs_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst))
+ FakeTs;
+ val Ts_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst))
+ Ts;
+
+ (* type-instantiate the var instantiations *)
+ val insts_tyinst = foldr (fn ((ix,(ty,t)),insts_tyinst) =>
+ (ix, (Term.typ_subst_TVars term_typ_inst ty,
+ Term.subst_TVars term_typ_inst t))
+ :: insts_tyinst)
+ [] unprepinsts;
+
+ (* cross-instantiate *)
+ val insts_tyinst_inst = cross_inst insts_tyinst;
+
+ (* create certms of instantiations *)
+ val cinsts_tyinst =
+ map (fn (ix,(ty,t)) => (ctermify (Var (ix, ty)),
+ ctermify t)) insts_tyinst_inst;
+
+ (* The instantiated rule *)
+ val rule_inst = rule_tyinst |> Thm.instantiate ([], cinsts_tyinst);
+
+ (* Create a table of vars to be renamed after instantiation - ie
+ other uninstantiated vars in the hyps the *instantiated* rule
+ ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *)
+ val renamings = mk_renamings (Thm.prop_of tgt_th_tyinst)
+ rule_inst;
+ val cterm_renamings =
+ map (fn (x,y) => (ctermify (Var x), ctermify y)) renamings;
+
+ (* Create the specific version of the rule for this target application *)
+ val outerterm_inst =
+ outerterm_tyinst
+ |> Term.subst_Vars (map (fn (ix,(ty,t)) => (ix,t)) insts_tyinst_inst)
+ |> Term.subst_Vars (map (fn ((ix,ty),t) => (ix,t)) renamings);
+ val couter_inst = Thm.reflexive (ctermify outerterm_inst);
+ val (cprems, abstract_rule_inst) =
+ rule_inst |> Thm.instantiate ([], cterm_renamings)
+ |> mk_abstractedrule FakeTs_tyinst Ts_tyinst;
+ val specific_tgt_rule =
+ beta_eta_contract
+ (Thm.combination couter_inst abstract_rule_inst);
+
+ (* create an instantiated version of the target thm *)
+ val tgt_th_inst =
+ tgt_th_tyinst |> Thm.instantiate ([], cinsts_tyinst)
+ |> Thm.instantiate ([], cterm_renamings);
+
+ val (vars,frees_of_fixed_vars) = Library.split_list cterm_renamings;
+
+ in
+ (beta_eta_contract tgt_th_inst)
+ |> Thm.equal_elim specific_tgt_rule
+ |> Drule.implies_intr_list cprems
+ |> Drule.forall_intr_list frees_of_fixed_vars
+ |> Drule.forall_elim_list vars
+ |> Thm.varifyT' othertfrees
+ |-> K Drule.zero_var_indexes
+ end;
+
+
+end; (* struct *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Provers/IsaPlanner/rw_tools.ML Sun Jun 11 00:28:18 2006 +0200
@@ -0,0 +1,188 @@
+(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
+(* Title: Pure/IsaPlanner/rw_tools.ML
+ ID: $Id$
+ Author: Lucas Dixon, University of Edinburgh
+ lucas.dixon@ed.ac.uk
+ Created: 28 May 2004
+*)
+(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
+(* DESCRIPTION:
+
+ term related tools used for rewriting
+
+*)
+(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
+
+signature RWTOOLS =
+sig
+end;
+
+structure RWTools
+= struct
+
+(* fake free variable names for locally bound variables - these work
+as placeholders. *)
+
+(* don't use dest_fake.. - we should instead be working with numbers
+and a list... else we rely on naming conventions which can break, or
+be violated - in contrast list locations are correct by
+construction/definition. *)
+(*
+fun dest_fake_bound_name n =
+ case (explode n) of
+ (":" :: realchars) => implode realchars
+ | _ => n; *)
+fun is_fake_bound_name n = (hd (explode n) = ":");
+fun mk_fake_bound_name n = ":b_" ^ n;
+
+
+
+(* fake free variable names for local meta variables - these work
+as placeholders. *)
+fun dest_fake_fix_name n =
+ case (explode n) of
+ ("@" :: realchars) => implode realchars
+ | _ => n;
+fun is_fake_fix_name n = (hd (explode n) = "@");
+fun mk_fake_fix_name n = "@" ^ n;
+
+
+
+(* fake free variable names for meta level bound variables *)
+fun dest_fake_all_name n =
+ case (explode n) of
+ ("+" :: realchars) => implode realchars
+ | _ => n;
+fun is_fake_all_name n = (hd (explode n) = "+");
+fun mk_fake_all_name n = "+" ^ n;
+
+
+
+
+(* Ys and Ts not used, Ns are real names of faked local bounds, the
+idea is that this will be mapped to free variables thus if a free
+variable is a faked local bound then we change it to being a meta
+variable so that it can later be instantiated *)
+(* FIXME: rename this - avoid the word fix! *)
+(* note we are not really "fix"'ing the free, more like making it variable! *)
+(* fun trymkvar_of_fakefree (Ns, Ts) Ys (n,ty) =
+ if n mem Ns then Var((n,0),ty) else Free (n,ty);
+*)
+
+(* make a var into a fixed free (ie prefixed with "@") *)
+fun mk_fakefixvar Ts ((n,i),ty) = Free(mk_fake_fix_name n, ty);
+
+
+(* mk_frees_bound: string list -> Term.term -> Term.term *)
+(* This function changes free variables to being represented as bound
+variables if the free's variable name is in the given list. The debruijn
+index is simply the position in the list *)
+(* THINKABOUT: danger of an existing free variable with the same name: fix
+this so that name conflict are avoided automatically! In the meantime,
+don't have free variables named starting with a ":" *)
+fun bounds_of_fakefrees Ys (a $ b) =
+ (bounds_of_fakefrees Ys a) $ (bounds_of_fakefrees Ys b)
+ | bounds_of_fakefrees Ys (Abs(n,ty,t)) =
+ Abs(n,ty, bounds_of_fakefrees (n::Ys) t)
+ | bounds_of_fakefrees Ys (Free (n,ty)) =
+ let fun try_mk_bound_of_free (i,[]) = Free (n,ty)
+ | try_mk_bound_of_free (i,(y::ys)) =
+ if n = y then Bound i else try_mk_bound_of_free (i+1,ys)
+ in try_mk_bound_of_free (0,Ys) end
+ | bounds_of_fakefrees Ys t = t;
+
+
+(* map a function f onto each free variables *)
+fun map_to_frees f Ys (a $ b) =
+ (map_to_frees f Ys a) $ (map_to_frees f Ys b)
+ | map_to_frees f Ys (Abs(n,ty,t)) =
+ Abs(n,ty, map_to_frees f ((n,ty)::Ys) t)
+ | map_to_frees f Ys (Free a) =
+ f Ys a
+ | map_to_frees f Ys t = t;
+
+
+(* map a function f onto each meta variable *)
+fun map_to_vars f Ys (a $ b) =
+ (map_to_vars f Ys a) $ (map_to_vars f Ys b)
+ | map_to_vars f Ys (Abs(n,ty,t)) =
+ Abs(n,ty, map_to_vars f ((n,ty)::Ys) t)
+ | map_to_vars f Ys (Var a) =
+ f Ys a
+ | map_to_vars f Ys t = t;
+
+(* map a function f onto each free variables *)
+fun map_to_alls f (Const("all",allty) $ Abs(n,ty,t)) =
+ let val (n2,ty2) = f (n,ty)
+ in (Const("all",allty) $ Abs(n2,ty2,map_to_alls f t)) end
+ | map_to_alls f x = x;
+
+(* map a function f to each type variable in a term *)
+(* implicit arg: term *)
+fun map_to_term_tvars f =
+ Term.map_term_types (fn TVar(ix,ty) => f (ix,ty) | x => x);
+
+
+
+(* what if a param desn't occur in the concl? think about! Note: This
+simply fixes meta level univ bound vars as Frees. At the end, we will
+change them back to schematic vars that will then unify
+appropriactely, ie with unfake_vars *)
+fun fake_concl_of_goal gt i =
+ let
+ val prems = Logic.strip_imp_prems gt
+ val sgt = List.nth (prems, i - 1)
+
+ val tbody = Logic.strip_imp_concl (Term.strip_all_body sgt)
+ val tparams = Term.strip_all_vars sgt
+
+ val fakefrees = map (fn (n, ty) => Free(mk_fake_all_name n, ty))
+ tparams
+ in
+ Term.subst_bounds (rev fakefrees,tbody)
+ end;
+
+(* what if a param desn't occur in the concl? think about! Note: This
+simply fixes meta level univ bound vars as Frees. At the end, we will
+change them back to schematic vars that will then unify
+appropriactely, ie with unfake_vars *)
+fun fake_goal gt i =
+ let
+ val prems = Logic.strip_imp_prems gt
+ val sgt = List.nth (prems, i - 1)
+
+ val tbody = Term.strip_all_body sgt
+ val tparams = Term.strip_all_vars sgt
+
+ val fakefrees = map (fn (n, ty) => Free(mk_fake_all_name n, ty))
+ tparams
+ in
+ Term.subst_bounds (rev fakefrees,tbody)
+ end;
+
+
+(* hand written - for some reason the Isabelle version in drule is broken!
+Example? something to do with Bin Yangs examples?
+ *)
+fun rename_term_bvars ns (Abs(s,ty,t)) =
+ let val s2opt = Library.find_first (fn (x,y) => s = x) ns
+ in case s2opt of
+ NONE => (Abs(s,ty,rename_term_bvars ns t))
+ | SOME (_,s2) => Abs(s2,ty, rename_term_bvars ns t) end
+ | rename_term_bvars ns (a$b) =
+ (rename_term_bvars ns a) $ (rename_term_bvars ns b)
+ | rename_term_bvars _ x = x;
+
+fun rename_thm_bvars ns th =
+ let val t = Thm.prop_of th
+ in Thm.rename_boundvars t (rename_term_bvars ns t) th end;
+
+(* Finish this to show how it breaks! (raises the exception):
+
+exception rename_thm_bvars_exp of ((string * string) list * Thm.thm)
+
+ Drule.rename_bvars ns th
+ handle TERM _ => raise rename_thm_bvars_exp (ns, th);
+*)
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Provers/IsaPlanner/zipper.ML Sun Jun 11 00:28:18 2006 +0200
@@ -0,0 +1,462 @@
+(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
+(* Title: Pure/IsaPlanner/zipper.ML
+ ID: $Id$
+ Author: Lucas Dixon, University of Edinburgh
+ lucas.dixon@ed.ac.uk
+ Created: 24 Mar 2006
+*)
+(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
+(* DESCRIPTION:
+ A notion roughly based on Huet's Zippers for Isabelle terms.
+*)
+
+(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
+
+(* abstract term for no more than pattern matching *)
+signature ABSTRACT_TRM =
+sig
+type typ (* types *)
+type aname (* abstraction names *)
+type fname (* parameter/free variable names *)
+type cname (* constant names *)
+type vname (* meta variable names *)
+type bname (* bound var name *)
+datatype term = Const of (cname * typ)
+ | Abs of (aname * typ * term)
+ | Free of (fname * typ)
+ | Var of (vname * typ)
+ | Bound of bname
+ | $ of term * term;
+type T = term;
+end;
+
+structure IsabelleTrmWrap : ABSTRACT_TRM=
+struct
+open Term;
+type typ = Term.typ; (* types *)
+type aname = string; (* abstraction names *)
+type fname = string; (* parameter/free variable names *)
+type cname = string; (* constant names *)
+type vname = string * int; (* meta variable names *)
+type bname = int; (* bound var name *)
+type T = term;
+end;
+
+(* Concrete version for the Trm structure *)
+signature TRM_CTXT_DATA =
+sig
+
+ structure Trm : ABSTRACT_TRM
+ datatype dtrm = Abs of Trm.aname * Trm.typ
+ | AppL of Trm.T
+ | AppR of Trm.T;
+ val apply : dtrm -> Trm.T -> Trm.T
+ val eq_pos : dtrm * dtrm -> bool
+end;
+
+(* A trm context = list of derivatives *)
+signature TRM_CTXT =
+sig
+ structure D : TRM_CTXT_DATA
+ type T = D.dtrm list
+
+ val empty : T
+ val is_empty : T -> bool
+
+ val eq_path : T * T -> bool
+
+ val add_outerctxt : T -> T -> T
+
+ val apply : T -> D.Trm.T -> D.Trm.T
+
+ val nty_ctxt : T -> (D.Trm.aname * D.Trm.typ) list;
+ val ty_ctxt : T -> D.Trm.typ list;
+
+ val depth : T -> int;
+ val map : (D.dtrm -> D.dtrm) -> T -> T
+ val fold : (D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a
+
+end;
+
+(* A zipper = a term looked at, at a particular point in the term *)
+signature ZIPPER =
+sig
+ structure C : TRM_CTXT
+ type T
+
+ val mktop : C.D.Trm.T -> T
+ val goto_top : T -> T
+ val at_top : T -> bool
+ val mk : (C.D.Trm.T * C.T) -> T
+ val set_trm : C.D.Trm.T -> T -> T
+ val set_ctxt : C.T -> T -> T
+
+ val split : T -> T * C.T
+ val add_outerctxt : C.T -> T -> T
+
+ val ctxt : T -> C.T
+ val trm : T -> C.D.Trm.T
+
+ val nty_ctxt : T -> (C.D.Trm.aname * C.D.Trm.typ) list;
+ val ty_ctxt : T -> C.D.Trm.typ list;
+
+ val depth_of_ctxt : T -> int;
+ val map_on_ctxt : (C.D.dtrm -> C.D.dtrm) -> T -> T
+ val fold_on_ctxt : (C.D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a
+
+ (* searching through a zipper *)
+ datatype zsearch = Here of T | LookIn of T;
+ (* lazily search through the zipper *)
+ val lzy_search : (T -> zsearch list) -> T -> T Seq.seq
+ (* lazy search with folded data *)
+ val pf_lzy_search : ('a -> T -> ('a * zsearch list))
+ -> 'a -> T -> T Seq.seq
+ (* zsearch list is or-choices *)
+ val searchfold : ('a -> T -> (('a * zsearch) list))
+ -> 'a -> T -> ('a * T) Seq.seq
+ (* limit function to the current focus of the zipper,
+ but give function the zipper's context *)
+ val limit_pcapply : (C.T -> T -> ('a * T) Seq.seq)
+ -> T -> ('a * T) Seq.seq
+ val limit_apply : (T -> T Seq.seq) -> T -> T Seq.seq
+ val limit_capply : (C.T -> T -> T Seq.seq) -> T -> T Seq.seq
+
+ (* moving around zippers with option types *)
+ val omove_up : T -> T option
+ val omove_up_abs : T -> T option
+ val omove_up_app : T -> T option
+ val omove_up_left : T -> T option
+ val omove_up_right : T -> T option
+ val omove_up_left_or_abs : T -> T option
+ val omove_up_right_or_abs : T -> T option
+ val omove_down_abs : T -> T option
+ val omove_down_left : T -> T option
+ val omove_down_right : T -> T option
+ val omove_down_app : T -> (T * T) option
+
+ (* moving around zippers, raising exceptions *)
+ exception move of string * T
+ val move_up : T -> T
+ val move_up_abs : T -> T
+ val move_up_app : T -> T
+ val move_up_left : T -> T
+ val move_up_right : T -> T
+ val move_up_left_or_abs : T -> T
+ val move_up_right_or_abs : T -> T
+ val move_down_abs : T -> T
+ val move_down_left : T -> T
+ val move_down_right : T -> T
+ val move_down_app : T -> T * T
+
+end;
+
+
+(* Zipper data for an generic trm *)
+functor TrmCtxtDataFUN(Trm : ABSTRACT_TRM)
+: TRM_CTXT_DATA
+= struct
+
+ structure Trm = Trm;
+
+ (* a dtrm is, in McBridge-speak, a differentiated term. It represents
+ the different ways a term can occur within its datatype constructors *)
+ datatype dtrm = Abs of Trm.aname * Trm.typ
+ | AppL of Trm.T
+ | AppR of Trm.T;
+
+ (* apply a dtrm to a term, ie put the dtrm above it, building context *)
+ fun apply (Abs (s,ty)) t = Trm.Abs (s,ty,t)
+ | apply (AppL tl) tr = Trm.$ (tl, tr)
+ | apply (AppR tr) tl = Trm.$ (tl, tr);
+
+ fun eq_pos (Abs _, Abs _) = true
+ | eq_pos (AppL _, AppL _) = true
+ | eq_pos (AppR _, AppR _) = true
+ | eq_pos _ = false;
+
+end;
+
+
+(* functor for making term contexts given term data *)
+functor TrmCtxtFUN(D : TRM_CTXT_DATA)
+ : TRM_CTXT =
+struct
+ structure D = D;
+
+ type T = D.dtrm list;
+
+ val empty = [];
+ val is_empty = List.null;
+
+ fun eq_path ([], []) = true
+ | eq_path ([], _::_) = false
+ | eq_path ( _::_, []) = false
+ | eq_path (h::t, h2::t2) =
+ D.eq_pos(h,h2) andalso eq_path (t, t2);
+
+ (* add context to outside of existing context *)
+ fun add_outerctxt ctop cbottom = cbottom @ ctop;
+
+ (* mkterm : zipper -> trm -> trm *)
+ val apply = Library.fold D.apply;
+
+ (* named type context *)
+ val nty_ctxt = List.foldr (fn (D.Abs nty,ntys) => nty::ntys
+ | (_,ntys) => ntys) [];
+ (* type context *)
+ val ty_ctxt = List.foldr (fn (D.Abs (_,ty),tys) => ty::tys
+ | (_,tys) => tys) [];
+
+ val depth = length : T -> int;
+
+ val map = List.map : (D.dtrm -> D.dtrm) -> T -> T
+
+ val fold = Library.fold : (D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a;
+
+end;
+
+(* zippers in terms of term contexts *)
+functor ZipperFUN(C : TRM_CTXT)
+ : ZIPPER
+= struct
+
+ structure C = C;
+ structure D = C.D;
+ structure Trm = D.Trm;
+
+ type T = C.D.Trm.T * C.T;
+
+ fun mktop t = (t, C.empty) : T
+
+ val mk = I;
+ val set_trm = apfst o K;
+ val set_ctxt = apsnd o K;
+
+ fun goto_top (z as (t,c)) =
+ if C.is_empty c then z else (C.apply c t, C.empty);
+
+ fun at_top (_,c) = C.is_empty c;
+
+ fun split (t,c) = ((t,C.empty) : T, c : C.T)
+ fun add_outerctxt c (t,c2) = (t, C.add_outerctxt c c2) : T
+
+ val ctxt = snd;
+ val trm = fst;
+
+ val nty_ctxt = C.nty_ctxt o ctxt;
+ val ty_ctxt = C.ty_ctxt o ctxt;
+
+ val depth_of_ctxt = C.depth o ctxt;
+ val map_on_ctxt = apsnd o C.map;
+ fun fold_on_ctxt f = C.fold f o ctxt;
+
+ fun omove_up (t,(d::c)) = SOME (D.apply d t, c)
+ | omove_up (z as (_,[])) = NONE;
+ fun omove_up_abs (t,((D.Abs(n,ty))::c)) = SOME (Trm.Abs(n,ty,t), c)
+ | omove_up_abs z = NONE;
+ fun omove_up_app (t,(D.AppL tl)::c) = SOME(Trm.$(tl,t), c)
+ | omove_up_app (t,(D.AppR tr)::c) = SOME(Trm.$(t,tr), c)
+ | omove_up_app z = NONE;
+ fun omove_up_left (t,(D.AppL tl)::c) = SOME(Trm.$(tl,t), c)
+ | omove_up_left z = NONE;
+ fun omove_up_right (t,(D.AppR tr)::c) = SOME(Trm.$(t,tr), c)
+ | omove_up_right _ = NONE;
+ fun omove_up_left_or_abs (t,(D.AppL tl)::c) =
+ SOME (Trm.$(tl,t), c)
+ | omove_up_left_or_abs (t,(D.Abs (n,ty))::c) =
+ SOME (Trm.Abs(n,ty,t), c)
+ | omove_up_left_or_abs z = NONE;
+ fun omove_up_right_or_abs (t,(D.Abs (n,ty))::c) =
+ SOME (Trm.Abs(n,ty,t), c)
+ | omove_up_right_or_abs (t,(D.AppR tr)::c) =
+ SOME (Trm.$(t,tr), c)
+ | omove_up_right_or_abs _ = NONE;
+ fun omove_down_abs (Trm.Abs(s,ty,t),c) = SOME (t,(D.Abs(s,ty))::c)
+ | omove_down_abs _ = NONE;
+ fun omove_down_left (Trm.$(l,r),c) = SOME (l,(D.AppR r)::c)
+ | omove_down_left _ = NONE;
+ fun omove_down_right (Trm.$(l,r),c) = SOME (r,(D.AppL l)::c)
+ | omove_down_right _ = NONE;
+ fun omove_down_app (Trm.$(l,r),c) =
+ SOME ((l,(D.AppR r)::c),(r,(D.AppL l)::c))
+ | omove_down_app _ = NONE;
+
+ exception move of string * T
+ fun move_up (t,(d::c)) = (D.apply d t, c)
+ | move_up (z as (_,[])) = raise move ("move_up",z);
+ fun move_up_abs (t,((D.Abs(n,ty))::c)) = (Trm.Abs(n,ty,t), c)
+ | move_up_abs z = raise move ("move_up_abs",z);
+ fun move_up_app (t,(D.AppL tl)::c) = (Trm.$(tl,t), c)
+ | move_up_app (t,(D.AppR tr)::c) = (Trm.$(t,tr), c)
+ | move_up_app z = raise move ("move_up_app",z);
+ fun move_up_left (t,((D.AppL tl)::c)) = (Trm.$(tl,t), c)
+ | move_up_left z = raise move ("move_up_left",z);
+ fun move_up_right (t,(D.AppR tr)::c) = (Trm.$(t,tr), c)
+ | move_up_right z = raise move ("move_up_right",z);
+ fun move_up_left_or_abs (t,(D.AppL tl)::c) = (Trm.$(tl,t), c)
+ | move_up_left_or_abs (t,(D.Abs (n,ty))::c) = (Trm.Abs(n,ty,t), c)
+ | move_up_left_or_abs z = raise move ("move_up_left_or_abs",z);
+ fun move_up_right_or_abs (t,(D.Abs (n,ty))::c) = (Trm.Abs(n,ty,t), c)
+ | move_up_right_or_abs (t,(D.AppR tr)::c) = (Trm.$(t,tr), c)
+ | move_up_right_or_abs z = raise move ("move_up_right_or_abs",z);
+ fun move_down_abs (Trm.Abs(s,ty,t),c) = (t,(D.Abs(s,ty))::c)
+ | move_down_abs z = raise move ("move_down_abs",z);
+ fun move_down_left (Trm.$(l,r),c) = (l,(D.AppR r)::c)
+ | move_down_left z = raise move ("move_down_left",z);
+ fun move_down_right (Trm.$(l,r),c) = (r,(D.AppL l)::c)
+ | move_down_right z = raise move ("move_down_right",z);
+ fun move_down_app (Trm.$(l,r),c) =
+ ((l,(D.AppR r)::c),(r,(D.AppL l)::c))
+ | move_down_app z = raise move ("move_down_app",z);
+
+
+ (* Note: interpretted as being examined depth first *)
+ datatype zsearch = Here of T | LookIn of T;
+
+ fun lzy_search fsearch =
+ let
+ fun lzyl [] () = NONE
+ | lzyl ((Here z) :: more) () = SOME(z, Seq.make (lzyl more))
+ | lzyl ((LookIn z) :: more) () =
+ (case lzy z
+ of NONE => NONE
+ | SOME (hz,mz) =>
+ SOME (hz, Seq.append (mz, Seq.make (lzyl more))))
+ and lzy z = lzyl (fsearch z) ()
+ in Seq.make o lzyl o fsearch end;
+
+ (* path folded lazy search - the search list is defined in terms of
+ the path passed through: the data a is updated with every zipper
+ considered *)
+ fun pf_lzy_search fsearch a0 z =
+ let
+ fun lzyl a [] () = NONE
+ | lzyl a ((Here z) :: more) () = SOME(z, Seq.make (lzyl a more))
+ | lzyl a ((LookIn z) :: more) () =
+ (case lzy a z
+ of NONE => lzyl a more ()
+ | SOME(hz,mz) => SOME(hz,Seq.append(mz,Seq.make(lzyl a more))))
+ and lzy a z =
+ let val (a2, slist) = (fsearch a z) in lzyl a2 slist () end
+
+ val (a,slist) = fsearch a0 z
+ in Seq.make (lzyl a slist) end;
+
+ (* Note: depth first over zsearch results *)
+ fun searchfold fsearch a0 z =
+ let
+ fun lzyl [] () = NONE
+ | lzyl ((a, Here z) :: more) () =
+ SOME((a,z), Seq.make (lzyl more))
+ | lzyl ((a, LookIn z) :: more) () =
+ (case lzyl (fsearch a z) () of
+ NONE => lzyl more ()
+ | SOME (z,mz) => SOME (z,Seq.append(mz, Seq.make (lzyl more))))
+ in Seq.make (lzyl (fsearch a0 z)) end;
+
+
+ fun limit_pcapply f z =
+ let val (z2,c) = split z
+ in Seq.map (apsnd (add_outerctxt c)) (f c z2) end;
+ fun limit_capply (f : C.T -> T -> T Seq.seq) (z : T) =
+ let val ((z2 : T),(c : C.T)) = split z
+ in Seq.map (add_outerctxt c) (f c z2) end
+
+ val limit_apply = limit_capply o K;
+
+end;
+
+(* now build these for Isabelle terms *)
+structure TrmCtxtData = TrmCtxtDataFUN(IsabelleTrmWrap);
+structure TrmCtxt = TrmCtxtFUN(TrmCtxtData);
+structure Zipper = ZipperFUN(TrmCtxt);
+
+
+
+(* For searching through Zippers below the current focus...
+ KEY for naming scheme:
+
+ td = starting at the top down
+ lr = going from left to right
+ rl = going from right to left
+
+ bl = starting at the bottom left
+ br = starting at the bottom right
+ ul = going up then left
+ ur = going up then right
+ ru = going right then up
+ lu = going left then up
+*)
+signature ZIPPER_SEARCH =
+sig
+ structure Z : ZIPPER;
+
+ val leaves_lr : Z.T -> Z.T Seq.seq
+ val leaves_rl : Z.T -> Z.T Seq.seq
+
+ val all_bl_ru : Z.T -> Z.T Seq.seq
+ val all_bl_ur : Z.T -> Z.T Seq.seq
+ val all_td_lr : Z.T -> Z.T Seq.seq
+ val all_td_rl : Z.T -> Z.T Seq.seq
+
+end;
+
+functor ZipperSearchFUN(Zipper : ZIPPER) : ZIPPER_SEARCH
+= struct
+
+structure Z = Zipper;
+structure C = Z.C;
+structure D = C.D;
+structure Trm = D.Trm;
+
+fun sf_leaves_lr z =
+ case Z.trm z
+ of Trm.$ _ => [Z.LookIn (Z.move_down_left z),
+ Z.LookIn (Z.move_down_right z)]
+ | Trm.Abs _ => [Z.LookIn (Z.move_down_abs z)]
+ | _ => [Z.Here z];
+fun sf_leaves_rl z =
+ case Z.trm z
+ of Trm.$ _ => [Z.LookIn (Z.move_down_right z),
+ Z.LookIn (Z.move_down_left z)]
+ | Trm.Abs _ => [Z.LookIn (Z.move_down_abs z)]
+ | _ => [Z.Here z];
+val leaves_lr = Z.lzy_search sf_leaves_lr;
+val leaves_rl = Z.lzy_search sf_leaves_rl;
+
+
+fun sf_all_td_lr z =
+ case Z.trm z
+ of Trm.$ _ => [Z.Here z, Z.LookIn (Z.move_down_left z),
+ Z.LookIn (Z.move_down_right z)]
+ | Trm.Abs _ => [Z.Here z, Z.LookIn (Z.move_down_abs z)]
+ | _ => [Z.Here z];
+fun sf_all_td_rl z =
+ case Z.trm z
+ of Trm.$ _ => [Z.Here z, Z.LookIn (Z.move_down_right z),
+ Z.LookIn (Z.move_down_left z)]
+ | Trm.Abs _ => [Z.Here z, Z.LookIn (Z.move_down_abs z)]
+ | _ => [Z.Here z];
+fun sf_all_bl_ur z =
+ case Z.trm z
+ of Trm.$ _ => [Z.LookIn (Z.move_down_left z), Z.Here z,
+ Z.LookIn (Z.move_down_right z)]
+ | Trm.Abs _ => [Z.LookIn (Z.move_down_abs z),
+ Z.Here z]
+ | _ => [Z.Here z];
+fun sf_all_bl_ru z =
+ case Z.trm z
+ of Trm.$ _ => [Z.LookIn (Z.move_down_left z),
+ Z.LookIn (Z.move_down_right z), Z.Here z]
+ | Trm.Abs _ => [Z.LookIn (Z.move_down_abs z), Z.Here z]
+ | _ => [Z.Here z];
+
+val all_td_lr = Z.lzy_search sf_all_td_lr;
+val all_td_rl = Z.lzy_search sf_all_td_lr;
+val all_bl_ur = Z.lzy_search sf_all_bl_ru;
+val all_bl_ru = Z.lzy_search sf_all_bl_ur;
+
+end;
+
+
+structure ZipperSearch = ZipperSearchFUN(Zipper);
--- a/src/Provers/eqsubst.ML Fri Jun 09 17:32:38 2006 +0200
+++ b/src/Provers/eqsubst.ML Sun Jun 11 00:28:18 2006 +0200
@@ -10,9 +10,13 @@
val setup : theory -> theory
end;
-structure EqSubst: EQSUBST =
-struct
+structure EqSubst
+(* : EQSUBST *)
+= struct
+structure Z = Zipper;
+
+(* changes object "=" to meta "==" which prepares a given rewrite rule *)
fun prep_meta_eq ctxt =
let val (_, {mk_rews = {mk, ...}, ...}) = Simplifier.rep_ss (Simplifier.local_simpset_of ctxt)
in mk #> map Drule.zero_var_indexes end;
@@ -29,7 +33,129 @@
type searchinfo =
theory
* int (* maxidx *)
- * BasicIsaFTerm.FcTerm (* focusterm to search under *)
+ * Zipper.T (* focusterm to search under *)
+
+
+(* skipping non-empty sub-sequences but when we reach the end
+ of the seq, remembering how much we have left to skip. *)
+datatype 'a skipseq = SkipMore of int
+ | SkipSeq of 'a Seq.seq Seq.seq;
+(* given a seqseq, skip the first m non-empty seq's, note deficit *)
+fun skipto_skipseq m s =
+ let
+ fun skip_occs n sq =
+ case Seq.pull sq of
+ NONE => SkipMore n
+ | SOME (h,t) =>
+ (case Seq.pull h of NONE => skip_occs n t
+ | SOME _ => if n <= 1 then SkipSeq (Seq.cons h t)
+ else skip_occs (n - 1) t)
+ in (skip_occs m s) end;
+
+(* note: outerterm is the taget with the match replaced by a bound
+ variable : ie: "P lhs" beocmes "%x. P x"
+ insts is the types of instantiations of vars in lhs
+ and typinsts is the type instantiations of types in the lhs
+ Note: Final rule is the rule lifted into the ontext of the
+ taget thm. *)
+fun mk_foo_match mkuptermfunc Ts t =
+ let
+ val ty = Term.type_of t
+ val bigtype = (rev (map snd Ts)) ---> ty
+ fun mk_foo 0 t = t
+ | mk_foo i t = mk_foo (i - 1) (t $ (Bound (i - 1)))
+ val num_of_bnds = (length Ts)
+ (* foo_term = "fooabs y0 ... yn" where y's are local bounds *)
+ val foo_term = mk_foo num_of_bnds (Bound num_of_bnds)
+ in Abs("fooabs", bigtype, mkuptermfunc foo_term) end;
+
+(* T is outer bound vars, n is number of locally bound vars *)
+(* THINK: is order of Ts correct...? or reversed? *)
+fun fakefree_badbounds Ts t =
+ let val (FakeTs,Ts,newnames) =
+ List.foldr (fn ((n,ty),(FakeTs,Ts,usednames)) =>
+ let val newname = Term.variant usednames n
+ in ((RWTools.mk_fake_bound_name newname,ty)::FakeTs,
+ (newname,ty)::Ts,
+ newname::usednames) end)
+ ([],[],[])
+ Ts
+ in (FakeTs, Ts, Term.subst_bounds (map Free FakeTs, t)) end;
+
+(* before matching we need to fake the bound vars that are missing an
+abstraction. In this function we additionally construct the
+abstraction environment, and an outer context term (with the focus
+abstracted out) for use in rewriting with RWInst.rw *)
+fun prep_zipper_match z =
+ let
+ val t = Z.trm z
+ val c = Z.ctxt z
+ val Ts = Z.C.nty_ctxt c
+ val (FakeTs', Ts', t') = fakefree_badbounds Ts t
+ val absterm = mk_foo_match (Z.C.apply c) Ts' t'
+ in
+ (t', (FakeTs', Ts', absterm))
+ end;
+
+(* Matching and Unification with exception handled *)
+fun clean_match thy (a as (pat, t)) =
+ let val (tyenv, tenv) = Pattern.match thy a (Vartab.empty, Vartab.empty)
+ in SOME (Vartab.dest tyenv, Vartab.dest tenv)
+ end handle Pattern.MATCH => NONE;
+(* given theory, max var index, pat, tgt; returns Seq of instantiations *)
+fun clean_unify sgn ix (a as (pat, tgt)) =
+ let
+ (* type info will be re-derived, maybe this can be cached
+ for efficiency? *)
+ val pat_ty = Term.type_of pat;
+ val tgt_ty = Term.type_of tgt;
+ (* is it OK to ignore the type instantiation info?
+ or should I be using it? *)
+ val typs_unify =
+ SOME (Sign.typ_unify sgn (pat_ty, tgt_ty) (Term.Vartab.empty, ix))
+ handle Type.TUNIFY => NONE;
+ in
+ case typs_unify of
+ SOME (typinsttab, ix2) =>
+ let
+ (* is it right to throw away the flexes?
+ or should I be using them somehow? *)
+ fun mk_insts env =
+ (Vartab.dest (Envir.type_env env),
+ Envir.alist_of env);
+ val initenv = Envir.Envir {asol = Vartab.empty,
+ iTs = typinsttab, maxidx = ix2};
+ val useq = (Unify.smash_unifiers (sgn,initenv,[a]))
+ handle UnequalLengths => Seq.empty
+ | Term.TERM _ => Seq.empty;
+ fun clean_unify' useq () =
+ (case (Seq.pull useq) of
+ NONE => NONE
+ | SOME (h,t) => SOME (mk_insts h, Seq.make (clean_unify' t)))
+ handle UnequalLengths => NONE
+ | Term.TERM _ => NONE;
+ in
+ (Seq.make (clean_unify' useq))
+ end
+ | NONE => Seq.empty
+ end;
+
+(* Matching and Unification for zippers *)
+(* Note: Ts is a modified version of the original names of the outer
+bound variables. New names have been introduced to make sure they are
+unique w.r.t all names in the term and each other. usednames' is
+oldnames + new names. *)
+fun clean_match_z thy pat z =
+ let val (t, (FakeTs,Ts,absterm)) = prep_zipper_match z in
+ case clean_match thy (pat, t) of
+ NONE => NONE
+ | SOME insts => SOME (insts, FakeTs, Ts, absterm) end;
+(* ix = max var index *)
+fun clean_unify_z sgn ix pat z =
+ let val (t, (FakeTs, Ts,absterm)) = prep_zipper_match z in
+ Seq.map (fn insts => (insts, FakeTs, Ts, absterm))
+ (clean_unify sgn ix (t, pat)) end;
+
(* FOR DEBUGGING...
type trace_subst_errT = int (* subgoal *)
@@ -46,54 +172,45 @@
val trace_subst_err = (ref NONE : trace_subst_errT option ref);
val trace_subst_search = ref false;
exception trace_subst_exp of trace_subst_errT;
- *)
+*)
+
+
+fun bot_left_leaf_of (l $ r) = bot_left_leaf_of l
+ | bot_left_leaf_of (Abs(s,ty,t)) = bot_left_leaf_of t
+ | bot_left_leaf_of x = x;
+fun valid_match_start z =
+ (case bot_left_leaf_of (Z.trm z) of
+ Const _ => true
+ | Free _ => true
+ | Abs _ => true (* allowed to look inside abs... search decides if we actually consider the abstraction itself *)
+ | _ => false); (* avoid vars - always suceeds uninterestingly. *)
+
(* search from top, left to right, then down *)
-fun search_tlr_all_f f ft =
- let
- fun maux ft =
- let val t' = (IsaFTerm.focus_of_fcterm ft)
- (* val _ =
- if !trace_subst_search then
- (writeln ("Examining: " ^ (TermLib.string_of_term t'));
- TermLib.writeterm t'; ())
- else (); *)
- in
- (case t' of
- (_ $ _) => Seq.append(maux (IsaFTerm.focus_left ft),
- Seq.cons (f ft) (maux (IsaFTerm.focus_right ft)))
- | (Abs _) => Seq.cons (f ft) (maux (IsaFTerm.focus_abs ft))
- | leaf => Seq.single (f ft)) end
- in maux ft end;
+val search_tlr_all = ZipperSearch.all_td_lr;
(* search from top, left to right, then down *)
-fun search_tlr_valid_f f ft =
- let
- fun maux ft =
- let
- val hereseq = if IsaFTerm.valid_match_start ft then f ft else Seq.empty
- in
- (case (IsaFTerm.focus_of_fcterm ft) of
- (_ $ _) => Seq.append(maux (IsaFTerm.focus_left ft),
- Seq.cons hereseq (maux (IsaFTerm.focus_right ft)))
- | (Abs _) => Seq.cons hereseq (maux (IsaFTerm.focus_abs ft))
- | leaf => Seq.single hereseq)
- end
- in maux ft end;
+fun search_tlr_valid validf =
+ let
+ fun sf_valid_td_lr z =
+ let val here = if validf z then [Z.Here z] else [] in
+ case Z.trm z
+ of _ $ _ => here @ [Z.LookIn (Z.move_down_left z),
+ Z.LookIn (Z.move_down_right z)]
+ | Abs _ => here @ [Z.LookIn (Z.move_down_abs z)]
+ | _ => here
+ end;
+ in Z.lzy_search sf_valid_td_lr end;
(* search all unifications *)
-fun searchf_tlr_unify_all (sgn, maxidx, ft) lhs =
- IsaFTerm.find_fcterm_matches
- search_tlr_all_f
- (IsaFTerm.clean_unify_ft sgn maxidx lhs)
- ft;
+fun searchf_tlr_unify_all (sgn, maxidx, z) lhs =
+ Seq.map (clean_unify_z sgn maxidx lhs)
+ (Z.limit_apply search_tlr_all z);
(* search only for 'valid' unifiers (non abs subterms and non vars) *)
-fun searchf_tlr_unify_valid (sgn, maxidx, ft) lhs =
- IsaFTerm.find_fcterm_matches
- search_tlr_valid_f
- (IsaFTerm.clean_unify_ft sgn maxidx lhs)
- ft;
+fun searchf_tlr_unify_valid (sgn, maxidx, z) lhs =
+ Seq.map (clean_unify_z sgn maxidx lhs)
+ (Z.limit_apply (search_tlr_valid valid_match_start) z);
(* apply a substitution in the conclusion of the theorem th *)
@@ -124,9 +241,9 @@
val conclterm = Logic.strip_imp_concl fixedbody;
val conclthm = trivify conclterm;
val maxidx = Term.maxidx_of_term conclterm;
- val ft = ((IsaFTerm.focus_right
- o IsaFTerm.focus_left
- o IsaFTerm.fcterm_of_term
+ val ft = ((Z.move_down_right (* ==> *)
+ o Z.move_down_left (* Trueprop *)
+ o Z.mktop
o Thm.prop_of) conclthm)
in
((cfvs, conclthm), (sgn, maxidx, ft))
@@ -150,12 +267,14 @@
(* General substitution of multiple occurances using one of
the given theorems*)
+
+
exception eqsubst_occL_exp of
string * (int list) * (thm list) * int * thm;
fun skip_first_occs_search occ srchf sinfo lhs =
- case (IsaPLib.skipto_seqseq occ (srchf sinfo lhs)) of
- IsaPLib.skipmore _ => Seq.empty
- | IsaPLib.skipseq ss => Seq.flat ss;
+ case (skipto_skipseq occ (srchf sinfo lhs)) of
+ SkipMore _ => Seq.empty
+ | SkipSeq ss => Seq.flat ss;
fun eqsubst_tac ctxt occL thms i th =
let val nprems = Thm.nprems_of th in
@@ -163,8 +282,10 @@
let val thmseq = (Seq.of_list thms)
fun apply_occ occ th =
thmseq |> Seq.maps
- (fn r => eqsubst_tac' ctxt (skip_first_occs_search
- occ searchf_tlr_unify_valid) r
+ (fn r => eqsubst_tac'
+ ctxt
+ (skip_first_occs_search
+ occ searchf_tlr_unify_valid) r
(i + ((Thm.nprems_of th) - nprems))
th);
val sortedoccL =
@@ -235,15 +356,15 @@
val pth = trivify asmt;
val maxidx = Term.maxidx_of_term asmt;
- val ft = ((IsaFTerm.focus_right
- o IsaFTerm.fcterm_of_term
+ val ft = ((Z.move_down_right (* trueprop *)
+ o Z.mktop
o Thm.prop_of) pth)
in ((cfvs, j, asm_nprems, pth), (sgn, maxidx, ft)) end;
(* prepare subst in every possible assumption *)
fun prep_subst_in_asms i gth =
map (prep_subst_in_asm i gth)
- ((rev o IsaPLib.mk_num_list o length)
+ ((fn l => Library.upto (1, length l))
(Logic.prems_of_goal (Thm.prop_of gth) i));
@@ -257,8 +378,8 @@
fun occ_search occ [] = Seq.empty
| occ_search occ ((asminfo, searchinfo)::moreasms) =
(case searchf searchinfo occ lhs of
- IsaPLib.skipmore i => occ_search i moreasms
- | IsaPLib.skipseq ss =>
+ SkipMore i => occ_search i moreasms
+ | SkipSeq ss =>
Seq.append (Seq.map (Library.pair asminfo)
(Seq.flat ss),
occ_search 1 moreasms))
@@ -270,7 +391,7 @@
fun skip_first_asm_occs_search searchf sinfo occ lhs =
- IsaPLib.skipto_seqseq occ (searchf sinfo lhs);
+ skipto_skipseq occ (searchf sinfo lhs);
fun eqsubst_asm_tac ctxt occL thms i th =
let val nprems = Thm.nprems_of th