src/FOL/simpdata.ML
changeset 11232 558a4feebb04
parent 10431 bb67f704d631
child 11344 57b7ad51971c
     1.1 --- a/src/FOL/simpdata.ML	Thu Mar 29 12:26:37 2001 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Thu Mar 29 13:59:54 2001 +0200
     1.3 @@ -218,6 +218,15 @@
     1.4      "(ALL x. P(x) & Q(x)) <-> ((ALL x. P(x)) & (ALL x. Q(x)))";
     1.5  
     1.6  
     1.7 +local
     1.8 +val uncurry = prove_goal (the_context()) "P --> Q --> R ==> P & Q --> R"
     1.9 +              (fn prems => [cut_facts_tac prems 1, Blast_tac 1]);
    1.10 +
    1.11 +val iff_allI = allI RS
    1.12 +    prove_goal (the_context()) "ALL x. P(x) <-> Q(x) ==> (ALL x. P(x)) <-> (ALL x. Q(x))"
    1.13 +               (fn prems => [cut_facts_tac prems 1, Blast_tac 1])
    1.14 +in
    1.15 +
    1.16  (** make simplification procedures for quantifier elimination **)
    1.17  structure Quantifier1 = Quantifier1Fun(
    1.18  struct
    1.19 @@ -226,30 +235,32 @@
    1.20      | dest_eq _ = None;
    1.21    fun dest_conj((c as Const("op &",_)) $ s $ t) = Some(c,s,t)
    1.22      | dest_conj _ = None;
    1.23 +  fun dest_imp((c as Const("op -->",_)) $ s $ t) = Some(c,s,t)
    1.24 +    | dest_imp _ = None;
    1.25    val conj = FOLogic.conj
    1.26    val imp  = FOLogic.imp
    1.27    (*rules*)
    1.28    val iff_reflection = iff_reflection
    1.29    val iffI = iffI
    1.30 -  val sym  = sym
    1.31    val conjI= conjI
    1.32    val conjE= conjE
    1.33    val impI = impI
    1.34 -  val impE = impE
    1.35    val mp   = mp
    1.36 +  val uncurry = uncurry
    1.37    val exI  = exI
    1.38    val exE  = exE
    1.39 -  val allI = allI
    1.40 -  val allE = allE
    1.41 +  val iff_allI = iff_allI
    1.42  end);
    1.43  
    1.44 +end;
    1.45 +
    1.46  local
    1.47  
    1.48  val ex_pattern =
    1.49    read_cterm (Theory.sign_of (the_context ())) ("EX x. P(x) & Q(x)", FOLogic.oT)
    1.50  
    1.51  val all_pattern =
    1.52 -  read_cterm (Theory.sign_of (the_context ())) ("ALL x. P(x) & P'(x) --> Q(x)", FOLogic.oT)
    1.53 +  read_cterm (Theory.sign_of (the_context ())) ("ALL x. P(x) --> Q(x)", FOLogic.oT)
    1.54  
    1.55  in
    1.56  val defEX_regroup =