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