src/FOL/IFOL.thy
author krauss
Tue Apr 08 18:30:40 2008 +0200 (2008-04-08)
changeset 26580 c3e597a476fd
parent 26286 3ff5d257f175
child 26956 1309a6a0a29f
permissions -rw-r--r--
Generic conversion and tactic "atomize_elim" to convert elimination rules
to the object logic
     1 (*  Title:      FOL/IFOL.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson and Markus Wenzel
     4 *)
     5 
     6 header {* Intuitionistic first-order logic *}
     7 
     8 theory IFOL
     9 imports Pure
    10 uses
    11   "~~/src/Provers/splitter.ML"
    12   "~~/src/Provers/hypsubst.ML"
    13   "~~/src/Tools/IsaPlanner/zipper.ML"
    14   "~~/src/Tools/IsaPlanner/isand.ML"
    15   "~~/src/Tools/IsaPlanner/rw_tools.ML"
    16   "~~/src/Tools/IsaPlanner/rw_inst.ML"
    17   "~~/src/Provers/eqsubst.ML"
    18   "~~/src/Provers/quantifier1.ML"
    19   "~~/src/Provers/project_rule.ML"
    20   "~~/src/Tools/atomize_elim.ML"
    21   ("fologic.ML")
    22   ("hypsubstdata.ML")
    23   ("intprover.ML")
    24 begin
    25 
    26 
    27 subsection {* Syntax and axiomatic basis *}
    28 
    29 global
    30 
    31 classes "term"
    32 defaultsort "term"
    33 
    34 typedecl o
    35 
    36 judgment
    37   Trueprop      :: "o => prop"                  ("(_)" 5)
    38 
    39 consts
    40   True          :: o
    41   False         :: o
    42 
    43   (* Connectives *)
    44 
    45   "op ="        :: "['a, 'a] => o"              (infixl "=" 50)
    46 
    47   Not           :: "o => o"                     ("~ _" [40] 40)
    48   "op &"        :: "[o, o] => o"                (infixr "&" 35)
    49   "op |"        :: "[o, o] => o"                (infixr "|" 30)
    50   "op -->"      :: "[o, o] => o"                (infixr "-->" 25)
    51   "op <->"      :: "[o, o] => o"                (infixr "<->" 25)
    52 
    53   (* Quantifiers *)
    54 
    55   All           :: "('a => o) => o"             (binder "ALL " 10)
    56   Ex            :: "('a => o) => o"             (binder "EX " 10)
    57   Ex1           :: "('a => o) => o"             (binder "EX! " 10)
    58 
    59 
    60 abbreviation
    61   not_equal :: "['a, 'a] => o"  (infixl "~=" 50) where
    62   "x ~= y == ~ (x = y)"
    63 
    64 notation (xsymbols)
    65   not_equal  (infixl "\<noteq>" 50)
    66 
    67 notation (HTML output)
    68   not_equal  (infixl "\<noteq>" 50)
    69 
    70 notation (xsymbols)
    71   Not       ("\<not> _" [40] 40) and
    72   "op &"    (infixr "\<and>" 35) and
    73   "op |"    (infixr "\<or>" 30) and
    74   All       (binder "\<forall>" 10) and
    75   Ex        (binder "\<exists>" 10) and
    76   Ex1       (binder "\<exists>!" 10) and
    77   "op -->"  (infixr "\<longrightarrow>" 25) and
    78   "op <->"  (infixr "\<longleftrightarrow>" 25)
    79 
    80 notation (HTML output)
    81   Not       ("\<not> _" [40] 40) and
    82   "op &"    (infixr "\<and>" 35) and
    83   "op |"    (infixr "\<or>" 30) and
    84   All       (binder "\<forall>" 10) and
    85   Ex        (binder "\<exists>" 10) and
    86   Ex1       (binder "\<exists>!" 10)
    87 
    88 local
    89 
    90 finalconsts
    91   False All Ex
    92   "op ="
    93   "op &"
    94   "op |"
    95   "op -->"
    96 
    97 axioms
    98 
    99   (* Equality *)
   100 
   101   refl:         "a=a"
   102 
   103   (* Propositional logic *)
   104 
   105   conjI:        "[| P;  Q |] ==> P&Q"
   106   conjunct1:    "P&Q ==> P"
   107   conjunct2:    "P&Q ==> Q"
   108 
   109   disjI1:       "P ==> P|Q"
   110   disjI2:       "Q ==> P|Q"
   111   disjE:        "[| P|Q;  P ==> R;  Q ==> R |] ==> R"
   112 
   113   impI:         "(P ==> Q) ==> P-->Q"
   114   mp:           "[| P-->Q;  P |] ==> Q"
   115 
   116   FalseE:       "False ==> P"
   117 
   118   (* Quantifiers *)
   119 
   120   allI:         "(!!x. P(x)) ==> (ALL x. P(x))"
   121   spec:         "(ALL x. P(x)) ==> P(x)"
   122 
   123   exI:          "P(x) ==> (EX x. P(x))"
   124   exE:          "[| EX x. P(x);  !!x. P(x) ==> R |] ==> R"
   125 
   126   (* Reflection *)
   127 
   128   eq_reflection:  "(x=y)   ==> (x==y)"
   129   iff_reflection: "(P<->Q) ==> (P==Q)"
   130 
   131 
   132 lemmas strip = impI allI
   133 
   134 
   135 text{*Thanks to Stephan Merz*}
   136 theorem subst:
   137   assumes eq: "a = b" and p: "P(a)"
   138   shows "P(b)"
   139 proof -
   140   from eq have meta: "a \<equiv> b"
   141     by (rule eq_reflection)
   142   from p show ?thesis
   143     by (unfold meta)
   144 qed
   145 
   146 
   147 defs
   148   (* Definitions *)
   149 
   150   True_def:     "True  == False-->False"
   151   not_def:      "~P    == P-->False"
   152   iff_def:      "P<->Q == (P-->Q) & (Q-->P)"
   153 
   154   (* Unique existence *)
   155 
   156   ex1_def:      "Ex1(P) == EX x. P(x) & (ALL y. P(y) --> y=x)"
   157 
   158 
   159 subsection {* Lemmas and proof tools *}
   160 
   161 lemma TrueI: True
   162   unfolding True_def by (rule impI)
   163 
   164 
   165 (*** Sequent-style elimination rules for & --> and ALL ***)
   166 
   167 lemma conjE:
   168   assumes major: "P & Q"
   169     and r: "[| P; Q |] ==> R"
   170   shows R
   171   apply (rule r)
   172    apply (rule major [THEN conjunct1])
   173   apply (rule major [THEN conjunct2])
   174   done
   175 
   176 lemma impE:
   177   assumes major: "P --> Q"
   178     and P
   179   and r: "Q ==> R"
   180   shows R
   181   apply (rule r)
   182   apply (rule major [THEN mp])
   183   apply (rule `P`)
   184   done
   185 
   186 lemma allE:
   187   assumes major: "ALL x. P(x)"
   188     and r: "P(x) ==> R"
   189   shows R
   190   apply (rule r)
   191   apply (rule major [THEN spec])
   192   done
   193 
   194 (*Duplicates the quantifier; for use with eresolve_tac*)
   195 lemma all_dupE:
   196   assumes major: "ALL x. P(x)"
   197     and r: "[| P(x); ALL x. P(x) |] ==> R"
   198   shows R
   199   apply (rule r)
   200    apply (rule major [THEN spec])
   201   apply (rule major)
   202   done
   203 
   204 
   205 (*** Negation rules, which translate between ~P and P-->False ***)
   206 
   207 lemma notI: "(P ==> False) ==> ~P"
   208   unfolding not_def by (erule impI)
   209 
   210 lemma notE: "[| ~P;  P |] ==> R"
   211   unfolding not_def by (erule mp [THEN FalseE])
   212 
   213 lemma rev_notE: "[| P; ~P |] ==> R"
   214   by (erule notE)
   215 
   216 (*This is useful with the special implication rules for each kind of P. *)
   217 lemma not_to_imp:
   218   assumes "~P"
   219     and r: "P --> False ==> Q"
   220   shows Q
   221   apply (rule r)
   222   apply (rule impI)
   223   apply (erule notE [OF `~P`])
   224   done
   225 
   226 (* For substitution into an assumption P, reduce Q to P-->Q, substitute into
   227    this implication, then apply impI to move P back into the assumptions.
   228    To specify P use something like
   229       eres_inst_tac [ ("P","ALL y. ?S(x,y)") ] rev_mp 1   *)
   230 lemma rev_mp: "[| P;  P --> Q |] ==> Q"
   231   by (erule mp)
   232 
   233 (*Contrapositive of an inference rule*)
   234 lemma contrapos:
   235   assumes major: "~Q"
   236     and minor: "P ==> Q"
   237   shows "~P"
   238   apply (rule major [THEN notE, THEN notI])
   239   apply (erule minor)
   240   done
   241 
   242 
   243 (*** Modus Ponens Tactics ***)
   244 
   245 (*Finds P-->Q and P in the assumptions, replaces implication by Q *)
   246 ML {*
   247   fun mp_tac i = eresolve_tac [@{thm notE}, @{thm impE}] i  THEN  assume_tac i
   248   fun eq_mp_tac i = eresolve_tac [@{thm notE}, @{thm impE}] i  THEN  eq_assume_tac i
   249 *}
   250 
   251 
   252 (*** If-and-only-if ***)
   253 
   254 lemma iffI: "[| P ==> Q; Q ==> P |] ==> P<->Q"
   255   apply (unfold iff_def)
   256   apply (rule conjI)
   257    apply (erule impI)
   258   apply (erule impI)
   259   done
   260 
   261 
   262 (*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *)
   263 lemma iffE:
   264   assumes major: "P <-> Q"
   265     and r: "P-->Q ==> Q-->P ==> R"
   266   shows R
   267   apply (insert major, unfold iff_def)
   268   apply (erule conjE)
   269   apply (erule r)
   270   apply assumption
   271   done
   272 
   273 (* Destruct rules for <-> similar to Modus Ponens *)
   274 
   275 lemma iffD1: "[| P <-> Q;  P |] ==> Q"
   276   apply (unfold iff_def)
   277   apply (erule conjunct1 [THEN mp])
   278   apply assumption
   279   done
   280 
   281 lemma iffD2: "[| P <-> Q;  Q |] ==> P"
   282   apply (unfold iff_def)
   283   apply (erule conjunct2 [THEN mp])
   284   apply assumption
   285   done
   286 
   287 lemma rev_iffD1: "[| P; P <-> Q |] ==> Q"
   288   apply (erule iffD1)
   289   apply assumption
   290   done
   291 
   292 lemma rev_iffD2: "[| Q; P <-> Q |] ==> P"
   293   apply (erule iffD2)
   294   apply assumption
   295   done
   296 
   297 lemma iff_refl: "P <-> P"
   298   by (rule iffI)
   299 
   300 lemma iff_sym: "Q <-> P ==> P <-> Q"
   301   apply (erule iffE)
   302   apply (rule iffI)
   303   apply (assumption | erule mp)+
   304   done
   305 
   306 lemma iff_trans: "[| P <-> Q;  Q<-> R |] ==> P <-> R"
   307   apply (rule iffI)
   308   apply (assumption | erule iffE | erule (1) notE impE)+
   309   done
   310 
   311 
   312 (*** Unique existence.  NOTE THAT the following 2 quantifications
   313    EX!x such that [EX!y such that P(x,y)]     (sequential)
   314    EX!x,y such that P(x,y)                    (simultaneous)
   315  do NOT mean the same thing.  The parser treats EX!x y.P(x,y) as sequential.
   316 ***)
   317 
   318 lemma ex1I:
   319   "P(a) \<Longrightarrow> (!!x. P(x) ==> x=a) \<Longrightarrow> EX! x. P(x)"
   320   apply (unfold ex1_def)
   321   apply (assumption | rule exI conjI allI impI)+
   322   done
   323 
   324 (*Sometimes easier to use: the premises have no shared variables.  Safe!*)
   325 lemma ex_ex1I:
   326   "EX x. P(x) \<Longrightarrow> (!!x y. [| P(x); P(y) |] ==> x=y) \<Longrightarrow> EX! x. P(x)"
   327   apply (erule exE)
   328   apply (rule ex1I)
   329    apply assumption
   330   apply assumption
   331   done
   332 
   333 lemma ex1E:
   334   "EX! x. P(x) \<Longrightarrow> (!!x. [| P(x);  ALL y. P(y) --> y=x |] ==> R) \<Longrightarrow> R"
   335   apply (unfold ex1_def)
   336   apply (assumption | erule exE conjE)+
   337   done
   338 
   339 
   340 (*** <-> congruence rules for simplification ***)
   341 
   342 (*Use iffE on a premise.  For conj_cong, imp_cong, all_cong, ex_cong*)
   343 ML {*
   344   fun iff_tac prems i =
   345     resolve_tac (prems RL @{thms iffE}) i THEN
   346     REPEAT1 (eresolve_tac [@{thm asm_rl}, @{thm mp}] i)
   347 *}
   348 
   349 lemma conj_cong:
   350   assumes "P <-> P'"
   351     and "P' ==> Q <-> Q'"
   352   shows "(P&Q) <-> (P'&Q')"
   353   apply (insert assms)
   354   apply (assumption | rule iffI conjI | erule iffE conjE mp |
   355     tactic {* iff_tac (thms "assms") 1 *})+
   356   done
   357 
   358 (*Reversed congruence rule!   Used in ZF/Order*)
   359 lemma conj_cong2:
   360   assumes "P <-> P'"
   361     and "P' ==> Q <-> Q'"
   362   shows "(Q&P) <-> (Q'&P')"
   363   apply (insert assms)
   364   apply (assumption | rule iffI conjI | erule iffE conjE mp |
   365     tactic {* iff_tac (thms "assms") 1 *})+
   366   done
   367 
   368 lemma disj_cong:
   369   assumes "P <-> P'" and "Q <-> Q'"
   370   shows "(P|Q) <-> (P'|Q')"
   371   apply (insert assms)
   372   apply (erule iffE disjE disjI1 disjI2 | assumption | rule iffI | erule (1) notE impE)+
   373   done
   374 
   375 lemma imp_cong:
   376   assumes "P <-> P'"
   377     and "P' ==> Q <-> Q'"
   378   shows "(P-->Q) <-> (P'-->Q')"
   379   apply (insert assms)
   380   apply (assumption | rule iffI impI | erule iffE | erule (1) notE impE |
   381     tactic {* iff_tac (thms "assms") 1 *})+
   382   done
   383 
   384 lemma iff_cong: "[| P <-> P'; Q <-> Q' |] ==> (P<->Q) <-> (P'<->Q')"
   385   apply (erule iffE | assumption | rule iffI | erule (1) notE impE)+
   386   done
   387 
   388 lemma not_cong: "P <-> P' ==> ~P <-> ~P'"
   389   apply (assumption | rule iffI notI | erule (1) notE impE | erule iffE notE)+
   390   done
   391 
   392 lemma all_cong:
   393   assumes "!!x. P(x) <-> Q(x)"
   394   shows "(ALL x. P(x)) <-> (ALL x. Q(x))"
   395   apply (assumption | rule iffI allI | erule (1) notE impE | erule allE |
   396     tactic {* iff_tac (thms "assms") 1 *})+
   397   done
   398 
   399 lemma ex_cong:
   400   assumes "!!x. P(x) <-> Q(x)"
   401   shows "(EX x. P(x)) <-> (EX x. Q(x))"
   402   apply (erule exE | assumption | rule iffI exI | erule (1) notE impE |
   403     tactic {* iff_tac (thms "assms") 1 *})+
   404   done
   405 
   406 lemma ex1_cong:
   407   assumes "!!x. P(x) <-> Q(x)"
   408   shows "(EX! x. P(x)) <-> (EX! x. Q(x))"
   409   apply (erule ex1E spec [THEN mp] | assumption | rule iffI ex1I | erule (1) notE impE |
   410     tactic {* iff_tac (thms "assms") 1 *})+
   411   done
   412 
   413 (*** Equality rules ***)
   414 
   415 lemma sym: "a=b ==> b=a"
   416   apply (erule subst)
   417   apply (rule refl)
   418   done
   419 
   420 lemma trans: "[| a=b;  b=c |] ==> a=c"
   421   apply (erule subst, assumption)
   422   done
   423 
   424 (**  **)
   425 lemma not_sym: "b ~= a ==> a ~= b"
   426   apply (erule contrapos)
   427   apply (erule sym)
   428   done
   429   
   430 (* Two theorms for rewriting only one instance of a definition:
   431    the first for definitions of formulae and the second for terms *)
   432 
   433 lemma def_imp_iff: "(A == B) ==> A <-> B"
   434   apply unfold
   435   apply (rule iff_refl)
   436   done
   437 
   438 lemma meta_eq_to_obj_eq: "(A == B) ==> A = B"
   439   apply unfold
   440   apply (rule refl)
   441   done
   442 
   443 lemma meta_eq_to_iff: "x==y ==> x<->y"
   444   by unfold (rule iff_refl)
   445 
   446 (*substitution*)
   447 lemma ssubst: "[| b = a; P(a) |] ==> P(b)"
   448   apply (drule sym)
   449   apply (erule (1) subst)
   450   done
   451 
   452 (*A special case of ex1E that would otherwise need quantifier expansion*)
   453 lemma ex1_equalsE:
   454     "[| EX! x. P(x);  P(a);  P(b) |] ==> a=b"
   455   apply (erule ex1E)
   456   apply (rule trans)
   457    apply (rule_tac [2] sym)
   458    apply (assumption | erule spec [THEN mp])+
   459   done
   460 
   461 (** Polymorphic congruence rules **)
   462 
   463 lemma subst_context: "[| a=b |]  ==>  t(a)=t(b)"
   464   apply (erule ssubst)
   465   apply (rule refl)
   466   done
   467 
   468 lemma subst_context2: "[| a=b;  c=d |]  ==>  t(a,c)=t(b,d)"
   469   apply (erule ssubst)+
   470   apply (rule refl)
   471   done
   472 
   473 lemma subst_context3: "[| a=b;  c=d;  e=f |]  ==>  t(a,c,e)=t(b,d,f)"
   474   apply (erule ssubst)+
   475   apply (rule refl)
   476   done
   477 
   478 (*Useful with eresolve_tac for proving equalties from known equalities.
   479         a = b
   480         |   |
   481         c = d   *)
   482 lemma box_equals: "[| a=b;  a=c;  b=d |] ==> c=d"
   483   apply (rule trans)
   484    apply (rule trans)
   485     apply (rule sym)
   486     apply assumption+
   487   done
   488 
   489 (*Dual of box_equals: for proving equalities backwards*)
   490 lemma simp_equals: "[| a=c;  b=d;  c=d |] ==> a=b"
   491   apply (rule trans)
   492    apply (rule trans)
   493     apply assumption+
   494   apply (erule sym)
   495   done
   496 
   497 (** Congruence rules for predicate letters **)
   498 
   499 lemma pred1_cong: "a=a' ==> P(a) <-> P(a')"
   500   apply (rule iffI)
   501    apply (erule (1) subst)
   502   apply (erule (1) ssubst)
   503   done
   504 
   505 lemma pred2_cong: "[| a=a';  b=b' |] ==> P(a,b) <-> P(a',b')"
   506   apply (rule iffI)
   507    apply (erule subst)+
   508    apply assumption
   509   apply (erule ssubst)+
   510   apply assumption
   511   done
   512 
   513 lemma pred3_cong: "[| a=a';  b=b';  c=c' |] ==> P(a,b,c) <-> P(a',b',c')"
   514   apply (rule iffI)
   515    apply (erule subst)+
   516    apply assumption
   517   apply (erule ssubst)+
   518   apply assumption
   519   done
   520 
   521 (*special cases for free variables P, Q, R, S -- up to 3 arguments*)
   522 
   523 ML {*
   524 bind_thms ("pred_congs",
   525   List.concat (map (fn c => 
   526                map (fn th => read_instantiate [("P",c)] th)
   527                    [@{thm pred1_cong}, @{thm pred2_cong}, @{thm pred3_cong}])
   528                (explode"PQRS")))
   529 *}
   530 
   531 (*special case for the equality predicate!*)
   532 lemma eq_cong: "[| a = a'; b = b' |] ==> a = b <-> a' = b'"
   533   apply (erule (1) pred2_cong)
   534   done
   535 
   536 
   537 (*** Simplifications of assumed implications.
   538      Roy Dyckhoff has proved that conj_impE, disj_impE, and imp_impE
   539      used with mp_tac (restricted to atomic formulae) is COMPLETE for 
   540      intuitionistic propositional logic.  See
   541    R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic
   542     (preprint, University of St Andrews, 1991)  ***)
   543 
   544 lemma conj_impE:
   545   assumes major: "(P&Q)-->S"
   546     and r: "P-->(Q-->S) ==> R"
   547   shows R
   548   by (assumption | rule conjI impI major [THEN mp] r)+
   549 
   550 lemma disj_impE:
   551   assumes major: "(P|Q)-->S"
   552     and r: "[| P-->S; Q-->S |] ==> R"
   553   shows R
   554   by (assumption | rule disjI1 disjI2 impI major [THEN mp] r)+
   555 
   556 (*Simplifies the implication.  Classical version is stronger. 
   557   Still UNSAFE since Q must be provable -- backtracking needed.  *)
   558 lemma imp_impE:
   559   assumes major: "(P-->Q)-->S"
   560     and r1: "[| P; Q-->S |] ==> Q"
   561     and r2: "S ==> R"
   562   shows R
   563   by (assumption | rule impI major [THEN mp] r1 r2)+
   564 
   565 (*Simplifies the implication.  Classical version is stronger. 
   566   Still UNSAFE since ~P must be provable -- backtracking needed.  *)
   567 lemma not_impE:
   568   "~P --> S \<Longrightarrow> (P ==> False) \<Longrightarrow> (S ==> R) \<Longrightarrow> R"
   569   apply (drule mp)
   570    apply (rule notI)
   571    apply assumption
   572   apply assumption
   573   done
   574 
   575 (*Simplifies the implication.   UNSAFE.  *)
   576 lemma iff_impE:
   577   assumes major: "(P<->Q)-->S"
   578     and r1: "[| P; Q-->S |] ==> Q"
   579     and r2: "[| Q; P-->S |] ==> P"
   580     and r3: "S ==> R"
   581   shows R
   582   apply (assumption | rule iffI impI major [THEN mp] r1 r2 r3)+
   583   done
   584 
   585 (*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*)
   586 lemma all_impE:
   587   assumes major: "(ALL x. P(x))-->S"
   588     and r1: "!!x. P(x)"
   589     and r2: "S ==> R"
   590   shows R
   591   apply (rule allI impI major [THEN mp] r1 r2)+
   592   done
   593 
   594 (*Unsafe: (EX x.P(x))-->S  is equivalent to  ALL x.P(x)-->S.  *)
   595 lemma ex_impE:
   596   assumes major: "(EX x. P(x))-->S"
   597     and r: "P(x)-->S ==> R"
   598   shows R
   599   apply (assumption | rule exI impI major [THEN mp] r)+
   600   done
   601 
   602 (*** Courtesy of Krzysztof Grabczewski ***)
   603 
   604 lemma disj_imp_disj:
   605   "P|Q \<Longrightarrow> (P==>R) \<Longrightarrow> (Q==>S) \<Longrightarrow> R|S"
   606   apply (erule disjE)
   607   apply (rule disjI1) apply assumption
   608   apply (rule disjI2) apply assumption
   609   done
   610 
   611 ML {*
   612 structure ProjectRule = ProjectRuleFun
   613 (struct
   614   val conjunct1 = @{thm conjunct1}
   615   val conjunct2 = @{thm conjunct2}
   616   val mp = @{thm mp}
   617 end)
   618 *}
   619 
   620 use "fologic.ML"
   621 
   622 lemma thin_refl: "!!X. [|x=x; PROP W|] ==> PROP W" .
   623 
   624 use "hypsubstdata.ML"
   625 setup hypsubst_setup
   626 use "intprover.ML"
   627 
   628 
   629 subsection {* Intuitionistic Reasoning *}
   630 
   631 lemma impE':
   632   assumes 1: "P --> Q"
   633     and 2: "Q ==> R"
   634     and 3: "P --> Q ==> P"
   635   shows R
   636 proof -
   637   from 3 and 1 have P .
   638   with 1 have Q by (rule impE)
   639   with 2 show R .
   640 qed
   641 
   642 lemma allE':
   643   assumes 1: "ALL x. P(x)"
   644     and 2: "P(x) ==> ALL x. P(x) ==> Q"
   645   shows Q
   646 proof -
   647   from 1 have "P(x)" by (rule spec)
   648   from this and 1 show Q by (rule 2)
   649 qed
   650 
   651 lemma notE':
   652   assumes 1: "~ P"
   653     and 2: "~ P ==> P"
   654   shows R
   655 proof -
   656   from 2 and 1 have P .
   657   with 1 show R by (rule notE)
   658 qed
   659 
   660 lemmas [Pure.elim!] = disjE iffE FalseE conjE exE
   661   and [Pure.intro!] = iffI conjI impI TrueI notI allI refl
   662   and [Pure.elim 2] = allE notE' impE'
   663   and [Pure.intro] = exI disjI2 disjI1
   664 
   665 setup {* ContextRules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac) *}
   666 
   667 
   668 lemma iff_not_sym: "~ (Q <-> P) ==> ~ (P <-> Q)"
   669   by iprover
   670 
   671 lemmas [sym] = sym iff_sym not_sym iff_not_sym
   672   and [Pure.elim?] = iffD1 iffD2 impE
   673 
   674 
   675 lemma eq_commute: "a=b <-> b=a"
   676 apply (rule iffI) 
   677 apply (erule sym)+
   678 done
   679 
   680 
   681 subsection {* Atomizing meta-level rules *}
   682 
   683 lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))"
   684 proof
   685   assume "!!x. P(x)"
   686   then show "ALL x. P(x)" ..
   687 next
   688   assume "ALL x. P(x)"
   689   then show "!!x. P(x)" ..
   690 qed
   691 
   692 lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A --> B)"
   693 proof
   694   assume "A ==> B"
   695   then show "A --> B" ..
   696 next
   697   assume "A --> B" and A
   698   then show B by (rule mp)
   699 qed
   700 
   701 lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)"
   702 proof
   703   assume "x == y"
   704   show "x = y" unfolding `x == y` by (rule refl)
   705 next
   706   assume "x = y"
   707   then show "x == y" by (rule eq_reflection)
   708 qed
   709 
   710 lemma atomize_iff [atomize]: "(A == B) == Trueprop (A <-> B)"
   711 proof
   712   assume "A == B"
   713   show "A <-> B" unfolding `A == B` by (rule iff_refl)
   714 next
   715   assume "A <-> B"
   716   then show "A == B" by (rule iff_reflection)
   717 qed
   718 
   719 lemma atomize_conj [atomize]:
   720   includes meta_conjunction_syntax
   721   shows "(A && B) == Trueprop (A & B)"
   722 proof
   723   assume conj: "A && B"
   724   show "A & B"
   725   proof (rule conjI)
   726     from conj show A by (rule conjunctionD1)
   727     from conj show B by (rule conjunctionD2)
   728   qed
   729 next
   730   assume conj: "A & B"
   731   show "A && B"
   732   proof -
   733     from conj show A ..
   734     from conj show B ..
   735   qed
   736 qed
   737 
   738 lemmas [symmetric, rulify] = atomize_all atomize_imp
   739   and [symmetric, defn] = atomize_all atomize_imp atomize_eq atomize_iff
   740 
   741 
   742 subsection {* Atomizing elimination rules *}
   743 
   744 setup AtomizeElim.setup
   745 
   746 lemma atomize_exL[atomize_elim]: "(!!x. P(x) ==> Q) == ((EX x. P(x)) ==> Q)"
   747 by rule iprover+
   748 
   749 lemma atomize_conjL[atomize_elim]: "(A ==> B ==> C) == (A & B ==> C)"
   750 by rule iprover+
   751 
   752 lemma atomize_disjL[atomize_elim]: "((A ==> C) ==> (B ==> C) ==> C) == ((A | B ==> C) ==> C)"
   753 by rule iprover+
   754 
   755 lemma atomize_elimL[atomize_elim]: "(!!B. (A ==> B) ==> B) == Trueprop(A)" ..
   756 
   757 
   758 subsection {* Calculational rules *}
   759 
   760 lemma forw_subst: "a = b ==> P(b) ==> P(a)"
   761   by (rule ssubst)
   762 
   763 lemma back_subst: "P(a) ==> a = b ==> P(b)"
   764   by (rule subst)
   765 
   766 text {*
   767   Note that this list of rules is in reverse order of priorities.
   768 *}
   769 
   770 lemmas basic_trans_rules [trans] =
   771   forw_subst
   772   back_subst
   773   rev_mp
   774   mp
   775   trans
   776 
   777 subsection {* ``Let'' declarations *}
   778 
   779 nonterminals letbinds letbind
   780 
   781 constdefs
   782   Let :: "['a::{}, 'a => 'b] => ('b::{})"
   783     "Let(s, f) == f(s)"
   784 
   785 syntax
   786   "_bind"       :: "[pttrn, 'a] => letbind"           ("(2_ =/ _)" 10)
   787   ""            :: "letbind => letbinds"              ("_")
   788   "_binds"      :: "[letbind, letbinds] => letbinds"  ("_;/ _")
   789   "_Let"        :: "[letbinds, 'a] => 'a"             ("(let (_)/ in (_))" 10)
   790 
   791 translations
   792   "_Let(_binds(b, bs), e)"  == "_Let(b, _Let(bs, e))"
   793   "let x = a in e"          == "Let(a, %x. e)"
   794 
   795 
   796 lemma LetI: 
   797   assumes "!!x. x=t ==> P(u(x))"
   798   shows "P(let x=t in u(x))"
   799   apply (unfold Let_def)
   800   apply (rule refl [THEN assms])
   801   done
   802 
   803 
   804 subsection {* Intuitionistic simplification rules *}
   805 
   806 lemma conj_simps:
   807   "P & True <-> P"
   808   "True & P <-> P"
   809   "P & False <-> False"
   810   "False & P <-> False"
   811   "P & P <-> P"
   812   "P & P & Q <-> P & Q"
   813   "P & ~P <-> False"
   814   "~P & P <-> False"
   815   "(P & Q) & R <-> P & (Q & R)"
   816   by iprover+
   817 
   818 lemma disj_simps:
   819   "P | True <-> True"
   820   "True | P <-> True"
   821   "P | False <-> P"
   822   "False | P <-> P"
   823   "P | P <-> P"
   824   "P | P | Q <-> P | Q"
   825   "(P | Q) | R <-> P | (Q | R)"
   826   by iprover+
   827 
   828 lemma not_simps:
   829   "~(P|Q)  <-> ~P & ~Q"
   830   "~ False <-> True"
   831   "~ True <-> False"
   832   by iprover+
   833 
   834 lemma imp_simps:
   835   "(P --> False) <-> ~P"
   836   "(P --> True) <-> True"
   837   "(False --> P) <-> True"
   838   "(True --> P) <-> P"
   839   "(P --> P) <-> True"
   840   "(P --> ~P) <-> ~P"
   841   by iprover+
   842 
   843 lemma iff_simps:
   844   "(True <-> P) <-> P"
   845   "(P <-> True) <-> P"
   846   "(P <-> P) <-> True"
   847   "(False <-> P) <-> ~P"
   848   "(P <-> False) <-> ~P"
   849   by iprover+
   850 
   851 (*The x=t versions are needed for the simplification procedures*)
   852 lemma quant_simps:
   853   "!!P. (ALL x. P) <-> P"
   854   "(ALL x. x=t --> P(x)) <-> P(t)"
   855   "(ALL x. t=x --> P(x)) <-> P(t)"
   856   "!!P. (EX x. P) <-> P"
   857   "EX x. x=t"
   858   "EX x. t=x"
   859   "(EX x. x=t & P(x)) <-> P(t)"
   860   "(EX x. t=x & P(x)) <-> P(t)"
   861   by iprover+
   862 
   863 (*These are NOT supplied by default!*)
   864 lemma distrib_simps:
   865   "P & (Q | R) <-> P&Q | P&R"
   866   "(Q | R) & P <-> Q&P | R&P"
   867   "(P | Q --> R) <-> (P --> R) & (Q --> R)"
   868   by iprover+
   869 
   870 
   871 text {* Conversion into rewrite rules *}
   872 
   873 lemma P_iff_F: "~P ==> (P <-> False)" by iprover
   874 lemma iff_reflection_F: "~P ==> (P == False)" by (rule P_iff_F [THEN iff_reflection])
   875 
   876 lemma P_iff_T: "P ==> (P <-> True)" by iprover
   877 lemma iff_reflection_T: "P ==> (P == True)" by (rule P_iff_T [THEN iff_reflection])
   878 
   879 
   880 text {* More rewrite rules *}
   881 
   882 lemma conj_commute: "P&Q <-> Q&P" by iprover
   883 lemma conj_left_commute: "P&(Q&R) <-> Q&(P&R)" by iprover
   884 lemmas conj_comms = conj_commute conj_left_commute
   885 
   886 lemma disj_commute: "P|Q <-> Q|P" by iprover
   887 lemma disj_left_commute: "P|(Q|R) <-> Q|(P|R)" by iprover
   888 lemmas disj_comms = disj_commute disj_left_commute
   889 
   890 lemma conj_disj_distribL: "P&(Q|R) <-> (P&Q | P&R)" by iprover
   891 lemma conj_disj_distribR: "(P|Q)&R <-> (P&R | Q&R)" by iprover
   892 
   893 lemma disj_conj_distribL: "P|(Q&R) <-> (P|Q) & (P|R)" by iprover
   894 lemma disj_conj_distribR: "(P&Q)|R <-> (P|R) & (Q|R)" by iprover
   895 
   896 lemma imp_conj_distrib: "(P --> (Q&R)) <-> (P-->Q) & (P-->R)" by iprover
   897 lemma imp_conj: "((P&Q)-->R)   <-> (P --> (Q --> R))" by iprover
   898 lemma imp_disj: "(P|Q --> R)   <-> (P-->R) & (Q-->R)" by iprover
   899 
   900 lemma de_Morgan_disj: "(~(P | Q)) <-> (~P & ~Q)" by iprover
   901 
   902 lemma not_ex: "(~ (EX x. P(x))) <-> (ALL x.~P(x))" by iprover
   903 lemma imp_ex: "((EX x. P(x)) --> Q) <-> (ALL x. P(x) --> Q)" by iprover
   904 
   905 lemma ex_disj_distrib:
   906   "(EX x. P(x) | Q(x)) <-> ((EX x. P(x)) | (EX x. Q(x)))" by iprover
   907 
   908 lemma all_conj_distrib:
   909   "(ALL x. P(x) & Q(x)) <-> ((ALL x. P(x)) & (ALL x. Q(x)))" by iprover
   910 
   911 
   912 subsection {* Legacy ML bindings *}
   913 
   914 ML {*
   915 val refl = @{thm refl}
   916 val trans = @{thm trans}
   917 val sym = @{thm sym}
   918 val subst = @{thm subst}
   919 val ssubst = @{thm ssubst}
   920 val conjI = @{thm conjI}
   921 val conjE = @{thm conjE}
   922 val conjunct1 = @{thm conjunct1}
   923 val conjunct2 = @{thm conjunct2}
   924 val disjI1 = @{thm disjI1}
   925 val disjI2 = @{thm disjI2}
   926 val disjE = @{thm disjE}
   927 val impI = @{thm impI}
   928 val impE = @{thm impE}
   929 val mp = @{thm mp}
   930 val rev_mp = @{thm rev_mp}
   931 val TrueI = @{thm TrueI}
   932 val FalseE = @{thm FalseE}
   933 val iff_refl = @{thm iff_refl}
   934 val iff_trans = @{thm iff_trans}
   935 val iffI = @{thm iffI}
   936 val iffE = @{thm iffE}
   937 val iffD1 = @{thm iffD1}
   938 val iffD2 = @{thm iffD2}
   939 val notI = @{thm notI}
   940 val notE = @{thm notE}
   941 val allI = @{thm allI}
   942 val allE = @{thm allE}
   943 val spec = @{thm spec}
   944 val exI = @{thm exI}
   945 val exE = @{thm exE}
   946 val eq_reflection = @{thm eq_reflection}
   947 val iff_reflection = @{thm iff_reflection}
   948 val meta_eq_to_obj_eq = @{thm meta_eq_to_obj_eq}
   949 val meta_eq_to_iff = @{thm meta_eq_to_iff}
   950 *}
   951 
   952 end