src/FOL/IFOL.thy
author wenzelm
Sun Nov 02 18:21:45 2014 +0100 (2014-11-02)
changeset 58889 5b7a9633cfa8
parent 58826 2ed2eaabe3df
child 58963 26bf09b95dda
permissions -rw-r--r--
modernized header uniformly as section;
     1 (*  Title:      FOL/IFOL.thy
     2     Author:     Lawrence C Paulson and Markus Wenzel
     3 *)
     4 
     5 section {* 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 ML_file "intprover.ML"
   595 
   596 
   597 subsection {* Intuitionistic Reasoning *}
   598 
   599 setup {* Intuitionistic.method_setup @{binding iprover} *}
   600 
   601 lemma impE':
   602   assumes 1: "P --> Q"
   603     and 2: "Q ==> R"
   604     and 3: "P --> Q ==> P"
   605   shows R
   606 proof -
   607   from 3 and 1 have P .
   608   with 1 have Q by (rule impE)
   609   with 2 show R .
   610 qed
   611 
   612 lemma allE':
   613   assumes 1: "ALL x. P(x)"
   614     and 2: "P(x) ==> ALL x. P(x) ==> Q"
   615   shows Q
   616 proof -
   617   from 1 have "P(x)" by (rule spec)
   618   from this and 1 show Q by (rule 2)
   619 qed
   620 
   621 lemma notE':
   622   assumes 1: "~ P"
   623     and 2: "~ P ==> P"
   624   shows R
   625 proof -
   626   from 2 and 1 have P .
   627   with 1 show R by (rule notE)
   628 qed
   629 
   630 lemmas [Pure.elim!] = disjE iffE FalseE conjE exE
   631   and [Pure.intro!] = iffI conjI impI TrueI notI allI refl
   632   and [Pure.elim 2] = allE notE' impE'
   633   and [Pure.intro] = exI disjI2 disjI1
   634 
   635 setup {* Context_Rules.addSWrapper (fn ctxt => fn tac => hyp_subst_tac ctxt ORELSE' tac) *}
   636 
   637 
   638 lemma iff_not_sym: "~ (Q <-> P) ==> ~ (P <-> Q)"
   639   by iprover
   640 
   641 lemmas [sym] = sym iff_sym not_sym iff_not_sym
   642   and [Pure.elim?] = iffD1 iffD2 impE
   643 
   644 
   645 lemma eq_commute: "a=b <-> b=a"
   646 apply (rule iffI) 
   647 apply (erule sym)+
   648 done
   649 
   650 
   651 subsection {* Atomizing meta-level rules *}
   652 
   653 lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))"
   654 proof
   655   assume "!!x. P(x)"
   656   then show "ALL x. P(x)" ..
   657 next
   658   assume "ALL x. P(x)"
   659   then show "!!x. P(x)" ..
   660 qed
   661 
   662 lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A --> B)"
   663 proof
   664   assume "A ==> B"
   665   then show "A --> B" ..
   666 next
   667   assume "A --> B" and A
   668   then show B by (rule mp)
   669 qed
   670 
   671 lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)"
   672 proof
   673   assume "x == y"
   674   show "x = y" unfolding `x == y` by (rule refl)
   675 next
   676   assume "x = y"
   677   then show "x == y" by (rule eq_reflection)
   678 qed
   679 
   680 lemma atomize_iff [atomize]: "(A == B) == Trueprop (A <-> B)"
   681 proof
   682   assume "A == B"
   683   show "A <-> B" unfolding `A == B` by (rule iff_refl)
   684 next
   685   assume "A <-> B"
   686   then show "A == B" by (rule iff_reflection)
   687 qed
   688 
   689 lemma atomize_conj [atomize]: "(A &&& B) == Trueprop (A & B)"
   690 proof
   691   assume conj: "A &&& B"
   692   show "A & B"
   693   proof (rule conjI)
   694     from conj show A by (rule conjunctionD1)
   695     from conj show B by (rule conjunctionD2)
   696   qed
   697 next
   698   assume conj: "A & B"
   699   show "A &&& B"
   700   proof -
   701     from conj show A ..
   702     from conj show B ..
   703   qed
   704 qed
   705 
   706 lemmas [symmetric, rulify] = atomize_all atomize_imp
   707   and [symmetric, defn] = atomize_all atomize_imp atomize_eq atomize_iff
   708 
   709 
   710 subsection {* Atomizing elimination rules *}
   711 
   712 lemma atomize_exL[atomize_elim]: "(!!x. P(x) ==> Q) == ((EX x. P(x)) ==> Q)"
   713   by rule iprover+
   714 
   715 lemma atomize_conjL[atomize_elim]: "(A ==> B ==> C) == (A & B ==> C)"
   716   by rule iprover+
   717 
   718 lemma atomize_disjL[atomize_elim]: "((A ==> C) ==> (B ==> C) ==> C) == ((A | B ==> C) ==> C)"
   719   by rule iprover+
   720 
   721 lemma atomize_elimL[atomize_elim]: "(!!B. (A ==> B) ==> B) == Trueprop(A)" ..
   722 
   723 
   724 subsection {* Calculational rules *}
   725 
   726 lemma forw_subst: "a = b ==> P(b) ==> P(a)"
   727   by (rule ssubst)
   728 
   729 lemma back_subst: "P(a) ==> a = b ==> P(b)"
   730   by (rule subst)
   731 
   732 text {*
   733   Note that this list of rules is in reverse order of priorities.
   734 *}
   735 
   736 lemmas basic_trans_rules [trans] =
   737   forw_subst
   738   back_subst
   739   rev_mp
   740   mp
   741   trans
   742 
   743 subsection {* ``Let'' declarations *}
   744 
   745 nonterminal letbinds and letbind
   746 
   747 definition Let :: "['a::{}, 'a => 'b] => ('b::{})" where
   748     "Let(s, f) == f(s)"
   749 
   750 syntax
   751   "_bind"       :: "[pttrn, 'a] => letbind"           ("(2_ =/ _)" 10)
   752   ""            :: "letbind => letbinds"              ("_")
   753   "_binds"      :: "[letbind, letbinds] => letbinds"  ("_;/ _")
   754   "_Let"        :: "[letbinds, 'a] => 'a"             ("(let (_)/ in (_))" 10)
   755 
   756 translations
   757   "_Let(_binds(b, bs), e)"  == "_Let(b, _Let(bs, e))"
   758   "let x = a in e"          == "CONST Let(a, %x. e)"
   759 
   760 
   761 lemma LetI: 
   762   assumes "!!x. x=t ==> P(u(x))"
   763   shows "P(let x=t in u(x))"
   764   apply (unfold Let_def)
   765   apply (rule refl [THEN assms])
   766   done
   767 
   768 
   769 subsection {* Intuitionistic simplification rules *}
   770 
   771 lemma conj_simps:
   772   "P & True <-> P"
   773   "True & P <-> P"
   774   "P & False <-> False"
   775   "False & P <-> False"
   776   "P & P <-> P"
   777   "P & P & Q <-> P & Q"
   778   "P & ~P <-> False"
   779   "~P & P <-> False"
   780   "(P & Q) & R <-> P & (Q & R)"
   781   by iprover+
   782 
   783 lemma disj_simps:
   784   "P | True <-> True"
   785   "True | P <-> True"
   786   "P | False <-> P"
   787   "False | P <-> P"
   788   "P | P <-> P"
   789   "P | P | Q <-> P | Q"
   790   "(P | Q) | R <-> P | (Q | R)"
   791   by iprover+
   792 
   793 lemma not_simps:
   794   "~(P|Q)  <-> ~P & ~Q"
   795   "~ False <-> True"
   796   "~ True <-> False"
   797   by iprover+
   798 
   799 lemma imp_simps:
   800   "(P --> False) <-> ~P"
   801   "(P --> True) <-> True"
   802   "(False --> P) <-> True"
   803   "(True --> P) <-> P"
   804   "(P --> P) <-> True"
   805   "(P --> ~P) <-> ~P"
   806   by iprover+
   807 
   808 lemma iff_simps:
   809   "(True <-> P) <-> P"
   810   "(P <-> True) <-> P"
   811   "(P <-> P) <-> True"
   812   "(False <-> P) <-> ~P"
   813   "(P <-> False) <-> ~P"
   814   by iprover+
   815 
   816 (*The x=t versions are needed for the simplification procedures*)
   817 lemma quant_simps:
   818   "!!P. (ALL x. P) <-> P"
   819   "(ALL x. x=t --> P(x)) <-> P(t)"
   820   "(ALL x. t=x --> P(x)) <-> P(t)"
   821   "!!P. (EX x. P) <-> P"
   822   "EX x. x=t"
   823   "EX x. t=x"
   824   "(EX x. x=t & P(x)) <-> P(t)"
   825   "(EX x. t=x & P(x)) <-> P(t)"
   826   by iprover+
   827 
   828 (*These are NOT supplied by default!*)
   829 lemma distrib_simps:
   830   "P & (Q | R) <-> P&Q | P&R"
   831   "(Q | R) & P <-> Q&P | R&P"
   832   "(P | Q --> R) <-> (P --> R) & (Q --> R)"
   833   by iprover+
   834 
   835 
   836 text {* Conversion into rewrite rules *}
   837 
   838 lemma P_iff_F: "~P ==> (P <-> False)" by iprover
   839 lemma iff_reflection_F: "~P ==> (P == False)" by (rule P_iff_F [THEN iff_reflection])
   840 
   841 lemma P_iff_T: "P ==> (P <-> True)" by iprover
   842 lemma iff_reflection_T: "P ==> (P == True)" by (rule P_iff_T [THEN iff_reflection])
   843 
   844 
   845 text {* More rewrite rules *}
   846 
   847 lemma conj_commute: "P&Q <-> Q&P" by iprover
   848 lemma conj_left_commute: "P&(Q&R) <-> Q&(P&R)" by iprover
   849 lemmas conj_comms = conj_commute conj_left_commute
   850 
   851 lemma disj_commute: "P|Q <-> Q|P" by iprover
   852 lemma disj_left_commute: "P|(Q|R) <-> Q|(P|R)" by iprover
   853 lemmas disj_comms = disj_commute disj_left_commute
   854 
   855 lemma conj_disj_distribL: "P&(Q|R) <-> (P&Q | P&R)" by iprover
   856 lemma conj_disj_distribR: "(P|Q)&R <-> (P&R | Q&R)" by iprover
   857 
   858 lemma disj_conj_distribL: "P|(Q&R) <-> (P|Q) & (P|R)" by iprover
   859 lemma disj_conj_distribR: "(P&Q)|R <-> (P|R) & (Q|R)" by iprover
   860 
   861 lemma imp_conj_distrib: "(P --> (Q&R)) <-> (P-->Q) & (P-->R)" by iprover
   862 lemma imp_conj: "((P&Q)-->R)   <-> (P --> (Q --> R))" by iprover
   863 lemma imp_disj: "(P|Q --> R)   <-> (P-->R) & (Q-->R)" by iprover
   864 
   865 lemma de_Morgan_disj: "(~(P | Q)) <-> (~P & ~Q)" by iprover
   866 
   867 lemma not_ex: "(~ (EX x. P(x))) <-> (ALL x.~P(x))" by iprover
   868 lemma imp_ex: "((EX x. P(x)) --> Q) <-> (ALL x. P(x) --> Q)" by iprover
   869 
   870 lemma ex_disj_distrib:
   871   "(EX x. P(x) | Q(x)) <-> ((EX x. P(x)) | (EX x. Q(x)))" by iprover
   872 
   873 lemma all_conj_distrib:
   874   "(ALL x. P(x) & Q(x)) <-> ((ALL x. P(x)) & (ALL x. Q(x)))" by iprover
   875 
   876 end