moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
authorwenzelm
Sat Feb 28 14:02:12 2009 +0100 (2009-02-28)
changeset 301605f7b17941730
parent 30159 7b55b6b5c0c2
child 30161 c26e515f1c29
moved some generic tools to src/Tools/ -- src/Provers is essentially obsolete;
src/FOL/IFOL.thy
src/FOL/IsaMakefile
src/HOL/HOL.thy
src/HOL/IsaMakefile
src/Provers/coherent.ML
src/Provers/eqsubst.ML
src/Provers/project_rule.ML
src/Tools/coherent.ML
src/Tools/eqsubst.ML
src/Tools/project_rule.ML
     1.1 --- a/src/FOL/IFOL.thy	Sat Feb 28 13:54:47 2009 +0100
     1.2 +++ b/src/FOL/IFOL.thy	Sat Feb 28 14:02:12 2009 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      FOL/IFOL.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Lawrence C Paulson and Markus Wenzel
     1.7  *)
     1.8  
     1.9 @@ -14,9 +13,9 @@
    1.10    "~~/src/Tools/IsaPlanner/isand.ML"
    1.11    "~~/src/Tools/IsaPlanner/rw_tools.ML"
    1.12    "~~/src/Tools/IsaPlanner/rw_inst.ML"
    1.13 -  "~~/src/Provers/eqsubst.ML"
    1.14 +  "~~/src/Tools/eqsubst.ML"
    1.15    "~~/src/Provers/quantifier1.ML"
    1.16 -  "~~/src/Provers/project_rule.ML"
    1.17 +  "~~/src/Tools/project_rule.ML"
    1.18    "~~/src/Tools/atomize_elim.ML"
    1.19    ("fologic.ML")
    1.20    ("hypsubstdata.ML")
     2.1 --- a/src/FOL/IsaMakefile	Sat Feb 28 13:54:47 2009 +0100
     2.2 +++ b/src/FOL/IsaMakefile	Sat Feb 28 14:02:12 2009 +0100
     2.3 @@ -32,9 +32,9 @@
     2.4    $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML			\
     2.5    $(SRC)/Tools/IsaPlanner/zipper.ML $(SRC)/Tools/IsaPlanner/isand.ML	\
     2.6    $(SRC)/Tools/IsaPlanner/rw_tools.ML					\
     2.7 -  $(SRC)/Tools/IsaPlanner/rw_inst.ML $(SRC)/Provers/eqsubst.ML		\
     2.8 +  $(SRC)/Tools/IsaPlanner/rw_inst.ML $(SRC)/Tools/eqsubst.ML		\
     2.9    $(SRC)/Provers/hypsubst.ML $(SRC)/Tools/induct.ML			\
    2.10 -  $(SRC)/Tools/atomize_elim.ML $(SRC)/Provers/project_rule.ML		\
    2.11 +  $(SRC)/Tools/atomize_elim.ML $(SRC)/Tools/project_rule.ML		\
    2.12    $(SRC)/Provers/quantifier1.ML $(SRC)/Provers/splitter.ML FOL.thy	\
    2.13    IFOL.thy ROOT.ML blastdata.ML cladata.ML document/root.tex		\
    2.14    fologic.ML hypsubstdata.ML intprover.ML simpdata.ML
     3.1 --- a/src/HOL/HOL.thy	Sat Feb 28 13:54:47 2009 +0100
     3.2 +++ b/src/HOL/HOL.thy	Sat Feb 28 14:02:12 2009 +0100
     3.3 @@ -12,14 +12,14 @@
     3.4    "~~/src/Tools/IsaPlanner/isand.ML"
     3.5    "~~/src/Tools/IsaPlanner/rw_tools.ML"
     3.6    "~~/src/Tools/IsaPlanner/rw_inst.ML"
     3.7 -  "~~/src/Provers/project_rule.ML"
     3.8 +  "~~/src/Tools/project_rule.ML"
     3.9    "~~/src/Provers/hypsubst.ML"
    3.10    "~~/src/Provers/splitter.ML"
    3.11    "~~/src/Provers/classical.ML"
    3.12    "~~/src/Provers/blast.ML"
    3.13    "~~/src/Provers/clasimp.ML"
    3.14 -  "~~/src/Provers/coherent.ML"
    3.15 -  "~~/src/Provers/eqsubst.ML"
    3.16 +  "~~/src/Tools/coherent.ML"
    3.17 +  "~~/src/Tools/eqsubst.ML"
    3.18    "~~/src/Provers/quantifier1.ML"
    3.19    ("Tools/simpdata.ML")
    3.20    "~~/src/Tools/random_word.ML"
     4.1 --- a/src/HOL/IsaMakefile	Sat Feb 28 13:54:47 2009 +0100
     4.2 +++ b/src/HOL/IsaMakefile	Sat Feb 28 14:02:12 2009 +0100
     4.3 @@ -78,38 +78,38 @@
     4.4  $(OUT)/Pure: Pure
     4.5  
     4.6  BASE_DEPENDENCIES = $(OUT)/Pure \
     4.7 +  $(SRC)/Provers/blast.ML \
     4.8 +  $(SRC)/Provers/clasimp.ML \
     4.9 +  $(SRC)/Provers/classical.ML \
    4.10 +  $(SRC)/Provers/hypsubst.ML \
    4.11 +  $(SRC)/Provers/quantifier1.ML \
    4.12 +  $(SRC)/Provers/splitter.ML \
    4.13 +  $(SRC)/Tools/IsaPlanner/isand.ML \
    4.14 +  $(SRC)/Tools/IsaPlanner/rw_inst.ML \
    4.15 +  $(SRC)/Tools/IsaPlanner/rw_tools.ML \
    4.16 +  $(SRC)/Tools/IsaPlanner/zipper.ML \
    4.17 +  $(SRC)/Tools/atomize_elim.ML \
    4.18 +  $(SRC)/Tools/code/code_funcgr.ML \
    4.19 +  $(SRC)/Tools/code/code_haskell.ML \
    4.20 +  $(SRC)/Tools/code/code_ml.ML \
    4.21 +  $(SRC)/Tools/code/code_name.ML \
    4.22 +  $(SRC)/Tools/code/code_printer.ML \
    4.23 +  $(SRC)/Tools/code/code_target.ML \
    4.24 +  $(SRC)/Tools/code/code_thingol.ML \
    4.25 +  $(SRC)/Tools/code/code_wellsorted.ML \
    4.26 +  $(SRC)/Tools/coherent.ML \
    4.27 +  $(SRC)/Tools/eqsubst.ML \
    4.28 +  $(SRC)/Tools/induct.ML \
    4.29 +  $(SRC)/Tools/induct_tacs.ML \
    4.30 +  $(SRC)/Tools/nbe.ML \
    4.31 +  $(SRC)/Tools/project_rule.ML \
    4.32 +  $(SRC)/Tools/random_word.ML \
    4.33 +  $(SRC)/Tools/value.ML \
    4.34    Code_Setup.thy \
    4.35    HOL.thy \
    4.36    Tools/hologic.ML \
    4.37    Tools/recfun_codegen.ML \
    4.38    Tools/simpdata.ML \
    4.39 -  $(SRC)/Tools/atomize_elim.ML \
    4.40 -  $(SRC)/Tools/code/code_funcgr.ML \
    4.41 -  $(SRC)/Tools/code/code_wellsorted.ML \
    4.42 -  $(SRC)/Tools/code/code_name.ML \
    4.43 -  $(SRC)/Tools/code/code_printer.ML \
    4.44 -  $(SRC)/Tools/code/code_target.ML \
    4.45 -  $(SRC)/Tools/code/code_ml.ML \
    4.46 -  $(SRC)/Tools/code/code_haskell.ML \
    4.47 -  $(SRC)/Tools/code/code_thingol.ML \
    4.48 -  $(SRC)/Tools/induct.ML \
    4.49 -  $(SRC)/Tools/induct_tacs.ML \
    4.50 -  $(SRC)/Tools/IsaPlanner/isand.ML \
    4.51 -  $(SRC)/Tools/IsaPlanner/rw_inst.ML \
    4.52 -  $(SRC)/Tools/IsaPlanner/rw_tools.ML \
    4.53 -  $(SRC)/Tools/IsaPlanner/zipper.ML \
    4.54 -  $(SRC)/Tools/nbe.ML \
    4.55 -  $(SRC)/Tools/random_word.ML \
    4.56 -  $(SRC)/Tools/value.ML \
    4.57 -  $(SRC)/Provers/blast.ML \
    4.58 -  $(SRC)/Provers/clasimp.ML \
    4.59 -  $(SRC)/Provers/classical.ML \
    4.60 -  $(SRC)/Provers/coherent.ML \
    4.61 -  $(SRC)/Provers/eqsubst.ML \
    4.62 -  $(SRC)/Provers/hypsubst.ML \
    4.63 -  $(SRC)/Provers/project_rule.ML \
    4.64 -  $(SRC)/Provers/quantifier1.ML \
    4.65 -  $(SRC)/Provers/splitter.ML \
    4.66  
    4.67  $(OUT)/HOL-Base: base.ML $(BASE_DEPENDENCIES)
    4.68  	@$(ISABELLE_TOOL) usedir -b -f base.ML -d false -g false $(OUT)/Pure HOL-Base
     5.1 --- a/src/Provers/coherent.ML	Sat Feb 28 13:54:47 2009 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,233 +0,0 @@
     5.4 -(*  Title:      Provers/coherent.ML
     5.5 -    Author:     Stefan Berghofer, TU Muenchen
     5.6 -    Author:     Marc Bezem, Institutt for Informatikk, Universitetet i Bergen 
     5.7 -
     5.8 -Prover for coherent logic, see e.g.
     5.9 -
    5.10 -  Marc Bezem and Thierry Coquand, Automating Coherent Logic, LPAR 2005
    5.11 -
    5.12 -for a description of the algorithm.
    5.13 -*)
    5.14 -
    5.15 -signature COHERENT_DATA =
    5.16 -sig
    5.17 -  val atomize_elimL: thm
    5.18 -  val atomize_exL: thm
    5.19 -  val atomize_conjL: thm
    5.20 -  val atomize_disjL: thm
    5.21 -  val operator_names: string list
    5.22 -end;
    5.23 -
    5.24 -signature COHERENT =
    5.25 -sig
    5.26 -  val verbose: bool ref
    5.27 -  val show_facts: bool ref
    5.28 -  val coherent_tac: thm list -> Proof.context -> int -> tactic
    5.29 -  val coherent_meth: thm list -> Proof.context -> Proof.method
    5.30 -  val setup: theory -> theory
    5.31 -end;
    5.32 -
    5.33 -functor CoherentFun(Data: COHERENT_DATA) : COHERENT =
    5.34 -struct
    5.35 -
    5.36 -val verbose = ref false;
    5.37 -
    5.38 -fun message f = if !verbose then tracing (f ()) else ();
    5.39 -
    5.40 -datatype cl_prf =
    5.41 -  ClPrf of thm * (Type.tyenv * Envir.tenv) * ((indexname * typ) * term) list *
    5.42 -  int list * (term list * cl_prf) list;
    5.43 -
    5.44 -val is_atomic = not o exists_Const (member (op =) Data.operator_names o #1);
    5.45 -
    5.46 -local open Conv in
    5.47 -
    5.48 -fun rulify_elim_conv ct =
    5.49 -  if is_atomic (Logic.strip_imp_concl (term_of ct)) then all_conv ct
    5.50 -  else concl_conv (length (Logic.strip_imp_prems (term_of ct)))
    5.51 -    (rewr_conv (symmetric Data.atomize_elimL) then_conv
    5.52 -     MetaSimplifier.rewrite true (map symmetric
    5.53 -       [Data.atomize_exL, Data.atomize_conjL, Data.atomize_disjL])) ct
    5.54 -
    5.55 -end;
    5.56 -
    5.57 -fun rulify_elim th = MetaSimplifier.norm_hhf (Conv.fconv_rule rulify_elim_conv th);
    5.58 -
    5.59 -(* Decompose elimination rule of the form
    5.60 -   A1 ==> ... ==> Am ==> (!!xs1. Bs1 ==> P) ==> ... ==> (!!xsn. Bsn ==> P) ==> P
    5.61 -*)
    5.62 -fun dest_elim prop =
    5.63 -  let
    5.64 -    val prems = Logic.strip_imp_prems prop;
    5.65 -    val concl = Logic.strip_imp_concl prop;
    5.66 -    val (prems1, prems2) =
    5.67 -      take_suffix (fn t => Logic.strip_assums_concl t = concl) prems;
    5.68 -  in
    5.69 -    (prems1,
    5.70 -     if null prems2 then [([], [concl])]
    5.71 -     else map (fn t =>
    5.72 -       (map snd (Logic.strip_params t), Logic.strip_assums_hyp t)) prems2)
    5.73 -  end;
    5.74 -
    5.75 -fun mk_rule th =
    5.76 -  let
    5.77 -    val th' = rulify_elim th;
    5.78 -    val (prems, cases) = dest_elim (prop_of th')
    5.79 -  in (th', prems, cases) end;
    5.80 -
    5.81 -fun mk_dom ts = fold (fn t =>
    5.82 -  Typtab.map_default (fastype_of t, []) (fn us => us @ [t])) ts Typtab.empty;
    5.83 -
    5.84 -val empty_env = (Vartab.empty, Vartab.empty);
    5.85 -
    5.86 -(* Find matcher that makes conjunction valid in given state *)
    5.87 -fun valid_conj ctxt facts env [] = Seq.single (env, [])
    5.88 -  | valid_conj ctxt facts env (t :: ts) =
    5.89 -      Seq.maps (fn (u, x) => Seq.map (apsnd (cons x))
    5.90 -        (valid_conj ctxt facts
    5.91 -           (Pattern.match (ProofContext.theory_of ctxt) (t, u) env) ts
    5.92 -         handle Pattern.MATCH => Seq.empty))
    5.93 -          (Seq.of_list (sort (int_ord o pairself snd) (Net.unify_term facts t)));
    5.94 -
    5.95 -(* Instantiate variables that only occur free in conlusion *)
    5.96 -fun inst_extra_vars ctxt dom cs =
    5.97 -  let
    5.98 -    val vs = fold Term.add_vars (maps snd cs) [];
    5.99 -    fun insts [] inst = Seq.single inst
   5.100 -      | insts ((ixn, T) :: vs') inst = Seq.maps
   5.101 -          (fn t => insts vs' (((ixn, T), t) :: inst))
   5.102 -          (Seq.of_list (case Typtab.lookup dom T of
   5.103 -             NONE => error ("Unknown domain: " ^
   5.104 -               Syntax.string_of_typ ctxt T ^ "\nfor term(s) " ^
   5.105 -               commas (maps (map (Syntax.string_of_term ctxt) o snd) cs))
   5.106 -           | SOME ts => ts))
   5.107 -  in Seq.map (fn inst =>
   5.108 -    (inst, map (apsnd (map (subst_Vars (map (apfst fst) inst)))) cs))
   5.109 -      (insts vs [])
   5.110 -  end;
   5.111 -
   5.112 -(* Check whether disjunction is valid in given state *)
   5.113 -fun is_valid_disj ctxt facts [] = false
   5.114 -  | is_valid_disj ctxt facts ((Ts, ts) :: ds) =
   5.115 -      let val vs = rev (map_index (fn (i, T) => Var (("x", i), T)) Ts)
   5.116 -      in case Seq.pull (valid_conj ctxt facts empty_env
   5.117 -        (map (fn t => subst_bounds (vs, t)) ts)) of
   5.118 -          SOME _ => true
   5.119 -        | NONE => is_valid_disj ctxt facts ds
   5.120 -      end;
   5.121 -
   5.122 -val show_facts = ref false;
   5.123 -
   5.124 -fun string_of_facts ctxt s facts = space_implode "\n"
   5.125 -  (s :: map (Syntax.string_of_term ctxt)
   5.126 -     (map fst (sort (int_ord o pairself snd) (Net.content facts)))) ^ "\n\n";
   5.127 -
   5.128 -fun print_facts ctxt facts =
   5.129 -  if !show_facts then message (fn () => string_of_facts ctxt "Facts:" facts)
   5.130 -  else ();
   5.131 -
   5.132 -fun valid ctxt rules goal dom facts nfacts nparams =
   5.133 -  let val seq = Seq.of_list rules |> Seq.maps (fn (th, ps, cs) =>
   5.134 -    valid_conj ctxt facts empty_env ps |> Seq.maps (fn (env as (tye, _), is) =>
   5.135 -      let val cs' = map (fn (Ts, ts) =>
   5.136 -        (map (Envir.typ_subst_TVars tye) Ts, map (Envir.subst_vars env) ts)) cs
   5.137 -      in
   5.138 -        inst_extra_vars ctxt dom cs' |>
   5.139 -          Seq.map_filter (fn (inst, cs'') =>
   5.140 -            if is_valid_disj ctxt facts cs'' then NONE
   5.141 -            else SOME (th, env, inst, is, cs''))
   5.142 -      end))
   5.143 -  in
   5.144 -    case Seq.pull seq of
   5.145 -      NONE => (tracing (string_of_facts ctxt "Countermodel found:" facts); NONE)
   5.146 -    | SOME ((th, env, inst, is, cs), _) =>
   5.147 -        if cs = [([], [goal])] then SOME (ClPrf (th, env, inst, is, []))
   5.148 -        else
   5.149 -          (case valid_cases ctxt rules goal dom facts nfacts nparams cs of
   5.150 -             NONE => NONE
   5.151 -           | SOME prfs => SOME (ClPrf (th, env, inst, is, prfs)))
   5.152 -  end
   5.153 -
   5.154 -and valid_cases ctxt rules goal dom facts nfacts nparams [] = SOME []
   5.155 -  | valid_cases ctxt rules goal dom facts nfacts nparams ((Ts, ts) :: ds) =
   5.156 -      let
   5.157 -        val _ = message (fn () => "case " ^ commas (map (Syntax.string_of_term ctxt) ts));
   5.158 -        val params = rev (map_index (fn (i, T) =>
   5.159 -          Free ("par" ^ string_of_int (nparams + i), T)) Ts);
   5.160 -        val ts' = map_index (fn (i, t) =>
   5.161 -          (subst_bounds (params, t), nfacts + i)) ts;
   5.162 -        val dom' = fold (fn (T, p) =>
   5.163 -          Typtab.map_default (T, []) (fn ps => ps @ [p]))
   5.164 -            (Ts ~~ params) dom;
   5.165 -        val facts' = fold (fn (t, i) => Net.insert_term op =
   5.166 -          (t, (t, i))) ts' facts
   5.167 -      in
   5.168 -        case valid ctxt rules goal dom' facts'
   5.169 -          (nfacts + length ts) (nparams + length Ts) of
   5.170 -          NONE => NONE
   5.171 -        | SOME prf => (case valid_cases ctxt rules goal dom facts nfacts nparams ds of
   5.172 -            NONE => NONE
   5.173 -          | SOME prfs => SOME ((params, prf) :: prfs))
   5.174 -      end;
   5.175 -
   5.176 -(** proof replaying **)
   5.177 -
   5.178 -fun thm_of_cl_prf thy goal asms (ClPrf (th, (tye, env), insts, is, prfs)) =
   5.179 -  let
   5.180 -    val _ = message (fn () => space_implode "\n"
   5.181 -      ("asms:" :: map Display.string_of_thm asms) ^ "\n\n");
   5.182 -    val th' = Drule.implies_elim_list
   5.183 -      (Thm.instantiate
   5.184 -         (map (fn (ixn, (S, T)) =>
   5.185 -            (Thm.ctyp_of thy (TVar ((ixn, S))), Thm.ctyp_of thy T))
   5.186 -               (Vartab.dest tye),
   5.187 -          map (fn (ixn, (T, t)) =>
   5.188 -            (Thm.cterm_of thy (Var (ixn, Envir.typ_subst_TVars tye T)),
   5.189 -             Thm.cterm_of thy t)) (Vartab.dest env) @
   5.190 -          map (fn (ixnT, t) =>
   5.191 -            (Thm.cterm_of thy (Var ixnT), Thm.cterm_of thy t)) insts) th)
   5.192 -      (map (nth asms) is);
   5.193 -    val (_, cases) = dest_elim (prop_of th')
   5.194 -  in
   5.195 -    case (cases, prfs) of
   5.196 -      ([([], [_])], []) => th'
   5.197 -    | ([([], [_])], [([], prf)]) => thm_of_cl_prf thy goal (asms @ [th']) prf
   5.198 -    | _ => Drule.implies_elim_list
   5.199 -        (Thm.instantiate (Thm.match
   5.200 -           (Drule.strip_imp_concl (cprop_of th'), goal)) th')
   5.201 -        (map (thm_of_case_prf thy goal asms) (prfs ~~ cases))
   5.202 -  end
   5.203 -
   5.204 -and thm_of_case_prf thy goal asms ((params, prf), (_, asms')) =
   5.205 -  let
   5.206 -    val cparams = map (cterm_of thy) params;
   5.207 -    val asms'' = map (cterm_of thy o curry subst_bounds (rev params)) asms'
   5.208 -  in
   5.209 -    Drule.forall_intr_list cparams (Drule.implies_intr_list asms''
   5.210 -      (thm_of_cl_prf thy goal (asms @ map Thm.assume asms'') prf))
   5.211 -  end;
   5.212 -
   5.213 -
   5.214 -(** external interface **)
   5.215 -
   5.216 -fun coherent_tac rules ctxt = SUBPROOF (fn {prems, concl, params, context, ...} =>
   5.217 -  rtac (rulify_elim_conv concl RS equal_elim_rule2) 1 THEN
   5.218 -  SUBPROOF (fn {prems = prems', concl, context, ...} =>
   5.219 -    let val xs = map term_of params @
   5.220 -      map (fn (_, s) => Free (s, the (Variable.default_type context s)))
   5.221 -        (Variable.fixes_of context)
   5.222 -    in
   5.223 -      case valid context (map mk_rule (prems' @ prems @ rules)) (term_of concl)
   5.224 -           (mk_dom xs) Net.empty 0 0 of
   5.225 -         NONE => no_tac
   5.226 -       | SOME prf =>
   5.227 -           rtac (thm_of_cl_prf (ProofContext.theory_of context) concl [] prf) 1
   5.228 -    end) context 1) ctxt;
   5.229 -
   5.230 -fun coherent_meth rules ctxt =
   5.231 -  Method.METHOD (fn facts => coherent_tac (facts @ rules) ctxt 1);
   5.232 -
   5.233 -val setup = Method.add_method
   5.234 -  ("coherent", Method.thms_ctxt_args coherent_meth, "Prove coherent formula");
   5.235 -
   5.236 -end;
     6.1 --- a/src/Provers/eqsubst.ML	Sat Feb 28 13:54:47 2009 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,575 +0,0 @@
     6.4 -(*  Title:      Provers/eqsubst.ML
     6.5 -    Author:     Lucas Dixon, University of Edinburgh
     6.6 -
     6.7 -A proof method to perform a substiution using an equation.
     6.8 -*)
     6.9 -
    6.10 -signature EQSUBST =
    6.11 -sig
    6.12 -  (* a type abbreviation for match information *)
    6.13 -  type match =
    6.14 -       ((indexname * (sort * typ)) list (* type instantiations *)
    6.15 -        * (indexname * (typ * term)) list) (* term instantiations *)
    6.16 -       * (string * typ) list (* fake named type abs env *)
    6.17 -       * (string * typ) list (* type abs env *)
    6.18 -       * term (* outer term *)
    6.19 -
    6.20 -  type searchinfo =
    6.21 -       theory
    6.22 -       * int (* maxidx *)
    6.23 -       * Zipper.T (* focusterm to search under *)
    6.24 -
    6.25 -    exception eqsubst_occL_exp of
    6.26 -       string * int list * Thm.thm list * int * Thm.thm
    6.27 -    
    6.28 -    (* low level substitution functions *)
    6.29 -    val apply_subst_in_asm :
    6.30 -       int ->
    6.31 -       Thm.thm ->
    6.32 -       Thm.thm ->
    6.33 -       (Thm.cterm list * int * 'a * Thm.thm) * match -> Thm.thm Seq.seq
    6.34 -    val apply_subst_in_concl :
    6.35 -       int ->
    6.36 -       Thm.thm ->
    6.37 -       Thm.cterm list * Thm.thm ->
    6.38 -       Thm.thm -> match -> Thm.thm Seq.seq
    6.39 -
    6.40 -    (* matching/unification within zippers *)
    6.41 -    val clean_match_z :
    6.42 -       Context.theory -> Term.term -> Zipper.T -> match option
    6.43 -    val clean_unify_z :
    6.44 -       Context.theory -> int -> Term.term -> Zipper.T -> match Seq.seq
    6.45 -
    6.46 -    (* skipping things in seq seq's *)
    6.47 -
    6.48 -   (* skipping non-empty sub-sequences but when we reach the end
    6.49 -      of the seq, remembering how much we have left to skip. *)
    6.50 -    datatype 'a skipseq = SkipMore of int
    6.51 -      | SkipSeq of 'a Seq.seq Seq.seq;
    6.52 -
    6.53 -    val skip_first_asm_occs_search :
    6.54 -       ('a -> 'b -> 'c Seq.seq Seq.seq) ->
    6.55 -       'a -> int -> 'b -> 'c skipseq
    6.56 -    val skip_first_occs_search :
    6.57 -       int -> ('a -> 'b -> 'c Seq.seq Seq.seq) -> 'a -> 'b -> 'c Seq.seq
    6.58 -    val skipto_skipseq : int -> 'a Seq.seq Seq.seq -> 'a skipseq
    6.59 -
    6.60 -    (* tactics *)
    6.61 -    val eqsubst_asm_tac :
    6.62 -       Proof.context ->
    6.63 -       int list -> Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
    6.64 -    val eqsubst_asm_tac' :
    6.65 -       Proof.context ->
    6.66 -       (searchinfo -> int -> Term.term -> match skipseq) ->
    6.67 -       int -> Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq
    6.68 -    val eqsubst_tac :
    6.69 -       Proof.context ->
    6.70 -       int list -> (* list of occurences to rewrite, use [0] for any *)
    6.71 -       Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
    6.72 -    val eqsubst_tac' :
    6.73 -       Proof.context -> (* proof context *)
    6.74 -       (searchinfo -> Term.term -> match Seq.seq) (* search function *)
    6.75 -       -> Thm.thm (* equation theorem to rewrite with *)
    6.76 -       -> int (* subgoal number in goal theorem *)
    6.77 -       -> Thm.thm (* goal theorem *)
    6.78 -       -> Thm.thm Seq.seq (* rewritten goal theorem *)
    6.79 -
    6.80 -
    6.81 -    val fakefree_badbounds :
    6.82 -       (string * Term.typ) list ->
    6.83 -       Term.term ->
    6.84 -       (string * Term.typ) list * (string * Term.typ) list * Term.term
    6.85 -
    6.86 -    val mk_foo_match :
    6.87 -       (Term.term -> Term.term) ->
    6.88 -       ('a * Term.typ) list -> Term.term -> Term.term
    6.89 -
    6.90 -    (* preparing substitution *)
    6.91 -    val prep_meta_eq : Proof.context -> Thm.thm -> Thm.thm list
    6.92 -    val prep_concl_subst :
    6.93 -       int -> Thm.thm -> (Thm.cterm list * Thm.thm) * searchinfo
    6.94 -    val prep_subst_in_asm :
    6.95 -       int -> Thm.thm -> int ->
    6.96 -       (Thm.cterm list * int * int * Thm.thm) * searchinfo
    6.97 -    val prep_subst_in_asms :
    6.98 -       int -> Thm.thm ->
    6.99 -       ((Thm.cterm list * int * int * Thm.thm) * searchinfo) list
   6.100 -    val prep_zipper_match :
   6.101 -       Zipper.T -> Term.term * ((string * Term.typ) list * (string * Term.typ) list * Term.term)
   6.102 -
   6.103 -    (* search for substitutions *)
   6.104 -    val valid_match_start : Zipper.T -> bool
   6.105 -    val search_lr_all : Zipper.T -> Zipper.T Seq.seq
   6.106 -    val search_lr_valid : (Zipper.T -> bool) -> Zipper.T -> Zipper.T Seq.seq
   6.107 -    val searchf_lr_unify_all :
   6.108 -       searchinfo -> Term.term -> match Seq.seq Seq.seq
   6.109 -    val searchf_lr_unify_valid :
   6.110 -       searchinfo -> Term.term -> match Seq.seq Seq.seq
   6.111 -    val searchf_bt_unify_valid :
   6.112 -       searchinfo -> Term.term -> match Seq.seq Seq.seq
   6.113 -
   6.114 -    (* syntax tools *)
   6.115 -    val ith_syntax : Args.T list -> int list * Args.T list
   6.116 -    val options_syntax : Args.T list -> bool * Args.T list
   6.117 -
   6.118 -    (* Isar level hooks *)
   6.119 -    val eqsubst_asm_meth : Proof.context -> int list -> Thm.thm list -> Proof.method
   6.120 -    val eqsubst_meth : Proof.context -> int list -> Thm.thm list -> Proof.method
   6.121 -    val subst_meth : Method.src -> Proof.context -> Proof.method
   6.122 -    val setup : theory -> theory
   6.123 -
   6.124 -end;
   6.125 -
   6.126 -structure EqSubst
   6.127 -: EQSUBST
   6.128 -= struct
   6.129 -
   6.130 -structure Z = Zipper;
   6.131 -
   6.132 -(* changes object "=" to meta "==" which prepares a given rewrite rule *)
   6.133 -fun prep_meta_eq ctxt =
   6.134 -  let val (_, {mk_rews = {mk, ...}, ...}) = Simplifier.rep_ss (Simplifier.local_simpset_of ctxt)
   6.135 -  in mk #> map Drule.zero_var_indexes end;
   6.136 -
   6.137 -
   6.138 -  (* a type abriviation for match information *)
   6.139 -  type match =
   6.140 -       ((indexname * (sort * typ)) list (* type instantiations *)
   6.141 -        * (indexname * (typ * term)) list) (* term instantiations *)
   6.142 -       * (string * typ) list (* fake named type abs env *)
   6.143 -       * (string * typ) list (* type abs env *)
   6.144 -       * term (* outer term *)
   6.145 -
   6.146 -  type searchinfo =
   6.147 -       theory
   6.148 -       * int (* maxidx *)
   6.149 -       * Zipper.T (* focusterm to search under *)
   6.150 -
   6.151 -
   6.152 -(* skipping non-empty sub-sequences but when we reach the end
   6.153 -   of the seq, remembering how much we have left to skip. *)
   6.154 -datatype 'a skipseq = SkipMore of int
   6.155 -  | SkipSeq of 'a Seq.seq Seq.seq;
   6.156 -(* given a seqseq, skip the first m non-empty seq's, note deficit *)
   6.157 -fun skipto_skipseq m s = 
   6.158 -    let 
   6.159 -      fun skip_occs n sq = 
   6.160 -          case Seq.pull sq of 
   6.161 -            NONE => SkipMore n
   6.162 -          | SOME (h,t) => 
   6.163 -            (case Seq.pull h of NONE => skip_occs n t
   6.164 -             | SOME _ => if n <= 1 then SkipSeq (Seq.cons h t)
   6.165 -                         else skip_occs (n - 1) t)
   6.166 -    in (skip_occs m s) end;
   6.167 -
   6.168 -(* note: outerterm is the taget with the match replaced by a bound 
   6.169 -         variable : ie: "P lhs" beocmes "%x. P x" 
   6.170 -         insts is the types of instantiations of vars in lhs
   6.171 -         and typinsts is the type instantiations of types in the lhs
   6.172 -         Note: Final rule is the rule lifted into the ontext of the 
   6.173 -         taget thm. *)
   6.174 -fun mk_foo_match mkuptermfunc Ts t = 
   6.175 -    let 
   6.176 -      val ty = Term.type_of t
   6.177 -      val bigtype = (rev (map snd Ts)) ---> ty
   6.178 -      fun mk_foo 0 t = t
   6.179 -        | mk_foo i t = mk_foo (i - 1) (t $ (Bound (i - 1)))
   6.180 -      val num_of_bnds = (length Ts)
   6.181 -      (* foo_term = "fooabs y0 ... yn" where y's are local bounds *)
   6.182 -      val foo_term = mk_foo num_of_bnds (Bound num_of_bnds)
   6.183 -    in Abs("fooabs", bigtype, mkuptermfunc foo_term) end;
   6.184 -
   6.185 -(* T is outer bound vars, n is number of locally bound vars *)
   6.186 -(* THINK: is order of Ts correct...? or reversed? *)
   6.187 -fun fakefree_badbounds Ts t = 
   6.188 -    let val (FakeTs,Ts,newnames) = 
   6.189 -            List.foldr (fn ((n,ty),(FakeTs,Ts,usednames)) => 
   6.190 -                           let val newname = Name.variant usednames n
   6.191 -                           in ((RWTools.mk_fake_bound_name newname,ty)::FakeTs,
   6.192 -                               (newname,ty)::Ts, 
   6.193 -                               newname::usednames) end)
   6.194 -                       ([],[],[])
   6.195 -                       Ts
   6.196 -    in (FakeTs, Ts, Term.subst_bounds (map Free FakeTs, t)) end;
   6.197 -
   6.198 -(* before matching we need to fake the bound vars that are missing an
   6.199 -abstraction. In this function we additionally construct the
   6.200 -abstraction environment, and an outer context term (with the focus
   6.201 -abstracted out) for use in rewriting with RWInst.rw *)
   6.202 -fun prep_zipper_match z = 
   6.203 -    let 
   6.204 -      val t = Z.trm z  
   6.205 -      val c = Z.ctxt z
   6.206 -      val Ts = Z.C.nty_ctxt c
   6.207 -      val (FakeTs', Ts', t') = fakefree_badbounds Ts t
   6.208 -      val absterm = mk_foo_match (Z.C.apply c) Ts' t'
   6.209 -    in
   6.210 -      (t', (FakeTs', Ts', absterm))
   6.211 -    end;
   6.212 -
   6.213 -(* Matching and Unification with exception handled *)
   6.214 -fun clean_match thy (a as (pat, t)) =
   6.215 -  let val (tyenv, tenv) = Pattern.match thy a (Vartab.empty, Vartab.empty)
   6.216 -  in SOME (Vartab.dest tyenv, Vartab.dest tenv)
   6.217 -  end handle Pattern.MATCH => NONE;
   6.218 -
   6.219 -(* given theory, max var index, pat, tgt; returns Seq of instantiations *)
   6.220 -fun clean_unify thry ix (a as (pat, tgt)) =
   6.221 -    let
   6.222 -      (* type info will be re-derived, maybe this can be cached
   6.223 -         for efficiency? *)
   6.224 -      val pat_ty = Term.type_of pat;
   6.225 -      val tgt_ty = Term.type_of tgt;
   6.226 -      (* is it OK to ignore the type instantiation info?
   6.227 -         or should I be using it? *)
   6.228 -      val typs_unify =
   6.229 -          SOME (Sign.typ_unify thry (pat_ty, tgt_ty) (Vartab.empty, ix))
   6.230 -            handle Type.TUNIFY => NONE;
   6.231 -    in
   6.232 -      case typs_unify of
   6.233 -        SOME (typinsttab, ix2) =>
   6.234 -        let
   6.235 -      (* is it right to throw away the flexes?
   6.236 -         or should I be using them somehow? *)
   6.237 -          fun mk_insts env =
   6.238 -            (Vartab.dest (Envir.type_env env),
   6.239 -             Envir.alist_of env);
   6.240 -          val initenv = Envir.Envir {asol = Vartab.empty,
   6.241 -                                     iTs = typinsttab, maxidx = ix2};
   6.242 -          val useq = Unify.smash_unifiers thry [a] initenv
   6.243 -	            handle UnequalLengths => Seq.empty
   6.244 -		               | Term.TERM _ => Seq.empty;
   6.245 -          fun clean_unify' useq () =
   6.246 -              (case (Seq.pull useq) of
   6.247 -                 NONE => NONE
   6.248 -               | SOME (h,t) => SOME (mk_insts h, Seq.make (clean_unify' t)))
   6.249 -	            handle UnequalLengths => NONE
   6.250 -                   | Term.TERM _ => NONE
   6.251 -        in
   6.252 -          (Seq.make (clean_unify' useq))
   6.253 -        end
   6.254 -      | NONE => Seq.empty
   6.255 -    end;
   6.256 -
   6.257 -(* Matching and Unification for zippers *)
   6.258 -(* Note: Ts is a modified version of the original names of the outer
   6.259 -bound variables. New names have been introduced to make sure they are
   6.260 -unique w.r.t all names in the term and each other. usednames' is
   6.261 -oldnames + new names. *)
   6.262 -fun clean_match_z thy pat z = 
   6.263 -    let val (t, (FakeTs,Ts,absterm)) = prep_zipper_match z in
   6.264 -      case clean_match thy (pat, t) of 
   6.265 -        NONE => NONE 
   6.266 -      | SOME insts => SOME (insts, FakeTs, Ts, absterm) end;
   6.267 -(* ix = max var index *)
   6.268 -fun clean_unify_z sgn ix pat z = 
   6.269 -    let val (t, (FakeTs, Ts,absterm)) = prep_zipper_match z in
   6.270 -    Seq.map (fn insts => (insts, FakeTs, Ts, absterm)) 
   6.271 -            (clean_unify sgn ix (t, pat)) end;
   6.272 -
   6.273 -
   6.274 -(* FOR DEBUGGING...
   6.275 -type trace_subst_errT = int (* subgoal *)
   6.276 -        * thm (* thm with all goals *)
   6.277 -        * (Thm.cterm list (* certified free var placeholders for vars *)
   6.278 -           * thm)  (* trivial thm of goal concl *)
   6.279 -            (* possible matches/unifiers *)
   6.280 -        * thm (* rule *)
   6.281 -        * (((indexname * typ) list (* type instantiations *)
   6.282 -              * (indexname * term) list ) (* term instantiations *)
   6.283 -             * (string * typ) list (* Type abs env *)
   6.284 -             * term) (* outer term *);
   6.285 -
   6.286 -val trace_subst_err = (ref NONE : trace_subst_errT option ref);
   6.287 -val trace_subst_search = ref false;
   6.288 -exception trace_subst_exp of trace_subst_errT;
   6.289 -*)
   6.290 -
   6.291 -
   6.292 -fun bot_left_leaf_of (l $ r) = bot_left_leaf_of l
   6.293 -  | bot_left_leaf_of (Abs(s,ty,t)) = bot_left_leaf_of t
   6.294 -  | bot_left_leaf_of x = x;
   6.295 -
   6.296 -(* Avoid considering replacing terms which have a var at the head as
   6.297 -   they always succeed trivially, and uninterestingly. *)
   6.298 -fun valid_match_start z =
   6.299 -    (case bot_left_leaf_of (Z.trm z) of 
   6.300 -      Var _ => false 
   6.301 -      | _ => true);
   6.302 -
   6.303 -(* search from top, left to right, then down *)
   6.304 -val search_lr_all = ZipperSearch.all_bl_ur;
   6.305 -
   6.306 -(* search from top, left to right, then down *)
   6.307 -fun search_lr_valid validf =
   6.308 -    let 
   6.309 -      fun sf_valid_td_lr z = 
   6.310 -          let val here = if validf z then [Z.Here z] else [] in
   6.311 -            case Z.trm z 
   6.312 -             of _ $ _ => [Z.LookIn (Z.move_down_left z)] 
   6.313 -                         @ here 
   6.314 -                         @ [Z.LookIn (Z.move_down_right z)]
   6.315 -              | Abs _ => here @ [Z.LookIn (Z.move_down_abs z)]
   6.316 -              | _ => here
   6.317 -          end;
   6.318 -    in Z.lzy_search sf_valid_td_lr end;
   6.319 -
   6.320 -(* search from bottom to top, left to right *)
   6.321 -
   6.322 -fun search_bt_valid validf =
   6.323 -    let 
   6.324 -      fun sf_valid_td_lr z = 
   6.325 -          let val here = if validf z then [Z.Here z] else [] in
   6.326 -            case Z.trm z 
   6.327 -             of _ $ _ => [Z.LookIn (Z.move_down_left z), 
   6.328 -                          Z.LookIn (Z.move_down_right z)] @ here
   6.329 -              | Abs _ => [Z.LookIn (Z.move_down_abs z)] @ here
   6.330 -              | _ => here
   6.331 -          end;
   6.332 -    in Z.lzy_search sf_valid_td_lr end;
   6.333 -
   6.334 -fun searchf_unify_gen f (sgn, maxidx, z) lhs =
   6.335 -    Seq.map (clean_unify_z sgn maxidx lhs) 
   6.336 -            (Z.limit_apply f z);
   6.337 -
   6.338 -(* search all unifications *)
   6.339 -val searchf_lr_unify_all =
   6.340 -    searchf_unify_gen search_lr_all;
   6.341 -
   6.342 -(* search only for 'valid' unifiers (non abs subterms and non vars) *)
   6.343 -val searchf_lr_unify_valid = 
   6.344 -    searchf_unify_gen (search_lr_valid valid_match_start);
   6.345 -
   6.346 -val searchf_bt_unify_valid =
   6.347 -    searchf_unify_gen (search_bt_valid valid_match_start);
   6.348 -
   6.349 -(* apply a substitution in the conclusion of the theorem th *)
   6.350 -(* cfvs are certified free var placeholders for goal params *)
   6.351 -(* conclthm is a theorem of for just the conclusion *)
   6.352 -(* m is instantiation/match information *)
   6.353 -(* rule is the equation for substitution *)
   6.354 -fun apply_subst_in_concl i th (cfvs, conclthm) rule m =
   6.355 -    (RWInst.rw m rule conclthm)
   6.356 -      |> IsaND.unfix_frees cfvs
   6.357 -      |> RWInst.beta_eta_contract
   6.358 -      |> (fn r => Tactic.rtac r i th);
   6.359 -
   6.360 -(* substitute within the conclusion of goal i of gth, using a meta
   6.361 -equation rule. Note that we assume rule has var indicies zero'd *)
   6.362 -fun prep_concl_subst i gth =
   6.363 -    let
   6.364 -      val th = Thm.incr_indexes 1 gth;
   6.365 -      val tgt_term = Thm.prop_of th;
   6.366 -
   6.367 -      val sgn = Thm.theory_of_thm th;
   6.368 -      val ctermify = Thm.cterm_of sgn;
   6.369 -      val trivify = Thm.trivial o ctermify;
   6.370 -
   6.371 -      val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
   6.372 -      val cfvs = rev (map ctermify fvs);
   6.373 -
   6.374 -      val conclterm = Logic.strip_imp_concl fixedbody;
   6.375 -      val conclthm = trivify conclterm;
   6.376 -      val maxidx = Thm.maxidx_of th;
   6.377 -      val ft = ((Z.move_down_right (* ==> *)
   6.378 -                 o Z.move_down_left (* Trueprop *)
   6.379 -                 o Z.mktop
   6.380 -                 o Thm.prop_of) conclthm)
   6.381 -    in
   6.382 -      ((cfvs, conclthm), (sgn, maxidx, ft))
   6.383 -    end;
   6.384 -
   6.385 -(* substitute using an object or meta level equality *)
   6.386 -fun eqsubst_tac' ctxt searchf instepthm i th =
   6.387 -    let
   6.388 -      val (cvfsconclthm, searchinfo) = prep_concl_subst i th;
   6.389 -      val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
   6.390 -      fun rewrite_with_thm r =
   6.391 -          let val (lhs,_) = Logic.dest_equals (Thm.concl_of r);
   6.392 -          in searchf searchinfo lhs
   6.393 -             |> Seq.maps (apply_subst_in_concl i th cvfsconclthm r) end;
   6.394 -    in stepthms |> Seq.maps rewrite_with_thm end;
   6.395 -
   6.396 -
   6.397 -(* distinct subgoals *)
   6.398 -fun distinct_subgoals th =
   6.399 -  the_default th (SINGLE distinct_subgoals_tac th);
   6.400 -
   6.401 -(* General substitution of multiple occurances using one of
   6.402 -   the given theorems*)
   6.403 -
   6.404 -
   6.405 -exception eqsubst_occL_exp of
   6.406 -          string * (int list) * (thm list) * int * thm;
   6.407 -fun skip_first_occs_search occ srchf sinfo lhs =
   6.408 -    case (skipto_skipseq occ (srchf sinfo lhs)) of
   6.409 -      SkipMore _ => Seq.empty
   6.410 -    | SkipSeq ss => Seq.flat ss;
   6.411 -
   6.412 -(* The occL is a list of integers indicating which occurence
   6.413 -w.r.t. the search order, to rewrite. Backtracking will also find later
   6.414 -occurences, but all earlier ones are skipped. Thus you can use [0] to
   6.415 -just find all rewrites. *)
   6.416 -
   6.417 -fun eqsubst_tac ctxt occL thms i th =
   6.418 -    let val nprems = Thm.nprems_of th in
   6.419 -      if nprems < i then Seq.empty else
   6.420 -      let val thmseq = (Seq.of_list thms)
   6.421 -        fun apply_occ occ th =
   6.422 -            thmseq |> Seq.maps
   6.423 -                    (fn r => eqsubst_tac' 
   6.424 -                               ctxt 
   6.425 -                               (skip_first_occs_search
   6.426 -                                  occ searchf_lr_unify_valid) r
   6.427 -                                 (i + ((Thm.nprems_of th) - nprems))
   6.428 -                                 th);
   6.429 -        val sortedoccL =
   6.430 -            Library.sort (Library.rev_order o Library.int_ord) occL;
   6.431 -      in
   6.432 -        Seq.map distinct_subgoals (Seq.EVERY (map apply_occ sortedoccL) th)
   6.433 -      end
   6.434 -    end
   6.435 -    handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
   6.436 -
   6.437 -
   6.438 -(* inthms are the given arguments in Isar, and treated as eqstep with
   6.439 -   the first one, then the second etc *)
   6.440 -fun eqsubst_meth ctxt occL inthms =
   6.441 -    Method.SIMPLE_METHOD' (eqsubst_tac ctxt occL inthms);
   6.442 -
   6.443 -(* apply a substitution inside assumption j, keeps asm in the same place *)
   6.444 -fun apply_subst_in_asm i th rule ((cfvs, j, ngoalprems, pth),m) =
   6.445 -    let
   6.446 -      val th2 = Thm.rotate_rule (j - 1) i th; (* put premice first *)
   6.447 -      val preelimrule =
   6.448 -          (RWInst.rw m rule pth)
   6.449 -            |> (Seq.hd o prune_params_tac)
   6.450 -            |> Thm.permute_prems 0 ~1 (* put old asm first *)
   6.451 -            |> IsaND.unfix_frees cfvs (* unfix any global params *)
   6.452 -            |> RWInst.beta_eta_contract; (* normal form *)
   6.453 -  (*    val elimrule =
   6.454 -          preelimrule
   6.455 -            |> Tactic.make_elim (* make into elim rule *)
   6.456 -            |> Thm.lift_rule (th2, i); (* lift into context *)
   6.457 -   *)
   6.458 -    in
   6.459 -      (* ~j because new asm starts at back, thus we subtract 1 *)
   6.460 -      Seq.map (Thm.rotate_rule (~j) ((Thm.nprems_of rule) + i))
   6.461 -      (Tactic.dtac preelimrule i th2)
   6.462 -
   6.463 -      (* (Thm.bicompose
   6.464 -                 false (* use unification *)
   6.465 -                 (true, (* elim resolution *)
   6.466 -                  elimrule, (2 + (Thm.nprems_of rule)) - ngoalprems)
   6.467 -                 i th2) *)
   6.468 -    end;
   6.469 -
   6.470 -
   6.471 -(* prepare to substitute within the j'th premise of subgoal i of gth,
   6.472 -using a meta-level equation. Note that we assume rule has var indicies
   6.473 -zero'd. Note that we also assume that premt is the j'th premice of
   6.474 -subgoal i of gth. Note the repetition of work done for each
   6.475 -assumption, i.e. this can be made more efficient for search over
   6.476 -multiple assumptions.  *)
   6.477 -fun prep_subst_in_asm i gth j =
   6.478 -    let
   6.479 -      val th = Thm.incr_indexes 1 gth;
   6.480 -      val tgt_term = Thm.prop_of th;
   6.481 -
   6.482 -      val sgn = Thm.theory_of_thm th;
   6.483 -      val ctermify = Thm.cterm_of sgn;
   6.484 -      val trivify = Thm.trivial o ctermify;
   6.485 -
   6.486 -      val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
   6.487 -      val cfvs = rev (map ctermify fvs);
   6.488 -
   6.489 -      val asmt = nth (Logic.strip_imp_prems fixedbody) (j - 1);
   6.490 -      val asm_nprems = length (Logic.strip_imp_prems asmt);
   6.491 -
   6.492 -      val pth = trivify asmt;
   6.493 -      val maxidx = Thm.maxidx_of th;
   6.494 -
   6.495 -      val ft = ((Z.move_down_right (* trueprop *)
   6.496 -                 o Z.mktop
   6.497 -                 o Thm.prop_of) pth)
   6.498 -    in ((cfvs, j, asm_nprems, pth), (sgn, maxidx, ft)) end;
   6.499 -
   6.500 -(* prepare subst in every possible assumption *)
   6.501 -fun prep_subst_in_asms i gth =
   6.502 -    map (prep_subst_in_asm i gth)
   6.503 -        ((fn l => Library.upto (1, length l))
   6.504 -           (Logic.prems_of_goal (Thm.prop_of gth) i));
   6.505 -
   6.506 -
   6.507 -(* substitute in an assumption using an object or meta level equality *)
   6.508 -fun eqsubst_asm_tac' ctxt searchf skipocc instepthm i th =
   6.509 -    let
   6.510 -      val asmpreps = prep_subst_in_asms i th;
   6.511 -      val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
   6.512 -      fun rewrite_with_thm r =
   6.513 -          let val (lhs,_) = Logic.dest_equals (Thm.concl_of r)
   6.514 -            fun occ_search occ [] = Seq.empty
   6.515 -              | occ_search occ ((asminfo, searchinfo)::moreasms) =
   6.516 -                (case searchf searchinfo occ lhs of
   6.517 -                   SkipMore i => occ_search i moreasms
   6.518 -                 | SkipSeq ss =>
   6.519 -                   Seq.append (Seq.map (Library.pair asminfo) (Seq.flat ss))
   6.520 -                               (occ_search 1 moreasms))
   6.521 -                              (* find later substs also *)
   6.522 -          in
   6.523 -            occ_search skipocc asmpreps |> Seq.maps (apply_subst_in_asm i th r)
   6.524 -          end;
   6.525 -    in stepthms |> Seq.maps rewrite_with_thm end;
   6.526 -
   6.527 -
   6.528 -fun skip_first_asm_occs_search searchf sinfo occ lhs =
   6.529 -    skipto_skipseq occ (searchf sinfo lhs);
   6.530 -
   6.531 -fun eqsubst_asm_tac ctxt occL thms i th =
   6.532 -    let val nprems = Thm.nprems_of th
   6.533 -    in
   6.534 -      if nprems < i then Seq.empty else
   6.535 -      let val thmseq = (Seq.of_list thms)
   6.536 -        fun apply_occ occK th =
   6.537 -            thmseq |> Seq.maps
   6.538 -                    (fn r =>
   6.539 -                        eqsubst_asm_tac' ctxt (skip_first_asm_occs_search
   6.540 -                                            searchf_lr_unify_valid) occK r
   6.541 -                                         (i + ((Thm.nprems_of th) - nprems))
   6.542 -                                         th);
   6.543 -        val sortedoccs =
   6.544 -            Library.sort (Library.rev_order o Library.int_ord) occL
   6.545 -      in
   6.546 -        Seq.map distinct_subgoals
   6.547 -                (Seq.EVERY (map apply_occ sortedoccs) th)
   6.548 -      end
   6.549 -    end
   6.550 -    handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
   6.551 -
   6.552 -(* inthms are the given arguments in Isar, and treated as eqstep with
   6.553 -   the first one, then the second etc *)
   6.554 -fun eqsubst_asm_meth ctxt occL inthms =
   6.555 -    Method.SIMPLE_METHOD' (eqsubst_asm_tac ctxt occL inthms);
   6.556 -
   6.557 -(* syntax for options, given "(asm)" will give back true, without
   6.558 -   gives back false *)
   6.559 -val options_syntax =
   6.560 -    (Args.parens (Args.$$$ "asm") >> (K true)) ||
   6.561 -     (Scan.succeed false);
   6.562 -
   6.563 -val ith_syntax =
   6.564 -    Scan.optional (Args.parens (Scan.repeat OuterParse.nat)) [0];
   6.565 -
   6.566 -(* combination method that takes a flag (true indicates that subst
   6.567 -should be done to an assumption, false = apply to the conclusion of
   6.568 -the goal) as well as the theorems to use *)
   6.569 -fun subst_meth src =
   6.570 -  Method.syntax ((Scan.lift options_syntax) -- (Scan.lift ith_syntax) -- Attrib.thms) src
   6.571 -  #> (fn (((asmflag, occL), inthms), ctxt) =>
   6.572 -    (if asmflag then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms);
   6.573 -
   6.574 -
   6.575 -val setup =
   6.576 -  Method.add_method ("subst", subst_meth, "single-step substitution");
   6.577 -
   6.578 -end;
     7.1 --- a/src/Provers/project_rule.ML	Sat Feb 28 13:54:47 2009 +0100
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,63 +0,0 @@
     7.4 -(*  Title:      Provers/project_rule.ML
     7.5 -    ID:         $Id$
     7.6 -    Author:     Makarius
     7.7 -
     7.8 -Transform mutual rule:
     7.9 -  HH ==> (x1:A1 --> P1 x1) & ... & (xn:An --> Pn xn)
    7.10 -into projection:
    7.11 -  xi:Ai ==> HH ==> Pi xi
    7.12 -*)
    7.13 -
    7.14 -signature PROJECT_RULE_DATA =
    7.15 -sig
    7.16 -  val conjunct1: thm
    7.17 -  val conjunct2: thm
    7.18 -  val mp: thm
    7.19 -end;
    7.20 -
    7.21 -signature PROJECT_RULE =
    7.22 -sig
    7.23 -  val project: Proof.context -> int -> thm -> thm
    7.24 -  val projects: Proof.context -> int list -> thm -> thm list
    7.25 -  val projections: Proof.context -> thm -> thm list
    7.26 -end;
    7.27 -
    7.28 -functor ProjectRuleFun(Data: PROJECT_RULE_DATA): PROJECT_RULE =
    7.29 -struct
    7.30 -
    7.31 -fun conj1 th = th RS Data.conjunct1;
    7.32 -fun conj2 th = th RS Data.conjunct2;
    7.33 -fun imp th = th RS Data.mp;
    7.34 -
    7.35 -fun projects ctxt is raw_rule =
    7.36 -  let
    7.37 -    fun proj 1 th = the_default th (try conj1 th)
    7.38 -      | proj k th = proj (k - 1) (conj2 th);
    7.39 -    fun prems k th =
    7.40 -      (case try imp th of
    7.41 -        NONE => (k, th)
    7.42 -      | SOME th' => prems (k + 1) th');
    7.43 -    val ((_, [rule]), ctxt') = Variable.import_thms true [raw_rule] ctxt;
    7.44 -    fun result i =
    7.45 -      rule
    7.46 -      |> proj i
    7.47 -      |> prems 0 |-> (fn k =>
    7.48 -        Thm.permute_prems 0 (~ k)
    7.49 -        #> singleton (Variable.export ctxt' ctxt)
    7.50 -        #> Drule.zero_var_indexes
    7.51 -        #> RuleCases.save raw_rule
    7.52 -        #> RuleCases.add_consumes k);
    7.53 -  in map result is end;
    7.54 -
    7.55 -fun project ctxt i th = hd (projects ctxt [i] th);
    7.56 -
    7.57 -fun projections ctxt raw_rule =
    7.58 -  let
    7.59 -    fun projs k th =
    7.60 -      (case try conj2 th of
    7.61 -        NONE => k
    7.62 -      | SOME th' => projs (k + 1) th');
    7.63 -    val ((_, [rule]), _) = Variable.import_thms true [raw_rule] ctxt;
    7.64 -  in projects ctxt (1 upto projs 1 rule) raw_rule end;
    7.65 -
    7.66 -end;
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/Tools/coherent.ML	Sat Feb 28 14:02:12 2009 +0100
     8.3 @@ -0,0 +1,233 @@
     8.4 +(*  Title:      Tools/coherent.ML
     8.5 +    Author:     Stefan Berghofer, TU Muenchen
     8.6 +    Author:     Marc Bezem, Institutt for Informatikk, Universitetet i Bergen 
     8.7 +
     8.8 +Prover for coherent logic, see e.g.
     8.9 +
    8.10 +  Marc Bezem and Thierry Coquand, Automating Coherent Logic, LPAR 2005
    8.11 +
    8.12 +for a description of the algorithm.
    8.13 +*)
    8.14 +
    8.15 +signature COHERENT_DATA =
    8.16 +sig
    8.17 +  val atomize_elimL: thm
    8.18 +  val atomize_exL: thm
    8.19 +  val atomize_conjL: thm
    8.20 +  val atomize_disjL: thm
    8.21 +  val operator_names: string list
    8.22 +end;
    8.23 +
    8.24 +signature COHERENT =
    8.25 +sig
    8.26 +  val verbose: bool ref
    8.27 +  val show_facts: bool ref
    8.28 +  val coherent_tac: thm list -> Proof.context -> int -> tactic
    8.29 +  val coherent_meth: thm list -> Proof.context -> Proof.method
    8.30 +  val setup: theory -> theory
    8.31 +end;
    8.32 +
    8.33 +functor CoherentFun(Data: COHERENT_DATA) : COHERENT =
    8.34 +struct
    8.35 +
    8.36 +val verbose = ref false;
    8.37 +
    8.38 +fun message f = if !verbose then tracing (f ()) else ();
    8.39 +
    8.40 +datatype cl_prf =
    8.41 +  ClPrf of thm * (Type.tyenv * Envir.tenv) * ((indexname * typ) * term) list *
    8.42 +  int list * (term list * cl_prf) list;
    8.43 +
    8.44 +val is_atomic = not o exists_Const (member (op =) Data.operator_names o #1);
    8.45 +
    8.46 +local open Conv in
    8.47 +
    8.48 +fun rulify_elim_conv ct =
    8.49 +  if is_atomic (Logic.strip_imp_concl (term_of ct)) then all_conv ct
    8.50 +  else concl_conv (length (Logic.strip_imp_prems (term_of ct)))
    8.51 +    (rewr_conv (symmetric Data.atomize_elimL) then_conv
    8.52 +     MetaSimplifier.rewrite true (map symmetric
    8.53 +       [Data.atomize_exL, Data.atomize_conjL, Data.atomize_disjL])) ct
    8.54 +
    8.55 +end;
    8.56 +
    8.57 +fun rulify_elim th = MetaSimplifier.norm_hhf (Conv.fconv_rule rulify_elim_conv th);
    8.58 +
    8.59 +(* Decompose elimination rule of the form
    8.60 +   A1 ==> ... ==> Am ==> (!!xs1. Bs1 ==> P) ==> ... ==> (!!xsn. Bsn ==> P) ==> P
    8.61 +*)
    8.62 +fun dest_elim prop =
    8.63 +  let
    8.64 +    val prems = Logic.strip_imp_prems prop;
    8.65 +    val concl = Logic.strip_imp_concl prop;
    8.66 +    val (prems1, prems2) =
    8.67 +      take_suffix (fn t => Logic.strip_assums_concl t = concl) prems;
    8.68 +  in
    8.69 +    (prems1,
    8.70 +     if null prems2 then [([], [concl])]
    8.71 +     else map (fn t =>
    8.72 +       (map snd (Logic.strip_params t), Logic.strip_assums_hyp t)) prems2)
    8.73 +  end;
    8.74 +
    8.75 +fun mk_rule th =
    8.76 +  let
    8.77 +    val th' = rulify_elim th;
    8.78 +    val (prems, cases) = dest_elim (prop_of th')
    8.79 +  in (th', prems, cases) end;
    8.80 +
    8.81 +fun mk_dom ts = fold (fn t =>
    8.82 +  Typtab.map_default (fastype_of t, []) (fn us => us @ [t])) ts Typtab.empty;
    8.83 +
    8.84 +val empty_env = (Vartab.empty, Vartab.empty);
    8.85 +
    8.86 +(* Find matcher that makes conjunction valid in given state *)
    8.87 +fun valid_conj ctxt facts env [] = Seq.single (env, [])
    8.88 +  | valid_conj ctxt facts env (t :: ts) =
    8.89 +      Seq.maps (fn (u, x) => Seq.map (apsnd (cons x))
    8.90 +        (valid_conj ctxt facts
    8.91 +           (Pattern.match (ProofContext.theory_of ctxt) (t, u) env) ts
    8.92 +         handle Pattern.MATCH => Seq.empty))
    8.93 +          (Seq.of_list (sort (int_ord o pairself snd) (Net.unify_term facts t)));
    8.94 +
    8.95 +(* Instantiate variables that only occur free in conlusion *)
    8.96 +fun inst_extra_vars ctxt dom cs =
    8.97 +  let
    8.98 +    val vs = fold Term.add_vars (maps snd cs) [];
    8.99 +    fun insts [] inst = Seq.single inst
   8.100 +      | insts ((ixn, T) :: vs') inst = Seq.maps
   8.101 +          (fn t => insts vs' (((ixn, T), t) :: inst))
   8.102 +          (Seq.of_list (case Typtab.lookup dom T of
   8.103 +             NONE => error ("Unknown domain: " ^
   8.104 +               Syntax.string_of_typ ctxt T ^ "\nfor term(s) " ^
   8.105 +               commas (maps (map (Syntax.string_of_term ctxt) o snd) cs))
   8.106 +           | SOME ts => ts))
   8.107 +  in Seq.map (fn inst =>
   8.108 +    (inst, map (apsnd (map (subst_Vars (map (apfst fst) inst)))) cs))
   8.109 +      (insts vs [])
   8.110 +  end;
   8.111 +
   8.112 +(* Check whether disjunction is valid in given state *)
   8.113 +fun is_valid_disj ctxt facts [] = false
   8.114 +  | is_valid_disj ctxt facts ((Ts, ts) :: ds) =
   8.115 +      let val vs = rev (map_index (fn (i, T) => Var (("x", i), T)) Ts)
   8.116 +      in case Seq.pull (valid_conj ctxt facts empty_env
   8.117 +        (map (fn t => subst_bounds (vs, t)) ts)) of
   8.118 +          SOME _ => true
   8.119 +        | NONE => is_valid_disj ctxt facts ds
   8.120 +      end;
   8.121 +
   8.122 +val show_facts = ref false;
   8.123 +
   8.124 +fun string_of_facts ctxt s facts = space_implode "\n"
   8.125 +  (s :: map (Syntax.string_of_term ctxt)
   8.126 +     (map fst (sort (int_ord o pairself snd) (Net.content facts)))) ^ "\n\n";
   8.127 +
   8.128 +fun print_facts ctxt facts =
   8.129 +  if !show_facts then message (fn () => string_of_facts ctxt "Facts:" facts)
   8.130 +  else ();
   8.131 +
   8.132 +fun valid ctxt rules goal dom facts nfacts nparams =
   8.133 +  let val seq = Seq.of_list rules |> Seq.maps (fn (th, ps, cs) =>
   8.134 +    valid_conj ctxt facts empty_env ps |> Seq.maps (fn (env as (tye, _), is) =>
   8.135 +      let val cs' = map (fn (Ts, ts) =>
   8.136 +        (map (Envir.typ_subst_TVars tye) Ts, map (Envir.subst_vars env) ts)) cs
   8.137 +      in
   8.138 +        inst_extra_vars ctxt dom cs' |>
   8.139 +          Seq.map_filter (fn (inst, cs'') =>
   8.140 +            if is_valid_disj ctxt facts cs'' then NONE
   8.141 +            else SOME (th, env, inst, is, cs''))
   8.142 +      end))
   8.143 +  in
   8.144 +    case Seq.pull seq of
   8.145 +      NONE => (tracing (string_of_facts ctxt "Countermodel found:" facts); NONE)
   8.146 +    | SOME ((th, env, inst, is, cs), _) =>
   8.147 +        if cs = [([], [goal])] then SOME (ClPrf (th, env, inst, is, []))
   8.148 +        else
   8.149 +          (case valid_cases ctxt rules goal dom facts nfacts nparams cs of
   8.150 +             NONE => NONE
   8.151 +           | SOME prfs => SOME (ClPrf (th, env, inst, is, prfs)))
   8.152 +  end
   8.153 +
   8.154 +and valid_cases ctxt rules goal dom facts nfacts nparams [] = SOME []
   8.155 +  | valid_cases ctxt rules goal dom facts nfacts nparams ((Ts, ts) :: ds) =
   8.156 +      let
   8.157 +        val _ = message (fn () => "case " ^ commas (map (Syntax.string_of_term ctxt) ts));
   8.158 +        val params = rev (map_index (fn (i, T) =>
   8.159 +          Free ("par" ^ string_of_int (nparams + i), T)) Ts);
   8.160 +        val ts' = map_index (fn (i, t) =>
   8.161 +          (subst_bounds (params, t), nfacts + i)) ts;
   8.162 +        val dom' = fold (fn (T, p) =>
   8.163 +          Typtab.map_default (T, []) (fn ps => ps @ [p]))
   8.164 +            (Ts ~~ params) dom;
   8.165 +        val facts' = fold (fn (t, i) => Net.insert_term op =
   8.166 +          (t, (t, i))) ts' facts
   8.167 +      in
   8.168 +        case valid ctxt rules goal dom' facts'
   8.169 +          (nfacts + length ts) (nparams + length Ts) of
   8.170 +          NONE => NONE
   8.171 +        | SOME prf => (case valid_cases ctxt rules goal dom facts nfacts nparams ds of
   8.172 +            NONE => NONE
   8.173 +          | SOME prfs => SOME ((params, prf) :: prfs))
   8.174 +      end;
   8.175 +
   8.176 +(** proof replaying **)
   8.177 +
   8.178 +fun thm_of_cl_prf thy goal asms (ClPrf (th, (tye, env), insts, is, prfs)) =
   8.179 +  let
   8.180 +    val _ = message (fn () => space_implode "\n"
   8.181 +      ("asms:" :: map Display.string_of_thm asms) ^ "\n\n");
   8.182 +    val th' = Drule.implies_elim_list
   8.183 +      (Thm.instantiate
   8.184 +         (map (fn (ixn, (S, T)) =>
   8.185 +            (Thm.ctyp_of thy (TVar ((ixn, S))), Thm.ctyp_of thy T))
   8.186 +               (Vartab.dest tye),
   8.187 +          map (fn (ixn, (T, t)) =>
   8.188 +            (Thm.cterm_of thy (Var (ixn, Envir.typ_subst_TVars tye T)),
   8.189 +             Thm.cterm_of thy t)) (Vartab.dest env) @
   8.190 +          map (fn (ixnT, t) =>
   8.191 +            (Thm.cterm_of thy (Var ixnT), Thm.cterm_of thy t)) insts) th)
   8.192 +      (map (nth asms) is);
   8.193 +    val (_, cases) = dest_elim (prop_of th')
   8.194 +  in
   8.195 +    case (cases, prfs) of
   8.196 +      ([([], [_])], []) => th'
   8.197 +    | ([([], [_])], [([], prf)]) => thm_of_cl_prf thy goal (asms @ [th']) prf
   8.198 +    | _ => Drule.implies_elim_list
   8.199 +        (Thm.instantiate (Thm.match
   8.200 +           (Drule.strip_imp_concl (cprop_of th'), goal)) th')
   8.201 +        (map (thm_of_case_prf thy goal asms) (prfs ~~ cases))
   8.202 +  end
   8.203 +
   8.204 +and thm_of_case_prf thy goal asms ((params, prf), (_, asms')) =
   8.205 +  let
   8.206 +    val cparams = map (cterm_of thy) params;
   8.207 +    val asms'' = map (cterm_of thy o curry subst_bounds (rev params)) asms'
   8.208 +  in
   8.209 +    Drule.forall_intr_list cparams (Drule.implies_intr_list asms''
   8.210 +      (thm_of_cl_prf thy goal (asms @ map Thm.assume asms'') prf))
   8.211 +  end;
   8.212 +
   8.213 +
   8.214 +(** external interface **)
   8.215 +
   8.216 +fun coherent_tac rules ctxt = SUBPROOF (fn {prems, concl, params, context, ...} =>
   8.217 +  rtac (rulify_elim_conv concl RS equal_elim_rule2) 1 THEN
   8.218 +  SUBPROOF (fn {prems = prems', concl, context, ...} =>
   8.219 +    let val xs = map term_of params @
   8.220 +      map (fn (_, s) => Free (s, the (Variable.default_type context s)))
   8.221 +        (Variable.fixes_of context)
   8.222 +    in
   8.223 +      case valid context (map mk_rule (prems' @ prems @ rules)) (term_of concl)
   8.224 +           (mk_dom xs) Net.empty 0 0 of
   8.225 +         NONE => no_tac
   8.226 +       | SOME prf =>
   8.227 +           rtac (thm_of_cl_prf (ProofContext.theory_of context) concl [] prf) 1
   8.228 +    end) context 1) ctxt;
   8.229 +
   8.230 +fun coherent_meth rules ctxt =
   8.231 +  Method.METHOD (fn facts => coherent_tac (facts @ rules) ctxt 1);
   8.232 +
   8.233 +val setup = Method.add_method
   8.234 +  ("coherent", Method.thms_ctxt_args coherent_meth, "Prove coherent formula");
   8.235 +
   8.236 +end;
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/Tools/eqsubst.ML	Sat Feb 28 14:02:12 2009 +0100
     9.3 @@ -0,0 +1,575 @@
     9.4 +(*  Title:      Tools/eqsubst.ML
     9.5 +    Author:     Lucas Dixon, University of Edinburgh
     9.6 +
     9.7 +A proof method to perform a substiution using an equation.
     9.8 +*)
     9.9 +
    9.10 +signature EQSUBST =
    9.11 +sig
    9.12 +  (* a type abbreviation for match information *)
    9.13 +  type match =
    9.14 +       ((indexname * (sort * typ)) list (* type instantiations *)
    9.15 +        * (indexname * (typ * term)) list) (* term instantiations *)
    9.16 +       * (string * typ) list (* fake named type abs env *)
    9.17 +       * (string * typ) list (* type abs env *)
    9.18 +       * term (* outer term *)
    9.19 +
    9.20 +  type searchinfo =
    9.21 +       theory
    9.22 +       * int (* maxidx *)
    9.23 +       * Zipper.T (* focusterm to search under *)
    9.24 +
    9.25 +    exception eqsubst_occL_exp of
    9.26 +       string * int list * Thm.thm list * int * Thm.thm
    9.27 +    
    9.28 +    (* low level substitution functions *)
    9.29 +    val apply_subst_in_asm :
    9.30 +       int ->
    9.31 +       Thm.thm ->
    9.32 +       Thm.thm ->
    9.33 +       (Thm.cterm list * int * 'a * Thm.thm) * match -> Thm.thm Seq.seq
    9.34 +    val apply_subst_in_concl :
    9.35 +       int ->
    9.36 +       Thm.thm ->
    9.37 +       Thm.cterm list * Thm.thm ->
    9.38 +       Thm.thm -> match -> Thm.thm Seq.seq
    9.39 +
    9.40 +    (* matching/unification within zippers *)
    9.41 +    val clean_match_z :
    9.42 +       Context.theory -> Term.term -> Zipper.T -> match option
    9.43 +    val clean_unify_z :
    9.44 +       Context.theory -> int -> Term.term -> Zipper.T -> match Seq.seq
    9.45 +
    9.46 +    (* skipping things in seq seq's *)
    9.47 +
    9.48 +   (* skipping non-empty sub-sequences but when we reach the end
    9.49 +      of the seq, remembering how much we have left to skip. *)
    9.50 +    datatype 'a skipseq = SkipMore of int
    9.51 +      | SkipSeq of 'a Seq.seq Seq.seq;
    9.52 +
    9.53 +    val skip_first_asm_occs_search :
    9.54 +       ('a -> 'b -> 'c Seq.seq Seq.seq) ->
    9.55 +       'a -> int -> 'b -> 'c skipseq
    9.56 +    val skip_first_occs_search :
    9.57 +       int -> ('a -> 'b -> 'c Seq.seq Seq.seq) -> 'a -> 'b -> 'c Seq.seq
    9.58 +    val skipto_skipseq : int -> 'a Seq.seq Seq.seq -> 'a skipseq
    9.59 +
    9.60 +    (* tactics *)
    9.61 +    val eqsubst_asm_tac :
    9.62 +       Proof.context ->
    9.63 +       int list -> Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
    9.64 +    val eqsubst_asm_tac' :
    9.65 +       Proof.context ->
    9.66 +       (searchinfo -> int -> Term.term -> match skipseq) ->
    9.67 +       int -> Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq
    9.68 +    val eqsubst_tac :
    9.69 +       Proof.context ->
    9.70 +       int list -> (* list of occurences to rewrite, use [0] for any *)
    9.71 +       Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
    9.72 +    val eqsubst_tac' :
    9.73 +       Proof.context -> (* proof context *)
    9.74 +       (searchinfo -> Term.term -> match Seq.seq) (* search function *)
    9.75 +       -> Thm.thm (* equation theorem to rewrite with *)
    9.76 +       -> int (* subgoal number in goal theorem *)
    9.77 +       -> Thm.thm (* goal theorem *)
    9.78 +       -> Thm.thm Seq.seq (* rewritten goal theorem *)
    9.79 +
    9.80 +
    9.81 +    val fakefree_badbounds :
    9.82 +       (string * Term.typ) list ->
    9.83 +       Term.term ->
    9.84 +       (string * Term.typ) list * (string * Term.typ) list * Term.term
    9.85 +
    9.86 +    val mk_foo_match :
    9.87 +       (Term.term -> Term.term) ->
    9.88 +       ('a * Term.typ) list -> Term.term -> Term.term
    9.89 +
    9.90 +    (* preparing substitution *)
    9.91 +    val prep_meta_eq : Proof.context -> Thm.thm -> Thm.thm list
    9.92 +    val prep_concl_subst :
    9.93 +       int -> Thm.thm -> (Thm.cterm list * Thm.thm) * searchinfo
    9.94 +    val prep_subst_in_asm :
    9.95 +       int -> Thm.thm -> int ->
    9.96 +       (Thm.cterm list * int * int * Thm.thm) * searchinfo
    9.97 +    val prep_subst_in_asms :
    9.98 +       int -> Thm.thm ->
    9.99 +       ((Thm.cterm list * int * int * Thm.thm) * searchinfo) list
   9.100 +    val prep_zipper_match :
   9.101 +       Zipper.T -> Term.term * ((string * Term.typ) list * (string * Term.typ) list * Term.term)
   9.102 +
   9.103 +    (* search for substitutions *)
   9.104 +    val valid_match_start : Zipper.T -> bool
   9.105 +    val search_lr_all : Zipper.T -> Zipper.T Seq.seq
   9.106 +    val search_lr_valid : (Zipper.T -> bool) -> Zipper.T -> Zipper.T Seq.seq
   9.107 +    val searchf_lr_unify_all :
   9.108 +       searchinfo -> Term.term -> match Seq.seq Seq.seq
   9.109 +    val searchf_lr_unify_valid :
   9.110 +       searchinfo -> Term.term -> match Seq.seq Seq.seq
   9.111 +    val searchf_bt_unify_valid :
   9.112 +       searchinfo -> Term.term -> match Seq.seq Seq.seq
   9.113 +
   9.114 +    (* syntax tools *)
   9.115 +    val ith_syntax : Args.T list -> int list * Args.T list
   9.116 +    val options_syntax : Args.T list -> bool * Args.T list
   9.117 +
   9.118 +    (* Isar level hooks *)
   9.119 +    val eqsubst_asm_meth : Proof.context -> int list -> Thm.thm list -> Proof.method
   9.120 +    val eqsubst_meth : Proof.context -> int list -> Thm.thm list -> Proof.method
   9.121 +    val subst_meth : Method.src -> Proof.context -> Proof.method
   9.122 +    val setup : theory -> theory
   9.123 +
   9.124 +end;
   9.125 +
   9.126 +structure EqSubst
   9.127 +: EQSUBST
   9.128 += struct
   9.129 +
   9.130 +structure Z = Zipper;
   9.131 +
   9.132 +(* changes object "=" to meta "==" which prepares a given rewrite rule *)
   9.133 +fun prep_meta_eq ctxt =
   9.134 +  let val (_, {mk_rews = {mk, ...}, ...}) = Simplifier.rep_ss (Simplifier.local_simpset_of ctxt)
   9.135 +  in mk #> map Drule.zero_var_indexes end;
   9.136 +
   9.137 +
   9.138 +  (* a type abriviation for match information *)
   9.139 +  type match =
   9.140 +       ((indexname * (sort * typ)) list (* type instantiations *)
   9.141 +        * (indexname * (typ * term)) list) (* term instantiations *)
   9.142 +       * (string * typ) list (* fake named type abs env *)
   9.143 +       * (string * typ) list (* type abs env *)
   9.144 +       * term (* outer term *)
   9.145 +
   9.146 +  type searchinfo =
   9.147 +       theory
   9.148 +       * int (* maxidx *)
   9.149 +       * Zipper.T (* focusterm to search under *)
   9.150 +
   9.151 +
   9.152 +(* skipping non-empty sub-sequences but when we reach the end
   9.153 +   of the seq, remembering how much we have left to skip. *)
   9.154 +datatype 'a skipseq = SkipMore of int
   9.155 +  | SkipSeq of 'a Seq.seq Seq.seq;
   9.156 +(* given a seqseq, skip the first m non-empty seq's, note deficit *)
   9.157 +fun skipto_skipseq m s = 
   9.158 +    let 
   9.159 +      fun skip_occs n sq = 
   9.160 +          case Seq.pull sq of 
   9.161 +            NONE => SkipMore n
   9.162 +          | SOME (h,t) => 
   9.163 +            (case Seq.pull h of NONE => skip_occs n t
   9.164 +             | SOME _ => if n <= 1 then SkipSeq (Seq.cons h t)
   9.165 +                         else skip_occs (n - 1) t)
   9.166 +    in (skip_occs m s) end;
   9.167 +
   9.168 +(* note: outerterm is the taget with the match replaced by a bound 
   9.169 +         variable : ie: "P lhs" beocmes "%x. P x" 
   9.170 +         insts is the types of instantiations of vars in lhs
   9.171 +         and typinsts is the type instantiations of types in the lhs
   9.172 +         Note: Final rule is the rule lifted into the ontext of the 
   9.173 +         taget thm. *)
   9.174 +fun mk_foo_match mkuptermfunc Ts t = 
   9.175 +    let 
   9.176 +      val ty = Term.type_of t
   9.177 +      val bigtype = (rev (map snd Ts)) ---> ty
   9.178 +      fun mk_foo 0 t = t
   9.179 +        | mk_foo i t = mk_foo (i - 1) (t $ (Bound (i - 1)))
   9.180 +      val num_of_bnds = (length Ts)
   9.181 +      (* foo_term = "fooabs y0 ... yn" where y's are local bounds *)
   9.182 +      val foo_term = mk_foo num_of_bnds (Bound num_of_bnds)
   9.183 +    in Abs("fooabs", bigtype, mkuptermfunc foo_term) end;
   9.184 +
   9.185 +(* T is outer bound vars, n is number of locally bound vars *)
   9.186 +(* THINK: is order of Ts correct...? or reversed? *)
   9.187 +fun fakefree_badbounds Ts t = 
   9.188 +    let val (FakeTs,Ts,newnames) = 
   9.189 +            List.foldr (fn ((n,ty),(FakeTs,Ts,usednames)) => 
   9.190 +                           let val newname = Name.variant usednames n
   9.191 +                           in ((RWTools.mk_fake_bound_name newname,ty)::FakeTs,
   9.192 +                               (newname,ty)::Ts, 
   9.193 +                               newname::usednames) end)
   9.194 +                       ([],[],[])
   9.195 +                       Ts
   9.196 +    in (FakeTs, Ts, Term.subst_bounds (map Free FakeTs, t)) end;
   9.197 +
   9.198 +(* before matching we need to fake the bound vars that are missing an
   9.199 +abstraction. In this function we additionally construct the
   9.200 +abstraction environment, and an outer context term (with the focus
   9.201 +abstracted out) for use in rewriting with RWInst.rw *)
   9.202 +fun prep_zipper_match z = 
   9.203 +    let 
   9.204 +      val t = Z.trm z  
   9.205 +      val c = Z.ctxt z
   9.206 +      val Ts = Z.C.nty_ctxt c
   9.207 +      val (FakeTs', Ts', t') = fakefree_badbounds Ts t
   9.208 +      val absterm = mk_foo_match (Z.C.apply c) Ts' t'
   9.209 +    in
   9.210 +      (t', (FakeTs', Ts', absterm))
   9.211 +    end;
   9.212 +
   9.213 +(* Matching and Unification with exception handled *)
   9.214 +fun clean_match thy (a as (pat, t)) =
   9.215 +  let val (tyenv, tenv) = Pattern.match thy a (Vartab.empty, Vartab.empty)
   9.216 +  in SOME (Vartab.dest tyenv, Vartab.dest tenv)
   9.217 +  end handle Pattern.MATCH => NONE;
   9.218 +
   9.219 +(* given theory, max var index, pat, tgt; returns Seq of instantiations *)
   9.220 +fun clean_unify thry ix (a as (pat, tgt)) =
   9.221 +    let
   9.222 +      (* type info will be re-derived, maybe this can be cached
   9.223 +         for efficiency? *)
   9.224 +      val pat_ty = Term.type_of pat;
   9.225 +      val tgt_ty = Term.type_of tgt;
   9.226 +      (* is it OK to ignore the type instantiation info?
   9.227 +         or should I be using it? *)
   9.228 +      val typs_unify =
   9.229 +          SOME (Sign.typ_unify thry (pat_ty, tgt_ty) (Vartab.empty, ix))
   9.230 +            handle Type.TUNIFY => NONE;
   9.231 +    in
   9.232 +      case typs_unify of
   9.233 +        SOME (typinsttab, ix2) =>
   9.234 +        let
   9.235 +      (* is it right to throw away the flexes?
   9.236 +         or should I be using them somehow? *)
   9.237 +          fun mk_insts env =
   9.238 +            (Vartab.dest (Envir.type_env env),
   9.239 +             Envir.alist_of env);
   9.240 +          val initenv = Envir.Envir {asol = Vartab.empty,
   9.241 +                                     iTs = typinsttab, maxidx = ix2};
   9.242 +          val useq = Unify.smash_unifiers thry [a] initenv
   9.243 +	            handle UnequalLengths => Seq.empty
   9.244 +		               | Term.TERM _ => Seq.empty;
   9.245 +          fun clean_unify' useq () =
   9.246 +              (case (Seq.pull useq) of
   9.247 +                 NONE => NONE
   9.248 +               | SOME (h,t) => SOME (mk_insts h, Seq.make (clean_unify' t)))
   9.249 +	            handle UnequalLengths => NONE
   9.250 +                   | Term.TERM _ => NONE
   9.251 +        in
   9.252 +          (Seq.make (clean_unify' useq))
   9.253 +        end
   9.254 +      | NONE => Seq.empty
   9.255 +    end;
   9.256 +
   9.257 +(* Matching and Unification for zippers *)
   9.258 +(* Note: Ts is a modified version of the original names of the outer
   9.259 +bound variables. New names have been introduced to make sure they are
   9.260 +unique w.r.t all names in the term and each other. usednames' is
   9.261 +oldnames + new names. *)
   9.262 +fun clean_match_z thy pat z = 
   9.263 +    let val (t, (FakeTs,Ts,absterm)) = prep_zipper_match z in
   9.264 +      case clean_match thy (pat, t) of 
   9.265 +        NONE => NONE 
   9.266 +      | SOME insts => SOME (insts, FakeTs, Ts, absterm) end;
   9.267 +(* ix = max var index *)
   9.268 +fun clean_unify_z sgn ix pat z = 
   9.269 +    let val (t, (FakeTs, Ts,absterm)) = prep_zipper_match z in
   9.270 +    Seq.map (fn insts => (insts, FakeTs, Ts, absterm)) 
   9.271 +            (clean_unify sgn ix (t, pat)) end;
   9.272 +
   9.273 +
   9.274 +(* FOR DEBUGGING...
   9.275 +type trace_subst_errT = int (* subgoal *)
   9.276 +        * thm (* thm with all goals *)
   9.277 +        * (Thm.cterm list (* certified free var placeholders for vars *)
   9.278 +           * thm)  (* trivial thm of goal concl *)
   9.279 +            (* possible matches/unifiers *)
   9.280 +        * thm (* rule *)
   9.281 +        * (((indexname * typ) list (* type instantiations *)
   9.282 +              * (indexname * term) list ) (* term instantiations *)
   9.283 +             * (string * typ) list (* Type abs env *)
   9.284 +             * term) (* outer term *);
   9.285 +
   9.286 +val trace_subst_err = (ref NONE : trace_subst_errT option ref);
   9.287 +val trace_subst_search = ref false;
   9.288 +exception trace_subst_exp of trace_subst_errT;
   9.289 +*)
   9.290 +
   9.291 +
   9.292 +fun bot_left_leaf_of (l $ r) = bot_left_leaf_of l
   9.293 +  | bot_left_leaf_of (Abs(s,ty,t)) = bot_left_leaf_of t
   9.294 +  | bot_left_leaf_of x = x;
   9.295 +
   9.296 +(* Avoid considering replacing terms which have a var at the head as
   9.297 +   they always succeed trivially, and uninterestingly. *)
   9.298 +fun valid_match_start z =
   9.299 +    (case bot_left_leaf_of (Z.trm z) of 
   9.300 +      Var _ => false 
   9.301 +      | _ => true);
   9.302 +
   9.303 +(* search from top, left to right, then down *)
   9.304 +val search_lr_all = ZipperSearch.all_bl_ur;
   9.305 +
   9.306 +(* search from top, left to right, then down *)
   9.307 +fun search_lr_valid validf =
   9.308 +    let 
   9.309 +      fun sf_valid_td_lr z = 
   9.310 +          let val here = if validf z then [Z.Here z] else [] in
   9.311 +            case Z.trm z 
   9.312 +             of _ $ _ => [Z.LookIn (Z.move_down_left z)] 
   9.313 +                         @ here 
   9.314 +                         @ [Z.LookIn (Z.move_down_right z)]
   9.315 +              | Abs _ => here @ [Z.LookIn (Z.move_down_abs z)]
   9.316 +              | _ => here
   9.317 +          end;
   9.318 +    in Z.lzy_search sf_valid_td_lr end;
   9.319 +
   9.320 +(* search from bottom to top, left to right *)
   9.321 +
   9.322 +fun search_bt_valid validf =
   9.323 +    let 
   9.324 +      fun sf_valid_td_lr z = 
   9.325 +          let val here = if validf z then [Z.Here z] else [] in
   9.326 +            case Z.trm z 
   9.327 +             of _ $ _ => [Z.LookIn (Z.move_down_left z), 
   9.328 +                          Z.LookIn (Z.move_down_right z)] @ here
   9.329 +              | Abs _ => [Z.LookIn (Z.move_down_abs z)] @ here
   9.330 +              | _ => here
   9.331 +          end;
   9.332 +    in Z.lzy_search sf_valid_td_lr end;
   9.333 +
   9.334 +fun searchf_unify_gen f (sgn, maxidx, z) lhs =
   9.335 +    Seq.map (clean_unify_z sgn maxidx lhs) 
   9.336 +            (Z.limit_apply f z);
   9.337 +
   9.338 +(* search all unifications *)
   9.339 +val searchf_lr_unify_all =
   9.340 +    searchf_unify_gen search_lr_all;
   9.341 +
   9.342 +(* search only for 'valid' unifiers (non abs subterms and non vars) *)
   9.343 +val searchf_lr_unify_valid = 
   9.344 +    searchf_unify_gen (search_lr_valid valid_match_start);
   9.345 +
   9.346 +val searchf_bt_unify_valid =
   9.347 +    searchf_unify_gen (search_bt_valid valid_match_start);
   9.348 +
   9.349 +(* apply a substitution in the conclusion of the theorem th *)
   9.350 +(* cfvs are certified free var placeholders for goal params *)
   9.351 +(* conclthm is a theorem of for just the conclusion *)
   9.352 +(* m is instantiation/match information *)
   9.353 +(* rule is the equation for substitution *)
   9.354 +fun apply_subst_in_concl i th (cfvs, conclthm) rule m =
   9.355 +    (RWInst.rw m rule conclthm)
   9.356 +      |> IsaND.unfix_frees cfvs
   9.357 +      |> RWInst.beta_eta_contract
   9.358 +      |> (fn r => Tactic.rtac r i th);
   9.359 +
   9.360 +(* substitute within the conclusion of goal i of gth, using a meta
   9.361 +equation rule. Note that we assume rule has var indicies zero'd *)
   9.362 +fun prep_concl_subst i gth =
   9.363 +    let
   9.364 +      val th = Thm.incr_indexes 1 gth;
   9.365 +      val tgt_term = Thm.prop_of th;
   9.366 +
   9.367 +      val sgn = Thm.theory_of_thm th;
   9.368 +      val ctermify = Thm.cterm_of sgn;
   9.369 +      val trivify = Thm.trivial o ctermify;
   9.370 +
   9.371 +      val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
   9.372 +      val cfvs = rev (map ctermify fvs);
   9.373 +
   9.374 +      val conclterm = Logic.strip_imp_concl fixedbody;
   9.375 +      val conclthm = trivify conclterm;
   9.376 +      val maxidx = Thm.maxidx_of th;
   9.377 +      val ft = ((Z.move_down_right (* ==> *)
   9.378 +                 o Z.move_down_left (* Trueprop *)
   9.379 +                 o Z.mktop
   9.380 +                 o Thm.prop_of) conclthm)
   9.381 +    in
   9.382 +      ((cfvs, conclthm), (sgn, maxidx, ft))
   9.383 +    end;
   9.384 +
   9.385 +(* substitute using an object or meta level equality *)
   9.386 +fun eqsubst_tac' ctxt searchf instepthm i th =
   9.387 +    let
   9.388 +      val (cvfsconclthm, searchinfo) = prep_concl_subst i th;
   9.389 +      val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
   9.390 +      fun rewrite_with_thm r =
   9.391 +          let val (lhs,_) = Logic.dest_equals (Thm.concl_of r);
   9.392 +          in searchf searchinfo lhs
   9.393 +             |> Seq.maps (apply_subst_in_concl i th cvfsconclthm r) end;
   9.394 +    in stepthms |> Seq.maps rewrite_with_thm end;
   9.395 +
   9.396 +
   9.397 +(* distinct subgoals *)
   9.398 +fun distinct_subgoals th =
   9.399 +  the_default th (SINGLE distinct_subgoals_tac th);
   9.400 +
   9.401 +(* General substitution of multiple occurances using one of
   9.402 +   the given theorems*)
   9.403 +
   9.404 +
   9.405 +exception eqsubst_occL_exp of
   9.406 +          string * (int list) * (thm list) * int * thm;
   9.407 +fun skip_first_occs_search occ srchf sinfo lhs =
   9.408 +    case (skipto_skipseq occ (srchf sinfo lhs)) of
   9.409 +      SkipMore _ => Seq.empty
   9.410 +    | SkipSeq ss => Seq.flat ss;
   9.411 +
   9.412 +(* The occL is a list of integers indicating which occurence
   9.413 +w.r.t. the search order, to rewrite. Backtracking will also find later
   9.414 +occurences, but all earlier ones are skipped. Thus you can use [0] to
   9.415 +just find all rewrites. *)
   9.416 +
   9.417 +fun eqsubst_tac ctxt occL thms i th =
   9.418 +    let val nprems = Thm.nprems_of th in
   9.419 +      if nprems < i then Seq.empty else
   9.420 +      let val thmseq = (Seq.of_list thms)
   9.421 +        fun apply_occ occ th =
   9.422 +            thmseq |> Seq.maps
   9.423 +                    (fn r => eqsubst_tac' 
   9.424 +                               ctxt 
   9.425 +                               (skip_first_occs_search
   9.426 +                                  occ searchf_lr_unify_valid) r
   9.427 +                                 (i + ((Thm.nprems_of th) - nprems))
   9.428 +                                 th);
   9.429 +        val sortedoccL =
   9.430 +            Library.sort (Library.rev_order o Library.int_ord) occL;
   9.431 +      in
   9.432 +        Seq.map distinct_subgoals (Seq.EVERY (map apply_occ sortedoccL) th)
   9.433 +      end
   9.434 +    end
   9.435 +    handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
   9.436 +
   9.437 +
   9.438 +(* inthms are the given arguments in Isar, and treated as eqstep with
   9.439 +   the first one, then the second etc *)
   9.440 +fun eqsubst_meth ctxt occL inthms =
   9.441 +    Method.SIMPLE_METHOD' (eqsubst_tac ctxt occL inthms);
   9.442 +
   9.443 +(* apply a substitution inside assumption j, keeps asm in the same place *)
   9.444 +fun apply_subst_in_asm i th rule ((cfvs, j, ngoalprems, pth),m) =
   9.445 +    let
   9.446 +      val th2 = Thm.rotate_rule (j - 1) i th; (* put premice first *)
   9.447 +      val preelimrule =
   9.448 +          (RWInst.rw m rule pth)
   9.449 +            |> (Seq.hd o prune_params_tac)
   9.450 +            |> Thm.permute_prems 0 ~1 (* put old asm first *)
   9.451 +            |> IsaND.unfix_frees cfvs (* unfix any global params *)
   9.452 +            |> RWInst.beta_eta_contract; (* normal form *)
   9.453 +  (*    val elimrule =
   9.454 +          preelimrule
   9.455 +            |> Tactic.make_elim (* make into elim rule *)
   9.456 +            |> Thm.lift_rule (th2, i); (* lift into context *)
   9.457 +   *)
   9.458 +    in
   9.459 +      (* ~j because new asm starts at back, thus we subtract 1 *)
   9.460 +      Seq.map (Thm.rotate_rule (~j) ((Thm.nprems_of rule) + i))
   9.461 +      (Tactic.dtac preelimrule i th2)
   9.462 +
   9.463 +      (* (Thm.bicompose
   9.464 +                 false (* use unification *)
   9.465 +                 (true, (* elim resolution *)
   9.466 +                  elimrule, (2 + (Thm.nprems_of rule)) - ngoalprems)
   9.467 +                 i th2) *)
   9.468 +    end;
   9.469 +
   9.470 +
   9.471 +(* prepare to substitute within the j'th premise of subgoal i of gth,
   9.472 +using a meta-level equation. Note that we assume rule has var indicies
   9.473 +zero'd. Note that we also assume that premt is the j'th premice of
   9.474 +subgoal i of gth. Note the repetition of work done for each
   9.475 +assumption, i.e. this can be made more efficient for search over
   9.476 +multiple assumptions.  *)
   9.477 +fun prep_subst_in_asm i gth j =
   9.478 +    let
   9.479 +      val th = Thm.incr_indexes 1 gth;
   9.480 +      val tgt_term = Thm.prop_of th;
   9.481 +
   9.482 +      val sgn = Thm.theory_of_thm th;
   9.483 +      val ctermify = Thm.cterm_of sgn;
   9.484 +      val trivify = Thm.trivial o ctermify;
   9.485 +
   9.486 +      val (fixedbody, fvs) = IsaND.fix_alls_term i tgt_term;
   9.487 +      val cfvs = rev (map ctermify fvs);
   9.488 +
   9.489 +      val asmt = nth (Logic.strip_imp_prems fixedbody) (j - 1);
   9.490 +      val asm_nprems = length (Logic.strip_imp_prems asmt);
   9.491 +
   9.492 +      val pth = trivify asmt;
   9.493 +      val maxidx = Thm.maxidx_of th;
   9.494 +
   9.495 +      val ft = ((Z.move_down_right (* trueprop *)
   9.496 +                 o Z.mktop
   9.497 +                 o Thm.prop_of) pth)
   9.498 +    in ((cfvs, j, asm_nprems, pth), (sgn, maxidx, ft)) end;
   9.499 +
   9.500 +(* prepare subst in every possible assumption *)
   9.501 +fun prep_subst_in_asms i gth =
   9.502 +    map (prep_subst_in_asm i gth)
   9.503 +        ((fn l => Library.upto (1, length l))
   9.504 +           (Logic.prems_of_goal (Thm.prop_of gth) i));
   9.505 +
   9.506 +
   9.507 +(* substitute in an assumption using an object or meta level equality *)
   9.508 +fun eqsubst_asm_tac' ctxt searchf skipocc instepthm i th =
   9.509 +    let
   9.510 +      val asmpreps = prep_subst_in_asms i th;
   9.511 +      val stepthms = Seq.of_list (prep_meta_eq ctxt instepthm);
   9.512 +      fun rewrite_with_thm r =
   9.513 +          let val (lhs,_) = Logic.dest_equals (Thm.concl_of r)
   9.514 +            fun occ_search occ [] = Seq.empty
   9.515 +              | occ_search occ ((asminfo, searchinfo)::moreasms) =
   9.516 +                (case searchf searchinfo occ lhs of
   9.517 +                   SkipMore i => occ_search i moreasms
   9.518 +                 | SkipSeq ss =>
   9.519 +                   Seq.append (Seq.map (Library.pair asminfo) (Seq.flat ss))
   9.520 +                               (occ_search 1 moreasms))
   9.521 +                              (* find later substs also *)
   9.522 +          in
   9.523 +            occ_search skipocc asmpreps |> Seq.maps (apply_subst_in_asm i th r)
   9.524 +          end;
   9.525 +    in stepthms |> Seq.maps rewrite_with_thm end;
   9.526 +
   9.527 +
   9.528 +fun skip_first_asm_occs_search searchf sinfo occ lhs =
   9.529 +    skipto_skipseq occ (searchf sinfo lhs);
   9.530 +
   9.531 +fun eqsubst_asm_tac ctxt occL thms i th =
   9.532 +    let val nprems = Thm.nprems_of th
   9.533 +    in
   9.534 +      if nprems < i then Seq.empty else
   9.535 +      let val thmseq = (Seq.of_list thms)
   9.536 +        fun apply_occ occK th =
   9.537 +            thmseq |> Seq.maps
   9.538 +                    (fn r =>
   9.539 +                        eqsubst_asm_tac' ctxt (skip_first_asm_occs_search
   9.540 +                                            searchf_lr_unify_valid) occK r
   9.541 +                                         (i + ((Thm.nprems_of th) - nprems))
   9.542 +                                         th);
   9.543 +        val sortedoccs =
   9.544 +            Library.sort (Library.rev_order o Library.int_ord) occL
   9.545 +      in
   9.546 +        Seq.map distinct_subgoals
   9.547 +                (Seq.EVERY (map apply_occ sortedoccs) th)
   9.548 +      end
   9.549 +    end
   9.550 +    handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
   9.551 +
   9.552 +(* inthms are the given arguments in Isar, and treated as eqstep with
   9.553 +   the first one, then the second etc *)
   9.554 +fun eqsubst_asm_meth ctxt occL inthms =
   9.555 +    Method.SIMPLE_METHOD' (eqsubst_asm_tac ctxt occL inthms);
   9.556 +
   9.557 +(* syntax for options, given "(asm)" will give back true, without
   9.558 +   gives back false *)
   9.559 +val options_syntax =
   9.560 +    (Args.parens (Args.$$$ "asm") >> (K true)) ||
   9.561 +     (Scan.succeed false);
   9.562 +
   9.563 +val ith_syntax =
   9.564 +    Scan.optional (Args.parens (Scan.repeat OuterParse.nat)) [0];
   9.565 +
   9.566 +(* combination method that takes a flag (true indicates that subst
   9.567 +should be done to an assumption, false = apply to the conclusion of
   9.568 +the goal) as well as the theorems to use *)
   9.569 +fun subst_meth src =
   9.570 +  Method.syntax ((Scan.lift options_syntax) -- (Scan.lift ith_syntax) -- Attrib.thms) src
   9.571 +  #> (fn (((asmflag, occL), inthms), ctxt) =>
   9.572 +    (if asmflag then eqsubst_asm_meth else eqsubst_meth) ctxt occL inthms);
   9.573 +
   9.574 +
   9.575 +val setup =
   9.576 +  Method.add_method ("subst", subst_meth, "single-step substitution");
   9.577 +
   9.578 +end;
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/Tools/project_rule.ML	Sat Feb 28 14:02:12 2009 +0100
    10.3 @@ -0,0 +1,65 @@
    10.4 +(*  Title:      Tools/project_rule.ML
    10.5 +    Author:     Makarius
    10.6 +
    10.7 +Transform mutual rule:
    10.8 +
    10.9 +  HH ==> (x1:A1 --> P1 x1) & ... & (xn:An --> Pn xn)
   10.10 +
   10.11 +into projection:
   10.12 +
   10.13 +  xi:Ai ==> HH ==> Pi xi
   10.14 +*)
   10.15 +
   10.16 +signature PROJECT_RULE_DATA =
   10.17 +sig
   10.18 +  val conjunct1: thm
   10.19 +  val conjunct2: thm
   10.20 +  val mp: thm
   10.21 +end;
   10.22 +
   10.23 +signature PROJECT_RULE =
   10.24 +sig
   10.25 +  val project: Proof.context -> int -> thm -> thm
   10.26 +  val projects: Proof.context -> int list -> thm -> thm list
   10.27 +  val projections: Proof.context -> thm -> thm list
   10.28 +end;
   10.29 +
   10.30 +functor ProjectRuleFun(Data: PROJECT_RULE_DATA): PROJECT_RULE =
   10.31 +struct
   10.32 +
   10.33 +fun conj1 th = th RS Data.conjunct1;
   10.34 +fun conj2 th = th RS Data.conjunct2;
   10.35 +fun imp th = th RS Data.mp;
   10.36 +
   10.37 +fun projects ctxt is raw_rule =
   10.38 +  let
   10.39 +    fun proj 1 th = the_default th (try conj1 th)
   10.40 +      | proj k th = proj (k - 1) (conj2 th);
   10.41 +    fun prems k th =
   10.42 +      (case try imp th of
   10.43 +        NONE => (k, th)
   10.44 +      | SOME th' => prems (k + 1) th');
   10.45 +    val ((_, [rule]), ctxt') = Variable.import_thms true [raw_rule] ctxt;
   10.46 +    fun result i =
   10.47 +      rule
   10.48 +      |> proj i
   10.49 +      |> prems 0 |-> (fn k =>
   10.50 +        Thm.permute_prems 0 (~ k)
   10.51 +        #> singleton (Variable.export ctxt' ctxt)
   10.52 +        #> Drule.zero_var_indexes
   10.53 +        #> RuleCases.save raw_rule
   10.54 +        #> RuleCases.add_consumes k);
   10.55 +  in map result is end;
   10.56 +
   10.57 +fun project ctxt i th = hd (projects ctxt [i] th);
   10.58 +
   10.59 +fun projections ctxt raw_rule =
   10.60 +  let
   10.61 +    fun projs k th =
   10.62 +      (case try conj2 th of
   10.63 +        NONE => k
   10.64 +      | SOME th' => projs (k + 1) th');
   10.65 +    val ((_, [rule]), _) = Variable.import_thms true [raw_rule] ctxt;
   10.66 +  in projects ctxt (1 upto projs 1 rule) raw_rule end;
   10.67 +
   10.68 +end;