# HG changeset patch
# User paulson
# Date 1057049426 -7200
# Node ID 8dc3e532959a2390ce167d5f04de313952d2210f
# Parent  ccb48f3239f7394937bf72ee62f5ff7257ea30c6
moved some lemmas here from ZF

diff -r ccb48f3239f7 -r 8dc3e532959a src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Mon Jun 30 18:15:51 2003 +0200
+++ b/src/FOL/FOL.thy	Tue Jul 01 10:50:26 2003 +0200
@@ -43,6 +43,38 @@
 setup Splitter.setup
 setup Clasimp.setup
 
+subsection {* Other simple lemmas *}
+
+lemma [simp]: "((P-->R) <-> (Q-->R)) <-> ((P<->Q) | R)"
+by blast
+
+lemma [simp]: "((P-->Q) <-> (P-->R)) <-> (P --> (Q<->R))"
+by blast
+
+lemma not_disj_iff_imp: "~P | Q <-> (P-->Q)"
+by blast
+
+(** Monotonicity of implications **)
+
+lemma conj_mono: "[| P1-->Q1; P2-->Q2 |] ==> (P1&P2) --> (Q1&Q2)"
+by fast (*or (IntPr.fast_tac 1)*)
+
+lemma disj_mono: "[| P1-->Q1; P2-->Q2 |] ==> (P1|P2) --> (Q1|Q2)"
+by fast (*or (IntPr.fast_tac 1)*)
+
+lemma imp_mono: "[| Q1-->P1; P2-->Q2 |] ==> (P1-->P2)-->(Q1-->Q2)"
+by fast (*or (IntPr.fast_tac 1)*)
+
+lemma imp_refl: "P-->P"
+by (rule impI, assumption)
+
+(*The quantifier monotonicity rules are also intuitionistically valid*)
+lemma ex_mono: "(!!x. P(x) --> Q(x)) ==> (EX x. P(x)) --> (EX x. Q(x))"
+by blast
+
+lemma all_mono: "(!!x. P(x) --> Q(x)) ==> (ALL x. P(x)) --> (ALL x. Q(x))"
+by blast
+
 
 subsection {* Proof by cases and induction *}
 
diff -r ccb48f3239f7 -r 8dc3e532959a src/FOL/IFOL_lemmas.ML
--- a/src/FOL/IFOL_lemmas.ML	Mon Jun 30 18:15:51 2003 +0200
+++ b/src/FOL/IFOL_lemmas.ML	Tue Jul 01 10:50:26 2003 +0200
@@ -30,6 +30,31 @@
 val eq_reflection = thm "eq_reflection";
 val iff_reflection = thm "iff_reflection";
 
+structure IFOL =
+struct
+  val thy = the_context ();
+  val refl = refl;
+  val subst = subst;
+  val conjI = conjI;
+  val conjunct1 = conjunct1;
+  val conjunct2 = conjunct2;
+  val disjI1 = disjI1;
+  val disjI2 = disjI2;
+  val disjE = disjE;
+  val impI = impI;
+  val mp = mp;
+  val FalseE = FalseE;
+  val True_def = True_def;
+  val not_def = not_def;
+  val iff_def = iff_def;
+  val ex1_def = ex1_def;
+  val allI = allI;
+  val spec = spec;
+  val exI = exI;
+  val exE = exE;
+  val eq_reflection = eq_reflection;
+  val iff_reflection = iff_reflection;
+end;
 
 
 Goalw [True_def]  "True";