mods due to changed 1-point simprocs (quantifier1).
authornipkow
Mon Dec 17 14:27:18 2001 +0100 (2001-12-17 ago)
changeset 125261b9db2581fe2
parent 12525 4ad978c8f550
child 12527 d6c91bc3e49c
mods due to changed 1-point simprocs (quantifier1).
src/FOL/IsaMakefile
src/FOL/simpdata.ML
     1.1 --- a/src/FOL/IsaMakefile	Mon Dec 17 14:24:11 2001 +0100
     1.2 +++ b/src/FOL/IsaMakefile	Mon Dec 17 14:27:18 2001 +0100
     1.3 @@ -29,7 +29,7 @@
     1.4  $(OUT)/FOL: $(OUT)/Pure $(SRC)/Provers/blast.ML	$(SRC)/Provers/make_elim.ML \
     1.5    $(SRC)/Provers/clasimp.ML $(SRC)/Provers/classical.ML \
     1.6    $(SRC)/Provers/hypsubst.ML $(SRC)/Provers/ind.ML $(SRC)/Provers/induct_method.ML \
     1.7 -  $(SRC)/Provers/simplifier.ML $(SRC)/Provers/splitter.ML \
     1.8 +  $(SRC)/Provers/simplifier.ML $(SRC)/Provers/splitter.ML $(SRC)/Provers/quantifier1.ML\
     1.9    FOL.ML FOL.thy FOL_lemmas1.ML FOL_lemmas2.ML IFOL.ML IFOL.thy \
    1.10    IFOL_lemmas.ML ROOT.ML blastdata.ML cladata.ML document/root.tex \
    1.11    fologic.ML hypsubstdata.ML intprover.ML simpdata.ML
     2.1 --- a/src/FOL/simpdata.ML	Mon Dec 17 14:24:11 2001 +0100
     2.2 +++ b/src/FOL/simpdata.ML	Mon Dec 17 14:27:18 2001 +0100
     2.3 @@ -225,6 +225,14 @@
     2.4  val iff_allI = allI RS
     2.5      prove_goal (the_context()) "ALL x. P(x) <-> Q(x) ==> (ALL x. P(x)) <-> (ALL x. Q(x))"
     2.6                 (fn prems => [cut_facts_tac prems 1, Blast_tac 1])
     2.7 +val iff_exI = allI RS
     2.8 +    prove_goal (the_context()) "ALL x. P(x) <-> Q(x) ==> (EX x. P(x)) <-> (EX x. Q(x))"
     2.9 +               (fn prems => [cut_facts_tac prems 1, Blast_tac 1])
    2.10 +
    2.11 +val all_comm = prove_goal (the_context()) "(ALL x y. P(x,y)) <-> (ALL y x. P(x,y))"
    2.12 +               (fn _ => [Blast_tac 1])
    2.13 +val ex_comm = prove_goal (the_context()) "(EX x y. P(x,y)) <-> (EX y x. P(x,y))"
    2.14 +               (fn _ => [Blast_tac 1])
    2.15  in
    2.16  
    2.17  (** make simplification procedures for quantifier elimination **)
    2.18 @@ -242,6 +250,7 @@
    2.19    (*rules*)
    2.20    val iff_reflection = iff_reflection
    2.21    val iffI = iffI
    2.22 +  val iff_trans = iff_trans
    2.23    val conjI= conjI
    2.24    val conjE= conjE
    2.25    val impI = impI
    2.26 @@ -250,6 +259,9 @@
    2.27    val exI  = exI
    2.28    val exE  = exE
    2.29    val iff_allI = iff_allI
    2.30 +  val iff_exI = iff_exI
    2.31 +  val all_comm = all_comm
    2.32 +  val ex_comm = ex_comm
    2.33  end);
    2.34  
    2.35  end;
    2.36 @@ -257,10 +269,10 @@
    2.37  local
    2.38  
    2.39  val ex_pattern =
    2.40 -  read_cterm (Theory.sign_of (the_context ())) ("EX x. P(x) & Q(x)", FOLogic.oT)
    2.41 +  read_cterm (Theory.sign_of (the_context ())) ("EX x. P(x)", FOLogic.oT)
    2.42  
    2.43  val all_pattern =
    2.44 -  read_cterm (Theory.sign_of (the_context ())) ("ALL x. P(x) --> Q(x)", FOLogic.oT)
    2.45 +  read_cterm (Theory.sign_of (the_context ())) ("ALL x. P(x)", FOLogic.oT)
    2.46  
    2.47  in
    2.48  val defEX_regroup =