Removed disjE from list of rules used to simplify elimination
authorberghofe
Fri Jul 03 11:02:01 1998 +0200 (1998-07-03)
changeset 5120f7f5442c934a
parent 5119 58d267fc8630
child 5121 5c1f89ae8aef
Removed disjE from list of rules used to simplify elimination
rules because it made mk_cases fail if elimination rules
contained disjunctive side conditions.
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Jul 03 10:55:32 1998 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Jul 03 11:02:01 1998 +0200
     1.3 @@ -57,7 +57,7 @@
     1.4       (fn _ => [assume_tac 1]);
     1.5  
     1.6  (*For simplifying the elimination rule*)
     1.7 -val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE, disjE, Pair_inject];
     1.8 +val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE, Pair_inject];
     1.9  
    1.10  val vimage_name = Sign.intern_const (sign_of Vimage.thy) "op -``";
    1.11  val mono_name = Sign.intern_const (sign_of Ord.thy) "mono";
    1.12 @@ -284,7 +284,6 @@
    1.13  (*Applies freeness of the given constructors, which *must* be unfolded by
    1.14    the given defs.  Cannot simply use the local con_defs because con_defs=[] 
    1.15    for inference systems.
    1.16 -  FIXME: proper handling of conjunctive / disjunctive side conditions?!
    1.17   *)
    1.18  fun con_elim_tac simps =
    1.19    let val elim_tac = REPEAT o (eresolve_tac elim_rls)
    1.20 @@ -296,10 +295,10 @@
    1.21    end;
    1.22  
    1.23  (*String s should have the form t:Si where Si is an inductive set*)
    1.24 -fun mk_cases elims defs s =
    1.25 +fun mk_cases elims simps s =
    1.26    let val prem = assume (read_cterm (sign_of_thm (hd elims)) (s, propT));
    1.27        val elims' = map (try (fn r =>
    1.28 -        rule_by_tactic (con_elim_tac defs) (prem RS r) |> standard)) elims
    1.29 +        rule_by_tactic (con_elim_tac simps) (prem RS r) |> standard)) elims
    1.30    in case find_first is_some elims' of
    1.31         Some (Some r) => r
    1.32       | None => error ("mk_cases: string '" ^ s ^ "' not of form 't : S_i'")