src/FOL/IFOL.thy
author wenzelm
Sun Oct 28 21:10:47 2001 +0100 (2001-10-28)
changeset 11976 075df6e46cef
parent 11953 f98623fdf6ef
child 12019 abe9b7c6016e
permissions -rw-r--r--
equal_intr_rule already declared in 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 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 (symbols)
    51   Not           :: "o => o"                     ("\<not> _" [40] 40)
    52   "op &"        :: "[o, o] => o"                (infixr "\<and>" 35)
    53   "op |"        :: "[o, o] => o"                (infixr "\<or>" 30)
    54   "op -->"      :: "[o, o] => o"                (infixr "\<midarrow>\<rightarrow>" 25)
    55   "op <->"      :: "[o, o] => o"                (infixr "\<leftarrow>\<rightarrow>" 25)
    56   "ALL "        :: "[idts, o] => o"             ("(3\<forall>_./ _)" [0, 10] 10)
    57   "EX "         :: "[idts, o] => o"             ("(3\<exists>_./ _)" [0, 10] 10)
    58   "EX! "        :: "[idts, o] => o"             ("(3\<exists>!_./ _)" [0, 10] 10)
    59   "op ~="       :: "['a, 'a] => o"              (infixl "\<noteq>" 50)
    60 
    61 syntax (xsymbols)
    62   "op -->"      :: "[o, o] => o"                (infixr "\<longrightarrow>" 25)
    63   "op <->"      :: "[o, o] => o"                (infixr "\<longleftrightarrow>" 25)
    64 
    65 syntax (HTML output)
    66   Not           :: "o => o"                     ("\<not> _" [40] 40)
    67 
    68 
    69 local
    70 
    71 axioms
    72 
    73   (* Equality *)
    74 
    75   refl:         "a=a"
    76   subst:        "[| a=b;  P(a) |] ==> P(b)"
    77 
    78   (* Propositional logic *)
    79 
    80   conjI:        "[| P;  Q |] ==> P&Q"
    81   conjunct1:    "P&Q ==> P"
    82   conjunct2:    "P&Q ==> Q"
    83 
    84   disjI1:       "P ==> P|Q"
    85   disjI2:       "Q ==> P|Q"
    86   disjE:        "[| P|Q;  P ==> R;  Q ==> R |] ==> R"
    87 
    88   impI:         "(P ==> Q) ==> P-->Q"
    89   mp:           "[| P-->Q;  P |] ==> Q"
    90 
    91   FalseE:       "False ==> P"
    92 
    93 
    94   (* Definitions *)
    95 
    96   True_def:     "True  == False-->False"
    97   not_def:      "~P    == P-->False"
    98   iff_def:      "P<->Q == (P-->Q) & (Q-->P)"
    99 
   100   (* Unique existence *)
   101 
   102   ex1_def:      "EX! x. P(x) == EX x. P(x) & (ALL y. P(y) --> y=x)"
   103 
   104 
   105   (* Quantifiers *)
   106 
   107   allI:         "(!!x. P(x)) ==> (ALL x. P(x))"
   108   spec:         "(ALL x. P(x)) ==> P(x)"
   109 
   110   exI:          "P(x) ==> (EX x. P(x))"
   111   exE:          "[| EX x. P(x);  !!x. P(x) ==> R |] ==> R"
   112 
   113   (* Reflection *)
   114 
   115   eq_reflection:  "(x=y)   ==> (x==y)"
   116   iff_reflection: "(P<->Q) ==> (P==Q)"
   117 
   118 
   119 subsection {* Lemmas and proof tools *}
   120 
   121 setup Simplifier.setup
   122 use "IFOL_lemmas.ML"
   123 
   124 declare impE [Pure.elim]  iffD1 [Pure.elim]  iffD2 [Pure.elim]
   125 
   126 use "fologic.ML"
   127 use "hypsubstdata.ML"
   128 setup hypsubst_setup
   129 use "intprover.ML"
   130 
   131 
   132 subsection {* Atomizing meta-level rules *}
   133 
   134 lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))"
   135 proof
   136   assume "!!x. P(x)"
   137   show "ALL x. P(x)" by (rule allI)
   138 next
   139   assume "ALL x. P(x)"
   140   thus "!!x. P(x)" by (rule allE)
   141 qed
   142 
   143 lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A --> B)"
   144 proof
   145   assume r: "A ==> B"
   146   show "A --> B" by (rule impI) (rule r)
   147 next
   148   assume "A --> B" and A
   149   thus B by (rule mp)
   150 qed
   151 
   152 lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)"
   153 proof
   154   assume "x == y"
   155   show "x = y" by (unfold prems) (rule refl)
   156 next
   157   assume "x = y"
   158   thus "x == y" by (rule eq_reflection)
   159 qed
   160 
   161 lemma atomize_conj [atomize]: "(!!C. (A ==> B ==> PROP C) ==> PROP C) == Trueprop (A & B)"
   162 proof
   163   assume "!!C. (A ==> B ==> PROP C) ==> PROP C"
   164   show "A & B" by (rule conjI)
   165 next
   166   fix C
   167   assume "A & B"
   168   assume "A ==> B ==> PROP C"
   169   thus "PROP C"
   170   proof this
   171     show A by (rule conjunct1)
   172     show B by (rule conjunct2)
   173   qed
   174 qed
   175 
   176 declare atomize_all [symmetric, rulify]  atomize_imp [symmetric, rulify]
   177 
   178 
   179 subsection {* Calculational rules *}
   180 
   181 lemma forw_subst: "a = b ==> P(b) ==> P(a)"
   182   by (rule ssubst)
   183 
   184 lemma back_subst: "P(a) ==> a = b ==> P(b)"
   185   by (rule subst)
   186 
   187 text {*
   188   Note that this list of rules is in reverse order of priorities.
   189 *}
   190 
   191 lemmas trans_rules [trans] =
   192   forw_subst
   193   back_subst
   194   rev_mp
   195   mp
   196   transitive
   197   trans
   198 
   199 lemmas [Pure.elim] = sym
   200 
   201 end