src/FOL/IFOL.thy
changeset 21539 c5cf9243ad62
parent 21524 7843e2fd14a9
child 22139 539a63b98f76
--- a/src/FOL/IFOL.thy	Sun Nov 26 23:09:25 2006 +0100
+++ b/src/FOL/IFOL.thy	Sun Nov 26 23:43:53 2006 +0100
@@ -7,7 +7,7 @@
 
 theory IFOL
 imports Pure
-uses ("IFOL_lemmas.ML") ("fologic.ML") ("hypsubstdata.ML") ("intprover.ML")
+uses ("fologic.ML") ("hypsubstdata.ML") ("intprover.ML")
 begin
 
 
@@ -55,22 +55,22 @@
   not_equal  (infixl "\<noteq>" 50)
 
 notation (xsymbols)
-  Not  ("\<not> _" [40] 40) and
-  "op &"  (infixr "\<and>" 35) and
-  "op |"  (infixr "\<or>" 30) and
-  All  (binder "\<forall>" 10) and
-  Ex  (binder "\<exists>" 10) and
-  Ex1  (binder "\<exists>!" 10) and
+  Not       ("\<not> _" [40] 40) and
+  "op &"    (infixr "\<and>" 35) and
+  "op |"    (infixr "\<or>" 30) and
+  All       (binder "\<forall>" 10) and
+  Ex        (binder "\<exists>" 10) and
+  Ex1       (binder "\<exists>!" 10) and
   "op -->"  (infixr "\<longrightarrow>" 25) and
   "op <->"  (infixr "\<longleftrightarrow>" 25)
 
 notation (HTML output)
-  Not  ("\<not> _" [40] 40) and
-  "op &"  (infixr "\<and>" 35) and
-  "op |"  (infixr "\<or>" 30) and
-  All  (binder "\<forall>" 10) and
-  Ex  (binder "\<exists>" 10) and
-  Ex1  (binder "\<exists>!" 10)
+  Not       ("\<not> _" [40] 40) and
+  "op &"    (infixr "\<and>" 35) and
+  "op |"    (infixr "\<or>" 30) and
+  All       (binder "\<forall>" 10) and
+  Ex        (binder "\<exists>" 10) and
+  Ex1       (binder "\<exists>!" 10)
 
 local
 
@@ -145,7 +145,471 @@
 
 subsection {* Lemmas and proof tools *}
 
-use "IFOL_lemmas.ML"
+lemma TrueI: True
+  unfolding True_def by (rule impI)
+
+
+(*** Sequent-style elimination rules for & --> and ALL ***)
+
+lemma conjE:
+  assumes major: "P & Q"
+    and r: "[| P; Q |] ==> R"
+  shows R
+  apply (rule r)
+   apply (rule major [THEN conjunct1])
+  apply (rule major [THEN conjunct2])
+  done
+
+lemma impE:
+  assumes major: "P --> Q"
+    and P
+  and r: "Q ==> R"
+  shows R
+  apply (rule r)
+  apply (rule major [THEN mp])
+  apply (rule `P`)
+  done
+
+lemma allE:
+  assumes major: "ALL x. P(x)"
+    and r: "P(x) ==> R"
+  shows R
+  apply (rule r)
+  apply (rule major [THEN spec])
+  done
+
+(*Duplicates the quantifier; for use with eresolve_tac*)
+lemma all_dupE:
+  assumes major: "ALL x. P(x)"
+    and r: "[| P(x); ALL x. P(x) |] ==> R"
+  shows R
+  apply (rule r)
+   apply (rule major [THEN spec])
+  apply (rule major)
+  done
+
+
+(*** Negation rules, which translate between ~P and P-->False ***)
+
+lemma notI: "(P ==> False) ==> ~P"
+  unfolding not_def by (erule impI)
+
+lemma notE: "[| ~P;  P |] ==> R"
+  unfolding not_def by (erule mp [THEN FalseE])
+
+lemma rev_notE: "[| P; ~P |] ==> R"
+  by (erule notE)
+
+(*This is useful with the special implication rules for each kind of P. *)
+lemma not_to_imp:
+  assumes "~P"
+    and r: "P --> False ==> Q"
+  shows Q
+  apply (rule r)
+  apply (rule impI)
+  apply (erule notE [OF `~P`])
+  done
+
+(* For substitution into an assumption P, reduce Q to P-->Q, substitute into
+   this implication, then apply impI to move P back into the assumptions.
+   To specify P use something like
+      eres_inst_tac [ ("P","ALL y. ?S(x,y)") ] rev_mp 1   *)
+lemma rev_mp: "[| P;  P --> Q |] ==> Q"
+  by (erule mp)
+
+(*Contrapositive of an inference rule*)
+lemma contrapos:
+  assumes major: "~Q"
+    and minor: "P ==> Q"
+  shows "~P"
+  apply (rule major [THEN notE, THEN notI])
+  apply (erule minor)
+  done
+
+
+(*** Modus Ponens Tactics ***)
+
+(*Finds P-->Q and P in the assumptions, replaces implication by Q *)
+ML {*
+  local
+    val notE = thm "notE"
+    val impE = thm "impE"
+  in
+    fun mp_tac i = eresolve_tac [notE,impE] i  THEN  assume_tac i
+    fun eq_mp_tac i = eresolve_tac [notE,impE] i  THEN  eq_assume_tac i
+  end
+*}
+
+
+(*** If-and-only-if ***)
+
+lemma iffI: "[| P ==> Q; Q ==> P |] ==> P<->Q"
+  apply (unfold iff_def)
+  apply (rule conjI)
+   apply (erule impI)
+  apply (erule impI)
+  done
+
+
+(*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *)
+lemma iffE:
+  assumes major: "P <-> Q"
+    and r: "P-->Q ==> Q-->P ==> R"
+  shows R
+  apply (insert major, unfold iff_def)
+  apply (erule conjE)
+  apply (erule r)
+  apply assumption
+  done
+
+(* Destruct rules for <-> similar to Modus Ponens *)
+
+lemma iffD1: "[| P <-> Q;  P |] ==> Q"
+  apply (unfold iff_def)
+  apply (erule conjunct1 [THEN mp])
+  apply assumption
+  done
+
+lemma iffD2: "[| P <-> Q;  Q |] ==> P"
+  apply (unfold iff_def)
+  apply (erule conjunct2 [THEN mp])
+  apply assumption
+  done
+
+lemma rev_iffD1: "[| P; P <-> Q |] ==> Q"
+  apply (erule iffD1)
+  apply assumption
+  done
+
+lemma rev_iffD2: "[| Q; P <-> Q |] ==> P"
+  apply (erule iffD2)
+  apply assumption
+  done
+
+lemma iff_refl: "P <-> P"
+  by (rule iffI)
+
+lemma iff_sym: "Q <-> P ==> P <-> Q"
+  apply (erule iffE)
+  apply (rule iffI)
+  apply (assumption | erule mp)+
+  done
+
+lemma iff_trans: "[| P <-> Q;  Q<-> R |] ==> P <-> R"
+  apply (rule iffI)
+  apply (assumption | erule iffE | erule (1) notE impE)+
+  done
+
+
+(*** Unique existence.  NOTE THAT the following 2 quantifications
+   EX!x such that [EX!y such that P(x,y)]     (sequential)
+   EX!x,y such that P(x,y)                    (simultaneous)
+ do NOT mean the same thing.  The parser treats EX!x y.P(x,y) as sequential.
+***)
+
+lemma ex1I:
+  assumes "P(a)"
+    and "!!x. P(x) ==> x=a"
+  shows "EX! x. P(x)"
+  apply (unfold ex1_def)
+  apply (assumption | rule assms exI conjI allI impI)+
+  done
+
+(*Sometimes easier to use: the premises have no shared variables.  Safe!*)
+lemma ex_ex1I:
+  assumes ex: "EX x. P(x)"
+    and eq: "!!x y. [| P(x); P(y) |] ==> x=y"
+  shows "EX! x. P(x)"
+  apply (rule ex [THEN exE])
+  apply (assumption | rule ex1I eq)+
+  done
+
+lemma ex1E:
+  assumes ex1: "EX! x. P(x)"
+    and r: "!!x. [| P(x);  ALL y. P(y) --> y=x |] ==> R"
+  shows R
+  apply (insert ex1, unfold ex1_def)
+  apply (assumption | erule exE conjE)+
+  done
+
+
+(*** <-> congruence rules for simplification ***)
+
+(*Use iffE on a premise.  For conj_cong, imp_cong, all_cong, ex_cong*)
+ML {*
+  local
+    val iffE = thm "iffE"
+    val mp = thm "mp"
+  in
+    fun iff_tac prems i =
+      resolve_tac (prems RL [iffE]) i THEN
+      REPEAT1 (eresolve_tac [asm_rl, mp] i)
+  end
+*}
+
+lemma conj_cong:
+  assumes "P <-> P'"
+    and "P' ==> Q <-> Q'"
+  shows "(P&Q) <-> (P'&Q')"
+  apply (insert assms)
+  apply (assumption | rule iffI conjI | erule iffE conjE mp |
+    tactic {* iff_tac (thms "assms") 1 *})+
+  done
+
+(*Reversed congruence rule!   Used in ZF/Order*)
+lemma conj_cong2:
+  assumes "P <-> P'"
+    and "P' ==> Q <-> Q'"
+  shows "(Q&P) <-> (Q'&P')"
+  apply (insert assms)
+  apply (assumption | rule iffI conjI | erule iffE conjE mp |
+    tactic {* iff_tac (thms "assms") 1 *})+
+  done
+
+lemma disj_cong:
+  assumes "P <-> P'" and "Q <-> Q'"
+  shows "(P|Q) <-> (P'|Q')"
+  apply (insert assms)
+  apply (erule iffE disjE disjI1 disjI2 | assumption | rule iffI | erule (1) notE impE)+
+  done
+
+lemma imp_cong:
+  assumes "P <-> P'"
+    and "P' ==> Q <-> Q'"
+  shows "(P-->Q) <-> (P'-->Q')"
+  apply (insert assms)
+  apply (assumption | rule iffI impI | erule iffE | erule (1) notE impE |
+    tactic {* iff_tac (thms "assms") 1 *})+
+  done
+
+lemma iff_cong: "[| P <-> P'; Q <-> Q' |] ==> (P<->Q) <-> (P'<->Q')"
+  apply (erule iffE | assumption | rule iffI | erule (1) notE impE)+
+  done
+
+lemma not_cong: "P <-> P' ==> ~P <-> ~P'"
+  apply (assumption | rule iffI notI | erule (1) notE impE | erule iffE notE)+
+  done
+
+lemma all_cong:
+  assumes "!!x. P(x) <-> Q(x)"
+  shows "(ALL x. P(x)) <-> (ALL x. Q(x))"
+  apply (assumption | rule iffI allI | erule (1) notE impE | erule allE |
+    tactic {* iff_tac (thms "assms") 1 *})+
+  done
+
+lemma ex_cong:
+  assumes "!!x. P(x) <-> Q(x)"
+  shows "(EX x. P(x)) <-> (EX x. Q(x))"
+  apply (erule exE | assumption | rule iffI exI | erule (1) notE impE |
+    tactic {* iff_tac (thms "assms") 1 *})+
+  done
+
+lemma ex1_cong:
+  assumes "!!x. P(x) <-> Q(x)"
+  shows "(EX! x. P(x)) <-> (EX! x. Q(x))"
+  apply (erule ex1E spec [THEN mp] | assumption | rule iffI ex1I | erule (1) notE impE |
+    tactic {* iff_tac (thms "assms") 1 *})+
+  done
+
+(*** Equality rules ***)
+
+lemma sym: "a=b ==> b=a"
+  apply (erule subst)
+  apply (rule refl)
+  done
+
+lemma trans: "[| a=b;  b=c |] ==> a=c"
+  apply (erule subst, assumption)
+  done
+
+(**  **)
+lemma not_sym: "b ~= a ==> a ~= b"
+  apply (erule contrapos)
+  apply (erule sym)
+  done
+  
+(* Two theorms for rewriting only one instance of a definition:
+   the first for definitions of formulae and the second for terms *)
+
+lemma def_imp_iff: "(A == B) ==> A <-> B"
+  apply unfold
+  apply (rule iff_refl)
+  done
+
+lemma meta_eq_to_obj_eq: "(A == B) ==> A = B"
+  apply unfold
+  apply (rule refl)
+  done
+
+lemma meta_eq_to_iff: "x==y ==> x<->y"
+  by unfold (rule iff_refl)
+
+(*substitution*)
+lemma ssubst: "[| b = a; P(a) |] ==> P(b)"
+  apply (drule sym)
+  apply (erule (1) subst)
+  done
+
+(*A special case of ex1E that would otherwise need quantifier expansion*)
+lemma ex1_equalsE:
+    "[| EX! x. P(x);  P(a);  P(b) |] ==> a=b"
+  apply (erule ex1E)
+  apply (rule trans)
+   apply (rule_tac [2] sym)
+   apply (assumption | erule spec [THEN mp])+
+  done
+
+(** Polymorphic congruence rules **)
+
+lemma subst_context: "[| a=b |]  ==>  t(a)=t(b)"
+  apply (erule ssubst)
+  apply (rule refl)
+  done
+
+lemma subst_context2: "[| a=b;  c=d |]  ==>  t(a,c)=t(b,d)"
+  apply (erule ssubst)+
+  apply (rule refl)
+  done
+
+lemma subst_context3: "[| a=b;  c=d;  e=f |]  ==>  t(a,c,e)=t(b,d,f)"
+  apply (erule ssubst)+
+  apply (rule refl)
+  done
+
+(*Useful with eresolve_tac for proving equalties from known equalities.
+        a = b
+        |   |
+        c = d   *)
+lemma box_equals: "[| a=b;  a=c;  b=d |] ==> c=d"
+  apply (rule trans)
+   apply (rule trans)
+    apply (rule sym)
+    apply assumption+
+  done
+
+(*Dual of box_equals: for proving equalities backwards*)
+lemma simp_equals: "[| a=c;  b=d;  c=d |] ==> a=b"
+  apply (rule trans)
+   apply (rule trans)
+    apply assumption+
+  apply (erule sym)
+  done
+
+(** Congruence rules for predicate letters **)
+
+lemma pred1_cong: "a=a' ==> P(a) <-> P(a')"
+  apply (rule iffI)
+   apply (erule (1) subst)
+  apply (erule (1) ssubst)
+  done
+
+lemma pred2_cong: "[| a=a';  b=b' |] ==> P(a,b) <-> P(a',b')"
+  apply (rule iffI)
+   apply (erule subst)+
+   apply assumption
+  apply (erule ssubst)+
+  apply assumption
+  done
+
+lemma pred3_cong: "[| a=a';  b=b';  c=c' |] ==> P(a,b,c) <-> P(a',b',c')"
+  apply (rule iffI)
+   apply (erule subst)+
+   apply assumption
+  apply (erule ssubst)+
+  apply assumption
+  done
+
+(*special cases for free variables P, Q, R, S -- up to 3 arguments*)
+
+ML {*
+bind_thms ("pred_congs",
+  List.concat (map (fn c => 
+               map (fn th => read_instantiate [("P",c)] th)
+                   [thm "pred1_cong", thm "pred2_cong", thm "pred3_cong"])
+               (explode"PQRS")))
+*}
+
+(*special case for the equality predicate!*)
+lemma eq_cong: "[| a = a'; b = b' |] ==> a = b <-> a' = b'"
+  apply (erule (1) pred2_cong)
+  done
+
+
+(*** Simplifications of assumed implications.
+     Roy Dyckhoff has proved that conj_impE, disj_impE, and imp_impE
+     used with mp_tac (restricted to atomic formulae) is COMPLETE for 
+     intuitionistic propositional logic.  See
+   R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic
+    (preprint, University of St Andrews, 1991)  ***)
+
+lemma conj_impE:
+  assumes major: "(P&Q)-->S"
+    and r: "P-->(Q-->S) ==> R"
+  shows R
+  by (assumption | rule conjI impI major [THEN mp] r)+
+
+lemma disj_impE:
+  assumes major: "(P|Q)-->S"
+    and r: "[| P-->S; Q-->S |] ==> R"
+  shows R
+  by (assumption | rule disjI1 disjI2 impI major [THEN mp] r)+
+
+(*Simplifies the implication.  Classical version is stronger. 
+  Still UNSAFE since Q must be provable -- backtracking needed.  *)
+lemma imp_impE:
+  assumes major: "(P-->Q)-->S"
+    and r1: "[| P; Q-->S |] ==> Q"
+    and r2: "S ==> R"
+  shows R
+  by (assumption | rule impI major [THEN mp] r1 r2)+
+
+(*Simplifies the implication.  Classical version is stronger. 
+  Still UNSAFE since ~P must be provable -- backtracking needed.  *)
+lemma not_impE:
+  assumes major: "~P --> S"
+    and r1: "P ==> False"
+    and r2: "S ==> R"
+  shows R
+  apply (assumption | rule notI impI major [THEN mp] r1 r2)+
+  done
+
+(*Simplifies the implication.   UNSAFE.  *)
+lemma iff_impE:
+  assumes major: "(P<->Q)-->S"
+    and r1: "[| P; Q-->S |] ==> Q"
+    and r2: "[| Q; P-->S |] ==> P"
+    and r3: "S ==> R"
+  shows R
+  apply (assumption | rule iffI impI major [THEN mp] r1 r2 r3)+
+  done
+
+(*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*)
+lemma all_impE:
+  assumes major: "(ALL x. P(x))-->S"
+    and r1: "!!x. P(x)"
+    and r2: "S ==> R"
+  shows R
+  apply (assumption | rule allI impI major [THEN mp] r1 r2)+
+  done
+
+(*Unsafe: (EX x.P(x))-->S  is equivalent to  ALL x.P(x)-->S.  *)
+lemma ex_impE:
+  assumes major: "(EX x. P(x))-->S"
+    and r: "P(x)-->S ==> R"
+  shows R
+  apply (assumption | rule exI impI major [THEN mp] r)+
+  done
+
+(*** Courtesy of Krzysztof Grabczewski ***)
+
+lemma disj_imp_disj:
+  assumes major: "P|Q"
+    and "P==>R" and "Q==>S"
+  shows "R|S"
+  apply (rule disjE [OF major])
+  apply (rule disjI1) apply assumption
+  apply (rule disjI2) apply assumption
+  done
 
 ML {*
 structure ProjectRule = ProjectRuleFun
@@ -157,6 +621,9 @@
 *}
 
 use "fologic.ML"
+
+lemma thin_refl: "!!X. [|x=x; PROP W|] ==> PROP W" .
+
 use "hypsubstdata.ML"
 setup hypsubst_setup
 use "intprover.ML"
@@ -314,16 +781,51 @@
 
 
 lemma LetI: 
-    assumes prem: "(!!x. x=t ==> P(u(x)))"
-    shows "P(let x=t in u(x))"
-apply (unfold Let_def)
-apply (rule refl [THEN prem])
-done
+  assumes "!!x. x=t ==> P(u(x))"
+  shows "P(let x=t in u(x))"
+  apply (unfold Let_def)
+  apply (rule refl [THEN assms])
+  done
+
+
+subsection {* ML bindings *}
 
-ML
-{*
-val Let_def = thm "Let_def";
-val LetI = thm "LetI";
+ML {*
+val refl = thm "refl"
+val trans = thm "trans"
+val sym = thm "sym"
+val subst = thm "subst"
+val ssubst = thm "ssubst"
+val conjI = thm "conjI"
+val conjE = thm "conjE"
+val conjunct1 = thm "conjunct1"
+val conjunct2 = thm "conjunct2"
+val disjI1 = thm "disjI1"
+val disjI2 = thm "disjI2"
+val disjE = thm "disjE"
+val impI = thm "impI"
+val impE = thm "impE"
+val mp = thm "mp"
+val rev_mp = thm "rev_mp"
+val TrueI = thm "TrueI"
+val FalseE = thm "FalseE"
+val iff_refl = thm "iff_refl"
+val iff_trans = thm "iff_trans"
+val iffI = thm "iffI"
+val iffE = thm "iffE"
+val iffD1 = thm "iffD1"
+val iffD2 = thm "iffD2"
+val notI = thm "notI"
+val notE = thm "notE"
+val allI = thm "allI"
+val allE = thm "allE"
+val spec = thm "spec"
+val exI = thm "exI"
+val exE = thm "exE"
+val eq_reflection = thm "eq_reflection"
+val iff_reflection = thm "iff_reflection"
+val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq"
+val meta_eq_to_iff = thm "meta_eq_to_iff"
 *}
 
 end