src/FOL/IFOL.thy
author kleing
Wed Apr 14 14:13:05 2004 +0200 (2004-04-14)
changeset 14565 c6dc17aab88a
parent 14236 c73d62ce9d1c
child 14854 61bdf2ae4dc5
permissions -rw-r--r--
use more symbols in HTML output
     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   "op &"        :: "[o, o] => o"                (infixr "\<and>" 35)
    64   "op |"        :: "[o, o] => o"                (infixr "\<or>" 30)
    65   "ALL "        :: "[idts, o] => o"             ("(3\<forall>_./ _)" [0, 10] 10)
    66   "EX "         :: "[idts, o] => o"             ("(3\<exists>_./ _)" [0, 10] 10)
    67   "EX! "        :: "[idts, o] => o"             ("(3\<exists>!_./ _)" [0, 10] 10)
    68   "_not_equal"  :: "['a, 'a] => o"              (infixl "\<noteq>" 50)
    69 
    70 
    71 local
    72 
    73 finalconsts
    74   False All Ex
    75   "op ="
    76   "op &"
    77   "op |"
    78   "op -->"
    79 
    80 axioms
    81 
    82   (* Equality *)
    83 
    84   refl:         "a=a"
    85   subst:        "[| a=b;  P(a) |] ==> P(b)"
    86 
    87   (* Propositional logic *)
    88 
    89   conjI:        "[| P;  Q |] ==> P&Q"
    90   conjunct1:    "P&Q ==> P"
    91   conjunct2:    "P&Q ==> Q"
    92 
    93   disjI1:       "P ==> P|Q"
    94   disjI2:       "Q ==> P|Q"
    95   disjE:        "[| P|Q;  P ==> R;  Q ==> R |] ==> R"
    96 
    97   impI:         "(P ==> Q) ==> P-->Q"
    98   mp:           "[| P-->Q;  P |] ==> Q"
    99 
   100   FalseE:       "False ==> P"
   101 
   102   (* Quantifiers *)
   103 
   104   allI:         "(!!x. P(x)) ==> (ALL x. P(x))"
   105   spec:         "(ALL x. P(x)) ==> P(x)"
   106 
   107   exI:          "P(x) ==> (EX x. P(x))"
   108   exE:          "[| EX x. P(x);  !!x. P(x) ==> R |] ==> R"
   109 
   110   (* Reflection *)
   111 
   112   eq_reflection:  "(x=y)   ==> (x==y)"
   113   iff_reflection: "(P<->Q) ==> (P==Q)"
   114 
   115 
   116 defs
   117   (* Definitions *)
   118 
   119   True_def:     "True  == False-->False"
   120   not_def:      "~P    == P-->False"
   121   iff_def:      "P<->Q == (P-->Q) & (Q-->P)"
   122 
   123   (* Unique existence *)
   124 
   125   ex1_def:      "Ex1(P) == EX x. P(x) & (ALL y. P(y) --> y=x)"
   126 
   127 
   128 subsection {* Lemmas and proof tools *}
   129 
   130 setup Simplifier.setup
   131 use "IFOL_lemmas.ML"
   132 
   133 use "fologic.ML"
   134 use "hypsubstdata.ML"
   135 setup hypsubst_setup
   136 use "intprover.ML"
   137 
   138 
   139 subsection {* Intuitionistic Reasoning *}
   140 
   141 lemma impE':
   142   assumes 1: "P --> Q"
   143     and 2: "Q ==> R"
   144     and 3: "P --> Q ==> P"
   145   shows R
   146 proof -
   147   from 3 and 1 have P .
   148   with 1 have Q by (rule impE)
   149   with 2 show R .
   150 qed
   151 
   152 lemma allE':
   153   assumes 1: "ALL x. P(x)"
   154     and 2: "P(x) ==> ALL x. P(x) ==> Q"
   155   shows Q
   156 proof -
   157   from 1 have "P(x)" by (rule spec)
   158   from this and 1 show Q by (rule 2)
   159 qed
   160 
   161 lemma notE':
   162   assumes 1: "~ P"
   163     and 2: "~ P ==> P"
   164   shows R
   165 proof -
   166   from 2 and 1 have P .
   167   with 1 show R by (rule notE)
   168 qed
   169 
   170 lemmas [Pure.elim!] = disjE iffE FalseE conjE exE
   171   and [Pure.intro!] = iffI conjI impI TrueI notI allI refl
   172   and [Pure.elim 2] = allE notE' impE'
   173   and [Pure.intro] = exI disjI2 disjI1
   174 
   175 ML_setup {*
   176   Context.>> (ContextRules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac));
   177 *}
   178 
   179 
   180 lemma iff_not_sym: "~ (Q <-> P) ==> ~ (P <-> Q)"
   181   by rules
   182 
   183 lemmas [sym] = sym iff_sym not_sym iff_not_sym
   184   and [Pure.elim?] = iffD1 iffD2 impE
   185 
   186 
   187 lemma eq_commute: "a=b <-> b=a"
   188 apply (rule iffI) 
   189 apply (erule sym)+
   190 done
   191 
   192 
   193 subsection {* Atomizing meta-level rules *}
   194 
   195 lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))"
   196 proof
   197   assume "!!x. P(x)"
   198   show "ALL x. P(x)" ..
   199 next
   200   assume "ALL x. P(x)"
   201   thus "!!x. P(x)" ..
   202 qed
   203 
   204 lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A --> B)"
   205 proof
   206   assume "A ==> B"
   207   thus "A --> B" ..
   208 next
   209   assume "A --> B" and A
   210   thus B by (rule mp)
   211 qed
   212 
   213 lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)"
   214 proof
   215   assume "x == y"
   216   show "x = y" by (unfold prems) (rule refl)
   217 next
   218   assume "x = y"
   219   thus "x == y" by (rule eq_reflection)
   220 qed
   221 
   222 lemma atomize_conj [atomize]:
   223   "(!!C. (A ==> B ==> PROP C) ==> PROP C) == Trueprop (A & B)"
   224 proof
   225   assume "!!C. (A ==> B ==> PROP C) ==> PROP C"
   226   show "A & B" by (rule conjI)
   227 next
   228   fix C
   229   assume "A & B"
   230   assume "A ==> B ==> PROP C"
   231   thus "PROP C"
   232   proof this
   233     show A by (rule conjunct1)
   234     show B by (rule conjunct2)
   235   qed
   236 qed
   237 
   238 lemmas [symmetric, rulify] = atomize_all atomize_imp
   239 
   240 
   241 subsection {* Calculational rules *}
   242 
   243 lemma forw_subst: "a = b ==> P(b) ==> P(a)"
   244   by (rule ssubst)
   245 
   246 lemma back_subst: "P(a) ==> a = b ==> P(b)"
   247   by (rule subst)
   248 
   249 text {*
   250   Note that this list of rules is in reverse order of priorities.
   251 *}
   252 
   253 lemmas basic_trans_rules [trans] =
   254   forw_subst
   255   back_subst
   256   rev_mp
   257   mp
   258   trans
   259 
   260 
   261 
   262 subsection {* ``Let'' declarations *}
   263 
   264 nonterminals letbinds letbind
   265 
   266 constdefs
   267   Let :: "['a::logic, 'a => 'b] => ('b::logic)"
   268     "Let(s, f) == f(s)"
   269 
   270 syntax
   271   "_bind"       :: "[pttrn, 'a] => letbind"           ("(2_ =/ _)" 10)
   272   ""            :: "letbind => letbinds"              ("_")
   273   "_binds"      :: "[letbind, letbinds] => letbinds"  ("_;/ _")
   274   "_Let"        :: "[letbinds, 'a] => 'a"             ("(let (_)/ in (_))" 10)
   275 
   276 translations
   277   "_Let(_binds(b, bs), e)"  == "_Let(b, _Let(bs, e))"
   278   "let x = a in e"          == "Let(a, %x. e)"
   279 
   280 
   281 lemma LetI: 
   282     assumes prem: "(!!x. x=t ==> P(u(x)))"
   283     shows "P(let x=t in u(x))"
   284 apply (unfold Let_def)
   285 apply (rule refl [THEN prem])
   286 done
   287 
   288 ML
   289 {*
   290 val Let_def = thm "Let_def";
   291 val LetI = thm "LetI";
   292 *}
   293 
   294 end