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