# HG changeset patch # User wenzelm # Date 1180637729 -7200 # Node ID 861f63a35d31cb084922727e4858801a1f6cf96f # Parent 94e9413bd7fc0efe269f78fd96d8a12d3859b4f3 moved IsaPlanner from Provers to Tools; diff -r 94e9413bd7fc -r 861f63a35d31 src/FOL/IFOL.thy --- a/src/FOL/IFOL.thy Thu May 31 19:11:19 2007 +0200 +++ b/src/FOL/IFOL.thy Thu May 31 20:55:29 2007 +0200 @@ -10,10 +10,10 @@ uses "~~/src/Provers/splitter.ML" "~~/src/Provers/hypsubst.ML" - "~~/src/Provers/IsaPlanner/zipper.ML" - "~~/src/Provers/IsaPlanner/isand.ML" - "~~/src/Provers/IsaPlanner/rw_tools.ML" - "~~/src/Provers/IsaPlanner/rw_inst.ML" + "~~/src/Tools/IsaPlanner/zipper.ML" + "~~/src/Tools/IsaPlanner/isand.ML" + "~~/src/Tools/IsaPlanner/rw_tools.ML" + "~~/src/Tools/IsaPlanner/rw_inst.ML" "~~/src/Provers/eqsubst.ML" "~~/src/Provers/induct_method.ML" "~~/src/Provers/classical.ML" diff -r 94e9413bd7fc -r 861f63a35d31 src/FOL/IsaMakefile --- a/src/FOL/IsaMakefile Thu May 31 19:11:19 2007 +0200 +++ b/src/FOL/IsaMakefile Thu May 31 20:55:29 2007 +0200 @@ -30,10 +30,10 @@ $(OUT)/FOL$(ML_SUFFIX): $(OUT)/Pure$(ML_SUFFIX) $(SRC)/Provers/blast.ML \ $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \ - $(SRC)/Provers/IsaPlanner/zipper.ML \ - $(SRC)/Provers/IsaPlanner/isand.ML \ - $(SRC)/Provers/IsaPlanner/rw_tools.ML \ - $(SRC)/Provers/IsaPlanner/rw_inst.ML \ + $(SRC)/Tools/IsaPlanner/zipper.ML \ + $(SRC)/Tools/IsaPlanner/isand.ML \ + $(SRC)/Tools/IsaPlanner/rw_tools.ML \ + $(SRC)/Tools/IsaPlanner/rw_inst.ML \ $(SRC)/Provers/eqsubst.ML $(SRC)/Provers/hypsubst.ML \ $(SRC)/Provers/induct_method.ML \ $(SRC)/Provers/project_rule.ML $(SRC)/Provers/quantifier1.ML \ diff -r 94e9413bd7fc -r 861f63a35d31 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Thu May 31 19:11:19 2007 +0200 +++ b/src/HOL/HOL.thy Thu May 31 20:55:29 2007 +0200 @@ -11,10 +11,10 @@ "hologic.ML" "~~/src/Provers/splitter.ML" "~~/src/Provers/hypsubst.ML" - "~~/src/Provers/IsaPlanner/zipper.ML" - "~~/src/Provers/IsaPlanner/isand.ML" - "~~/src/Provers/IsaPlanner/rw_tools.ML" - "~~/src/Provers/IsaPlanner/rw_inst.ML" + "~~/src/Tools/IsaPlanner/zipper.ML" + "~~/src/Tools/IsaPlanner/isand.ML" + "~~/src/Tools/IsaPlanner/rw_tools.ML" + "~~/src/Tools/IsaPlanner/rw_inst.ML" "~~/src/Provers/eqsubst.ML" "~~/src/Provers/induct_method.ML" "~~/src/Provers/classical.ML" diff -r 94e9413bd7fc -r 861f63a35d31 src/Provers/IsaPlanner/ROOT.ML --- a/src/Provers/IsaPlanner/ROOT.ML Thu May 31 19:11:19 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,16 +0,0 @@ -(* 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 94e9413bd7fc -r 861f63a35d31 src/Provers/IsaPlanner/isand.ML --- a/src/Provers/IsaPlanner/isand.ML Thu May 31 19:11:19 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,642 +0,0 @@ -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) -(* 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. - - 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.theory_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_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 = Name.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.theory_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 = Name.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.theory_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.theory_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.theory_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.theory_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.theory_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 - (Name.variant_list names (map fst alls) - ~~ (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 - (Name.variant_list names (map fst alls) - ~~ (map snd alls)); - in ((subst_bounds (fvs,body)), fvs) end; - -fun fix_alls_cterm i th = - let - val ctermify = Thm.cterm_of (Thm.theory_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.theory_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.theory_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 94e9413bd7fc -r 861f63a35d31 src/Provers/IsaPlanner/rw_inst.ML --- a/src/Provers/IsaPlanner/rw_inst.ML Thu May 31 19:11:19 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,315 +0,0 @@ -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) -(* 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.theory_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 = Name.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' = Name.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 = Name.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 (member (op =) ignore_ixs ix)) 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.theory_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 94e9413bd7fc -r 861f63a35d31 src/Provers/IsaPlanner/rw_tools.ML --- a/src/Provers/IsaPlanner/rw_tools.ML Thu May 31 19:11:19 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,188 +0,0 @@ -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) -(* 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_types (fn TVar(ix,ty) => f (ix,ty) | x => x); (* FIXME map_atyps !? *) - - - -(* 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 94e9413bd7fc -r 861f63a35d31 src/Provers/IsaPlanner/zipper.ML --- a/src/Provers/IsaPlanner/zipper.ML Thu May 31 19:11:19 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,491 +0,0 @@ -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) -(* 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 add_abs : D.Trm.aname * D.Trm.typ -> T -> T; - val add_appl : D.Trm.T -> T -> T; - val add_appr : D.Trm.T -> T -> T; - - val add_dtrm : D.dtrm -> T -> T; - - 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_up : (D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a - val fold_down : (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 mk : (C.D.Trm.T * C.T) -> T - - val goto_top : T -> T - val at_top : T -> bool - - val split : T -> T * C.T - val add_outerctxt : C.T -> T -> T - - val set_trm : C.D.Trm.T -> T -> T - val set_ctxt : C.T -> T -> T - - val ctxt : T -> C.T - val trm : T -> C.D.Trm.T - val top_trm : T -> C.D.Trm.T - - val zipto : C.T -> T -> T (* follow context down *) - - 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_up_ctxt : (C.D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a - val fold_down_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 add_abs d l = (D.Abs d) :: l; - fun add_appl d l = (D.AppL d) :: l; - fun add_appr d l = (D.AppR d) :: l; - - fun add_dtrm d l = d::l; - - 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 = Basics.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_up = Basics.fold : (D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a; - val fold_down = Basics.fold_rev : (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; - fun set_trm x = apfst (K x); - fun set_ctxt x = apsnd (K x); - - 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 top_trm = trm o goto_top; - - fun nty_ctxt x = C.nty_ctxt (ctxt x); - fun ty_ctxt x = C.ty_ctxt (ctxt x); - - fun depth_of_ctxt x = C.depth (ctxt x); - fun map_on_ctxt x = apsnd (C.map x); - fun fold_up_ctxt f = C.fold_up f o ctxt; - fun fold_down_ctxt f = C.fold_down 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); - - (* follow the given path down the given zipper *) - (* implicit arguments: C.D.dtrm list, then T *) - val zipto = C.fold_down - (fn C.D.Abs _ => move_down_abs - | C.D.AppL _ => move_down_right - | C.D.AppR _ => move_down_left); - - (* Note: interpretted as being examined depth first *) - datatype zsearch = Here of T | LookIn of T; - - (* lazy search *) - 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_rl; -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 94e9413bd7fc -r 861f63a35d31 src/Tools/IsaPlanner/README --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/IsaPlanner/README Thu May 31 20:55:29 2007 +0200 @@ -0,0 +1,4 @@ +ID: $Id$ +Author: Lucas Dixon, University of Edinburgh + +Support files for IsaPlanner (see http://isaplanner.sourceforge.net). diff -r 94e9413bd7fc -r 861f63a35d31 src/Tools/IsaPlanner/isand.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/IsaPlanner/isand.ML Thu May 31 20:55:29 2007 +0200 @@ -0,0 +1,642 @@ +(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) +(* 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. + + 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.theory_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_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 = Name.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.theory_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 = Name.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.theory_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.theory_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.theory_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.theory_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.theory_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 + (Name.variant_list names (map fst alls) + ~~ (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 + (Name.variant_list names (map fst alls) + ~~ (map snd alls)); + in ((subst_bounds (fvs,body)), fvs) end; + +fun fix_alls_cterm i th = + let + val ctermify = Thm.cterm_of (Thm.theory_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.theory_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.theory_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 94e9413bd7fc -r 861f63a35d31 src/Tools/IsaPlanner/rw_inst.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/IsaPlanner/rw_inst.ML Thu May 31 20:55:29 2007 +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.theory_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 = Name.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' = Name.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 = Name.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 (member (op =) ignore_ixs ix)) 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.theory_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 94e9413bd7fc -r 861f63a35d31 src/Tools/IsaPlanner/rw_tools.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/IsaPlanner/rw_tools.ML Thu May 31 20:55:29 2007 +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_types (fn TVar(ix,ty) => f (ix,ty) | x => x); (* FIXME map_atyps !? *) + + + +(* 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 94e9413bd7fc -r 861f63a35d31 src/Tools/IsaPlanner/zipper.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/IsaPlanner/zipper.ML Thu May 31 20:55:29 2007 +0200 @@ -0,0 +1,491 @@ +(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) +(* 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 add_abs : D.Trm.aname * D.Trm.typ -> T -> T; + val add_appl : D.Trm.T -> T -> T; + val add_appr : D.Trm.T -> T -> T; + + val add_dtrm : D.dtrm -> T -> T; + + 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_up : (D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a + val fold_down : (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 mk : (C.D.Trm.T * C.T) -> T + + val goto_top : T -> T + val at_top : T -> bool + + val split : T -> T * C.T + val add_outerctxt : C.T -> T -> T + + val set_trm : C.D.Trm.T -> T -> T + val set_ctxt : C.T -> T -> T + + val ctxt : T -> C.T + val trm : T -> C.D.Trm.T + val top_trm : T -> C.D.Trm.T + + val zipto : C.T -> T -> T (* follow context down *) + + 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_up_ctxt : (C.D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a + val fold_down_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 add_abs d l = (D.Abs d) :: l; + fun add_appl d l = (D.AppL d) :: l; + fun add_appr d l = (D.AppR d) :: l; + + fun add_dtrm d l = d::l; + + 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 = Basics.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_up = Basics.fold : (D.dtrm -> 'a -> 'a) -> T -> 'a -> 'a; + val fold_down = Basics.fold_rev : (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; + fun set_trm x = apfst (K x); + fun set_ctxt x = apsnd (K x); + + 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 top_trm = trm o goto_top; + + fun nty_ctxt x = C.nty_ctxt (ctxt x); + fun ty_ctxt x = C.ty_ctxt (ctxt x); + + fun depth_of_ctxt x = C.depth (ctxt x); + fun map_on_ctxt x = apsnd (C.map x); + fun fold_up_ctxt f = C.fold_up f o ctxt; + fun fold_down_ctxt f = C.fold_down 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); + + (* follow the given path down the given zipper *) + (* implicit arguments: C.D.dtrm list, then T *) + val zipto = C.fold_down + (fn C.D.Abs _ => move_down_abs + | C.D.AppL _ => move_down_right + | C.D.AppR _ => move_down_left); + + (* Note: interpretted as being examined depth first *) + datatype zsearch = Here of T | LookIn of T; + + (* lazy search *) + 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_rl; +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);