src/FOL/IFOL.thy
author paulson
Tue Feb 01 18:01:57 2005 +0100 (2005-02-01)
changeset 15481 fc075ae929e4
parent 15377 3d99eea28a9b
child 16019 0e1405402d53
permissions -rw-r--r--
the new subst tactic, by Lucas Dixon
     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 files ("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 setup Simplifier.setup
   144 use "IFOL_lemmas.ML"
   145 
   146 use "fologic.ML"
   147 use "hypsubstdata.ML"
   148 setup hypsubst_setup
   149 use "intprover.ML"
   150 
   151 
   152 subsection {* Intuitionistic Reasoning *}
   153 
   154 lemma impE':
   155   assumes 1: "P --> Q"
   156     and 2: "Q ==> R"
   157     and 3: "P --> Q ==> P"
   158   shows R
   159 proof -
   160   from 3 and 1 have P .
   161   with 1 have Q by (rule impE)
   162   with 2 show R .
   163 qed
   164 
   165 lemma allE':
   166   assumes 1: "ALL x. P(x)"
   167     and 2: "P(x) ==> ALL x. P(x) ==> Q"
   168   shows Q
   169 proof -
   170   from 1 have "P(x)" by (rule spec)
   171   from this and 1 show Q by (rule 2)
   172 qed
   173 
   174 lemma notE':
   175   assumes 1: "~ P"
   176     and 2: "~ P ==> P"
   177   shows R
   178 proof -
   179   from 2 and 1 have P .
   180   with 1 show R by (rule notE)
   181 qed
   182 
   183 lemmas [Pure.elim!] = disjE iffE FalseE conjE exE
   184   and [Pure.intro!] = iffI conjI impI TrueI notI allI refl
   185   and [Pure.elim 2] = allE notE' impE'
   186   and [Pure.intro] = exI disjI2 disjI1
   187 
   188 ML_setup {*
   189   Context.>> (ContextRules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac));
   190 *}
   191 
   192 
   193 lemma iff_not_sym: "~ (Q <-> P) ==> ~ (P <-> Q)"
   194   by rules
   195 
   196 lemmas [sym] = sym iff_sym not_sym iff_not_sym
   197   and [Pure.elim?] = iffD1 iffD2 impE
   198 
   199 
   200 lemma eq_commute: "a=b <-> b=a"
   201 apply (rule iffI) 
   202 apply (erule sym)+
   203 done
   204 
   205 
   206 subsection {* Atomizing meta-level rules *}
   207 
   208 lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))"
   209 proof
   210   assume "!!x. P(x)"
   211   show "ALL x. P(x)" ..
   212 next
   213   assume "ALL x. P(x)"
   214   thus "!!x. P(x)" ..
   215 qed
   216 
   217 lemma atomize_imp [atomize]: "(A ==> B) == Trueprop (A --> B)"
   218 proof
   219   assume "A ==> B"
   220   thus "A --> B" ..
   221 next
   222   assume "A --> B" and A
   223   thus B by (rule mp)
   224 qed
   225 
   226 lemma atomize_eq [atomize]: "(x == y) == Trueprop (x = y)"
   227 proof
   228   assume "x == y"
   229   show "x = y" by (unfold prems) (rule refl)
   230 next
   231   assume "x = y"
   232   thus "x == y" by (rule eq_reflection)
   233 qed
   234 
   235 lemma atomize_conj [atomize]:
   236   "(!!C. (A ==> B ==> PROP C) ==> PROP C) == Trueprop (A & B)"
   237 proof
   238   assume "!!C. (A ==> B ==> PROP C) ==> PROP C"
   239   show "A & B" by (rule conjI)
   240 next
   241   fix C
   242   assume "A & B"
   243   assume "A ==> B ==> PROP C"
   244   thus "PROP C"
   245   proof this
   246     show A by (rule conjunct1)
   247     show B by (rule conjunct2)
   248   qed
   249 qed
   250 
   251 lemmas [symmetric, rulify] = atomize_all atomize_imp
   252 
   253 
   254 subsection {* Calculational rules *}
   255 
   256 lemma forw_subst: "a = b ==> P(b) ==> P(a)"
   257   by (rule ssubst)
   258 
   259 lemma back_subst: "P(a) ==> a = b ==> P(b)"
   260   by (rule subst)
   261 
   262 text {*
   263   Note that this list of rules is in reverse order of priorities.
   264 *}
   265 
   266 lemmas basic_trans_rules [trans] =
   267   forw_subst
   268   back_subst
   269   rev_mp
   270   mp
   271   trans
   272 
   273 subsection {* ``Let'' declarations *}
   274 
   275 nonterminals letbinds letbind
   276 
   277 constdefs
   278   Let :: "['a::{}, 'a => 'b] => ('b::{})"
   279     "Let(s, f) == f(s)"
   280 
   281 syntax
   282   "_bind"       :: "[pttrn, 'a] => letbind"           ("(2_ =/ _)" 10)
   283   ""            :: "letbind => letbinds"              ("_")
   284   "_binds"      :: "[letbind, letbinds] => letbinds"  ("_;/ _")
   285   "_Let"        :: "[letbinds, 'a] => 'a"             ("(let (_)/ in (_))" 10)
   286 
   287 translations
   288   "_Let(_binds(b, bs), e)"  == "_Let(b, _Let(bs, e))"
   289   "let x = a in e"          == "Let(a, %x. e)"
   290 
   291 
   292 lemma LetI: 
   293     assumes prem: "(!!x. x=t ==> P(u(x)))"
   294     shows "P(let x=t in u(x))"
   295 apply (unfold Let_def)
   296 apply (rule refl [THEN prem])
   297 done
   298 
   299 ML
   300 {*
   301 val Let_def = thm "Let_def";
   302 val LetI = thm "LetI";
   303 *}
   304 
   305 end