moved to new location in Provers.
--- a/src/Pure/IsaPlanner/ROOT.ML Sun Jun 11 00:28:18 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-(* ID: $Id$
- Author: Lucas Dixon, University of Edinburgh
- lucasd@dai.ed.ac.uk
-
-The IsaPlanner subsystem.
-*)
-
-use "isand.ML";
-use "isaplib.ML";
-use "term_lib.ML";
-use "upterm_lib.ML";
-use "focus_term_lib.ML";
-use "rw_tools.ML";
-use "rw_inst.ML";
-use "isa_fterm.ML";
--- a/src/Pure/IsaPlanner/focus_term_lib.ML Sun Jun 11 00:28:18 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,386 +0,0 @@
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
-(* Title: Pure/IsaPlanner/focus_term_lib.ML
- ID: $Id$
- Author: Lucas Dixon, University of Edinburgh
- lucasd@dai.ed.ac.uk
- Date: 16 April 2003
-*)
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
-(* DESCRIPTION:
-
- Generic Foucs terms (like Zippers), which allows modification and
- manipulation of term keeping track of how we got to the position
- in the term. We provide a signature for terms, ie any kind of
- lamda calculus with abs and application, and some notion of types
- and naming of abstracted vars.
-
- FIXME: at some point in the future make a library to work simply
- with polymorphic upterms - that way if I want to use them without
- the focus part, then I don't need to include all the focus stuff.
-
-*)
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
-
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
-
-(* to endoce and decode general terms into the type needed by focus
-term, this is an easy thing to write, but needs to be done for each
-type that is going to be used with focus terms. *)
-
-signature F_ENCODE_TERM_SIG =
-sig
-
- type term (* type of term to be encoded into TermT for focus term manip *)
- type TypeT (* type annotation for abstractions *)
- type LeafT (* type for other leaf types in term sturcture *)
-
- (* the type to be encoded into *)
- datatype TermT = $ of TermT * TermT
- | Abs of string * TypeT * TermT
- | lf of LeafT
-
- (* the encode and decode functions *)
- val fakebounds : string * TypeT -> term -> term
- val encode : term -> TermT
- val decode : TermT -> term
-
-end;
-
-
-
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
-signature FOCUS_TERM_SIG =
-sig
- structure MinTermS : F_ENCODE_TERM_SIG
-
- exception focus_term_exp of string;
- exception out_of_term_exception of string;
-
- type Term (* = MinTermS.TermT *)
- type Type (* = MinTermS.TypeT *)
-
- type UpTerm (* = (Term,Type) UpTermLib.T *)
-
-(* datatype
- UpTerm =
- abs of string * Type * UpTerm
- | appl of Term * UpTerm
- | appr of Term * UpTerm
- | root *)
-
- datatype FcTerm = focus of Term * UpTerm
-
- (* translating *)
- val fcterm_of_term : MinTermS.term -> FcTerm
- val term_of_fcterm : FcTerm -> MinTermS.term
-
- (* editing/constrution *)
- val enc_appl : (MinTermS.term * UpTerm) -> UpTerm
- val enc_appr : (MinTermS.term * UpTerm) -> UpTerm
-
- (* upterm creatioin *)
- val upterm_of : FcTerm -> UpTerm
- val add_upterm : UpTerm -> FcTerm -> FcTerm
- val mk_term_of_upterm : (MinTermS.term * UpTerm) -> MinTermS.term
- val mk_termf_of_upterm : UpTerm ->
- (((string * Type) list) *
- (MinTermS.term -> MinTermS.term))
- val pure_mk_termf_of_upterm : (MinTermS.term, Type) UpTermLib.T ->
- (((string * Type) list) *
- (MinTermS.term -> MinTermS.term))
-
- (* focusing, throws exceptions *)
- val focus_bot_left_leaf : FcTerm -> FcTerm
- val focus_bot_left_nonabs_leaf : FcTerm -> FcTerm
- val focus_left : FcTerm -> FcTerm
- val focus_strict_left : FcTerm -> FcTerm
- val focus_right : FcTerm -> FcTerm
- val focus_abs : FcTerm -> FcTerm
- val focus_fake_abs : FcTerm -> FcTerm
- val focus_to_top : FcTerm -> FcTerm
- val focus_up : FcTerm -> FcTerm
- val focus_up_right : FcTerm -> FcTerm
- val focus_up_right1 : FcTerm -> FcTerm
-
- (* optional focus changes *)
- val focus_up_abs : FcTerm -> FcTerm option
- val focus_up_appr : FcTerm -> FcTerm option
- val focus_up_appl : FcTerm -> FcTerm option
- val focus_up_abs_or_appr : FcTerm -> FcTerm option
-
- val tyenv_of_focus : FcTerm -> (string * Type) list
- val tyenv_of_focus' : FcTerm -> Type list
-
- (* set/get the focus term *)
- val set_focus_of_fcterm : FcTerm -> MinTermS.term -> FcTerm
- val focus_of_fcterm : FcTerm -> MinTermS.term
-
- (* leaf navigation *)
- val leaf_seq_of_fcterm : FcTerm -> FcTerm Seq.seq
- val next_leaf_fcterm : FcTerm -> FcTerm
- val next_leaf_of_fcterm_seq : FcTerm -> FcTerm Seq.seq
-
- (* analysis *)
- val upsize_of_fcterm : FcTerm -> int
-end;
-
-
-
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
-(*
-
- NOTE!!! I think this can be done in a purely functional way with a
- pair of a term (the focus) and a function, that when applied
- unfocuses one level... maybe think about this as it would be a very
- nice generic consrtuction, without the need for encoding/decoding
- strutcures.
-
-*)
-functor FocusTermFUN(structure EncodeTerm : F_ENCODE_TERM_SIG)
- : FOCUS_TERM_SIG =
-struct
-
-structure MinTermS = EncodeTerm;
-
-local open MinTermS open UpTermLib in
-
- type Term = MinTermS.TermT;
- type Type = MinTermS.TypeT;
-
- exception focus_term_exp of string;
- exception out_of_term_exception of string;
-
- infix 9 $
-
- (* datatype to hold a term tree and the path to where you are in the term *)
-(* datatype UpTerm = root
- | appl of (Term * UpTerm)
- | appr of (Term * UpTerm)
- | abs of (string * Type * UpTerm); *)
-
- type UpTerm = (Term,Type) UpTermLib.T;
-
- fun enc_appl (t,u) = appl((MinTermS.encode t),u);
- fun enc_appr (t,u) = appr((MinTermS.encode t),u);
-
- datatype FcTerm = focus of (Term * UpTerm);
-
- (* the the term of the upterm *)
- fun mk_term_of_upt_aux (t, root) = MinTermS.decode t
- | mk_term_of_upt_aux (t, appl (l,m)) = mk_term_of_upt_aux(l$t, m)
- | mk_term_of_upt_aux (t, appr (r,m)) = mk_term_of_upt_aux(t$r, m)
- | mk_term_of_upt_aux (t, abs (s,ty,m)) = mk_term_of_upt_aux(Abs(s,ty,t),m);
-
- fun mk_term_of_upterm (t, ut) = mk_term_of_upt_aux (MinTermS.encode t, ut);
-
- (* a function version of the above, given an upterm it returns:
- a function on that given a term puts it in the context of the upterm,
- and a list of bound variables that are in the upterm, added as
- we go up - so in reverse order from that typiclaly used by top-down
- parsing of terms. *)
- fun mk_termf_of_upt_aux (f, bs, root) =
- (bs, fn t => MinTermS.decode (f t))
- | mk_termf_of_upt_aux (f, bs, appl (l,m)) =
- mk_termf_of_upt_aux (fn t => l $ (f t), bs, m)
- | mk_termf_of_upt_aux (f, bs, appr (r,m)) =
- mk_termf_of_upt_aux (fn t => (f t) $ r, bs, m)
- | mk_termf_of_upt_aux (f, bs, abs (s,ty,m)) =
- mk_termf_of_upt_aux (fn t => Abs(s,ty,(f t)), (s,ty)::bs, m);
-
- fun mk_termf_of_upterm ut = mk_termf_of_upt_aux (MinTermS.encode, [], ut);
-
-
- fun upterm_of (focus(t, u)) = u;
-
- (* put a new upterm at the start of our current term *)
- fun add_upterm u2 (focus(t, u)) = focus(t, UpTermLib.apply u2 u);
-
-
- (* As above but work on the pure originial upterm type *)
- fun pure_mk_termf_of_upterm ut =
- mk_termf_of_upt_aux
- (encode, [], (map_to_upterm_parts (encode, I) ut));
-
- fun fcterm_of_term t = focus(encode t, root);
-
- fun term_of_fcterm (focus (t, m)) = mk_term_of_upt_aux (t, m);
-
-(* fun term_of_fcterm (focus (t, root)) = mk_term_of_upt_aux (t, root)
- | term_of_fcterm _ = raise focus_term_exp "term_of_fcterm: something bad has happened here."; *)
-
- fun focus_of_fcterm (focus(t, _)) = MinTermS.decode t;
-
- (* replace the focus term with a new term... *)
- fun set_focus_of_fcterm (focus(_, m)) nt = focus(MinTermS.encode nt, m);
-
- fun focus_left (focus(a $ b, m)) = focus(a, appr(b, m))
- | focus_left (focus(Abs(s,ty,t), m)) = focus_left (focus(t, abs(s,ty,m)))
- | focus_left (focus(l, m)) = raise out_of_term_exception "focus_left";
-
- fun focus_strict_left (focus(a $ b, m)) = focus(a, appr(b, m))
- | focus_strict_left (focus(l, m)) = raise out_of_term_exception "focus_left";
-
-(* Note: ":" is standard for faked bound vars... see: EQStepTacTermTools *)
- fun focus_fake_abs (focus(Abs(s,ty,t), m)) =
- let val t' = MinTermS.encode (fakebounds (s,ty) (MinTermS.decode t))
- in focus(t', abs(s,ty,m)) end
- | focus_fake_abs (focus(l, m)) = raise out_of_term_exception "focus_fake_abs";
-
- fun focus_abs (focus(Abs(s,ty,t), m)) = focus(t, abs(s,ty,m))
- | focus_abs (focus(l, m)) = raise out_of_term_exception "focus_abs";
-
-
- fun focus_right (focus(a $ b, m)) = focus(b, appl(a, m))
- | focus_right (focus(Abs(s,ty,t), m)) = focus_right (focus(t, abs(s,ty,m)))
- | focus_right (focus(l, m)) = raise out_of_term_exception "focus_right";
-
- fun focus_up (focus(t, appl(l,m))) = focus(l$t, m)
- | focus_up (focus(t, appr(r,m))) = focus(t$r, m)
- | focus_up (focus(t, abs(s,ty,m))) = focus_up (focus(Abs(s,ty,t), m))
- | focus_up (focus(t, root)) = raise out_of_term_exception "focus_up";
-
- fun focus_to_top t =
- focus_to_top (focus_up t) handle out_of_term_exception _ => t;
-
- (* focus up until you can move right, and then do so *)
- fun focus_up_right (focus(t, appl(l,m))) =
- focus_up_right (focus(l$t, m))
- | focus_up_right (focus(t, appr(r,m))) =
- focus(r, appl(t,m))
- | focus_up_right (focus(t, abs(s,ty,m))) =
- focus_up_right (focus(Abs(s,ty,t), m))
- | focus_up_right (focus(t, root)) =
- raise out_of_term_exception "focus_up_right";
-
- (* as above, but do not move up over a left application *)
- fun focus_up_right1 (focus(t, appl(l,m))) =
- raise out_of_term_exception "focus_up_right1"
- | focus_up_right1 (focus(t, appr(r,m))) =
- focus(r, appl(t,m))
- | focus_up_right1 (focus(t, abs(s,ty,m))) =
- focus_up_right (focus(Abs(s,ty,t), m))
- | focus_up_right1 (focus(t, root)) =
- raise out_of_term_exception "focus_up_right1";
-
- (* move focus to the bottom left through abstractions *)
- fun focus_bot_left_leaf (ft as focus(t, _)) =
- focus_bot_left_leaf (focus_left ft)
- handle out_of_term_exception _=> ft;
-
- (* move focus to the bottom left, but not into abstractions *)
- fun focus_bot_left_nonabs_leaf (ft as focus(t, _)) =
- focus_bot_left_nonabs_leaf (focus_strict_left ft)
- handle out_of_term_exception _=> ft;
-
- (* focus tools for working directly with the focus representation *)
- fun focus_up_appr (focus(t, appl(l,m))) = NONE
- | focus_up_appr (focus(t, appr(r,m))) = SOME (focus(t$r, m))
- | focus_up_appr (focus(t, abs(s,ty,m))) = NONE
- | focus_up_appr (focus(t, root)) = NONE;
-
- fun focus_up_appl (focus(t, appl(l,m))) = SOME (focus(l$t, m))
- | focus_up_appl (focus(t, appr(r,m))) = NONE
- | focus_up_appl (focus(t, abs(s,ty,m))) = NONE
- | focus_up_appl (focus(t, root)) = NONE;
-
- fun focus_up_abs (focus(t, appl(l,m))) = NONE
- | focus_up_abs (focus(t, appr(r,m))) = NONE
- | focus_up_abs (focus(t, abs(s,ty,m))) =
- SOME (focus_up (focus(Abs(s,ty,t), m)))
- | focus_up_abs (focus(t, root)) = NONE;
-
- fun focus_up_abs_or_appr (focus(t, appl(l,m))) = NONE
- | focus_up_abs_or_appr (focus(t, appr(r,m))) = SOME (focus(t$r, m))
- | focus_up_abs_or_appr (focus(t, abs(s,ty,m))) =
- SOME (focus(Abs(s,ty,t), m))
- | focus_up_abs_or_appr (focus(t, root)) = NONE;
-
-
- fun tyenv_of_focus (focus(t, u)) = tyenv_of_upterm u;
- fun tyenv_of_focus' (focus(t, u)) = tyenv_of_upterm' u;
-
- (* return the Term.type of the focus term, computes bound vars type,
- does a quick check only. *)
-(* fun fastype_of_focus (focus(t, m)) =
- let
- fun boundtypes_of_upterm (abs(s,ty,m)) =
- ty::(boundtypes_of_upterm m)
- | boundtypes_of_upterm (appl(t,m)) =
- boundtypes_of_upterm m
- | boundtypes_of_upterm (appr(t,m)) =
- boundtypes_of_upterm m
- | boundtypes_of_upterm (root) = []
- in
- fastype_of1 ((boundtypes_of_upterm m), t)
- end; *)
-
- (* gets the next left hand side term, or throws an exception *)
- fun next_leaf_fcterm ft = focus_bot_left_leaf (focus_up_right ft);
-
- fun next_leaf_of_fcterm_seq_aux t () =
- let val nextt = next_leaf_fcterm t
- in
- SOME (nextt, Seq.make (next_leaf_of_fcterm_seq_aux nextt))
- end handle out_of_term_exception _ => NONE;
-
- (* sequence of next upterms from start upterm...
- ie a sequence of all leafs after this one*)
- fun next_leaf_of_fcterm_seq in_t =
- Seq.make (next_leaf_of_fcterm_seq_aux in_t);
-
- (* returns a sequence of all leaf up terms from term, ie DFS on
- leafs of term, ie uses time O(n), n = sizeof term. *)
- fun leaf_seq_of_fcterm in_t =
- let
- val botleft = (focus_bot_left_leaf in_t)
- in
- Seq.cons botleft (Seq.make (next_leaf_of_fcterm_seq_aux botleft))
- end;
-
- fun upsize_of_fcterm (focus(t, ut)) = upsize_of_upterm ut;
-
-end; (* local *)
-
-end; (* functor *)
-
-
-
-
-
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
-(* focus term encoding sturcture for isabelle terms *)
-structure EncodeIsaFTerm : F_ENCODE_TERM_SIG =
-struct
- infix 9 $;
-
- type term = Term.term;
-
- type TypeT = Term.typ;
-
- datatype LeafT = lConst of string * Term.typ
- | lVar of ((string * int) * Term.typ)
- | lFree of (string * Term.typ)
- | lBound of int;
-
- datatype TermT = op $ of TermT * TermT
- | Abs of string * TypeT * TermT
- | lf of LeafT;
-
- fun fakebounds (s, ty) t = subst_bound (Free(":" ^ s, ty), t);
-
- fun encode (Term.$(a,b)) = (encode a) $ (encode b)
- | encode (Term.Abs(s,ty,t)) = Abs(s,ty,(encode t))
- | encode (Term.Const(s,ty)) = lf(lConst(s,ty))
- | encode (Term.Var((s,i),ty)) = lf(lVar((s,i),ty))
- | encode (Term.Free(s,ty)) = lf(lFree(s,ty))
- | encode (Term.Bound i) = lf(lBound i);
-
- fun decode (a $ b) = Term.$(decode a, decode b)
- | decode (Abs(s,ty,t)) = (Term.Abs(s,ty,decode t))
- | decode (lf(lConst(s,ty))) = Term.Const(s,ty)
- | decode (lf(lVar((s,i),ty))) = Term.Var((s,i),ty)
- | decode (lf(lFree(s,ty))) = (Term.Free(s,ty))
- | decode (lf(lBound i)) = (Term.Bound i);
-
-end;
-
--- a/src/Pure/IsaPlanner/isa_fterm.ML Sun Jun 11 00:28:18 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,543 +0,0 @@
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
-(* Title: Pure/IsaPlanner/isa_fterm.ML
- ID: $Id$
- Author: Lucas Dixon, University of Edinburgh
- lucasd@dai.ed.ac.uk
- Date: 16 April 2003
-*)
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
-(* DESCRIPTION:
-
- Generic Foucs terms (like Zippers) instantiation for Isabelle terms.
-
-*)
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
-
-signature ISA_ENCODE_TERM = (* cf. F_ENCODE_TERM_SIG *)
-sig
- type term
- type typ
- type LeafT
- datatype TermT = $ of TermT * TermT
- | Abs of string * typ * TermT
- | lf of LeafT
- val fakebounds : string * typ -> term -> term
- val encode : term -> TermT
- val decode : TermT -> term
-end;
-
-(* signature BASIC_ISA_FTERM =
-FOCUS_TERM_SIG where type Term = ISA_ENCODE_TERM.Term *)
-
-signature ISA_FTERM =
- sig
- type Term (*= EncodeIsaFTerm.TermT*)
- type Type (*= Term.typ*)
- type UpTerm
- datatype FcTerm = focus of Term * UpTerm
- structure MinTermS : F_ENCODE_TERM_SIG
- val add_upterm :
- UpTerm -> FcTerm -> FcTerm
- val clean_match_ft :
- theory ->
- Term.term ->
- FcTerm ->
- (
- ((Term.indexname * (Term.sort * Term.typ)) list
- * (Term.indexname * (Term.typ * Term.term)) list)
- * (string * Term.typ) list
- * (string * Term.typ) list
- * Term.term)
- option
- val clean_unify_ft :
- theory ->
- int ->
- Term.term ->
- FcTerm ->
- (
- ((Term.indexname * (Term.sort * Term.typ)) list
- * (Term.indexname * (Term.typ * Term.term)) list)
- * (string * Term.typ) list * (string * Term.typ) list * Term.term)
- Seq.seq
- val enc_appl :
- EncodeIsaFTerm.term * UpTerm -> UpTerm
- val enc_appr :
- EncodeIsaFTerm.term * UpTerm -> UpTerm
-
- val fcterm_of_term : EncodeIsaFTerm.term -> FcTerm
- val find_fcterm_matches :
- ((FcTerm -> 'a) -> FcTerm -> 'b) ->
- (FcTerm -> 'a) -> FcTerm -> 'b
- val find_sg_concl_matches :
- ((FcTerm -> 'a) -> FcTerm -> 'b) ->
- (FcTerm -> 'a) -> int -> EncodeIsaFTerm.term -> 'b
- val find_sg_concl_thm_matches :
- ((FcTerm -> 'a) -> FcTerm -> 'b) ->
- (FcTerm -> 'a) -> int -> Thm.thm -> 'b
- val find_sg_matches :
- ((FcTerm -> 'a) -> FcTerm -> 'b) ->
- (FcTerm -> 'a) -> int -> EncodeIsaFTerm.term -> 'b
- val find_sg_thm_matches :
- ((FcTerm -> 'a) -> FcTerm -> 'b) ->
- (FcTerm -> 'a) -> int -> Thm.thm -> 'b
- val focus_abs : FcTerm -> FcTerm
- val focus_bot_left_leaf : FcTerm -> FcTerm
- val focus_bot_left_nonabs_leaf :
- FcTerm -> FcTerm
- val focus_fake_abs : FcTerm -> FcTerm
- val focus_left : FcTerm -> FcTerm
- val focus_of_fcterm : FcTerm -> EncodeIsaFTerm.term
- val focus_right : FcTerm -> FcTerm
- val focus_strict_left : FcTerm -> FcTerm
- exception focus_term_exp of string
- val focus_to_concl : FcTerm -> FcTerm
- val focus_to_concl_of_term : EncodeIsaFTerm.term -> FcTerm
- val focus_to_dest_impl :
- FcTerm -> FcTerm * FcTerm
- val focus_to_subgoal :
- int -> FcTerm -> FcTerm
- val focus_to_subgoal_of_term :
- int -> EncodeIsaFTerm.term -> FcTerm
- val focus_to_term_goal_prem :
- int * int -> EncodeIsaFTerm.term -> FcTerm
- val focus_to_top : FcTerm -> FcTerm
- val focus_up : FcTerm -> FcTerm
- val focus_up_abs : FcTerm -> FcTerm option
- val focus_up_abs_or_appr :
- FcTerm -> FcTerm option
- val focus_up_appl : FcTerm -> FcTerm option
- val focus_up_appr : FcTerm -> FcTerm option
- val focus_up_right : FcTerm -> FcTerm
- val focus_up_right1 : FcTerm -> FcTerm
- val focuseq_to_subgoals :
- FcTerm -> FcTerm Seq.seq
- exception isa_focus_term_exp of string
- val leaf_seq_of_fcterm :
- FcTerm -> FcTerm Seq.seq
- val mk_term_of_upterm :
- EncodeIsaFTerm.term * UpTerm -> EncodeIsaFTerm.term
- val mk_termf_of_upterm :
- UpTerm ->
- (string * Type) list *
- (EncodeIsaFTerm.term -> EncodeIsaFTerm.term)
- val next_leaf_fcterm : FcTerm -> FcTerm
- val next_leaf_of_fcterm_seq :
- FcTerm -> FcTerm Seq.seq
- exception out_of_term_exception of string
-
- val pure_mk_termf_of_upterm :
- (EncodeIsaFTerm.term, Type) UpTermLib.T ->
- (string * Type) list *
- (EncodeIsaFTerm.term -> EncodeIsaFTerm.term)
- val search_all_bl_ru_f :
- (FcTerm -> 'a Seq.seq) ->
- FcTerm -> 'a Seq.seq
- val search_all_bl_ur_f :
- (FcTerm -> 'a Seq.seq) ->
- FcTerm -> 'a Seq.seq
- val search_tlr_all_f :
- (FcTerm -> 'a Seq.seq) ->
- FcTerm -> 'a Seq.seq
- val search_tlr_valid_f :
- (FcTerm -> 'a Seq.seq) ->
- FcTerm -> 'a Seq.seq
- val search_valid_bl_ru_f :
- (FcTerm -> 'a Seq.seq) ->
- FcTerm -> 'a Seq.seq
- val search_valid_bl_ur_f :
- (FcTerm -> 'a Seq.seq) ->
- FcTerm -> 'a Seq.seq
- val set_focus_of_fcterm :
- FcTerm -> EncodeIsaFTerm.term -> FcTerm
- val term_of_fcterm : FcTerm -> EncodeIsaFTerm.term
- val tyenv_of_focus :
- FcTerm -> (string * Type) list
- val tyenv_of_focus' : FcTerm -> Type list
- val upsize_of_fcterm : FcTerm -> int
- val upterm_of : FcTerm -> UpTerm
- val valid_match_start : FcTerm -> bool
-
- (* pre-matching/pre-unification *)
- val fakefree_badbounds :
- (string * Term.typ) list -> Term.term ->
- (string * Term.typ) list * (string * Term.typ) list * Term.term
- val mk_foo_match :
- (Term.term -> Term.term) ->
- ('a * Term.typ) list -> Term.term -> Term.term
- val prepmatch :
- FcTerm ->
- Term.term *
- ((string * Term.typ) list * (string * Term.typ) list * Term.term)
-
-
- val pretty : Theory.theory -> FcTerm -> Pretty.T
-
- end;
-
-
-
-structure BasicIsaFTerm =
-FocusTermFUN( structure EncodeTerm = EncodeIsaFTerm);
-
-(* HOL Dependent *)
-structure IsaFTerm : ISA_FTERM=
-struct
-
-(* include BasicIsaFTerm *)
-(* open FocusTermFUN( structure EncodeTerm = EncodeIsaFTerm ); *)
-
-open BasicIsaFTerm;
-
-
-(* Some general search within a focus term... *)
-
-(* Note: only upterms with a free or constant are going to yeald a
-match, thus if we get anything else (bound or var) skip it! This is
-important if we switch to a unification net! in particular to avoid
-vars. *)
-
-fun valid_match_start ft =
- (case TermLib.bot_left_leaf_of (focus_of_fcterm ft) of
- Const _ => true
- | Free _ => true
- | Abs _ => true (* allowed to look inside abs... search decides if we actually consider the abstraction itself *)
- | _ => false); (* avoid vars - always suceeds uninterestingly. *)
-
-(* match starting at the bottom left, moving up to top of the term,
- then moving right to the next leaf and up again etc *)
-(* FIXME: make properly lazy! *)
-fun search_valid_bl_ur_f f ft =
- let
- val fts =
- Seq.filter valid_match_start
- (leaf_seq_of_fcterm ft)
-
- fun mk_match_up_seq ft =
- (* avoid abstractions? - possibly infinite unifiers? *)
- let val hereseq = case (focus_of_fcterm ft) of
- Abs _ => Seq.empty
- | _ => f ft
- in
- case focus_up_abs_or_appr ft of
- SOME ft' => Seq.append(hereseq, mk_match_up_seq ft')
- | NONE => hereseq
- end
- in
- Seq.flat (Seq.map mk_match_up_seq fts)
- end;
-
-fun search_all_bl_ur_f f ft =
- let
- val fts = (leaf_seq_of_fcterm ft)
-
- fun mk_match_up_seq ft =
- case focus_up_abs_or_appr ft of
- SOME ft' => Seq.append(f ft, mk_match_up_seq ft')
- | NONE => f ft
- in
- Seq.flat (Seq.map mk_match_up_seq fts)
- end;
-
-
-(* FIXME: make properly lazy! *)
-(* FIXME: make faking of bound vars local - for speeeeed *)
-fun search_valid_bl_ru_f f ft =
- let
- fun mauxtop ft =
- if (valid_match_start ft)
- then maux ft else Seq.empty
- and maux ft =
- let val t' = (focus_of_fcterm ft)
- (* val _ = writeln ("Examining: " ^ (TermLib.string_of_term t')) *)
- in
- (case t' of
- (_ $ _) => Seq.append (maux (focus_left ft),
- Seq.append(mauxtop (focus_right ft),
- f ft))
- | (Abs _) => maux (focus_abs ft)
- | leaf => f ft) end
- in
- mauxtop ft
- end;
-
-
-fun search_all_bl_ru_f f ft =
- let
- fun maux ft =
- let val t' = (focus_of_fcterm ft)
- (* val _ = writeln ("Examining: " ^ (TermLib.string_of_term t')) *)
- in
- (case t' of
- (_ $ _) => Seq.append (maux (focus_left ft),
- Seq.append(maux (focus_right ft),
- f ft))
- | (Abs _) => Seq.append (maux (focus_abs ft),
- f ft)
- | leaf => f ft) end
- in maux ft end;
-
-(* search from top, left to right, then down *)
-fun search_tlr_all_f f ft =
- let
- fun maux ft =
- let val t' = (focus_of_fcterm ft)
- (* val _ =
- if !trace_subst_search then
- (writeln ("Examining: " ^ (TermLib.string_of_term t'));
- TermLib.writeterm t'; ())
- else (); *)
- in
- (case t' of
- (_ $ _) => Seq.append(maux (focus_left ft),
- Seq.append(f ft,
- maux (focus_right ft)))
- | (Abs _) => Seq.append(f ft, maux (focus_abs ft))
- | leaf => f ft) end
- in maux ft end;
-
-fun search_tlr_valid_f f ft =
- let
- fun maux ft =
- let
- val hereseq = if valid_match_start ft then f ft else Seq.empty
- in
- (case (focus_of_fcterm ft) of
- (_ $ _) => Seq.append(maux (focus_left ft),
- Seq.append(hereseq,
- maux (focus_right ft)))
- | (Abs _) => Seq.append(hereseq, maux (focus_abs ft))
- | leaf => hereseq)
- end
- in maux ft end;
-
-
-
-exception isa_focus_term_exp of string;
-
-
-fun focus_to_dest_impl ft =
- let val (lhs, rhs) =
- Logic.dest_implies (focus_of_fcterm ft)
- in (focus_left ft, focus_right ft) end
- handle Term.TERM _ =>
- raise isa_focus_term_exp
- "focus_to_dest_impl: applied to non implication";
-
-
-(* move focus to the conlusion *)
-fun focus_to_concl ft =
- let val (lhs, rhs) =
- Logic.dest_implies (focus_of_fcterm ft)
- in focus_to_concl (focus_right ft) end
- handle Term.TERM _ => ft;
-
-val focus_to_concl_of_term = focus_to_concl o fcterm_of_term;
-
-
-
-(* give back sequence of focuses at different subgoals *)
-(* FIXME: make truly lazy *)
-fun focuseq_to_subgoals ft =
- if (Logic.is_implies (focus_of_fcterm ft)) then
- Seq.cons (focus_right (focus_left ft)) (focuseq_to_subgoals (focus_right ft))
- else
- Seq.empty;
-
-(* move focus to a specific subgoal, 0 is first *)
-fun focus_to_subgoal j ft =
- let fun focus_to_subgoal' (ft, 0) =
- let val (lhs, rhs) = Logic.dest_implies (focus_of_fcterm ft)
- in ft |> focus_left |> focus_right end
- | focus_to_subgoal' (ft, i) =
- let val (lhs, rhs) = Logic.dest_implies (focus_of_fcterm ft)
- in focus_to_subgoal' (focus_right ft, i - 1) end
- in focus_to_subgoal' (ft, j - 1) end
- handle Term.TERM _ =>
- raise isa_focus_term_exp
- ("focus_to_subgoal: No such subgoal: " ^
- (string_of_int j));
-
-fun focus_to_subgoal_of_term i t =
- focus_to_subgoal i (fcterm_of_term t)
-
-(* move focus to a specific premise *)
-(* fun focus_past_params i ft =
- (focus_to_subgoal (focus_right ft, i))
- handle isa_focus_term_exp _ =>
- raise isa_focus_term_exp
- ("focus_to_prmise: No such premise: " ^ (string_of_int i)); *)
-
-fun focus_to_term_goal_prem (premid,gaolid) t =
- focus_to_subgoal premid (focus_to_subgoal_of_term gaolid t);
-
-
-
-(* FIXME: make a sturcture for holding free variable names and making
-them distinct --- ? maybe part of the new prooftree datatype ?
-Alos: use this to fix below... *)
-
-(* T is outer bound vars, n is number of locally bound vars *)
-(* THINK: is order of Ts correct...? or reversed? *)
-fun fakefree_badbounds Ts t =
- let val (FakeTs,Ts,newnames) =
- List.foldr (fn ((n,ty),(FakeTs,Ts,usednames)) =>
- let val newname = Term.variant usednames n
- in ((RWTools.mk_fake_bound_name newname,ty)::FakeTs,
- (newname,ty)::Ts,
- newname::usednames) end)
- ([],[],[])
- Ts
- in (FakeTs, Ts, Term.subst_bounds (map Free FakeTs, t)) end;
-
-(* fun fakefree_badbounds usednames T n (a $ b) = *)
-(* let val (usednames', T', a') = fakefree_badbounds usednames T n a *)
-(* val (usednames'', T'', b') = fakefree_badbounds usednames' T n b in *)
-(* (usednames'', T'', a' $ b') end *)
-(* | fakefree_badbounds usednames T n (Abs(s,ty,t)) = *)
-(* let val (usednames', T', t') = fakefree_badbounds usednames T (n + 1) t in *)
-(* (usednames', T', Abs(s,ty, t')) *)
-(* | fakefree_badbounds usednames T n (b as Bound i) = *)
-(* let fun mkfake_bound j [] = *)
-(* raise ERROR_MESSAGE "fakefree_badbounds: bound is outside of the known types!" *)
-(* | mkfake_bound 0 ((s,ty)::Ts) = *)
-(* let val newname = Term.variant s usednames in *)
-(* usednames, (newname,ty) :: T, Free (newname,ty) *)
-(* | mkfake_bound j (d::Ts) = mkfake_bound (j - 1) Ts *)
-(* in if n <= i then mkfake_bound (i - n) T else b end *)
-(* | fakefree_badbounds usednames T t = t; *)
-
-
-(* note: outerterm is the taget with the match replaced by a bound
- variable : ie: "P lhs" beocmes "%x. P x"
- insts is the types of instantiations of vars in lhs
- and typinsts is the type instantiations of types in the lhs
- Note: Final rule is the rule lifted into the ontext of the
- taget thm. *)
-fun mk_foo_match mkuptermfunc Ts t =
- let
- val ty = Term.type_of t
- val bigtype = (rev (map snd Ts)) ---> ty
- fun mk_foo 0 t = t
- | mk_foo i t = mk_foo (i - 1) (t $ (Bound (i - 1)))
- val num_of_bnds = (length Ts)
- (* foo_term = "fooabs y0 ... yn" where y's are local bounds *)
- val foo_term = mk_foo num_of_bnds (Bound num_of_bnds)
- in Abs("fooabs", bigtype, mkuptermfunc foo_term) end;
-
-(* before matching we need to fake the bound vars that are missing an
-abstraction. In this function we additionally construct the
-abstraction environment, and an outer context term (with the focus
-abstracted out) for use in rewriting with RWInst.rw *)
-fun prepmatch ft =
- let
- val t = focus_of_fcterm ft
- val Ts = tyenv_of_focus ft
- val (FakeTs', Ts', t') = fakefree_badbounds Ts t
- fun mktermf t =
- term_of_fcterm (set_focus_of_fcterm ft t)
- val absterm = mk_foo_match mktermf Ts' t'
- in
- (t', (FakeTs', Ts', absterm))
- end;
-
-
-fun pretty thy ft =
- let val (t', (_,_,absterm)) = prepmatch ft in
- Pretty.chunks
- [ Pretty.block [Pretty.str "(Abs:",
- Pretty.quote (Display.pretty_cterm (Thm.cterm_of thy absterm)),
- Pretty.str ","],
- Pretty.block [Pretty.str " Foc:",
- Pretty.quote (Display.pretty_cterm (Thm.cterm_of thy t')),
- Pretty.str ")" ] ]
- end;
-
-(*
- Pretty.str "no yet implemented";
- Display.pretty_cterm (Thm.cterm_of t)
- Term.Free ("FOCUS", Term.type_of t)
-*)
-
-
-(* matching and unification for a focus term's focus *)
-
-(* Note: Ts is a modified version of the original names of the outer
-bound variables. New names have been introduced to make sure they are
-unique w.r.t all names in the term and each other. usednames' is
-oldnames + new names. *)
-fun clean_match_ft thy pat ft =
- let val (t, (FakeTs,Ts,absterm)) = prepmatch ft in
- case TermLib.clean_match thy (pat, t) of
- NONE => NONE
- | SOME insts => SOME (insts, FakeTs, Ts, absterm) end;
-(* ix = max var index *)
-fun clean_unify_ft sgn ix pat ft =
- let val (t, (FakeTs, Ts,absterm)) = prepmatch ft in
- Seq.map (fn insts => (insts, FakeTs, Ts, absterm))
- (TermLib.clean_unify sgn ix (t, pat)) end;
-
-
-(* THINK: ? do we not need to incremement bound indices? *)
-(* THINK: it should be the search which localisaes the search to the
-current focus, not this hack in the matcher... ? *)
-(* find matches below this particular focus term *)
-(* The search function is to find a match within a term... *)
-(* the matcher is something that is applied to each node chosen by the
-searchf and the results are flattened to form a lazy list. *)
-fun find_fcterm_matches searchf matcher ft =
- let
- val ftupterm = upterm_of ft
- val focusft = focus_of_fcterm ft
- val add_uptermf = add_upterm ftupterm
- in
- searchf
- (fn ft' => matcher (add_uptermf ft'))
- (fcterm_of_term focusft)
- end;
-
-(* FIXME: move argument orders for efficiency...
-i.e. wenzel style val foofunc = x o y;
-*)
-
-(* find the matches inside subgoal i of th *)
-fun find_sg_matches searchf matcher i t =
- let
- val subgoal_fcterm = focus_to_subgoal_of_term i t
- in find_fcterm_matches searchf matcher subgoal_fcterm end;
-
-(* find the matches inside subgoal i of th *)
-fun find_sg_thm_matches searchf matcher i th =
- find_sg_matches searchf matcher i (Thm.prop_of th);
-
-
-(* find the matches inside subgoal i's conclusion of th *)
-fun find_sg_concl_matches searchf matcher i t =
- let
- val subgoal_fcterm =
- focus_to_concl (focus_to_subgoal_of_term i t)
- in
- find_fcterm_matches searchf matcher subgoal_fcterm
- end;
-
-(* find the matches inside subgoal i's conclusion of th *)
-fun find_sg_concl_thm_matches searchf matcher i th =
- find_sg_concl_matches searchf matcher i (Thm.prop_of th);
-
-end;
-
-(*
-test...
-
-f_encode_isatermS.encode (read "P a");
-isafocustermS.fcterm_of_term (read "f a");
-isafocustermS.term_of_fcterm it;
-
-Goal "P b ==> P (suc b)";
-
-TermLib.string_of_term ((focus_of_fcterm o focus_to_subgoal_of_term 1 o prop_of) (topthm()));
-
-TermLib.string_of_term ((focus_of_fcterm o focus_to_concl o focus_to_subgoal_of_term 1 o prop_of) (topthm()));
-
-TermLib.string_of_term ((focus_of_fcterm o focus_to_term_goal_prem (1,1) o prop_of) (topthm()));
-
-*)
--- a/src/Pure/IsaPlanner/isand.ML Sun Jun 11 00:28:18 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,644 +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.
-
- debugging tools:
-
- fun asm_mk t = (assume (cterm_of (Theory.sign_of (the_context())) t));
- fun asm_read s =
- (assume (read_cterm (Theory.sign_of (Context.the_context())) (s,propT)));
-
- THINK: are we really ok with our varify name w.r.t the prop - do
- we also need to avoid names in the hidden hyps? What about
- unification contraints in flex-flex pairs - might they also have
- extra free vars?
-*)
-
-signature ISA_ND =
-sig
-
- (* export data *)
- datatype export = export of
- {gth: Thm.thm, (* initial goal theorem *)
- sgid: int, (* subgoal id which has been fixed etc *)
- fixes: Thm.cterm list, (* frees *)
- assumes: Thm.cterm list} (* assumptions *)
- val fixes_of_exp : export -> Thm.cterm list
- val export_back : export -> Thm.thm -> Thm.thm Seq.seq
- val export_solution : export -> Thm.thm -> Thm.thm
- val export_solutions : export list * Thm.thm -> Thm.thm
-
- (* inserting meta level params for frees in the conditions *)
- val allify_conditions :
- (Term.term -> Thm.cterm) ->
- (string * Term.typ) list -> Thm.thm -> Thm.thm * Thm.cterm list
- val allify_conditions' :
- (string * Term.typ) list -> Thm.thm -> Thm.thm * Thm.cterm list
- val assume_allified :
- theory -> (string * Term.sort) list * (string * Term.typ) list
- -> Term.term -> (Thm.cterm * Thm.thm)
-
- (* meta level fixed params (i.e. !! vars) *)
- val fix_alls_in_term : Term.term -> Term.term * Term.term list
- val fix_alls_term : int -> Term.term -> Term.term * Term.term list
- val fix_alls_cterm : int -> Thm.thm -> Thm.cterm * Thm.cterm list
- val fix_alls' : int -> Thm.thm -> Thm.thm * Thm.cterm list
- val fix_alls : int -> Thm.thm -> Thm.thm * export
-
- (* meta variables in types and terms *)
- val fix_tvars_to_tfrees_in_terms
- : string list (* avoid these names *)
- -> Term.term list ->
- (((string * int) * Term.sort) * (string * Term.sort)) list (* renamings *)
- val fix_vars_to_frees_in_terms
- : string list (* avoid these names *)
- -> Term.term list ->
- (((string * int) * Term.typ) * (string * Term.typ)) list (* renamings *)
- val fix_tvars_to_tfrees : Thm.thm -> Thm.ctyp list * Thm.thm
- val fix_vars_to_frees : Thm.thm -> Thm.cterm list * Thm.thm
- val fix_vars_and_tvars :
- Thm.thm -> (Thm.cterm list * Thm.ctyp list) * Thm.thm
- val fix_vars_upto_idx : int -> Thm.thm -> Thm.thm
- val fix_tvars_upto_idx : int -> Thm.thm -> Thm.thm
- val unfix_frees : Thm.cterm list -> Thm.thm -> Thm.thm
- val unfix_tfrees : Thm.ctyp list -> Thm.thm -> Thm.thm
- val unfix_frees_and_tfrees :
- (Thm.cterm list * Thm.ctyp list) -> Thm.thm -> Thm.thm
-
- (* assumptions/subgoals *)
- val assume_prems :
- int -> Thm.thm -> Thm.thm list * Thm.thm * Thm.cterm list
- val fixed_subgoal_thms : Thm.thm -> Thm.thm list * (Thm.thm list -> Thm.thm)
- val fixes_and_assumes : int -> Thm.thm -> Thm.thm list * Thm.thm * export
- val hide_other_goals : Thm.thm -> Thm.thm * Thm.cterm list
- val hide_prems : Thm.thm -> Thm.thm * Thm.cterm list
-
- (* abstracts cterms (vars) to locally meta-all bounds *)
- val prepare_goal_export : string list * Thm.cterm list -> Thm.thm
- -> int * Thm.thm
- val solve_with : Thm.thm -> Thm.thm -> Thm.thm Seq.seq
- val subgoal_thms : Thm.thm -> Thm.thm list * (Thm.thm list -> Thm.thm)
-end
-
-
-structure IsaND
-: ISA_ND
-= struct
-
-(* Solve *some* subgoal of "th" directly by "sol" *)
-(* Note: this is probably what Markus ment to do upon export of a
-"show" but maybe he used RS/rtac instead, which would wrongly lead to
-failing if there are premices to the shown goal.
-
-given:
-sol : Thm.thm = [| Ai... |] ==> Ci
-th : Thm.thm =
- [| ... [| Ai... |] ==> Ci ... |] ==> G
-results in:
- [| ... [| Ai-1... |] ==> Ci-1
- [| Ai+1... |] ==> Ci+1 ...
- |] ==> G
-i.e. solves some subgoal of th that is identical to sol.
-*)
-fun solve_with sol th =
- let fun solvei 0 = Seq.empty
- | solvei i =
- Seq.append (bicompose false (false,sol,0) i th,
- solvei (i - 1))
- in
- solvei (Thm.nprems_of th)
- end;
-
-
-(* Given ctertmify function, (string,type) pairs capturing the free
-vars that need to be allified in the assumption, and a theorem with
-assumptions possibly containing the free vars, then we give back the
-assumptions allified as hidden hyps.
-
-Given: x
-th: A vs ==> B vs
-Results in: "B vs" [!!x. A x]
-*)
-fun allify_conditions ctermify Ts th =
- let
- val premts = Thm.prems_of th;
-
- fun allify_prem_var (vt as (n,ty),t) =
- (Term.all ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
-
- fun allify_prem Ts p = foldr allify_prem_var p Ts
-
- val cTs = map (ctermify o Free) Ts
- val cterm_asms = map (ctermify o allify_prem Ts) premts
- val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms
- in
- (Library.foldl (fn (x,y) => y COMP x) (th, allifyied_asm_thms), cterm_asms)
- end;
-
-fun allify_conditions' Ts th =
- allify_conditions (Thm.cterm_of (Thm.sign_of_thm th)) Ts th;
-
-(* allify types *)
-fun allify_typ ts ty =
- let
- fun trec (x as (TFree (s,srt))) =
- (case Library.find_first (fn (s2,srt2) => s = s2) ts
- of NONE => x
- | SOME (s2,_) => TVar ((s,0),srt))
- (* Maybe add in check here for bad sorts?
- if srt = srt2 then TVar ((s,0),srt)
- else raise ("thaw_typ", ts, ty) *)
- | trec (Type (s,typs)) = Type (s, map trec typs)
- | trec (v as TVar _) = v;
- in trec ty end;
-
-(* implicit types and term *)
-fun allify_term_typs ty = Term.map_term_types (allify_typ ty);
-
-(* allified version of term, given frees to allify over. Note that we
-only allify over the types on the given allified cterm, we can't do
-this for the theorem as we are not allowed type-vars in the hyp. *)
-fun assume_allified sgn (tyvs,vs) t =
- let
- fun allify_var (vt as (n,ty),t) =
- (Term.all ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
- fun allify Ts p = List.foldr allify_var p Ts
-
- val ctermify = Thm.cterm_of sgn;
- val cvars = map (fn (n,ty) => ctermify (Var ((n,0),ty))) vs
- val allified_term = t |> allify vs;
- val ct = ctermify allified_term;
- val typ_allified_ct = ctermify (allify_term_typs tyvs allified_term);
- in (typ_allified_ct,
- Drule.forall_elim_vars 0 (Thm.assume ct)) end;
-
-
-(* change type-vars to fresh type frees *)
-fun fix_tvars_to_tfrees_in_terms names ts =
- let
- val tfree_names = map fst (List.foldr Term.add_term_tfrees [] ts);
- val tvars = List.foldr Term.add_term_tvars [] ts;
- val (names',renamings) =
- List.foldr (fn (tv as ((n,i),s),(Ns,Rs)) =>
- let val n2 = Term.variant Ns n in
- (n2::Ns, (tv, (n2,s))::Rs)
- end) (tfree_names @ names,[]) tvars;
- in renamings end;
-fun fix_tvars_to_tfrees th =
- let
- val sign = Thm.sign_of_thm th;
- val ctypify = Thm.ctyp_of sign;
- val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
- val renamings = fix_tvars_to_tfrees_in_terms
- [] ((Thm.prop_of th) :: tpairs);
- val crenamings =
- map (fn (v,f) => (ctypify (TVar v), ctypify (TFree f)))
- renamings;
- val fixedfrees = map snd crenamings;
- in (fixedfrees, Thm.instantiate (crenamings, []) th) end;
-
-
-(* change type-free's to type-vars *)
-fun unfix_tfrees ns th =
- let
- val varfiytfrees = (map (fn x => Term.dest_TFree (Thm.typ_of x)) 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 *)
-fun fix_vars_to_frees_in_terms names ts =
- let
- val vars = map Term.dest_Var (List.foldr Term.add_term_vars [] ts);
- val Ns = List.foldr Term.add_term_names names ts;
- val (_,renamings) =
- Library.foldl (fn ((Ns,Rs),v as ((n,i),ty)) =>
- let val n2 = Term.variant Ns n in
- (n2 :: Ns, (v, (n2,ty)) :: Rs)
- end) ((Ns,[]), vars);
- in renamings end;
-fun fix_vars_to_frees th =
- let
- val ctermify = Thm.cterm_of (Thm.sign_of_thm th)
- val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
- val renamings = fix_vars_to_frees_in_terms
- [] ([Thm.prop_of th] @ tpairs);
- val crenamings =
- map (fn (v,f) => (ctermify (Var v), ctermify (Free f)))
- renamings;
- val fixedfrees = map snd crenamings;
- in (fixedfrees, Thm.instantiate ([], crenamings) th) end;
-
-fun fix_tvars_upto_idx ix th =
- let
- val sgn = Thm.sign_of_thm th;
- val ctypify = Thm.ctyp_of sgn
- val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
- val prop = (Thm.prop_of th);
- val tvars = List.foldr Term.add_term_tvars [] (prop :: tpairs);
- val ctyfixes =
- map_filter
- (fn (v as ((s,i),ty)) =>
- if i <= ix then SOME (ctypify (TVar v), ctypify (TFree (s,ty)))
- else NONE) tvars;
- in Thm.instantiate (ctyfixes, []) th end;
-fun fix_vars_upto_idx ix th =
- let
- val sgn = Thm.sign_of_thm th;
- val ctermify = Thm.cterm_of sgn
- val tpairs = Thm.terms_of_tpairs (Thm.tpairs_of th);
- val prop = (Thm.prop_of th);
- val vars = map Term.dest_Var (List.foldr Term.add_term_vars
- [] (prop :: tpairs));
- val cfixes =
- map_filter
- (fn (v as ((s,i),ty)) =>
- if i <= ix then SOME (ctermify (Var v), ctermify (Free (s,ty)))
- else NONE) vars;
- in Thm.instantiate ([], cfixes) th end;
-
-
-(* make free vars into schematic vars with index zero *)
- fun unfix_frees frees =
- apply (map (K (Drule.forall_elim_var 0)) frees)
- o Drule.forall_intr_list frees;
-
-(* fix term and type variables *)
-fun fix_vars_and_tvars th =
- let val (tvars, th') = fix_tvars_to_tfrees th
- val (vars, th'') = fix_vars_to_frees th'
- in ((vars, tvars), th'') end;
-
-(* implicit Thm.thm argument *)
-(* assumes: vars may contain fixed versions of the frees *)
-(* THINK: what if vs already has types varified? *)
-fun unfix_frees_and_tfrees (vs,tvs) =
- (unfix_tfrees tvs o unfix_frees vs);
-
-(* datatype to capture an exported result, ie a fix or assume. *)
-datatype export =
- export of {fixes : Thm.cterm list, (* fixed vars *)
- assumes : Thm.cterm list, (* hidden hyps/assumed prems *)
- sgid : int,
- gth : Thm.thm}; (* subgoal/goalthm *)
-
-fun fixes_of_exp (export rep) = #fixes rep;
-
-(* export the result of the new goal thm, ie if we reduced teh
-subgoal, then we get a new reduced subtgoal with the old
-all-quantified variables *)
-local
-
-(* allify puts in a meta level univ quantifier for a free variavble *)
-fun allify_term (v, t) =
- let val vt = #t (Thm.rep_cterm v)
- val (n,ty) = Term.dest_Free vt
- in (Term.all ty) $ (Abs(n,ty,Term.abstract_over (vt, t))) end;
-
-fun allify_for_sg_term ctermify vs t =
- let val t_alls = foldr allify_term t vs;
- val ct_alls = ctermify t_alls;
- in
- (ct_alls, Drule.forall_elim_list vs (Thm.assume ct_alls))
- end;
-(* lookup type of a free var name from a list *)
-fun lookupfree vs vn =
- case Library.find_first (fn (n,ty) => n = vn) vs of
- NONE => error ("prepare_goal_export:lookupfree: " ^ vn ^ " does not occur in the term")
- | SOME x => x;
-in
-fun export_back (export {fixes = vs, assumes = hprems,
- sgid = i, gth = gth}) newth =
- let
- val sgn = Thm.sign_of_thm newth;
- val ctermify = Thm.cterm_of sgn;
-
- val sgs = prems_of newth;
- val (sgallcts, sgthms) =
- Library.split_list (map (allify_for_sg_term ctermify vs) sgs);
- val minimal_newth =
- (Library.foldl (fn ( newth', sgthm) =>
- Drule.compose_single (sgthm, 1, newth'))
- (newth, sgthms));
- val allified_newth =
- minimal_newth
- |> Drule.implies_intr_list hprems
- |> Drule.forall_intr_list vs
-
- val newth' = Drule.implies_intr_list sgallcts allified_newth
- in
- bicompose false (false, newth', (length sgallcts)) i gth
- end;
-
-(*
-Given "vs" : names of free variables to abstract over,
-Given cterms : premices to abstract over (P1... Pn) in terms of vs,
-Given a thm of the form:
-P1 vs; ...; Pn vs ==> Goal(C vs)
-
-Gives back:
-(n, length of given cterms which have been allified
- [| !! vs. P1 vs; !! vs. Pn vs |] ==> !! C vs) the allified thm
-*)
-(* note: C may contain further premices etc
-Note that cterms is the assumed facts, ie prems of "P1" that are
-reintroduced in allified form.
-*)
-fun prepare_goal_export (vs, cterms) th =
- let
- val sgn = Thm.sign_of_thm th;
- val ctermify = Thm.cterm_of sgn;
-
- val allfrees = map Term.dest_Free (Term.term_frees (Thm.prop_of th))
- val cfrees = map (ctermify o Free o lookupfree allfrees) vs
-
- val sgs = prems_of th;
- val (sgallcts, sgthms) =
- Library.split_list (map (allify_for_sg_term ctermify cfrees) sgs);
-
- val minimal_th =
- Goal.conclude (Library.foldl (fn ( th', sgthm) =>
- Drule.compose_single (sgthm, 1, th'))
- (th, sgthms));
-
- val allified_th =
- minimal_th
- |> Drule.implies_intr_list cterms
- |> Drule.forall_intr_list cfrees
-
- val th' = Drule.implies_intr_list sgallcts allified_th
- in
- ((length sgallcts), th')
- end;
-
-end;
-
-
-(* exporting function that takes a solution to the fixed/assumed goal,
-and uses this to solve the subgoal in the main theorem *)
-fun export_solution (export {fixes = cfvs, assumes = hcprems,
- sgid = i, gth = gth}) solth =
- let
- val solth' =
- solth |> Drule.implies_intr_list hcprems
- |> Drule.forall_intr_list cfvs
- in Drule.compose_single (solth', i, gth) end;
-
-fun export_solutions (xs,th) = foldr (uncurry export_solution) th xs;
-
-
-(* fix parameters of a subgoal "i", as free variables, and create an
-exporting function that will use the result of this proved goal to
-show the goal in the original theorem.
-
-Note, an advantage of this over Isar is that it supports instantiation
-of unkowns in the earlier theorem, ie we can do instantiation of meta
-vars!
-
-avoids constant, free and vars names.
-
-loosely corresponds to:
-Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm
-Result:
- ("(As ==> SGi x') ==> (As ==> SGi x')" : thm,
- expf :
- ("As ==> SGi x'" : thm) ->
- ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm)
-*)
-fun fix_alls_in_term alledt =
- let
- val t = Term.strip_all_body alledt;
- val alls = rev (Term.strip_all_vars alledt);
- val varnames = map (fst o fst o Term.dest_Var) (Term.term_vars t)
- val names = Term.add_term_names (t,varnames);
- val fvs = map Free
- ((Term.variantlist (map fst alls, names))
- ~~ (map snd alls));
- in ((subst_bounds (fvs,t)), fvs) end;
-
-fun fix_alls_term i t =
- let
- val varnames = map (fst o fst o Term.dest_Var) (Term.term_vars t)
- val names = Term.add_term_names (t,varnames);
- val gt = Logic.get_goal t i;
- val body = Term.strip_all_body gt;
- val alls = rev (Term.strip_all_vars gt);
- val fvs = map Free
- ((Term.variantlist (map fst alls, names))
- ~~ (map snd alls));
- in ((subst_bounds (fvs,body)), fvs) end;
-
-fun fix_alls_cterm i th =
- let
- val ctermify = Thm.cterm_of (Thm.sign_of_thm th);
- val (fixedbody, fvs) = fix_alls_term i (Thm.prop_of th);
- val cfvs = rev (map ctermify fvs);
- val ct_body = ctermify fixedbody
- in
- (ct_body, cfvs)
- end;
-
-fun fix_alls' i =
- (apfst Thm.trivial) o (fix_alls_cterm i);
-
-
-(* hide other goals *)
-(* note the export goal is rotated by (i - 1) and will have to be
-unrotated to get backto the originial position(s) *)
-fun hide_other_goals th =
- let
- (* tl beacuse fst sg is the goal we are interested in *)
- val cprems = tl (Drule.cprems_of th)
- val aprems = map Thm.assume cprems
- in
- (Drule.implies_elim_list (Drule.rotate_prems 1 th) aprems,
- cprems)
- end;
-
-(* a nicer version of the above that leaves only a single subgoal (the
-other subgoals are hidden hyps, that the exporter suffles about)
-namely the subgoal that we were trying to solve. *)
-(* loosely corresponds to:
-Given "[| SG0; ... !! x. As ==> SGi x; ... SGm |] ==> G" : thm
-Result:
- ("(As ==> SGi x') ==> SGi x'" : thm,
- expf :
- ("SGi x'" : thm) ->
- ("[| SG0; ... SGi-1; SGi+1; ... SGm |] ==> G") : thm)
-*)
-fun fix_alls i th =
- let
- val (fixed_gth, fixedvars) = fix_alls' i th
- val (sml_gth, othergoals) = hide_other_goals fixed_gth
- in
- (sml_gth, export {fixes = fixedvars,
- assumes = othergoals,
- sgid = i, gth = th})
- end;
-
-
-(* assume the premises of subgoal "i", this gives back a list of
-assumed theorems that are the premices of subgoal i, it also gives
-back a new goal thm and an exporter, the new goalthm is as the old
-one, but without the premices, and the exporter will use a proof of
-the new goalthm, possibly using the assumed premices, to shoe the
-orginial goal.
-
-Note: Dealing with meta vars, need to meta-level-all them in the
-shyps, which we can later instantiate with a specific value.... ?
-think about this... maybe need to introduce some new fixed vars and
-then remove them again at the end... like I do with rw_inst.
-
-loosely corresponds to:
-Given "[| SG0; ... [| A0; ... An |] ==> SGi; ... SGm |] ==> G" : thm
-Result:
-(["A0" [A0], ... ,"An" [An]] : thm list, -- assumptions
- "SGi ==> SGi" : thm, -- new goal
- "SGi" ["A0" ... "An"] : thm -> -- export function
- ("[| SG0 ... SGi-1, SGi+1, SGm |] ==> G" : thm) list)
-*)
-fun assume_prems i th =
- let
- val t = (prop_of th);
- val gt = Logic.get_goal t i;
- val _ = case Term.strip_all_vars gt of [] => ()
- | _ => error "assume_prems: goal has params"
- val body = gt;
- val prems = Logic.strip_imp_prems body;
- val concl = Logic.strip_imp_concl body;
-
- val sgn = Thm.sign_of_thm th;
- val ctermify = Thm.cterm_of sgn;
- val cprems = map ctermify prems;
- val aprems = map Thm.assume cprems;
- val gthi = Thm.trivial (ctermify concl);
-
- (* fun explortf thi =
- Drule.compose (Drule.implies_intr_list cprems thi,
- i, th) *)
- in
- (aprems, gthi, cprems)
- end;
-
-
-(* first fix the variables, then assume the assumptions *)
-(* loosely corresponds to:
-Given
- "[| SG0; ...
- !! xs. [| A0 xs; ... An xs |] ==> SGi xs;
- ... SGm |] ==> G" : thm
-Result:
-(["A0 xs'" [A0 xs'], ... ,"An xs'" [An xs']] : thm list, -- assumptions
- "SGi xs' ==> SGi xs'" : thm, -- new goal
- "SGi xs'" ["A0 xs'" ... "An xs'"] : thm -> -- export function
- ("[| SG0 ... SGi-1, SGi+1, SGm |] ==> G" : thm) list)
-*)
-
-(* Note: the fix_alls actually pulls through all the assumptions which
-means that the second export is not needed. *)
-fun fixes_and_assumes i th =
- let
- val (fixgth, exp1) = fix_alls i th
- val (assumps, goalth, _) = assume_prems 1 fixgth
- in
- (assumps, goalth, exp1)
- end;
-
-
-(* Fixme: allow different order of subgoals given to expf *)
-(* make each subgoal into a separate thm that needs to be proved *)
-(* loosely corresponds to:
-Given
- "[| SG0; ... SGm |] ==> G" : thm
-Result:
-(["SG0 ==> SG0", ... ,"SGm ==> SGm"] : thm list, -- goals
- ["SG0", ..., "SGm"] : thm list -> -- export function
- "G" : thm)
-*)
-fun subgoal_thms th =
- let
- val t = (prop_of th);
-
- val prems = Logic.strip_imp_prems t;
-
- val sgn = Thm.sign_of_thm th;
- val ctermify = Thm.cterm_of sgn;
-
- val aprems = map (Thm.trivial o ctermify) prems;
-
- fun explortf premths =
- Drule.implies_elim_list th premths
- in
- (aprems, explortf)
- end;
-
-
-(* make all the premices of a theorem hidden, and provide an unhide
-function, that will bring them back out at a later point. This is
-useful if you want to get back these premices, after having used the
-theorem with the premices hidden *)
-(* loosely corresponds to:
-Given "As ==> G" : thm
-Result: ("G [As]" : thm,
- "G [As]" : thm -> "As ==> G" : thm
-*)
-fun hide_prems th =
- let
- val cprems = Drule.cprems_of th;
- val aprems = map Thm.assume cprems;
- (* val unhidef = Drule.implies_intr_list cprems; *)
- in
- (Drule.implies_elim_list th aprems, cprems)
- end;
-
-
-
-
-(* Fixme: allow different order of subgoals in exportf *)
-(* as above, but also fix all parameters in all subgoals, and uses
-fix_alls, not fix_alls', ie doesn't leave extra asumptions as apparent
-subgoals. *)
-(* loosely corresponds to:
-Given
- "[| !! x0s. A0s x0s ==> SG0 x0s;
- ...; !! xms. Ams xms ==> SGm xms|] ==> G" : thm
-Result:
-(["(A0s x0s' ==> SG0 x0s') ==> SG0 x0s'",
- ... ,"(Ams xms' ==> SGm xms') ==> SGm xms'"] : thm list, -- goals
- ["SG0 x0s'", ..., "SGm xms'"] : thm list -> -- export function
- "G" : thm)
-*)
-(* requires being given solutions! *)
-fun fixed_subgoal_thms th =
- let
- val (subgoals, expf) = subgoal_thms th;
-(* fun export_sg (th, exp) = exp th; *)
- fun export_sgs expfs solthms =
- expf (map2 (curry (op |>)) solthms expfs);
-(* expf (map export_sg (ths ~~ expfs)); *)
- in
- apsnd export_sgs (Library.split_list (map (apsnd export_solution o
- fix_alls 1) subgoals))
- end;
-
-end;
--- a/src/Pure/IsaPlanner/isaplib.ML Sun Jun 11 00:28:18 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,317 +0,0 @@
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
-(* Title: Pure/IsaPlanner/isaplib.ML
- ID: $Id$
- Author: Lucas Dixon, University of Edinburgh
- lucasd@dai.ed.ac.uk
-*)
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
-(* DESCRIPTION:
-
- A few useful system-independent utilities.
-*)
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
-signature ISAP_LIB =
-sig
- (* seq operations *)
- val ALL_BUT_LAST : ('a -> 'b Seq.seq) -> 'a -> 'b Seq.seq
- val FST : ('a -> 'b Seq.seq) -> 'a -> 'b Seq.seq
- val NTH : int -> ('a -> 'b Seq.seq) -> 'a -> 'b Seq.seq
- val all_but_last_of_seq : 'a Seq.seq -> 'a Seq.seq
- val nat_seq : int Seq.seq
- val nth_of_seq : int -> 'a Seq.seq -> 'a option
- val pair_seq : 'a Seq.seq -> 'b Seq.seq -> ('a * 'b) Seq.seq
- val number_seq : 'a Seq.seq -> (int * 'a) Seq.seq
-
- datatype 'a skipseqT =
- skipmore of int
- | skipseq of 'a Seq.seq Seq.seq;
- val skipto_seqseq : int -> 'a Seq.seq Seq.seq -> 'a skipseqT
- val seqflat_seq : 'a Seq.seq Seq.seq -> 'a Seq.seq
-
- (* lists *)
- val mk_num_list : int -> int list
- val number_list : int -> 'a list -> (int * 'a) list
- val repeated_list : int -> 'a -> 'a list
- val all_pairs : 'a list -> 'b list -> ('a * 'b) list
- val get_ends_of : ('a * 'a -> bool) ->
- ('a * 'a) -> 'a list -> ('a * 'a)
- val flatmap : ('a -> 'b list) -> 'a list -> 'b list
-
- val lrem : ('a * 'b -> bool) -> 'a list -> 'b list -> 'b list
- val forall_list : ('a -> bool) -> 'a list -> bool
-
- (* the list of lists with one of each of the original sublists *)
- val one_of_each : 'a list list -> 'a list list
-
- (* type changing *)
- exception NOT_A_DIGIT of string
- val int_of_string : string -> int
-
- (* string manipulations *)
- val remove_end_spaces : string -> string
- val str_indent : string -> string
- val string_of_intlist : int list -> string
- val string_of_list : ('a -> string) -> 'a list -> string
-
- (* options *)
- val aptosome : 'a option -> ('a -> 'b) -> 'b option
- val seq_mapfilter : ('a -> 'b option) -> 'a Seq.seq -> 'b Seq.seq
- val seq_map_to_some_filter : ('a -> 'b) -> 'a option Seq.seq
- -> 'b Seq.seq
-end;
-
-
-
-structure IsaPLib : ISAP_LIB =
-struct
-
-(* Seq *)
-fun seq_map_to_some_filter f = Seq.map_filter (Option.map f);
-fun seq_mapfilter f = Seq.map_filter f;
-
-(* the sequence of natural numbers *)
-val nat_seq =
- let fun nseq i () = SOME (i, Seq.make (nseq (i+1)))
- in Seq.make (nseq 1)
- end;
-
-(* a simple function to pair with each element of a list, a number *)
-fun number_list i [] = []
- | number_list i (h::t) =
- (i,h)::(number_list (i+1) t)
-
-(* create a sequence of pairs of the elements of the two sequences
- If one sequence becomes empty, then so does the pairing of them.
-
- This is particularly useful if you wish to perform counting or
- other repeated operations on a sequence and you want to combvine
- this infinite sequence with a possibly finite one.
-
- behaviour:
- s1: a1, a2, ... an
- s2: b1, b2, ... bn ...
-
- pair_seq s1 s2: (a1,b1), (a2,b2), ... (an,bn)
-*)
-fun pair_seq seq1 seq2 =
- let
- fun pseq s1 s2 () =
- case Seq.pull s1 of
- NONE => NONE
- | SOME (s1h, s1t) =>
- case Seq.pull s2 of
- NONE => NONE
- | SOME (s2h, s2t) =>
- SOME ((s1h, s2h), Seq.make (pseq s1t s2t))
- in
- Seq.make (pseq seq1 seq2)
- end;
-
-(* number a sequence *)
-fun number_seq s = pair_seq nat_seq s;
-
-(* cuts off the last element of a sequence *)
-fun all_but_last_of_seq s =
- let
- fun f () =
- case Seq.pull s of
- NONE => NONE
- | SOME (a, s2) =>
- (case Seq.pull s2 of
- NONE => NONE
- | SOME (a2,s3) =>
- SOME (a, all_but_last_of_seq (Seq.cons a2 s3)))
- in
- Seq.make f
- end;
-
- fun ALL_BUT_LAST r st = all_but_last_of_seq (r st);
-
-
- (* nth elem for sequenes, return none if out of bounds *)
- fun nth_of_seq i l =
- (case Seq.pull l of
- NONE => NONE
- | SOME (x, xq) =>
- if i <= 1 then SOME x
- else nth_of_seq (i - 1) xq);
-
- (* for use with tactics... gives no_tac if element isn't there *)
- fun NTH n f st =
- (case nth_of_seq n (f st) of
- NONE => Seq.empty
- | SOME r => Seq.single r);
-
- (* First result of a tactic... uses NTH, so if there is no elements,
-
- then no_tac is returned. *)
- fun FST f = NTH 1 f;
-
-datatype 'a skipseqT = skipmore of int
- | skipseq of 'a Seq.seq Seq.seq;
-(* given a seqseq, skip the first m non-empty seq's *)
-fun skipto_seqseq m s =
- let
- fun skip_occs n sq =
- case Seq.pull sq of
- NONE => skipmore n
- | SOME (h,t) =>
- (case Seq.pull h of NONE => skip_occs n t
- | SOME _ => if n <= 1 then skipseq (Seq.cons h t)
- else skip_occs (n - 1) t)
- in (skip_occs m s) end;
-
-(* handy function for re-arranging Sequence operations *)
-(* [[a,b,c],[d,e],...] => flatten [[a,d,...], [b,e,...], [c, ...]] *)
-fun seqflat_seq ss =
- let
- fun pulltl LL () =
- (case Seq.pull LL of
- NONE => NONE
- | SOME (hL,tLL) =>
- (case Seq.pull hL of
- NONE => pulltl tLL ()
- | SOME (h,tL) =>
- SOME (h, Seq.make (recf (tLL, (Seq.single tL))))))
- and recf (fstLL,sndLL) () =
- (case Seq.pull fstLL of
- NONE => pulltl sndLL ()
- | SOME (hL, tLL) =>
- (case Seq.pull hL of
- NONE => recf (tLL, sndLL) ()
- | SOME (h,tL) =>
- SOME (h, Seq.make (recf (tLL, Seq.append (sndLL, Seq.single tL))))))
- in Seq.make (pulltl ss) end;
-(* tested with:
-val ss = Seq.of_list [Seq.of_list [1,2,3], Seq.of_list [4,5], Seq.of_list [7,8,9,10]];
-Seq.list_of (seqflat_seq ss);
-val it = [1, 4, 7, 2, 5, 8, 3, 9, 10] : int list
-*)
-
-
-
- (* create a list opf the form (n, n-1, n-2, ... ) *)
- fun mk_num_list n =
- if n < 1 then [] else (n :: (mk_num_list (n-1)));
-
- fun repeated_list n a =
- if n < 1 then [] else (a :: (repeated_list (n-1) a));
-
- (* create all possible pairs with fst element from the first list
- and snd element from teh second list *)
- fun all_pairs xs ys =
- let
- fun all_pairs_aux yss [] _ acc = acc
- | all_pairs_aux yss (x::xs) [] acc =
- all_pairs_aux yss xs yss acc
- | all_pairs_aux yss (xs as (x1::x1s)) (y::ys) acc =
- all_pairs_aux yss xs ys ((x1,y)::acc)
- in
- all_pairs_aux ys xs ys []
- end;
-
-
- (* create all possible pairs with fst element from the first list
- and snd element from teh second list *)
- (* FIXME: make tail recursive and quick *)
- fun one_of_each [] = []
- | one_of_each [[]] = []
- | one_of_each [(h::t)] = [h] :: (one_of_each [t])
- | one_of_each ([] :: xs) = []
- | one_of_each ((h :: t) :: xs) =
- (map (fn z => h :: z) (one_of_each xs))
- @ (one_of_each (t :: xs));
-
-
-(* function to get the upper/lower bounds of a list
-given:
-gr : 'a * 'a -> bool = greater than check
-e as (u,l) : ('a * 'a) = upper and lower bits
-l : 'a list = the list to get the upper and lower bounds of
-returns a pair ('a * 'a) of the biggest and lowest value w.r.t "gr"
-*)
-fun get_ends_of gr (e as (u,l)) [] = e
- | get_ends_of gr (e as (u,l)) (h :: t) =
- if gr(h,u) then get_ends_of gr (h,l) t
- else if gr(l,h) then get_ends_of gr (u,h) t
- else get_ends_of gr (u,l) t;
-
-fun flatmap f = maps f;
-
- (* quick removal of "rs" elements from "ls" when (eqf (r,l)) is true
- Ignores ordering. *)
- fun lrem eqf rs ls =
- let fun list_remove rs ([],[]) = []
- | list_remove [] (xs,_) = xs
- | list_remove (r::rs) ([],leftovers) =
- list_remove rs (leftovers,[])
- | list_remove (r1::rs) ((x::xs),leftovers) =
- if eqf (r1, x) then list_remove (r1::rs) (xs,leftovers)
- else list_remove (r1::rs) (xs, x::leftovers)
- in
- list_remove rs (ls,[])
- end;
-
-fun forall_list f [] = true
- | forall_list f (a::t) = f a orelse forall_list f t;
-
-
- (* crappy string indeter *)
- fun str_indent s =
- implode (map (fn s => if s = "\n" then "\n " else s) (explode s));
-
-
- fun remove_end_spaces s =
- let
- fun rem_starts [] = []
- | rem_starts (" " :: t) = rem_starts t
- | rem_starts ("\t" :: t) = rem_starts t
- | rem_starts ("\n" :: t) = rem_starts t
- | rem_starts l = l
- fun rem_ends l = rev (rem_starts (rev l))
- in
- implode (rem_ends (rem_starts (explode s)))
- end;
-
-(* convert a string to an integer *)
- exception NOT_A_DIGIT of string;
-
- fun int_of_string s =
- let
- fun digits_to_int [] x = x
- | digits_to_int (h :: t) x = digits_to_int t (x * 10 + h);
-
- fun char_to_digit c =
- case c of
- "0" => 0
- | "1" => 1
- | "2" => 2
- | "3" => 3
- | "4" => 4
- | "5" => 5
- | "6" => 6
- | "7" => 7
- | "8" => 8
- | "9" => 9
- | _ => raise NOT_A_DIGIT c
- in
- digits_to_int (map char_to_digit (explode (remove_end_spaces s))) 0
- end;
-
- (* Debugging/printing code for this datatype *)
- fun string_of_list f l =
- let
- fun auxf [] = ""
- | auxf [a] = (f a)
- | auxf (h :: (t as (h2 :: t2))) = (f h) ^ ", " ^ (auxf t)
- in
- "[" ^ (auxf l) ^ "]"
- end;
-
- val string_of_intlist = string_of_list string_of_int;
-
-
- (* options *)
- fun aptosome opt f = Option.map f opt;
-
-end;
--- a/src/Pure/IsaPlanner/rw_inst.ML Sun Jun 11 00:28:18 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,304 +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;
-
-(* Given a list of variables that were bound, and a that has been
-instantiated with free variable placeholders for the bound vars, it
-creates an abstracted version of the theorem, with local bound vars as
-lambda-params:
-
-Ts:
-("x", ty)
-
-rule::
-C :x ==> P :x = Q :x
-
-results in:
-("!! x. C x", (%x. p x = %y. p y) [!! x. C x])
-
-note: assumes rule is instantiated
-*)
-(* Note, we take abstraction in the order of last abstraction first *)
-fun mk_abstractedrule TsFake Ts rule =
- let
- val ctermify = Thm.cterm_of (Thm.sign_of_thm rule);
-
- (* now we change the names of temporary free vars that represent
- bound vars with binders outside the redex *)
- val prop = Thm.prop_of rule;
- val names = TermLib.usednames_of_thm rule;
- val (fromnames,tonames,names2,Ts') =
- Library.foldl (fn ((rnf,rnt,names, Ts''),((faken,_),(n,ty))) =>
- let val n2 = Term.variant names n in
- (ctermify (Free(faken,ty)) :: rnf,
- ctermify (Free(n2,ty)) :: rnt,
- n2 :: names,
- (n2,ty) :: Ts'')
- end)
- (([],[],names, []), TsFake~~Ts);
-
- (* rename conflicting free's in the rule to avoid cconflicts
- with introduced vars from bounds outside in redex *)
- val rule' = rule |> Drule.forall_intr_list fromnames
- |> Drule.forall_elim_list tonames;
-
- (* make unconditional rule and prems *)
- val (uncond_rule, cprems) = IsaND.allify_conditions ctermify (rev Ts')
- rule';
-
- (* using these names create lambda-abstracted version of the rule *)
- val abstractions = rev (Ts' ~~ tonames);
- val abstract_rule = Library.foldl (fn (th,((n,ty),ct)) =>
- Thm.abstract_rule n ct th)
- (uncond_rule, abstractions);
- in (cprems, abstract_rule) end;
-
-
-(* given names to avoid, and vars that need to be fixed, it gives
-unique new names to the vars so that they can be fixed as free
-variables *)
-(* make fixed unique free variable instantiations for non-ground vars *)
-(* Create a table of vars to be renamed after instantiation - ie
- other uninstantiated vars in the hyps of the rule
- ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *)
-fun mk_renamings tgt rule_inst =
- let
- val rule_conds = Thm.prems_of rule_inst
- val names = foldr Term.add_term_names [] (tgt :: rule_conds);
- val (conds_tyvs,cond_vs) =
- Library.foldl (fn ((tyvs, vs), t) =>
- (Library.union
- (Term.term_tvars t, tyvs),
- Library.union
- (map Term.dest_Var (Term.term_vars t), vs)))
- (([],[]), rule_conds);
- val termvars = map Term.dest_Var (Term.term_vars tgt);
- val vars_to_fix = Library.union (termvars, cond_vs);
- val (renamings, names2) =
- foldr (fn (((n,i),ty), (vs, names')) =>
- let val n' = Term.variant names' n in
- ((((n,i),ty), Free (n', ty)) :: vs, n'::names')
- end)
- ([], names) vars_to_fix;
- in renamings end;
-
-(* make a new fresh typefree instantiation for the given tvar *)
-fun new_tfree (tv as (ix,sort), (pairs,used)) =
- let val v = variant used (string_of_indexname ix)
- in ((ix,(sort,TFree(v,sort)))::pairs, v::used) end;
-
-
-(* make instantiations to fix type variables that are not
- already instantiated (in ignore_ixs) from the list of terms. *)
-fun mk_fixtvar_tyinsts ignore_insts ts =
- let
- val ignore_ixs = map fst ignore_insts;
- val (tvars, tfrees) =
- foldr (fn (t, (varixs, tfrees)) =>
- (Term.add_term_tvars (t,varixs),
- Term.add_term_tfrees (t,tfrees)))
- ([],[]) ts;
- val unfixed_tvars =
- List.filter (fn (ix,s) => not (ix mem ignore_ixs)) tvars;
- val (fixtyinsts, _) = foldr new_tfree ([], map fst tfrees) unfixed_tvars
- in (fixtyinsts, tfrees) end;
-
-
-(* cross-instantiate the instantiations - ie for each instantiation
-replace all occurances in other instantiations - no loops are possible
-and thus only one-parsing of the instantiations is necessary. *)
-fun cross_inst insts =
- let
- fun instL (ix, (ty,t)) =
- map (fn (ix2,(ty2,t2)) =>
- (ix2, (ty2,Term.subst_vars ([], [(ix, t)]) t2)));
-
- fun cross_instL ([], l) = rev l
- | cross_instL ((ix, t) :: insts, l) =
- cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l));
-
- in cross_instL (insts, []) end;
-
-(* as above but for types -- I don't know if this is needed, will we ever incur mixed up types? *)
-fun cross_inst_typs insts =
- let
- fun instL (ix, (srt,ty)) =
- map (fn (ix2,(srt2,ty2)) =>
- (ix2, (srt2,Term.typ_subst_TVars [(ix, ty)] ty2)));
-
- fun cross_instL ([], l) = rev l
- | cross_instL ((ix, t) :: insts, l) =
- cross_instL (instL (ix, t) insts, (ix, t) :: (instL (ix, t) l));
-
- in cross_instL (insts, []) end;
-
-
-(* assume that rule and target_thm have distinct var names. THINK:
-efficient version with tables for vars for: target vars, introduced
-vars, and rule vars, for quicker instantiation? The outerterm defines
-which part of the target_thm was modified. Note: we take Ts in the
-upterm order, ie last abstraction first., and with an outeterm where
-the abstracted subterm has the arguments in the revered order, ie
-first abstraction first. FakeTs has abstractions using the fake name
-- ie the name distinct from all other abstractions. *)
-
-fun rw ((nonfixed_typinsts, unprepinsts), FakeTs, Ts, outerterm) rule target_thm =
- let
- (* general signature info *)
- val target_sign = (Thm.sign_of_thm target_thm);
- val ctermify = Thm.cterm_of target_sign;
- val ctypeify = Thm.ctyp_of target_sign;
-
- (* fix all non-instantiated tvars *)
- val (fixtyinsts, othertfrees) =
- mk_fixtvar_tyinsts nonfixed_typinsts
- [Thm.prop_of rule, Thm.prop_of target_thm];
- val new_fixed_typs = map (fn ((s,i),(srt,ty)) => (Term.dest_TFree ty))
- fixtyinsts;
- val typinsts = cross_inst_typs (nonfixed_typinsts @ fixtyinsts);
-
- (* certified instantiations for types *)
- val ctyp_insts =
- map (fn (ix,(s,ty)) => (ctypeify (TVar (ix,s)), ctypeify ty))
- typinsts;
-
- (* type instantiated versions *)
- val tgt_th_tyinst = Thm.instantiate (ctyp_insts,[]) target_thm;
- val rule_tyinst = Thm.instantiate (ctyp_insts,[]) rule;
-
- val term_typ_inst = map (fn (ix,(srt,ty)) => (ix,ty)) typinsts;
- (* type instanitated outer term *)
- val outerterm_tyinst = Term.subst_TVars term_typ_inst outerterm;
-
- val FakeTs_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst))
- FakeTs;
- val Ts_tyinst = map (apsnd (Term.typ_subst_TVars term_typ_inst))
- Ts;
-
- (* type-instantiate the var instantiations *)
- val insts_tyinst = foldr (fn ((ix,(ty,t)),insts_tyinst) =>
- (ix, (Term.typ_subst_TVars term_typ_inst ty,
- Term.subst_TVars term_typ_inst t))
- :: insts_tyinst)
- [] unprepinsts;
-
- (* cross-instantiate *)
- val insts_tyinst_inst = cross_inst insts_tyinst;
-
- (* create certms of instantiations *)
- val cinsts_tyinst =
- map (fn (ix,(ty,t)) => (ctermify (Var (ix, ty)),
- ctermify t)) insts_tyinst_inst;
-
- (* The instantiated rule *)
- val rule_inst = rule_tyinst |> Thm.instantiate ([], cinsts_tyinst);
-
- (* Create a table of vars to be renamed after instantiation - ie
- other uninstantiated vars in the hyps the *instantiated* rule
- ie ?z in C ?z ?x ==> A ?x ?y = B ?x ?y *)
- val renamings = mk_renamings (Thm.prop_of tgt_th_tyinst)
- rule_inst;
- val cterm_renamings =
- map (fn (x,y) => (ctermify (Var x), ctermify y)) renamings;
-
- (* Create the specific version of the rule for this target application *)
- val outerterm_inst =
- outerterm_tyinst
- |> Term.subst_Vars (map (fn (ix,(ty,t)) => (ix,t)) insts_tyinst_inst)
- |> Term.subst_Vars (map (fn ((ix,ty),t) => (ix,t)) renamings);
- val couter_inst = Thm.reflexive (ctermify outerterm_inst);
- val (cprems, abstract_rule_inst) =
- rule_inst |> Thm.instantiate ([], cterm_renamings)
- |> mk_abstractedrule FakeTs_tyinst Ts_tyinst;
- val specific_tgt_rule =
- beta_eta_contract
- (Thm.combination couter_inst abstract_rule_inst);
-
- (* create an instantiated version of the target thm *)
- val tgt_th_inst =
- tgt_th_tyinst |> Thm.instantiate ([], cinsts_tyinst)
- |> Thm.instantiate ([], cterm_renamings);
-
- val (vars,frees_of_fixed_vars) = Library.split_list cterm_renamings;
-
- in
- (beta_eta_contract tgt_th_inst)
- |> Thm.equal_elim specific_tgt_rule
- |> Drule.implies_intr_list cprems
- |> Drule.forall_intr_list frees_of_fixed_vars
- |> Drule.forall_elim_list vars
- |> Thm.varifyT' othertfrees
- |-> K Drule.zero_var_indexes
- end;
-
-
-end; (* struct *)
--- a/src/Pure/IsaPlanner/rw_tools.ML Sun Jun 11 00:28:18 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,195 +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
-
-(* THINKABOUT: don't need this: should be able to generate the paired
- NsTs directly ? --already implemented as ~~
-fun join_lists ([],[]) = []
- | join_lists (x::xs, y::ys) = (x,y) :: (join_lists (xs,ys))
- | join_lists (_, _) = raise ERROR_MESSAGE "join_lists: unequal size lists";
- *)
-
-(* fake free variable names for locally bound variables - these work
-as placeholders. *)
-
-(* don't use dest_fake.. - we should instead be working with numbers
-and a list... else we rely on naming conventions which can break, or
-be violated - in contrast list locations are correct by
-construction/definition. *)
-(*
-fun dest_fake_bound_name n =
- case (explode n) of
- (":" :: realchars) => implode realchars
- | _ => n; *)
-fun is_fake_bound_name n = (hd (explode n) = ":");
-fun mk_fake_bound_name n = ":b_" ^ n;
-
-
-
-(* fake free variable names for local meta variables - these work
-as placeholders. *)
-fun dest_fake_fix_name n =
- case (explode n) of
- ("@" :: realchars) => implode realchars
- | _ => n;
-fun is_fake_fix_name n = (hd (explode n) = "@");
-fun mk_fake_fix_name n = "@" ^ n;
-
-
-
-(* fake free variable names for meta level bound variables *)
-fun dest_fake_all_name n =
- case (explode n) of
- ("+" :: realchars) => implode realchars
- | _ => n;
-fun is_fake_all_name n = (hd (explode n) = "+");
-fun mk_fake_all_name n = "+" ^ n;
-
-
-
-
-(* Ys and Ts not used, Ns are real names of faked local bounds, the
-idea is that this will be mapped to free variables thus if a free
-variable is a faked local bound then we change it to being a meta
-variable so that it can later be instantiated *)
-(* FIXME: rename this - avoid the word fix! *)
-(* note we are not really "fix"'ing the free, more like making it variable! *)
-(* fun trymkvar_of_fakefree (Ns, Ts) Ys (n,ty) =
- if n mem Ns then Var((n,0),ty) else Free (n,ty);
-*)
-
-(* make a var into a fixed free (ie prefixed with "@") *)
-fun mk_fakefixvar Ts ((n,i),ty) = Free(mk_fake_fix_name n, ty);
-
-
-(* mk_frees_bound: string list -> Term.term -> Term.term *)
-(* This function changes free variables to being represented as bound
-variables if the free's variable name is in the given list. The debruijn
-index is simply the position in the list *)
-(* THINKABOUT: danger of an existing free variable with the same name: fix
-this so that name conflict are avoided automatically! In the meantime,
-don't have free variables named starting with a ":" *)
-fun bounds_of_fakefrees Ys (a $ b) =
- (bounds_of_fakefrees Ys a) $ (bounds_of_fakefrees Ys b)
- | bounds_of_fakefrees Ys (Abs(n,ty,t)) =
- Abs(n,ty, bounds_of_fakefrees (n::Ys) t)
- | bounds_of_fakefrees Ys (Free (n,ty)) =
- let fun try_mk_bound_of_free (i,[]) = Free (n,ty)
- | try_mk_bound_of_free (i,(y::ys)) =
- if n = y then Bound i else try_mk_bound_of_free (i+1,ys)
- in try_mk_bound_of_free (0,Ys) end
- | bounds_of_fakefrees Ys t = t;
-
-
-(* map a function f onto each free variables *)
-fun map_to_frees f Ys (a $ b) =
- (map_to_frees f Ys a) $ (map_to_frees f Ys b)
- | map_to_frees f Ys (Abs(n,ty,t)) =
- Abs(n,ty, map_to_frees f ((n,ty)::Ys) t)
- | map_to_frees f Ys (Free a) =
- f Ys a
- | map_to_frees f Ys t = t;
-
-
-(* map a function f onto each meta variable *)
-fun map_to_vars f Ys (a $ b) =
- (map_to_vars f Ys a) $ (map_to_vars f Ys b)
- | map_to_vars f Ys (Abs(n,ty,t)) =
- Abs(n,ty, map_to_vars f ((n,ty)::Ys) t)
- | map_to_vars f Ys (Var a) =
- f Ys a
- | map_to_vars f Ys t = t;
-
-(* map a function f onto each free variables *)
-fun map_to_alls f (Const("all",allty) $ Abs(n,ty,t)) =
- let val (n2,ty2) = f (n,ty)
- in (Const("all",allty) $ Abs(n2,ty2,map_to_alls f t)) end
- | map_to_alls f x = x;
-
-(* map a function f to each type variable in a term *)
-(* implicit arg: term *)
-fun map_to_term_tvars f =
- Term.map_term_types (fn TVar(ix,ty) => f (ix,ty) | x => x);
-
-
-
-(* what if a param desn't occur in the concl? think about! Note: This
-simply fixes meta level univ bound vars as Frees. At the end, we will
-change them back to schematic vars that will then unify
-appropriactely, ie with unfake_vars *)
-fun fake_concl_of_goal gt i =
- let
- val prems = Logic.strip_imp_prems gt
- val sgt = List.nth (prems, i - 1)
-
- val tbody = Logic.strip_imp_concl (Term.strip_all_body sgt)
- val tparams = Term.strip_all_vars sgt
-
- val fakefrees = map (fn (n, ty) => Free(mk_fake_all_name n, ty))
- tparams
- in
- Term.subst_bounds (rev fakefrees,tbody)
- end;
-
-(* what if a param desn't occur in the concl? think about! Note: This
-simply fixes meta level univ bound vars as Frees. At the end, we will
-change them back to schematic vars that will then unify
-appropriactely, ie with unfake_vars *)
-fun fake_goal gt i =
- let
- val prems = Logic.strip_imp_prems gt
- val sgt = List.nth (prems, i - 1)
-
- val tbody = Term.strip_all_body sgt
- val tparams = Term.strip_all_vars sgt
-
- val fakefrees = map (fn (n, ty) => Free(mk_fake_all_name n, ty))
- tparams
- in
- Term.subst_bounds (rev fakefrees,tbody)
- end;
-
-
-(* hand written - for some reason the Isabelle version in drule is broken!
-Example? something to do with Bin Yangs examples?
- *)
-fun rename_term_bvars ns (Abs(s,ty,t)) =
- let val s2opt = Library.find_first (fn (x,y) => s = x) ns
- in case s2opt of
- NONE => (Abs(s,ty,rename_term_bvars ns t))
- | SOME (_,s2) => Abs(s2,ty, rename_term_bvars ns t) end
- | rename_term_bvars ns (a$b) =
- (rename_term_bvars ns a) $ (rename_term_bvars ns b)
- | rename_term_bvars _ x = x;
-
-fun rename_thm_bvars ns th =
- let val t = Thm.prop_of th
- in Thm.rename_boundvars t (rename_term_bvars ns t) th end;
-
-(* Finish this to show how it breaks! (raises the exception):
-
-exception rename_thm_bvars_exp of ((string * string) list * Thm.thm)
-
- Drule.rename_bvars ns th
- handle TERM _ => raise rename_thm_bvars_exp (ns, th);
-*)
-
-end;
--- a/src/Pure/IsaPlanner/term_lib.ML Sun Jun 11 00:28:18 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,676 +0,0 @@
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
-(* Title: Pure/IsaPlanner/term_lib.ML
- ID: $Id$
- Author: Lucas Dixon, University of Edinburgh
- lucasd@dai.ed.ac.uk
- Created: 17 Aug 2002
-*)
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
-(* DESCRIPTION:
-
- Additional code to work with terms.
-
-*)
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
-signature TERM_LIB =
-sig
- val fo_term_height : term -> int
- val ho_term_height : term -> int
-
- (* Matching/unification with exceptions handled *)
- val clean_match : theory -> term * term
- -> ((indexname * (sort * typ)) list
- * (indexname * (typ * term)) list) option
- val clean_unify : theory -> int -> term * term
- -> ((indexname * (sort * typ)) list
- * (indexname * (typ * term)) list) Seq.seq
-
- (* managing variables in terms, can doing conversions *)
- val bounds_to_frees : term -> term
- val bounds_to_frees_with_vars :
- (string * typ) list -> term -> term
-
- val change_bounds_to_frees : term -> term
- val change_frees_to_vars : term -> term
- val change_vars_to_frees : term -> term
- val loose_bnds_to_frees :
- (string * typ) list -> term -> term
-
- (* make all variables named uniquely *)
- val unique_namify : term -> term
-
- (* breasking up a term and putting it into a normal form
- independent of internal term context *)
- val cleaned_term_conc : term -> term
- val cleaned_term_parts : term -> term list * term
- val cterm_of_term : term -> cterm
-
- (* terms of theorems and subgoals *)
- val term_of_thm : thm -> term
- val get_prems_of_sg_term : term -> term list
- val triv_thm_from_string : string -> thm
-
- (* some common term manipulations *)
- val try_dest_Trueprop : term -> term
-
- val bot_left_leaf_of : term -> term
- val bot_left_leaf_noabs_of : term -> term
-
- (* term containing another term - an embedding check *)
- val term_contains : term -> term -> bool
-
- (* name-convertable checking - like ae-convertable, but allows for
- var's and free's to be mixed - and doesn't used buggy code. :-) *)
- val get_name_eq_member : term -> term list -> term option
- val name_eq_member : term -> term list -> bool
- val term_name_eq :
- term ->
- term ->
- (term * term) list ->
- (term * term) list option
-
- (* is the typ a function or is it atomic *)
- val is_fun_typ : typ -> bool
- val is_atomic_typ : typ -> bool
-
- (* variable analysis *)
- val is_some_kind_of_var : term -> bool
- val same_var_check :
- ''a -> ''b -> (''a * ''b) list -> (''a * ''b) list option
- val has_new_vars : term * term -> bool
- val has_new_typ_vars : term * term -> bool
- (* checks to see if the lhs -> rhs is a invalid rewrite rule *)
- val is_not_valid_rwrule : theory -> (term * term) -> bool
-
- (* get the frees in a term that are of atomic type, ie non-functions *)
- val atomic_frees_of_term : term -> (string * typ) list
-
- (* get used names in a theorem to avoid upon instantiation. *)
- val usednames_of_term : term -> string list
- val usednames_of_thm : thm -> string list
-
- (* Isar term skolemisationm and unsolemisation *)
- (* I think this is written also in IsarRTechn and also in somewhere else *)
- (* val skolemise_term : (string,typ) list -> term -> term *)
- val unskolemise_all_term :
- term ->
- (((string * typ) * string) list * term)
-
- (* given a string describing term then a string for its type, returns
- read term *)
- val readwty : string -> string -> term
-
- (* pretty stuff *)
- val print_term : term -> unit
- val pretty_print_sort : string list -> string
- val pretty_print_term : term -> string
- val pretty_print_type : typ -> string
- val pretty_print_typelist :
- typ list -> (typ -> string) -> string
-
- (* for debugging: quickly get a string of a term w.r.t the_context() *)
- val string_of_term : term -> string
-
- (* Pretty printing in a way that allows them to be parsed by ML.
- these are perhaps redundent, check the standard basis
- lib for generic versions for any datatype? *)
- val writesort : string list -> unit
- val writeterm : term -> unit
- val writetype : typ -> unit
- end
-
-
-structure TermLib : TERM_LIB =
-struct
-
-(* Two kinds of depth measure for HOAS terms, a first order (flat) and a
- higher order one.
- Note: not stable of eta-contraction: embedding eta-expands term,
- thus we assume eta-expanded *)
-fun fo_term_height (a $ b) =
- Int.max (1 + fo_term_height b, (fo_term_height a))
- | fo_term_height (Abs(_,_,t)) = fo_term_height t
- | fo_term_height _ = 0;
-
-fun ho_term_height (a $ b) =
- 1 + (Int.max (ho_term_height b, ho_term_height a))
- | ho_term_height (Abs(_,_,t)) = ho_term_height t
- | ho_term_height _ = 0;
-
-
-(* Higher order matching with exception handled *)
-(* returns optional instantiation *)
-fun clean_match thy (a as (pat, t)) =
- let val (tyenv, tenv) = Pattern.match thy a (Vartab.empty, Vartab.empty)
- in SOME (Vartab.dest tyenv, Vartab.dest tenv)
- end handle Pattern.MATCH => NONE;
-(* Higher order unification with exception handled, return the instantiations *)
-(* given Signature, max var index, pat, tgt *)
-(* returns Seq of instantiations *)
-fun clean_unify sgn ix (a as (pat, tgt)) =
- let
- (* type info will be re-derived, maybe this can be cached
- for efficiency? *)
- val pat_ty = Term.type_of pat;
- val tgt_ty = Term.type_of tgt;
- (* is it OK to ignore the type instantiation info?
- or should I be using it? *)
- val typs_unify =
- SOME (Sign.typ_unify sgn (pat_ty, tgt_ty) (Term.Vartab.empty, ix))
- handle Type.TUNIFY => NONE;
- in
- case typs_unify of
- SOME (typinsttab, ix2) =>
- let
- (* is it right to throw away the flexes?
- or should I be using them somehow? *)
- fun mk_insts env =
- (Vartab.dest (Envir.type_env env),
- Envir.alist_of env);
- val initenv = Envir.Envir {asol = Vartab.empty,
- iTs = typinsttab, maxidx = ix2};
- val useq = (Unify.smash_unifiers (sgn,initenv,[a]))
- handle UnequalLengths => Seq.empty
- | Term.TERM _ => Seq.empty;
- fun clean_unify' useq () =
- (case (Seq.pull useq) of
- NONE => NONE
- | SOME (h,t) => SOME (mk_insts h, Seq.make (clean_unify' t)))
- handle UnequalLengths => NONE
- | Term.TERM _ => NONE;
- in
- (Seq.make (clean_unify' useq))
- end
- | NONE => Seq.empty
- end;
-
-fun asm_mk t = assume (cterm_of (the_context()) t);
-fun asm_read s = (Thm.assume (read_cterm (the_context()) (s,propT)));
-
-
-(* more pretty printing code for Isabelle terms etc *)
-
-
-(* pretty_print_typelist l f = print a typelist.
- l = list of types to print : typ list
- f = function used to print a single type : typ -> string
-*)
-fun pretty_print_typelist [] f = ""
- | pretty_print_typelist [(h: typ)] (f : typ -> string) = (f h)
- | pretty_print_typelist ((h: typ) :: t) (f : typ -> string) =
- (f h) ^ ", " ^ (pretty_print_typelist t f);
-
-
-
-(* pretty_print_sort s = print a sort
- s = sort to print : string list
-*)
-fun pretty_print_sort [] = ""
- | pretty_print_sort ([h]) = "\"" ^ h ^ "\""
- | pretty_print_sort (h :: t) = "\"" ^ h ^ "\"," ^ (pretty_print_sort t);
-
-
-(* pretty_print_type t = print a type
- t = type to print : type
-*)
-fun pretty_print_type (Type (n, l)) =
- "Type(\"" ^ n ^ "\", [" ^ (pretty_print_typelist l pretty_print_type) ^ "])"
- | pretty_print_type (TFree (n, s)) =
- "TFree(\"" ^ n ^ "\", [" ^ (pretty_print_sort s) ^ "])"
- | pretty_print_type (TVar ((n, i), s)) =
- "TVar( (\"" ^ n ^ "\", " ^ (string_of_int i) ^ "), [" ^ (pretty_print_sort s) ^ "])";
-
-
-(* pretty_print_term t = print a term prints types and sorts too.
- t = term to print : term
-*)
-fun pretty_print_term (Const (s, t)) =
- "Const(\"" ^ s ^ "\", " ^ (pretty_print_type t) ^ ")"
- | pretty_print_term (Free (s, t)) =
- "Free(\"" ^ s ^ "\", " ^ (pretty_print_type t) ^ ")"
- | pretty_print_term (Var ((n, i), t)) =
- "Var( (\"" ^ n ^ "\"," ^ (string_of_int i) ^ "), " ^ (pretty_print_type t) ^ ")"
- | pretty_print_term (Bound i) =
- "Bound(" ^ (string_of_int i) ^ ")"
- | pretty_print_term (Abs (s, t, r)) =
- "Abs(\"" ^ s ^ "\"," ^ (pretty_print_type t) ^ ", \n " ^ (pretty_print_term r) ^ ")"
- | pretty_print_term (op $ (t1, t2)) =
- "(" ^ (pretty_print_term t1) ^ ") $\n (" ^ (pretty_print_term t2) ^ ")";
-
-(* Write the term out nicly instead of just creating a string for it *)
-fun writeterm t = writeln (pretty_print_term t);
-fun writetype t = writeln (pretty_print_type t);
-fun writesort s = writeln (pretty_print_sort s);
-
-fun cterm_of_term (t : term) = Thm.cterm_of (the_context()) t;
-fun term_of_thm t = (Thm.prop_of t);
-
-fun string_of_term t = Sign.string_of_term (the_context()) t;
-fun print_term t = writeln (string_of_term t);
-
-(* create a trivial thm from anything... *)
-fun triv_thm_from_string s =
- let val thy = the_context()
- in Thm.trivial (cterm_of thy (Sign.read_prop thy s)) end;
-
- (* Checks if vars could be the same - alpha convertable
- w.r.t. previous vars, a and b are assumed to be vars,
- free vars, but not bound vars,
- Note frees and vars must all have unique names. *)
- fun same_var_check a b L =
- let
- fun bterm_from t [] = NONE
- | bterm_from t ((a,b)::m) =
- if t = a then SOME b else bterm_from t m
-
- val bl_opt = bterm_from a L
- in
- case bterm_from a L of
- NONE => SOME ((a,b)::L)
- | SOME b2 => if b2 = b then SOME L else NONE
- end;
-
- (* FIXME: make more efficient, only require a single new var! *)
- (* check if the new term has any meta variables not in the old term *)
- fun has_new_vars (old, new) =
- (case IsaPLib.lrem (op =) (Term.term_vars old) (Term.term_vars new) of
- [] => false
- | (_::_) => true);
- (* check if the new term has any meta variables not in the old term *)
- fun has_new_typ_vars (old, new) =
- (case IsaPLib.lrem (op =) (Term.term_tvars old) (Term.term_tvars new) of
- [] => false
- | (_::_) => true);
-
-(* This version avoids name conflicts that might be introduced by
-unskolemisation, and returns a list of (string * Term.typ) * string,
-where the outer string is the original name, and the inner string is
-the new name, and the type is the type of the free variable that was
-renamed. *)
-local
- fun myadd (n,ty) (L as (renames, names)) =
- let val n' = Syntax.dest_skolem n in
- case (Library.find_first (fn (_,n2) => (n2 = n)) renames) of
- NONE =>
- let val renamedn = Term.variant names n' in
- (renamedn, (((renamedn, ty), n) :: renames,
- renamedn :: names)) end
- | (SOME ((renamedn, _), _)) => (renamedn, L)
- end
- handle Fail _ => (n, L);
-
- fun unsk (L,f) (t1 $ t2) =
- let val (L', t1') = unsk (L, I) t1
- in unsk (L', (fn x => f (t1' $ x))) t2 end
- | unsk (L,f) (Abs(n,ty,t)) =
- unsk (L, (fn x => Abs(n,ty,x))) t
- | unsk (L, f) (Free (n,ty)) =
- let val (renamed_n, L') = myadd (n ,ty) L
- in (L', f (Free (renamed_n, ty))) end
- | unsk (L, f) l = (L, f l);
-in
-fun unskolemise_all_term t =
- let
- val names = Term.add_term_names (t,[])
- val ((renames,names'),t') = unsk (([], names),I) t
- in (renames,t') end;
-end
-
-(* true if the type t is a function *)
-fun is_fun_typ (Type(s, l)) =
- if s = "fun" then true else false
- | is_fun_typ _ = false;
-
-val is_atomic_typ = not o is_fun_typ;
-
-(* get the frees in a term that are of atomic type, ie non-functions *)
-val atomic_frees_of_term =
- List.filter (is_atomic_typ o snd)
- o map Term.dest_Free
- o Term.term_frees;
-
-fun usednames_of_term t = Term.add_term_names (t,[]);
-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;
-
-(* read in a string and a top-level type and this will give back a term *)
-fun readwty tstr tystr =
- let val thy = the_context()
- in Sign.simple_read_term thy (Sign.read_typ (thy, K NONE) tystr) tstr end;
-
- (* first term is equal to the second in some name convertable
- way... Note: This differs from the aeconv in the Term.ML file of
- Isabelle in that it allows a var to be alpha-equiv to a free var.
-
- Also, the isabelle term.ML version of aeconv uses a
- function that it claims doesn't work! *)
- fun term_name_eq (Abs(_,ty1,t1)) (Abs(_,ty2,t2)) l =
- if ty1 = ty2 then term_name_eq t1 t2 l
- else NONE
- | term_name_eq (ah $ at) (bh $ bt) l =
- (case term_name_eq ah bh l of
- NONE => NONE
- | SOME l' => term_name_eq at bt l')
- | term_name_eq (Const(a,T)) (Const(b,U)) l =
- if a=b andalso T=U then SOME l
- else NONE
- | term_name_eq (a as Free(s1,ty1)) (b as Free(s2,ty2)) l =
- same_var_check a b l
- | term_name_eq (a as Free(s1,ty1)) (b as Var(n2,ty2)) l =
- same_var_check a b l
- | term_name_eq (a as Var(n1,ty1)) (b as Free(s2,ty2)) l =
- same_var_check a b l
- | term_name_eq (a as Var(n1,ty1)) (b as Var(n2,ty2)) l =
- same_var_check a b l
- | term_name_eq (Bound i) (Bound j) l =
- if i = j then SOME l else NONE
- | term_name_eq a b l = ((*writeln ("unchecked case:\n" ^ "a:\n" ^ (pretty_print_term a) ^ "\nb:\n" ^ (pretty_print_term b));*) NONE);
-
- (* checks to see if the term in a name-equivalent member of the list of terms. *)
- fun get_name_eq_member a [] = NONE
- | get_name_eq_member a (h :: t) =
- if is_some (term_name_eq a h []) then SOME h
- else get_name_eq_member a t;
-
- fun name_eq_member a [] = false
- | name_eq_member a (h :: t) =
- if is_some (term_name_eq a h []) then true
- else name_eq_member a t;
-
- (* true if term is a variable *)
- fun is_some_kind_of_var (Free(s, ty)) = true
- | is_some_kind_of_var (Var(i, ty)) = true
- | is_some_kind_of_var (Bound(i)) = true
- | is_some_kind_of_var _ = false;
-
- (* checks to see if the lhs -> rhs is a invalid rewrite rule *)
-(* FIXME: we should really check that there is a subterm on the lhs
-which embeds into the rhs, this would be much closer to the normal
-notion of valid wave rule - ie there exists at least one case where it
-is a valid wave rule... *)
- fun is_not_valid_rwrule thy (lhs, rhs) =
- Term.is_Var (Term.head_of lhs) (* if lhs is essentially just a var *)
- orelse has_new_vars (lhs,rhs)
- orelse has_new_typ_vars (lhs,rhs)
- orelse Pattern.matches_subterm thy (lhs, rhs);
-
-
- (* first term contains the second in some name convertable way... *)
- (* note: this is equivalent to an alpha-convertable emedding *)
- (* takes as args: term containing a, term contained b,
- (bound vars of a, bound vars of b),
- current alpha-conversion-pairs,
- returns: bool:can convert, new alpha-conversion table *)
- (* in bellow: we *don't* use: a loose notion that only requires
- variables to match variables, and doesn't worry about the actual
- pattern in the variables. *)
- fun term_contains1 (Bs, FVs) (Abs(s,ty,t)) (Abs(s2,ty2,t2)) =
- if ty = ty2 then
- term_contains1 ((SOME(s,s2,ty)::Bs), FVs) t t2
- else []
-
- | term_contains1 T t1 (Abs(s2,ty2,t2)) = []
-
- | term_contains1 (Bs, FVs) (Abs(s,ty,t)) t2 =
- term_contains1 (NONE::Bs, FVs) t t2
-
- | term_contains1 T (ah $ at) (bh $ bt) =
- (term_contains1 T ah (bh $ bt)) @
- (term_contains1 T at (bh $ bt)) @
- (maps (fn inT => (term_contains1 inT at bt)) (term_contains1 T ah bh))
-
- | term_contains1 T a (bh $ bt) = []
-
- | term_contains1 T (ah $ at) b =
- (term_contains1 T ah b) @ (term_contains1 T at b)
-
- | term_contains1 T a b =
- (* simple list table lookup to check if a named variable has been
- mapped to a variable, if not adds the mapping and return some new
- list mapping, if it is then it checks that the pair are mapped to
- each other, if so returns the current mapping list, else none. *)
- let
- fun bterm_from t [] = NONE
- | bterm_from t ((a,b)::m) =
- if t = a then SOME b else bterm_from t m
-
- (* check to see if, w.r.t. the variable mapping, two terms are leaf
- terms and are mapped to each other. Note constants are only mapped
- to the same constant. *)
- fun same_leaf_check (T as (Bs,FVs)) (Bound i) (Bound j) =
- let
- fun aux_chk (i1,i2) [] = false
- | aux_chk (0,0) ((SOME _) :: bnds) = true
- | aux_chk (i1,0) (NONE :: bnds) = false
- | aux_chk (i1,i2) ((SOME _) :: bnds) =
- aux_chk (i1 - 1,i2 - 1) bnds
- | aux_chk (i1,i2) (NONE :: bnds) =
- aux_chk (i1,i2 - 1) bnds
- in
- if (aux_chk (i,j) Bs) then [T]
- else []
- end
- | same_leaf_check (T as (Bs,(Fs,Vs)))
- (a as (Free (an,aty)))
- (b as (Free (bn,bty))) =
- (case bterm_from an Fs of
- SOME b2n => if bn = b2n then [T]
- else [] (* conflict of var name *)
- | NONE => [(Bs,((an,bn)::Fs,Vs))])
- | same_leaf_check (T as (Bs,(Fs,Vs)))
- (a as (Var (an,aty)))
- (b as (Var (bn,bty))) =
- (case bterm_from an Vs of
- SOME b2n => if bn = b2n then [T]
- else [] (* conflict of var name *)
- | NONE => [(Bs,(Fs,(an,bn)::Vs))])
- | same_leaf_check T (a as (Const _)) (b as (Const _)) =
- if a = b then [T] else []
- | same_leaf_check T _ _ = []
-
- in
- same_leaf_check T a b
- end;
-
- (* wrapper for term_contains1: checks if the term "a" contains in
- some embedded way, (w.r.t. name -convertable) the term "b" *)
- fun term_contains a b =
- case term_contains1 ([],([],[])) a b of
- (_ :: _) => true
- | [] => false;
-
- (* change all bound variables to see ones with appropriate name and
- type *)
- (* naming convention is OK as we use 'variant' from term.ML *)
- (* Note "bounds_to_frees" defined below, its better and quicker, but
- keeps the quantifiers handing about, and changes all bounds, not
- just universally quantified ones. *)
- fun change_bounds_to_frees t =
- let
- val vars = strip_all_vars t
- val frees_names = map (fn Free(s,n) => s | _ => "") (term_frees t)
- val body = strip_all_body t
-
- fun bnds_to_frees [] _ acc = acc
- | bnds_to_frees ((name,ty)::more) names acc =
- let
- val new_name = variant names name
- in
- bnds_to_frees more (new_name::names) (Free(new_name,ty)::acc)
- end
- in
- (subst_bounds ((bnds_to_frees vars frees_names []), body))
- end;
-
-(* a runtime-quick function which makes sure that every variable has a
-unique name *)
-fun unique_namify_aux (ntab,(Abs(s,ty,t))) =
- (case Symtab.lookup ntab s of
- NONE =>
- let
- val (ntab2,t2) = unique_namify_aux (Symtab.update (s, s) ntab, t)
- in
- (ntab2,Abs(s,ty,t2))
- end
- | SOME s2 =>
- let
- val s_new = (Term.variant (Symtab.keys ntab) s)
- val (ntab2,t2) =
- unique_namify_aux (Symtab.update (s_new, s_new) ntab, t)
- in
- (ntab2,Abs(s_new,ty,t2))
- end)
- | unique_namify_aux (ntab,(a $ b)) =
- let
- val (ntab1,t1) = unique_namify_aux (ntab,a)
- val (ntab2,t2) = unique_namify_aux (ntab1,b)
- in
- (ntab2, t1$t2)
- end
- | unique_namify_aux (nt as (ntab,Const x)) = nt
- | unique_namify_aux (nt as (ntab,f as Free (s,ty))) =
- (case Symtab.lookup ntab s of
- NONE => (Symtab.update (s, s) ntab, f)
- | SOME _ => nt)
- | unique_namify_aux (nt as (ntab,v as Var ((s,i),ty))) =
- (case Symtab.lookup ntab s of
- NONE => (Symtab.update (s, s) ntab, v)
- | SOME _ => nt)
- | unique_namify_aux (nt as (ntab, Bound i)) = nt;
-
-fun unique_namify t =
- #2 (unique_namify_aux (Symtab.empty, t));
-
-(* a runtime-quick function which makes sure that every variable has a
-unique name and also changes bound variables to free variables, used
-for embedding checks, Note that this is a pretty naughty term
-manipulation, which doesn't have necessary relation to the original
-sematics of the term. This is really a trick for our embedding code. *)
-
-fun bounds_to_frees_aux T (ntab,(Abs(s,ty,t))) =
- (case Symtab.lookup ntab s of
- NONE =>
- let
- val (ntab2,t2) =
- bounds_to_frees_aux ((s,ty)::T) (Symtab.update (s, s) ntab, t)
- in
- (ntab2,Abs(s,ty,t2))
- end
- | SOME s2 =>
- let
- val s_new = (Term.variant (Symtab.keys ntab) s)
- val (ntab2,t2) =
- bounds_to_frees_aux ((s_new,ty)::T)
- (Symtab.update (s_new, s_new) ntab, t)
- in
- (ntab2,Abs(s_new,ty,t2))
- end)
- | bounds_to_frees_aux T (ntab,(a $ b)) =
- let
- val (ntab1,t1) = bounds_to_frees_aux T (ntab,a)
- val (ntab2,t2) = bounds_to_frees_aux T (ntab1,b)
- in
- (ntab2, t1$t2)
- end
- | bounds_to_frees_aux T (nt as (ntab,Const x)) = nt
- | bounds_to_frees_aux T (nt as (ntab,f as Free (s,ty))) =
- (case Symtab.lookup ntab s of
- NONE => (Symtab.update (s, s) ntab, f)
- | SOME _ => nt)
- | bounds_to_frees_aux T (nt as (ntab,v as Var ((s,i),ty))) =
- (case Symtab.lookup ntab s of
- NONE => (Symtab.update (s, s) ntab, v)
- | SOME _ => nt)
- | bounds_to_frees_aux T (nt as (ntab, Bound i)) =
- let
- val (s,ty) = List.nth (T,i)
- in
- (ntab, Free (s,ty))
- end;
-
-
-fun bounds_to_frees t =
- #2 (bounds_to_frees_aux [] (Symtab.empty,t));
-
-fun bounds_to_frees_with_vars vars t =
- #2 (bounds_to_frees_aux vars (Symtab.empty,t));
-
-
-
-(* loose bounds to frees *)
-fun loose_bnds_to_frees_aux (bnds,vars) (Abs(s,ty,t)) =
- Abs(s,ty,loose_bnds_to_frees_aux (bnds + 1,vars) t)
- | loose_bnds_to_frees_aux (bnds,vars) (a $ b) =
- (loose_bnds_to_frees_aux (bnds,vars) a)
- $ (loose_bnds_to_frees_aux (bnds,vars) b)
- | loose_bnds_to_frees_aux (bnds,vars) (t as (Bound i)) =
- if (bnds <= i) then Free (List.nth (vars,i - bnds))
- else t
- | loose_bnds_to_frees_aux (bnds,vars) t = t;
-
-
-fun loose_bnds_to_frees vars t =
- loose_bnds_to_frees_aux (0,vars) t;
-
-
- (* FIXME ObjectLogic.drop_judgment *)
- fun try_dest_Trueprop (Const("Trueprop", _) $ T) = T
- | try_dest_Trueprop T = T;
-
- fun bot_left_leaf_of (l $ r) = bot_left_leaf_of l
- | bot_left_leaf_of (Abs(s,ty,t)) = bot_left_leaf_of t
- | bot_left_leaf_of x = x;
-
- fun bot_left_leaf_noabs_of (l $ r) = bot_left_leaf_noabs_of l
- | bot_left_leaf_noabs_of x = x;
-
-(* cleaned up normal form version of the subgoal terms conclusion *)
-fun cleaned_term_conc t =
- let
- val concl = Logic.strip_imp_concl (change_bounds_to_frees t)
- in
- (try_dest_Trueprop (Logic.unprotect concl handle TERM _ => concl))
- end;
-
-(* fun get_prems_of_sg_term t =
- map opt_dest_Trueprop (Logic.strip_imp_prems t); *)
-
-fun get_prems_of_sg_term t =
- map try_dest_Trueprop (Logic.strip_assums_hyp t);
-
-
-(* drop premises, clean bound var stuff, and make a trueprop... *)
- fun cleaned_term_parts t =
- let
- val t2 = (change_bounds_to_frees t)
- val concl = Logic.strip_imp_concl t2
- val prems = map try_dest_Trueprop (Logic.strip_imp_prems t2)
- in
- (prems, (try_dest_Trueprop ((Logic.unprotect concl handle TERM _ => concl))))
- end;
-
- (* change free variables to vars and visa versa *)
- (* *** check naming is OK, can we just use the vasr old name? *)
- (* *** Check: Logic.varify and Logic.unvarify *)
- fun change_vars_to_frees (a$b) =
- (change_vars_to_frees a) $ (change_vars_to_frees b)
- | change_vars_to_frees (Abs(s,ty,t)) =
- (Abs(s, Logic.legacy_varifyT ty,change_vars_to_frees t))
- | change_vars_to_frees (Var((s,i),ty)) = (Free(s, Logic.legacy_unvarifyT ty))
- | change_vars_to_frees l = l;
-
- fun change_frees_to_vars (a$b) =
- (change_frees_to_vars a) $ (change_frees_to_vars b)
- | change_frees_to_vars (Abs(s,ty,t)) =
- (Abs(s, Logic.legacy_varifyT ty,change_frees_to_vars t))
- | change_frees_to_vars (Free(s,ty)) = (Var((s,0), Logic.legacy_varifyT ty))
- | change_frees_to_vars l = l;
-
-
-end;
--- a/src/Pure/IsaPlanner/upterm_lib.ML Sun Jun 11 00:28:18 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,133 +0,0 @@
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
-(* Title: Pure/IsaPlanner/upterm_lib.ML
- ID: $Id$
- Author: Lucas Dixon, University of Edinburgh
- lucas.dixon@ed.ac.uk
- Created: 26 Jan 2004
-*)
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
-(* DESCRIPTION:
-
- generic upterms for lambda calculus
-
-*)
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
-
-
-signature UPTERM_LIB =
-sig
-
-
- (* type for upterms defined in terms of a 't : a downterm type, and
- 'y : types for bound variable in the downterm type *)
- datatype ('t,'y) T =
- abs of string * 'y * (('t,'y) T)
- | appl of 't * (('t,'y) T)
- | appr of 't * (('t,'y) T)
- | root
-
- (* analysis *)
- val tyenv_of_upterm : ('t,'y) T -> (string * 'y) list
- val tyenv_of_upterm' : ('t,'y) T -> 'y list
- val addr_of_upterm : ('t,'y) T -> int list
- val upsize_of_upterm : ('t,'y) T -> int
-
- (* editing *)
- val map_to_upterm_parts : ('t -> 't2) * ('y -> 'y2) ->
- ('t,'y) T -> ('t2,'y2) T
-
- val expand_map_to_upterm_parts : ('t -> 't2 list) * ('y -> 'y2) ->
- ('t,'y) T -> ('t2,'y2) T list
-
- val fold_upterm : ('a * 't -> 'a) -> (* left *)
- ('a * 't -> 'a) -> (* right *)
- ('a * (string * 'y) -> 'a) -> (* abs *)
- ('a * ('t,'y) T) -> 'a (* everything *)
-
- (* apply one term to another *)
- val apply : ('t,'y) T -> ('t,'y) T -> ('t,'y) T
-
-end;
-
-
-
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
-structure UpTermLib : UPTERM_LIB =
-struct
-
- (* type for upterms defined in terms of a 't : a downterm type, and
- 'y : types for bound variable in the downterm type *)
- datatype ('t,'y) T =
- abs of string * 'y * ('t,'y) T
- | appl of 't * ('t,'y) T
- | appr of 't * ('t,'y) T
- | root;
-
- (* get the bound variable names and types for the current foucs *)
- fun tyenv_of_upterm (appl(l,m)) = tyenv_of_upterm m
- | tyenv_of_upterm (appr(r,m)) = tyenv_of_upterm m
- | tyenv_of_upterm (abs(s,ty,m)) = (s, ty) :: (tyenv_of_upterm m)
- | tyenv_of_upterm root = [];
-
- (* get the bound variable types for the current foucs *)
- fun tyenv_of_upterm' (appl(l,m)) = tyenv_of_upterm' m
- | tyenv_of_upterm' (appr(r,m)) = tyenv_of_upterm' m
- | tyenv_of_upterm' (abs(s,ty,m)) = ty :: (tyenv_of_upterm' m)
- | tyenv_of_upterm' root = [];
-
- (* an address construction for the upterm, ie if we were at the
- root, address describes how to get to this point. *)
- fun addr_of_upterm1 A root = A
- | addr_of_upterm1 A (appl (l,m)) = addr_of_upterm1 (1::A) m
- | addr_of_upterm1 A (appr (r,m)) = addr_of_upterm1 (2::A) m
- | addr_of_upterm1 A (abs (s,ty,m)) = addr_of_upterm1 (0::A) m;
-
- fun addr_of_upterm m = addr_of_upterm1 [] m;
-
- (* the size of the upterm, ie how far to get to root *)
- fun upsize_of_upterm root = 0
- | upsize_of_upterm (appl (l,m)) = (upsize_of_upterm m) + 1
- | upsize_of_upterm (appr (r,m)) = (upsize_of_upterm m) + 1
- | upsize_of_upterm (abs (s,ty,m)) = (upsize_of_upterm m) + 1;
-
- (* apply an upterm to to another upterm *)
- fun apply x root = x
- | apply x (appl (l,m)) = appl(l, apply x m)
- | apply x (appr (r,m)) = appr(r, apply x m)
- | apply x (abs (s,ty,m)) = abs(s, ty, apply x m);
-
- (* applies the term function to each term in each part of the upterm *)
- fun map_to_upterm_parts (tf,yf) root = root
-
- | map_to_upterm_parts (tf,yf) (abs(s,ty,m)) =
- abs(s,yf ty,map_to_upterm_parts (tf,yf) m)
-
- | map_to_upterm_parts (tf,yf) (appr(t,m)) =
- appr (tf t, map_to_upterm_parts (tf,yf) m)
-
- | map_to_upterm_parts (tf,yf) (appl(t,m)) =
- appl (tf t, map_to_upterm_parts (tf,yf) m);
-
-
- (* applies the term function to each term in each part of the upterm *)
- fun expand_map_to_upterm_parts (tf,yf) root = [root]
- | expand_map_to_upterm_parts (tf,yf) (abs(s,ty,m)) =
- map (fn x => abs(s,yf ty, x))
- (expand_map_to_upterm_parts (tf,yf) m)
- | expand_map_to_upterm_parts (tf,yf) (appr(t,m)) =
- map appr (IsaPLib.all_pairs
- (tf t) (expand_map_to_upterm_parts (tf,yf) m))
- | expand_map_to_upterm_parts (tf,yf) (appl(t,m)) =
- map appl (IsaPLib.all_pairs
- (tf t) (expand_map_to_upterm_parts (tf,yf) m));
-
- (* fold along each 't (down term) in the upterm *)
- fun fold_upterm fl fr fa (d, u) =
- let
- fun fold_upterm' (d, root) = d
- | fold_upterm' (d, abs(s,ty,m)) = fold_upterm' (fa(d,(s,ty)), m)
- | fold_upterm' (d, appr(t,m)) = fold_upterm' (fr(d,t), m)
- | fold_upterm' (d, appl(t,m)) = fold_upterm' (fl(d,t), m)
- in fold_upterm' (d,u) end;
-
-end;