src/Provers/eqsubst.ML
changeset 15959 366d39e95d3c
parent 15936 817ac93ee786
child 16004 031f56012483
     1.1 --- a/src/Provers/eqsubst.ML	Fri May 13 19:55:09 2005 +0200
     1.2 +++ b/src/Provers/eqsubst.ML	Fri May 13 20:21:41 2005 +0200
     1.3 @@ -27,6 +27,9 @@
     1.4  signature EQSUBST_TAC = 
     1.5  sig
     1.6  
     1.7 +  exception eqsubst_occL_exp of 
     1.8 +            string * (int list) * (Thm.thm list) * int * Thm.thm;
     1.9 +
    1.10    type match = 
    1.11         ((Term.indexname * (Term.sort * Term.typ)) list (* type instantiations *)
    1.12          * (Term.indexname * (Term.typ * Term.term)) list) (* term instantiations *)
    1.13 @@ -273,9 +276,29 @@
    1.14  
    1.15      in (stepthms :-> rewrite_with_thm) end;
    1.16  
    1.17 +(* Tactic.distinct_subgoals_tac *)
    1.18 +
    1.19 +(* custom version of distinct subgoals that works with term and 
    1.20 +   type variables. Asssumes th is in beta-eta normal form. 
    1.21 +   Also, does nothing if flexflex contraints are present. *)
    1.22 +fun distinct_subgoals th =
    1.23 +    if List.null (Thm.tpairs_of th) then
    1.24 +      let val (fixes,fixedthm) = IsaND.fix_vars_and_tvars th
    1.25 +        val (fixedthconcl,cprems) = IsaND.hide_prems fixedthm
    1.26 +      in
    1.27 +        IsaND.unfix_frees_and_tfrees 
    1.28 +          fixes
    1.29 +          (Drule.implies_intr_list 
    1.30 +             (Library.gen_distinct 
    1.31 +                (fn (x, y) => Thm.term_of x = Thm.term_of y)
    1.32 +                cprems) fixedthconcl)
    1.33 +      end
    1.34 +    else th;
    1.35  
    1.36  (* General substiuttion of multiple occurances using one of 
    1.37     the given theorems*)
    1.38 +exception eqsubst_occL_exp of 
    1.39 +          string * (int list) * (Thm.thm list) * int * Thm.thm;
    1.40  fun eqsubst_occL tac occL thms i th = 
    1.41      let val nprems = Thm.nprems_of th in
    1.42        if nprems < i then Seq.empty else
    1.43 @@ -287,10 +310,15 @@
    1.44                                   (i + ((Thm.nprems_of th) - nprems))
    1.45                                   th);
    1.46        in
    1.47 -        Seq.EVERY (map apply_occ (Library.sort (Library.rev_order o Library.int_ord) occL)) 
    1.48 -                  th
    1.49 +        Seq.map distinct_subgoals
    1.50 +                (Seq.EVERY (map apply_occ 
    1.51 +                                (Library.sort (Library.rev_order 
    1.52 +                                               o Library.int_ord) occL)) th)
    1.53        end
    1.54 -    end;
    1.55 +    end
    1.56 +    handle THM _ => raise eqsubst_occL_exp ("THM",occL,thms,i,th);
    1.57 +
    1.58 +        
    1.59  
    1.60  (* implicit argus: occL thms i th *)
    1.61  val eqsubst_tac = eqsubst_occL eqsubst_tac';