lucas - fixed a big with renaming of bound variables. Other small changes.
--- a/src/Provers/eqsubst.ML Fri Apr 22 14:15:01 2005 +0200
+++ b/src/Provers/eqsubst.ML Fri Apr 22 15:10:42 2005 +0200
@@ -29,9 +29,10 @@
type match =
((Term.indexname * Term.typ) list (* type instantiations *)
- * (Term.indexname * Term.term) list) (* term instantiations *)
- * (string * Term.typ) list (* type abs env *)
- * Term.term (* outer term *)
+ * (Term.indexname * Term.term) list) (* term instantiations *)
+ * (string * Term.typ) list (* fake named type abs env *)
+ * (string * Term.typ) list (* type abs env *)
+ * Term.term (* outer term *)
val prep_subst_in_asm :
(Sign.sg (* sign for matching *)
@@ -86,13 +87,32 @@
-> match
-> Thm.thm Seq.seq (* substituted goal *)
+ val searchf_tlr_unify_all :
+ (Sign.sg -> int ->
+ Term.term ->
+ BasicIsaFTerm.FcTerm ->
+ match Seq.seq)
+ val searchf_tlr_unify_valid :
+ (Sign.sg -> int ->
+ Term.term ->
+ BasicIsaFTerm.FcTerm ->
+ match Seq.seq)
+
val eqsubst_asm_meth : Thm.thm list -> Proof.method
val eqsubst_asm_tac : Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
- val eqsubst_asm_tac' : Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq
+ val eqsubst_asm_tac' :
+ (Sign.sg -> int ->
+ Term.term ->
+ BasicIsaFTerm.FcTerm ->
+ match Seq.seq) -> Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq
val eqsubst_meth : Thm.thm list -> Proof.method
val eqsubst_tac : Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
- val eqsubst_tac' : Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq
+ val eqsubst_tac' :
+ (Sign.sg -> int ->
+ Term.term ->
+ BasicIsaFTerm.FcTerm ->
+ match Seq.seq) -> Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq
val meth : bool * Thm.thm list -> Proof.context -> Proof.method
val setup : (Theory.theory -> Theory.theory) list
@@ -106,6 +126,7 @@
type match =
((Term.indexname * Term.typ) list (* type instantiations *)
* (Term.indexname * Term.term) list) (* term instantiations *)
+ * (string * Term.typ) list (* fake named type abs env *)
* (string * Term.typ) list (* type abs env *)
* Term.term (* outer term *)
@@ -132,8 +153,8 @@
infix 5 :->;
fun s :-> f = Seq.flat (Seq.map f s);
-(* search from the top to bottom, left to right *)
-fun search_lr_f f ft =
+(* search from top, left to right, then down *)
+fun search_tlr_all_f f ft =
let
fun maux ft =
let val t' = (IsaFTerm.focus_of_fcterm ft)
@@ -147,15 +168,39 @@
(_ $ _) => Seq.append(maux (IsaFTerm.focus_left ft),
Seq.append(f ft,
maux (IsaFTerm.focus_right ft)))
- | (Abs _) => Seq.append (f ft, maux (IsaFTerm.focus_abs ft))
+ | (Abs _) => Seq.append(f ft, maux (IsaFTerm.focus_abs ft))
| leaf => f ft) end
in maux ft end;
-fun search_for_match sgn maxidx lhs =
+(* search from top, left to right, then down *)
+fun search_tlr_valid_f f ft =
+ let
+ fun maux ft =
+ let
+ val hereseq = if IsaFTerm.valid_match_start ft then f ft else Seq.empty
+ in
+ (case (IsaFTerm.focus_of_fcterm ft) of
+ (_ $ _) => Seq.append(maux (IsaFTerm.focus_left ft),
+ Seq.append(hereseq,
+ maux (IsaFTerm.focus_right ft)))
+ | (Abs _) => Seq.append(hereseq, maux (IsaFTerm.focus_abs ft))
+ | leaf => hereseq)
+ end
+ in maux ft end;
+
+(* search all unifications *)
+fun searchf_tlr_unify_all sgn maxidx lhs =
IsaFTerm.find_fcterm_matches
- search_lr_f
+ search_tlr_all_f
(IsaFTerm.clean_unify_ft sgn maxidx lhs);
+(* search only for 'valid' unifiers (non abs subterms and non vars) *)
+fun searchf_tlr_unify_valid sgn maxidx lhs =
+ IsaFTerm.find_fcterm_matches
+ search_tlr_valid_f
+ (IsaFTerm.clean_unify_ft sgn maxidx lhs);
+
+
(* apply a substitution in the conclusion of the theorem th *)
(* cfvs are certified free var placeholders for goal params *)
(* conclthm is a theorem of for just the conclusion *)
@@ -168,9 +213,7 @@
|> (fn r => Tactic.rtac r i th);
(*
-? is the following equivalent to rtac ?
- |> Thm.lift_rule (th, i)
|> (fn r => Thm.bicompose false (false, r, Thm.nprems_of r) i th)
*)
@@ -203,10 +246,10 @@
(* substitute using an object or meta level equality *)
-fun eqsubst_tac' instepthm i th =
+fun eqsubst_tac' searchf instepthm i th =
let
val (cvfsconclthm, findmatchf) =
- prep_concl_subst search_for_match i th;
+ prep_concl_subst searchf i th;
val stepthms =
Seq.map Drule.zero_var_indexes
@@ -223,7 +266,8 @@
(* substitute using one of the given theorems *)
fun eqsubst_tac instepthms i th =
if Thm.nprems_of th < i then Seq.empty else
- (Seq.of_list instepthms) :-> (fn r => eqsubst_tac' r i th);
+ (Seq.of_list instepthms)
+ :-> (fn r => eqsubst_tac' searchf_tlr_unify_valid r i th);
(* inthms are the given arguments in Isar, and treated as eqstep with
the first one, then the second etc *)
@@ -293,9 +337,9 @@
(* substitute in an assumption using an object or meta level equality *)
-fun eqsubst_asm_tac' instepthm i th =
+fun eqsubst_asm_tac' searchf instepthm i th =
let
- val asmpreps = prep_subst_in_asms search_for_match i th;
+ val asmpreps = prep_subst_in_asms searchf i th;
val stepthms =
Seq.map Drule.zero_var_indexes
(Seq.of_list (EqRuleData.prep_meta_eq instepthm))
@@ -311,7 +355,8 @@
(* substitute using one of the given theorems *)
fun eqsubst_asm_tac instepthms i th =
if Thm.nprems_of th < i then Seq.empty else
- (Seq.of_list instepthms) :-> (fn r => eqsubst_asm_tac' r i th);
+ (Seq.of_list instepthms)
+ :-> (fn r => eqsubst_asm_tac' searchf_tlr_unify_valid r i th);
(* inthms are the given arguments in Isar, and treated as eqstep with
the first one, then the second etc *)
--- a/src/Pure/IsaPlanner/focus_term_lib.ML Fri Apr 22 14:15:01 2005 +0200
+++ b/src/Pure/IsaPlanner/focus_term_lib.ML Fri Apr 22 15:10:42 2005 +0200
@@ -90,7 +90,9 @@
(* 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
@@ -215,6 +217,9 @@
| 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))
@@ -257,11 +262,16 @@
| focus_up_right1 (focus(t, root)) =
raise out_of_term_exception "focus_up_right1";
- (* move focus to the bottom left *)
+ (* 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))
--- a/src/Pure/IsaPlanner/isa_fterm.ML Fri Apr 22 14:15:01 2005 +0200
+++ b/src/Pure/IsaPlanner/isa_fterm.ML Fri Apr 22 15:10:42 2005 +0200
@@ -20,28 +20,40 @@
(* signature BASIC_ISA_FTERM =
FOCUS_TERM_SIG where type Term = ISA_ENCODE_TERM.Term *)
-(*
signature ISA_FTERM =
-sig
- include F_ENCODE_TERM_SIG
-
+ 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 :
Type.tsig ->
+ Term.term ->
FcTerm ->
- Term.term ->
(
((Term.indexname * Term.typ) list * (Term.indexname * Term.term) list)
- * (string * Type) list * Term.term) option
+ * (string * Term.typ) list * (string * Term.typ) list * Term.term)
+ option
val clean_unify_ft :
Sign.sg ->
int ->
+ Term.term ->
FcTerm ->
- Term.term ->
(
((Term.indexname * Term.typ) list * (Term.indexname * Term.term) list)
- * (string * Type) list * Term.term) Seq.seq
- val fakefree_badbounds :
- (string * Term.typ) list -> int -> Term.term -> Term.term
+ * (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 fakefree_badbounds :
+ (string * Term.typ) list -> Term.term ->
+ (string * Term.typ) list * (string * Term.typ) list * Term.term
+ val fcterm_of_term : EncodeIsaFTerm.term -> FcTerm
val find_fcterm_matches :
((FcTerm -> 'a) -> FcTerm -> 'b) ->
(FcTerm -> 'a) -> FcTerm -> 'b
@@ -57,38 +69,98 @@
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_foo_match :
(Term.term -> Term.term) ->
('a * Term.typ) list -> Term.term -> Term.term
+ 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 prepmatch :
FcTerm ->
- Term.term * ((string * Type) list * Term.term)
- val search_bl_ru_f :
+ Term.term *
+ ((string * Term.typ) list * (string * Term.typ) list * Term.term)
+ val pretty_fcterm : FcTerm -> Pretty.T
+ 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_bl_ur_f :
+ 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
+ end
-end *)
+
structure BasicIsaFTerm =
FocusTermFUN( structure EncodeTerm = EncodeIsaFTerm);
(* HOL Dependent *)
-structure IsaFTerm =
+structure IsaFTerm : ISA_FTERM=
struct
(* include BasicIsaFTerm *)
@@ -107,32 +179,38 @@
fun valid_match_start ft =
(case TermLib.bot_left_leaf_of (focus_of_fcterm ft) of
Const _ => true
- | Free _ => true
- | Abs _ => true
- | _ => false);
+ | 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_nonvar_bl_ur_f f ft =
+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 =
- case focus_up_abs_or_appr ft of
- SOME ft' => Seq.append(f ft, mk_match_up_seq ft')
- | NONE => f 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_bl_ur_f f ft =
+fun search_all_bl_ur_f f ft =
let
val fts = (leaf_seq_of_fcterm ft)
- fun mk_match_up_seq 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
@@ -143,7 +221,7 @@
(* FIXME: make properly lazy! *)
(* FIXME: make faking of bound vars local - for speeeeed *)
-fun search_nonvar_bl_ru_f f ft =
+fun search_valid_bl_ru_f f ft =
let
fun mauxtop ft =
if (valid_match_start ft)
@@ -156,15 +234,14 @@
(_ $ _) => Seq.append (maux (focus_left ft),
Seq.append(mauxtop (focus_right ft),
f ft))
- | (Abs _) => Seq.append (maux (focus_abs ft),
- f ft)
+ | (Abs _) => maux (focus_abs ft)
| leaf => f ft) end
in
mauxtop ft
end;
-fun search_bl_ru_f f ft =
+fun search_all_bl_ru_f f ft =
let
fun maux ft =
let val t' = (focus_of_fcterm ft)
@@ -179,6 +256,40 @@
| 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;
@@ -240,21 +351,39 @@
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 *)
-fun fakefree_badbounds T n (a $ b) =
- (fakefree_badbounds T n a) $ (fakefree_badbounds T n b)
- | fakefree_badbounds T n (Abs(s,ty,t)) =
- Abs(s,ty, fakefree_badbounds T (n + 1) t)
- | fakefree_badbounds 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) =
- Free (RWTools.mk_fake_bound_name s,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 T n t = t;
+(* 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
@@ -274,7 +403,7 @@
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 missing an
+(* 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 *)
@@ -282,24 +411,29 @@
let
val t = focus_of_fcterm ft
val Ts = tyenv_of_focus ft
- val t' = fakefree_badbounds Ts 0 t
+ 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'
+ val absterm = mk_foo_match mktermf Ts' t'
in
- (t', (Ts, absterm))
+ (t', (FakeTs', Ts', absterm))
end;
(* 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 tsig pat ft =
- let val (t, (Ts,absterm)) = prepmatch ft in
+ let val (t, (FakeTs,Ts,absterm)) = prepmatch ft in
case TermLib.clean_match tsig (pat, t) of
NONE => NONE
- | SOME insts => SOME (insts, Ts, absterm) end;
+ | SOME insts => SOME (insts, FakeTs, Ts, absterm) end;
(* ix = max var index *)
fun clean_unify_ft sgn ix pat ft =
- let val (t, (Ts,absterm)) = prepmatch ft in
- Seq.map (fn insts => (insts, Ts, absterm))
+ 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;
@@ -327,7 +461,8 @@
(* 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
+ 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 *)
--- a/src/Pure/IsaPlanner/rw_inst.ML Fri Apr 22 14:15:01 2005 +0200
+++ b/src/Pure/IsaPlanner/rw_inst.ML Fri Apr 22 15:10:42 2005 +0200
@@ -18,19 +18,22 @@
(* Rewrite: give it instantiation infromation, a rule, and the
target thm, and it will return the rewritten target thm *)
val rw :
- ((Term.indexname * Term.typ) list * (* type var instantiations *)
- (Term.indexname * Term.term) list) (* schematic var instantiations *)
- * (string * Term.typ) list * (* 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 *)
+ ((Term.indexname * Term.typ) list * (* type var instantiations *)
+ (Term.indexname * 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 -> Thm.thm -> Thm.cterm list * Thm.thm
+ (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 list ->
Term.term list -> ((string * int) * Term.typ) list * (string * sort) list
@@ -80,25 +83,26 @@
note: assumes rule is instantiated
*)
(* Note, we take abstraction in the order of last abstraction first *)
-fun mk_abstractedrule Ts rule =
+fun mk_abstractedrule TsFake Ts rule =
let
val ctermify = Thm.cterm_of (Thm.sign_of_thm rule);
- (* now we change the names the temporary free vars that represent
+ (* 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 = Term.add_term_names (prop, []);
+ val names = TermLib.usednames_of_thm rule;
val (fromnames,tonames,names2,Ts') =
- Library.foldl (fn ((rnf,rnt,names, Ts'),(n,ty)) =>
+ Library.foldl (fn ((rnf,rnt,names, Ts''),((faken,_),(n,ty))) =>
let val n2 = Term.variant names n in
- (ctermify (Free(RWTools.mk_fake_bound_name n,
- ty)) :: rnf,
+ (ctermify (Free(faken,ty)) :: rnf,
ctermify (Free(n2,ty)) :: rnt,
n2 :: names,
- (n2,ty) :: Ts')
+ (n2,ty) :: Ts'')
end)
- (([],[],names, []), Ts);
+ (([],[],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;
@@ -194,7 +198,7 @@
(* 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. *)
-fun rw ((nonfixed_typinsts, unprepinsts), Ts, outerterm) rule target_thm =
+fun rw ((nonfixed_typinsts, unprepinsts), FakeTs, Ts, outerterm) rule target_thm =
let
(* general signature info *)
val target_sign = (Thm.sign_of_thm target_thm);
@@ -258,7 +262,7 @@
val couter_inst = Thm.reflexive (ctermify outerterm_inst);
val (cprems, abstract_rule_inst) =
rule_inst |> Thm.instantiate ([], cterm_renamings)
- |> mk_abstractedrule Ts;
+ |> mk_abstractedrule FakeTs Ts;
val specific_tgt_rule =
beta_eta_contract_tac
(Thm.combination couter_inst abstract_rule_inst);
--- a/src/Pure/IsaPlanner/rw_tools.ML Fri Apr 22 14:15:01 2005 +0200
+++ b/src/Pure/IsaPlanner/rw_tools.ML Fri Apr 22 15:10:42 2005 +0200
@@ -28,12 +28,18 @@
(* 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;
+ | _ => n; *)
fun is_fake_bound_name n = (hd (explode n) = ":");
-fun mk_fake_bound_name n = ":" ^ n;
+fun mk_fake_bound_name n = ":b_" ^ n;
@@ -65,8 +71,9 @@
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 (dest_fake_bound_name n) mem Ns then Var((n,0),ty) else Free (n,ty);
+(* 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);
--- a/src/Pure/IsaPlanner/term_lib.ML Fri Apr 22 14:15:01 2005 +0200
+++ b/src/Pure/IsaPlanner/term_lib.ML Fri Apr 22 15:10:42 2005 +0200
@@ -63,6 +63,7 @@
val try_dest_Trueprop : Term.term -> Term.term
val bot_left_leaf_of : Term.term -> Term.term
+ val bot_left_leaf_noabs_of : Term.term -> Term.term
(* term containing another term - an embedding check *)
val term_contains : Term.term -> Term.term -> bool
@@ -93,6 +94,10 @@
(* get the frees in a term that are of atomic type, ie non-functions *)
val atomic_frees_of_term : Term.term -> (string * Term.typ) list
+ (* get used names in a theorem to avoid upon instantiation. *)
+ val usednames_of_term : Term.term -> string list
+ val usednames_of_thm : 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,Term.typ) list -> Term.term -> Term.term
@@ -113,9 +118,11 @@
val pretty_print_typelist :
Term.typ list -> (Term.typ -> string) -> string
+ (* for debugging: quickly get a string of a term w.r.t the_context() *)
val string_of_term : Term.term -> string
- (* these are perhaps redundent, check the standard basis
+ (* 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.term -> unit
@@ -387,6 +394,15 @@
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 =
@@ -460,11 +476,12 @@
(* 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... *)
+is a valid wave rule... *)
fun is_not_valid_rwrule tysig (lhs, rhs) =
- (Pattern.matches_subterm tysig (lhs, rhs)) orelse
- has_new_vars (lhs,rhs) orelse
- has_new_typ_vars (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 tysig (lhs, rhs);
(* first term contains the second in some name convertable way... *)
@@ -739,6 +756,8 @@
| 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 =