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