ObjectLogic.is_elim;
authorwenzelm
Tue Mar 14 16:29:34 2006 +0100 (2006-03-14)
changeset 192574463aee061bc
parent 19256 a49c0f7c9634
child 19258 ada9977f1e98
ObjectLogic.is_elim;
src/Provers/classical.ML
     1.1 --- a/src/Provers/classical.ML	Tue Mar 14 16:29:32 2006 +0100
     1.2 +++ b/src/Provers/classical.ML	Tue Mar 14 16:29:34 2006 +0100
     1.3 @@ -178,29 +178,13 @@
     1.4      [| inj f; ~ W ==> f x = f y; x = y ==> W |] ==> W
     1.5  *)
     1.6  
     1.7 -local
     1.8 -
     1.9 -fun equal_concl concl prop =
    1.10 -  concl aconv Logic.strip_assums_concl prop;
    1.11 -
    1.12 -fun is_elim rule =
    1.13 -  let
    1.14 -    val thy = Thm.theory_of_thm rule;
    1.15 -    val concl = Thm.concl_of rule;
    1.16 -  in
    1.17 -    Term.is_Var (ObjectLogic.drop_judgment thy concl) andalso
    1.18 -    exists (equal_concl concl) (Thm.prems_of rule)
    1.19 -  end;
    1.20 -
    1.21 -in
    1.22 -
    1.23  fun classical_rule rule =
    1.24 -  if is_elim rule then
    1.25 +  if ObjectLogic.is_elim rule then
    1.26      let
    1.27        val rule' = rule RS classical;
    1.28        val concl' = Thm.concl_of rule';
    1.29        fun redundant_hyp goal =
    1.30 -         equal_concl concl' goal orelse
    1.31 +        concl' aconv Logic.strip_assums_concl goal orelse
    1.32            (case Logic.strip_assums_hyp goal of
    1.33              hyp :: hyps => exists (fn t => t aconv hyp) hyps
    1.34            | _ => false);
    1.35 @@ -215,7 +199,6 @@
    1.36      in if Drule.weak_eq_thm (rule, rule'') then rule else rule'' end
    1.37    else rule;
    1.38  
    1.39 -end;
    1.40  
    1.41  
    1.42  (*** Useful tactics for classical reasoning ***)