src/FOL/simpdata.ML
changeset 12526 1b9db2581fe2
parent 12038 343a9888e875
child 12720 f8a134b9a57f
     1.1 --- a/src/FOL/simpdata.ML	Mon Dec 17 14:24:11 2001 +0100
     1.2 +++ b/src/FOL/simpdata.ML	Mon Dec 17 14:27:18 2001 +0100
     1.3 @@ -225,6 +225,14 @@
     1.4  val iff_allI = allI RS
     1.5      prove_goal (the_context()) "ALL x. P(x) <-> Q(x) ==> (ALL x. P(x)) <-> (ALL x. Q(x))"
     1.6                 (fn prems => [cut_facts_tac prems 1, Blast_tac 1])
     1.7 +val iff_exI = allI RS
     1.8 +    prove_goal (the_context()) "ALL x. P(x) <-> Q(x) ==> (EX x. P(x)) <-> (EX x. Q(x))"
     1.9 +               (fn prems => [cut_facts_tac prems 1, Blast_tac 1])
    1.10 +
    1.11 +val all_comm = prove_goal (the_context()) "(ALL x y. P(x,y)) <-> (ALL y x. P(x,y))"
    1.12 +               (fn _ => [Blast_tac 1])
    1.13 +val ex_comm = prove_goal (the_context()) "(EX x y. P(x,y)) <-> (EX y x. P(x,y))"
    1.14 +               (fn _ => [Blast_tac 1])
    1.15  in
    1.16  
    1.17  (** make simplification procedures for quantifier elimination **)
    1.18 @@ -242,6 +250,7 @@
    1.19    (*rules*)
    1.20    val iff_reflection = iff_reflection
    1.21    val iffI = iffI
    1.22 +  val iff_trans = iff_trans
    1.23    val conjI= conjI
    1.24    val conjE= conjE
    1.25    val impI = impI
    1.26 @@ -250,6 +259,9 @@
    1.27    val exI  = exI
    1.28    val exE  = exE
    1.29    val iff_allI = iff_allI
    1.30 +  val iff_exI = iff_exI
    1.31 +  val all_comm = all_comm
    1.32 +  val ex_comm = ex_comm
    1.33  end);
    1.34  
    1.35  end;
    1.36 @@ -257,10 +269,10 @@
    1.37  local
    1.38  
    1.39  val ex_pattern =
    1.40 -  read_cterm (Theory.sign_of (the_context ())) ("EX x. P(x) & Q(x)", FOLogic.oT)
    1.41 +  read_cterm (Theory.sign_of (the_context ())) ("EX x. P(x)", FOLogic.oT)
    1.42  
    1.43  val all_pattern =
    1.44 -  read_cterm (Theory.sign_of (the_context ())) ("ALL x. P(x) --> Q(x)", FOLogic.oT)
    1.45 +  read_cterm (Theory.sign_of (the_context ())) ("ALL x. P(x)", FOLogic.oT)
    1.46  
    1.47  in
    1.48  val defEX_regroup =