src/FOL/IFOL.thy
author wenzelm
Fri Nov 09 00:09:47 2001 +0100 (2001-11-09)
changeset 12114 a8e860c86252
parent 12019 abe9b7c6016e
child 12349 94e812f9683e
permissions -rw-r--r--
eliminated old "symbols" syntax, use "xsymbols" instead;
     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   "~="          :: "['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   "op ~="       :: "['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 declare impE [Pure.elim]  iffD1 [Pure.elim]  iffD2 [Pure.elim]
   121 
   122 use "fologic.ML"
   123 use "hypsubstdata.ML"
   124 setup hypsubst_setup
   125 use "intprover.ML"
   126 
   127 
   128 subsection {* Atomizing meta-level rules *}
   129 
   130 lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))"
   131 proof
   132   assume "!!x. P(x)"
   133   show "ALL x. P(x)" by (rule allI)
   134 next
   135   assume "ALL x. P(x)"
   136   thus "!!x. P(x)" by (rule allE)
   137 qed
   138 
   139 lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A --> B)"
   140 proof
   141   assume r: "A ==> B"
   142   show "A --> B" by (rule impI) (rule r)
   143 next
   144   assume "A --> B" and A
   145   thus B by (rule mp)
   146 qed
   147 
   148 lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)"
   149 proof
   150   assume "x == y"
   151   show "x = y" by (unfold prems) (rule refl)
   152 next
   153   assume "x = y"
   154   thus "x == y" by (rule eq_reflection)
   155 qed
   156 
   157 lemma atomize_conj [atomize]: "(!!C. (A ==> B ==> PROP C) ==> PROP C) == Trueprop (A & B)"
   158 proof
   159   assume "!!C. (A ==> B ==> PROP C) ==> PROP C"
   160   show "A & B" by (rule conjI)
   161 next
   162   fix C
   163   assume "A & B"
   164   assume "A ==> B ==> PROP C"
   165   thus "PROP C"
   166   proof this
   167     show A by (rule conjunct1)
   168     show B by (rule conjunct2)
   169   qed
   170 qed
   171 
   172 declare atomize_all [symmetric, rulify]  atomize_imp [symmetric, rulify]
   173 
   174 
   175 subsection {* Calculational rules *}
   176 
   177 lemma forw_subst: "a = b ==> P(b) ==> P(a)"
   178   by (rule ssubst)
   179 
   180 lemma back_subst: "P(a) ==> a = b ==> P(b)"
   181   by (rule subst)
   182 
   183 text {*
   184   Note that this list of rules is in reverse order of priorities.
   185 *}
   186 
   187 lemmas basic_trans_rules [trans] =
   188   forw_subst
   189   back_subst
   190   rev_mp
   191   mp
   192   trans
   193 
   194 lemmas [Pure.elim] = sym
   195 
   196 end