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