src/FOL/IFOL.thy
author wenzelm
Tue Jan 08 00:03:42 2002 +0100 (2002-01-08)
changeset 12662 a9bbba3473f3
parent 12368 2af9ad81ea56
child 12875 bda60442bf02
permissions -rw-r--r--
syntax "_not_equal";
     1 (*  Title:      FOL/IFOL.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson and Markus Wenzel
     4 *)
     5 
     6 header {* Intuitionistic first-order logic *}
     7 
     8 theory IFOL = Pure
     9 files ("IFOL_lemmas.ML") ("fologic.ML") ("hypsubstdata.ML") ("intprover.ML"):
    10 
    11 
    12 subsection {* Syntax and axiomatic basis *}
    13 
    14 global
    15 
    16 classes "term" < logic
    17 defaultsort "term"
    18 
    19 typedecl o
    20 
    21 judgment
    22   Trueprop      :: "o => prop"                  ("(_)" 5)
    23 
    24 consts
    25   True          :: o
    26   False         :: o
    27 
    28   (* Connectives *)
    29 
    30   "="           :: "['a, 'a] => o"              (infixl 50)
    31 
    32   Not           :: "o => o"                     ("~ _" [40] 40)
    33   &             :: "[o, o] => o"                (infixr 35)
    34   "|"           :: "[o, o] => o"                (infixr 30)
    35   -->           :: "[o, o] => o"                (infixr 25)
    36   <->           :: "[o, o] => o"                (infixr 25)
    37 
    38   (* Quantifiers *)
    39 
    40   All           :: "('a => o) => o"             (binder "ALL " 10)
    41   Ex            :: "('a => o) => o"             (binder "EX " 10)
    42   Ex1           :: "('a => o) => o"             (binder "EX! " 10)
    43 
    44 
    45 syntax
    46   "_not_equal"  :: "['a, 'a] => o"              (infixl "~=" 50)
    47 translations
    48   "x ~= y"      == "~ (x = y)"
    49 
    50 syntax (xsymbols)
    51   Not           :: "o => o"                     ("\<not> _" [40] 40)
    52   "op &"        :: "[o, o] => o"                (infixr "\<and>" 35)
    53   "op |"        :: "[o, o] => o"                (infixr "\<or>" 30)
    54   "ALL "        :: "[idts, o] => o"             ("(3\<forall>_./ _)" [0, 10] 10)
    55   "EX "         :: "[idts, o] => o"             ("(3\<exists>_./ _)" [0, 10] 10)
    56   "EX! "        :: "[idts, o] => o"             ("(3\<exists>!_./ _)" [0, 10] 10)
    57   "_not_equal"  :: "['a, 'a] => o"              (infixl "\<noteq>" 50)
    58   "op -->"      :: "[o, o] => o"                (infixr "\<longrightarrow>" 25)
    59   "op <->"      :: "[o, o] => o"                (infixr "\<longleftrightarrow>" 25)
    60 
    61 syntax (HTML output)
    62   Not           :: "o => o"                     ("\<not> _" [40] 40)
    63 
    64 
    65 local
    66 
    67 axioms
    68 
    69   (* Equality *)
    70 
    71   refl:         "a=a"
    72   subst:        "[| a=b;  P(a) |] ==> P(b)"
    73 
    74   (* Propositional logic *)
    75 
    76   conjI:        "[| P;  Q |] ==> P&Q"
    77   conjunct1:    "P&Q ==> P"
    78   conjunct2:    "P&Q ==> Q"
    79 
    80   disjI1:       "P ==> P|Q"
    81   disjI2:       "Q ==> P|Q"
    82   disjE:        "[| P|Q;  P ==> R;  Q ==> R |] ==> R"
    83 
    84   impI:         "(P ==> Q) ==> P-->Q"
    85   mp:           "[| P-->Q;  P |] ==> Q"
    86 
    87   FalseE:       "False ==> P"
    88 
    89 
    90   (* Definitions *)
    91 
    92   True_def:     "True  == False-->False"
    93   not_def:      "~P    == P-->False"
    94   iff_def:      "P<->Q == (P-->Q) & (Q-->P)"
    95 
    96   (* Unique existence *)
    97 
    98   ex1_def:      "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
    99 
   100 
   101   (* Quantifiers *)
   102 
   103   allI:         "(!!x. P(x)) ==> (ALL x. P(x))"
   104   spec:         "(ALL x. P(x)) ==> P(x)"
   105 
   106   exI:          "P(x) ==> (EX x. P(x))"
   107   exE:          "[| EX x. P(x);  !!x. P(x) ==> R |] ==> R"
   108 
   109   (* Reflection *)
   110 
   111   eq_reflection:  "(x=y)   ==> (x==y)"
   112   iff_reflection: "(P<->Q) ==> (P==Q)"
   113 
   114 
   115 subsection {* Lemmas and proof tools *}
   116 
   117 setup Simplifier.setup
   118 use "IFOL_lemmas.ML"
   119 
   120 use "fologic.ML"
   121 use "hypsubstdata.ML"
   122 setup hypsubst_setup
   123 use "intprover.ML"
   124 
   125 
   126 subsubsection {* Intuitionistic Reasoning *}
   127 
   128 lemma impE':
   129   (assumes 1: "P --> Q" and 2: "Q ==> R" and 3: "P --> Q ==> P") R
   130 proof -
   131   from 3 and 1 have P .
   132   with 1 have Q by (rule impE)
   133   with 2 show R .
   134 qed
   135 
   136 lemma allE':
   137   (assumes 1: "ALL x. P(x)" and 2: "P(x) ==> ALL x. P(x) ==> Q") Q
   138 proof -
   139   from 1 have "P(x)" by (rule spec)
   140   from this and 1 show Q by (rule 2)
   141 qed
   142 
   143 lemma notE': (assumes 1: "~ P" and 2: "~ P ==> P") R
   144 proof -
   145   from 2 and 1 have P .
   146   with 1 show R by (rule notE)
   147 qed
   148 
   149 lemmas [Pure.elim!] = disjE iffE FalseE conjE exE
   150   and [Pure.intro!] = iffI conjI impI TrueI notI allI refl
   151   and [Pure.elim 2] = allE notE' impE'
   152   and [Pure.intro] = exI disjI2 disjI1
   153 
   154 ML_setup {*
   155   Context.>> (ContextRules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac));
   156 *}
   157 
   158 
   159 lemma iff_not_sym: "~ (Q <-> P) ==> ~ (P <-> Q)"
   160   by rules
   161 
   162 lemmas [sym] = sym iff_sym not_sym iff_not_sym
   163   and [Pure.elim?] = iffD1 iffD2 impE
   164 
   165 
   166 subsection {* Atomizing meta-level rules *}
   167 
   168 lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))"
   169 proof
   170   assume "!!x. P(x)"
   171   show "ALL x. P(x)" ..
   172 next
   173   assume "ALL x. P(x)"
   174   thus "!!x. P(x)" ..
   175 qed
   176 
   177 lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A --> B)"
   178 proof
   179   assume "A ==> B"
   180   thus "A --> B" ..
   181 next
   182   assume "A --> B" and A
   183   thus B by (rule mp)
   184 qed
   185 
   186 lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)"
   187 proof
   188   assume "x == y"
   189   show "x = y" by (unfold prems) (rule refl)
   190 next
   191   assume "x = y"
   192   thus "x == y" by (rule eq_reflection)
   193 qed
   194 
   195 lemma atomize_conj [atomize]: "(!!C. (A ==> B ==> PROP C) ==> PROP C) == Trueprop (A & B)"
   196 proof
   197   assume "!!C. (A ==> B ==> PROP C) ==> PROP C"
   198   show "A & B" by (rule conjI)
   199 next
   200   fix C
   201   assume "A & B"
   202   assume "A ==> B ==> PROP C"
   203   thus "PROP C"
   204   proof this
   205     show A by (rule conjunct1)
   206     show B by (rule conjunct2)
   207   qed
   208 qed
   209 
   210 lemmas [symmetric, rulify] = atomize_all atomize_imp
   211 
   212 
   213 subsection {* Calculational rules *}
   214 
   215 lemma forw_subst: "a = b ==> P(b) ==> P(a)"
   216   by (rule ssubst)
   217 
   218 lemma back_subst: "P(a) ==> a = b ==> P(b)"
   219   by (rule subst)
   220 
   221 text {*
   222   Note that this list of rules is in reverse order of priorities.
   223 *}
   224 
   225 lemmas basic_trans_rules [trans] =
   226   forw_subst
   227   back_subst
   228   rev_mp
   229   mp
   230   trans
   231 
   232 end