src/FOL/IFOL.thy
author wenzelm
Sat Oct 20 20:18:45 2001 +0200 (2001-10-20)
changeset 11848 6e3017adb8c0
parent 11771 b7b100a2de1d
child 11953 f98623fdf6ef
permissions -rw-r--r--
calculational rules moved from FOL to IFOL;
     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 (rule equal_intr_rule)
   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 (rule equal_intr_rule)
   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 (rule equal_intr_rule)
   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 declare atomize_all [symmetric, rulify]  atomize_imp [symmetric, rulify]
   162 
   163 
   164 subsection {* Calculational rules *}
   165 
   166 lemma forw_subst: "a = b ==> P(b) ==> P(a)"
   167   by (rule ssubst)
   168 
   169 lemma back_subst: "P(a) ==> a = b ==> P(b)"
   170   by (rule subst)
   171 
   172 text {*
   173   Note that this list of rules is in reverse order of priorities.
   174 *}
   175 
   176 lemmas trans_rules [trans] =
   177   forw_subst
   178   back_subst
   179   rev_mp
   180   mp
   181   transitive
   182   trans
   183 
   184 lemmas [Pure.elim] = sym
   185 
   186 end