# HG changeset patch # User dixon # Date 1149978498 -7200 # Node ID 81d6dc59755959c987809339356bbefec2bed5a2 # Parent 2290cc06049b4fde7341be8158bd8961b08c349d added updated version of IsaPlanner and substitution. diff -r 2290cc06049b -r 81d6dc597559 src/FOL/ROOT.ML --- 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"; diff -r 2290cc06049b -r 81d6dc597559 src/HOL/ROOT.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"; diff -r 2290cc06049b -r 81d6dc597559 src/Provers/IsaPlanner/ROOT.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"; diff -r 2290cc06049b -r 81d6dc597559 src/Provers/IsaPlanner/isand.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; diff -r 2290cc06049b -r 81d6dc597559 src/Provers/IsaPlanner/rw_inst.ML --- /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 *) diff -r 2290cc06049b -r 81d6dc597559 src/Provers/IsaPlanner/rw_tools.ML --- /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; diff -r 2290cc06049b -r 81d6dc597559 src/Provers/IsaPlanner/zipper.ML --- /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); diff -r 2290cc06049b -r 81d6dc597559 src/Provers/eqsubst.ML --- 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