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 =
```