1.1 --- a/src/Provers/eqsubst.ML Fri Apr 22 14:15:01 2005 +0200
1.2 +++ b/src/Provers/eqsubst.ML Fri Apr 22 15:10:42 2005 +0200
1.3 @@ -29,9 +29,10 @@
1.4
1.5 type match =
1.6 ((Term.indexname * Term.typ) list (* type instantiations *)
1.7 - * (Term.indexname * Term.term) list) (* term instantiations *)
1.8 - * (string * Term.typ) list (* type abs env *)
1.9 - * Term.term (* outer term *)
1.10 + * (Term.indexname * Term.term) list) (* term instantiations *)
1.11 + * (string * Term.typ) list (* fake named type abs env *)
1.12 + * (string * Term.typ) list (* type abs env *)
1.13 + * Term.term (* outer term *)
1.14
1.15 val prep_subst_in_asm :
1.16 (Sign.sg (* sign for matching *)
1.17 @@ -86,13 +87,32 @@
1.18 -> match
1.19 -> Thm.thm Seq.seq (* substituted goal *)
1.20
1.21 + val searchf_tlr_unify_all :
1.22 + (Sign.sg -> int ->
1.23 + Term.term ->
1.24 + BasicIsaFTerm.FcTerm ->
1.25 + match Seq.seq)
1.26 + val searchf_tlr_unify_valid :
1.27 + (Sign.sg -> int ->
1.28 + Term.term ->
1.29 + BasicIsaFTerm.FcTerm ->
1.30 + match Seq.seq)
1.31 +
1.32 val eqsubst_asm_meth : Thm.thm list -> Proof.method
1.33 val eqsubst_asm_tac : Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
1.34 - val eqsubst_asm_tac' : Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq
1.35 + val eqsubst_asm_tac' :
1.36 + (Sign.sg -> int ->
1.37 + Term.term ->
1.38 + BasicIsaFTerm.FcTerm ->
1.39 + match Seq.seq) -> Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq
1.40
1.41 val eqsubst_meth : Thm.thm list -> Proof.method
1.42 val eqsubst_tac : Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
1.43 - val eqsubst_tac' : Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq
1.44 + val eqsubst_tac' :
1.45 + (Sign.sg -> int ->
1.46 + Term.term ->
1.47 + BasicIsaFTerm.FcTerm ->
1.48 + match Seq.seq) -> Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq
1.49
1.50 val meth : bool * Thm.thm list -> Proof.context -> Proof.method
1.51 val setup : (Theory.theory -> Theory.theory) list
1.52 @@ -106,6 +126,7 @@
1.53 type match =
1.54 ((Term.indexname * Term.typ) list (* type instantiations *)
1.55 * (Term.indexname * Term.term) list) (* term instantiations *)
1.56 + * (string * Term.typ) list (* fake named type abs env *)
1.57 * (string * Term.typ) list (* type abs env *)
1.58 * Term.term (* outer term *)
1.59
1.60 @@ -132,8 +153,8 @@
1.61 infix 5 :->;
1.62 fun s :-> f = Seq.flat (Seq.map f s);
1.63
1.64 -(* search from the top to bottom, left to right *)
1.65 -fun search_lr_f f ft =
1.66 +(* search from top, left to right, then down *)
1.67 +fun search_tlr_all_f f ft =
1.68 let
1.69 fun maux ft =
1.70 let val t' = (IsaFTerm.focus_of_fcterm ft)
1.71 @@ -147,15 +168,39 @@
1.72 (_ $ _) => Seq.append(maux (IsaFTerm.focus_left ft),
1.73 Seq.append(f ft,
1.74 maux (IsaFTerm.focus_right ft)))
1.75 - | (Abs _) => Seq.append (f ft, maux (IsaFTerm.focus_abs ft))
1.76 + | (Abs _) => Seq.append(f ft, maux (IsaFTerm.focus_abs ft))
1.77 | leaf => f ft) end
1.78 in maux ft end;
1.79
1.80 -fun search_for_match sgn maxidx lhs =
1.81 +(* search from top, left to right, then down *)
1.82 +fun search_tlr_valid_f f ft =
1.83 + let
1.84 + fun maux ft =
1.85 + let
1.86 + val hereseq = if IsaFTerm.valid_match_start ft then f ft else Seq.empty
1.87 + in
1.88 + (case (IsaFTerm.focus_of_fcterm ft) of
1.89 + (_ $ _) => Seq.append(maux (IsaFTerm.focus_left ft),
1.90 + Seq.append(hereseq,
1.91 + maux (IsaFTerm.focus_right ft)))
1.92 + | (Abs _) => Seq.append(hereseq, maux (IsaFTerm.focus_abs ft))
1.93 + | leaf => hereseq)
1.94 + end
1.95 + in maux ft end;
1.96 +
1.97 +(* search all unifications *)
1.98 +fun searchf_tlr_unify_all sgn maxidx lhs =
1.99 IsaFTerm.find_fcterm_matches
1.100 - search_lr_f
1.101 + search_tlr_all_f
1.102 (IsaFTerm.clean_unify_ft sgn maxidx lhs);
1.103
1.104 +(* search only for 'valid' unifiers (non abs subterms and non vars) *)
1.105 +fun searchf_tlr_unify_valid sgn maxidx lhs =
1.106 + IsaFTerm.find_fcterm_matches
1.107 + search_tlr_valid_f
1.108 + (IsaFTerm.clean_unify_ft sgn maxidx lhs);
1.109 +
1.110 +
1.111 (* apply a substitution in the conclusion of the theorem th *)
1.112 (* cfvs are certified free var placeholders for goal params *)
1.113 (* conclthm is a theorem of for just the conclusion *)
1.114 @@ -168,9 +213,7 @@
1.115 |> (fn r => Tactic.rtac r i th);
1.116
1.117 (*
1.118 -? is the following equivalent to rtac ?
1.119
1.120 - |> Thm.lift_rule (th, i)
1.121 |> (fn r => Thm.bicompose false (false, r, Thm.nprems_of r) i th)
1.122
1.123 *)
1.124 @@ -203,10 +246,10 @@
1.125
1.126
1.127 (* substitute using an object or meta level equality *)
1.128 -fun eqsubst_tac' instepthm i th =
1.129 +fun eqsubst_tac' searchf instepthm i th =
1.130 let
1.131 val (cvfsconclthm, findmatchf) =
1.132 - prep_concl_subst search_for_match i th;
1.133 + prep_concl_subst searchf i th;
1.134
1.135 val stepthms =
1.136 Seq.map Drule.zero_var_indexes
1.137 @@ -223,7 +266,8 @@
1.138 (* substitute using one of the given theorems *)
1.139 fun eqsubst_tac instepthms i th =
1.140 if Thm.nprems_of th < i then Seq.empty else
1.141 - (Seq.of_list instepthms) :-> (fn r => eqsubst_tac' r i th);
1.142 + (Seq.of_list instepthms)
1.143 + :-> (fn r => eqsubst_tac' searchf_tlr_unify_valid r i th);
1.144
1.145 (* inthms are the given arguments in Isar, and treated as eqstep with
1.146 the first one, then the second etc *)
1.147 @@ -293,9 +337,9 @@
1.148
1.149
1.150 (* substitute in an assumption using an object or meta level equality *)
1.151 -fun eqsubst_asm_tac' instepthm i th =
1.152 +fun eqsubst_asm_tac' searchf instepthm i th =
1.153 let
1.154 - val asmpreps = prep_subst_in_asms search_for_match i th;
1.155 + val asmpreps = prep_subst_in_asms searchf i th;
1.156 val stepthms =
1.157 Seq.map Drule.zero_var_indexes
1.158 (Seq.of_list (EqRuleData.prep_meta_eq instepthm))
1.159 @@ -311,7 +355,8 @@
1.160 (* substitute using one of the given theorems *)
1.161 fun eqsubst_asm_tac instepthms i th =
1.162 if Thm.nprems_of th < i then Seq.empty else
1.163 - (Seq.of_list instepthms) :-> (fn r => eqsubst_asm_tac' r i th);
1.164 + (Seq.of_list instepthms)
1.165 + :-> (fn r => eqsubst_asm_tac' searchf_tlr_unify_valid r i th);
1.166
1.167 (* inthms are the given arguments in Isar, and treated as eqstep with
1.168 the first one, then the second etc *)