--- a/src/Provers/eqsubst.ML Fri Feb 18 15:20:27 2005 +0100
+++ b/src/Provers/eqsubst.ML Sat Feb 19 18:44:34 2005 +0100
@@ -1,7 +1,8 @@
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
-(* Title: sys/eqsubst_tac.ML
+(* Title: Provers/eqsubst.ML
Author: Lucas Dixon, University of Edinburgh
lucas.dixon@ed.ac.uk
+ Modified: 18 Feb 2005 - Lucas -
Created: 29 Jan 2005
*)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
@@ -12,79 +13,166 @@
*)
(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
-(* Logic specific data *)
+(* Logic specific data stub *)
signature EQRULE_DATA =
sig
+
(* to make a meta equality theorem in the current logic *)
val prep_meta_eq : thm -> thm list
+
end;
+
(* the signature of an instance of the SQSUBST tactic *)
signature EQSUBST_TAC =
sig
+
+ val prep_subst_in_asm :
+ (Sign.sg (* sign for matching *)
+ -> int (* maxidx *)
+ -> 'a (* input object kind *)
+ -> BasicIsaFTerm.FcTerm (* focusterm to search under *)
+ -> 'b) (* result type *)
+ -> int (* subgoal to subst in *)
+ -> Thm.thm (* target theorem with subgoals *)
+ -> int (* premise to subst in *)
+ -> (Thm.cterm list (* certified free var placeholders for vars *)
+ * int (* premice no. to subst *)
+ * int (* number of assumptions of premice *)
+ * Thm.thm) (* premice as a new theorem for forward reasoning *)
+ * ('a -> 'b) (* matchf *)
+
+ val prep_subst_in_asms :
+ (Sign.sg -> int -> 'a -> BasicIsaFTerm.FcTerm -> 'b)
+ -> int (* subgoal to subst in *)
+ -> Thm.thm (* target theorem with subgoals *)
+ -> ((Thm.cterm list (* certified free var placeholders for vars *)
+ * int (* premice no. to subst *)
+ * int (* number of assumptions of premice *)
+ * Thm.thm) (* premice as a new theorem for forward reasoning *)
+ * ('a -> 'b)) (* matchf *)
+ Seq.seq
+
+ val apply_subst_in_asm :
+ int (* subgoal *)
+ -> Thm.thm (* overall theorem *)
+ -> (Thm.cterm list (* certified free var placeholders for vars *)
+ * int (* assump no being subst *)
+ * int (* num of premises of asm *)
+ * Thm.thm) (* premthm *)
+ -> Thm.thm (* rule *)
+ -> (((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 *)
+ -> Thm.thm Seq.seq
+
+ val prep_concl_subst :
+ (Sign.sg -> int -> 'a -> BasicIsaFTerm.FcTerm -> 'b) (* searchf *)
+ -> int (* subgoal *)
+ -> Thm.thm (* overall goal theorem *)
+ -> (Thm.cterm list * Thm.thm) * ('a -> 'b) (* (cvfs, conclthm), matchf *)
+
+ val apply_subst_in_concl :
+ int (* subgoal *)
+ -> Thm.thm (* thm with all goals *)
+ -> Thm.cterm list (* certified free var placeholders for vars *)
+ * Thm.thm (* trivial thm of goal concl *)
+ (* possible matches/unifiers *)
+ -> Thm.thm (* rule *)
+ -> (((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 *)
+ -> Thm.thm Seq.seq (* substituted goal *)
+
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_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 meth : bool * Thm.thm list -> Proof.context -> Proof.method
- val subst : Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq
- val subst_asm : Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq
-
val setup : (Theory.theory -> Theory.theory) list
end;
functor EQSubstTacFUN (structure EqRuleData : EQRULE_DATA)
-(* : EQSUBST_TAC *)
+ : EQSUBST_TAC
= struct
-fun search_tb_lr_f f ft =
+(* FOR DEBUGGING...
+type trace_subst_errT = int (* subgoal *)
+ * Thm.thm (* thm with all goals *)
+ * (Thm.cterm list (* certified free var placeholders for vars *)
+ * Thm.thm) (* trivial thm of goal concl *)
+ (* possible matches/unifiers *)
+ * Thm.thm (* rule *)
+ * (((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 *);
+
+val trace_subst_err = (ref NONE : trace_subst_errT option ref);
+val trace_subst_search = ref false;
+exception trace_subst_exp of trace_subst_errT;
+ *)
+
+(* also defined in /HOL/Tools/inductive_codegen.ML,
+ maybe move this to seq.ML ? *)
+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 =
let
fun maux ft =
let val t' = (IsaFTerm.focus_of_fcterm ft)
- (* val _ = writeln ("Examining: " ^ (TermLib.string_of_term t')) *)
+ (* val _ =
+ if !trace_subst_search then
+ (writeln ("Examining: " ^ (TermLib.string_of_term t'));
+ TermLib.writeterm t'; ())
+ else (); *)
in
(case t' of
- (_ $ _) => Seq.append(f ft,
- Seq.append(maux (IsaFTerm.focus_left ft),
+ (_ $ _) => 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))
| leaf => f ft) end
in maux ft end;
-fun search_for_match sgn lhs maxidx =
+fun search_for_match sgn maxidx lhs =
IsaFTerm.find_fcterm_matches
- search_tb_lr_f
+ search_lr_f
(IsaFTerm.clean_unify_ft sgn maxidx lhs);
-
-(* CLEANUP: lots of duplication of code for substituting in
-assumptions and conclusion - this could be cleaned up a little. *)
+(* 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 *)
+(* m is instantiation/match information *)
+(* rule is the equation for substitution *)
+fun apply_subst_in_concl i th (cfvs, conclthm) rule m =
+ (RWInst.rw m rule conclthm)
+ |> IsaND.schemify_frees_to_vars cfvs
+ |> RWInst.beta_eta_contract_tac
+ |> (fn r => Tactic.rtac r i th);
-fun subst_concl rule cfvs i th (conclthm, concl_matches)=
- let
- fun apply_subst m =
- (RWInst.rw m rule conclthm)
- |> IsaND.schemify_frees_to_vars cfvs
- |> RWInst.beta_eta_contract_tac
- |> (fn r => Tactic.rtac r i th)
- |> Seq.map Drule.zero_var_indexes
- in
- Seq.flat (Seq.map apply_subst concl_matches)
- end;
+(*
+? is the following equivalent to rtac ?
+ |> Thm.lift_rule (th, i)
+ |> (fn r => Thm.bicompose false (false, r, Thm.nprems_of r) i th)
+
+*)
(* substitute within the conclusion of goal i of gth, using a meta
-equation rule *)
-fun subst rule i gth =
+equation rule. Note that we assume rule has var indicies zero'd *)
+fun prep_concl_subst searchf i gth =
let
val th = Thm.incr_indexes 1 gth;
val tgt_term = Thm.prop_of th;
- val maxidx = Term.maxidx_of_term tgt_term;
-
- val rule' = Drule.zero_var_indexes rule;
- val (lhs,_) = Logic.dest_equals (Thm.concl_of rule');
val sgn = Thm.sign_of_thm th;
val ctermify = Thm.cterm_of sgn;
@@ -93,61 +181,79 @@
val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
val cfvs = rev (map ctermify fvs);
- val conclthm = trivify (Logic.strip_imp_concl fixedbody);
- val concl_matches =
- search_for_match sgn lhs maxidx
- ((IsaFTerm.focus_right
- o IsaFTerm.focus_left
- o IsaFTerm.fcterm_of_term
- o Thm.prop_of) conclthm);
+ val conclterm = Logic.strip_imp_concl fixedbody;
+ val conclthm = trivify conclterm;
+ val maxidx = Term.maxidx_of_term conclterm;
in
- subst_concl rule' cfvs i th (conclthm, concl_matches)
+ ((cfvs, conclthm),
+ (fn lhs => searchf sgn maxidx lhs
+ ((IsaFTerm.focus_right
+ o IsaFTerm.focus_left
+ o IsaFTerm.fcterm_of_term
+ o Thm.prop_of) conclthm)))
end;
+
(* substitute using an object or meta level equality *)
fun eqsubst_tac' instepthm i th =
- let val stepthms = Seq.of_list (EqRuleData.prep_meta_eq instepthm) in
- Seq.flat (Seq.map (fn rule => subst rule i th) stepthms)
- end;
+ let
+ val (cvfsconclthm, findmatchf) =
+ prep_concl_subst search_for_match i th;
+
+ val stepthms =
+ Seq.map Drule.zero_var_indexes
+ (Seq.of_list (EqRuleData.prep_meta_eq instepthm));
+
+ fun rewrite_with_thm r =
+ let val (lhs,_) = Logic.dest_equals (Thm.concl_of r);
+ in (findmatchf lhs)
+ :-> (apply_subst_in_concl i th cvfsconclthm r) end;
+
+ in (stepthms :-> rewrite_with_thm) end;
+
+
(* substitute using one of the given theorems *)
fun eqsubst_tac instepthms i th =
- Seq.flat (Seq.map (fn r => eqsubst_tac' r i th) (Seq.of_list instepthms));
+ if Thm.nprems_of th < i then Seq.empty else
+ (Seq.of_list instepthms) :-> (fn r => eqsubst_tac' r i th);
(* inthms are the given arguments in Isar, and treated as eqstep with
the first one, then the second etc *)
fun eqsubst_meth inthms =
Method.METHOD
- (fn facts => (*first, insert chained facts*)
- HEADGOAL (Method.insert_tac facts THEN' eqsubst_tac inthms));
+ (fn facts =>
+ HEADGOAL ( Method.insert_tac facts THEN' eqsubst_tac inthms ));
-fun apply_subst_in_asm rule cfvs i th matchseq =
- let
- fun apply_subst ((j, pth), mseq) =
- Seq.flat (Seq.map
- (fn m =>
- (RWInst.rw m rule pth)
- |> Thm.permute_prems 0 ~1
- |> IsaND.schemify_frees_to_vars cfvs
- |> RWInst.beta_eta_contract_tac
- |> (fn r => Tactic.dtac r i th)
- |> Seq.map Drule.zero_var_indexes)
- mseq)
- in
- Seq.flat (Seq.map apply_subst matchseq)
- end;
+fun apply_subst_in_asm i th (cfvs, j, nprems, pth) rule m =
+ (RWInst.rw m rule pth)
+ |> Thm.permute_prems 0 ~1
+ |> IsaND.schemify_frees_to_vars cfvs
+ |> RWInst.beta_eta_contract_tac
+ |> (fn r => Tactic.dtac r i th);
+
+(*
+? should I be using bicompose what if we match more than one
+assumption, even after instantiation ? (back will work, but it would
+be nice to avoid the redudent search)
+
+something like...
+ |> Thm.lift_rule (th, i)
+ |> (fn r => Thm.bicompose false (false, r, Thm.nprems_of r - nprems) i th)
+
+*)
-(* substitute within an assumption of goal i of gth, using a meta
-equation rule *)
-fun subst_asm rule i gth =
+(* prepare to substitute within the j'th premise of subgoal i of gth,
+using a meta-level equation. Note that we assume rule has var indicies
+zero'd. Note that we also assume that premt is the j'th premice of
+subgoal i of gth. Note the repetition of work done for each
+assumption, i.e. this can be made more efficient for search over
+multiple assumptions. *)
+fun prep_subst_in_asm searchf i gth j =
let
val th = Thm.incr_indexes 1 gth;
val tgt_term = Thm.prop_of th;
- val maxidx = Term.maxidx_of_term tgt_term;
-
- val rule' = Drule.zero_var_indexes rule;
- val (lhs,_) = Logic.dest_equals (Thm.concl_of rule');
val sgn = Thm.sign_of_thm th;
val ctermify = Thm.cterm_of sgn;
@@ -156,37 +262,55 @@
val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
val cfvs = rev (map ctermify fvs);
- val premthms = Seq.of_list (IsaPLib.number_list 1
- (map trivify (Logic.strip_imp_prems fixedbody)));
- val prem_matches =
- Seq.map (fn (i, pth) =>
- ((i, pth), search_for_match sgn lhs maxidx
- ((IsaFTerm.focus_right
- o IsaFTerm.fcterm_of_term
- o Thm.prop_of) pth)))
- premthms;
+ val asmt = Library.nth_elem(j - 1,(Logic.strip_imp_prems fixedbody));
+ val asm_nprems = length (Logic.strip_imp_prems asmt);
+
+ val pth = trivify asmt;
+ val maxidx = Term.maxidx_of_term asmt;
+
in
- apply_subst_in_asm rule' cfvs i th prem_matches
+ ((cfvs, j, asm_nprems, pth),
+ (fn lhs => (searchf sgn maxidx lhs
+ ((IsaFTerm.focus_right
+ o IsaFTerm.fcterm_of_term
+ o Thm.prop_of) pth))))
end;
-(* substitute using an object or meta level equality *)
+(* prepare subst in every possible assumption *)
+fun prep_subst_in_asms searchf i gth =
+ Seq.map
+ (prep_subst_in_asm searchf i gth)
+ (Seq.of_list (IsaPLib.mk_num_list
+ (length (Logic.prems_of_goal (Thm.prop_of gth) i))));
+
+
+(* substitute in an assumption using an object or meta level equality *)
fun eqsubst_asm_tac' instepthm i th =
- let val stepthms = Seq.of_list (EqRuleData.prep_meta_eq instepthm) in
- Seq.flat (Seq.map (fn rule => subst_asm rule i th) stepthms)
+ let
+ val asmpreps = prep_subst_in_asms search_for_match i th;
+ val stepthms =
+ Seq.map Drule.zero_var_indexes
+ (Seq.of_list (EqRuleData.prep_meta_eq instepthm))
+
+ fun rewrite_with_thm (asminfo, findmatchf) r =
+ let val (lhs,_) = Logic.dest_equals (Thm.concl_of r);
+ in (findmatchf lhs)
+ :-> (apply_subst_in_asm i th asminfo r) end;
+ in
+ (asmpreps :-> (fn a => stepthms :-> rewrite_with_thm a))
end;
(* substitute using one of the given theorems *)
fun eqsubst_asm_tac instepthms i th =
- Seq.flat (Seq.map (fn r => eqsubst_asm_tac' r i th)
- (Seq.of_list instepthms));
+ if Thm.nprems_of th < i then Seq.empty else
+ (Seq.of_list instepthms) :-> (fn r => eqsubst_asm_tac' r i th);
(* inthms are the given arguments in Isar, and treated as eqstep with
the first one, then the second etc *)
fun eqsubst_asm_meth inthms =
Method.METHOD
- (fn facts => (*first, insert chained facts*)
- HEADGOAL (Method.insert_tac facts THEN' eqsubst_asm_tac inthms));
-
+ (fn facts =>
+ HEADGOAL (Method.insert_tac facts THEN' eqsubst_asm_tac inthms ));
(* combination method that takes a flag (true indicates that subst
should be done to an assumption, false = apply to the conclusion of