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