1.1 --- a/src/Provers/eqsubst.ML Tue Jun 13 15:07:58 2006 +0200
1.2 +++ b/src/Provers/eqsubst.ML Tue Jun 13 15:42:19 2006 +0200
1.3 @@ -7,11 +7,117 @@
1.4
1.5 signature EQSUBST =
1.6 sig
1.7 - val setup : theory -> theory
1.8 + (* a type abriviation for match information *)
1.9 + type match =
1.10 + ((indexname * (sort * typ)) list (* type instantiations *)
1.11 + * (indexname * (typ * term)) list) (* term instantiations *)
1.12 + * (string * typ) list (* fake named type abs env *)
1.13 + * (string * typ) list (* type abs env *)
1.14 + * term (* outer term *)
1.15 +
1.16 + type searchinfo =
1.17 + theory
1.18 + * int (* maxidx *)
1.19 + * Zipper.T (* focusterm to search under *)
1.20 +
1.21 + exception eqsubst_occL_exp of
1.22 + string * int list * Thm.thm list * int * Thm.thm
1.23 +
1.24 + (* low level substitution functions *)
1.25 + val apply_subst_in_asm :
1.26 + int ->
1.27 + Thm.thm ->
1.28 + Thm.thm ->
1.29 + (Thm.cterm list * int * 'a * Thm.thm) * match -> Thm.thm Seq.seq
1.30 + val apply_subst_in_concl :
1.31 + int ->
1.32 + Thm.thm ->
1.33 + Thm.cterm list * Thm.thm ->
1.34 + Thm.thm -> match -> Thm.thm Seq.seq
1.35 +
1.36 + (* matching/unification within zippers *)
1.37 + val clean_match_z :
1.38 + Context.theory -> Term.term -> Zipper.T -> match option
1.39 + val clean_unify_z :
1.40 + Context.theory -> int -> Term.term -> Zipper.T -> match Seq.seq
1.41 +
1.42 + (* skipping things in seq seq's *)
1.43 +
1.44 + (* skipping non-empty sub-sequences but when we reach the end
1.45 + of the seq, remembering how much we have left to skip. *)
1.46 + datatype 'a skipseq = SkipMore of int
1.47 + | SkipSeq of 'a Seq.seq Seq.seq;
1.48 +
1.49 + val skip_first_asm_occs_search :
1.50 + ('a -> 'b -> 'c Seq.seq Seq.seq) ->
1.51 + 'a -> int -> 'b -> 'c skipseq
1.52 + val skip_first_occs_search :
1.53 + int -> ('a -> 'b -> 'c Seq.seq Seq.seq) -> 'a -> 'b -> 'c Seq.seq
1.54 + val skipto_skipseq : int -> 'a Seq.seq Seq.seq -> 'a skipseq
1.55 +
1.56 + (* tactics *)
1.57 + val eqsubst_asm_tac :
1.58 + Proof.context ->
1.59 + int list -> Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
1.60 + val eqsubst_asm_tac' :
1.61 + Proof.context ->
1.62 + (searchinfo -> int -> Term.term -> match skipseq) ->
1.63 + int -> Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq
1.64 + val eqsubst_tac :
1.65 + Proof.context ->
1.66 + int list -> Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
1.67 + val eqsubst_tac' :
1.68 + Proof.context ->
1.69 + (searchinfo -> Term.term -> match Seq.seq)
1.70 + -> Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq
1.71 +
1.72 +
1.73 + val fakefree_badbounds :
1.74 + (string * Term.typ) list ->
1.75 + Term.term ->
1.76 + (string * Term.typ) list * (string * Term.typ) list * Term.term
1.77 +
1.78 + val mk_foo_match :
1.79 + (Term.term -> Term.term) ->
1.80 + ('a * Term.typ) list -> Term.term -> Term.term
1.81 +
1.82 + (* preparing substitution *)
1.83 + val prep_meta_eq : Proof.context -> Thm.thm -> Thm.thm list
1.84 + val prep_concl_subst :
1.85 + int -> Thm.thm -> (Thm.cterm list * Thm.thm) * searchinfo
1.86 + val prep_subst_in_asm :
1.87 + int -> Thm.thm -> int ->
1.88 + (Thm.cterm list * int * int * Thm.thm) * searchinfo
1.89 + val prep_subst_in_asms :
1.90 + int -> Thm.thm ->
1.91 + ((Thm.cterm list * int * int * Thm.thm) * searchinfo) list
1.92 + val prep_zipper_match :
1.93 + Zipper.T -> Term.term * ((string * Term.typ) list * (string * Term.typ) list * Term.term)
1.94 +
1.95 + (* search for substitutions *)
1.96 + val valid_match_start : Zipper.T -> bool
1.97 + val search_lr_all : Zipper.T -> Zipper.T Seq.seq
1.98 + val search_lr_valid : (Zipper.T -> bool) -> Zipper.T -> Zipper.T Seq.seq
1.99 + val searchf_lr_unify_all :
1.100 + searchinfo -> Term.term -> match Seq.seq Seq.seq
1.101 + val searchf_lr_unify_valid :
1.102 + searchinfo -> Term.term -> match Seq.seq Seq.seq
1.103 +
1.104 +
1.105 + (* syntax tools *)
1.106 + val ith_syntax : Args.T list -> int list * Args.T list
1.107 + val options_syntax : Args.T list -> bool * Args.T list
1.108 +
1.109 + (* Isar level hooks *)
1.110 + val eqsubst_asm_meth : Proof.context -> int list -> Thm.thm list -> Method.method
1.111 + val eqsubst_meth : Proof.context -> int list -> Thm.thm list -> Method.method
1.112 + val subst_meth : Method.src -> ProofContext.context -> Method.method
1.113 + val setup : theory -> theory
1.114 +
1.115 end;
1.116
1.117 structure EqSubst
1.118 -(* : EQSUBST *)
1.119 +: EQSUBST
1.120 = struct
1.121
1.122 structure Z = Zipper;
1.123 @@ -187,30 +293,31 @@
1.124 | _ => false); (* avoid vars - always suceeds uninterestingly. *)
1.125
1.126 (* search from top, left to right, then down *)
1.127 -val search_tlr_all = ZipperSearch.all_td_lr;
1.128 +val search_lr_all = ZipperSearch.all_bl_ur;
1.129
1.130 (* search from top, left to right, then down *)
1.131 -fun search_tlr_valid validf =
1.132 +fun search_lr_valid validf =
1.133 let
1.134 fun sf_valid_td_lr z =
1.135 let val here = if validf z then [Z.Here z] else [] in
1.136 case Z.trm z
1.137 - of _ $ _ => here @ [Z.LookIn (Z.move_down_left z),
1.138 - Z.LookIn (Z.move_down_right z)]
1.139 + of _ $ _ => [Z.LookIn (Z.move_down_left z)]
1.140 + @ here
1.141 + @ [Z.LookIn (Z.move_down_right z)]
1.142 | Abs _ => here @ [Z.LookIn (Z.move_down_abs z)]
1.143 | _ => here
1.144 end;
1.145 in Z.lzy_search sf_valid_td_lr end;
1.146
1.147 (* search all unifications *)
1.148 -fun searchf_tlr_unify_all (sgn, maxidx, z) lhs =
1.149 +fun searchf_lr_unify_all (sgn, maxidx, z) lhs =
1.150 Seq.map (clean_unify_z sgn maxidx lhs)
1.151 - (Z.limit_apply search_tlr_all z);
1.152 + (Z.limit_apply search_lr_all z);
1.153
1.154 (* search only for 'valid' unifiers (non abs subterms and non vars) *)
1.155 -fun searchf_tlr_unify_valid (sgn, maxidx, z) lhs =
1.156 +fun searchf_lr_unify_valid (sgn, maxidx, z) lhs =
1.157 Seq.map (clean_unify_z sgn maxidx lhs)
1.158 - (Z.limit_apply (search_tlr_valid valid_match_start) z);
1.159 + (Z.limit_apply (search_lr_valid valid_match_start) z);
1.160
1.161
1.162 (* apply a substitution in the conclusion of the theorem th *)
1.163 @@ -285,7 +392,7 @@
1.164 (fn r => eqsubst_tac'
1.165 ctxt
1.166 (skip_first_occs_search
1.167 - occ searchf_tlr_unify_valid) r
1.168 + occ searchf_lr_unify_valid) r
1.169 (i + ((Thm.nprems_of th) - nprems))
1.170 th);
1.171 val sortedoccL =
1.172 @@ -401,7 +508,7 @@
1.173 thmseq |> Seq.maps
1.174 (fn r =>
1.175 eqsubst_asm_tac' ctxt (skip_first_asm_occs_search
1.176 - searchf_tlr_unify_valid) occK r
1.177 + searchf_lr_unify_valid) occK r
1.178 (i + ((Thm.nprems_of th) - nprems))
1.179 th);
1.180 val sortedoccs =