--- 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"
--- 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 \
--- 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"
--- 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";
--- 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;
--- 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 *)
--- 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;
--- 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);
--- /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).
--- /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;
--- /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 *)
--- /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;
--- /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);