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