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