src/FOL/IFOL.thy
author haftmann
Fri Jun 17 16:12:49 2005 +0200 (2005-06-17)
changeset 16417 9bc16273c2d4
parent 16121 a80aa66d2271
child 17276 3bb24e8b2cb2
permissions -rw-r--r--
migrated theory headers to new format
     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
     9 imports Pure
    10 uses ("IFOL_lemmas.ML") ("fologic.ML") ("hypsubstdata.ML") ("intprover.ML")
    11 begin
    12 
    13 
    14 subsection {* Syntax and axiomatic basis *}
    15 
    16 global
    17 
    18 classes "term"
    19 defaultsort "term"
    20 
    21 typedecl o
    22 
    23 judgment
    24   Trueprop      :: "o => prop"                  ("(_)" 5)
    25 
    26 consts
    27   True          :: o
    28   False         :: o
    29 
    30   (* Connectives *)
    31 
    32   "="           :: "['a, 'a] => o"              (infixl 50)
    33 
    34   Not           :: "o => o"                     ("~ _" [40] 40)
    35   &             :: "[o, o] => o"                (infixr 35)
    36   "|"           :: "[o, o] => o"                (infixr 30)
    37   -->           :: "[o, o] => o"                (infixr 25)
    38   <->           :: "[o, o] => o"                (infixr 25)
    39 
    40   (* Quantifiers *)
    41 
    42   All           :: "('a => o) => o"             (binder "ALL " 10)
    43   Ex            :: "('a => o) => o"             (binder "EX " 10)
    44   Ex1           :: "('a => o) => o"             (binder "EX! " 10)
    45 
    46 
    47 syntax
    48   "_not_equal"  :: "['a, 'a] => o"              (infixl "~=" 50)
    49 translations
    50   "x ~= y"      == "~ (x = y)"
    51 
    52 syntax (xsymbols)
    53   Not           :: "o => o"                     ("\<not> _" [40] 40)
    54   "op &"        :: "[o, o] => o"                (infixr "\<and>" 35)
    55   "op |"        :: "[o, o] => o"                (infixr "\<or>" 30)
    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   "_not_equal"  :: "['a, 'a] => o"              (infixl "\<noteq>" 50)
    60   "op -->"      :: "[o, o] => o"                (infixr "\<longrightarrow>" 25)
    61   "op <->"      :: "[o, o] => o"                (infixr "\<longleftrightarrow>" 25)
    62 
    63 syntax (HTML output)
    64   Not           :: "o => o"                     ("\<not> _" [40] 40)
    65   "op &"        :: "[o, o] => o"                (infixr "\<and>" 35)
    66   "op |"        :: "[o, o] => o"                (infixr "\<or>" 30)
    67   "ALL "        :: "[idts, o] => o"             ("(3\<forall>_./ _)" [0, 10] 10)
    68   "EX "         :: "[idts, o] => o"             ("(3\<exists>_./ _)" [0, 10] 10)
    69   "EX! "        :: "[idts, o] => o"             ("(3\<exists>!_./ _)" [0, 10] 10)
    70   "_not_equal"  :: "['a, 'a] => o"              (infixl "\<noteq>" 50)
    71 
    72 
    73 local
    74 
    75 finalconsts
    76   False All Ex
    77   "op ="
    78   "op &"
    79   "op |"
    80   "op -->"
    81 
    82 axioms
    83 
    84   (* Equality *)
    85 
    86   refl:         "a=a"
    87 
    88   (* Propositional logic *)
    89 
    90   conjI:        "[| P;  Q |] ==> P&Q"
    91   conjunct1:    "P&Q ==> P"
    92   conjunct2:    "P&Q ==> Q"
    93 
    94   disjI1:       "P ==> P|Q"
    95   disjI2:       "Q ==> P|Q"
    96   disjE:        "[| P|Q;  P ==> R;  Q ==> R |] ==> R"
    97 
    98   impI:         "(P ==> Q) ==> P-->Q"
    99   mp:           "[| P-->Q;  P |] ==> Q"
   100 
   101   FalseE:       "False ==> P"
   102 
   103   (* Quantifiers *)
   104 
   105   allI:         "(!!x. P(x)) ==> (ALL x. P(x))"
   106   spec:         "(ALL x. P(x)) ==> P(x)"
   107 
   108   exI:          "P(x) ==> (EX x. P(x))"
   109   exE:          "[| EX x. P(x);  !!x. P(x) ==> R |] ==> R"
   110 
   111   (* Reflection *)
   112 
   113   eq_reflection:  "(x=y)   ==> (x==y)"
   114   iff_reflection: "(P<->Q) ==> (P==Q)"
   115 
   116 
   117 text{*Thanks to Stephan Merz*}
   118 theorem subst:
   119   assumes eq: "a = b" and p: "P(a)"
   120   shows "P(b)"
   121 proof -
   122   from eq have meta: "a \<equiv> b"
   123     by (rule eq_reflection)
   124   from p show ?thesis
   125     by (unfold meta)
   126 qed
   127 
   128 
   129 defs
   130   (* Definitions *)
   131 
   132   True_def:     "True  == False-->False"
   133   not_def:      "~P    == P-->False"
   134   iff_def:      "P<->Q == (P-->Q) & (Q-->P)"
   135 
   136   (* Unique existence *)
   137 
   138   ex1_def:      "Ex1(P) == EX x. P(x) & (ALL y. P(y) --> y=x)"
   139 
   140 
   141 subsection {* Lemmas and proof tools *}
   142 
   143 use "IFOL_lemmas.ML"
   144 
   145 use "fologic.ML"
   146 use "hypsubstdata.ML"
   147 setup hypsubst_setup
   148 use "intprover.ML"
   149 
   150 
   151 subsection {* Intuitionistic Reasoning *}
   152 
   153 lemma impE':
   154   assumes 1: "P --> Q"
   155     and 2: "Q ==> R"
   156     and 3: "P --> Q ==> P"
   157   shows R
   158 proof -
   159   from 3 and 1 have P .
   160   with 1 have Q by (rule impE)
   161   with 2 show R .
   162 qed
   163 
   164 lemma allE':
   165   assumes 1: "ALL x. P(x)"
   166     and 2: "P(x) ==> ALL x. P(x) ==> Q"
   167   shows Q
   168 proof -
   169   from 1 have "P(x)" by (rule spec)
   170   from this and 1 show Q by (rule 2)
   171 qed
   172 
   173 lemma notE':
   174   assumes 1: "~ P"
   175     and 2: "~ P ==> P"
   176   shows R
   177 proof -
   178   from 2 and 1 have P .
   179   with 1 show R by (rule notE)
   180 qed
   181 
   182 lemmas [Pure.elim!] = disjE iffE FalseE conjE exE
   183   and [Pure.intro!] = iffI conjI impI TrueI notI allI refl
   184   and [Pure.elim 2] = allE notE' impE'
   185   and [Pure.intro] = exI disjI2 disjI1
   186 
   187 setup {*
   188   [ContextRules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac)]
   189 *}
   190 
   191 
   192 lemma iff_not_sym: "~ (Q <-> P) ==> ~ (P <-> Q)"
   193   by rules
   194 
   195 lemmas [sym] = sym iff_sym not_sym iff_not_sym
   196   and [Pure.elim?] = iffD1 iffD2 impE
   197 
   198 
   199 lemma eq_commute: "a=b <-> b=a"
   200 apply (rule iffI) 
   201 apply (erule sym)+
   202 done
   203 
   204 
   205 subsection {* Atomizing meta-level rules *}
   206 
   207 lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))"
   208 proof
   209   assume "!!x. P(x)"
   210   show "ALL x. P(x)" ..
   211 next
   212   assume "ALL x. P(x)"
   213   thus "!!x. P(x)" ..
   214 qed
   215 
   216 lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A --> B)"
   217 proof
   218   assume "A ==> B"
   219   thus "A --> B" ..
   220 next
   221   assume "A --> B" and A
   222   thus B by (rule mp)
   223 qed
   224 
   225 lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)"
   226 proof
   227   assume "x == y"
   228   show "x = y" by (unfold prems) (rule refl)
   229 next
   230   assume "x = y"
   231   thus "x == y" by (rule eq_reflection)
   232 qed
   233 
   234 lemma atomize_conj [atomize]:
   235   "(!!C. (A ==> B ==> PROP C) ==> PROP C) == Trueprop (A & B)"
   236 proof
   237   assume "!!C. (A ==> B ==> PROP C) ==> PROP C"
   238   show "A & B" by (rule conjI)
   239 next
   240   fix C
   241   assume "A & B"
   242   assume "A ==> B ==> PROP C"
   243   thus "PROP C"
   244   proof this
   245     show A by (rule conjunct1)
   246     show B by (rule conjunct2)
   247   qed
   248 qed
   249 
   250 lemmas [symmetric, rulify] = atomize_all atomize_imp
   251 
   252 
   253 subsection {* Calculational rules *}
   254 
   255 lemma forw_subst: "a = b ==> P(b) ==> P(a)"
   256   by (rule ssubst)
   257 
   258 lemma back_subst: "P(a) ==> a = b ==> P(b)"
   259   by (rule subst)
   260 
   261 text {*
   262   Note that this list of rules is in reverse order of priorities.
   263 *}
   264 
   265 lemmas basic_trans_rules [trans] =
   266   forw_subst
   267   back_subst
   268   rev_mp
   269   mp
   270   trans
   271 
   272 subsection {* ``Let'' declarations *}
   273 
   274 nonterminals letbinds letbind
   275 
   276 constdefs
   277   Let :: "['a::{}, 'a => 'b] => ('b::{})"
   278     "Let(s, f) == f(s)"
   279 
   280 syntax
   281   "_bind"       :: "[pttrn, 'a] => letbind"           ("(2_ =/ _)" 10)
   282   ""            :: "letbind => letbinds"              ("_")
   283   "_binds"      :: "[letbind, letbinds] => letbinds"  ("_;/ _")
   284   "_Let"        :: "[letbinds, 'a] => 'a"             ("(let (_)/ in (_))" 10)
   285 
   286 translations
   287   "_Let(_binds(b, bs), e)"  == "_Let(b, _Let(bs, e))"
   288   "let x = a in e"          == "Let(a, %x. e)"
   289 
   290 
   291 lemma LetI: 
   292     assumes prem: "(!!x. x=t ==> P(u(x)))"
   293     shows "P(let x=t in u(x))"
   294 apply (unfold Let_def)
   295 apply (rule refl [THEN prem])
   296 done
   297 
   298 ML
   299 {*
   300 val Let_def = thm "Let_def";
   301 val LetI = thm "LetI";
   302 *}
   303 
   304 end