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