src/FOL/IFOL.thy
author wenzelm
Fri Oct 12 12:11:39 2001 +0200 (2001-10-12)
changeset 11734 7a21bf539412
parent 11677 ee12f18599e5
child 11747 17a6dcd6f3cf
permissions -rw-r--r--
declare impE iffD1 iffD2 ad elim of Pure;
     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 consts
    22 
    23   Trueprop      :: "o => prop"                  ("(_)" 5)
    24   True          :: o
    25   False         :: o
    26 
    27   (* Connectives *)
    28 
    29   "="           :: "['a, 'a] => o"              (infixl 50)
    30 
    31   Not           :: "o => o"                     ("~ _" [40] 40)
    32   &             :: "[o, o] => o"                (infixr 35)
    33   "|"           :: "[o, o] => o"                (infixr 30)
    34   -->           :: "[o, o] => o"                (infixr 25)
    35   <->           :: "[o, o] => o"                (infixr 25)
    36 
    37   (* Quantifiers *)
    38 
    39   All           :: "('a => o) => o"             (binder "ALL " 10)
    40   Ex            :: "('a => o) => o"             (binder "EX " 10)
    41   Ex1           :: "('a => o) => o"             (binder "EX! " 10)
    42 
    43 
    44 syntax
    45   "~="          :: "['a, 'a] => o"              (infixl 50)
    46 translations
    47   "x ~= y"      == "~ (x = y)"
    48 
    49 syntax (symbols)
    50   Not           :: "o => o"                     ("\<not> _" [40] 40)
    51   "op &"        :: "[o, o] => o"                (infixr "\<and>" 35)
    52   "op |"        :: "[o, o] => o"                (infixr "\<or>" 30)
    53   "op -->"      :: "[o, o] => o"                (infixr "\<midarrow>\<rightarrow>" 25)
    54   "op <->"      :: "[o, o] => o"                (infixr "\<leftarrow>\<rightarrow>" 25)
    55   "ALL "        :: "[idts, o] => o"             ("(3\<forall>_./ _)" [0, 10] 10)
    56   "EX "         :: "[idts, o] => o"             ("(3\<exists>_./ _)" [0, 10] 10)
    57   "EX! "        :: "[idts, o] => o"             ("(3\<exists>!_./ _)" [0, 10] 10)
    58   "op ~="       :: "['a, 'a] => o"              (infixl "\<noteq>" 50)
    59 
    60 syntax (xsymbols)
    61   "op -->"      :: "[o, o] => o"                (infixr "\<longrightarrow>" 25)
    62   "op <->"      :: "[o, o] => o"                (infixr "\<longleftrightarrow>" 25)
    63 
    64 syntax (HTML output)
    65   Not           :: "o => o"                     ("\<not> _" [40] 40)
    66 
    67 
    68 local
    69 
    70 axioms
    71 
    72   (* Equality *)
    73 
    74   refl:         "a=a"
    75   subst:        "[| a=b;  P(a) |] ==> P(b)"
    76 
    77   (* Propositional logic *)
    78 
    79   conjI:        "[| P;  Q |] ==> P&Q"
    80   conjunct1:    "P&Q ==> P"
    81   conjunct2:    "P&Q ==> Q"
    82 
    83   disjI1:       "P ==> P|Q"
    84   disjI2:       "Q ==> P|Q"
    85   disjE:        "[| P|Q;  P ==> R;  Q ==> R |] ==> R"
    86 
    87   impI:         "(P ==> Q) ==> P-->Q"
    88   mp:           "[| P-->Q;  P |] ==> Q"
    89 
    90   FalseE:       "False ==> P"
    91 
    92 
    93   (* Definitions *)
    94 
    95   True_def:     "True  == False-->False"
    96   not_def:      "~P    == P-->False"
    97   iff_def:      "P<->Q == (P-->Q) & (Q-->P)"
    98 
    99   (* Unique existence *)
   100 
   101   ex1_def:      "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
   102 
   103 
   104   (* Quantifiers *)
   105 
   106   allI:         "(!!x. P(x)) ==> (ALL x. P(x))"
   107   spec:         "(ALL x. P(x)) ==> P(x)"
   108 
   109   exI:          "P(x) ==> (EX x. P(x))"
   110   exE:          "[| EX x. P(x);  !!x. P(x) ==> R |] ==> R"
   111 
   112   (* Reflection *)
   113 
   114   eq_reflection:  "(x=y)   ==> (x==y)"
   115   iff_reflection: "(P<->Q) ==> (P==Q)"
   116 
   117 
   118 subsection {* Lemmas and proof tools *}
   119 
   120 setup Simplifier.setup
   121 use "IFOL_lemmas.ML"
   122 
   123 declare impE [Pure.elim]  iffD1 [Pure.elim]  iffD2 [Pure.elim]
   124 
   125 use "fologic.ML"
   126 use "hypsubstdata.ML"
   127 setup hypsubst_setup
   128 use "intprover.ML"
   129 
   130 
   131 subsection {* Atomizing meta-level rules *}
   132 
   133 lemma atomize_all: "(!!x. P(x)) == Trueprop (ALL x. P(x))"
   134 proof (rule equal_intr_rule)
   135   assume "!!x. P(x)"
   136   show "ALL x. P(x)" by (rule allI)
   137 next
   138   assume "ALL x. P(x)"
   139   thus "!!x. P(x)" by (rule allE)
   140 qed
   141 
   142 lemma atomize_imp: "(A ==> B) == Trueprop (A --> B)"
   143 proof (rule equal_intr_rule)
   144   assume r: "A ==> B"
   145   show "A --> B" by (rule impI) (rule r)
   146 next
   147   assume "A --> B" and A
   148   thus B by (rule mp)
   149 qed
   150 
   151 lemma atomize_eq: "(x == y) == Trueprop (x = y)"
   152 proof (rule equal_intr_rule)
   153   assume "x == y"
   154   show "x = y" by (unfold prems) (rule refl)
   155 next
   156   assume "x = y"
   157   thus "x == y" by (rule eq_reflection)
   158 qed
   159 
   160 lemmas atomize = atomize_all atomize_imp
   161 lemmas atomize' = atomize atomize_eq
   162 
   163 end